exception Error of string open Ident (* 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 P = struct type t = descr let rec compare (t1,fv1,d1) (t2,fv2,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 end module Print = struct module M = Map.Make(P) module S = Set.Make(P) 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 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) (* 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