Ur/Web: src/iflow.sml comparison

comparison src/iflow.sml @ 1253:9d65866ab9ab

Some Iflow improvements for gradebook

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 06 May 2010 12:14:00 -0400
parents	2e4159a7d2d3
children	3d06e0f7a6f3

comparison

equal deleted inserted replaced

-:2e4159a7d2d3
+:9d65866ab9ab
 val assert : database * atom -> unit
 val check : database * atom -> bool
 val p_database : database Print.printer
-val builtFrom : database * {UseKnown : bool, Base : exp list, Derived : exp} -> bool
+val builtFrom : database * {Base : exp list, Derived : exp} -> bool
 val p_repOf : database -> exp Print.printer
 end = struct
 local
 ()
 else
 raise Contradiction
 | Nothing =>
 let
+val cons = ref SM.empty
 val r'' = ref (Node {Id = nodeId (),
 Rep = ref NONE,
-Cons = ref SM.empty,
+Cons = cons,
 Variety = Nothing,
 Known = ref (!(#Known (unNode r))),
 Ge = ref NONE})
 val r' = ref (Node {Id = nodeId (),
 Cons = ref SM.empty,
 Variety = Dt1 (f, r''),
 Known = #Known (unNode r),
 Ge = ref NONE})
 in
+cons := SM.insert (!cons, f, r');
 #Rep (unNode r) := SOME r'
 end
 | _ => raise Contradiction
 end
 | (Eq, [e1, e2]) =>
 | _ => false
 end
 | _ => false)
 handle Undetermined => false
-fun builtFrom (db, {UseKnown = uk, Base = bs, Derived = d}) =
+fun builtFrom (db, {Base = bs, Derived = d}) =
 let
 val bs = map (fn b => representative (db, b)) bs
 fun loop d =
 let
 val d = repOf d
 in
