Mercurial > urweb

comparison src/iflow.sml @ 1235:a7b773f1d053

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Command-line use of Iflow
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 11:34:59 -0400
parents e799c8df3146
children d5ecceb7d1a1
comparison
equal deleted inserted replaced
1234:e799c8df3146 1235:a7b773f1d053
500 500
501 fun p_rep n = 501 fun p_rep n =
502 case !(#Rep (unNode n)) of 502 case !(#Rep (unNode n)) of
503 SOME n => p_rep n 503 SOME n => p_rep n
504 | NONE => 504 | NONE =>
505 box [string (Int.toString (Unsafe.cast n) ^ ":"), 505 box [string (Int.toString 0(*Unsafe.cast n*) ^ ":"),
506 space, 506 space,
507 case #Variety (unNode n) of 507 case #Variety (unNode n) of
508 Nothing => string "?" 508 Nothing => string "?"
509 | Dt0 s => string ("Dt0(" ^ s ^ ")") 509 | Dt0 s => string ("Dt0(" ^ s ^ ")")
510 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","), 510 | Dt1 (s, n) => box[string ("Dt1(" ^ s ^ ","),
2180 val (es, st) = ListUtil.foldlMap (evalExp env) st es 2180 val (es, st) = ListUtil.foldlMap (evalExp env) st es
2181 in 2181 in
2182 (Func (Other ("Cl" ^ Int.toString n), es), st) 2182 (Func (Other ("Cl" ^ Int.toString n), es), st)
2183 end 2183 end
2184 2184
2185 | EQuery {query = q, body = b, initial = i, ...} => 2185 | EQuery {query = q, body = b, initial = i, state = state, ...} =>
2186 let 2186 let
2187 val (_, st) = evalExp env (q, st) 2187 val (_, st) = evalExp env (q, st)
2188 val (i, st) = evalExp env (i, st) 2188 val (i, st) = evalExp env (i, st)
2189 2189
2190 val (st', r) = St.nextVar st 2190 val (st', r) = St.nextVar st
2201 in 2201 in
2202 (st', Var rv) 2202 (st', Var rv)
2203 end) 2203 end)
2204 (AllCols (Var r)) q 2204 (AllCols (Var r)) q
2205 2205
2206 val (st, res) = if varInP acc (St.ambient st') then 2206 val (st, res) =
2207 let 2207 case #1 state of
2208 val (st, r) = St.nextVar st 2208 TRecord [] =>
2209 in 2209 (st, Func (DtCon0 "unit", []))
2210 (st, Var r) 2210 | _ =>
2211 end 2211 if varInP acc (St.ambient st') then
2212 else 2212 let
2213 let 2213 val (st, r) = St.nextVar st
2214 val (st', out) = St.nextVar st' 2214 in
2215 2215 (st, Var r)
2216 val p = And (St.ambient st, 2216 end
2217 Or (Reln (Eq, [Var out, i]), 2217 else
2218 And (Reln (Eq, [Var out, b]), 2218 let
2219 And (qp, amb)))) 2219 val (st', out) = St.nextVar st'
2220 in 2220
2221 (St.setAmbient (st', p), Var out) 2221 val p = And (St.ambient st,
2222 end 2222 Or (Reln (Eq, [Var out, i]),
2223 And (Reln (Eq, [Var out, b]),
2224 And (qp, amb))))
2225 in
2226 (St.setAmbient (st', p), Var out)
2227 end
2223 2228
2224 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st') 2229 val sent = map (fn ((loc, e, p), fl) => ((loc, e, And (qp, p)), fl)) (St.sent st')
2225 2230
2226 val p' = And (qp, St.ambient st') 2231 val p' = And (qp, St.ambient st')
2227 val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used 2232 val paths = map (fn (p'', e) => ((loc, e, And (p', p'')), Where)) used