[r2004-12-22 01:14:22 by afrisch] Better factorization

Original author: afrisch
Date: 2004-12-22 01:14:22+00:00

driver/cduce.ml

@@ -217,20 +217,15 @@ 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
-      let c = Patterns.approx (Patterns.descr p) (Types.descr t) in
-      List.iter 
+      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
 	(fun (x,c) ->
-	   Format.fprintf ppf "%a:" U.print (Id.value x);
-	   (match c with
-	      | None -> Format.fprintf ppf "*"
-	      | Some (v,c) ->
-		  if v then Format.fprintf ppf "# ";
-		  match c with
-		    | Some c -> 
-			Format.fprintf ppf "%a" Types.Print.print_const c
-		    | None -> ());
-	   Format.fprintf ppf "@."
-	) c
+	   Format.fprintf ppf "%a=%a "
+	     U.print (Id.value x) 
+	     Types.Print.print_const c
+	) c;
+      Format.fprintf ppf "@."
 
 
 let flush_ppf ppf = Format.fprintf ppf "@."

types/patterns.ml

@@ -407,6 +407,11 @@ let filter t p =
   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 *)
 
@@ -1556,66 +1561,51 @@ module Compile2 = struct
 	   - Some (true,_): can only bind to the matched value
 	   - Some (_, Some c): can only bind to the constant c *)
 
-    let merge_times2 a b = match (a,b) with
-      | Some (x1,c1), Some (x2,c2) ->
-	  Some (x1 && x2,
-		match c1,c2 with
-		  | Some c1, Some c2 -> Some (Types.Pair (c1,c2))
-		  | _ -> None)
-      | _ ->
-	  Some (true, None) (* Todo:  Pair (c,None) *)
-    let merge_times1 = function
-      | Some (x,c) -> Some (false,c)
-      | None -> None
-
-    let merge a b = match (a,b) with
-      | None, x | x, None -> x
-      | Some (x1, c1), Some (x2,c2) ->
-	  Some (x1 && x2,
-		match c1,c2 with
-		  | Some c1, Some c2 when 
-		      Types.Const.compare c1 c2 = 0 -> Some c1
-(* Note: the same constant can have several representations.
-   Currently, Const.compare will distinguish them. E.g.:
-# debug approx (x := "ab") & Int | (x := ('a',"b")) Any;;
-[DEBUG:approx]
-*)
-		  | _ -> None)
-
-  let rec approx seen ((a,fv,d) as p) 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 then IdSet.Map.empty
-    else if (Types.is_empty t) then IdSet.Map.constant None xs
+    if (IdSet.is_empty xs) || (Types.is_empty t) then xs
     else match d with
       | Cup ((a1,_,_) as p1,p2) ->
-	  IdSet.Map.merge merge 
-	    (approx seen p1 (Types.cap t a1) xs) 
-	    (approx seen p2 (Types.diff t a1) xs)
+	  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.Map.union_disj
-	    (approx seen p1 t (IdSet.cap fv1 xs))
-	    (approx seen p2 t (IdSet.cap fv2 xs))
-      | Capture x ->
-	  IdSet.Map.singleton x 
-	    (Some (true, Sample.single_opt t))
-      | Constant (x,c) -> 
-	  IdSet.Map.singleton x 
-	    (Some (Types.subtype t (Types.constant c), Some c))
-      | Times (q1,q2) ->
-	  IdSet.Map.combine merge_times1 merge_times1 merge_times2
-	    (approx_node seen q1 (pi1 t) (IdSet.cap q1.fv xs)) 
-	    (approx_node seen q2 (pi2 t) (IdSet.cap q2.fv xs))
-      | _ ->
-	  IdSet.Map.constant (Some (false, None)) xs
-	  (* TODO: recursive factorization   (x,x) -> x *)
-  and approx_node seen q t xs =
+	  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 IdSet.Map.constant None xs
-    else approx (NodeSet.add q seen) q.descr t xs
+    then xs
+    else approx_var (NodeSet.add q seen) q.descr t xs
+
 
+  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)
+      
 
-  let approx = approx NodeSet.empty
+  let approx = approx_var NodeSet.empty
   end
 
   type dpat =
@@ -1662,4 +1652,6 @@ module Compile2 = struct
 end
 
 let approx ((_,fv,_) as  p) t = 
-  IdSet.Map.get (Compile2.Approx.approx p t fv)
+  let l = IdSet.get (Compile2.Approx.approx p t fv) in
+  let m = Compile2.Approx.approx_cst p t in
+  l , m

types/patterns.mli

@@ -85,4 +85,4 @@ end
 val approx :
   descr ->
   Types.descr ->
-  (id * (bool * Types.Const.t option) option) list
+  id list * (id * Types.Const.t) list