diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2014-12-30 14:06:39 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2014-12-30 14:06:39 +0000 |
commit | b75bf02626b639bad8fe28796b7ee9163fd54323 (patch) | |
tree | c56e1abd9fe17c143d32f95d63f10701c707ed3f /coq | |
parent | a9660f46b64132dec0d0efc8ff4419ec8899558b (diff) |
fixed indentation (lexing of 'with') + made local coq-load-path.
Diffstat (limited to 'coq')
-rw-r--r-- | coq/TODO | 3 | ||||
-rw-r--r-- | coq/coq-compile-common.el | 2 | ||||
-rw-r--r-- | coq/coq-indent.el | 8 | ||||
-rw-r--r-- | coq/coq-smie.el | 8 | ||||
-rw-r--r-- | coq/ex/indent.v | 99 |
5 files changed, 76 insertions, 44 deletions
@@ -49,3 +49,6 @@ Proof with intro. +** dealing with several project files. + + diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index a66f68c8..a3c08feb 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -293,6 +293,8 @@ directory (see `coq-load-path-include-current')." :safe 'coq-load-path-safep :group 'coq-auto-compile) +(make-variable-buffer-local 'coq-load-path) + (defcustom coq-compile-auto-save 'ask-coq "Buffers to save before checking dependencies for compilation. There are two orthogonal choices: Firstly one can save all or only the coq diff --git a/coq/coq-indent.el b/coq/coq-indent.el index fc229d6e..352931c0 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -327,6 +327,7 @@ command end regexp." (not (coq-empty-command-p))) nil) (and + (message "ICI") (goto-char foundend) (proof-buffer-syntactic-context)))) ;; go back as far as possible before the start of the current @@ -367,11 +368,8 @@ and return nil." (re-search-backward proof-script-command-end-regexp limit 'dummy) (match-beginning 1))) (setq next-pos (- (match-end 0) 1)) - (or (if (or (string-equal (match-string 1) "}") - (string-equal (match-string 1) "{") - (string-equal (match-string 1) "-") - (string-equal (match-string 1) "+") - (string-equal (match-string 1) "*")) + (or (if (not (or (string-equal (match-string 1) ".") + (string-equal (match-string 1) "..."))) (save-excursion (goto-char (match-beginning 1)) (not (coq-empty-command-p))) diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 3d2d421c..6d84b686 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -10,6 +10,11 @@ ;;; Commentary: ;; Lexer. + +;; Due to the verycomplex grammar of Coq, and to the architecture of +;; smie, we deambiguate all kinds of tokens during lexing. This is a +;; complex piece of code but it allows for all smie goodies. +;; Some examples of deambigations: ;; - We distinguish ":=" from ":= inductive" to avoid the circular precedence ;; constraint ":= < | < ; < :=" where ":= < |" is due to Inductive ;; definitions, "| < ;" is due to tactics precedence, "; < :=" is due to @@ -139,6 +144,7 @@ the token of \".\" is simply \".\"." (coq-smie-find-unclosed-match-backward) (coq-smie-find-unclosed-match-backward))))) +;; point supposed to be at start of the "with" (defun coq-smie-with-deambiguate() (let ((p (point))) (if (coq-smie-find-unclosed-match-backward) @@ -147,7 +153,7 @@ the token of \".\" is simply \".\"." (coq-find-real-start) (cond ((looking-at "\\(Co\\)?Inductive") "with inductive") - ((looking-at "\\(Co\\)?Fixpoint\\|Function\\|Program") "with fixpoint") + ((looking-at "\\(Co\\)?Fixpoint\\|Function\\|Program\\|Lemma") "with fixpoint") ((looking-at "Module\\|Declare") "with module") (t "with"))))) diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 6644df83..cd263810 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -9,7 +9,7 @@ Record a : Type := make_a { aa : nat }. -{ +Module foo. Inductive test : nat -> Prop := | C1 : forall n, test n | C2 : forall n, test n @@ -17,21 +17,34 @@ Record a : Type := make_a { | C4 : forall n, test n. Inductive test2 : nat -> Prop - := C1 : forall n, test n - | C2 : forall n, test n - | C3 : forall n, test n - | C4 : forall n, test n. + := C21 : forall n, test2 n + | C22 : forall n, test2 n + | C23 : forall n, test2 n + | C24 : forall n, test2 n. + + Inductive test' : nat -> Prop := + | C1' : forall n, test' n + | C2' : forall n, test' n + | C3' : forall n, test' n + | C4' : forall n, test' n + with + test2' : nat -> Prop := + C21' : forall n, test2' n + | C22' : forall n, test2' n + | C23' : forall n, test2' n + | C24' : forall n, test2' n. - Let x : = 1. Let y := 2. + Let x := 1. Let y := 2. - Let y := (1, 2, 3, - 4, 5). + Let y2 := (1, 2, 3, + 4, 5). Inductive test3 (* fixindent *) : nat -> Prop - := C1 : forall n, test n - | C2 : forall n, test n -} + := C31 : forall n, test3 n + | C32 : forall n, test3 n. + +End foo. Lemma toto:nat. Proof. @@ -40,7 +53,7 @@ Proof. }} Qed. -Let x (* Precedence of "else" w.r.t "," and "->"! *) +Let xxx (* Precedence of "else" w.r.t "," and "->"! *) : if true then nat * nat else nat -> nat := (if true then 1 else 2, @@ -49,6 +62,7 @@ Let x (* Precedence of "else" w.r.t "," and "->"! *) Module Y. Lemma L : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x. Proof with auto with arith. + intros x. induction x;simpl;intros... Qed. Lemma L2 : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x. @@ -63,6 +77,13 @@ Module Y. intros. auto with arith. Qed. + + Lemma L' : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x + with L'' : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x. + Proof with auto with arith. + - induction x;simpl;intros... + - induction x;simpl;intros... + Qed. End Y. Function div2 (n : nat) {struct n}: nat := @@ -87,26 +108,26 @@ Module M1. Qed. Lemma l6: forall n:nat, n = n. intros. - Lemma l7: forall n:nat, n = n. + Lemma l7: forall n:nat, n = n. destruct n. - BeginSubproof. + { auto. - EndSubproof. - BeginSubproof. + } + { destruct n. - BeginSubproof. + { auto. - EndSubproof. + } auto. - EndSubproof. + } Qed. - BeginSubproof. + { destruct n. - BeginSubproof. - auto. EndSubproof. - BeginSubproof. auto. - EndSubproof. - EndSubproof. + { + auto. } + { auto. + } + } Qed. End M2. End M1. @@ -114,10 +135,10 @@ End M1. Module M1'. Module M2'. - Lemma l6: forall n:nat, n = n. + Lemma l6: forall n:nat, n = n. Proof. intros. - Lemma l7: forall n:nat, n = n. + Lemma l7: forall n:nat, n = n. Proof. destruct n. { @@ -142,7 +163,7 @@ Module M1'. End M2'. End M1'. - +(* TODO: add multichar bullets once coq 8.5 is out *) Module M4'. Module M2'. Lemma l6: forall n:nat, n = n. @@ -156,7 +177,9 @@ Module M4'. + idtac;[ auto ]. - + auto. + + destruct n. + * auto. + * auto. Qed. {destruct n. - auto. @@ -180,13 +203,13 @@ Module M1''. End M1''. -Record rec:Set := { +Record rec:Set := { fld1:nat; fld2:nat; fld3:bool }. -Class cla {X:Set}:Set := { +Class cla {X:Set}:Set := { cfld1:nat; cld2:nat; cld3:bool @@ -201,8 +224,8 @@ Module X. exists r':rec, r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1). Proof. - intros r. - { exists + intros r. + { exists {| fld1:=r.(fld2); fld2:=r.(fld1); @@ -223,10 +246,10 @@ Module X. /\ r.(fld2) = r'.(fld1). Proof. - intros r. + intros r. {{ idtac; - exists + exists {| fld1:=r.(fld2); fld2:=r.(fld1); @@ -235,7 +258,7 @@ Module X. (* ltac *) match goal with | _:rec |- ?a /\ ?b => split - | _ => fail + | _ => fail end. { simpl. auto. } { simpl. auto. }}} @@ -247,7 +270,7 @@ Generalizable All Variables. Open Local Scope signature_scope. Require Import RelationClasses. -Module foo. +Module TC. Instance: (@RewriteRelation nat) impl. (* No goal created *) Definition XX := 0. @@ -277,7 +300,7 @@ Module foo. intuition ; specialize (H x0) ; intuition. Qed. -End foo. +End TC. Require Import Sets.Ensembles. Require Import Bool.Bvector. |