Imported Upstream version 0.2.pl2upstream/0.2.pl2

1 files changed, 217 insertions, 130 deletions

diff --git a/AAC_matcher.ml b/AAC_matcher.ml
index 47ab840..5d738e0 100644
--- a/AAC_matcher.ml
+++ b/AAC_matcher.ml
@@ -41,6 +41,8 @@ end
 module Debug = AAC_helper.Debug (Control)
 open Debug
 
+module Search = AAC_search_monad 	(* a handle *)
+
 type symbol = int
 type var = int
 type units = (symbol * symbol) list (* from AC/A symbols to the unit *)
@@ -64,7 +66,7 @@ let get_unit units op =
 let is_unit units op unit  = List.mem (op,unit) units
 
 
-open AAC_search_monad
+open Search
 
 type 'a mset = ('a * int) list
 let linear p =
@@ -126,7 +128,11 @@ module Terms : sig
 		 | TUnit of symbol
 		 | TVar of var
 
-		    
+  (** {2 Fresh variables: we provide some functions to pick some fresh variables with respect to a term}  *)
+  val fresh_var_term : t -> int
+  val fresh_var_nfterm : nf_term -> int
+
+		     
   (** {2 Constructors: we ensure that the terms are always
       normalised
      
@@ -175,9 +181,31 @@ end
       | TUnit of symbol
       | TVar of var
 
-
-
-     
+	  
+    (** {2 Picking fresh variables}  *)
+
+    (** [fresh_var_term] picks a fresh variable with respect to a term *)
+    let fresh_var_term t =
+      let rec aux = function
+    	| Dot (_,t1,t2)
+    	| Plus (_,t1,t2) -> max (aux t1) (aux t2)
+    	| Sym (_,v) -> Array.fold_left (fun acc x -> max acc (aux x)) 0 v
+    	| Var v -> assert (v >= 0); v
+    	| Unit _ -> 0
+      in
+      aux t
+	  
+    (**  [fresh_var_nfterm] picks a fresh_variable with respect to a term *)
+    let fresh_var_nfterm t =
+      let rec aux = function
+    	| TAC (_,l) -> List.fold_left (fun acc (x,_) -> max acc (aux x)) 0 l
+    	| TA (_,l)
+    	| TSym (_,l) ->  List.fold_left (fun acc x -> max acc (aux x)) 0 l
+    	| TVar v -> assert (v >= 0); v
+    	| TUnit _ -> 0
+      in
+      aux t
+	  
     (** {2 Constructors: we ensure that the terms are always
 	normalised} *)
       	
@@ -453,20 +481,6 @@ end
   
    open X
 
-   let nullifiable p =
-     let nullable = not strict in
-     let has_unit s =
-     try let _ = get_unit units s in true
-     with NoUnit -> false 
-     in
-     let rec aux = function
-       | TA (s,l) -> has_unit s && List.for_all (aux) l
-       | TAC (s,l) -> has_unit s && List.for_all (fun (x,n) -> aux x) l
-       | TSym _ -> false
-       | TVar _ -> nullable
-       | TUnit _ -> true
-     in aux p
-    
    let print_units ()=
      List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units;
      Printf.printf "\n%!"
@@ -801,7 +815,7 @@ let build_a (current : symbol)
   right_pat p >> left_pat >> (fun p -> return p)
 
 
-let conts (unit : symbol) (l : symbol list) p : t m =
+let conts (hole : t) (l : symbol list) p : t m =
   let p = t_of_term p in
   (* - aller chercher les symboles ac et les symboles a
      - construire pour chaque
@@ -813,24 +827,23 @@ let conts (unit : symbol) (l : symbol list) p : t m =
   let acc =   fail () in
   let acc = List.fold_left
     (fun acc s ->
-      acc >>| return (Plus (s,p,Unit unit))
+      acc >>| return (Plus (s,p,hole))
     ) acc ac in
   let acc =
     List.fold_left
       (fun acc s ->
-	acc >>| return (Dot (s,p,Unit unit)) >>| return (Dot (s,Unit unit,p))
+	acc >>| return (Dot (s,p,hole)) >>| return (Dot (s,hole,p))
       ) acc a
   in acc
 
    
 (**
-
     Return the same thing as subterm :
     - The size of the context
     - The context
     - A collection of substitutions (here == return Subst.empty)
 *)
-let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
+let unit_subterm (t : nf_term) (unit : symbol) (hole : t): (int * t * Subst.t m) m =
   let symbols = List.fold_left
     (fun acc (ac,u) -> if u = unit then ac :: acc else acc ) [] units
   in
@@ -846,15 +859,15 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 		(
 		  match r with
 		    | [p,1] ->
-		      positions p >>| conts unit symbols' p
+		      positions p >>| conts hole symbols' p
 		    | _ ->
-		      mk_TAC' s r >> conts unit symbols'
+		      mk_TAC' s r >> conts hole symbols'
 		) >> build_ac s l	  ))
       | TA (s,l) ->
 	let symbols' = List.filter (fun x -> x <> s) symbols in
 	(
 	  (* first the other symbols, and then the more simple case of
-	     this aprticular symbol *)
+	     this particular symbol *)
 	  a_nondet_middle l >>
 	    (fun (l,m,r) ->
 	      (* meant to break the symmetry *)
@@ -864,23 +877,23 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 		(
 		  match m with
 		    | [p] ->
-		      positions p >>| conts unit symbols' p
+		      positions p >>| conts hole symbols' p
 		    | _ ->
-		      mk_TA' s m >> conts unit symbols'
+		      mk_TA' s m >> conts hole symbols'
 		) >> build_a s l r   ))
 	>>|
 	    (
 	      if List.mem s symbols then
 		begin match l with
 		  | [a] -> assert false
-		  | [a;b] -> build_a s [a] [b] (Unit unit)
+		  | [a;b] -> build_a s [a] [b] (hole)
 		  | _ ->
 		    (* on ne construit que les elements interieurs,
 		       d'ou la disymetrie *)
 		    (Positions.a l >>
 		       (fun (left,p,right) ->
 			 if left = [] then fail () else
-			   (build_a s left right (Dot (s,Unit unit,t_of_term p)))))
+			   (build_a s left right (Dot (s,hole,t_of_term p)))))
 		end
 	      else fail ()
 	    )