-(uk andalso !(#Known (unNode d)))
+!(#Known (unNode d))
 orelse List.exists (fn b => repOf b = d) bs
 orelse (case #Variety (unNode d) of
 Dt0 _ => true
 | Dt1 (_, d) => loop d
 | Prim _ => true
 | Recrd (xes, _) => List.all loop (SM.listItems (!xes))
 | Nothing => false)
+orelse List.exists (fn r => List.exists (fn b => repOf b = repOf r) bs)
+(SM.listItems (!(#Cons (unNode d))))
 end
 fun decomp e =
 case e of
 Func (Other _, es) => List.all decomp es
 | Binop of Rel * sqexp * sqexp
 | SqKnown of sqexp
 | Inj of Mono.exp
 | SqFunc of string * sqexp
 | Unmodeled
+| Null
 fun cmp s r = wrap (const s) (fn () => Exps (fn (e1, e2) => Reln (r, [e1, e2])))
 val sqbrel = altL [cmp "=" Eq,
 cmp "<>" Ne,
 fun sqexp chs =
 log "sqexp"
 (altL [wrap prim SqConst,
 wrap (const "TRUE") (fn () => SqTrue),
 wrap (const "FALSE") (fn () => SqFalse),
+wrap (const "NULL") (fn () => Null),
 wrap field Field,
 wrap uw_ident Computed,
 wrap known SqKnown,
 wrap func SqFunc,
 wrap unmodeled (fn () => Unmodeled),
 val assert : atom list -> unit
 val addPath : check -> unit
 val allowSend : atom list * exp list -> unit
-val send : bool -> check -> unit
+val send : check -> unit
 val allowInsert : atom list -> unit
 val insert : ErrorMsg.span -> unit
 val allowDelete : atom list -> unit
 | ACond _ :: _ => false
 in
 checkGoals goals IM.empty
 end
-fun buildable uk (e, loc) =
+fun buildable (e, loc) =
 let
 fun doPols pols acc =
 case pols of
-[] => ((*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
+[] =>
-("Derived", p_exp e),
+let
-("Hyps", Print.p_list p_atom (#2 (!hyps)))];*)
+val b = Cc.builtFrom (db, {Base = acc, Derived = e})
-Cc.builtFrom (db, {UseKnown = uk, Base = acc, Derived = e}))
+in
+(*Print.prefaces "buildable" [("Base", Print.p_list p_exp acc),
+("Derived", p_exp e),
+("Hyps", Print.p_list p_atom (#2 (!hyps))),
+("Good", Print.PD.string (Bool.toString b))];*)
+b
+end
 | (goals, es) :: pols =>
 checkGoals goals (fn unifs => doPols pols (map (simplify unifs) es @ acc))
 orelse doPols pols acc
 in
 if doPols (!sendable) [] then
 let
 val (_, hs, _) = !hyps
 in
 ErrorMsg.errorAt loc "The information flow policy may be violated here.";
 Print.prefaces "Situation" [("User learns", p_exp e),
-("Hypotheses", Print.p_list p_atom hs)(*,
+("Hypotheses", Print.p_list p_atom hs),
-("E-graph", Cc.p_database db)*)]
+("E-graph", Cc.p_database db)]
 end
 end
 fun checkPaths () =
 let
 case !r of
 NONE => ()
 | SOME (hs, e) =>
 (r := NONE;
 setHyps hs;
-buildable true e)) (!path);
+buildable e)) (!path);
 setHyps hs
 end
 fun allowSend v = ((*Print.prefaces "Allow" [("goals", Print.p_list p_atom (#1 v)),
 ("exps", Print.p_list p_exp (#2 v))];*)
 sendable := v :: !sendable)
-fun send uk (e, loc) = ((*Print.preface ("Send", p_exp e);*)
+fun send (e, loc) = ((*Print.preface ("Send[" ^ Bool.toString uk ^ "]", p_exp e);*)
 complete ();
 checkPaths ();
 if isKnown e then
 ()
 else
-buildable uk (e, loc))
+buildable (e, loc))
 fun doable pols (loc : ErrorMsg.span) =
 let
 val pols = !pols
 in
 in
 case e of
 SqConst p => inl (Const p)
 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
+| Null => inl (Func (DtCon0 "None", []))
 | SqNot e =>
 inr (case expIn e of
 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
 | inr _ => Unknown)
 | Field (v, f) => inl (Proj (rvOf v, f))
 Env : exp list,
 NextVar : unit -> exp,
 Add : atom -> unit,
 Save : unit -> 'a,
 Restore : 'a -> unit,
-UsedExp : bool * exp -> unit,
 Cont : queryMode
 }
 fun doQuery (arg : 'a doQuery) (e as (_, loc)) =
 let
 fun usedFields e =
 case e of
 SqConst _ => []
 | SqTrue => []
 | SqFalse => []
+| Null => []
 | SqNot e => usedFields e
 | Field (v, f) => [(false, Proj (rvOf v, f))]
 | Computed _ => []
 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
 | SqKnown _ => []
 NONE => (ErrorMsg.errorAt loc "Expression injected into SQL is too complicated";
 [])
 | SOME e => [(true, e)])
 | SqFunc (_, e) => usedFields e
 | Unmodeled => []
-fun doUsed () = case #Where r of
-NONE => ()
-| SOME e =>
-app (#UsedExp arg) (usedFields e)
 fun normal' () =
 case #Cont arg of
 SomeCol k =>
 let
 end
 fun doWhere final =
 (addFrom ();
 case #Where r of
-NONE => (doUsed (); final ())
+NONE => final ()
 | SOME e =>
 let
 val p = case expIn e of
 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.True", [])])
 | inr p => p
 val saved = #Save arg ()
 in
 decomp {Save = #Save arg, Restore = #Restore arg, Add = #Add arg}
-p (fn () => (doUsed (); final ()) handle Cc.Contradiction => ());
+p (fn () => final () handle Cc.Contradiction => ());
 #Restore arg saved
 end)
 handle Cc.Contradiction => ()
 fun normal () = doWhere normal'
 | _ => ()
 else
 ();
 k (Recd []))
 | e :: es =>
-evalExp env e (fn e => (St.send true (e, loc); doArgs es))
+evalExp env e (fn e => (St.send (e, loc); doArgs es))
 in
 doArgs es
 end
 else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then
 default ()
 | EField (e, s) => evalExp env e (fn e => k (Proj (e, s)))
 | ECase (e, pes, {result = res, ...}) =>
 evalExp env e (fn e =>
 if List.all (fn (_, (EWrite (EPrim _, _), _)) => true
 | _ => false) pes then
-(St.send true (e, loc);
+(St.send (e, loc);
 k (Recd []))
 else
 (St.addPath (e, loc);
 app (fn (p, pe) =>
 let
 end) pes))
 | EStrcat (e1, e2) =>
 evalExp env e1 (fn e1 =>
 evalExp env e2 (fn e2 =>
 k (Func (Other "cat", [e1, e2]))))
-| EError (e, _) => evalExp env e (fn e => St.send true (e, loc))
+| EError (e, _) => evalExp env e (fn e => St.send (e, loc))
 | EReturnBlob {blob = b, mimeType = m, ...} =>
 evalExp env b (fn b =>
-(St.send true (b, loc);
+(St.send (b, loc);
 evalExp env m
-(fn m => St.send true (m, loc))))
+(fn m => St.send (m, loc))))
 | ERedirect (e, _) =>
-evalExp env e (fn e => St.send true (e, loc))
+evalExp env e (fn e => St.send (e, loc))
 | EWrite e =>
-evalExp env e (fn e => (St.send true (e, loc);
+evalExp env e (fn e => (St.send (e, loc);
 k (Recd [])))
 | ESeq (e1, e2) =>
 let
 val path = St.stashPath ()
 in
 doQuery {Env = env,
 NextVar = Var o St.nextVar,
 Add = fn a => St.assert [a],
 Save = St.stash,
 Restore = St.reinstate,
-UsedExp = fn (b, e) => St.send b (e, loc),
 Cont = AllCols (fn x =>
 (St.assert [AReln (Eq, [r, x])];
 evalExp (acc :: r :: env) b k))} q
 end)
 | EDml e =>
 fun doQ k = doQuery {Env = [],
 NextVar = rv,
 Add = fn a => atoms := a :: !atoms,
 Save = fn () => !atoms,
 Restore = fn ls => atoms := ls,
-UsedExp = fn _ => (),
 Cont = SomeCol (fn r => k (rev (!atoms), r))}
 fun untab (tab, nams) = List.filter (fn AReln (Sql tab', [Lvar lv]) =>
 tab' <> tab
 orelse List.all (fn Lvar lv' => lv' <> lv

Mercurial > urweb

comparison src/iflow.sml @ 1253:9d65866ab9ab