exception Error of string open Ident let print_lab ppf l = if (l == LabelPool.dummy_max) then Format.fprintf ppf "" else Label.print ppf (LabelPool.value l) (* 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 (LabelPool.value l) n.id; to_print := n :: !to_print | Capture x -> Format.fprintf ppf "%a" U.print (Id.value x) | Constant (x,c) -> Format.fprintf ppf "(%a := %a)" U.print (Id.value 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 = State.ref "Patterns.counter" 0 let dummy = (Types.empty,IdSet.empty,Dummy) let make fv = incr counter; { id = !counter; descr = dummy; accept = Types.make (); fv = 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 -> match IdSet.pick (IdSet.diff fv2 fv1) with Some x -> x | None -> assert false in raise (Error ("The capture variable " ^ (U.to_string (Id.value 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) = if not (IdSet.disjoint fv1 fv2) then ( match IdSet.pick (IdSet.cap fv1 fv2) with | Some x -> raise (Error ("The capture variable " ^ (U.to_string (Id.value x)) ^ " cannot appear on both side of this & pattern")) | None -> assert false ); (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)) 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 = print_node module SMemo = Set.Make(Custom.Int) let memo = Serialize.Put.mk_property (fun t -> ref SMemo.empty) let rec serialize t n = let l = Serialize.Put.get_property memo t in Serialize.Put.int t n.id; if not (SMemo.mem n.id !l) then ( l := SMemo.add n.id !l; Types.Node.serialize t n.accept; IdSet.serialize t n.fv; serialize_descr t n.descr ) and serialize_descr s (_,_,d) = serialize_d s d and serialize_d s = function | Constr t -> Serialize.Put.bits 3 s 0; Types.serialize s t | Cup (p1,p2) -> Serialize.Put.bits 3 s 1; serialize_descr s p1; serialize_descr s p2 | Cap (p1,p2) -> Serialize.Put.bits 3 s 2; serialize_descr s p1; serialize_descr s p2 | Times (p1,p2) -> Serialize.Put.bits 3 s 3; serialize s p1; serialize s p2 | Xml (p1,p2) -> Serialize.Put.bits 3 s 4; serialize s p1; serialize s p2 | Record (l,p) -> Serialize.Put.bits 3 s 5; LabelPool.serialize s l; serialize s p | Capture x -> Serialize.Put.bits 3 s 6; Id.serialize s x | Constant (x,c) -> Serialize.Put.bits 3 s 7; Id.serialize s x; Types.Const.serialize s c | Dummy -> assert false module DMemo = Map.Make(Custom.Int) let memo = Serialize.Get.mk_property (fun t -> ref DMemo.empty) let rec deserialize t = let l = Serialize.Get.get_property memo t in let id = Serialize.Get.int t in try DMemo.find id !l with Not_found -> let accept = Types.Node.deserialize t in let fv = IdSet.deserialize t in incr counter; let n = { id = !counter; descr = dummy; accept = accept; fv = fv } in l := DMemo.add id n !l; n.descr <- deserialize_descr t; n and deserialize_descr s = match Serialize.Get.bits 3 s with | 0 -> constr (Types.deserialize s) | 1 -> (* Avoid unnecessary tests *) let (acc1,fv1,_) as x1 = deserialize_descr s in let (acc2,fv2,_) as x2 = deserialize_descr s in (Types.cup acc1 acc2, IdSet.cup fv1 fv2, Cup (x1,x2)) | 2 -> let (acc1,fv1,_) as x1 = deserialize_descr s in let (acc2,fv2,_) as x2 = deserialize_descr s in (Types.cap acc1 acc2, IdSet.cup fv1 fv2, Cap (x1,x2)) | 3 -> let x = deserialize s in let y = deserialize s in times x y | 4 -> let x = deserialize s in let y = deserialize s in xml x y | 5 -> let l = LabelPool.deserialize s in let x = deserialize s in record l x | 6 -> capture (Id.deserialize s) | 7 -> let x = Id.deserialize s in let c = Types.Const.deserialize s in constant x c | _ -> assert false 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 = LabelPool.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 * (LabelPool.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 end module Print = 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 (LabelPool.value 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 (* Static semantics *) let cup_res v1 v2 = Types.Positive.cup [v1;v2] 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) = 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) and filter_node t p : Types.Positive.v id_map = try MemoFilter.find (t,p) !memo_filter with Not_found -> let (_,fv,_) as d = 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.get (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) as p) 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) as p) 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 LabelPool.dummy_max else match d with | Constr t -> Types.Record.first_label t | Cap (p,q) -> min (first_label p) (first_label q) | Cup ((acc1,_,_) as p,q) -> min (first_label p) (first_label q) | Record (l,p) -> l | _ -> LabelPool.dummy_max module Normal = struct type source = | SCatch | SConst of Types.const | SLeft | SRight | SRecompose type result = source id_map let compare_source s1 s2 = if s1 == s2 then 0 else match (s1,s2) with | SCatch, _ -> -1 | _, SCatch -> 1 | SLeft, _ -> -1 | _, SLeft -> 1 | SRight, _ -> -1 | _, SRight -> 1 | SRecompose, _ -> -1 | _, SRecompose -> 1 | SConst c1, SConst c2 -> Types.Const.compare c1 c2 let hash_source = function | SCatch -> 1 | SLeft -> 2 | SRight -> 3 | SRecompose -> 4 | SConst c -> Types.Const.hash c let compare_result r1 r2 = IdMap.compare compare_source r1 r2 let hash_result r = IdMap.hash hash_source r let print_result ppf r = Format.fprintf ppf "" let print_result_option ppf = function | Some x -> Format.fprintf ppf "Some(%a)" print_result x | None -> Format.fprintf ppf "None" module NodeSet = SortedList.Make(Node) module Nnf = struct 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)@]" NodeSet.dump pl Types.Print.print t 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) = List.fold_left (fun l p -> min l (first_label (descr p))) (Types.Record.first_label t) pl end module NBasic = struct include Custom.Dummy let serialize s _ = failwith "Patterns.NLineBasic.serialize" type t = result * Types.t let compare (r1,t1) (r2,t2) = let c = compare_result r1 r2 in if c <> 0 then c else Types.compare t1 t2 let equal x y = compare x y == 0 let hash (r,t) = hash_result r + 17 * Types.hash t end module NProd = struct type t = result * Nnf.t * Nnf.t let serialize s _ = failwith "Patterns.NLineProd.serialize" let deserialize s = failwith "Patterns.NLineProd.deserialize" let check x = () let dump ppf (r,x,y) = Format.fprintf ppf "@[(result=%a;x=%a;y=%a)@]" print_result r Nnf.print x Nnf.print y 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 let equal x y = compare x y == 0 let hash (r,x,y) = hash_result r + 17 * (Nnf.hash x) + 267 * (Nnf.hash y) end module NLineBasic = SortedList.Make(NBasic) module NLineProd = SortedList.Make(NProd) type record = | RecNolabel of result option * result option | RecLabel of label * NLineProd.t type t = { nfv : fv; na : Types.t; nbasic : NLineBasic.t; nprod : NLineProd.t; nxml : NLineProd.t; nrecord: record } let print_record ppf = function | RecLabel (lab,l) -> Format.fprintf ppf "RecLabel(@[%a@],@ @[%a@])" Label.print (LabelPool.value lab) NLineProd.dump l | RecNolabel (a,b) -> Format.fprintf ppf "RecNolabel(@[%a@],@[%a@])" print_result_option a print_result_option b let print ppf nf = Format.fprintf ppf "@[NF{na=%a;@[nrecord=@ @[%a@]@]}@]" Types.Print.print nf.na print_record nf.nrecord include Custom.Dummy let compare_record t1 t2 = match t1,t2 with | RecNolabel (s1,n1), RecNolabel (s2,n2) -> (match (s1,s2,n1,n2) with | Some r1, Some r2, _, _ -> compare_result r1 r2 | None, Some _, _, _ -> -1 | Some _, None, _, _ -> 1 | None,None,Some r1, Some r2 -> compare_result r1 r2 | None,None,None, Some _ -> -1 | None,None, Some _, None -> 1 | None,None, None, None -> 0) | RecNolabel (_,_), _ -> -1 | _, RecNolabel (_,_) -> 1 | RecLabel (l1,p1), RecLabel (l2,p2) -> let c = LabelPool.compare l1 l2 in if c <> 0 then c else NLineProd.compare p1 p2 let compare t1 t2 = if t1 == t2 then 0 else (* TODO: reorder; remove comparison of nfv ? *) let c = IdSet.compare t1.nfv t2.nfv in if c <> 0 then c else let c = Types.compare t1.na t2.na in if c <> 0 then c else let c = NLineBasic.compare t1.nbasic t2.nbasic in if c <> 0 then c else let c = NLineProd.compare t1.nprod t2.nprod in if c <> 0 then c else let c = NLineProd.compare t1.nxml t2.nxml in if c <> 0 then c else compare_record t1.nrecord t2.nrecord let fus = IdMap.union_disj let nempty lab = { nfv = IdSet.empty; na = Types.empty; nbasic = NLineBasic.empty; 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 = (* assert (Types.is_empty (Types.cap nf1.na nf2.na)); *) (* assert (nf1.nfv = nf2.nfv); *) { nfv = nf1.nfv; na = Types.cup nf1.na nf2.na; nbasic = NLineBasic.cup nf1.nbasic nf2.nbasic; nprod = NLineProd.cup nf1.nprod nf2.nprod; nxml = NLineProd.cup nf1.nxml nf2.nxml; nrecord = (match (nf1.nrecord,nf2.nrecord) with | RecLabel (l1,r1), RecLabel (l2,r2) -> (* assert (l1 = l2); *) RecLabel (l1, NLineProd.cup 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 f l1 l2 = List.fold_left (fun accu x1 -> List.fold_left (fun accu x2 -> f accu x1 x2) accu l2) [] l1 let double_fold_prod f l1 l2 = double_fold f (NLineProd.get l1) (NLineProd.get l2) 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 (fus res1 res2, (NodeSet.cup pl1 pl2, t, IdSet.cup xs1 xs2), (NodeSet.cup ql1 ql2, s, IdSet.cup ys1 ys2)) :: accu in let basic accu (res1,t1) (res2,t2) = let t = Types.cap t1 t2 in if Types.is_empty t then accu else (fus res1 res2, t) :: accu in let record r1 r2 = match r1,r2 with | RecLabel (l1,r1), RecLabel (l2,r2) -> (* assert (l1 = l2); *) RecLabel(l1, NLineProd.from_list (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 { nfv = IdSet.cup nf1.nfv nf2.nfv; na = Types.cap nf1.na nf2.na; nbasic = NLineBasic.from_list (double_fold basic (NLineBasic.get nf1.nbasic) (NLineBasic.get nf2.nbasic)); nprod = NLineProd.from_list (double_fold_prod prod nf1.nprod nf2.nprod); nxml = NLineProd.from_list (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_basic src t = NLineBasic.singleton (src, t) 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 let src_p = IdMap.constant SLeft xsp and src_q = IdMap.constant SRight xsq in let src = IdMap.merge_elem SRecompose src_p src_q in { nempty lab with nfv = xs; na = acc; nprod = single_prod src (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 let src_p = IdMap.constant SLeft xsp and src_q = IdMap.constant SRight xsq in let src = IdMap.merge_elem SRecompose src_p src_q in { nempty lab with nfv = xs; na = acc; nxml = single_prod src (nnode p xsp) (nnode q xsq) } let nrecord lab acc l p xs = match lab with | None -> assert false | Some label -> assert (label <= l); let src,lft,rgt = if l == label then SLeft, nnode p xs, ncany else SRight, ncany_abs, nnode (cons p.fv (record l p)) xs in let src = IdMap.constant src xs in { nempty lab with nfv = xs; na = acc; nrecord = RecLabel(label, single_prod src lft rgt) } let nconstr lab t = let aux l = NLineProd.from_list (List.map (fun (t1,t2) -> empty_res, nc t1,nc t2) 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 { nempty lab with na = t; nbasic = single_basic empty_res (Types.cap t any_basic); nprod = aux (Types.Product.normal t); nxml = aux (Types.Product.normal ~kind:`XML t); nrecord = record } let nany lab res = { nfv = IdMap.domain res; na = Types.any; nbasic = single_basic res any_basic; 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) as p) xs = let xs = IdSet.cap xs fv in (* if not (IdSet.equal xs fv) then (Format.fprintf Format.std_formatter "ERR: p=%a xs=%a fv=%a@." Print.print p Print.print_xs xs Print.print_xs fv; exit 1); *) 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 print_node_list ppf pl = List.iter (fun p -> Format.fprintf ppf "%a;" Node.dump p) pl let facto f t xs pl = List.fold_left (fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs))) IdSet.empty pl let normal f l t pl xs = let a = nconstr l t in let vs_var = facto Factorize.var t xs pl in let xs = IdSet.diff xs vs_var in let vs_var,a = if f then vs_var,a else IdSet.empty, List.fold_left (fun a x -> ncap a (ncapture l x)) a vs_var in let vs_nil = facto Factorize.nil t xs pl in let xs = IdSet.diff xs vs_nil in let vs_nil,a = if f then vs_nil,a else IdSet.empty, List.fold_left (fun a x -> ncap a (nconstant l x Sequence.nil_cst)) a vs_nil in vs_var,vs_nil, List.fold_left (fun a p -> ncap a (nnormal l (descr p) xs)) a pl let nnf facto lab t0 (pl,t,xs) = let t = if Types.subtype t t0 then t else Types.cap t t0 in (* let ppf = Format.std_formatter in Format.fprintf ppf "normal nnf=%a@." Nnf.print (pl,t,xs); *) normal facto lab t (NodeSet.get pl) xs (* let normal l t pl = let nf = normal l t pl in (match l with Some l -> Format.fprintf Format.std_formatter "normal(l=%a;t=%a;pl=%a)=%a@." Label.print (LabelPool.value l) Types.Print.print t print_node_list pl print nf | None -> Format.fprintf Format.std_formatter "normal(t=%a;pl=%a)=%a@." Types.Print.print t print_node_list pl print nf); nf *) end module Compile = struct type actions = | AIgnore of result | AKind of actions_kind and actions_kind = { basic: (Types.t * result) list; atoms: result Atoms.map; chars: result Chars.map; prod: result dispatch dispatch; xml: result dispatch dispatch; record: record option; } and record = | RecLabel of label * result dispatch dispatch | RecNolabel of result option * result option and 'a dispatch = | Dispatch of dispatcher * 'a array | TailCall of dispatcher | Ignore of 'a | Impossible and result = int * source array * int and source = | Catch | Const of Types.const | Stack of int | Left | Right | Nil | Recompose of int * int and return_code = Types.t * int * (* accepted type, arity *) int id_map option array and interface = [ `Result of int | `Switch of interface * interface | `None ] and dispatcher = { id : int; t : Types.t; pl : Normal.t array; label : label option; interface : interface; codes : return_code array; mutable actions : actions option; mutable printed : bool } let types_of_codes d = Array.map (fun (t,ar,_) -> t) d.codes 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 = basic; atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic); chars = Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic); 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) && (array_for_all ( f act.(0) ) act) then Ignore act.(0) else Dispatch (disp, 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 = State.ref "Patterns.cur_id" 0 (* TODO: save dispatchers ? *) module NfMap = Map.Make(Normal) module NfSet = Set.Make(Normal) module DispMap = Map.Make(Custom.Pair(Types)(Custom.Array(Normal))) (* Try with a hash-table ! *) let dispatchers = ref DispMap.empty let timer_disp = Stats.Timer.create "Patterns.dispatcher loop" 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 dispatcher t pl lab : dispatcher = try DispMap.find (t,pl) !dispatchers with Not_found -> 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 p = pl.(i) in let tp = p.Normal.na 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 v = p.Normal.nfv in 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 Stats.Timer.start timer_disp; let iface = if Types.is_empty t then `None else aux t 0 0 [] in Stats.Timer.stop timer_disp (); let res = { id = !cur_id; t = t; label = lab; pl = pl; interface = iface; codes = Array.of_list (List.rev !codes); actions = None; printed = false } in incr cur_id; dispatchers := DispMap.add (t,pl) res !dispatchers; res let find_code d a = let rec aux i = function | `Result code -> code | `None -> 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 | _ -> assert false in let final = Array.map aux pl in (find_code disp final, create_result final, ar) let conv_source_basic s = match s with | Normal.SCatch -> Catch | Normal.SConst c -> Const c | _ -> assert false let return_basic disp selected = let aux_final res = IdMap.map_to_list conv_source_basic res in return disp selected aux_final 0 let assoc v (vars,nils,l) ofs = try ofs - IdMap.assoc v l with Not_found -> if IdSet.mem vars v then -1 else if IdSet.mem nils v then -2 else assert false let conv_source_prod ofs1 ofs2 left right v s = match s with | Normal.SCatch -> Catch | Normal.SConst c -> Const c | Normal.SLeft -> (match assoc v left (ofs1 + ofs2) with | -1 -> Left | -2 -> Nil | i -> Stack i) | Normal.SRight -> (match assoc v right ofs2 with | -1 -> Right | -2 -> Nil | i -> Stack i) | Normal.SRecompose -> (match (assoc v left (ofs1 + ofs2), assoc v right ofs2) with | (-1,-1) -> Catch | (l,r) -> Recompose (l,r)) module TypeList = SortedList.Make(Types) let dispatch_basic disp : (Types.t * result) list = (* TODO: try other algo, using disp.codes .... *) let pl = Array.map (fun p -> p.Normal.nbasic) disp.pl in let tests = let accu = ref [] in let aux i (res,x) = accu := (x, [i,res]) :: !accu in Array.iteri (fun i -> Normal.NLineBasic.iter (aux i)) 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.create (Array.length 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 first_lab pl = let aux l (req,_) = min l (Normal.Nnf.first_label req) in let lab = Array.fold_left (List.fold_left aux) LabelPool.dummy_max pl in if lab == LabelPool.dummy_max then None else Some lab let get_tests facto pl f t d post = let pl = Array.map (List.map f) pl in let lab = first_lab pl in let pl = Array.map (List.map (fun (x,info) -> Normal.nnf facto lab t x,info)) pl in (* Collect all subrequests *) let aux reqs ((_,_,req),_) = NfSet.add req 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 *) let disp = dispatcher t reqs lab in (* Build continuation *) let result (t,ar,m) = let get a ((vars,nils,req),info) = match m.(NfMap.find req idx) with Some res -> ((vars,nils,res),info)::a | _ -> a in let pl = Array.map (List.fold_left get []) pl in d t ar pl in let res = Array.map result disp.codes in post (disp,res) type 'a rhs = Match of (id * int) list * 'a | Fail let make_branches t brs = let t0 = ref t in let aux (p,e) = let xs = fv p in let nnf = (Normal.NodeSet.singleton p, !t0, xs) in t0 := Types.diff !t0 (Types.descr (accept p)); [(nnf, (xs, e))] in let res _ _ pl = let aux r = function | [(([],[],res), (xs,e))] -> assert (r == Fail); let m = List.map (fun x -> (x,IdMap.assoc x res)) xs in Match (m,e) | [] -> r | _ -> assert false in Array.fold_left aux Fail pl in let pl = Array.map aux (Array.of_list brs) in get_tests false pl (fun x -> x) t res (fun x -> x) let rec dispatch_prod ?(kind=`Normal) disp = let extr = match kind with | `Normal -> fun p -> Normal.NLineProd.get p.Normal.nprod | `XML -> fun p -> Normal.NLineProd.get p.Normal.nxml in let t = Types.Product.get ~kind disp.t in dispatch_prod0 disp t (Array.map extr disp.pl) and 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)) = IdMap.mapi_to_list (conv_source_prod ar1 ar2 ret1 ret2) res in return disp pl aux_final (ar1 + ar2) let dispatch_record disp : 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) disp.pl in Some (return disp pl (IdMap.map_to_list conv_source_basic) 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) disp.pl in Some (return disp pl (IdMap.map_to_list conv_source_basic) 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.get l | _ -> assert false) disp.pl in Some (RecLabel (lab,dispatch_prod0 disp t pl)) let actions disp = match disp.actions with | Some a -> a | None -> let a = combine_kind (dispatch_basic disp) (dispatch_prod disp) (dispatch_prod ~kind:`XML disp) (dispatch_record disp) in disp.actions <- Some a; a let to_print = ref [] module DSET = Set.Make (struct type t = int let compare (x:t) (y:t) = x - y end) let printed = ref DSET.empty let queue d = if not d.printed then ( d.printed <- true; to_print := d :: !to_print ) let rec print_source lhs ppf = function | Catch -> Format.fprintf ppf "v" | Const c -> Types.Print.print_const ppf c | Nil -> Format.fprintf ppf "`nil" | Left -> Format.fprintf ppf "v1" | Right -> Format.fprintf ppf "v2" | Stack i -> Format.fprintf ppf "%s" (List.nth lhs (i-1)) | Recompose (i,j) -> Format.fprintf ppf "(%s,%s)" (match i with (-1) -> "v1" | (-2) -> "nil" | i -> List.nth lhs (i-1)) (match j with (-1) -> "v2" | (-2) -> "nil" | j -> List.nth lhs (j-1)) let print_result lhs ppf = Array.iteri (fun i s -> if i > 0 then Format.fprintf ppf ","; print_source lhs ppf s; ) let print_ret lhs ppf (code,ret,ar) = Format.fprintf ppf "$%i{%i}" code ar; if Array.length ret <> 0 then Format.fprintf ppf "(%a)" (print_result lhs) ret let print_ret_opt ppf = function | None -> Format.fprintf ppf "*" | Some r -> print_ret [] ppf r let gen_lhs (code,prefix,d) = let arity = match d.codes.(code) with (_,a,_) -> a in let r = ref [] in for i = 0 to arity - 1 do r := Format.sprintf "%s%i" prefix i :: !r done; !r let print_kind ppf actions = let print_lhs ppf (code,lhs) = Format.fprintf ppf "$%i(" code; let rec aux = function | [] -> () | [x] -> Format.fprintf ppf "%s" x | x::r -> Format.fprintf ppf "%s,x" x; aux r in aux lhs; Format.fprintf ppf ")" in let print_basic (t,ret) = Format.fprintf ppf " | %a -> %a@\n" Types.Print.print t (print_ret []) ret in let print_prod2 lhs = function | Impossible -> assert false | Ignore r -> Format.fprintf ppf "%a\n" (print_ret lhs) r | TailCall d -> queue d; Format.fprintf ppf "disp_%i v2@\n" d.id | Dispatch (d, branches) -> queue d; Format.fprintf ppf "@\n match disp_%i v2 with@\n" d.id; Array.iteri (fun code r -> let rhs = gen_lhs (code,"r",d) in Format.fprintf ppf " | %a -> %a@\n" print_lhs (code,rhs) (print_ret (rhs@lhs)) r; ) branches in let print_prod prefix ppf = function | Impossible -> () | Ignore d2 -> Format.fprintf ppf " | %s(v1,v2) -> " prefix; print_prod2 [] d2 | TailCall d -> queue d; Format.fprintf ppf " | %s(v1,v2) -> disp_%i v1@\n" prefix d.id | Dispatch (d,branches) -> queue d; Format.fprintf ppf " | %s(v1,v2) -> @\n" prefix; Format.fprintf ppf " match disp_%i v1 with@\n" d.id; Array.iteri (fun code d2 -> let lhs = gen_lhs (code, "l", d) in Format.fprintf ppf " | %a -> " print_lhs (code,lhs); print_prod2 lhs d2; ) branches in let rec print_record_opt ppf = function | None -> () | Some (RecLabel (l,d)) -> let l = LabelPool.value l in print_prod ("record:"^(Label.to_string l)) ppf d | Some (RecNolabel (r1,r2)) -> Format.fprintf ppf " | Record -> @\n"; Format.fprintf ppf " SomeField:%a;NoField:%a@\n" print_ret_opt r1 print_ret_opt r2 in List.iter print_basic actions.basic; print_prod "" ppf actions.prod; print_prod "XML" ppf actions.xml; print_record_opt ppf actions.record let print_actions ppf = function | AKind k -> print_kind ppf k | AIgnore r -> Format.fprintf ppf "v -> %a@\n" (print_ret []) r let print_dispatcher ppf d = (* Format.fprintf ppf "Dispatcher %i accepts [%a]@\n" d.id Types.Print.print (Types.normalize d.t); let print_code code (t, arity, m) = Format.fprintf ppf " Returns $%i(arity=%i) for [%a]" code arity Types.Print.print (Types.normalize t); (* List.iter (fun (i,b) -> Format.fprintf ppf "[%i:" i; List.iter (fun (v,i) -> Format.fprintf ppf "%s=>%i;" v i) b; Format.fprintf ppf "]" ) m; *) Format.fprintf ppf "@\n"; in Array.iteri print_code d.codes; *) Format.fprintf ppf "let disp_%i = function@\n" d.id; print_actions ppf (actions d); Format.fprintf ppf "====================================@\n" let rec print_dispatchers ppf = match !to_print with | [] -> () | d :: rem -> to_print := rem; print_dispatcher ppf d; print_dispatchers ppf let show ppf t pl lab = let disp = dispatcher t pl lab in queue disp; print_dispatchers ppf let debug_compile ppf t pl = let t = Types.descr t in let lab = List.fold_left (fun l p -> min l (first_label (descr p))) (Types.Record.first_label t) pl in let lab = if lab == LabelPool.dummy_max then None else Some lab in let pl = Array.of_list (List.map (fun p -> let n = Normal.nnf false lab t ([p],t,fv p) in match n with | [],[],x -> x | _ -> assert false ) pl) in show ppf t pl lab; (* Format.fprintf ppf "# compiled dispatchers: %i@\n" !cur_id *) end (* New compilation procedure *) module Compile2 = struct let any_or_abs = Types.Record.any_or_absent module PatList = SortedList.Make(struct include Custom.Dummy include Pat end) module TypesFv = Custom.Pair(Types)(IdSet) module Req = PatList.MakeMap(TypesFv) (* Invariant for (p |-> (t,X)): i) t != Empty ii) X \subset fv(p) *) let empty_reqs = PatList.Map.empty let merge_reqs = PatList.Map.merge (fun (t1,xs1) (t2,xs2) -> Types.cup t1 t2, IdSet.cup xs1 xs2) let add_req reqs p t xs = merge_reqs reqs (PatList.Map.singleton p (t,xs)) module NodeSet = Set.Make(Node) let pi1 ~kind t = Types.Product.pi1 (Types.Product.get ~kind t) let pi2 ~kind t = Types.Product.pi2 (Types.Product.get ~kind t) module TargExpr = struct type t = source IdMap.map and source = | SrcCapture | SrcLeft | SrcRight | SrcCst of Types.const | SrcPair of source * source | SrcFetchLeft of int | SrcFetchRight of int | SrcLocal of int (* let rec equal_src s1 s2 = (s1 == s2) || match (s1,s2) with | SrcCst c1, SrcCst c2 -> Types.Const.equal c1 c2 | SrcPair (s1,ss1), SrcPair (s2,ss2) -> equal_src s1 s2 && equal_src ss1 ss2 | SrcFetchLeft i, SrcFetchLeft j | SrcFetchRight i, SrcFetchRight j | SrcLocal i, SrcLocal j when i == j -> true | _ -> false let equal = IdMap.equal equal_src *) type push = PushConst of Types.const | PushField | PushCapture let capture x = IdMap.singleton x SrcCapture let captures xs = IdMap.constant SrcCapture xs let cst x c = IdMap.singleton x (SrcCst c) let constants cs = IdMap.map (fun c -> SrcCst c) cs let fetch_left f = SrcFetchLeft f let fetch_right f = SrcFetchRight f let fetch_local ofs i = SrcLocal (ofs + i) let empty = IdMap.empty let merge e1 e2 = IdMap.merge (fun s1 s2 -> SrcPair (s1,s2)) e1 e2 let captures_left xs = IdMap.constant SrcLeft xs let captures_right xs = IdMap.constant SrcRight xs let rec print_src ppf = function | SrcCapture -> Format.fprintf ppf "v" | SrcLeft -> Format.fprintf ppf "v1" | SrcRight -> Format.fprintf ppf "v2" | SrcCst c -> Types.Print.print_const ppf c | SrcPair (s1,s2) -> Format.fprintf ppf "(%a,%a)" print_src s1 print_src s2 | SrcFetchLeft x -> Format.fprintf ppf "x%i" x | SrcFetchRight x -> Format.fprintf ppf "y%i" x | SrcLocal x -> Format.fprintf ppf "local(%i)" x let print ppf r = Format.fprintf ppf "{ "; List.iter (fun (x,s) -> Format.fprintf ppf "%a:=%a " U.print (Id.value x) print_src s) (IdMap.get r); Format.fprintf ppf "}"; end module Derivation = struct type t = | TSucceed | TFail | TConstr of Types.t * Types.t | TCapt of TargExpr.t * t | TAlt of descr * Types.t * t * t | TConj of Types.t * fv * t * t | TTimes of Types.pair_kind * int * descr * Types.t * fv * node * node | TRecord of int * descr * Types.t * fv * label * node (* let rec same p1 p2 = (p1 == p2) || match (p1,p2) with | TConstr (t1,s1), TConstr (t2,s2) -> Types.equiv s1 s2 && Types.equiv (Types.cap t1 s1) (Types.cap t2 s2) | TCapt (pr1,p1), TCapt (pr2,p2) -> TargExpr.equal pr1 pr2 && same p1 p2 | TAlt (p1,_,a1,b1), TAlt (p2,_,a2,b2) -> (p1 == p2) && (same a1 a2) && (same b1 b2) | TConj (_,_,a1,b1), TConj (_,_,a2,b2) -> same a1 a2 && same b1 b2 | TTimes (k1,uid1,p1,t1,xs1,a1,b1), TTimes (k2,uid2,p2,t2,xs2,a2,b2) -> assert false | TRecord (uid1,_,t1,_,_,_), TRecord (uid2,_,t2,_,_,_) -> (uid1 == uid2) && (Types.equiv t1 t2) | _ -> false *) (* TODO: allocate the stack locations by sorting the ids (to allow ({ l = (x,y) } | (x:=1)&(y:=2))) *) let push_csts pushes locals = let push x = pushes := x :: !pushes; let loc = TargExpr.SrcLocal !locals in incr locals; loc in let reloc = function | TargExpr.SrcCst c -> push (TargExpr.PushConst c) | TargExpr.SrcLeft -> push TargExpr.PushField | TargExpr.SrcCapture -> push TargExpr.PushCapture | TargExpr.SrcLocal _ as s -> s | _ -> assert false in let rec aux = function | TCapt (pr,p) -> TCapt (IdMap.map reloc pr, p) | TAlt (p,a1,p1,p2) -> TAlt (p,a1,aux p1,aux p2) | TConj (a1,fv1,p1,p2) -> TConj (a1,fv1,aux p1, aux p2) | p -> p in aux let capt pr p = if IdMap.is_empty pr then p else match p with | TCapt (pr2,p) -> TCapt (TargExpr.merge pr pr2,p) | TFail -> TFail | p -> TCapt (pr,p) let success pr = capt pr TSucceed let success_if_present pr = capt pr (TConstr (Types.any,any_or_abs)) let rec conj a1 fv1 r1 r2 = match (r1,r2) with | TSucceed,r | r,TSucceed -> r | TFail,r | r,TFail -> TFail | TCapt (f,r1), r2 | r2, TCapt (f,r1) -> capt f (conj a1 fv1 r1 r2) | r1,r2 -> TConj (a1,fv1,r1,r2) let constrain a t = if Types.disjoint a t then TFail else if Types.subtype t a then ( (* Format.fprintf Format.std_formatter "Optimize constraint -> Succeed a=%a t=%a@." Types.Print.print a Types.Print.print t; *) TSucceed ) else TConstr (a,t) let alt p a1 r1 r2 = match (r1,r2) with | TFail,r | r,TFail -> r | TSucceed, _ -> assert false (* Note: this cannot happen because if the lhs succeeds, then the rhs must fail (it is evaluated under the assumption that the lhs fails, so the static assumption is empty in this case). *) | r1,r2 -> TAlt (p,a1,r1,r2) let rec print ppf = function | TSucceed -> Format.fprintf ppf "Succeed" | TFail -> Format.fprintf ppf "Fail" | TConstr (t,s) -> Format.fprintf ppf "%a/%a" Types.Print.print t Types.Print.print s | TCapt (pr,r) -> Format.fprintf ppf "{%a}(%a)" TargExpr.print pr print r | TAlt (_,_,l,r) -> Format.fprintf ppf "(%a | %a)" print l print r | TConj (_,_,l,r) -> Format.fprintf ppf "(%a & %a)" print l print r | TRecord (_,_,t,xs,l,q) -> Format.fprintf ppf "" Types.Print.print t Print.print_xs xs Label.print (LabelPool.value l) Print.print q.descr | TTimes (kind,_,_,t,xs,q1,q2) -> Format.fprintf ppf "" Types.Print.print t Print.print_xs xs Print.print q1.descr Print.print q2.descr exception NotAResult let get_result = function | TSucceed -> Some TargExpr.empty | TCapt (r,TSucceed) -> Some r | TFail -> None | r -> raise NotAResult (* Format.fprintf Format.std_formatter "ERR: %a@." print r; *) let print_result ppf = function | None -> Format.fprintf ppf "Fail" | Some r -> TargExpr.print ppf r let uid = ref 0 let rec mk ((a,fv,d) as p) = match d with | Constr t -> TConstr (t, any_or_abs) | Cup ((a1,_,_) as p1,p2) -> TAlt (p, a1,mk p1, mk p2) | Cap ((a1,fv1,_) as p1,p2) -> TConj (a1,fv1,mk p1,mk p2) | Capture x -> success_if_present (TargExpr.capture x) | Constant (x,c) -> success_if_present (TargExpr.cst x c) | Times (q1,q2) -> TTimes (`Normal,(incr uid; !uid), p, any_or_abs,fv,q1,q2) | Xml (q1,q2) -> TTimes (`XML,(incr uid; !uid), p,any_or_abs,fv,q1,q2) | Record (l,q) -> TRecord ((incr uid; !uid),p, any_or_abs,fv,l,q) | Dummy -> assert false let approx_var p t xs f = let vs = Factorize.var p t xs in let xs = IdSet.diff xs vs in let pr = f vs in (pr,xs) let approx_cst p t xs f = let vs = Factorize.cst p t xs in let xs = IdSet.diff xs (IdMap.domain vs) in let pr = f vs in (pr,xs) let factorize ((a,_,_) as p) t xs f = if Types.disjoint a t then TFail else (* let () = Format.fprintf Format.std_formatter "Factorize p=%a t=%a a=%a@." Print.print p Types.Print.print t Types.Print.print a in *) let pr,xs = approx_var p t xs TargExpr.captures in let pr',xs = approx_cst p t xs TargExpr.constants in let pr = TargExpr.merge pr pr' in capt pr (if (IdSet.is_empty xs) then constrain a t else f xs) let rec optimize t xs = function | TCapt (pr,p) -> let pr = IdMap.restrict pr xs in capt pr (optimize t (IdSet.diff xs (IdMap.domain pr)) p) | TAlt (p,a1,p1,p2) -> factorize p t xs (fun xs -> alt p a1 (optimize t xs p1) (optimize (Types.diff t a1) xs p2)) | TConj (a1,fv1,p1,p2) -> (* We don't factorize above a & pattern eagerly, because if factorization would occur, it would also occur below and be lifted by the conj function, which produces the same effect. *) conj a1 fv1 (optimize t (IdSet.cap xs fv1) p1) (optimize (Types.cap t a1) (IdSet.diff xs fv1) p2) | TConstr (a,_) -> constrain a t | TTimes (kind,uid, p,_,_,q1,q2) -> factorize p t xs (fun xs -> TTimes (kind,uid, p,t,xs,q1,q2)) | TRecord (uid,p,_,_,l,q) -> factorize p t xs (fun xs -> TRecord (uid,p,t,xs,l,q)) | TSucceed -> if Types.is_empty t then TFail else TSucceed | TFail -> TFail (* let optimize t xs p = let p' = optimize t xs p in Format.fprintf Format.std_formatter "Optimize %a // (t=%a) ===> %a@." print p Types.Print.print t print p'; p' *) let fold f accu = function | TCapt (_,p) -> f accu p | TAlt (_,_,p1,p2) | TConj (_,_,p1,p2) -> f (f accu p1) p2 | _ -> accu let iter f = function | TCapt (_,p) -> f p | TAlt (_,_,p1,p2) | TConj (_,_,p1,p2) -> f p1; f p2 | _ -> () let map f = function | TCapt (pr,p) -> capt pr (f p) | TAlt (p,a1,p1,p2) -> alt p a1 (f p1) (f p2) | TConj (a1,fv1,p1,p2) -> conj a1 fv1 (f p1) (f p2) | x -> x let iter_constr f = let rec aux = function | TConstr (t,s) -> f (t,s) | p -> iter aux p in aux let iter_times k f = let rec aux = function | TTimes (kind,uid,_,t,xs,q1,q2) when k == kind -> f (uid,t,xs,q1,q2) | p -> iter aux p in aux let iter_records f = let rec aux = function | TRecord (uid,_,t,xs,l,q) -> f (uid,t,xs,l,q) | p -> iter aux p in aux let iter_field l f = let rec aux = function | TRecord (uid,_,t,xs,l',q) when l == l' -> f (uid,t,xs,q) | p -> iter aux p in aux let opt_all t0 = List.map (fun (p,t,xs) -> if Types.subtype t t0 then (p,t,xs) else let t = Types.cap t t0 in (optimize t xs p, t, xs)) let get_results reqs = List.map (fun (p,_,_) -> get_result p) reqs let iter_all f g reqs = List.iter (fun (p,_,_) -> f g p) reqs let get_all pi get sel extract iter side reqs = let extra = ref [] in let res = ref empty_reqs in let aux3 s1 t12 = let t1 = sel t12 in if not ((Types.subtype s1 t1) || (Types.disjoint s1 t1)) then res := add_req !res (constr t1) s1 IdSet.empty in let aux2 (t,s) = List.iter (aux3 (pi s)) (get (Types.cap t s)) in let aux z = let uid,t,xs,q = extract z in let xs = IdSet.cap xs q.fv and p = q.descr and t = pi t in (* let p = cap p (constr Types.any) in *) let pr,xs = approx_var p t xs side in let pr',xs = approx_cst p t xs TargExpr.constants in let pr = TargExpr.merge pr pr' in extra := (uid,pr)::!extra; if not ((IdSet.is_empty xs) && (Types.subtype t (Types.descr q.accept))) then res := add_req !res p t xs in iter_all iter aux reqs; iter_all iter_constr aux2 reqs; !extra,!res let prod_all k side pi sel selq reqs = get_all pi (fun t -> Types.Product.clean_normal (Types.Product.normal ~kind:k t)) sel (fun (uid,t,xs,q1,q2) -> uid,t,xs,selq (q1,q2)) (iter_times k) side reqs let all_labels reqs = let res = ref LabelSet.empty in let aux2 (t,_) = res := LabelSet.cup !res (Types.Record.all_labels t) in let aux (_,_,_,l,_) = res := LabelSet.add l !res in iter_all iter_records aux reqs; iter_all iter_constr aux2 reqs; LabelSet.get !res let record_all l reqs = let extra,res = get_all (Types.Record.pi l) (fun t -> Types.Record.split_normal t l) fst (fun z -> z) (iter_field l) TargExpr.captures_left reqs in extra,res let rec find_binds q reqs binds fetch = match (reqs,binds) with | (p2,_)::_, Some b::_ when Pat.equal q.descr p2 -> IdMap.map fetch b | _::reqs, _::binds -> find_binds q reqs binds fetch | _ -> raise Not_found let find_binds q reqs binds fetch uid extra = let r = List.assq uid extra in try TargExpr.merge r (find_binds q (PatList.Map.get reqs) binds fetch) with Not_found -> r let pair swap l r = let (l,r) = swap (l,r) in TargExpr.SrcPair (l,r) let rec set_times k swap swap' extra1 extra2 reqs1 reqs2 binds1 binds2 = let rec aux = function | TTimes (kind,uid,_,t,xs,q1,q2) when k == kind-> let (q1,q2) = swap (q1,q2) in let r1 = find_binds q1 reqs1 binds1 TargExpr.fetch_left uid extra1 and r2 = find_binds q2 reqs2 binds2 TargExpr.fetch_right uid extra2 in let r = IdMap.merge (pair swap') r1 r2 in success (IdMap.restrict r xs) | x -> map aux x in aux let rec set_field l locals extra1 reqs1 binds1 = let rec aux = function | TRecord (uid,_,t,xs,l',q) when l == l' -> let r = find_binds q reqs1 binds1 (TargExpr.fetch_local locals) uid extra1 in success (IdMap.restrict r xs) | x -> map aux x in aux let mkopt p t xs = optimize t xs (mk p) let demo ppf ((_,fv,_) as p) t = let p = mk p in (* Format.fprintf ppf "%a@." print p; *) let p = optimize t fv p in Format.fprintf ppf "%a@." print p; Format.fprintf ppf "@.Fields:@."; iter_records (fun (_,t,xs,l,q) -> Format.fprintf ppf "(%a=%a) / %a@." print_lab l Print.print q.descr Types.Print.print (Types.Record.project_opt t l) ) p end type output = Types.t * int * int id_map option list (* Obtained type, arity, bindings *) type rescode = | RFail | RCode of int | RSwitch of rescode * rescode | RIgnore of rescode type result = int * TargExpr.source array type actions = | AResult of result | AKind of actions_kind and actions_kind = { basic: (Types.t * result) list; atoms: result Atoms.map; chars: result Chars.map; prod: actions_prod; xml: actions_prod; record: actions_record; } and actions_record = | RecordLabel of label * dispatcher * record_tr array | RecordLabelSkip of label * record_tr | RecordResult of result | RecordMore of result * result (* nomore, more *) | RecordImpossible and record_tr = (TargExpr.push list * actions_record) Lazy.t and actions_prod = | LeftRight of result dispatch dispatch | RightLeft of result dispatch dispatch | Impossible and 'a dispatch = | Dispatch of dispatcher * 'a array | TailCall of dispatcher | Ignore of 'a and dispatcher = { id : int; outputs : output array; rescode : rescode; reqs : (Derivation.t * Types.t * fv) list; (* initial derivation; assumption; variables *) assumpt : Types.t; mutable actions : actions option; } let print_queue = Queue.create () let to_print d = Queue.push d print_queue let print_binds ppf binds = List.iter (function | None -> Format.fprintf ppf "* " | Some m -> Format.fprintf ppf "( "; IdMap.iteri (fun x i -> Format.fprintf Format.std_formatter "%a:%i " Ident.print x i) m; Format.fprintf ppf ") ";) binds let print_reqs ppf reqs = List.iter (fun (p,t,xs) -> Format.fprintf ppf "%a. t=%a. xs=%a@." Derivation.print p Types.Print.print t Print.print_xs xs) reqs let print ppf r = Format.fprintf ppf "disp_%i:@." r.id; Array.iteri (fun i (t,ar,binds) -> Format.fprintf ppf "[%i]{%i}{%a} @." i ar print_binds binds (*Types.Print.print t*) ) r.outputs; print_reqs ppf r.reqs; () let print_result ppf (code,a) = Format.fprintf ppf "$%i(" code; Array.iteri (fun i x -> Format.fprintf ppf "%s%a" (if i > 0 then "," else "") TargExpr.print_src x) a; Format.fprintf ppf ")" let print_basic_disp ppf l = List.iter (fun (t,res) -> Format.fprintf ppf " | %a -> %a@." Types.Print.print t print_result res ) l let arity d code = let (_,n,_) = d.outputs.(code) in n let print_lhs ppf (s,n) = if n > 0 then ( Format.fprintf ppf "(%s0" s; for i = 1 to n - 1 do Format.fprintf ppf ",%s%i" s i done; Format.fprintf ppf ")" ) let print_prod2 ppf = function | Dispatch (d, branches) -> to_print d; Format.fprintf ppf " match disp_%i v2 with@\n" d.id; Array.iteri (fun code res -> Format.fprintf ppf " | $%i%a -> %a@." code print_lhs ("y", arity d code) print_result res) branches | Ignore res -> Format.fprintf ppf " %a@." print_result res | TailCall d -> to_print d; Format.fprintf ppf " disp_%i v2@\n" d.id let print_prod1 ppf = function | Dispatch (d,branches) -> to_print d; Format.fprintf ppf " match disp_%i v1 with@." d.id; Array.iteri (fun code d2 -> Format.fprintf ppf " | $%i%a -> %a@." code print_lhs ("x", arity d code) print_prod2 d2) branches | Ignore d2 -> Format.fprintf ppf " %a@." print_prod2 d2 | TailCall d -> to_print d; Format.fprintf ppf " disp_%i v1@\n" d.id let print_prod pr ppf = function | LeftRight d -> Format.fprintf ppf " | %s(v1,v2) -> @.%a" pr print_prod1 d | RightLeft d -> Format.fprintf ppf " | %s(v2,v1) -> @.%a" pr print_prod1 d | Impossible -> () let print_pushes ppf l = List.iter (function | TargExpr.PushConst c -> Format.fprintf ppf "{push %a}" Types.Print.print_const c | TargExpr.PushField -> Format.fprintf ppf "{push field}" | TargExpr.PushCapture -> Format.fprintf ppf "{push record}" ) l let rec print_record_tr ppf (pushes,x) = Format.fprintf ppf "%a%a" print_pushes pushes print_field x and print_field ppf = function | RecordImpossible -> Format.fprintf ppf "#" | RecordLabel (l,d,cts) -> to_print d; Format.fprintf ppf "(label:%a,disp_%i" print_lab l d.id; Array.iteri (fun i x -> Format.fprintf ppf ";%i->%a" i print_record_tr (Lazy.force x)) cts; Format.fprintf ppf ")" | RecordLabelSkip (l,x) -> Format.fprintf ppf "(label:%a;%a)" print_lab l print_record_tr (Lazy.force x) | RecordMore (nomore,more) -> Format.fprintf ppf "[nomore:%a;more:%a]" print_result nomore print_result more | RecordResult res -> Format.fprintf ppf "[%a]" print_result res let print_record ppf r = Format.fprintf ppf "Record:%a@." print_field r let rec print_rescode ppf = function | RFail -> Format.fprintf ppf "Fail" | RCode i -> Format.fprintf ppf "(%i)" i | RSwitch (a,b) -> Format.fprintf ppf "S(%a,%a)" print_rescode a print_rescode b | RIgnore a -> Format.fprintf ppf "I(%a)" print_rescode a let rec find_code bl rc = match (bl,rc) with | Some _::bl,RSwitch (rc,_) | None::bl,RSwitch (_,rc) -> find_code bl rc | _::bl,RIgnore rc -> find_code bl rc | [], RCode i -> i | _ -> (-1) (* assert false *) (* let find_code bl rc = Format.fprintf Format.std_formatter "%a@." print_rescode rc; List.iter (fun x -> Format.fprintf Format.std_formatter "%b " (x != None)) bl; Format.fprintf Format.std_formatter "@."; find_code bl rc *) let alloc pos fv = let i = ref (pos - 1) in let r = IdMap.map_from_slist (fun x -> incr i; !i) fv in (r,!i + 1) let disp_id = ref 0 let mk reqs = let nb = ref (-1) in let codes = ref [] in let rec aux t0 ar binds l = if Types.is_empty t0 then RFail else match l with | [] -> (* Printf.printf "nb=%i " !nb; flush stdout; *) incr nb; codes := (t0,ar,List.rev binds) :: !codes; RCode !nb | ((a,_,_),(t,xs)) :: rem -> if Types.disjoint t t0 then RIgnore (aux t0 ar (None::binds) rem) else let (alc,ar') = alloc ar xs in RSwitch (aux (Types.diff t0 (Types.diff t a)) ar' (Some alc::binds) rem, aux (Types.diff t0 (Types.cap t a)) ar (None::binds) rem) in let reqs = PatList.Map.get reqs in (* Printf.printf "reqs:%i " (List.length reqs); flush stdout; *) let t0 = List.fold_left (fun accu (_,(t,_)) -> Types.cup accu t) Types.empty reqs in (* let t0 = any_or_abs in *) let rc = aux t0 0 [] reqs in let reqs = List.map (fun (p,(t,xs)) -> (Derivation.mkopt p t xs, t, xs)) reqs in let os = Array.of_list (List.rev !codes) in { id = (incr disp_id; !disp_id); outputs = os; rescode = rc; reqs = reqs; assumpt = t0; actions = None } module ReqTable = Hashtbl.Make(Req) let disps = ReqTable.create 1023 let mk reqs = try ReqTable.find disps reqs with Not_found -> (* print_endline "mk: START"; flush stdout; List.iter (fun (p,(t,xs)) -> Format.fprintf Format.std_formatter "%a. t=%a. xs=%a@." Print.print p Types.Print.print t Print.print_xs xs ) (PatList.Map.get reqs); *) let d = mk reqs in (* print_endline "mk: STOP"; flush stdout; *) ReqTable.add disps reqs d; d let mk_res r reqs = (* Format.fprintf Format.std_formatter "mk_res t=%a@." Types.Print.print t0; List.iter (fun (p,_,_) -> Format.fprintf Format.std_formatter "%a@." Derivation.print p) reqs; *) let res = Derivation.get_results reqs in let code = find_code res r.rescode in if (code < 0) then (code,[||]) else let (_,ar,fill) = r.outputs.(code) in let o = Array.make ar (TargExpr.SrcFetchLeft (-1)) in List.iter2 (fun res fill -> match (res,fill) with | Some res, Some fill -> (* Format.fprintf Format.std_formatter "Res=%a@." TargExpr.print res; IdMap.iteri (fun x i -> Format.fprintf Format.std_formatter "%a->%i@." Ident.print x i) fill; let fill = IdMap.restrict fill (IdMap.domain res) in *) IdMap.collide (fun i r -> o.(i) <- r) fill res | None, None -> () | _ -> assert false) res fill; (code,o) let basic_disp r = let t0 = Types.cap r.assumpt Types.non_constructed_or_absent in if Types.is_empty t0 then [] else let reqs = Derivation.opt_all t0 r.reqs in let qs = ref [] in let aux x = qs := x::!qs in Derivation.iter_all Derivation.iter_constr aux reqs; let part = Types.cond_partition t0 !qs in List.map (fun t -> (t, mk_res r (Derivation.opt_all t reqs))) part let call_disp reqs f = if PatList.Map.is_empty reqs then Ignore (f (any_or_abs,0,[])) else let d = mk reqs in Dispatch (d, Array.map f d.outputs) let check_tail_call2 d brs = let chk i = function | TargExpr.SrcFetchRight j when i = j -> () | _ -> raise Exit in let aux code (code',a) = let n = arity d code in if (code != code') || (n != Array.length a) then raise Exit; Array.iteri chk a in try Array.iteri aux brs; true with Exit -> false let opt_tail_call2 = function | Dispatch (d, brs) when check_tail_call2 d brs -> TailCall d | d -> d let check_tail_call1 d brs = let chk i = function | TargExpr.SrcFetchLeft j when i = j -> () | _ -> raise Exit in let aux code = function | Ignore (code',a) -> let n = arity d code in if (code != code') || (n != Array.length a) then raise Exit; Array.iteri chk a | _ -> raise Exit in try Array.iteri aux brs; true with Exit -> false let opt_tail_call1 = function | Dispatch (d, brs) when check_tail_call1 d brs -> TailCall d | d -> d let restr1 c t0 t1 = Types.cap t0 (c (Types.cons t1) Types.any_node) let restr2 c t0 t2 = Types.cap t0 (c Types.any_node (Types.cons t2)) let swap (x,y) = (y,x) let noswap (x,y) = (x,y) let times_disp direction k r = let c = match k with `XML -> Types.xml | `Normal -> Types.times in let pi1,pi2,fst,fst',snd,snd',restr1,restr2,swap,swap' = match direction with | `LeftRight -> pi1 ~kind:k,pi2 ~kind:k, fst,fst,snd,snd,restr1 c,restr2 c,noswap,noswap | `RightLeft -> pi2 ~kind:k,pi1 ~kind:k, snd,snd,fst,fst,restr2 c,restr1 c,swap,swap in let t0 = Types.cap r.assumpt (Types.Product.any_of k) in if Types.is_empty t0 then Impossible else let reqs = Derivation.opt_all t0 r.reqs in let extra1,reqs1 = Derivation.prod_all k TargExpr.captures_left pi1 fst fst' reqs in let second (t1,ar1,binds1) = (* Printf.printf "second\n"; flush stdout; Format.fprintf Format.std_formatter "Restrict t1=%a@." Types.Print.print t1;*) let t0 = restr1 t0 t1 in let reqs = Derivation.opt_all t0 reqs in let extra2,reqs2 = Derivation.prod_all k TargExpr.captures_right pi2 snd snd' reqs in let final (t2,ar2,binds2) = let t0 = restr2 t0 t2 in let reqs = Derivation.opt_all t0 reqs in let aux = Derivation.set_times k swap swap' extra1 extra2 reqs1 reqs2 binds1 binds2 in let reqs = List.map (fun (p,t,xs) -> (aux p,t,xs)) reqs in mk_res r reqs in opt_tail_call2 (call_disp reqs2 final) in let r = opt_tail_call1 (call_disp reqs1 second) in match direction with | `LeftRight -> LeftRight r | `RightLeft -> RightLeft r (* let same_all reqs1 reqs2 = let aux (p1,t1,xs1) (p2,t2,xs2) = Derivation.same p1 p2 in List.for_all2 aux reqs1 reqs2 *) let record_disp r = let t0 = Types.cap r.assumpt Types.Record.any in let reqs = Derivation.opt_all t0 r.reqs in let all_labs = Derivation.all_labels reqs in (* TODO: memoize the field function *) let rec field t0 reqs locals labs = if Types.is_empty t0 then RecordImpossible else try RecordResult (mk_res r reqs) with Derivation.NotAResult -> field' t0 reqs locals labs and field' t0 reqs locals = function | [] -> (* TODO: distinguish between More / No more fields *) let fs = List.map (fun x -> x,Types.Record.any_or_absent_node) all_labs in let t = Types.record' (false, LabelMap.from_list_disj fs) in let nomore = mk_res r (Derivation.opt_all (Types.cap t0 t) reqs) and more = mk_res r (Derivation.opt_all (Types.diff t0 t) reqs) in RecordMore (nomore,more) | l::labs -> let cont t0 locals reqs = let locals = ref locals in let pushes = ref [] in let aux = Derivation.push_csts pushes locals in let reqs = List.map (fun (p,t,xs) -> (aux p,t,xs)) reqs in (List.rev !pushes, field t0 reqs !locals labs) in let extra1,reqs1 = Derivation.record_all l reqs in let contin (t1,ar1,binds1) = let t0 = Types.cap t0 (Types.record l (Types.cons t1)) in let reqs = Derivation.opt_all t0 reqs in let aux = Derivation.set_field l locals extra1 reqs1 binds1 in let reqs = List.map (fun (p,t,xs) -> (aux p,t,xs)) reqs in cont t0 (locals + ar1) reqs in let lazy_contin x = (* print_string "CONTIN\n"; flush stdout;*) lazy (contin x) in if PatList.Map.is_empty reqs1 then RecordLabelSkip (l,lazy_contin (any_or_abs,0,[])) else let d = mk reqs1 in RecordLabel (l, d, Array.map lazy_contin d.outputs) in field t0 reqs 0 all_labs (* let count = ref 0 let record_disp r = incr count; Printf.printf "record_disp:START %i\n" !count; flush stdout; (* if !count = 42 then Format.fprintf Format.std_formatter "%a@." print r; *) let a = record_disp r in print_string "record_disp:DONE\n"; flush stdout; a let times_disp x y r = incr count; Printf.printf "times_disp:START %i\n" !count; flush stdout; if !count = 239 then Format.fprintf Format.std_formatter "%a@." print r; let a = times_disp x y r in print_string "times_disp:DONE\n"; flush stdout; a let basic_disp r = incr count; Printf.printf "basic_disp:START %i\n" !count; flush stdout; let a = basic_disp r in print_string "basic_disp:DONE\n"; flush stdout; a *) let compute_action r = try AResult (mk_res r r.reqs) with Derivation.NotAResult -> let basic = basic_disp r in let atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic) in let chars = Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic) in AKind { basic = basic; atoms = atoms; chars = chars; prod = times_disp `LeftRight `Normal r; xml = times_disp `LeftRight `XML r; record = record_disp r } (* let compute_action r = print_string "Compute_action:START\n"; flush stdout; let a = compute_action r in print_string "Compute_action:DONE\n"; flush stdout; a *) let print_action ppf = function | AKind a -> print_basic_disp ppf a.basic; print_prod "" ppf a.prod; print_prod "XML" ppf a.xml; print_record ppf a.record | AResult res -> Format.fprintf ppf "%a@." print_result res let print_disp ppf r = match r.actions with | Some _ -> () | None -> print ppf r; let act = compute_action r in print_action ppf act; r.actions <- Some act let actions r = match r.actions with | Some a -> a | None -> let a = compute_action r in Format.fprintf Format.std_formatter "%a%a@." print r print_action a; r.actions <- Some a; a let print_dispatcher ppf r = print ppf r; print_action ppf (actions r) let demo ppf t pl = let (reqs,_) = List.fold_left (fun (reqs,t) ((a,fv,_) as p) -> (add_req reqs p t fv, Types.diff t a)) (empty_reqs,t) pl in let r = mk reqs in to_print r; (try while true do print_disp ppf (Queue.take print_queue) done; with Queue.Empty -> ()) include TargExpr let make_branches t0 brs = let reqs = ref empty_reqs in (* let t0 = ref t0 in let aux ({ descr = (a,fv,_) as p} , _) = reqs := add_req !reqs p !t0 fv; t0 := Types.diff !t0 a in *) let t = ref t0 in let aux ({ descr = (a,fv,_) as p} , _) = reqs := add_req !reqs (cap p (constr !t)) t0 fv; t := Types.diff !t a in List.iter aux brs; let r = mk !reqs in let out (t,ar,binds) = let rec find_bind = function | [] -> None | Some b :: _ -> Some (IdMap.map_to_list (fun i -> i) b) | _ :: rem -> find_bind rem in let rec find_rhs = function | ({ descr = (a,_,_)} , rhs)::_ when Types.subtype t a -> Some rhs | _::rem -> find_rhs rem | [] -> None in match find_bind binds, find_rhs brs with | None,None -> None | Some b, Some rhs -> Some (b,rhs) | _ -> assert false in (r, Array.map out r.outputs) end let approx ((_,fv,_) as p) t = let l = IdSet.get (Factorize.var p t fv) in let m = IdMap.get (Factorize.cst p t fv) in l , m let demo = Compile2.Derivation.demo let demo_compile = Compile2.demo (* Failure: debug compile [ Int* Char* ] [ (x::Int|y::_)* ];; debug approx { a = x; b = y } | { a = y; b = x } Any;; *)