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 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 q2.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) (* 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 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) type nnf = NodeSet.t * Types.t (* pl,t; t <= \accept{pl} *) let check_nnf (pl,t) = List.iter (fun p -> assert(Types.subtype t (Types.descr p.accept))) (NodeSet.get pl) let print_nnf ppf (pl,t) = Format.fprintf ppf "@[(pl=%a;t=%a)@]" NodeSet.dump pl Types.Print.print t let compare_nnf (l1,t1) (l2,t2) = let c = NodeSet.compare l1 l2 in if c <> 0 then c else Types.compare t1 t2 let hash_nnf (l,t) = (NodeSet.hash l) + 17 * (Types.hash t) module NLineBasic = SortedList.Make( 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 NLineProd = SortedList.Make( struct (* include Custom.Dummy*) 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 print_nnf x print_nnf y type t = result * nnf * nnf let compare (r1,x1,y1) (r2,x2,y2) = let c = compare_result r1 r2 in if c <> 0 then c else let c = compare_nnf x1 x2 in if c <> 0 then c else compare_nnf y1 y2 let equal x y = compare x y == 0 let hash (r,x,y) = hash_result r + 17 * (hash_nnf x) + 267 * (hash_nnf y) end ) type record = | RecNolabel of result option * result option | RecLabel of label * NLineProd.t type t = { nfv : fv; ncatchv: 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 let compare_nf 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 = IdSet.compare t1.ncatchv t2.ncatchv 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 match t1.nrecord, t2.nrecord with | RecNolabel (s1,n1), RecNolabel (s2,n2) -> let c = match (s1,s2) with | None,None -> 0 | Some r1, Some r2 -> compare_result r1 r2 | None, _ -> -1 | _, None -> 1 in if c <> 0 then c else (match (n1,n2) with | None,None -> 0 | Some r1, Some r2 -> compare_result r1 r2 | None, _ -> -1 | _, None -> 1) | 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 fus = IdMap.union_disj let nempty lab = { nfv = IdSet.empty; ncatchv = 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; ncatchv = IdSet.cap nf1.ncatchv nf2.ncatchv; 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),(ql1,s1)) (res2,(pl2,t2),(ql2,s2)) = 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),(NodeSet.cup ql1 ql2,s)) :: 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; ncatchv = IdSet.cup nf1.ncatchv nf2.ncatchv; 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 = NodeSet.singleton p, Types.descr p.accept let nc t = NodeSet.empty, t let ncany = nc Types.any let empty_res = IdMap.empty let ntimes lab acc p q = let src_p = IdMap.constant SLeft p.fv and src_q = IdMap.constant SRight q.fv in let src = IdMap.merge_elem SRecompose src_p src_q in { nempty lab with nfv = IdSet.cup p.fv q.fv; na = acc; nprod = NLineProd.singleton (src, nnode p, nnode q); } let nxml lab acc p q = let src_p = IdMap.constant SLeft p.fv and src_q = IdMap.constant SRight q.fv in let src = IdMap.merge_elem SRecompose src_p src_q in { nempty lab with nfv = IdSet.cup p.fv q.fv; na = acc; nxml = NLineProd.singleton (src, nnode p, nnode q); } let nrecord lab acc l p = match lab with | None -> assert false | Some label -> assert (label <= l); if l == label then let src = IdMap.constant SLeft p.fv in { nempty lab with nfv = p.fv; na = acc; nrecord = RecLabel(label, NLineProd.singleton (src,nnode p, ncany))} else let src = IdMap.constant SRight p.fv in let p' = make p.fv in (* optimize this ... *) (* cache the results to avoid looping ... *) define p' (record l p); { nempty lab with nfv = p.fv; na = acc; nrecord = RecLabel(label, NLineProd.singleton(src,nc Types.Record.any_or_absent, nnode p') )} 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 -> (* let ppf = Format.std_formatter in Format.fprintf ppf "Constr record t=%a l=%a@." Types.Print.print t Label.print (LabelPool.value l); let sp = Types.Record.split_normal t l in List.iter (fun (t1,t2) -> Format.fprintf ppf "t1=%a t2=%a@." Types.Print.print t1 Types.Print.print t2) sp; *) RecLabel (l,aux (Types.Record.split_normal t l)) in { nempty lab with na = t; nbasic = NLineBasic.singleton (empty_res, Types.cap t any_basic); nprod = aux (Types.Product.normal t); nxml = aux (Types.Product.normal ~kind:`XML t); nrecord = record } let nconstant lab x c = let l = IdMap.singleton x (SConst c) in { nfv = IdSet.singleton x; ncatchv = IdSet.empty; na = Types.any; nbasic = NLineBasic.singleton (l,any_basic); nprod = NLineProd.singleton (l,ncany,ncany); nxml = NLineProd.singleton (l,ncany,ncany); nrecord = match lab with | None -> RecNolabel (Some l, Some l) | Some lab -> RecLabel (lab, NLineProd.singleton (l,nc Types.Record.any_or_absent, ncany)) } let ncapture lab x = let l = IdMap.singleton x SCatch in { nfv = IdSet.singleton x; ncatchv = IdSet.singleton x; na = Types.any; nbasic = NLineBasic.singleton (l,any_basic); nprod = NLineProd.singleton (l,ncany,ncany); nxml = NLineProd.singleton (l,ncany,ncany); nrecord = match lab with | None -> RecNolabel (Some l, Some l) | Some lab -> RecLabel (lab, NLineProd.singleton (l,nc Types.Record.any_or_absent, ncany)) } let rec nnormal lab (acc,fv,d) = if Types.is_empty acc then nempty lab else match d with | Constr t -> nconstr lab t | Cap (p,q) -> ncap (nnormal lab p) (nnormal lab q) | Cup ((acc1,_,_) as p,q) -> ncup (nnormal lab p) (ncap (nnormal lab q) (nconstr lab (Types.neg acc1))) | Times (p,q) -> ntimes lab acc p q | Xml (p,q) -> nxml lab acc p q | Capture x -> ncapture lab x | Constant (x,c) -> nconstant lab x c | Record (l,p) -> nrecord lab acc l p | Dummy -> assert false (*TODO: when an operand of Cap has its first_label > lab, directly shift it*) 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) (* should "first_label_type acc1" ? *) | Record (l,p) -> l | _ -> LabelPool.dummy_max let remove_catchv n = let ncv = n.ncatchv in let nlinesbasic l = NLineBasic.map (fun (res,x) -> (IdMap.diff res ncv,x)) l in let nlinesprod l = NLineProd.map (fun (res,x,y) -> (IdMap.diff res ncv,x,y)) l in { nfv = IdSet.diff n.nfv ncv; ncatchv = n.ncatchv; na = n.na; nbasic = nlinesbasic n.nbasic; nprod = nlinesprod n.nprod; nxml = nlinesprod n.nxml; nrecord = (match n.nrecord with | RecNolabel (x,y) -> let x = match x with | Some res -> Some (IdMap.diff res ncv) | None -> None in let y = match y with | Some res -> Some (IdMap.diff res ncv) | None -> None in RecNolabel (x,y) | RecLabel (lab,l) -> RecLabel (lab, nlinesprod l)) } let print_node_list ppf pl = List.iter (fun p -> Format.fprintf ppf "%a;" Node.dump p) pl let normal l t pl = remove_catchv (List.fold_left (fun a p -> ncap a (nnormal l (descr p))) (nconstr l t) pl) (* 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 and source = | Catch | Const of Types.const | Left of int | Right of int | Recompose of int * int and return_code = Types.t * int * (* accepted type, arity *) (int * int id_map) list 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 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 equal_source s1 s2 = (s1 == s2) || match (s1,s2) with | Const x, Const y -> Types.Const.equal x y | Left x, Left y -> x == y | Right x, Right y -> x == y | Recompose (x1,x2), Recompose (y1,y2) -> (x1 == y1) && (x2 == y2) | _ -> false let equal_result (r1,s1) (r2,s2) = (r1 == r2) && (equal_array equal_source s1 s2) 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 array_for_all f a = let rec aux f a i = if i == Array.length a then true else f a.(i) && (aux f a (succ i)) in aux f a 0 let array_for_all_i f a = let rec aux f a i = if i == Array.length a then true else f i a.(i) && (aux f a (succ i)) in aux f a 0 let combine_kind basic prod xml record = try ( let rs = [] in let rs = match basic with | [_,r] -> r :: rs | [] -> rs | _ -> raise Exit in let rs = match prod with | Impossible -> rs | Ignore (Ignore r) -> r :: rs | _ -> raise Exit in let rs = match xml with | Impossible -> rs | Ignore (Ignore r) -> r :: rs | _ -> raise Exit in let rs = match record with | None -> rs | Some (RecLabel (_,Ignore (Ignore r))) -> r :: rs | Some (RecNolabel (Some r1, Some r2)) -> r1 :: r2 :: rs | _ -> raise Exit in match rs with | ((_, ret) as r) :: rs when List.for_all ( equal_result r ) rs && array_for_all (function Catch | Const _ -> true | _ -> false) ret -> AIgnore r | _ -> raise Exit ) with Exit -> AKind { 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 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_right_tail_call = function | Dispatch (disp,branches) when array_for_all_i (fun i (code,ret) -> (i == code) && (array_for_all_i (fun pos -> function Right j when pos == j -> true | _ -> false) ret ) ) branches -> TailCall disp | x -> x let detect_left_tail_call = function | Dispatch (disp,branches) when array_for_all_i (fun i -> function | Ignore (code,ret) -> (i == code) && (array_for_all_i (fun pos -> function Left j when pos == j -> true | _ -> false) ret ) | _ -> false ) branches -> TailCall disp | x -> x let cur_id = State.ref "Patterns.cur_id" 0 (* TODO: save dispatchers ? *) module NfMap = Map.Make( struct type t = Normal.t let compare = Normal.compare_nf end) module DispMap = Map.Make( struct type t = Types.t * Normal.t array let rec compare_rec a1 a2 i = if i < 0 then 0 else let c = Normal.compare_nf a1.(i) a2.(i) in if c <> 0 then c else compare_rec a1 a2 (i - 1) let compare (t1,a1) (t2,a2) = let c = Types.compare t1 t2 in if c <> 0 then c else let l1 = Array.length a1 and l2 = Array.length a2 in if l1 < l2 then -1 else if l1 > l2 then 1 else compare_rec a1 a2 (l1 - 1) end ) (* 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 ppf = Format.std_formatter in Format.fprintf ppf "dispatcher %i:" !cur_id; Array.iter (fun x -> Format.fprintf ppf "%a;" Normal.print x) pl; Format.fprintf ppf "@."; *) let nb = ref 0 in let codes = ref [] in let rec aux t arity i accu = if i == Array.length pl then (incr nb; codes := (t,arity,accu)::!codes; `Result (!nb - 1)) else let p = pl.(i) in let tp = p.Normal.na in (* let tp = Types.normalize tp in *) let a1 = Types.cap t tp in if Types.is_empty a1 then `Switch (`None,aux t arity (i+1) accu) else let v = p.Normal.nfv in let a2 = Types.diff t tp in let accu' = (i,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) 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 (* Array.iteri (fun i p -> Format.fprintf Format.std_formatter "Pattern %i/%i accepts %a@." i (Array.length pl) Types.Print.print p.Normal.na) pl; *) 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 (); (* Format.fprintf Format.std_formatter "iface=%a@." print_iface iface;*) 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 (* let ppf = Format.std_formatter in Format.fprintf ppf "find_code iface=%a [ " print_iface d.interface; for i = 0 to Array.length a - 1 do if (a.(i) != None) then Format.fprintf ppf "+ " else Format.fprintf ppf "- " done; Format.fprintf ppf "]@."; *) 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 = 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) let conv_source_basic s = match s with | Normal.SCatch -> Catch | Normal.SConst c -> Const c | _ -> assert false let assoc v l = try IdMap.assoc v l with Not_found -> -1 let conv_source_prod left right v s = match s with | Normal.SCatch -> Catch | Normal.SConst c -> Const c | Normal.SLeft -> Left (assoc v left) | Normal.SRight -> Right (assoc v right) | Normal.SRecompose -> Recompose (assoc v left, assoc v right) 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; let aux_final res = IdMap.map_to_list conv_source_basic res in accu := (t, return disp selected aux_final) :: !accu | (ty,i) :: rem -> aux (i @ success) (Types.cap t ty) rem; aux success (Types.diff t ty) rem in aux [] t tests; !accu let get_tests pl f t d post = let accu = ref [] in let aux i x = let (pl,ty), info = f x in let pl = Normal.NodeSet.get pl in accu := (ty,pl,i,info) :: !accu in Array.iteri (fun i -> List.iter (aux i)) pl; let lab = List.fold_left (fun l (ty,pl,_,_) -> List.fold_left (fun l p -> min l (Normal.first_label (descr p))) (min l (Types.Record.first_label ty)) pl ) LabelPool.dummy_max !accu in let lab = if lab == LabelPool.dummy_max then None else Some lab in let pats = ref NfMap.empty in let nb_p = ref 0 in List.iter (fun (ty,pl,i,info) -> let p = Normal.normal lab ty pl in let x = (i, p.Normal.ncatchv, info) in try let s = NfMap.find p !pats in s := x :: !s with Not_found -> pats := NfMap.add p (ref [x]) !pats; incr nb_p ) !accu; let infos = Array.make !nb_p [] in let ps = Array.make !nb_p Normal.dummy in let count = ref 0 in NfMap.iter (fun p l -> let i = !count in infos.(i) <- !l; ps.(i) <- p; count := succ i) !pats; assert( !nb_p == !count ); let disp = dispatcher t ps lab in let result (t,_,m) = (* Format.fprintf Format.std_formatter "Result=%a@." Types.Print.print t;*) let selected = Array.create (Array.length pl) [] in let add r (i, ncv, inf) = selected.(i) <- (r,ncv,inf) :: selected.(i) in List.iter (fun (j,r) -> List.iter (add r) infos.(j)) m; d t selected 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 (_,brs) = List.fold_left (fun (t,brs) (p,e) -> let p' = (Normal.NodeSet.singleton p,t) in (* let td = Types.descr (accept p) in let t' = if Types.is_empty (Types.cap t td) then t else Types.diff t td in*) let t' = Types.diff t (Types.descr (accept p)) in (t', (p',(fv p, e)) :: brs) ) (t,[]) brs in let pl = Array.map (fun x -> [x]) (Array.of_list brs) in get_tests pl (fun x -> x) t (fun _ pl -> let r = ref Fail in let aux = function | [(res,catchv,(fvl,e))] -> assert (!r == Fail); let catchv = IdMap.constant (-1) catchv in let m = IdMap.union_disj catchv res in let m = List.map (fun x -> (x,IdMap.assoc x m)) fvl in r := Match (m,e) | [] -> () | _ -> assert false in Array.iter aux pl; !r ) (fun x -> x) let rec dispatch_prod ?(kind=`Normal) disp = let pl = match kind with | `Normal -> Array.map (fun p -> Normal.NLineProd.get p.Normal.nprod) disp.pl | `XML -> Array.map (fun p -> Normal.NLineProd.get p.Normal.nxml) disp.pl in let t = Types.Product.get ~kind disp.t in dispatch_prod0 disp t pl and dispatch_prod0 disp t pl = get_tests 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 pl = get_tests pl (fun (ret1, ncatchv, (res,q)) -> q, (ret1,res) ) (Types.Product.pi2_restricted t1 t) (dispatch_prod2 disp) (fun x -> detect_right_tail_call (combine equal_result x)) and dispatch_prod2 disp t2 pl = let aux_final (ret2, ncatchv, (ret1, res)) = IdMap.mapi_to_list (conv_source_prod ret1 ret2) res in return disp pl aux_final 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)) 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)) else None in Some (RecNolabel (some,none)) | Some lab -> (* Format.fprintf Format.std_formatter "lab=%a Split:@." Label.print (LabelPool.value lab);*) let t = Types.Record.split t lab in (* List.iter (fun (t1,t2) -> Format.fprintf Format.std_formatter "t1=%a t2=%a@." Types.Print.print t1 Types.Print.print t2) t; *) 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)) (* soucis avec les ncatchv ?? *) 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 ppf = function | Catch -> Format.fprintf ppf "v" | Const c -> Types.Print.print_const ppf c | Left (-1) -> Format.fprintf ppf "v1" | Right (-1) -> Format.fprintf ppf "v2" | Left i -> Format.fprintf ppf "l%i" i | Right j -> Format.fprintf ppf "r%i" j | Recompose (i,j) -> Format.fprintf ppf "(%a,%a)" print_source (Left i) print_source (Right j) let print_result ppf = Array.iteri (fun i s -> if i > 0 then Format.fprintf ppf ","; print_source ppf s; ) let print_ret ppf (code,ret) = Format.fprintf ppf "$%i" code; if Array.length ret <> 0 then Format.fprintf ppf "(%a)" print_result ret let print_ret_opt ppf = function | None -> Format.fprintf ppf "*" | Some r -> print_ret ppf r let print_kind ppf actions = let print_lhs ppf (code,prefix,d) = let arity = match d.codes.(code) with (_,a,_) -> a in Format.fprintf ppf "$%i(" code; for i = 0 to arity - 1 do if i > 0 then Format.fprintf ppf ","; Format.fprintf ppf "%s%i" prefix i; done; 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 = function | Impossible -> assert false | Ignore r -> Format.fprintf ppf " %a\n" print_ret r | TailCall d -> queue d; Format.fprintf ppf " disp_%i v2@\n" d.id | Dispatch (d, branches) -> queue d; Format.fprintf ppf " match v2 with disp_%i@\n" d.id; Array.iteri (fun code r -> Format.fprintf ppf " | %a -> %a\n" print_lhs (code, "r", d) print_ret r; ) branches in let print_prod prefix ppf = function | Impossible -> () | Ignore d2 -> Format.fprintf ppf " | %s(v1,v2) -> @\n" prefix; print_prod2 d2 | TailCall d -> queue d; Format.fprintf ppf " | %s(v1,v2) -> @\n" prefix; Format.fprintf ppf " disp_%i v1@\n" d.id | Dispatch (d,branches) -> queue d; Format.fprintf ppf " | %s(v1,v2) -> @\n" prefix; Format.fprintf ppf " match v1 with disp_%i@\n" d.id; Array.iteri (fun code d2 -> Format.fprintf ppf " | %a -> @\n" print_lhs (code, "l", d); print_prod2 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 (Normal.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 -> Normal.normal lab (*t*) Types.Record.any_or_absent [p]) pl) in show ppf t pl lab; Format.fprintf ppf "# compiled dispatchers: %i@\n" !cur_id end (* New compilation procedure *) module Compile2 = struct 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 Approx = struct (* 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) -> IdSet.cap (approx_var seen p1 (Types.cap t a1) xs) (approx_var seen p2 (Types.diff 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 (NodeSet.mem q seen) then xs else approx_var (NodeSet.add q seen) q.descr t xs let approx_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 approx_var ((a,_,_) as p) t = approx_var NodeSet.empty p (Types.cap t a) end 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 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 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 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 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 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 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 let get_result = function | TSucceed -> Some TargExpr.empty | TCapt (r,TSucceed) -> Some r | TFail -> None | r -> Format.fprintf Format.std_formatter "ERR: %a@." print r; assert false 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, Types.any) | 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 (TargExpr.capture x) | Constant (x,c) -> success (TargExpr.cst x c) | Times (q1,q2) -> TTimes (`Normal,(incr uid; !uid), p,Types.any,fv,q1,q2) | Xml (q1,q2) -> TTimes (`XML,(incr uid; !uid), p,Types.any,fv,q1,q2) | Record (l,q) -> TRecord ((incr uid; !uid),p, Types.any,fv,l,q) | Dummy -> assert false let constrain a t = if Types.disjoint a t then TFail else if Types.subtype t a then TSucceed else TConstr (a,t) let factorize ((a,_,_) as p) t xs f = if Types.disjoint a t then TFail else let vs = Approx.approx_var p t xs in let xs = IdSet.diff xs vs in let pr = TargExpr.captures vs in let vs = Approx.approx_cst p t xs in let xs = IdSet.diff xs (IdMap.domain vs) in let pr = TargExpr.merge (TargExpr.constants vs) 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 fold f accu = function | TCapt (_,p) -> f accu p | TAlt (_,_,p1,p2) | TConj (_,_,p1,p2) -> f (f accu p1) p2 | _ -> accu 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 rec collect_constr accu = function | TConstr (t,s) -> (t,s)::accu | p -> fold collect_constr accu p let rec collect_times k accu = function | TTimes (kind,uid,_,t,xs,q1,q2) when k == kind -> (uid,t,xs,q1,q2)::accu | p -> fold (collect_times k) accu p let rec collect_record accu = function | TRecord (uid,_,t,xs,l,q) -> (uid,t,xs,l,q)::accu | p -> fold collect_record accu p 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 collect_all f reqs = List.fold_left (fun accu (p,_,_) -> f accu p) [] reqs let prod_all k side pi sel selq reqs = let extra = ref [] in let aux3 s1 accu t12 = let t1 = sel t12 in if (Types.subtype s1 t1) || (Types.disjoint s1 t1) then accu else add_req accu (constr t1) s1 IdSet.empty in let aux2 accu (t,s) = List.fold_left (aux3 (pi s)) accu (Types.Product.get ~kind:k t) in let aux accu (uid,t,xs,q1,q2) = let q = selq (q1,q2) in let xs = IdSet.cap xs q.fv in let p = q.descr in let t = pi t in let vs = Approx.approx_var p t xs in let xs = IdSet.diff xs vs in let pr = side vs in extra := (uid,pr)::!extra; if (IdSet.is_empty xs) && (Types.subtype t (Types.descr q.accept)) then accu else add_req accu p t xs in let accu = List.fold_left aux empty_reqs (collect_all (collect_times k) reqs) in let accu = List.fold_left aux2 accu (collect_all collect_constr reqs) in !extra,accu let first_label reqs = let min = ref LabelPool.dummy_max in let f l = if l < !min then min := l in let aux2 (t,_) = f (Types.Record.first_label t) in let aux (_,_,_,l,_) = f l in List.iter aux (collect_all collect_record reqs); List.iter aux2 (collect_all collect_constr reqs); !min 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 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; let ts = collect_record [] p in Format.fprintf ppf "@.Fields:@."; List.iter (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) ) ts end module Request = struct type output = Types.t * int * int id_map option list type rescode = | RFail | RCode of int | RSwitch of rescode * rescode type result = int * TargExpr.source array type actions = | AIgnore of result | AKind of actions_kind and actions_kind = { basic: (Types.t * result) list; prod: actions_prod; xml: actions_prod; record: label; } 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 ppf r = Format.fprintf ppf "disp_%i:@." r.id; (* Array.iteri (fun i (t,ar,binds) -> Format.fprintf ppf "[%i]{%i}{%a} %a@." i ar print_binds binds Types.Print.print t ) r.outputs; 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) 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_record ppf l = Format.fprintf ppf "First label = %a@." print_lab l 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 let rec find_code bl rc = match (bl,rc) with | Some _::bl,RSwitch (rc,_) | None::bl,RSwitch (_,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 find_code_t0 t0 r = let rec aux i = if i = Array.length r.outputs then (-1) else let (t,_,_) = r.outputs.(i) in if Types.subtype t0 t then i else aux (succ i) in aux 0 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 | [] -> incr nb; codes := (t0,ar,List.rev binds) :: !codes; RCode !nb | ((a,_,_),(t,xs)) :: rem -> 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 let t0 = List.fold_left (fun accu (_,(t,_)) -> Types.cup accu t) Types.empty reqs in (* let t0 = Types.any 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 -> let d = mk reqs in ReqTable.add disps reqs d; d let mk_res t0 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 (* let code = find_code_t0 t0 r 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 in if Types.is_empty t0 then [] else let reqs = Derivation.opt_all t0 r.reqs in let qs = Derivation.collect_all Derivation.collect_constr reqs in let part = Types.cond_partition t0 qs in List.map (fun t -> (t, mk_res t r (Derivation.opt_all t reqs))) part let prod_all k side pi sel selq reqs = let extra = ref [] in let aux3 s1 accu t12 = let t1 = sel t12 in if (Types.subtype s1 t1) || (Types.disjoint s1 t1) then accu else add_req accu (constr t1) s1 IdSet.empty in let aux2 accu (t,s) = List.fold_left (aux3 (pi s)) accu (Types.Product.get ~kind:k t) in let aux accu (uid,t,xs,q1,q2) = let q = selq (q1,q2) in let xs = IdSet.cap xs q.fv in let p = q.descr in let t = pi t in let vs = Approx.approx_var p t xs in let xs = IdSet.diff xs vs in let pr = side vs in extra := (uid,pr)::!extra; if (IdSet.is_empty xs) && (Types.subtype t (Types.descr q.accept)) then accu else add_req accu p t xs in let accu = List.fold_left aux empty_reqs (Derivation.collect_all (Derivation.collect_times k) reqs) in let accu = List.fold_left aux2 accu (Derivation.collect_all Derivation.collect_constr reqs) in !extra,accu let call_disp reqs f = if PatList.Map.is_empty reqs then Ignore (f (Types.any,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 = prod_all k TargExpr.captures_left pi1 fst fst' reqs in let second (t1,ar1,binds1) = let t0 = restr1 t0 t1 in let reqs = Derivation.opt_all t0 reqs in let extra2,reqs2 = 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 t0 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 record_disp r = let t0 = Types.cap r.assumpt Types.Record.any in let reqs = Derivation.opt_all t0 r.reqs in Derivation.first_label reqs let print_disp ppf r = match r.actions with | Some _ -> () | None -> print ppf r; let basic = basic_disp r and prod = times_disp `RightLeft `Normal r and xml = times_disp `LeftRight `XML r and record = record_disp r in print_basic_disp ppf basic; print_prod "" ppf prod; print_prod "XML" ppf xml; print_record ppf record; r.actions <- Some (AKind { basic = basic; prod = prod; xml = xml; record = record; }) 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 -> ()) end end let approx ((_,fv,_) as p) t = let l = IdSet.get (Compile2.Approx.approx_var p t fv) in let m = IdMap.get (Compile2.Approx.approx_cst p t fv) in l , m let demo = Compile2.Derivation.demo let demo_compile = Compile2.Request.demo (* Failure: debug compile [ Int* Char* ] [ (x::Int|y::_)* ];; debug approx { a = x; b = y } | { a = y; b = x } Any;; *)