Mercurial > urweb

comparison src/termination.sml @ 314:a07f476d9b61

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
313:e0ed0d4dabc9 314:a07f476d9b61
124 124
125 fun apps () = 125 fun apps () =
126 let 126 let
127 fun combiner calls e = 127 fun combiner calls e =
128 case #1 e of 128 case #1 e of
129 EApp (e1, e2) => 129 EApp ((ECApp (
130 (ECApp (
131 (ECApp (
132 (ECApp (
133 (ECApp (
134 (ECApp (
135 (ECApp (
136 (ECApp (
137 (EModProj (m, [], "tag"), _),
138 _), _),
139 _), _),
140 _), _),
141 _), _),
142 _), _),
143 _), _),
144 _), _),
145 _), _),
146 (ERecord xets, _)) =>
147 let
148 val checkName =
149 case E.lookupStrNamed env m of
150 ("Basis", _) => (fn x : con => case #1 x of
151 CName s => s = "Link"
152 orelse s = "Action"
153 | _ => false)
154 | _ => (fn _ => false)
155
156 val calls = foldl (fn ((x, e, _), calls) =>
157 if checkName x then
158 calls
159 else
160 #2 (exp (penv, calls) e)) calls xets
161 in
162 (Rabble, [Rabble], calls)
163 end
164
165 | EApp (e1, e2) =>
130 let 166 let
131 val (p1, ps, calls) = combiner calls e1 167 val (p1, ps, calls) = combiner calls e1
132 val (p2, calls) = exp (penv, calls) e2 168 val (p2, calls) = exp (penv, calls) e2
133 169
134 val p = case p1 of 170 val p = case p1 of
185 | SOME n' => Func n' 221 | SOME n' => Func n'
186 in 222 in
187 (p, calls) 223 (p, calls)
188 end 224 end
189 | EModProj _ => default 225 | EModProj _ => default
226
190 | EApp _ => apps () 227 | EApp _ => apps ()
191 | EAbs (_, _, _, e) => 228 | EAbs (_, _, _, e) =>
192 let 229 let
193 val (_, calls) = exp (Rabble :: penv, calls) e 230 val (_, calls) = exp (Rabble :: penv, calls) e
194 in 231 in