Merge remote-tracking branch 'dk/master' into db

CHANGES.md

@@ -3,6 +3,26 @@ 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
+
+- support for Pratter 3.0.0
+- printing of unification and coercion rules
+
+### Improved
+
+- unification
+
+### Fixed
+
+- Coq export
+- matita.sh script
+
 ## 2.4.0 (2023-07-28)
 
 ### Added

Makefile

@@ -1,16 +1,6 @@
 VIMDIR = $(HOME)/.vim
 EMACS  = $(shell which emacs)
 
-LIB_ROOT := $(shell\
-  if test -n "$(LAMBDAPI_LIB_ROOT)";\
-  then echo $(LAMBDAPI_LIB_ROOT);\
-  else\
-    if test -n "$(OPAM_SWITCH_PREFIX)";\
-    then echo $(OPAM_SWITCH_PREFIX);\
-    else echo /usr/local;\
-    fi;\
-  fi)/lib/lambdapi/lib_root
-
 #### Compilation (binary, library and documentation) #########################
 
 .PHONY: default
@@ -35,7 +25,7 @@ bnf:
 #### Unit tests and sanity check #############################################
 
 .PHONY: tests
-tests: lambdapi $(LIB_ROOT)
+tests: lambdapi
 	@dune runtest
 	@dune exec --only-packages lambdapi -- tests/runtests.sh
 	@dune exec --only-packages lambdapi -- tests/dtrees.sh
@@ -123,11 +113,8 @@ fullclean: distclean
 
 #### Installation and release targets ########################################
 
-$(LIB_ROOT):
-	mkdir -p $@
-
 .PHONY: install
-install: install_lambdapi $(LIB_ROOT)
+install: install_lambdapi
 
 .PHONY: uninstall
 uninstall: uninstall_lambdapi

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``

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
 

dune-project

@@ -63,7 +63,7 @@ the Why3 platform.")
   (timed (>= 1.0))
   (pratter (and (>= 3.0.0) (< 4)))
   (camlp-streams (>= 5.0))
-  (why3 (and (>= 1.6.0) (< 1.7~)))
+  (why3 (and (>= 1.6.0) (< 1.8~)))
   (yojson (>= 1.6.0))
   (cmdliner (>= 1.1.0))
   (stdlib-shims (>= 0.1.0))

lambdapi.opam

@@ -58,7 +58,7 @@ depends: [
   "timed" {>= "1.0"}
   "pratter" {>= "3.0.0" & < "4"}
   "camlp-streams" {>= "5.0"}
-  "why3" {>= "1.6.0" & < "1.7~"}
+  "why3" {>= "1.6.0" & < "1.8~"}
   "yojson" {>= "1.6.0"}
   "cmdliner" {>= "1.1.0"}
   "stdlib-shims" {>= "0.1.0"}

src/cli/dune

@@ -4,4 +4,4 @@
  (modes byte native)
  (modules :standard)
  (libraries cmdliner lambdapi.lsp lambdapi.tool lambdapi.handle
-            lambdapi.export))
+            lambdapi.export unix))

src/core/dune

@@ -10,4 +10,4 @@
  (public_name lambdapi.core)
  (synopsis "LambdaPi interactive theorem prover [core]")
  (modules :standard)
- (libraries lambdapi.common lambdapi.lplib pratter why3))
+ (libraries lambdapi.common lambdapi.lplib pratter why3 unix))

src/core/eval.ml

@@ -222,7 +222,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 ->
@@ -559,7 +559,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 ->

src/core/term.ml

@@ -127,7 +127,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. *)
@@ -231,7 +231,7 @@ let create_sym : Path.t -> expo -> prop -> match_strat -> bool ->
   fun sym_path sym_expo sym_prop sym_mstrat sym_opaq
     { 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. *)
@@ -240,7 +240,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

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. *)

src/export/dk.ml

@@ -188,7 +188,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

src/handle/command.ml

@@ -184,6 +184,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)

src/handle/rewrite.ml

@@ -158,22 +158,19 @@ let matches : term -> term -> bool =
     match l with
     | [] -> ()
     | (p,t)::l ->
