[r2004-12-27 17:00:18 by afrisch] Factorization for capture and `nil

Original author: afrisch
Date: 2004-12-27 17:00:18+00:00

Makefile.distrib

@@ -155,7 +155,7 @@ OBJECTS = \
  types/sortedList.cmo types/boolean.cmo types/ident.cmo \
  types/intervals.cmo types/chars.cmo types/atoms.cmo \
  types/normal.cmo \
- types/types.cmo types/sample.cmo types/patterns.cmo types/sequence.cmo \
+ types/types.cmo types/sample.cmo types/sequence.cmo types/patterns.cmo \
  types/builtin_defs.cmo \
  \
  compile/lambda.cmo \

driver/cduce.ml

@@ -194,8 +194,10 @@ 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

types/patterns.ml

@@ -447,6 +447,100 @@ let filter_descr t p =
   IdMap.get (IdMap.map Types.Positive.solve r)
 
 
+(* Factorization of capture variables and constant patterns *)
+
+module Factorize = struct
+  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)
+
+(* 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 rec approx_nil 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_nil seen p1 (Types.cap t a1) xs) 
+	    (approx_nil seen p2 (Types.diff t a1) xs)
+      | Cap ((_,fv1,_) as p1,((_,fv2,_) as p2)) ->
+	  IdSet.cup
+	    (approx_nil seen p1 t (IdSet.cap fv1 xs))
+	    (approx_nil seen p2 t (IdSet.cap fv2 xs))
+      | Constant (_,c) when Types.Const.equal c Sequence.nil_cst -> xs
+      | Times (q1,q2) ->
+	  let xs = IdSet.cap q2.fv (IdSet.diff xs q1.fv) in
+	  approx_nil_node seen q2 (pi2 ~kind:`Normal t) xs
+      | _ -> IdSet.empty
+	  
+  and approx_nil_node seen q t xs =
+    if (NodeSet.mem q seen) 
+    then xs
+    else approx_nil (NodeSet.add q seen) q.descr t xs
+
+  let 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 var ((a,_,_) as p) t = 
+    approx_var NodeSet.empty p (Types.cap t a)
+
+  let nil ((a,_,_) as p) t = 
+    approx_nil NodeSet.empty p (Types.cap t a)
+end
+
+
+
+
 (* Normal forms for patterns and compilation *)
 
 let min (a:int) (b:int) = if a < b then a else b
@@ -636,7 +730,8 @@ module Normal = struct
       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)
+		       (* 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))
@@ -724,7 +819,6 @@ module Normal = struct
     }
     
   let nrecord lab acc l p xs =
-    assert (IdSet.equal xs (fv p));
     match lab with
       | None -> assert false
       | Some label ->
@@ -774,10 +868,12 @@ module Normal = struct
 
   let rec nnormal lab ((acc,fv,d) as p) xs =
     let xs = IdSet.cap xs fv in
+(*
     if not (IdSet.equal xs fv) then
       (Format.fprintf Format.std_formatter
 	 "ERR: p=%a  xs=%a  fv=%a@." Print.print p Print.print_xs xs Print.print_xs fv;
        exit 1);
+*)
     if Types.is_empty acc then nempty lab
     else if IdSet.is_empty xs then nconstr lab acc
     else match d with
@@ -802,15 +898,31 @@ module Normal = struct
   let print_node_list ppf pl =
     List.iter (fun p -> Format.fprintf ppf "%a;" Node.dump p) pl
 
-  let normal l t pl xs =
+  let facto f t xs pl =
     List.fold_left 
-      (fun a p -> ncap a (nnormal l (descr p) xs)) 
-      (nconstr l t) 
+      (fun vs p -> IdSet.cup vs (f (descr p) t (IdSet.cap (fv p) xs)))
+      IdSet.empty
       pl
 
-  let nnf lab (pl,t,xs) =
-    let pl = NodeSet.get pl in
-    normal lab t pl xs
+  let normal l t pl xs =
+    let a = nconstr l t in
+
+    let vs = facto Factorize.var t xs pl in
+    let xs = IdSet.diff xs vs in
+    let a = List.fold_left (fun a x -> ncap a (ncapture l x)) a vs in
+
+    let vs = facto Factorize.nil t xs pl in
+    let xs = IdSet.diff xs vs in
+    let a = List.fold_left (fun a x -> ncap a (nconstant l x Sequence.nil_cst)) a vs in
+
+    List.fold_left (fun a p -> ncap a (nnormal l (descr p) xs)) a pl
+
+  let nnf lab t0 (pl,t,xs) = 
+    let t =
+      if Types.subtype t t0 then t else Types.cap t t0 in
+(*    let ppf = Format.std_formatter in
+     Format.fprintf ppf "normal nnf=%a@." Nnf.print (pl,t,xs); *)
+    normal lab t (NodeSet.get pl) xs
     
 
 (*
@@ -1123,7 +1235,7 @@ struct
   let get_tests pl f t d post =
     let pl = Array.map (List.map f) pl in
     let lab = first_lab pl in
-    let pl = Array.map (List.map (fun (x,info) -> (Normal.nnf lab x,info))) pl
+    let pl = Array.map (List.map (fun (x,info) -> (Normal.nnf lab t x,info))) pl
     in
     (* Collect all subrequests *)
     let aux reqs (req,_) = NfSet.add req reqs in
@@ -1399,8 +1511,7 @@ struct
     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] (fv p)) pl) in
-
+	       (List.map (fun p -> Normal.nnf lab t ([p],t,fv p)) pl) in
     show ppf t pl lab;
     Format.fprintf ppf "# compiled dispatchers: %i@\n" !cur_id
 end
@@ -1435,64 +1546,6 @@ module Compile2 = struct
   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
 
@@ -1706,13 +1759,13 @@ x=(1,2)
 
  
     let approx_var p t xs f =
-      let vs = Approx.approx_var p t xs in
+      let vs = Factorize.var p t xs in
       let xs = IdSet.diff xs vs in
       let pr = f vs in
       (pr,xs)
 
     let approx_cst p t xs f =
-      let vs = Approx.approx_cst p t xs in
+      let vs = Factorize.cst p t xs in
       let xs = IdSet.diff xs (IdMap.domain vs) in
       let pr = f vs in
       (pr,xs)
@@ -2487,8 +2540,8 @@ x=(1,2)
 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
+  let l = IdSet.get (Factorize.var p t fv) in
+  let m = IdMap.get (Factorize.cst p t fv) in
   l , m