diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-09-09 12:36:13 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-09-09 12:36:13 -0400 |
| commit | 9e804908dd69043c8a9942cdf6042b8dc0d76175 (patch) | |
| tree | 4437f1d468859452358a91bf5ba7071b11a1a419 | |
| parent | 4960cd8c2ec1e02c90e42d16db13f045427b4173 (diff) | |
Termination checking allows anything in links and actions
| -rw-r--r-- | src/cjr_print.sml | 2 | ||||
| -rw-r--r-- | src/monoize.sml | 2 | ||||
| -rw-r--r-- | src/termination.sml | 39 | ||||
| -rw-r--r-- | tests/rec.ur | 3 | ||||
| -rw-r--r-- | tests/rec.urp | 5 |
5 files changed, 48 insertions, 3 deletions
diff --git a/src/cjr_print.sml b/src/cjr_print.sml index b5d8806a..e2bc37fa 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -1529,7 +1529,7 @@ fun p_file env (ds, ps) = let val (ts, defInputs, inputsVar) = case ek of - Core.Link => (ts, string "", string "") + Core.Link => (List.take (ts, length ts - 1), string "", string "") | Core.Action => case List.nth (ts, length ts - 2) of (TRecord i, _) => diff --git a/src/monoize.sml b/src/monoize.sml index e7e28ef0..472e04cb 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -1594,6 +1594,8 @@ fun monoDecl (env, fm) (all as (d, loc)) = fun unwind (t, _) = case t of L.TFun (dom, ran) => dom :: unwind ran + | L.CApp ((L.CFfi ("Basis", "transaction"), _), t) => + (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc) :: unwind t | _ => [] val ts = map (monoType env) (unwind t) diff --git a/src/termination.sml b/src/termination.sml index 18ff0785..65c770df 100644 --- a/src/termination.sml +++ b/src/termination.sml @@ -126,7 +126,43 @@ fun declOk' env (d, loc) = 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 @@ fun declOk' env (d, loc) = (p, calls) end | EModProj _ => default + | EApp _ => apps () | EAbs (_, _, _, e) => let diff --git a/tests/rec.ur b/tests/rec.ur index 6131337e..0a0c7445 100644 --- a/tests/rec.ur +++ b/tests/rec.ur @@ -1,3 +1,4 @@ -val rec main = fn () => <html><body> + +fun main () : transaction page = return <html><body> <a link={main ()}>Ride again!</a> </body></html> diff --git a/tests/rec.urp b/tests/rec.urp new file mode 100644 index 00000000..8c3adc2c --- /dev/null +++ b/tests/rec.urp @@ -0,0 +1,5 @@ +debug +database dbname=test +exe /tmp/webapp + +rec |