748f87636a
checkpoint failing test after fixing tests checkpoint checkpoint checkpoint re-work asd checkpoint checkpoint checkpoint mix proj checkpoint mix first parser impl checkpoint fix tests re-org parser checkpoint strings fix multiline strings tuples checkpoint maps checkpoint checkpoint checkpoint checkpoint fix weird eof expression parse error checkpoint before typing checkpoint checpoint checkpoint checkpoint checkpoint ids in primitive types checkpoint checkpoint fix tests initial annotation checkpoint checkpoint checkpoint union subtyping conventions refactor - split typer typing tuples checkpoint test refactor checkpoint test refactor parsing atoms checkpoint atoms wip lists checkpoint typing lists checkopint checkpoint wip fixing correct list typing map discussion checkpoint map basic typing fix tests checkpoint checkpoint checkpoint checkpoint fix condition typing fix literal keys in map types checkpoint union types checkpoint union type checkpoint row types discussion & bidirectional typecheck checkpoint basic lambdas checkpoint lambdas typing application wip function application checkpoint checkpoint checkpoint cduce checkpoint checkpoint checkpoint checkpoint checkpoint checkpoint checkpoint
192 KiB
192 KiB
CDuce Source Code Reference
Below is the full content of relevant CDuce source files for context.
types/bdd.ml
type 'a line = 'a list * 'a list
type 'a dnf = 'a line list
type ('elem, 'leaf) bdd =
| False
| True
| Leaf of 'leaf
| Split of
int * 'elem * ('elem, 'leaf) bdd * ('elem, 'leaf) bdd * ('elem, 'leaf) bdd
let empty = False
type 'atom var_bdd = (Var.t, ('atom, bool) bdd) bdd
(* Ternary decision diagrams:
False → 𝟘
True → 𝟙
Leaf (v) → ⟦ v ⟧
Split (h, x, p, i, n) →
(⟦ x ⟧ ∩ ⟦ p ⟧) ∪ ⟦ i ⟧ ∪ (⟦ n ⟧ \ ⟦ x ⟧)
Invariants maintained (see simplify split and leaf smart constructors and simplify functions:)
- p ≠ n
- ∀ i st. t ≡ Split (h, x, p, Split (…, Split (_, _, i, _) …), n), p ≠ i
Indeed, given the equation above, if some bdd is in ⟦ i ⟧, it can be removed,
from ⟦ p ⟧ and ⟦ n ⟧ safely. A corollary is that if ⟦ i ⟧ contains True, both p and
n are useless, and therefore the whole bdd is replaced by true.
- if t ≡ Leaf (v), ⟦ v ⟧ ≠ 𝟘 and ⟦ v ⟧ ≠ 𝟙
(if v is recursively a bdd of atoms (while t is a bdd of variables) then
it means that v is not trivially False or True, but it could be a complex
bdd that is in fine equal to True, but we would need subtyping to decide this).
*)
module MK
(E : Custom.T) (Leaf : sig
include Tset.S
val iter : (elem -> unit) -> t -> unit
end) =
struct
type elem = E.t
type t = (E.t, Leaf.t) bdd
let test x =
match x with
| Leaf l -> Leaf.test l
| _ -> Tset.Unknown
let rec equal a b =
a == b
||
match (a, b) with
| Split (h1, x1, p1, i1, n1), Split (h2, x2, p2, i2, n2) ->
h1 == h2 && E.equal x1 x2 && equal p1 p2 && equal i1 i2 && equal n1 n2
| Leaf l1, Leaf l2 -> Leaf.equal l1 l2
| _ -> false
let rec compare a b =
if a == b then 0
else
match (a, b) with
| Split (h1, x1, p1, i1, n1), Split (h2, x2, p2, i2, n2) ->
if h1 < h2 then -1
else if h1 > h2 then 1
else
let c = E.compare x1 x2 in
if c <> 0 then c
else
let c = compare p1 p2 in
if c <> 0 then c
else
let c = compare i1 i2 in
if c <> 0 then c else compare n1 n2
| Leaf l1, Leaf l2 -> Leaf.compare l1 l2
| True, _ -> -1
| _, True -> 1
| False, _ -> -1
| _, False -> 1
| Leaf _, Split _ -> 1
| Split _, Leaf _ -> -1
let hash = function
| False -> 0
| True -> 1
| Leaf l -> 17 * Leaf.hash l
| Split (h, _, _, _, _) -> h
let compute_hash x p i n =
let h = E.hash x in
let h = h lxor (257 * hash p) in
let h = h lxor (8191 * hash i) in
let h = h lxor (16637 * hash n) in
h
let rec check = function
| True
| False ->
()
| Leaf l -> Leaf.check l
| Split (h, x, p, i, n) ->
assert (h = compute_hash x p i n);
(match p with
| Split (_, y, _, _, _) -> assert (E.compare x y < 0)
| _ -> ());
(match i with
| Split (_, y, _, _, _) -> assert (E.compare x y < 0)
| _ -> ());
(match n with
| Split (_, y, _, _, _) -> assert (E.compare x y < 0)
| _ -> ());
E.check x;
check p;
check i;
check n
let any = True
let empty = empty
let leaf l =
match Leaf.test l with
| Tset.Empty -> empty
| Tset.Full -> any
| _ -> Leaf l
let rec iter_partial fe fleaf = function
| Split (_, x, p, i, n) ->
fe x;
iter_partial fe fleaf p;
iter_partial fe fleaf i;
iter_partial fe fleaf n
| Leaf leaf -> fleaf leaf
| _ -> ()
let iter_full fe fl = iter_partial fe (Leaf.iter fl)
let rec dump s ppf = function
| False -> Format.fprintf ppf "F"
| True -> Format.fprintf ppf "T"
| Leaf l -> Format.fprintf ppf "%s%a" s Leaf.dump l
| Split (_, x, p, i, n) ->
Format.fprintf ppf "@[%s%a@[(@[%a@],@,@[%a@],@,@[%a@])@]@]" s E.dump x
(dump "+") p (dump "=") i (dump "-") n
let dump ppf a = (dump "") ppf a
let rec get accu pos neg = function
| False -> accu
| True -> ((pos, neg), Leaf.any) :: accu
| Leaf leaf -> ((pos, neg), leaf) :: accu
| Split (_, x, p, i, n) ->
(*OPT: can avoid creating this list cell when pos or neg =False *)
let accu = get accu (x :: pos) neg p in
let accu = get accu pos (x :: neg) n in
let accu = get accu pos neg i in
accu
let get (l : t) = get [] [] [] l
let compute_full ~empty ~any ~cup ~cap ~diff ~atom ~leaf b =
let rec aux t =
match t with
| False -> empty
| True -> any
| Leaf l -> leaf l
| Split (_, x, p, i, n) ->
let atx = atom x in
let p = cap atx (aux p)
and i = aux i
and n = diff (aux n) atx in
cup (cup p i) n
in
aux b
let split0 x pos ign neg = Split (compute_hash x pos ign neg, x, pos, ign, neg)
let atom x = split0 x any empty empty
(* Smart constructor for split, ensures that the envariants are preserved
with the use of simplify *)
let rec split x p i n =
if i == True then any
else if equal p n then if equal p i then p else p ++ i
else
let p = simplify p [ i ]
and n = simplify n [ i ] in
if equal p n then if equal p i then p else p ++ i else split0 x p i n
(* ensures that a does not contain any of the bdds in l,
if it does, replace it does, remove it. *)
and simplify a l =
match a with
| False -> empty
| Split (_, x, p, i, n) -> restrict_from_list a x p i n [] [] [] False l
| _ -> restrict_true_or_same a l
and restrict_true_or_same a = function
| [] -> a
| True :: _ -> empty
| b :: l -> if equal a b then empty else restrict_true_or_same a l
(* traverses a list of bdds b and
accumulate in ap ai an those that might be present in each
component p, i, n of a (a ≡ Split (h, x, p, i, n)) the arguments
are passed to avoid reconstructing it.
The _dummy argument keeps the arguments of both functions
in the same order which prevent ocaml from spilling too much on the stack.
*)
and restrict_from_list a x p i n ap ai an _dummy = function
| [] ->
let p = simplify p ap
and n = simplify n an
and i = simplify i ai in
if equal p n then p ++ i else split0 x p i n
| b :: l -> restrict_elem a x p i n ap ai an b l
and restrict_elem a x p i n ap ai an b l =
match b with
| False -> restrict_from_list a x p i n ap ai an b l
| True -> empty
| Leaf _ as b ->
(* inline then next case, knowing that a = Split ...
and b is Leaf b is greater*)
restrict_from_list a x p i n (b :: ap) (b :: ai) (b :: an) b l
| Split (_, x2, p2, i2, n2) as b ->
let c = E.compare x2 x in
if c < 0 then restrict_elem a x p i n ap ai an i2 l
else if c > 0 then
restrict_from_list a x p i n (b :: ap) (b :: ai) (b :: an) b l
else if equal a b then empty
else
restrict_from_list a x p i n (p2 :: i2 :: ap) (i2 :: ai)
(n2 :: i2 :: an) b l
and ( ++ ) a b =
if a == b then a
else
match (a, b) with
| True, _
| _, True ->
any
| False, _ -> b
| _, False -> a
| Leaf l1, Leaf l2 -> leaf (Leaf.cup l1 l2)
| Split (_, x1, p1, i1, n1), Split (_, x2, p2, i2, n2) ->
let c = E.compare x1 x2 in
if c = 0 then split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
else if c < 0 then split x1 p1 (i1 ++ b) n1
else split x2 p2 (i2 ++ a) n2
| Split (_, x1, p1, i1, n1), Leaf _ -> split x1 p1 (i1 ++ b) n1
| Leaf _, Split (_, x2, p2, i2, n2) -> split x2 p2 (i2 ++ a) n2
let rec ( ** ) a b =
if a == b then a
else
match (a, b) with
| False, _
| _, False ->
empty
| True, _ -> b
| _, True -> a
| Leaf l1, Leaf l2 -> leaf (Leaf.cap l1 l2)
| Split (_, x1, p1, i1, n1), Split (_, x2, p2, i2, n2) ->
let c = E.compare x1 x2 in
if c = 0 then
split x1
((p1 ** (p2 ++ i2)) ++ (p2 ** i1))
(i1 ** i2)
((n1 ** (n2 ++ i2)) ++ (n2 ** i1))
else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b)
else split x2 (p2 ** a) (i2 ** a) (n2 ** a)
| Split (_, x1, p1, i1, n1), Leaf _ ->
split x1 (p1 ** b) (i1 ** b) (n1 ** b)
| Leaf _, Split (_, x2, p2, i2, n2) ->
split x2 (p2 ** a) (i2 ** a) (n2 ** a)
let rec neg = function
| False -> any
| True -> empty
| Leaf l -> leaf (Leaf.neg l)
| Split (_, x, p, i, False) -> split x empty (neg (i ++ p)) (neg i)
| Split (_, x, False, i, n) -> split x (neg i) (neg (i ++ n)) empty
| Split (_, x, p, False, n) -> split x (neg p) (neg (p ++ n)) (neg n)
| Split (_, x, p, i, n) -> neg i ** split x (neg p) (neg (p ++ n)) (neg n)
let rec ( // ) a b =
if a == b then empty
else
match (a, b) with
| False, _
| _, True ->
empty
| _, False -> a
| True, _ -> neg b
| Leaf l1, Leaf l2 -> leaf (Leaf.diff l1 l2)
| Split (_, x1, p1, i1, n1), Split (_, x2, p2, i2, n2) ->
let c = E.compare x1 x2 in
if c = 0 then
if i2 == empty && n2 == empty then
split x1 (p1 // p2) (i1 // p2) (n1 ++ i1)
else
split x1
((p1 ++ i1) // (p2 ++ i2))
empty
((n1 ++ i1) // (n2 ++ i2))
else if c < 0 then split x1 (p1 // b) (i1 // b) (n1 // b)
else split x2 (a // (i2 ++ p2)) empty (a // (i2 ++ n2))
| _ -> a ** neg b
let ( ~~ ) = neg
let cup = ( ++ )
let cap = ( ** )
let diff = ( // )
let extract_var = function
| Split
( _,
v,
((False | True | Leaf _) as p),
((False | True | Leaf _) as i),
((False | True | Leaf _) as n) ) ->
Some (v, p, i, n)
| _ -> None
end
module Bool : sig
include Tset.S with type t = bool and type elem = bool
val iter : (elem -> unit) -> t -> unit
end = struct
include Custom.Bool
type elem = bool
let empty = false
let any = true
let test (x : bool) : Tset.cardinal = Obj.magic x
let atom b = b
let cup a b = a || b
let cap a b = a && b
let neg a = not a
let diff a b = a && not b
let iter _ _ = ()
end
module type S = sig
type atom
(** The type of atoms in the Boolean combinations *)
type mono
(** The type of Boolean combinations of atoms. *)
include Custom.T with type t = (Var.t, mono) bdd
type line
(** An explicit representation of conjunctions of atoms. *)
type dnf
(** An explicit representation fo the DNF. *)
val atom : atom -> t
val mono : mono -> t
val mono_dnf : mono -> dnf
val any : t
val empty : t
val cup : t -> t -> t
val cap : t -> t -> t
val diff : t -> t -> t
val neg : t -> t
val get : t -> dnf
val get_mono : t -> mono
val iter : (atom -> unit) -> t -> unit
val compute :
empty:'b ->
any:'b ->
cup:('b -> 'b -> 'b) ->
cap:('b -> 'b -> 'b) ->
diff:('b -> 'b -> 'b) ->
atom:(atom -> 'b) ->
t ->
'b
val var : Var.t -> t
val extract_var : t -> (Var.t * t * t * t) option
(** {2 Polymorphic interface. }*)
val get_partial : t -> ((Var.t list * Var.t list) * mono) list
val get_full : t -> ((Var.t list * Var.t list) * line) list
val iter_partial : (Var.t -> unit) -> (mono -> unit) -> t -> unit
val iter_full : (Var.t -> unit) -> (atom -> unit) -> t -> unit
val compute_partial :
empty:'b ->
any:'b ->
cup:('b -> 'b -> 'b) ->
cap:('b -> 'b -> 'b) ->
diff:('b -> 'b -> 'b) ->
mono:(mono -> 'b) ->
var:(Var.t -> 'b) ->
t ->
'b
val compute_full :
empty:'b ->
any:'b ->
cup:('b -> 'b -> 'b) ->
cap:('b -> 'b -> 'b) ->
diff:('b -> 'b -> 'b) ->
atom:(atom -> 'b) ->
var:(Var.t -> 'b) ->
t ->
'b
val ( ++ ) : t -> t -> t
val ( ** ) : t -> t -> t
val ( // ) : t -> t -> t
val ( ~~ ) : t -> t
end
module Make (E : Custom.T) :
S
with type atom = E.t
and type line = E.t list * E.t list
and type dnf = (E.t list * E.t list) list
and type mono = (E.t, Bool.t) bdd = struct
module Atom = MK (E) (Bool)
type atom = E.t
type mono = (E.t, Bool.t) bdd
include
MK
(Var)
(struct
include Atom
let iter f b = iter_full f ignore b
end)
type line = E.t list * E.t list
type dnf = (E.t list * E.t list) list
let var x = atom x
let atom x = leaf (Atom.atom x)
let mono x = leaf x
let get_aux combine acc b =
List.fold_left
(fun acc ((p, n), dnf) ->
let p = List.rev p in
let n = List.rev n in
let dnf = Atom.get dnf in
List.fold_left
(fun acc ((p2, n2), b) -> if b then combine p n p2 n2 acc else acc)
acc dnf)
acc (get b)
let get_full = get_aux (fun p n p2 n2 acc -> ((p, n), (p2, n2)) :: acc) []
let mono_dnf mono =
let l = Atom.get mono in
List.map fst l
let get_partial b : ((Var.t list * Var.t list) * mono) list =
List.rev_map (fun ((p, n), m) -> ((List.rev p, List.rev n), m)) (get b)
let get b = get_aux (fun _ _ p2 n2 acc -> (p2, n2) :: acc) [] b
let get_mono b : mono =
List.fold_left
(fun acc (_, dnf) -> Atom.cup acc dnf)
Atom.empty (get_partial b)
(* Temporary List.rev to order elements as before introduction of
polymorphic variables.
*)
let iter = iter_full (fun _ -> ())
let compute_partial ~empty ~any ~cup ~cap ~diff ~mono ~(var : Var.t -> 'a) b =
compute_full ~empty ~any ~cup ~cap ~diff ~atom:var ~leaf:mono b
let compute_full ~empty ~any ~cup ~cap ~diff ~atom ~(var : Var.t -> 'a) b =
compute_full ~empty ~any ~cup ~cap ~diff ~atom:var
~leaf:
(Atom.compute_full ~empty ~any ~cup ~cap ~diff ~atom ~leaf:(function
| false -> empty
| true -> any))
b
let compute ~empty ~any ~cup ~cap ~diff ~atom b =
compute_full ~empty ~any ~cup ~cap ~diff ~atom ~var:(fun _ -> any) b
end
module MKBasic (T : Tset.S) :
S with type atom = T.elem and type mono = T.t and type dnf = T.t = struct
type atom = T.elem
type mono = T.t
include
MK
(Var)
(struct
include T
let iter _ _ = assert false
end)
type line
type dnf = T.t
let var v = atom v
let mono x = leaf x
let atom x = leaf (T.atom x)
let get_partial t =
List.map (fun ((p, n), m) -> ((List.rev p, List.rev n), m)) (get t)
let mono_dnf x = x
let get_mono t =
List.fold_left (fun acc ((_, _), dnf) -> T.cup acc dnf) T.empty (get t)
let get _ = assert false
let get_full _ = assert false
let compute_partial ~empty ~any ~cup ~cap ~diff ~mono ~var b =
compute_full ~empty ~any ~cup ~cap ~diff ~atom:var ~leaf:mono b
let[@ocaml.warning "-27"] compute_full
~empty
~any
~cup
~cap
~diff
~atom
~var
b =
assert false
let[@ocaml.warning "-27"] compute ~empty ~any ~cup ~cap ~diff ~atom b =
assert false
let iter _ _ = assert false
let iter_full _ _ _ = assert false
end
module VarIntervals = MKBasic (Intervals)
module VarCharSet = MKBasic (CharSet)
module VarAtomSet = MKBasic (AtomSet)
module VarAbstractSet = MKBasic (AbstractSet)
types/types.ml
let std_compare = compare
open Ident
module U = Encodings.Utf8
let count = ref 0
let () =
Stats.register Stats.Summary (fun ppf ->
Format.fprintf ppf "Allocated type nodes:%i@\n" !count)
(*
To be sure not to use generic comparison ...
*)
let ( = ) : int -> int -> bool = ( == )
let ( < ) : int -> int -> bool = ( < )
let[@ocaml.warning "-32"] ( <= ) : int -> int -> bool = ( <= )
let[@ocaml.warning "-32"] ( <> ) : int -> int -> bool = ( <> )
let[@ocaml.warning "-32"] compare = 1
type const =
| Integer of Intervals.V.t
| Atom of AtomSet.V.t
| Char of CharSet.V.t
| Pair of const * const
| Xml of const * const
| Record of const label_map
| String of U.uindex * U.uindex * U.t * const
module Const = struct
type t = const
let check _ = ()
let dump ppf _ = Format.fprintf ppf "<Types.Const.t>"
let rec compare c1 c2 =
match (c1, c2) with
| Integer x, Integer y -> Intervals.V.compare x y
| Integer _, _ -> -1
| _, Integer _ -> 1
| Atom x, Atom y -> AtomSet.V.compare x y
| Atom _, _ -> -1
| _, Atom _ -> 1
| Char x, Char y -> CharSet.V.compare x y
| Char _, _ -> -1
| _, Char _ -> 1
| Pair (x1, x2), Pair (y1, y2) ->
let c = compare x1 y1 in
if c <> 0 then c else compare x2 y2
| Pair (_, _), _ -> -1
| _, Pair (_, _) -> 1
| Xml (x1, x2), Xml (y1, y2) ->
let c = compare x1 y1 in
if c <> 0 then c else compare x2 y2
| Xml (_, _), _ -> -1
| _, Xml (_, _) -> 1
| Record x, Record y -> LabelMap.compare compare x y
| Record _, _ -> -1
| _, Record _ -> 1
| String (i1, j1, s1, r1), String (i2, j2, s2, r2) ->
let c = std_compare i1 i2 in
if c <> 0 then c
else
let c = std_compare j1 j2 in
if c <> 0 then c
else
let c = U.compare s1 s2 in
if c <> 0 then c
(* Should compare
only the substring *)
else compare r1 r2
let rec hash = function
| Integer x -> 1 + (17 * Intervals.V.hash x)
| Atom x -> 2 + (17 * AtomSet.V.hash x)
| Char x -> 3 + (17 * CharSet.V.hash x)
| Pair (x, y) -> 4 + (17 * hash x) + (257 * hash y)
| Xml (x, y) -> 5 + (17 * hash x) + (257 * hash y)
| Record x -> 6 + (17 * LabelMap.hash hash x)
| String (_, _, s, r) -> 7 + (17 * U.hash s) + (257 * hash r)
(* Note: improve hash for String *)
let equal c1 c2 = compare c1 c2 = 0
end
type pair_kind =
[ `Normal
| `XML
]
type descr = {
atoms : Bdd.VarAtomSet.t;
ints : Bdd.VarIntervals.t;
chars : Bdd.VarCharSet.t;
times : (node * node) Bdd.var_bdd;
xml : (node * node) Bdd.var_bdd;
arrow : (node * node) Bdd.var_bdd;
record : (bool * node label_map) Bdd.var_bdd;
abstract : Bdd.VarAbstractSet.t;
absent : bool;
mutable hash : int;
}
and node = {
id : int;
cu : Compunit.t;
mutable descr : descr;
}
let empty =
{
atoms = Bdd.empty;
ints = Bdd.empty;
chars = Bdd.empty;
times = Bdd.empty;
xml = Bdd.empty;
arrow = Bdd.empty;
record = Bdd.empty;
abstract = Bdd.empty;
absent = false;
hash = -1;
}
let todo_dump = Hashtbl.create 16
let forward_print = ref (fun _ _ -> assert false)
module Node = struct
type t = node
let check _ = ()
let dump ppf n =
if not (Hashtbl.mem todo_dump n.id) then
Hashtbl.add todo_dump n.id (n, false);
Format.fprintf ppf "X%i" n.id
let hash x = x.id + Compunit.hash x.cu
let compare x y =
let c = x.id - y.id in
if c = 0 then Compunit.compare x.cu y.cu else c
let equal x y = x == y || (x.id == y.id && Compunit.equal x.cu y.cu)
let mk id d = { id; cu = Compunit.current (); descr = d }
end
module BoolPair = Bdd.Make (Custom.Pair (Node) (Node))
module BoolRec = Bdd.Make (Custom.Pair (Custom.Bool) (LabelSet.MakeMap (Node)))
module Descr = struct
type t = descr
let _print_lst ppf =
List.iter (fun f ->
f ppf;
Format.fprintf ppf " |")
let hash a =
if a.hash >= 0 then a.hash
else
let accu = Bdd.VarCharSet.hash a.chars in
let accu = accu + (accu lsl 4) + Bdd.VarIntervals.hash a.ints in
let accu = accu + (accu lsl 4) + Bdd.VarAtomSet.hash a.atoms in
let accu = accu + (accu lsl 4) + BoolPair.hash a.times in
let accu = accu + (accu lsl 4) + BoolPair.hash a.xml in
let accu = accu + (accu lsl 4) + BoolPair.hash a.arrow in
let accu = accu + (accu lsl 4) + BoolRec.hash a.record in
let accu = accu + (accu lsl 4) + Bdd.VarAbstractSet.hash a.abstract in
let accu = if a.absent then accu + 5 else accu in
let accu = max_int land accu in
let () = a.hash <- accu in
accu
let equal a b =
a == b
|| hash a == hash b
&& Bdd.VarAtomSet.equal a.atoms b.atoms
&& Bdd.VarCharSet.equal a.chars b.chars
&& Bdd.VarIntervals.equal a.ints b.ints
&& BoolPair.equal a.times b.times
&& BoolPair.equal a.xml b.xml
&& BoolPair.equal a.arrow b.arrow
&& BoolRec.equal a.record b.record
&& Bdd.VarAbstractSet.equal a.abstract b.abstract
&& a.absent == b.absent
let compare a b =
if a == b then 0
else
let c = Bdd.VarAtomSet.compare a.atoms b.atoms in
if c <> 0 then c
else
let c = Bdd.VarCharSet.compare a.chars b.chars in
if c <> 0 then c
else
let c = Bdd.VarIntervals.compare a.ints b.ints in
if c <> 0 then c
else
let c = BoolPair.compare a.times b.times in
if c <> 0 then c
else
let c = BoolPair.compare a.xml b.xml in
if c <> 0 then c
else
let c = BoolPair.compare a.arrow b.arrow in
if c <> 0 then c
else
let c = BoolRec.compare a.record b.record in
if c <> 0 then c
else
let c = Bdd.VarAbstractSet.compare a.abstract b.abstract in
if c <> 0 then c else Bdd.Bool.compare a.absent b.absent
let check a =
Bdd.VarCharSet.check a.chars;
Bdd.VarIntervals.check a.ints;
Bdd.VarAtomSet.check a.atoms;
BoolPair.check a.times;
BoolPair.check a.xml;
BoolPair.check a.arrow;
BoolRec.check a.record;
Bdd.VarAbstractSet.check a.abstract;
()
let forward_any = ref empty
let dump_descr ppf d =
if equal d empty then Format.fprintf ppf "EMPTY"
else if equal d !forward_any then Format.fprintf ppf "ANY"
else
Format.fprintf ppf
"<@[types = @[%a@]@\n\
\ ints(@[%a@])@\n\
\ atoms(@[%a@])@\n\
\ chars(@[%a@])@\n\
\ abstract(@[%a@])@\n\
\ times(@[%a@])@\n\
\ xml(@[%a@])@\n\
\ record(@[%a@])@\n\
\ arrow(@[%a@])@\n\
\ absent=%b@]>" !forward_print d Bdd.VarIntervals.dump d.ints
Bdd.VarAtomSet.dump d.atoms Bdd.VarCharSet.dump d.chars
Bdd.VarAbstractSet.dump d.abstract BoolPair.dump d.times BoolPair.dump
d.xml BoolRec.dump d.record BoolPair.dump d.arrow d.absent
let dump ppf d =
Hashtbl.clear todo_dump;
dump_descr ppf d;
let continue = ref true in
let seen_list = ref [] in
while !continue do
continue := false;
Hashtbl.iter
(fun _ (n, seen) ->
if not seen then begin
seen_list := n :: !seen_list;
continue := true
end)
todo_dump;
List.iter
(fun n ->
Hashtbl.replace todo_dump n.id (n, true);
Format.fprintf ppf "@\n%a=@[" Node.dump n;
dump_descr ppf n.descr;
Format.fprintf ppf "@]")
!seen_list;
seen_list := []
done;
Hashtbl.clear todo_dump
end
module DescrHash = Hashtbl.Make (Descr)
module DescrMap = Map.Make (Descr)
module DescrSet = Set.Make (Descr)
module DescrSList = SortedList.Make (Descr)
let dummy_descr =
let () = incr count in
let loop = Node.mk !count empty in
let dummy =
{ empty with times = BoolPair.atom (loop, loop); absent = true; hash = -1 }
in
let () = loop.descr <- dummy in
dummy
let make () =
incr count;
let res = Node.mk !count dummy_descr in
res
let is_opened n = n.descr == dummy_descr
let define n d =
assert (n.descr == dummy_descr);
n.descr <- d
let cons d =
incr count;
Node.mk !count d
let any =
{
times = BoolPair.any;
xml = BoolPair.any;
arrow = BoolPair.any;
record = BoolRec.any;
ints = Bdd.VarIntervals.any;
atoms = Bdd.VarAtomSet.any;
chars = Bdd.VarCharSet.any;
abstract = Bdd.VarAbstractSet.any;
absent = false;
hash = -1;
}
let () = Descr.forward_any := any
module type Kind = sig
module Dnf : Bdd.S
val any : Descr.t
val get : Descr.t -> Dnf.mono
val get_vars : Descr.t -> Dnf.t
val mk : Dnf.t -> Descr.t
val update : Descr.t -> Dnf.t -> Descr.t
end
module Int = struct
module Dnf = Bdd.VarIntervals
let get_vars d = d.ints
let get d = Dnf.get_mono d.ints
let update t c = { t with ints = c; hash = -1 }
let mk c = update empty c
let any = mk (get_vars any)
end
module Abstract = struct
module Dnf = Bdd.VarAbstractSet
let get_vars d = d.abstract
let get d = Dnf.get_mono d.abstract
let update t c = { t with abstract = c; hash = -1 }
let mk c = update empty c
let any = mk (get_vars any)
end
module Atom = struct
module Dnf = Bdd.VarAtomSet
let get_vars d = d.atoms
let get d = Dnf.get_mono d.atoms
let update t c = { t with atoms = c; hash = -1 }
let mk c = update empty c
let any = mk (get_vars any)
end
module Char = struct
module Dnf = Bdd.VarCharSet
let get_vars d = d.chars
let get d = Dnf.get_mono d.chars
let update t c = { t with chars = c; hash = -1 }
let mk c = update empty c
let any = mk (get_vars any)
end
module Times = struct
module Dnf = BoolPair
let get d = Dnf.get_mono d.times
let get_vars d = d.times
let update t c = { t with times = c; hash = -1 }
let mk c = update empty c
let any = mk (get_vars any)
end
module Xml = struct
module Dnf = BoolPair
let get_vars d = d.xml
let get d = Dnf.get_mono (get_vars d)
let update t c = { t with xml = c; hash = -1 }
let mk c = update empty c
let any = mk (get_vars any)
end
module Function = struct
module Dnf = BoolPair
let get_vars d = d.arrow
let get d = Dnf.get_mono (get_vars d)
let update t c = { t with arrow = c; hash = -1 }
let mk c = update empty c
let any = mk (get_vars any)
end
module Rec = struct
module Dnf = BoolRec
let get_vars d = d.record
let get d = Dnf.get_mono (get_vars d)
let update t c = { t with record = c; hash = -1 }
let mk c = update empty c
let any = mk (get_vars any)
end
module Absent = struct
module Dnf = Bdd.Bool
let get d = d.absent
let update t c = { t with absent = c; hash = -1 }
let mk c = update empty c
let any = mk true
end
include Descr
let non_constructed =
{
any with
times = empty.times;
xml = empty.xml;
record = empty.record;
hash = -1;
}
let interval i = Int.mk (Int.Dnf.mono i)
let times x y = Times.mk (Times.Dnf.atom (x, y))
let xml x y = Xml.mk (Xml.Dnf.atom (x, y))
let arrow x y = Function.mk (Function.Dnf.atom (x, y))
let record label t = Rec.mk (Rec.Dnf.atom (true, LabelMap.singleton label t))
let record_fields (x : bool * node Ident.label_map) = Rec.mk (Rec.Dnf.atom x)
let atom a = Atom.mk (Atom.Dnf.mono a)
let char c = Char.mk (Char.Dnf.mono c)
let abstract a = Abstract.mk (Abstract.Dnf.mono a)
let get_abstract = Abstract.get
let var x =
{
times = BoolPair.var x;
xml = BoolPair.var x;
arrow = BoolPair.var x;
record = BoolRec.var x;
ints = Bdd.VarIntervals.var x;
atoms = Bdd.VarAtomSet.var x;
chars = Bdd.VarCharSet.var x;
abstract = Bdd.VarAbstractSet.var x;
absent = false;
hash = -1;
}
let cup x y =
if x == y then x
else
{
times = Times.Dnf.cup x.times y.times;
xml = Xml.Dnf.cup x.xml y.xml;
arrow = Function.Dnf.cup x.arrow y.arrow;
record = Rec.Dnf.cup x.record y.record;
ints = Int.Dnf.cup x.ints y.ints;
atoms = Atom.Dnf.cup x.atoms y.atoms;
chars = Char.Dnf.cup x.chars y.chars;
abstract = Abstract.Dnf.cup x.abstract y.abstract;
absent = Absent.Dnf.cup x.absent y.absent;
hash = -1;
}
let cap x y =
if x == y then x
else
{
times = Times.Dnf.cap x.times y.times;
xml = Xml.Dnf.cap x.xml y.xml;
arrow = Function.Dnf.cap x.arrow y.arrow;
record = Rec.Dnf.cap x.record y.record;
ints = Int.Dnf.cap x.ints y.ints;
atoms = Atom.Dnf.cap x.atoms y.atoms;
chars = Char.Dnf.cap x.chars y.chars;
abstract = Abstract.Dnf.cap x.abstract y.abstract;
absent = Absent.Dnf.cap x.absent y.absent;
hash = -1;
}
let diff x y =
if x == y then empty
else
{
times = Times.Dnf.diff x.times y.times;
xml = Xml.Dnf.diff x.xml y.xml;
arrow = Function.Dnf.diff x.arrow y.arrow;
record = Rec.Dnf.diff x.record y.record;
ints = Int.Dnf.diff x.ints y.ints;
atoms = Atom.Dnf.diff x.atoms y.atoms;
chars = Char.Dnf.diff x.chars y.chars;
abstract = Abstract.Dnf.diff x.abstract y.abstract;
absent = Absent.Dnf.diff x.absent y.absent;
hash = -1;
}
let descr n =
assert (n.descr != dummy_descr);
n.descr
let internalize n = n
let id n = n.id
let rec constant = function
| Integer i -> interval (Intervals.atom i)
| Atom a -> atom (AtomSet.atom a)
| Char c -> char (CharSet.atom c)
| 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)
| String (i, j, s, c) ->
if U.equal_index i j then constant c
else
let ch, i' = U.next s i in
constant (Pair (Char (CharSet.V.mk_int ch), String (i', j, s, c)))
and const_node c = cons (constant c)
let neg x = diff any x
module LabelS = Set.Make (Label)
let any_or_absent = { any with absent = true; hash = -1 }
let only_absent = { empty with absent = true; hash = -1 }
let get_single_record r =
let labs accu (_, r) =
List.fold_left (fun accu (l, _) -> LabelS.add l accu) accu (LabelMap.get r)
in
let extend descrs labs (o, r) =
let rec aux i labs r =
match labs with
| [] -> ()
| l1 :: labs -> (
match r with
| (l2, x) :: r when l1 == l2 ->
descrs.(i) <- cap descrs.(i) (descr x);
aux (i + 1) labs r
| r ->
if not o then descrs.(i) <- cap descrs.(i) only_absent;
(* TODO:OPT *)
aux (i + 1) labs r)
in
aux 0 labs (LabelMap.get r);
o
in
let line (p, n) =
let labels = List.fold_left labs (List.fold_left labs LabelS.empty p) n in
let labels = LabelS.elements labels in
let nlab = List.length labels in
let mk () = Array.make nlab any_or_absent in
let pos = mk () in
let opos =
List.fold_left (fun accu x -> extend pos labels x && accu) true p
in
let p = (opos, pos) in
let n =
List.map
(fun x ->
let neg = mk () in
let o = extend neg labels x in
(o, neg))
n
in
(labels, p, n)
in
line r
let[@ocaml.warning "-32"] get_record r = List.map get_single_record (BoolRec.get r)
let get_record_full r =
List.map (fun (vars, r) ->
vars, get_single_record r)
Rec.(r |> get_vars |> Dnf.get_full)
(* Subtyping algorithm *)
let diff_t d t = diff d (descr t)
let cap_t d t = cap d (descr t)
let cap_product any_left any_right l =
List.fold_left
(fun (d1, d2) (t1, t2) -> (cap_t d1 t1, cap_t d2 t2))
(any_left, any_right) l
let any_pair = { empty with times = any.times; hash = -1 }
let rec exists max f = max > 0 && (f (max - 1) || exists (max - 1) f)
exception NotEmpty
module Witness = struct
module NodeSet = Set.Make (Node)
type witness =
| WInt of Intervals.V.t
| WAtom of AtomSet.sample
| WChar of CharSet.V.t
| WAbsent
| WAbstract of AbstractSet.elem option
| WPair of witness * witness * witness_slot
| WXml of witness * witness * witness_slot
| WRecord of witness label_map * bool * witness_slot
(* Invariant: WAbsent cannot actually appear *)
| WFun of (witness * witness option) list * witness_slot
(* Poly *)
| WPoly of Var.Set.t * Var.Set.t * witness
and witness_slot = {
mutable wnodes_in : NodeSet.t;
mutable wnodes_out : NodeSet.t;
mutable wuid : int;
}
module WHash = Hashtbl.Make (struct
type t = witness
let rec hash_small = function
| WInt i -> 17 * Intervals.V.hash i
| WChar c -> 1 + (17 * CharSet.V.hash c)
| WAtom None -> 2
| WAtom (Some (ns, None)) -> 3 + (17 * Ns.Uri.hash ns)
| WAtom (Some (_, Some t)) -> 4 + (17 * Ns.Label.hash t)
| WAbsent -> 5
| WAbstract None -> 6
| WAbstract (Some t) -> 7 + (17 * AbstractSet.T.hash t)
| WPair (_, _, s)
| WXml (_, _, s)
| WRecord (_, _, s)
| WFun (_, s) ->
8 + (17 * s.wuid)
| WPoly (pos, neg, w) ->
9 + Var.Set.hash pos + 17 * Var.Set.hash neg + 257 * hash_small w
let hash = function
| WPair (p1, p2, _) -> (257 * hash_small p1) + (65537 * hash_small p2)
| WXml (p1, p2, _) -> 1 + (257 * hash_small p1) + (65537 * hash_small p2)
| WRecord (r, o, _) ->
(if o then 2 else 3) + (257 * LabelMap.hash hash_small r)
| WFun (f, _) ->
4
+ 257
* Hashtbl.hash
(List.map
(function
| x, None -> 17 * hash_small x
| x, Some y ->
1 + (17 * hash_small x) + (257 * hash_small y))
f)
| _ -> assert false
let rec equal_small w1 w2 =
match (w1, w2) with
| WInt i1, WInt i2 -> Intervals.V.equal i1 i2
| WChar c1, WChar c2 -> CharSet.V.equal c1 c2
| WAtom None, WAtom None -> true
| WAtom (Some (ns1, None)), WAtom (Some (ns2, None)) ->
Ns.Uri.equal ns1 ns2
| WAtom (Some (_, Some t1)), WAtom (Some (_, Some t2)) ->
Ns.Label.equal t1 t2
| WAbsent, WAbsent -> true
| WAbstract None, WAbstract None -> false
| WAbstract (Some t1), WAbstract (Some t2) -> AbstractSet.T.equal t1 t2
| WPoly (p1, n1, w1), WPoly (p2, n2, w2) ->
Var.Set.equal p1 p2 &&
Var.Set.equal n1 n2 &&
equal_small w1 w2
| _ -> w1 == w2
let equal w1 w2 =
match (w1, w2) with
| WPair (p1, q1, _), WPair (p2, q2, _)
| WXml (p1, q1, _), WXml (p2, q2, _) ->
equal_small p1 p2 && equal_small q1 q2
| WRecord (r1, o1, _), WRecord (r2, o2, _) ->
o1 == o2 && LabelMap.equal equal_small r1 r2
| WFun (f1, _), WFun (f2, _) ->
List.length f1 = List.length f2
&& List.for_all2
(fun (x1, y1) (x2, y2) ->
equal_small x1 x2
&&
match (y1, y2) with
| Some y1, Some y2 -> equal_small y1 y2
| None, None -> true
| _ -> false)
f1 f2
| _ -> false
end)
let wmemo = WHash.create 1024
let wuid = ref 0
let wslot () =
{ wuid = !wuid; wnodes_in = NodeSet.empty; wnodes_out = NodeSet.empty }
let () =
Stats.register Stats.Summary (fun ppf ->
Format.fprintf ppf "Allocated witnesses:%i@\n" !wuid)
let rec print_witness ppf = function
| WInt i -> Format.fprintf ppf "%a" Intervals.V.print i
| WChar c -> Format.fprintf ppf "%a" CharSet.V.print c
| WAtom None -> Format.fprintf ppf "`#:#"
| WAtom (Some (ns, None)) ->
Format.fprintf ppf "`%a" Ns.InternalPrinter.print_any_ns ns
| WAtom (Some (_, Some t)) -> Format.fprintf ppf "`%a" Ns.Label.print_attr t
| WPair (w1, w2, _) ->
Format.fprintf ppf "(%a,%a)" print_witness w1 print_witness w2
| WXml (w1, w2, _) ->
Format.fprintf ppf "XML(%a,%a)" print_witness w1 print_witness w2
| WRecord (ws, o, _) ->
Format.fprintf ppf "{";
LabelMap.iteri
(fun l w ->
Format.fprintf ppf " %a=%a" Label.print_attr l print_witness w)
ws;
if o then Format.fprintf ppf " ..";
Format.fprintf ppf " }"
| WFun (f, _) ->
Format.fprintf ppf "FUN{";
List.iter
(fun (x, y) ->
Format.fprintf ppf " %a->" print_witness x;
match y with
| None -> Format.fprintf ppf "#"
| Some y -> print_witness ppf y)
f;
Format.fprintf ppf " }"
| WAbstract None -> Format.fprintf ppf "Abstract(..)"
| WAbstract (Some s) -> Format.fprintf ppf "Abstract(%s)" s
| WAbsent -> Format.fprintf ppf "Absent"
| WPoly (pos, neg, w) ->
Format.fprintf ppf "Poly(%a, %a, %a)"
Var.Set.print pos
Var.Set.print neg
print_witness w
let wmk w =
(* incr wuid; w *)
(* hash-consing disabled *)
try WHash.find wmemo w with
| Not_found ->
incr wuid;
WHash.add wmemo w w;
(* Format.fprintf Format.std_formatter "W:%a@."
print_witness w; *)
w
let wpair p1 p2 = wmk (WPair (p1, p2, wslot ()))
let wxml p1 p2 = wmk (WXml (p1, p2, wslot ()))
let wrecord r o = wmk (WRecord (r, o, wslot ()))
let wfun f = wmk (WFun (f, wslot ()))
(* A witness with variables wpos wneg
belongs to type with variables tpos tneg
if :
- wpos and tneg are disjoint (a witness 'a&0 cannot belong
to a type T\'a)
- likewise for wneg and tpos
- wpos is a superset of tpos, that is 'a&'b&'c&42 is
belongs to the type 'a&Int
- wneg is a super set of tneg
*)
let subset_vars wpos wneg tpos tneg =
let sneg = Var.Set.from_list tneg in
Var.Set.disjoint wpos sneg &&
Var.Set.subset sneg wneg &&
let spos = Var.Set.from_list tpos in
Var.Set.disjoint wneg spos &&
Var.Set.subset spos wpos
let basic_dnf (type mono) (module M : Kind with type Dnf.mono = mono)
pos neg t f =
M.get_vars t
|> M.Dnf.get_partial
|> List.exists (fun ((vp, vn), mono) ->
subset_vars pos neg vp vn &&
f mono)
let full_dnf (type atom) (module M : Kind
with type Dnf.atom = atom
and type Dnf.line = atom list * atom list)
pos neg t f =
M.get_vars t
|> M.Dnf.get_full
|> List.exists (fun ((vp, vn), (ap, an)) ->
subset_vars pos neg vp vn &&
List.for_all f ap &&
not (List.exists f an)
)
let rec node_has n = function
| (WXml (_, _, s) | WPair (_, _, s) | WFun (_, s) | WRecord (_, _, s)) as w
->
if NodeSet.mem n s.wnodes_in then true
else if NodeSet.mem n s.wnodes_out then false
else
let r = type_has (descr n) w in
if r then s.wnodes_in <- NodeSet.add n s.wnodes_in
else s.wnodes_out <- NodeSet.add n s.wnodes_out;
r
| w -> type_has (descr n) w
and type_has t w =
let pos, neg, w =
match w with
WPoly (pos, neg, w) -> pos, neg, w
| _ -> Var.Set.empty, Var.Set.empty, w
in
match w with
WPoly _ -> assert false
| WInt i ->
basic_dnf (module Int) pos neg t (Intervals.contains i)
| WChar c ->
basic_dnf (module Char) pos neg t (CharSet.contains c)
| WAtom a ->
basic_dnf (module Atom) pos neg t (AtomSet.contains_sample a)
| WAbsent -> t.absent
| WAbstract a ->
basic_dnf (module Abstract) pos neg t (AbstractSet.contains_sample a)
| WPair (w1, w2, _) ->
full_dnf (module Times) pos neg t
(fun (n1, n2) -> node_has n1 w1 && node_has n2 w2)
| WXml (w1, w2, _) ->
full_dnf (module Xml) pos neg t
(fun (n1, n2) -> node_has n1 w1 && node_has n2 w2)
| WFun (f, _) ->
full_dnf (module Function) pos neg t
(fun (n1, n2) ->
List.for_all
(fun (x, y) ->
(not (node_has n1 x))
||
match y with
| None -> false
| Some y -> node_has n2 y)
f)
| WRecord (f, o, _) ->
full_dnf (module Rec) pos neg t
(fun (o', f') ->
((not o) || o')
&&
let checked = ref 0 in
try
LabelMap.iteri
(fun l n ->
let w =
try
let w = LabelMap.assoc l f in
incr checked;
w
with
| Not_found -> WAbsent
in
if not (node_has n w) then raise Exit)
f';
o' || LabelMap.length f == !checked
(* All the remaining fields cannot be WAbsent
because of an invariant. Otherwise, we must
check that all are WAbsent here. *)
with
| Exit -> false)
end
type slot = {
mutable status : status;
mutable notify : notify;
mutable active : bool;
}
and status =
| Empty
| NEmpty of Witness.witness
| Maybe
and notify =
| Nothing
| Do of slot * (Witness.witness -> unit) * notify
let slot_nempty w = { status = NEmpty w; active = false; notify = Nothing }
let rec notify w = function
| Nothing -> ()
| Do (n, f, rem) ->
(if n.status == Maybe then
try f w with
| NotEmpty -> ());
notify w rem
let mk_poly vars w =
match vars with
[], [] -> w
| p, n -> Witness.WPoly (Var.Set.from_list p,
Var.Set.from_list n, w)
let rec iter_s s f = function
| [] -> ()
| (x,y) :: rem ->
f x y s;
iter_s s f rem
let set s w =
s.status <- NEmpty w;
notify w s.notify;
s.notify <- Nothing;
raise NotEmpty
let rec big_conj f l n w =
match l with
| [] -> set n w
| [ arg ] -> f w arg n
| arg :: rem -> (
let s =
{
status = Maybe;
active = false;
notify = Do (n, big_conj f rem n, Nothing);
}
in
try
f w arg s;
if s.active then n.active <- true
with
| NotEmpty when n.status == Empty || n.status == Maybe -> ())
let memo = DescrHash.create 8191
let marks = ref []
let count_subtype = Stats.Counter.create "Subtyping internal loop"
let rec find_map f = function
[] -> None
| e :: l ->
match f e with
None -> find_map f l
| r -> r
let check_basic (type mono) (module M : Kind with type Dnf.mono = mono) d is_empty mk =
M.get_vars d
|> M.Dnf.get_partial
|> find_map (fun ((pos, neg), m) ->
if is_empty m then None
else
let w = mk m in
let w = match pos, neg with
[], [] -> w
| _ -> Witness.WPoly (Var.Set.from_list pos,
Var.Set.from_list neg, w)
in
Some (slot_nempty w))
let (let*) o f =
match o with
Some e -> e
| None -> f ()
let rec slot d =
Stats.Counter.incr count_subtype;
if d == empty then { status = Empty; active = false; notify = Nothing }
else if d.absent then slot_nempty Witness.WAbsent
else
let* () = check_basic (module Int) d Intervals.is_empty
(fun i -> Witness.WInt (Intervals.sample i)) in
let* () = check_basic (module Atom) d AtomSet.is_empty
(fun a -> Witness.WAtom (AtomSet.sample a)) in
let* () = check_basic (module Char) d CharSet.is_empty
(fun c -> Witness.WChar (CharSet.sample c)) in
let* () = check_basic (module Abstract) d AbstractSet.is_empty
(fun a -> Witness.WAbstract (AbstractSet.sample a)) in
try DescrHash.find memo d with
| Not_found ->
let s = { status = Maybe; active = false; notify = Nothing } in
DescrHash.add memo d s;
(try
iter_s s check_times Times.(d |> get_vars |> Dnf.get_full);
iter_s s check_xml Xml.(d |> get_vars |> Dnf.get_full);
iter_s s check_arrow Function.(d |> get_vars |> Dnf.get_full);
iter_s s check_record (get_record_full d);
if s.active then marks := s :: !marks else s.status <- Empty
with
| NotEmpty -> ());
s
and guard n t f =
match slot t with
| { status = Empty; _ } -> ()
| { status = Maybe; _ } as s ->
n.active <- true;
s.notify <- Do (n, f, s.notify)
| { status = NEmpty v; _ } -> f v
and check_product vars any_right mk_witness (left, right) s =
let rec aux w1 w2 accu1 accu2 seen = function
(* Find a product in right which contains (w1,w2) *)
| [] ->
(* no such product: the current witness is in the difference. *)
set s (mk_poly vars (mk_witness w1 w2))
| (n1, n2) :: rest when Witness.node_has n1 w1 && Witness.node_has n2 w2 ->
let right = List.rev_append seen rest in
let accu2' = diff accu2 (descr n2) in
guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right);
let accu1' = diff accu1 (descr n1) in
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right)
| k :: rest -> aux w1 w2 accu1 accu2 (k :: seen) rest
in
let t1, t2 = cap_product any any_right left in
guard s t1 (fun w1 -> guard s t2 (fun w2 -> aux w1 w2 t1 t2 [] right))
and check_times vars prod s = check_product vars any Witness.wpair prod s
and check_xml vars prod s = check_product vars any_pair Witness.wxml prod s
and check_arrow (vpos, vneg) (left, right) s =
let single_right f (s1, s2) s =
let rec aux w1 w2 accu1 accu2 left =
match left with
| (t1, t2) :: left ->
let accu1' = diff_t accu1 t1 in
guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);
let accu2' = cap_t accu2 t2 in
guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
| [] ->
let op, on, f =
match f with
| Witness.WFun (f, _) -> [], [], f
| Witness.WPoly (op, on, Witness.WFun (f, _)) ->
Var.Set.(get op, get on, f)
| _ -> assert false
in
set s (mk_poly (op @ vpos, on@vneg) (Witness.wfun ((w1, w2) :: f)))
in
let accu1 = descr s1 in
guard s accu1 (fun w1 -> aux w1 None accu1 (neg (descr s2)) left)
in
big_conj single_right right s (Witness.wfun [])
and check_record vars (labels, (oleft, left), rights) s =
let rec aux ws accus seen = function
| [] ->
let rec aux w i = function
| [] ->
assert (i == Array.length ws);
w
| l :: labs ->
let w =
match ws.(i) with
| Witness.WAbsent -> w
| wl -> LabelMap.add l wl w
in
aux w (succ i) labs
in
set s (mk_poly vars (Witness.wrecord (aux LabelMap.empty 0 labels) oleft))
| (false, _) :: rest when oleft -> aux ws accus seen rest
| (_, f) :: rest
when not
(exists (Array.length left) (fun i ->
not (Witness.type_has f.(i) ws.(i)))) ->
(* TODO: a version f get_record which keeps nodes in neg records. *)
let right = seen @ rest in
for i = 0 to Array.length left - 1 do
let di = diff accus.(i) f.(i) in
guard s di (fun wi ->
let accus' = Array.copy accus in
accus'.(i) <- di;
let ws' = Array.copy ws in
ws'.(i) <- wi;
aux ws' accus' [] right)
done
| k :: rest -> aux ws accus (k :: seen) rest
in
let rec start wl i =
if i < 0 then aux (Array.of_list wl) left [] rights
else guard s left.(i) (fun w -> start (w :: wl) (i - 1))
in
start [] (Array.length left - 1)
let timer_subtype = Stats.Timer.create "Types.is_empty"
let is_empty d =
Stats.Timer.start timer_subtype;
let s = slot d in
List.iter
(fun s' ->
if s'.status == Maybe then s'.status <- Empty;
s'.notify <- Nothing)
!marks;
marks := [];
Stats.Timer.stop timer_subtype (s.status == Empty)
let getwit t =
match (slot t).status with
| NEmpty w -> w
| _ -> assert false
(* Assumes that is_empty has been called on t before. *)
let witness t = if is_empty t then raise Not_found else getwit t
let print_witness ppf t = Witness.print_witness ppf (witness t)
let non_empty d = not (is_empty d)
let disjoint d1 d2 = is_empty (cap d1 d2)
let subtype d1 d2 = is_empty (diff d1 d2)
let equiv d1 d2 = subtype d1 d2 && subtype d2 d1
(* redefine operations to take subtyping into account and perform hash consing *)
let forward_pointers = DescrHash.create 16
module NL = SortedList.Make (Node)
let get_all n =
if is_opened n then NL.singleton n
else
try DescrHash.find forward_pointers (descr n) with
| Not_found -> NL.empty
let add t n =
let lold =
try DescrHash.find forward_pointers t with
| Not_found -> NL.empty
in
DescrHash.replace forward_pointers t (NL.cup n lold)
let times n1 n2 =
let f1 = get_all n1 in
let f2 = get_all n2 in
let t = times n1 n2 in
add t f1;
add t f2;
t
module Cache = struct
(*
let type_has_witness t w =
Format.fprintf Format.std_formatter
"check wit:%a@." print_witness w;
let r = type_has_witness t w in
Format.fprintf Format.std_formatter "Done@.";
r
*)
type 'a cache =
| Empty
| Type of t * 'a
| Split of Witness.witness * 'a cache * 'a cache
let rec find f t = function
| Empty ->
let r = f t in
(Type (t, r), r)
| Split (w, yes, no) ->
if Witness.type_has t w then
let yes, r = find f t yes in
(Split (w, yes, no), r)
else
let no, r = find f t no in
(Split (w, yes, no), r)
| Type (s, rs) as c -> (
let f1 () =
let w = witness (diff t s) in
let rt = f t in
(Split (w, Type (t, rt), c), rt)
and f2 () =
let w = witness (diff s t) in
let rt = f t in
(Split (w, c, Type (t, rt)), rt)
in
if Random.int 2 = 0 then
try f1 () with
| Not_found -> (
try f2 () with
| Not_found -> (c, rs))
else
try f2 () with
| Not_found -> (
try f1 () with
| Not_found -> (c, rs)))
let rec lookup t = function
| Empty -> None
| Split (w, yes, no) -> lookup t (if Witness.type_has t w then yes else no)
| Type (s, rs) -> if equiv s t then Some rs else None
let emp = Empty
let[@ocaml.warning "-32"] rec dump_cache f ppf = function
| Empty -> Format.fprintf ppf "Empty"
| Type (_, s) -> Format.fprintf ppf "*%a" f s
| Split (_, c1, c2) ->
Format.fprintf ppf "?(%a,%a)"
(*Witness.print_witness w *) (dump_cache f)
c1 (dump_cache f) c2
let memo f =
let c = ref emp in
fun t ->
let c', r = find f t !c in
c := c';
r
end
module Product = struct
type t = (descr * descr) list
let _other ?(kind = `Normal) d =
match kind with
| `Normal -> { d with times = empty.times; hash = -1 }
| `XML -> { d with xml = empty.xml; hash = -1 }
let _is_product ?kind d = is_empty (_other ?kind d)
let need_second = function
| _ :: _ :: _ -> true
| _ -> false
let normal_aux = function
| ([] | [ _ ]) as d -> d
| d ->
let res = ref [] in
let add (t1, t2) =
let rec loop t1 t2 = function
| [] -> res := ref (t1, t2) :: !res
| ({ contents = d1, d2 } as r) :: l ->
(*OPT*)
(* if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
let i = cap t1 d1 in
if is_empty i then loop t1 t2 l
else (
r := (i, cup t2 d2);
let k = diff d1 t1 in
if non_empty k then res := ref (k, d2) :: !res;
let j = diff t1 d1 in
if non_empty j then loop j t2 l)
in
loop t1 t2 !res
in
List.iter add d;
List.map ( ! ) !res
(* Partitioning:
(t,s) - ((t1,s1) | (t2,s2) | ... | (tn,sn))
=
(t & t1, s - s1) | ... | (t & tn, s - sn) | (t - (t1|...|tn), s)
*)
let get_aux any_right d =
let accu = ref [] in
let line (left, right) =
let d1, d2 = cap_product any any_right left in
if non_empty d1 && non_empty d2 then
let right = List.map (fun (t1, t2) -> (descr t1, descr t2)) right in
let right = normal_aux right in
let resid1 = ref d1 in
let () =
List.iter
(fun (t1, t2) ->
let t1 = cap d1 t1 in
if non_empty t1 then
let () = resid1 := diff !resid1 t1 in
let t2 = diff d2 t2 in
if non_empty t2 then accu := (t1, t2) :: !accu)
right
in
if non_empty !resid1 then accu := (!resid1, d2) :: !accu
in
List.iter line (BoolPair.get d);
!accu
let partition = get_aux
(* Maybe, can improve this function with:
(t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
don't call normal_aux *)
let get ?(kind = `Normal) d =
match kind with
| `Normal -> get_aux any d.times
| `XML -> get_aux any_pair d.xml
let pi1 = List.fold_left (fun acc (t1, _) -> cup acc t1) empty
let pi2 = List.fold_left (fun acc (_, t2) -> cup acc t2) empty
let pi2_restricted restr =
List.fold_left
(fun acc (t1, t2) -> if disjoint t1 restr then acc else cup acc t2)
empty
let restrict_1 rects pi1 =
let aux acc (t1, t2) =
let t1 = cap t1 pi1 in
if is_empty t1 then acc else (t1, t2) :: acc
in
List.fold_left aux [] rects
type normal = t
module Memo = Map.Make (BoolPair)
(* TODO: try with an hashtable *)
(* Also, avoid lookup for simple products (t1,t2) *)
let memo = ref Memo.empty
let normal_times d =
try Memo.find d !memo with
| Not_found ->
let gd = get_aux any d in
let n = normal_aux gd in
(* Could optimize this call to normal_aux because one already
know that each line is normalized ... *)
memo := Memo.add d n !memo;
n
let memo_xml = ref Memo.empty
let normal_xml d =
try Memo.find d !memo_xml with
| Not_found ->
let gd = get_aux any_pair d in
let n = normal_aux gd in
memo_xml := Memo.add d n !memo_xml;
n
let normal ?(kind = `Normal) d =
match kind with
| `Normal -> normal_times d.times
| `XML -> normal_xml d.xml
(*
let merge_same_2 r =
let r =
List.fold_left
(fun accu (t1,t2) ->
let t = try DescrMap.find t2 accu with Not_found -> empty in
DescrMap.add t2 (cup t t1) accu
) DescrMap.empty r in
DescrMap.fold (fun t2 t1 accu -> (t1,t2)::accu) r []
*)
let constraint_on_2 n t1 =
List.fold_left
(fun accu (d1, d2) -> if disjoint d1 t1 then accu else cap accu d2)
any n
let merge_same_first tr =
let trs = ref [] in
let _ =
List.fold_left
(fun memo (t1, t2) ->
let memo', l =
Cache.find
(fun t1 ->
let l = ref empty in
trs := (t1, l) :: !trs;
l)
t1 memo
in
l := cup t2 !l;
memo')
Cache.emp tr
in
List.map (fun (t1, l) -> (t1, !l)) !trs
(* same on second component: use the same implem? *)
let clean_normal l =
let rec aux accu (t1, t2) =
match accu with
| [] -> [ (t1, t2) ]
| (s1, s2) :: rem when equiv t2 s2 -> (cup s1 t1, s2) :: rem
| (s1, s2) :: rem -> (s1, s2) :: aux rem (t1, t2)
in
List.fold_left aux [] l
let is_empty d = d == []
end
module Record = struct
let has_record d = not (is_empty { empty with record = d.record; hash = -1 })
let or_absent d = { d with absent = true; hash = -1 }
let absent = or_absent empty
let any_or_absent = any_or_absent
let has_absent d = d.absent
let absent_node = cons absent
module T = struct
type t = descr
let any = any_or_absent
let cap = cap
let cup = cup
let diff = diff
let is_empty = is_empty
let empty = empty
end
module R = struct
type t = descr
let any = { empty with record = any.record; hash = -1 }
let cap = cap
let cup = cup
let diff = diff
let is_empty = is_empty
let empty = empty
end
module TR = Normal.Make (T) (R)
let any_record = { empty with record = BoolRec.any; hash = -1 }
let atom o l =
if o && LabelMap.is_empty l then any_record
else { empty with record = BoolRec.atom (o, l); hash = -1 }
type zor =
| Pair of descr * descr
| Any
(* given a type t and a label l, this function computes the projection on
l on each component of the DNF *)
let aux_split d l =
let f (o, r) =
try
(* separate a record type between the type of its label l, if it appears
explicitely and the type of the reminder of the record *)
let lt, rem = LabelMap.assoc_remove l r in
Pair (descr lt, atom o rem)
with
| Not_found ->
(* if the label l is not present explicitely *)
if o then
(* if the record is open *)
if LabelMap.is_empty r then Any
(* if there are no explicity fields return Any,
the record type is not splited *)
else
(* otherwise returns the fact that the field may or may not be present
*)
Pair
( any_or_absent,
{ empty with record = BoolRec.atom (o, r); hash = -1 } )
else
(* for closed records, return the fact that the label was absent *)
Pair (absent, { empty with record = BoolRec.atom (o, r); hash = -1 })
in
List.fold_left
(fun b (p, n) ->
(* for each positive/negative intersections*)
let rec aux_p accu = function
| x :: p -> (
(*get the ucrrent positive record, and split according to l*)
match f x with
(* if something, add (typof l, rest) to the positive accumulator*)
| Pair (t1, t2) -> aux_p ((t1, t2) :: accu) p
| Any ->
aux_p accu p
(* if we have { ..} in this positive
intersection, we can ignore it. *))
| [] -> aux_n accu [] n
(* now follow up with negative*)
and aux_n p accu = function
| x :: n -> (
match f x with
(* if we have a pair add it to the current negative accmulator*)
| Pair (t1, t2) -> aux_n p ((t1, t2) :: accu) n
(* if { .. } is in a negative intersection, the whole branch (p,n)
can be discarded *)
| Any -> b)
| [] -> (p, accu) :: b
(* add the current pair of line *)
in
aux_p [] p)
[] (BoolRec.get d.record)
(* We now have a DNF of pairs where the left component is the type of
a label l and the right component the rest of the record types.
split returns a simplified DNF where the intersection are pushed
below the products.
Given a type d and a label l, this function returns
a list of pairs : the first component represents the disjoint union
of types associated to l
the second projection the remaining types (records \ l)
*)
let split (d : descr) l = TR.boolean (aux_split d l)
(* same as above, but the types for .l are disjoint *)
let split_normal d l = TR.boolean_normal (aux_split d l)
(* returns the union of the first projections. If one of the record
had an absent l, then absent will end up in the result. *)
let pi l d = TR.pi1 (split d l)
(* Same but check that the resulting type does not contain absent *)
let project d l =
let t = pi l d in
if t.absent then raise Not_found;
t
(* Same but erase the status of absent : meaning return the type of l
if it is present.*)
let project_opt d l =
let t = pi l d in
{ t with absent = false; hash = -1 }
let _condition d l t = TR.pi2_restricted t (split d l)
(* TODO: eliminate this cap ... (record l absent_node) when
not necessary. eg. { ..... } \ l *)
(* get the pi2 part of split, that is the union of all the record types where
l has been removed explicitely. And cap it with an open record where l
is absent, to eliminate l from open record types where it was implicitely present.
*)
let remove_field d l = cap (TR.pi2 (split d l)) (record l absent_node)
let _all_labels d =
let res = ref LabelSet.empty in
let aux (_, r) =
let ls = LabelMap.domain r in
res := LabelSet.cup ls !res
in
BoolRec.iter aux d.record;
!res
let first_label d =
let min = ref Label.dummy in
let aux (_, r) =
match LabelMap.get r with
| (l, _) :: _ -> min := Label.min l !min
| _ -> ()
in
Rec.Dnf.iter aux d.record;
!min
let empty_cases d =
let x =
BoolRec.compute ~empty:0 ~any:3
~cup:(fun x y -> x lor y)
~cap:(fun x y -> x land y)
~diff:(fun a b -> a land lnot b)
~atom:(function
| o, r ->
assert (LabelMap.get r == []);
if o then 3 else 1)
d.record
in
(x land 2 <> 0, x land 1 <> 0)
let has_empty_record d =
BoolRec.compute ~empty:false ~any:true ~cup:( || ) ~cap:( && )
~diff:(fun a b -> a && not b)
~atom:(function
| _, r -> List.for_all (fun (_, t) -> (descr t).absent) (LabelMap.get r))
d.record
(*TODO: optimize merge
- pre-compute the sequence of labels
- remove empty or full { l = t }
*)
let merge d1 d2 =
let res = ref empty in
let rec aux accu d1 d2 =
let l = Label.min (first_label d1) (first_label d2) in
if l == Label.dummy then
let some1, none1 = empty_cases d1
and some2, none2 = empty_cases d2 in
let _none = none1 && none2
and some = some1 || some2 in
let accu = LabelMap.from_list (fun _ _ -> assert false) accu in
(* approx for the case (some && not none) ... *)
res := cup !res (record_fields (some, accu))
else
let l1 = split d1 l
and l2 = split d2 l in
let loop (t1, d1) (t2, d2) =
let t =
if t2.absent then cup t1 { t2 with absent = false; hash = -1 }
else t2
in
aux ((l, cons t) :: accu) d1 d2
in
List.iter (fun x -> List.iter (loop x) l2) l1
in
aux [] d1 d2;
!res
let get d =
let rec aux r accu d =
let l = first_label d in
if l == Label.dummy then
let o1, o2 = empty_cases d in
if o1 || o2 then (LabelMap.from_list_disj r, o1, o2) :: accu else accu
else
List.fold_left
(fun accu (t1, t2) ->
let x = (t1.absent, { t1 with absent = false }) in
aux ((l, x) :: r) accu t2)
accu (split d l)
in
aux [] [] d
type t = TR.t
let focus = split_normal
let get_this r = { (TR.pi1 r) with absent = false; hash = -1 }
let need_others = function
| _ :: _ :: _ -> true
| _ -> false
let constraint_on_others r t1 =
List.fold_left
(fun accu (d1, d2) -> if disjoint d1 t1 then accu else cap accu d2)
any_record r
end
let memo_normalize = ref DescrMap.empty
let rec rec_normalize d =
try DescrMap.find d !memo_normalize with
| Not_found ->
let n = make () in
memo_normalize := DescrMap.add d n !memo_normalize;
let times =
List.fold_left
(fun accu (d1, d2) ->
BoolPair.cup accu
(BoolPair.atom (rec_normalize d1, rec_normalize d2)))
BoolPair.empty (Product.normal d)
in
let xml =
List.fold_left
(fun accu (d1, d2) ->
BoolPair.cup accu
(BoolPair.atom (rec_normalize d1, rec_normalize d2)))
BoolPair.empty
(Product.normal ~kind:`XML d)
in
let record = d.record in
define n { d with times; xml; record; hash = -1 };
n
let normalize n = descr (internalize (rec_normalize n))
module Arrow = struct
let trivially_arrow t =
if subtype Function.any t then `Arrow
else if is_empty { empty with arrow = t.arrow; hash = -1 } then `NotArrow
else `Other
let check_simple left (s1, s2) =
let rec aux accu1 accu2 = function
| (t1, t2) :: left ->
let accu1' = diff_t accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap_t accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
is_empty accu1
||
try
aux accu1 (diff any (descr s2)) left;
true
with
| NotEmpty -> false
let check_line_non_empty (left, right) =
not (List.exists (check_simple left) right)
let sample t =
let left, _right =
List.find check_line_non_empty (Function.Dnf.get t.arrow)
in
List.fold_left
(fun accu (t, s) -> cap accu (arrow t s))
{ empty with arrow = any.arrow; hash = -1 }
left
(* [check_strenghten t s]
Assume that [t] is an intersection of arrow types
representing the interface of an abstraction;
check that this abstraction has type [s] (otherwise raise Not_found)
and returns a refined type for this abstraction.
*)
let _check_strenghten t s =
(*
let left = match (BoolPair.get t.arrow) with [ (p,[]) ] -> p | _ -> assert false in
let rec aux = function
| [] -> raise Not_found
| (p,n) :: rem ->
if (List.for_all (fun (a,b) -> check_simple left a b) p) &&
(List.for_all (fun (a,b) -> not (check_simple left a b)) n) then
{ empty with arrow = Obj.magic [ (SortedList.cup left p, n) ] } (* rework this ! *)
else aux rem
in
aux (BoolPair.get s.arrow)
*)
if subtype t s then t else raise Not_found
let check_simple_iface left s1 s2 =
let rec aux accu1 accu2 = function
| (t1, t2) :: left ->
let accu1' = diff accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
is_empty accu1
||
try
aux accu1 (diff any (descr s2)) left;
true
with
| NotEmpty -> false
let check_iface iface s =
let rec aux = function
| [] -> false
| (p, n) :: rem ->
List.for_all (fun (a, b) -> check_simple_iface iface a b) p
&& List.for_all (fun (a, b) -> not (check_simple_iface iface a b)) n
|| aux rem
in
aux (Function.Dnf.get s.arrow)
type t = descr * (descr * descr) list list
let get t =
List.fold_left
(fun ((dom, arr) as accu) (left, right) ->
if check_line_non_empty (left, right) then
let left = List.map (fun (t, s) -> (descr t, descr s)) left in
let d = List.fold_left (fun d (t, _) -> cup d t) empty left in
(cap dom d, left :: arr)
else accu)
(any, []) (BoolPair.get t.arrow)
let domain (dom, _) = dom
let apply_simple t result left =
let rec aux result accu1 accu2 = function
| (t1, s1) :: left ->
let result =
let accu1 = diff accu1 t1 in
if non_empty accu1 then aux result accu1 accu2 left else result
in
let result =
let accu2 = cap accu2 s1 in
aux result accu1 accu2 left
in
result
| [] -> if subtype accu2 result then result else cup result accu2
in
aux result t any left
let apply (_, arr) t =
if is_empty t then empty else List.fold_left (apply_simple t) empty arr
let need_arg (_dom, arr) =
List.exists
(function
| [ _ ] -> false
| _ -> true)
arr
let apply_noarg (_, arr) =
List.fold_left
(fun accu -> function
| [ (_t, s) ] -> cup accu s
| _ -> assert false)
empty arr
let is_empty (_, arr) = arr == []
end
let rec tuple = function
| [ t1; t2 ] -> times t1 t2
| t :: tl -> times t (cons (tuple tl))
| _ -> failwith "tuple: invalid length"
let rec_of_list o l =
let map =
LabelMap.from_list
(fun _ _ -> failwith "rec_of_list: duplicate fields")
(List.map
(fun (opt, qname, typ) ->
(qname, cons (if opt then Record.or_absent typ else typ)))
l)
in
record_fields (o, map)
let empty_closed_record = rec_of_list false []
let empty_open_record = Rec.any
let cond_partition univ qs =
let add accu (t, s) =
let t = if subtype t s then t else cap t s in
if subtype s t || is_empty t then accu
else
let aux accu u =
let c = cap u t in
if is_empty c || subtype (cap u s) t then u :: accu
else c :: diff u t :: accu
in
List.fold_left aux [] accu
in
List.fold_left add [ univ ] qs
lang/typing/typepat.ml
open Ident
open Cduce_error
let any_node = Types.(cons any)
let any_or_absent_node = Types.(cons Record.any_or_absent)
type err = string -> exn
let deferr s = raise_err Typer_Pattern s
type node = {
mutable desc : desc;
mutable smallhash : int;
(* Local hash *)
mutable rechash : int;
(* Global (recursive) hash *)
mutable sid : int;
(* Sequential id used to compute rechash *)
mutable t : Types.t option;
mutable tnode : Types.Node.t option;
mutable p : Patterns.descr option;
mutable pnode : Patterns.node option;
mutable fv : fv option;
}
and desc =
| ILink of node
| IType of Types.descr * int
| IOr of node * node * err
| IAnd of node * node * err
| IDiff of node * node * err
| ITimes of node * node
| IXml of node * node
| IArrow of node * node
| IOptional of node * err
| IRecord of bool * (node * node option) label_map * err
| ICapture of id
| IConstant of id * Types.const
| IConcat of node * node * err
| IMerge of node * node * err
let concats = ref []
let rec node_temp =
{
desc = ILink node_temp;
smallhash = 0;
rechash = 0;
sid = 0;
t = None;
tnode = None;
p = None;
pnode = None;
fv = None;
}
let mk d = { node_temp with desc = d }
let mk_delayed () = { node_temp with desc = ILink node_temp }
let mk_type t = mk (IType (t, Types.hash t))
let mk_or ?(err = deferr) n1 n2 = mk (IOr (n1, n2, err))
let mk_and ?(err = deferr) n1 n2 = mk (IAnd (n1, n2, err))
let mk_diff ?(err = deferr) n1 n2 = mk (IDiff (n1, n2, err))
let mk_prod n1 n2 = mk (ITimes (n1, n2))
let mk_xml n1 n2 = mk (IXml (n1, n2))
let mk_arrow n1 n2 = mk (IArrow (n1, n2))
let mk_optional ?(err = deferr) n = mk (IOptional (n, err))
let mk_record ?(err = deferr) n1 n2 = mk (IRecord (n1, n2, err))
let mk_capture n = mk (ICapture n)
let mk_constant n1 n2 = mk (IConstant (n1, n2))
let mk_concat ?(err = deferr) n1 n2 =
let n = mk (IConcat (n1, n2, err)) in
concats := n :: !concats;
n
let mk_merge ?(err = deferr) n1 n2 =
let n = mk (IMerge (n1, n2, err)) in
concats := n :: !concats;
n
let iempty = mk_type Types.empty
let mk_or ?err p1 p2 =
if p1.desc == iempty.desc then p2
else if p2.desc == iempty.desc then p1
else mk_or ?err p1 p2
let mk_and ?err p1 p2 =
if p1.desc == iempty.desc || p2.desc == iempty.desc then iempty
else mk_and ?err p1 p2
(* Recursive hash-consing *)
let hash_field f = function
| p, Some e -> 1 + (17 * f p) + (257 * f e)
| p, None -> 2 + (17 * f p)
let rec hash f n =
match n.desc with
| ILink n -> hash f n
| IType (t, h) -> 1 + (17 * h)
| IOr (p1, p2, _) -> 2 + (17 * f p1) + (257 * f p2)
| IAnd (p1, p2, _) -> 3 + (17 * f p1) + (257 * f p2)
| IDiff (p1, p2, _) -> 4 + (17 * f p1) + (257 * f p2)
| ITimes (p1, p2) -> 5 + (17 * f p1) + (257 * f p2)
| IXml (p1, p2) -> 6 + (17 * f p1) + (257 * f p2)
| IArrow (p1, p2) -> 7 + (17 * f p1) + (257 * f p2)
| IOptional (p, _) -> 8 + (17 * f p)
| IRecord (o, r, _) ->
9 + (if o then 17 else 0) + (257 * LabelMap.hash (hash_field f) r)
| ICapture x -> 10 + (17 * Id.hash x)
| IConstant (x, c) -> 11 + (17 * Id.hash x) + (257 * Types.Const.hash c)
| IConcat _
| IMerge _ ->
assert false
let hash0 = hash (fun n -> 1)
let hash1 = hash hash0
let hash2 = hash hash1
let hash3 = hash hash2
let smallhash n =
if n.smallhash != 0 then n.smallhash
else
let h = hash2 n in
n.smallhash <- h;
h
let rec repr = function
| { desc = ILink n } as m ->
let z = repr n in
m.desc <- ILink z;
z
| n -> n
let back = ref []
let rec prot_repr = function
| { desc = ILink n } -> repr n
| n -> n
let link x y =
match (x, y) with
| ({ t = None } as x), y
| y, ({ t = None } as x) ->
back := (x, x.desc) :: !back;
x.desc <- ILink y
| _ -> assert false
let rec unify x y =
if x == y then ()
else
let x = prot_repr x
and y = prot_repr y in
if x == y then ()
else if smallhash x != smallhash y then raise_err Typepat_Unify ()
else if x.t != None && y.t != None then raise_err Typepat_Unify ()
(* x and y have been internalized; if they were equivalent,
they would be equal *)
else
match (x.desc, y.desc) with
| IType (tx, _), IType (ty, _) when Types.equal tx ty -> link x y
| IOr (x1, x2, _), IOr (y1, y2, _)
| IAnd (x1, x2, _), IAnd (y1, y2, _)
| IDiff (x1, x2, _), IDiff (y1, y2, _)
| ITimes (x1, x2), ITimes (y1, y2)
| IXml (x1, x2), IXml (y1, y2)
| IArrow (x1, x2), IArrow (y1, y2) ->
link x y;
unify x1 y1;
unify x2 y2
| IOptional (x1, _), IOptional (y1, _) ->
link x y;
unify x1 y1
| IRecord (xo, xr, _), IRecord (yo, yr, _) when xo == yo ->
link x y;
LabelMap.may_collide unify_field (Error (Unlocated, (Typepat_Unify, ()))) xr yr
| ICapture xv, ICapture yv when Id.equal xv yv -> ()
| IConstant (xv, xc), IConstant (yv, yc)
when Id.equal xv yv && Types.Const.equal xc yc ->
()
| _ -> raise_err Typepat_Unify ()
and unify_field f1 f2 =
match (f1, f2) with
| (p1, Some e1), (p2, Some e2) ->
unify p1 p2;
unify e1 e2
| (p1, None), (p2, None) -> unify p1 p2
| _ -> raise_err Typepat_Unify ()
let may_unify x y =
try
unify x y;
back := [];
true
with
| Error (_, (Typepat_Unify, ())) ->
List.iter (fun (x, xd) -> x.desc <- xd) !back;
back := [];
false
module SmallHash = Hashtbl.Make (struct
type t = node
let equal = may_unify
let hash = smallhash
end)
let iter_field f = function
| x, Some y ->
f x;
f y
| x, None -> f x
let iter f = function
| IOr (x, y, _)
| IAnd (x, y, _)
| IDiff (x, y, _)
| ITimes (x, y)
| IXml (x, y)
| IArrow (x, y) ->
f x;
f y
| IOptional (x, _) -> f x
| IRecord (_, r, _) -> LabelMap.iter (iter_field f) r
| _ -> ()
let minimize (mem, add) =
let rec aux n =
let n = repr n in
if mem n then ()
else
let n = repr n in
add n ();
if n.t == None then iter aux n.desc
in
aux
let to_clear = ref []
let sid = ref 0
let rec rechash n =
let n = repr n in
if n.sid != 0 then 17 * n.sid
else (
incr sid;
n.sid <- !sid;
to_clear := n :: !to_clear;
hash rechash n)
let clear () =
sid := 0;
List.iter (fun x -> x.sid <- 0) !to_clear;
to_clear := []
let rechash n =
let n = repr n in
if n.rechash != 0 then n.rechash
else
let h = rechash n in
clear ();
n.rechash <- h;
h
module RecHash = Hashtbl.Make (struct
type t = node
let equal = may_unify
let hash = smallhash
end)
(** Two-phases recursive hash-consing **)
(*
let gtable = RecHash.create 17577
let internalize n =
let local = SmallHash.create 17 in
minimize (SmallHash.mem local, SmallHash.add local) n;
minimize (RecHash.mem gtable, RecHash.add gtable) n;
()
*)
(** Single-phase hash-consing **)
let gtable = SmallHash.create 17
let internalize n = minimize (SmallHash.mem gtable, SmallHash.add gtable) n
(* let internalize n = () *)
(* Compute free variables *)
let fv n =
let fv = ref IdSet.empty in
let rec aux n =
let n = repr n in
if n.sid = 0 then (
n.sid <- 1;
to_clear := n :: !to_clear;
match (n.fv, n.desc) with
| Some x, _ -> fv := IdSet.cup !fv x
| None, (ICapture x | IConstant (x, _)) -> fv := IdSet.add x !fv
| None, d -> iter aux d)
in
assert (!to_clear == []);
match n.fv with
| Some x -> x
| None ->
aux n;
clear ();
n.fv <- Some !fv;
!fv
(* optimized version to check closedness *)
let no_fv = Some IdSet.empty
let peek_fv n =
let err x = raise_err Typepat_FoundFv x in
let rec aux n =
let n = repr n in
if n.sid = 0 then (
n.sid <- 1;
to_clear := n :: !to_clear;
match (n.fv, n.desc) with
| Some x, _ when IdSet.is_empty x -> ()
| Some x, _ -> err (IdSet.choose x)
| None, (ICapture x | IConstant (x, _)) -> err x
| None, d -> iter aux d)
in
assert (!to_clear == []);
try
match n.fv with
| Some x when IdSet.is_empty x -> ()
| Some x -> err (IdSet.choose x)
| None ->
aux n;
List.iter
(fun n ->
n.sid <- 0;
n.fv <- no_fv)
!to_clear;
to_clear := []
with
| exn ->
clear ();
raise exn
let has_no_fv n =
try
peek_fv n;
true
with
| Error (_, (Typepat_FoundFv, _)) -> false
let peek_fv n =
try
peek_fv n;
None
with
| Cduce_error.Error (_, (Typepat_FoundFv, x)) -> Some (x : Ident.id)
(* From the intermediate representation to the internal one *)
let rec typ n =
let n = repr n in
match n.t with
| Some t -> t
| None ->
let t = compute_typ n.desc in
n.t <- Some t;
t
and compute_typ = function
| IType (t, _) -> t
| IOr (s1, s2, _) -> Types.cup (typ s1) (typ s2)
| IAnd (s1, s2, _) -> Types.cap (typ s1) (typ s2)
| IDiff (s1, s2, _) -> Types.diff (typ s1) (typ s2)
| ITimes (s1, s2) -> Types.times (typ_node s1) (typ_node s2)
| IXml (s1, s2) -> Types.xml (typ_node s1) (typ_node s2)
| IArrow (s1, s2) -> Types.arrow (typ_node s1) (typ_node s2)
| IOptional (s, _) -> Types.Record.or_absent (typ s)
| IRecord (o, r, err) ->
Types.record_fields (o, LabelMap.map (compute_typ_field err) r)
| ILink _ -> assert false
| ICapture _
| IConstant (_, _) ->
assert false
| IConcat _
| IMerge _ ->
assert false
and compute_typ_field err = function
| s, None -> typ_node s
| s, Some _ -> raise (err "Or-else clauses are not allowed in types")
and typ_node n =
let n = repr n in
match n.tnode with
| Some t -> t
| None ->
let x = Types.make () in
n.tnode <- Some x;
Types.define x (typ n);
x
let rec pat n =
let n = repr n in
if has_no_fv n then
let t = typ n in
if Var.Set.is_empty (Types.Subst.vars t) then Patterns.constr t
else raise_err Typer_Pattern "Polymorphic types are not allowed in patterns"
else
match n.p with
| Some p -> p
| None ->
let p = compute_pat n.desc in
n.p <- Some p;
p
and compute_pat = function
| IOr (s1, s2, err) -> (
try Patterns.cup (pat s1) (pat s2) with
| Cduce_error.Error (_, (Typer_Pattern, s)) -> raise (err s))
| IAnd (s1, s2, err) -> (
try Patterns.cap (pat s1) (pat s2) with
| Cduce_error.Error (_, (Typer_Pattern, s)) -> raise (err s))
| IDiff (s1, s2, _) when IdSet.is_empty (fv s2) ->
let s2 = Types.neg (typ s2) in
Patterns.cap (pat s1) (Patterns.constr s2)
| IDiff (_, _, err) -> raise (err "Differences are not allowed in patterns")
| ITimes (s1, s2) -> Patterns.times (pat_node s1) (pat_node s2)
| IXml (s1, s2) -> Patterns.xml (pat_node s1) (pat_node s2)
| IOptional (_, err) ->
raise (err "Optional fields are not allowed in record patterns")
| IRecord (o, r, err) ->
let pats = ref [] in
let aux l = function
| s, None ->
if IdSet.is_empty (fv s) then typ_node s
else (
pats := Patterns.record l (pat_node s) :: !pats;
any_node)
| s, Some e ->
if IdSet.is_empty (fv s) then
raise (err "Or-else clauses are not allowed in types")
else (
pats :=
Patterns.cup (Patterns.record l (pat_node s)) (pat e) :: !pats;
any_or_absent_node)
in
let constr = Types.record_fields (o, LabelMap.mapi aux r) in
List.fold_left Patterns.cap (Patterns.constr constr) !pats
(* TODO: can avoid constr when o=true, and all fields have fv *)
| ICapture x -> Patterns.capture x
| IConstant (x, c) -> Patterns.constant x c
| IArrow _ -> raise_err Typer_Pattern "Arrows are not allowed in patterns"
| IType _
| ILink _
| IConcat _
| IMerge _ ->
assert false
and pat_node n =
let n = repr n in
match n.pnode with
| Some p -> p
| None -> (
let x = Patterns.make (fv n) in
try
n.pnode <- Some x;
Patterns.define x (pat n);
x
with
| exn ->
n.pnode <- None;
raise exn)
type regexp =
| PElem of node
| PGuard of node
| PSeq of regexp list
| PAlt of regexp list
| PStar of regexp
| PWeakStar of regexp
let rec nullable = function
| PElem _ -> false
| PSeq rl -> List.for_all nullable rl
| PAlt rl -> List.exists nullable rl
| PStar _
| PWeakStar _
| PGuard _ ->
true
let eps = PSeq []
let emp = PAlt []
let star x = PStar x
let elem x = PElem x
let seq r1 r2 =
let r1 =
match r1 with
| PSeq l -> l
| x -> [ x ]
in
let r2 =
match r2 with
| PSeq l -> l
| x -> [ x ]
in
match r1 @ r2 with
| [ x ] -> x
| l -> PSeq l
let alt r1 r2 =
let r1 =
match r1 with
| PAlt l -> l
| x -> [ x ]
in
let r2 =
match r2 with
| PAlt l -> l
| x -> [ x ]
in
match r1 @ r2 with
| [ x ] -> x
| l -> PAlt l
let rec merge_alt = function
| PElem p :: PElem q :: l -> merge_alt (PElem (mk_or p q) :: l)
| r :: l -> r :: merge_alt l
| [] -> []
(* Works only for types, not patterns, because
[ (x&Int|_) R' ] is possible *)
let rec simplify_regexp = function
| PSeq l -> PSeq (List.map simplify_regexp l)
| PAlt l -> PAlt (merge_alt (List.map simplify_regexp l))
| PStar r
| PWeakStar r ->
PStar (simplify_regexp r)
| x -> x
let rec print_regexp ppf = function
| PElem _ -> Format.fprintf ppf "Elem"
| PGuard _ -> Format.fprintf ppf "Guard"
| PSeq l -> Format.fprintf ppf "Seq(%a)" print_regexp_list l
| PAlt l -> Format.fprintf ppf "Alt(%a)" print_regexp_list l
| PStar r -> Format.fprintf ppf "Star(%a)" print_regexp r
| PWeakStar r -> Format.fprintf ppf "WStar(%a)" print_regexp r
and print_regexp_list ppf l =
List.iter (fun x -> Format.fprintf ppf "%a;" print_regexp x) l
let rec remove_regexp r q =
match r with
| PElem p -> mk_prod p q
| PGuard p -> mk_and p q
| PSeq l -> List.fold_right (fun r a -> remove_regexp r a) l q
| PAlt rl -> List.fold_left (fun a r -> mk_or a (remove_regexp r q)) iempty rl
| PStar r ->
let x = mk_delayed () in
let res = mk_or x q in
x.desc <- ILink (remove_regexp_nullable r res iempty);
res
| PWeakStar r ->
let x = mk_delayed () in
let res = mk_or q x in
x.desc <- ILink (remove_regexp_nullable r res iempty);
res
and remove_regexp_nullable r q_nonempty q_empty =
if nullable r then remove_regexp2 r q_nonempty q_empty
else remove_regexp r q_nonempty
and remove_regexp2 r q_nonempty q_empty =
(* Assume r is nullable *)
if q_nonempty == q_empty then remove_regexp r q_nonempty
else
match r with
| PSeq [] -> q_empty
| PElem p -> assert false
| PGuard p -> mk_and p q_empty
| PSeq (r :: rl) ->
remove_regexp2 r
(remove_regexp (PSeq rl) q_nonempty)
(remove_regexp2 (PSeq rl) q_nonempty q_empty)
| PAlt rl ->
List.fold_left
(fun a r -> mk_or a (remove_regexp_nullable r q_nonempty q_empty))
iempty rl
| PStar r ->
let x = mk_delayed () in
x.desc <- ILink (remove_regexp_nullable r (mk_or x q_nonempty) iempty);
mk_or x q_empty
| PWeakStar r ->
let x = mk_delayed () in
x.desc <- ILink (remove_regexp_nullable r (mk_or q_nonempty x) iempty);
mk_or q_empty x
let pcdata = star (PElem (mk_type Types.(char CharSet.any)))
let mix_regexp regexp =
let rec aux = function
| PSeq [] -> eps
| PElem re -> PElem re
| PGuard re -> assert false
| PSeq (r :: rl) -> seq (aux r) (seq pcdata (aux (PSeq rl)))
| PAlt rl -> PAlt (List.map aux rl)
| PStar re -> star (seq pcdata (aux re))
| PWeakStar re -> assert false
in
seq pcdata (seq (aux regexp) pcdata)
let cst_nil = Types.(Atom Sequence.nil_atom)
let capture_all vars p = IdSet.fold (fun p x -> mk_and p (mk_capture x)) p vars
let termin b vars p =
if b then p
else IdSet.fold (fun p x -> seq p (PGuard (mk_constant x cst_nil))) p vars
type re =
| Epsilon
| Empty
| Elem of node
| Guard of node
| Seq of re * re
| Alt of re * re
| Star of re
| WeakStar of re
| SeqCapture of id * re
let mk_empty = Empty
let mk_epsilon = Epsilon
let mk_elem n = Elem n
let mk_guard n = Guard n
let mk_seq n1 n2 = Seq (n1, n2)
let mk_alt n1 n2 = Alt (n1, n2)
let mk_star n = Star n
let mk_weakstar n = WeakStar n
let mk_seqcapt x n = SeqCapture (x, n)
let mk_str s =
let j = Encodings.Utf8.end_index s in
let rec aux i =
if Encodings.Utf8.equal_index i j then Epsilon
else
let c, i = Encodings.Utf8.next s i in
let t = Types.(char CharSet.(atom (V.mk_int c))) in
Seq (Elem (mk_type t), aux i)
in
aux (Encodings.Utf8.start_index s)
let rec prepare_regexp vars b rvars f = function
(* - vars: seq variables to be propagated top-down and added
to each captured element
- b: below a star ?
- rvars: seq variables that appear on the right of the regexp
- f: tail position
returns the set of seq variable of the regexp minus rvars
(they have already been terminated if not below a star)
*)
| Epsilon -> (PSeq [], IdSet.empty)
| Empty -> (PAlt [], IdSet.empty)
| Elem p -> (PElem (capture_all vars p), IdSet.empty)
| Guard p -> (PGuard p, IdSet.empty)
| Seq (p1, p2) ->
let p2, v2 = prepare_regexp vars b rvars f p2 in
let p1, v1 = prepare_regexp vars b (IdSet.cup rvars v2) false p1 in
(seq p1 p2, IdSet.cup v1 v2)
| Alt (p1, p2) ->
let p1, v1 = prepare_regexp vars b rvars f p1
and p2, v2 = prepare_regexp vars b rvars f p2 in
( alt (termin b (IdSet.diff v2 v1) p1) (termin b (IdSet.diff v1 v2) p2),
IdSet.cup v1 v2 )
| Star p ->
let p, v = prepare_regexp vars true rvars false p in
(termin b v (PStar p), v)
| WeakStar p ->
let p, v = prepare_regexp vars true rvars false p in
(termin b v (PWeakStar p), v)
| SeqCapture (x, p) ->
let vars = if f then vars else IdSet.add x vars in
let after = IdSet.mem rvars x in
let rvars = IdSet.add x rvars in
let p, v = prepare_regexp vars b rvars false p in
( (if f then seq (PGuard (mk (ICapture x))) p
else termin (after || b) (IdSet.singleton x) p),
if after then v else IdSet.add x v )
let rexp r =
let r, _ = prepare_regexp IdSet.empty false IdSet.empty true r in
remove_regexp r (mk_type Types.Sequence.nil_type)
let rexp_simplify ~mix r =
let r, _ = prepare_regexp IdSet.empty false IdSet.empty true r in
let r = if mix then mix_regexp r else r in
let r = simplify_regexp r in
remove_regexp r (mk_type Types.Sequence.nil_type)
let check_wf p =
let rec aux q =
if p == q then raise Exit;
aux2 q.desc
and aux2 = function
| IOr (q1, q2, _)
| IAnd (q1, q2, _)
| IDiff (q1, q2, _) ->
aux q1;
aux q2
| ILink q -> aux q
| _ -> ()
in
try
aux2 p.desc;
true
with
| Exit -> false
module H = Hashtbl.Make (Types)
let rec elim_concat n =
match n.desc with
| IConcat (a, b, err) ->
if n.sid > 0 then raise (err "Ill-formed concatenation loop");
n.sid <- 1;
n.desc <- ILink (elim_conc a b err)
| IMerge (a, b, err) ->
if n.sid > 0 then raise (err "Ill-formed merge loop");
n.sid <- 1;
n.desc <- ILink (elim_merge a b err)
| _ -> ()
and elim_merge a b err =
let get_rec t =
let t = Types.Record.get t in
List.map
(fun (l, o, _) ->
( o,
LabelMap.map
(fun (opt, x) ->
let x = mk_type x in
((if opt then mk_optional x else x), None))
l ))
t
in
let merge (o1, l1) (o2, l2) =
mk_record (o1 || o2) (LabelMap.merge (fun _ x -> x) l1 l2)
in
(* Problem: repr can loop with ill-formed recursion.
type t = s + t where s = s | s;; *)
let a = repr a
and b = repr b in
elim_concat a;
elim_concat b;
let a = repr a
and b = repr b in
match (a.desc, b.desc) with
| IType (t1, _), IType (t2, _) ->
if not (Types.subtype t1 Types.Rec.any) then
raise (err "Left argument of record concatenation is not a record type");
if not (Types.subtype t2 Types.Rec.any) then
raise
(err "Right argument of record concatenation is not a record type");
mk_type (Types.Record.merge t1 t2)
| IOr (a1, a2, _), _ -> mk_or (elim_merge a1 b err) (elim_merge a2 b err)
| _, IOr (b1, b2, _) -> mk_or (elim_merge a b1 err) (elim_merge a b2 err)
| IRecord (o1, l1, _), IRecord (o2, l2, _) -> merge (o1, l1) (o2, l2)
| IType (t1, _), IRecord (o2, l2, _) ->
if not (Types.subtype t1 Types.Rec.any) then
raise (err "Left argument of record concatenation is not a record type");
List.fold_left
(fun accu (o1, l1) -> mk_or accu (merge (o1, l1) (o2, l2)))
iempty (get_rec t1)
| IRecord (o1, l1, _), IType (t2, _) ->
if not (Types.subtype t2 Types.Rec.any) then
raise
(err "Right argument of record concatenation is not a record type");
List.fold_left
(fun accu (o2, l2) -> mk_or accu (merge (o1, l1) (o2, l2)))
iempty (get_rec t2)
| _ -> raise (err "Cannot compute record concatenation")
and elim_conc n q err =
let mem = ref [] in
let rec aux n =
try List.assq n !mem with
| Not_found ->
let r = mk_delayed () in
mem := (n, r) :: !mem;
let rec aux2 n =
match n.desc with
| ILink n' -> aux2 n'
| IOr (a, b, _) -> mk_or (aux a) (aux b)
| ITimes (a, b) -> mk_prod a (aux b)
| IConcat (a, b, _) ->
elim_concat n;
aux2 n
| IType (t, _) -> elim_concat_type t q err
| _ -> raise (err "Cannot compute concatenation")
in
r.desc <- ILink (aux2 n);
r
in
aux n
and elim_concat_type t q err =
if not Types.(subtype t Sequence.any) then
raise (err "Left argument of concatenation is not a sequence type");
let mem = H.create 17 in
let rec aux t =
try H.find mem t with
| Not_found ->
let n = mk_delayed () in
H.add mem t n;
let d =
List.fold_left
(fun accu (t1, t2) -> mk_or accu (mk_prod (mk_type t1) (aux t2)))
(if Types.(AtomSet.contains Sequence.nil_atom (Atom.get t)) then q
else iempty)
(Types.Product.get t)
in
n.desc <- ILink d;
n
in
aux t
let elim_concats () =
try
List.iter elim_concat !concats;
List.iter (fun n -> n.sid <- 0) !concats;
concats := []
with
| exn ->
List.iter (fun n -> n.sid <- 0) !concats;
concats := [];
raise exn
let link a b = a.desc <- ILink b
let get_ct c =
let c = repr c in
match c.desc with
| ITimes (k, content) -> (
match (repr k).desc with
| IType (t, _) -> (t, content)
| _ -> assert false)
| _ -> assert false
lang/typing/patterns.ml
open Ident
let get_opt = function
| Some x -> x
| None -> assert false
(*
To be sure not to use generic comparison ...
*)
let ( = ) : int -> int -> bool = ( == )
let ( < ) : int -> int -> bool = ( < )
let ( <= ) : int -> int -> bool = ( <= )
let ( <> ) : int -> int -> bool = ( <> )
let compare = 1
(* Syntactic algebra *)
(* Constraint: any node except Constr has fv<>[] ... *)
type d =
| Constr of Types.t
| Cup of descr * descr
| Cap of descr * descr
| Times of node * node
| Xml of node * node
| Record of label * node
| Capture of id
| Constant of id * Types.const
| Dummy
and node = {
id : int;
mutable descr : descr;
accept : Types.Node.t;
fv : fv;
}
and descr = Types.t * fv * d
let id x = x.id
let descr x = x.descr
let fv x = x.fv
let accept x = Types.internalize x.accept
let printed = ref []
let to_print = ref []
let rec print ppf (a, _, d) =
match d with
| Constr t -> Types.Print.print ppf t
| Cup (p1, p2) -> Format.fprintf ppf "(%a | %a)" print p1 print p2
| Cap (p1, p2) -> Format.fprintf ppf "(%a & %a)" print p1 print p2
| Times (n1, n2) ->
Format.fprintf ppf "(P%i,P%i)" n1.id n2.id;
to_print := n1 :: n2 :: !to_print
| Xml (n1, n2) ->
Format.fprintf ppf "XML(P%i,P%i)" n1.id n2.id;
to_print := n1 :: n2 :: !to_print
| Record (l, n) ->
Format.fprintf ppf "{ %a = P%i }" Label.print_attr l n.id;
to_print := n :: !to_print
| Capture x -> Format.fprintf ppf "%a" Ident.print x
| Constant (x, c) ->
Format.fprintf ppf "(%a := %a)" Ident.print x Types.Print.print_const c
| Dummy -> Format.fprintf ppf "*DUMMY*"
let dump_print ppf =
while !to_print != [] do
let p = List.hd !to_print in
to_print := List.tl !to_print;
if not (List.mem p.id !printed) then (
printed := p.id :: !printed;
Format.fprintf ppf "P%i:=%a\n" p.id print (descr p))
done
let print ppf d =
Format.fprintf ppf "%a@\n" print d;
dump_print ppf
let print_node ppf n =
Format.fprintf ppf "P%i" n.id;
to_print := n :: !to_print;
dump_print ppf
let counter = ref 0
let dummy = (Types.empty, IdSet.empty, Dummy)
let make fv =
incr counter;
{ id = !counter; descr = dummy; accept = Types.make (); fv }
let define x ((accept, fv, _) as d) =
(* assert (x.fv = fv); *)
Types.define x.accept accept;
x.descr <- d
let cons fv d =
let q = make fv in
define q d;
q
let constr x = (x, IdSet.empty, Constr x)
let cup ((acc1, fv1, _) as x1) ((acc2, fv2, _) as x2) =
(if not (IdSet.equal fv1 fv2) then
let x =
match IdSet.pick (IdSet.diff fv1 fv2) with
| Some x -> x
| None -> get_opt (IdSet.pick (IdSet.diff fv2 fv1))
in
Cduce_error.(raise_err Typer_Pattern
("The capture variable " ^ Ident.to_string x
^ "should appear on both sides of this | pattern")));
Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1, x2)
let cap ((acc1, fv1, _) as x1) ((acc2, fv2, _) as x2) =
(if not (IdSet.disjoint fv1 fv2) then
let x = get_opt (IdSet.pick (IdSet.cap fv1 fv2)) in
Cduce_error.(raise_err Typer_Pattern
("The capture variable " ^ Ident.to_string x
^ "cannot appear on both sides of this & pattern")));
(Types.cap acc1 acc2, IdSet.cup fv1 fv2, Cap (x1, x2))
let times x y =
(Types.times x.accept y.accept, IdSet.cup x.fv y.fv, Times (x, y))
let xml x y = (Types.xml x.accept y.accept, IdSet.cup x.fv y.fv, Xml (x, y))
let record l x = (Types.record l x.accept, x.fv, Record (l, x))
let capture x = (Types.any, IdSet.singleton x, Capture x)
let constant x c = (Types.any, IdSet.singleton x, Constant (x, c))
let print_node = ref (fun _ _ -> assert false)
module Node = struct
type t = node
let compare n1 n2 = n1.id - n2.id
let equal n1 n2 = n1.id == n2.id
let hash n = n.id
let check n = ()
let dump ppf x = !print_node ppf x
end
(* Pretty-print *)
module Pat = struct
type t = descr
let rec compare (_, _, d1) (_, _, d2) =
if d1 == d2 then 0
else
match (d1, d2) with
| Constr t1, Constr t2 -> Types.compare t1 t2
| Constr _, _ -> -1
| _, Constr _ -> 1
| Cup (x1, y1), Cup (x2, y2)
| Cap (x1, y1), Cap (x2, y2) ->
let c = compare x1 x2 in
if c <> 0 then c else compare y1 y2
| Cup _, _ -> -1
| _, Cup _ -> 1
| Cap _, _ -> -1
| _, Cap _ -> 1
| Times (x1, y1), Times (x2, y2)
| Xml (x1, y1), Xml (x2, y2) ->
let c = Node.compare x1 x2 in
if c <> 0 then c else Node.compare y1 y2
| Times _, _ -> -1
| _, Times _ -> 1
| Xml _, _ -> -1
| _, Xml _ -> 1
| Record (x1, y1), Record (x2, y2) ->
let c = Label.compare x1 x2 in
if c <> 0 then c else Node.compare y1 y2
| Record _, _ -> -1
| _, Record _ -> 1
| Capture x1, Capture x2 -> Id.compare x1 x2
| Capture _, _ -> -1
| _, Capture _ -> 1
| Constant (x1, y1), Constant (x2, y2) ->
let c = Id.compare x1 x2 in
if c <> 0 then c else Types.Const.compare y1 y2
| Constant _, _ -> -1
| _, Constant _ -> 1
| Dummy, Dummy -> assert false
let equal p1 p2 = compare p1 p2 == 0
let rec hash (_, _, d) =
match d with
| Constr t -> 1 + (17 * Types.hash t)
| Cup (p1, p2) -> 2 + (17 * hash p1) + (257 * hash p2)
| Cap (p1, p2) -> 3 + (17 * hash p1) + (257 * hash p2)
| Times (q1, q2) -> 4 + (17 * q1.id) + (257 * q2.id)
| Xml (q1, q2) -> 5 + (17 * q1.id) + (257 * q2.id)
| Record (l, q) -> 6 + (17 * Label.hash l) + (257 * q.id)
| Capture x -> 7 + Id.hash x
| Constant (x, c) -> 8 + (17 * Id.hash x) + (257 * Types.Const.hash c)
| Dummy -> assert false
let check _ = assert false
let dump _ = assert false
end
module PrintN = struct
module M = Map.Make (Pat)
module S = Set.Make (Pat)
let names = ref M.empty
let printed = ref S.empty
let toprint = Queue.create ()
let id = ref 0
let rec mark seen ((_, _, d) as p) =
if M.mem p !names then ()
else if S.mem p seen then (
incr id;
names := M.add p !id !names;
Queue.add p toprint)
else
let seen = S.add p seen in
match d with
| Cup (p1, p2)
| Cap (p1, p2) ->
mark seen p1;
mark seen p2
| Times (q1, q2)
| Xml (q1, q2) ->
mark seen q1.descr;
mark seen q2.descr
| Record (_, q) -> mark seen q.descr
| _ -> ()
let rec print ppf p =
try
let i = M.find p !names in
Format.fprintf ppf "P%i" i
with
| Not_found -> real_print ppf p
and real_print ppf (_, _, d) =
match d with
| Constr t -> Types.Print.print ppf t
| Cup (p1, p2) -> Format.fprintf ppf "(%a | %a)" print p1 print p2
| Cap (p1, p2) -> Format.fprintf ppf "(%a & %a)" print p1 print p2
| Times (q1, q2) ->
Format.fprintf ppf "(%a,%a)" print q1.descr print q2.descr
| Xml (q1, { descr = _, _, Times (q2, q3) }) ->
Format.fprintf ppf "<(%a) (%a)>(%a)" print q1.descr print q2.descr print
q3.descr
| Xml _ -> assert false
| Record (l, q) ->
Format.fprintf ppf "{%a=%a}" Label.print_attr l print q.descr
| Capture x -> Format.fprintf ppf "%a" Ident.print x
| Constant (x, c) ->
Format.fprintf ppf "(%a:=%a)" Ident.print x Types.Print.print_const c
| Dummy -> assert false
let print ppf p =
mark S.empty p;
print ppf p;
let first = ref true in
(try
while true do
let p = Queue.pop toprint in
if not (S.mem p !printed) then (
printed := S.add p !printed;
Format.fprintf ppf " %s@ @[%a=%a@]"
(if !first then (
first := false;
"where")
else "and")
print p real_print p)
done
with
| Queue.Empty -> ());
id := 0;
names := M.empty;
printed := S.empty
let print_xs ppf xs =
Format.fprintf ppf "{";
let rec aux = function
| [] -> ()
| [ x ] -> Ident.print ppf x
| x :: q ->
Ident.print ppf x;
Format.fprintf ppf ",";
aux q
in
aux xs;
Format.fprintf ppf "}"
end
let () = print_node := fun ppf n -> PrintN.print ppf (descr n)
(* Static semantics *)
let cup_res v1 v2 = Types.Positive.cup [ v1; v2 ]
let empty_res fv = IdMap.constant Types.(Positive.ty empty) fv
let times_res v1 v2 = Types.Positive.times v1 v2
(* Try with a hash-table *)
module MemoFilter = Map.Make (struct
type t = Types.t * node
let compare (t1, n1) (t2, n2) =
if n1.id < n2.id then -1
else if n1.id > n2.id then 1
else Types.compare t1 t2
end)
let memo_filter = ref MemoFilter.empty
let rec filter_descr t (_, fv, d) : Types.Positive.v id_map =
(* TODO: avoid is_empty t when t is not changing (Cap) *)
if Types.is_empty t then empty_res fv
else
match d with
| Constr _ -> IdMap.empty
| Cup (((a, _, _) as d1), d2) ->
IdMap.merge cup_res
(filter_descr (Types.cap t a) d1)
(filter_descr (Types.diff t a) d2)
| Cap (d1, d2) ->
IdMap.merge cup_res (filter_descr t d1) (filter_descr t d2)
| Times (p1, p2) -> filter_prod fv p1 p2 t
| Xml (p1, p2) -> filter_prod ~kind:`XML fv p1 p2 t
| Record (l, p) -> filter_node (Types.Record.project t l) p
| Capture c -> IdMap.singleton c (Types.Positive.ty t)
| Constant (c, cst) ->
IdMap.singleton c (Types.Positive.ty (Types.constant cst))
| Dummy -> assert false
and filter_prod ?kind fv p1 p2 t =
List.fold_left
(fun accu (d1, d2) ->
let term =
IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
in
IdMap.merge cup_res accu term)
(empty_res fv)
(Types.(Product.normal ?kind t) :> Types.Product.t)
and filter_node t p : Types.Positive.v id_map =
try MemoFilter.find (t, p) !memo_filter with
| Not_found ->
let _, fv, _ = descr p in
let res = IdMap.map_from_slist (fun _ -> Types.Positive.forward ()) fv in
memo_filter := MemoFilter.add (t, p) res !memo_filter;
let r = filter_descr t (descr p) in
IdMap.collide Types.Positive.define res r;
r
let filter t p =
let r = filter_node t p in
memo_filter := MemoFilter.empty;
IdMap.map Types.Positive.solve r
let filter_descr t p =
let r = filter_descr t p in
memo_filter := MemoFilter.empty;
IdMap.get (IdMap.map Types.Positive.solve r)
(* Factorization of capture variables and constant patterns *)
module Factorize = struct
module NodeTypeSet = Set.Make (Custom.Pair (Node) (Types))
let pi1 ~kind t = Types.Product.pi1 (Types.Product.get ~kind t)
let pi2 ~kind t = Types.Product.pi2 (Types.Product.get ~kind t)
(* Note: this is incomplete because of non-atomic constant patterns:
# debug approx (_,(x:=(1,2))) (1,2);;
[DEBUG:approx]
x=(1,2)
*)
let rec approx_var seen (a, fv, d) t xs =
(* assert (Types.subtype t a);
assert (IdSet.subset xs fv); *)
if IdSet.is_empty xs || Types.is_empty t then xs
else
match d with
| Cup (((a1, _, _) as p1), p2) ->
approx_var seen p2 (Types.diff t a1)
(approx_var seen p1 (Types.cap t a1) xs)
| Cap (((_, fv1, _) as p1), ((_, fv2, _) as p2)) ->
IdSet.cup
(approx_var seen p1 t (IdSet.cap fv1 xs))
(approx_var seen p2 t (IdSet.cap fv2 xs))
| Capture _ -> xs
| Constant (_, c) ->
if Types.subtype t (Types.constant c) then xs else IdSet.empty
| Times (q1, q2) ->
let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
IdSet.cap
(approx_var_node seen q1 (pi1 ~kind:`Normal t) xs)
(approx_var_node seen q2 (pi2 ~kind:`Normal t) xs)
| Xml (q1, q2) ->
let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
IdSet.cap
(approx_var_node seen q1 (pi1 ~kind:`XML t) xs)
(approx_var_node seen q2 (pi2 ~kind:`XML t) xs)
| Record _ -> IdSet.empty
| _ -> assert false
and approx_var_node seen q t xs =
if NodeTypeSet.mem (q, t) seen then xs
else approx_var (NodeTypeSet.add (q, t) seen) q.descr t xs
(* Obviously not complete ! *)
let rec approx_nil seen (a, fv, d) t xs =
assert (Types.subtype t a);
assert (IdSet.subset xs fv);
if IdSet.is_empty xs || Types.is_empty t then xs
else
match d with
| Cup (((a1, _, _) as p1), p2) ->
approx_nil seen p2 (Types.diff t a1)
(approx_nil seen p1 (Types.cap t a1) xs)
| Cap (((_, fv1, _) as p1), ((_, fv2, _) as p2)) ->
IdSet.cup
(approx_nil seen p1 t (IdSet.cap fv1 xs))
(approx_nil seen p2 t (IdSet.cap fv2 xs))
| Constant (_, c) when Types.(Const.equal c Sequence.nil_cst) -> xs
| Times (q1, q2) ->
let xs = IdSet.cap q2.fv (IdSet.diff xs q1.fv) in
approx_nil_node seen q2 (pi2 ~kind:`Normal t) xs
| _ -> IdSet.empty
and approx_nil_node seen q t xs =
if NodeTypeSet.mem (q, t) seen then xs
else approx_nil (NodeTypeSet.add (q, t) seen) q.descr t xs
(*
let cst ((a,_,_) as p) t xs =
if IdSet.is_empty xs then IdMap.empty
else
let rec aux accu (x,t) =
if (IdSet.mem xs x) then
match Sample.single_opt (Types.descr t) with
| Some c -> (x,c)::accu
| None -> accu
else accu in
let t = Types.cap t a in
IdMap.from_list_disj (List.fold_left aux [] (filter_descr t p))
*)
let var ((a, _, _) as p) t = approx_var NodeTypeSet.empty p (Types.cap t a)
let nil ((a, _, _) as p) t = approx_nil NodeTypeSet.empty p (Types.cap t a)
end
(* Normal forms for patterns and compilation *)
let min (a : int) (b : int) = if a < b then a else b
let any_basic = Types.Record.or_absent Types.non_constructed
let rec first_label (acc, fv, d) =
if Types.is_empty acc then Label.dummy
else
match d with
| Constr t -> Types.Record.first_label t
| Cap (p, q) -> Label.min (first_label p) (first_label q)
| Cup (((acc1, _, _) as p), q) -> Label.min (first_label p) (first_label q)
| Record (l, p) -> l
| _ -> Label.dummy
module Normal = struct
type source =
| SCatch
| SConst of Types.const
type result = source id_map
let compare_source s1 s2 =
if s1 == s2 then 0
else
match (s1, s2) with
| SCatch, _ -> -1
| _, SCatch -> 1
| SConst c1, SConst c2 -> Types.Const.compare c1 c2
(*
let hash_source = function
| SCatch -> 1
| SConst c -> Types.Const.hash c
*)
let compare_result r1 r2 = IdMap.compare compare_source r1 r2
module ResultMap = Map.Make (struct
type t = result
let compare = compare_result
end)
module NodeSet = SortedList.Make (Node)
module Nnf = struct
include Custom.Dummy
type t = NodeSet.t * Types.t * IdSet.t (* pl,t; t <= \accept{pl} *)
let check (pl, t, xs) =
List.iter
(fun p -> assert (Types.subtype t (Types.descr p.accept)))
(NodeSet.get pl)
let print ppf (pl, t, xs) =
Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]" NodeSet.dump pl
Types.Print.print t IdSet.dump xs
let compare (l1, t1, xs1) (l2, t2, xs2) =
let c = NodeSet.compare l1 l2 in
if c <> 0 then c
else
let c = Types.compare t1 t2 in
if c <> 0 then c else IdSet.compare xs1 xs2
let hash (l, t, xs) =
NodeSet.hash l + (17 * Types.hash t) + (257 * IdSet.hash xs)
let equal x y = compare x y == 0
let first_label (pl, t, xs) =
NodeSet.fold
(fun l p -> Label.min l (first_label (descr p)))
(Types.Record.first_label t)
pl
end
module NProd = struct
type t = result * Nnf.t * Nnf.t
let compare (r1, x1, y1) (r2, x2, y2) =
let c = compare_result r1 r2 in
if c <> 0 then c
else
let c = Nnf.compare x1 x2 in
if c <> 0 then c else Nnf.compare y1 y2
end
module NLineProd = Set.Make (NProd)
type record =
| RecNolabel of result option * result option
| RecLabel of label * NLineProd.t
type t = {
nprod : NLineProd.t;
nxml : NLineProd.t;
nrecord : record;
}
let fus = IdMap.union_disj
let nempty lab =
{
nprod = NLineProd.empty;
nxml = NLineProd.empty;
nrecord =
(match lab with
| Some l -> RecLabel (l, NLineProd.empty)
| None -> RecNolabel (None, None));
}
let dummy = nempty None
let ncup nf1 nf2 =
{
nprod = NLineProd.union nf1.nprod nf2.nprod;
nxml = NLineProd.union nf1.nxml nf2.nxml;
nrecord =
(match (nf1.nrecord, nf2.nrecord) with
| RecLabel (l1, r1), RecLabel (l2, r2) ->
(* assert (l1 = l2); *)
RecLabel (l1, NLineProd.union r1 r2)
| RecNolabel (x1, y1), RecNolabel (x2, y2) ->
RecNolabel
((if x1 == None then x2 else x1), if y1 == None then y2 else y1)
| _ -> assert false);
}
let double_fold_prod f l1 l2 =
NLineProd.fold
(fun x1 accu -> NLineProd.fold (fun x2 accu -> f accu x1 x2) l2 accu)
l1 NLineProd.empty
let ncap nf1 nf2 =
let prod
accu
(res1, (pl1, t1, xs1), (ql1, s1, ys1))
(res2, (pl2, t2, xs2), (ql2, s2, ys2)) =
let t = Types.cap t1 t2 in
if Types.is_empty t then accu
else
let s = Types.cap s1 s2 in
if Types.is_empty s then accu
else
NLineProd.add
( fus res1 res2,
(NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
(NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2) )
accu
in
let record r1 r2 =
match (r1, r2) with
| RecLabel (l1, r1), RecLabel (l2, r2) ->
(* assert (l1 = l2); *)
RecLabel (l1, double_fold_prod prod r1 r2)
| RecNolabel (x1, y1), RecNolabel (x2, y2) ->
let x =
match (x1, x2) with
| Some res1, Some res2 -> Some (fus res1 res2)
| _ -> None
and y =
match (y1, y2) with
| Some res1, Some res2 -> Some (fus res1 res2)
| _ -> None
in
RecNolabel (x, y)
| _ -> assert false
in
{
nprod = double_fold_prod prod nf1.nprod nf2.nprod;
nxml = double_fold_prod prod nf1.nxml nf2.nxml;
nrecord = record nf1.nrecord nf2.nrecord;
}
let nnode p xs = (NodeSet.singleton p, Types.descr p.accept, xs)
let nc t = (NodeSet.empty, t, IdSet.empty)
let ncany = nc Types.any
let ncany_abs = nc Types.Record.any_or_absent
let empty_res = IdMap.empty
let single_prod src p q = NLineProd.singleton (src, p, q)
let ntimes lab acc p q xs =
let xsp = IdSet.cap xs p.fv
and xsq = IdSet.cap xs q.fv in
{
(nempty lab) with
nprod = single_prod empty_res (nnode p xsp) (nnode q xsq);
}
let nxml lab acc p q xs =
let xsp = IdSet.cap xs p.fv
and xsq = IdSet.cap xs q.fv in
{
(nempty lab) with
nxml = single_prod empty_res (nnode p xsp) (nnode q xsq);
}
let nrecord (lab : Label.t option) acc (l : Label.t) p xs =
let label = get_opt lab in
(* Format.fprintf
Format.std_formatter "label=%a l=%a@."
Label.print label Label.print l; *)
assert (Label.compare label l <= 0);
let lft, rgt =
if Label.equal l label then (nnode p xs, ncany)
else (ncany_abs, nnode (cons p.fv (record l p)) xs)
in
{
(nempty lab) with
nrecord = RecLabel (label, single_prod empty_res lft rgt);
}
let nconstr lab t =
let aux l =
List.fold_left
(fun accu (t1, t2) -> NLineProd.add (empty_res, nc t1, nc t2) accu)
NLineProd.empty l
in
let record =
match lab with
| None ->
let x, y = Types.Record.empty_cases t in
RecNolabel
( (if x then Some empty_res else None),
if y then Some empty_res else None )
| Some l -> RecLabel (l, aux (Types.Record.split_normal t l))
in
{
nprod = aux (Types.Product.clean_normal (Types.Product.normal t));
nxml =
aux (Types.Product.clean_normal (Types.Product.normal ~kind:`XML t));
nrecord = record;
}
let nany lab res =
{
nprod = single_prod res ncany ncany;
nxml = single_prod res ncany ncany;
nrecord =
(match lab with
| None -> RecNolabel (Some res, Some res)
| Some lab -> RecLabel (lab, single_prod res ncany_abs ncany));
}
let nconstant lab x c = nany lab (IdMap.singleton x (SConst c))
let ncapture lab x = nany lab (IdMap.singleton x SCatch)
let rec nnormal lab (acc, fv, d) xs =
let xs = IdSet.cap xs fv in
if Types.is_empty acc then nempty lab
else if IdSet.is_empty xs then nconstr lab acc
else
match d with
| Constr t -> assert false
| Cap (p, q) -> ncap (nnormal lab p xs) (nnormal lab q xs)
| Cup (((acc1, _, _) as p), q) ->
ncup (nnormal lab p xs)
(ncap (nnormal lab q xs) (nconstr lab (Types.neg acc1)))
| Times (p, q) -> ntimes lab acc p q xs
| Xml (p, q) -> nxml lab acc p q xs
| Capture x -> ncapture lab x
| Constant (x, c) -> nconstant lab x c
| Record (l, p) -> nrecord lab acc l p xs
| Dummy -> assert false
(*TODO: when an operand of Cap has its first_label > lab,
directly shift it*)
let facto f t xs pl =
NodeSet.fold
(fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs)))
IdSet.empty pl
let factorize t0 (pl, t, xs) =
let t0 = if Types.subtype t t0 then t else Types.cap t t0 in
let vs_var = facto Factorize.var t0 xs pl in
let xs = IdSet.diff xs vs_var in
let vs_nil = facto Factorize.nil t0 xs pl in
let xs = IdSet.diff xs vs_nil in
(vs_var, vs_nil, (pl, t, xs))
let normal l t pl xs =
NodeSet.fold (fun a p -> ncap a (nnormal l (descr p) xs)) (nconstr l t) pl
let nnf lab t0 (pl, t, xs) =
(* assert (not (Types.disjoint t t0)); *)
let t = if Types.subtype t t0 then t else Types.cap t t0 in
normal lab t pl xs
let basic_tests f ((pl, t, xs) : NodeSet.t * _ * _) =
let rec aux more s accu t res = function
(* Invariant: t and s disjoint, t not empty *)
| [] ->
let accu =
try
let t' = ResultMap.find res accu in
ResultMap.add res (Types.cup t t') accu
with
| Not_found -> ResultMap.add res t accu
in
cont (Types.cup t s) accu more
| (tp, xp, d) :: r -> (
if IdSet.disjoint xp xs then
aux_check more s accu (Types.cap t tp) res r
else
match d with
| Cup (p1, p2) ->
aux ((t, res, p2 :: r) :: more) s accu t res (p1 :: r)
| Cap (p1, p2) -> aux more s accu t res (p1 :: p2 :: r)
| Capture x -> aux more s accu t (IdMap.add x SCatch res) r
| Constant (x, c) ->
aux more s accu t (IdMap.add x (SConst c) res) r
| _ -> cont s accu more)
and aux_check more s accu t res pl =
if Types.is_empty t then cont s accu more else aux more s accu t res pl
and cont s accu = function
| [] -> ResultMap.iter f accu
| (t, res, pl) :: tl -> aux_check tl s accu (Types.diff t s) res pl
in
aux_check [] Types.empty ResultMap.empty (Types.cap t any_basic) IdMap.empty
(List.map descr (pl :> Node.t list))
(*
let prod_tests (pl,t,xs) =
let rec aux accu q1 q2 res = function
| [] -> (res,q1,q2) :: accu
| (tp,xp,d) :: r ->
if (IdSet.disjoint xp xs)
then aux_check accu q1 q2 res tp r
else match d with
| Cup (p1,p2) -> aux (aux accu q1 q2 res (p2::r)) q1 q2 res (p1::r)
| Cap (p1,p2) -> aux accu q1 q2 res (p1 :: p2 :: r)
| Capture x -> aux accu q1 q2 (IdMap.add x SCatch res) r
| Constant (x,c) -> aux accu q1 q2 (IdMap.add x (SConst c) res) r
| Times (p1,p2) ->
let (pl1,t1,xs1) = q1 and (pl2,t2,xs2) = q2 in
let t1 = Types.cap t1 (Types.descr (accept p1)) in
if Types.is_empty t1 then accu
else let t2 = Types.cap t2 (Types.descr (accept p2)) in
if Types.is_empty t2 then accu
else
let q1 =
let xs1' = IdSet.cap (fv p1) xs in
if IdSet.is_empty xs1' then (pl1,t1,xs1)
else (NodeSet.add p1 pl1, t1, IdSet.cup xs1 xs1')
and q2 =
let xs2' = IdSet.cap (fv p2) xs in
if IdSet.is_empty xs2' then (pl2,t2,xs2)
else (NodeSet.add p2 pl2, t2, IdSet.cup xs2 xs2')
in
aux accu q1 q2 res r
| _ -> accu
and aux_check accu q1 q2 res t r =
List.fold_left
(fun accu (t1',t2') ->
let (pl1,t1,xs1) = q1 and (pl2,t2,xs2) = q2 in
let t1 = Types.cap t1 t1' in
if Types.is_empty t1 then accu
else let t2 = Types.cap t2 t2' in
if Types.is_empty t2 then accu
else aux accu (pl1,t1,xs1) (pl2,t2,xs2) res r)
accu (Types.Product.clean_normal (Types.Product.normal t))
in
aux_check [] ncany ncany IdMap.empty t (List.map descr pl)
*)
end
module Compile = struct
open Auto_pat
type return_code =
Types.t * int * (* accepted type, arity *)
int id_map option array
type interface =
[ `Result of int
| `Switch of interface * interface
| `None
]
type dispatcher = {
id : int;
t : Types.t;
pl : Normal.Nnf.t array;
label : label option;
interface : interface;
codes : return_code array;
state : state;
}
let dispatcher_of_state = Hashtbl.create 1024
let equal_array f a1 a2 =
let rec aux i = i < 0 || (f a1.(i) a2.(i) && aux (i - 1)) in
let l1 = Array.length a1
and l2 = Array.length a2 in
l1 == l2 && aux (l1 - 1)
let array_for_all f a =
let rec aux f a i = i < 0 || (f a.(i) && aux f a (pred i)) in
aux f a (Array.length a - 1)
let array_for_all_i f a =
let rec aux f a i = i < 0 || (f i a.(i) && aux f a (pred i)) in
aux f a (Array.length a - 1)
let equal_source s1 s2 =
s1 == s2
||
match (s1, s2) with
| Const x, Const y -> Types.Const.equal x y
| Stack x, Stack y -> x == y
| Recompose (x1, x2), Recompose (y1, y2) -> x1 == y1 && x2 == y2
| _ -> false
let equal_result (r1, s1, l1) (r2, s2, l2) =
r1 == r2 && equal_array equal_source s1 s2 && l1 == l2
let equal_result_dispatch d1 d2 =
d1 == d2
||
match (d1, d2) with
| Dispatch (d1, a1), Dispatch (d2, a2) ->
d1 == d2 && equal_array equal_result a1 a2
| TailCall d1, TailCall d2 -> d1 == d2
| Ignore a1, Ignore a2 -> equal_result a1 a2
| _ -> false
let immediate_res basic prod xml record =
let res : result option ref = ref None in
let chk = function
| Catch
| Const _ ->
true
| _ -> false
in
let f ((_, ret, _) as r) =
match !res with
| Some r0 when equal_result r r0 -> ()
| None when array_for_all chk ret -> res := Some r
| _ -> raise Exit
in
(match basic with
| [ (_, r) ] -> f r
| [] -> ()
| _ -> raise Exit);
(match prod with
| Ignore (Ignore r) -> f r
| Impossible -> ()
| _ -> raise Exit);
(match xml with
| Ignore (Ignore r) -> f r
| Impossible -> ()
| _ -> raise Exit);
(match record with
| None -> ()
| Some (RecLabel (_, Ignore (Ignore r))) -> f r
| Some (RecNolabel (Some r1, Some r2)) ->
f r1;
f r2
| _ -> raise Exit);
match !res with
| Some r -> r
| None -> raise Exit
let split_kind basic prod xml record =
{
basic;
atoms =
AtomSet.mk_map (List.map (fun (t, r) -> (Types.Atom.get t, r)) basic);
chars =
CharSet.mk_map (List.map (fun (t, r) -> (Types.Char.get t, r)) basic);
prod;
xml;
record;
}
let combine_kind basic prod xml record =
try AIgnore (immediate_res basic prod xml record) with
| Exit -> AKind (split_kind basic prod xml record)
let combine f (disp, act) =
if Array.length act == 0 then Impossible
else if
array_for_all (fun (_, ar, _) -> ar == 0) disp.codes
&& array_for_all (f act.(0)) act
then Ignore act.(0)
else Dispatch (disp.state, act)
let detect_tail_call f = function
| Dispatch (disp, branches) when array_for_all_i f branches -> TailCall disp
| x -> x
let detect_right_tail_call =
detect_tail_call (fun i (code, ret, _) ->
i == code
&&
let ar = Array.length ret in
array_for_all_i
(fun pos -> function
| Stack j when pos + j == ar -> true
| _ -> false)
ret)
let detect_left_tail_call =
detect_tail_call (fun i -> function
| Ignore (code, ret, _) when i == code ->
let ar = Array.length ret in
array_for_all_i
(fun pos -> function
| Stack j when pos + j == ar -> true
| _ -> false)
ret
| _ -> false)
let cur_id = ref 0
module NfMap = Map.Make (Normal.Nnf)
module NfSet = Set.Make (Normal.Nnf)
module DispMap = Map.Make (Custom.Pair (Types) (Custom.Array (Normal.Nnf)))
(* Try with a hash-table ! *)
let dispatchers = ref DispMap.empty
let rec print_iface ppf = function
| `Result i -> Format.fprintf ppf "Result(%i)" i
| `Switch (yes, no) ->
Format.fprintf ppf "Switch(%a,%a)" print_iface yes print_iface no
| `None -> Format.fprintf ppf "None"
let dump_disp disp =
let ppf = Format.std_formatter in
Format.fprintf ppf "Dispatcher t=%a@." Types.Print.print disp.t;
Array.iter
(fun p -> Format.fprintf ppf " pat %a@." Normal.Nnf.print p)
disp.pl
let first_lab t reqs =
let aux l req = Label.min l (Normal.Nnf.first_label req) in
let lab = Array.fold_left aux (Types.Record.first_label t) reqs in
if lab == Label.dummy then None else Some lab
let dummy_actions = AIgnore (-1, [||], -1)
let compute_actions = ref (fun _ -> assert false)
let dispatcher t pl : dispatcher =
try DispMap.find (t, pl) !dispatchers with
| Not_found ->
let lab = first_lab t pl in
let nb = ref 0 in
let codes = ref [] in
let rec aux t arity i accu =
if i == Array.length pl then (
incr nb;
let r = Array.of_list (List.rev accu) in
codes := (t, arity, r) :: !codes;
`Result (!nb - 1))
else
let _, tp, v = pl.(i) in
let a1 = Types.cap t tp in
if Types.is_empty a1 then
`Switch (`None, aux t arity (i + 1) (None :: accu))
else
let a2 = Types.diff t tp in
let accu' = Some (IdMap.num arity v) :: accu in
if Types.is_empty a2 then
`Switch (aux t (arity + IdSet.length v) (i + 1) accu', `None)
else
`Switch
( aux a1 (arity + IdSet.length v) (i + 1) accu',
aux a2 arity (i + 1) (None :: accu) )
(* Unopt version:
`Switch
(
aux (Types.cap t tp) (arity + (IdSet.length v)) (i+1) accu',
aux (Types.diff t tp) arity (i+1) accu
)
*)
in
let iface = if Types.is_empty t then `None else aux t 0 0 [] in
let codes = Array.of_list (List.rev !codes) in
let state =
{
uid = !cur_id;
arity = Array.map (fun (_, ar, _) -> ar) codes;
actions = dummy_actions;
fail_code = -1;
expected_type = "";
}
in
let disp =
{ id = !cur_id; t; label = lab; pl; interface = iface; codes; state }
in
incr cur_id;
Hashtbl.add dispatcher_of_state state.uid disp;
dispatchers := DispMap.add (t, pl) disp !dispatchers;
!compute_actions disp;
disp
let find_code d a =
let rec aux i = function
| `Result code -> code
| `None ->
Format.fprintf Format.std_formatter "IFACE=%a@." print_iface
d.interface;
for i = 0 to Array.length a - 1 do
Format.fprintf Format.std_formatter "a.(%i)=%b@." i (a.(i) != None)
done;
assert false
| `Switch (yes, _) when a.(i) != None -> aux (i + 1) yes
| `Switch (_, no) -> aux (i + 1) no
in
aux 0 d.interface
let create_result pl =
let aux x accu =
match x with
| Some b -> b @ accu
| None -> accu
in
Array.of_list (Array.fold_right aux pl [])
let return disp pl f ar =
let aux = function
| x :: _ -> Some (f x)
| [] -> None
in
let final = Array.map aux pl in
(find_code disp final, create_result final, ar)
let conv_source = function
| Normal.SCatch -> Catch
| Normal.SConst c -> Const c
let return_basic disp selected =
let aux_final res = IdMap.map_to_list conv_source res in
return disp selected aux_final 0
(* let print_idset ppf s =
let s = String.concat "," (List.map (fun x -> Ident.to_string x) s) in
Format.fprintf ppf "{%s}" s
let print_idmap ppf s =
print_idset ppf (IdMap.domain s) *)
let merge_res_prod ofs1 ofs2 (lvars, lnils, lres) (rvars, rnils, rres) extra =
let lres =
IdMap.union_disj
(IdMap.map (fun i -> Stack (ofs1 + ofs2 - i)) lres)
(IdMap.union_disj
(IdMap.constant Left lvars)
(IdMap.constant Nil lnils))
in
let rres =
IdMap.union_disj
(IdMap.map (fun i -> Stack (ofs2 - i)) rres)
(IdMap.union_disj
(IdMap.constant Right rvars)
(IdMap.constant Nil rnils))
in
let sub =
IdMap.merge
(fun l r ->
match (l, r) with
| Left, Right -> Catch
| _ ->
let l =
match l with
| Left -> -1
| Nil -> -2
| Stack i -> i
| _ -> assert false
in
let r =
match r with
| Right -> -1
| Nil -> -2
| Stack i -> i
| _ -> assert false
in
Recompose (l, r))
lres rres
in
IdMap.map_to_list
(fun x -> x)
(IdMap.union_disj sub (IdMap.map conv_source extra))
module TypeList = SortedList.Make (Types)
let dispatch_basic disp : (Types.t * result) list =
let tests =
let accu = ref [] in
let aux i res t = accu := (t, [ (i, res) ]) :: !accu in
Array.iteri (fun i p -> Normal.basic_tests (aux i) p) disp.pl;
TypeList.Map.get (TypeList.Map.from_list ( @ ) !accu)
in
let t = Types.cap any_basic disp.t in
let accu = ref [] in
let rec aux (success : (int * Normal.result) list) t l =
if Types.non_empty t then
match l with
| [] ->
let selected = Array.make (Array.length disp.pl) [] in
let add (i, res) = selected.(i) <- res :: selected.(i) in
List.iter add success;
accu := (t, return_basic disp selected) :: !accu
| (ty, i) :: rem ->
aux (i @ success) (Types.cap t ty) rem;
aux success (Types.diff t ty) rem
in
aux [] t tests;
!accu
let get_tests facto pl f t d post =
let pl = Array.map (List.map f) pl in
let factorized = ref NfMap.empty in
(* Collect all subrequests *)
let aux reqs (req, _) =
let ((_, _, ((_, tr, xs) as r')) as req') =
if facto then Normal.factorize t req else IdSet.(empty, empty, req)
in
factorized := NfMap.add req req' !factorized;
if IdSet.is_empty xs && Types.subtype t tr then reqs
else NfSet.add r' reqs
in
let reqs = Array.fold_left (List.fold_left aux) NfSet.empty pl in
let reqs = Array.of_list (NfSet.elements reqs) in
(* Map subrequest -> idx in reqs *)
let idx = ref NfMap.empty in
Array.iteri (fun i req -> idx := NfMap.add req i !idx) reqs;
let idx = !idx in
(* Build dispatcher *)
(* if Array.length reqs = 0 then print_endline "NOREQ!"; *)
let disp =
dispatcher
(if Array.length reqs = 0 then Types.Record.any_or_absent else t)
reqs
in
(* Build continuation *)
let result (t, ar, m) =
let get (req, info) a =
let var, nil, r' =
try NfMap.find req !factorized with
| Not_found -> assert false
in
try
let i = NfMap.find r' idx in
match m.(i) with
| Some res -> ((var, nil, res), info) :: a
| _ -> a
with
| Not_found -> ((var, nil, IdMap.empty), info) :: a
in
let pl = Array.map (fun l -> List.fold_right get l []) pl in
d t ar pl
in
let res = Array.map result disp.codes in
post (disp, res)
let add_factorized disp rhs =
let result ((code, srcs, pop) as r) =
match rhs.(code) with
| Fail -> r
| Match (_, (var, nil, xs, _)) ->
let pos = ref (-1) in
let var x =
if IdSet.mem var x then Catch
else if IdSet.mem nil x then Nil
else (
incr pos;
srcs.(!pos))
in
let srcs' = Array.of_list (List.map var (IdSet.get xs)) in
assert (succ !pos = Array.length srcs);
(code, srcs', pop)
in
let dispatch1 = function
| Dispatch (s, a) -> Dispatch (s, Array.map result a)
| TailCall s ->
let f code (_, ar, _) =
let srcs = Array.init ar (fun i -> Stack (ar - i)) in
result (code, srcs, ar)
in
Dispatch (s, Array.mapi f disp.codes)
| Ignore r -> Ignore (result r)
| Impossible -> Impossible
in
let dispatch2 = function
| Dispatch (s, a) -> Dispatch (s, Array.map dispatch1 a)
| TailCall s ->
let f code (_, ar, _) =
let srcs = Array.init ar (fun i -> Stack (ar - i)) in
Ignore (result (code, srcs, ar))
in
Dispatch (s, Array.mapi f disp.codes)
| Ignore r -> Ignore (dispatch1 r)
| Impossible -> Impossible
in
let state = disp.state in
let actions =
match state.actions with
| AIgnore r -> AIgnore (result r)
| AKind k ->
AKind
{
basic = List.map (fun (t, r) -> (t, result r)) k.basic;
atoms = AtomSet.map_map result k.atoms;
chars = CharSet.map_map result k.chars;
prod = dispatch2 k.prod;
xml = dispatch2 k.xml;
record =
(match k.record with
| None -> None
| Some (RecLabel (l, x)) -> Some (RecLabel (l, dispatch2 x))
| Some (RecNolabel (x, y)) ->
Some
(RecNolabel
( (match x with
| None -> None
| Some r -> Some (result r)),
match y with
| None -> None
| Some r -> Some (result r) )));
}
in
{ state with actions }
let make_branches t brs =
let t0 = ref t in
let aux (p, e) =
let xs = fv p in
let tp = Types.descr (accept p) in
let nnf = (Normal.NodeSet.singleton p, Types.cap !t0 tp, xs) in
t0 := Types.diff !t0 tp;
[ (nnf, (xs, e)) ]
in
let has_facto = ref false in
let res _ _ pl =
let aux r = function
| [ ((var, nil, res), (xs, e)) ] ->
assert (r == Fail);
let i = ref 0 in
IdSet.iter
(fun x ->
if IdSet.mem var x || IdSet.mem nil x then has_facto := true
else (
assert (IdMap.assoc x res = !i);
incr i))
xs;
Match (IdSet.length xs, (var, nil, xs, e))
| [] -> r
| _ -> assert false
in
Array.fold_left aux Fail pl
in
(* Format.fprintf Format.std_formatter
"make_branches t=%a #branches=%i@." Types.Print.print t (List.length brs); *)
let pl = Array.map aux (Array.of_list brs) in
let disp, rhs = get_tests true pl (fun x -> x) t res (fun x -> x) in
let state = if !has_facto then add_factorized disp rhs else disp.state in
( state,
Array.map
(function
| Match (n, (_, _, _, e)) -> Match (n, e)
| Fail -> Fail)
rhs )
let rec dispatch_prod0 disp t pl =
get_tests true pl
(fun (res, p, q) -> (p, (res, q)))
(Types.Product.pi1 t) (dispatch_prod1 disp t)
(fun x -> detect_left_tail_call (combine equal_result_dispatch x))
and dispatch_prod1 disp t t1 ar1 pl =
get_tests true pl
(fun (ret1, (res, q)) -> (q, (ret1, res)))
(Types.Product.pi2_restricted t1 t)
(dispatch_prod2 disp ar1)
(fun x -> detect_right_tail_call (combine equal_result x))
and dispatch_prod2 disp ar1 t2 ar2 pl =
let aux_final (ret2, (ret1, res)) = merge_res_prod ar1 ar2 ret1 ret2 res in
return disp pl aux_final (ar1 + ar2)
let dispatch_prod disp pl =
let t = Types.Product.get disp.t in
if t == [] then Impossible
else
dispatch_prod0 disp t
(Array.map (fun p -> Normal.NLineProd.elements p.Normal.nprod) pl)
(* dispatch_prod0 disp t (Array.map Normal.prod_tests disp.pl) *)
let dispatch_xml disp pl =
let t = Types.Product.get ~kind:`XML disp.t in
if t == [] then Impossible
else
dispatch_prod0 disp t
(Array.map (fun p -> Normal.NLineProd.elements p.Normal.nxml) pl)
let dispatch_record disp pl : record option =
let t = disp.t in
if not (Types.Record.has_record t) then None
else
match disp.label with
| None ->
let some, none = Types.Record.empty_cases t in
let some =
if some then
let pl =
Array.map
(fun p ->
match p.Normal.nrecord with
| Normal.RecNolabel (Some x, _) -> [ x ]
| Normal.RecNolabel (None, _) -> []
| _ -> assert false)
pl
in
Some (return disp pl (IdMap.map_to_list conv_source) 0)
else None
in
let none =
if none then
let pl =
Array.map
(fun p ->
match p.Normal.nrecord with
| Normal.RecNolabel (_, Some x) -> [ x ]
| Normal.RecNolabel (_, None) -> []
| _ -> assert false)
pl
in
Some (return disp pl (IdMap.map_to_list conv_source) 0)
else None
in
Some (RecNolabel (some, none))
| Some lab ->
let t = Types.Record.split t lab in
let pl =
Array.map
(fun p ->
match p.Normal.nrecord with
| Normal.RecLabel (_, l) -> Normal.NLineProd.elements l
| _ -> assert false)
pl
in
Some (RecLabel (lab, dispatch_prod0 disp t pl))
(*
let iter_disp_disp f g = function
| Dispatch (d,a) -> f d; Array.iter g a
| TailCall d -> f d
| Ignore a -> g a
| Impossible -> ()
let iter_disp_prod f = iter_disp_disp f (iter_disp_disp f (fun _ -> ()))
let rec iter_disp_actions f = function
| AIgnore _ -> ()
| AKind k ->
iter_disp_prod f k.prod;
iter_disp_prod f k.xml;
(match k.record with Some (RecLabel (_,p)) -> iter_disp_prod f p
| _ -> ())
*)
let () =
compute_actions :=
fun disp ->
let pl = Array.map (Normal.nnf disp.label disp.t) disp.pl in
let a =
combine_kind (dispatch_basic disp) (dispatch_prod disp pl)
(dispatch_xml disp pl) (dispatch_record disp pl)
in
disp.state.actions <- a
let find_array pred a =
let res = ref (-1) in
for i = 0 to Array.length a - 1 do
if pred a.(i) then (
assert (!res = -1);
res := i)
done;
!res
let new_fail_res fail =
find_array (function
| code, _, _ when code = fail -> true
| _ -> false)
let new_fail_disp fail =
find_array (function
| Ignore (code, _, _) when code = fail -> true
| _ -> false)
let rec prepare_checker fail state =
if state.fail_code >= 0 then assert (state.fail_code == fail)
else (
state.fail_code <- fail;
let expect = ref Types.empty in
Array.iteri
(fun i (t, _, _) -> if i != fail then expect := Types.cup t !expect)
(Hashtbl.find dispatcher_of_state state.uid).codes;
state.expected_type <- Types.Print.to_string !expect;
prepare_checker_actions fail state.actions)
and prepare_checker_actions fail = function
| AIgnore _ -> ()
| AKind k -> (
prepare_checker_prod fail k.prod;
prepare_checker_prod fail k.xml;
match k.record with
| Some (RecLabel (_, d)) -> prepare_checker_prod fail d
| _ -> ())
and prepare_checker_prod fail = function
| Dispatch (state, cont) ->
let f = new_fail_disp fail cont in
if f >= 0 then prepare_checker f state;
Array.iter (prepare_checker_prod2 fail) cont
| TailCall state -> prepare_checker fail state
| Ignore d2 -> prepare_checker_prod2 fail d2
| Impossible -> ()
and prepare_checker_prod2 fail = function
| Dispatch (state, cont) ->
let f = new_fail_res fail cont in
assert (f >= 0);
prepare_checker f state
| TailCall state -> prepare_checker fail state
| Ignore _ -> ()
| Impossible -> ()
let make_checker t0 t =
let p = make IdSet.empty in
define p (constr t);
let d, rhs = make_branches t0 [ (p, ()) ] in
let code = ref (-1) in
Array.iteri
(fun (i : int) rhs ->
match rhs with
| Fail ->
assert (!code < 0);
code := i
| _ -> ())
rhs;
if !code >= 0 then prepare_checker !code d;
d
end
module Print = PrintN
lang/typing/typer.ml
open Cduce_loc
open Ast
open Ident
let ( = ) (x : int) y = x = y
let ( <= ) (x : int) y = x <= y
let ( < ) (x : int) y = x < y
let ( >= ) (x : int) y = x >= y
let ( > ) (x : int) y = x > y
let _warning loc msg =
let ppf = Format.err_formatter in
Cduce_loc.print_loc ppf (loc, `Full);
Format.fprintf ppf ": Warning: %s@." msg
type schema = {
sch_uri : string;
sch_ns : Ns.Uri.t;
sch_comps : (Types.t * Schema_validator.t) Ident.Env.t;
}
type item =
(* These are really exported by CDuce units: *)
| Type of (Types.t * Var.t list)
| Val of Types.t
| ECDuce of Compunit.t
| ESchema of schema
| ENamespace of Ns.Uri.t
(* These are only used internally: *)
| EVal of Compunit.t * id * Types.t
| EOCaml of string
| EOCamlComponent of string
| ESchemaComponent of (Types.t * Schema_validator.t)
type t = {
ids : item Env.t;
ids_loc : loc Env.t;
ns : Ns.table;
keep_ns : bool;
poly_vars : (U.t * Var.t) list;
mono_vars : Var.Set.t;
mutable weak_vars : Types.t option Var.Map.map;
}
(* Namespaces *)
let set_ns_table_for_printer env = Ns.InternalPrinter.set_table env.ns
let get_ns_table tenv = tenv.ns
let type_keep_ns env k = { env with keep_ns = k }
let protect_error_ns loc f x =
try f x with
| Ns.UnknownPrefix ns ->
Cduce_error.(raise_err_loc ~loc Generic ("Undefined namespace prefix " ^ U.to_string ns))
let qname env loc t = protect_error_ns loc (Ns.map_tag env.ns) t
let ident env loc t = protect_error_ns loc (Ns.map_attr env.ns) t
let parse_atom env loc t = AtomSet.V.mk (qname env loc t)
let parse_ns env loc ns = protect_error_ns loc (Ns.map_prefix env.ns) ns
let parse_label env loc t =
Label.mk (protect_error_ns loc (Ns.map_attr env.ns) t)
let parse_record env loc f r =
let r = List.map (fun (l, x) -> (parse_label env loc l, f x)) r in
LabelMap.from_list
(fun _ _ -> Cduce_error.raise_err_loc ~loc Generic "Duplicated record field")
r
(*fun _ _ -> assert false*)
let from_comp_unit = ref (fun _ -> assert false)
let load_comp_unit = ref (fun _ -> assert false)
let has_ocaml_unit = ref (fun _ -> false)
let has_static_external = ref (fun _ -> assert false)
let type_schema env loc name uri =
let x = ident env loc name in
let ns, sch = Schema_converter.load_schema (U.to_string name) uri in
let sch = { sch_uri = uri; sch_comps = sch; sch_ns = ns } in
{ env with ids = Env.add x (ESchema sch) env.ids }
let empty_env =
{
ids = Env.empty;
ids_loc = Env.empty;
ns = Ns.def_table;
keep_ns = false;
poly_vars = [];
mono_vars = Var.Set.empty;
weak_vars = Var.Map.empty;
}
let enter_id x i env = { env with ids = Env.add x i env.ids }
let type_using env loc x cu =
try
let cu = !load_comp_unit cu in
enter_id (ident env loc x) (ECDuce cu) env
with
| Not_found -> Cduce_error.raise_err_loc ~loc Typer_Error ("Cannot find external unit " ^ U.to_string cu)
let enter_type id t env = enter_id id (Type t) env
let enter_types l env =
{
env with
ids =
List.fold_left
(fun accu (id, t, al) -> Env.add id (Type (t, al)) accu)
env.ids l;
}
let find_id env0 env loc head x =
let id = ident env0 loc x in
try Env.find id env.ids with
| Not_found when head -> (
try ECDuce (!load_comp_unit x) with
| Not_found -> Cduce_error.(raise_err_loc ~loc Typer_Error ("Cannot resolve this identifier: " ^ U.get_str x)))
let find_id_comp env0 env loc x =
if
(match (U.get_str x).[0] with
| 'A' .. 'Z' -> true
| _ -> false)
&& !has_ocaml_unit x
then EOCaml (U.get_str x)
else find_id env0 env loc true x
let enter_value id t env = { env with ids = Env.add id (Val t) env.ids }
let enter_values l env =
{
env with
ids = List.fold_left (fun accu (id, t) -> Env.add id (Val t) accu) env.ids l;
}
let enter_values_dummy l env =
{
env with
ids =
List.fold_left
(fun accu id -> Env.add id (Val Types.empty) accu)
env.ids l;
}
let value_name_ok id env =
try
match Env.find id env.ids with
| Val _
| EVal _ ->
true
| _ -> false
with
| Not_found -> true
let iter_values env f =
Env.iter
(fun x -> function
| Val t -> f x t
| _ -> ())
env.ids
let register_types cu env =
Env.iter
(fun x t ->
match t with
| Type (t, vparams) ->
let params = List.map Types.var vparams in
Types.Print.register_global cu x ~params t
| _ -> ())
env.ids
let rec const env loc = function
| LocatedExpr (loc, e) -> const env loc e
| Pair (x, y) -> Types.Pair (const env loc x, const env loc y)
| Xml (x, y) -> Types.Xml (const env loc x, const env loc y)
| 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)
| Integer i -> Types.Integer i
| Char c -> Types.Char c
| Const c -> c
| _ -> Cduce_error.raise_err_loc ~loc Typer_InvalidConstant ()
(* I. Transform the abstract syntax of types and patterns into
the internal form *)
let find_schema_component sch name =
try ESchemaComponent (Env.find name sch.sch_comps) with
| Not_found ->
Cduce_error.(raise_err Typer_Error
(Printf.sprintf "No component named '%s' found in schema '%s'"
(Ns.QName.to_string name) sch.sch_uri))
let navig loc env0 (env, comp) id =
match comp with
| ECDuce cu ->
let env = !from_comp_unit cu in
let c =
try find_id env0 env loc false id with
| Not_found -> Cduce_error.raise_err_loc ~loc Typer_UnboundId ((Ns.empty, id), false)
in
let c =
match c with
| Val t -> EVal (cu, ident env0 loc id, t)
| c -> c
in
(env, c)
| EOCaml cu -> (
let s = cu ^ "." ^ U.get_str id in
match (U.get_str id).[0] with
| 'A' .. 'Z' -> (env, EOCaml s)
| _ -> (env, EOCamlComponent s))
| ESchema sch -> (env, find_schema_component sch (ident env0 loc id))
| Type _ -> Cduce_error.(raise_err_loc ~loc Typer_Error "Types don't have components")
| Val _
| EVal _ ->
Cduce_error.(raise_err_loc ~loc Typer_Error "Values don't have components")
| ENamespace _ -> Cduce_error.(raise_err_loc ~loc Typer_Error "Namespaces don't have components")
| EOCamlComponent _ -> Cduce_error.(raise_err_loc ~loc Typer_Error "Caml values don't have components")
| ESchemaComponent _ -> Cduce_error.(raise_err_loc ~loc Typer_Error "Schema components don't have components")
(*
| _ -> error loc "Invalid dot access"
*)
let rec find_global env loc ids =
match ids with
| id :: rest ->
let comp = find_id env env loc true id in
snd (List.fold_left (navig loc env) (env, comp) rest)
| _ -> assert false
let eval_ns env loc = function
| `Uri ns -> ns
| `Path ids -> (
match find_global env loc ids with
| ENamespace ns -> ns
| ESchema sch -> sch.sch_ns
| _ -> Cduce_error.(raise_err_loc ~loc Typer_Error "This path does not refer to a namespace or schema"))
let type_ns env loc p ns =
(* TODO: check that p has no prefix *)
let ns = eval_ns env loc ns in
{
env with
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, pargs) -> (t, pargs)
| ESchemaComponent (t, _) -> (t, []) (*TODO CHECK*)
| _ -> Cduce_error.raise_err_loc ~loc Typer_Error "This path does not refer to a type"
let find_global_schema_component env loc ids =
match find_global env loc ids with
| ESchemaComponent c -> c
| _ -> Cduce_error.(raise_err_loc ~loc Typer_Error "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
| _ -> raise Not_found
let find_value id env =
match Env.find id env.ids with
| Val t
| EVal (_, _, t) ->
t
| _ -> raise Not_found
let do_open env cu =
let env_cu = !from_comp_unit cu in
let ids =
Env.fold
(fun n d ids ->
let d =
match d with
| Val t -> EVal (cu, n, t)
| d -> d
in
Env.add n d ids)
env_cu.ids env.ids
in
{ env with ids; ns = Ns.merge_tables env.ns env_cu.ns }
let type_open env loc ids =
match find_global env loc ids with
| ECDuce cu -> do_open env cu
| _ -> Cduce_error.(raise_err_loc ~loc Typer_Error "This path does not refer to a CDuce unit")
module IType = struct
open Typepat
(* From AST to the intermediate representation *)
(* We need to be careful about the order of type definitions in case
of polymorphic types. Mutually recursive polymorphic types
cannot be recursively called with different parameters within
their recursive groups. We build a graph from the type
definitions and use Tarjan's algorithm to find all strongly
connected components in topological order. Then we translate the
AST into intermediate representation in that order. *)
(* [scc defs] takes a list of definitions and returns [ldefs, map] where
- [ldefs] is a list of list of definitions in topological order. Each
internal list is a group of mutually recursive definitions.
- [map] is mapping from type names to their rank and list of parameters.
*)
let scc defs =
let module Info = struct
type t = {
mutable index : int;
mutable lowlink : int;
mutable is_removed : bool;
def : loc * U.t * U.t list * ppat;
}
let empty =
{
index = -1;
lowlink = -1;
is_removed = false;
def = (noloc, U.empty, [], mknoloc (Internal Types.empty));
}
end in
let open Info in
let index = ref 0
and stack = ref [] in
let res = ref []
and map = Hashtbl.create 17
and rank = ref ~-1 in
let g = Hashtbl.create 17 in
List.iter
(fun ((_, v, _, _) as def) -> Hashtbl.add g v { empty with def })
defs;
let rec strong_connect v vinfo =
vinfo.index <- !index;
vinfo.lowlink <- !index;
incr index;
stack := v :: !stack;
vinfo.is_removed <- false;
let _, _, _, vdef = vinfo.def in
pat_iter
(fun p ->
match p.descr with
| PatVar ([ w ], _) -> (
let winfo =
try Some (Hashtbl.find g w) with
| Not_found -> None
in
match winfo with
| Some winfo ->
if winfo.index == -1 then begin
strong_connect w winfo;
vinfo.lowlink <- min vinfo.lowlink winfo.lowlink
end
else if not winfo.is_removed then
vinfo.lowlink <- min vinfo.lowlink winfo.index
| _ -> ())
| _ -> ())
vdef;
if vinfo.lowlink == vinfo.index then begin
let cc = ref [] in
incr rank;
while
let w = List.hd !stack in
stack := List.tl !stack;
let winfo = Hashtbl.find g w in
let _, _, params, _ = winfo.def in
(*TODO remove U.get_str*)
Hashtbl.add map w
(!rank, List.map (fun v -> (v, Var.mk (U.get_str v))) params);
cc := winfo.def :: !cc;
winfo.is_removed <- true;
not (U.equal w v)
do
()
done;
res := (!cc, Hashtbl.copy map) :: !res;
Hashtbl.clear map
end
in
let () =
List.iter
(fun (_, v, _, _) ->
let vinfo = Hashtbl.find g v in
if vinfo.index == -1 then strong_connect v vinfo)
defs
in
List.rev !res
type penv = {
penv_tenv : t;
penv_derec : (node * U.t list) Env.t;
mutable penv_var : (U.t * Var.t) list;
}
let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty; penv_var = [] }
let all_delayed = ref []
let dummy_params = (-1, [], Hashtbl.create 0)
let current_params = ref dummy_params
let to_register = ref []
let clean_params () =
current_params := dummy_params;
to_register := []
let clean_on_err () =
all_delayed := [];
clean_params ()
let delayed loc =
let s = mk_delayed () in
all_delayed := (loc, s) :: !all_delayed;
s
let check_one_delayed (loc, p) =
if not (check_wf p) then Cduce_error.(raise_err_loc ~loc Typer_Error "Ill-formed recursion")
let check_delayed () =
let l = !all_delayed in
all_delayed := [];
List.iter check_one_delayed l
let rec comp_var_pat vl pl =
match (vl, pl) with
| [], [] -> true
| (v, _) :: vll, { descr = Poly p; _ } :: pll when U.equal v p ->
comp_var_pat vll pll
| _ -> false
let rec untuple p =
match p.descr with
| Prod (p1, p2) -> p1 :: untuple p2
| _ -> [ p ]
let rec tuple = function
| [] -> assert false
| [ p ] -> p
| p1 :: rest -> Cduce_loc.mknoloc (Prod (p1, tuple rest))
let match_type_params l args =
let aux l args =
if List.length l == List.length args then Some args else None
in
match (l, args) with
| [ _ ], _ :: _ :: _ -> aux l [ tuple args ]
| _ :: _ :: _, [ p ] -> aux l (untuple p)
| _ -> aux l args
let invalid_instance_error loc s =
Cduce_error.raise_err_loc ~loc Typer_InvalidRecInst (U.to_string s)
let rec clean_regexp r =
match r with
| Epsilon
| Elem _
| Guard _ ->
r
| Alt (r1, r2) -> Alt (clean_regexp r1, clean_regexp r2)
| Star r -> Star (clean_regexp r)
| WeakStar r -> WeakStar (clean_regexp r)
| SeqCapture (loc, id, r) -> SeqCapture (loc, id, clean_regexp r)
| Seq (r1, r2) -> (
match clean_regexp r1 with
| Seq (e, rr1) -> Seq (e, clean_regexp (Seq (rr1, r2)))
| e -> Seq (e, clean_regexp r2))
let rec derecurs env p =
let err s = Cduce_error.(mk_loc p.loc (Typer_Pattern, s)) in
match p.descr with
| Poly v ->
let vv =
try List.assoc v env.penv_var with
| Not_found ->
let vv = Var.mk (U.get_str v) in
env.penv_var <- (v, vv) :: env.penv_var;
vv
in
mk_type (Types.var vv)
| PatVar ids -> derecurs_var env p.loc ids
| Recurs (p, b) ->
let b = List.map (fun (l, n, p) -> (l, n, [], p)) b in
derecurs (fst (derecurs_def env b)) p
| Internal t -> mk_type t
| NsT ns ->
mk_type
(Types.atom (AtomSet.any_in_ns (parse_ns env.penv_tenv p.loc ns)))
| Or (p1, p2) -> mk_or ~err (derecurs env p1) (derecurs env p2)
| And (p1, p2) -> mk_and ~err (derecurs env p1) (derecurs env p2)
| Diff (p1, p2) -> mk_diff ~err (derecurs env p1) (derecurs env p2)
| Prod (p1, p2) -> mk_prod (derecurs env p1) (derecurs env p2)
| XmlT (p1, p2) -> mk_xml (derecurs env p1) (derecurs env p2)
| Arrow (p1, p2) -> mk_arrow (derecurs env p1) (derecurs env p2)
| Optional p -> mk_optional ~err (derecurs env p)
| Record (o, r) ->
let aux = function
| p, Some e -> (derecurs env p, Some (derecurs env e))
| p, None -> (derecurs env p, None)
in
mk_record ~err o (parse_record env.penv_tenv p.loc aux r)
| Constant (x, c) ->
mk_constant (ident env.penv_tenv p.loc x) (const env.penv_tenv p.loc c)
| Cst c -> mk_type (Types.constant (const env.penv_tenv p.loc c))
| Regexp r -> rexp (derecurs_regexp env (clean_regexp r))
| Concat (p1, p2) -> mk_concat ~err (derecurs env p1) (derecurs env p2)
| Merge (p1, p2) -> mk_merge ~err (derecurs env p1) (derecurs env p2)
and derecurs_regexp env = function
| Epsilon -> mk_epsilon
| Elem p -> mk_elem (derecurs env p)
| Guard p -> mk_guard (derecurs env p)
| Seq
( (Elem { descr = PatVar ((id :: rest as ids), []); loc } as p1),
((Elem _ | Seq (Elem _, _)) as p2) ) ->
let arg, make =
match p2 with
| Elem arg -> (arg, fun x -> x)
| Seq (Elem arg, pp2) ->
(arg, fun x -> mk_seq x (derecurs_regexp env pp2))
| _ -> assert false
in
let v = ident env.penv_tenv loc id in
let patch_arg =
try
try snd (Env.find v env.penv_derec) != [] with
| Not_found ->
let _, pargs =
if rest == [] then find_local_type env.penv_tenv loc v
else find_global_type env.penv_tenv loc ids
in
pargs != []
with
| Not_found -> false
in
if patch_arg then
make (mk_elem (derecurs env { descr = PatVar (ids, [ arg ]); loc }))
else mk_seq (derecurs_regexp env p1) (derecurs_regexp env p2)
| Seq (p1, p2) -> mk_seq (derecurs_regexp env p1) (derecurs_regexp env p2)
| Alt (p1, p2) -> mk_alt (derecurs_regexp env p1) (derecurs_regexp env p2)
| Star p -> mk_star (derecurs_regexp env p)
| WeakStar p -> mk_weakstar (derecurs_regexp env p)
| SeqCapture (loc, x, p) ->
mk_seqcapt (ident env.penv_tenv loc x) (derecurs_regexp env p)
and derecurs_var env loc ids =
match ids with
| (id :: rest as ids), args -> (
let cidx, cparams, cmap = !current_params in
let v = ident env.penv_tenv loc id in
try
let node, _ = Env.find v env.penv_derec in
if args == [] || comp_var_pat cparams args then node
else invalid_instance_error loc id
with
| Not_found -> (
try
let (cu, name), (t, pargs), tidx =
if rest == [] then
( ("", v),
find_local_type env.penv_tenv loc v,
try fst (Hashtbl.find cmap id) with
| Not_found -> ~-1 )
else
let t, pargs = find_global_type env.penv_tenv loc ids in
match find_id env.penv_tenv env.penv_tenv loc true id with
| ECDuce _
| EOCaml _ ->
( ( U.get_str id,
ident env.penv_tenv loc
(U.mk @@ String.concat "."
@@ List.map U.get_str rest) ),
(t, pargs),
~-1 )
| _ -> assert false
in
if cidx >= 0 && tidx == cidx && not (comp_var_pat cparams args)
then invalid_instance_error loc id;
let _err s = Error s in
let l =
match match_type_params pargs args with
| Some args ->
List.map2 (fun v p -> (v, typ (derecurs env p))) pargs args
| None ->
Cduce_error.raise_err_loc
~loc Typer_InvalidInstArity
(U.to_string id, List.length pargs, List.length args)
in
let sub = Types.Subst.from_list l in
let ti = mk_type (Types.Subst.apply_full sub t) in
to_register := (cu, name, List.map snd l, ti, loc) :: !to_register;
ti
with
| Not_found ->
assert (rest == []);
if args != [] then
Cduce_error.raise_err_loc ~loc Typer_UnboundId (v, true)
else mk_capture v))
| _ -> assert false
and derecurs_def env b =
let seen = ref IdMap.empty in
let b =
List.map
(fun (loc, v, args, p) ->
let v = ident env.penv_tenv loc v in
try
let old_loc = IdMap.assoc v !seen in
Cduce_error.raise_err_loc ~loc Typer_MultipleTypeDef (v, old_loc)
with Not_found ->
seen := IdMap.add v loc !seen ;
(v, loc, args, p, delayed loc))
b
in
let env =
List.fold_left
(fun env (v, _, a, p, s) ->
{
env with
penv_derec = Env.add v (s, a) env.penv_derec;
penv_var =
List.fold_left
(fun acc v -> (v, Var.mk (U.get_str v)) :: acc)
env.penv_var a;
})
env b
in
List.iter
(fun (v, _, a, p, s) ->
(* Copy. The unknown polymorphic variables that are not already in
penv_var are introduced for the scope of the current type and
discarded afterwards.
*)
let env = { env with penv_var = env.penv_var } in
link s (derecurs env p))
b;
(env, b)
let derec penv p =
let d = derecurs penv p in
elim_concats ();
check_delayed ();
internalize d;
d
(* API *)
let check_no_fv loc n =
match peek_fv n with
| None -> ()
| Some x ->
Cduce_error.raise_err_loc ~loc Typer_CaptureNotAllowed x
let type_defs env b =
let penv, b = derecurs_def (penv env) b in
elim_concats ();
check_delayed ();
let aux loc d =
internalize d;
check_no_fv loc d;
try typ d with
| Cduce_error.Error ((Located loc' | PreciselyLocated (loc', _)) , (Typer_Pattern, s)) ->
Cduce_error.raise_err_loc ~loc:loc' Typer_Error s
| Cduce_error.Error (Unlocated, (Typer_Pattern, s)) -> Cduce_error.raise_err_loc ~loc Generic s
in
let b =
List.map
(fun (v, loc, args, _, d) ->
let t_rhs = aux loc d in
if loc <> noloc && Types.is_empty t_rhs then
Cduce_error.(warning ~loc
("This definition yields an empty type for " ^ Ident.to_string v) ());
let vars_rhs = Types.Subst.vars t_rhs in
let vars_lhs = Var.Set.from_list (List.map snd penv.penv_var) in
let undecl = Var.Set.diff vars_rhs vars_lhs in
if not (Var.Set.is_empty undecl) then
Cduce_error.raise_err_loc ~loc
Typer_UnboundTypeVariable (v, Var.Set.choose undecl);
(* recreate the mapping in the correct order *)
let vars_args = List.map (fun v -> List.assoc v penv.penv_var) args in
let final_vars =
(* create a sequence 'a -> 'a_0 for all variables *)
List.map (fun v -> (v, Var.(mk (name v)))) vars_args
in
let subst =
Types.Subst.from_list
(List.map (fun (v, vv) -> (v, Types.var vv)) final_vars)
in
let t_rhs = Types.Subst.apply_full subst t_rhs in
(v, t_rhs, List.map snd final_vars))
(List.rev b)
in
List.iter
(fun (v, t, al) ->
let params = List.map Types.var al in
Types.Print.register_global "" v ~params t)
b;
let env = enter_types b env in
List.iter
(fun (cu, name, params, ti, loc) ->
let tti = aux loc ti in
Types.Print.register_global cu name ~params tti)
!to_register;
env
let equal_params l1 l2 =
try List.for_all2 U.equal l1 l2 with
| _ -> false
let check_params l =
match l with
| [] -> assert false
| [ (_, u, _, _) ] -> u
| (loc1, u, p, _) :: r -> (
try
let loc2, v, _, _ =
List.find (fun (_, _, q, _) -> not (equal_params p q)) r
in
let loc = merge_loc loc1 loc2 in
Cduce_error.raise_err_loc ~loc
Typer_Error (Printf.sprintf (* TODO create an error *)
"mutually recursive types %s and %s have different arities"
(U.to_string u) (U.to_string v))
with
| Not_found -> u)
let type_defs env b =
try
let b = scc b in
let r =
List.fold_left
(fun env (b, map) ->
let u = check_params b in
let idx, params = Hashtbl.find map u in
current_params := (idx, params, map);
type_defs env b)
env b
in
clean_params ();
r
with
| exn ->
clean_on_err ();
raise exn
let typ vars env t =
let aux loc d =
internalize d;
check_no_fv loc d;
try typ_node d with
| Cduce_error.Error (_, (Typer_Pattern, s)) -> Cduce_error.raise_err_loc ~loc Typer_Error s
in
try
let penv = { (penv env) with penv_var = vars } in
let d = derec penv t in
let res = aux t.loc d in
List.iter
(fun (cu, name, params, ti, loc) ->
let tti = aux loc ti in
Types.Print.register_global cu name ~params (Types.descr tti))
!to_register;
clean_params ();
res
with
| exn ->
clean_on_err ();
raise exn
let pat env t =
try
let d = derec (penv env) t in
try pat_node d with
| Cduce_error.Error (_, (Typer_Pattern, s)) ->
Cduce_error.raise_err_loc ~loc:t.loc Typer_Error s
with
| exn ->
clean_on_err ();
raise exn
end
let typ = IType.typ []
let var_typ = IType.typ
let pat = IType.pat
let type_defs = IType.type_defs
let dump_types ppf env =
Env.iter
(fun v -> function
| Type _ -> Format.fprintf ppf " %a" Ident.print v
| _ -> ())
env.ids
let dump_ns ppf env = Ns.dump_table ppf env.ns
(* II. Build skeleton *)
type type_fun = Cduce_loc.loc -> Types.t -> bool -> Types.t
module Fv = IdSet
type branch = Branch of Typed.branch * branch list
let cur_branch : branch list ref = ref []
let exp' loc e =
{ Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e }
let exp loc fv e = (fv, exp' loc e)
let exp_nil = exp' noloc (Typed.Cst Types.Sequence.nil_cst)
let pat_true =
let n = Patterns.make Fv.empty in
Patterns.define n (Patterns.constr Builtin_defs.true_type);
n
let pat_false =
let n = Patterns.make Fv.empty in
Patterns.define n (Patterns.constr Builtin_defs.false_type);
n
let ops = Hashtbl.create 13
let register_op op arity f = Hashtbl.add ops op (arity, f)
let typ_op op = snd (Hashtbl.find ops op)
let fun_name env a =
match a.fun_name with
| None -> None
| Some (loc, s) -> Some (ident env loc s)
let is_op env s =
if Env.mem s env.ids then None
else
let ns, s = s in
if Ns.Uri.equal ns Ns.empty then
let s = U.get_str s in
try
let o = Hashtbl.find ops s in
Some (s, fst o)
with
| Not_found -> None
else None
module USet = Set.Make (U)
let collect_vars acc p =
let vset = ref acc in
pat_iter
(function
| { descr = Poly v; _ } -> vset := USet.add v !vset
| _ -> ())
p;
!vset
let rec get_dot_for_annot loc expr =
match expr with
| Dot _ -> expr
| LocatedExpr (_, e) -> get_dot_for_annot loc e
| e -> Cduce_error.raise_err_loc ~loc Typer_Error "Only OCaml external can have type arguments"
let rec expr env loc = function
| LocatedExpr (loc, e) -> expr env loc e
| Forget (e, t) ->
let fv, e = expr env loc e
and t = typ env t in
exp loc fv (Typed.Forget (e, t))
| Check (e, t) ->
let fv, e = expr env loc e
and t = typ env t in
exp loc fv (Typed.Check (ref Types.empty, e, t))
| Var s -> var env loc s
| Apply (e1, e2) -> (
let fv1, e1 = expr env loc e1
and fv2, e2 = expr env loc e2 in
let fv = Fv.cup fv1 fv2 in
match e1.Typed.exp_descr with
| Typed.Op (op, arity, args) when arity > 0 ->
exp loc fv (Typed.Op (op, arity - 1, args @ [ e2 ]))
| _ -> exp loc fv (Typed.Apply (e1, e2)))
| Abstraction a -> abstraction env loc a
| (Integer _ | Char _ | Atom _ | Const _) as c ->
exp loc Fv.empty (Typed.Cst (const env loc c))
| Abstract v -> exp loc Fv.empty (Typed.Abstract v)
| Pair (e1, e2) ->
let fv1, e1 = expr env loc e1
and fv2, e2 = expr env loc e2 in
exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1, e2))
| Xml (e1, e2) ->
let fv1, e1 = expr env loc e1
and fv2, e2 = expr env loc e2 in
let n = if env.keep_ns then Some env.ns else None in
exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1, e2, n))
| Dot _ as e -> dot loc env e []
| TyArgs (e, args) ->
(*let e = get_dot_for_annot loc e in*)
dot loc env e args
| RemoveField (e, l) ->
let fv, e = expr env loc e in
exp loc fv (Typed.RemoveField (e, parse_label env loc l))
| RecordLitt r ->
let fv = ref Fv.empty in
let r =
parse_record env loc
(fun e ->
let fv2, e = expr env loc e in
fv := Fv.cup !fv fv2;
e)
r
in
exp loc !fv (Typed.RecordLitt r)
| String (i, j, s, e) ->
let fv, e = expr env loc e in
exp loc fv (Typed.String (i, j, s, e))
| Match (e, b) ->
let fv1, e = expr env loc e
and fv2, b = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
| Map (e, b) ->
let fv1, e = expr env loc e
and fv2, b = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
| Transform (e, b) ->
let fv1, e = expr env loc e
and fv2, b = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
| Xtrans (e, b) ->
let fv1, e = expr env loc e
and fv2, b = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
| Validate (e, ids) ->
let fv, e = expr env loc e in
let t, v = find_global_schema_component env loc ids in
exp loc fv (Typed.Validate (e, t, v))
| SelectFW (e, from, where) -> select_from_where env loc e from where
| Try (e, b) ->
let fv1, e = expr env loc e
and fv2, b = branches env b in
exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
| NamespaceIn (pr, ns, e) ->
let env = type_ns env loc pr ns in
expr env loc e
| KeepNsIn (k, e) -> expr (type_keep_ns env k) loc e
| Ref (e, t) ->
let fv, e = expr env loc e
and t = var_typ env.poly_vars env t in
exp loc fv (Typed.Ref (e, t))
and if_then_else loc cond yes no =
let b =
{
Typed.br_typ = Types.empty;
Typed.br_branches =
[
{
Typed.br_loc = yes.Typed.exp_loc;
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = Fv.empty;
Typed.br_pat = pat_true;
Typed.br_body = yes;
};
{
Typed.br_loc = no.Typed.exp_loc;
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = Fv.empty;
Typed.br_pat = pat_false;
Typed.br_body = no;
};
];
Typed.br_accept = Builtin_defs.bool;
}
in
exp' loc (Typed.Match (cond, b))
and dot loc env0 e args =
let dot_access loc (fv, e) l =
exp loc fv (Typed.Dot (e, parse_label env0 loc l))
in
let no_args () =
if args <> [] then Cduce_error.raise_err_loc ~loc Typer_Error "Only OCaml externals can have type arguments"
in
let rec aux loc = function
| LocatedExpr (loc, e) -> aux loc e
| Dot (e, id) -> (
match aux loc e with
| `Val e -> `Val (dot_access loc e id)
| `Comp c -> `Comp (navig loc env0 c id))
| Var id -> (
match find_id_comp env0 env0 loc id with
| Val _ -> `Val (var env0 loc id)
| c -> `Comp (env0, c))
| e -> `Val (expr env0 loc e)
in
match aux loc e with
| `Val e ->
no_args ();
e
| `Comp (_, EVal (cu, id, t)) ->
no_args ();
exp loc Fv.empty (Typed.ExtVar (cu, id, t))
| `Comp (_, EOCamlComponent s) -> extern loc env0 s args
| _ -> Cduce_error.raise_err_loc ~loc Typer_Error "This dot notation does not refer to a value"
and extern loc env s args =
let args = List.map (typ env) args in
try
let i, t =
let i, t = Externals.resolve s args in
if !has_static_external s then
(`Builtin (s,i), t)
else
(`Ext i, t)
in
exp loc Fv.empty (Typed.External (t, i))
with
| Cduce_error.Error (Unlocated, (err, arg)) -> Cduce_error.raise_err_loc ~loc err arg
| Cduce_error.Error (Located loc, (err, arg)) -> Cduce_error.raise_err_loc ~loc err arg
| Cduce_error.Error (PreciselyLocated (loc, _), (err, arg)) -> Cduce_error.raise_err_loc ~loc err arg
| exn -> Cduce_error.raise_err_loc ~loc Other_Exn exn
and var env loc s =
let id = ident env loc s in
match is_op env id with
| Some (s, arity) ->
let e =
match s with
| "print_xml"
| "print_xml_utf8" ->
Typed.NsTable (env.ns, Typed.Op (s, arity, []))
| "load_xml" when env.keep_ns -> Typed.Op ("!load_xml", arity, [])
| _ -> Typed.Op (s, arity, [])
in
exp loc Fv.empty e
| None -> (
try
match Env.find id env.ids with
| Val _ -> exp loc (Fv.singleton id) (Typed.Var id)
| EVal (cu, id, t) -> exp loc Fv.empty (Typed.ExtVar (cu, id, t))
| _ -> Cduce_error.raise_err_loc ~loc Typer_Error "This identifier does not refer to a value"
with
| Not_found -> Cduce_error.raise_err_loc ~loc Typer_UnboundId (id, false))
and abstraction env loc a =
(* When entering a function (fun 'a 'b ... .('a -> 'b -> … ))
for each variable 'x from the interface
- if 'x is in env.poly_vars, it is bound higher in the AST, we need
to keep the associated unique variable
- if 'x is not in env.poly_vars or 'x is in a.fun_poly, a fresh
name must be generated and kept for subsequent use of the variable.
*)
let vset =
(* collect all type variables from the interface*)
List.fold_left
(fun acc (t1, t2) -> collect_vars (collect_vars acc t1) t2)
USet.empty a.fun_iface
in
let vset =
(* remove variables that are in scope *)
List.fold_left (fun acc (v, _) -> USet.remove v acc) vset env.poly_vars
in
let vset = List.fold_left (fun acc v -> USet.add v acc) vset a.fun_poly in
(* add those that are explicitely polymorphic. *)
let all_vars =
USet.fold (fun v acc -> (v, Var.mk (U.get_str v)) :: acc) vset env.poly_vars
in
let iface =
List.map
(fun (t1, t2) -> (var_typ all_vars env t1, var_typ all_vars env t2))
a.fun_iface
in
let env = { env with poly_vars = all_vars } in
let t =
List.fold_left
(fun accu (t1, t2) -> Types.cap accu (Types.arrow t1 t2))
Types.any iface
in
let iface =
List.map (fun (t1, t2) -> (Types.descr t1, Types.descr t2)) iface
in
let fun_name = fun_name env a in
let env' =
match fun_name with
| None -> env
| Some f -> enter_values_dummy [ f ] env
in
let fv0, body = branches env' a.fun_body in
let fv =
match fun_name with
| None -> fv0
| Some f -> Fv.remove f fv0
in
let e =
Typed.Abstraction
{
Typed.fun_name;
Typed.fun_iface = iface;
Typed.fun_body = body;
Typed.fun_typ = t;
Typed.fun_fv = fv;
Typed.fun_is_poly = not (Var.Set.is_empty (Types.Subst.vars t));
}
in
exp loc fv e
and branches env b =
let fv = ref Fv.empty in
let accept = ref Types.empty in
let branch (p, e) =
let cur_br = !cur_branch in
cur_branch := [];
let ploc = p.loc in
let p = pat env p in
let fvp = Patterns.fv p in
let fv2, e = expr (enter_values_dummy (fvp :> Id.t list) env) noloc e in
let br_loc = merge_loc ploc e.Typed.exp_loc in
(match Fv.pick (Fv.diff fvp fv2) with
| None -> ()
| Some x ->
let x = Ident.to_string x in
warning br_loc
("The capture variable " ^ x
^ " is declared in the pattern but not used in the body of this \
branch. It might be a misspelled or undeclared type or name (if it \
isn't, use _ instead)."));
let fv2 = Fv.diff fv2 fvp in
fv := Fv.cup !fv fv2;
accept := Types.cup !accept (Types.descr (Patterns.accept p));
let ghost = br_loc == noloc in
let br =
{
Typed.br_loc;
Typed.br_used = ghost;
Typed.br_ghost = ghost;
Typed.br_vars_empty = fvp;
Typed.br_pat = p;
Typed.br_body = e;
}
in
cur_branch := Branch (br, !cur_branch) :: cur_br;
br
in
let b = List.map branch b in
( !fv,
{
Typed.br_typ = Types.empty;
Typed.br_branches = b;
Typed.br_accept = !accept;
} )
and select_from_where env loc e from where =
let env = ref env in
let all_fv = ref Fv.empty in
let bound_fv = ref Fv.empty in
let clause (p, e) =
let ploc = p.loc in
let p = pat !env p in
let fvp = Patterns.fv p in
let fv2, e = expr !env noloc e in
env := enter_values_dummy (fvp :> Id.t list) !env;
all_fv := Fv.cup (Fv.diff fv2 !bound_fv) !all_fv;
bound_fv := Fv.cup fvp !bound_fv;
(ploc, p, fvp, e)
in
let from = List.map clause from in
let where = List.map (expr !env noloc) where in
let put_cond rest (fv, cond) =
all_fv := Fv.cup (Fv.diff fv !bound_fv) !all_fv;
if_then_else loc cond rest exp_nil
in
let aux (ploc, p, fvp, e) (where, rest) =
(* Put here the conditions that depends on variables in fvp *)
let above, here = List.partition (fun (v, _) -> Fv.disjoint v fvp) where in
(* if cond then ... else [] *)
let rest = List.fold_left put_cond rest here in
(* transform e with p -> ... *)
let br =
{
Typed.br_loc = ploc;
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = fvp;
Typed.br_pat = p;
Typed.br_body = rest;
}
in
cur_branch := [ Branch (br, !cur_branch) ];
let b =
{
Typed.br_typ = Types.empty;
Typed.br_branches = [ br ];
Typed.br_accept = Types.descr (Patterns.accept p);
}
in
let br_loc = merge_loc ploc e.Typed.exp_loc in
(above, exp' br_loc (Typed.Transform (e, b)))
in
let cur_br = !cur_branch in
cur_branch := [];
let fv, e = expr !env noloc (Pair (e, cst_nil)) in
cur_branch := !cur_branch @ cur_br;
let where, rest = List.fold_right aux from (where, e) in
(* The remaining conditions are constant. Gives a warning for that. *)
(match where with
| (_, e) :: _ ->
warning e.Typed.exp_loc
"This 'where' condition does not depend on any captured variable"
| _ -> ());
let rest = List.fold_left put_cond rest where in
(Fv.cup !all_fv (Fv.diff fv !bound_fv), rest)
let expr env e = snd (expr env noloc e)
let let_decl env p e =
{ Typed.let_pat = pat env p; Typed.let_body = expr env e }
(* Hide global "typing/parsing" environment *)
(* III. Type-checks *)
open Typed
let any_node = Types.(cons any)
let localize loc f x =
try f x with
| Cduce_error.Error (_, (Typer_Error, msg)) -> Cduce_error.raise_err_loc ~loc Typer_Error msg
| Cduce_error.Error (_,(Typer_Constraint, arg)) -> Cduce_error.raise_err_loc ~loc Typer_Constraint arg
let raise_constraint_exn ?loc ?precise t s =
let open Cduce_error in
let r (type a) (e : a error_t) (a : a) =
match loc, precise with
None, _ -> raise_err e a
| Some loc, Some precise -> raise_err_precise ~loc precise e a
| Some loc, None -> raise_err_loc ~loc e a
in
if
Var.Set.is_empty (Types.Subst.vars t)
&& Var.Set.is_empty (Types.Subst.vars s)
then r Typer_Constraint (t, s)
else r Typer_ShouldHave2 (t, "but its inferred type is:", s)
let require loc t s =
if not (Types.subtype t s) then raise_constraint_exn ~loc t s
let verify loc t s =
require loc t s;
t
let verify_noloc t s =
if not (Types.subtype t s) then raise_constraint_exn t s;
t
let check_str loc ofs t s =
if not (Types.subtype t s) then raise_constraint_exn ~loc ~precise:(`Char ofs) t s;
t
let should_have loc constr s = Cduce_error.raise_err_loc ~loc Typer_ShouldHave (constr, s)
let should_have_str loc ofs constr s =
Cduce_error.raise_err_precise ~loc (`Char ofs) Typer_ShouldHave (constr, s)
let flatten arg loc constr precise =
let open Types in
let constr' =
Sequence.star (Sequence.approx (Types.cap Sequence.any constr))
in
let sconstr' = Sequence.star constr' in
let exact = Types.subtype constr' constr in
if exact then
let t = arg loc sconstr' precise in
if precise then Sequence.flatten t else constr
else
let t = arg loc sconstr' true in
verify loc (Sequence.flatten t) constr
let pat_any () =
let n = Patterns.make IdSet.empty in
Patterns.define n (Patterns.constr Types.any);
n
let pat_var id =
let s = IdSet.singleton id in
let n = Patterns.make s in
Patterns.define n (Patterns.capture id);
n
let pat_node d fv =
let n = Patterns.make fv in
Patterns.define n d;
n
let pat_pair kind e1 e2 fv =
pat_node
((match kind with
| `Normal -> Patterns.times
| `Xml -> Patterns.xml)
e1 e2)
fv
let pat_cap p1 p2 =
let fv1 = Patterns.fv p1 in
let fv2 = Patterns.fv p2 in
pat_node Patterns.(cap (descr p1) (descr p2)) (IdSet.cup fv1 fv2)
let rec pat_of_expr fv te =
match te.exp_descr with
| Var s when not (IdSet.mem fv s) -> pat_var s
| Pair (e1, e2)
| Xml (e1, e2, _) ->
let kind =
match te.exp_descr with
| Pair _ -> `Normal
| _ -> `Xml
in
let p1 = pat_of_expr fv e1
and p2 = pat_of_expr fv e2 in
let fv1 = Patterns.fv p1 in
let fv2 = Patterns.fv p2 in
pat_pair kind p1 p2 (IdSet.cup fv1 fv2)
| RecordLitt lmap ->
List.fold_left
(fun acc (lab, tel) ->
let pel = pat_of_expr fv tel in
let prec = pat_node (Patterns.record lab pel) (Patterns.fv pel) in
pat_cap prec acc)
(pat_any ()) (LabelMap.get lmap)
| _ -> pat_any ()
let refine_pat p1 op2 =
match op2 with
| None -> p1
| Some te ->
let fv = Patterns.fv p1 in
let p2 = pat_of_expr fv te in
pat_cap p1 p2
let rec type_check env e constr precise =
let d = type_check' e.exp_loc env e.exp_descr constr precise in
let d = if precise then d else constr in
e.exp_typ <- Types.cup e.exp_typ d;
d
and type_check' loc env e constr precise =
match e with
| Forget (e, t) ->
let t = Types.descr t in
ignore (type_check env e t false);
verify loc t constr
| Check (t0, e, t) ->
if Var.Set.is_empty Types.(Subst.vars (descr t)) then (
let te = type_check env e Types.any true in
t0 := Types.cup !t0 te;
verify loc (Types.cap te (Types.descr t)) constr)
else
Cduce_error.raise_err_loc
~loc Typer_Error "Polymorphic type variables cannot occur in dynamic type-checks"
| Abstraction a ->
let t =
if Types.subtype a.fun_typ constr then a.fun_typ
else
let name =
match a.fun_name with
| Some s -> "abstraction " ^ Ident.to_string s
| None -> "the abstraction"
in
should_have loc constr
(Format.asprintf
"but the interface (%a) of %s is not compatible with type\n\
\ (%a)" Types.Print.print a.fun_typ name
Types.Print.print constr)
in
let env =
{
env with
mono_vars = Var.Set.cup env.mono_vars (Types.Subst.vars a.fun_typ);
}
in
let env =
match a.fun_name with
| None -> env
| Some f -> enter_value f a.fun_typ env
in
List.iter
(fun (t1, t2) ->
let acc = a.fun_body.br_accept in
if not (Types.subtype t1 acc) then
Cduce_error.(raise_err_loc ~loc Typer_NonExhaustive (Types.diff t1 acc));
ignore (type_check_branches loc env t1 a.fun_body t2 false))
a.fun_iface;
t
| Match (e, b) ->
let t = type_check env e b.br_accept true in
type_check_branches loc env t b constr precise
| Try (e, b) ->
let te = type_check env e constr precise in
let tb = type_check_branches loc env Types.any b constr precise in
Types.cup te tb
| Pair (e1, e2) -> type_check_pair loc env e1 e2 constr precise
| Xml (e1, e2, _) -> type_check_pair ~kind:`XML loc env e1 e2 constr precise
| RecordLitt r -> type_record loc env r constr precise
| Map (e, b) -> type_map loc env false e b constr precise
| Transform (e, b) ->
localize loc (flatten (fun l -> type_map loc env true e b) loc constr) precise
| Apply (e1, e2) ->
let t1 = type_check env e1 Types.Function.any true in
let t1arrow = Types.Arrow.get t1 in
let dom = Types.Arrow.domain t1arrow in
let t2 = type_check env e2 Types.any true in
let res =
if
Var.Set.is_empty (Types.Subst.vars t1)
&& Var.Set.is_empty (Types.Subst.vars t2)
then
(* TODO don't retype e2 *)
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1arrow t2
else
match Types.Tallying.apply_raw env.mono_vars t1 t2 with
| None -> raise_constraint_exn ~loc t2 dom
| Some (subst, tx, ty, res) ->
List.iter
(fun s ->
Var.Map.iteri
(fun wv t ->
match Var.kind wv with
| `generated
| `user ->
()
| `weak ->
let tt = Types.Subst.clean_type env.mono_vars t in
env.weak_vars <-
Var.Map.update
(fun prev next ->
match (prev, next) with
| None, Some t -> next
| Some tp, Some tn when Types.equiv tp tn -> next
| Some tp, Some tn ->
Cduce_error.(raise_err_loc ~loc
Typer_Error (Format.asprintf
"the weak polymorphic variable %a is \
instantiated several times in the \
same expression."
Var.print wv))
| _ -> assert false)
wv (Some tt) env.weak_vars)
s)
subst;
res
(*
if Types.Arrow.need_arg t1 then
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1 t2
else (
ignore (type_check env e2 dom false);
Types.Arrow.apply_noarg t1) *)
in
verify loc res constr
| Var s -> verify loc (find_value s env) constr
| ExtVar (cu, s, t) -> verify loc t constr
| Cst c -> verify loc (Types.constant c) constr
| Abstract (t, _) -> verify loc Types.(abstract (AbstractSet.atom t)) constr
| String (i, j, s, e) -> type_check_string loc env 0 s i j e constr precise
| Dot (e, l) -> (
let expect_rec = Types.record l (Types.cons constr) in
let expect_elt =
Types.xml any_node
(Types.cons (Types.times (Types.cons expect_rec) any_node))
in
let t = type_check env e (Types.cup expect_rec expect_elt) precise in
let t_elt =
let t = Types.Product.pi2 (Types.Product.get ~kind:`XML t) in
let t = Types.Product.pi1 (Types.Product.get t) in
t
in
if not precise then constr
else
try Types.Record.project (Types.cup t t_elt) l with
| Not_found -> assert false)
| RemoveField (e, l) ->
let t = type_check env e Types.Rec.any true in
let t = Types.Record.remove_field t l in
verify loc t constr
| Xtrans (e, b) ->
let t = type_check env e Types.Sequence.any true in
let t =
try
Types.Sequence.map_tree constr
(fun cstr t ->
let resid = Types.diff t b.br_accept in
let res = type_check_branches loc env t b cstr true in
(res, resid))
t
with
| Types.Sequence.Error _ as exn -> (
let rec find_loc = function
| Cduce_error.Error (PreciselyLocated (loc, precise), _) -> ((loc, precise), exn)
| Types.Sequence.(Error (Types.Sequence.UnderTag (t, exn))) ->
let l, exn = find_loc exn in
(l, Types.Sequence.Error (Types.Sequence.UnderTag (t, exn)))
| exn -> raise Not_found
in
try
let (loc, precise), exn = find_loc exn in
Cduce_error.raise_err_precise ~loc precise Other_Exn exn
with
| Not_found -> Cduce_error.raise_err_loc ~loc Other_Exn exn)
in
verify loc t constr
| Validate (e, t, _) ->
ignore (type_check env e Types.any false);
verify loc t constr
| Ref (e, t) ->
ignore (type_check env e (Types.descr t) false);
verify loc (Builtin_defs.ref_type t) constr
| External (t, _) -> verify loc t constr
| Op (op, _, args) ->
let args : type_fun list = List.map (fun e (_:Cduce_loc.loc) -> type_check env e ) args in
let t = localize loc (typ_op op args loc constr) precise in
verify loc t constr
| NsTable (ns, e) -> type_check' loc env e constr precise
and type_check_pair ?(kind = `Normal) loc env e1 e2 constr precise =
let rects = Types.Product.normal ~kind constr in
(if Types.Product.is_empty rects then
match kind with
| `Normal -> should_have loc constr "but it is a pair"
| `XML -> should_have loc constr "but it is an XML element");
let need_s = Types.Product.need_second rects in
let t1 = type_check env e1 (Types.Product.pi1 rects) (precise || need_s) in
let c2 = Types.Product.constraint_on_2 rects t1 in
if Types.is_empty c2 then
Cduce_error.raise_err_loc ~loc
Typer_ShouldHave2 (constr, "but the first component has type:", t1);
let t2 = type_check env e2 c2 precise in
if precise then
match kind with
| `Normal -> Types.times (Types.cons t1) (Types.cons t2)
| `XML -> Types.xml (Types.cons t1) (Types.cons t2)
else constr
and type_check_string loc env ofs s i j e constr precise =
if U.equal_index i j then type_check env e constr precise
else
let rects = Types.Product.normal constr in
if Types.Product.is_empty rects then
should_have_str loc ofs constr "but it is a string"
else
let ch, i' = U.next s i in
let ch = CharSet.V.mk_int ch in
let tch = Types.constant (Types.Char ch) in
let t1 = check_str loc ofs tch (Types.Product.pi1 rects) in
let c2 = Types.Product.constraint_on_2 rects t1 in
let t2 = type_check_string loc env (ofs + 1) s i' j e c2 precise in
if precise then Types.times (Types.cons t1) (Types.cons t2) else constr
and type_record loc env r constr precise =
if not (Types.Record.has_record constr) then
should_have loc constr "but it is a record";
let rconstr, res =
List.fold_left
(fun (rconstr, res) (l, e) ->
let r = Types.Record.focus rconstr l in
let pi = Types.Record.get_this r in
(if Types.is_empty pi then
let l = Label.string_of_attr l in
should_have loc constr
(Printf.sprintf "Field %s is not allowed here." l));
let t = type_check env e pi (precise || Types.Record.need_others r) in
let rconstr = Types.Record.constraint_on_others r t in
(if Types.is_empty rconstr then
let l = Label.string_of_attr l in
should_have loc constr
(Printf.sprintf "Type of field %s is not precise enough." l));
let res = if precise then LabelMap.add l (Types.cons t) res else res in
(rconstr, res))
(constr, LabelMap.empty) (LabelMap.get r)
in
if not (Types.Record.has_empty_record rconstr) then
should_have loc constr "More fields should be present";
if precise then Types.record_fields (false, res) else constr
and type_check_branches ?expr loc env targ brs constr precise =
if Types.is_empty targ then Types.empty
else (
brs.br_typ <- Types.cup brs.br_typ targ;
branches_aux expr loc env targ
(if precise then Types.empty else constr)
constr precise brs.br_branches)
and branches_aux expr loc env targ tres constr precise = function
| [] -> tres
| b :: rem ->
let p = refine_pat b.br_pat expr in
let acc = Types.descr (Patterns.accept p) in
let targ' = Types.cap targ acc in
if Types.is_empty targ' then
branches_aux expr loc env targ tres constr precise rem
else (
b.br_used <- true;
let res = Patterns.filter targ' p in
let res = IdMap.map Types.descr res in
b.br_vars_empty <-
IdMap.domain
(IdMap.filter
(fun x t -> Types.(subtype t Sequence.nil_type))
(IdMap.restrict res b.br_vars_empty));
let env' = enter_values (IdMap.get res) env in
let t = type_check env' b.br_body constr precise in
let tres = if precise then Types.cup t tres else tres in
let targ'' = Types.diff targ acc in
if Types.non_empty targ'' then
branches_aux expr loc env targ'' tres constr precise rem
else tres)
and type_map loc env def e b constr precise =
let open Types in
let acc = if def then Sequence.any else Sequence.star b.br_accept in
let t = type_check env e acc true in
let constr' = Sequence.approx (Types.cap Sequence.any constr) in
let exact = Types.subtype (Sequence.star constr') constr in
(* Note:
- could be more precise by integrating the decomposition
of constr inside Sequence.map.
*)
let res =
Sequence.map
(fun t ->
let res =
type_check_branches loc env t b constr' (precise || not exact)
in
if def && not (Types.subtype t b.br_accept) then (
require loc Sequence.nil_type constr';
Types.cup res Sequence.nil_type)
else res)
t
in
if exact then res else verify loc res constr
and type_let_decl env l =
let acc = Types.descr (Patterns.accept l.let_pat) in
let t = type_check env l.let_body acc true in
let res = Patterns.filter t l.let_pat in
IdMap.mapi_to_list (fun x t -> (x, Types.descr t)) res
and type_rec_funs env l =
let typs =
List.fold_left
(fun accu -> function
| {
exp_descr = Abstraction { fun_typ = t; fun_name = Some f };
exp_loc = loc;
} ->
if not (value_name_ok f env) then
Cduce_error.raise_err_loc ~loc
Typer_Error "This function name clashes with another kind of identifier";
(f, t) :: accu
| _ -> assert false)
[] l
in
let env = enter_values typs env in
List.iter (fun e -> ignore (type_check env e Types.any false)) l;
typs
let rec unused_branches b =
List.iter
(fun (Branch (br, s)) ->
if br.br_ghost then ()
else if not br.br_used then warning br.br_loc "This branch is not used"
else (
(if not (IdSet.is_empty br.br_vars_empty) then
let msg =
try
let l =
List.map
(fun x ->
let x = Ident.to_string x in
if String.compare x "$$$" = 0 then raise Exit else x)
(br.br_vars_empty :> Id.t list)
in
let l = String.concat "," l in
"The following variables always match the empty sequence: " ^ l
with
| Exit -> "This projection always returns the empty sequence"
in
warning br.br_loc msg);
unused_branches s))
b
let report_unused_branches () =
unused_branches !cur_branch;
cur_branch := []
let clear_unused_branches () = cur_branch := []
(* API *)
let update_weak_variables env =
let to_patch, to_keep =
Var.Map.split
(fun v -> function
| Some _ -> true
| None -> false)
env.weak_vars
in
let to_patch =
Var.Map.map
(function
| Some t -> t
| None -> assert false)
to_patch
in
{
env with
ids =
Env.mapi
(fun v -> function
| Val t ->
let tt = Types.Subst.apply_full to_patch t in
Val tt
| x -> x)
env.ids;
weak_vars = to_keep;
}
let type_expr env e =
clear_unused_branches ();
let e = expr env e in
let t = type_check env e Types.any true in
report_unused_branches ();
(update_weak_variables env, e, t)
let type_let_decl env p e =
clear_unused_branches ();
let decl = let_decl env p e in
let typs = type_let_decl env decl in
report_unused_branches ();
let is_value = Typed.is_value decl.let_body in
(* patch env to update weak variables *)
let env = update_weak_variables env in
let typs =
List.map
(fun (id, t) ->
let tt = Types.Subst.clean_type Var.Set.empty t in
let vars = Types.Subst.vars tt in
if (not (Var.Set.is_empty vars)) && not is_value then
let weak_vars, all_weak_vars, _ =
Var.Set.fold
(fun (acc, accw, i) v ->
let wv = Var.mk ~kind:`weak ("_weak" ^ string_of_int i) in
((v, Types.var wv) :: acc, Var.Map.add wv None accw, i + 1))
([], env.weak_vars, Var.Map.length env.weak_vars)
vars
in
let () = env.weak_vars <- all_weak_vars in
let subst = Types.Subst.from_list weak_vars in
(id, Types.Subst.apply_full subst tt)
else
(* raise_loc_generic p.loc
(Format.asprintf
"The type of identifier %a is %a.@\n\
It contains polymorphic variables that cannot be generalized."
Ident.print id Types.Print.print tt);*)
(id, tt))
typs
in
let env = enter_values typs env in
( {
env with
ids_loc =
List.fold_left
(fun acc (id, _) -> Env.add id p.loc acc)
env.ids_loc typs;
mono_vars = Var.Set.empty;
poly_vars = [];
},
decl,
typs )
let type_let_funs env funs =
clear_unused_branches ();
let rec id = function
| Ast.LocatedExpr (_, e) -> id e
| Ast.Abstraction a -> fun_name env a
| _ -> assert false
in
let ids =
List.fold_left
(fun accu f ->
match id f with
| Some x -> x :: accu
| None -> accu)
[] funs
in
let env' = enter_values_dummy ids env in
let funs = List.map (expr env') funs in
let typs = type_rec_funs env funs in
report_unused_branches ();
let env = update_weak_variables env in
let env = enter_values typs env in
let env = { env with mono_vars = Var.Set.empty; poly_vars = [] } in
(env, funs, typs)
(*
let find_cu x env =
match find_cu noloc x env with
| ECDuce cu -> cu
| _ -> raise (Error ("Cannot find external unit " ^ (U.to_string x)))
*)
let check_weak_variables env =
Env.iter
(fun id -> function
| Val t ->
let vrs = Types.Subst.vars t in
Var.Set.iter
(fun v ->
match Var.kind v with
| `generated
| `user ->
()
| `weak ->
let loc = Env.find id env.ids_loc in
Cduce_error.(raise_err_loc ~loc Typer_WeakVar (id, t)))
vrs
| _ -> ())
env.ids