WIP: Add opaque command (#1016)

* WIP add opaque command The opaque command allow to set a defined symbol opaque * Fix review comments * Make opaque symbol injective * Use bool ref for sym_opaque type * Fix warning and PR comment * Modify doc and BNF to mention opaque command * Remove modifier list for Inductive type Remove shift/reduce conflicts with opaque command, and property modifiers cannot be used on inductive types * Make possible to opacify symbol defined in another file * fix fold_command opaque case and modify scope_rule error message for opaque symbol * Update CHANGES.md * Add warning message if symbol is already opaque, and add exposition modifier for inductive type Inductive type can not use property modifiers but can use expositions modifiers: private, protected --------- Co-authored-by: Frédéric Blanqui <[email protected]>
Deducteam · Nov 23, 2023 · 5a3017d · 5a3017d
1 parent b905e6d
commit 5a3017d
Show file tree

Hide file tree

Showing 14 changed files with 92 additions and 18 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -3,6 +3,10 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## [Unreleased]
+
+- Add the command `opaque` that opacifies a symbol already defined.
+
 ## 2.4.1 (2023-11-22)
 
 ### Added

diff --git a/doc/commands.rst b/doc/commands.rst
@@ -287,6 +287,18 @@ and ``"+1"`` as follows:
    builtin "+1" ≔ succ; // : N → N
    type 42;
 
+.. _opaque:
+
+``opaque``
+---------------
+
+The command ``opaque`` allows to set opaque (see **Opacity modifier**) a previously defined symbol.
+
+::
+
+   symbol πᶜ p ≔ π (¬ ¬ p); // interpretation of classical propositions as types
+   opaque πᶜ;
+
 .. _rule:
 
 ``rule``

diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
@@ -18,15 +18,16 @@ QID ::= [UID "."]+ UID
 
 <search_query_alone> ::= <search_query> EOF
 
-<command> ::= "require" "open" <path>* ";"
+<command> ::= "opaque" <qid_or_nat> ";"
+            | "require" "open" <path>* ";"
             | "require" <path>* ";"
             | "require" <path> "as" <uid> ";"
             | "open" <path>* ";"
             | <modifier>* "symbol" <uid_or_nat> <param_list>* ":" <term>
               [<proof>] ";"
             | <modifier>* "symbol" <uid_or_nat> <param_list>* [":" <term>]
               "≔" <term_proof> ";"
-            | <modifier>* <param_list>* "inductive" <inductive> ("with"
+            | [<exposition>] <param_list>* "inductive" <inductive> ("with"
               <inductive>)* ";"
             | "rule" <rule> ("with" <rule>)* ";"
             | "builtin" <stringlit> "≔" <qid_or_nat> ";"
@@ -61,9 +62,11 @@ QID ::= [UID "."]+ UID
              | "constant"
              | "injective"
              | "opaque"
-             | "private"
-             | "protected"
              | "sequential"
+             | <exposition>
+
+<exposition> ::= "private"
+               | "protected"
 
 <uid> ::= UID
 

diff --git a/src/core/eval.ml b/src/core/eval.ml
@@ -220,7 +220,7 @@ and whnf_stk : config -> term -> stack -> term * stack = fun cfg t stk ->
   | (Symb s as h, stk) as r ->
     begin match !(s.sym_def) with
     | Some t ->
-      if s.sym_opaq || not cfg.Config.expand_defs then r else
+      if !(s.sym_opaq) || not cfg.Config.expand_defs then r else
         (Stdlib.incr steps; whnf_stk cfg t stk)
     | None when not cfg.Config.rewrite -> r
     | None ->
@@ -566,7 +566,7 @@ let unfold_sym : sym -> term -> term =
     in unfold_sym
   in
   fun s ->
-  if s.sym_opaq then fun t -> t else
+  if !(s.sym_opaq) then fun t -> t else
   match !(s.sym_def) with
   | Some d -> unfold_sym s (add_args d)
   | None ->

diff --git a/src/core/term.ml b/src/core/term.ml
@@ -95,7 +95,7 @@ and sym =
   ; sym_impl  : bool list (** Implicit arguments ([true] meaning implicit). *)
   ; sym_prop  : prop (** Property. *)
   ; sym_def   : term option ref (** Definition with ≔. *)
-  ; sym_opaq  : bool (** Opacity. *)
+  ; sym_opaq  : bool ref (** Opacity. *)
   ; sym_rules : rule list ref (** Rewriting rules. *)
   ; sym_mstrat: match_strat (** Matching strategy. *)
   ; sym_dtree : dtree ref (** Decision tree used for matching. *)
@@ -365,7 +365,7 @@ let create_sym : Path.t -> expo -> prop -> match_strat -> bool ->
     { elt = sym_name; pos = sym_pos } sym_decl_pos
     typ sym_impl ->
   {sym_path; sym_name; sym_type = ref typ; sym_impl; sym_def = ref None;
-   sym_opaq; sym_rules = ref []; sym_dtree = ref Tree_type.empty_dtree;
+   sym_opaq = ref sym_opaq; sym_rules = ref []; sym_dtree = ref Tree_type.empty_dtree;
    sym_mstrat; sym_prop; sym_expo; sym_pos ; sym_decl_pos }
 
 (** [is_constant s] tells whether [s] is a constant. *)
@@ -374,7 +374,7 @@ let is_constant : sym -> bool = fun s -> s.sym_prop = Const
 (** [is_injective s] tells whether [s] is injective, which is in partiular the
    case if [s] is constant. *)
 let is_injective : sym -> bool = fun s ->
-  match s.sym_prop with Const | Injec -> true | _ -> false
+  match s.sym_prop with Const | Injec -> true | _ -> !(s.sym_opaq)
 
 (** [is_private s] tells whether the symbol [s] is private. *)
 let is_private : sym -> bool = fun s -> s.sym_expo = Privat

diff --git a/src/core/term.mli b/src/core/term.mli
@@ -92,7 +92,7 @@ and sym =
   ; sym_impl  : bool list (** Implicit arguments ([true] meaning implicit). *)
   ; sym_prop  : prop (** Property. *)
   ; sym_def   : term option ref (** Definition with ≔. *)
-  ; sym_opaq  : bool (** Opacity. *)
+  ; sym_opaq  : bool ref (** Opacity. *)
   ; sym_rules : rule list ref (** Rewriting rules. *)
   ; sym_mstrat: match_strat (** Matching strategy. *)
   ; sym_dtree : dtree ref (** Decision tree used for matching. *)

diff --git a/src/export/dk.ml b/src/export/dk.ml
@@ -196,7 +196,7 @@ let sym_decl : sym pp = fun ppf s ->
           ident s.sym_name (term true) !(s.sym_type)
     end
   | Some d ->
-    if s.sym_opaq then
+    if !(s.sym_opaq) then
       out ppf "thm %a : %a := %a.@."
         ident s.sym_name (term true) !(s.sym_type) (term true) d
     else

diff --git a/src/handle/command.ml b/src/handle/command.ml
@@ -204,6 +204,11 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   Console.out 3 (Color.cya "%a") Pos.pp pos;
   Console.out 4 "%a" Pretty.command cmd;
   match elt with
+  | P_opaque qid ->
+    let s = Sig_state.find_sym ~prt:true ~prv:true ss qid in
+    if !(s.sym_opaq) then fatal pos "Symbol already opaque.";
+    s.sym_opaq := true;
+    (ss, None, None)
   | P_query(q) -> (ss, None, Query.handle ss None q)
   | P_require(b,ps) ->
       (List.fold_left (handle_require compile b) ss ps, None, None)

diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly
@@ -147,6 +147,7 @@ search_query_alone:
     { q }
 
 command:
+  | OPAQUE i=qid_or_nat SEMICOLON { make_pos $sloc (P_opaque i) }
   | REQUIRE OPEN l=list(path) SEMICOLON
     { make_pos $sloc (P_require(true,l)) }
   | REQUIRE l=list(path) SEMICOLON
@@ -167,9 +168,9 @@ command:
         {p_sym_mod=ms; p_sym_nam=s; p_sym_arg=al; p_sym_typ=ao;
          p_sym_trm=fst tp; p_sym_prf=snd tp; p_sym_def=true}
       in make_pos $sloc (P_symbol(sym)) }
-  | ms=modifier* xs=param_list* INDUCTIVE
+  | exp=exposition? xs=param_list* INDUCTIVE
     is=separated_nonempty_list(WITH, inductive) SEMICOLON
-      { make_pos $sloc (P_inductive(ms,xs,is)) }
+      { make_pos $sloc (P_inductive(Option.to_list exp,xs,is)) }
   | RULE rs=separated_nonempty_list(WITH, rule) SEMICOLON
       { make_pos $sloc (P_rules(rs)) }
   | BUILTIN s=STRINGLIT ASSIGN i=qid_or_nat SEMICOLON
@@ -225,9 +226,12 @@ modifier:
   | CONSTANT { make_pos $sloc (P_prop Term.Const) }
   | INJECTIVE { make_pos $sloc (P_prop Term.Injec) }
   | OPAQUE { make_pos $sloc P_opaq }
-  | PRIVATE { make_pos $sloc (P_expo Term.Privat) }
-  | PROTECTED { make_pos $sloc (P_expo Term.Protec) }
   | SEQUENTIAL { make_pos $sloc (P_mstrat Term.Sequen) }
+  | exp=exposition { exp }
+
+exposition:
+| PRIVATE { make_pos $sloc (P_expo Term.Privat) }
+| PROTECTED { make_pos $sloc (P_expo Term.Protec) }
 
 uid: s=UID { make_pos $sloc s}
 

diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
@@ -341,6 +341,7 @@ let command : p_command pp = fun ppf { elt; _ } ->
     end
   | P_unif_rule ur -> out ppf "unif_rule %a" unif_rule ur
   | P_coercion c -> out ppf "%a" (rule "coerce_rule") c
+  | P_opaque qid -> out ppf "opaque %a" qident qid
   end;
   out ppf ";"
 

diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
@@ -647,8 +647,8 @@ let scope_rule :
     fatal p_lhs.pos
       "Symbol %s has been declared constant, it cannot be used as the \
        head of a rewrite rule LHS." pr_sym.sym_name;
-  if pr_sym.sym_opaq || Timed.(!(pr_sym.sym_def)) <> None then
-    fatal p_lhs.pos "No rewriting rule can be given on a defined symbol.";
+  if Timed.(!(pr_sym.sym_opaq) || (!(pr_sym.sym_def) <> None)) then
+    fatal p_lhs.pos "No rewriting rule can be added on an opaque symbol or a symbol already defined with ≔";
   if pr_sym.sym_expo = Protec
     && ss.signature.sign_path <> pr_sym.sym_path then
     fatal p_lhs.pos "Cannot define rules on foreign protected symbols.";

diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
@@ -289,6 +289,7 @@ type p_command_aux =
   | P_unif_rule of p_rule
   | P_coercion of p_rule
   | P_query of p_query
+  | P_opaque of p_qident
 
 (** Parser-level representation of a single (located) command. *)
 type p_command = p_command_aux loc
@@ -617,6 +618,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
     | P_require_as (_, _)
     | P_open _ -> a
     | P_query q -> fold_query_vars StrSet.empty a q
+    | P_opaque qid
     | P_builtin (_, qid)
     | P_notation (qid, _) -> f a qid
     | P_coercion r

diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml
@@ -50,7 +50,7 @@ let is_ho : rule -> bool = fun r ->
 (** [is_definable s] says if [s] is definable and non opaque but not AC. *)
 let is_definable : sym -> bool = fun s ->
   (match s.sym_prop with Defin | Injec -> true | _ -> false)
-  && not s.sym_opaq
+  && not !(s.sym_opaq)
 
 (** [rule_of_def s d] creates the rule [s --> d]. *)
 let rule_of_def : sym -> term -> rule = fun s d ->

diff --git a/tests/OK/opaque.lp b/tests/OK/opaque.lp
@@ -0,0 +1,43 @@
+// Classical logic Gödel–Gentzen negative translation 
+constant symbol Prop : TYPE;
+
+builtin "Prop" ≔ Prop;
+
+injective symbol π : Prop → TYPE; // `p
+builtin "P" ≔ π;
+
+symbol ⊥: Prop;
+symbol a: Prop;
+
+constant symbol ⇒ : Prop → Prop → Prop; notation ⇒ infix right 5; // =>
+rule π ($p ⇒ $q) ↪ π $p → π $q;
+
+symbol ¬ p ≔ p ⇒ ⊥; notation ¬ prefix 35;
+
+constant symbol ∨ : Prop → Prop → Prop; notation ∨ infix left 6; // \/ or \vee
+constant symbol ∨ᵢ₁ [p q] : π p → π (p ∨ q);
+
+symbol πᶜ p ≔ π (¬ ¬ p);
+
+symbol ∨ᶜ p q ≔ (¬ ¬ p) ∨ (¬ ¬ q); notation ∨ᶜ infix right 20;
+
+opaque symbol ∨ᶜᵢ₁ [p q] : πᶜ p → πᶜ (p ∨ᶜ q) ≔
+begin
+    simplify;
+    assume p q Hnnp;
+    assume Hnnp_or_nnq;
+    apply Hnnp_or_nnq;
+    apply ∨ᵢ₁;
+    refine Hnnp;
+end;
+
+opaque πᶜ;
+opaque ∨ᶜ;
+
+opaque symbol ∨ᶜᵢ₁' [p q] : πᶜ p → πᶜ (p ∨ᶜ q) ≔
+begin
+    assume p q Hp;
+    simplify;
+    apply ∨ᶜᵢ₁;
+    apply Hp;
+end;