Helper.hs revision 31d6d9286988dc31639d105841296759aeb743e0
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerModule : $Header$
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederDescription : Helper functions for dealing with terms (mainly for pretty printing which is directly adapted from hollight)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : jonathan.von_schroeder@dfki.de
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerStability : experimental
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport Data.Maybe (fromJust,isJust,maybe,catMaybes)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerimport List (union,(\\))
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerfromRight e = case e of
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner Right t -> t
d23ecf32e56cce69bc42eb5c96dddf7909c623abjelmd Left _ -> error "fromRight"
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkneris_prefix tm = case tm of
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner Var _ _ Prefix -> True
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner Const _ _ Prefix -> True
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerpp_print_type = sot 0
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknersoc sep flag ss = if length ss == 0 then empty
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner else let s = foldr1 (\s1 s2 -> hcat[s1,text sep,s2]) ss
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner in if flag then parens s else s
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknersot pr ty = case (dest_vartype ty,dest_type ty) of {- exactly one of these is not Nothing-}
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner (Just vtype,_) -> text vtype
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner (_,Just t) -> case t of
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa (con,[]) -> text con
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa ("fun",[ty1,ty2]) -> soc "->" (pr > 0) [sot 1 ty1,sot 0 ty2]
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa ("sum",[ty1,ty2]) -> soc "+" (pr > 2) [sot 3 ty1,sot 2 ty2]
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa ("prod",[ty1,ty2]) -> soc "#" (pr > 4) [sot 5 ty1,sot 4 ty2]
ab4256496e72886018b78571057331f373da6883Eugen Kuksa ("cart",[ty1,ty2]) -> soc "^" (pr > 6) [sot 6 ty1,sot 7 ty2]
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa (con,args) -> hcat [soc "," True (map (sot 0) args),text con]
f8597aabc9db75dcf504e3151faf220a165c90d1Eugen Kuksa _ -> empty {- doesn't happen -}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksarev_assocd a l d = case l of
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa (x,y):t -> if y == a then x
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner else rev_assocd a t d
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerdest_var v = case v of
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa Var s ty _ -> Just (s,ty)
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa _ -> Nothing
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkneris_var v = isJust (dest_var v)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerfrees tm = case tm of
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner Var _ _ _ -> [tm]
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner Const _ _ _ -> []
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner Abs bv bod -> (frees bod) \\ [bv]
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner Comb s t -> union (frees s) (frees t)
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maedervfree_in v tm = case tm of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Abs bv bod -> v /= bv && vfree_in v bod
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Comb s t -> vfree_in v s || vfree_in v t
c0c2380bced8159ff0297ece14eba948bd236471Christian Maedervariant avoid v = if not (any (vfree_in v) avoid) then Just v
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich else case v of
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder Var s ty p -> variant avoid (Var (s++"'") ty p)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let vsubst' ilist tm = case tm of
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder Var _ _ _ -> Just $ rev_assocd tm ilist tm
ce5b44277ea06257548ff625e928cb1290c6d297cmaeder Const _ _ _ -> Just tm
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder Comb s t -> case (vsubst' ilist s,vsubst ilist t) of
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder (Just s',Just t') -> if (s'==s && t'==t)
ce5b44277ea06257548ff625e928cb1290c6d297cmaeder then Just tm
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else Just (Comb s' t')
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Abs v s -> let ilist' = filter (\ (t,x) -> x /= v)
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder in if ilist' == [] then Just tm
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder else case vsubst ilist' s of
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder Just s' -> if s' == s
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder else if any (\ (t,x) -> vfree_in v t
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder && vfree_in x s)
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder then case variant [s'] v of
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder Just v' -> case vsubst
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder ((v',v):ilist') s of
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder Just t' -> Just (Abs v' t')
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder else Just (Abs v s')
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder in \ theta ->
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder if theta == [] then (\ tm -> Just tm) else
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder if all (\ (t,x) -> case (type_of t, dest_var x) of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (Just t',Just (_,x')) -> t' == x'
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder _ -> False) theta then vsubst theta
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder else (\ _ -> Nothing)
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maederdest_comb c = case c of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Comb f x -> Just (f,x)
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maederis_comb c = isJust (dest_comb c)
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maederdest_const c = case c of
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich Const s ty _ -> Just (s,ty)
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maederis_const c = isJust (dest_const c)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederdest_abs a = case a of
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian Maeder Abs v b -> Just (v,b)
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederis_abs a = isJust (dest_abs a)
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederrator tm = maybe Nothing (Just . fst) (dest_comb tm)
961087225d1d2b9534152a346d1a3755ed952fcdJens Elknerrand tm = maybe Nothing (Just . snd) (dest_comb tm)
961087225d1d2b9534152a346d1a3755ed952fcdJens Elknersplitlist dest x = case dest x of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just (l,r) -> let (ls,res) = splitlist dest r
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in (l:ls,res)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederrev_splitlist dest x =
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder let rsplist ls x' = case dest x' of
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner Just (l,r) -> rsplist (r:ls) l
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner _ -> (x',ls)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder in rsplist [] x
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maedertype_of tm = case tm of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Var _ ty _ -> Just ty
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Const _ ty _ -> Just ty
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Comb s _ -> case type_of s of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Just t -> case dest_type t of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Just (_,x:x1:xs) -> Just x1
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Abs (Var _ ty _) t -> case type_of t of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Just t' -> Just (TyApp "fun" [ty,t'])
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maederdest_type a = case a of
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder TyApp s ty -> Just (s,ty)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maederdest_vartype t = case t of
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder TyVar s -> Just s
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner _ -> Nothing
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedertype_subst i ty = case ty of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder TyApp tycon args -> let args' = map (type_subst i) args
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder in if args' == args then ty else TyApp tycon args'
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner _ -> rev_assocd ty i ty
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedermk_eq (l,r) = case (type_of l,mk_const ("=",[])) of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (Just ty,Just eq) -> case inst [(ty,TyVar "A")] eq of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Right eq_tm -> case mk_comb (eq_tm,l) of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just m1 -> mk_comb (m1,r)
8037b7d21021a94b69e4a092f5c98e491333d939cmaeder _ -> Nothing
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner _ -> Nothing
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder let inst' env tyin tm = case tm of
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Var n ty at -> let ty' = type_subst tyin ty
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder in let tm' = if ty' == ty then tm
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner else (Var n ty' at)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder in if (rev_assocd tm' env tm) == tm
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner then Right tm'
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder else Left tm'
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner Const c ty at -> let ty' = type_subst tyin ty
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in if ty' == ty
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder then Right tm
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder else Right (Const c ty' at)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Comb f x -> case (inst' env tyin f,
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder inst' env tyin x) of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder (Right f',Right x') -> if f' == f
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder && x' == x then Right tm
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder else Right (Comb f' x')
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder (Left c, _) -> Left c
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder (_,Left c) -> Left c
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett Abs y t -> case inst' [] tyin y of
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder Right y' -> let env' = (y,y'):env
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder in case inst' env' tyin t of
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder Right t' -> if y' == y &&
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder then Right tm
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers else Right (Abs y' t')
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Left w' -> if w' /= y'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else let ifrees = map (fromRight .
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (inst' [] tyin))
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder case variant ifrees y' of
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder case (dest_var y'',dest_var y) of
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder (Just (v1,_),Just (_,v2)) ->
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers let z = (Var v1 v2 Normal)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in case vsubst [(z,y)] t of
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Just s -> inst' env tyin
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder in (\tyin -> if tyin == [] then (\tm -> Right tm) else inst' [] tyin)
3554301a34639efb6c9961a8571775d0061284c9Christian Maedermk_comb (f,a) = case type_of f of
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder Just (TyApp "fun" [ty,_]) -> case type_of a of
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Just t -> if ty == t then Just (Comb f a) else Nothing
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maedereq_type = TyApp "fun" [
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder TyApp "fun" [
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder TyApp "bool" []
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maedermk_const (name,theta) = if name == "="
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder then Just (Const name
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder (type_subst theta eq_type)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederdest_binder s tm = case tm of
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder Comb (Const s' _ _) (Abs x t) ->
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder if (s'==s) then Just (x,t)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maederdest_exists = dest_binder "?"
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maederstrip_exists = splitlist dest_exists
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maederdest_forall = dest_binder "!"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederstrip_forall = splitlist dest_forall
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederstrip_comb = rev_splitlist dest_comb
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maederbody tm = case dest_abs tm of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just (_,ret) -> Just ret
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederdest_numeral tm =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let dest_num tm = case dest_const tm of
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder Just ("_0",_) -> Just (toInteger 0)
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder _ -> case dest_comb tm of
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder Just (l,r) -> case dest_num r of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder let n = (toInteger 2) * i
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder in case dest_const l of
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder Just ("BIT0",_) -> Just n
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder Just ("BIT1",_) -> Just (n
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder + (toInteger 1))
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder in case dest_comb tm of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Just (l,r) -> case dest_const l of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just ("NUMERAL",_) -> dest_num r
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reillydest_binary' s tm = case tm of
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Comb (Comb (Const s' _ _) l) r -> if s' == s then Just (l,r)
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maederdest_cons = dest_binary' "CONS"
31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroederdest_list tm = let (tms,nil) = splitlist dest_cons tm
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu in case dest_const nil of
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder Just ("NIL",_) -> Just tms
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke let dest_geq = dest_binary' "GEQ"
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke in if is_abs tm then dest_abs tm
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else case dest_comb tm of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Just (l,r) -> case dest_const l of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Just ("GABS",_) -> case body r of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Just b -> case dest_geq(snd(strip_forall b)) of
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder Just (ltm,rtm) -> case rand ltm of
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder Just r -> Just (r,rtm)
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maederis_gabs tm = isJust (dest_gabs tm)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederstrip_gabs = splitlist dest_gabs
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichdest_fun_ty ty = case ty of
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder TyApp "fun" [ty1,ty2] -> Just (ty1,ty2)
dd6f22b9dcff2695181b86372e4df03d5b96e92dKristina Sojakovadest_let tm = let (l,aargs) = strip_comb tm
005e0f0c6b0cc898003b03801158c208f3071fc5Kristina Sojakova in case dest_const l of
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich Just ("LET",_) ->
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder let (vars,lebod) = strip_gabs (head aargs)
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder in let eqs = zip vars (tail aargs)
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder in case dest_comb lebod of
76b9b2974795a6fb31f242fd032de3ff66df6204Christian Maeder Just (le,bod) -> case dest_const le of
74a992bd019d3319df2f21f9d358ff06cafb5f7eMihaela Turcu Just ("LET_END",_) -> Just (eqs,bod)
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksaname_of tm = case tm of
48aa0645e25883048369afc02aac3f49b14a50daChristian Maeder Var x ty _ -> x
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder Const x ty _ -> x
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder{- printer.ml - pp_print_term -}
3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroederreverse_interface (s0,_) = s0
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulzdest_binary c tm = case (dest_comb tm) of {- original name: DEST_BINARY -}
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz Just (il,r) -> case (dest_comb il) of
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance Just (i,l) -> if (i == c) ||
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder (is_const i && is_const c &&
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (reverse_interface(fromJust(dest_const i))
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian Maeder == reverse_interface(fromJust(dest_const c))))
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance then Just (l,r)
d62661e54e2662d53b583ae48609f5037701078dcmaederpowerof10 n = (10*(div n 10)) == n
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksabool_of_term t = case t of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa Const "T" _ _ -> Just True
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Const "F" _ _ -> Just False
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maedercode_of_term t =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder let (f,tms) = strip_comb t in
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder if not(is_const f && fst(fromJust(dest_const f)) == "ASCII")
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder || not(length tms == 8)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder else let bools = map bool_of_term (reverse tms)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in if length (filter ((==)Nothing) bools) == 0 then
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder Just (foldr (\b f -> if b then 1 + 2 * f else 2 * f)
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder 0 (catMaybes bools))
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescurand_rator v = case rator v of
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu Just v1 -> rand v1
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdest_clause tm = case maybe Nothing (Just . strip_exists)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (maybe Nothing body (body tm)) of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Just (_,pbod) -> let (s,args) = strip_comb pbod
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in case (name_of s,length args) of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder ("_UNGUARDED_PATTERN",2) ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder case (rand_rator (args!!0),
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder rand_rator (args!!1)) of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (Just _1,Just _2) -> Just [_1,_2]
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder ("_GUARDED_PATTERN",3) ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder case (rand_rator (args!!0),
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder rand_rator (args!!2)) of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder (Just _1, Just _3) -> Just [_1,args!!1,_3]
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdest_clauses tm = let (s,args) = strip_comb tm
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in if name_of s == "_SEQPATTERN" && length args == 2
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder then case dest_clauses (args!!1) of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Just cs -> case (dest_clause (args!!0)) of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Just c -> Just (c:cs)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder else case dest_clause tm of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Just c -> Just [c]
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederaright tm = case tm of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Var _ _ (InfixR _) -> True
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Const _ _ (InfixR _) -> True
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederget_prec tm = case tm of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Var _ _ (InfixR i) -> i
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Const _ _ (InfixR i) -> i
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederparses_as_binder tm = case tm of
5199920ca3b698b2149c8cb9d2ce2e98a280ff9dChristian Maeder Var _ _ Binder -> True
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Const _ _ Binder -> True
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maedercan_get_infix_status tm = case tm of
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova Var _ _ (InfixR _) -> True
48aa0645e25883048369afc02aac3f49b14a50daChristian Maeder Var _ _ (InfixL _) -> True
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova Const _ _ (InfixR _) -> True
79834070d6d3c63a098e570b12fa3405c607dc70Kristina Sojakova Const _ _ (InfixL _) -> True