aboutsummaryrefslogtreecommitdiff
path: root/sucl/pfun.dcl
blob: 49db62de6b6922255105c6faac8c9eb86fc2965c (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
definition module pfun

// $Id$

from StdString import toString
from StdOverloaded import ==

// Partial function abstract type
:: Pfun dom ran

// The empty partial function
emptypfun :: .Pfun .dom .ran

// Extend a partial function
extend :: .dom .ran (Pfun .dom .ran) -> Pfun .dom .ran

// Restrict a partial function (take away one mapping)
restrict :: .dom (Pfun .dom .ran) -> Pfun .dom .ran

// Overwrite partial function with a new one
// first arg is the new p.f.
// second arg is overwritten
overwrite :: !(Pfun .dom .ran) (Pfun .dom .ran) -> (Pfun .dom .ran)

// Modify a partial function by applying a function to all its results
postcomp :: (.ran1 -> .ran2) !(Pfun .dom .ran1) -> Pfun .dom .ran2

// Build a total function from a partial one by supplying a default value
total :: .ran !(Pfun dom .ran) dom -> .ran | == dom

// Domain restriction of a partial function
domres :: !.[dom] .(Pfun dom ran) -> Pfun dom ran | == dom

// Apply a partial function to an argument
// getting a result that may fail
apply :: !(Pfun dom .ran) dom -> (.Bool,.ran) | == dom

// Partial functions are printable
instance toString Pfun dom ran | toString dom & toString ran

/* `Idpfun dom pfun' checks whether partial function `pfun' is the identity
   on the nodes in `dom' for which it is defined.
*/
idpfun :: !.[dom] .(Pfun dom dom) -> Bool | == dom