From 89a607256107cd0e10b6f1e876b8974752edddc9 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Mon, 25 Mar 2019 17:47:38 +0100 Subject: [PATCH 01/26] Define the relation used in the algorithm --- src/subject_reduction.ml | 43 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 src/subject_reduction.ml diff --git a/src/subject_reduction.ml b/src/subject_reduction.ml new file mode 100644 index 000000000..4d368a056 --- /dev/null +++ b/src/subject_reduction.ml @@ -0,0 +1,43 @@ +open Terms +open Print +open Basics + +module Eset = Set.Make( + struct + type t = (term * term) + let compare = Pervasives.compare + end) + +exception No_relation + +(** [find_relation t] calculates a pair of {!type:term} [A] and {!type:Eset.t} + [E] such that t:A[E] holds and raises the exception [No_relation] if + such a pair does not exist. Note that such a pair is unique if it exists + **) +let find_relation : term -> (term * Eset.t) = fun t -> + let t = unfold t in + match t with + | Symb (s, _) -> (!s.sym_type, Eset.empty) + | Appl (_, _) -> + (* Check if t is of the form ft₁...tn” *) + let rec appl_aux : term list -> term -> (sym * term list) = fun acc t -> + match t with + | Appl (t1, t2) -> appl_aux (t2 :: acc) t1 + | Symb (s, _) -> (s, acc) + | _ -> raise No_relation in + let (s, ts) = appl_aux [] t in + let rs = List.map find_relation ts in + let rec cal_relation t tlist rs es = match tlist with + | [] -> (t, es) + | t1 :: ts -> begin + match t with + | Prod (a, b) -> + let t' = Bindlib.subst b t1 in + let (a1, e1) :: rs' = rs in + let es' = Eset.add (a1, a) (Eset.union es e1) in + cal_relation t' ts rs' es' + | _ -> raise No_relation + end + in + cal_relation s.sym_type ts rs Eset.empty + | _ -> raise No_relation From 6b01d0609f17baa2137d5c69c84a326485ce2834 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Mon, 1 Apr 2019 16:06:43 +0200 Subject: [PATCH 02/26] Add the translation from Xml-light to Lambdapi --- src/sr.ml | 58 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/src/sr.ml b/src/sr.ml index e79773481..79a968534 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -69,6 +69,64 @@ let build_meta_type : int -> term = fun k -> let tk = _Meta mk (Array.map _Vari vs) in Bindlib.unbox (build_prod k tk) +(** Translation from Xml-light + (https://opam.ocaml.org/packages/xml-light/xml-light.2.4/) to Lambdapi **) + +(** [find_trs xml] finds the Xml node corresponding to the TRS in an Xml node + obtained from a CPF file. In a valid CPF file generated from external + tools for the Knuth-Bendix completion, there is exactly one such node. **) +let find_trs : Xml.xml -> Xml.xml = fun xml -> + let rec find_tag : string -> Xml.xml -> Xml.xml option = fun s xml -> + if Xml.tag xml = s then Some xml + else + let rec iter f = function + | [] -> None + | x :: xs -> match f x with + | None -> iter f xs + | y -> y in + iter (find_tag s) (Xml.children xml) + in + match find_tag "completionInput" xml with + | None -> assert false + | Some xml -> + match find_tag "trs" xml with + | None -> assert false + | Some xml -> xml + +(** [get_only_child xml] returns the only child of an Xml node given **) +let get_only_child : Xml.xml -> Xml.xml = fun xml -> + match Xml.children xml with + | [xml] -> xml + | _ -> assert false + +(** [get_term sign xml] translates an Xml node of tag name "var" or "funapp" + into a term according to the signature state of the original system **) +let rec get_term : Sign.t -> Xml.xml -> term = fun sign xml -> + match Xml.tag xml with + | "var" -> (* to finish *) assert false + | "funapp" -> begin match Xml.children xml with + | [] -> assert false + | f :: args -> + match get_only_child f with + | Xml.Element _ -> assert false + | Xml.PCData str -> + let args = List.map get_arg args in + let s, path = + match String.split_on_char '_' str with + | ["c"; path; s] -> + s, String.split_on_char '.' path + | _ -> assert false in + let sign = PathMap.find path Sign.(!loaded) in + let sym = + try symb (Sign.find sign s) with Not_found -> assert false in + List.fold_left (fun u v -> Appl (u, v)) s args + end + | _ -> assert false + +(** [get_arg xml] translates an Xml node of tag name "arg" into a term **) +and get_arg : Xml.xml -> term = fun xml -> get_term (get_only_child xml) + + (** [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 From 66be875e0d532bd935622817f76f9290f31c4602 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Tue, 2 Apr 2019 13:15:50 +0200 Subject: [PATCH 03/26] Fix some bugs --- src/sr.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/sr.ml b/src/sr.ml index 79a968534..9ea83336d 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -5,6 +5,7 @@ open Console open Terms open Print open Extra +open Files (** Logging function for typing. *) let log_subj = @@ -108,24 +109,24 @@ let rec get_term : Sign.t -> Xml.xml -> term = fun sign xml -> | [] -> assert false | f :: args -> match get_only_child f with - | Xml.Element _ -> assert false + | Xml.Element _ -> assert false | Xml.PCData str -> - let args = List.map get_arg args in + let args = List.map (get_arg sign) args in let s, path = match String.split_on_char '_' str with | ["c"; path; s] -> s, String.split_on_char '.' path - | _ -> assert false in + | _ -> assert false in let sign = PathMap.find path Sign.(!loaded) in let sym = try symb (Sign.find sign s) with Not_found -> assert false in - List.fold_left (fun u v -> Appl (u, v)) s args + List.fold_left (fun u v -> Appl (u, v)) sym args end - | _ -> assert false + | _ -> assert false (** [get_arg xml] translates an Xml node of tag name "arg" into a term **) -and get_arg : Xml.xml -> term = fun xml -> get_term (get_only_child xml) - +and get_arg : Sign.t -> Xml.xml -> term = fun sign xml -> + get_term sign (get_only_child xml) (** [check_rule builtins r] check whether rule [r] is well-typed. The program fails gracefully in case of error. *) From 09bf732045d87955c3bce9eb53d86f747366bfc6 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Tue, 9 Apr 2019 15:15:07 +0200 Subject: [PATCH 04/26] Add the function calculating critical pairs for algebraic LHS --- src/completion.ml | 147 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 src/completion.ml diff --git a/src/completion.ml b/src/completion.ml new file mode 100644 index 000000000..b3558bcb8 --- /dev/null +++ b/src/completion.ml @@ -0,0 +1,147 @@ +(** Completion procedure *) + +open Terms +open Basics +open Extra + +(** total strict order *) +type 'a order = 'a -> 'a -> bool + +let gt : 'a order -> 'a -> 'a -> bool = fun ord a b -> ord a b + +(** [ge ord] calculates the reflexive closure of [ord] *) +let ge : 'a order -> 'a -> 'a -> bool = fun ord a b -> a = b || ord a b + +(** [ord_lex ord] calculates the lexicographic order corresponding to the + alphabetical order [ord] *) +let ord_lex : 'a order -> ('a list) order = fun ord l1 l2 -> + let rec elim_comm l1 l2 = match (l1, l2) with + | h1 :: t1, h2 :: t2 -> begin match ord h1 h2 with + | false -> if h1 = h2 then elim_comm t1 t2 else assert false + | _ -> l1, l2 + end + | _ -> l1, l2 in + match elim_comm l1 l2 with + | [], _ -> false + | _, [] -> true + | h1 :: _, h2 :: _ -> ord h1 h2 + +let get_sym : term -> sym = fun t -> match unfold t with + | Symb (s, _) -> s + | _ -> assert false + +(** [lpo ord] calculates the lexicographic path ordering corresponding to + the strict total order [ord] on the set of all function symbols *) +let rec lpo : sym order -> term order = fun ord t1 t2 -> + let f, args = get_args t1 in + let f = get_sym f in + if List.exists (fun x -> ge (lpo ord) x t2) args then true + else + let g, args' = get_args t2 in + let g = get_sym g in + match ord f g with + | true -> + if List.for_all (fun x -> gt (lpo ord) t1 x) args' then true + else + false + | false -> + if f = g then + List.for_all (fun x -> gt (lpo ord) t1 x) args' && + ord_lex (lpo ord) args args' + else false + +(** [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 + 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) + +type rule_ = sym * pp_hint * rule + +(** [cp builtins r1 r2] calculates the critical pairs of the rules r1 and r2 + *) +let cp : sym StrMap.t -> rule_ -> rule_ -> (term * term) list + = fun builtins (s1, h1, r1) (s2, h2, r2) -> + let arity1 = Bindlib.mbinder_arity r1.rhs in + let arity2 = Bindlib.mbinder_arity r2.rhs in + let cps = ref [] in + let rec to_m : 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 (to_m 0 metas a) (Bindlib.bind_var x (to_m 0 metas t)) + | Appl (t, u) -> _Appl (to_m (k + 1) metas t) (to_m 0 metas u) + | Patt (i, n, a) -> + begin + let a = Array.map (to_m 0 metas) 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 + | _ -> assert false in + let metas1 = Array.init arity1 (fun _ -> None) in + let lhs1 = List.map (fun p -> Bindlib.unbox (to_m 0 metas1 p)) r1.lhs in + let lhs1 = Basics.add_args (Symb (s1, h1)) lhs1 in + let find_cp : term -> unit = fun t -> + let metas1 = Array.init arity1 (fun _ -> None) in + let metas2 = Array.init arity2 (fun _ -> None) in + let lhs2 = List.map (fun p -> Bindlib.unbox (to_m 0 metas2 p)) r2.lhs in + let lhs2 = Basics.add_args (Symb (s2, h2)) lhs2 in + 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_envs1 = Array.map fn metas1 in + let te_envs2 = Array.map fn metas2 in + let rhs1 = Bindlib.msubst r1.rhs te_envs1 in + let rhs2 = Bindlib.msubst r2.rhs te_envs2 in + let to_solve = [(t, lhs2)] in + match Unif.(solve builtins false {no_problems with to_solve}) with + | None -> () + | Some cs -> + if cs <> [] then () else cps := (rhs1, rhs2) :: !cps in + Basics.iter find_cp lhs1; (* This only works for algebraic LHS *) + !cps + +(** [critical_pairs builtins rs] calculates the list of all critical pairs + of the rewrite system rs *) +let rec critical_pairs : sym StrMap.t -> rule_ list -> (term * term) list + = fun builtins rs -> + match rs with + | [] -> [] + | r :: rs' -> + let cps = critical_pairs builtins rs in + List.fold_left + (fun acc r' -> + cp builtins r r' @ cp builtins r' r @ acc) + (cp builtins r r @ cps) rs' From cc7a69218f7022b020dbfa0f6e1962405bb24b36 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Thu, 11 Apr 2019 16:47:29 +0200 Subject: [PATCH 05/26] Add first-order syntactic unification --- src/completion.ml | 241 ++++++++++++++++++++++++++-------------------- 1 file changed, 138 insertions(+), 103 deletions(-) diff --git a/src/completion.ml b/src/completion.ml index b3558bcb8..519bf4162 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -1,54 +1,46 @@ -(** Completion procedure *) +(** Completion procedure for closed equations *) open Terms open Basics open Extra +open Timed -(** total strict order *) -type 'a order = 'a -> 'a -> bool +type 'a cmp = 'a -> 'a -> int -let gt : 'a order -> 'a -> 'a -> bool = fun ord a b -> ord a b - -(** [ge ord] calculates the reflexive closure of [ord] *) -let ge : 'a order -> 'a -> 'a -> bool = fun ord a b -> a = b || ord a b - -(** [ord_lex ord] calculates the lexicographic order corresponding to the +(** [ord_lex ord] computes the lexicographic order corresponding to the alphabetical order [ord] *) -let ord_lex : 'a order -> ('a list) order = fun ord l1 l2 -> - let rec elim_comm l1 l2 = match (l1, l2) with - | h1 :: t1, h2 :: t2 -> begin match ord h1 h2 with - | false -> if h1 = h2 then elim_comm t1 t2 else assert false - | _ -> l1, l2 - end - | _ -> l1, l2 in - match elim_comm l1 l2 with - | [], _ -> false - | _, [] -> true - | h1 :: _, h2 :: _ -> ord h1 h2 +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 let get_sym : term -> sym = fun t -> match unfold t with | Symb (s, _) -> s - | _ -> assert false + | _ -> assert false -(** [lpo ord] calculates the lexicographic path ordering corresponding to +(** [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 order -> term order = fun ord t1 t2 -> +let rec lpo : sym cmp -> term cmp = fun ord t1 t2 -> let f, args = get_args t1 in let f = get_sym f in - if List.exists (fun x -> ge (lpo ord) x t2) args then true + if List.exists (fun x -> lpo ord x t2 >= 0) args then 1 else let g, args' = get_args t2 in let g = get_sym g in match ord f g with - | true -> - if List.for_all (fun x -> gt (lpo ord) t1 x) args' then true - else - false - | false -> - if f = g then - List.for_all (fun x -> gt (lpo ord) t1 x) args' && + | 1 -> + 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 false + else -1 + | _ -> -1 (** [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 @@ -72,76 +64,119 @@ let build_meta_type : int -> term = fun k -> let tk = _Meta mk (Array.map _Vari vs) in Bindlib.unbox (build_prod k tk) -type rule_ = sym * pp_hint * rule +type rule = sym * Terms.rule + +(** [to_m k metas t] computes a new (boxed) term by replacing every pattern + variable in [t] by a fresh meta-variable and store the latter in [metas], + where [k] indicates the order of the term obtained *) +let rec to_m : 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 (to_m 0 metas a) (Bindlib.bind_var x (to_m 0 metas t)) + | Appl (t, u) -> _Appl (to_m (k + 1) metas t) (to_m 0 metas u) + | Patt (i, n, a) -> + begin + let a = Array.map (to_m 0 metas) 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 + | _ -> assert false + +(** [to_term r] translates the rule [r] into a pair of terms *) +let to_term : rule -> term * term = fun (s, r) -> + let arity = Bindlib.mbinder_arity r.rhs in + let metas = Array.init arity (fun _ -> None) in + let lhs = List.map (fun p -> Bindlib.unbox (to_m 0 metas p)) r.lhs in + let lhs = add_args (symb s) lhs in + (* [to_term_env m] computes the term with environment correspoding to the + meta-variable [m] *) + let to_term_env : meta option -> term_env = fun 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 + let terms_env = Array.map to_term_env metas in + let rhs = Bindlib.msubst r.rhs terms_env in + (lhs, rhs) + +(** First-order syntactic unification *) + +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, ts1), Meta (_, ts2) -> + assert (ts1 = [||] && ts2 = [||]); + 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, ts1), t2) + | (t2, Meta (m1, ts1)) -> + if occurs m1 t2 then raise Unsolvable + else + assert (ts1 = [||]); + 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 -(** [cp builtins r1 r2] calculates the critical pairs of the rules r1 and r2 - *) -let cp : sym StrMap.t -> rule_ -> rule_ -> (term * term) list - = fun builtins (s1, h1, r1) (s2, h2, r2) -> - let arity1 = Bindlib.mbinder_arity r1.rhs in - let arity2 = Bindlib.mbinder_arity r2.rhs in - let cps = ref [] in - let rec to_m : 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 (to_m 0 metas a) (Bindlib.bind_var x (to_m 0 metas t)) - | Appl (t, u) -> _Appl (to_m (k + 1) metas t) (to_m 0 metas u) - | Patt (i, n, a) -> - begin - let a = Array.map (to_m 0 metas) 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 - | _ -> assert false in - let metas1 = Array.init arity1 (fun _ -> None) in - let lhs1 = List.map (fun p -> Bindlib.unbox (to_m 0 metas1 p)) r1.lhs in - let lhs1 = Basics.add_args (Symb (s1, h1)) lhs1 in - let find_cp : term -> unit = fun t -> - let metas1 = Array.init arity1 (fun _ -> None) in - let metas2 = Array.init arity2 (fun _ -> None) in - let lhs2 = List.map (fun p -> Bindlib.unbox (to_m 0 metas2 p)) r2.lhs in - let lhs2 = Basics.add_args (Symb (s2, h2)) lhs2 in - 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_envs1 = Array.map fn metas1 in - let te_envs2 = Array.map fn metas2 in - let rhs1 = Bindlib.msubst r1.rhs te_envs1 in - let rhs2 = Bindlib.msubst r2.rhs te_envs2 in - let to_solve = [(t, lhs2)] in - match Unif.(solve builtins false {no_problems with to_solve}) with - | None -> () - | Some cs -> - if cs <> [] then () else cps := (rhs1, rhs2) :: !cps in - Basics.iter find_cp lhs1; (* This only works for algebraic LHS *) - !cps +(** [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 -(** [critical_pairs builtins rs] calculates the list of all critical pairs - of the rewrite system rs *) -let rec critical_pairs : sym StrMap.t -> rule_ list -> (term * term) list - = fun builtins rs -> - match rs with - | [] -> [] - | r :: rs' -> - let cps = critical_pairs builtins rs in - List.fold_left - (fun acc r' -> - cp builtins r r' @ cp builtins r' r @ acc) - (cp builtins r r @ cps) rs' +(** [cps rs] computes the critical pairs of the rewrite system [rs] *) +let cps : rule list -> (term * term) list = fun rs -> + let acc = ref [] in + let cps_aux : rule -> rule -> unit = fun r1 r2 -> + let lhs1, rhs1 = to_term r1 in + let lhs2, rhs2 = to_term r2 in + let find_cp : term -> term -> unit = fun t1 t2 -> + 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 (iter (find_cp lhs1)) args2; + List.iter (iter (fun t -> find_cp t lhs2)) args1 in + let rec cps rs = + match rs with + | [] -> () + | r :: rs' -> List.iter (cps_aux r) rs; cps rs' in + cps rs; + !acc From 03fde4064b04c9fa7b9d7bd8b01bbe7ad93da1ea Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 12 Apr 2019 11:39:00 +0200 Subject: [PATCH 06/26] Add rewriting for closed terms and closed rules --- src/completion.ml | 58 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/src/completion.ml b/src/completion.ml index 519bf4162..f4ad7d160 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -180,3 +180,61 @@ let cps : rule list -> (term * term) list = fun rs -> | r :: rs' -> List.iter (cps_aux r) rs; cps rs' in cps rs; !acc + +(** Rewriting for closed rules and closed terms *) + +type ctxt = term -> term + +(** [match_rule ctxt t (s, r)] attempts to rewrite [ctxt[t]] by appling the + rule [(s, t)]. *) +let match_rule : ctxt -> term -> rule -> term option = fun ctxt t (s, r) -> + let lhs = add_args (symb s) r.lhs in + if eq t lhs then Some (ctxt (term_of_rhs r)) else None + +(** [match_rules ctxt t rs] attempts to rewrite [ctxt[t]] by appling the + rules [rs]. *) +let match_rules : ctxt -> term -> rule list -> term option = fun ctxt t rs -> + List.map_find (match_rule ctxt t) rs + +(** [rewrite t rs] attempts to rewrite [t] in the rewrite system [rs] *) +let rewrite : term -> rule list -> term option = fun t rs -> + let t = unfold t in + match t with + | Wild + | TRef _ + | Vari _ + | Type + | Kind + | Patt _ + | Meta _ + | TEnv _ + | Prod _ + | Abst _ -> None + | Symb _ -> match_rules (fun t -> t) t rs + | Appl (t, u) -> + match match_rules (fun t -> t) t rs with + | None -> + let ctxt = fun t -> Appl (t, u) in + begin match match_rules ctxt t rs with + | None -> + let ctxt = fun u -> Appl (t, u) in + match_rules ctxt u rs + | res -> res + end + | res -> res + +(** [nf t rs] attempts to compute a normal form of [t] in the rewrite system + [rs]. *) +let rec nf : term -> rule list -> term = fun t rs -> + match rewrite t rs with + | None -> t + | Some t -> nf t rs + +(** [to_rule (lhs, rhs)] translates the pair [(lhs, rhs)] into a rule for + closed lhs and rhs *) +let to_rule : term * term -> rule = fun (lhs, rhs) -> + let (s, args) = get_args lhs in + let s = get_sym s in + 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 = [||] } From 768f1b65051a486d0b508bef5515bd6e156273e0 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 12 Apr 2019 14:37:56 +0200 Subject: [PATCH 07/26] Add Huet's completion procedure --- src/completion.ml | 56 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 54 insertions(+), 2 deletions(-) diff --git a/src/completion.ml b/src/completion.ml index f4ad7d160..fb6282dea 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -196,7 +196,7 @@ let match_rule : ctxt -> term -> rule -> term option = fun ctxt t (s, r) -> let match_rules : ctxt -> term -> rule list -> term option = fun ctxt t rs -> List.map_find (match_rule ctxt t) rs -(** [rewrite t rs] attempts to rewrite [t] in the rewrite system [rs] *) +(** [rewrite t rs] attempts to rewrite [t] in the rewrite system [rs]. *) let rewrite : term -> rule list -> term option = fun t rs -> let t = unfold t in match t with @@ -231,10 +231,62 @@ let rec nf : term -> rule list -> term = fun t rs -> | Some t -> nf t rs (** [to_rule (lhs, rhs)] translates the pair [(lhs, rhs)] into a rule for - closed lhs and rhs *) + closed lhs and rhs. *) let to_rule : term * term -> rule = fun (lhs, rhs) -> let (s, args) = get_args lhs in let s = get_sym s in 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 = [||] } + +(** [completion eqs ord] applies Huet's completion procedure on the set of + equations [eqs] by using the lexicographic path ordering corresponding to + the order [ord] on the set of function symbols. *) +let completion : (term * term) list -> sym cmp -> rule list = fun eqs ord -> + let ord = lpo ord in + let eqs = ref eqs in + let marked_rs = ref [] in + let unmarked_rs = ref [] in + let get_head l = + match l with + | [] -> assert false + | hd :: tl -> (hd, tl) in + while !eqs <> [] || !unmarked_rs <> [] do + while !eqs <> [] do + let (s, t), eqs' = get_head !eqs in + let rs = !marked_rs @ !unmarked_rs in + let snf = nf s rs in + let tnf = nf t rs in + if eq snf tnf then eqs := eqs' + else begin + let lhs, rhs = if ord snf tnf > 0 then snf, tnf else tnf, snf in + let new_rule = to_rule (lhs, rhs) in + let sep_rule b (mrs, umrs, eqs) r = + let lhs, rhs = to_term r in + match rewrite lhs [new_rule] with + | None -> + let rhs = nf rhs (new_rule :: rs) in + let r = to_rule (lhs, rhs) in + if b then (r :: mrs, umrs, eqs) else (mrs, r :: umrs, eqs) + | Some lhs' -> + (mrs, umrs, (lhs', rhs) :: eqs) in + let (mrs, umrs, eqs') = + List.fold_left (sep_rule true) ([], [new_rule], eqs') !marked_rs in + let (mrs, umrs, eqs') = + List.fold_left (sep_rule false) (mrs, umrs, eqs') !unmarked_rs in + marked_rs := mrs; + unmarked_rs := umrs; + eqs := eqs' + end + done; + if !unmarked_rs <> [] then begin + let r, umrs = get_head !unmarked_rs in + let cps = + List.fold_left (fun acc r' -> cps [r; r'] @ acc) [] (r :: !marked_rs) + in + eqs := cps; + unmarked_rs := umrs; + marked_rs := r :: !marked_rs + end; + done; + !marked_rs From 9ae656731b1b7b4b02d7181bd1bced0e49e754db Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Wed, 17 Apr 2019 13:38:40 +0200 Subject: [PATCH 08/26] Simplify the completion procedure --- src/completion.ml | 347 +++++++++++----------------------------------- 1 file changed, 82 insertions(+), 265 deletions(-) diff --git a/src/completion.ml b/src/completion.ml index fb6282dea..61d770490 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -5,288 +5,105 @@ open Basics open Extra open Timed -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 - -let get_sym : term -> sym = fun t -> match unfold t with - | Symb (s, _) -> s - | _ -> assert false - (** [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 -> + the strict total order [ord] on the set of all function symbols. *) +let rec lpo : sym Ord.cmp -> term Ord.cmp = fun ord t1 t2 -> let f, args = get_args t1 in - let f = get_sym f in + let f = get_symb f in if List.exists (fun x -> lpo ord x t2 >= 0) args then 1 else let g, args' = get_args t2 in - let g = get_sym g in + let g = get_symb g in match ord f g with | 1 -> 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' + Ord.ord_lex (lpo ord) args args' else -1 | _ -> -1 -(** [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 - 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) - -type rule = sym * Terms.rule - -(** [to_m k metas t] computes a new (boxed) term by replacing every pattern - variable in [t] by a fresh meta-variable and store the latter in [metas], - where [k] indicates the order of the term obtained *) -let rec to_m : 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 (to_m 0 metas a) (Bindlib.bind_var x (to_m 0 metas t)) - | Appl (t, u) -> _Appl (to_m (k + 1) metas t) (to_m 0 metas u) - | Patt (i, n, a) -> - begin - let a = Array.map (to_m 0 metas) 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 - | _ -> assert false - -(** [to_term r] translates the rule [r] into a pair of terms *) -let to_term : rule -> term * term = fun (s, r) -> - let arity = Bindlib.mbinder_arity r.rhs in - let metas = Array.init arity (fun _ -> None) in - let lhs = List.map (fun p -> Bindlib.unbox (to_m 0 metas p)) r.lhs in - let lhs = add_args (symb s) lhs in - (* [to_term_env m] computes the term with environment correspoding to the - meta-variable [m] *) - let to_term_env : meta option -> term_env = fun 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 - let terms_env = Array.map to_term_env metas in - let rhs = Bindlib.msubst r.rhs terms_env in - (lhs, rhs) - -(** First-order syntactic unification *) - -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, ts1), Meta (_, ts2) -> - assert (ts1 = [||] && ts2 = [||]); - 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, ts1), t2) - | (t2, Meta (m1, ts1)) -> - if occurs m1 t2 then raise Unsolvable - else - assert (ts1 = [||]); - 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 : rule list -> (term * term) list = fun rs -> - let acc = ref [] in - let cps_aux : rule -> rule -> unit = fun r1 r2 -> - let lhs1, rhs1 = to_term r1 in - let lhs2, rhs2 = to_term r2 in - let find_cp : term -> term -> unit = fun t1 t2 -> - 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 (iter (find_cp lhs1)) args2; - List.iter (iter (fun t -> find_cp t lhs2)) args1 in - let rec cps rs = - match rs with - | [] -> () - | r :: rs' -> List.iter (cps_aux r) rs; cps rs' in - cps rs; - !acc - -(** Rewriting for closed rules and closed terms *) - -type ctxt = term -> term - -(** [match_rule ctxt t (s, r)] attempts to rewrite [ctxt[t]] by appling the - rule [(s, t)]. *) -let match_rule : ctxt -> term -> rule -> term option = fun ctxt t (s, r) -> - let lhs = add_args (symb s) r.lhs in - if eq t lhs then Some (ctxt (term_of_rhs r)) else None - -(** [match_rules ctxt t rs] attempts to rewrite [ctxt[t]] by appling the - rules [rs]. *) -let match_rules : ctxt -> term -> rule list -> term option = fun ctxt t rs -> - List.map_find (match_rule ctxt t) rs - -(** [rewrite t rs] attempts to rewrite [t] in the rewrite system [rs]. *) -let rewrite : term -> rule list -> term option = fun t rs -> - let t = unfold t in - match t with - | Wild - | TRef _ - | Vari _ - | Type - | Kind - | Patt _ - | Meta _ - | TEnv _ - | Prod _ - | Abst _ -> None - | Symb _ -> match_rules (fun t -> t) t rs - | Appl (t, u) -> - match match_rules (fun t -> t) t rs with - | None -> - let ctxt = fun t -> Appl (t, u) in - begin match match_rules ctxt t rs with - | None -> - let ctxt = fun u -> Appl (t, u) in - match_rules ctxt u rs - | res -> res - end - | res -> res - -(** [nf t rs] attempts to compute a normal form of [t] in the rewrite system - [rs]. *) -let rec nf : term -> rule list -> term = fun t rs -> - match rewrite t rs with - | None -> t - | Some t -> nf t rs - -(** [to_rule (lhs, rhs)] translates the pair [(lhs, rhs)] into a rule for - closed lhs and rhs. *) -let to_rule : term * term -> rule = fun (lhs, rhs) -> +(** [to_rule (lhs, rhs)] tranlates the pair [(lhs, rhs)] of closed terms into + a rule. *) +let to_rule : term * term -> sym * rule = fun (lhs, rhs) -> let (s, args) = get_args lhs in - let s = get_sym s in + let s = get_symb s in 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 = [||] } -(** [completion eqs ord] applies Huet's completion procedure on the set of - equations [eqs] by using the lexicographic path ordering corresponding to - the order [ord] on the set of function symbols. *) -let completion : (term * term) list -> sym cmp -> rule list = fun eqs ord -> - let ord = lpo ord in - let eqs = ref eqs in - let marked_rs = ref [] in - let unmarked_rs = ref [] in - let get_head l = - match l with - | [] -> assert false - | hd :: tl -> (hd, tl) in - while !eqs <> [] || !unmarked_rs <> [] do - while !eqs <> [] do - let (s, t), eqs' = get_head !eqs in - let rs = !marked_rs @ !unmarked_rs in - let snf = nf s rs in - let tnf = nf t rs in - if eq snf tnf then eqs := eqs' - else begin - let lhs, rhs = if ord snf tnf > 0 then snf, tnf else tnf, snf in - let new_rule = to_rule (lhs, rhs) in - let sep_rule b (mrs, umrs, eqs) r = - let lhs, rhs = to_term r in - match rewrite lhs [new_rule] with - | None -> - let rhs = nf rhs (new_rule :: rs) in - let r = to_rule (lhs, rhs) in - if b then (r :: mrs, umrs, eqs) else (mrs, r :: umrs, eqs) - | Some lhs' -> - (mrs, umrs, (lhs', rhs) :: eqs) in - let (mrs, umrs, eqs') = - List.fold_left (sep_rule true) ([], [new_rule], eqs') !marked_rs in - let (mrs, umrs, eqs') = - List.fold_left (sep_rule false) (mrs, umrs, eqs') !unmarked_rs in - marked_rs := mrs; - unmarked_rs := umrs; - eqs := eqs' - end - done; - if !unmarked_rs <> [] then begin - let r, umrs = get_head !unmarked_rs in - let cps = - List.fold_left (fun acc r' -> cps [r; r'] @ acc) [] (r :: !marked_rs) +(** [completion eqs ord] returns a pair of time points [(t1, t2)] where t1 + corresponds to the used-defined rewrite system and t2 to the convergent + rewrite system obtained using the completion procedure. *) +let completion : (term * term) list -> sym Ord.cmp -> Time.t * Time.t + = fun eqs ord -> + let t1 = Time.save () in + 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 (to_rule (t1, t2)) + | _ -> add_rule (to_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) = to_terms (s, r) in + let lhs' = Eval.snf lhs in + let rhs' = Eval.snf rhs in + if eq lhs lhs' then acc + else begin + match lpo lhs' rhs' with + | 0 -> acc + | k when k > 0 -> + to_add := to_rule (lhs', rhs') :: !to_add; + b := true; + r :: acc + | _ -> + to_add := to_rule (rhs', lhs') :: !to_add; + b := true; + r :: acc + end in - eqs := cps; - unmarked_rs := umrs; - marked_rs := r :: !marked_rs - end; - done; - !marked_rs + let rec aux acc f rs = + match rs with + | [] -> () + | r :: rs' -> let acc = f acc rs' r in aux 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; + let t2 = Time.save () in + t1, t2 From dc52db0c7e2b2fccc1e0fe49cfec664a57fc2acd Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Wed, 17 Apr 2019 13:45:43 +0200 Subject: [PATCH 09/26] Reorganize some files --- src/basics.ml | 77 ++++++++++++++++++++++++++++++++++++++++++++++ src/confluence.ml | 78 +++++++++++++++++++++++++++++++++++++++++++++++ src/extra.ml | 21 +++++++++++++ 3 files changed, 176 insertions(+) create mode 100644 src/confluence.ml diff --git a/src/basics.ml b/src/basics.ml index a2dd27b98..eea4a8ad6 100644 --- a/src/basics.ml +++ b/src/basics.ml @@ -112,6 +112,11 @@ let is_symb : sym -> term -> bool = fun s t -> | Symb(r,_) -> r == s | _ -> false +let get_symb : term -> sym = fun t -> + match unfold t with + | Symb (s, _) -> s + | _ -> assert false + (** [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 @@ -201,6 +206,57 @@ let has_metas : term -> bool = let exception Found in fun t -> try iter_meta (fun _ -> raise Found) t; false with Found -> true +(** [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 + 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) + +(** [to_m 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 to_m : 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 (to_m 0 metas a) (Bindlib.bind_var x (to_m 0 metas t)) + | Appl (t, u) -> _Appl (to_m (k + 1) metas t) (to_m 0 metas u) + | Patt (i, n, a) -> + begin + let a = Array.map (to_m 0 metas) 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 + | _ -> assert false + (** [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 +295,24 @@ 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) + +(** [to_terms r] translates the rule [r] into a pair of terms. The pattern + variables in the LHS are replaced by metavariables and the terms with + environment in the RHS are replaced by their corresponding metavariables. + *) +let to_terms : sym * rule -> term * term = fun (s, r) -> + let arity = Bindlib.mbinder_arity r.rhs in + let metas = Array.init arity (fun _ -> None) in + let lhs = List.map (fun p -> Bindlib.unbox (to_m 0 metas p)) r.lhs in + let lhs = add_args (symb s) lhs in + (* [to_term_env m] computes the term with environment corresponding to the + metavariable [m]. *) + let to_term_env : meta option -> term_env = fun 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 + let terms_env = Array.map to_term_env metas in + let rhs = Bindlib.msubst r.rhs terms_env in + (lhs, rhs) diff --git a/src/confluence.ml b/src/confluence.ml new file mode 100644 index 000000000..172d3214d --- /dev/null +++ b/src/confluence.ml @@ -0,0 +1,78 @@ +(** 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, ts1), Meta (_, ts2) -> + assert (ts1 = [||] && ts2 = [||]); + 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, ts1), t2) + | (t2, Meta (m1, ts1)) -> + if occurs m1 t2 then raise Unsolvable + else + assert (ts1 = [||]); + 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 to_terms 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 -> + 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..d8ce766e0 100644 --- a/src/extra.ml +++ b/src/extra.ml @@ -130,6 +130,27 @@ module Array = Array.length a1 = Array.length a2 && for_all2 eq a1 a2 end +module Ord = + struct + (** 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 + end + (* Functional maps with [int] keys. *) module IntMap = Map.Make(Int) From 9b006fb3b16a8e0886bd7ebf6ceb983fe274cd51 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 19 Apr 2019 13:39:05 +0200 Subject: [PATCH 10/26] Remove subject_reduction.ml --- src/subject_reduction.ml | 43 ---------------------------------------- 1 file changed, 43 deletions(-) delete mode 100644 src/subject_reduction.ml diff --git a/src/subject_reduction.ml b/src/subject_reduction.ml deleted file mode 100644 index 4d368a056..000000000 --- a/src/subject_reduction.ml +++ /dev/null @@ -1,43 +0,0 @@ -open Terms -open Print -open Basics - -module Eset = Set.Make( - struct - type t = (term * term) - let compare = Pervasives.compare - end) - -exception No_relation - -(** [find_relation t] calculates a pair of {!type:term} [A] and {!type:Eset.t} - [E] such that t:A[E] holds and raises the exception [No_relation] if - such a pair does not exist. Note that such a pair is unique if it exists - **) -let find_relation : term -> (term * Eset.t) = fun t -> - let t = unfold t in - match t with - | Symb (s, _) -> (!s.sym_type, Eset.empty) - | Appl (_, _) -> - (* Check if t is of the form ft₁...tn” *) - let rec appl_aux : term list -> term -> (sym * term list) = fun acc t -> - match t with - | Appl (t1, t2) -> appl_aux (t2 :: acc) t1 - | Symb (s, _) -> (s, acc) - | _ -> raise No_relation in - let (s, ts) = appl_aux [] t in - let rs = List.map find_relation ts in - let rec cal_relation t tlist rs es = match tlist with - | [] -> (t, es) - | t1 :: ts -> begin - match t with - | Prod (a, b) -> - let t' = Bindlib.subst b t1 in - let (a1, e1) :: rs' = rs in - let es' = Eset.add (a1, a) (Eset.union es e1) in - cal_relation t' ts rs' es' - | _ -> raise No_relation - end - in - cal_relation s.sym_type ts rs Eset.empty - | _ -> raise No_relation From 6aa0da75e2647224cdd2c4ac144280d637c723c9 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 19 Apr 2019 13:40:38 +0200 Subject: [PATCH 11/26] Modify the completion procedure --- src/completion.ml | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/completion.ml b/src/completion.ml index 61d770490..ff43a1eae 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -36,9 +36,8 @@ let to_rule : term * term -> sym * rule = fun (lhs, rhs) -> (** [completion eqs ord] returns a pair of time points [(t1, t2)] where t1 corresponds to the used-defined rewrite system and t2 to the convergent rewrite system obtained using the completion procedure. *) -let completion : (term * term) list -> sym Ord.cmp -> Time.t * Time.t +let completion : (term * term) list -> sym Ord.cmp -> (sym * rule list) list = fun eqs ord -> - let t1 = Time.save () in let lpo = lpo ord in (* [symbs] is used to store all the symbols appearing in the equations. *) let symbs = ref [] in @@ -52,8 +51,7 @@ let completion : (term * term) list -> sym Ord.cmp -> Time.t * Time.t | _ -> () 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 + 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 @@ -81,29 +79,27 @@ let completion : (term * term) list -> sym Ord.cmp -> Time.t * Time.t let (lhs, rhs) = to_terms (s, r) in let lhs' = Eval.snf lhs in let rhs' = Eval.snf rhs in - if eq lhs lhs' then acc + s.sym_rules := r :: !(s.sym_rules); + if eq lhs lhs' then () else begin match lpo lhs' rhs' with - | 0 -> acc + | 0 -> () | k when k > 0 -> to_add := to_rule (lhs', rhs') :: !to_add; b := true; - r :: acc | _ -> to_add := to_rule (rhs', lhs') :: !to_add; b := true; - r :: acc end in let rec aux acc f rs = match rs with | [] -> () - | r :: rs' -> let acc = f acc rs' r in aux acc f rs' in + | 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; - let t2 = Time.save () in - t1, t2 + List.map (fun s -> (s, !(s.sym_rules))) !symbs From 14ad33326e513cf2c9382a69ef338ebcb1c21137 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 19 Apr 2019 13:43:27 +0200 Subject: [PATCH 12/26] Modify the main function for checking SR --- src/basics.ml | 75 +++++++++++++- src/handle.ml | 6 +- src/sr.ml | 266 ++++++++++++-------------------------------------- src/unif.ml | 3 +- 4 files changed, 140 insertions(+), 210 deletions(-) diff --git a/src/basics.ml b/src/basics.ml index eea4a8ad6..a26659246 100644 --- a/src/basics.ml +++ b/src/basics.ml @@ -112,6 +112,8 @@ let is_symb : sym -> term -> bool = fun s t -> | Symb(r,_) -> r == s | _ -> false +(** [get_symb t] checks that [t] is of the form [Symb (s , _)] and returns + [s]. *) let get_symb : term -> sym = fun t -> match unfold t with | Symb (s, _) -> s @@ -228,6 +230,12 @@ let build_meta_type : int -> term = fun k -> 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 } + (** [to_m 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 *) @@ -245,18 +253,51 @@ let rec to_m : int -> (meta option) array -> term -> tbox = fun k metas t -> let l = Array.length a in match i with | None -> - let m = fresh_meta ~name:n (build_meta_type (l + k)) l in + let m = fresh_meta ~name:n Kind 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 + let m = fresh_meta ~name:n Kind l in metas.(i) <- Some m; _Meta m a end | _ -> assert false +(** [to_closed 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 to_closed : (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 (to_closed symbs a) (Bindlib.bind_var x (to_closed symbs t)) + | Appl (t, u) -> _Appl (to_closed symbs t) (to_closed symbs u) + | Patt (i, n, _) -> + begin + match i with + | None -> + let t_n = new_symb ("t_" ^ n) Kind 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) Kind 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 + | _ -> assert false + (** [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 = @@ -316,3 +357,33 @@ let to_terms : sym * rule -> term * term = fun (s, r) -> let terms_env = Array.map to_term_env metas in let rhs = Bindlib.msubst r.rhs terms_env in (lhs, rhs) + +(** [to_closed_terms r] translates the rule [r] into a pair of terms. The + pattern variables in the LHS are replaced by fresh symbols as in the + function [to_closed] and the terms with environment in the RHS are + replaced by their corresponding symbols. *) +let to_closed_terms : sym * rule -> term * term = fun (s, r) -> + let arity = Bindlib.mbinder_arity r.rhs in + let symbs = Array.init arity (fun _ -> None) in + let lhs = List.map (fun p -> Bindlib.unbox (to_closed symbs p)) r.lhs in + let lhs = add_args (symb s) lhs in + let to_term_env : sym option -> term_env = fun s -> + let s = match s with Some s -> s | None -> assert false in + TE_Some (Bindlib.unbox (Bindlib.bind_mvar [||] (_Symb s Nothing))) in + let terms_env = Array.map to_term_env symbs in + let rhs = Bindlib.msubst r.rhs terms_env in + (lhs, rhs) + +exception Not_FO + +(** [check_fo t] checks that [t] is a first-order term. *) +let rec check_fo : term -> unit = fun t -> + match t with + | Type + | Kind + | Symb _ + | Wild + | Patt _ -> () + | Meta (_, ar) when ar = [||] -> () + | Appl (u, v) -> check_fo u; check_fo v + | _ -> raise Not_FO diff --git a/src/handle.ml b/src/handle.ml index 9fb56e070..6a92418d4 100644 --- a/src/handle.ml +++ b/src/handle.ml @@ -125,7 +125,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = let (s,_,_) as r = scope_rule ss r in if !(s.sym_def) <> None then fatal_no_pos "Symbol [%s] cannot be (re)defined." s.sym_name; - Sr.check_rule ss.builtins r; r + r in let rs = List.map handle_rule rs in (* Adding the rules all at once. *) @@ -133,7 +133,8 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = out 3 "(rule) %a\n" Print.pp_rule (s,h,r.elt); Sign.add_rule ss.signature s r.elt in - List.iter add_rule rs; (ss, None) + List.iter add_rule rs; + List.iter (Sr.check_rule ss.builtins) rs; (ss, None) | P_definition(op,x,xs,ao,t) -> (* We check that [x] is not already used. *) if Sign.mem ss.signature x.elt then @@ -208,6 +209,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = wrn cmd.pos "Proof aborted."; ss | P_proof_admit -> (* If the proof is finished, display a warning. *) + if Proof.finished st then wrn cmd.pos "The proof is finished. You can use 'qed' instead."; (* Add a symbol corresponding to the proof, with a warning. *) diff --git a/src/sr.ml b/src/sr.ml index 9ea83336d..e6d280c4f 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -2,222 +2,80 @@ open Timed open Console -open Terms open Print open Extra -open Files +open Terms +open Basics (** Logging function for typing. *) let log_subj = new_logger 'j' "subj" "debugging information for subject-reduction" let log_subj = log_subj.logger -(** Representation of a substitution. *) -type subst = tvar array * term array - -(** [subst_from_constrs cs] builds a //typing substitution// from the list of - constraints [cs]. The returned substitution is given by a couple of arrays - [(xs,ts)] of the same length. The array [xs] contains the variables to be - substituted using the terms of [ts] at the same index. *) -let subst_from_constrs : (term * term) list -> subst = fun cs -> - let rec build_sub acc cs = - match cs with - | [] -> List.split acc - | (a,b)::cs -> - let (ha,argsa) = Basics.get_args a in - let (hb,argsb) = Basics.get_args b in - let na = List.length argsa in - let nb = List.length argsb in - match (unfold ha, unfold hb) with - | (Symb(sa,_), Symb(sb,_)) when sa == sb && na = nb && Sign.is_inj sa -> - let fn l t1 t2 = (t1,t2) :: l in - build_sub acc (List.fold_left2 fn cs argsa argsb) - | (Vari(x) , _ ) when argsa = [] -> build_sub ((x,b)::acc) cs - | (_ , Vari(x) ) when argsb = [] -> build_sub ((x,a)::acc) cs - | (_ , _ ) -> build_sub acc cs - in - let (vs,ts) = build_sub [] cs in - (Array.of_list vs, Array.of_list ts) - -(* Does not work in examples/cic.dk - -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,[||]) -*) - -(** [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 - 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) - -(** Translation from Xml-light - (https://opam.ocaml.org/packages/xml-light/xml-light.2.4/) to Lambdapi **) - -(** [find_trs xml] finds the Xml node corresponding to the TRS in an Xml node - obtained from a CPF file. In a valid CPF file generated from external - tools for the Knuth-Bendix completion, there is exactly one such node. **) -let find_trs : Xml.xml -> Xml.xml = fun xml -> - let rec find_tag : string -> Xml.xml -> Xml.xml option = fun s xml -> - if Xml.tag xml = s then Some xml - else - let rec iter f = function - | [] -> None - | x :: xs -> match f x with - | None -> iter f xs - | y -> y in - iter (find_tag s) (Xml.children xml) +let reduce_eqs : (term * term) list -> (term * term) list = fun eqs -> + let rec reduce_aux acc eqs = + match eqs with + | [] -> acc + | (t, u) :: eqs -> + let (ht, argst) = Basics.get_args t in + let (hu, argsu) = Basics.get_args u in + let nt = List.length argst in + let nu = List.length argsu in + if Eval.eq_modulo t u then reduce_aux acc eqs + else + match (unfold ht, unfold hu) with + | Symb (st, _), Symb (su, _) when st == su && nt = nu + && Sign.is_inj st -> + let add_eqs l t1 t2 = (t1, t2) :: l in + reduce_aux acc (List.fold_left2 add_eqs eqs argst argsu) + | _ -> reduce_aux ((t, u) :: acc) eqs in - match find_tag "completionInput" xml with - | None -> assert false - | Some xml -> - match find_tag "trs" xml with - | None -> assert false - | Some xml -> xml - -(** [get_only_child xml] returns the only child of an Xml node given **) -let get_only_child : Xml.xml -> Xml.xml = fun xml -> - match Xml.children xml with - | [xml] -> xml - | _ -> assert false - -(** [get_term sign xml] translates an Xml node of tag name "var" or "funapp" - into a term according to the signature state of the original system **) -let rec get_term : Sign.t -> Xml.xml -> term = fun sign xml -> - match Xml.tag xml with - | "var" -> (* to finish *) assert false - | "funapp" -> begin match Xml.children xml with - | [] -> assert false - | f :: args -> - match get_only_child f with - | Xml.Element _ -> assert false - | Xml.PCData str -> - let args = List.map (get_arg sign) args in - let s, path = - match String.split_on_char '_' str with - | ["c"; path; s] -> - s, String.split_on_char '.' path - | _ -> assert false in - let sign = PathMap.find path Sign.(!loaded) in - let sym = - try symb (Sign.find sign s) with Not_found -> assert false in - List.fold_left (fun u v -> Appl (u, v)) sym args - end - | _ -> assert false + reduce_aux [] eqs -(** [get_arg xml] translates an Xml node of tag name "arg" into a term **) -and get_arg : Sign.t -> Xml.xml -> term = fun sign xml -> - get_term sign (get_only_child xml) - -(** [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 symbs 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 = 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 + (* We process the LHS to replace pattern variables by fresh function + symbols. *) + let lhs, rhs = to_terms_closed (s, r.elt) in (* Infer the type of the LHS and the constraints. *) 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 + | None -> wrn r.pos "Untypable LHS." + | Some (lhs_constrs, ty_lhs) -> + let lhs_constrs = reduce_eqs lhs_constrs in + if !log_enabled 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) + 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; + let ord s1 s2 = Pervasives.compare s1.sym_name s2.sym_name in + let t1 = Time.save () in + let check_fo (t, u) = Basics.check_fo t; Basics.check_fo u in + try + List.iter check_fo lhs_constrs; + let rules_to_add = Completion.completion lhs_constrs ord in + Time.restore t1; + List.iter + (fun (s, rs) -> s.sym_rules := rs @ !(s.sym_rules)) rules_to_add; + (* 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 + 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 + else Time.restore t1 + | None -> + fatal r.pos "Rule [%a] does not preserve typing." + pp_rule (s, h, r.elt) + with Not_FO -> + wrn r.pos "Rule [%a] may not preserve typing." pp_rule (s, h, r.elt) diff --git a/src/unif.ml b/src/unif.ml index 1a2ee56f1..7850aebed 100644 --- a/src/unif.ml +++ b/src/unif.ml @@ -237,7 +237,7 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> injective. Currently, it only handles a specific case: when s is the builtin P. *) let solve_inj s ts v = - if !(s.sym_rules) = [] then error () + if !(s.sym_rules) = [] then add_to_unsolved () else match Pervasives.(!config) with | None -> add_to_unsolved () @@ -277,7 +277,6 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> if !(s1.sym_rules) <> [] || List.same_length ts1 ts2 then add_to_unsolved () 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 -> From 106f893fc6cb5a17d5156569ae0244574ddc8ca8 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 19 Apr 2019 13:48:44 +0200 Subject: [PATCH 13/26] Remove a redundant function --- src/sr.ml | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/src/sr.ml b/src/sr.ml index e6d280c4f..63d7acb22 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -12,26 +12,6 @@ let log_subj = new_logger 'j' "subj" "debugging information for subject-reduction" let log_subj = log_subj.logger -let reduce_eqs : (term * term) list -> (term * term) list = fun eqs -> - let rec reduce_aux acc eqs = - match eqs with - | [] -> acc - | (t, u) :: eqs -> - let (ht, argst) = Basics.get_args t in - let (hu, argsu) = Basics.get_args u in - let nt = List.length argst in - let nu = List.length argsu in - if Eval.eq_modulo t u then reduce_aux acc eqs - else - match (unfold ht, unfold hu) with - | Symb (st, _), Symb (su, _) when st == su && nt = nu - && Sign.is_inj st -> - let add_eqs l t1 t2 = (t1, t2) :: l in - reduce_aux acc (List.fold_left2 add_eqs eqs argst argsu) - | _ -> reduce_aux ((t, u) :: acc) eqs - in - reduce_aux [] eqs - (** [check_rule symbs builtins r] check whether rule [r] is well-typed. The program fails gracefully in case of error. *) let check_rule : @@ -45,7 +25,6 @@ let check_rule : match Typing.infer_constr builtins Ctxt.empty lhs with | None -> wrn r.pos "Untypable LHS." | Some (lhs_constrs, ty_lhs) -> - let lhs_constrs = reduce_eqs lhs_constrs in if !log_enabled then begin log_subj "LHS has type [%a]" pp ty_lhs; From 4b44d53e8b2afd1e3df53c1518db34f6a6a048e3 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 19 Apr 2019 16:38:11 +0200 Subject: [PATCH 14/26] Fix some bugs and typos --- src/basics.ml | 10 +++++----- src/completion.ml | 47 ++++++++++++++++++++++++++++------------------- src/sr.ml | 2 +- 3 files changed, 34 insertions(+), 25 deletions(-) diff --git a/src/basics.ml b/src/basics.ml index a26659246..69302f63b 100644 --- a/src/basics.ml +++ b/src/basics.ml @@ -112,12 +112,12 @@ let is_symb : sym -> term -> bool = fun s t -> | Symb(r,_) -> r == s | _ -> false -(** [get_symb t] checks that [t] is of the form [Symb (s , _)] and returns - [s]. *) -let get_symb : term -> sym = fun t -> +(** [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, _) -> s - | _ -> assert false + | 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 diff --git a/src/completion.ml b/src/completion.ml index ff43a1eae..c625cd8db 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -10,32 +10,41 @@ open Timed let rec lpo : sym Ord.cmp -> term Ord.cmp = fun ord t1 t2 -> let f, args = get_args t1 in let f = get_symb f in - 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 ord f g with - | 1 -> - 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.ord_lex (lpo ord) args args' - else -1 - | _ -> -1 + match 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 + | 1 -> + 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.ord_lex (lpo ord) args args' + else -1 + | _ -> -1 (** [to_rule (lhs, rhs)] tranlates the pair [(lhs, rhs)] of closed terms into a rule. *) let to_rule : term * term -> sym * rule = fun (lhs, rhs) -> let (s, args) = get_args lhs in let s = get_symb s in - 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 = [||] } + match 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 = [||] } -(** [completion eqs ord] returns a pair of time points [(t1, t2)] where t1 - corresponds to the used-defined rewrite system and t2 to the convergent - rewrite system obtained using the completion procedure. *) +(** [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 Ord.cmp -> (sym * rule list) list = fun eqs ord -> let lpo = lpo ord in diff --git a/src/sr.ml b/src/sr.ml index 63d7acb22..a02974801 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -20,7 +20,7 @@ let check_rule : if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, r.elt); (* We process the LHS to replace pattern variables by fresh function symbols. *) - let lhs, rhs = to_terms_closed (s, r.elt) in + let lhs, rhs = to_closed_terms (s, r.elt) in (* Infer the type of the LHS and the constraints. *) match Typing.infer_constr builtins Ctxt.empty lhs with | None -> wrn r.pos "Untypable LHS." From 3a22261f2bd745c9c535090fc05c5e17d2e1c4d6 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Tue, 23 Apr 2019 14:27:15 +0200 Subject: [PATCH 15/26] Modify the main function for checking SR --- src/basics.ml | 29 +++++++------ src/sr.ml | 117 +++++++++++++++++++++++++++++++++++++++----------- 2 files changed, 107 insertions(+), 39 deletions(-) diff --git a/src/basics.ml b/src/basics.ml index 69302f63b..3945e4b27 100644 --- a/src/basics.ml +++ b/src/basics.ml @@ -253,18 +253,20 @@ let rec to_m : int -> (meta option) array -> term -> tbox = fun k metas t -> let l = Array.length a in match i with | None -> - let m = fresh_meta ~name:n Kind l in + 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 Kind l in + let m = fresh_meta ~name:n (build_meta_type (l + k)) l in metas.(i) <- Some m; _Meta m a end | _ -> assert false +exception Not_FO + (** [to_closed 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 @@ -272,31 +274,32 @@ let rec to_m : int -> (meta option) array -> term -> tbox = fun k metas t -> let rec to_closed : (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) -> + | Vari x -> _Vari x + | Symb (s, h) -> _Symb s h + | Abst (a, t) -> let (x, t) = Bindlib.unbind t in _Abst (to_closed symbs a) (Bindlib.bind_var x (to_closed symbs t)) - | Appl (t, u) -> _Appl (to_closed symbs t) (to_closed symbs u) - | Patt (i, n, _) -> + | Appl (t, u) -> _Appl (to_closed symbs t) (to_closed symbs u) + | Patt (i, n, [||]) -> begin match i with | None -> - let t_n = new_symb ("t_" ^ n) Kind in + let t_n = new_symb ("{t_" ^ n) Kind in let term_t_n = symb t_n in - let c_n = new_symb ("c_" ^ n) term_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) Kind in + let t_n = new_symb ("{t_" ^ n) Kind in let term_t_n = symb t_n in - let c_n = new_symb ("c_" ^ n) term_t_n in + let c_n = new_symb ("{c_" ^ n) term_t_n in symbs.(i) <- Some c_n; _Symb c_n Nothing end - | _ -> assert false + | Patt _ -> raise Not_FO + | _ -> assert false (** [distinct_vars_opt ts] checks that [ts] is made of distinct variables and returns these variables. *) @@ -374,8 +377,6 @@ let to_closed_terms : sym * rule -> term * term = fun (s, r) -> let rhs = Bindlib.msubst r.rhs terms_env in (lhs, rhs) -exception Not_FO - (** [check_fo t] checks that [t] is a first-order term. *) let rec check_fo : term -> unit = fun t -> match t with diff --git a/src/sr.ml b/src/sr.ml index a02974801..b390792c3 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -6,35 +6,71 @@ open Print open Extra open Terms open Basics +open Pos (** Logging function for typing. *) let log_subj = new_logger 'j' "subj" "debugging information for subject-reduction" let log_subj = log_subj.logger +(** Representation of a substitution. *) +type subst = tvar array * term array + +(** [subst_from_constrs cs] builds a //typing substitution// from the list of + constraints [cs]. The returned substitution is given by a couple of arrays + [(xs,ts)] of the same length. The array [xs] contains the variables to be + substituted using the terms of [ts] at the same index. *) +let subst_from_constrs : (term * term) list -> subst = fun cs -> + let rec build_sub acc cs = + match cs with + | [] -> List.split acc + | (a,b)::cs -> + let (ha,argsa) = Basics.get_args a in + let (hb,argsb) = Basics.get_args b in + let na = List.length argsa in + let nb = List.length argsb in + match (unfold ha, unfold hb) with + | (Symb(sa,_), Symb(sb,_)) when sa == sb && na = nb && Sign.is_inj sa -> + let fn l t1 t2 = (t1,t2) :: l in + build_sub acc (List.fold_left2 fn cs argsa argsb) + | (Vari(x) , _ ) when argsa = [] -> build_sub ((x,b)::acc) cs + | (_ , Vari(x) ) when argsb = [] -> build_sub ((x,a)::acc) cs + | (_ , _ ) -> build_sub acc cs + in + let (vs,ts) = build_sub [] cs in + (Array.of_list vs, Array.of_list ts) + +let unsolved_msg (t, u) = fatal_msg "Cannot solve [%a] ~ [%a]\n" pp t pp u + +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] does not preserve typing." pp_rule (s, h, r.elt) + (** [check_rule symbs 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 = fun builtins (s,h,r) -> - if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, r.elt); + try + if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, r.elt); (* We process the LHS to replace pattern variables by fresh function symbols. *) - let lhs, rhs = to_closed_terms (s, r.elt) in + let lhs, rhs = to_closed_terms (s, r.elt) in (* Infer the type of the LHS and the constraints. *) - 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; - let ord s1 s2 = Pervasives.compare s1.sym_name s2.sym_name in - let t1 = Time.save () in - let check_fo (t, u) = Basics.check_fo t; Basics.check_fo u in - try + 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; + let ord s1 s2 = Pervasives.compare s1.sym_name s2.sym_name in + let t1 = Time.save () in + let check_fo (t, u) = Basics.check_fo t; Basics.check_fo u in List.iter check_fo lhs_constrs; let rules_to_add = Completion.completion lhs_constrs ord in Time.restore t1; @@ -44,17 +80,48 @@ let check_rule : 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 raise Not_FO + else Time.restore t1 + | None -> sr_not_preserved_msg (s, h, r) + with Not_FO -> + let lhs, rhs = to_terms (s, r.elt) in + begin 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; + 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 + 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; + let problems = Unif.{no_problems with to_solve} in + begin match Unif.(solve builtins false problems) 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) + List.iter unsolved_msg cs; + sr_unproved_msg (s, h, r) end - else Time.restore t1 | None -> - fatal r.pos "Rule [%a] does not preserve typing." - pp_rule (s, h, r.elt) - with Not_FO -> - wrn r.pos "Rule [%a] may not preserve typing." pp_rule (s, h, r.elt) + sr_not_preserved_msg (s, h, r) + end + end From f425f279de2a381fe4c76e87e03b1620192642c6 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 3 May 2019 13:45:35 +0200 Subject: [PATCH 16/26] Modify the order on symbols used in the completion procedure --- src/completion.ml | 120 ++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 117 insertions(+), 3 deletions(-) diff --git a/src/completion.ml b/src/completion.ml index c625cd8db..a100b1cf1 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -21,14 +21,14 @@ let rec lpo : sym Ord.cmp -> term Ord.cmp = fun ord t1 t2 -> | None -> 1 | Some g -> match ord f g with - | 1 -> + | k when k > 0 -> if List.for_all (fun x -> lpo ord t1 x > 0) args' then 1 else -1 - | 0 -> + | 0 -> if List.for_all (fun x -> lpo ord t1 x > 0) args' then Ord.ord_lex (lpo ord) args args' else -1 - | _ -> -1 + | _ -> -1 (** [to_rule (lhs, rhs)] tranlates the pair [(lhs, rhs)] of closed terms into a rule. *) @@ -42,6 +42,120 @@ let to_rule : term * term -> sym * rule = fun (lhs, rhs) -> 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) + +module StrMap = Map.Make(struct + type t = string + let compare = compare +end) + +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, then 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 Ord.cmp = fun eqs -> + let symbs, deps = find_deps eqs in + try + let ord = topo_sort symbs deps 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 + with Not_DAG -> + fun s1 s2 -> 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]. *) From 550ad3ea86d13cf6a8747baf048e805eab13debe Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 3 May 2019 13:58:10 +0200 Subject: [PATCH 17/26] Combine the two algorithms for checking SR --- src/basics.ml | 4 +++ src/sr.ml | 96 ++++++++++++++++++++++++++++++++------------------- 2 files changed, 65 insertions(+), 35 deletions(-) diff --git a/src/basics.ml b/src/basics.ml index 3945e4b27..0e21e67a8 100644 --- a/src/basics.ml +++ b/src/basics.ml @@ -301,6 +301,10 @@ let rec to_closed : (sym option) array -> term -> tbox | Patt _ -> raise Not_FO | _ -> 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 = diff --git a/src/sr.ml b/src/sr.ml index b390792c3..2c9f82488 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -40,6 +40,12 @@ 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) +(** 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 unsolved_msg (t, u) = fatal_msg "Cannot solve [%a] ~ [%a]\n" pp t pp u let sr_unproved_msg (s, h, r) = @@ -48,79 +54,99 @@ let sr_unproved_msg (s, h, r) = let sr_not_preserved_msg (s, h, r) = fatal r.pos "Rule [%a] does not preserve typing." pp_rule (s, h, r.elt) -(** [check_rule symbs builtins r] check whether rule [r] is well-typed. The +(** [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 + List.exists (eq_comm eq) eqs + +(** [check_rule symbs builtins 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) -> + let t1 = Time.save () in try if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, r.elt); - (* We process the LHS to replace pattern variables by fresh function - symbols. *) + (* We process the LHS to replace pattern variables by fresh function + symbols. *) let lhs, rhs = to_closed_terms (s, r.elt) in - (* Infer the type of the LHS and the constraints. *) + (* Infer the type of the LHS and the constraints. *) 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; - let ord s1 s2 = Pervasives.compare s1.sym_name s2.sym_name in - let t1 = Time.save () in - let check_fo (t, u) = Basics.check_fo t; Basics.check_fo u in - List.iter check_fo lhs_constrs; - let rules_to_add = Completion.completion lhs_constrs ord in + if !log_enabled then typ_cond "LHS" ty_lhs lhs_constrs; + (* We distinguish three types of equations: first-order equations, + symbol-higher-order equations (of the form s = t where s is a + new symbol and t is a higher-order term), and other equations. *) + let split_constrs (fo, r_sym_ho, others) (t, u) = + try + Basics.check_fo t; + Basics.check_fo u; + (t, u) :: fo, r_sym_ho, others + with Not_FO -> + match (t, u) with + | Symb (s, _), _ when is_new_symb s -> + let r = Completion.to_rule (t, u) in + fo, r :: r_sym_ho, others + | _, Symb (s, _) when is_new_symb s -> + let r = Completion.to_rule (u, t) in + fo, r :: r_sym_ho, others + | _ -> + fo, r_sym_ho, (t, u) :: others in + let constrs_fo, r_sym_ho, others = + List.fold_left split_constrs ([], [], []) lhs_constrs in + let ord = Completion.ord_from_eqs constrs_fo in + let rules_to_add = Completion.completion constrs_fo ord in Time.restore t1; + (* Add the rules obtained by the completion procedure *) List.iter (fun (s, rs) -> s.sym_rules := rs @ !(s.sym_rules)) rules_to_add; + (* Add the rules generated by symbol-higher-order equations *) + List.iter + (fun (s, r) -> s.sym_rules := r :: !(s.sym_rules)) r_sym_ho; (* 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 raise Not_FO + if cs <> [] then + let cs = List.filter (fun c -> not (check_eq c others)) cs in + if cs <> [] then + begin + List.iter unsolved_msg cs; + sr_unproved_msg (s, h, r) + end + else Time.restore t1 else Time.restore t1 | None -> sr_not_preserved_msg (s, h, r) with Not_FO -> + Time.restore t1; let lhs, rhs = to_terms (s, r.elt) in begin 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; + if !log_enabled then typ_cond "LHS" ty_lhs lhs_constrs; 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 - 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; + typ_cond "RHS" ty_lhs to_solve; let problems = Unif.{no_problems with to_solve} in begin match Unif.(solve builtins false problems) 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 + 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 t1 | None -> sr_not_preserved_msg (s, h, r) end From 11e842834a2d3cc04e63dfc2e985de3157dbedf4 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Wed, 5 Jun 2019 19:32:41 +0200 Subject: [PATCH 18/26] Rename some functions --- src/basics.ml | 196 +++++++++++++++++++++++++++++++++------------- src/completion.ml | 63 +++++++-------- src/sr.ml | 32 +++++--- 3 files changed, 189 insertions(+), 102 deletions(-) diff --git a/src/basics.ml b/src/basics.ml index 0e21e67a8..d4ac74b75 100644 --- a/src/basics.ml +++ b/src/basics.ml @@ -190,6 +190,76 @@ 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 + +let rec map_meta : (meta -> meta) -> 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) -> Meta (f m, Array.map (map_meta f) ts) + | _ -> t + +module IntMap = Map.Make(struct type t = int let compare = compare end) + +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 + lhs, map_meta (fun m -> IntMap.find m.meta_key metamap) 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 -> @@ -203,15 +273,25 @@ let get_metas : term -> meta list = fun t -> iter_meta (fun m -> l := m :: !l) t; List.sort_uniq (fun m1 m2 -> m1.meta_key - m2.meta_key) !l +let get_metas' : term -> meta list = fun t -> + let open Pervasives in + let l = ref [] in + let fn t = match t with + | Meta (m, _) -> l := m :: !l + | _ -> () in + iter fn t; + List.sort_uniq (fun m1 m2 -> m1.meta_key - m2.meta_key) !l + (** [has_metas t] checks that there are metavariables in [t]. *) let has_metas : term -> bool = let exception Found in fun t -> try iter_meta (fun _ -> raise Found) t; false with Found -> true -(** [build_meta_type k] builds the type “∀(x₁:A₁) (x₂:A₂) ⋯ (xk:Ak), B” where +(** [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 metavar of arity “i-1” and type “∀(x₁:A₂) ⋯ (x(i-1):A(i-1), TYPE”. *) -let build_meta_type : int -> term = fun k -> + 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 = @@ -236,55 +316,62 @@ 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 } -(** [to_m 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 to_m : int -> (meta option) array -> term -> tbox = fun k metas t -> +(** [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 (to_m 0 metas a) (Bindlib.bind_var x (to_m 0 metas t)) - | Appl (t, u) -> _Appl (to_m (k + 1) metas t) (to_m 0 metas u) + _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 (to_m 0 metas) a in + 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_meta_type (l + k)) l in + 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_meta_type (l + k)) l in + let m = fresh_meta ~name:n (build_prod (l + k)) l in metas.(i) <- Some m; _Meta m a end | _ -> assert false -exception Not_FO +(** Exception raised when a term contains non-nullary metavariables. *) +exception Non_nullary_meta -(** [to_closed 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 to_closed : (sym option) array -> term -> tbox +(** [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 (to_closed symbs a) (Bindlib.bind_var x (to_closed symbs t)) - | Appl (t, u) -> _Appl (to_closed symbs t) (to_closed symbs u) + _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) Kind in + 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 @@ -292,13 +379,13 @@ let rec to_closed : (sym option) array -> term -> tbox match symbs.(i) with | Some s -> _Symb s Nothing | None -> - let t_n = new_symb ("{t_" ^ n) Kind in + 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 Not_FO + | Patt _ -> raise Non_nullary_meta | _ -> assert false (** [is_new_symb s] checks if [s] is a function symbol created for checking @@ -344,51 +431,48 @@ let term_of_rhs : rule -> term = fun r -> in Bindlib.msubst r.rhs (Array.mapi fn r.vars) -(** [to_terms r] translates the rule [r] into a pair of terms. The pattern - variables in the LHS are replaced by metavariables and the terms with - environment in the RHS are replaced by their corresponding metavariables. - *) -let to_terms : sym * rule -> term * term = fun (s, r) -> +(** [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 metas = Array.init arity (fun _ -> None) in - let lhs = List.map (fun p -> Bindlib.unbox (to_m 0 metas p)) r.lhs in - let lhs = add_args (symb s) lhs in - (* [to_term_env m] computes the term with environment corresponding to the - metavariable [m]. *) - let to_term_env : meta option -> term_env = fun m -> + 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 + +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 - let terms_env = Array.map to_term_env metas in - let rhs = Bindlib.msubst r.rhs terms_env in - (lhs, rhs) + replace_patt_rule (replace_patt_by_meta 0) to_term_env -(** [to_closed_terms r] translates the rule [r] into a pair of terms. The - pattern variables in the LHS are replaced by fresh symbols as in the - function [to_closed] and the terms with environment in the RHS are - replaced by their corresponding symbols. *) -let to_closed_terms : sym * rule -> term * term = fun (s, r) -> - let arity = Bindlib.mbinder_arity r.rhs in - let symbs = Array.init arity (fun _ -> None) in - let lhs = List.map (fun p -> Bindlib.unbox (to_closed symbs p)) r.lhs in - let lhs = add_args (symb s) lhs in - let to_term_env : sym option -> term_env = fun s -> +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 - let terms_env = Array.map to_term_env symbs in - let rhs = Bindlib.msubst r.rhs terms_env in - (lhs, rhs) + replace_patt_rule replace_patt_by_symb to_term_env -(** [check_fo t] checks that [t] is a first-order term. *) -let rec check_fo : term -> unit = fun t -> +(** [check_nullary_meta t] checks that all the metavariables in [t] are of + arity 0. *) +let rec check_nullary_meta : term -> unit = fun t -> match t with | Type | Kind | Symb _ | Wild - | Patt _ -> () - | Meta (_, ar) when ar = [||] -> () - | Appl (u, v) -> check_fo u; check_fo v - | _ -> raise Not_FO + | 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 index a100b1cf1..6aa24247f 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -9,8 +9,7 @@ open Timed the strict total order [ord] on the set of all function symbols. *) let rec lpo : sym Ord.cmp -> term Ord.cmp = fun ord t1 t2 -> let f, args = get_args t1 in - let f = get_symb f in - match f with + 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 @@ -30,12 +29,11 @@ let rec lpo : sym Ord.cmp -> term Ord.cmp = fun ord t1 t2 -> else -1 | _ -> -1 -(** [to_rule (lhs, rhs)] tranlates the pair [(lhs, rhs)] of closed terms into - a rule. *) -let to_rule : term * term -> sym * rule = fun (lhs, rhs) -> +(** [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 - let s = get_symb s in - match s with + match get_symb s with | None -> assert false | Some s -> let vs = Bindlib.new_mvar te_mkfree [||] in @@ -74,11 +72,8 @@ let find_deps : (term * term) list -> string list * (string * string) list (fun (t1, t2) -> find_dep_aux (t1, t2); find_dep_aux (t2, t1)) eqs; (!symbs, !deps) -module StrMap = Map.Make(struct - type t = string - let compare = compare -end) - +(** 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 @@ -134,27 +129,25 @@ let topo_sort : string list -> (string * string) list -> int StrMap.t 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, then if the topological order is well - defined then we compare their positions in this latter one. Otherwise, + 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 Ord.cmp = fun eqs -> let symbs, deps = find_deps eqs in - try - let ord = topo_sort symbs deps 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 - with Not_DAG -> - fun s1 s2 -> Pervasives.compare s1.sym_name s2.sym_name + 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 @@ -179,8 +172,8 @@ let completion : (term * term) list -> sym Ord.cmp -> (sym * rule list) list let orient (t1, t2) = match lpo t1 t2 with | 0 -> () - | k when k > 0 -> add_rule (to_rule (t1, t2)) - | _ -> add_rule (to_rule (t2, t1)) in + | 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 @@ -199,7 +192,7 @@ let completion : (term * term) list -> sym Ord.cmp -> (sym * rule list) list other than [r]. *) let f acc rs' r = s.sym_rules := acc @ rs'; - let (lhs, rhs) = to_terms (s, r) in + 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); @@ -208,10 +201,10 @@ let completion : (term * term) list -> sym Ord.cmp -> (sym * rule list) list match lpo lhs' rhs' with | 0 -> () | k when k > 0 -> - to_add := to_rule (lhs', rhs') :: !to_add; + to_add := make_rule (lhs', rhs') :: !to_add; b := true; | _ -> - to_add := to_rule (rhs', lhs') :: !to_add; + to_add := make_rule (rhs', lhs') :: !to_add; b := true; end in diff --git a/src/sr.ml b/src/sr.ml index 2c9f82488..31ce64243 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -2,9 +2,9 @@ open Timed open Console +open Terms open Print open Extra -open Terms open Basics open Pos @@ -52,7 +52,7 @@ 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] does not preserve typing." pp_rule (s, h, r.elt) + 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) @@ -64,7 +64,7 @@ let check_eq eq eqs = in List.exists (eq_comm eq) eqs -(** [check_rule symbs builtins r] checks whether rule [r] is well-typed. The +(** [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 @@ -74,7 +74,7 @@ let check_rule : if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, r.elt); (* We process the LHS to replace pattern variables by fresh function symbols. *) - let lhs, rhs = to_closed_terms (s, r.elt) in + let lhs, rhs = replace_patt_by_symb_rule (s, r.elt) in (* Infer the type of the LHS and the constraints. *) match Typing.infer_constr builtins Ctxt.empty lhs with | None -> wrn r.pos "Untypable LHS." @@ -85,16 +85,16 @@ let check_rule : new symbol and t is a higher-order term), and other equations. *) let split_constrs (fo, r_sym_ho, others) (t, u) = try - Basics.check_fo t; - Basics.check_fo u; + check_nullary_meta t; + check_nullary_meta u; (t, u) :: fo, r_sym_ho, others - with Not_FO -> + with Non_nullary_meta -> match (t, u) with | Symb (s, _), _ when is_new_symb s -> - let r = Completion.to_rule (t, u) in + let r = Completion.make_rule (t, u) in fo, r :: r_sym_ho, others | _, Symb (s, _) when is_new_symb s -> - let r = Completion.to_rule (u, t) in + let r = Completion.make_rule (u, t) in fo, r :: r_sym_ho, others | _ -> fo, r_sym_ho, (t, u) :: others in @@ -117,15 +117,25 @@ let check_rule : let cs = List.filter (fun c -> not (check_eq c others)) cs in if cs <> [] then begin + let detect_inj acc (t, u) = + let ht, _ = get_args t in + let hu, _ = get_args u in + match (get_symb ht, get_symb hu) with + | Some s, Some s' when s == s' -> + if List.mem s.sym_name acc then acc + else s.sym_name :: acc + | _ -> acc in + let ss = List.fold_left detect_inj [] cs in + List.iter (wrn None "Check if [%s] is injective") ss; List.iter unsolved_msg cs; sr_unproved_msg (s, h, r) end else Time.restore t1 else Time.restore t1 | None -> sr_not_preserved_msg (s, h, r) - with Not_FO -> + with Non_nullary_meta -> Time.restore t1; - let lhs, rhs = to_terms (s, r.elt) in + let lhs, rhs = replace_patt_by_meta_rule (s, r.elt) in begin match Typing.infer_constr builtins Ctxt.empty lhs with | None -> wrn r.pos "Untypable LHS" | Some (lhs_constrs, ty_lhs) -> From 6c69f328ef280a710c0aaa62a3a3b4165bfe255f Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Wed, 5 Jun 2019 19:34:24 +0200 Subject: [PATCH 19/26] Add an function for checking injectivity of symbols --- src/handle.ml | 10 +- src/terms.ml | 4 +- src/unif.ml | 247 +++++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 242 insertions(+), 19 deletions(-) diff --git a/src/handle.ml b/src/handle.ml index 6a92418d4..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. *) @@ -125,7 +127,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = let (s,_,_) as r = scope_rule ss r in if !(s.sym_def) <> None then fatal_no_pos "Symbol [%s] cannot be (re)defined." s.sym_name; - r + Sr.check_rule ss.builtins r; r in let rs = List.map handle_rule rs in (* Adding the rules all at once. *) @@ -133,8 +135,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = out 3 "(rule) %a\n" Print.pp_rule (s,h,r.elt); Sign.add_rule ss.signature s r.elt in - List.iter add_rule rs; - List.iter (Sr.check_rule ss.builtins) rs; (ss, None) + List.iter add_rule rs; (ss, None) | P_definition(op,x,xs,ao,t) -> (* We check that [x] is not already used. *) if Sign.mem ss.signature x.elt then @@ -209,7 +210,6 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = wrn cmd.pos "Proof aborted."; ss | P_proof_admit -> (* If the proof is finished, display a warning. *) - if Proof.finished st then wrn cmd.pos "The proof is finished. You can use 'qed' instead."; (* Add a symbol corresponding to the proof, with a warning. *) 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 7850aebed..dc40baa90 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" @@ -98,6 +99,7 @@ let rec solve : problems -> unif_constrs = fun p -> (** [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 -> + if Eval.eq_modulo t1 t2 then solve p else let (h1, ts1) = Eval.whnf_stk t1 [] in let (h2, ts2) = Eval.whnf_stk t2 [] in if !log_enabled then @@ -120,14 +122,18 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> 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} 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), @@ -269,14 +275,17 @@ 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 + if check_inj_sym bls s1 then decompose_part bls () + else add_to_unsolved () + else error () else add_to_unsolved () | (Meta(m,ts) , _ ) when ts1 = [] && instantiate m ts t2 -> @@ -298,6 +307,220 @@ 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. *) + +(** [unif constrs t1 t2] attempts to unify [t1] and [t2], and adds the + constraints obtained into [constrs]. *) +and unif : unif_constrs ref -> term -> term -> unit = fun constrs t1 t2 -> + let to_solve = [(t1, t2)] in + let problems = { no_problems with to_solve } in + constrs := (solve problems) @ (!constrs) + +(** [check_incl bls blss] checks if there exists [bls'] in [blss] such that + 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 check_incl : bool list -> bool list list -> bool = fun bls blss -> + let check_incl_aux bls' = + List.for_all2 (fun b b' -> b || not b') bls bls' in + List.exists check_incl_aux blss + +(** [hypo_inj bls s] adds the hypothesis that [s] is I-injective where I is + represented by [bls]. *) +and hypo_inj : bool list -> sym -> unit = fun bls s -> + match s.sym_mode with + | Const -> () + | Defin -> s.sym_mode <- Injec [bls] + | Injec l -> s.sym_mode <- Injec (bls :: l) + +(** [remove_hypo_inj s] removes the last hypothesis on [s]. *) +and remove_hypo_inj : sym -> unit = fun s -> + match s.sym_mode with + | Const + | Defin -> () + | Injec l -> s.sym_mode <- Injec (List.tl l) + +(** [eq_modulo_constrs constrs (t1, t2)] returns if 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 + List.exists fn constrs + +(** [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 + hypo_inj bls s; + let _, args1 = get_args lhs1 in + let _, args2 = get_args lhs2 in + let args = List.combine args1 args2 in + let constrs = ref [] in + List.iter2 + (fun b (arg1, arg2) -> if b then unif constrs arg1 arg2) bls args; + unif constrs rhs1 rhs2; + let to_solve = + List.map + snd (List.filter (fun (b, _) -> not b) (List.combine bls args)) in + begin try + let cs = solve {no_problems with to_solve} in + let res = + List.for_all (eq_modulo_constrs !constrs) cs in + Time.restore t; + remove_hypo_inj s; + res + with Fatal _ -> Time.restore t; remove_hypo_inj s; false end + with + | Fatal _ -> Time.restore t; remove_hypo_inj s; true + | _ -> Time.restore t; remove_hypo_inj s; false + +(** [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 + try match h1 with + | Meta (m, _) -> + let _, args2 = get_args lhs in + let fn = function + | Meta (m', _) -> m == m' + | _ -> false in + List.exists2 (fun b arg -> b && fn arg) bls args2 + | Symb (s', _) when !(s'.sym_rules) = [] -> true + | Symb (s', _) when s == s' -> + let _, args2 = get_args lhs in + let new_args = new_args (List.length args2) in + let constrs = ref [] in + List.iter2 (unif constrs) args1 new_args; + let argss = List.combine args2 new_args in + List.iter2 + (fun b (arg1, arg2) -> if b then unif constrs arg1 arg2) bls argss; + let to_solve = + List.map + snd (List.filter (fun (b, _) -> not b) (List.combine bls argss)) + in + begin try + let cs = solve {no_problems with to_solve} in + let res = + List.for_all (eq_modulo_constrs !constrs) cs in + Time.restore t; + res + with Fatal _ -> Time.restore t; false end + | _ -> 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]. *) +and check_inj_sym : bool list -> sym -> bool = fun bls s -> + match s.sym_mode with + | Injec l when check_incl 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 + let res = + List.for_all (check_single_rule bls s) terms_of_rules && + check_inj_rules terms_of_rules in + res + (** [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 From abe4a3cca4738c8e44de2c13119845c6b867e75b Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Tue, 11 Jun 2019 18:12:35 +0200 Subject: [PATCH 20/26] Add some comments and make some modifications --- src/basics.ml | 36 +++++++++++++++++++++++------------- src/unif.ml | 4 ++-- 2 files changed, 25 insertions(+), 15 deletions(-) diff --git a/src/basics.ml b/src/basics.ml index d4ac74b75..9f1a6baf5 100644 --- a/src/basics.ml +++ b/src/basics.ml @@ -196,7 +196,10 @@ let is_meta : term -> bool = fun t -> | Meta _ -> true | _ -> false -let rec map_meta : (meta -> meta) -> term -> term = fun f t -> +(** [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 @@ -209,11 +212,13 @@ let rec map_meta : (meta -> meta) -> term -> term = fun f t -> 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) -> Meta (f m, Array.map (map_meta f) ts) + | 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 = @@ -258,7 +263,12 @@ let copy_rule : term * term -> term * term = fun (lhs, rhs) -> | _ -> t, metamap in let lhs, metamap = copy_term metamap lhs in - lhs, map_meta (fun m -> IntMap.find m.meta_key metamap) rhs + 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 = @@ -273,15 +283,6 @@ let get_metas : term -> meta list = fun t -> iter_meta (fun m -> l := m :: !l) t; List.sort_uniq (fun m1 m2 -> m1.meta_key - m2.meta_key) !l -let get_metas' : term -> meta list = fun t -> - let open Pervasives in - let l = ref [] in - let fn t = match t with - | Meta (m, _) -> l := m :: !l - | _ -> () in - iter fn t; - List.sort_uniq (fun m1 m2 -> m1.meta_key - m2.meta_key) !l - (** [has_metas t] checks that there are metavariables in [t]. *) let has_metas : term -> bool = let exception Found in fun t -> @@ -449,6 +450,10 @@ let replace_patt_rule : 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 @@ -458,6 +463,10 @@ let replace_patt_by_meta_rule = 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 @@ -465,7 +474,8 @@ let replace_patt_by_symb_rule = 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. *) + 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 diff --git a/src/unif.ml b/src/unif.ml index dc40baa90..45f391007 100644 --- a/src/unif.ml +++ b/src/unif.ml @@ -243,7 +243,7 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> injective. Currently, it only handles a specific case: when s is the builtin P. *) let solve_inj s ts v = - if !(s.sym_rules) = [] then add_to_unsolved () + if !(s.sym_rules) = [] then error () else match Pervasives.(!config) with | None -> add_to_unsolved () @@ -256,7 +256,6 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> 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 ) @@ -286,6 +285,7 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> if check_inj_sym bls s1 then decompose_part bls () else add_to_unsolved () 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 -> From 1c2a2e4eb43168d6fac94f48fbece228203e445a Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Tue, 11 Jun 2019 18:14:10 +0200 Subject: [PATCH 21/26] Modify the main funciton of SR-checking --- src/sr.ml | 93 ++++++++++++++++++++----------------------------------- 1 file changed, 34 insertions(+), 59 deletions(-) diff --git a/src/sr.ml b/src/sr.ml index 31ce64243..f06af2bff 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -69,77 +69,54 @@ let check_eq eq eqs = let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit = fun builtins (s,h,r) -> - let t1 = Time.save () in - try - if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, r.elt); - (* We process the LHS to replace pattern variables by fresh function - symbols. *) - let lhs, rhs = replace_patt_by_symb_rule (s, r.elt) in - (* Infer the type of the LHS and the constraints. *) - match Typing.infer_constr builtins Ctxt.empty lhs with - | None -> wrn r.pos "Untypable LHS." - | Some (lhs_constrs, ty_lhs) -> - if !log_enabled then typ_cond "LHS" ty_lhs lhs_constrs; - (* We distinguish three types of equations: first-order equations, - symbol-higher-order equations (of the form s = t where s is a - new symbol and t is a higher-order term), and other equations. *) - let split_constrs (fo, r_sym_ho, others) (t, u) = + 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) -> + let t0 = Time.save () in + if !log_enabled then typ_cond "LHS" ty_lhs lhs_constrs; + try + 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 split_constrs (fo, others) (t, u) = try check_nullary_meta t; check_nullary_meta u; - (t, u) :: fo, r_sym_ho, others + (t, u) :: fo, others with Non_nullary_meta -> - match (t, u) with - | Symb (s, _), _ when is_new_symb s -> - let r = Completion.make_rule (t, u) in - fo, r :: r_sym_ho, others - | _, Symb (s, _) when is_new_symb s -> - let r = Completion.make_rule (u, t) in - fo, r :: r_sym_ho, others - | _ -> - fo, r_sym_ho, (t, u) :: others in - let constrs_fo, r_sym_ho, others = - List.fold_left split_constrs ([], [], []) lhs_constrs in + fo, (t, u) :: others in + iter_meta fn lhs; + let constrs_fo, others = + List.fold_left split_constrs ([], []) lhs_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; (* Add the rules obtained by the completion procedure *) + Time.restore t1; List.iter (fun (s, rs) -> s.sym_rules := rs @ !(s.sym_rules)) rules_to_add; - (* Add the rules generated by symbol-higher-order equations *) - List.iter - (fun (s, r) -> s.sym_rules := r :: !(s.sym_rules)) r_sym_ho; (* 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 others)) cs in - if cs <> [] then - begin - let detect_inj acc (t, u) = - let ht, _ = get_args t in - let hu, _ = get_args u in - match (get_symb ht, get_symb hu) with - | Some s, Some s' when s == s' -> - if List.mem s.sym_name acc then acc - else s.sym_name :: acc - | _ -> acc in - let ss = List.fold_left detect_inj [] cs in - List.iter (wrn None "Check if [%s] is injective") ss; - List.iter unsolved_msg cs; - sr_unproved_msg (s, h, r) - end - else Time.restore t1 - else Time.restore t1 + 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 t1; - let lhs, rhs = replace_patt_by_meta_rule (s, r.elt) in - begin match Typing.infer_constr builtins Ctxt.empty lhs with - | None -> wrn r.pos "Untypable LHS" - | Some (lhs_constrs, ty_lhs) -> - if !log_enabled then typ_cond "LHS" ty_lhs lhs_constrs; + 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 @@ -148,7 +125,7 @@ let check_rule : if !log_enabled && to_solve <> [] then typ_cond "RHS" ty_lhs to_solve; let problems = Unif.{no_problems with to_solve} in - begin match Unif.(solve builtins false problems) with + 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 @@ -156,8 +133,6 @@ let check_rule : List.iter unsolved_msg cs; sr_unproved_msg (s, h, r) end - else Time.restore t1 + else Time.restore t0 | None -> sr_not_preserved_msg (s, h, r) - end - end From 47d1ffd87187b1ab9094a28250a1941adb807898 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Wed, 12 Jun 2019 16:56:07 +0200 Subject: [PATCH 22/26] Fix some bugs in the function for injectivity checking --- src/sr.ml | 32 ++------------------------ src/unif.ml | 65 ++++++++++++++++++++++++++++++++++++++--------------- 2 files changed, 49 insertions(+), 48 deletions(-) diff --git a/src/sr.ml b/src/sr.ml index f06af2bff..0e31366de 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -76,41 +76,13 @@ let check_rule : let t0 = Time.save () in if !log_enabled then typ_cond "LHS" ty_lhs lhs_constrs; try - 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 split_constrs (fo, others) (t, u) = - try - check_nullary_meta t; - check_nullary_meta u; - (t, u) :: fo, others - with Non_nullary_meta -> - fo, (t, u) :: others in - iter_meta fn lhs; - let constrs_fo, others = - List.fold_left split_constrs ([], []) lhs_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 - (* Add the rules obtained by the completion procedure *) - Time.restore t1; - List.iter - (fun (s, rs) -> s.sym_rules := rs @ !(s.sym_rules)) rules_to_add; + let constrs = Unif.add_rules_from_constrs lhs_constrs in (* 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 others)) cs in + let cs = List.filter (fun c -> not (check_eq c constrs)) cs in if cs <> [] then raise Non_nullary_meta else Time.restore t0 else Time.restore t0 diff --git a/src/unif.ml b/src/unif.ml index 45f391007..452a8e96c 100644 --- a/src/unif.ml +++ b/src/unif.ml @@ -419,14 +419,46 @@ and remove_hypo_inj : sym -> unit = fun s -> | Defin -> () | Injec l -> s.sym_mode <- Injec (List.tl l) -(** [eq_modulo_constrs constrs (t1, t2)] returns if there exists (t1', t2') - in [constrs] such that t1 ~ t1' (resp. t2') and t2 ~ t2' (resp. t1'). *) +(** [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 - List.exists fn constrs + 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 returns the rest of it. *) +and add_rules_from_constrs : unif_constrs -> unif_constrs = 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 split_constrs (fo, others) (t, u) = + try + check_nullary_meta t; + check_nullary_meta u; + iter_meta fn t; + iter_meta fn u; + (t, u) :: fo, others + with Non_nullary_meta -> fo, (t, u) :: others in + let constrs_fo, others = List.fold_left split_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; + others (** [check_pair_of_rules bls (lhs1, rhs1) (lhs2, rhs2)] checks if the rules [lhs1 -> rhs1] and [lhs2 -> rhs2] satisfy the conditions @@ -447,14 +479,12 @@ and check_pair_of_rules : let to_solve = List.map snd (List.filter (fun (b, _) -> not b) (List.combine bls args)) in - begin try - let cs = solve {no_problems with to_solve} in - let res = - List.for_all (eq_modulo_constrs !constrs) cs in - Time.restore t; - remove_hypo_inj s; - res - with Fatal _ -> Time.restore t; remove_hypo_inj s; false end + let constrs = add_rules_from_constrs !constrs in + let res = + List.for_all (eq_modulo_constrs constrs) to_solve in + Time.restore t; + remove_hypo_inj s; + res with | Fatal _ -> Time.restore t; remove_hypo_inj s; true | _ -> Time.restore t; remove_hypo_inj s; false @@ -487,13 +517,12 @@ and check_single_rule : bool list -> sym -> term * term -> bool List.map snd (List.filter (fun (b, _) -> not b) (List.combine bls argss)) in - begin try - let cs = solve {no_problems with to_solve} in - let res = - List.for_all (eq_modulo_constrs !constrs) cs in - Time.restore t; - res - with Fatal _ -> Time.restore t; false end + let constrs = add_rules_from_constrs !constrs in + let res = + List.for_all (eq_modulo_constrs constrs) to_solve in + Time.restore t; + remove_hypo_inj s; + res | _ -> false (* TODO *) with | Fatal _ -> Time.restore t; true From 2f7a5e7aa0536b408ac43c61594d8a904590cb03 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Mon, 17 Jun 2019 13:34:08 +0200 Subject: [PATCH 23/26] Rename some functions --- src/completion.ml | 8 ++++---- src/confluence.ml | 30 ++++++++++++++++-------------- src/extra.ml | 39 ++++++++++++++++++--------------------- 3 files changed, 38 insertions(+), 39 deletions(-) diff --git a/src/completion.ml b/src/completion.ml index 6aa24247f..618dc075d 100644 --- a/src/completion.ml +++ b/src/completion.ml @@ -7,7 +7,7 @@ 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 Ord.cmp -> term Ord.cmp = fun ord t1 t2 -> +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 @@ -25,7 +25,7 @@ let rec lpo : sym Ord.cmp -> term Ord.cmp = fun ord t1 t2 -> else -1 | 0 -> if List.for_all (fun x -> lpo ord t1 x > 0) args' then - Ord.ord_lex (lpo ord) args args' + ord_lex (lpo ord) args args' else -1 | _ -> -1 @@ -132,7 +132,7 @@ let topo_sort : string list -> (string * string) list -> int StrMap.t 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 Ord.cmp = fun eqs -> +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 @@ -152,7 +152,7 @@ let ord_from_eqs : (term * term) list -> sym Ord.cmp = fun eqs -> (** [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 Ord.cmp -> (sym * rule list) list +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. *) diff --git a/src/confluence.ml b/src/confluence.ml index 172d3214d..4bc80eb97 100644 --- a/src/confluence.ml +++ b/src/confluence.ml @@ -21,17 +21,15 @@ let rec unif_aux : term -> term -> unif_constrs -> unit = fun t1 t2 eqs -> | Abst _, _ | _, Abst _ -> assert false | Appl (t1, u1), Appl (t2, u2) -> unif ((t1, t2) :: (u1, u2) :: eqs) - | Meta (m1, ts1), Meta (_, ts2) -> - assert (ts1 = [||] && ts2 = [||]); + | 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, ts1), t2) - | (t2, Meta (m1, ts1)) -> + | (Meta (m1, [||]), t2) + | (t2, Meta (m1, [||])) -> if occurs m1 t2 then raise Unsolvable else - assert (ts1 = [||]); let vs = Bindlib.new_mvar mkfree [||] in let bt2 = Bindlib.bind_mvar vs (lift t2) in set_meta m1 (Bindlib.unbox bt2); @@ -47,7 +45,7 @@ and unif : unif_constrs -> unit = fun 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 to_terms rs 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 @@ -55,13 +53,17 @@ let cps : (sym * rule) list -> (term * term) list = fun rs -> (* [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 -> - 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 + 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; @@ -72,7 +74,7 @@ let cps : (sym * rule) list -> (term * term) list = fun rs -> | [] -> () | r :: rs' -> begin List.iter (cps_aux true r) rs'; - cps_aux false r r; + cps_aux false r r; cps rs' end in cps rs; !acc diff --git a/src/extra.ml b/src/extra.ml index d8ce766e0..8d1162f13 100644 --- a/src/extra.ml +++ b/src/extra.ml @@ -130,27 +130,6 @@ module Array = Array.length a1 = Array.length a2 && for_all2 eq a1 a2 end -module Ord = - struct - (** 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 - end - (* Functional maps with [int] keys. *) module IntMap = Map.Make(Int) @@ -193,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 From f13d037980c0eadc381b6a410d91e7d2d484b02e Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Mon, 17 Jun 2019 13:40:25 +0200 Subject: [PATCH 24/26] Fix some bugs --- src/unif.ml | 66 +++++++++++++++++++++++++++-------------------------- 1 file changed, 34 insertions(+), 32 deletions(-) diff --git a/src/unif.ml b/src/unif.ml index 452a8e96c..99321802c 100644 --- a/src/unif.ml +++ b/src/unif.ml @@ -472,14 +472,14 @@ and check_pair_of_rules : let _, args1 = get_args lhs1 in let _, args2 = get_args lhs2 in let args = List.combine args1 args2 in - let constrs = ref [] in - List.iter2 - (fun b (arg1, arg2) -> if b then unif constrs arg1 arg2) bls args; - unif constrs rhs1 rhs2; + let to_solve = + (rhs1, rhs2) :: List.map snd (List.filter fst (List.combine bls args)) + in + let constrs = solve {no_problems with to_solve} in let to_solve = List.map snd (List.filter (fun (b, _) -> not b) (List.combine bls args)) in - let constrs = add_rules_from_constrs !constrs in + let constrs = add_rules_from_constrs constrs in let res = List.for_all (eq_modulo_constrs constrs) to_solve in Time.restore t; @@ -497,33 +497,37 @@ and check_single_rule : bool list -> sym -> term * term -> bool 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 () = + hypo_inj bls s; + 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} in + let to_solve = + List.map + snd (List.filter (fun (b, _) -> not b) (List.combine bls argss)) + in + let constrs = add_rules_from_constrs constrs in + let res = + List.for_all (eq_modulo_constrs constrs) to_solve in + Time.restore t; + remove_hypo_inj s; + res + in try match h1 with - | Meta (m, _) -> - let _, args2 = get_args lhs in + | Meta (m, _) when args1 = [] -> let fn = function | Meta (m', _) -> m == m' | _ -> false in - List.exists2 (fun b arg -> b && fn arg) bls args2 - | Symb (s', _) when !(s'.sym_rules) = [] -> true - | Symb (s', _) when s == s' -> - let _, args2 = get_args lhs in - let new_args = new_args (List.length args2) in - let constrs = ref [] in - List.iter2 (unif constrs) args1 new_args; - let argss = List.combine args2 new_args in - List.iter2 - (fun b (arg1, arg2) -> if b then unif constrs arg1 arg2) bls argss; - let to_solve = - List.map - snd (List.filter (fun (b, _) -> not b) (List.combine bls argss)) - in - let constrs = add_rules_from_constrs !constrs in - let res = - List.for_all (eq_modulo_constrs constrs) to_solve in - Time.restore t; - remove_hypo_inj s; - res - | _ -> false (* TODO *) + 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 _ -> true + | _ -> false (* TODO *) with | Fatal _ -> Time.restore t; true | _ -> Time.restore t; false @@ -545,10 +549,8 @@ and check_inj_sym : bool list -> sym -> bool = fun bls s -> List.fold_left (fun acc r' -> acc && check_pair_of_rules bls s r r') true rs' in - let res = - List.for_all (check_single_rule bls s) terms_of_rules && - check_inj_rules terms_of_rules in - res + 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, From 71eacf822b6b97d6dabc83ce27b9d0e37f9d5343 Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Thu, 27 Jun 2019 16:59:17 +0200 Subject: [PATCH 25/26] Fix some bugs --- src/sr.ml | 5 +- src/unif.ml | 130 ++++++++++++++++++++++++++-------------------------- 2 files changed, 67 insertions(+), 68 deletions(-) diff --git a/src/sr.ml b/src/sr.ml index 0e31366de..f82feaa0d 100644 --- a/src/sr.ml +++ b/src/sr.ml @@ -76,13 +76,14 @@ let check_rule : let t0 = Time.save () in if !log_enabled then typ_cond "LHS" ty_lhs lhs_constrs; try - let constrs = Unif.add_rules_from_constrs lhs_constrs in + 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 constrs)) cs in + 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 diff --git a/src/unif.ml b/src/unif.ml index 99321802c..24bc250c8 100644 --- a/src/unif.ml +++ b/src/unif.ml @@ -40,6 +40,9 @@ type problems = ; recompute : bool (** Indicates whether unsolved problems should be rechecked. *) } +(** Type of a hypothesis on injectivity. *) +type inj_hypo = sym * bool list + (** Empty problem. *) let no_problems : problems = {to_solve = []; unsolved = []; recompute = false} @@ -88,18 +91,19 @@ let instantiate : meta -> term array -> term -> bool = fun m ts u -> (** [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 -> +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 -> - if Eval.eq_modulo t1 t2 then solve p else +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 @@ -114,8 +118,8 @@ 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 @@ -128,7 +132,7 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> let to_solve = 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 @@ -163,7 +167,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 @@ -221,7 +225,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 @@ -251,7 +255,7 @@ 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 () @@ -259,12 +263,12 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> 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) ) -> @@ -282,16 +286,23 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> let t = snd Pervasives.(!t) in let u = snd Pervasives.(!u) in Eval.eq_modulo t u) ts1 ts2 in - if check_inj_sym bls s1 then decompose_part bls () - else add_to_unsolved () + 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 @@ -389,35 +400,16 @@ and solve_aux : term -> term -> problems -> unif_constrs = fun t1 t2 p -> 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. *) -(** [unif constrs t1 t2] attempts to unify [t1] and [t2], and adds the - constraints obtained into [constrs]. *) -and unif : unif_constrs ref -> term -> term -> unit = fun constrs t1 t2 -> - let to_solve = [(t1, t2)] in - let problems = { no_problems with to_solve } in - constrs := (solve problems) @ (!constrs) - -(** [check_incl bls blss] checks if there exists [bls'] in [blss] such that - 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 check_incl : bool list -> bool list list -> bool = fun bls blss -> - let check_incl_aux bls' = - List.for_all2 (fun b b' -> b || not b') bls bls' in - List.exists check_incl_aux blss - -(** [hypo_inj bls s] adds the hypothesis that [s] is I-injective where I is - represented by [bls]. *) -and hypo_inj : bool list -> sym -> unit = fun bls s -> - match s.sym_mode with - | Const -> () - | Defin -> s.sym_mode <- Injec [bls] - | Injec l -> s.sym_mode <- Injec (bls :: l) +(** [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' -(** [remove_hypo_inj s] removes the last hypothesis on [s]. *) -and remove_hypo_inj : sym -> unit = fun s -> - match s.sym_mode with - | Const - | Defin -> () - | Injec l -> s.sym_mode <- Injec (List.tl l) +(** [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' @@ -431,8 +423,8 @@ and eq_modulo_constrs : unif_constrs -> term * term -> bool (** [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 returns the rest of it. *) -and add_rules_from_constrs : unif_constrs -> unif_constrs = fun constrs -> + 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 -> @@ -443,22 +435,21 @@ and add_rules_from_constrs : unif_constrs -> unif_constrs = fun constrs -> m.meta_value := Some (Bindlib.unbox (Bindlib.bind_mvar [||] (_Symb c_m Nothing))) | Some _ -> () in - let split_constrs (fo, others) (t, u) = + 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, others - with Non_nullary_meta -> fo, (t, u) :: others in - let constrs_fo, others = List.fold_left split_constrs ([], []) constrs in + (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; - others + (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 @@ -468,26 +459,35 @@ and check_pair_of_rules : = fun bls s (lhs1, rhs1) (lhs2, rhs2) -> let t = Time.save () in try - hypo_inj bls s; 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} 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 - let constrs = add_rules_from_constrs constrs in + add_rules_from_constrs constrs; let res = List.for_all (eq_modulo_constrs constrs) to_solve in Time.restore t; - remove_hypo_inj s; res with - | Fatal _ -> Time.restore t; remove_hypo_inj s; true - | _ -> Time.restore t; remove_hypo_inj s; false + | 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. *) @@ -502,20 +502,18 @@ and check_single_rule : bool list -> sym -> term * term -> bool let argss = List.combine args2 new_args in let new_term = add_args (Symb (s, Nothing)) new_args in let infer_from_constrs () = - hypo_inj bls s; 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} 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 - let constrs = add_rules_from_constrs constrs in + add_rules_from_constrs constrs; let res = List.for_all (eq_modulo_constrs constrs) to_solve in Time.restore t; - remove_hypo_inj s; res in try match h1 with @@ -526,7 +524,7 @@ and check_single_rule : bool list -> sym -> term * term -> bool 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 _ -> true + | Symb (s', _) -> non_erasing_rec s' | _ -> false (* TODO *) with | Fatal _ -> Time.restore t; true @@ -536,7 +534,7 @@ and check_single_rule : bool list -> sym -> term * term -> bool I is represented by [bls]. *) and check_inj_sym : bool list -> sym -> bool = fun bls s -> match s.sym_mode with - | Injec l when check_incl bls l -> true + | Injec l when inj_incls bls l -> true | _ -> let rules = !(s.sym_rules) in let terms_of_rules = @@ -560,5 +558,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 From 9aa4992af63daaddbc5c9567d30d32d5b3dd4a3a Mon Sep 17 00:00:00 2001 From: wujuihsuan2016 Date: Fri, 28 Jun 2019 10:17:45 +0200 Subject: [PATCH 26/26] Add missing comments --- src/unif.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/unif.ml b/src/unif.ml index 24bc250c8..bd76c6fee 100644 --- a/src/unif.ml +++ b/src/unif.ml @@ -40,7 +40,10 @@ type problems = ; recompute : bool (** Indicates whether unsolved problems should be rechecked. *) } -(** Type of a hypothesis on injectivity. *) +(** 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. *) @@ -89,8 +92,8 @@ 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. *) +(** [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 = []; _ } -> [] @@ -99,8 +102,9 @@ let rec solve : problems -> inj_hypo option -> unif_constrs = fun p hypo -> | { to_solve = []; unsolved = cs; _ } -> cs | { 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. *) +(** [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 @@ -531,7 +535,8 @@ and check_single_rule : bool list -> sym -> term * term -> bool | _ -> Time.restore t; false (** [check_inj_sym bls s] checks if the symbol [s] is I-injective, where - I is represented by [bls]. *) + 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