aboutsummaryrefslogtreecommitdiff
path: root/sucl/pfun.icl
diff options
context:
space:
mode:
Diffstat (limited to 'sucl/pfun.icl')
-rw-r--r--sucl/pfun.icl77
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