Mercurial > urweb
diff src/termination.sml @ 314:a07f476d9b61
Termination checking allows anything in links and actions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 09 Sep 2008 12:36:13 -0400 |
parents | e0ed0d4dabc9 |
children | 075b36dbb1a4 |
line wrap: on
line diff
--- a/src/termination.sml Tue Sep 09 11:46:33 2008 -0400 +++ b/src/termination.sml Tue Sep 09 12:36:13 2008 -0400 @@ -126,7 +126,43 @@ let fun combiner calls e = case #1 e of - EApp (e1, e2) => + EApp ((ECApp ( + (ECApp ( + (ECApp ( + (ECApp ( + (ECApp ( + (ECApp ( + (ECApp ( + (ECApp ( + (EModProj (m, [], "tag"), _), + _), _), + _), _), + _), _), + _), _), + _), _), + _), _), + _), _), + _), _), + (ERecord xets, _)) => + let + val checkName = + case E.lookupStrNamed env m of + ("Basis", _) => (fn x : con => case #1 x of + CName s => s = "Link" + orelse s = "Action" + | _ => false) + | _ => (fn _ => false) + + val calls = foldl (fn ((x, e, _), calls) => + if checkName x then + calls + else + #2 (exp (penv, calls) e)) calls xets + in + (Rabble, [Rabble], calls) + end + + | EApp (e1, e2) => let val (p1, ps, calls) = combiner calls e1 val (p2, calls) = exp (penv, calls) e2 @@ -187,6 +223,7 @@ (p, calls) end | EModProj _ => default + | EApp _ => apps () | EAbs (_, _, _, e) => let