@@ -894,7 +907,7 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 		return (Sym (s, Array.of_list (List.rev_append l (p::r))))		  ))
 	  >>|
 	      (
-		conts unit symbols t >>
+		conts hole symbols t >>
 		  (fun (p) ->
 	      	    let l = List.map t_of_term l in
 	      	    let r = List.map t_of_term r in
@@ -903,15 +916,15 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 	  >>|  acc
 	) l (fail())
       | TVar x -> assert false
-      | TUnit x  when x = unit -> return (Unit unit)
-      | TUnit x as t -> conts unit symbols t
+      | TUnit x  when x = unit -> return (hole)
+      | TUnit x as t -> conts hole symbols t
   in
   (positions t
    >>|
        (match t with
-	 | TSym _ -> conts unit symbols t
-	 | TAC (s,l)  -> conts unit symbols t
-	 | TA (s,l)  -> conts unit symbols t
+	 | TSym _ -> conts hole symbols t
+	 | TAC (s,l)  -> conts hole symbols t
+	 | TA (s,l)  -> conts hole symbols t
 	 | _ -> fail())
   )
   >> fun (p) -> return (Terms.size p,p,return Subst.empty)
@@ -919,7 +932,7 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 
 
 
-(************)
+			    (************)
 			    (* Matching *)
 			    (************)
 
@@ -942,8 +955,8 @@ let unit_subterm (t : nf_term) (unit : symbol) : (int * t * Subst.t m) m =
 
 *)
 
-let matching  =  
-  let rec matching env (p : nf_term) (t: nf_term) : Subst.t AAC_search_monad.m=    
+let matching  :  Subst.t  -> nf_term -> nf_term -> Subst.t Search.m=  
+  let rec matching env (p : nf_term) (t: nf_term) : Subst.t Search.m=    
     match p with
       | TAC (s,l) ->
 	  let l = linear l in
@@ -1040,11 +1053,55 @@ let matching  =
     fun env l r ->
       let _ = debug (Printf.sprintf "pattern :%s\nterm    :%s\n%!" (Terms.sprint_nf_term l) (Terms.sprint_nf_term r)) in
       let m = matching env l r  in
-      let _ = debug (Printf.sprintf "count %i" (AAC_search_monad.count m)) in
+      let _ = debug (Printf.sprintf "count %i" (Search.count m)) in
 	m
 
 
