diff options
| -rw-r--r-- | doc/memo-v8.tex | 53 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 10 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 2 | ||||
| -rw-r--r-- | translate/ppconstrnew.ml | 15 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 43 |
5 files changed, 63 insertions, 60 deletions
diff --git a/doc/memo-v8.tex b/doc/memo-v8.tex index a04381200..23e5b6708 100644 --- a/doc/memo-v8.tex +++ b/doc/memo-v8.tex @@ -8,7 +8,7 @@ \usepackage{fullpage} \author{B.~Barras} -\title{A introduction to syntax of Coq V8} +\title{An introduction to syntax of Coq V8} %% Le _ est un caractère normal \catcode`\_=13 @@ -47,8 +47,8 @@ The lexical conventions changed: \TERM{_} is not a regular identifier anymore. It is used in terms as a placeholder for subterms to be inferred at type-checking, and in patterns as a non-binding variable. -Furthermore, only letters, digits, single quotes and _ are allowed -after the first character. +Furthermore, only letters (unicode letters), digits, single quotes and +_ are allowed after the first character. \subsection{Quoted string} @@ -75,15 +75,17 @@ in many contexts. \subsection{Arithmetics and scopes} -The specialized notation for \TERM{Z} and \TERM{R} (introduced by symbols \TERM{`} and \TERM{``}) have disappeared. They have been replaced by the general notion of scope. +The specialized notation for \TERM{Z} and \TERM{R} (introduced by +symbols \TERM{`} and \TERM{``}) have disappeared. They have been +replaced by the general notion of scope. \begin{center} \begin{tabular}{l|l|l} -type & scope name & key \\ +type & scope name & delimiter \\ \hline types & type_scope & \TERM{T} \\ \TERM{bool} & bool_scope & \\ -\TERM{nat} & nat_scope & \TERM{N} \\ +\TERM{nat} & nat_scope & \TERM{nat} \\ \TERM{Z} & Z_scope & \TERM{Z} \\ \TERM{R} & R_scope & \TERM{R} \\ \TERM{positive} & positive_scope & \TERM{P} @@ -93,7 +95,7 @@ types & type_scope & \TERM{T} \\ In order to use notations of arithmetics on \TERM{Z}, its scope must be opened with command \verb+Open Scope Z_scope.+ Another possibility is using the scope change notation (\TERM{\%}). The latter notation is to be used when notations of several scopes appear in the same expression. In examples below, scope changes are not needed if the appropriate scope -has been opened. +has been opened. Scope nat_scope is opened in the initial state of Coq. \begin{transbox} \TRANSCOM{`0+x=x+0`}{0+x=x+0}{\textrm{Z_scope}} \TRANSCOM{``0 + [if b then ``1`` else ``2``]``}{0 + if b then 1 else 2}{\textrm{R_scope}} @@ -113,24 +115,24 @@ scope & notations \\ \hline nat_scope & $+ ~- ~* ~< ~\leq ~> ~\geq$ \\ Z_scope & $+ ~- ~* ~/ ~\TERM{mod} ~< ~\leq ~> ~\geq ~?=$ \\ -R_scope & $+ ~- ~* ~/ ~< ~\leq ~> ~\geq ~{}^2$ \\ +R_scope & $+ ~- ~* ~/ ~< ~\leq ~> ~\geq$ \\ type_scope & $* ~+$ \\ -bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{!!}$ +bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{-}$ \\ +list_scope & $\TERM{::} ~\TERM{++}$ \end{tabular} \end{center} -(Note: $\leq$ is written \TERM{$<=$}, and the square notation uses iso-latin -character 178) +(Note: $\leq$ is written \TERM{$<=$}) \subsection{Notation for implicit arguments} The explicitation of arguments is closer to the \emph{bindings} notation in -tactics. +tactics. Argument positions follow the argument names of the head constant. \begin{transbox} -\TRANS{f 1!x 2!y}{f @1:=x @2:=y} -\TRANS{!f x y}{@f x y} +\TRANS{f 1!t1 2!t2}{f (x:=t1) (y:=t2)} +\TRANS{!f t1 t2}{@f t1 t2} \end{transbox} @@ -228,7 +230,9 @@ Ltac keywords. \subsection{Ltac} -Definitions of macros are introduced by \TERM{Ltac} instead of \TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive Definition}. +Definitions of macros are introduced by \TERM{Ltac} instead of +\TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive +Definition}. Rules of a match command are not between square brackets anymore. @@ -239,24 +243,19 @@ became \TERM{context}. Syntax is unified with subterm matching. \TRANS{match t with [C[x=y]] => inst C[y=x]}{match t with context C[x=y] => context C[y=x]} \end{transbox} -\subsection{List of arguments} - -Since the precedence of application is now very tight, tactics that take -a list of terms would require to put parenthesis around each argument -very often. In the new syntax, terms are separated by commas. Tactics -affected by this change are: \TERM{pattern}, \TERM{unfold}, \TERM{fold}, -\TERM{generalize} and the list of dependent bindings of \TERM{apply}, -\TERM{elim}, \TERM{case}, \TERM{specialize}, \TERM{left}, \TERM{right}, -\TERM{exists}, \TERM{split} and \TERM{constructor}. +\subsection{Named arguments of theorems} \begin{transbox} -\TRANS{Generalize t (f x)}{generalize t, f x} -\TRANS{Apply t with (f x) b (g y)}{apply t with f x, b, g y} +\TRANS{Apply thm with x:=t 1:=u}{apply thm with (x:=t) (1:=u)} \end{transbox} + \subsection{Occurrences} -Occurences of a term are now listed after the term itself. +To avoid ambiguity between a numeric literal and the optionnal +occurence numbers of this term, the occurence numbers are put after +the term itself. This applies to tactic \TERM{pattern} and also +\TERM{unfold} \begin{transbox} \TRANS{Pattern 1 2 (f x) 3 4 d}{pattern (f x) 1 2, d 3 4} \end{transbox} diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index fa9a402eb..bba623da3 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -280,8 +280,8 @@ GEXTEND Gram | -> [] ] ] ; fixdecl: - [ [ id = base_ident; bl=LIST0 Constr.binder; ann=fixannot; - ":"; ty=lconstr -> (loc,id,bl,ann,ty) ] ] + [ [ "("; id = base_ident; bl=LIST0 Constr.binder; ann=fixannot; + ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] ; fixannot: [ [ "{"; IDENT "struct"; id=name; "}" -> Some id @@ -323,11 +323,11 @@ GEXTEND Gram | IDENT "casetype"; c = constr -> TacCaseType c | "fix"; n = natural -> TacFix (None,n) | "fix"; id = base_ident; n = natural -> TacFix (Some id,n) - | "fix"; id = base_ident; n = natural; "with"; fd = LIST0 fixdecl -> + | "fix"; id = base_ident; n = natural; "with"; fd = LIST1 fixdecl -> TacMutualFix (id,n,List.map mk_fix_tac fd) | "cofix" -> TacCofix None | "cofix"; id = base_ident -> TacCofix (Some id) - | "cofix"; id = base_ident; "with"; fd = LIST0 fixdecl -> + | "cofix"; id = base_ident; "with"; fd = LIST1 fixdecl -> TacMutualCofix (id,List.map mk_cofix_tac fd) | IDENT "cut"; c = constr -> TacCut c @@ -342,7 +342,7 @@ GEXTEND Gram | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c - | IDENT "lettac"; "("; id = base_ident; ":="; c = lconstr; ")"; + | IDENT "set"; "("; id = base_ident; ":="; c = lconstr; ")"; p = clause_pattern -> TacLetTac (id,c,p) | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")" -> TacInstantiate (n,c) diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 250ab423b..cddc1a541 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -410,7 +410,7 @@ Qed. (***********) Definition Rsqr:R->R:=[r:R]``r*r``. -Notation "x ²" := (Rsqr x) (at level 2,left associativity). +V7only[Notation "x ²" := (Rsqr x) (at level 2,left associativity).]. (***********) Lemma Rsqr_O:(Rsqr ``0``)==``0``. diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 281ca2c5c..7e71f5623 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -394,12 +394,14 @@ let rec pr inherited a = | CRef r -> pr_reference r, latom | CFix (_,id,fix) -> let p = hov 0 (str"fix " ++ pr_recursive (pr_fixdecl pr) (snd id) fix) in - (if List.length fix = 1 & prec_less (fst inherited) ltop - then surround p else p), - lfix + if List.length fix = 1 & prec_less (fst inherited) ltop + then surround p, latom else p, lfix | CCoFix (_,id,cofix) -> - hov 0 (str "cofix " ++ pr_recursive (pr_cofixdecl pr) (snd id) cofix), - lfix + let p = + hov 0 (str "cofix " ++ + pr_recursive (pr_cofixdecl pr) (snd id) cofix) in + if List.length cofix = 1 & prec_less (fst inherited) ltop + then surround p, latom else p, lfix | CArrow (_,a,b) -> hov 0 (pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr (-larrow,E) b), larrow @@ -504,9 +506,6 @@ let rec pr inherited a = str "end"), latom | CHole _ -> str "_", latom -(* - | CEvar (_,n) -> str "?" ++ int n, latom -*) | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_sort s, latom diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index f36e053fc..cf8c57ae9 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -362,16 +362,15 @@ let pr_fix_tac env (id,n,c) = let annot = if List.length names = 1 then mt() else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in - spc() ++ str"with " ++ - hov 0 (pr_id id ++ - prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++ spc() ++ - pr_lconstr env ty) in + hov 1 (str"(" ++ pr_id id ++ + prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++ + pr_lconstrarg env ty ++ str")") in (* spc() ++ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg env c) *) let pr_cofix_tac env (id,c) = - spc() ++ str"with " ++ hov 0 (pr_id id ++ str":" ++ pr_constrarg env c) in + hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in (* Printing tactics as arguments *) @@ -421,26 +420,29 @@ and pr_atom1 env = function | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c) | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> - hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ - prlist (pr_fix_tac env) l) + hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ cut() ++ + str"with " ++ prlist_with_sep spc (pr_fix_tac env) l) | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> - hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc () ++ - prlist (pr_cofix_tac env) l) + hov 1 (str "cofix" ++ spc () ++ pr_id id ++ cut () ++ + str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l) | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c) | TacTrueCut (None,c) -> hov 1 (str "assert" ++ pr_constrarg env c) | TacTrueCut (Some id,c) -> - hov 1 (str "assert" ++ spc () ++ str"(" ++ pr_id id ++ str ":" ++ - pr_lconstrarg env c ++ str")") + hov 1 (str "assert" ++ spc () ++ + hov 1 (str"(" ++ pr_id id ++ str " :" ++ + pr_lconstrarg env c ++ str")")) | TacForward (false,na,c) -> - hov 1 (str "assert" ++ spc () ++ str"(" ++ pr_name na ++ str " :=" ++ - pr_lconstrarg env c ++ str")") + hov 1 (str "assert" ++ spc () ++ + hov 1 (str"(" ++ pr_name na ++ str " :=" ++ + pr_lconstrarg env c ++ str")")) | TacForward (true,Anonymous,c) -> hov 1 (str "pose" ++ pr_constrarg env c) | TacForward (true,Name id,c) -> - hov 1 (str "pose" ++ spc() ++ str"(" ++ pr_id id ++ str " :=" ++ - pr_lconstrarg env c ++ str")") + hov 1 (str "pose" ++ spc() ++ + hov 1 (str"(" ++ pr_id id ++ str " :=" ++ + pr_lconstrarg env c ++ str")")) | TacGeneralize l -> hov 1 (str "generalize" ++ spc () ++ prlist_with_sep spc (pr_constr env) l) @@ -448,11 +450,14 @@ and pr_atom1 env = function hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ pr_constrarg env c) | TacLetTac (id,c,cl) -> - hov 1 (str "lettac" ++ spc () ++ str"(" ++ pr_id id ++ str " :=" ++ - pr_lconstrarg env c ++ str")" ++ pr_clause_pattern pr_ident cl) + hov 1 (str "set" ++ spc () ++ + hov 1 (str"(" ++ pr_id id ++ str " :=" ++ + pr_lconstrarg env c ++ str")") ++ + pr_clause_pattern pr_ident cl) | TacInstantiate (n,c) -> - hov 1 (str "instantiate" ++ str"(" ++ pr_arg int n ++ str":=" ++ - pr_lconstrarg env c ++ str")") + hov 1 (str "instantiate" ++ spc() ++ + hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ + pr_lconstrarg env c ++ str")")) (* Derived basic tactics *) | TacSimpleInduction h -> |