diff --git a/src/core/basics.ml b/src/core/basics.ml index 4c0a4890a..457b0f9ea 100644 --- a/src/core/basics.ml +++ b/src/core/basics.ml @@ -4,15 +4,11 @@ open Extra open Timed open Terms -(** 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) +(** [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.make n "_var_") (** [to_tvar t] returns [x] if [t] is of the form [Vari x] and fails otherwise. *) @@ -71,48 +67,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 @@ -178,13 +132,18 @@ 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 -> +(** [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 l = ref [] in - iter_meta b (fun m -> l := m :: !l) t; - List.sort_uniq cmp_meta !l + 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. *) @@ -209,29 +168,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 @@ -240,7 +176,8 @@ let nl_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 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/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 diff --git a/src/core/extra.ml b/src/core/extra.ml index a982078ad..3e20091d9 100644 --- a/src/core/extra.ml +++ b/src/core/extra.ml @@ -239,6 +239,14 @@ module List = | _ -> false in in_sorted + (** [insert cmp x l] inserts [x] in the list [l] assuming that [l] is + sorted wrt [cmp]. *) + let insert : 'a cmp -> 'a -> 'a list -> 'a list = fun cmp x -> + let rec insert acc l = + match l with + | y :: l when cmp x y > 0 -> insert (y::acc) l + | _ -> List.rev_append acc (x::l) + in insert [] end module Array = diff --git a/src/core/handle.ml b/src/core/handle.ml index 4619cebe6..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; 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/infer.ml b/src/core/infer.ml index 655f1e64a..e1e9c7126 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 @@ -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. *) @@ -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 ----------------------------------------- @@ -127,54 +135,16 @@ let rec infer : ctxt -> term -> term = fun ctx t -> (* ctx ⊢ term_of_meta m e ⇒ a ---------------------------- 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) + | 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] 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; - 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]. @@ -187,8 +157,8 @@ 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; - List.iter (log_infr " assuming %a" pp_constr) constrs; + log_infr (gre "infer %a : %a") pp t pp a; + List.iter (log_infr " if %a" pp_constr) constrs; end; Stdlib.(constraints := []); (a, constrs) @@ -204,8 +174,8 @@ 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; - List.iter (log_infr " assuming %a" pp_constr) constrs; + log_infr (gre "check %a : %a") pp t pp c; + List.iter (log_infr " if %a" pp_constr) constrs; end; Stdlib.(constraints := []); constrs 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/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/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/rewrite.ml b/src/core/rewrite.ml index 6cb0fffe3..d8117bdcf 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. 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 occurrence checking. *) +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, @@ -165,7 +210,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) @@ -198,7 +243,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 @@ -218,7 +263,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/scope.ml b/src/core/scope.ml index b13878baa..e413054d3 100644 --- a/src/core/scope.ml +++ b/src/core/scope.ml @@ -39,9 +39,9 @@ let open_sign : sig_state -> Sign.t -> sig_state = fun ss sign -> 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 @@ -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 = @@ -132,25 +129,37 @@ 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 = - | 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 bool * m_lhs_data (** 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 - allowed. *) - | 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.sym_exposition.Private} 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]. *) @@ -182,11 +191,26 @@ 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 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 - 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. *) @@ -194,9 +218,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 @@ -239,15 +263,22 @@ 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(_,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 @@ -275,21 +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(_) ) -> fresh_patt 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 [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 - _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. *) @@ -306,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,_) ) -> + | (P_Patt(id,ts) , M_LHS(_,d) ) -> (* Check that [ts] are variables. *) let scope_var t = match unfold (Bindlib.unbox (scope env t)) with @@ -324,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; - _Patt None (fresh_patt_name ()) (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(_,_) , _ ) -> @@ -472,15 +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 check [nl = []] here. *) 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 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 -> @@ -489,44 +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; - (* 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. *) - 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. *) - (* 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 lhs = Bindlib.unbox (scope (M_LHS(map, prv)) 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 scope the RHS and bind the meta-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 - 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] to facilitate confluence / termination checking. *) - let vars = 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}) + 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 7fe610ed1..7b179d92d 100644 --- a/src/core/sr.ml +++ b/src/core/sr.ml @@ -1,45 +1,22 @@ (** 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" 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”. *) +(** [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 @@ -48,7 +25,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) @@ -61,38 +38,23 @@ 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 -> 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 - 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. *) +(** [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 + | None -> assert false (* Cannot appear in LHS. *) + | Some(i) -> try vars.(i) with Invalid_argument(_) -> assert false + in + 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 0 a) (Bindlib.bind_var x (to_m 0 t)) - | Appl(t,u) -> _Appl (to_m (k+1) t) (to_m 0 u) - | Patt(i,n,a) -> - begin - let a = Array.map (to_m 0) a in - let l = Array.length a in - match i with - | None -> - let m = fresh_meta ~name:n (build_meta_type (l+k)) l in - _Meta m a - | Some(i) -> - match metas.(i) with - | Some(m) -> _Meta m a - | None -> - let m = fresh_meta ~name:n (build_meta_type (l+k)) l in - metas.(i) <- Some(m); - _Meta m a - end + | 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. *) @@ -102,50 +64,187 @@ 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 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 e = Array.map _Vari xs in - TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m e))) + 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 -> + (* 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 + (_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(_,_) -> + 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 + +(** [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 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 - let te_envs = Array.map fn metas in - let rhs = Bindlib.msubst r.elt.rhs te_envs in - (* Infer the type of the LHS and the constraints. *) - match Typing.infer_constr builtins [] lhs with - | None -> wrn r.pos "Untypable LHS." + (* 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 bmap [] lhs_typing with + | None -> fatal pos "The LHS is not typable." | 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 + log_subj (gre "LHS has type %a") pp ty_lhs; + 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; - (* Turn constraints into a substitution and apply it. *) - let (xs,ts) = subst_from_constrs lhs_constrs in - let p = Bindlib.box_pair (lift rhs) (lift ty_lhs) in - let p = Bindlib.unbox (Bindlib.bind_mvar xs p) in - let (rhs,ty_lhs) = Bindlib.msubst p ts in - (* Check that the RHS has the same type as the LHS. *) - let to_solve = Infer.check [] rhs ty_lhs in - if !log_enabled && to_solve <> [] then + (* 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 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 = + match !(m.meta_value) with + | Some(_) -> + (* Instantiate recursively the meta-variables of the definition. *) + let t = Meta(m, Array.make m.meta_arity Kind) in + 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 + Array.iter instantiate metas; Stdlib.(!symbols) + in + (* Compute the constraints for the RHS to have the same type as the LHS. *) + let to_solve = Infer.check [] rhs_typing ty_lhs in + if !log_enabled then begin - log_subj "RHS has type [%a]" pp ty_lhs; - List.iter (log_subj " if %a" pp_constr) to_solve + log_subj (gre "RHS has type %a") pp ty_lhs; + 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; - (* 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) + (* 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 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) = - (* 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 @@ -155,13 +254,13 @@ 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 type preservation for a rewriting rule." end; - (* 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 - fatal r.pos "Cannot instantiate all metavariables in rule [%a]." - pp_rule (s,h,r.elt) - in - Basics.iter_meta false f rhs + (* Replace metavariable symbols by term_env variables, and bind them. *) + 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/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..fd3c2a445 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 rules 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 @@ -137,14 +137,16 @@ 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. *) - ; vars : (string * int) array - (** Name and arity of the pattern variables bound in the RHS. *) } + ; 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 (on which the rule is defined) applied to a list of pattern arguments. The @@ -184,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. *) @@ -242,12 +244,6 @@ 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 - -(** Equality on metavariables. *) -let eq_meta : meta -> meta -> bool = fun m1 m2 -> m1.meta_key = m2.meta_key - (** [symb s] returns the term [Symb (s, Nothing)]. *) let symb : sym -> term = fun s -> Symb (s, Nothing) @@ -298,27 +294,28 @@ 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 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) - -(** [internal m] returns [true] if [m] is unnamed (i.e., not user-defined). *) -let internal : meta -> bool = fun m -> m.meta_name = None + 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 -> - 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 @@ -455,3 +452,45 @@ 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) + +(** [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 + let compare m1 m2 = m1.meta_key - m2.meta_key +end + +module MetaSet = Set.Make(Meta) +module MetaMap = Map.Make(Meta) + +(** Sets of term variables. *) +module VarSet = Set.Make( + struct + type t = tvar + let compare = Bindlib.compare_vars + end) + +(** Maps over term variables. *) +module VarMap = Map.Make( + struct + type t = tvar + let compare = Bindlib.compare_vars + end) 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/typing.ml b/src/core/typing.ml index 8317aea32..4de0b79fc 100644 --- a/src/core/typing.ml +++ b/src/core/typing.ml @@ -11,14 +11,11 @@ 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) -> - 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 @@ -28,7 +25,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] @@ -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 diff --git a/src/core/unif.ml b/src/core/unif.ml index c01d1ed5d..54e0db76c 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -33,18 +33,80 @@ 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 +(** [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 + (* 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) + 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 (!can_instantiate || internal m) && not (occurs m u) then - match nl_distinct_vars ctx ts with - | None -> None - | Some(vs) -> Some (Bindlib.bind_mvar vs (lift u)) + if not (occurs m u) then + match nl_distinct_vars ctx ts with (* Theoretical justification ? *) + | None -> None + | 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 @@ -52,7 +114,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 @@ -103,7 +168,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 @@ -261,7 +326,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 @@ -270,8 +335,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 () @@ -340,16 +404,23 @@ 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 - - | (_ , _ ) -> error () - -(** [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; + | (Symb(s,_) , _ ) when not (is_constant s) -> solve_inj s ts1 t2 + | (_ , Symb(s,_) ) when not (is_constant s) -> solve_inj s ts2 t1 + + (* 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]. 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 diff --git a/src/core/why3_tactic.ml b/src/core/why3_tactic.ml index bc77d5737..33e1c5e4e 100644 --- a/src/core/why3_tactic.ml +++ b/src/core/why3_tactic.ml @@ -89,7 +89,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 (Basics.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 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) ≔ diff --git a/tests/OK/273.lp b/tests/OK/273.lp index 61fefbb53..c44d6786a 100644 --- a/tests/OK/273.lp +++ b/tests/OK/273.lp @@ -11,7 +11,7 @@ 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 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/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) diff --git a/tests/OK/330.lp b/tests/OK/330.lp new file mode 100644 index 000000000..0e2d05465 --- /dev/null +++ b/tests/OK/330.lp @@ -0,0 +1,9 @@ +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 + +rule prf (equals &x &y) → ∀ P, prf (P &x) ⇒ prf (P &y) diff --git a/tests/OK/330b.lp b/tests/OK/330b.lp new file mode 100644 index 000000000..a45bee83f --- /dev/null +++ b/tests/OK/330b.lp @@ -0,0 +1,8 @@ +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 + +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/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 ;) diff --git a/tests/OK/append.lp b/tests/OK/append.lp index e44c550a3..3c6536d75 100644 --- a/tests/OK/append.lp +++ b/tests/OK/append.lp @@ -1,14 +1,6 @@ -/// 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 @@ -24,10 +16,3 @@ symbol append : ∀ (n:Nat) (m:Nat), Vec n ⇒ Vec m ⇒ Vec (plus n m) 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 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 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