diff options
Diffstat (limited to 'AAC_matcher.ml')
-rw-r--r-- | AAC_matcher.ml | 1293 |
1 files changed, 0 insertions, 1293 deletions
diff --git a/AAC_matcher.ml b/AAC_matcher.ml deleted file mode 100644 index 5d738e0..0000000 --- a/AAC_matcher.ml +++ /dev/null @@ -1,1293 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** This module defines our matching functions, modulo associativity - and commutativity (AAC). - - The basic idea is to find a substitution [env] such that the - pattern [p] instantiated by [env] is equal to [t] modulo AAC. - - We proceed by structural decomposition of the pattern, and try all - possible non-deterministic split of the subject when needed. The - function {!matcher} is limited to top-level matching, that is, the - subject must make a perfect match against the pattern ([x+x] do - not match [a+a+b] ). We use a search monad {!Search} to perform - non-deterministic splits in an almost transparent way. We also - provide a function {!subterm} for finding a match that is a - subterm modulo AAC of the subject. Therefore, we are able to solve - the aforementioned case [x+x] against [a+b+a]. - - This file is structured as follows. First, we define the search - monad. Then,we define the two representations of terms (one - representing the AST, and one in normal form ), and environments - from variables to terms. Then, we use these parts to solve - matching problem. Finally, we wrap this function {!matcher} into - {!subterm} -*) - - -module Control = -struct - let debug = false - let time = false - let printing = false -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 *) -type ext_units = - { - unit_for : units; - is_ac : (symbol * bool) list - } - -let print_units units= - List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units; - Printf.printf "\n%!" - -exception NoUnit - -let get_unit units op = - try List.assoc op units - with - | Not_found -> raise NoUnit - -let is_unit units op unit = List.mem (op,unit) units - - -open Search - -type 'a mset = ('a * int) list -let linear p = - let rec ncons t l = function - | 0 -> l - | n -> t::ncons t l (n-1) - in - let rec aux = function - [ ] -> [] - | (t,n)::q -> let q = aux q in - ncons t q n - in aux p - - - -(** The module {!Terms} defines two different types for expressions. - - - a public type {!Terms.t} that represent abstract syntax trees of - expressions with binary associative (and commutative) operators - - - a private type {!Terms.nf_term} that represent an equivalence - class for terms that are equal modulo AAC. The constructions - functions on this type ensure the property that the term is in - normal form (that is, no sum can appear as a subterm of the same - sum, no trailing units, etc...). - -*) - -module Terms : sig - - (** {1 Abstract syntax tree of terms} - - Terms represented using this datatype are representation of the - AST of an expression. *) - - type t = - Dot of (symbol * t * t) - | Plus of (symbol * t * t) - | Sym of (symbol * t array) - | Var of var - | Unit of symbol - - val equal_aac : units -> t -> t -> bool - val size: t -> int - - (** {1 Terms in normal form} - - A term in normal form is the canonical representative of the - equivalence class of all the terms that are equal modulo - Associativity and Commutativity. Outside the {!AAC_matcher} module, - one does not need to access the actual representation of this - type. *) - - - type nf_term = private - | TAC of symbol * nf_term mset - | TA of symbol * nf_term list - | TSym of symbol * nf_term list - | 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 - - braibant - Fri 27 Aug 2010, 15:11 - Moreover, we assure that we will not build empty sums or empty - products, leaving this task to the caller function. - } - *) - val mk_TAC : units -> symbol -> nf_term mset -> nf_term - val mk_TA : units -> symbol -> nf_term list -> nf_term - val mk_TSym : symbol -> nf_term list -> nf_term - val mk_TVar : var -> nf_term - val mk_TUnit : symbol -> nf_term - - (** {2 Comparisons} *) - val nf_term_compare : nf_term -> nf_term -> int - val nf_equal : nf_term -> nf_term -> bool - - (** {2 Printing function} *) - val sprint_nf_term : nf_term -> string - - (** {2 Conversion functions} *) - val term_of_t : units -> t -> nf_term - val t_of_term : nf_term -> t (* we could return the units here *) -end - = struct - - type t = - Dot of (symbol * t * t) - | Plus of (symbol * t * t) - | Sym of (symbol * t array) - | Var of var - | Unit of symbol - - let rec size = function - | Dot (_,x,y) - | Plus (_,x,y) -> size x+ size y + 1 - | Sym (_,v)-> Array.fold_left (fun acc x -> size x + acc) 1 v - | _ -> 1 - - - type nf_term = - | TAC of symbol * nf_term mset - | TA of symbol * nf_term list - | TSym of symbol * nf_term list - | 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} *) - - (** {3 Pre constructors : These constructors ensure that sums and - products are not degenerated (no trailing units)} *) - let mk_TAC' units (s : symbol) l = match l with - | [] -> TUnit (get_unit units s ) - | [_,0] -> assert false - | [t,1] -> t - | _ -> TAC (s,l) - let mk_TA' units (s : symbol) l = match l with - | [] -> TUnit (get_unit units s ) - | [t] -> t - | _ -> TA (s,l) - - - (** {2 Comparison} *) - - let nf_term_compare = Pervasives.compare - let nf_equal a b = - a = b - - (** [merge_ac comp l1 l2] merges two lists of terms with coefficients - into one. Terms that are equal modulo the comparison function - [comp] will see their arities added. *) - - (* This function could be improved by the use of sorted msets *) - let merge_ac (compare : 'a -> 'a -> int) (l : 'a mset) (l' : 'a mset) : 'a mset = - let rec aux l l'= - match l,l' with - | [], _ -> l' - | _, [] -> l - | (t,tar)::q, (t',tar')::q' -> - begin match compare t t' with - | 0 -> ( t,tar+tar'):: aux q q' - | -1 -> (t, tar):: aux q l' - | _ -> (t', tar'):: aux l q' - end - in aux l l' - - (** [merge_map f l] uses the combinator [f] to combine the head of the - list [l] with the merge_maped tail of [l] *) - let rec merge_map (f : 'a -> 'b list -> 'b list) (l : 'a list) : 'b list = - match l with - | [] -> [] - | t::q -> f t (merge_map f q) - - - (** This function has to deal with the arities *) - let rec merge (l : nf_term mset) (l' : nf_term mset) : nf_term mset= - merge_ac nf_term_compare l l' - - let extract_A units s t = - match t with - | TA (s',l) when s' = s -> l - | TUnit u when is_unit units s u -> [] - | _ -> [t] - - let extract_AC units s (t,ar) : nf_term mset = - match t with - | TAC (s',l) when s' = s -> List.map (fun (x,y) -> (x,y*ar)) l - | TUnit u when is_unit units s u -> [] - | _ -> [t,ar] - - - (** {3 Constructors of {!nf_term}}*) - let mk_TAC units (s : symbol) (l : (nf_term *int) list) = - mk_TAC' units s - (merge_map (fun u l -> merge (extract_AC units s u) l) l) - let mk_TA units s l = - mk_TA' units s - (merge_map (fun u l -> (extract_A units s u) @ l) l) - let mk_TSym s l = TSym (s,l) - let mk_TVar v = TVar v - let mk_TUnit s = TUnit s - - - (** {2 Printing function} *) - let print_binary_list (single : 'a -> string) - (unit : string) - (binary : string -> string -> string) (l : 'a list) = - let rec aux l = - match l with - [] -> unit - | [t] -> single t - | t::q -> - let r = aux q in - Printf.sprintf "%s" (binary (single t) r) - in - aux l - - let print_symbol s = - match s with - | s, None -> Printf.sprintf "%i" s - | s , Some u -> Printf.sprintf "%i(unit %i)" s u - - let sprint_ac (single : 'a -> string) (l : 'a mset) = - (print_binary_list - (fun (x,t) -> - if t = 1 - then single x - else Printf.sprintf "%i*%s" t (single x) - ) - "0" - (fun x y -> x ^ " , " ^ y) - l - ) - - let print_symbol single s l = - match l with - [] -> Printf.sprintf "%i" s - | _ -> - Printf.sprintf "%i(%s)" - s - (print_binary_list single "" (fun x y -> x ^ "," ^ y) l) - - - let print_ac single s l = - Printf.sprintf "[%s:AC]{%s}" - (string_of_int s ) - (sprint_ac - single - l - ) - - let print_a single s l = - Printf.sprintf "[%s:A]{%s}" - (string_of_int s) - (print_binary_list single "1" (fun x y -> x ^ " , " ^ y) l) - - let rec sprint_nf_term = function - | TSym (s,l) -> print_symbol sprint_nf_term s l - | TAC (s,l) -> print_ac sprint_nf_term s l - | TA (s,l) -> print_a sprint_nf_term s l - | TVar v -> Printf.sprintf "x%i" v - | TUnit s -> Printf.sprintf "unit%i" s - - - - - (** {2 Conversion functions} *) - - (* rebuilds a tree out of a list, under the assumption that the list is not empty *) - let rec binary_of_list f comb l = - let l = List.rev l in - let rec aux = function - | [] -> assert false - | [t] -> f t - | t::q -> comb (aux q) (f t) - in - aux l - - let term_of_t units : t -> nf_term = - let rec term_of_t = function - | Dot (s,l,r) -> - let l = term_of_t l in - let r = term_of_t r in - mk_TA units s [l;r] - | Plus (s,l,r) -> - let l = term_of_t l in - let r = term_of_t r in - mk_TAC units s [l,1;r,1] - | Unit x -> - mk_TUnit x - | Sym (s,t) -> - let t = Array.to_list t in - let t = List.map term_of_t t in - mk_TSym s t - | Var i -> - mk_TVar ( i) - in - term_of_t - - let rec t_of_term : nf_term -> t = function - | TAC (s,l) -> - (binary_of_list - t_of_term - (fun l r -> Plus ( s,l,r)) - (linear l) - ) - | TA (s,l) -> - (binary_of_list - t_of_term - (fun l r -> Dot ( s,l,r)) - l - ) - | TSym (s,l) -> - let v = Array.of_list l in - let v = Array.map (t_of_term) v in - Sym ( s,v) - | TVar x -> Var x - | TUnit s -> Unit s - - - let equal_aac units x y = - nf_equal (term_of_t units x) (term_of_t units y) - end - - (** Terms environments defined as association lists from variables to - terms in normal form {! Terms.nf_term} *) - module Subst : sig - type t - - val find : t -> var -> Terms.nf_term option - val add : t -> var -> Terms.nf_term -> t - val empty : t - val instantiate : t -> Terms.t -> Terms.t - val sprint : t -> string - val to_list : t -> (var*Terms.t) list - end - = - struct - open Terms - - (** Terms environments, with nf_terms, to avoid costly conversions - of {!Terms.nf_terms} to {!Terms.t}, that will be mostly discarded*) - type t = (var * nf_term) list - - let find : t -> var -> nf_term option = fun t x -> - try Some (List.assoc x t) with | _ -> None - let add t x v = (x,v) :: t - let empty = [] - - let sprint (l : t) = - match l with - | [] -> Printf.sprintf "Empty environment\n" - | _ -> - let s = List.fold_left - (fun acc (x,y) -> - Printf.sprintf "%sX%i -> %s\n" - acc - x - (sprint_nf_term y) - ) - "" - (List.rev l) in - Printf.sprintf "%s\n%!" s - - - - (** [instantiate] is an homomorphism except for the variables*) - let instantiate (t: t) (x:Terms.t) : Terms.t = - let rec aux = function - | Unit _ as x -> x - | Sym (s,t) -> Sym (s,Array.map aux t) - | Plus (s,l,r) -> Plus (s, aux l, aux r) - | Dot (s,l,r) -> Dot (s, aux l, aux r) - | Var i -> - begin match find t i with - | None -> Util.error "aac_tactics: instantiate failure" - | Some x -> t_of_term x - end - in aux x - - let to_list t = List.map (fun (x,y) -> x,Terms.t_of_term y) t - end - - (******************) - (* MATCHING UTILS *) - (******************) - - open Terms - - (** Since most of the folowing functions require an extra parameter, - the units, we package them in a module. This functor will then be - applied to a module containing the units, in the exported - functions. *) - module M (X : sig - val units : units - val is_ac : (symbol * bool) list - val strict : bool (* variables cannot be instantiated with units *) - end) = struct - - open X - - let print_units ()= - List.iter (fun (op,unit) -> Printf.printf "%i %i\t" op unit) units; - Printf.printf "\n%!" - - let mk_TAC s l = mk_TAC units s l - let mk_TA s l = mk_TA units s l - let mk_TAC' s l = - try return( mk_TAC s l) - with _ -> fail () - let mk_TA' s l = - try return( mk_TA s l) - with _ -> fail () - - (** First, we need to be able to perform non-deterministic choice of - term splitting to satisfy a pattern. Indeed, we want to show that: - (x+a*b)*c <= a*b*c - *) - let a_nondet_split_raw t : ('a list * 'a list) m = - let rec aux l l' = - match l' with - | [] -> - return ( l,[]) - | t::q -> - return ( l,l' ) - >>| aux (l @ [t]) q - in - aux [] t - - (** Same as the previous [a_nondet_split], but split the list in 3 - parts *) - let a_nondet_middle t : ('a list * 'a list * 'a list) m = - a_nondet_split_raw t >> - (fun (left, right) -> - a_nondet_split_raw left >> - (fun (left, middle) -> return (left, middle, right)) - ) - - (** Non deterministic splits of ac lists *) - let dispatch f n = - let rec aux k = - if k = 0 then return (f n 0) - else return (f (n-k) k) >>| aux (k-1) - in - aux (n ) - - let add_with_arith x ar l = - if ar = 0 then l else (x,ar) ::l - - let ac_nondet_split_raw (l : 'a mset) : ('a mset * 'a mset) m = - let rec aux = function - | [] -> return ([],[]) - | (t,tar)::q -> - aux q - >> - (fun (left,right) -> - dispatch (fun arl arr -> - add_with_arith t arl left, - add_with_arith t arr right - ) - tar - ) - in - aux l - - let a_nondet_split current t : (nf_term * nf_term list) m= - a_nondet_split_raw t - >> - (fun (l,r) -> - if strict && (l=[]) - then fail() - else - mk_TA' current l >> - fun t -> return (t, r) - ) - - let ac_nondet_split current t : (nf_term * nf_term mset) m= - ac_nondet_split_raw t - >> - (fun (l,r) -> - if strict && (l=[]) - then fail() - else - mk_TAC' current l >> - fun t -> return (t, r) - ) - - - (** Try to affect the variable [x] to each left factor of [t]*) - let var_a_nondet_split env current x t = - a_nondet_split current t - >> - (fun (t,res) -> - return ((Subst.add env x t), res) - ) - - (** Try to affect variable [x] to _each_ subset of t. *) - let var_ac_nondet_split (current: symbol) env (x : var) (t : nf_term mset) : (Subst.t * (nf_term mset)) m = - ac_nondet_split current t - >> - (fun (t,res) -> - return ((Subst.add env x t), res) - ) - - (** See the term t as a given AC symbol. Unwrap the first constructor - if necessary *) - let get_AC (s : symbol) (t : nf_term) : (nf_term *int) list = - match t with - | TAC (s',l) when s' = s -> l - | TUnit u when is_unit units s u -> [] - | _ -> [t,1] - - (** See the term t as a given A symbol. Unwrap the first constructor - if necessary *) - let get_A (s : symbol) (t : nf_term) : nf_term list = - match t with - | TA (s',l) when s' = s -> l - | TUnit u when is_unit units s u -> [] - | _ -> [t] - - (** See the term [t] as an symbol [s]. Fail if it is not such - symbol. *) - let get_Sym s t = - match t with - | TSym (s',l) when s' = s -> return l - | _ -> fail () - - (*************) - (* A Removal *) - (*************) - - (** We remove the left factor v in a term list. This function runs - linearly with respect to the size of the first pattern symbol *) - - let left_factor current (v : nf_term) (t : nf_term list) = - let rec aux a b = - match a,b with - | t::q , t' :: q' when nf_equal t t' -> aux q q' - | [], q -> return q - | _, _ -> fail () - in - match v with - | TA (s,l) when s = current -> aux l t - | TUnit u when is_unit units current u -> return t - | _ -> - begin match t with - | [] -> fail () - | t::q -> - if nf_equal v t - then return q - else fail () - end - - - (**************) - (* AC Removal *) - (**************) - - (** {!pick_sym} gather all elements of a list that satisfies a - predicate, and combine them with the residual of the list. That - is, each element of the residual contains exactly one element less - than the original term. - - TODO : This function not as efficient as it could be, using a - proper data-structure *) - - let pick_sym (s : symbol) (t : nf_term mset ) = - let rec aux front back = - match back with - | [] -> fail () - | (t,tar)::q -> - begin match t with - | TSym (s',v') when s = s' -> - let back = - if tar > 1 - then (t,tar -1) ::q - else q - in - return (v' , List.rev_append front back ) - >>| aux ((t,tar)::front) q - | _ -> aux ((t,tar)::front) q - end - in - aux [] t - - - - (** We have to check if we are trying to remove a unit from a term. Could also be located in Terms*) - let is_unit_AC s t = - try nf_equal t (mk_TAC s []) - with | NoUnit -> false - - let is_same_AC s t : nf_term mset option= - match t with - TAC (s',l) when s = s' -> Some l - | _ -> None - - (** We want to remove the term [v] from the term list [t] under an AC - symbol *) - let single_AC_factor (s : symbol) (v : nf_term) v_ar (t : nf_term mset) : (nf_term mset) m = - let rec aux front back = - match back with - | [] -> fail () - | (t,tar)::q -> - begin - if nf_equal v t - then - match () with - | _ when tar < v_ar -> fail () - | _ when tar = v_ar -> return (List.rev_append front q) - | _ -> return (List.rev_append front ((t,tar-v_ar)::q)) - else - aux ((t,tar) :: front) q - end - in - if is_unit_AC s v - then - return t - else - aux [] t - - (* Remove a constant from a mset. If this constant is also a mset for - the same symbol, we remove every elements, one at a time (and we do - care of the arities) *) - let factor_AC (s : symbol) (v: nf_term) (t : nf_term mset) : ( nf_term mset ) m = - match is_same_AC s v with - | None -> single_AC_factor s v 1 t - | Some l -> - (* We are trying to remove an AC factor *) - List.fold_left (fun acc (v,v_ar) -> - acc >> (single_AC_factor s v v_ar) - ) - (return t) - l - - -(** [tri_fold f l acc] folds on the list [l] and give to f the - beginning of the list in reverse order, the considered element, and - the last part of the list - - as an exemple, on the list [1;2;3;4], we get the trace - f () [] 1 [2; 3; 4] - f () [1] 2 [3; 4] - f () [2;1] 3 [ 4] - f () [3;2;1] 4 [] - - it is the duty of the user to reverse the front if needed -*) - -let tri_fold f (l : 'a list) (acc : 'b)= match l with - [] -> acc - | _ -> - let _,_,acc = List.fold_left (fun acc (t : 'a) -> - let l,r,acc = acc in - let r = List.tl r in - t::l,r,f acc l t r - ) ([], l,acc) l - in acc - -(* let test = tri_fold (fun acc l t r -> (l,t,r) :: acc) [1;2;3;4] [] *) - - - - (*****************************) - (* ENUMERATION DES POSITIONS *) - (*****************************) - - -(** The pattern is a unit: we need to try to make it appear at each - position. We do not need to go further with a real matching, since - the match should be trivial. Hence, we proceed recursively to - enumerate all the positions. *) - -module Positions = struct - - - let ac (l: 'a mset) : ('a mset * 'a )m = - let rec aux = function - | [] -> assert false - | [t,1] -> return ([],t) - | [t,tar] -> return ([t,tar -1],t) - | (t,tar) as h :: q -> - (aux q >> (fun (c,x) -> return (h :: c,x))) - >>| (if tar > 1 then return ((t,tar-1) :: q,t) else return (q,t)) - in - aux l - - let ac' current (l: 'a mset) : ('a mset * 'a )m = - ac_nondet_split_raw l >> - (fun (l,r) -> - if l = [] || r = [] - then fail () - else - mk_TAC' current r >> - fun t -> return (l, t) - ) - - let a (l : 'a list) : ('a list * 'a * 'a list) m = - let rec aux left right : ('a list * 'a * 'a list) m = - match right with - | [] -> assert false - | [t] -> return (left,t,[]) - | t::q -> - aux (left@[t]) q - >>| return (left,t,q) - in - aux [] l -end - -let build_ac (current : symbol) (context : nf_term mset) (p : t) : t m= - if context = [] - then return p - else - mk_TAC' current context >> - fun t -> return (Plus (current,t_of_term t,p)) - -let build_a (current : symbol) - (left : nf_term list) (right : nf_term list) (p : t) : t 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) - - -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 - * * + - / \ / \ / \ - 1 p p 1 p 1 - *) - let ac,a = List.partition (fun s -> List.assoc s is_ac) l in - let acc = fail () in - let acc = List.fold_left - (fun acc s -> - acc >>| return (Plus (s,p,hole)) - ) acc ac in - let acc = - List.fold_left - (fun acc s -> - 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) (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 - (* make a unit appear at each strict sub-position of the term*) - let rec positions (t : nf_term) : t m = - match t with - (* with a final unit at the end *) - | TAC (s,l) -> - let symbols' = List.filter (fun x -> x <> s) symbols in - ( - ac_nondet_split_raw l >> - (fun (l,r) -> if l = [] || r = [] then fail () else - ( - match r with - | [p,1] -> - positions p >>| conts hole symbols' p - | _ -> - 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 particular symbol *) - a_nondet_middle l >> - (fun (l,m,r) -> - (* meant to break the symmetry *) - if (l = [] && r = []) - then fail () - else - ( - match m with - | [p] -> - positions p >>| conts hole symbols' p - | _ -> - 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] (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,hole,t_of_term p))))) - end - else fail () - ) - - | TSym (s,l) -> - tri_fold (fun acc l t r -> - ((positions t) >> - (fun (p) -> - let l = List.map t_of_term l in - let r = List.map t_of_term r in - return (Sym (s, Array.of_list (List.rev_append l (p::r)))) )) - >>| - ( - conts hole symbols t >> - (fun (p) -> - let l = List.map t_of_term l in - let r = List.map t_of_term r in - return (Sym (s, Array.of_list (List.rev_append l (p::r)))) ) - ) - >>| acc - ) l (fail()) - | TVar x -> assert false - | TUnit x when x = unit -> return (hole) - | TUnit x as t -> conts hole symbols t - in - (positions t - >>| - (match t with - | 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) - - - - - (************) - (* Matching *) - (************) - - - -(** {!matching} is the generic matching judgement. Each time a - non-deterministic split is made, we have to come back to this one. - - {!matchingSym} is used to match two applications that have the - same (free) head-symbol. - - {!matchingAC} is used to match two sums (with the subtlety that - [x+y] matches [f a] which is a function application or [a*b] which - is a product). - - {!matchingA} is used to match two products (with the subtlety that - [x*y] matches [f a] which is a function application, or [a+b] - which is a sum). - - -*) - -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 - matchingAC env s l (get_AC s t) - | TA (s,l) -> - matchingA env s l (get_A s t) - | TSym (s,l) -> - (get_Sym s t) - >> (fun t -> matchingSym env l t) - | TVar x -> - begin match Subst.find env x with - | None -> return (Subst.add env x t) - | Some v -> if nf_equal v t then return env else fail () - end - | TUnit s -> - if nf_equal p t then return env else fail () - and - matchingAC (env : Subst.t) (current : symbol) (l : nf_term list) (t : (nf_term *int) list) = - match l with - | TSym (s,v):: q -> - pick_sym s t - >> (fun (v',t') -> - matchingSym env v v' - >> (fun env -> matchingAC env current q t')) - - | TAC (s,v)::q when s = current -> - assert false - | TVar x:: q -> (* This is an optimization *) - begin match Subst.find env x with - | None -> - (var_ac_nondet_split current env x t) - >> (fun (env,residual) -> matchingAC env current q residual) - | Some v -> - (factor_AC current v t) - >> (fun residual -> matchingAC env current q residual) - end - | TUnit s as v :: q -> (* this is an optimization *) - (factor_AC current v t) >> - (fun residual -> matchingAC env current q residual) - | h :: q ->(* PAC =/= curent or PA or unit for this symbol*) - (ac_nondet_split current t) - >> - (fun (t,right) -> - matching env h t - >> - ( - fun env -> - matchingAC env current q right - ) - ) - | [] -> if t = [] then return env else fail () - and - matchingA (env : Subst.t) (current : symbol) (l : nf_term list) (t : nf_term list) = - match l with - | TSym (s,v) :: l -> - begin match t with - | TSym (s',v') :: r when s = s' -> - (matchingSym env v v') - >> (fun env -> matchingA env current l r) - | _ -> fail () - end - | TA (s,v) :: l when s = current -> - assert false - | TVar x :: l -> - begin match Subst.find env x with - | None -> - debug (Printf.sprintf "var %i (%s)" x - (let b = Buffer.create 21 in List.iter (fun t -> Buffer.add_string b ( Terms.sprint_nf_term t)) t; Buffer.contents b )); - var_a_nondet_split env current x t - >> (fun (env,residual)-> debug (Printf.sprintf "pl %i %i" x(List.length residual)); matchingA env current l residual) - | Some v -> - (left_factor current v t) - >> (fun residual -> matchingA env current l residual) - end - | TUnit s as v :: q -> (* this is an optimization *) - (left_factor current v t) >> - (fun residual -> matchingA env current q residual) - | h :: l -> - a_nondet_split current t - >> (fun (t,r) -> - matching env h t - >> (fun env -> matchingA env current l r) - ) - | [] -> if t = [] then return env else fail () - and - matchingSym (env : Subst.t) (l : nf_term list) (t : nf_term list) = - List.fold_left2 - (fun acc p t -> acc >> (fun env -> matching env p t)) - (return env) - l - t - - in - 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" (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 *) -(***********) - - - -(** [subterm] solves a sub-term pattern matching. - - This function is more high-level than {!matcher}, thus takes {!t} - as arguments rather than terms in normal form {!nf_term}. - - We use three mutually recursive functions {!subterm}, - {!subterm_AC}, {!subterm_A} to find the matching subterm, making - non-deterministic choices to split the term into a context and an - intersting sub-term. Intuitively, the only case in which we have to - go in depth is when we are left with a sub-term that is atomic. - - Indeed, rewriting [H: b = c |- a+b+a = a+a+c], we do not want to - find recursively the sub-terms of [a+b] and [b+a], since they will - overlap with the sub-terms of [a+b+a]. - - We rebuild the context on the fly, leaving the variables in the - pattern uninstantiated. We do so in order to allow interaction - with the user, to choose the env. - - Strange patterms like x*y*x can be instanciated by nothing, inside - a product. Therefore, we need to check that all the term is not - going into the context. With proper support for interaction with - the user, we should lift these tests. However, at the moment, they - 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 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,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 = - 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 - 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 = - let module M = M (struct - let is_ac = units.is_ac - let units = units.unit_for - let strict = strict - end) in - let sols = time (M.subterm raw) t "%fs spent in subterm (including matching)\n" in - debug - (Printf.sprintf "%i possible solution(s)\n" - (Search.fold (fun (_,_,envm) acc -> count envm + acc) sols 0)); - sols - - -let matcher ?(strict = false) units p t = - let module M = M (struct - let is_ac = units.is_ac - let units = units.unit_for - let strict = false - end) in - let units = units.unit_for in - let sols = time - (fun (p,t) -> - let p = (Terms.term_of_t units p) in - let t = (Terms.term_of_t units t) in - M.matching Subst.empty p t) (p,t) - "%fs spent in the matcher\n" - in - debug (Printf.sprintf "%i solutions\n" (count sols)); - sols - |