Skip to content

GitLab

Commit ad742151 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2005-02-22 00:41:58 by afrisch] New translation for types 

Original author: afrisch
Date: 2005-02-22 00:41:59+00:00
parent 01a9eb8f
Hide whitespace changes
Inline Side-by-side
driver/cduce.ml
View file @ ad742151
......@@ -258,9 +258,8 @@ let directive ppf tenv cenv = function
Typer.dump_type ppf tenv name;
flush_ppf ppf
| `Print_schema_type schema_ref ->
assert false
(* Typer.dump_schema_type ppf tenv schema_ref;
flush_ppf ppf *)
Typer.dump_schema_type ppf tenv schema_ref;
flush_ppf ppf
| `Reinit_ns ->
Typer.set_ns_table_for_printer tenv
| `Help ->
......
misc/stats.ml
View file @ ad742151
......@@ -59,6 +59,9 @@ module Counter = struct
let incr c =
c.count <- c.count + 1
let add c n =
c.count <- c.count + n
end
......
misc/stats.mli
View file @ ad742151
......@@ -9,6 +9,7 @@ module Counter: sig
val create: string -> t
val incr: t -> unit
val add: t -> int -> unit
val print: Format.formatter -> t -> unit
end
......
typing/typer.ml
View file @ ad742151
......@@ -285,49 +285,49 @@ module IType = struct
fv = None
}
(* Recursive hash-consing *)
let rec hash0 n = match n.desc with
| ILink n -> hash0 n
| IType (t,h) -> 1 + 17 * h
| IOr _ -> 2
| IAnd _ -> 3
| IDiff _ -> 4
| ITimes _ -> 5
| IXml _ -> 6
| IArrow _ -> 7
| IOptional _ -> 8
| IRecord _ -> 9
| ICapture x -> 10 + 17*(Id.hash x)
| IConstant (x,_) -> 11 + 17*(Id.hash x)
let hash0_field = function
| (p, Some e) -> 1 + 17 * hash0 p + 257 * hash0 e
| (p, None) -> 2 + 17 * hash0 p
let rec hash1 n = match n.desc with
| ILink n -> hash1 n
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 * hash0 p1 + 257 * hash0 p2
| IAnd (p1,p2) -> 3 + 17 * hash0 p1 + 257 * hash0 p2
| IDiff (p1,p2) -> 4 + 17 * hash0 p1 + 257 * hash0 p2
| ITimes (p1,p2) -> 5 + 17 * hash0 p1 + 257 * hash0 p2
| IXml (p1,p2) -> 6 + 17 * hash0 p1 + 257 * hash0 p2
| IArrow (p1,p2) -> 7 + 17 * hash0 p1 + 257 * hash0 p2
| IOptional p -> 8 + 17 * hash0 p
| IRecord (o,r)->9+(if o then 17 else 0)+257*(LabelMap.hash hash0_field r)
| 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)
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 = hash1 n in n.smallhash <- h; h)
else (
let h = hash2 n in
n.smallhash <- h; h
)
let rec repr = function
| { desc = ILink n } -> repr n
| { 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
......@@ -337,20 +337,20 @@ module IType = struct
let rec unify x y =
if x == y then ()
else let x = repr x and y = repr y in if x == y then ()
(* else if (smallhash x != smallhash y) then raise Unify *)
else let x = prot_repr x and y = prot_repr y in if x == y then ()
else if (smallhash x != smallhash y) then raise Unify
else if (x.t != None) && (y.t != None) then raise 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
| 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
| 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 Unify xr yr
| ICapture xv, ICapture yv when Id.equal xv yv -> ()
......@@ -362,9 +362,10 @@ module IType = struct
| (p1, None), (p2, None) -> unify p1 p2
| _ -> raise Unify
let may_unify x y =
try unify x y; back := []; true
with Unify ->
with Unify ->
List.iter (fun (x,xd) -> x.desc <- xd) !back; back := []; false
module SmallHash = Hashtbl.Make(
......@@ -388,7 +389,10 @@ module IType = struct
let minimize ((mem,add) as h) =
let rec aux n =
let n = repr n in
if mem n then () else (add n (); if n.t == None then iter aux n.desc)
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 []
......@@ -396,27 +400,11 @@ module IType = struct
let rec rechash n =
let n = repr n in
if (n.sid != 0) then 17 * n.sid
else begin incr sid; n.sid <- !sid; to_clear := n :: !to_clear;
match n.desc with
| ILink _ -> assert false
| IType (t,h) -> 1 + 17 * h
| IOr (p1,p2) -> 2 + 17 * rechash p1 + 257 * rechash p2
| IAnd (p1,p2) -> 3 + 17 * rechash p1 + 257 * rechash p2
| IDiff (p1,p2) -> 4 + 17 * rechash p1 + 257 * rechash p2
| ITimes (p1,p2) -> 5 + 17 * rechash p1 + 257 * rechash p2
| IXml (p1,p2) -> 6 + 17 * rechash p1 + 257 * rechash p2
| IArrow (p1,p2) -> 7 + 17 * rechash p1 + 257 * rechash p2
| IOptional p -> 8 + 17 * rechash p
| IRecord(o,r)->9+(if o then 17 else 0)+257*(LabelMap.hash rechash_field r)
| ICapture x -> 10 + 17 * (Id.hash x)
| IConstant (x,c) -> 11 + 17 * (Id.hash x) + 257*(Types.Const.hash c)
end
and rechash_field = function
| (p, Some e) -> 1 + 17 * rechash p + 257 * rechash e
| (p, None) -> 2 + 17 * rechash p
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
sid := 0; List.iter (fun x -> x.sid <- 0) !to_clear;
to_clear := []
let rechash n =
let n = repr n in
......@@ -431,12 +419,27 @@ module IType = struct
end
)
(** Two-phases recursive hash-consing **)
(*
let gtable = RecHash.create 17577
let internalize n =
let local = SmallHash.create 67 in
minimize (SmallHash.mem local, SmallHash.add local) n;
minimize (RecHash.mem gtable, RecHash.add gtable) 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 *)
......@@ -446,7 +449,7 @@ module IType = struct
let n = repr n in
if (n.sid = 0) then (
n.sid <- 1;
to_clear := n :: !to_clear;
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
......@@ -457,7 +460,34 @@ module IType = struct
| Some x -> x
| None -> aux n; clear (); n.fv <- Some !fv; !fv
(* To the internal representation *)
(* optimized version to check closedness *)
let no_fv = Some IdSet.empty
let check_no_fv loc n =
let err x =
raise_loc_generic loc
("Capture variable not allowed: " ^ (Ident.to_string 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, _ -> (match IdSet.pick x with Some x -> err x | None -> ())
| None, (ICapture x | IConstant (x,_)) -> err x;
| None, d -> iter aux d
)
in
try
match n.fv with
| Some x -> (match IdSet.pick x with Some x -> err x | None -> ())
| None -> aux n;
List.iter (fun n -> n.sid <- 0; n.fv <- no_fv) !to_clear;
to_clear := []
with exn -> clear (); raise exn
(* From the intermediate representation to the internal one *)
let rec typ n =
......@@ -483,6 +513,7 @@ module IType = struct
raise (Patterns.Error "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 ->
......@@ -538,6 +569,7 @@ module IType = struct
| IType _ | ILink _ -> assert false
and pat_node n =
let n = repr n in
match n.pnode with
| Some p -> p
| None ->
......@@ -563,12 +595,12 @@ module IType = struct
let iempty = itype Types.empty
let ior p1 p2 =
if p1 == iempty then p2
else if p2 == iempty then p1
if p1.desc == iempty.desc then p2
else if p2.desc == iempty.desc then p1
else mk (IOr (p1,p2))
let iand p1 p2 =
if (p1 == iempty) || (p2 == iempty) then iempty
if (p1.desc == iempty.desc) || (p2.desc == iempty.desc) then iempty
else mk (IAnd (p1,p2))
type regexp =
......@@ -639,6 +671,28 @@ module IType = struct
let rexp r = remove_regexp r (itype Sequence.nil_type)
let all_delayed = ref []
let delayed loc =
let s = mk_delayed () in
all_delayed := (loc,s) :: !all_delayed;
s
let check_one_delayed (loc,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
with Exit -> error loc "Ill-formed recursion"
let check_delayed () =
let l = !all_delayed in
all_delayed := [];
List.iter check_one_delayed l
let rec derecurs env p = match p.descr with
| PatVar v -> derecurs_var env p.loc v
| SchemaVar (kind, schema_name, component_name) ->
......@@ -727,26 +781,21 @@ module IType = struct
("Unbound external type " ^ cu ^ ":" ^ (U.to_string v))
and derecurs_def env b =
let b = List.map (fun (v,p) -> (v,p,mk_delayed ())) b in
let b = List.map (fun (v,p) -> (v,p,delayed p.loc)) b in
let n =
List.fold_left (fun env (v,p,s) -> Env.add v s env) env.penv_derec b in
let env = { env with penv_derec = n } in
List.iter (fun (v,p,s) -> s.desc <- ILink (derecurs env p)) b;
env
let check_no_capture loc s =
match IdSet.pick s with
| Some x ->
raise_loc_generic loc
("Capture variable not allowed: " ^ (Ident.to_string x))
| None -> ()
let derec penv p =
let d = derecurs penv p in
check_delayed ();
internalize d;
d
let typ env t =
let d = derecurs (penv env) t in
check_no_capture t.loc (fv d);
typ_node d
let pat env t = pat_node (derecurs (penv env) t)
(* API *)
module Ids = Set.Make(Id)
let type_defs env b =
......@@ -761,12 +810,16 @@ module IType = struct
) Ids.empty b);
let penv = derecurs_def (penv env) b in
let b = List.map (fun (v,p) -> (v,p,derecurs penv p)) b in
let aux t =
let d = derec penv t in
check_no_fv t.loc d;
try typ d
with Patterns.Error s -> raise_loc_generic t.loc s
in
let b =
List.map
(fun (v,p,s) ->
check_no_capture p.loc (fv s);
let t = Types.descr (typ_node s) in
(fun (v,p) ->
let t = aux p in
if (p.loc <> noloc) && (Types.is_empty t) then
warning p.loc
("This definition yields an empty type for " ^ (Ident.to_string v));
......@@ -774,731 +827,27 @@ module IType = struct
List.iter (fun (v,t) -> Types.Print.register_global (Id.value v) t) b;
b
end
(*
(* Eliminate Recursion, propagate Sequence Capture Variables *)
(* We use two intermediate representation from AST types/patterns
to internal ones:
AST -(1)-> derecurs -(2)-> slot -(3)-> internal
(1) eliminate recursion, schema,
propagate sequence capture variables, keep regexps
(2) stratify, detect ill-formed recursion, compile regexps
(3) check additional constraints on types / patterns;
deep (recursive) hash-consing
*)
type derecurs_slot = {
ploc : Location.loc;
pid : int;
mutable ploop : bool;
mutable pdescr : derecurs;
} and derecurs =
| PDummy
| PAlias of derecurs_slot
| PType of Types.descr * int
| POr of derecurs * derecurs
| PAnd of derecurs * derecurs
| PDiff of derecurs * derecurs
| PTimes of derecurs * derecurs
| PXml of derecurs * derecurs
| PArrow of derecurs * derecurs
| POptional of derecurs
| PRecord of bool * (derecurs * derecurs option) label_map
| PCapture of id
| PConstant of id * Types.const
| PRegexp of derecurs_regexp
and derecurs_regexp =
| PEpsilon
| PElem of derecurs
| PGuard of derecurs
| PSeq of derecurs_regexp * derecurs_regexp
| PAlt of derecurs_regexp * derecurs_regexp
| PStar of derecurs_regexp
| PWeakStar of derecurs_regexp
let rec print_derecurs ppf = function
| PDummy -> Format.fprintf ppf "Dummy"
| PAlias a -> Format.fprintf ppf "Alias %i" a.pid
| PType _ -> Format.fprintf ppf "Type"
| POr (r1,r2) -> Format.fprintf ppf "Or(%a,%a)"
print_derecurs r1 print_derecurs r2
| PAnd (r1,r2) -> Format.fprintf ppf "And(%a,%a)"
print_derecurs r1 print_derecurs r2
| PDiff (r1,r2) -> Format.fprintf ppf "Diff(%a,%a)"
print_derecurs r1 print_derecurs r2
| PTimes (r1,r2) -> Format.fprintf ppf "Times(%a,%a)"
print_derecurs r1 print_derecurs r2
| PXml (r1,r2) -> Format.fprintf ppf "Xml(%a,%a)"
print_derecurs r1 print_derecurs r2
| PRegexp r -> Format.fprintf ppf "Regexp(%a)" print_regexp r
| _ -> Format.fprintf ppf "Other"
and print_regexp ppf = function
| PEpsilon -> Format.fprintf ppf "e"
| PElem r -> Format.fprintf ppf "(%a)" print_derecurs r
| PGuard r -> Format.fprintf ppf "/(%a)" print_derecurs r
| PSeq (r1,r2) -> Format.fprintf ppf "%a,%a" print_regexp r1 print_regexp r2
| PAlt (r1,r2) -> Format.fprintf ppf "%a|%a" print_regexp r1 print_regexp r2
| PStar r | PWeakStar r -> Format.fprintf ppf "%a*" print_regexp r
type descr =
| IDummy
| IType of Types.descr * int
| IOr of descr * descr
| IAnd of descr * descr
| IDiff of descr * descr
| ITimes of slot * slot
| IXml of slot * slot
| IArrow of slot * slot
| IOptional of descr
| IRecord of bool * (slot * descr option) label_map
| ICapture of id
| IConstant of id * Types.const
and slot = {
mutable fv : fv option;
mutable hash : int option;
mutable rank1: int; mutable rank2: int;
mutable gen1 : int; mutable gen2: int;
mutable d : descr;
}
let counter = ref 0
let mk_derecurs_slot loc =
incr counter;
{ ploop = false; ploc = loc; pid = !counter; pdescr = PDummy }
let mk_slot () =
{ d=IDummy; fv=None; hash=None; rank1=0; rank2=0; gen1=0; gen2=0 }
(* This environment is used in phase (1) to eliminate recursion *)
type penv = {
penv_tenv : t;
penv_derec : derecurs_slot Env.t;
}
let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty }
let rec hash_derecurs = function
| PDummy -> assert false
| PAlias s ->
s.pid
| PType (t,hash) ->
1 + 17 * hash
| POr (p1,p2) ->
2 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
| PAnd (p1,p2) ->
3 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
| PDiff (p1,p2) ->
4 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
| PTimes (p1,p2) ->
5 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
| PXml (p1,p2) ->
6 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
| PArrow (p1,p2) ->
7 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
| POptional p ->
8 + 17 * (hash_derecurs p)
| PRecord (o,r) ->
(if o then 9 else 10) + 17 * (LabelMap.hash hash_derecurs_field r)
| PCapture x ->
11 + 17 * (Id.hash x)
| PConstant (x,c) ->
12 + 17 * (Id.hash x) + 257 * (Types.Const.hash c)
| PRegexp p ->
13 + 17 * (hash_derecurs_regexp p)
and hash_derecurs_field = function
| (p, Some e) -> 1 + 17 * hash_derecurs p + 257 * hash_derecurs e
| (p, None) -> 2 + 17 * hash_derecurs p
and hash_derecurs_regexp = function
| PEpsilon ->
1
| PElem p ->
2 + 17 * (hash_derecurs p)
| PSeq (p1,p2) ->
3 + 17 * (hash_derecurs_regexp p1) + 257 * (hash_derecurs_regexp p2)
| PAlt (p1,p2) ->
4 + 17 * (hash_derecurs_regexp p1) + 257 * (hash_derecurs_regexp p2)
| PStar p ->
5 + 17 * (hash_derecurs_regexp p)
| PWeakStar p ->
6 + 17 * (hash_derecurs_regexp p)
| PGuard p ->
7 + 17 * (hash_derecurs p)
let rec equal_derecurs p1 p2 = (p1 == p2) || match p1,p2 with
| PAlias s1, PAlias s2 ->
s1 == s2
| PType (t1,h1), PType (t2,h2) ->
(h1 == h2) && (Types.equal t1 t2)
| POr (p1,q1), POr (p2,q2)
| PAnd (p1,q1), PAnd (p2,q2)
| PDiff (p1,q1), PDiff (p2,q2)
| PTimes (p1,q1), PTimes (p2,q2)
| PXml (p1,q1), PXml (p2,q2)
| PArrow (p1,q1), PArrow (p2,q2) ->
(equal_derecurs p1 p2) && (equal_derecurs q1 q2)
| POptional p1, POptional p2 ->
equal_derecurs p1 p2
| PRecord (o1,r1), PRecord (o2,r2) ->
(o1 == o2) && (LabelMap.equal equal_derecurs_field r1 r2)
| PCapture x1, PCapture x2 ->
Id.equal x1 x2
| PConstant (x1,c1), PConstant (x2,c2) ->
(Id.equal x1 x2) && (Types.Const.equal c1 c2)
| PRegexp p1, PRegexp p2 ->
equal_derecurs_regexp p1 p2
| _ -> false
and equal_derecurs_field r1 r2 = match (r1,r2) with
| (p1,None),(p2,None) -> equal_derecurs p1 p2
| (p1, Some e1), (p2, Some e2) -> equal_derecurs p1 p2 && equal_derecurs e1 e2
| _ -> false
and equal_derecurs_regexp r1 r2 = match r1,r2 with
| PEpsilon, PEpsilon ->
true
| PElem p1, PElem p2 ->
equal_derecurs p1 p2
| PGuard p1, PGuard p2 ->
equal_derecurs p1 p2
| PSeq (p1,q1), PSeq (p2,q2)
| PAlt (p1,q1), PAlt (p2,q2) ->
(equal_derecurs_regexp p1 p2) && (equal_derecurs_regexp q1 q2)
| PStar p1, PStar p2
| PWeakStar p1, PWeakStar p2 ->
equal_derecurs_regexp p1 p2
| _ -> false
module DerecursTable = Hashtbl.Make(
struct
type t = derecurs
let hash = hash_derecurs
let equal = equal_derecurs
end
)
let gen = ref 0
let rank = ref 0
let rec hash_descr = function
| IDummy -> assert false
| IType (t,h) -> h
| IOr (d1,d2) -> 1 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IAnd (d1,d2) -> 2 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IDiff (d1,d2) -> 3 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IOptional d -> 4 + 17 * (hash_descr d)
| ITimes (s1,s2) -> 5 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IXml (s1,s2) -> 6 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IArrow (s1,s2) -> 7 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IRecord (o,r) -> (if o then 8 else 9) + 17 * (LabelMap.hash hash_descr_field r)
| ICapture x -> 10 + 17 * (Id.hash x)
| IConstant (x,y) -> 11 + 17 * (Id.hash x) + 257 * (Types.Const.hash y)
and hash_descr_field = function
| (d, Some e) -> 1 + 17 * hash_slot d + 257 * hash_descr e
| (d, None) -> 2 + 17 * hash_slot d
and hash_slot s =
if s.gen1 = !gen then 13 * s.rank1
else (
incr rank;