diff --git a/src/basics.ml b/src/basics.ml index a2dd27b98..9f1a6baf5 100644 --- a/src/basics.ml +++ b/src/basics.ml @@ -112,6 +112,13 @@ let is_symb : sym -> term -> bool = fun s t -> | Symb(r,_) -> r == s | _ -> false +(** [get_symb t] returns [Some s] if [t] is of the form [Symb (s , _)]. + Otherwise, it returns [None]. *) +let get_symb : term -> sym option = fun t -> + match unfold t with + | Symb (s, _) -> Some s + | _ -> None + (** [iter_ctxt f t] applies the function [f] to every node of the term [t]. At each call, the function is given the list of the free variables in the term, in the reverse order they were given. Free variables that were @@ -183,6 +190,86 @@ let rec iter_meta : (meta -> unit) -> term -> unit = fun f t -> (** {b NOTE} that {!val:iter_meta} is not implemented using {!val:iter} due to the fact this it is performance-critical. *) +(** [is_meta t] checks if [t] is a metavariable. *) +let is_meta : term -> bool = fun t -> + match unfold t with + | Meta _ -> true + | _ -> false + +(** [map_meta f t] returns a new term [t'] obtained from [t] by replacing each + metavariable [m[ts]] with [f m ts'] where [ts'] is the array of terms + obtained by applying [map_meta f] recursively on [ts]. *) +let rec map_meta : (meta -> term array -> term) -> term -> term = fun f t -> + match unfold t with + | Prod (a, b) -> + let x, b' = Bindlib.unbind b in + let b = + Bindlib.unbox (Bindlib.bind_var x (lift (map_meta f b'))) in + Prod (map_meta f a, b) + | Abst (a, b) -> + let x, b' = Bindlib.unbind b in + let b = + Bindlib.unbox (Bindlib.bind_var x (lift (map_meta f b'))) in + Abst (map_meta f a, b) + | Appl (t, u) -> Appl (map_meta f t, map_meta f u) + | Meta (m, ts) -> f m (Array.map (map_meta f) ts) + | _ -> t + +module IntMap = Map.Make(struct type t = int let compare = compare end) + +(** [copy_rule (lhs, rhs)] returns a copy (lhs', rhs') of the rule (lhs, rhs) + by replacing each metavariable with a fresh metavariable. *) +let copy_rule : term * term -> term * term = fun (lhs, rhs) -> + let metamap = IntMap.empty in + let rec copy_term metamap t = + match unfold t with + | Prod (a, b) -> + let a, metamap = copy_term metamap a in + let x, b' = Bindlib.unbind b in + let b', metamap = copy_term metamap b' in + let b = + Bindlib.unbox (Bindlib.bind_var x (lift b')) in + Prod (a, b), metamap + | Abst (a, b) -> + let a, metamap = copy_term metamap a in + let x, b' = Bindlib.unbind b in + let b', metamap = copy_term metamap b' in + let b = + Bindlib.unbox (Bindlib.bind_var x (lift b')) in + Abst (a, b), metamap + | Appl (t, u) -> + let t, metamap = copy_term metamap t in + let u, metamap = copy_term metamap u in + Appl (t, u), metamap + | Meta (m, ts) -> + begin try + let new_m = IntMap.find m.meta_key metamap in + let ts, metamap = + List.fold_right + (fun t (acc, metamap) -> + let t, metamap = copy_term metamap t in + t :: acc, metamap) (Array.to_list ts) ([], metamap) in + Meta (new_m, Array.of_list ts), metamap + with Not_found -> + let new_m = fresh_meta !(m.meta_type) m.meta_arity in + let ts, metamap = + List.fold_right + (fun t (acc, metamap) -> + let t, metamap = copy_term metamap t in + t :: acc, metamap) + (Array.to_list ts) ([], IntMap.add m.meta_key new_m metamap) in + Meta (new_m, Array.of_list ts), metamap + end + | _ -> t, metamap + in + let lhs, metamap = copy_term metamap lhs in + let rhs = + let fn = fun m ts -> + Bindlib.unbox + (_Meta (IntMap.find m.meta_key metamap) (Array.map lift ts)) in + map_meta fn rhs in + lhs, rhs + (** [occurs m t] tests whether the metavariable [m] occurs in the term [t]. *) let occurs : meta -> term -> bool = let exception Found in fun m t -> @@ -201,6 +288,111 @@ let has_metas : term -> bool = let exception Found in fun t -> try iter_meta (fun _ -> raise Found) t; false with Found -> true +(** [build_prod k] builds the type “∀(x₁:A₁) (x₂:A₂) ⋯ (xk:Ak), A(k+1)” where + “x₁” through “xk” are fresh variables, “Ai = Mi[x₁,⋯,x(i-1)]”, “Mi” is a + new metavariable of arity “i-1” and type “∀(x₁:A₂) ⋯ (x(i-1):A(i-1)), TYPE + ”. *) +let build_prod : int -> term = fun k -> + assert (k>=0); + let vs = Bindlib.new_mvar mkfree (Array.make k "x") in + let rec build_prod k p = + if k = 0 then p + else + let k = k-1 in + let mk_typ = Bindlib.unbox (build_prod k _Type) in + let mk = fresh_meta mk_typ k in + let tk = _Meta mk (Array.map _Vari (Array.sub vs 0 k)) in + let b = Bindlib.bind_var vs.(k) p in + let p = Bindlib.box_apply2 (fun a b -> Prod(a,b)) tk b in + build_prod k p + in + let mk_typ = Bindlib.unbox (build_prod k _Type) (*FIXME?*) in + let mk = fresh_meta mk_typ k in + let tk = _Meta mk (Array.map _Vari vs) in + Bindlib.unbox (build_prod k tk) + +(** [new_symb name t] returns a new function symbol of name [name] and of + type [t]. *) +let new_symb name t = + { sym_name = name ; sym_type = ref t ; sym_path = [] ; sym_def = ref None + ; sym_impl = [] ; sym_rules = ref [] ; sym_mode = Const } + +(** [replace_patt_by_meta k metas t] computes a new (boxed) term by replacing + every pattern variable in [t] by a fresh metavariable and store the latter + in [metas], where [k] indicates the order of the term obtained *) +let rec replace_patt_by_meta : int -> meta option array -> term -> tbox + = fun k metas t -> + match unfold t with + | Vari x -> _Vari x + | Symb (s, h) -> _Symb s h + | Abst (a, t) -> + let (x, t) = Bindlib.unbind t in + _Abst (replace_patt_by_meta 0 metas a) + (Bindlib.bind_var x (replace_patt_by_meta 0 metas t)) + | Appl (t, u) -> + _Appl (replace_patt_by_meta (k + 1) metas t) + (replace_patt_by_meta 0 metas u) + | Patt (i, n, a) -> + begin + let a = Array.map (replace_patt_by_meta 0 metas) a in + let l = Array.length a in + match i with + | None -> + let m = fresh_meta ~name:n (build_prod (l + k)) l in + _Meta m a + | Some i -> + match metas.(i) with + | Some m -> _Meta m a + | None -> + let m = fresh_meta ~name:n (build_prod (l + k)) l in + metas.(i) <- Some m; + _Meta m a + end + | _ -> assert false + +(** Exception raised when a term contains non-nullary metavariables. *) +exception Non_nullary_meta + +(** [replace_patt_by_symb symbs t] computes a new (boxed) term by replacing + every pattern variable in [t] by a fresh symbol [c_n] of type [t_n] + ([t_n] is another fresh symbol of type [Kind]) and store [c_n] the latter + in [symbs]. *) +let rec replace_patt_by_symb : sym option array -> term -> tbox + = fun symbs t -> + match unfold t with + | Vari x -> _Vari x + | Symb (s, h) -> _Symb s h + | Abst (a, t) -> + let (x, t) = Bindlib.unbind t in + _Abst (replace_patt_by_symb symbs a) + (Bindlib.bind_var x (replace_patt_by_symb symbs t)) + | Appl (t, u) -> + _Appl (replace_patt_by_symb symbs t) (replace_patt_by_symb symbs u) + | Patt (i, n, [||]) -> + begin + match i with + | None -> + let t_n = new_symb ("{t_" ^ n) Type in + let term_t_n = symb t_n in + let c_n = new_symb ("{c_" ^ n) term_t_n in + _Symb c_n Nothing + | Some i -> + match symbs.(i) with + | Some s -> _Symb s Nothing + | None -> + let t_n = new_symb ("{t_" ^ n) Type in + let term_t_n = symb t_n in + let c_n = new_symb ("{c_" ^ n) term_t_n in + symbs.(i) <- Some c_n; + _Symb c_n Nothing + end + | Patt _ -> raise Non_nullary_meta + | _ -> assert false + +(** [is_new_symb s] checks if [s] is a function symbol created for checking + SR. *) +let is_new_symb s = s.sym_name.[0] = '{' + (** [distinct_vars_opt ts] checks that [ts] is made of distinct variables and returns these variables. *) let distinct_vars_opt : term array -> tvar array option = @@ -239,3 +431,58 @@ let term_of_rhs : rule -> term = fun r -> TE_Some(Bindlib.unbox (Bindlib.bind_mvar vars p)) in Bindlib.msubst r.rhs (Array.mapi fn r.vars) + +(** [replace_patt_rule replace_patt to_term_env r] translates the + rule [r] into a pair of terms. The pattern variables in the LHS are + replaced by fresh metavariables (resp. fresh symbols) if [replace_patt] = + [replace_patt_by_meta] (resp. [replace_patt_by_symb]). The terms with + environment in the RHS are replaced by their corresponding metavariables + (resp. symbols). *) +let replace_patt_rule : + ('a option array -> term -> tbox) -> ('a option -> term_env) -> + sym * rule -> term * term + = fun replace_patt to_term_env (s, r) -> + let arity = Bindlib.mbinder_arity r.rhs in + let arr = Array.init arity (fun _ -> None) in + let lhs = + List.map (fun arg -> Bindlib.unbox (replace_patt arr arg)) r.lhs in + let terms_env = Array.map to_term_env arr in + let rhs = Bindlib.msubst r.rhs terms_env in + add_args (symb s) lhs, rhs + +(** [replace_patt_by_meta_rule r] translates the rule [r] into a pair of + terms. The pattern variables in the LHS are replaced by fresh + metavariables. The terms with environment in the RHS are replaced by + their corresponding metavariables. *) +let replace_patt_by_meta_rule = + let to_term_env m = + let m = match m with Some m -> m | None -> assert false in + let xs = Array.init m.meta_arity (Printf.sprintf "x%i") in + let xs = Bindlib.new_mvar mkfree xs in + let ar = Array.map _Vari xs in + TE_Some (Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m ar))) in + replace_patt_rule (replace_patt_by_meta 0) to_term_env + +(** [replace_patt_by_symb_rule r] translates the rule [r] into a pair of + terms. The pattern variables in the LHS are replaced by fresh symbols. + The terms with environment in the RHS are replaced by their corresponding + symbols. *) +let replace_patt_by_symb_rule = + let to_term_env s = + let s = match s with Some s -> s | None -> assert false in + TE_Some (Bindlib.unbox (Bindlib.bind_mvar [||] (_Symb s Nothing))) in + replace_patt_rule replace_patt_by_symb to_term_env + +(** [check_nullary_meta t] checks that all the metavariables in [t] are of + arity 0 and raises the exception Non_nullary_meta if it is not the case. + *) +let rec check_nullary_meta : term -> unit = fun t -> + match t with + | Type + | Kind + | Symb _ + | Wild + | Patt _ -> () + | Meta (_, [||]) -> () + | Appl (u, v) -> check_nullary_meta u; check_nullary_meta v + | _ -> raise Non_nullary_meta diff --git a/src/completion.ml b/src/completion.ml new file mode 100644 index 000000000..618dc075d --- /dev/null +++ b/src/completion.ml @@ -0,0 +1,221 @@ +(** Completion procedure for closed equations *) + +open Terms +open Basics +open Extra +open Timed + +(** [lpo ord] computes the lexicographic path ordering corresponding to + the strict total order [ord] on the set of all function symbols. *) +let rec lpo : sym cmp -> term cmp = fun ord t1 t2 -> + let f, args = get_args t1 in + match get_symb f with + | None -> if t1 == t2 then 0 else -1 + | Some f -> + if List.exists (fun x -> lpo ord x t2 >= 0) args then 1 + else + let g, args' = get_args t2 in + let g = get_symb g in + match g with + | None -> 1 + | Some g -> + match ord f g with + | k when k > 0 -> + if List.for_all (fun x -> lpo ord t1 x > 0) args' then 1 + else -1 + | 0 -> + if List.for_all (fun x -> lpo ord t1 x > 0) args' then + ord_lex (lpo ord) args args' + else -1 + | _ -> -1 + +(** [make_rule (lhs, rhs)] tranlates the pair [(lhs, rhs)] of closed terms + into a rule. *) +let make_rule : term * term -> sym * rule = fun (lhs, rhs) -> + let (s, args) = get_args lhs in + match get_symb s with + | None -> assert false + | Some s -> + let vs = Bindlib.new_mvar te_mkfree [||] in + let rhs = Bindlib.unbox (Bindlib.bind_mvar vs (lift rhs)) in + s, { lhs = args ; rhs = rhs ; arity = List.length args ; vars = [||] } + +(** [find_deps eqs] returns a pair [(symbs, deps)], where [symbs] is a list of + (names of) new symbols and [deps] is a list of pairs of symbols. (s, t) + is added into [deps] iff there is a equation (l, r) in [eqs] such that + (l = s and t is a proper subterm of r) or (r = s and t is a proper subterm + of l). In this case, we also add s and t into [symbs]. *) +let find_deps : (term * term) list -> string list * (string * string) list + = fun eqs -> + let deps = ref [] in + let symbs = ref [] in + let add_symb name = + if not (List.mem name !symbs) then symbs := name :: !symbs in + let add_dep dep = + if not (List.mem dep !deps) then deps := dep :: !deps in + let find_dep_aux (t1, t2) = + match get_symb t1 with + | Some sym -> + if is_new_symb sym then + let check_root t = + let g, _ = get_args t in + match get_symb g with + | Some sym' when is_new_symb sym' -> + add_dep (sym.sym_name, sym'.sym_name); + add_symb sym.sym_name; + add_symb sym'.sym_name; + | _ -> () in + let _, args = get_args t2 in + List.iter (Basics.iter check_root) args + | None -> () in + List.iter + (fun (t1, t2) -> find_dep_aux (t1, t2); find_dep_aux (t2, t1)) eqs; + (!symbs, !deps) + +(** Exception raised by [topo_sort] when the directed graph considered is not + a DAG *) +exception Not_DAG + +(** [topo_sort symbs edges] computes a topological sort on the directed graph + [(symbs, edges)]. *) +let topo_sort : string list -> (string * string) list -> int StrMap.t + = fun symbs edges -> + let n = List.length symbs in + let i = ref (-1) in + let name_map = + List.fold_left + (fun map s -> incr i; StrMap.add s !i map) StrMap.empty symbs in + let adj = Array.make_matrix n n 0 in + let incoming = Array.make n 0 in + List.iter + (fun (s1, s2) -> + let i1 = StrMap.find s1 name_map in + let i2 = StrMap.find s2 name_map in + adj.(i1).(i2) <- 1 + adj.(i1).(i2); + incoming.(i2) <- 1 + incoming.(i2)) edges; + let no_incoming = ref [] in + let remove_edge (i, j) = + if adj.(i).(j) <> 0 then begin + adj.(i).(j) <- 0; + incoming.(j) <- incoming.(j) - 1; + if incoming.(j) = 0 then no_incoming := j :: !no_incoming + end + in + Array.iteri + (fun i incoming -> + if incoming = 0 then no_incoming := i :: !no_incoming) incoming; + let ord = ref 0 in + let ord_array = Array.make n (-1) in + while !no_incoming <> [] do + let s = List.hd !no_incoming in + ord_array.(s) <- !ord; + incr ord; + no_incoming := List.tl !no_incoming; + for i = 0 to n-1 do + remove_edge (s, i) + done; + done; + if Array.exists (fun x -> x > 0) incoming then raise Not_DAG + else + List.fold_left + (fun map s -> + let i = StrMap.find s name_map in + StrMap.add s (ord_array.(i)) map) StrMap.empty symbs + +(** [ord_from_eqs eqs s1 s2] computes the order induced by the equations + [eqs]. We first use [find_deps] to find the dependency between the new + symbols (symbols introduced for checking SR) and compute its corresponding + DAG. The order obtained satisfies the following property: + 1. New symbols are always larger than the orginal ones. + 2. If [s1] and [s2] are not new symbols, then we use the usual + lexicographic order. + 3. If [s1] and [s2] are new symbols and if the topological order is well + defined, then we compare their positions in this latter one. Otherwise, + we use the usual lexicographic order. *) +let ord_from_eqs : (term * term) list -> sym cmp = fun eqs -> + let symbs, deps = find_deps eqs in + let ord = + try topo_sort symbs deps with Not_DAG -> StrMap.empty in + fun s1 s2 -> + match (is_new_symb s1, is_new_symb s2) with + | true, true -> + if s1 == s2 then 0 + else begin + try + StrMap.find s2.sym_name ord - StrMap.find s1.sym_name ord + with _ -> Pervasives.compare s1.sym_name s2.sym_name + end + | true, false -> 1 + | false, true -> -1 + | false, false -> Pervasives.compare s1.sym_name s2.sym_name + +(** [completion eqs ord] returns the convergent rewrite system obtained from + the completion procedure on the set of equations [eqs] using the LPO + [lpo ord]. *) +let completion : (term * term) list -> sym cmp -> (sym * rule list) list + = fun eqs ord -> + let lpo = lpo ord in + (* [symbs] is used to store all the symbols appearing in the equations. *) + let symbs = ref [] in + (* [reset_sym t] erases all the rules defined for all the symbols in + [symbs]. Note that these rules can be retrieved using [t1]. *) + let reset_sym t = + match t with + | Symb (s, _) when not (List.mem s !symbs) -> + s.sym_rules := []; + symbs := s :: !symbs + | _ -> () in + List.iter + (fun (t1, t2) -> Basics.iter reset_sym t1; Basics.iter reset_sym t2) eqs; + let add_rule (s, r) = s.sym_rules := r :: !(s.sym_rules) in + (* [orient (t1, t2)] orients the equation [t1 = t2] using LPO. *) + let orient (t1, t2) = + match lpo t1 t2 with + | 0 -> () + | k when k > 0 -> add_rule (make_rule (t1, t2)) + | _ -> add_rule (make_rule (t2, t1)) in + List.iter orient eqs; + let completion_aux : unit -> bool = fun () -> + let b = ref false in + (* [to_add] is used to store the new rules that need to be added. *) + let to_add = ref [] in + (* [find_cp s] applies the following procedure to all the rules of head + symbol [s]. *) + let find_cp s = + (* Intuitively, [f acc rs' r] corresponds to a sequence of Deduce, + Simplify, and Orient (or Delete) steps in the Knuth-Bendix + completion algorithm. Here, we attempts to deal with the critical + pairs between [r] and the other rules. Since only closed equations + are considered here, a critical pair between the rules (l1, r1) and + (l2, r2) is of the form (r1, r2') or (r1', r2) where ri' is a reduct + of ri. Note that [acc @ rs'] is the list of rules of head symbol [s] + other than [r]. *) + let f acc rs' r = + s.sym_rules := acc @ rs'; + let lhs, rhs = replace_patt_by_meta_rule (s, r) in + let lhs' = Eval.snf lhs in + let rhs' = Eval.snf rhs in + s.sym_rules := r :: !(s.sym_rules); + if eq lhs lhs' then () + else begin + match lpo lhs' rhs' with + | 0 -> () + | k when k > 0 -> + to_add := make_rule (lhs', rhs') :: !to_add; + b := true; + | _ -> + to_add := make_rule (rhs', lhs') :: !to_add; + b := true; + end + in + let rec aux acc f rs = + match rs with + | [] -> () + | r :: rs' -> f acc rs' r; aux (r :: acc) f rs' in + aux [] f !(s.sym_rules) in + List.iter find_cp !symbs; + List.iter add_rule !to_add; + !b in + let b = ref true in + while !b do b := completion_aux () done; + List.map (fun s -> (s, !(s.sym_rules))) !symbs diff --git a/src/confluence.ml b/src/confluence.ml new file mode 100644 index 000000000..4bc80eb97 --- /dev/null +++ b/src/confluence.ml @@ -0,0 +1,80 @@ +(** First-order syntactic unification *) + +open Terms +open Basics +open Timed + +exception Unsolvable + +(** [unif_aux t1 t2 eqs] attempts to solve the first-order unification + problem [(t1 = t2) :: eqs]. *) +let rec unif_aux : term -> term -> unif_constrs -> unit = fun t1 t2 eqs -> + match (t1, t2) with + | Type, Type + | Kind, Kind -> unif eqs + | Symb(s1, _), Symb(s2, _) -> + if s1 == s2 then unif eqs else raise Unsolvable + | Vari _, _ + | _, Vari _ + | Prod _, _ + | _, Prod _ + | Abst _, _ + | _, Abst _ -> assert false + | Appl (t1, u1), Appl (t2, u2) -> unif ((t1, t2) :: (u1, u2) :: eqs) + | Meta (m1, [||]), Meta (_, [||]) -> + let vs = Bindlib.new_mvar mkfree [||] in + let bt2 = Bindlib.bind_mvar vs (lift t2) in + set_meta m1 (Bindlib.unbox bt2); + unif eqs + | (Meta (m1, [||]), t2) + | (t2, Meta (m1, [||])) -> + if occurs m1 t2 then raise Unsolvable + else + let vs = Bindlib.new_mvar mkfree [||] in + let bt2 = Bindlib.bind_mvar vs (lift t2) in + set_meta m1 (Bindlib.unbox bt2); + unif eqs + | _ -> raise Unsolvable + +(** [unif eqs] attempts to solve the unification problem [eqs]. *) +and unif : unif_constrs -> unit = fun eqs -> + match eqs with + | [] -> () + | (t1, t2) :: eqs -> unif_aux t1 t2 eqs + +(** [cps rs] computes the critical pairs of the rewrite system [rs]. *) +let cps : (sym * rule) list -> (term * term) list = fun rs -> + let acc = ref [] in + let rs = List.map replace_patt_by_meta_rule rs in + (* [cps_aux b r1 r2] computes the critical pairs between [r1] and [r2], + where [b] indicates if the rules considered are different. *) + let cps_aux : bool -> term * term -> term * term -> unit + = fun b (lhs1, rhs1) (lhs2, rhs2) -> + (* [find_cp t1 t2] computes the critical pairs between [r1] and [r2] by + unifying [t1] and [t2], where [ti] is a subterm of the LHS of [ri]. *) + let find_cp : term -> term -> unit = fun t1 t2 -> + match (t1, t2) with + | Meta _, _ -> () + | _, Meta _ -> () + | _ -> + let reset_meta m = m.meta_value := None in + iter_meta reset_meta lhs1; + iter_meta reset_meta lhs2; + try + unif [(t1, t2)]; + acc := (rhs1, rhs2) :: !acc + with Unsolvable -> () in + let _, args1 = get_args lhs1 in + let _, args2 = get_args lhs2 in + find_cp lhs1 lhs2; + List.iter (Basics.iter (find_cp lhs1)) args2; + if b then List.iter (Basics.iter (fun t -> find_cp t lhs2)) args1 in + let rec cps rs = + match rs with + | [] -> () + | r :: rs' -> begin + List.iter (cps_aux true r) rs'; + cps_aux false r r; + cps rs' end in + cps rs; + !acc diff --git a/src/extra.ml b/src/extra.ml index 1701abf58..8d1162f13 100644 --- a/src/extra.ml +++ b/src/extra.ml @@ -172,3 +172,21 @@ let input_lines : in_channel -> string list = fun ic -> done; assert false (* Unreachable. *) with End_of_file -> List.rev !lines + +(** Type of a total ordering function. A total ordering function [f] is a + function such that [f x y] is zero if the two elements [x] and [y] + are equal, [f x y] is strictly negative if [x] is smaller than [y], + and [f x y] is strictly positive if [x] is greater than [y]. *) + type 'a cmp = 'a -> 'a -> int + + (** [ord_lex ord] computes the lexicographic order corresponding to the + alphabetical order [ord]. *) + let rec ord_lex : 'a cmp -> 'a list cmp = fun ord l1 l2 -> + match (l1, l2) with + | [], [] -> 0 + | [], _ -> -1 + | _, [] -> 1 + | h1 :: t1, h2 :: t2 -> + match ord h1 h2 with + | 0 -> ord_lex ord t1 t2 + | x -> x diff --git a/src/handle.ml b/src/handle.ml index 9fb56e070..cf955703c 100644 --- a/src/handle.ml +++ b/src/handle.ml @@ -10,6 +10,7 @@ open Pos open Files open Syntax open Scope +open Basics (** [check_builtin_nat s] checks that the builtin symbol [s] for non-negative literals has a good type. *) @@ -112,7 +113,8 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = match ts with | [] -> Defin | Sym_const :: [] -> Const - | Sym_inj :: [] -> Injec + | Sym_inj :: [] -> + Injec [List.init (count_products a) (fun _ -> false)] | _ -> fatal cmd.pos "Multiple symbol tags." in (* Actually add the symbol to the signature and the state. *) diff --git a/src/sr.ml b/src/sr.ml index e79773481..f82feaa0d 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -5,6 +5,8 @@ open Console open Terms open Print open Extra +open Basics +open Pos (** Logging function for typing. *) let log_subj = @@ -38,127 +40,72 @@ let subst_from_constrs : (term * term) list -> subst = fun cs -> let (vs,ts) = build_sub [] cs in (Array.of_list vs, Array.of_list ts) -(* Does not work in examples/cic.dk +(** Logging functions and error messages *) +let typ_cond s t conds = + log_subj "%s has type [%a]" s pp t; + let fn (t, u) = log_subj " if [%a] ~ [%a]" pp t pp u in + List.iter fn conds -let build_meta_type : int -> term = fun k -> - let m' = new_meta Type (*FIXME?*) k in - let m_typ = Meta(m',[||]) in - let m = new_meta m_typ k in - Meta(m,[||]) -*) +let unsolved_msg (t, u) = fatal_msg "Cannot solve [%a] ~ [%a]\n" pp t pp u -(** [build_meta_type k] builds the type “∀(x₁:A₁) (x₂:A₂) ⋯ (xk:Ak), B” where - “x₁” through “xk” are fresh variables, “Ai = Mi[x₁,⋯,x(i-1)]”, “Mi” is a - new metavar of arity “i-1” and type “∀(x₁:A₂) ⋯ (x(i-1):A(i-1), TYPE”. *) -let build_meta_type : int -> term = fun k -> - assert (k>=0); - let vs = Bindlib.new_mvar mkfree (Array.make k "x") in - let rec build_prod k p = - if k = 0 then p - else - let k = k-1 in - let mk_typ = Bindlib.unbox (build_prod k _Type) in - let mk = fresh_meta mk_typ k in - let tk = _Meta mk (Array.map _Vari (Array.sub vs 0 k)) in - let b = Bindlib.bind_var vs.(k) p in - let p = Bindlib.box_apply2 (fun a b -> Prod(a,b)) tk b in - build_prod k p +let sr_unproved_msg (s, h, r) = + fatal r.pos "Unable to prove SR for rule [%a]." pp_rule (s, h, r.elt) + +let sr_not_preserved_msg (s, h, r) = + fatal r.pos "Rule [%a] may not preserve typing." pp_rule (s, h, r.elt) + +(** [check_eq eq eqs] checks if there exists an equation [eq'] in [eqs] such + that (t_i == u_i (or u_(1-i)) for i = 0, 1) where [eq] = (t_0, t_1) + and [eq'] = (u_0, u_1). *) +let check_eq eq eqs = + let eq_comm (t0, t1) (u0, u1) = + (Eval.eq_modulo t0 u0 && Eval.eq_modulo t1 u1) || + (Eval.eq_modulo t1 u0 && Eval.eq_modulo t0 u1) in - let mk_typ = Bindlib.unbox (build_prod k _Type) (*FIXME?*) in - let mk = fresh_meta mk_typ k in - let tk = _Meta mk (Array.map _Vari vs) in - Bindlib.unbox (build_prod k tk) + List.exists (eq_comm eq) eqs -(** [check_rule builtins r] check whether rule [r] is well-typed. The program - fails gracefully in case of error. *) -let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit +(** [check_rule builtins (s, h, r)] checks whether rule [r] is well-typed. The + program fails gracefully in case of error. *) +let check_rule : + sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit = fun builtins (s,h,r) -> - if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, r.elt); - (* We process the LHS to replace pattern variables by metavariables. *) - let arity = Bindlib.mbinder_arity r.elt.rhs in - let metas = Array.init arity (fun _ -> None) in - let rec to_m : int -> term -> tbox = fun k t -> - match unfold t with - | Vari(x) -> _Vari x - | Symb(s,h) -> _Symb s h - | Abst(a,t) -> let (x,t) = Bindlib.unbind t in - _Abst (to_m 0 a) (Bindlib.bind_var x (to_m 0 t)) - | Appl(t,u) -> _Appl (to_m (k+1) t) (to_m 0 u) - | Patt(i,n,a) -> - begin - let a = Array.map (to_m 0) a in - let l = Array.length a in - match i with - | None -> - let m = fresh_meta ~name:n (build_meta_type (l+k)) l in - _Meta m a - | Some(i) -> - match metas.(i) with - | Some(m) -> _Meta m a - | None -> - let m = fresh_meta ~name:n (build_meta_type (l+k)) l in - metas.(i) <- Some(m); - _Meta m a - end - | Type -> assert false (* Cannot appear in LHS. *) - | Kind -> assert false (* Cannot appear in LHS. *) - | Prod(_,_) -> assert false (* Cannot appear in LHS. *) - | Meta(_,_) -> assert false (* Cannot appear in LHS. *) - | TEnv(_,_) -> assert false (* Cannot appear in LHS. *) - | Wild -> assert false (* Cannot appear in LHS. *) - | TRef(_) -> assert false (* Cannot appear in LHS. *) - in - let lhs = List.map (fun p -> Bindlib.unbox (to_m 0 p)) r.elt.lhs in - let lhs = Basics.add_args (Symb(s,h)) lhs in - (* We substitute the RHS with the corresponding metavariables.*) - let fn m = - let m = match m with Some(m) -> m | None -> assert false in - let xs = Array.init m.meta_arity (Printf.sprintf "x%i") in - let xs = Bindlib.new_mvar mkfree xs in - let e = Array.map _Vari xs in - TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m e))) - in - let te_envs = Array.map fn metas in - let rhs = Bindlib.msubst r.elt.rhs te_envs in - (* Infer the type of the LHS and the constraints. *) + let lhs, rhs = replace_patt_by_meta_rule (s, r.elt) in match Typing.infer_constr builtins Ctxt.empty lhs with - | None -> wrn r.pos "Untypable LHS." - | Some(lhs_constrs, ty_lhs) -> - if !log_enabled then - begin - log_subj "LHS has type [%a]" pp ty_lhs; - let fn (t,u) = log_subj " if [%a] ~ [%a]" pp t pp u in - List.iter fn lhs_constrs - end; - (* Turn constraints into a substitution and apply it. *) - let (xs,ts) = subst_from_constrs lhs_constrs in - let p = Bindlib.box_pair (lift rhs) (lift ty_lhs) in - let p = Bindlib.unbox (Bindlib.bind_mvar xs p) in - let (rhs,ty_lhs) = Bindlib.msubst p ts in - (* Check that the RHS has the same type as the LHS. *) - let to_solve = Infer.check Ctxt.empty rhs ty_lhs in - if !log_enabled && to_solve <> [] then - begin - log_subj "RHS has type [%a]" pp ty_lhs; - let fn (t,u) = log_subj " if [%a] ~ [%a]" pp t pp u in - List.iter fn to_solve - end; - (* Solving the constraints. *) - match Unif.(solve builtins false {no_problems with to_solve}) with - | Some(cs) -> - let is_constr c = - let eq_comm (t1,u1) (t2,u2) = - (Eval.eq_modulo t1 t2 && Eval.eq_modulo u1 u2) || - (Eval.eq_modulo t1 u2 && Eval.eq_modulo t2 u1) - in - List.exists (eq_comm c) lhs_constrs - in - let cs = List.filter (fun c -> not (is_constr c)) cs in - if cs <> [] then - begin - let fn (t,u) = fatal_msg "Cannot solve [%a] ~ [%a]\n" pp t pp u in - List.iter fn cs; - fatal r.pos "Unable to prove SR for rule [%a]." pp_rule (s,h,r.elt) - end - | None -> - fatal r.pos "Rule [%a] does not preserve typing." pp_rule (s,h,r.elt) + | None -> wrn r.pos "Untypable LHS" + | Some (lhs_constrs, ty_lhs) -> + let t0 = Time.save () in + if !log_enabled then typ_cond "LHS" ty_lhs lhs_constrs; + try + Unif.add_rules_from_constrs lhs_constrs; + (* Check that the RHS has the same type as the LHS. *) + let to_solve = Infer.check Ctxt.empty rhs ty_lhs in + match Unif.(solve builtins false {no_problems with to_solve}) with + | Some cs -> + if cs <> [] then + let cs = + List.filter (fun c -> not (check_eq c lhs_constrs)) cs in + if cs <> [] then raise Non_nullary_meta + else Time.restore t0 + else Time.restore t0 + | None -> sr_not_preserved_msg (s, h, r) + with Non_nullary_meta -> + Time.restore t0; + let (xs, ts) = subst_from_constrs lhs_constrs in + let p = Bindlib.box_pair (lift rhs) (lift ty_lhs) in + let p = Bindlib.unbox (Bindlib.bind_mvar xs p) in + let (rhs, ty_lhs) = Bindlib.msubst p ts in + let to_solve = Infer.check Ctxt.empty rhs ty_lhs in + if !log_enabled && to_solve <> [] then + typ_cond "RHS" ty_lhs to_solve; + let problems = Unif.{no_problems with to_solve} in + match Unif.(solve builtins false problems) with + | Some cs -> + let cs = List.filter (fun c -> not (check_eq c lhs_constrs)) cs in + if cs <> [] then + begin + List.iter unsolved_msg cs; + sr_unproved_msg (s, h, r) + end + else Time.restore t0 + | None -> + sr_not_preserved_msg (s, h, r) diff --git a/src/terms.ml b/src/terms.ml index b63ba16fa..1232ed94b 100644 --- a/src/terms.ml +++ b/src/terms.ml @@ -65,7 +65,7 @@ type term = (** Implicitness of the first arguments ([true] meaning implicit). *) ; sym_rules : rule list ref (** Rewriting rules for the symbol. *) - ; sym_mode : sym_mode + ; mutable sym_mode : sym_mode (** Tells what kind of symbol it is. *) } (** {b NOTE} that {!field:sym_type} holds a (timed) reference for a technical @@ -87,7 +87,7 @@ type term = (** The symbol is constant: it has no definition and no rewriting rule. *) | Defin (** The symbol may have a definition or rewriting rules (but NOT both). *) - | Injec + | Injec of bool list list (** Same as [Defin], but the symbol is considered to be injective. *) (** {b NOTE} the value of the {!field:sym_mode} field of symbols restricts the diff --git a/src/unif.ml b/src/unif.ml index 1a2ee56f1..bd76c6fee 100644 --- a/src/unif.ml +++ b/src/unif.ml @@ -6,6 +6,7 @@ open Console open Terms open Basics open Print +open Eval (** Logging function for unification. *) let log_solv = new_logger 's' "solv" "debugging information for unification" @@ -39,6 +40,12 @@ type problems = ; recompute : bool (** Indicates whether unsolved problems should be rechecked. *) } +(** Type of a hypothesis on injectivity. A hypothesis (f, l) means that f is + assumed to be I-injective i.e., + (ft ~ fu and ti ~ ui for all i in I) => (ti ~ ui for all i not in I) + where I = { i | li = true }. *) +type inj_hypo = sym * bool list + (** Empty problem. *) let no_problems : problems = {to_solve = []; unsolved = []; recompute = false} @@ -85,19 +92,22 @@ let instantiate : meta -> term array -> term -> bool = fun m ts u -> variable of [vs] occurring in [u]. *) && (set_meta m (Bindlib.unbox bu); true) -(** [solve cfg p] tries to solve the unification problems of [p] and - returns the constraints that could not be solved. *) -let rec solve : problems -> unif_constrs = fun p -> +(** [solve p hypo] tries to solve the unification problems of [p] under the + hypothesis [hypo] and returns the constraints that could not be solved. *) +let rec solve : problems -> inj_hypo option -> unif_constrs = fun p hypo -> match p with | { to_solve = []; unsolved = []; _ } -> [] | { to_solve = []; unsolved = cs; recompute = true } -> - solve {no_problems with to_solve = cs} + solve {no_problems with to_solve = cs} hypo | { to_solve = []; unsolved = cs; _ } -> cs - | { to_solve = (t,u)::to_solve; _ } -> solve_aux t u {p with to_solve} + | { to_solve = (t,u)::to_solve; _ } -> solve_aux t u {p with to_solve} hypo -(** [solve_aux t1 t2 p] tries to solve the unificaton problem given by [p] and - the constraint [(t1,t2)], starting with the latter. *) -and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> +(** [solve_aux t1 t2 p hypo] tries to solve the unificaton problem given by + [p] and the constraint [(t1,t2)] under the hypothesis [hypo], starting + with the latter. Note that [hypo] = None if there is no hypothesis. *) +and solve_aux : term -> term -> problems -> inj_hypo option -> unif_constrs + = fun t1 t2 p hypo -> + if Eval.eq_modulo t1 t2 then solve p hypo else let (h1, ts1) = Eval.whnf_stk t1 [] in let (h2, ts2) = Eval.whnf_stk t2 [] in if !log_enabled then @@ -112,22 +122,26 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> let add_to_unsolved () = let t1 = Eval.to_term h1 ts1 in let t2 = Eval.to_term h2 ts2 in - if Eval.eq_modulo t1 t2 then solve p - else solve {p with unsolved = (t1,t2) :: p.unsolved} + if Eval.eq_modulo t1 t2 then solve p hypo + else solve {p with unsolved = (t1,t2) :: p.unsolved} hypo in let error () = let t1 = Eval.to_term h1 ts1 in let t2 = Eval.to_term h2 ts2 in fatal_no_pos "[%a] and [%a] are not convertible." pp t1 pp t2 in - let decompose () = - let add_arg_pb l t1 t2 = Pervasives.(snd !t1, snd !t2)::l in + let decompose_part bls () = + let add_arg_pb l b (t1, t2) = + if b then l else Pervasives.(snd !t1, snd !t2) :: l in let to_solve = - try List.fold_left2 add_arg_pb p.to_solve ts1 ts2 + try List.fold_left2 add_arg_pb p.to_solve bls (List.combine ts1 ts2) with Invalid_argument _ -> error () in - solve {p with to_solve} + solve {p with to_solve} hypo + in + let decompose () = + let bls = List.map (fun _ -> false) ts1 in + decompose_part bls () in - (* For a problem m[vs]=s(ts), where [vs] are distinct variables, m is a meta of type ∀y0:a0,..,∀yk-1:ak-1,b (k = length vs), s is an injective symbol of type ∀x0:b0,..,∀xn-1:bn-1,c (n = length ts), @@ -157,7 +171,7 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> in build (List.length ts) [] !(s.sym_type) in set_meta m (Bindlib.unbox (Bindlib.bind_mvar vars (lift t))); - solve_aux t1 t2 p + solve_aux t1 t2 p hypo with Unsolvable -> add_to_unsolved () in @@ -215,7 +229,7 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> let xu1 = _Abst a (Bindlib.bind_var x u1) in let v = Bindlib.bind_mvar (Env.vars env) xu1 in set_meta m (Bindlib.unbox v); - solve_aux t1 t2 p + solve_aux t1 t2 p hypo in (* [inverse c s t] computes a term [u] such that [s(u)] reduces to @@ -245,21 +259,20 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> try if s == c.symb_P then match ts with - | [t] -> solve_aux Pervasives.(snd !t) (inverse c s v) p + | [t] -> solve_aux Pervasives.(snd !t) (inverse c s v) p hypo | _ -> raise Unsolvable else raise Unsolvable with Unsolvable -> add_to_unsolved () in - match (h1, h2) with (* Cases in which [ts1] and [ts2] must be empty due to typing / whnf. *) | (Type , Type ) - | (Kind , Kind ) -> solve p + | (Kind , Kind ) -> solve p hypo | (Prod(a1,b1), Prod(a2,b2)) | (Abst(a1,b1), Abst(a2,b2)) -> let (_,b1,b2) = Bindlib.unbind2 b1 b2 in - solve_aux a1 a2 {p with to_solve = (b1,b2) :: p.to_solve} + solve_aux a1 a2 {p with to_solve = (b1,b2) :: p.to_solve} hypo (* Other cases. *) | (Vari(x1) , Vari(x2) ) -> @@ -269,21 +282,31 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> if s1 == s2 then match s1.sym_mode with | Const -> decompose () - | Injec -> - if List.same_length ts1 ts2 then decompose () - else if !(s1.sym_rules) = [] then error () - else add_to_unsolved () - | Defin -> - if !(s1.sym_rules) <> [] || List.same_length ts1 ts2 - then add_to_unsolved () - else error () + | _ -> + if List.same_length ts1 ts2 then + let bls = + List.map2 + (fun t u -> + let t = snd Pervasives.(!t) in + let u = snd Pervasives.(!u) in + Eval.eq_modulo t u) ts1 ts2 in + let check_inj_and_decompose () = + if check_inj_sym bls s1 then decompose_part bls () + else add_to_unsolved () in + match hypo with + | None -> check_inj_and_decompose () + | Some (s, bls') -> + if s == s1 && inj_incl bls bls' then + decompose_part bls () + else check_inj_and_decompose () + else error () else if !(s1.sym_rules) = [] && !(s2.sym_rules) = [] then error () else add_to_unsolved () | (Meta(m,ts) , _ ) when ts1 = [] && instantiate m ts t2 -> - solve {p with recompute = true} + solve {p with recompute = true} hypo | (_ , Meta(m,ts) ) when ts2 = [] && instantiate m ts t1 -> - solve {p with recompute = true} + solve {p with recompute = true} hypo | (Meta(m,_) , _ ) when imitate_lam_cond h1 ts1 -> imitate_lam m | (_ , Meta(m,_) ) when imitate_lam_cond h2 ts2 -> imitate_lam m @@ -299,6 +322,239 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> | (_ , _ ) -> error () +(** The following functions are used to determine whether a function symbol + f is I-injective (I is a subset of {1, ..., n} where n is the arity of + f). + A function symbol f is said to be I-injective if + ( f t1 ... tn ~ f u1 ... un and ti ~ ui for all i in I ) implies + ( ti ~ ui for all i not in I. ). In the following, I is represented by + a list of boolean values [b1; ...; bn] such that bi is true iff i is in + I. *) + +(** Intuitively, we want to prove the I-injectivity of f by well-founded + induction. Let > be the union of subterm relation and the reduction. + We prove [(f t1 ... tn ~ f u1 ... un and ti ~ ui for all i in I) => + (ti ~ ui for all i)] by induction using >_seq on (ft1...tn, fu1...un). + Consider ft ~ fu where t = t1...tn and u = u1...un. We write t ~ u if + ti ~ ui for all i. + We distinguish three cases: + - ft and fu are in normal form : Then ft = fu and t = u. + - ft is in normal form and there exists v s.t. fu -> v. + Suppose that there exists k and uk' s.t. uk -> uk'. We have fu -> fu' + (and thus (ft, fu) >_seq (ft, fu') where u' = u1...uk'...un and it is + clear that ti ~ (u')i for all i in I. + Hence by applying the induction hypothesis, ti ~ (u')i and thus ti ~ ui + for all i in I. + Suppose that ui are all in normal form. Then there exists a rule R such + that fu ->_R v by applying R at the root. + We do not have a general solution in this case now but we could give + some sufficient conditions for dealing with this case. + - If a rule R' is of the form fl -> sr where s is a constant symbol, + then R cannot be R'. + In fact, if R = R' then ft, the normal form of v, is + headed by s, which is impossible. + - If a rule R' is of the form fl -> x s.t. li = x for some i in I, + then R cannot be R'. + In fact, if R = R' then v = ui ~ ti by hypothesis. We have also + v ~ ft. Since ti and ft are in normal form, ti = ft, which is + impossible since ti is a proper subterm of ft. + Hence, if all the rules are in one of the above forms, then there is no + need to deal with this case. + - There exist v and w such that ft -> v and fu -> w. + If there exist k and tk' (resp. uk') s.t. tk -> tk' (resp. uk -> uk'), + then by applying the induction hypothesis, ti ~ ui for all i. + Suppose that ti and ui are all in normal form. There exist thus two + rules (not nessarily distinct) R1 and R2 s.t. ft ->_R1 v and fu ->_R2 w + by applying R1 and R2 at the roots. + In this case, we suppose R1 = fl1 -> r1 and R2 = fl2 -> r2. There exist + therefore two substitutions σ1 and σ2 s.t. ft = fl1σ1 and fu = fl2σ2. + Let σ be the union of σ1 and σ2. + We now attempt to unify (r, r') and ((l1)i, (l2)i) for all i in I. + During this unification procedure, we use the hypothesis that f is + I-injective, which is justified by the following property: + whenever we unify (r, s), if ft' (resp. fu') is a subterm of r (resp. s) + then there exists t'' (resp. u'') s.t. ft'' < ft and t'σ ->* t'' + (resp. fu'' < fu and u'σ ->* u''). + Proof sketch: + By induction on the unification steps. + Initially, the property is clearly verified since v < t (resp. w < u) + and ti < t (resp. ui < u). + The only induction step that needs to be checked is the instantiation of + a metavariable. + After instantiating a metavariable m with a term s, every pair + (ft', fu') becomes (ft'[m <- s], fu'[m <- s]). + By I.H., there exist t'' and u'' s.t. ft'' < ft, fu'' < fu, t'σ ->* t'' + and u'σ ->* u''. + Let σ' be the restriction of σ to dom(σ)\{m}. + We have thus t'σ = t'σ'[m <- mσ] and t'[m <- s]σ = t'σ'[m <- sσ] + (similarly for u'σ and u'[m <- s]σ). mσ is in normal form since it + is a subterm of t, which is itself in normal form. + We know that the unification (m, s) implicitly means that mσ ~ sσ and + thus sσ ->* mσ. Therefore, t'[m <- s]σ ->* t'σ ->* t'' and + u'[m <- s]σ ->* u'σ -> u''. + Therefore, when we unify (ft', fu'), if (t')i ~ (u')i for all i in I, + then we can remove this pair from the problem and add the pairs + {((t')i, (u')i), i in I}. + After unifying (r, r') and ((l1)i, (l2)i) for all i in I, we attempt to + unify ((l1)i, (l2)i) for all i not in I and use the constraints deduced + in the previous part to solve the constraints obtained in this part. + If both parts of unification succeed or the first part fails, then we + say that this pair of rules (R_1, R_2) is "good". + + Our algorithm consists of checking that every pair of rules is good and + that every rule is in one of the forms mentioned in the second case. *) + +(** [inj_incl bls bls'] checks if bls'_i => bls_i for all i. This + corresponds to the property that I-injectivity implies J-injectivity if I + is included in J. *) +and inj_incl : bool list -> bool list -> bool = fun bls bls' -> + List.for_all2 (fun b b' -> b || not b') bls bls' + +(** [inj_incls bls blss] checks if there exists [bls'] in [blss] such that + bls'_i => bls_i for all i. *) +and inj_incls : bool list -> bool list list -> bool = fun bls blss -> + List.exists (fun bls' -> inj_incl bls bls') blss + +(** [eq_modulo_constrs constrs (t1, t2)] returns if t1 ~ t2 or there exists + (t1', t2') in [constrs] such that t1 ~ t1' (resp. t2') and t2 ~ t2' + (resp. t1'). *) +and eq_modulo_constrs : unif_constrs -> term * term -> bool + = fun constrs (t1, t2) -> + let fn (t1', t2') = + (eq_modulo t1 t1' && eq_modulo t2 t2') || + (eq_modulo t1 t2' && eq_modulo t2 t1') in + eq_modulo t1 t2 || List.exists fn constrs + +(** [add_rules_from_constrs constrs] first replaces each metavariable in + [constrs] with a fresh symbol, then applies the completion procedure on + the first-order constraints in [constrs]. *) +and add_rules_from_constrs : unif_constrs -> unit = fun constrs -> + let fn m = + match !(m.meta_value) with + | None -> + let n = string_of_int m.meta_key in + let term_t_m = !(m.meta_type) in + let c_m = new_symb ("{c_" ^ n) term_t_m in + if m.meta_arity <> 0 then raise Non_nullary_meta; + m.meta_value := + Some (Bindlib.unbox (Bindlib.bind_mvar [||] (_Symb c_m Nothing))) + | Some _ -> () in + let fo_constrs fo (t, u) = + try + check_nullary_meta t; + check_nullary_meta u; + iter_meta fn t; + iter_meta fn u; + (t, u) :: fo + with Non_nullary_meta -> fo in + let constrs_fo = List.fold_left fo_constrs [] constrs in + let t1 = Time.save () in + let ord = Completion.ord_from_eqs constrs_fo in + let rules_to_add = Completion.completion constrs_fo ord in + Time.restore t1; + List.iter + (fun (s, rs) -> s.sym_rules := rs @ !(s.sym_rules)) rules_to_add + +(** [check_pair_of_rules bls (lhs1, rhs1) (lhs2, rhs2)] checks if + the rules [lhs1 -> rhs1] and [lhs2 -> rhs2] satisfy the conditions + mentioned above. *) +and check_pair_of_rules : + bool list -> sym -> term * term -> term * term -> bool + = fun bls s (lhs1, rhs1) (lhs2, rhs2) -> + let t = Time.save () in + try + let _, args1 = get_args lhs1 in + let _, args2 = get_args lhs2 in + let args = List.combine args1 args2 in + let to_solve = + (rhs1, rhs2) :: List.map snd (List.filter fst (List.combine bls args)) + in + let constrs = solve {no_problems with to_solve} (Some (s, bls)) in + let to_solve = + List.map + snd (List.filter (fun (b, _) -> not b) (List.combine bls args)) in + add_rules_from_constrs constrs; + let res = + List.for_all (eq_modulo_constrs constrs) to_solve in + Time.restore t; + res + with + | Fatal _ -> Time.restore t; true + | _ -> Time.restore t; false + +(** [non_erasing_rec s] returns true if the normal form of any term [st] is + of the form [s't'] with s' <= s. This function only makes sense when there + is an order on symbols compatible with their dependency. *) +and non_erasing_rec : sym -> bool = fun s -> + let check_head_of_rule : rule -> bool = fun r -> + let h, _ = get_args (term_of_rhs r) in + match h with + | Symb (s', _) -> s' == s || non_erasing_rec s + | _ -> false in + List.for_all check_head_of_rule !(s.sym_rules) + +(** [check_single_rule bls s (lhs, rhs)] checks if the rule [lhs -> rhs] + satisfies the conditions mentioned above. *) +and check_single_rule : bool list -> sym -> term * term -> bool + = fun bls s (lhs, rhs) -> + let t = Time.save () in + let new_args n = + List.init n (fun _ -> (Meta (fresh_meta Kind 0, [||]))) in + let h1, args1 = get_args rhs in + let _, args2 = get_args lhs in + let new_args = new_args (List.length args2) in + let argss = List.combine args2 new_args in + let new_term = add_args (Symb (s, Nothing)) new_args in + let infer_from_constrs () = + let to_solve = + (new_term, rhs) :: + List.map snd (List.filter fst (List.combine bls argss)) in + let constrs = solve {no_problems with to_solve} (Some (s, bls)) in + let to_solve = + List.map + snd (List.filter (fun (b, _) -> not b) (List.combine bls argss)) + in + add_rules_from_constrs constrs; + let res = + List.for_all (eq_modulo_constrs constrs) to_solve in + Time.restore t; + res + in + try match h1 with + | Meta (m, _) when args1 = [] -> + let fn = function + | Meta (m', _) -> m == m' + | _ -> false in + if List.exists2 (fun b arg -> b && fn arg) bls args2 then true + else infer_from_constrs () + | Symb (s', _) when s == s' -> infer_from_constrs () + | Symb (s', _) -> non_erasing_rec s' + | _ -> false (* TODO *) + with + | Fatal _ -> Time.restore t; true + | _ -> Time.restore t; false + +(** [check_inj_sym bls s] checks if the symbol [s] is I-injective, where + I is represented by [bls]. Note that this function gives only a + sufficient condition. It may returns false whereas [s] is I-injective. *) +and check_inj_sym : bool list -> sym -> bool = fun bls s -> + match s.sym_mode with + | Injec l when inj_incls bls l -> true + | _ -> + let rules = !(s.sym_rules) in + let terms_of_rules = + List.map (fun r -> replace_patt_by_meta_rule (s, r)) rules in + let rec check_inj_rules : (term * term) list -> bool = function + | [] -> true + | r :: rs' -> + check_inj_rules rs' && + check_pair_of_rules bls s r (copy_rule r) && + List.fold_left + (fun acc r' -> acc && check_pair_of_rules bls s r r') + true rs' in + List.for_all (check_single_rule bls s) terms_of_rules && + check_inj_rules terms_of_rules + (** [solve builtins flag problems] attempts to solve [problems], after having sets the value of [can_instantiate] to [flag]. If there is no solution, the value [None] is returned. Otherwise [Some(cs)] is returned, where the @@ -307,5 +563,5 @@ let solve : sym StrMap.t -> bool -> problems -> unif_constrs option = fun builtins b p -> set_config builtins; can_instantiate := b; - try Some (solve p) with Fatal(_,m) -> + try Some (solve p None) with Fatal(_,m) -> if !log_enabled then log_solv (red "solve: %s") m; None