Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1251:70092a661f70

Basic handling of recursive functions in Iflow

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 01 May 2010 09:51:46 -0400
parents	e80582b927f2
children	2e4159a7d2d3

comparison

equal deleted inserted replaced

-:e80582b927f2
+:70092a661f70
 val update : ErrorMsg.span -> unit
 val havocReln : reln -> unit
 val havocCookie : string -> unit
+val check : atom -> bool
 val debug : unit -> unit
 end = struct
 val hnames = ref 1
 in
 hnames := n + 1;
 hyps := (n, List.filter (fn AReln (Eq, [_, Func (Other f, [])]) => f <> cname | _ => true) hs, ref false)
 end
+fun check a = Cc.check (db, a)
 fun debug () =
 let
 val (_, hs, _) = !hyps
 in
 Print.preface ("Hyps", Print.p_list p_atom hs)
 ERel n => SOME (List.nth (env, n))
 | EField (e, f) =>
 (case deinj env e of
 NONE => NONE
 | SOME e => SOME (Proj (e, f)))
+| EApp ((EFfi mf, _), e) =>
+if Settings.isEffectful mf orelse Settings.isBenignEffectful mf then
+NONE
+else (case deinj env e of
+NONE => NONE
+| SOME e => SOME (Func (Other (#1 mf ^ "." ^ #2 mf), [e])))
 | _ => NONE
 fun expIn rv env rvOf =
 let
 fun expIn e =
 in
 St.assert [AReln (PCon1 "Some", [e])];
 env
 end
+datatype arg_mode = Fixed | Decreasing | Arbitrary
+type rfun = {args : arg_mode list, tables : SS.set, cookies : SS.set, body : Mono.exp}
+val rfuns = ref (IM.empty : rfun IM.map)
 fun evalExp env (e as (_, loc)) k =
 let
 (*val () = St.debug ()*)
 (*val () = Print.preface ("evalExp", MonoPrint.p_exp MonoEnv.empty e)*)
 k e
 end
 | EFfiApp x => doFfi x
 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
-| EApp (e1, e2) => evalExp env e1 (fn _ => evalExp env e2 (fn _ => default ()))
+| EApp (e1 as (EError _, _), _) => evalExp env e1 k
+| EApp (e1, e2) =>
+let
+fun adefault () = (ErrorMsg.errorAt loc "Excessively fancy function call";
+Print.preface ("Call", MonoPrint.p_exp MonoEnv.empty e);
+default ())
+fun doArgs (e, args) =
+case #1 e of
+EApp (e1, e2) => doArgs (e1, e2 :: args)
+| ENamed n =>
+(case IM.find (!rfuns, n) of
+NONE => adefault ()
+| SOME rf =>
+if length (#args rf) <> length args then
+adefault ()
+else
+let
+val () = (SS.app (St.havocReln o Sql) (#tables rf);
+SS.app St.havocCookie (#cookies rf))
+val saved = St.stash ()
+fun doArgs (args, modes, env') =
+case (args, modes) of
+([], []) => (evalExp env' (#body rf) (fn _ => ());
+St.reinstate saved;
+default ())
+| (arg :: args, mode :: modes) =>
+evalExp env arg (fn arg =>
+let
+val v = case mode of
+Arbitrary => Var (St.nextVar ())
+| Fixed => arg
+| Decreasing =>
+let
+val v = Var (St.nextVar ())
+in
+if St.check (AReln (Known, [arg])) then
+St.assert [(AReln (Known, [v]))]
+else
+();
+v
+end
+in
+doArgs (args, modes, v :: env')
+end)
+| _ => raise Fail "Iflow.doArgs: Impossible"
+in
+doArgs (args, #args rf, [])
+end)
+| _ => adefault ()
+in
+doArgs (e, [])
+end
 | EAbs _ => default ()
 | EUnop (s, e1) => evalExp env e1 (fn e1 => k (Func (Other s, [e1])))
 | EBinop (s, e1, e2) => evalExp env e1 (fn e1 => evalExp env e2 (fn e2 => k (Func (Other s, [e1, e2]))))
 | ERecord xets =>
 val saved = St.stash ()
 in
 St.assert [AReln (Sql (tab ^ "$New"), [Recd es])];
 St.insert loc;
 St.reinstate saved;
+St.assert [AReln (Sql tab, [Recd es])];
 k (Recd [])
 end
 | Delete (tab, e) =>
 let
 val old = St.nextVar ()
 | ERecv _ => default ()
 | ESleep _ => default ()
 | ESpawn _ => default ()
 end
+datatype var_source = Input of int | SubInput of int | Unknown
 fun check file =
 let
-val () = St.reset ()
+val () = (St.reset ();
+rfuns := IM.empty)
 val file = MonoReduce.reduce file
 val file = MonoOpt.optimize file
 val file = Fuse.fuse file
 val file = MonoOpt.optimize file
 St.assert ps;
 (evalExp env e (fn _ => ()) handle Cc.Contradiction => ());
 St.reinstate saved
 end
-| DValRec _ => ErrorMsg.errorAt loc "Iflow can't check recursive functions."
+| DValRec [(x, n, _, e, _)] =>
+let
+val tables = ref SS.empty
+val cookies = ref SS.empty
+fun deAbs (e, env, modes) =
+case #1 e of
+EAbs (_, _, _, e) => deAbs (e, Input (length env) :: env, ref Fixed :: modes)
+| _ => (e, env, rev modes)
+val (e, env, modes) = deAbs (e, [], [])
+fun doExp env (e as (_, loc)) =
+case #1 e of
+EPrim _ => e
+| ERel _ => e
+| ENamed _ => e
+| ECon (_, _, NONE) => e
+| ECon (dk, pc, SOME e) => (ECon (dk, pc, SOME (doExp env e)), loc)
+| ENone _ => e
+| ESome (t, e) => (ESome (t, doExp env e), loc)
+| EFfi _ => e
+| EFfiApp (m, f, es) =>
+(case (m, f, es) of
+("Basis", "set_cookie", [_, (EPrim (Prim.String cname), _), _, _, _]) =>
+cookies := SS.add (!cookies, cname)
+| _ => ();
+(EFfiApp (m, f, map (doExp env) es), loc))
+| EApp (e1, e2) =>
+let
+fun default () = (EApp (doExp env e1, doExp env e2), loc)
+fun explore (e, args) =
+case #1 e of
+EApp (e1, e2) => explore (e1, e2 :: args)
+| ENamed n' =>
+if n' = n then
+let
+fun doArgs (pos, args, modes) =
+case (args, modes) of
+((e1, _) :: args, m1 :: modes) =>
+(case e1 of
+ERel n =>
+(case List.nth (env, n) of
+Input pos' =>
+if pos' = pos then
+()
+else
+m1 := Arbitrary
+| SubInput pos' =>
+if pos' = pos then
+if !m1 = Arbitrary then
+()
+else
+m1 := Decreasing
+else
+m1 := Arbitrary
+| Unknown => m1 := Arbitrary)
+| _ => m1 := Arbitrary;
+doArgs (pos + 1, args, modes))
+| (_ :: _, []) => ()
+| ([], ms) => app (fn m => m := Arbitrary) ms
+in
+doArgs (0, args, modes);
+(EFfi ("Basis", "?"), loc)
+end
+else
+default ()
+| _ => default ()
+in
+explore (e, [])
+end
+| EAbs (x, t1, t2, e) => (EAbs (x, t1, t2, doExp (Unknown :: env) e), loc)
+| EUnop (uo, e1) => (EUnop (uo, doExp env e1), loc)
+| EBinop (bo, e1, e2) => (EBinop (bo, doExp env e1, doExp env e2), loc)
+| ERecord xets => (ERecord (map (fn (x, e, t) => (x, doExp env e, t)) xets), loc)
+| EField (e1, f) => (EField (doExp env e1, f), loc)
+| ECase (e, pes, ts) =>
+let
+val source =
+case #1 e of
+ERel n =>
+(case List.nth (env, n) of
+Input n => SOME n
+| SubInput n => SOME n
+| Unknown => NONE)
+| _ => NONE
+fun doV v =
+let
+fun doPat (p, env) =
+case #1 p of
+PWild => env
+| PVar _ => v :: env
+| PPrim _ => env
+| PCon (_, _, NONE) => env
+| PCon (_, _, SOME p) => doPat (p, env)
+| PRecord xpts => foldl (fn ((_, p, _), env) => doPat (p, env)) env xpts
+| PNone _ => env
+| PSome (_, p) => doPat (p, env)
+in
+(ECase (e, map (fn (p, e) => (p, doExp (doPat (p, env)) e)) pes, ts), loc)
+end
+in
+case source of
+NONE => doV Unknown
+| SOME inp => doV (SubInput inp)
+end
+| EStrcat (e1, e2) => (EStrcat (doExp env e1, doExp env e2), loc)
+| EError (e1, t) => (EError (doExp env e1, t), loc)
+| EReturnBlob {blob = b, mimeType = m, t} =>
+(EReturnBlob {blob = doExp env b, mimeType = doExp env m, t = t}, loc)
+| ERedirect (e1, t) => (ERedirect (doExp env e1, t), loc)
+| EWrite e1 => (EWrite (doExp env e1), loc)
+| ESeq (e1, e2) => (ESeq (doExp env e1, doExp env e2), loc)
+| ELet (x, t, e1, e2) => (ELet (x, t, doExp env e1, doExp (Unknown :: env) e2), loc)
+| EClosure (n, es) => (EClosure (n, map (doExp env) es), loc)
+| EQuery {exps, tables, state, query, body, initial} =>
+(EQuery {exps = exps, tables = tables, state = state,
+query = doExp env query,
+body = doExp (Unknown :: Unknown :: env) body,
+initial = doExp env initial}, loc)
+| EDml e1 =>
+(case parse dml e1 of
+NONE => ()
+| SOME c =>
+case c of
+Insert _ => ()
+| Delete (tab, _) =>
+tables := SS.add (!tables, tab)
+| Update (tab, _, _) =>
+tables := SS.add (!tables, tab);
+(EDml (doExp env e1), loc))
+| ENextval e1 => (ENextval (doExp env e1), loc)
+| ESetval (e1, e2) => (ESetval (doExp env e1, doExp env e2), loc)
+| EUnurlify (e1, t, b) => (EUnurlify (doExp env e1, t, b), loc)
+| EJavaScript (m, e) => (EJavaScript (m, doExp env e), loc)
+| ESignalReturn _ => e
+| ESignalBind _ => e
+| ESignalSource _ => e
+| EServerCall _ => e
+| ERecv _ => e
+| ESleep _ => e
+| ESpawn _ => e
+val e = doExp env e
+in
+rfuns := IM.insert (!rfuns, n, {tables = !tables, cookies = !cookies,
+args = map (fn r => !r) modes, body = e})
+end
+| DValRec _ => ErrorMsg.errorAt loc "Iflow can't check mutually-recursive functions yet."
 | DPolicy pol =>
 let
 val rvN = ref 0
 fun rv () =

Mercurial > urweb

comparison src/iflow.sml @ 1251:70092a661f70