+      if Term.cmp p t = 0 then eq l else begin
       let hp, ps, k = get_args_len p and ht, ts, n = get_args_len t in
       if Logger.log_enabled() then
         log_rewr "matches %a %a ≡ %a %a"
           term hp (D.list term) ps term ht (D.list term) ts;
       match hp with
-      | Wild -> assert false
-      | Meta _ -> assert false
-      | Patt _ -> assert false
+      | Wild -> assert false (* used in user syntax only *)
+      | Patt _ -> assert false (* used in rules only *)
+      | Plac _ -> assert false (* used in scoping only *)
+      | Appl _ -> assert false (* not possible after get_args_len *)
+      | Type -> assert false (* not possible because of typing *)
+      | Kind -> assert false (* not possible because of typing *)
       | Db _ -> assert false
-      | Plac _ -> assert false
-      | Appl _ -> assert false
-      | Prod _ -> assert false
-      | Abst _ -> assert false
-      | LLet _ -> assert false
-      | Type -> assert false
-      | Kind -> assert false
       | TRef r ->
         if k > n then raise Not_equal;
         let ts1, ts2 = List.cut ts (n-k) in
@@ -182,7 +179,12 @@ let matches : term -> term -> bool =
           log_rewr (Color.red "<TRef> ≔ %a") term u;
         r := Some u;
         eq (List.fold_left2 (fun l pi ti -> (pi,ti)::l) l ps ts2)
-      | _ ->
+      | Meta _
+      | Prod _
+      | Abst _
+      | LLet _
+      | Symb _
+      | Vari _ ->
         if k <> n then raise Not_equal;
         let add_args l =
           List.fold_left2 (fun l pi ti -> (pi,ti)::l) l ps ts in
@@ -192,6 +194,7 @@ let matches : term -> term -> bool =
         | _ ->
           if Logger.log_enabled() then log_rewr "distinct heads";
           raise Not_equal
+      end
   in
   fun p t ->
     try

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}
 

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 ";"
 

src/parsing/scope.ml

@@ -569,8 +569,9 @@ 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." sym.sym_name;
-  if sym.sym_opaq || Timed.(!(sym.sym_def)) <> None then
-    fatal rule_pos "No rewriting rule can be given on a defined symbol.";
+  if Timed.(!(sym.sym_opaq) || !(sym.sym_def) <> None) then
+    fatal rule_pos "No rewriting rule can be added on an opaque symbol or \
+                    a symbol already defined with ≔.";
   if sym.sym_expo = Protec
     && ss.signature.sign_path <> sym.sym_path then
     fatal p_lhs.pos "Cannot define rules on foreign protected symbols.";

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

src/tool/dune

@@ -2,7 +2,7 @@
  (name tool)
  (public_name lambdapi.tool)
  (modules :standard)
- (libraries lambdapi.parsing lambdapi.core dream)
+ (libraries lambdapi.parsing lambdapi.core dream unix)
  (preprocess (pps lwt_ppx)))
 
 (rule

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 rhs ->

tests/OK/1026.lp

@@ -0,0 +1,31 @@
+symbol Prop: TYPE;
+symbol π: Prop → TYPE;
+symbol Set: TYPE;
+constant symbol τ: Set → TYPE;
+builtin "T" ≔ τ;
+builtin "P" ≔ π;
+
+symbol = [a:Set] : τ a → τ a → Prop;
+
+notation = infix 10;
+
+constant symbol eq_refl [a:Set] (x:τ a) : π (x = x);
+constant symbol ind_eq [a:Set] [x y:τ a] : π (x = y) → Π p, π (p y) → π (p x);
+
+builtin "eq"    ≔ =;
+builtin "refl"  ≔ eq_refl;
+builtin "eqind" ≔ ind_eq;
+
+symbol set: Set;
+symbol cset [T]: (τ T → Prop) → τ set;
+
+symbol T: Set;
+symbol P: τ T → Prop;
+symbol U: τ set;
+symbol Q: τ set → Prop;
+symbol th: π (cset (λ x, P x) = U) → π (Q U) → π (Q (cset (λ x, P x))) ≔
+begin
+  assume h1 h2;
+  rewrite h1;
+  apply h2;
+end;