Commit 9da1d67c authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Add a workaround in case pattern compilation failed (after typechecking) due...

Add a workaround in case pattern compilation failed (after typechecking) due to the presence of type variables in some types.
parent cd7eaf51
......@@ -39,18 +39,18 @@ let accept x = Types.internalize x.accept
let printed = ref []
let to_print = ref []
let rec print ppf (a,_,d) =
let rec print ppf (a,_,d) =
match d with
| Constr t -> Types.Print.pp_type 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) ->
| Times (n1,n2) ->
Format.fprintf ppf "(P%i,P%i)" n1.id n2.id;
to_print := n1 :: n2 :: !to_print
| Xml (n1,n2) ->
| Xml (n1,n2) ->
Format.fprintf ppf "XML(P%i,P%i)" n1.id n2.id;
to_print := n1 :: n2 :: !to_print
| Record (l,n) ->
| Record (l,n) ->
Format.fprintf ppf "{ %a = P%i }" Label.print_attr l n.id;
to_print := n :: !to_print
| Capture x ->
......@@ -111,31 +111,31 @@ let cons fv d =
q
let constr x = (x,IdSet.empty,Constr x)
let cup ((acc1,fv1,_) as x1) ((acc2,fv2,_) as x2) =
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
raise
(Error
("The capture variable " ^ (Ident.to_string x) ^
raise
(Error
("The capture variable " ^ (Ident.to_string x) ^
" should appear on both side of this | pattern"))
);
(Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1,x2))
let cap ((acc1,fv1,_) as x1) ((acc2,fv2,_) as 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
raise
(Error
("The capture variable " ^ (Ident.to_string x) ^
raise
(Error
("The capture variable " ^ (Ident.to_string x) ^
" cannot appear on both side 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 =
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))
......@@ -163,7 +163,7 @@ module Pat = struct
| 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
let c = compare x1 x2 in if c <> 0 then c
else compare y1 y2
| Cup _, _ -> -1 | _, Cup _ -> 1
| Cap _, _ -> -1 | _, Cap _ -> 1
......@@ -222,7 +222,7 @@ module Print = struct
(incr id;
names := M.add p !id !names;
Queue.add p toprint)
else
else
let seen = S.add p seen in
match d with
| Cup (p1,p2) | Cap (p1,p2) -> mark seen p1; mark seen p2
......@@ -231,7 +231,7 @@ module Print = struct
| _ -> ()
let rec print ppf p =
try
try
let i = M.find p !names in
Format.fprintf ppf "P%i" i
with Not_found ->
......@@ -255,14 +255,14 @@ module Print = struct
| Constant (x,c) ->
Format.fprintf ppf "(%a:=%a)" Ident.print x Types.Print.pp_const c
| Dummy -> assert false
let pp 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
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")
......@@ -298,10 +298,10 @@ let empty_res fv = IdMap.constant (Types.Positive.ty Types.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) =
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)
......@@ -314,7 +314,7 @@ let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
else
match d with
| Constr t0 ->
if Types.subtype t t0 then IdMap.empty
if Types.subtype t t0 then IdMap.empty
else (empty_res fv) (* omega *)
| Cup ((a,_,_) as d1,d2) ->
IdMap.merge cup_res
......@@ -333,9 +333,9 @@ let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
| Dummy -> assert false
and filter_prod ?kind fv p1 p2 t =
List.fold_left
List.fold_left
(fun accu (d1,d2) ->
let term =
let term =
IdMap.merge times_res (filter_node d1 p1) (filter_node d2 p2)
in
IdMap.merge cup_res accu term
......@@ -377,20 +377,20 @@ module Factorize = struct
x=(1,2)
*)
let rec approx_var seen (a,fv,d) t xs =
(* assert (Types.subtype t a);
(* 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)
(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) ->
| 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
......@@ -404,22 +404,22 @@ x=(1,2)
(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)
if (NodeTypeSet.mem (q,t) seen)
then xs
else approx_var (NodeTypeSet.add (q,t) seen) q.descr t xs
(* Obviously not complete ! *)
(* Obviously not complete ! *)
let rec approx_nil seen (a,fv,d) t xs =
assert (Types.subtype t a);
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)
(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))
......@@ -429,9 +429,9 @@ x=(1,2)
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)
if (NodeTypeSet.mem (q,t) seen)
then xs
else approx_nil (NodeTypeSet.add (q,t) seen) q.descr t xs
......@@ -448,11 +448,11 @@ x=(1,2)
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 =
let var ((a,_,_) as p) t =
approx_var NodeTypeSet.empty p (Types.cap t a)
let nil ((a,_,_) as p) t =
let nil ((a,_,_) as p) t =
approx_nil NodeTypeSet.empty p (Types.cap t a)
end
......@@ -466,7 +466,7 @@ 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
if Types.is_empty acc
then Label.dummy
else match d with
| Constr t -> Types.Record.first_label t
......@@ -477,11 +477,11 @@ let rec first_label (acc,fv,d) =
module Normal = struct
type source = SCatch | SConst of Types.const
type source = SCatch | SConst of Types.const
type result = source id_map
let compare_source s1 s2 =
if s1 == s2 then 0
if s1 == s2 then 0
else match (s1,s2) with
| SCatch, _ -> -1 | _, SCatch -> 1
| SConst c1, SConst c2 -> Types.Const.compare c1 c2
......@@ -491,7 +491,7 @@ module Normal = struct
| SCatch -> 1
| SConst c -> Types.Const.hash c
*)
let compare_result r1 r2 =
IdMap.compare compare_source r1 r2
......@@ -506,19 +506,19 @@ module Normal = struct
include Custom.Dummy
type t = NodeSet.t * Types.t * IdSet.t (* pl,t; t <= \accept{pl} *)
let check ((pl,t,xs) : t) =
List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept)))
(pl :> Node.t list)
let print ppf (pl,t,xs) =
Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]"
Format.fprintf ppf "@[(pl=%a;t=%a;xs=%a)@]"
NodeSet.dump pl Types.Print.pp_type 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) =
let hash (l,t,xs) =
(NodeSet.hash l) + 17 * (Types.hash t) + 257 * (IdSet.hash xs)
let equal x y = compare x y == 0
......@@ -554,24 +554,24 @@ module Normal = struct
let fus = IdMap.union_disj
let nempty lab =
{ nprod = NLineProd.empty;
let nempty lab =
{ nprod = NLineProd.empty;
nxml = NLineProd.empty;
nrecord = (match lab with
nrecord = (match lab with
| Some l -> RecLabel (l,NLineProd.empty)
| None -> RecNolabel (None,None))
}
let dummy = nempty None
let ncup nf1 nf2 =
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,r1), RecLabel (l2,r2) ->
(* assert (l1 = l2); *)
RecLabel (l1, NLineProd.union r1 r2)
| RecNolabel (x1,y1), RecNolabel (x2,y2) ->
| RecNolabel (x1,y1), RecNolabel (x2,y2) ->
RecNolabel((if x1 == None then x2 else x1),
(if y1 == None then y2 else y1))
| _ -> assert false)
......@@ -588,9 +588,9 @@ module Normal = struct
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,
NLineProd.add (fus res1 res2,
(NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2),
(NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2))
(NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2))
accu
in
let record r1 r2 = match r1,r2 with
......@@ -598,8 +598,8 @@ module Normal = struct
(* 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)
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)
......@@ -621,18 +621,18 @@ module Normal = struct
let single_prod src p q = NLineProd.singleton (src, p,q)
let ntimes lab acc p q xs =
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
{ (nempty lab) with
nprod = single_prod empty_res (nnode p xsp) (nnode q xsq)
}
let nxml lab acc p q xs =
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
{ (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
......@@ -649,18 +649,18 @@ module Normal = struct
let nconstr lab t =
let aux l =
List.fold_left (fun accu (t1,t2) ->
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),
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 =
nxml =
aux (Types.Product.clean_normal (Types.Product.normal ~kind:`XML t));
nrecord = record
}
......@@ -683,9 +683,9 @@ module Normal = struct
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)
| 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
......@@ -699,7 +699,7 @@ module Normal = struct
let facto f t xs pl =
List.fold_left
List.fold_left
(fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs)))
IdSet.empty
pl
......@@ -713,10 +713,10 @@ module Normal = struct
(vs_var,vs_nil,(pl,t,xs))
let normal l t pl xs =
List.fold_left
List.fold_left
(fun a p -> ncap a (nnormal l (descr p) xs)) (nconstr l t) pl
let nnf lab t0 (pl,t,xs) =
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 (NodeSet.get pl) xs
......@@ -724,21 +724,21 @@ module Normal = struct
let basic_tests f (pl,t,xs) =
let rec aux more s accu t res = function
(* Invariant: t and s disjoint, t not empty *)
| [] ->
| [] ->
let accu =
try
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)
| (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) ->
| 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 =
......@@ -747,22 +747,22 @@ module Normal = struct
| [] -> 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)
aux_check [] Types.empty ResultMap.empty (Types.cap t any_basic)
IdMap.empty (List.map descr (NodeSet.get pl))
(*
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)
| (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) ->
| 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
......@@ -773,7 +773,7 @@ module Normal = struct
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 =
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')
......@@ -798,8 +798,8 @@ end
module Compile = struct
open Auto_pat
type return_code =
type return_code =
Types.t * int * (* accepted type, arity *)
int id_map option array
......@@ -835,7 +835,7 @@ module Compile = struct
let equal_source s1 s2 =
(s1 == s2) || match (s1,s2) with
| Const x, Const y -> Types.Const.equal x y
| 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
......@@ -844,7 +844,7 @@ module Compile = struct
(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) ->
| 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
......@@ -867,24 +867,24 @@ module Compile = struct
| 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 = basic;
atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.BoolAtoms.leafconj (Types.Atom.get t), r) basic);
chars = Chars.mk_map (List.map (fun (t,r) -> Types.BoolChars.leafconj (Types.Char.get t), r) basic);
prod = prod;
xml = xml;
prod = prod;
xml = xml;
record = 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)
if (array_for_all (fun (_,ar,_) -> ar == 0) disp.codes)
&& (array_for_all ( f act.(0) ) act) then
Ignore act.(0)
else
......@@ -897,10 +897,10 @@ module Compile = struct
let detect_right_tail_call =
detect_tail_call
(fun i (code,ret,_) ->
(i == code) &&
(i == code) &&
let ar = Array.length ret in
(array_for_all_i
(fun pos ->
(array_for_all_i
(fun pos ->
function Stack j when pos + j == ar -> true | _ -> false)
ret
)
......@@ -908,26 +908,26 @@ module Compile = struct
let detect_left_tail_call =
detect_tail_call
(fun i ->
function
(fun i ->
function
| Ignore (code,ret,_) when (i == code) ->
let ar = Array.length ret in
array_for_all_i
(fun pos ->
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
......@@ -935,17 +935,17 @@ module Compile = struct
| `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.pp_type disp.t;
Array.iter (fun p ->
Format.fprintf ppf " pat %a@." Normal.Nnf.print p;
) disp.pl
let first_lab t (reqs : Normal.Nnf.t array) =
let aux l req = Label.min l (Normal.Nnf.first_label req) in
let lab =
let lab =
Array.fold_left aux (Types.Record.first_label t) reqs in
if lab == Label.dummy then None else Some lab
......@@ -959,9 +959,9 @@ module Compile = struct
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
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
...