Commit 6ee8a6b0 authored by Pietro Abate's avatar Pietro Abate

Parse type variables as patterns

- type variables are now correctly parsed as patterns
  and not as expressions

- Add a new module Var that contains all the type variables
  related machinery

- Remove old functions and unit tests about BoolVar of only
  variables, since now variables are always stored associated
  with one or more kinds
parent c6f59119
......@@ -7,6 +7,7 @@ State
Pool
Ns
SortedList
Var
Atoms
Bool
Chars
......
......@@ -169,25 +169,3 @@ module Sum(X : T)(Y : T) = struct
| Left t -> Format.fprintf ppf "L%a" X.dump t
| Right t -> Format.fprintf ppf "R%a" Y.dump t
end
type var = [ `Var of String.t ]
type 'a pairvar = [ `Atm of 'a | var ]
module Var (X : T) = struct
type t = X.t pairvar
let hash = function `Atm t -> X.hash t | `Var s -> (* String.hash s *) Hashtbl.hash (`Var s)
let check = function `Atm t -> X.check t | `Var _ -> ()
let compare t1 t2 =
match t1,t2 with
|`Atm x, `Atm y -> X.compare x y
|`Var x, `Var y when x = y -> 0
(* HACK fix BoolVar.get to get variables in the correct order *)
|`Var x, `Var y -> if String.compare x y = -1 then 1 else -1
|`Var _, `Atm _ -> -1
|`Atm _, `Var _ -> 1
let equal t1 t2 = (compare t1 t2) = 0
let dump ppf = function
|`Atm x -> X.dump ppf x
|`Var x -> Format.fprintf ppf "`$%a" String.dump x
end
......@@ -45,8 +45,6 @@ and pexpr =
(* CDuce is a Lambda-calculus ... *)
| Var of U.t
(* this TVar must be moved to patt *)
| TVar of BoolVar.Vars.V.t
| Apply of pexpr * pexpr
| Abstraction of abstr
......@@ -105,6 +103,7 @@ and branches = (ppat * pexpr) list
and ppat = ppat' located
and ppat' =
| TVar of Var.t (** type variables *)
| PatVar of U.t list
| Cst of pexpr
| NsT of U.t
......
......@@ -404,7 +404,7 @@ EXTEND Gram
tag_type: [
[ "_" -> mk _loc (Internal (Types.atom Atoms.any))
| "$"; a = ident_or_keyword -> mk _loc (Cst (TVar a))
| "$"; a = ident_or_keyword -> mk _loc (TVar a)
| a = ident_or_keyword -> mk _loc (Cst (Atom (ident a)))
| t = ANY_IN_NS -> mk _loc (NsT (ident t))
]
......
......@@ -25,12 +25,6 @@ module BoolIntervals : S with type s = Intervals.t = struct
let mk_atm s = atom (`Atm (Intervals.atom (Intervals.V.mk s)))
end
module BoolVars : S with type s = BoolVar.Vars.t = struct
include BoolVar.BoolVars
let mk_var s = atom (`Var s)
let mk_atm s = failwith "AA"
end
module ExprParser (B : S) = struct
open Camlp4.PreCast
......@@ -64,7 +58,6 @@ end
module BCP = ExprParser(BoolChars)
module BAP = ExprParser(BoolAtoms)
module BIP = ExprParser(BoolIntervals)
module BVP = ExprParser(BoolVars)
(*
XXX this needs much more infrastructure as in types.ml
......@@ -82,20 +75,6 @@ let atoms_tests = [
"difference empty", BAP.os "atm foo ^ atm bar", BAP.os "Empty";
];;
let atoms_splitvar_vars =
"vars splitvar" >:::
List.map (fun (descr, s1,s2) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
assert_equal (BoolVar.BoolVars.equal ( s1 :> BoolVar.BoolVars.t ) s2) true
)
) [
"vars empty", fst(BoolAtoms.extractvars (BAP.os "atm foo")), BVP.os "Empty";
"vars 1 ", fst(BoolAtoms.extractvars (BAP.os "var alpha v (atm foo ^ var beta) v var gamma")), BVP.os "var alpha v var gamma";
"vars 2", fst(BoolAtoms.extractvars (BAP.os "var alpha v atm foo")), BVP.os "var alpha";
"vars 2", fst(BoolAtoms.extractvars (BAP.os "var alpha v atm foo")), fst(BoolChars.extractvars (BCP.os "var alpha v atm c"));
]
;;
let atoms_splitvar_atm =
"atoms splitvar" >:::
List.map (fun (descr, s1,s2) ->
......@@ -109,19 +88,6 @@ let atoms_splitvar_atm =
]
;;
let splitvar_mixed_union_var =
"splitvar union" >:::
List.map (fun (descr, s1,s2,r) ->
(Printf.sprintf "test %s" descr) >:: (fun _ ->
assert_equal (BoolVar.BoolVars.equal (BoolVar.BoolVars.cup s1 s2) r) true
)
) [
"atoms/chars", fst(BoolAtoms.extractvars (BAP.os "atm foo")), fst(BoolChars.extractvars (BCP.os "var alpha v atm x")), BVP.os "var alpha";
"atoms/chars", fst(BoolAtoms.extractvars (BAP.os "var alpha v atm foo")), fst(BoolChars.extractvars (BCP.os "var alpha v atm c")), BVP.os "var alpha";
]
;;
let splitvar_mixed_union_atm =
"splitvar union" >:::
List.map (fun (descr, s1,s2,r) ->
......@@ -154,7 +120,7 @@ let atoms_contains =
(Printf.sprintf "test %s" descr) >:: (fun _ ->
let a = Atoms.V.mk_ascii i in
let t = BAP.os s in
assert_equal (Atoms.contains a (BoolAtoms.get t)) true
assert_equal (Atoms.contains a (BoolAtoms.leafconj t)) true
)
)
[
......@@ -169,9 +135,7 @@ let all =
atoms_structure;
atoms_contains;
atoms_splitvar_atm;
atoms_splitvar_vars;
splitvar_mixed_union_atm;
splitvar_mixed_union_var
]
let main () =
......
......@@ -3,8 +3,7 @@ let (>) : int -> int -> bool = (>)
let (=) : int -> int -> bool = (=)
(* this is the the of the Constructor container *)
module type E =
sig
module type E = sig
type elem
include Custom.T
......@@ -17,10 +16,9 @@ sig
end
module type S =
sig
module type S = sig
type s
type elem = s Custom.pairvar
type elem = s Var.pairvar
type 'a bdd =
[ `True
| `False
......@@ -45,7 +43,7 @@ sig
val neg_atom : elem -> t
(* vars a : return a bdd that is ( Any ^ Var a ) *)
val vars : Custom.var -> t
val vars : Var.var -> t
val iter: (elem-> unit) -> t -> unit
......@@ -59,7 +57,7 @@ sig
val trivially_disjoint: t -> t -> bool
val extractvars : t -> [> `Var of Custom.String.t ] bdd * t
val extractvars : t -> [> `Var of Var.t ] bdd * t
end
......@@ -93,8 +91,8 @@ struct
* `Var are String
*)
type s = T.t
module X = Custom.Var(T)
type elem = s Custom.pairvar
module X = Var.Make(T)
type elem = s Var.pairvar
type 'a bdd =
[ `True
| `False
......@@ -455,7 +453,7 @@ struct
let cap = ( ** )
let diff = ( // )
(* return a couple of trees (v,a), the second where all variables
(* return a couple of trees (v,a)
* v = only variables as leaves
* a = only atoms as leaves
*)
......@@ -476,10 +474,3 @@ struct
(v,t)
end
module Vars = struct
module V = struct include Custom.String end
include Bool.Make(V)
end
module BoolVars = Make(Vars)
......@@ -19,7 +19,6 @@ let compare = 1
type const =
| Integer of Intervals.V.t
| Atom of Atoms.V.t
| Var of BoolVar.Vars.V.t
| Char of Chars.V.t
| Pair of const * const
| Xml of const * const
......@@ -63,9 +62,6 @@ module Const = struct
| Atom x, Atom y -> Atoms.V.compare x y
| Atom _, _ -> -1
| _, Atom _ -> 1
| Var x, Var y -> BoolVar.Vars.V.compare x y
| Var _, _ -> -1
| _, Var _ -> 1
| Char x, Char y -> Chars.V.compare x y
| Char _, _ -> -1
......@@ -99,7 +95,6 @@ module Const = struct
| Xml (x,y) -> 5 + 17 * (hash x) + 257 * (hash y)
| Record x -> 6 + 17 * (LabelMap.hash hash x)
| String (i,j,s,r) -> 7 + 17 * (U.hash s) + 257 * hash r
| Var x -> 7 + 17 * (BoolVar.Vars.V.hash x)
(* Note: improve hash for String *)
let equal c1 c2 = compare c1 c2 = 0
......@@ -355,15 +350,15 @@ let record label t =
let record_fields x =
{ empty with record = BoolRec.atom (`Atm (Rec.atom x)) }
let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
let vars a = {
let var a = {
(* Atm = Any ^ a *)
times = BoolPair.vars (`Var a);
xml = BoolPair.vars (`Var a);
arrow = BoolPair.vars (`Var a);
record= BoolRec.vars (`Var a);
ints = BoolIntervals.vars (`Var a);
atoms = BoolAtoms.vars (`Var a);
chars = BoolChars.vars (`Var a);
times = BoolPair.vars a;
xml = BoolPair.vars a;
arrow = BoolPair.vars a;
record= BoolRec.vars a;
ints = BoolIntervals.vars a;
atoms = BoolAtoms.vars a;
chars = BoolChars.vars a;
abstract = Abstract.any;
absent= false;
}
......@@ -446,7 +441,6 @@ let rec constant = function
| Integer i -> interval (Intervals.atom i)
| Atom a -> atom (Atoms.atom a)
| Char c -> char (Chars.atom c)
| Var a -> vars a
| Pair (x,y) -> times (const_node x) (const_node y)
| Xml (x,y) -> xml (const_node x) (const_node y)
| Record x -> record_fields (false ,LabelMap.map const_node x)
......@@ -1365,7 +1359,6 @@ struct
let rec print_const ppf = function
| Integer i -> Intervals.V.print ppf i
| Atom a -> Atoms.V.print_quote ppf a
| Var a -> Format.fprintf ppf "`$%s" a
| Char c -> Chars.V.print ppf c
| Pair (x,y) -> Format.fprintf ppf "(%a,%a)" print_const x print_const y
| Xml (x,y) -> Format.fprintf ppf "XML(%a,%a)" print_const x print_const y
......@@ -2201,35 +2194,74 @@ module Tallying = struct
exception UnSatConstr
type constr = (bool * Custom.var * s)
type constr = (bool * Var.var * s)
module CS = struct
type key = (bool * Custom.var)
let print_lst f ppf l =
let rec aux ppf = function
|[] -> Format.fprintf ppf "@."
|[h] -> Format.fprintf ppf "%a@." f h
|h::t -> Format.fprintf ppf "%a ,%a" f h aux t
in
match l with
|[] -> Format.fprintf ppf "{}"
|_ -> Format.fprintf ppf "{ %a }" aux l
(* constraint set : map to store constraints of the form (alpha,t) or (t,alpha) *)
module M = Map.Make(struct
type t = key
let compare = Pervasives.compare
end)
module M = struct
include Map.Make(struct
type t = (bool * Var.var)
let compare = Pervasives.compare
end)
(* Set of constraint sets *)
module S = Set.Make(struct
type t = Descr.s M.t
let compare = M.compare Descr.compare
end)
let print ppf m =
print_lst (fun ppf -> fun ((b,`Var v),s) ->
if b then
Format.fprintf ppf "(`$%s,%a)" v Print.print s
else
Format.fprintf ppf "(%a,`$%s)" Print.print s v
) ppf (bindings m);
end
(* equation set : (s < alpha < t) stored as ( alpha -> (s,t) ) *)
module E = Map.Make(struct
type t = Custom.var
let compare = Pervasives.compare
end)
module E = struct
include Map.Make(struct
type t = Var.var
let compare = Pervasives.compare
end)
let print ppf e =
print_lst (fun ppf -> fun (`Var v,t) ->
Format.fprintf ppf "`$%s = %a@," v Print.print t
) ppf (bindings e)
type cs = S.t
type c = S.elt
end
(* Set of constraint sets *)
module S = struct
include Set.Make(struct
type t = Descr.s M.t
let compare = M.compare Descr.compare
end)
let print ppf s = print_lst M.print ppf (elements s)
end
type s = S.t
type m = Descr.s M.t
type e = Descr.s E.t
let singleton (b,v,s) =
S.singleton (M.singleton (b,v) s)
let print = S.print
let print_m = M.print
let print_e = E.print
let merge m1 m2 =
let f k v1 v2 = match (k,v1,v2) with
|(k,None,None) -> None
......@@ -2241,27 +2273,6 @@ module Tallying = struct
in
M.merge f m1 m2
let print ppf s =
let print_lst f ppf l =
let rec aux ppf = function
|[] -> Format.fprintf ppf "@."
|[h] -> Format.fprintf ppf "%a@." f h
|h::t -> Format.fprintf ppf "%a ,%a" f h aux t
in
match l with
|[] -> Format.fprintf ppf "{}"
|_ -> Format.fprintf ppf "{ %a }" aux l
in
print_lst (fun ppf -> fun m ->
print_lst (fun ppf -> fun ((b,`Var v),s) ->
if b then
Format.fprintf ppf "(`$%s,%a)" v Print.print s
else
Format.fprintf ppf "(%a,`$%s)" Print.print s v
) ppf (M.bindings m);
) ppf (S.elements s)
let sat = S.singleton M.empty
let unsat = S.empty
let cup = S.union
......@@ -2286,7 +2297,7 @@ module Tallying = struct
let aux f constr acc l =
List.fold_left (fun acc ->
function
|`Var a -> cap acc (f(vars a))
|`Var a -> cap acc (f(var (`Var a)))
|`Atm a -> cap acc (f(constr a))
) acc l
in
......@@ -2443,70 +2454,73 @@ module Tallying = struct
let norm t = norm (t,DescrSet.empty)
let rec merge (cs,mem) =
let aux (b,v) s =
let rec merge (m,mem) =
let aux (b,v) s m =
try
let t = CS.M.find (not b,v) cs in
let t = CS.M.find (not b,v) m in
let x = if b then diff t s else diff s t in
if DescrSet.mem x mem then None
else
let c1 = CS.cap (CS.S.singleton cs) (norm x) in
let c2 = CS.S.fold (fun m acc -> CS.cup acc (merge (m,DescrSet.add x mem))) c1 CS.S.empty in
let c1 = CS.cap (CS.S.singleton m) (norm x) in
let c2 = CS.S.fold (fun m1 acc -> CS.cup acc (merge (m1,DescrSet.add x mem))) c1 CS.S.empty in
Some c2
with Not_found -> None
in
let s =
let mm =
CS.M.fold (fun (b,v) s acc ->
match aux (b,v) s with
match aux (b,v) s m with
|None -> acc
|Some c -> CS.cup c acc
) cs CS.S.empty
in if CS.S.is_empty s then CS.S.singleton cs else s
let merge c = try merge (c,DescrSet.empty) with UnSatConstr -> CS.unsat
(*
CS.S.fold (fun c acc -> CS.cup acc (merge (c,DescrSet.empty))) cs CS.S.empty
*)
) m CS.S.empty
in
if CS.S.is_empty mm then CS.S.singleton m else mm
(*
let solve cs =
CS.M.fold (fun (b,v) s acc -> match (b,v) with
|(true,v) ->
try
let t = CS.M.find (false,v) cs in
let b = fresh () in
CS.E.add v ((cup s b) cap t) acc
with Not_found ->
let b = fresh () in
CS.E.add v (cup s b)
|(false,v) ->
(* merge and solve *)
let merge m =
let aux v (s,t) acc =
let b = var (Var.fresh ()) in
CS.E.add v (cap (cup s b) t) acc
in
let solve m =
CS.M.fold (fun (b,v) s acc ->
try
let t = CS.M.find (not b,v) m in
(*
try
let t = CS.M.find (true,v) cs in
let b = fresh () in
CS.E.add v ((cup t b) cap s) acc
with Not_found ->
let b = fresh () in
CS.E.add v (cap s b)
) cs CS.E.empty
let z = justavar t in
let acc1 = CS.E.add z (if b then (any,s) else (s,empty)) acc in
CS.E.add v (if b then (any,t) else (t,empty)) acc1
with Not_found ->
*)
if b then aux v (t,s) acc else aux v (s,t) acc
with Not_found ->
if b then aux v (any,s) acc else aux v (s,empty) acc
) m CS.E.empty
in
try
let l = merge (m,DescrSet.empty) in
CS.S.fold (fun m acc -> (solve m)::acc) l []
with UnSatConstr -> []
(*
let unify e =
let aux acc e =
if CS.E.is_empty then []
if CS.E.is_empty e then []
else
let (a,t) = CS.E.pop e in
let e1 = CS.E.remove (a,t) e in
let (v,t) = CS.E.pop e in
let e1 = CS.E.remove (v,t) e in
let x = fresh () in
(* replace in e1 all occurrences of a by ... *)
aux (t,a,x)::acc (subst e1 t a x)
in
aux e
*)
let tallying l =
let n = List.fold_left (fun acc (s,t) -> CS.cap acc (norm(diff s t))) CS.S.empty l in
let m = CS.S.fold (fun c acc -> CS.cup acc (merge (c))) n CS.S.empty in
m
(*
let s = CS.S.fold (fun c acc -> CS.cup acc (solve (c))) m CS.S.empty in
CS.S.fold (fun c acc -> CS.cup acc (unify(c))) s CS.S.empty
let m = CS.S.fold (fun c acc -> acc @ (merge (c))) n [] in
m
(*
List.fold_left (fun acc e -> (unify e)::acc) [] m
*)
end
......@@ -2,18 +2,17 @@ open Ident
module BoolAtoms : BoolVar.S with
type s = Atoms.t and
type elem = Atoms.t Custom.pairvar
type elem = Atoms.t Var.pairvar
module BoolIntervals : BoolVar.S with
type s = Intervals.t and
type elem = Intervals.t Custom.pairvar
type elem = Intervals.t Var.pairvar
module BoolChars : BoolVar.S with
type s = Chars.t and
type elem = Chars.t Custom.pairvar
type elem = Chars.t Var.pairvar
type const =
| Integer of Intervals.V.t
| Atom of Atoms.V.t
| Var of BoolVar.Vars.V.t
| Char of Chars.V.t
| Pair of const * const
| Xml of const * const
......@@ -86,10 +85,10 @@ include Custom.T
module Node : Custom.T
module Pair : Bool.S with type elem = (Node.t * Node.t)
module BoolPair : BoolVar.S with type s = Pair.t and type elem = Pair.t Custom.pairvar
module BoolPair : BoolVar.S with type s = Pair.t and type elem = Pair.t Var.pairvar
module Rec : Bool.S with type elem = bool * Node.t Ident.label_map
module BoolRec : BoolVar.S with type s = Rec.t and type elem = Rec.t Custom.pairvar
module BoolRec : BoolVar.S with type s = Rec.t and type elem = Rec.t Var.pairvar
type descr = t
......@@ -121,6 +120,7 @@ val non_constructed_or_absent : t
type pair_kind = [ `Normal | `XML ]
val var : Var.var -> t
val interval : Intervals.t -> t
val atom : Atoms.t -> t
val times : Node.t -> Node.t -> t
......@@ -348,26 +348,41 @@ module Cache : sig
end
module Tallying : sig
type constr = (bool * Custom.var * t)
type constr = (bool * Var.var * t)
module CS : sig
type key = (bool * Custom.var)
module M : Map.S with type key = key
module S : Set.S with type elt = t M.t
type cs = S.t
type c = S.elt
val print : Format.formatter -> S.t -> unit
val merge : S.elt -> S.elt -> S.elt
val singleton : constr -> cs
val sat : cs
val unsat : cs
val cup : cs -> cs -> cs
val cap : cs -> cs -> cs
module M : sig
include Map.S with type key = (bool * Var.var)
val print : Format.formatter -> descr t -> unit
end
module E : sig
include Map.S with type key = Var.var
val print : Format.formatter -> descr t -> unit
end
module S : sig
include Set.S with type elt = descr M.t
val print : Format.formatter -> t -> unit
end
type s = S.t
type m = t M.t
type e = t E.t
val print : Format.formatter -> s -> unit
val print_m : Format.formatter -> m -> unit
val print_e : Format.formatter -> e -> unit
val merge : m -> m -> m
val singleton : constr -> s
val sat : s
val unsat : s
val cup : s -> s -> s
val cap : s -> s -> s
end
val norm : t -> CS.cs
val merge : CS.c -> CS.cs
val tallying : (t * t) list -> CS.cs
val norm : t -> CS.s
val merge : CS.m -> CS.e list
val tallying : (t * t) list -> CS.e list
end
type t = String.t
type var = [ `Var of t ]
type 'a pairvar = [ `Atm of 'a | var ]
module Make (X : Custom.T) = struct
type t = X.t pairvar
let hash = function `Atm t -> X.hash t | `Var s -> Hashtbl.hash (`Var s)
let check = function `Atm t -> X.check t | `Var _ -> ()
let compare t1 t2 =
match t1,t2 with
|`Atm x, `Atm y -> X.compare x y
|`Var x, `Var y when x = y -> 0
(* HACK fix BoolVar.get to get variables in the correct order *)
|`Var x, `Var y -> if String.compare x y = -1 then 1 else -1
|`Var _, `Atm _ -> -1
|`Atm _, `Var _ -> 1
let equal t1 t2 = (compare t1 t2) = 0
let dump ppf = function
|`Atm x -> X.dump ppf x
|`Var x -> Format.fprintf ppf "`$%s" x
end
let fresh : unit -> var =
let counter = ref 0 in
fun _ ->
let v = `Var (Printf.sprintf "_fresh_%d" !counter) in
incr counter;
v
......@@ -7,6 +7,7 @@ State
Pool
Ns
SortedList
Var
Atoms
Bool
Chars
......
......@@ -173,7 +173,6 @@ let rec const env loc = function
| RecordLitt x -> Types.Record (parse_record env loc (const env loc) x)
| String (i,j,s,c) -> Types.String (i,j,s,const env loc c)
| Atom t -> Types.Atom (parse_atom env loc t)
| TVar t -> Types.Var t
| Integer i -> Types.Integer i
| Char c -> Types.Char c
| Const c -> c
......@@ -240,8 +239,6 @@ let type_ns env loc p ns =
ns = Ns.add_prefix p ns env.ns;
ids = Env.add (Ns.empty,p) (ENamespace ns) env.ids }
let find_global_type env loc ids =
match find_global env loc ids with
| Type t | ESchemaComponent (t,_) -> t
......@@ -252,7 +249,6 @@ let find_global_schema_component env loc ids =
| ESchemaComponent c -> c
| _ -> error loc "This path does not refer to a schema component"
let find_local_type env loc id =
match Env.find id env.ids with
| Type t -> t
......@@ -314,6 +310,7 @@ module IType = struct
List.iter check_one_delayed l
let rec derecurs env p = match p.descr with
| TVar v -> mk_type (Types.var (`Var v))
| PatVar ids -> derecurs_var env p.loc ids
| Recurs (p,b) -> derecurs (fst (derecurs_def env b)) p
| Internal t -> mk_type t
......@@ -522,7 +519,7 @@ let rec expr env loc = function
| _ ->
exp loc fv (Typed.Apply (e1,e2)))
| Abstraction a -> abstraction env loc a
| (Integer _ | Char _ | Atom _ | Const _ | TVar _) as c ->
| (Integer _ | Char _ | Atom _ | Const _ ) as c ->
exp loc Fv.empty (Typed.Cst (const env loc c))
| Pair (e1,e2) ->
let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
......@@ -920,8 +917,12 @@ and type_check' loc env e constr precise = match e with
| Var s ->
verify loc (find_value s env) constr
| TVar s ->
verify loc (find_value s env) constr
| ExtVar (cu,s,t) ->
verify loc t constr
| Cst c ->
verify loc (Types.constant c) constr
......
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