From 9216cffaaa1ef137ef5bdb5b290a930cc6198850 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 21 Feb 2011 17:34:06 +0100 Subject: Imported Upstream version 0.2.pl2 --- AAC_matcher.ml | 347 ++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 217 insertions(+), 130 deletions(-) (limited to 'AAC_matcher.ml') 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 -- cgit v1.2.3