Commit 2f1d479d authored by Pietro Abate's avatar Pietro Abate
Browse files

API change. Tallying.tallying now returns a list of maps

parent 74752b11
......@@ -46,7 +46,7 @@ let register_cst op t v =
let register_fun op dom codom eval =
register_cst op
(Types.arrow (Types.cons dom) (Types.cons codom))
(Value.Abstraction (Some [(dom,codom)],eval, `List([[]])))
(Value.Abstraction (Some [(dom,codom)],eval, `List([])))
let register_fun2 op dom1 dom2 codom eval =
let t2 = Types.arrow (Types.cons dom2) (Types.cons codom) in
......@@ -55,7 +55,7 @@ let register_fun2 op dom1 dom2 codom eval =
(Types.arrow (Types.cons dom1) (Types.cons t2))
(Value.Abstraction (Some [(dom1,t2)],(fun v1 ->
Value.Abstraction (iface2,
eval v1, `List([[]]))), `List([[]])))
eval v1, `List([]))), `List([])))
let register_op op ?(expect=Types.any) typ eval =
register_unary op
(fun tf _ _ -> let t = tf expect true in typ t)
......
......@@ -48,9 +48,9 @@ let attrib att =
let elem ns tag att child =
if !keep_ns then
XmlNs (Atom tag, Record (attrib att, `List([[]])), child, ns, `List([[]]))
XmlNs (Atom tag, Record (attrib att, `List([])), child, ns, `List([]))
else
Xml (Atom tag, Record (attrib att, `List([[]])), child, `List([[]]))
Xml (Atom tag, Record (attrib att, `List([])), child, `List([]))
type stack =
| Element of Value.t * stack
......@@ -64,7 +64,7 @@ let ns_table = ref Ns.empty_table
let rec create_elt accu = function
| String (s,st) -> create_elt (string s accu) st
| Element (x,st) -> create_elt (Pair (x,accu, `List([[]]))) st
| Element (x,st) -> create_elt (Pair (x,accu, `List([]))) st
| Start (ns,name,att,old_table,st) ->
stack := Element (elem ns name att accu, st);
ns_table := old_table
......@@ -132,7 +132,7 @@ let load_html s =
| Nethtml.Element (tag, att, child) ->
let att = List.map (fun (n,v) -> (Label.mk (Ns.empty, U.mk n), U.mk v)) att in
Pair (elem Ns.empty_table (Atoms.V.mk (Ns.empty,U.mk tag) )
att (val_of_docs child), q, `List([[]]))
att (val_of_docs child), q, `List([]))
and val_of_docs = function
| [] -> nil
| h::t -> val_of_doc (val_of_docs t) h
......
......@@ -59,7 +59,7 @@ module H = Hashtbl.Make(Ns.Uri)
let exn_print_xml = CDuceExn (Pair (
Atom (Atoms.V.mk_ascii "Invalid_argument"),
string_latin1 "print_xml", `List([[]])))
string_latin1 "print_xml", `List([])))
let blank = U.mk " "
let true_literal = U.mk "true"
......
......@@ -85,42 +85,42 @@ let exn_load_file_utf8 = lazy (
Value.CDuceExn (
Value.Pair (
Value.Atom (Atoms.V.mk_ascii "load_file_utf8"),
Value.string_latin1 "File is not a valid UTF-8 stream", `List([[]])))
Value.string_latin1 "File is not a valid UTF-8 stream", `List([])))
)
let exn_int_of = lazy (
Value.CDuceExn (
Value.Pair (
Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
Value.string_latin1 "int_of", `List([[]])))
Value.string_latin1 "int_of", `List([])))
)
let exn_char_of = lazy (
Value.CDuceExn (
Value.Pair (
Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
Value.string_latin1 "char_of", `List([[]])))
Value.string_latin1 "char_of", `List([])))
)
let exn_float_of = lazy (
Value.CDuceExn (
Value.Pair (
Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
Value.string_latin1 "float_of", `List([[]])))
Value.string_latin1 "float_of", `List([])))
)
let exn_namespaces = lazy (
Value.CDuceExn (
Value.Pair (
Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
Value.string_latin1 "namespaces", `List([[]])))
Value.string_latin1 "namespaces", `List([])))
)
let exn_cdata_of = lazy (
Value.CDuceExn (
Value.Pair (
Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
Value.string_latin1 "cdata_of", `List([[]])))
Value.string_latin1 "cdata_of", `List([])))
)
let eval_load_file ~utf8 e =
......@@ -301,7 +301,7 @@ register_fun "split_atom"
let (ns,l) = Atoms.V.value q in
Value.Pair(
Value.string_utf8 (Ns.Uri.value ns),
Value.string_utf8 l, `List([[]]))
Value.string_utf8 l, `List([]))
| _ -> assert false);;
register_fun "make_atom"
......
......@@ -2842,9 +2842,8 @@ module Tallying = struct
type s = S.t
type m = M.t
type e = Descr.s E.t
type es = ES.t
type sigma = (Var.var * t) list
type sigma = Descr.s E.t
type sl = sigma list
let singleton = function
......@@ -2854,10 +2853,7 @@ module Tallying = struct
let pp_s = S.print
let pp_m = M.print
let pp_e = E.print
let pp_sl ppf ll =
print_lst (fun ppf l ->
(print_lst (fun ppf (v,t) -> Format.fprintf ppf "(%a/%a)" Var.print v Print.print t) ppf l)
) ppf ll
let pp_sl ppf ll = print_lst E.print ppf ll
let sat = S.singleton M.empty
let unsat = S.empty
......@@ -3150,28 +3146,24 @@ module Tallying = struct
let tallying l =
let n = List.fold_left (fun acc (s,t) ->
let d = diff s t in
if is_empty d then CS.sat else
if no_var d then CS.unsat else
CS.prod acc (norm d)) CS.sat l
if is_empty d then CS.sat
else if no_var d then CS.unsat
else CS.prod acc (norm d)) CS.sat l
in
(* Format.printf "Norm : %a\n" CS.pp_s n;*)
if Pervasives.(n = CS.unsat) then raise Step1Fail else
let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr _ -> acc) n CS.ES.empty in
(* Format.printf "Union/Merge : %a \n" CS.ES.print m;*)
if CS.ES.is_empty m then raise Step2Fail else
let el = CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc) m CS.ES.empty in
(* Format.printf "Unify : %a\n" CS.ES.print el;*)
List.map (CS.E.bindings) (CS.ES.elements el)
(* List.map (CS.E.bindings) *) (CS.ES.elements el)
let apply_subst t subl =
List.fold_left (fun acc s ->
Positive.substitute acc s) t subl
CS.E.fold (fun var subst acc -> Positive.substitute acc (var,subst)) subl t
let domain ll =
List.fold_left (fun acc l ->
List.fold_left (fun acc (v,_) ->
List.fold_left (fun acc e ->
CS.E.fold (fun v _ acc ->
Var.Set.add v acc
) acc l
) e acc
) Var.Set.empty ll
end
......@@ -3188,8 +3180,8 @@ let apply_raw s t =
let rec aux (i,acc1) (j,acc2) t1 t2 () =
let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
try
(Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]),
(acc1, acc2)
let sl = Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))] in
(sl,(acc1, acc2))
with
|Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1")
|Tallying.Step2Fail -> begin
......@@ -3214,28 +3206,39 @@ let apply_raw s t =
!result
let apply_full s t =
let subst_lst,(s,t) = apply_raw s t in
let (subst_lst,(s,t)) = apply_raw s t in
let gamma = Var.mk "Gamma" in
let ss,tt,res =
List.fold_left (fun (ssacc,ttacc,resacc) e ->
let ss = Tallying.CS.E.fold (fun var subst acc -> Positive.substitute acc (var,subst)) e s in
let tt = Tallying.CS.E.fold (fun var subst acc -> Positive.substitute acc (var,subst)) e t in
let res = Tallying.CS.E.find gamma e in
(cap ssacc (Positive.clean_type ss),
cap ttacc (Positive.clean_type tt),
cap resacc (Positive.clean_type res)
)
) (any,any,any) subst_lst
in
(*
let ss =
List.fold_left (fun tacc constr_lst ->
cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) s constr_lst)) any subst_lst
List.fold_left (fun tacc e ->
cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) s (Tallying.CS.E.bindings e))) any subst_lst
in
let tt =
List.fold_left (fun tacc constr_lst ->
List.fold_left (fun tacc e ->
cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) t constr_lst)) any subst_lst
Positive.substitute tacc subst) t (Tallying.CS.E.bindings e))) any subst_lst
in
(*let arr = Arrow.get ss in
let res = Arrow.apply arr (tt) in *)
let ss = Positive.clean_type ss in
let tt = Positive.clean_type tt in
(*let res = Positive.clean_type res in *)
let res2 = List.fold_left
let res2 = List.fold_left (fun acc e -> cap acc (Tallying.CS.E.find gamma e)) any subst_lst in
(fun acc l -> cap acc (snd (List.find (fun (`Var v, _) -> 0 == String.compare v.Var.id "Gamma") l))) any subst_lst
in
let res2 = Positive.clean_type res2 in
*)
Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n%!"
Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res2; res2
Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res; res
let apply s t = fst (apply_raw s t)
......@@ -398,14 +398,13 @@ module Tallying : sig
type s = S.t
type m = M.t
type e = t E.t
type es = ES.t
type sigma = (Var.var * t) list
type sigma = t E.t
type sl = sigma list
val pp_s : Format.formatter -> s -> unit
val pp_m : Format.formatter -> m -> unit
val pp_e : Format.formatter -> e -> unit
val pp_e : Format.formatter -> sigma -> unit
val pp_sl : Format.formatter -> sl -> unit
val merge : m -> m -> m
......@@ -419,7 +418,7 @@ module Tallying : sig
val norm : t -> CS.s
val merge : CS.m -> CS.s
val solve : CS.s -> CS.es
val unify : CS.e -> CS.e
val unify : CS.sigma -> CS.sigma
val tallying : (t * t) list -> CS.sl
val apply_subst : t -> CS.sigma -> t
val domain : CS.sl -> Var.Set.t
......@@ -428,4 +427,4 @@ end
val apply : t -> t -> Tallying.CS.sl
val apply_full : t -> t -> t
val apply_raw : t -> t -> Tallying.CS.sl * (t*t)
val apply_raw : t -> t -> (Tallying.CS.sl * (t * t))
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