+(** [unitifiable p : Subst.t m] *)
+let unitifiable p : (symbol * Subst.t m) m = 
+  let m = List.fold_left 
+    (fun acc (_,unit) -> acc >>| 
+	let m =  matching Subst.empty p (mk_TUnit unit) in 
+	if Search.is_empty m then 
+	  fail ()
+	else 
+	  begin 
+	    return (unit,m)
+	  end
+    ) (fail ()) units
+  in 
+  m
+;;
+
+let nullifiable p =
+  let nullable = not strict in
+  let has_unit s =
+    try let _ = get_unit units s in true
+    with NoUnit -> false 
+  in
+  let rec aux = function
+    | TA (s,l) -> has_unit s && List.for_all (aux) l
+    | TAC (s,l) -> has_unit s && List.for_all (fun (x,n) -> aux x) l
+    | TSym _ -> false
+    | TVar _ -> nullable
+    | TUnit _ -> true
+  in aux p
 
+let unit_warning p ~nullif ~unitif =
+  assert ((Search.is_empty unitif) || nullif);
+  if not (Search.is_empty unitif)
+  then
+    begin
+      Pp.msg_warning
+	(Pp.str
+	   "[aac_tactics] This pattern can be instanciated to match units, some solutions can be missing");
+    end
+
+;;
+
+  
+
+  
 (***********)
 (* Subterm *)
 (***********)
@@ -1077,101 +1134,131 @@ let matching  =
     serve as heuristics to return "interesting" matchings
 *)
 
-let return_non_empty raw_p m =
-  if is_empty m
-  then
-    fail ()
-  else
-    return (raw_p ,m)
-
-let subterm  (raw_p:t) (raw_t:t): (int * t * Subst.t m) m=
-  let _ = debug (String.make 40 '=') in
-  let p = term_of_t units raw_p in
-  let t = term_of_t units raw_t in    
-  let _ =
-    if nullifiable  p
+  let return_non_empty raw_p m =
+    if is_empty m
     then
-      Pp.msg_warning
-	(Pp.str
-	   "[aac_tactics] This pattern might be nullifiable, some solutions can be missing");
-  in
-
-  let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term p)) in
-  let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term t)) in
-  let filter_right current right (p,m) = 
-    if right = []
-    then return (p,m)
-    else 
-      mk_TAC' current right >>
-	fun t -> return (Plus (current,p,t_of_term t),m)
-  in
-  let filter_middle current left right (p,m) =
-    let right_pat p =
+      fail ()
+    else
+      return (raw_p ,m)
+
+  let subterm  (raw_p:t) (raw_t:t): (int * t * Subst.t m) m=
+    let _ = debug (String.make 40 '=') in
+    let p = term_of_t units raw_p in
+    let t = term_of_t units raw_t in    
+    let nullif = nullifiable p in 
+    let unitif = unitifiable p in 
+    let _ = unit_warning p ~nullif ~unitif in
+    let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term p)) in
+    let _ = debug (Printf.sprintf "%s" (Terms.sprint_nf_term t)) in
+    let filter_right current right (p,m) = 
       if right = []
-      then return p
-      else
-	mk_TA' current right >>
-	  fun t -> return (Dot (current,p,t_of_term t))
+      then return (p,m)
+      else 
+	mk_TAC' current right >>
+	  fun t -> return (Plus (current,p,t_of_term t),m)
     in
