From 7dab18549208ccf89271ac054b4572939ee1b5e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 21 Feb 2024 16:38:47 +0100 Subject: [PATCH] do not keep definition of opaque symbols only (fix #1035) (#1051) --- src/core/inverse.ml | 18 +++++++++--------- src/handle/command.ml | 15 ++++++--------- tests/OK/1035.lp | 18 ++++++++++++++++++ 3 files changed, 33 insertions(+), 18 deletions(-) create mode 100644 tests/OK/1035.lp diff --git a/src/core/inverse.ml b/src/core/inverse.ml index 4ddd9217e..e5fd0a084 100644 --- a/src/core/inverse.ml +++ b/src/core/inverse.ml @@ -7,8 +7,8 @@ open Print open Lplib (** Logging function for unification. *) -let log_inv = Logger.make 'v' "invr" "inverse" -let log_inv = log_inv.pp +let log = Logger.make 'v' "invr" "inverse" +let log = log.pp (** [cache f s] is equivalent to [f s] but [f s] is computed only once unless the rules of [s] are changed. *) @@ -23,10 +23,10 @@ let cache : (sym -> 'a) -> (sym -> 'a) = fun f -> (** [const_graph s] returns the list of pairs [(s0,s1)] such that [s] has a rule of the form [s (s0 ...) ↪ s1 ...]. *) let const_graph : sym -> (sym * sym) list = fun s -> - if Logger.log_enabled () then log_inv "check rules of %a" sym s; + if Logger.log_enabled () then log "check rules of %a" sym s; let add s0 s1 l = if Logger.log_enabled () then - log_inv (Color.yel "%a %a ↪ %a") sym s sym s0 sym s1; + log (Color.yel "%a %a ↪ %a") sym s sym s0 sym s1; (s0,s1)::l in let f l rule = @@ -61,12 +61,12 @@ let inverse_const : sym -> sym -> sym = fun s s' -> a rule of the form [s (s0 _ _) ↪ Π x:s1 _, s2 r] with [b=true] iff [x] occurs in [r]. *) let prod_graph : sym -> (sym * sym * sym * bool) list = fun s -> - if Logger.log_enabled () then log_inv "check rules of %a" sym s; + if Logger.log_enabled () then log "check rules of %a" sym s; let add (s0,s1,s2,b) l = if Logger.log_enabled () then - if b then log_inv (Color.yel "%a (%a _ _) ↪ Π x:%a _, %a _[x]") + if b then log (Color.yel "%a (%a _ _) ↪ Π x:%a _, %a _[x]") sym s sym s0 sym s1 sym s2 - else log_inv (Color.yel "%a (%a _ _) ↪ %a _ → %a _") + else log (Color.yel "%a (%a _ _) ↪ %a _ → %a _") sym s sym s0 sym s1 sym s2; (s0,s1,s2,b)::l in @@ -119,7 +119,7 @@ let inverse_prod : sym -> sym -> sym * sym * sym * bool = fun s s' -> (** [inverse s v] tries to compute a term [u] such that [s(u)] reduces to [v]. @raise [Not_found] otherwise. *) let rec inverse : sym -> term -> term = fun s v -> - if Logger.log_enabled () then log_inv "compute %a⁻¹(%a)" sym s term v; + if Logger.log_enabled () then log "compute %a⁻¹(%a)" sym s term v; match get_args v with | Symb s', [t] when s' == s -> t | Symb s', ts -> add_args (mk_Symb (inverse_const s s')) ts @@ -143,5 +143,5 @@ let rec inverse : sym -> term -> term = fun s v -> let inverse : sym -> term -> term = fun s v -> let t = inverse s v in let v' = mk_Appl(mk_Symb s,t) in if Eval.eq_modulo [] v' v then t - else (if Logger.log_enabled() then log_inv "%a ≢ %a@" term v' term v; + else (if Logger.log_enabled() then log "%a ≢ %a@" term v' term v; raise Not_found) diff --git a/src/handle/command.ml b/src/handle/command.ml index 25bb420bb..c4631c04b 100644 --- a/src/handle/command.ml +++ b/src/handle/command.ml @@ -416,7 +416,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = (* Verify modifiers. *) let prop, expo, mstrat = handle_modifiers p_sym_mod in let opaq = List.exists Syntax.is_opaq p_sym_mod in - let pdata_prv = expo = Privat || (p_sym_def && opaq) in + let pdata_prv = opaq || expo = Privat in (match p_sym_def, opaq, prop, mstrat with | false, true, _, _ -> fatal pos "Symbol declarations cannot be opaque." | true, _, Const, _ -> fatal pos "Definitions cannot be constant." @@ -515,9 +515,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = wrn pe.pos "Proof admitted."; (* Keep the definition only if the symbol is not opaque. *) let d = - if pdata_prv then None - else - Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term + if opaq then None + else Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term in (* Add the symbol in the signature. *) fst (Sig_state.add_symbol @@ -526,12 +525,10 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = (* Check that the proof is indeed finished. *) if not (finished ps) then fatal pe.pos "The proof is not finished:@.%a" goals ps; - (* Keep the definition only if the symbol is not private and not - opaque. *) + (* Keep the definition only if the symbol is not opaque. *) let d = - if pdata_prv then None - else - Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term + if opaq then None + else Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term in (* Add the symbol in the signature. *) Console.out 2 (Color.red "symbol %a : %a") uid id term a; diff --git a/tests/OK/1035.lp b/tests/OK/1035.lp new file mode 100644 index 000000000..ba1a60078 --- /dev/null +++ b/tests/OK/1035.lp @@ -0,0 +1,18 @@ +symbol Set:TYPE; +injective symbol τ:Set → TYPE; +symbol ℕ:TYPE; +symbol 0:ℕ; +symbol 𝑰 [a]: ℕ → τ a; + +symbol code_S' : Set; +symbol S' ≔ τ code_S'; +//print S'; +//debug +uv; +symbol a':S' ≔ 𝑰 0; +//debug -uv; + +private symbol code_S : Set; +private symbol S ≔ τ code_S; +//print S; +//debug +uv; +private symbol a: S ≔ 𝑰 0;