From f2bd761fed232e3c99f3dd281d492e74622091e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 2 Apr 2020 09:46:54 +0200 Subject: [PATCH 01/66] fix #303 handling of metavariables in RHS --- src/core/basics.ml | 14 +++++++------- src/core/extra.ml | 9 +++++++++ src/core/proof.ml | 6 ++++++ src/core/scope.ml | 27 ++++++++++++++------------- src/core/sr.ml | 20 +++++++++++++++----- src/core/tactics.ml | 5 ++++- src/core/terms.ml | 15 +++++++++------ src/core/xtc.ml | 2 +- tests/OK/303.lp | 11 +++++++++++ tests/OK/logic.lp | 2 +- 10 files changed, 77 insertions(+), 34 deletions(-) create mode 100644 tests/OK/303.lp diff --git a/src/core/basics.ml b/src/core/basics.ml index 4c0a4890a..afee7f1ae 100644 --- a/src/core/basics.ml +++ b/src/core/basics.ml @@ -178,13 +178,13 @@ let occurs : meta -> term -> bool = let fn p = if m == p then raise Found in try iter_meta false fn t; false with Found -> true -(** [get_metas b t] returns the list of all the metavariables in [t], and in - the types of metavariables recursively if [b], sorted wrt [cmp_meta]. *) -let get_metas : bool -> term -> meta list = fun b t -> +(** [get_metas b t] returns the set of all the metavariables in [t], and in + the types of metavariables recursively if [b]. *) +let get_metas : bool -> term -> MetaSet.t = fun b t -> let open Stdlib in - let l = ref [] in - iter_meta b (fun m -> l := m :: !l) t; - List.sort_uniq cmp_meta !l + let ms = ref MetaSet.empty in + iter_meta b (fun m -> ms := MetaSet.add m !ms) t; + !ms (** [has_metas b t] checks whether there are metavariables in [t], and in the types of metavariables recursively if [b] is true. *) @@ -246,4 +246,4 @@ let term_of_rhs : rule -> term = fun r -> let p = _Patt (Some(i)) name (Array.map Bindlib.box_var vars) in TE_Some(Bindlib.unbox (Bindlib.bind_mvar vars p)) in - Bindlib.msubst r.rhs (Array.mapi fn r.vars) + Bindlib.msubst r.rhs (Array.mapi fn r.pvs) diff --git a/src/core/extra.ml b/src/core/extra.ml index a982078ad..ad6c53ae2 100644 --- a/src/core/extra.ml +++ b/src/core/extra.ml @@ -239,6 +239,15 @@ module List = | _ -> false in in_sorted + (** [insert cmp x l] inserts [x] in the list [l] assuming that [l] is + sirted wrt [cmp]. *) + let insert : 'a cmp -> 'a -> 'a list -> 'a list = fun cmp x -> + let rec insert acc l = + match l with + | y :: m when cmp x y > 0 -> insert (y::acc) m + | _ -> List.rev_append acc (x::l) + in insert [] + end module Array = diff --git a/src/core/proof.ml b/src/core/proof.ml index 401abff98..9b1246c36 100644 --- a/src/core/proof.ml +++ b/src/core/proof.ml @@ -22,6 +22,9 @@ module Goal : (** [simpl g] simplifies the given goal, evaluating its type to SNF. *) val simpl : t -> t + + (** Comparison function. *) + val compare : t -> t -> int end = struct type t = @@ -42,6 +45,9 @@ module Goal : let simpl : t -> t = fun g -> {g with goal_type = Eval.snf (Env.to_ctxt g.goal_hyps) g.goal_type} + + let compare : t -> t -> int = fun g1 g2 -> + Meta.compare g1.goal_meta g2.goal_meta end (** Representation of the proof state of a theorem. *) diff --git a/src/core/scope.ml b/src/core/scope.ml index a3022db60..d029b73ad 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -282,13 +282,14 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> | (P_Wild , M_LHS(_) ) -> fresh_patt env | (P_Wild , M_Patt ) -> _Wild | (P_Wild , _ ) -> - (* We create a metavariable [m] of type [m_ty], which is itself also a - metavariable (of type [Type]). Note that this case applies both to - regular terms, and to the RHS of rewriting rules. *) + (* We create a metavariable [m] of type [tm], which itself is also a + metavariable [x] of type [Type]. Note that this case applies both + to regular terms, and to the RHS of rewriting rules. *) let vs = Env.to_tbox env in - let m_ty = fresh_meta (Env.to_prod env _Type) (Array.length vs) in - let a = Env.to_prod env (_Meta m_ty vs) in - let m = fresh_meta a (Array.length vs) in + let n = Array.length vs in + let x = fresh_meta (Env.to_prod env _Type) n in + let tm = Env.to_prod env (_Meta x vs) in + let m = fresh_meta tm n in _Meta m vs | (P_Meta(id,ts) , M_Term(m,_) ) -> let m2 = @@ -480,7 +481,7 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> let (pvs_lhs, nl) = patt_vars p_lhs in let (pvs_rhs, _ ) = patt_vars p_rhs in (* NOTE to reject non-left-linear rules, we can check [nl = []] here. *) - (* Check that the meta-variables of the RHS exist in the LHS. *) + (* Check that the pattern variables of the RHS exist in the LHS. *) let check_in_lhs (m,i) = let j = try List.assoc m pvs_lhs with Not_found -> @@ -491,11 +492,11 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> List.iter check_in_lhs pvs_rhs; (* Get the non-linear variables not in the RHS. *) let nl = List.filter (fun m -> not (List.mem_assoc m pvs_rhs)) nl in - (* Reserve space for meta-variables that appear non-linearly in the LHS. *) + (* Reserve space for pattern variables that appear non-linearly in the LHS. *) let pvs = List.map (fun m -> (m, List.assoc m pvs_lhs)) nl @ pvs_rhs in let map = List.mapi (fun i (m,_) -> (m,i)) pvs in - (* NOTE [map] maps meta-variables to their position in the environment. *) - (* NOTE meta-variables not in [map] can be considered as wildcards. *) + (* NOTE [map] maps pattern variables to their position in the environment. *) + (* NOTE pattern variables not in [map] can be considered as wildcards. *) (* Get privacy of the head of the rule, and scope the rest with this privacy. *) let prv = is_private (fst (get_root p_lhs ss)) in @@ -515,7 +516,7 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> fatal p_lhs.pos "No head symbol in LHS." in if lhs = [] then wrn p_lhs.pos "LHS head symbol with no argument."; - (* We scope the RHS and bind the meta-variables. *) + (* We scope the RHS and bind the pattern variables. *) let names = Array.of_list (List.map fst map) in let vars = Bindlib.new_mvar te_mkfree names in let rhs = @@ -524,9 +525,9 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> Bindlib.unbox (Bindlib.bind_mvar vars (scope mode ss Env.empty p_rhs)) in (* We also store [pvs] to facilitate confluence / termination checking. *) - let vars = Array.of_list pvs in + let pvs = Array.of_list pvs in (* We put everything together to build the rule. *) - (sym, hint, Pos.make r.pos {lhs; rhs; arity = List.length lhs; vars}) + (sym, hint, Pos.make r.pos {lhs; rhs; arity = List.length lhs; pvs; vars}) (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term that will correspond to selection pattern (rewrite tactic). *) diff --git a/src/core/sr.ml b/src/core/sr.ml index 7fe610ed1..56667371e 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -66,8 +66,11 @@ let build_meta_type : int -> term = fun k -> 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 binder_arity = Bindlib.mbinder_arity r.elt.rhs in + (* Compute the metavariables of the RHS. *) + let rhs = Bindlib.msubst r.elt.rhs (Array.make binder_arity TE_None) in + let rhs_metas = Basics.get_metas true rhs in + (* We process the LHS to replace pattern variables by metavariables. *) let metas = Array.make binder_arity None in let rec to_m : int -> term -> tbox = fun k t -> (* [k] is the number of arguments to which [m] is applied. *) @@ -102,8 +105,8 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit = | 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 + let lhs_args = List.map (fun p -> Bindlib.unbox (to_m 0 p)) r.elt.lhs in + let lhs = Basics.add_args (Symb(s,h)) lhs_args in let metas = Array.map (function Some m -> m | None -> assert false) metas in (* We substitute the RHS with the corresponding metavariables. *) let fn m = @@ -113,7 +116,14 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit = 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 + let subst t = Bindlib.msubst t te_envs in + let rhs = subst r.elt.rhs in + (* We substitute the metavariables of the RHS as well. *) + let fn m = + let bt = lift !(m.meta_type) in + m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar r.elt.vars bt)) + in + MetaSet.iter fn rhs_metas; (* Infer the type of the LHS and the constraints. *) match Typing.infer_constr builtins [] lhs with | None -> wrn r.pos "Untypable LHS." @@ -160,7 +170,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit = (* Check that there is no uninstanciated metas left. *) let lhs_metas = Basics.get_metas false lhs in let f m = - if not (List.in_sorted cmp_meta m lhs_metas) then + if not (MetaSet.mem m lhs_metas) then fatal r.pos "Cannot instantiate all metavariables in rule [%a]." pp_rule (s,h,r.elt) in diff --git a/src/core/tactics.ml b/src/core/tactics.ml index 63ce6a02e..d301b4c86 100644 --- a/src/core/tactics.ml +++ b/src/core/tactics.ml @@ -56,9 +56,12 @@ let handle_tactic : sig_state -> Proof.t -> p_tactic -> Proof.t = set_meta m (Bindlib.unbox (Bindlib.bind_mvar (Env.vars env) (lift t))); (* New subgoals and focus. *) let metas = Basics.get_metas true t in - let new_goals = List.map Proof.Goal.of_meta metas in + let add_goal m = List.insert Proof.Goal.compare (Proof.Goal.of_meta m) in + let new_goals = MetaSet.fold add_goal metas [] in + (* New goals must appear first. *) Proof.({ps with proof_goals = new_goals @ gs}) in + match tac.elt with | P_tac_print | P_tac_proofterm diff --git a/src/core/terms.ml b/src/core/terms.ml index 34af12642..f3c9ec224 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -143,8 +143,10 @@ type term = (** Right hand side (or RHS). *) ; arity : int (** Required number of arguments to be applicable. *) - ; vars : (string * int) array - (** Name and arity of the pattern variables bound in the RHS. *) } + ; pvs : (string * int) array + (** Name and arity of the pattern variables bound in the RHS. *) + ; vars : term_env Bindlib.var array + (** Bindlib variables used to build [rhs]. *) } (** The LHS (or pattern) of a rewriting rule is always formed of a head symbol (on which the rule is defined) applied to a list of pattern arguments. The @@ -242,11 +244,12 @@ type term = ; meta_value : (term, term) Bindlib.mbinder option ref (** Definition of the metavariable, if known. *) } -(** Comparison function on metavariables. *) -let cmp_meta : meta -> meta -> int = fun m1 m2 -> m1.meta_key - m2.meta_key +module Meta = struct + type t = meta + let compare m1 m2 = m1.meta_key - m2.meta_key +end -(** Equality on metavariables. *) -let eq_meta : meta -> meta -> bool = fun m1 m2 -> m1.meta_key = m2.meta_key +module MetaSet = Set.Make(Meta) (** [symb s] returns the term [Symb (s, Nothing)]. *) let symb : sym -> term = fun s -> Symb (s, Nothing) diff --git a/src/core/xtc.ml b/src/core/xtc.ml index 23caed2a5..496c256fa 100644 --- a/src/core/xtc.ml +++ b/src/core/xtc.ml @@ -118,7 +118,7 @@ let print_tl_rule : Format.formatter -> int -> sym -> rule -> unit = in the form of a pair containing the name of the variable and its type, inferred by the solver. *) let get_vars : sym -> rule -> (string * Terms.term) list = fun s r -> - let rule_ctx : tvar option array = Array.make (Array.length r.vars) None in + let rule_ctx : tvar option array = Array.make (Array.length r.pvs) None in let var_list : tvar list ref = ref [] in let rec subst_patt v t = match t with diff --git a/tests/OK/303.lp b/tests/OK/303.lp new file mode 100644 index 000000000..ea0c0230f --- /dev/null +++ b/tests/OK/303.lp @@ -0,0 +1,11 @@ +constant symbol U : TYPE + +constant symbol u : U + +constant symbol f : (U ⇒ U) ⇒ TYPE + +symbol G : U ⇒ TYPE + +constant symbol H : U ⇒ TYPE + +rule G &v → ∀ (a : H &v), f (λ _, u) diff --git a/tests/OK/logic.lp b/tests/OK/logic.lp index 81e1b4918..5a9578352 100644 --- a/tests/OK/logic.lp +++ b/tests/OK/logic.lp @@ -111,4 +111,4 @@ set builtin "top" ≔ top set builtin "imp" ≔ imp set builtin "and" ≔ {|and|} set builtin "or" ≔ or -set builtin "not" ≔ not \ No newline at end of file +set builtin "not" ≔ not From 8f068a09a842ce30380f1edc3d7570b207fcea67 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 2 Apr 2020 11:36:56 +0200 Subject: [PATCH 02/66] fix typo in comment --- src/core/extra.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/extra.ml b/src/core/extra.ml index ad6c53ae2..2cd5599e3 100644 --- a/src/core/extra.ml +++ b/src/core/extra.ml @@ -240,7 +240,7 @@ module List = in in_sorted (** [insert cmp x l] inserts [x] in the list [l] assuming that [l] is - sirted wrt [cmp]. *) + sorted wrt [cmp]. *) let insert : 'a cmp -> 'a -> 'a list -> 'a list = fun cmp x -> let rec insert acc l = match l with From a8b991686e3f4edfecb9704f9acdf6eefc47cb0b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 2 Apr 2020 19:18:32 +0200 Subject: [PATCH 03/66] fix typo in comment --- src/core/terms.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/terms.ml b/src/core/terms.ml index f3c9ec224..85ef6916a 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -52,9 +52,9 @@ type term = | Meta of meta * term array (** Metavariable application (used by unification and for proof goals). *) | Patt of int option * string * term array - (** Pattern variable application (only used in a rewriting rules LHS). *) + (** Pattern variable application (only used in rewriting rule LHS). *) | TEnv of term_env * term array - (** Term environment (only used in a rewriting rules RHS). *) + (** Term environment (only used in rewriting rules RHS). *) | Wild (** Wildcard (only used for surface matching, never in a LHS). *) | TRef of term option ref From 50069df108afb731d16d214a2ae7beaf5bd7da43 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 2 Apr 2020 19:19:56 +0200 Subject: [PATCH 04/66] prepare fix --- src/core/handle.ml | 2 +- src/core/sr.ml | 39 +++++++++++++++++++++++---------------- 2 files changed, 24 insertions(+), 17 deletions(-) diff --git a/src/core/handle.ml b/src/core/handle.ml index a60662d86..82c431ba1 100644 --- a/src/core/handle.ml +++ b/src/core/handle.ml @@ -123,7 +123,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = if !(s.sym_def) <> None then fatal pr.pos "Rewriting rules cannot be given for defined \ symbol [%s]." s.sym_name; - Sr.check_rule ss.builtins r; r + Sr.check_rule ss.builtins r in let rs = List.map handle_rule rs in (* Adding the rules all at once. *) diff --git a/src/core/sr.ml b/src/core/sr.ml index 56667371e..258b25599 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -63,12 +63,13 @@ let build_meta_type : int -> term = fun k -> (** [check_rule builtins r] checks whether rule [r] is well-typed. The [Fatal] exception is raised 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); - let binder_arity = Bindlib.mbinder_arity r.elt.rhs in +let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc + -> sym * pp_hint * rule Pos.loc = + fun builtins ((s, h, { elt = rule; pos = pos }) as shrp) -> + if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, rule); + let binder_arity = Bindlib.mbinder_arity rule.rhs in (* Compute the metavariables of the RHS. *) - let rhs = Bindlib.msubst r.elt.rhs (Array.make binder_arity TE_None) in + let rhs = Bindlib.msubst rule.rhs (Array.make binder_arity TE_None) in let rhs_metas = Basics.get_metas true rhs in (* We process the LHS to replace pattern variables by metavariables. *) let metas = Array.make binder_arity None in @@ -105,28 +106,28 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit = | Wild -> assert false (* Cannot appear in LHS. *) | TRef(_) -> assert false (* Cannot appear in LHS. *) in - let lhs_args = List.map (fun p -> Bindlib.unbox (to_m 0 p)) r.elt.lhs in + let lhs_args = List.map (fun p -> Bindlib.unbox (to_m 0 p)) rule.lhs in let lhs = Basics.add_args (Symb(s,h)) lhs_args in let metas = Array.map (function Some m -> m | None -> assert false) metas in (* We substitute the RHS with the corresponding metavariables. *) let fn m = - let xs = Array.init m.meta_arity (Printf.sprintf "x%i") in - let xs = Bindlib.new_mvar mkfree xs in + let ns = Array.init m.meta_arity (Printf.sprintf "x%i") in + let xs = Bindlib.new_mvar mkfree ns 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 subst t = Bindlib.msubst t te_envs in - let rhs = subst r.elt.rhs in + let rhs = subst rule.rhs in (* We substitute the metavariables of the RHS as well. *) let fn m = let bt = lift !(m.meta_type) in - m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar r.elt.vars bt)) + m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar rule.vars bt)) in MetaSet.iter fn rhs_metas; (* Infer the type of the LHS and the constraints. *) match Typing.infer_constr builtins [] lhs with - | None -> wrn r.pos "Untypable LHS." + | None -> wrn pos "Untypable LHS."; shrp | Some(ty_lhs, lhs_constrs) -> if !log_enabled then begin @@ -149,7 +150,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit = (* Solving the constraints. *) match Unif.(solve builtins false {no_problems with to_solve}) with | None -> - fatal r.pos "Rule [%a] does not preserve typing." pp_rule (s,h,r.elt) + fatal pos "Rule [%a] does not preserve typing." pp_rule (s,h,rule) | Some(cs) -> let is_constr c = let eq_comm (_,t1,u1) (_,t2,u2) = @@ -165,13 +166,19 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit = if cs <> [] then begin List.iter (fatal_msg "Cannot solve %a\n" pp_constr) cs; - fatal r.pos "Unable to prove SR for rule [%a]." pp_rule (s,h,r.elt) + fatal pos "Unable to prove SR for rule [%a]." pp_rule (s,h,rule) end; (* Check that there is no uninstanciated metas left. *) let lhs_metas = Basics.get_metas false lhs in let f m = if not (MetaSet.mem m lhs_metas) then - fatal r.pos "Cannot instantiate all metavariables in rule [%a]." - pp_rule (s,h,r.elt) + fatal pos "Cannot instantiate all metavariables in rule [%a]." + pp_rule (s,h,rule) in - Basics.iter_meta false f rhs + Basics.iter_meta false f rhs; + (* Return rule with metavariables instanciated. We need to replace + metavariables by term_env variables, and bind them. *) + let new_rhs = rule.rhs in + (*Bindlib.unbox (Bindlib.bind_mvar rule.vars (lift rhs))*) + let new_rule = { rule with rhs = new_rhs } in + (s, h, { elt = new_rule; pos = pos }) From 17a6a503b8cf453ff88c73fda0568b7afad10a74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 2 Apr 2020 23:13:09 +0200 Subject: [PATCH 05/66] fix typos in comments --- src/core/scope.ml | 14 +++++++------- src/core/terms.ml | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/core/scope.ml b/src/core/scope.ml index d029b73ad..366ec8362 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -33,15 +33,15 @@ let open_sign : sig_state -> Sign.t -> sig_state = fun ss sign -> let builtins = StrMap.union fn ss.builtins Sign.(!(sign.sign_builtins)) in {ss with in_scope; builtins} -(** [find_sym ~prt ~prv b st qid] returns the symbol and printing hint +(** [find_sym prt prv b st qid] returns the symbol and printing hint corresponding to the qualified identifier [qid]. If [fst qid.elt] is empty, we search for the name [snd qid.elt] in the opened modules of [st]. The boolean [b] only indicates if the error message should mention variables, in the case where the module path is empty and the symbol is unbound. This is reported using the [Fatal] exception. - {!constructor:Terms.sym_exposition.Protected} symbols from other modules + {!constructor:Terms.expo.Protec} symbols from other modules are allowed in left-hand side of rewrite rules (only) iff [~prt] is true. - {!constructor:Terms.sym_exposition.Private} symbols are allowed iff [~prv] + {!constructor:Terms.expo.Privat} symbols are allowed iff [~prv] is [true]. *) let find_sym : prt:bool -> prv:bool -> bool -> sig_state -> qident -> sym * pp_hint = fun ~prt ~prv b st qid -> @@ -100,10 +100,10 @@ let find_sym : prt:bool -> prv:bool -> bool -> sig_state -> qident -> first search for the name [snd qid.elt] in the environment, and if it is not mapped we also search in the opened modules. The exception [Fatal] is raised if an error occurs (e.g., when the name cannot be found). If [prt] - is true, {!constructor:Terms.sym_exposition.Protected} symbols from + is true, {!constructor:Terms.expo.Protec} symbols from foreign modules are allowed (protected symbols from current modules are always allowed). If [prv] is true, - {!constructor:Terms.sym_exposition.Private} symbols are allowed. *) + {!constructor:Terms.expo.Privat} symbols are allowed. *) let find_qid : bool -> bool -> sig_state -> env -> qident -> tbox = fun prt prv st env qid -> let (mp, s) = qid.elt in @@ -144,13 +144,13 @@ type mode = | M_LHS of (string * int) list * bool (** Scoping mode for rewriting rule left-hand sides. The constructor carries a map associating an index to every free variable along with a flag set - to [true] if {!constructor:Terms.sym_exposition.Private} symbols are + to [true] if {!constructor:Terms.expo.Privat} symbols are allowed. *) | M_RHS of (string * tevar) list * bool (** Scoping mode for rewriting rule righ-hand sides. The constructor carries the environment for variables that will be bound in the representation of the RHS along with a flag indicating whether - {!constructor:Terms.sym_exposition.Private} terms are allowed. *) + {!constructor:Terms.expo.Privat} terms are allowed. *) (** [get_implicitness t] gives the specified implicitness of the parameters of a symbol having the (parser-level) type [t]. *) diff --git a/src/core/terms.ml b/src/core/terms.ml index 85ef6916a..80b856235 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -186,7 +186,7 @@ type term = minimal number of arguments required to match the LHS of the rule. *) (** The RHS (or action) or a rewriting rule is represented by a term, in which - (higher-order) variables representing a "terms with environments" (see the + (higher-order) variables representing "terms with environments" (see the {!type:term_env} type) are bound. To effectively apply the rewriting rule, these bound variables must be substituted using "terms with environments" that are constructed when matching the LHS of the rule. *) From 465215c4fe684be0db74e839efa57969614dd355 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 2 Apr 2020 23:31:35 +0200 Subject: [PATCH 06/66] fix typo in comment --- src/core/scope.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/scope.ml b/src/core/scope.ml index 366ec8362..02e1510a4 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -33,7 +33,7 @@ let open_sign : sig_state -> Sign.t -> sig_state = fun ss sign -> let builtins = StrMap.union fn ss.builtins Sign.(!(sign.sign_builtins)) in {ss with in_scope; builtins} -(** [find_sym prt prv b st qid] returns the symbol and printing hint +(** [find_sym ~prt ~prv b st qid] returns the symbol and printing hint corresponding to the qualified identifier [qid]. If [fst qid.elt] is empty, we search for the name [snd qid.elt] in the opened modules of [st]. The boolean [b] only indicates if the error message should mention From 9865cc8e8266a61c8d1461254cfabdcad3cbcd5f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 2 Apr 2020 23:53:50 +0200 Subject: [PATCH 07/66] fix typo in comment --- src/core/terms.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/terms.ml b/src/core/terms.ml index 80b856235..7c60f009d 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -52,7 +52,7 @@ type term = | Meta of meta * term array (** Metavariable application (used by unification and for proof goals). *) | Patt of int option * string * term array - (** Pattern variable application (only used in rewriting rule LHS). *) + (** Pattern variable application (only used in rewriting rules LHS). *) | TEnv of term_env * term array (** Term environment (only used in rewriting rules RHS). *) | Wild From ce199bc501ff5091740dd94cc1beb7af443d6470 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 00:13:32 +0200 Subject: [PATCH 08/66] indentation --- src/core/scope.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/core/scope.ml b/src/core/scope.ml index 02e1510a4..3e591b122 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -144,8 +144,7 @@ type mode = | M_LHS of (string * int) list * bool (** Scoping mode for rewriting rule left-hand sides. The constructor carries a map associating an index to every free variable along with a flag set - to [true] if {!constructor:Terms.expo.Privat} symbols are - allowed. *) + to [true] if {!constructor:Terms.expo.Privat} symbols are allowed. *) | M_RHS of (string * tevar) list * bool (** Scoping mode for rewriting rule righ-hand sides. The constructor carries the environment for variables that will be bound in the representation From d82b01970aa041b46ddecadfcb4f48cea8fd1ed5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 13:33:49 +0200 Subject: [PATCH 09/66] comment optim: reserve space for all LHS variables and not only those that are non-linear or appears in the RHS as it may change after SR --- src/core/scope.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/core/scope.ml b/src/core/scope.ml index 3e591b122..4c28c3faa 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -477,10 +477,11 @@ let patt_vars : p_term -> (string * int) list * string list = let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> let (p_lhs, p_rhs) = r.elt in (* Compute the set of pattern variables on both sides. *) - let (pvs_lhs, nl) = patt_vars p_lhs in + let (pvs_lhs, _nl) = patt_vars p_lhs in let (pvs_rhs, _ ) = patt_vars p_rhs in (* NOTE to reject non-left-linear rules, we can check [nl = []] here. *) - (* Check that the pattern variables of the RHS exist in the LHS. *) + (* Check that the pattern variables of the RHS exist in the LHS and have the + same arities. *) let check_in_lhs (m,i) = let j = try List.assoc m pvs_lhs with Not_found -> @@ -489,12 +490,14 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> if i <> j then fatal p_lhs.pos "Arity mismatch for [%s]." m in List.iter check_in_lhs pvs_rhs; + (* Optimization to do *after* SR if really needed: (* Get the non-linear variables not in the RHS. *) let nl = List.filter (fun m -> not (List.mem_assoc m pvs_rhs)) nl in - (* Reserve space for pattern variables that appear non-linearly in the LHS. *) - let pvs = List.map (fun m -> (m, List.assoc m pvs_lhs)) nl @ pvs_rhs in + (* Reserve space for non-linear LHS pattern variables. *) + let pvs = List.map (fun m -> (m, List.assoc m pvs_lhs)) nl @ pvs_rhs in*) + let pvs = pvs_lhs in let map = List.mapi (fun i (m,_) -> (m,i)) pvs in - (* NOTE [map] maps pattern variables to their position in the environment. *) + (* NOTE [map] maps pattern variables to their position in [pvs]. *) (* NOTE pattern variables not in [map] can be considered as wildcards. *) (* Get privacy of the head of the rule, and scope the rest with this privacy. *) From db583e2a86ab0f2771e06698d5def10c018fc2e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 13:34:25 +0200 Subject: [PATCH 10/66] remove subst_from_constrs as it is useless --- src/core/sr.ml | 66 ++++++++++++++++++-------------------------------- 1 file changed, 24 insertions(+), 42 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 258b25599..d24b763b0 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -13,25 +13,6 @@ 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 : unif_constrs -> subst = fun cs -> - let rec build_sub acc cs = - match cs with - | [] -> List.split acc - | (c,a,b)::cs -> - match Ctxt.get_args c a with - | Vari(x), [] -> build_sub ((x,b)::acc) cs - | _, _ -> - match Ctxt.get_args c b with - | Vari(x), [] -> 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) - (** [build_meta_type k] builds the type “∀(x1:A1) ⋯ (xk:Ak), A(k+1)” where the type “Ai = Mi[x1,⋯,x(i-1)]” is defined as the metavariable “Mi” (which has arity “i-1”). The type of “Mi” is “∀(x1:A1) ⋯ (x(i-1):A(i-1)), TYPE”. *) @@ -68,9 +49,12 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc fun builtins ((s, h, { elt = rule; pos = pos }) as shrp) -> if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, rule); let binder_arity = Bindlib.mbinder_arity rule.rhs in - (* Compute the metavariables of the RHS. *) - let rhs = Bindlib.msubst rule.rhs (Array.make binder_arity TE_None) in - let rhs_metas = Basics.get_metas true rhs in + (* Compute the metavariables of the RHS, including the metavariables of + their types. *) + let rhs_metas = + Basics.get_metas true + (Bindlib.msubst rule.rhs (Array.make binder_arity TE_None)) + in (* We process the LHS to replace pattern variables by metavariables. *) let metas = Array.make binder_arity None in let rec to_m : int -> term -> tbox = fun k t -> @@ -109,6 +93,15 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let lhs_args = List.map (fun p -> Bindlib.unbox (to_m 0 p)) rule.lhs in let lhs = Basics.add_args (Symb(s,h)) lhs_args in let metas = Array.map (function Some m -> m | None -> assert false) metas in + (* Infer the type of the LHS and the constraints. *) + match Typing.infer_constr builtins [] lhs with + | None -> wrn pos "Untypable LHS."; shrp + | Some(ty_lhs, lhs_constrs) -> + if !log_enabled then + begin + log_subj "LHS has type %a" pp ty_lhs; + List.iter (log_subj " if %a" pp_constr) lhs_constrs + end; (* We substitute the RHS with the corresponding metavariables. *) let fn m = let ns = Array.init m.meta_arity (Printf.sprintf "x%i") in @@ -125,38 +118,27 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar rule.vars bt)) in MetaSet.iter fn rhs_metas; - (* Infer the type of the LHS and the constraints. *) - match Typing.infer_constr builtins [] lhs with - | None -> wrn pos "Untypable LHS."; shrp - | Some(ty_lhs, lhs_constrs) -> - if !log_enabled then - begin - log_subj "LHS has type [%a]" pp ty_lhs; - let fn (c,t,u) = log_subj " if %a[%a] ~ [%a]" pp_ctxt c 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 + (* Here, we should instantiate the LHS metas by fresh function symbols and + complete the constraints into a set of rewriting rules on those function + symbols. *) (* Check that the RHS has the same type as the LHS. *) let to_solve = Infer.check [] rhs ty_lhs in if !log_enabled && to_solve <> [] then begin - log_subj "RHS has type [%a]" pp ty_lhs; + log_subj "RHS has type %a" pp ty_lhs; List.iter (log_subj " if %a" pp_constr) to_solve end; - (* Solving the constraints. *) + (* Solving the constraints. To help resolution, metavariable symbols having + no constraint could be replaced by fresh variables. *) match Unif.(solve builtins false {no_problems with to_solve}) with | None -> fatal pos "Rule [%a] does not preserve typing." pp_rule (s,h,rule) | Some(cs) -> let is_constr c = let eq_comm (_,t1,u1) (_,t2,u2) = - (* Contexts ignored: [infer_constr] is called with an empty context and - * neither [check] nor [solve] generate contexts with defined - * variables. *) + (* Contexts ignored: [Infer.check] is called with an empty context and + neither [Infer.check] nor [Unif.solve] generate contexts with defined + variables. *) (Eval.eq_modulo [] t1 t2 && Eval.eq_modulo [] u1 u2) || (Eval.eq_modulo [] t1 u2 && Eval.eq_modulo [] t2 u1) in From e91ee90d8941d9128c3e67ade7d61235fe301615 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:39:07 +0200 Subject: [PATCH 11/66] basics: add fresh_vars --- src/core/basics.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/core/basics.ml b/src/core/basics.ml index afee7f1ae..2cea5bd00 100644 --- a/src/core/basics.ml +++ b/src/core/basics.ml @@ -4,6 +4,10 @@ open Extra open Timed open Terms +(** Create an array of fresh variables [|x1;..;xn|]. *) +let fresh_vars : int -> tvar array = fun n -> + Bindlib.new_mvar mkfree (Array.init n (Printf.sprintf "x%i")) + (** Sets and maps of variables. *) module Var = struct From 588eddcae36f6075167dd8978e3b56abf20aacc0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:39:44 +0200 Subject: [PATCH 12/66] infer: change in log message --- src/core/infer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/infer.ml b/src/core/infer.ml index 655f1e64a..30981f63e 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -188,7 +188,7 @@ let infer : ctxt -> term -> term * unif_constrs = fun ctx t -> if !log_enabled then begin log_infr (gre "infer [%a] yields [%a]") pp t pp a; - List.iter (log_infr " assuming %a" pp_constr) constrs; + List.iter (log_infr " if %a" pp_constr) constrs; end; Stdlib.(constraints := []); (a, constrs) From d369293f2888a40a568d44fd2dc27fc6f6ab2b16 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:40:46 +0200 Subject: [PATCH 13/66] Terms.set_meta: do not erase the type! --- src/core/terms.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/terms.ml b/src/core/terms.ml index 7c60f009d..7ca91d268 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -312,7 +312,7 @@ let fresh_meta : ?name:string -> term -> int -> meta = (** [set_meta m v] sets the value of the metavariable [m] to [v]. Note that no specific check is performed, so this function may lead to cyclic terms. *) let set_meta : meta -> (term, term) Bindlib.mbinder -> unit = fun m v -> - m.meta_type := Kind (* to save memory *); m.meta_value := Some(v) + m.meta_value := Some(v) (** [internal m] returns [true] if [m] is unnamed (i.e., not user-defined). *) let internal : meta -> bool = fun m -> m.meta_name = None From 2706e78330340f3a142157c1d27f77cea650d48b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:41:35 +0200 Subject: [PATCH 14/66] unif: log instantiations --- src/core/unif.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/core/unif.ml b/src/core/unif.ml index c01d1ed5d..fd32d6b72 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -52,7 +52,10 @@ let instantiation : ctxt -> meta -> term array -> term -> let instantiate : ctxt -> meta -> term array -> term -> bool = fun ctx m ts u -> match instantiation ctx m ts u with - | Some(bu) when Bindlib.is_closed bu -> set_meta m (Bindlib.unbox bu); true + | Some(bu) when Bindlib.is_closed bu -> + if !log_enabled then + log_unif (yel "%a ≔ %a") pp_meta m pp_term u; + set_meta m (Bindlib.unbox bu); true | _ -> false (** [solve cfg p] tries to solve the unification problems of [p] and From 212e1ccd2d0dfa0c8e0336d2a8713ace7ac9b28d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:43:45 +0200 Subject: [PATCH 15/66] scope: replace wildcard pattern variables by fresh named pattern variables --- src/core/scope.ml | 48 ++++++++++++++++++++++++----------------------- 1 file changed, 25 insertions(+), 23 deletions(-) diff --git a/src/core/scope.ml b/src/core/scope.ml index 4c28c3faa..e81373f3e 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -116,9 +116,6 @@ let find_qid : bool -> bool -> sig_state -> env -> qident -> tbox = let (s, hint) = find_sym ~prt ~prv true st qid in _Symb s hint -(** Map of metavariables. *) -type metamap = meta StrMap.t - (** [get_root t ss] returns the symbol at the root of term [t]. *) let get_root : p_term -> sig_state -> sym * pp_hint = fun t ss -> let rec get_root t = @@ -135,15 +132,15 @@ let get_root : p_term -> sig_state -> sym * pp_hint = fun t ss -> (** Representation of the different scoping modes. Note that the constructors hold specific information for the given mode. *) type mode = - | M_Term of metamap Stdlib.ref * expo + | M_Term of meta StrMap.t Stdlib.ref * expo (** Standard scoping mode for terms, holding a map of metavariables that can be updated with new metavariables on scoping and the exposition of the scoped term. *) | M_Patt (** Scoping mode for patterns in the rewrite tactic. *) - | M_LHS of (string * int) list * bool + | M_LHS of (string * int) list * bool * int Stdlib.ref (** Scoping mode for rewriting rule left-hand sides. The constructor carries - a map associating an index to every free variable along with a flag set + a map associating an index to every pattern variable along with a flag set to [true] if {!constructor:Terms.expo.Privat} symbols are allowed. *) | M_RHS of (string * tevar) list * bool (** Scoping mode for rewriting rule righ-hand sides. The constructor carries @@ -181,11 +178,10 @@ let get_args : p_term -> p_term * p_term list = state [ss] is used to hande module aliasing according to [find_qid]. *) let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> (* Unique pattern variable generation for wildcards in a LHS. *) - let fresh_patt_name = - let c = Stdlib.ref (-1) in - fun _ -> Stdlib.(incr c; Printf.sprintf "#%i" !c) + let fresh_patt_name k = Stdlib.(incr k; Printf.sprintf "#%i" !k) in + let fresh_patt k = + let n = fresh_patt_name k in _Patt (Some Stdlib.(!k)) n in - let fresh_patt env = _Patt None (fresh_patt_name ()) (Env.to_tbox env) in (* Toplevel scoping function, with handling of implicit arguments. *) let rec scope : env -> p_term -> tbox = fun env t -> (* Extract the spine. *) @@ -193,9 +189,9 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> (* Check that LHS pattern variables are applied to no argument. *) begin match (p_head.elt, md) with - | (P_Patt(_,_), M_LHS(_,_)) when args <> [] -> + | (P_Patt(_,_), M_LHS(_)) when args <> [] -> fatal t.pos "Pattern variables cannot be applied." - | _ -> () + | _ -> () end; (* Scope the head and obtain the implicitness of arguments. *) let h = scope_head env p_head in @@ -238,10 +234,10 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> (* Scoping function for the domain of functions or products. *) and scope_domain : env -> p_term option -> tbox = fun env a -> match (a, md) with - | (Some(a), M_LHS(_)) -> fatal a.pos "Annotation not allowed in a LHS." - | (None , M_LHS(_)) -> fresh_patt env - | (Some(a), _ ) -> scope env a - | (None , _ ) -> + | (Some(a), M_LHS(_) ) -> fatal a.pos "Annotation not allowed in a LHS." + | (None , M_LHS(_,_,k)) -> fresh_patt k (Env.to_tbox env) + | (Some(a), _ ) -> scope env a + | (None , _ ) -> (* Create a new metavariable of type [TYPE] for the missing domain. *) let vs = Env.to_tbox env in _Meta (fresh_meta (Env.to_prod env _Type) (Array.length vs)) vs @@ -274,11 +270,11 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> | (P_Type , M_LHS(_) ) -> fatal t.pos "[%a] is not allowed in a LHS." Print.pp Type | (P_Type , _ ) -> _Type - | (P_Iden(qid,_) , M_LHS(_,p) ) -> find_qid true p ss env qid + | (P_Iden(qid,_) , M_LHS(_,p,_) ) -> find_qid true p ss env qid | (P_Iden(qid,_) , M_Term(_,Privat )) -> find_qid false true ss env qid | (P_Iden(qid,_) , M_RHS(_,p) ) -> find_qid false p ss env qid | (P_Iden(qid,_) , _ ) -> find_qid false false ss env qid - | (P_Wild , M_LHS(_) ) -> fresh_patt env + | (P_Wild , M_LHS(_,_,k) ) -> fresh_patt k (Env.to_tbox env) | (P_Wild , M_Patt ) -> _Wild | (P_Wild , _ ) -> (* We create a metavariable [m] of type [tm], which itself is also a @@ -306,7 +302,7 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> _Meta m2 (Array.map (scope env) ts) | (P_Meta(_,_) , _ ) -> fatal t.pos "Metavariables are not allowed in rewriting rules." - | (P_Patt(id,ts) , M_LHS(m,_) ) -> + | (P_Patt(id,ts) , M_LHS(m,_,k) ) -> (* Check that [ts] are variables. *) let scope_var t = match unfold (Bindlib.unbox (scope env t)) with @@ -328,10 +324,11 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> begin match id with | None -> - if List.length env = Array.length vs then + let l = List.length env in + if l = Array.length vs then wrn t.pos "Pattern [%a] could be replaced by [_]." Pretty.pp_p_term t; - _Patt None (fresh_patt_name ()) (Array.map Bindlib.box_var vs) + fresh_patt k (Array.map Bindlib.box_var vs) | Some(id) -> let i = try Some(List.assoc id.elt m) with Not_found -> @@ -503,7 +500,9 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> privacy. *) let prv = is_private (fst (get_root p_lhs ss)) in (* We scope the LHS and add indexes in the environment for metavariables. *) - let lhs = Bindlib.unbox (scope (M_LHS(map, prv)) ss Env.empty p_lhs) in + let l = List.length map in + let k = Stdlib.ref (l-1) in + let lhs = Bindlib.unbox (scope (M_LHS(map,prv,k)) ss Env.empty p_lhs) in let (sym, hint, lhs) = let (h, args) = Basics.get_args lhs in match h with @@ -518,8 +517,11 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> fatal p_lhs.pos "No head symbol in LHS." in if lhs = [] then wrn p_lhs.pos "LHS head symbol with no argument."; + (* We extend [map] with the fresh pattern variables created in scoping. *) + let k = Stdlib.(!k-(l-1)) in + let fresh_patts = Array.init k (fun i -> Printf.sprintf "#%i" (l+i)) in + let names = Array.append (Array.of_list (List.map fst map)) fresh_patts in (* We scope the RHS and bind the pattern variables. *) - let names = Array.of_list (List.map fst map) in let vars = Bindlib.new_mvar te_mkfree names in let rhs = let map = Array.map2 (fun n v -> (n,v)) names vars in From 779064457f018d516405f5b35a192fab1dc3c019 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:45:39 +0200 Subject: [PATCH 16/66] fix sr by replacing LHS metas by fresh function symbols before solving RHS typing constraints --- src/core/sr.ml | 54 +++++++++++++++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 20 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index d24b763b0..32a9c468b 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -10,17 +10,12 @@ open Extra let log_subj = new_logger 's' "subj" "subject-reduction" let log_subj = log_subj.logger -(** Representation of a substitution. *) -type subst = tvar array * term array - -(** [build_meta_type k] builds the type “∀(x1:A1) ⋯ (xk:Ak), A(k+1)” where the - type “Ai = Mi[x1,⋯,x(i-1)]” is defined as the metavariable “Mi” (which has - arity “i-1”). The type of “Mi” is “∀(x1:A1) ⋯ (x(i-1):A(i-1)), TYPE”. *) +(** [build_meta_type k] builds the type “∀x1:A1,⋯,xk:Ak,A(k+1)” where the + type “Ai = Mi[x1,⋯,x(i-1)]” is defined as the metavariable “Mi” which has + arity “i-1” and type “∀(x1:A1) ⋯ (x(i-1):A(i-1)), TYPE”. *) let build_meta_type : int -> term = fun k -> assert (k >= 0); - (* We create the variables “xi”. *) - let xs = Bindlib.new_mvar mkfree (Array.init k (Printf.sprintf "x%i")) in - (* We also make a boxed version of the variables. *) + let xs = Basics.fresh_vars k in let ts = Array.map _Vari xs in (* We create the types for the “Mi” metavariables. *) let ty_m = Array.make (k+1) _Type in @@ -29,7 +24,7 @@ let build_meta_type : int -> term = fun k -> ty_m.(i) <- _Prod ty_m.(j) (Bindlib.bind_var xs.(j) ty_m.(i)) done done; - (* We create the “Ai” terms (and the “Mi” metavariables). *) + (* We create the “Ai” terms and the “Mi” metavariables. *) let fn i = let m = fresh_meta (Bindlib.unbox ty_m.(i)) i in _Meta m (Array.sub ts 0 i) @@ -99,15 +94,14 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc | Some(ty_lhs, lhs_constrs) -> if !log_enabled then begin - log_subj "LHS has type %a" pp ty_lhs; + log_subj (gre "LHS has type %a") pp ty_lhs; List.iter (log_subj " if %a" pp_constr) lhs_constrs end; (* We substitute the RHS with the corresponding metavariables. *) let fn m = - let ns = Array.init m.meta_arity (Printf.sprintf "x%i") in - let xs = Bindlib.new_mvar mkfree ns in - let e = Array.map _Vari xs in - TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m e))) + let xs = Basics.fresh_vars m.meta_arity in + let ts = Array.map _Vari xs in + TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m ts))) in let te_envs = Array.map fn metas in let subst t = Bindlib.msubst t te_envs in @@ -118,19 +112,39 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar rule.vars bt)) in MetaSet.iter fn rhs_metas; - (* Here, we should instantiate the LHS metas by fresh function symbols and - complete the constraints into a set of rewriting rules on those function - symbols. *) + (* We instantiate the LHS metas by fresh function symbols. *) + let sym n t = + { sym_name = n + ; sym_type = ref t + ; sym_path = [] + ; sym_def = ref None + ; sym_impl = [] + ; sym_rules = ref [] + ; sym_tree = ref Tree_types.empty_dtree + ; sym_prop = Defin + ; sym_expo = Public } + in + let fn m = + let n = match m.meta_name with Some n -> n | None -> assert false in + let s = _Symb (sym n !(m.meta_type)) Nothing in + let xs = Basics.fresh_vars m.meta_arity in + let t = Array.fold_right (fun x t -> _Appl t (_Vari x)) xs s in + if !(m.meta_value) = None then + m.meta_value := Some (Bindlib.unbox (Bindlib.bind_mvar xs t)) + in + Array.iter fn metas; + (* Here, we should complete the constraints into a set of rewriting rules on + those function symbols. *) (* Check that the RHS has the same type as the LHS. *) let to_solve = Infer.check [] rhs ty_lhs in if !log_enabled && to_solve <> [] then begin - log_subj "RHS has type %a" pp ty_lhs; + log_subj (gre "RHS has type %a") pp ty_lhs; List.iter (log_subj " if %a" pp_constr) to_solve end; (* Solving the constraints. To help resolution, metavariable symbols having no constraint could be replaced by fresh variables. *) - match Unif.(solve builtins false {no_problems with to_solve}) with + match Unif.(solve builtins true {no_problems with to_solve}) with | None -> fatal pos "Rule [%a] does not preserve typing." pp_rule (s,h,rule) | Some(cs) -> From b2b7d03b5a8de548d0b85302a9a4f144ee835592 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:46:46 +0200 Subject: [PATCH 17/66] details in tests --- tests/OK/273.lp | 3 ++- tests/OK/append.lp | 20 ++++---------------- 2 files changed, 6 insertions(+), 17 deletions(-) diff --git a/tests/OK/273.lp b/tests/OK/273.lp index 61fefbb53..ce4a6f535 100644 --- a/tests/OK/273.lp +++ b/tests/OK/273.lp @@ -11,8 +11,9 @@ constant symbol consC : ∀x, C x (f x) symbol k : ∀a, B a ⇒ A rule k _ (consB &b) → &b -symbol calc : ∀a b, ∀c : C (f a) (k a b), TYPE +symbol calc : ∀a b, C (f a) (k a b) ⇒ TYPE constant symbol D : ∀x, B (f (f x)) ⇒ TYPE +//set debug +siu rule calc &a (consB &b) (consC _) → D &b (consB &a) diff --git a/tests/OK/append.lp b/tests/OK/append.lp index e44c550a3..a4eff2af4 100644 --- a/tests/OK/append.lp +++ b/tests/OK/append.lp @@ -1,18 +1,10 @@ -/// Implementation of vectors -/// ========================= -/// -/// This module provides: -/// - a definition of vectors (lists of a given length), -/// - the usual **append** function for concatenation. - constant symbol A : TYPE - constant symbol Nat : TYPE - constant symbol zero : Nat constant symbol succ : Nat ⇒ Nat symbol plus : Nat ⇒ Nat ⇒ Nat + rule plus zero &m → &m rule plus (succ &n) &m → succ (plus &n &m) @@ -21,13 +13,9 @@ constant symbol nil : Vec zero constant symbol cns : ∀ (n:Nat), A ⇒ Vec n ⇒ Vec (succ n) symbol append : ∀ (n:Nat) (m:Nat), Vec n ⇒ Vec m ⇒ Vec (plus n m) + +//set debug +siu rule append _ _ nil &l2 → &l2 + rule append _ &m (cns &n &e &l1) &l2 → cns (plus &n &m) &e (append &n &m &l1 &l2) - -// FIXME add more functions. - -//theorem add_comm : ∀ (m:Nat) (n:Nat), eq Nat (add m n) (add n m) -//proof -// intro m n -//abort From 28e84a0031dc7da8e822329620518982aea57629 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:47:26 +0200 Subject: [PATCH 18/66] new test --- tests/OK/tail.lp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 tests/OK/tail.lp diff --git a/tests/OK/tail.lp b/tests/OK/tail.lp new file mode 100644 index 000000000..eb6813084 --- /dev/null +++ b/tests/OK/tail.lp @@ -0,0 +1,14 @@ +constant symbol N:TYPE +constant symbol o : N +constant symbol s : N⇒N + +constant symbol A:TYPE + +constant symbol V:N⇒TYPE +constant symbol nil:V o +constant symbol cons:A⇒∀n,V n⇒V(s n) + +symbol tail:∀n,V(s n)⇒V n + +//set debug +sui +rule tail _ (cons _ _ &v) → &v From 05996f8f9d095e33d63914f4a86e63f919491f57 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 16:50:22 +0200 Subject: [PATCH 19/66] infer: change in log message --- src/core/infer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/infer.ml b/src/core/infer.ml index 30981f63e..c83f44ee6 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -205,7 +205,7 @@ let check : ctxt -> term -> term -> unif_constrs = fun ctx t c -> if !log_enabled then begin log_infr (gre "check [%a] [%a]") pp t pp c; - List.iter (log_infr " assuming %a" pp_constr) constrs; + List.iter (log_infr " if %a" pp_constr) constrs; end; Stdlib.(constraints := []); constrs From 0b8037a6f9ec2cd42814513e7cded7efdc43aaa1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 18:20:25 +0200 Subject: [PATCH 20/66] add basics.add_metas --- src/core/basics.ml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/core/basics.ml b/src/core/basics.ml index 2cea5bd00..58ad4be23 100644 --- a/src/core/basics.ml +++ b/src/core/basics.ml @@ -182,14 +182,19 @@ let occurs : meta -> term -> bool = let fn p = if m == p then raise Found in try iter_meta false fn t; false with Found -> true -(** [get_metas b t] returns the set of all the metavariables in [t], and in - the types of metavariables recursively if [b]. *) -let get_metas : bool -> term -> MetaSet.t = fun b t -> +(** [add_metas b t ms] extends [ms] with all the metavariables of [t], and + those in the types of these metavariables recursively if [b]. *) +let add_metas : bool -> term -> MetaSet.t -> MetaSet.t = fun b t ms -> let open Stdlib in - let ms = ref MetaSet.empty in + let ms = ref ms in iter_meta b (fun m -> ms := MetaSet.add m !ms) t; !ms +(** [get_metas b t] returns the set of all the metavariables in [t], and in + the types of metavariables recursively if [b]. *) +let get_metas : bool -> term -> MetaSet.t = fun b t -> + add_metas b t MetaSet.empty + (** [has_metas b t] checks whether there are metavariables in [t], and in the types of metavariables recursively if [b] is true. *) let has_metas : bool -> term -> bool = From e7b7bc77a32a068dc09d538fc78d461e081f5150 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 18:22:44 +0200 Subject: [PATCH 21/66] sr: details --- src/core/sr.ml | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 32a9c468b..712ab8473 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -88,7 +88,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let lhs_args = List.map (fun p -> Bindlib.unbox (to_m 0 p)) rule.lhs in let lhs = Basics.add_args (Symb(s,h)) lhs_args in let metas = Array.map (function Some m -> m | None -> assert false) metas in - (* Infer the type of the LHS and the constraints. *) + (* Infer the typing constraints of the LHS. *) match Typing.infer_constr builtins [] lhs with | None -> wrn pos "Untypable LHS."; shrp | Some(ty_lhs, lhs_constrs) -> @@ -97,7 +97,8 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc log_subj (gre "LHS has type %a") pp ty_lhs; List.iter (log_subj " if %a" pp_constr) lhs_constrs end; - (* We substitute the RHS with the corresponding metavariables. *) + (* We apply the mapping pattern variable -> metavariable to the RHS and the + types of its metavariables. *) let fn m = let xs = Basics.fresh_vars m.meta_arity in let ts = Array.map _Vari xs in @@ -106,15 +107,14 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let te_envs = Array.map fn metas in let subst t = Bindlib.msubst t te_envs in let rhs = subst rule.rhs in - (* We substitute the metavariables of the RHS as well. *) let fn m = let bt = lift !(m.meta_type) in m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar rule.vars bt)) in MetaSet.iter fn rhs_metas; - (* We instantiate the LHS metas by fresh function symbols. *) + (* We instantiate the uninstantiated LHS metas by fresh function symbols. *) let sym n t = - { sym_name = n + { sym_name = "?" ^ n ; sym_type = ref t ; sym_path = [] ; sym_def = ref None @@ -142,8 +142,9 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc log_subj (gre "RHS has type %a") pp ty_lhs; List.iter (log_subj " if %a" pp_constr) to_solve end; - (* Solving the constraints. To help resolution, metavariable symbols having - no constraint could be replaced by fresh variables. *) + (* To help resolution, metavariable symbols with no constraint are + replaced by fresh variables. *) + (* Solving the typing constraints of the RHS. *) match Unif.(solve builtins true {no_problems with to_solve}) with | None -> fatal pos "Rule [%a] does not preserve typing." pp_rule (s,h,rule) @@ -161,17 +162,18 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let cs = List.filter (fun c -> not (is_constr c)) cs in if cs <> [] then begin - List.iter (fatal_msg "Cannot solve %a\n" pp_constr) cs; - fatal pos "Unable to prove SR for rule [%a]." pp_rule (s,h,rule) + List.iter (fatal_msg "\nCannot solve %a" pp_constr) cs; + fatal pos "\nUnable to prove type preservation for the rule\n%a." + pp_rule (s,h,rule) end; (* Check that there is no uninstanciated metas left. *) let lhs_metas = Basics.get_metas false lhs in - let f m = + let fn m = if not (MetaSet.mem m lhs_metas) then fatal pos "Cannot instantiate all metavariables in rule [%a]." pp_rule (s,h,rule) in - Basics.iter_meta false f rhs; + Basics.iter_meta false fn rhs; (* Return rule with metavariables instanciated. We need to replace metavariables by term_env variables, and bind them. *) let new_rhs = rule.rhs in From e285838252e545cb67e8b2f25d40c09775ce8211 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 19:43:21 +0200 Subject: [PATCH 22/66] terms: add MetaMap --- src/core/terms.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/terms.ml b/src/core/terms.ml index 7ca91d268..ab7518ac7 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -250,6 +250,7 @@ module Meta = struct end module MetaSet = Set.Make(Meta) +module MetaMap = Map.Make(Meta) (** [symb s] returns the term [Symb (s, Nothing)]. *) let symb : sym -> term = fun s -> Symb (s, Nothing) From e0d283dd18ff749898defbaf9340ce0bb7e4e9e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 3 Apr 2020 19:45:26 +0200 Subject: [PATCH 23/66] improve sr --- src/core/sr.ml | 93 ++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 68 insertions(+), 25 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 712ab8473..1cef5e97f 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -51,7 +51,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc (Bindlib.msubst rule.rhs (Array.make binder_arity TE_None)) in (* We process the LHS to replace pattern variables by metavariables. *) - let metas = Array.make binder_arity None in + let lhs_metas = Array.make binder_arity None in let rec to_m : int -> term -> tbox = fun k t -> (* [k] is the number of arguments to which [m] is applied. *) match unfold t with @@ -69,11 +69,11 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let m = fresh_meta ~name:n (build_meta_type (l+k)) l in _Meta m a | Some(i) -> - match metas.(i) with + match lhs_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); + lhs_metas.(i) <- Some(m); _Meta m a end | Type -> assert false (* Cannot appear in LHS. *) @@ -87,7 +87,9 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc in let lhs_args = List.map (fun p -> Bindlib.unbox (to_m 0 p)) rule.lhs in let lhs = Basics.add_args (Symb(s,h)) lhs_args in - let metas = Array.map (function Some m -> m | None -> assert false) metas in + let lhs_metas = + Array.map (function Some m -> m | None -> assert false) lhs_metas + in (* Infer the typing constraints of the LHS. *) match Typing.infer_constr builtins [] lhs with | None -> wrn pos "Untypable LHS."; shrp @@ -104,7 +106,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let ts = Array.map _Vari xs in TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m ts))) in - let te_envs = Array.map fn metas in + let te_envs = Array.map fn lhs_metas in let subst t = Bindlib.msubst t te_envs in let rhs = subst rule.rhs in let fn m = @@ -112,38 +114,79 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar rule.vars bt)) in MetaSet.iter fn rhs_metas; - (* We instantiate the uninstantiated LHS metas by fresh function symbols. *) - let sym n t = - { sym_name = "?" ^ n - ; sym_type = ref t - ; sym_path = [] - ; sym_def = ref None - ; sym_impl = [] - ; sym_rules = ref [] - ; sym_tree = ref Tree_types.empty_dtree - ; sym_prop = Defin - ; sym_expo = Public } + (* We compute the set of all uninstantiated metavariables of the LHS, + including in the types of LHS metavariables. *) + let all_lhs_metas = + let open MetaSet in + let add_metas m ms = + match !(m.meta_value) with + | Some _ -> + let t = Meta(m, Array.make m.meta_arity Kind) in + Basics.add_metas true t ms + | None -> add m (Basics.add_metas true !(m.meta_type) ms) + in + Array.fold_right add_metas lhs_metas empty + in + (* We instantiate these metavariables by fresh function symbols, and create + a map metavariable -> function symbol. *) + let instantiate m t = + let xs = Basics.fresh_vars m.meta_arity in + let t = Array.fold_right (fun x t -> _Appl t (_Vari x)) xs t in + m.meta_value := Some (Bindlib.unbox (Bindlib.bind_mvar xs t)) in let fn m = let n = match m.meta_name with Some n -> n | None -> assert false in - let s = _Symb (sym n !(m.meta_type)) Nothing in - let xs = Basics.fresh_vars m.meta_arity in - let t = Array.fold_right (fun x t -> _Appl t (_Vari x)) xs s in - if !(m.meta_value) = None then - m.meta_value := Some (Bindlib.unbox (Bindlib.bind_mvar xs t)) + let s = { sym_name = "?" ^ n + ; sym_type = m.meta_type + ; sym_path = [] + ; sym_def = ref None + ; sym_impl = [] + ; sym_rules = ref [] + ; sym_tree = ref Tree_types.empty_dtree + ; sym_prop = Defin + ; sym_expo = Public } + in + instantiate m (_Symb s Nothing) in - Array.iter fn metas; + MetaSet.iter fn all_lhs_metas; (* Here, we should complete the constraints into a set of rewriting rules on those function symbols. *) + (* We compute the set of metavariables in constraints. *) + let lhs_constrs_metas = + let open MetaSet in + let add_constr ms (_,l,r) = + Basics.add_metas false l (Basics.add_metas false r ms) + in + List.fold_left add_constr empty lhs_constrs + in + (* We compute the set of LHS metavariables having NO constraints, including + in their types. *) + let free_lhs_metas = + let open MetaSet in + let is_cstr m = mem m lhs_constrs_metas in + let fn m ms = + if is_cstr m || exists is_cstr (Basics.get_metas true !(m.meta_type)) + then ms + else add m ms + in + MetaSet.fold fn all_lhs_metas empty + in + (* To help resolution, metavariable symbols with no constraint are + replaced by fresh variables. *) + let fn m ctx = + let n = match m.meta_name with Some n -> n | None -> assert false in + let v = Bindlib.new_var mkfree n in + instantiate m (_Vari v); + (v, !(m.meta_type), None) :: ctx + in + let ctx = MetaSet.fold fn free_lhs_metas [] in (* Check that the RHS has the same type as the LHS. *) - let to_solve = Infer.check [] rhs ty_lhs in + let to_solve = Infer.check ctx rhs ty_lhs in if !log_enabled && to_solve <> [] then begin log_subj (gre "RHS has type %a") pp ty_lhs; List.iter (log_subj " if %a" pp_constr) to_solve end; - (* To help resolution, metavariable symbols with no constraint are - replaced by fresh variables. *) (* Solving the typing constraints of the RHS. *) match Unif.(solve builtins true {no_problems with to_solve}) with | None -> From c051cefa6054f401a1c96746d6e3c7d11e84c438 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 4 Apr 2020 19:41:24 +0200 Subject: [PATCH 24/66] change some log message --- src/core/sr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 1cef5e97f..b785075f9 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -42,7 +42,7 @@ let build_meta_type : int -> term = fun k -> let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> sym * pp_hint * rule Pos.loc = fun builtins ((s, h, { elt = rule; pos = pos }) as shrp) -> - if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, rule); + if !log_enabled then log_subj "check_rule %a" pp_rule (s, h, rule); let binder_arity = Bindlib.mbinder_arity rule.rhs in (* Compute the metavariables of the RHS, including the metavariables of their types. *) From 542660bbe9b03aae334235d5238d9a8021cc0c66 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 4 Apr 2020 19:42:01 +0200 Subject: [PATCH 25/66] unif: improvement --- src/core/unif.ml | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/core/unif.ml b/src/core/unif.ml index fd32d6b72..a80584e27 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -106,7 +106,7 @@ and solve_aux : ctxt -> term -> term -> problems -> unif_constrs = bi{x0=m0[vs],..,xi-1=mi-1[vs]}. *) let imitate_inj m vs us s h ts = if !log_enabled then - log_unif "imitate_inj [%a] [%a]" + log_unif "imitate_inj %a ≡ %a" pp (add_args (Meta(m,vs)) us) pp (add_args (symb s) ts); let exception Cannot_imitate in try @@ -264,7 +264,7 @@ and solve_aux : ctxt -> term -> term -> problems -> unif_constrs = let inverse_opt s ts v = if is_injective s then match ts with - | [t] -> begin try Some (t, inverse s v) with Not_invertible -> None end + | [t] -> (try Some (t, inverse s v) with Not_invertible -> None) | _ -> None else None in @@ -273,8 +273,7 @@ and solve_aux : ctxt -> term -> term -> problems -> unif_constrs = [t = s^{-1}(v)] when [s] is injective and [ts=[t]]. *) let solve_inj s ts v = if !log_enabled then - log_unif "solve_inj [%a] [%a]" pp (add_args (symb s) ts) pp v; - if is_constant s then error (); + log_unif "solve_inj %a ≡ %a" pp (add_args (symb s) ts) pp v; match inverse_opt s ts v with | Some (a, b) -> solve_aux ctx a b p | None -> add_to_unsolved () @@ -343,10 +342,18 @@ and solve_aux : ctxt -> term -> term -> problems -> unif_constrs = | (Meta(_,_) , _ ) | (_ , Meta(_,_) ) -> add_to_unsolved () - | (Symb(s,_) , _ ) -> solve_inj s ts1 t2 - | (_ , Symb(s,_) ) -> solve_inj s ts2 t1 + | (Symb(s,_) , _ ) when not (is_constant s) -> solve_inj s ts1 t2 + | (_ , Symb(s,_) ) when not (is_constant s) -> solve_inj s ts2 t1 - | (_ , _ ) -> error () + (* Cases of error *) + | (Type, (Kind|Prod(_)|Symb(_)|Vari(_)|Abst(_))) + | (Kind, (Type|Prod(_)|Symb(_)|Vari(_)|Abst(_))) + | (Prod(_), (Type|Kind|Vari(_)|Abst(_))) + | (Vari(_), (Type|Kind|Vari(_)|Prod(_))) + | (Abst(_), (Type|Kind|Prod(_))) + -> error () + + | (_ , _ ) -> add_to_unsolved () (** [solve builtins flag problems] attempts to solve [problems], after having sets the value of [can_instantiate] to [flag]. If there is no solution, From f798b2abb6ec1dd1913de7b029750c4ac689974d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 4 Apr 2020 19:42:44 +0200 Subject: [PATCH 26/66] handle first example of #330 --- tests/OK/330.lp | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 tests/OK/330.lp diff --git a/tests/OK/330.lp b/tests/OK/330.lp new file mode 100644 index 000000000..280e7c71a --- /dev/null +++ b/tests/OK/330.lp @@ -0,0 +1,11 @@ +constant symbol Term : TYPE +constant symbol Prop : TYPE +symbol prf : Prop ⇒ TYPE +symbol equals : Term ⇒ Term ⇒ Prop + +set flag "print_implicits" on +set debug +siu + +//type ∀ P, prf (P _) ⇒ prf (P _) + +rule prf (equals &x &y) → ∀ P, prf (P &x) ⇒ prf (P &y) From 27ceb83094c9fb0932552313b4434ced67224a6b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sun, 5 Apr 2020 10:26:02 +0200 Subject: [PATCH 27/66] fix bug in infer --- src/core/infer.ml | 32 +++----------------------------- 1 file changed, 3 insertions(+), 29 deletions(-) diff --git a/src/core/infer.ml b/src/core/infer.ml index c83f44ee6..e4cd05873 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -37,7 +37,7 @@ let make_meta_codomain : ctxt -> term -> tbinder = fun ctx a -> constraints are satisfied. [ctx] must be well-formed. This function never fails (but constraints may be unsatisfiable). *) let rec infer : ctxt -> term -> term = fun ctx t -> - if !log_enabled then log_infr "infer [%a]" pp t; + if !log_enabled then log_infr "infer %a" pp t; match unfold t with | Patt(_,_,_) -> assert false (* Forbidden case. *) | TEnv(_,_) -> assert false (* Forbidden case. *) @@ -147,34 +147,8 @@ let rec infer : ctxt -> term -> term = fun ctx t -> This avoids to build a product to destructure it just after. *) and check : ctxt -> term -> term -> unit = fun ctx t c -> - if !log_enabled then log_infr "check [%a] [%a]" pp t pp c; - match unfold t with - (* c → Prod(d,b) a ~ d ctx, x : A ⊢ t ⇐ b - ---------------------------------------------------- - ctx ⊢ Abst(a,t) ⇐ c *) - | Abst(a,t) -> - (* We ensure that [a] is of type [Type]. *) - check ctx a Type; - (* We (hopefully) evaluate [c] to a product, and get its body. *) - let b = - let c = Eval.whnf ctx c in - match c with - | Prod(d,b) -> conv ctx d a; b (* Domains must be convertible. *) - | Meta(m,ts) -> - let mxs, p, _bp1, bp2 = Env.extend_meta_type m in - conv ctx mxs p; Bindlib.msubst bp2 ts - | _ -> - let b = make_meta_codomain ctx a in - conv ctx c (Prod(a,b)); b - in - (* We type-check the body with the codomain. *) - let (x,t,ctx') = Ctxt.unbind ctx a None t in - check ctx' t (Bindlib.subst b (Vari(x))) - | t -> - (* ctx ⊢ t ⇒ a - ------------- - ctx ⊢ t ⇐ a *) - conv ctx (infer ctx t) c + if !log_enabled then log_infr "check %a : %a" pp t pp c; + conv ctx (infer ctx t) c (** [infer ctx t] returns a pair [(a,cs)] where [a] is a type for the term [t] in the context [ctx], under unification constraints [cs]. From 5a3040ca8704114cf3657561631fb24e53a72ace Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sun, 5 Apr 2020 10:26:29 +0200 Subject: [PATCH 28/66] fix second problem in #330 --- tests/OK/330b.lp | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/OK/330b.lp diff --git a/tests/OK/330b.lp b/tests/OK/330b.lp new file mode 100644 index 000000000..35ff31ff3 --- /dev/null +++ b/tests/OK/330b.lp @@ -0,0 +1,12 @@ +constant symbol Term : TYPE +constant symbol Prop : TYPE +symbol prf : Prop ⇒ TYPE +symbol prop_and : Prop ⇒ Prop ⇒ Prop +rule prf (prop_and &A &B) → ∀ C, (prf &A ⇒ prf &B ⇒ prf C) ⇒ prf C + +//set flag "print_implicits" on +//set flag "print_domains" on +//set debug +siu + +definition and_elim_1 : ∀ A B, prf (prop_and A B) ⇒ prf A +≔ λ A B h, h A (λ a _, a) From a94a34bbede288006d9cbfce03d61c898bf98e08 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sun, 5 Apr 2020 10:27:34 +0200 Subject: [PATCH 29/66] remove old comment --- src/core/infer.ml | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/src/core/infer.ml b/src/core/infer.ml index e4cd05873..3680e8eba 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -136,16 +136,6 @@ let rec infer : ctxt -> term -> term = fun ctx t -> [ctx], possibly under some constraints recorded in [constraints] using [conv]. [ctx] must be well-formed and [c] well-sorted. This function never fails (but constraints may be unsatisfiable). *) - -(* [check ctx t c] could be reduced to the default case [conv - (infer ctx t) c]. We however provide some more efficient - code when [t] is an abstraction, as witnessed by 'make holide': - - Finished in 3:56.61 at 99% with 3180096Kb of RAM - - Finished in 3:46.13 at 99% with 2724844Kb of RAM - - This avoids to build a product to destructure it just after. *) and check : ctxt -> term -> term -> unit = fun ctx t c -> if !log_enabled then log_infr "check %a : %a" pp t pp c; conv ctx (infer ctx t) c From 95057aa4b25be066235ac136a9281151f1743ba9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sun, 5 Apr 2020 10:30:55 +0200 Subject: [PATCH 30/66] sanity --- src/core/scope.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/core/scope.ml b/src/core/scope.ml index e81373f3e..c3ac4343c 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -140,8 +140,8 @@ type mode = (** Scoping mode for patterns in the rewrite tactic. *) | M_LHS of (string * int) list * bool * int Stdlib.ref (** Scoping mode for rewriting rule left-hand sides. The constructor carries - a map associating an index to every pattern variable along with a flag set - to [true] if {!constructor:Terms.expo.Privat} symbols are allowed. *) + a map associating an index to every pattern variable along with a flag + set to [true] if {!constructor:Terms.expo.Privat} symbols are allowed. *) | M_RHS of (string * tevar) list * bool (** Scoping mode for rewriting rule righ-hand sides. The constructor carries the environment for variables that will be bound in the representation @@ -234,7 +234,8 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> (* Scoping function for the domain of functions or products. *) and scope_domain : env -> p_term option -> tbox = fun env a -> match (a, md) with - | (Some(a), M_LHS(_) ) -> fatal a.pos "Annotation not allowed in a LHS." + | (Some(a), M_LHS(_) ) -> + fatal a.pos "Annotation not allowed in a LHS." | (None , M_LHS(_,_,k)) -> fresh_patt k (Env.to_tbox env) | (Some(a), _ ) -> scope env a | (None , _ ) -> From d5dd1ee530e0bece055801c66127149dafd62832 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 15:46:08 +0200 Subject: [PATCH 31/66] remove lib directory --- GNUmakefile | 2 +- lib/example/bool.lp | 57 --------------------------------------- lib/example/dune | 11 -------- lib/example/nat/binary.lp | 52 ----------------------------------- lib/example/nat/dune | 18 ------------- lib/example/nat/unary.lp | 56 -------------------------------------- 6 files changed, 1 insertion(+), 195 deletions(-) delete mode 100644 lib/example/bool.lp delete mode 100644 lib/example/dune delete mode 100644 lib/example/nat/binary.lp delete mode 100644 lib/example/nat/dune delete mode 100644 lib/example/nat/unary.lp diff --git a/GNUmakefile b/GNUmakefile index d09db2133..b0e67d15b 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -16,7 +16,7 @@ doc: #### Unit tests and sanity check ############################################# -LAMBDAPI = dune exec -- lambdapi check --lib-root lib +LAMBDAPI = dune exec -- lambdapi check OK_TESTFILES = $(sort $(wildcard tests/OK/*.dk tests/OK/*.lp)) KO_TESTFILES = $(sort $(wildcard tests/KO/*.dk tests/KO/*.lp)) diff --git a/lib/example/bool.lp b/lib/example/bool.lp deleted file mode 100644 index 546bee54c..000000000 --- a/lib/example/bool.lp +++ /dev/null @@ -1,57 +0,0 @@ -// Data type of booleans. - -constant symbol B : TYPE - -constant symbol true : B -constant symbol false : B - -// Declaration of the main boolean functions, with their notation. - -symbol bool_neg : B ⇒ B -symbol bool_and : B ⇒ B ⇒ B -symbol bool_or : B ⇒ B ⇒ B - -set infix right 18 "∧" ≔ bool_and -set infix right 16 "∨" ≔ bool_and -set prefix 20 "¬" ≔ bool_neg - -// Definition of negation. - -rule ¬ true → false -rule ¬ false → true -rule ¬ ¬ &a → &a - -// Definition of conjunction - -rule true ∧ &b → &b - and &b ∧ true → &b - and false ∧ _ → false - and _ ∧ false → false - -// Definition of disjunction. - -rule true ∨ _ → true - and _ ∨ true → true - and false ∨ &b → &b - and &b ∨ false → &b - -// Conditional. - -symbol bool_if : B ⇒ B ⇒ B ⇒ B - -rule bool_if true &x _ → &x -rule bool_if false _ &x → &x - -// More (defined) boolean functions. - -definition bool_impl a b ≔ b ∨ ¬ a -definition bool_xor a b ≔ (a ∨ b) ∧ ¬ (a ∧ b) - -set infix right 14 "⇨" ≔ bool_impl -set infix right 16 "⊕" ≔ bool_xor - -// Some tests. - -assert (x y z : B) ⊢ x ∨ y ∨ ¬ z ≡ x ∨ (y ∨ ¬ z) -assert (x y z : B) ⊢ x ∨ y ∧ z ≡ x ∨ (y ∧ z) -assert (x y z : B) ⊢ z ⇨ x ∨ y ∧ z ≡ z ⇨ (x ∨ (y ∧ z)) diff --git a/lib/example/dune b/lib/example/dune deleted file mode 100644 index 94244e49f..000000000 --- a/lib/example/dune +++ /dev/null @@ -1,11 +0,0 @@ -(rule - (target bool.lpo) - (deps bool.lp) - (action (run lambdapi check --lib-root .. --verbose 0 --gen-obj %{deps}))) - -(install - (section lib) - (files - (bool.lp as lib_root/example/bool.lp) - (bool.lpo as lib_root/example/bool.lpo))) - diff --git a/lib/example/nat/binary.lp b/lib/example/nat/binary.lp deleted file mode 100644 index 71091614d..000000000 --- a/lib/example/nat/binary.lp +++ /dev/null @@ -1,52 +0,0 @@ -require open example.bool - -// Data type of binary natural numbers. - -constant symbol N : TYPE - -constant symbol zero : N -constant symbol times2plus0 : N ⇒ N -constant symbol times2plus1 : N ⇒ N - -// Successor function. - -symbol succ : N ⇒ N - -rule succ zero → times2plus1 zero - and succ (times2plus0 &n) → times2plus1 &n - and succ (times2plus1 &n) → times2plus0 (succ &n) - -// Enabling built-in natural number literal, and example. - -set builtin "0" ≔ zero -set builtin "+1" ≔ succ - -definition forty_two ≔ 42 - -// Addition function. - -symbol add : N ⇒ N ⇒ N -set infix left 6 "+" ≔ add - -rule zero + &m → &m - and &n + zero → &n - and times2plus0 &n + times2plus0 &m → times2plus0 (&n + &m) - and times2plus0 &n + times2plus1 &m → times2plus1 (&n + &m) - and times2plus1 &n + times2plus0 &m → times2plus1 (&n + &m) - and times2plus1 &n + times2plus1 &m → times2plus0 (succ (&n + &m)) - -// Multiplication function. - -symbol mul : N ⇒ N ⇒ N -set infix left 7 "×" ≔ mul - -definition times4 : N ⇒ N ≔ λ n, times2plus0 (times2plus0 n) - -rule zero × _ → zero - and _ × zero → zero - and times2plus0 &n × times2plus0 &m → &n × times4 (&n × &m) - and times2plus0 &n × times2plus1 &m → &n × times4 (&n × &m) + times2plus0 &n - and times2plus1 &n × times2plus0 &m → &n × times4 (&n × &m) + times2plus0 &m - and times2plus1 &n × times2plus1 &m → times4 (&n × &m) + times2plus1(&n + &m) - -definition double n ≔ times2plus0 n diff --git a/lib/example/nat/dune b/lib/example/nat/dune deleted file mode 100644 index 7ccf249cf..000000000 --- a/lib/example/nat/dune +++ /dev/null @@ -1,18 +0,0 @@ -(rule - (target unary.lpo) - (deps unary.lp ../bool.lpo) - (action (run lambdapi check --lib-root ../.. --verbose 0 --gen-obj unary.lp))) - -(rule - (target binary.lpo) - (deps binary.lp ../bool.lpo) - (action (run lambdapi check --lib-root ../.. --verbose 0 --gen-obj binary.lp))) - -(install - (section lib) - (files - (unary.lp as lib_root/example/nat/unary.lp) - (binary.lp as lib_root/example/nat/binary.lp) - (unary.lpo as lib_root/example/nat/unary.lpo) - (binary.lpo as lib_root/example/nat/binary.lpo))) - diff --git a/lib/example/nat/unary.lp b/lib/example/nat/unary.lp deleted file mode 100644 index 42855c4c0..000000000 --- a/lib/example/nat/unary.lp +++ /dev/null @@ -1,56 +0,0 @@ -require open example.bool - -// Data type of natural numbers. - -constant symbol N : TYPE - -constant symbol z : N -constant symbol s : N ⇒ N - -// Enabling built-in natural number literal, and example. - -set builtin "0" ≔ z -set builtin "+1" ≔ s - -definition forty_two ≔ 42 - -// Addition function. - -symbol add : N ⇒ N ⇒ N -set infix left 6 "+" ≔ add - -rule z + &n → &n - and (s &m) + &n → s (&m + &n) - and &m + z → &m - and &m + (s &n) → s (&m + &n) - -// Multiplication function. - -symbol mul : N ⇒ N ⇒ N -set infix left 7 "×" ≔ mul - -rule z × _ → z - and (s &m) × &n → &n + &m × &n - and _ × z → z - and &m × (s &n) → &m + &m × &n - -// Doubling function. - -definition double n ≔ mul n 2 - -// Equality function. - -symbol eq_nat : N ⇒ N ⇒ B - -rule eq_nat z z → true - and eq_nat (s &m) (s &n) → eq_nat &m &n - and eq_nat z (s _) → false - and eq_nat (s _) z → false - -// Less than function. - -symbol le_nat : N ⇒ N ⇒ B - -rule le_nat z z → false - and le_nat z (s _) → true - and le_nat (s &m) (s &n) → le_nat &m &n From 105d47df4639d99b0a7e72fee37cda681a9b1bf0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 15:48:45 +0200 Subject: [PATCH 32/66] move eq from basics to rewrite --- src/core/basics.ml | 42 ------------------------------ src/core/rewrite.ml | 57 ++++++++++++++++++++++++++++++++++++----- src/core/tree.ml | 9 ++++--- src/core/why3_tactic.ml | 2 +- 4 files changed, 58 insertions(+), 52 deletions(-) diff --git a/src/core/basics.ml b/src/core/basics.ml index 58ad4be23..a20e8ee1e 100644 --- a/src/core/basics.ml +++ b/src/core/basics.ml @@ -75,48 +75,6 @@ let add_args : term -> term list -> term = fun t args -> | u::args -> add_args (Appl(t,u)) args in add_args t args -(** [eq ctx t u] tests the equality of [t] and [u] (up to α-equivalence). It - fails if [t] or [u] contain terms of the form [Patt(i,s,e)] or - [TEnv(te,env)]. In the process, subterms of the form [TRef(r)] in [t] and - [u] may be set with the corresponding value to enforce equality, and - variables appearing in [ctx] can be unfolded. In other words, [eq t u] can - be used to implement non-linear matching (see {!module:Rewrite}). When the - matching feature is used, one should make sure that [TRef] constructors do - not appear both in [t] and in [u] at the same time. Indeed, the references - are set naively, without checking occurrence. *) -let eq : ctxt -> term -> term -> bool = fun ctx a b -> a == b || - let exception Not_equal in - let rec eq l = - match l with - | [] -> () - | (a,b)::l -> - match (Ctxt.unfold ctx a, Ctxt.unfold ctx b) with - | (a , b ) when a == b -> eq l - | (Vari(x1) , Vari(x2) ) when Bindlib.eq_vars x1 x2 -> eq l - | (Type , Type ) - | (Kind , Kind ) -> eq l - | (Symb(s1,_) , Symb(s2,_) ) when s1 == s2 -> eq l - | (Prod(a1,b1), Prod(a2,b2)) - | (Abst(a1,b1), Abst(a2,b2)) -> let (_, b1, b2) = Bindlib.unbind2 b1 b2 in - eq ((a1,a2)::(b1,b2)::l) - | (LLet(a1,t1,u1), LLet(a2,t2,u2)) -> - let (_, u1, u2) = Bindlib.unbind2 u1 u2 in - eq ((a1,a2)::(t1,t2)::(u1,u2)::l) - | (Appl(t1,u1), Appl(t2,u2)) -> eq ((t1,t2)::(u1,u2)::l) - | (Meta(m1,e1), Meta(m2,e2)) when m1 == m2 -> - eq (if e1 == e2 then l else List.add_array2 e1 e2 l) - | (Wild , _ ) - | (_ , Wild ) -> eq l - | (TRef(r) , b ) -> r := Some(b); eq l - | (a , TRef(r) ) -> r := Some(a); eq l - | (Patt(_,_,_), _ ) - | (_ , Patt(_,_,_)) - | (TEnv(_,_) , _ ) - | (_ , TEnv(_,_) ) -> assert false - | (_ , _ ) -> raise Not_equal - in - try eq [(a,b)]; true with Not_equal -> false - (** [is_symb s t] tests whether [t] is of the form [Symb(s)]. *) let is_symb : sym -> term -> bool = fun s t -> match unfold t with diff --git a/src/core/rewrite.ml b/src/core/rewrite.ml index 6185992fa..e5b9dd919 100644 --- a/src/core/rewrite.ml +++ b/src/core/rewrite.ml @@ -13,6 +13,51 @@ open Print let log_rewr = new_logger 'r' "rewr" "the rewrite tactic" let log_rewr = log_rewr.logger +(** [eq ctx t u] tests the equality of [t] and [u] (up to α-equivalence). It + fails if [t] or [u] contain terms of the form [Patt(i,s,e)] or + [TEnv(te,env)]. In the process, subterms of the form [TRef(r)] in [t] and + [u] may be set with the corresponding value to enforce equality, and + variables appearing in [ctx] can be unfolded. In other words, [eq t u] can + be used to implement non-linear matching (see {!module:Rewrite}). When the + matching feature is used, one should make sure that [TRef] constructors do + not appear both in [t] and in [u] at the same time. Indeed, the references + are set naively, without checking occurrence. *) +let eq : ctxt -> term -> term -> bool = fun ctx a b -> a == b || + let exception Not_equal in + let rec eq l = + match l with + | [] -> () + | (a,b)::l -> + begin + if !log_enabled then log_rewr "eq [%a] [%a]" pp_term a pp_term b; + match (Ctxt.unfold ctx a, Ctxt.unfold ctx b) with + | (a , b ) when a == b -> eq l + | (Vari(x1) , Vari(x2) ) when Bindlib.eq_vars x1 x2 -> eq l + | (Type , Type ) + | (Kind , Kind ) -> eq l + | (Symb(s1,_) , Symb(s2,_) ) when s1 == s2 -> eq l + | (Prod(a1,b1), Prod(a2,b2)) + | (Abst(a1,b1), Abst(a2,b2)) -> let (_, b1, b2) = Bindlib.unbind2 b1 b2 in + eq ((a1,a2)::(b1,b2)::l) + | (LLet(a1,t1,u1), LLet(a2,t2,u2)) -> + let (_, u1, u2) = Bindlib.unbind2 u1 u2 in + eq ((a1,a2)::(t1,t2)::(u1,u2)::l) + | (Appl(t1,u1), Appl(t2,u2)) -> eq ((t1,t2)::(u1,u2)::l) + | (Meta(m1,e1), Meta(m2,e2)) when m1 == m2 -> + eq (if e1 == e2 then l else List.add_array2 e1 e2 l) + | (Wild , _ ) + | (_ , Wild ) -> eq l + | (TRef(r) , b ) -> r := Some(b); eq l + | (a , TRef(r) ) -> r := Some(a); eq l + | (Patt(_,_,_), _ ) + | (_ , Patt(_,_,_)) + | (TEnv(_,_) , _ ) + | (_ , TEnv(_,_) ) -> assert false + | (_ , _ ) -> raise Not_equal + end + in + try eq [(a,b)]; true with Not_equal -> false + (** Rewrite patterns as in Coq/SSReflect. See "A Small Scale Reflection Extension for the Coq system", by Georges Gonthier, Assia Mahboubi and Enrico Tassi, INRIA Research Report 6455, 2016, @@ -86,7 +131,7 @@ let check_builtin : popt -> sym StrMap.t -> string -> sym -> unit let ta = Appl (symb symb_T, Vari a) in let c = [(y, ta, None); (x, ta, None); (a, term_U, None)] in let (eq_type, _) = Ctxt.to_prod c term_Prop in - if not (Basics.eq [] eq_type !(sym.sym_type)) then + if not (eq [] eq_type !(sym.sym_type)) then fatal pos "The type of [%s] is not of the form [%a]" sym.sym_name pp eq_type end @@ -104,7 +149,7 @@ let check_builtin : popt -> sym StrMap.t -> string -> sym -> unit let c = [(x, Appl(symb symb_T, Vari a), None); (a, term_U, None)] in let t = Basics.add_args (symb symb_eq) [Vari a; Vari x; Vari x] in let (refl_type, _) = Ctxt.to_prod c (Appl (symb symb_P, t)) in - if not (Basics.eq [] refl_type !(sym.sym_type)) + if not (eq [] refl_type !(sym.sym_type)) then fatal pos "The type of [%s] is not of the form [%a]." sym.sym_name pp refl_type end @@ -141,7 +186,7 @@ let check_builtin : popt -> sym StrMap.t -> string -> sym -> unit ;(a , term_U , None)] in let (eqind_type, _) = Ctxt.to_prod c (p_of x) in - if not (Basics.eq [] eqind_type !(sym.sym_type)) + if not (eq [] eqind_type !(sym.sym_type)) then fatal pos "The type of [%s] is not of the form [%a]." sym.sym_name pp eqind_type end @@ -194,7 +239,7 @@ let break_prod : term -> term * tvar array = fun a -> let match_pattern : to_subst -> term -> term array option = fun (xs,p) t -> let ts = Array.map (fun _ -> TRef(ref None)) xs in let p = Bindlib.msubst (Bindlib.unbox (Bindlib.bind_mvar xs (lift p))) ts in - if Basics.eq [] p t then Some(Array.map unfold ts) else None + if eq [] p t then Some(Array.map unfold ts) else None (** [find_subst t (xs,p)] is given a term [t] and a pattern [p] (with “pattern variables” of [xs]), and it finds the first instance of (a term matching) @@ -227,7 +272,7 @@ let find_subst : term -> to_subst -> term array option = fun t (xs,p) -> let make_pat : term -> term -> bool = fun t p -> let time = Time.save () in let rec make_pat_aux : term -> bool = fun t -> - if Basics.eq [] t p then true else + if eq [] t p then true else begin Time.restore time; match unfold t with @@ -247,7 +292,7 @@ let make_pat : term -> term -> bool = fun t p -> let bind_match : term -> term -> tbinder = fun p t -> let x = Bindlib.new_var mkfree "X" in let rec lift_subst : term -> tbox = fun t -> - if Basics.eq [] p t then _Vari x else + if eq [] p t then _Vari x else match unfold t with | Vari(y) -> _Vari y | Type -> _Type diff --git a/src/core/tree.ml b/src/core/tree.ml index 6980aee96..4c7c180f7 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -525,9 +525,12 @@ module CM = struct let ph, pargs, lenp = get_args_len pat in let h, args, lenh = get_args_len r.c_lhs.(col) in match ph, h with - | Symb(_), Symb(_) - | Vari(_), Vari(_) -> - if lenh = lenp && Basics.eq [] ph h + | Symb(f,_), Symb(g,_) -> + if lenh = lenp && f == g + then Some({r with c_lhs = insert (Array.of_list args)}) + else None + | Vari(x), Vari(y) -> + if lenh = lenp && Bindlib.eq_vars x y then Some({r with c_lhs = insert (Array.of_list args)}) else None | _ , Patt(_) -> diff --git a/src/core/why3_tactic.ml b/src/core/why3_tactic.ml index 219dbe102..83f1e7dc6 100644 --- a/src/core/why3_tactic.ml +++ b/src/core/why3_tactic.ml @@ -88,7 +88,7 @@ let translate_term : config -> cnst_table -> term -> (tbl, Why3.Term.t_true) | (_ , _ ) -> (* If the term [p] is mapped in [tbl] then use it. *) - try (tbl, Why3.Term.ps_app (List.assoc_eq (Basics.eq []) t tbl) []) + try (tbl, Why3.Term.ps_app (List.assoc_eq (Rewrite.eq []) t tbl) []) with Not_found -> (* Otherwise generate a new constant in why3. *) let sym = Why3.Term.create_psymbol (Why3.Ident.id_fresh "P") [] in From 036b8b52c0f2ba73c75f953c01ffc78c49f52da4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 15:49:55 +0200 Subject: [PATCH 33/66] infer: use eq_modulo in conv + more log messages --- src/core/infer.ml | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/core/infer.ml b/src/core/infer.ml index 3680e8eba..4e3aac6d8 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -14,7 +14,7 @@ let constraints = Stdlib.ref [] (** Function adding a constraint. *) let conv ctx a b = - if not (Basics.eq ctx a b) then + if not (Eval.eq_modulo ctx a b) then begin if !log_enabled then log_infr (yel "add %a") pp_constr (ctx,a,b); let open Stdlib in constraints := (ctx,a,b) :: !constraints @@ -51,11 +51,19 @@ let rec infer : ctxt -> term -> term = fun ctx t -> (* --------------------------------- ctx ⊢ Vari(x) ⇒ Ctxt.find x ctx *) - | Vari(x) -> (try Ctxt.type_of x ctx with Not_found -> assert false) + | Vari(x) -> + let a = try Ctxt.type_of x ctx with Not_found -> assert false in + if !log_enabled then + log_infr (blu "%a : %a") pp_term t pp_term a; + a (* ------------------------------- ctx ⊢ Symb(s) ⇒ !(s.sym_type) *) - | Symb(s,_) -> !(s.sym_type) + | Symb(s,_) -> + let a = !(s.sym_type) in + if !log_enabled then + log_infr (blu "%a : %a") pp_term t pp_term a; + a (* ctx ⊢ a ⇐ Type ctx, x : a ⊢ b ⇒ s ----------------------------------------- @@ -128,8 +136,6 @@ let rec infer : ctxt -> term -> term = fun ctx t -> ---------------------------- ctx ⊢ Meta(m,e) ⇒ a *) | Meta(m,e) -> - if !log_enabled then - log_infr (yel "%s is of type [%a]") (meta_name m) pp !(m.meta_type); infer ctx (term_of_meta m e) (** [check ctx t c] checks that the term [t] has type [c] in context @@ -151,7 +157,7 @@ let infer : ctxt -> term -> term * unif_constrs = fun ctx t -> let constrs = Stdlib.(!constraints) in if !log_enabled then begin - log_infr (gre "infer [%a] yields [%a]") pp t pp a; + log_infr (gre "%a : %a") pp t pp a; List.iter (log_infr " if %a" pp_constr) constrs; end; Stdlib.(constraints := []); From f440308f99bb27881e871f68da9b8fe4874c962c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 15:50:53 +0200 Subject: [PATCH 34/66] scope: fix some comments --- src/core/scope.ml | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/src/core/scope.ml b/src/core/scope.ml index c3ac4343c..b959da317 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -140,8 +140,9 @@ type mode = (** Scoping mode for patterns in the rewrite tactic. *) | M_LHS of (string * int) list * bool * int Stdlib.ref (** Scoping mode for rewriting rule left-hand sides. The constructor carries - a map associating an index to every pattern variable along with a flag - set to [true] if {!constructor:Terms.expo.Privat} symbols are allowed. *) + a map associating an index to every pattern variable, a flag set to + [true] if {!constructor:Terms.expo.Privat} symbols are allowed, and an + index counter to be incremented for every implicit argument. *) | M_RHS of (string * tevar) list * bool (** Scoping mode for rewriting rule righ-hand sides. The constructor carries the environment for variables that will be bound in the representation @@ -488,14 +489,8 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> if i <> j then fatal p_lhs.pos "Arity mismatch for [%s]." m in List.iter check_in_lhs pvs_rhs; - (* Optimization to do *after* SR if really needed: - (* Get the non-linear variables not in the RHS. *) - let nl = List.filter (fun m -> not (List.mem_assoc m pvs_rhs)) nl in - (* Reserve space for non-linear LHS pattern variables. *) - let pvs = List.map (fun m -> (m, List.assoc m pvs_lhs)) nl @ pvs_rhs in*) - let pvs = pvs_lhs in - let map = List.mapi (fun i (m,_) -> (m,i)) pvs in - (* NOTE [map] maps pattern variables to their position in [pvs]. *) + let map = List.mapi (fun i (m,_) -> (m,i)) pvs_lhs in + (* NOTE [map] maps pattern variables to their position in [pvs_lhs]. *) (* NOTE pattern variables not in [map] can be considered as wildcards. *) (* Get privacy of the head of the rule, and scope the rest with this privacy. *) @@ -529,10 +524,10 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> let mode = M_RHS(Array.to_list map, is_private sym) in Bindlib.unbox (Bindlib.bind_mvar vars (scope mode ss Env.empty p_rhs)) in - (* We also store [pvs] to facilitate confluence / termination checking. *) - let pvs = Array.of_list pvs in + (* We also store [pvs_lhs] to facilitate confluence/termination checking. *) + let pvs = Array.of_list pvs_lhs and arity = List.length lhs in (* We put everything together to build the rule. *) - (sym, hint, Pos.make r.pos {lhs; rhs; arity = List.length lhs; pvs; vars}) + (sym, hint, Pos.make r.pos {lhs; rhs; arity; pvs; vars}) (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term that will correspond to selection pattern (rewrite tactic). *) From 4aa951e83777fa3932db785ea45d2c62185d9f76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 15:56:55 +0200 Subject: [PATCH 35/66] remove Solve.can_instantiate and Terms.internal --- src/core/queries.ml | 2 +- src/core/terms.ml | 11 ++++------- src/core/typing.ml | 4 ++-- src/core/unif.ml | 18 +++++++----------- 4 files changed, 14 insertions(+), 21 deletions(-) diff --git a/src/core/queries.ml b/src/core/queries.ml index 2d2eea744..3594e3cc3 100644 --- a/src/core/queries.ml +++ b/src/core/queries.ml @@ -31,7 +31,7 @@ let handle_query : sig_state -> Proof.t option -> p_query -> unit = | (Some(a), Some(b)) -> let pb = { no_problems with to_solve = [[], a, b] } in begin - match solve ss.builtins true pb with + match solve ss.builtins pb with | None -> fatal q.pos "Infered types are not convertible." | Some [] -> Eval.eq_modulo [] t u | Some cs -> diff --git a/src/core/terms.ml b/src/core/terms.ml index ab7518ac7..6e9799155 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -307,7 +307,7 @@ let fresh_meta : ?name:string -> term -> int -> meta = let counter = Stdlib.ref (-1) in let fresh_meta ?name a n = { meta_key = Stdlib.(incr counter; !counter) ; meta_name = name - ; meta_type = ref a ; meta_arity = n ; meta_value = ref None} + ; meta_type = ref a ; meta_arity = n ; meta_value = ref None } in fresh_meta (** [set_meta m v] sets the value of the metavariable [m] to [v]. Note that no @@ -315,14 +315,11 @@ let fresh_meta : ?name:string -> term -> int -> meta = let set_meta : meta -> (term, term) Bindlib.mbinder -> unit = fun m v -> m.meta_value := Some(v) -(** [internal m] returns [true] if [m] is unnamed (i.e., not user-defined). *) -let internal : meta -> bool = fun m -> m.meta_name = None - (** [meta_name m] returns a string representation of [m]. *) let meta_name : meta -> string = fun m -> - match m.meta_name with - | Some(n) -> "?" ^ n - | None -> "?" ^ string_of_int m.meta_key + "?" ^ match m.meta_name with + | Some(n) -> n + | None -> string_of_int m.meta_key (** [term_of_meta m env] constructs the application of a dummy symbol with the same type as [m], to the element of the environment [env]. The idea is to diff --git a/src/core/typing.ml b/src/core/typing.ml index 8317aea32..b921f7869 100644 --- a/src/core/typing.ml +++ b/src/core/typing.ml @@ -11,7 +11,7 @@ open Unif let check : sym StrMap.t -> ctxt -> term -> term -> bool = fun builtins ctx t a -> let to_solve = Infer.check ctx t a in - match solve builtins true {no_problems with to_solve} with + match solve builtins {no_problems with to_solve} with | None -> false | Some([]) -> true | Some(cs) -> @@ -28,7 +28,7 @@ let infer_constr fun builtins ctx t -> let (a, to_solve) = Infer.infer ctx t in Option.map (fun cs -> (a, cs)) - (solve builtins true {no_problems with to_solve}) + (solve builtins {no_problems with to_solve}) (** [infer builtins ctx t] tries to infer a type [a] for [t] in the context [ctx]. The function returns [Some(a)] in case of success, and [None] diff --git a/src/core/unif.ml b/src/core/unif.ml index a80584e27..1982b684b 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -33,15 +33,12 @@ let pp_problem oc p = let no_problems : problems = {to_solve = []; unsolved = []; recompute = false} -(** Boolean saying whether user metavariables can be set or not. *) -let can_instantiate : bool ref = ref true - (** [instantiation ctx m ts u] checks whether, in a problem [m[ts]=u], [m] can be instantiated and returns the corresponding instantiation. It does not check whether the instantiation is closed though. *) let instantiation : ctxt -> meta -> term array -> term -> tmbinder Bindlib.box option = fun ctx m ts u -> - if (!can_instantiate || internal m) && not (occurs m u) then + if not (occurs m u) then match nl_distinct_vars ctx ts with | None -> None | Some(vs) -> Some (Bindlib.bind_mvar vs (lift u)) @@ -355,11 +352,10 @@ and solve_aux : ctxt -> term -> term -> problems -> unif_constrs = | (_ , _ ) -> add_to_unsolved () -(** [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 - list [cs] is a list of unsolved convertibility constraints. *) -let solve : sym StrMap.t -> bool -> problems -> unif_constrs option = - fun _builtins b p -> - can_instantiate := b; +(** [solve builtins flag problems] attempts to solve [problems]. If there is + no solution, the value [None] is returned. Otherwise [Some(cs)] is + returned, where the list [cs] is a list of unsolved convertibility + constraints. *) +let solve : sym StrMap.t -> problems -> unif_constrs option = + fun _builtins p -> try Some (solve p) with Unsolvable -> None From f86ad7b18cc727034a142a1804f74aab4fc7cef2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 15:58:08 +0200 Subject: [PATCH 36/66] improvement in sr --- src/core/sr.ml | 102 ++++++++++++++++++++++++++++++++++--------------- 1 file changed, 72 insertions(+), 30 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index b785075f9..b2bf13d2c 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -40,9 +40,10 @@ let build_meta_type : int -> term = fun k -> (** [check_rule builtins r] checks whether rule [r] is well-typed. The [Fatal] exception is raised in case of error. *) let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc - -> sym * pp_hint * rule Pos.loc = + -> sym * pp_hint * rule Pos.loc = fun builtins ((s, h, { elt = rule; pos = pos }) as shrp) -> - if !log_enabled then log_subj "check_rule %a" pp_rule (s, h, rule); + if !log_enabled then log_subj (mag "check rule %a") pp_rule (s, h, rule); + let binder_arity = Bindlib.mbinder_arity rule.rhs in (* Compute the metavariables of the RHS, including the metavariables of their types. *) @@ -50,6 +51,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc Basics.get_metas true (Bindlib.msubst rule.rhs (Array.make binder_arity TE_None)) in + (* We process the LHS to replace pattern variables by metavariables. *) let lhs_metas = Array.make binder_arity None in let rec to_m : int -> term -> tbox = fun k t -> @@ -90,6 +92,17 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let lhs_metas = Array.map (function Some m -> m | None -> assert false) lhs_metas in + + (* Build a map LHS pattern variable -> term_env variable. *) + let map = + let map = ref StrMap.empty in + let fn i m = + map := StrMap.add (meta_name m) (rule.vars.(i), m.meta_arity) !map + in + Array.iteri fn lhs_metas; + !map + in + (* Infer the typing constraints of the LHS. *) match Typing.infer_constr builtins [] lhs with | None -> wrn pos "Untypable LHS."; shrp @@ -99,6 +112,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc log_subj (gre "LHS has type %a") pp ty_lhs; List.iter (log_subj " if %a" pp_constr) lhs_constrs end; + (* We apply the mapping pattern variable -> metavariable to the RHS and the types of its metavariables. *) let fn m = @@ -109,11 +123,13 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let te_envs = Array.map fn lhs_metas in let subst t = Bindlib.msubst t te_envs in let rhs = subst rule.rhs in + log_subj "rhs %a" pp_term rhs; let fn m = let bt = lift !(m.meta_type) in m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar rule.vars bt)) in MetaSet.iter fn rhs_metas; + (* We compute the set of all uninstantiated metavariables of the LHS, including in the types of LHS metavariables. *) let all_lhs_metas = @@ -127,16 +143,14 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc in Array.fold_right add_metas lhs_metas empty in - (* We instantiate these metavariables by fresh function symbols, and create - a map metavariable -> function symbol. *) + (* We instantiate these metavariables by fresh function symbols. *) let instantiate m t = let xs = Basics.fresh_vars m.meta_arity in - let t = Array.fold_right (fun x t -> _Appl t (_Vari x)) xs t in + let t = Array.fold_left (fun t x -> _Appl t (_Vari x)) t xs in m.meta_value := Some (Bindlib.unbox (Bindlib.bind_mvar xs t)) in let fn m = - let n = match m.meta_name with Some n -> n | None -> assert false in - let s = { sym_name = "?" ^ n + let s = { sym_name = meta_name m ; sym_type = m.meta_type ; sym_path = [] ; sym_def = ref None @@ -149,10 +163,15 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc instantiate m (_Symb s Nothing) in MetaSet.iter fn all_lhs_metas; + (* Here, we should complete the constraints into a set of rewriting rules on those function symbols. *) + (* TODO *) + + (* To help resolution, metavariable symbols with no constraint are + replaced by fresh variables. *) (* We compute the set of metavariables in constraints. *) - let lhs_constrs_metas = + (*let lhs_constrs_metas = let open MetaSet in let add_constr ms (_,l,r) = Basics.add_metas false l (Basics.add_metas false r ms) @@ -170,25 +189,26 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc else add m ms in MetaSet.fold fn all_lhs_metas empty - in - (* To help resolution, metavariable symbols with no constraint are - replaced by fresh variables. *) + in*) + (* let fn m ctx = let n = match m.meta_name with Some n -> n | None -> assert false in let v = Bindlib.new_var mkfree n in instantiate m (_Vari v); (v, !(m.meta_type), None) :: ctx in - let ctx = MetaSet.fold fn free_lhs_metas [] in - (* Check that the RHS has the same type as the LHS. *) - let to_solve = Infer.check ctx rhs ty_lhs in + let ctx = MetaSet.fold fn free_lhs_metas [] in*) + + (* Compute the constraints for the RHS to have the same type as the LHS. *) + let to_solve = Infer.check [] rhs ty_lhs in if !log_enabled && to_solve <> [] then begin log_subj (gre "RHS has type %a") pp ty_lhs; List.iter (log_subj " if %a" pp_constr) to_solve end; + (* Solving the typing constraints of the RHS. *) - match Unif.(solve builtins true {no_problems with to_solve}) with + match Unif.(solve builtins {no_problems with to_solve}) with | None -> fatal pos "Rule [%a] does not preserve typing." pp_rule (s,h,rule) | Some(cs) -> @@ -205,21 +225,43 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let cs = List.filter (fun c -> not (is_constr c)) cs in if cs <> [] then begin - List.iter (fatal_msg "\nCannot solve %a" pp_constr) cs; - fatal pos "\nUnable to prove type preservation for the rule\n%a." + List.iter (fatal_msg "Cannot solve %a\n" pp_constr) cs; + fatal pos "Unable to prove type preservation for the rule %a." pp_rule (s,h,rule) end; - (* Check that there is no uninstanciated metas left. *) - let lhs_metas = Basics.get_metas false lhs in - let fn m = - if not (MetaSet.mem m lhs_metas) then - fatal pos "Cannot instantiate all metavariables in rule [%a]." - pp_rule (s,h,rule) + + (* Replace metavariable symbols by term_env variables, and bind them. *) + let rec to_tenv t = + log_subj "to_tenv %a" pp_term t; + let t = unfold t in + let h, ts = Basics.get_args t in + let ts = List.map to_tenv ts in + match h with + | Symb(f,_) -> + if f.sym_name = "" || f.sym_name.[0] <> '?' then Basics.add_args h ts + else + begin + try + let (v,k) = StrMap.find f.sym_name map in + let (ts1,ts2) = List.cut ts k in + Basics.add_args (TEnv (TE_Vari v, Array.of_list ts1)) ts2 + with Not_found -> assert false + end + | Prod(a,b) -> Prod(to_tenv a, to_tenv_binder b) + | Abst(a,b) -> Basics.add_args (Abst(to_tenv a, to_tenv_binder b)) ts + | LLet(a,t,u) -> + Basics.add_args (LLet(to_tenv a, to_tenv t, to_tenv_binder u)) ts + | Appl(_,_) -> assert false + | Meta(_,_) -> assert false + | Patt(_) -> assert false + | Wild -> assert false + | _ -> Basics.add_args h ts + and to_tenv_binder b = + let (x,b) = Bindlib.unbind b in + Bindlib.unbox (Bindlib.bind_var x (lift (to_tenv b))) in - Basics.iter_meta false fn rhs; - (* Return rule with metavariables instanciated. We need to replace - metavariables by term_env variables, and bind them. *) - let new_rhs = rule.rhs in - (*Bindlib.unbox (Bindlib.bind_mvar rule.vars (lift rhs))*) - let new_rule = { rule with rhs = new_rhs } in - (s, h, { elt = new_rule; pos = pos }) + log_subj "rhs %a" pp_term rhs; + let rhs = to_tenv rhs in + let rhs = Bindlib.unbox (Bindlib.bind_mvar rule.vars (lift rhs)) in + let elt = { rule with rhs } in + (s, h, { elt; pos }) From f727612c2c8610d031f1296e869a5e9ece285b7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 15:59:04 +0200 Subject: [PATCH 37/66] remove warnings --- tests/OK/FO.dk | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/OK/FO.dk b/tests/OK/FO.dk index 1aebdc228..bcd3fa344 100644 --- a/tests/OK/FO.dk +++ b/tests/OK/FO.dk @@ -40,11 +40,11 @@ def imp_intro : A:Prop -> B:Prop -> (prf A -> prf B) -> prf (imp A B) (; disjunction ;) def or_intro_1 : A:Prop -> B:Prop -> prf A -> prf (or A B) := A:Prop => B:Prop => p:prf A => - P:Prop => f:(prf A -> prf P) => g:(prf B -> prf P) => f p. + P:Prop => f:(prf A -> prf P) => _:(prf B -> prf P) => f p. def or_intro_2 : A:Prop -> B:Prop -> prf B -> prf (or A B) := A:Prop => B:Prop => p:prf B => - P:Prop => f:(prf A -> prf P) => g:(prf B -> prf P) => g p. + P:Prop => _:(prf A -> prf P) => g:(prf B -> prf P) => g p. def or_elim : A:Prop -> B:Prop -> prf (or A B) -> C:Prop -> prf (imp A C) -> prf (imp B C) -> prf C := A:Prop => B:Prop => p:prf (or A B) => p. @@ -54,16 +54,16 @@ def conj_intro : A:Prop -> B:Prop -> prf A -> prf B -> prf (conj A B) := A:Prop => B:Prop => a:prf A => b:prf B => P:Prop => f:(prf A -> prf B -> prf P) => f a b. def conj_elim_1 : A:Prop -> B:Prop -> prf (conj A B) -> prf A -:= A:Prop => B:Prop => p:prf (conj A B) => p A (a:prf A => b:prf B => a). +:= A:Prop => B:Prop => p:prf (conj A B) => p A (a:prf A => _:prf B => a). def conj_elim_2 : A:Prop -> B:Prop -> prf (conj A B) -> prf B -:= A:Prop => B:Prop => p:prf (conj A B) => p B (a:prf A => b:prf B => b). +:= A:Prop => B:Prop => p:prf (conj A B) => p B (_:prf A => b:prf B => b). (; Universal quantificator ;) def forall_intro: P:(Term->Prop) -> (t:Term -> prf (P t)) -> prf (forall P) := P:(Term->Prop) => p:(t:Term -> prf (P t)) => p. -def forall_elim: P:(Term->Prop) -> t:Term -> p:prf (forall P) -> prf (P t) +def forall_elim: P:(Term->Prop) -> t:Term -> prf (forall P) -> prf (P t) := P:(Term->Prop) => t:Term => p:prf (forall P) => p t. (; Existential quantificator ;) From fccfd7c6352c52c36488595a46e0923f26891704 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 16:27:28 +0200 Subject: [PATCH 38/66] update comment --- src/core/rewrite.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/rewrite.ml b/src/core/rewrite.ml index e5b9dd919..75cad92e0 100644 --- a/src/core/rewrite.ml +++ b/src/core/rewrite.ml @@ -18,10 +18,10 @@ let log_rewr = log_rewr.logger [TEnv(te,env)]. In the process, subterms of the form [TRef(r)] in [t] and [u] may be set with the corresponding value to enforce equality, and variables appearing in [ctx] can be unfolded. In other words, [eq t u] can - be used to implement non-linear matching (see {!module:Rewrite}). When the + be used to implement non-linear matching. When the matching feature is used, one should make sure that [TRef] constructors do not appear both in [t] and in [u] at the same time. Indeed, the references - are set naively, without checking occurrence. *) + are set naively, without occurrence checking. *) let eq : ctxt -> term -> term -> bool = fun ctx a b -> a == b || let exception Not_equal in let rec eq l = From b0e1bb9fade1f9bbb64d7a193f3d7993ba11d232 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 16:49:31 +0200 Subject: [PATCH 39/66] Terms.set_meta: erase type again for saving memory usage --- src/core/terms.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/terms.ml b/src/core/terms.ml index 6e9799155..6f73525a7 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -313,7 +313,7 @@ let fresh_meta : ?name:string -> term -> int -> meta = (** [set_meta m v] sets the value of the metavariable [m] to [v]. Note that no specific check is performed, so this function may lead to cyclic terms. *) let set_meta : meta -> (term, term) Bindlib.mbinder -> unit = fun m v -> - m.meta_value := Some(v) + m.meta_type := Kind; (* to save memory *) m.meta_value := Some(v) (** [meta_name m] returns a string representation of [m]. *) let meta_name : meta -> string = fun m -> From d1e0561e6c83c59d00d024809bd09de61f89b31b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 16:51:04 +0200 Subject: [PATCH 40/66] test 330 does not pass anymore --- tests/OK/330.lp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/tests/OK/330.lp b/tests/OK/330.lp index 280e7c71a..4956a0edb 100644 --- a/tests/OK/330.lp +++ b/tests/OK/330.lp @@ -3,9 +3,7 @@ constant symbol Prop : TYPE symbol prf : Prop ⇒ TYPE symbol equals : Term ⇒ Term ⇒ Prop -set flag "print_implicits" on -set debug +siu +//set flag "print_implicits" on +//set debug +siu -//type ∀ P, prf (P _) ⇒ prf (P _) - -rule prf (equals &x &y) → ∀ P, prf (P &x) ⇒ prf (P &y) +//rule prf (equals &x &y) → ∀ P, prf (P &x) ⇒ prf (P &y) From cd798e5d49d2cfe71216e556c5302118f060cb68 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 16:56:34 +0200 Subject: [PATCH 41/66] rewrite: use eq_modulo for checking builtins --- src/core/rewrite.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/core/rewrite.ml b/src/core/rewrite.ml index 75cad92e0..4955e5781 100644 --- a/src/core/rewrite.ml +++ b/src/core/rewrite.ml @@ -131,7 +131,7 @@ let check_builtin : popt -> sym StrMap.t -> string -> sym -> unit let ta = Appl (symb symb_T, Vari a) in let c = [(y, ta, None); (x, ta, None); (a, term_U, None)] in let (eq_type, _) = Ctxt.to_prod c term_Prop in - if not (eq [] eq_type !(sym.sym_type)) then + if not (Eval.eq_modulo [] eq_type !(sym.sym_type)) then fatal pos "The type of [%s] is not of the form [%a]" sym.sym_name pp eq_type end @@ -149,7 +149,7 @@ let check_builtin : popt -> sym StrMap.t -> string -> sym -> unit let c = [(x, Appl(symb symb_T, Vari a), None); (a, term_U, None)] in let t = Basics.add_args (symb symb_eq) [Vari a; Vari x; Vari x] in let (refl_type, _) = Ctxt.to_prod c (Appl (symb symb_P, t)) in - if not (eq [] refl_type !(sym.sym_type)) + if not (Eval.eq_modulo [] refl_type !(sym.sym_type)) then fatal pos "The type of [%s] is not of the form [%a]." sym.sym_name pp refl_type end @@ -186,7 +186,7 @@ let check_builtin : popt -> sym StrMap.t -> string -> sym -> unit ;(a , term_U , None)] in let (eqind_type, _) = Ctxt.to_prod c (p_of x) in - if not (eq [] eqind_type !(sym.sym_type)) + if not (Eval.eq_modulo [] eqind_type !(sym.sym_type)) then fatal pos "The type of [%s] is not of the form [%a]." sym.sym_name pp eqind_type end From 759131aa18e5216f8ddb73f37089de286fe8bd99 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 18:10:04 +0200 Subject: [PATCH 42/66] changes in log messages --- src/core/infer.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/core/infer.ml b/src/core/infer.ml index 4e3aac6d8..f547e5891 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -135,8 +135,8 @@ let rec infer : ctxt -> term -> term = fun ctx t -> (* ctx ⊢ term_of_meta m e ⇒ a ---------------------------- ctx ⊢ Meta(m,e) ⇒ a *) - | Meta(m,e) -> - infer ctx (term_of_meta m e) + | Meta(m,ts) -> + infer ctx (term_of_meta m ts) (** [check ctx t c] checks that the term [t] has type [c] in context [ctx], possibly under some constraints recorded in [constraints] @@ -157,7 +157,7 @@ let infer : ctxt -> term -> term * unif_constrs = fun ctx t -> let constrs = Stdlib.(!constraints) in if !log_enabled then begin - log_infr (gre "%a : %a") pp t pp a; + log_infr (gre "infer %a : %a") pp t pp a; List.iter (log_infr " if %a" pp_constr) constrs; end; Stdlib.(constraints := []); @@ -174,7 +174,7 @@ let check : ctxt -> term -> term -> unif_constrs = fun ctx t c -> let constrs = Stdlib.(!constraints) in if !log_enabled then begin - log_infr (gre "check [%a] [%a]") pp t pp c; + log_infr (gre "check %a : %a") pp t pp c; List.iter (log_infr " if %a" pp_constr) constrs; end; Stdlib.(constraints := []); From 624573886b324276a3aa4c736c62de54a9e65f33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 18:10:39 +0200 Subject: [PATCH 43/66] details --- src/core/typing.ml | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/core/typing.ml b/src/core/typing.ml index b921f7869..4de0b79fc 100644 --- a/src/core/typing.ml +++ b/src/core/typing.ml @@ -15,10 +15,7 @@ let check : sym StrMap.t -> ctxt -> term -> term -> bool = | None -> false | Some([]) -> true | Some(cs) -> - let fn (c,a,b) = - fatal_msg "Cannot solve %a.\n" pp_constr (c, a, b) - in - List.iter fn cs; false + List.iter (fatal_msg "Cannot solve %a.\n" pp_constr) cs; false (** [infer_constr builtins ctx t] tries to infer a type [a], together with unification constraints [cs], for the term [t] in context [ctx]. The @@ -39,10 +36,7 @@ let infer : sym StrMap.t -> ctxt -> term -> term option = | None -> None | Some(a,[]) -> Some(a) | Some(_,cs) -> - let fn (c,a,b) = - fatal_msg "Cannot solve %a.\n" pp_constr (c, a, b) - in - List.iter fn cs; None + List.iter (fatal_msg "Cannot solve %a.\n" pp_constr) cs; None (** [sort_type builtins ctx t] checks that the type of the term [t] in context [ctx] is a sort. If that is not the case, the exception [Fatal] is @@ -50,8 +44,8 @@ let infer : sym StrMap.t -> ctxt -> term -> term option = let sort_type : sym StrMap.t -> ctxt -> term -> unit = fun builtins ctx t -> match infer builtins ctx t with - | None -> fatal None "Unable to infer a sort for [%a]." pp t + | None -> fatal None "Unable to infer a sort for %a." pp t | Some(a) -> match unfold a with | Type | Kind -> () - | a -> fatal None "[%a] has type [%a] (not a sort)." pp t pp a + | a -> fatal None "%a has type %a (not a sort)." pp t pp a From d1f39ebe72afb566375c0e055904e9a132ca1be7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 18:11:09 +0200 Subject: [PATCH 44/66] details --- tests/OK/245.lp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/OK/245.lp b/tests/OK/245.lp index 9a93eab3e..56b55afd6 100644 --- a/tests/OK/245.lp +++ b/tests/OK/245.lp @@ -4,6 +4,7 @@ injective symbol eta : Type ⇒ TYPE // function type constant symbol Ar : Type ⇒ Type ⇒ Type set infix right 6 ">" ≔ Ar + rule eta (&a > &b) → eta &a ⇒ eta &b constant symbol i : Type @@ -12,7 +13,9 @@ constant symbol o : Type injective symbol eps : eta o ⇒ TYPE constant symbol imp : eta (o > o > o) + rule eps (imp &a &b) → eps &a ⇒ eps &b + set infix right 6 "-->" ≔ imp constant symbol all : ∀ {A : Type}, eta ((A > o) > o) @@ -30,9 +33,6 @@ definition eq_refl : λ A x q H, H // symmetry of equality -//set flag "print_domains" on -//set flag "print_implicits" on -//set debug +iu definition eq_sym : ∀ {A : Type} (x y : eta A), eps (x = y --> y = x) ≔ From 91a1452f6173f560862c893c64e90049c6190d62 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 6 Apr 2020 18:13:03 +0200 Subject: [PATCH 45/66] details --- src/core/sr.ml | 39 +++++++++++++++++++++++---------------- 1 file changed, 23 insertions(+), 16 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index b2bf13d2c..1a43a65a0 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -168,16 +168,21 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc those function symbols. *) (* TODO *) + (* The following piece of code doesn't work as metavariables cannot be + instantiated by terms containing free variables. *) + (* (* To help resolution, metavariable symbols with no constraint are replaced by fresh variables. *) (* We compute the set of metavariables in constraints. *) - (*let lhs_constrs_metas = + let lhs_constrs_metas = let open MetaSet in let add_constr ms (_,l,r) = Basics.add_metas false l (Basics.add_metas false r ms) in List.fold_left add_constr empty lhs_constrs in + let pp_metas oc = MetaSet.iter (Format.fprintf oc "%a, " pp_meta) in + log_subj "lhs_constr_metas: %a" pp_metas lhs_constrs_metas; (* We compute the set of LHS metavariables having NO constraints, including in their types. *) let free_lhs_metas = @@ -189,15 +194,15 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc else add m ms in MetaSet.fold fn all_lhs_metas empty - in*) - (* + in + log_subj "free_lhs_metas: %a" pp_metas free_lhs_metas; let fn m ctx = - let n = match m.meta_name with Some n -> n | None -> assert false in - let v = Bindlib.new_var mkfree n in + let v = Bindlib.new_var mkfree (meta_name m) in instantiate m (_Vari v); (v, !(m.meta_type), None) :: ctx in - let ctx = MetaSet.fold fn free_lhs_metas [] in*) + let ctx = MetaSet.fold fn free_lhs_metas [] in + *) (* Compute the constraints for the RHS to have the same type as the LHS. *) let to_solve = Infer.check [] rhs ty_lhs in @@ -237,16 +242,8 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let h, ts = Basics.get_args t in let ts = List.map to_tenv ts in match h with - | Symb(f,_) -> - if f.sym_name = "" || f.sym_name.[0] <> '?' then Basics.add_args h ts - else - begin - try - let (v,k) = StrMap.find f.sym_name map in - let (ts1,ts2) = List.cut ts k in - Basics.add_args (TEnv (TE_Vari v, Array.of_list ts1)) ts2 - with Not_found -> assert false - end + (*| Vari(x) -> to_tenv_patt h ts (Bindlib.name_of x)*) + | Symb(f,_) -> to_tenv_patt h ts f.sym_name | Prod(a,b) -> Prod(to_tenv a, to_tenv_binder b) | Abst(a,b) -> Basics.add_args (Abst(to_tenv a, to_tenv_binder b)) ts | LLet(a,t,u) -> @@ -259,6 +256,16 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc and to_tenv_binder b = let (x,b) = Bindlib.unbind b in Bindlib.unbox (Bindlib.bind_var x (lift (to_tenv b))) + and to_tenv_patt h ts s = + if s = "" || s.[0] <> '?' then Basics.add_args h ts + else + begin + try + let (v,k) = StrMap.find s map in + let (ts1,ts2) = List.cut ts k in + Basics.add_args (TEnv (TE_Vari v, Array.of_list ts1)) ts2 + with Not_found -> assert false + end in log_subj "rhs %a" pp_term rhs; let rhs = to_tenv rhs in From f76704b08fa9cb619ecb1f1d44bc49fec39d4088 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 7 Apr 2020 07:53:06 +0200 Subject: [PATCH 46/66] why3_tactic: replace Rewrite.eq by Eval.eq_modulo --- src/core/why3_tactic.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/core/why3_tactic.ml b/src/core/why3_tactic.ml index 83f1e7dc6..9bc389614 100644 --- a/src/core/why3_tactic.ml +++ b/src/core/why3_tactic.ml @@ -88,7 +88,9 @@ let translate_term : config -> cnst_table -> term -> (tbl, Why3.Term.t_true) | (_ , _ ) -> (* If the term [p] is mapped in [tbl] then use it. *) - try (tbl, Why3.Term.ps_app (List.assoc_eq (Rewrite.eq []) t tbl) []) + try + let sym = List.assoc_eq (Eval.eq_modulo []) t tbl in + (tbl, Why3.Term.ps_app sym []) with Not_found -> (* Otherwise generate a new constant in why3. *) let sym = Why3.Term.create_psymbol (Why3.Ident.id_fresh "P") [] in From 935bff82c366a622fd11be4d1f4602fd6a2fa92b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 7 Apr 2020 08:18:16 +0200 Subject: [PATCH 47/66] Makefile: add lib root for tests --- GNUmakefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index b0e67d15b..bdadfd3cf 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -16,7 +16,8 @@ doc: #### Unit tests and sanity check ############################################# -LAMBDAPI = dune exec -- lambdapi check +LIB_ROOT = $(shell pwd) +LAMBDAPI = dune exec -- lambdapi check --lib-root $(LIB_ROOT) OK_TESTFILES = $(sort $(wildcard tests/OK/*.dk tests/OK/*.lp)) KO_TESTFILES = $(sort $(wildcard tests/KO/*.dk tests/KO/*.lp)) From abe746274548cf1720fb3b50ab23cc4f4db5622b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 7 Apr 2020 08:45:17 +0200 Subject: [PATCH 48/66] Makefile: change lib root to /tmp --- GNUmakefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/GNUmakefile b/GNUmakefile index bdadfd3cf..9329f971a 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -16,8 +16,7 @@ doc: #### Unit tests and sanity check ############################################# -LIB_ROOT = $(shell pwd) -LAMBDAPI = dune exec -- lambdapi check --lib-root $(LIB_ROOT) +LAMBDAPI = dune exec -- lambdapi check --lib-root /tmp OK_TESTFILES = $(sort $(wildcard tests/OK/*.dk tests/OK/*.lp)) KO_TESTFILES = $(sort $(wildcard tests/KO/*.dk tests/KO/*.lp)) From a188591e318b5e917a0cfb79dbbc8d27c6d2e4d0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 7 Apr 2020 09:32:21 +0200 Subject: [PATCH 49/66] sr: remove useless comments + replace ? by & in function symbol names --- src/core/sr.ml | 47 +++++++---------------------------------------- 1 file changed, 7 insertions(+), 40 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 1a43a65a0..734513758 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -94,10 +94,14 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc in (* Build a map LHS pattern variable -> term_env variable. *) + let sym_name m = "&" ^ match m.meta_name with + | Some(n) -> n + | None -> string_of_int m.meta_key + in let map = let map = ref StrMap.empty in let fn i m = - map := StrMap.add (meta_name m) (rule.vars.(i), m.meta_arity) !map + map := StrMap.add (sym_name m) (rule.vars.(i), m.meta_arity) !map in Array.iteri fn lhs_metas; !map @@ -150,7 +154,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc m.meta_value := Some (Bindlib.unbox (Bindlib.bind_mvar xs t)) in let fn m = - let s = { sym_name = meta_name m + let s = { sym_name = sym_name m ; sym_type = m.meta_type ; sym_path = [] ; sym_def = ref None @@ -168,42 +172,6 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc those function symbols. *) (* TODO *) - (* The following piece of code doesn't work as metavariables cannot be - instantiated by terms containing free variables. *) - (* - (* To help resolution, metavariable symbols with no constraint are - replaced by fresh variables. *) - (* We compute the set of metavariables in constraints. *) - let lhs_constrs_metas = - let open MetaSet in - let add_constr ms (_,l,r) = - Basics.add_metas false l (Basics.add_metas false r ms) - in - List.fold_left add_constr empty lhs_constrs - in - let pp_metas oc = MetaSet.iter (Format.fprintf oc "%a, " pp_meta) in - log_subj "lhs_constr_metas: %a" pp_metas lhs_constrs_metas; - (* We compute the set of LHS metavariables having NO constraints, including - in their types. *) - let free_lhs_metas = - let open MetaSet in - let is_cstr m = mem m lhs_constrs_metas in - let fn m ms = - if is_cstr m || exists is_cstr (Basics.get_metas true !(m.meta_type)) - then ms - else add m ms - in - MetaSet.fold fn all_lhs_metas empty - in - log_subj "free_lhs_metas: %a" pp_metas free_lhs_metas; - let fn m ctx = - let v = Bindlib.new_var mkfree (meta_name m) in - instantiate m (_Vari v); - (v, !(m.meta_type), None) :: ctx - in - let ctx = MetaSet.fold fn free_lhs_metas [] in - *) - (* Compute the constraints for the RHS to have the same type as the LHS. *) let to_solve = Infer.check [] rhs ty_lhs in if !log_enabled && to_solve <> [] then @@ -242,7 +210,6 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let h, ts = Basics.get_args t in let ts = List.map to_tenv ts in match h with - (*| Vari(x) -> to_tenv_patt h ts (Bindlib.name_of x)*) | Symb(f,_) -> to_tenv_patt h ts f.sym_name | Prod(a,b) -> Prod(to_tenv a, to_tenv_binder b) | Abst(a,b) -> Basics.add_args (Abst(to_tenv a, to_tenv_binder b)) ts @@ -257,7 +224,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc let (x,b) = Bindlib.unbind b in Bindlib.unbox (Bindlib.bind_var x (lift (to_tenv b))) and to_tenv_patt h ts s = - if s = "" || s.[0] <> '?' then Basics.add_args h ts + if s = "" || s.[0] <> '&' then Basics.add_args h ts else begin try From ee234b981e13cf1c6a7b5bbdb93427391a8fed2a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 7 Apr 2020 16:09:27 +0200 Subject: [PATCH 50/66] unif: improve nl_distinct_vars and instantiation to take into account symbols replacing pattern variables in SR this allows to handle 330.lp move VarSet and VarMap from basics to terms move nl_distinct_vars from basics to unif --- src/core/basics.ml | 33 ---------------------- src/core/terms.ml | 27 ++++++++++++------ src/core/unif.ml | 68 ++++++++++++++++++++++++++++++++++++++++++++-- tests/OK/330.lp | 2 +- 4 files changed, 85 insertions(+), 45 deletions(-) diff --git a/src/core/basics.ml b/src/core/basics.ml index a20e8ee1e..da6df21a0 100644 --- a/src/core/basics.ml +++ b/src/core/basics.ml @@ -8,16 +8,6 @@ open Terms let fresh_vars : int -> tvar array = fun n -> Bindlib.new_mvar mkfree (Array.init n (Printf.sprintf "x%i")) -(** Sets and maps of variables. *) -module Var = - struct - type t = term Bindlib.var - let compare = Bindlib.compare_vars - end - -module VarSet = Set.Make(Var) -module VarMap = Map.Make(Var) - (** [to_tvar t] returns [x] if [t] is of the form [Vari x] and fails otherwise. *) let to_tvar : term -> tvar = fun t -> @@ -176,29 +166,6 @@ let distinct_vars : ctxt -> term array -> tvar array option = fun ctx ts -> in try Some (Array.map to_var ts) with Not_unique_var -> None -(** [nl_distinct_vars ctx ts] checks that [ts] is made of variables [vs] only - and returns some copy of [vs] where variables occurring more than once are - replaced by fresh variables. Variables defined in [ctx] are unfolded. It - returns [None] otherwise. *) -let nl_distinct_vars : ctxt -> term array -> tvar array option = fun ctx ts -> - let exception Not_a_var in - let open Stdlib in - let vars = ref VarSet.empty - and nl_vars = ref VarSet.empty in - let to_var t = - match Ctxt.unfold ctx t with - | Vari(x) -> - if VarSet.mem x !vars then nl_vars := VarSet.add x !nl_vars else - vars := VarSet.add x !vars; - x - | _ -> raise Not_a_var - in - let replace_nl_var x = - if VarSet.mem x !nl_vars then Bindlib.new_var mkfree "_" else x - in - try Some (Array.map replace_nl_var (Array.map to_var ts)) - with Not_a_var -> None - (** {3 Conversion of a rule into a "pair" of terms} *) (** [terms_of_rule r] converts the RHS (right hand side) of the rewriting rule diff --git a/src/core/terms.ml b/src/core/terms.ml index 6f73525a7..074d925f0 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -244,14 +244,6 @@ type term = ; meta_value : (term, term) Bindlib.mbinder option ref (** Definition of the metavariable, if known. *) } -module Meta = struct - type t = meta - let compare m1 m2 = m1.meta_key - m2.meta_key -end - -module MetaSet = Set.Make(Meta) -module MetaMap = Map.Make(Meta) - (** [symb s] returns the term [Symb (s, Nothing)]. *) let symb : sym -> term = fun s -> Symb (s, Nothing) @@ -456,3 +448,22 @@ let rec lift : term -> tbox = fun t -> the names of bound variables updated. This is useful to avoid any form of "visual capture" while printing terms. *) let cleanup : term -> term = fun t -> Bindlib.unbox (lift t) + +(** Sets and maps of metavariables. *) +module Meta = struct + type t = meta + let compare m1 m2 = m1.meta_key - m2.meta_key +end + +module MetaSet = Set.Make(Meta) +module MetaMap = Map.Make(Meta) + +(** Sets and maps of variables. *) +module Var = + struct + type t = term Bindlib.var + let compare = Bindlib.compare_vars + end + +module VarSet = Set.Make(Var) +module VarMap = Map.Make(Var) diff --git a/src/core/unif.ml b/src/core/unif.ml index 1982b684b..e4c516921 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -33,15 +33,77 @@ let pp_problem oc p = let no_problems : problems = {to_solve = []; unsolved = []; recompute = false} +(** [nl_distinct_vars ctx ts] checks that [ts] is made of variables [vs] only + and returns some copy of [vs] where variables occurring more than once are + replaced by fresh variables. Variables defined in [ctx] are unfolded. It + returns [None] otherwise. *) +let nl_distinct_vars + : ctxt -> term array -> (tvar array * tvar StrMap.t) option + = fun ctx ts -> + let exception Not_a_var in + let open Stdlib in + let vars = ref VarSet.empty + and nl_vars = ref VarSet.empty + and patt_vars = ref StrMap.empty in + let rec to_var t = + match Ctxt.unfold ctx t with + | Vari(v) -> + if VarSet.mem v !vars then nl_vars := VarSet.add v !nl_vars + else vars := VarSet.add v !vars; + v + | Symb(f,_) when f.sym_name <> "" && f.sym_name.[0] = '&' -> + (* Symbols replacing pattern variables are considered as variables. *) + let v = + try StrMap.find f.sym_name !patt_vars + with Not_found -> + let v = Bindlib.new_var mkfree f.sym_name in + patt_vars := StrMap.add f.sym_name v !patt_vars; + v + in to_var (Vari v) + | _ -> raise Not_a_var + in + let replace_nl_var v = + if VarSet.mem v !nl_vars + then Bindlib.new_var mkfree (Bindlib.name_of v) + else v + in + try + let vs = Array.map to_var ts in + let vs = Array.map replace_nl_var vs in + let fn n v m = if VarSet.mem v !nl_vars then m else StrMap.add n v m in + let map = StrMap.fold fn !patt_vars StrMap.empty in + Some (vs, map) + with Not_a_var -> None + +(** [sym_to_var m t] replaces in [t] every symbol [f] by a variable according + to [m]. *) +let sym_to_var : tvar StrMap.t -> term -> term = fun m -> + let rec to_var t = + match unfold t with + | Symb(f,_) -> (try Vari (StrMap.find f.sym_name m) with Not_found -> t) + | Prod(a,b) -> Prod (to_var a, to_var_binder b) + | Abst(a,b) -> Abst (to_var a, to_var_binder b) + | LLet(a,t,u) -> LLet (to_var a, to_var t, to_var_binder u) + | Appl(a,b) -> Appl(to_var a, to_var b) + | Meta(m,ts) -> Meta(m, Array.map to_var ts) + | Patt(_) -> assert false + | TEnv(_) -> assert false + | TRef(_) -> assert false + | _ -> t + and to_var_binder b = + let (x,b) = Bindlib.unbind b in + Bindlib.unbox (Bindlib.bind_var x (lift (to_var b))) + in to_var + (** [instantiation ctx m ts u] checks whether, in a problem [m[ts]=u], [m] can be instantiated and returns the corresponding instantiation. It does not check whether the instantiation is closed though. *) let instantiation : ctxt -> meta -> term array -> term -> tmbinder Bindlib.box option = fun ctx m ts u -> if not (occurs m u) then - match nl_distinct_vars ctx ts with - | None -> None - | Some(vs) -> Some (Bindlib.bind_mvar vs (lift u)) + match nl_distinct_vars ctx ts with (* Theoretical justification ? *) + | None -> None + | Some(vs,m) -> Some (Bindlib.bind_mvar vs (lift (sym_to_var m u))) else None (** [instantiate ctx m ts u] check whether, in a problem [m[ts]=u], [m] can be diff --git a/tests/OK/330.lp b/tests/OK/330.lp index 4956a0edb..0e2d05465 100644 --- a/tests/OK/330.lp +++ b/tests/OK/330.lp @@ -6,4 +6,4 @@ symbol equals : Term ⇒ Term ⇒ Prop //set flag "print_implicits" on //set debug +siu -//rule prf (equals &x &y) → ∀ P, prf (P &x) ⇒ prf (P &y) +rule prf (equals &x &y) → ∀ P, prf (P &x) ⇒ prf (P &y) From 9c9ce7c2c03b73430381e32af111042d266021ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 7 Apr 2020 16:18:18 +0200 Subject: [PATCH 51/66] Unif.instantiation optim: do not apply sym_to_var if m is empty --- src/core/unif.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/core/unif.ml b/src/core/unif.ml index e4c516921..54e0db76c 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -70,6 +70,7 @@ let nl_distinct_vars try let vs = Array.map to_var ts in let vs = Array.map replace_nl_var vs in + (* We remove non-linear variables from [!patt_vars] as well. *) let fn n v m = if VarSet.mem v !nl_vars then m else StrMap.add n v m in let map = StrMap.fold fn !patt_vars StrMap.empty in Some (vs, map) @@ -103,7 +104,9 @@ let instantiation : ctxt -> meta -> term array -> term -> if not (occurs m u) then match nl_distinct_vars ctx ts with (* Theoretical justification ? *) | None -> None - | Some(vs,m) -> Some (Bindlib.bind_mvar vs (lift (sym_to_var m u))) + | Some(vs,m) -> + let u = if StrMap.is_empty m then u else sym_to_var m u in + Some (Bindlib.bind_mvar vs (lift u)) else None (** [instantiate ctx m ts u] check whether, in a problem [m[ts]=u], [m] can be From f1a94f17c9053a28b012f48ae53fc3061e409824 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Apr 2020 09:29:42 +0200 Subject: [PATCH 52/66] change log message --- src/core/eval.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/eval.ml b/src/core/eval.ml index 084e658a7..1ad652202 100644 --- a/src/core/eval.ml +++ b/src/core/eval.ml @@ -49,7 +49,7 @@ type stack = term list (** [whnf_beta t] computes a weak head beta normal form of the term [t]. *) let rec whnf_beta : term -> term = fun t -> - if !log_enabled then log_eval "evaluating [%a]" pp t; + if !log_enabled then log_eval "evaluating %a" pp t; let s = Stdlib.(!steps) in let (u, stk) = whnf_beta_stk t [] in if Stdlib.(!steps) <> s then add_args u stk else unfold t From 6b532da2b37ff3ec2753f6794acc3fa7d9223d25 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Apr 2020 09:44:30 +0200 Subject: [PATCH 53/66] fix remarks by Gabriel --- src/core/infer.ml | 2 +- src/core/scope.ml | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/core/infer.ml b/src/core/infer.ml index f547e5891..e1e9c7126 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -37,7 +37,7 @@ let make_meta_codomain : ctxt -> term -> tbinder = fun ctx a -> constraints are satisfied. [ctx] must be well-formed. This function never fails (but constraints may be unsatisfiable). *) let rec infer : ctxt -> term -> term = fun ctx t -> - if !log_enabled then log_infr "infer %a" pp t; + if !log_enabled then log_infr "infer %a%a" pp_ctxt ctx pp t; match unfold t with | Patt(_,_,_) -> assert false (* Forbidden case. *) | TEnv(_,_) -> assert false (* Forbidden case. *) diff --git a/src/core/scope.ml b/src/core/scope.ml index b457c5daa..47281fc70 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -326,8 +326,7 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> begin match id with | None -> - let l = List.length env in - if l = Array.length vs then + if List.length env = Array.length vs then wrn t.pos "Pattern [%a] could be replaced by [_]." Pretty.pp_p_term t; fresh_patt k (Array.map Bindlib.box_var vs) @@ -477,7 +476,7 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> let (p_lhs, p_rhs) = r.elt in (* Compute the set of pattern variables on both sides. *) let (pvs_lhs, _nl) = patt_vars p_lhs in - let (pvs_rhs, _ ) = patt_vars p_rhs in + let (pvs_rhs, _nl) = patt_vars p_rhs in (* NOTE to reject non-left-linear rules, we can check [nl = []] here. *) (* Check that the pattern variables of the RHS exist in the LHS and have the same arities. *) From f6a34057e8f60c92f0952e26e9c38cbf7a0bc928 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Apr 2020 11:54:32 +0200 Subject: [PATCH 54/66] comments by Rodolphe --- src/core/sr.ml | 26 ++++++++++++-------------- tests/OK/273.lp | 1 - tests/OK/330b.lp | 4 ---- tests/OK/append.lp | 5 +---- 4 files changed, 13 insertions(+), 23 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 734513758..4c7232655 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -100,11 +100,8 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc in let map = let map = ref StrMap.empty in - let fn i m = - map := StrMap.add (sym_name m) (rule.vars.(i), m.meta_arity) !map - in - Array.iteri fn lhs_metas; - !map + let fn x m = map := StrMap.add (sym_name m) (x, m.meta_arity) !map in + Array.iter2 fn rule.vars lhs_metas; !map in (* Infer the typing constraints of the LHS. *) @@ -154,15 +151,16 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc m.meta_value := Some (Bindlib.unbox (Bindlib.bind_mvar xs t)) in let fn m = - let s = { sym_name = sym_name m - ; sym_type = m.meta_type - ; sym_path = [] - ; sym_def = ref None - ; sym_impl = [] - ; sym_rules = ref [] - ; sym_tree = ref Tree_types.empty_dtree - ; sym_prop = Defin - ; sym_expo = Public } + let s = + { sym_name = sym_name m + ; sym_type = m.meta_type + ; sym_path = [] + ; sym_def = ref None + ; sym_impl = [] + ; sym_rules = ref [] + ; sym_tree = ref Tree_types.empty_dtree + ; sym_prop = Defin + ; sym_expo = Public } in instantiate m (_Symb s Nothing) in diff --git a/tests/OK/273.lp b/tests/OK/273.lp index ce4a6f535..c44d6786a 100644 --- a/tests/OK/273.lp +++ b/tests/OK/273.lp @@ -15,5 +15,4 @@ symbol calc : ∀a b, C (f a) (k a b) ⇒ TYPE constant symbol D : ∀x, B (f (f x)) ⇒ TYPE -//set debug +siu rule calc &a (consB &b) (consC _) → D &b (consB &a) diff --git a/tests/OK/330b.lp b/tests/OK/330b.lp index 35ff31ff3..a45bee83f 100644 --- a/tests/OK/330b.lp +++ b/tests/OK/330b.lp @@ -4,9 +4,5 @@ symbol prf : Prop ⇒ TYPE symbol prop_and : Prop ⇒ Prop ⇒ Prop rule prf (prop_and &A &B) → ∀ C, (prf &A ⇒ prf &B ⇒ prf C) ⇒ prf C -//set flag "print_implicits" on -//set flag "print_domains" on -//set debug +siu - definition and_elim_1 : ∀ A B, prf (prop_and A B) ⇒ prf A ≔ λ A B h, h A (λ a _, a) diff --git a/tests/OK/append.lp b/tests/OK/append.lp index a4eff2af4..3c6536d75 100644 --- a/tests/OK/append.lp +++ b/tests/OK/append.lp @@ -1,10 +1,10 @@ constant symbol A : TYPE + constant symbol Nat : TYPE constant symbol zero : Nat constant symbol succ : Nat ⇒ Nat symbol plus : Nat ⇒ Nat ⇒ Nat - rule plus zero &m → &m rule plus (succ &n) &m → succ (plus &n &m) @@ -13,9 +13,6 @@ constant symbol nil : Vec zero constant symbol cns : ∀ (n:Nat), A ⇒ Vec n ⇒ Vec (succ n) symbol append : ∀ (n:Nat) (m:Nat), Vec n ⇒ Vec m ⇒ Vec (plus n m) - -//set debug +siu rule append _ _ nil &l2 → &l2 - rule append _ &m (cns &n &e &l1) &l2 → cns (plus &n &m) &e (append &n &m &l1 &l2) From 057d6a07136940689c2d0adf8b55f0d01d318c6a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Apr 2020 13:02:56 +0200 Subject: [PATCH 55/66] comment by Gabriel --- src/core/scope.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/scope.ml b/src/core/scope.ml index 47281fc70..7ce38d44e 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -476,8 +476,8 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> let (p_lhs, p_rhs) = r.elt in (* Compute the set of pattern variables on both sides. *) let (pvs_lhs, _nl) = patt_vars p_lhs in - let (pvs_rhs, _nl) = patt_vars p_rhs in (* NOTE to reject non-left-linear rules, we can check [nl = []] here. *) + let (pvs_rhs, _) = patt_vars p_rhs in (* Check that the pattern variables of the RHS exist in the LHS and have the same arities. *) let check_in_lhs (m,i) = From 2d7742b49ed22ce247d0bfa938d56b376a14897b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Apr 2020 13:54:46 +0200 Subject: [PATCH 56/66] put back lib directory --- GNUmakefile | 2 +- lib/example/bool.lp | 57 +++++++++++++++++++++++++++++++++++++++ lib/example/dune | 11 ++++++++ lib/example/nat/binary.lp | 52 +++++++++++++++++++++++++++++++++++ lib/example/nat/dune | 18 +++++++++++++ lib/example/nat/unary.lp | 56 ++++++++++++++++++++++++++++++++++++++ 6 files changed, 195 insertions(+), 1 deletion(-) create mode 100644 lib/example/bool.lp create mode 100644 lib/example/dune create mode 100644 lib/example/nat/binary.lp create mode 100644 lib/example/nat/dune create mode 100644 lib/example/nat/unary.lp diff --git a/GNUmakefile b/GNUmakefile index 1880def04..18f62ca73 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -15,7 +15,7 @@ doc: #### Unit tests and sanity check ############################################# -LAMBDAPI = dune exec -- lambdapi check --lib-root /tmp +LAMBDAPI = dune exec -- lambdapi check --lib-root lib OK_TESTFILES = $(sort $(wildcard tests/OK/*.dk tests/OK/*.lp)) KO_TESTFILES = $(sort $(wildcard tests/KO/*.dk tests/KO/*.lp)) diff --git a/lib/example/bool.lp b/lib/example/bool.lp new file mode 100644 index 000000000..546bee54c --- /dev/null +++ b/lib/example/bool.lp @@ -0,0 +1,57 @@ +// Data type of booleans. + +constant symbol B : TYPE + +constant symbol true : B +constant symbol false : B + +// Declaration of the main boolean functions, with their notation. + +symbol bool_neg : B ⇒ B +symbol bool_and : B ⇒ B ⇒ B +symbol bool_or : B ⇒ B ⇒ B + +set infix right 18 "∧" ≔ bool_and +set infix right 16 "∨" ≔ bool_and +set prefix 20 "¬" ≔ bool_neg + +// Definition of negation. + +rule ¬ true → false +rule ¬ false → true +rule ¬ ¬ &a → &a + +// Definition of conjunction + +rule true ∧ &b → &b + and &b ∧ true → &b + and false ∧ _ → false + and _ ∧ false → false + +// Definition of disjunction. + +rule true ∨ _ → true + and _ ∨ true → true + and false ∨ &b → &b + and &b ∨ false → &b + +// Conditional. + +symbol bool_if : B ⇒ B ⇒ B ⇒ B + +rule bool_if true &x _ → &x +rule bool_if false _ &x → &x + +// More (defined) boolean functions. + +definition bool_impl a b ≔ b ∨ ¬ a +definition bool_xor a b ≔ (a ∨ b) ∧ ¬ (a ∧ b) + +set infix right 14 "⇨" ≔ bool_impl +set infix right 16 "⊕" ≔ bool_xor + +// Some tests. + +assert (x y z : B) ⊢ x ∨ y ∨ ¬ z ≡ x ∨ (y ∨ ¬ z) +assert (x y z : B) ⊢ x ∨ y ∧ z ≡ x ∨ (y ∧ z) +assert (x y z : B) ⊢ z ⇨ x ∨ y ∧ z ≡ z ⇨ (x ∨ (y ∧ z)) diff --git a/lib/example/dune b/lib/example/dune new file mode 100644 index 000000000..94244e49f --- /dev/null +++ b/lib/example/dune @@ -0,0 +1,11 @@ +(rule + (target bool.lpo) + (deps bool.lp) + (action (run lambdapi check --lib-root .. --verbose 0 --gen-obj %{deps}))) + +(install + (section lib) + (files + (bool.lp as lib_root/example/bool.lp) + (bool.lpo as lib_root/example/bool.lpo))) + diff --git a/lib/example/nat/binary.lp b/lib/example/nat/binary.lp new file mode 100644 index 000000000..71091614d --- /dev/null +++ b/lib/example/nat/binary.lp @@ -0,0 +1,52 @@ +require open example.bool + +// Data type of binary natural numbers. + +constant symbol N : TYPE + +constant symbol zero : N +constant symbol times2plus0 : N ⇒ N +constant symbol times2plus1 : N ⇒ N + +// Successor function. + +symbol succ : N ⇒ N + +rule succ zero → times2plus1 zero + and succ (times2plus0 &n) → times2plus1 &n + and succ (times2plus1 &n) → times2plus0 (succ &n) + +// Enabling built-in natural number literal, and example. + +set builtin "0" ≔ zero +set builtin "+1" ≔ succ + +definition forty_two ≔ 42 + +// Addition function. + +symbol add : N ⇒ N ⇒ N +set infix left 6 "+" ≔ add + +rule zero + &m → &m + and &n + zero → &n + and times2plus0 &n + times2plus0 &m → times2plus0 (&n + &m) + and times2plus0 &n + times2plus1 &m → times2plus1 (&n + &m) + and times2plus1 &n + times2plus0 &m → times2plus1 (&n + &m) + and times2plus1 &n + times2plus1 &m → times2plus0 (succ (&n + &m)) + +// Multiplication function. + +symbol mul : N ⇒ N ⇒ N +set infix left 7 "×" ≔ mul + +definition times4 : N ⇒ N ≔ λ n, times2plus0 (times2plus0 n) + +rule zero × _ → zero + and _ × zero → zero + and times2plus0 &n × times2plus0 &m → &n × times4 (&n × &m) + and times2plus0 &n × times2plus1 &m → &n × times4 (&n × &m) + times2plus0 &n + and times2plus1 &n × times2plus0 &m → &n × times4 (&n × &m) + times2plus0 &m + and times2plus1 &n × times2plus1 &m → times4 (&n × &m) + times2plus1(&n + &m) + +definition double n ≔ times2plus0 n diff --git a/lib/example/nat/dune b/lib/example/nat/dune new file mode 100644 index 000000000..7ccf249cf --- /dev/null +++ b/lib/example/nat/dune @@ -0,0 +1,18 @@ +(rule + (target unary.lpo) + (deps unary.lp ../bool.lpo) + (action (run lambdapi check --lib-root ../.. --verbose 0 --gen-obj unary.lp))) + +(rule + (target binary.lpo) + (deps binary.lp ../bool.lpo) + (action (run lambdapi check --lib-root ../.. --verbose 0 --gen-obj binary.lp))) + +(install + (section lib) + (files + (unary.lp as lib_root/example/nat/unary.lp) + (binary.lp as lib_root/example/nat/binary.lp) + (unary.lpo as lib_root/example/nat/unary.lpo) + (binary.lpo as lib_root/example/nat/binary.lpo))) + diff --git a/lib/example/nat/unary.lp b/lib/example/nat/unary.lp new file mode 100644 index 000000000..42855c4c0 --- /dev/null +++ b/lib/example/nat/unary.lp @@ -0,0 +1,56 @@ +require open example.bool + +// Data type of natural numbers. + +constant symbol N : TYPE + +constant symbol z : N +constant symbol s : N ⇒ N + +// Enabling built-in natural number literal, and example. + +set builtin "0" ≔ z +set builtin "+1" ≔ s + +definition forty_two ≔ 42 + +// Addition function. + +symbol add : N ⇒ N ⇒ N +set infix left 6 "+" ≔ add + +rule z + &n → &n + and (s &m) + &n → s (&m + &n) + and &m + z → &m + and &m + (s &n) → s (&m + &n) + +// Multiplication function. + +symbol mul : N ⇒ N ⇒ N +set infix left 7 "×" ≔ mul + +rule z × _ → z + and (s &m) × &n → &n + &m × &n + and _ × z → z + and &m × (s &n) → &m + &m × &n + +// Doubling function. + +definition double n ≔ mul n 2 + +// Equality function. + +symbol eq_nat : N ⇒ N ⇒ B + +rule eq_nat z z → true + and eq_nat (s &m) (s &n) → eq_nat &m &n + and eq_nat z (s _) → false + and eq_nat (s _) z → false + +// Less than function. + +symbol le_nat : N ⇒ N ⇒ B + +rule le_nat z z → false + and le_nat z (s _) → true + and le_nat (s &m) (s &n) → le_nat &m &n From 8277830d01cd5f579d7314eca40f2e7d033760d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Apr 2020 13:56:24 +0200 Subject: [PATCH 57/66] remark by Rodolphe --- src/core/sr.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 4c7232655..19e38d585 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -94,9 +94,12 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc in (* Build a map LHS pattern variable -> term_env variable. *) - let sym_name m = "&" ^ match m.meta_name with - | Some(n) -> n - | None -> string_of_int m.meta_key + let sym_name m = + let name = + match m.meta_name with + | Some(n) -> n + | None -> string_of_int m.meta_key + in "&" ^ name in let map = let map = ref StrMap.empty in From 17c2d41bb782c94c0be5aa37df94095b5f480a4b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Apr 2020 14:04:59 +0200 Subject: [PATCH 58/66] add tests/OK/328.lp --- tests/OK/328.lp | 50 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 tests/OK/328.lp diff --git a/tests/OK/328.lp b/tests/OK/328.lp new file mode 100644 index 000000000..03a33b97a --- /dev/null +++ b/tests/OK/328.lp @@ -0,0 +1,50 @@ +//set flag "print_implicits" on +//set verbose 3 + +// Type of set codes + +constant symbol Set : TYPE + +// Interpretation of set codes in TYPE + +set declared "τ" + +injective symbol τ : Set ⇒ TYPE + +// Type of natural numbers + +constant symbol nat : Set + +definition N ≔ τ nat + +constant symbol zero : N +constant symbol succ : N ⇒ N + +// Type of polymorphic lists + +constant symbol list : Set ⇒ Set + +definition L a ≔ τ (list a) + +set declared "□" + +constant symbol □ {a} : L a +constant symbol cons {a} : τa ⇒ L a ⇒ L a + +set infix 4 "⸬" ≔ cons + +// Length of a list + +symbol length {a} : L a ⇒ N + +rule length □ → zero +and length (_ ⸬ &l) → succ (length &l) + +// Concatenation of two lists + +symbol concat {a} : L a ⇒ L a ⇒ L a + +set infix right 5 "⋅" ≔ concat + +rule □ ⋅ &m → &m +and (&x ⸬ &l) ⋅ &m → &x ⸬ (&l ⋅ &m) From 264dd666e82a5d64a4993a2508dd780998ca3fea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Apr 2020 14:22:25 +0200 Subject: [PATCH 59/66] sr: simplification of to_m (type extension is taken care by unification now) --- src/core/sr.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 19e38d585..bad7a91b6 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -54,27 +54,26 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc (* We process the LHS to replace pattern variables by metavariables. *) let lhs_metas = Array.make binder_arity None in - let rec to_m : int -> term -> tbox = fun k t -> - (* [k] is the number of arguments to which [m] is applied. *) + let rec to_m : term -> tbox = fun 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) + _Abst (to_m a) (Bindlib.bind_var x (to_m t)) + | Appl(t,u) -> _Appl (to_m t) (to_m u) | Patt(i,n,a) -> begin - let a = Array.map (to_m 0) a in + let a = Array.map to_m 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_meta_type l) l in _Meta m a | Some(i) -> match lhs_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_meta_type l) l in lhs_metas.(i) <- Some(m); _Meta m a end @@ -87,7 +86,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc | Wild -> assert false (* Cannot appear in LHS. *) | TRef(_) -> assert false (* Cannot appear in LHS. *) in - let lhs_args = List.map (fun p -> Bindlib.unbox (to_m 0 p)) rule.lhs in + let lhs_args = List.map (fun p -> Bindlib.unbox (to_m p)) rule.lhs in let lhs = Basics.add_args (Symb(s,h)) lhs_args in let lhs_metas = Array.map (function Some m -> m | None -> assert false) lhs_metas From 8a784d170734ec1718ed442010c2f6418ec479ab Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Thu, 9 Apr 2020 23:17:42 +0200 Subject: [PATCH 60/66] Cleaning up SR and scoping of rules. --- src/core/basics.ml | 5 +- src/core/env.ml | 16 ++- src/core/handle.ml | 11 +- src/core/pretty.ml | 3 + src/core/scope.ml | 243 +++++++++++++++++++++------------ src/core/sr.ml | 328 ++++++++++++++++++++++++--------------------- src/core/terms.ml | 45 +++++-- src/core/xtc.ml | 2 +- 8 files changed, 390 insertions(+), 263 deletions(-) diff --git a/src/core/basics.ml b/src/core/basics.ml index da6df21a0..2d76790f4 100644 --- a/src/core/basics.ml +++ b/src/core/basics.ml @@ -174,10 +174,11 @@ let distinct_vars : ctxt -> term array -> tvar array option = fun ctx ts -> LHS counterparts. This is a more convenient way of representing terms when analysing confluence or termination. *) let term_of_rhs : rule -> term = fun r -> - let fn i (name, arity) = + let fn i x = + let (name, arity) = (Bindlib.name_of x, r.arities.(i)) in let make_var i = Bindlib.new_var mkfree (Printf.sprintf "x%i" i) in let vars = Array.init arity make_var in let p = _Patt (Some(i)) name (Array.map Bindlib.box_var vars) in TE_Some(Bindlib.unbox (Bindlib.bind_mvar vars p)) in - Bindlib.msubst r.rhs (Array.mapi fn r.pvs) + Bindlib.msubst r.rhs (Array.mapi fn r.vars) diff --git a/src/core/env.ml b/src/core/env.ml index d8aa88a2e..60a123f73 100644 --- a/src/core/env.ml +++ b/src/core/env.ml @@ -27,17 +27,21 @@ let add : tvar -> tbox -> tbox option -> env -> env = fun v a t env -> let find : string -> env -> tvar = fun n env -> let (x,_,_) = List.assoc n env in x -(** [to_prod env t] builds a sequence of products or let-bindings whose - domains are the variables of the environment [env] (from left to right), - and which body is the term [t]: - [to_prod [(xn,an,None);..;(x1,a1,None)] t = ∀x1:a1,..,∀xn:an,t]. *) -let to_prod : env -> tbox -> term = fun env t -> +(** [to_prod env t] builds a sequence of products / let-bindings whose domains + are the variables of the environment [env] (from left to right), and whose + body is the term [t]. By calling [to_prod [(xn,an,None);⋯;(x1,a1,None)] t] + you obtain a term of the form [∀x1:a1,..,∀xn:an,t]. *) +let to_prod_box : env -> tbox -> tbox = fun env t -> let fn t (_,(x,a,u)) = match u with | Some(u) -> _LLet a u (Bindlib.bind_var x t) | None -> _Prod a (Bindlib.bind_var x t) in - Bindlib.unbox (List.fold_left fn t env) + List.fold_left fn t env + +(** [to_prod] is an “unboxed” version of [to_prod_box]. *) +let to_prod : env -> tbox -> term = fun env t -> + Bindlib.unbox (to_prod_box env t) (** [to_abst env t] builds a sequence of abstractions or let bindings, depending on the definition of the elements in the environment whose diff --git a/src/core/handle.ml b/src/core/handle.ml index 8caa24583..27203fbf0 100644 --- a/src/core/handle.ml +++ b/src/core/handle.ml @@ -112,12 +112,13 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option = ({ss with in_scope = StrMap.add x.elt (s, x.pos) ss.in_scope}, None) | P_rules(rs) -> (* Scoping and checking each rule in turn. *) - let handle_rule pr = - let (s,_,_) as r = scope_rule ss pr in - if !(s.sym_def) <> None then + let handle_rule r = + let pr = scope_rule ss r in + let (sym, hint) = pr.elt.pr_sym in + if !(sym.sym_def) <> None then fatal pr.pos "Rewriting rules cannot be given for defined \ - symbol [%s]." s.sym_name; - Sr.check_rule ss.builtins r + symbol [%s]." sym.sym_name; + (sym, hint, Pos.make r.pos (Sr.check_rule ss.builtins pr)) in let rs = List.map handle_rule rs in (* Adding the rules all at once. *) diff --git a/src/core/pretty.ml b/src/core/pretty.ml index 7e697d90e..18e0a771e 100644 --- a/src/core/pretty.ml +++ b/src/core/pretty.ml @@ -235,6 +235,9 @@ let rec pp_ast : ast pp = fun oc cs -> | [c] -> Format.fprintf oc "%a@." pp_command c | c::cs -> Format.fprintf oc "%a\n@.%a" pp_command c pp_ast cs +(** Short synonym of [pp_p_term]. *) +let pp : p_term pp = pp_p_term + (** [beautify cmds] pretty-prints the commands [cmds] to standard output. *) let beautify : ast -> unit = pp_ast Format.std_formatter diff --git a/src/core/scope.ml b/src/core/scope.ml index 7ce38d44e..e413054d3 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -129,6 +129,19 @@ let get_root : p_term -> sig_state -> sym * pp_hint = fun t ss -> in get_root t +(** Data used when scoping a LHS. *) +type m_lhs_data = + { m_lhs_indices : (string, int ) Hashtbl.t + (** Stores the index reserved for a pattern variable of the given name. *) + ; m_lhs_arities : (int , int ) Hashtbl.t + (** Stores the arity of the pattern variable at the given index. *) + ; m_lhs_names : (int , string) Hashtbl.t + (** Stores the name of the pattern variable at the given index (if any). *) + ; mutable m_lhs_size : int + (** Stores the current known size of the environment of the RHS. *) + ; m_lhs_in_env : string list + (** Pattern variables definitely needed in the RHS environment. *) } + (** Representation of the different scoping modes. Note that the constructors hold specific information for the given mode. *) type mode = @@ -138,16 +151,15 @@ type mode = scoped term. *) | M_Patt (** Scoping mode for patterns in the rewrite tactic. *) - | M_LHS of (string * int) list * bool * int Stdlib.ref + | M_LHS of bool * m_lhs_data (** Scoping mode for rewriting rule left-hand sides. The constructor carries - a map associating an index to every pattern variable, a flag set to - [true] if {!constructor:Terms.expo.Privat} symbols are allowed, and an - index counter to be incremented for every implicit argument. *) - | M_RHS of (string * tevar) list * bool + a flag that is set to [true] if {!constructor:Terms.expo.Privat} symbols + are allowed, and also additional data. *) + | M_RHS of bool * (string, tevar) Hashtbl.t (** Scoping mode for rewriting rule righ-hand sides. The constructor carries - the environment for variables that will be bound in the representation - of the RHS along with a flag indicating whether - {!constructor:Terms.expo.Privat} terms are allowed. *) + a flag that is set to [true] if {!constructor:Terms.expo.Privat} symbols + are allowed, and the environment for variables that we known to be bound + in the RHS. *) (** [get_implicitness t] gives the specified implicitness of the parameters of a symbol having the (parser-level) type [t]. *) @@ -179,9 +191,25 @@ let get_args : p_term -> p_term * p_term list = state [ss] is used to hande module aliasing according to [find_qid]. *) let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> (* Unique pattern variable generation for wildcards in a LHS. *) - let fresh_patt_name k = Stdlib.(incr k; Printf.sprintf "#%i" !k) in - let fresh_patt k = - let n = fresh_patt_name k in _Patt (Some Stdlib.(!k)) n + let fresh_patt data name env = + let fresh_index () = + let i = data.m_lhs_size in + data.m_lhs_size <- i + 1; + let arity = Array.length env in + Hashtbl.add data.m_lhs_arities i arity; i + in + match name with + | Some(name) -> + let i = + try Hashtbl.find data.m_lhs_indices name with Not_found -> + let i = fresh_index () in + Hashtbl.add data.m_lhs_indices name i; + Hashtbl.add data.m_lhs_names i name; i + in + _Patt (Some(i)) (Printf.sprintf "#%i_%s" i name) env + | None -> + let i = fresh_index () in + _Patt (Some(i)) (Printf.sprintf "#%i" i) env in (* Toplevel scoping function, with handling of implicit arguments. *) let rec scope : env -> p_term -> tbox = fun env t -> @@ -237,14 +265,20 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> match (a, md) with | (Some(a), M_LHS(_) ) -> fatal a.pos "Annotation not allowed in a LHS." - | (None , M_LHS(_,_,k)) -> fresh_patt k (Env.to_tbox env) + | (None , M_LHS(_,d) ) -> fresh_patt d None (Env.to_tbox env) | (Some(a), _ ) -> scope env a | (None , _ ) -> (* Create a new metavariable of type [TYPE] for the missing domain. *) let vs = Env.to_tbox env in - _Meta (fresh_meta (Env.to_prod env _Type) (Array.length vs)) vs + let a = Env.to_prod_box env _Type in + let m = _Meta_full (fresh_meta_box a (Array.length vs)) vs in + (* Sanity check: only variables of [env] free in [m] if not in RHS. *) + match md with + | M_RHS(_,_) -> m + | _ -> + assert (Bindlib.is_closed (Bindlib.bind_mvar (Env.vars env) m)); m (* Scoping of a binder (abstraction or product). The environment made of the - * variables is also returned. *) + variables is also returned. *) and scope_binder cons env xs t = let rec aux env xs = match xs with @@ -272,22 +306,31 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> | (P_Type , M_LHS(_) ) -> fatal t.pos "[%a] is not allowed in a LHS." Print.pp Type | (P_Type , _ ) -> _Type - | (P_Iden(qid,_) , M_LHS(_,p,_) ) -> find_qid true p ss env qid + | (P_Iden(qid,_) , M_LHS(p,_) ) -> find_qid true p ss env qid | (P_Iden(qid,_) , M_Term(_,Privat )) -> find_qid false true ss env qid - | (P_Iden(qid,_) , M_RHS(_,p) ) -> find_qid false p ss env qid + | (P_Iden(qid,_) , M_RHS(p,_) ) -> find_qid false p ss env qid | (P_Iden(qid,_) , _ ) -> find_qid false false ss env qid - | (P_Wild , M_LHS(_,_,k) ) -> fresh_patt k (Env.to_tbox env) + | (P_Wild , M_LHS(_,d) ) -> + fresh_patt d None (Env.to_tbox env) | (P_Wild , M_Patt ) -> _Wild | (P_Wild , _ ) -> (* We create a metavariable [m] of type [tm], which itself is also a metavariable [x] of type [Type]. Note that this case applies both to regular terms, and to the RHS of rewriting rules. *) let vs = Env.to_tbox env in - let n = Array.length vs in - let x = fresh_meta (Env.to_prod env _Type) n in - let tm = Env.to_prod env (_Meta x vs) in - let m = fresh_meta tm n in - _Meta m vs + let arity = Array.length vs in + let tm = + let x = fresh_meta_box (Env.to_prod_box env _Type) arity in + Env.to_prod_box env (_Meta_full x vs) + in + let m = _Meta_full (fresh_meta_box tm arity) vs in + (* Sanity check: only variables of [env] free in [m] if not in RHS. *) + begin + match md with + | M_RHS(_,_) -> m + | _ -> + assert (Bindlib.is_closed (Bindlib.bind_mvar (Env.vars env) m)); m + end | (P_Meta(id,ts) , M_Term(m,_) ) -> let m2 = (* We first check if the metavariable is in the map. *) @@ -304,7 +347,7 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> _Meta m2 (Array.map (scope env) ts) | (P_Meta(_,_) , _ ) -> fatal t.pos "Metavariables are not allowed in rewriting rules." - | (P_Patt(id,ts) , M_LHS(m,_,k) ) -> + | (P_Patt(id,ts) , M_LHS(_,d) ) -> (* Check that [ts] are variables. *) let scope_var t = match unfold (Bindlib.unbox (scope env t)) with @@ -322,33 +365,28 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t -> environment of a pattern variable." name done done; - (* Find the reserved index, if any. *) + let ar = Array.map Bindlib.box_var vs in begin match id with - | None -> + | None when List.length env = Array.length vs -> + wrn t.pos "Pattern [%a] could be replaced by [_]." Pretty.pp t; + | Some(id) when not (List.mem id.elt d.m_lhs_in_env) -> if List.length env = Array.length vs then - wrn t.pos "Pattern [%a] could be replaced by [_]." - Pretty.pp_p_term t; - fresh_patt k (Array.map Bindlib.box_var vs) - | Some(id) -> - let i = - try Some(List.assoc id.elt m) with Not_found -> - if List.length env = Array.length vs then - wrn t.pos "Pattern variable [%a] can be replaced by a \ - wildcard [_]." Pretty.pp_p_term t - else - wrn t.pos "Pattern variable [&%s] does not need to be \ - named." id.elt; - None - in - _Patt i id.elt (Array.map Bindlib.box_var vs) - end - | (P_Patt(id,ts) , M_RHS(m,_) ) -> + wrn t.pos "Pattern variable [%a] can be replaced by a \ + wildcard [_]." Pretty.pp t + else + wrn t.pos "Pattern variable [&%s] does not need to be \ + named." id.elt + | _ -> () + end; + fresh_patt d (Option.map (fun id -> id.elt) id) ar + | (P_Patt(id,ts) , M_RHS(_,h) ) -> let x = match id with | None -> fatal t.pos "Wildcard pattern not allowed in a RHS." - | Some(id) -> try List.assoc id.elt m with Not_found -> - fatal t.pos "Pattern variable not in scope." + | Some(id) -> + try Hashtbl.find h id.elt with Not_found -> + fatal t.pos "Pattern variable not in scope." in _TEnv (Bindlib.box_var x) (Array.map (scope env) ts) | (P_Patt(_,_) , _ ) -> @@ -470,16 +508,30 @@ let patt_vars : p_term -> (string * int) list * string list = in patt_vars ([],[]) +(** Representation of a rewriting rule prior to SR-checking. *) +type pre_rule = + { pr_sym : sym * pp_hint + (** Head symbol of the LHS with its printing hint. *) + ; pr_lhs : term list + (** Arguments of the LHS. *) + ; pr_vars : term_env Bindlib.mvar + (** Pattern variables that can appear in the RHS. *) + ; pr_rhs : tbox + (** Body of the RHS, should only be unboxed once. *) + ; pr_names : (int, string) Hashtbl.t + (** Gives the original name (if any) of pattern variable at given index. *) + ; pr_arities : int array + (** Gives the arity of all the pattern varialbes in field [pr_vars]. *) } + (** [scope_rule ss r] turns a parser-level rewriting rule [r] into a rewriting rule (and the associated head symbol). *) -let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> +let scope_rule : sig_state -> p_rule -> pre_rule loc = fun ss r -> let (p_lhs, p_rhs) = r.elt in (* Compute the set of pattern variables on both sides. *) - let (pvs_lhs, _nl) = patt_vars p_lhs in - (* NOTE to reject non-left-linear rules, we can check [nl = []] here. *) - let (pvs_rhs, _) = patt_vars p_rhs in - (* Check that the pattern variables of the RHS exist in the LHS and have the - same arities. *) + let (pvs_lhs, nl) = patt_vars p_lhs in + (* NOTE to reject non-left-linear rules check [nl = []] here. *) + let (pvs_rhs, _ ) = patt_vars p_rhs in + (* Check that pattern variables of RHS exist LHS (with right arities). *) let check_in_lhs (m,i) = let j = try List.assoc m pvs_lhs with Not_found -> @@ -488,45 +540,68 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r -> if i <> j then fatal p_lhs.pos "Arity mismatch for [%s]." m in List.iter check_in_lhs pvs_rhs; - let map = List.mapi (fun i (m,_) -> (m,i)) pvs_lhs in - (* NOTE [map] maps pattern variables to their position in [pvs_lhs]. *) - (* NOTE pattern variables not in [map] can be considered as wildcards. *) - (* Get privacy of the head of the rule, and scope the rest with this - privacy. *) + (* Get privacy of head of the rule, scope the rest accordingly. *) let prv = is_private (fst (get_root p_lhs ss)) in - (* We scope the LHS and add indexes in the environment for metavariables. *) - let l = List.length map in - let k = Stdlib.ref (l-1) in - let lhs = Bindlib.unbox (scope (M_LHS(map,prv,k)) ss Env.empty p_lhs) in - let (sym, hint, lhs) = - let (h, args) = Basics.get_args lhs in + (* Scope the LHS and get the reserved index for named pattern variables. *) + let (pr_lhs, data) = + let data = + { m_lhs_indices = Hashtbl.create 7 + ; m_lhs_arities = Hashtbl.create 7 + ; m_lhs_names = Hashtbl.create 7 + ; m_lhs_size = 0 + ; m_lhs_in_env = nl @ (List.map fst pvs_rhs) } + in + let pr_lhs = scope (M_LHS(prv, data)) ss Env.empty p_lhs in + (Bindlib.unbox pr_lhs, data) + in + (* Check the head symbol and build actual LHS. *) + let (sym, hint, pr_lhs) = + let (h, args) = Basics.get_args pr_lhs in match h with - | Symb(s,_) when is_constant s -> - fatal p_lhs.pos "Constant LHS head symbol." - | Symb(({sym_expo=Protec; sym_path; _} as s),h) -> - if ss.signature.sign_path <> sym_path then - fatal p_lhs.pos "Cannot define rules on foreign protected symbols." - else (s, h, args) - | Symb(s,h) -> (s, h, args) - | _ -> + | Symb(s,h) -> + if is_constant s then + fatal p_lhs.pos "Constant LHS head symbol."; + if s.sym_expo = Protec && ss.signature.sign_path <> s.sym_path then + fatal p_lhs.pos "Cannot define rules on foreign protected symbols."; + (s, h, args) + | _ -> fatal p_lhs.pos "No head symbol in LHS." in - if lhs = [] then wrn p_lhs.pos "LHS head symbol with no argument."; - (* We extend [map] with the fresh pattern variables created in scoping. *) - let k = Stdlib.(!k-(l-1)) in - let fresh_patts = Array.init k (fun i -> Printf.sprintf "#%i" (l+i)) in - let names = Array.append (Array.of_list (List.map fst map)) fresh_patts in - (* We scope the RHS and bind the pattern variables. *) - let vars = Bindlib.new_mvar te_mkfree names in - let rhs = - let map = Array.map2 (fun n v -> (n,v)) names vars in - let mode = M_RHS(Array.to_list map, is_private sym) in - Bindlib.unbox (Bindlib.bind_mvar vars (scope mode ss Env.empty p_rhs)) + if pr_lhs = [] then wrn p_lhs.pos "LHS head symbol with no argument."; + (* Create the pattern variables that can be bound in the RHS. *) + let pr_vars = + let fn i = + let name = + try Printf.sprintf "#%i_%s" i (Hashtbl.find data.m_lhs_names i) + with Not_found -> Printf.sprintf "#%i" i + in + Bindlib.new_var te_mkfree name + in + Array.init data.m_lhs_size fn + in + (* We scope the RHS. *) + let pr_rhs = + let mode = + let htbl_vars = Hashtbl.create (Hashtbl.length data.m_lhs_indices) in + let fn k i = Hashtbl.add htbl_vars k pr_vars.(i) in + Hashtbl.iter fn data.m_lhs_indices; + M_RHS(is_private sym, htbl_vars) + in + scope mode ss Env.empty p_rhs + in + (* We put everything together to build the pre-rule. *) + let pr_arities = + let fn i = + try Hashtbl.find data.m_lhs_arities i + with Not_found -> assert false (* Unreachable. *) + in + Array.init data.m_lhs_size fn + in + let pr = + { pr_sym = (sym, hint) ; pr_lhs ; pr_vars ; pr_rhs ; pr_arities + ; pr_names = data.m_lhs_names } in - (* We also store [pvs_lhs] to facilitate confluence/termination checking. *) - let pvs = Array.of_list pvs_lhs and arity = List.length lhs in - (* We put everything together to build the rule. *) - (sym, hint, Pos.make r.pos {lhs; rhs; arity; pvs; vars}) + Pos.make r.pos pr (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term that will correspond to selection pattern (rewrite tactic). *) diff --git a/src/core/sr.ml b/src/core/sr.ml index bad7a91b6..0378df783 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -1,10 +1,11 @@ (** Type-checking and inference. *) +open Extra open Timed open Console open Terms +open Scope open Print -open Extra (** Logging function for typing. *) let log_subj = new_logger 's' "subj" "subject-reduction" @@ -37,46 +38,20 @@ let build_meta_type : int -> term = fun k -> done; Bindlib.unbox !res -(** [check_rule builtins r] checks whether rule [r] is well-typed. The [Fatal] - exception is raised in case of error. *) -let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc - -> sym * pp_hint * rule Pos.loc = - fun builtins ((s, h, { elt = rule; pos = pos }) as shrp) -> - if !log_enabled then log_subj (mag "check rule %a") pp_rule (s, h, rule); - - let binder_arity = Bindlib.mbinder_arity rule.rhs in - (* Compute the metavariables of the RHS, including the metavariables of - their types. *) - let rhs_metas = - Basics.get_metas true - (Bindlib.msubst rule.rhs (Array.make binder_arity TE_None)) +let patt_to_tenv : term_env Bindlib.var array -> term -> tbox = fun vars -> + let get_te i = + match i with + | None -> assert false (* Cannot appear in LHS. *) + | Some(i) -> try vars.(i) with Invalid_argument(_) -> assert false in - - (* We process the LHS to replace pattern variables by metavariables. *) - let lhs_metas = Array.make binder_arity None in - let rec to_m : term -> tbox = fun t -> + let rec trans 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 a) (Bindlib.bind_var x (to_m t)) - | Appl(t,u) -> _Appl (to_m t) (to_m u) - | Patt(i,n,a) -> - begin - let a = Array.map to_m a in - let l = Array.length a in - match i with - | None -> - let m = fresh_meta ~name:n (build_meta_type l) l in - _Meta m a - | Some(i) -> - match lhs_metas.(i) with - | Some(m) -> _Meta m a - | None -> - let m = fresh_meta ~name:n (build_meta_type l) l in - lhs_metas.(i) <- Some(m); - _Meta m a - end + | Abst(a,b) -> let (x, t) = Bindlib.unbind b in + _Abst (trans a) (Bindlib.bind_var x (trans t)) + | Appl(t,u) -> _Appl (trans t) (trans u) + | Patt(i,_,a) -> _TEnv (Bindlib.box_var (get_te i)) (Array.map trans a) | Type -> assert false (* Cannot appear in LHS. *) | Kind -> assert false (* Cannot appear in LHS. *) | Prod(_,_) -> assert false (* Cannot appear in LHS. *) @@ -86,104 +61,179 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc | Wild -> assert false (* Cannot appear in LHS. *) | TRef(_) -> assert false (* Cannot appear in LHS. *) in - let lhs_args = List.map (fun p -> Bindlib.unbox (to_m p)) rule.lhs in - let lhs = Basics.add_args (Symb(s,h)) lhs_args in - let lhs_metas = - Array.map (function Some m -> m | None -> assert false) lhs_metas + trans + +(** [new_function_symbol name a] creates a fresh function symbol named [name], + with type [a]. The symbols created using this function should not outlive + the SR-checking phase. *) +let new_function_symbol name a = + { sym_name = name ; sym_type = ref a ; sym_path = [] ; sym_def = ref None + ; sym_impl = [] ; sym_rules = ref [] ; sym_tree = ref Tree_types.empty_dtree + ; sym_prop = Defin ; sym_expo = Public } + +(** Mapping of pattern variable names to their reserved index. *) +type index_tbl = (string, int) Hashtbl.t + +(** [symb_to_tenv pr syms htbl t] builds a RHS for the pre-rule [pr]. The term + [t] is expected to be a version of the RHS of [pr] whose term environments + have been replaced by function symbols of [syms]. This function builds the + reverse transformation, replacing symbols by the term environment variable + they stand for. Here, [htbl] should give the index in the RHS environment + for the symbols of [syms] that have corresponding [term_env] variable. The + pre-rule [pr] is provided to give access to these variables and also their + expected arities. *) +let symb_to_tenv : pre_rule Pos.loc -> sym list -> index_tbl -> term -> tbox = + fun {elt={pr_vars=vars;pr_arities=arities;_};pos} syms htbl t -> + let rec symb_to_tenv t = + log_subj "symb_to_tenv %a" pp_term t; + let (h, ts) = Basics.get_args t in + let ts = List.map symb_to_tenv ts in + let (h, ts) = + match h with + | Symb(f,_) when List.memq f syms -> + let i = + try Hashtbl.find htbl f.sym_name with Not_found -> + fatal pos "Introduced symbol [%s] cannot be removed." f.sym_name + in + let (ts1, ts2) = List.cut ts arities.(i) in + (_TEnv (Bindlib.box_var vars.(i)) (Array.of_list ts1), ts2) + | Symb(s,h) -> (_Symb s h, ts) + | Vari(x) -> (_Vari x , ts) + | Type -> (_Type , ts) + | Kind -> (_Kind , ts) + | Abst(a,b) -> + let (x, t) = Bindlib.unbind b in + let b = Bindlib.bind_var x (symb_to_tenv t) in + (_Abst (symb_to_tenv a) b, ts) + | Prod(a,b) -> + let (x, t) = Bindlib.unbind b in + let b = Bindlib.bind_var x (symb_to_tenv t) in + (_Prod (symb_to_tenv a) b, ts) + | LLet(a,t,b) -> + let (x, u) = Bindlib.unbind b in + let b = Bindlib.bind_var x (symb_to_tenv u) in + (_LLet (symb_to_tenv a) (symb_to_tenv t) b, ts) + | Meta(m,ar) -> + ignore (m, ar); + fatal pos "A metavariable could not be instantiated in the RHS." + | TEnv(_,_) -> assert false (* TEnv have been replaced in [t]. *) + | Appl(_,_) -> assert false (* Cannot appear in RHS. *) + | Patt(_,_,_) -> assert false (* Cannot appear in RHS. *) + | Wild -> assert false (* Cannot appear in RHS. *) + | TRef(_) -> assert false (* Cannot appear in RHS. *) + in + List.fold_left _Appl h ts in + symb_to_tenv t - (* Build a map LHS pattern variable -> term_env variable. *) - let sym_name m = - let name = - match m.meta_name with - | Some(n) -> n - | None -> string_of_int m.meta_key - in "&" ^ name +(** [check_rule bmap r] checks whether the pre-rule [r] is well-typed and then + construct the corresponding rule. The “bultin map” [bmap] is passed to the + unification engine. Note that [Fatal] is raised in case of error. *) +let check_rule : sym StrMap.t -> pre_rule Pos.loc -> rule = fun bmap pr -> + (* Unwrap the contents of the pre-rule. *) + let (pos, (s, h), lhs, vars, rhs_vars, arities) = + let Pos.{elt={pr_sym;pr_lhs;pr_vars;pr_rhs;pr_arities;_}; pos} = pr in + (pos, pr_sym, pr_lhs, pr_vars, pr_rhs, pr_arities) in - let map = - let map = ref StrMap.empty in - let fn x m = map := StrMap.add (sym_name m) (x, m.meta_arity) !map in - Array.iter2 fn rule.vars lhs_metas; !map + let arity = List.length lhs in + if !log_enabled then + begin + (* The unboxing here could be harmful since it leads to [rhs_vars] being + unboxed twice. However things should be fine here since the result is + only used for printing. *) + let rhs = Bindlib.(unbox (bind_mvar vars rhs_vars)) in + let naive_rule = {lhs; rhs; arity; arities; vars} in + log_subj "check rule [%a]" pp_rule (s, h, naive_rule); + end; + (* Replace [Patt] nodes of LHS with corresponding elements of [vars]. *) + let lhs_vars = + let args = List.map (patt_to_tenv vars) lhs in + List.fold_left _Appl (_Symb s h) args in - + (* Create metavariables that will stand for the variables of [vars]. *) + let var_names = Array.map (fun x -> "&" ^ Bindlib.name_of x) vars in + let metas = + let fn i name = + let arity = arities.(i) in + fresh_meta ~name (build_meta_type arity) arity + in + Array.mapi fn var_names + in + (* Substitute them in the LHS and in the RHS. *) + let (lhs_typing, rhs_typing) = + let lhs_rhs = Bindlib.box_pair lhs_vars rhs_vars in + let b = Bindlib.(unbox (bind_mvar vars lhs_rhs)) in + let meta_to_tenv m = + let xs = Basics.fresh_vars m.meta_arity in + let ts = Array.map _Vari xs in + TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m ts))) + in + let te_envs = Array.map meta_to_tenv metas in + Bindlib.msubst b te_envs + in + if !log_enabled then + begin + log_subj (mag "transformed LHS is [%a]") pp lhs_typing; + log_subj (mag "transformed RHS is [%a]") pp rhs_typing + end; (* Infer the typing constraints of the LHS. *) - match Typing.infer_constr builtins [] lhs with - | None -> wrn pos "Untypable LHS."; shrp + match Typing.infer_constr bmap [] lhs_typing with + | None -> fatal pos "The LHS is not typable." | Some(ty_lhs, lhs_constrs) -> if !log_enabled then begin log_subj (gre "LHS has type %a") pp ty_lhs; - List.iter (log_subj " if %a" pp_constr) lhs_constrs + List.iter (log_subj " if %a" pp_constr) lhs_constrs; + log_subj (mag "LHS is now [%a]") pp lhs_typing; + log_subj (mag "RHS is now [%a]") pp rhs_typing end; - - (* We apply the mapping pattern variable -> metavariable to the RHS and the - types of its metavariables. *) - let fn m = - let xs = Basics.fresh_vars m.meta_arity in - let ts = Array.map _Vari xs in - TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m ts))) - in - let te_envs = Array.map fn lhs_metas in - let subst t = Bindlib.msubst t te_envs in - let rhs = subst rule.rhs in - log_subj "rhs %a" pp_term rhs; - let fn m = - let bt = lift !(m.meta_type) in - m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar rule.vars bt)) - in - MetaSet.iter fn rhs_metas; - - (* We compute the set of all uninstantiated metavariables of the LHS, - including in the types of LHS metavariables. *) - let all_lhs_metas = - let open MetaSet in - let add_metas m ms = + (* We build a map allowing to find a variable index from its name. *) + let htbl : index_tbl = Hashtbl.create (Array.length vars) in + Array.iteri (fun i name -> Hashtbl.add htbl name i) var_names; + (* We instantiate all the uninstantiated metavariables of the LHS (including + those appearing in the types of LHS metavariabeles) with a fresh function + symbol. We also keep a list of those symbols. *) + let symbols = + let symbols = Stdlib.ref [] in + let rec instantiate m = match !(m.meta_value) with - | Some _ -> + | Some(_) -> + (* Instantiate recursively the meta-variables of the definition. *) let t = Meta(m, Array.make m.meta_arity Kind) in - Basics.add_metas true t ms - | None -> add m (Basics.add_metas true !(m.meta_type) ms) - in - Array.fold_right add_metas lhs_metas empty - in - (* We instantiate these metavariables by fresh function symbols. *) - let instantiate m t = - let xs = Basics.fresh_vars m.meta_arity in - let t = Array.fold_left (fun t x -> _Appl t (_Vari x)) t xs in - m.meta_value := Some (Bindlib.unbox (Bindlib.bind_mvar xs t)) - in - let fn m = - let s = - { sym_name = sym_name m - ; sym_type = m.meta_type - ; sym_path = [] - ; sym_def = ref None - ; sym_impl = [] - ; sym_rules = ref [] - ; sym_tree = ref Tree_types.empty_dtree - ; sym_prop = Defin - ; sym_expo = Public } + Basics.iter_meta true instantiate t + | None -> + (* Instantiate recursively the meta-variables of the type. *) + Basics.iter_meta true instantiate !(m.meta_type); + (* Instantiation of [m]. *) + let sym_name = + match m.meta_name with + | Some(n) -> n + | None -> string_of_int m.meta_key + in + let s = new_function_symbol sym_name !(m.meta_type) in + Stdlib.(symbols := s :: !symbols); + (* Build a definition for [m]. *) + let xs = Basics.fresh_vars m.meta_arity in + let s = _Symb s Nothing in + let def = Array.fold_left (fun t x -> _Appl t (_Vari x)) s xs in + m.meta_value := Some(Bindlib.unbox (Bindlib.bind_mvar xs def)) in - instantiate m (_Symb s Nothing) + Array.iter instantiate metas; Stdlib.(!symbols) in - MetaSet.iter fn all_lhs_metas; - - (* Here, we should complete the constraints into a set of rewriting rules on - those function symbols. *) - (* TODO *) - (* Compute the constraints for the RHS to have the same type as the LHS. *) - let to_solve = Infer.check [] rhs ty_lhs in - if !log_enabled && to_solve <> [] then + let to_solve = Infer.check [] rhs_typing ty_lhs in + if !log_enabled then begin log_subj (gre "RHS has type %a") pp ty_lhs; - List.iter (log_subj " if %a" pp_constr) to_solve + List.iter (log_subj " if %a" pp_constr) to_solve; + log_subj (mag "LHS is now [%a]") pp lhs_typing; + log_subj (mag "RHS is now [%a]") pp rhs_typing end; - + (* TODO we should complete the constraints into a set of rewriting rule on + the function symbols of [symbols]. *) (* Solving the typing constraints of the RHS. *) - match Unif.(solve builtins {no_problems with to_solve}) with - | None -> - fatal pos "Rule [%a] does not preserve typing." pp_rule (s,h,rule) + match Unif.(solve bmap {no_problems with to_solve}) with + | None -> fatal pos "The rewriting rule does not preserve typing." | Some(cs) -> let is_constr c = let eq_comm (_,t1,u1) (_,t2,u2) = @@ -199,43 +249,13 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc if cs <> [] then begin List.iter (fatal_msg "Cannot solve %a\n" pp_constr) cs; - fatal pos "Unable to prove type preservation for the rule %a." - pp_rule (s,h,rule) + fatal pos "Unable to prove type preservation for a rewriting rule." end; - (* Replace metavariable symbols by term_env variables, and bind them. *) - let rec to_tenv t = - log_subj "to_tenv %a" pp_term t; - let t = unfold t in - let h, ts = Basics.get_args t in - let ts = List.map to_tenv ts in - match h with - | Symb(f,_) -> to_tenv_patt h ts f.sym_name - | Prod(a,b) -> Prod(to_tenv a, to_tenv_binder b) - | Abst(a,b) -> Basics.add_args (Abst(to_tenv a, to_tenv_binder b)) ts - | LLet(a,t,u) -> - Basics.add_args (LLet(to_tenv a, to_tenv t, to_tenv_binder u)) ts - | Appl(_,_) -> assert false - | Meta(_,_) -> assert false - | Patt(_) -> assert false - | Wild -> assert false - | _ -> Basics.add_args h ts - and to_tenv_binder b = - let (x,b) = Bindlib.unbind b in - Bindlib.unbox (Bindlib.bind_var x (lift (to_tenv b))) - and to_tenv_patt h ts s = - if s = "" || s.[0] <> '&' then Basics.add_args h ts - else - begin - try - let (v,k) = StrMap.find s map in - let (ts1,ts2) = List.cut ts k in - Basics.add_args (TEnv (TE_Vari v, Array.of_list ts1)) ts2 - with Not_found -> assert false - end - in - log_subj "rhs %a" pp_term rhs; - let rhs = to_tenv rhs in - let rhs = Bindlib.unbox (Bindlib.bind_mvar rule.vars (lift rhs)) in - let elt = { rule with rhs } in - (s, h, { elt; pos }) + let rhs = symb_to_tenv pr symbols htbl rhs_typing in + if !log_enabled then + log_subj "final RHS is [%a]" pp (Bindlib.unbox rhs); + (* TODO optimisation for evaluation: environment minimisation. *) + (* Construct the rule. *) + let rhs = Bindlib.unbox (Bindlib.bind_mvar vars rhs) in + { lhs ; rhs ; arity ; arities ; vars } diff --git a/src/core/terms.ml b/src/core/terms.ml index 074d925f0..11dc46b98 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -137,15 +137,15 @@ type term = rule to apply, and a RHS (right hand side) giving the action to perform if the rule applies. More explanations are given below. *) and rule = - { lhs : term list + { lhs : term list (** Left hand side (or LHS). *) - ; rhs : (term_env, term) Bindlib.mbinder + ; rhs : (term_env, term) Bindlib.mbinder (** Right hand side (or RHS). *) - ; arity : int + ; arity : int (** Required number of arguments to be applicable. *) - ; pvs : (string * int) array - (** Name and arity of the pattern variables bound in the RHS. *) - ; vars : term_env Bindlib.var array + ; arities : int array + (** Arrities of the pattern variables bound in the RHS. *) + ; vars : term_env Bindlib.var array (** Bindlib variables used to build [rhs]. *) } (** The LHS (or pattern) of a rewriting rule is always formed of a head symbol @@ -294,12 +294,13 @@ let rec unfold : term -> term = fun t -> (** [unset m] returns [true] if [m] is not instantiated. *) let unset : meta -> bool = fun m -> !(m.meta_value) = None -(** [fresh_meta a n] creates a new metavariable of type [a] and arity [n]. *) +(** [fresh_meta ?name a n] creates a fresh metavariable with the optional name + [name], and of type [a] and arity [n]. *) let fresh_meta : ?name:string -> term -> int -> meta = let counter = Stdlib.ref (-1) in let fresh_meta ?name a n = { meta_key = Stdlib.(incr counter; !counter) ; meta_name = name - ; meta_type = ref a ; meta_arity = n ; meta_value = ref None } + ; meta_type = ref a ; meta_arity = n ; meta_value = ref None } in fresh_meta (** [set_meta m v] sets the value of the metavariable [m] to [v]. Note that no @@ -309,9 +310,12 @@ let set_meta : meta -> (term, term) Bindlib.mbinder -> unit = fun m v -> (** [meta_name m] returns a string representation of [m]. *) let meta_name : meta -> string = fun m -> - "?" ^ match m.meta_name with - | Some(n) -> n - | None -> string_of_int m.meta_key + let name = + match m.meta_name with + | Some(n) -> n + | None -> string_of_int m.meta_key + in + "?" ^ name (** [term_of_meta m env] constructs the application of a dummy symbol with the same type as [m], to the element of the environment [env]. The idea is to @@ -449,6 +453,25 @@ let rec lift : term -> tbox = fun t -> "visual capture" while printing terms. *) let cleanup : term -> term = fun t -> Bindlib.unbox (lift t) +(** [fresh_meta_box ?name a n] is the boxed counterpart of [fresh_meta]. It is + only useful in the rare cases where the type of a metavariables contains a + free term variable environement. This should only happens when scoping the + rewriting rules, use this function with care. The metavariable is created + immediately with a dummy type, and the type becomes valid at unboxing. The + boxed metavariable should be unboxed at most once, otherwise its type may + be rendered invalid in some contexts. *) +let fresh_meta_box : ?name:string -> tbox -> int -> meta Bindlib.box = + fun ?name a n -> + let m = fresh_meta ?name Kind n in + Bindlib.box_apply (fun a -> m.meta_type := a; m) a + +(** [_Meta_full m ar] is similar to [_Meta m ar] but works with a metavariable + that is boxed. This is useful in very rare cases, when metavariables need + to be able to contain free term environment variables. Using this function + in bad places is harmful for efficiency but not unsound. *) +let _Meta_full : meta Bindlib.box -> tbox array -> tbox = fun u ar -> + Bindlib.box_apply2 (fun u ar -> Meta(u,ar)) u (Bindlib.box_array ar) + (** Sets and maps of metavariables. *) module Meta = struct type t = meta diff --git a/src/core/xtc.ml b/src/core/xtc.ml index 496c256fa..23caed2a5 100644 --- a/src/core/xtc.ml +++ b/src/core/xtc.ml @@ -118,7 +118,7 @@ let print_tl_rule : Format.formatter -> int -> sym -> rule -> unit = in the form of a pair containing the name of the variable and its type, inferred by the solver. *) let get_vars : sym -> rule -> (string * Terms.term) list = fun s r -> - let rule_ctx : tvar option array = Array.make (Array.length r.pvs) None in + let rule_ctx : tvar option array = Array.make (Array.length r.vars) None in let var_list : tvar list ref = ref [] in let rec subst_patt v t = match t with From 2af80c3bfc6b2c1028208976b15c271031bd3c4c Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 10 Apr 2020 15:53:43 +0200 Subject: [PATCH 61/66] Apply a comment I forgot. --- src/core/sr.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 0378df783..2b63db155 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -113,8 +113,7 @@ let symb_to_tenv : pre_rule Pos.loc -> sym list -> index_tbl -> term -> tbox = let (x, u) = Bindlib.unbind b in let b = Bindlib.bind_var x (symb_to_tenv u) in (_LLet (symb_to_tenv a) (symb_to_tenv t) b, ts) - | Meta(m,ar) -> - ignore (m, ar); + | Meta(_,_) -> fatal pos "A metavariable could not be instantiated in the RHS." | TEnv(_,_) -> assert false (* TEnv have been replaced in [t]. *) | Appl(_,_) -> assert false (* Cannot appear in RHS. *) From 5eb7edac82e9aa2d040e896a0fee88afd43b49c5 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 10 Apr 2020 15:58:52 +0200 Subject: [PATCH 62/66] Typo. --- src/core/sr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/sr.ml b/src/core/sr.ml index 2b63db155..3205d0ef6 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -190,8 +190,8 @@ let check_rule : sym StrMap.t -> pre_rule Pos.loc -> rule = fun bmap pr -> let htbl : index_tbl = Hashtbl.create (Array.length vars) in Array.iteri (fun i name -> Hashtbl.add htbl name i) var_names; (* We instantiate all the uninstantiated metavariables of the LHS (including - those appearing in the types of LHS metavariabeles) with a fresh function - symbol. We also keep a list of those symbols. *) + those appearing in the types of these metavariables) using fresh function + symbols. We also keep a list of those symbols. *) let symbols = let symbols = Stdlib.ref [] in let rec instantiate m = From 07a3f39813d774db0748abc1c55c4a8a2c1be28a Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 10 Apr 2020 16:16:46 +0200 Subject: [PATCH 63/66] Apply my own comments. --- src/core/basics.ml | 6 ++++-- src/core/terms.ml | 16 ++++++++++------ 2 files changed, 14 insertions(+), 8 deletions(-) diff --git a/src/core/basics.ml b/src/core/basics.ml index 2d76790f4..457b0f9ea 100644 --- a/src/core/basics.ml +++ b/src/core/basics.ml @@ -4,9 +4,11 @@ open Extra open Timed open Terms -(** Create an array of fresh variables [|x1;..;xn|]. *) +(** [fresh_vars n] creates an array of [n] fresh variables. The names of these + variables is ["_var_i"], where [i] is a number introduced by the [Bindlib] + library to avoid name clashes (minimal renaming is done). *) let fresh_vars : int -> tvar array = fun n -> - Bindlib.new_mvar mkfree (Array.init n (Printf.sprintf "x%i")) + Bindlib.new_mvar mkfree (Array.make n "_var_") (** [to_tvar t] returns [x] if [t] is of the form [Vari x] and fails otherwise. *) diff --git a/src/core/terms.ml b/src/core/terms.ml index 11dc46b98..fd3c2a445 100644 --- a/src/core/terms.ml +++ b/src/core/terms.ml @@ -481,12 +481,16 @@ end module MetaSet = Set.Make(Meta) module MetaMap = Map.Make(Meta) -(** Sets and maps of variables. *) -module Var = +(** Sets of term variables. *) +module VarSet = Set.Make( struct - type t = term Bindlib.var + type t = tvar let compare = Bindlib.compare_vars - end + end) -module VarSet = Set.Make(Var) -module VarMap = Map.Make(Var) +(** Maps over term variables. *) +module VarMap = Map.Make( + struct + type t = tvar + let compare = Bindlib.compare_vars + end) From d3672736d5890210346d8e890a00d1238fa03618 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 10 Apr 2020 16:29:51 +0200 Subject: [PATCH 64/66] Add missing comment. --- src/core/sr.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/core/sr.ml b/src/core/sr.ml index 3205d0ef6..b44c90911 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -38,6 +38,9 @@ let build_meta_type : int -> term = fun k -> done; Bindlib.unbox !res +(** [patt_to_tenv vars t] converts pattern variables of [t] into corresponding + term environment variables of [vars]. The index [i] in [Patt(Some(i),_,_)] + indicates the index of the corresponding variable in [vars]. *) let patt_to_tenv : term_env Bindlib.var array -> term -> tbox = fun vars -> let get_te i = match i with From 0cc857f3d7ce318b8c1933a04477870b00f4aea7 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 10 Apr 2020 16:35:16 +0200 Subject: [PATCH 65/66] Apply my own comment again. --- src/core/extra.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/core/extra.ml b/src/core/extra.ml index 2cd5599e3..3e20091d9 100644 --- a/src/core/extra.ml +++ b/src/core/extra.ml @@ -240,14 +240,13 @@ module List = in in_sorted (** [insert cmp x l] inserts [x] in the list [l] assuming that [l] is - sorted wrt [cmp]. *) + sorted wrt [cmp]. *) let insert : 'a cmp -> 'a -> 'a list -> 'a list = fun cmp x -> let rec insert acc l = match l with - | y :: m when cmp x y > 0 -> insert (y::acc) m - | _ -> List.rev_append acc (x::l) + | y :: l when cmp x y > 0 -> insert (y::acc) l + | _ -> List.rev_append acc (x::l) in insert [] - end module Array = From a0e1f3e92bff86cc29998d4fe1a8e96ed5cc00fd Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 10 Apr 2020 17:08:11 +0200 Subject: [PATCH 66/66] Added comment. --- src/core/sr.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/core/sr.ml b/src/core/sr.ml index b44c90911..7b179d92d 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -96,6 +96,9 @@ let symb_to_tenv : pre_rule Pos.loc -> sym list -> index_tbl -> term -> tbox = | Symb(f,_) when List.memq f syms -> let i = try Hashtbl.find htbl f.sym_name with Not_found -> + (* A symbol may also come from a metavariable that appeared in the + type of a metavariable that was replaced by a symbol. We do not + have concrete examples of that happening yet. *) fatal pos "Introduced symbol [%s] cannot be removed." f.sym_name in let (ts1, ts2) = List.cut ts arities.(i) in