-    let left_pat p=
-      if left = []
-      then return p
-      else
-	mk_TA' current left >>
-	  fun t -> return (Dot (current,t_of_term t,p))
-    in  
-    right_pat p >> left_pat >> (fun p -> return (p,m))
-  in
-  let rec subterm (t:nf_term) : (t * Subst.t m) m=
-    match t with
-      | TAC (s,l) ->
-	((ac_nondet_split_raw l) >>
-	    (fun (left,right) ->
-	      (subterm_AC s left) >> (filter_right s right)
-	    ))
-      | TA (s,l) ->
-	(a_nondet_middle l) >>
-	  (fun (left, middle, right) ->
-	    (subterm_A s middle) >>
-	      (filter_middle s left right)
-	  )
-      | TSym (s, l) ->
-	let init =
-	  return_non_empty raw_p (matching  Subst.empty p t)
-	in
-	tri_fold (fun acc l t r ->
-	  ((subterm  t) >>
-	      (fun (p,m) ->
-		let l = List.map t_of_term l in
-		let r = List.map t_of_term r in
-		let p = Sym (s, Array.of_list (List.rev_append l (p::r))) in
-		return (p,m)
-	      )) >>| acc
-	) l init
-      | TVar x -> assert false
-      | TUnit s -> fail ()
-	
-  and subterm_AC s tl   =
-    match tl with
-	[x,1] -> subterm  x
-      | _ ->
-	mk_TAC' s tl >> fun t ->
-	  return_non_empty raw_p (matching  Subst.empty p t)
-  and subterm_A s  tl =
-    match tl with
-	[x] -> subterm  x
-      | _ ->
-	mk_TA' s tl >>
-	  fun t ->
+    let filter_middle current left right (p,m) =
+      let right_pat p =
+	if right = []
+	then return p
+	else
+	  mk_TA' current right >>
+	    fun t -> return (Dot (current,p,t_of_term t))
+      in
+      let left_pat p=
+	if left = []
+	then return p
+	else
+	  mk_TA' current left >>
+	    fun t -> return (Dot (current,t_of_term t,p))
+      in  
+      right_pat p >> left_pat >> (fun p -> return (p,m))
+    in
+    let rec subterm (t:nf_term) : (t * Subst.t m) m=
+      match t with
+	| TAC (s,l) ->
+	  ((ac_nondet_split_raw l) >>
+	      (fun (left,right) ->
+		(subterm_AC s left) >> (filter_right s right)
+	      ))
+	| TA (s,l) ->
+	  (a_nondet_middle l) >>
+	    (fun (left, middle, right) ->
+	      (subterm_A s middle) >>
+		(filter_middle s left right)
+	    )
+	| TSym (s, l) ->
+	  let init =
 	    return_non_empty raw_p (matching  Subst.empty p t)
-  in
-  match p with
-    | TUnit x ->
-      unit_subterm t x
-    | _ -> (subterm t >> fun (p,m) -> return (Terms.size p,p,m))
+	  in
+	  tri_fold (fun acc l t r ->
+	    ((subterm  t) >>
+		(fun (p,m) ->
+		  let l = List.map t_of_term l in
+		  let r = List.map t_of_term r in
+		  let p = Sym (s, Array.of_list (List.rev_append l (p::r))) in
+		  return (p,m)
+		)) >>| acc
+	  ) l init
+	| TVar x -> assert false
+	(* this case is superseded by the later disjunction *)
+	| TUnit s -> fail () 		
+	  
+    and subterm_AC s tl   =
+      match tl with
+	  [x,1] -> subterm  x
+	| _ ->
+	  mk_TAC' s tl >> fun t ->
+	    return_non_empty raw_p (matching  Subst.empty p t)
+    and subterm_A s  tl =
+      match tl with
+	  [x] -> subterm  x
+	| _ ->
+	  mk_TA' s tl >>
+	    fun t ->
+	      return_non_empty raw_p (matching  Subst.empty p t)
+    in
+    match p with
+      | TUnit unit -> unit_subterm t unit raw_p
+      | _ when not (Search.is_empty unitif) ->
+	let unit_matches = 
+	  Search.fold 
+	    (fun (unit,inst) acc -> 
+	      Search.fold 
+		(fun subst acc' ->
+		 let m = unit_subterm t unit (Subst.instantiate subst raw_p) 
+		 in 
+		 m>>| acc'
+		)
+		inst
+		acc      
+	    ) 
+	    unitif 
+	    (fail ())
+	in
+	let nullifies (t : Subst.t) = 
+	  List.for_all (fun (_,x) -> 
+	    List.exists (fun (_,y) -> Unit y = x ) units 
+	  ) (Subst.to_list t)
+	in 
+	let nonunit_matches = 
+	  subterm t >> 
+	    (
+	      fun (p,m) -> 
+		let m = Search.filter (fun subst -> not( nullifies subst)) m in 
+		if Search.is_empty m 
+		then fail ()
+	      else return (Terms.size p,p,m)
+	    )
+	in
+	  unit_matches >>| nonunit_matches  
+	     
+      | _ -> (subterm t >> fun (p,m) -> return (Terms.size p,p,m))
+
 
  end
 
+
 (* The functions we export, handlers for the previous ones. Some debug
    information also *)
 let subterm ?(strict = false) units raw t =
@@ -1183,7 +1270,7 @@ let subterm ?(strict = false) units raw t =
   let sols = time (M.subterm raw) t "%fs spent in subterm (including matching)\n" in
     debug
       (Printf.sprintf "%i possible solution(s)\n"
-	 (AAC_search_monad.fold (fun (_,_,envm) acc -> count envm + acc) sols 0));
+	 (Search.fold (fun (_,_,envm) acc -> count envm + acc) sols 0));
     sols