diff options
Diffstat (limited to 'sucl/pfun.icl')
-rw-r--r-- | sucl/pfun.icl | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/sucl/pfun.icl b/sucl/pfun.icl new file mode 100644 index 0000000..f720f51 --- /dev/null +++ b/sucl/pfun.icl @@ -0,0 +1,77 @@ +implementation module pfun + +import basic +import StdEnv + +/* + +pfun.lit - Partial functions +============================ + +Description +----------- + +This script implements an abstract type for partial functions and useful +operations on them. + +Implementation +-------------- + +*/ + +:: Pfun dom ran + = EmptyPfun + | Extend dom ran (Pfun dom ran) + | Restrict dom (Pfun dom ran) + +emptypfun :: .Pfun .dom .ran +emptypfun = EmptyPfun + +extend :: .dom .ran (Pfun .dom .ran) -> Pfun .dom .ran +extend arg res pfun = Extend arg res pfun + +restrict :: .dom (Pfun .dom .ran) -> Pfun .dom .ran +restrict arg pfun = Restrict arg pfun + +overwrite :: !(Pfun .dom .ran) (Pfun .dom .ran) -> (Pfun .dom .ran) +overwrite EmptyPfun old = old +overwrite (Extend org img new) old = Extend org img (overwrite new old) +overwrite (Restrict org new) old = Restrict org (overwrite new old) + +postcomp :: (.ran1 -> .ran2) !(Pfun .dom .ran1) -> Pfun .dom .ran2 +postcomp f EmptyPfun = EmptyPfun +postcomp f (Extend x y p) = Extend x (f y) (postcomp f p) +postcomp f (Restrict x p) = Restrict x (postcomp f p) + +total :: .ran !(Pfun dom .ran) dom -> .ran | == dom +total def EmptyPfun arg = def +total def (Extend x y p) arg +| arg==x = y + = total def p arg +total def (Restrict x p) arg +| arg==x = def + = total def p arg + +domres :: !.[dom] .(Pfun dom ran) -> Pfun dom ran | == dom +domres domain oldpfun += foldr adddom emptypfun domain + where adddom org = total id (postcomp (extend org) oldpfun) org + +apply :: !(Pfun dom .ran) dom -> (.Bool,.ran) | == dom +apply pfun arg += total (False,baddomain) (postcomp s pfun) arg + where s x = (True,x) + baddomain = abort "apply: partial function applied outside domain" + +instance toString Pfun dom ran | toString dom & toString ran +where toString pfun + = toString ['{':drop 1 (flatten (map ((cons ',') o printlink) (pfunlist pfun)))++['}']] + where printlink (arg,res) = fromString (toString arg)++['|->']++fromString (toString res) + +pfunlist :: (Pfun dom res) -> [(dom,res)] +pfunlist _ = abort "pfunlist not implemented" + +idpfun :: !.[dom] .(Pfun dom dom) -> Bool | == dom +idpfun domain pfun += all idelem domain + where idelem x = total True (postcomp ((==) x) pfun) x |