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

fblanqui · Oct 30, 2024 · 6205012 · 6205012
2 parents 11a0004 + 3223066
commit 6205012
Show file tree

Hide file tree

Showing 9 changed files with 23 additions and 15 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -8,7 +8,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.1, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
+        ocaml-version: [5.2.0, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1]
     runs-on: ubuntu-latest
     steps:
       - name: checking out lambdapi repo ...

diff --git a/doc/commands.rst b/doc/commands.rst
@@ -128,14 +128,14 @@ the system with additional information on its properties and behavior.
     for every canonical term of the form ``f t u``, we have ``t ≤ u``,
     where ``≤`` is a total ordering on terms left unspecified.
 
-    If a symbol ``f`` is ``associative left`` then there is no
-    canonical term of the form ``f t (f u v)`` and thus every
-    canonical term headed by ``f`` is of the form ``f … (f (f t₁ t₂)
-    t₃) …  tₙ``. If a symbol ``f`` is ``associative`` or ``associative
-    right`` then there is no canonical term of the form ``f (f t u)
-    v`` and thus every canonical term headed by ``f`` is of the form
-    ``f t₁ (f t₂ (f t₃ … tₙ) … )``. Moreover, in both cases, if ``f``
-    is also ``commutative`` then we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``.
+    If a symbol ``f`` is ``commutative`` and ``associative left`` then
+    there is no canonical term of the form ``f t (f u v)`` and thus
+    every canonical term headed by ``f`` is of the form ``f … (f (f t₁
+    t₂) t₃) …  tₙ``. If a symbol ``f`` is ``commutative`` and
+    ``associative`` or ``associative right`` then there is no
+    canonical term of the form ``f (f t u) v`` and thus every
+    canonical term headed by ``f`` is of the form ``f t₁ (f t₂ (f t₃ …
+    tₙ) … )``. Moreover, in both cases, we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``.
 
 - **Exposition modifiers** define how a symbol can be used outside the
   module where it is defined. By default, the symbol can be used

diff --git a/editors/vscode/package.json b/editors/vscode/package.json
@@ -8,7 +8,7 @@
     "François Lefoulon <[email protected]>",
     "Ashish Barnawal <[email protected]>"
   ],
-  "version": "0.2.2",
+  "version": "0.2.3",
   "publisher": "Deducteam",
   "engines": {
     "vscode": "^1.82.0"

diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts
@@ -704,9 +704,8 @@ function sendGoalsRequest(position: Position, panel: WebviewPanel, docUri: Uri,
             return;
         }
         // Take focus back if the goal panel lost it.
-        window.showErrorMessage("Going through Goals");
         if(!panel.active) {
-            panel.reveal(2, false);
+            panel.reveal(2, true);
         }
 
         updateTerminalText(goals.logs);

diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml
@@ -145,6 +145,7 @@ let ind_data : popt -> Env.t -> term -> Sign.ind_data = fun pos env a ->
       begin
         try
           let ind = SymMap.find s !(sign.sign_ind) in
+          let _, ts = List.cut ts ind.ind_nb_params (*remove parameters*) in
           let ctxt = Env.to_ctxt env in
           if LibTerm.distinct_vars ctxt (Array.of_list ts) = None
           then fatal pos "%a is not applied to distinct variables." sym s

diff --git a/tests/OK/1141.lp b/tests/OK/1141.lp
@@ -0,0 +1,8 @@
+require open tests.OK.Set tests.OK.Prop tests.OK.Nat tests.OK.List;
+
+symbol sample_1 (list : 𝕃 nat) : π ⊤ ≔
+begin
+  induction
+    { apply ⊤ᵢ }
+    { assume x l ih; apply ih }
+end;
diff --git a/tests/OK/922.lp b/tests/OK/922.lp
@@ -20,5 +20,5 @@ with is0 (_ +1) ↪ false;
 
 opaque symbol s≠0 [n] : π (n +1 ≠ 0) ≔
 begin
-  assume n h; refine ind_eq h (λ n, istrue(is0 n)) top
+  assume n h; refine ind_eq h (λ n, istrue(is0 n)) ⊤ᵢ
 end;
diff --git a/tests/OK/Prop.lp b/tests/OK/Prop.lp
@@ -14,7 +14,7 @@ builtin "P" ≔ π;
 
 constant symbol ⊤ : Prop; // \top
 
-constant symbol top : π ⊤;
+constant symbol ⊤ᵢ : π ⊤;
 
 // false
 

diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
@@ -60,7 +60,7 @@ do
         # proofs
         why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit);;
         # "open"
-        triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215);;
+        triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141);;
         # "inductive"
         strictly_positive_*|inductive|989|904|830|341);;
         # underscore in query