Commit f02d2733 authored by Pietro Abate's avatar Pietro Abate

[r2004-12-23 13:31:47 by afrisch] Compil

Original author: afrisch
Date: 2004-12-23 13:31:48+00:00
parent bc96cafb
......@@ -194,7 +194,8 @@ let debug ppf tenv cenv = function
Format.fprintf ppf "[DEBUG:compile]@.";
let t = Typer.typ tenv t
and pl = List.map (Typer.pat tenv) pl in
Patterns.Compile.debug_compile ppf t pl
(* Patterns.Compile.debug_compile ppf t pl *)
Patterns.demo_compile ppf (Types.descr t) (List.map Patterns.descr pl)
| `Explain (t,e) ->
Format.fprintf ppf "[DEBUG:explain]@.";
let t = Typer.typ tenv t in
......
......@@ -236,7 +236,7 @@ end
module Pat = struct
type t = descr
let rec compare (t1,fv1,d1) (t2,fv2,d2) = if d1 == d2 then 0 else
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
......@@ -268,6 +268,19 @@ module Pat = struct
| 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
......@@ -1556,11 +1569,20 @@ module Compile2 = struct
include Pat
end)
module TypesFv = Custom.Pair(Types)(IdSet)
module Request = PatList.MakeMap(TypesFv)
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 t = Types.Product.pi1 (Types.Product.get t)
......@@ -1658,6 +1680,12 @@ x=(1,2)
| TConj of Types.t * fv * ('a,'b) t * ('a,'b) t
| TOther of descr * Types.t * fv * 'b
type atoms =
| TConstr of Types.t
| TTimes of node * node
| TXml of node * node
| TRecord of 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)
......@@ -1680,11 +1708,6 @@ x=(1,2)
| r1,r2 -> TAlt (p,a1,r1,r2)
let get_result = function
| TCapt (r,TSucceed) -> Some r
| TFail -> None
| _ -> assert false
let rec print f g ppf = function
| TSucceed -> Format.fprintf ppf "Succeed"
| TFail -> Format.fprintf ppf "Fail"
......@@ -1700,18 +1723,31 @@ x=(1,2)
Print.print_xs xs
g (t,xs,x)
let get_result = function
| TSucceed -> Some TargExpr.empty
| TCapt (r,TSucceed) -> Some r
| TFail -> None
| r ->
Format.fprintf Format.std_formatter "ERR: %a@."
(print (fun ppf _ -> ()) (fun ppf _ -> ())) r;
assert false
let print_result f ppf = function
| None -> Format.fprintf ppf "Fail"
| Some r -> TargExpr.print f ppf r
let rec mk ((a,fv,d) as p) =
let oth x = TOther (p,Types.any,fv,x) in
match d with
| Constr t -> oth (`Constr t)
| Constr t -> oth (TConstr t)
| 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 -> TCapt (TargExpr.capture x, TSucceed)
| Constant (x,c) -> TCapt (TargExpr.cst x c, TSucceed)
| Times (q1,q2) -> oth (`Times (q1,q2))
| Xml (q1,q2) -> oth (`Xml (q1,q2))
| Record (l,q) -> oth (`Record (l,q))
| Times (q1,q2) -> oth (TTimes (q1,q2))
| Xml (q1,q2) -> oth (TXml (q1,q2))
| Record (l,q) -> oth (TRecord (l,q))
| Dummy -> assert false
let factorize ((a,_,_) as p) t xs f =
......@@ -1744,24 +1780,174 @@ x=(1,2)
(optimize (Types.cap t a1) (IdSet.diff xs fv1) p2)
| TOther (p,_,_,x) ->
factorize p t xs (fun xs -> TOther (p,t,xs,x))
| (TFail | TSucceed) as p -> p
| TSucceed -> if Types.is_empty t then TFail else TSucceed
| TFail -> TFail
let rec fold f accu = function
| TCapt (_,p) -> fold f accu p
| TAlt (_,_,p1,p2) | TConj (_,_,p1,p2) -> fold f (fold f accu p1) p2
| TOther (_,t,xs,x) -> f accu t xs x
| _ -> accu
let collect_basic accu p =
fold (fun accu s xs x -> match x with
| TConstr t -> (t,s) :: accu
| _ -> accu
) accu p
let mkopt p t xs = optimize t xs (mk p)
let demo ppf ((_,fv,_) as p) t =
let oth ppf (t,xs,d) = match d with
| `Constr t -> Types.Print.print ppf t
| `Times (q1,q2) ->
| TConstr t -> Types.Print.print ppf t
| TTimes (q1,q2) ->
if IdSet.is_empty xs then
Format.fprintf ppf "(%a,%a)"
Types.Print.print_node q1.accept Types.Print.print_node q2.accept
else
Format.fprintf ppf "(%a,%a)"
Print.print q1.descr Print.print q2.descr
| `Xml _ -> Format.fprintf ppf "<_>_"
| `Record _ -> Format.fprintf ppf "{_}" in
print oth oth ppf (optimize t fv (mk p))
| TXml _ -> Format.fprintf ppf "<_>_"
| TRecord _ -> Format.fprintf ppf "{_}" in
let p = mkopt p t fv in
print oth oth ppf p;
let qs = collect_basic [] p in
let part = Types.cond_partition Types.non_constructed qs in
let t = Types.cap t Types.non_constructed in
Format.fprintf ppf "@.Partition:@.";
List.iter (fun t' ->
let t = Types.cap t t' in
let r = optimize t fv p in
Format.fprintf ppf "%a => %a@."
Types.Print.print t
(print oth oth) r;
(* Format.fprintf ppf " => %a@."
(print_result oth) (get_result r) *)
) part
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 t = {
outputs : output array;
rescode : rescode;
reqs : ((unit,Derivation.atoms) Derivation.t * Types.t * fv) list;
assumpt : Types.t;
}
type basic_disp = (Types.t * int * unit TargExpr.source array) list
let print ppf r =
Format.fprintf ppf "Request@.";
Array.iteri
(fun i (t,ar,_) ->
Format.fprintf ppf "[%i] %a@." i Types.Print.print t
) r.outputs
let print_basic_disp ppf l =
List.iter
(fun (t,code,a) ->
Format.fprintf ppf "%a => $%i(" Types.Print.print t code;
Array.iter (fun x ->
Format.fprintf ppf "%a;"
(TargExpr.print_src (fun ppf _ -> assert false))
x) a;
Format.fprintf ppf ")@.";
) l
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
| _ -> assert false
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 mk reqs t0 =
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,fv,_) as p,(t,xs)) :: rem ->
let (alc,ar') = alloc ar fv in
RSwitch
(aux (Types.cap t0 a)
ar' (Some alc::binds) rem,
aux (Types.diff t0 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 rc = aux t0 0 [] reqs in
let os = Array.of_list (List.rev !codes) in
let ders = List.map
(fun (p,(t,xs)) -> (Derivation.mkopt p t xs, t, xs)) reqs in
{ outputs = os;
rescode = rc;
reqs = ders;
assumpt = t0
}
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
(Derivation.optimize t xs p, t, xs))
let get_results reqs =
List.map (fun (p,_,_) -> Derivation.get_result p) reqs
let basic_disp r : basic_disp =
let t0 = Types.cap r.assumpt Types.non_constructed in
let reqs = opt_all t0 r.reqs in
let qs =
List.fold_left
(fun accu (p,_,_) -> Derivation.collect_basic accu p) [] reqs in
let part = Types.cond_partition t0 qs in
List.map
(fun t ->
let reqs = opt_all t reqs in
let res = get_results reqs in
let code = find_code res r.rescode in
let (_,ar,fill) = r.outputs.(code) in
let o = Array.make ar (TargExpr.SrcFetch ()) in
List.iter2
(fun res fill -> match (res,fill) with
| Some res, Some fill ->
IdMap.iteri (fun x i -> o.(i) <- IdMap.assoc x res) fill
| None, None -> ()
| _ -> assert false)
res fill;
(t,code,o)
) part
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 t in
print ppf r;
print_basic_disp ppf (basic_disp r)
end
end
let approx ((_,fv,_) as p) t =
......@@ -1771,3 +1957,4 @@ let approx ((_,fv,_) as p) t =
let demo = Compile2.Derivation.demo
let demo_compile = Compile2.Request.demo
......@@ -88,3 +88,4 @@ val approx :
id list * (id * Types.Const.t) list
val demo: Format.formatter -> descr -> Types.descr -> unit
val demo_compile: Format.formatter -> Types.descr -> descr list -> unit
......@@ -162,6 +162,10 @@ module Map = struct
| (_,y)::l -> f y; iter f l
| [] -> ()
let rec iteri f = function
| (x,y)::l -> f x y; iteri f l
| [] -> ()
let rec filter f = function
| ((x,y) as c)::l -> if f x y then c::(filter f l) else filter f l
| [] -> []
......
......@@ -35,6 +35,7 @@ sig
val restrict: 'a map -> t -> 'a map
val empty: 'a map
val iter: ('a -> unit) -> 'a map -> unit
val iteri: (X.t -> 'a -> unit) -> 'a map -> unit
val filter: (X.t -> 'a -> bool) -> 'a map -> 'a map
val is_empty: 'a map -> bool
val singleton: X.t -> 'a -> 'a map
......
......@@ -1869,3 +1869,18 @@ let empty_closed_record = rec_of_list ~opened:false []
let empty_opened_record = rec_of_list ~opened:true []
(* </helpers> *)
let cond_partition univ qs =
let rec add accu (t,s) =
let t = if subtype t s then t else cap t s in
if (subtype s t) || (is_empty t) then accu else
let rec aux accu u =
let c = cap u t in
if (is_empty c) || (subtype (cap u s) t) then u::accu
else c::(diff u t)::accu
in
List.fold_left aux [] accu
in
List.fold_left add [ univ ] qs
......@@ -249,6 +249,15 @@ val non_empty: t -> bool
val subtype : t -> t -> bool
val disjoint : t -> t -> bool
(** Tools for compilation of PM **)
val cond_partition: t -> (t * t) list -> t list
(* The second argument is a list of pair of types (ti,si)
interpreted as the question "member of ti under the assumption si".
The result is a partition of the first argument which is precise enough
to answer all the questions. *)
module Print :
sig
val register_global : U.t -> t -> unit
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment