Commit b4b4d74d authored by Pietro Abate's avatar Pietro Abate

[r2004-12-23 00:10:05 by afrisch] Derivation

Original author: afrisch
Date: 2004-12-23 00:10:05+00:00
parent 7a3acc55
......@@ -217,6 +217,8 @@ let debug ppf tenv cenv = function
Format.fprintf ppf "[DEBUG:approx]@.";
let t = Typer.typ tenv t in
let p = Typer.pat tenv p in
Patterns.demo ppf (Patterns.descr p) (Types.descr t);
(*
let (x,c) = Patterns.approx (Patterns.descr p) (Types.descr t) in
List.iter (fun x -> Format.fprintf ppf "%a=* " U.print (Id.value x)) x;
List.iter
......@@ -224,10 +226,9 @@ let debug ppf tenv cenv = function
Format.fprintf ppf "%a=%a "
U.print (Id.value x)
Types.Print.print_const c
) c;
) c; *)
Format.fprintf ppf "@."
let flush_ppf ppf = Format.fprintf ppf "@."
let directive ppf tenv cenv = function
......
......@@ -336,6 +336,17 @@ module Print = struct
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
......@@ -1556,74 +1567,198 @@ module Compile2 = struct
let pi2 t = Types.Product.pi2 (Types.Product.get t)
module Approx = struct
type t = (bool * Types.const option) option
(* - None: cannot match
- Some (true,_): can only bind to the matched value
- Some (_, Some c): can only bind to the constant c *)
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) | Xml (q1,q2) ->
let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
IdSet.cap
(approx_var_node seen q1 (pi1 t) xs)
(approx_var_node seen q2 (pi2 t) xs)
(* Note: this is incomplete because of non-atomic constant patterns:
# debug approx (_,(x:=(1,2))) (1,2);;
[DEBUG:approx]
x=(1,2)
*)
| 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 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) | Xml (q1,q2) ->
let xs = IdSet.cap xs (IdSet.cap q1.fv q2.fv) in
IdSet.cap
(approx_var_node seen q1 (pi1 t) xs)
(approx_var_node seen q2 (pi2 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 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
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
let approx_cst p t =
let rec aux accu (x,t) =
match Sample.single_opt (Types.descr t) with
| Some c -> (x,c)::accu
| None -> accu in
List.fold_left aux [] (filter_descr t p)
module TargExpr = struct
type 'a t = 'a source IdMap.map
and 'a source =
| SrcCapture
| SrcCst of Types.const
| SrcPair of 'a source * 'a source
| SrcFetch of 'a
let capture x = IdMap.singleton x SrcCapture
let captures xs = IdMap.constant SrcCapture xs
let cst x c = IdMap.singleton x (SrcCst c)
let fetch x f = IdMap.singleton x (SrcFetch f)
let empty = IdMap.empty
let merge e1 e2 = IdMap.merge (fun s1 s2 -> SrcPair (s1,s2)) e1 e2
let rec print_src f ppf = function
| SrcCapture -> Format.fprintf ppf "#"
| SrcCst c -> Types.Print.print_const ppf c
| SrcPair (s1,s2) ->
Format.fprintf ppf "(%a,%a)" (print_src f) s1 (print_src f) s2
| SrcFetch x -> f ppf x
let print f ppf r =
Format.fprintf ppf "{ ";
List.iter (fun (x,s) ->
Format.fprintf ppf "%a:=%a "
U.print (Id.value x)
(print_src f) s) (IdMap.get r);
Format.fprintf ppf "}";
end
module Derivation = struct
type ('a,'b) t =
| TSucceed
| TFail
| TAlt of descr * Types.t * ('a,'b) t * ('a,'b) t
| TConj of Types.t * fv * ('a,'b) t * ('a,'b) t
| TOther of descr * Types.t * fv * 'b
| TFact of 'a TargExpr.t * ('a,'b) t
let get_result = function
| TFact (r,TSucceed) -> Some r
| TFail -> None
| _ -> assert false
let approx = approx_var NodeSet.empty
let rec print f g ppf = function
| TSucceed -> Format.fprintf ppf "#"
| TFail -> Format.fprintf ppf "Fail"
| TFact (fact,r) ->
Format.fprintf ppf "{%a}(%a)"
(TargExpr.print f) fact (print f g) r
| TAlt (_,_,l,r) ->
Format.fprintf ppf "(%a | %a)"
(print f g) l (print f g) r
| TConj (_,_,l,r) ->
Format.fprintf ppf "(%a & %a)" (print f g) l (print f g) r
| TOther (_,t,xs,x) ->
Format.fprintf ppf "<t=%a;xs=%a;%a>"
Types.Print.print t
Print.print_xs xs
g (t,xs,x)
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)
| 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 -> TFact (TargExpr.capture x, TSucceed)
| Constant (x,c) -> TFact (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))
| Dummy -> assert false
let fact f p = match p with
| TFact (f2,p) -> TFact (TargExpr.merge f f2,p)
| TFail -> TFail
| p -> if IdMap.is_empty f then p else TFact (f,p)
let rec conj a1 fv1 r1 r2 = match (r1,r2) with
| TSucceed,r | r,TSucceed -> r
| TFail,r | r,TFail -> TFail
| TFact (f,r1), r2 | r2, TFact (f,r1) -> fact 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
| r1,r2 -> TAlt (p,a1,r1,r2)
let opt ((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 p =
if (Types.subtype t a) && (IdSet.is_empty xs)
then TSucceed
else f xs
in
fact pr p
let rec optimize t xs = function
| TFact (pr,p) ->
let pr = IdMap.restrict pr xs in
fact pr (optimize t (IdSet.diff xs (IdMap.domain pr)) p)
| TAlt (p,a1,p1,p2) ->
opt p t xs
(fun xs ->
alt p a1
(optimize t xs p1)
(optimize (Types.diff t a1) xs p2))
| TConj (a1,fv1,p1,p2) ->
conj a1 fv1
(optimize t (IdSet.cap xs fv1) p1)
(optimize (Types.cap t a1) (IdSet.diff xs fv1) p2)
| TOther (p,_,_,x) ->
opt p t xs (fun xs -> TOther (p,t,xs,x))
| (TFail | TSucceed) as p -> 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) ->
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))
end
type dpat =
| TFail
| TSucceed
| TConstr of Types.t
| TCup of pat * pat
| TCap of pat * pat
| TTimes of req * req
| TXml of req * req
| TCapture of id
| TConstant of id * Types.const
and pat = dpat
and req = descr * Types.t * fv
let rec eval_pat (a,fv,d) t xs =
if Types.disjoint a t then TFail
(*
let rec eval_pat (a,fv,d) t xs = if Types.disjoint a t then TFail
else if (IdSet.is_empty xs) && (Types.subtype t a) then TSucceed
else eval_d t xs d
and eval_d t xs = function
......@@ -1636,8 +1771,7 @@ x=(1,2)
eval_pat p2 (Types.cap t a1) (IdSet.cap xs fv2))
| Constant (x,c) when Types.subtype t (Types.constant c) ->
TCapture x
| Constant (x,c) ->
TConstant (x,c)
| Constant (x,c) -> TConstant (x,c)
| Capture x ->
TCapture x
| Times (q1,q2) ->
......@@ -1649,9 +1783,13 @@ x=(1,2)
| Record (l,q) ->
assert false
| Dummy -> assert false
*)
end
let approx ((_,fv,_) as p) t =
let l = IdSet.get (Compile2.Approx.approx p t fv) in
let m = Compile2.Approx.approx_cst p t in
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
......@@ -86,3 +86,5 @@ val approx :
descr ->
Types.descr ->
id list * (id * Types.Const.t) list
val demo: Format.formatter -> descr -> Types.descr -> unit
......@@ -156,6 +156,8 @@ module Map = struct
let is_empty l = l = []
let singleton x y = [ (x,y) ]
let domain l = List.map fst l
let rec iter f = function
| (_,y)::l -> f y; iter f l
| [] -> ()
......@@ -247,6 +249,15 @@ module Map = struct
else diff l1 q2
| _ -> l1
let rec restrict l1 l2 =
match (l1,l2) with
| (((x1,y1) as t1)::q1, x2::q2) ->
let c = X.compare x1 x2 in
if c = 0 then t1::(restrict q1 q2)
else if c < 0 then restrict q1 l2
else restrict l1 q2
| _ -> []
let from_list f l =
let rec initlist = function
| [] -> []
......
......@@ -31,6 +31,8 @@ sig
module Map: sig
type 'a map
external get: 'a map -> (X.t * 'a) list = "%identity"
val domain: 'a map -> t
val restrict: 'a map -> t -> 'a map
val empty: 'a map
val iter: ('a -> unit) -> 'a map -> unit
val filter: (X.t -> 'a -> bool) -> 'a map -> 'a map
......
......@@ -1625,6 +1625,8 @@ struct
count_name := 0;
to_print := [];
DescrHash.clear memo
let print_node ppf n = print ppf (descr n)
end
module Positive =
......
......@@ -254,6 +254,7 @@ sig
val register_global : U.t -> t -> unit
val print_const : Format.formatter -> const -> unit
val print: Format.formatter -> t -> unit
val print_node: Format.formatter -> Node.t -> unit
end
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