Mercurial > urweb

comparison src/iflow.sml @ 1250:e80582b927f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add rand to Basis and handle it in Iflow
author Adam Chlipala <adamc@hcoop.net>
date Thu, 29 Apr 2010 17:24:42 -0400
parents 7c6fc92f6c31
children 70092a661f70
comparison
equal deleted inserted replaced
1249:7c6fc92f6c31 1250:e80582b927f2
970 970
971 datatype sqexp = 971 datatype sqexp =
972 SqConst of Prim.t 972 SqConst of Prim.t
973 | SqTrue 973 | SqTrue
974 | SqFalse 974 | SqFalse
975 | SqNot of sqexp
975 | Field of string * string 976 | Field of string * string
976 | Computed of string 977 | Computed of string
977 | Binop of Rel * sqexp * sqexp 978 | Binop of Rel * sqexp * sqexp
978 | SqKnown of sqexp 979 | SqKnown of sqexp
979 | Inj of Mono.exp 980 | Inj of Mono.exp
1073 wrap unmodeled (fn () => Unmodeled), 1074 wrap unmodeled (fn () => Unmodeled),
1074 wrap sqlify Inj, 1075 wrap sqlify Inj,
1075 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",") 1076 wrap (follow (const "COALESCE(") (follow sqexp (follow (const ",")
1076 (follow (keep (fn ch => ch <> #")")) (const ")"))))) 1077 (follow (keep (fn ch => ch <> #")")) (const ")")))))
1077 (fn ((), (e, _)) => e), 1078 (fn ((), (e, _)) => e),
1079 wrap (follow (const "(NOT ") (follow sqexp (const ")")))
1080 (fn ((), (e, _)) => SqNot e),
1078 wrap (follow (ws (const "(")) 1081 wrap (follow (ws (const "("))
1079 (follow (wrap 1082 (follow (wrap
1080 (follow sqexp 1083 (follow sqexp
1081 (alt 1084 (alt
1082 (wrap 1085 (wrap
1469 else 1472 else
1470 let 1473 let
1471 val (_, hs, _) = !hyps 1474 val (_, hs, _) = !hyps
1472 in 1475 in
1473 ErrorMsg.errorAt loc "The database update policy may be violated here."; 1476 ErrorMsg.errorAt loc "The database update policy may be violated here.";
1474 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs), 1477 Print.prefaces "Situation" [("Hypotheses", Print.p_list p_atom hs)(*,
1475 ("E-graph", Cc.p_database db)] 1478 ("E-graph", Cc.p_database db)*)]
1476 end 1479 end
1477 end 1480 end
1478 1481
1479 val insertable = ref ([] : atom list list) 1482 val insertable = ref ([] : atom list list)
1480 fun allowInsert v = insertable := v :: !insertable 1483 fun allowInsert v = insertable := v :: !insertable
1556 in 1559 in
1557 case e of 1560 case e of
1558 SqConst p => inl (Const p) 1561 SqConst p => inl (Const p)
1559 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", [])) 1562 | SqTrue => inl (Func (DtCon0 "Basis.bool.True", []))
1560 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", [])) 1563 | SqFalse => inl (Func (DtCon0 "Basis.bool.False", []))
1564 | SqNot e =>
1565 inr (case expIn e of
1566 inl e => Reln (Eq, [e, Func (DtCon0 "Basis.bool.False", [])])
1567 | inr _ => Unknown)
1561 | Field (v, f) => inl (Proj (rvOf v, f)) 1568 | Field (v, f) => inl (Proj (rvOf v, f))
1562 | Computed _ => default () 1569 | Computed _ => default ()
1563 | Binop (bo, e1, e2) => 1570 | Binop (bo, e1, e2) =>
1564 let 1571 let
1565 val e1 = expIn e1 1572 val e1 = expIn e1
1672 fun usedFields e = 1679 fun usedFields e =
1673 case e of 1680 case e of
1674 SqConst _ => [] 1681 SqConst _ => []
1675 | SqTrue => [] 1682 | SqTrue => []
1676 | SqFalse => [] 1683 | SqFalse => []
1684 | SqNot e => usedFields e
1677 | Field (v, f) => [(false, Proj (rvOf v, f))] 1685 | Field (v, f) => [(false, Proj (rvOf v, f))]
1678 | Computed _ => [] 1686 | Computed _ => []
1679 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2 1687 | Binop (_, e1, e2) => usedFields e1 @ usedFields e2
1680 | SqKnown _ => [] 1688 | SqKnown _ => []
1681 | Inj e => 1689 | Inj e =>
1863 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e]))) 1871 | ECon (_, pc, SOME e) => evalExp env e (fn e => k (Func (DtCon1 (patCon pc), [e])))
1864 | ENone _ => k (Func (DtCon0 "None", [])) 1872 | ENone _ => k (Func (DtCon0 "None", []))
1865 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e]))) 1873 | ESome (_, e) => evalExp env e (fn e => k (Func (DtCon1 "Some", [e])))
1866 | EFfi _ => default () 1874 | EFfi _ => default ()
1867 1875
1876 | EFfiApp ("Basis", "rand", []) =>
1877 let
1878 val e = Var (St.nextVar ())
1879 in
1880 St.assert [AReln (Known, [e])];
1881 k e
1882 end
1868 | EFfiApp x => doFfi x 1883 | EFfiApp x => doFfi x
1869 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e]) 1884 | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e])
1870 1885
1871 | EApp (e1, e2) => evalExp env e1 (fn _ => evalExp env e2 (fn _ => default ())) 1886 | EApp (e1, e2) => evalExp env e1 (fn _ => evalExp env e2 (fn _ => default ()))
1872 1887