Commit 32448f02 authored by Pietro Abate's avatar Pietro Abate
Browse files

WIP

parent 5005c436
......@@ -46,21 +46,15 @@ end)
type pp = P of vv * string | N of string * vv
and vv = V of string
let mk_pp = function
|P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (Var.mk alpha,parse_typ t))
|N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,Var.mk alpha))
let mk_prod l =
List.fold_left (fun acc c ->
Tallying.CS.prod (mk_pp c) acc
) Tallying.CS.sat l
let mk_union l1 l2 =
Tallying.CS.union (mk_prod l1) (mk_prod l2)
let mk_s ll =
let aux l =
List.fold_left (fun acc -> function
|P(V alpha,t) -> Tallying.CS.M.add (true,Var.mk alpha) (parse_typ t) acc
|N(t,V alpha) -> Tallying.CS.M.add (false,Var.mk alpha) (parse_typ t) acc
) Tallying.CS.M.empty l
in
List.fold_left (fun acc l ->
Tallying.CS.union (mk_prod l) acc
Tallying.CS.S.add (aux l) acc
) Tallying.CS.S.empty ll
let mk_union_res l1 l2 =
......@@ -84,8 +78,19 @@ let mk_union_res l1 l2 =
|[],l2 -> (Tallying.CS.S.singleton (aux l2))
|l1,l2 -> Tallying.CS.S.union (Tallying.CS.S.singleton (aux l1)) (Tallying.CS.S.singleton (aux l2))
(* check invariants on the constraints sets *)
let mk_pp = function
|P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (Var.mk alpha,parse_typ t))
|N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,Var.mk alpha))
let mk_prod l =
List.fold_left (fun acc c ->
Tallying.CS.prod (mk_pp c) acc
) Tallying.CS.sat l
let mk_union l1 l2 =
Tallying.CS.union (mk_prod l1) (mk_prod l2)
let test_constraint_ops () = [
"prod pos",mk_prod [P(V "A","Int");P(V "A","Bool")], mk_pp (P(V "A","Int & Bool"));
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment