diff options
| -rw-r--r-- | CHANGES | 18 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 47 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 12 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 77 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
7 files changed, 113 insertions, 45 deletions
@@ -13,7 +13,7 @@ Language - New syntax "forall {A}, T" for specifying maximally inserted implicit arguments in terms. - Sort of Record/Structure, Inductive and CoInductive defaults to Type - if omitted. (DOC TODO?) + if omitted. - Record/Structure now usable for defining coinductive types (e.g. "Record stream := { hd : nat; tl : stream }.") - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent @@ -53,7 +53,8 @@ Libraries (DOC TO CHECK) - Better computational behavior of some constants (eq_nat_dec and le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare transparent, ...) (exceptional source of incompatibilities). -- Boolean operators moved from module Bool to module Datatypes. +- Boolean operators moved from module Bool to module Datatypes (may need + to rename qualified references in script) - Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular a better power function). - In SetoidList, eqlistA now expresses that two lists have similar elements @@ -87,7 +88,7 @@ Libraries (DOC TO CHECK) logic. Addition of files providing intuitionistic axiomatizations of descriptions: Epsilon.v, Description.v and IndefiniteDescription.v. -Notations and implicit arguments +Notations, coercions and implicit arguments - New options "Set Maximal Implicit Insertion", "Set Reversible Pattern Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit @@ -100,7 +101,9 @@ Notations and implicit arguments surviving or non export outside module. - Level "constr" moved from 9 to 8. (DOC TODO?) - Structure/Record now printed as Record (unless option Printing All is set). -- Support for parametric notations defining constants (i.e. abbreviations). +- Support for parametric notations defining constants. +- Insertion of coercions below product types refrains to unfold + constants (possible source of incompatibility). Tactic Language @@ -130,8 +133,8 @@ Tactic Language Tactics -- New tactics [apply -> term], [apply <- term], [apply -> term in - ident], [apply <- term in ident] for applying equivalences (iff). (DOC TODO) +- New tactics "apply -> term", "apply <- term", "apply -> term in + ident", "apply <- term in ident" for applying equivalences (iff). (DOC TODO) - Slight improvement of the hnf and simpl tactics when applied on expressions with explicit occurrences of match or fix. - New tactics "eapply in", "erewrite", "erewrite in". @@ -150,7 +153,7 @@ Tactics is still legal but equivalent to intros ?a ?b. - New intro pattern "{A,B,C}" synonym to "(A,(B,C))" - rewrite now supports "by" to solve side-conditions and "at" to select - occurrences. + occurrences. (DOC TODO) - New syntax "rewrite A,B" for "rewrite A; rewrite B" - New syntax "rename a into b, c into d" for "rename a into b; rename c into d" - New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]" @@ -163,6 +166,7 @@ Tactics - Tactic "apply" now able to traverse conjunctions and to select the first matching lemma among the components of the conjunction; tactic apply also able to apply lemmas of conclusion an empty type. +- Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)". Program diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index c19e01538..5baf84bec 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -20,7 +20,7 @@ construction allows to define ``signatures''. {\sentence} & ++= & {\record}\\ & & \\ {\record} & ::= & - {\tt Record} {\ident} \sequence{\binderlet}{} {\tt :} {\sort} \verb.:=. \\ + {\tt Record} {\ident} \sequence{\binderlet}{} \zeroone{{\tt :} {\sort}} \verb.:=. \\ && ~~~~\zeroone{\ident} \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\ & & \\ @@ -45,7 +45,8 @@ construction allows to define ``signatures''. \noindent the identifier {\ident} is the name of the defined record and {\sort} is its type. The identifier {\ident$_0$} is the name of its constructor. If {\ident$_0$} is omitted, the default name {\tt -Build\_{\ident}} is used. The identifiers {\ident$_1$}, .., +Build\_{\ident}} is used. If {\sort} is omitted, the default sort is ``{\Type}''. +The identifiers {\ident$_1$}, .., {\ident$_n$} are the names of fields and {\term$_1$}, .., {\term$_n$} their respective types. Remark that the type of {\ident$_i$} may depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the @@ -289,17 +290,15 @@ declared as such (see Section~\ref{printing-options}). \index{let in@{\tt let ... in}} \label{Letin}} -Closed terms (that is not relying on any axiom or variable) in an -inductive type having only one constructor, say {\tt foo}, have -necessarily the form \texttt{(foo ...)}. In this case, the {\tt match} -construction can be written with a syntax close to the {\tt let ... in -...} construction. +Pattern-matching on terms inhabiting inductive type having only one +constructor can be alternatively written using {\tt let ... in ...} +constructions. There are two variants of them. -\subsubsection{Destructuring {\tt let}} -Expression {\tt let +\subsubsection{First destructuring {\tt let} syntax} +The expression {\tt let (}~{\ident$_1$},\ldots,{\ident$_n$}~{\tt ) :=}~{\term$_0$}~{\tt -in}~{\term$_1$} performs case analysis on {\term$_0$} which must be in -an inductive type with one constructor with $n$ arguments. Variables +in}~{\term$_1$} performs case analysis on a {\term$_0$} which must be in +an inductive type with one constructor having itself $n$ arguments. Variables {\ident$_1$}\ldots{\ident$_n$} are bound to the $n$ arguments of the constructor in expression {\term$_1$}. For instance, the definition @@ -317,23 +316,25 @@ Reset fst. \begin{coq_example} Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. \end{coq_example} -Note however that reduction is slightly different from regular {\tt -let ... in ...} construction since it can occur only if {\term$_0$} -can be put in constructor form. Otherwise, reduction is blocked. +Notice that reduction is different from regular {\tt let ... in ...} +construction since it happens only if {\term$_0$} is in constructor +form. Otherwise, the reduction is blocked. The pretty-printing of a definition by matching on a irrefutable pattern can either be done using {\tt match} or the {\tt let} construction (see Section~\ref{printing-options}). -The general equivalence for an inductive type with one constructors {\tt C} is +If {\term} inhabits an inductive type with one constructor {\tt C}, +we have an equivalence between + +{\tt let ({\ident}$_1$,\ldots,{\ident}$_n$) \zeroone{\ifitem} := {\term} in {\term}'} + +\noindent and -\smallskip -{\tt let ({\ident}$_1$,\ldots,{\ident}$_n$) \zeroone{\ifitem} := {\term} in {\term}'} \\ -$\equiv$~ {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end} -\subsubsection{{\tt let} pattern} +\subsubsection{Second destructuring {\tt let} syntax\index{let '... in}} Another destructuring {\tt let} syntax is available for inductive types with one constructor by giving an arbitrary pattern instead of just a tuple @@ -342,19 +343,19 @@ for all the arguments. For example, the preceding example can be written: Reset fst. \end{coq_eval} \begin{coq_example} -Definition fst (A B:Set) (p:A * B) := let| pair x _ := p in x. +Definition fst (A B:Set) (p:A * B) := let 'pair x _ := p in x. \end{coq_example} This is useful to match deeper inside tuples and also to use notations -for the pattern, as the syntax {\tt let| p := t in b} allows arbitrary +for the pattern, as the syntax {\tt let 'p := t in b} allows arbitrary patterns to do the deconstruction. For example: \begin{coq_example} Definition deep_tuple (A : Set) (x : (A * A) * (A * A)) : A * A * A * A := - let| ((a,b), (c, d)) := x in (a,b,c,d). + let '((a,b), (c, d)) := x in (a,b,c,d). Notation " x 'with' p " := (exist _ x p) (at level 20). Definition proj1_sig' (A :Set) (P : A -> Prop) (t:{ x : A | P x }) : A := - let| x with p := t in x. + let 'x with p := t in x. \end{coq_example} When printing definitions which are written using this construct it diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index cd32fb35a..5ccbaf130 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -497,7 +497,12 @@ This allows to specify which occurrences of the conclusion are concerned. {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. Each {\tt at} part is optional. -\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} +\item {\tt set (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )} + + This is equivalent to {\tt set (} {\ident} {\tt :=} {\tt fun} + \nelist{\binder}{} {\tt =>} {\term} {\tt )}. + +\item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term} {\tt ) in} {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} {\tt |- *} {\tt at} {\num$'_1$} \dots\ {\num$'_n$} @@ -517,6 +522,11 @@ This allows to specify which occurrences of the conclusion are concerned. context without performing any replacement in the goal or in the hypotheses. +\item {\tt pose (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )} + + This is equivalent to {\tt pose (} {\ident} {\tt :=} {\tt fun} + \nelist{\binder}{} {\tt =>} {\term} {\tt )}. + \item{\tt pose {\term}} This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index f5ea021d4..41f89a541 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -131,7 +131,7 @@ GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr sort global constr_pattern lconstr_pattern Constr.ident binder binder_let binders_let delimited_binder_let delimited_binders_let - binders_let_fixannot typeclass_constraint pattern; + binders_let_fixannot typeclass_constraint pattern appl_arg; Constr.ident: [ [ id = Prim.ident -> id diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 035bdced7..a76b2386c 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -17,6 +17,8 @@ open Tacexpr open Rawterm open Genarg open Topconstr +open Term +open Libnames let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta] @@ -88,6 +90,13 @@ let guess_lpar_coloneq = let guess_lpar_colon = Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":") +let test_not_ident = + Gram.Entry.of_parser "not_ident" + (fun strm -> + match Stream.npeek 1 strm with + | [("IDENT",_)] -> raise Stream.Failure + | _ -> ()) + open Constr open Prim open Tactic @@ -117,6 +126,36 @@ let induction_arg_of_constr (c,lbind as clbind) = with _ -> ElimOnConstr clbind else ElimOnConstr clbind +(* Turn a simple binder as the argument for an application *) +let appl_args_of_simple_named_binder = function +| (idl,CHole _) -> + List.map (fun id -> CRef (Ident id), None) idl +| (idl,t) -> + let loc = join_loc (fst (List.hd idl)) (constr_loc t) in + let mk id = CCast (loc,CRef (Ident id),CastConv (DEFAULTcast,t)), None in + List.map mk idl + +let appl_args_of_simple_named_binders bl = + List.flatten (List.map appl_args_of_simple_named_binder bl) + +let rec mkCLambdaN_simple_loc loc bll c = + match bll with + | ((loc1,_)::_ as idl,bk,t) :: bll -> + CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (join_loc loc1 loc) bll c) + | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c + | [] -> c + +let mkCLambdaN_simple bl1 bl2 c = + let bl = + List.map (fun (idl,c) -> + (List.map (fun (loc,id) -> (loc,Names.Name id)) idl, + Default Explicit,c)) bl1 + @ bl2 in + if bl=[] then c + else + let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in + mkCLambdaN_simple_loc loc bl c + (* Auxiliary grammar rules *) GEXTEND Gram @@ -297,13 +336,18 @@ GEXTEND Gram | "-" -> false | -> true ]] ; - simple_fix_binder: + simple_binder: [ [ id=name -> ([id],Default Explicit,CHole (loc, None)) | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) ] ] ; + simple_named_binder: + [ [ id=identref -> ([id],CHole (loc, None)) + | "("; idl=LIST1 identref; ":"; c=lconstr; ")" -> (idl,c) + ] ] + ; fixdecl: - [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ann=fixannot; + [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot; ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] ; fixannot: @@ -311,9 +355,20 @@ GEXTEND Gram | -> None ] ] ; cofixdecl: - [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ":"; ty=lconstr; ")" -> + [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" -> (loc,id,bl,None,ty) ] ] ; + constr_or_decl: + [ [ "("; lid = identref; bl1 = LIST0 simple_named_binder; + ":="; c = lconstr; ")" -> + (Names.Name (snd lid), mkCLambdaN_simple bl1 [] c) + | "("; lid = identref; bl = LIST0 simple_named_binder; + args = LIST0 appl_arg; ")" -> + let first_args = appl_args_of_simple_named_binders bl in + (Names.Anonymous, CApp(loc,(None,CRef (Ident lid)),first_args@args)) + | "("; c = lconstr; ")" -> (Names.Anonymous, c) + | c = lconstr -> (Names.Anonymous, c) ] ] + ; hintbases: [ [ "with"; "*" -> None | "with"; l = LIST1 IDENT -> Some l @@ -345,10 +400,10 @@ GEXTEND Gram (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally produce a pattern_ident *) c = pattern_ident -> - let c = (CRef (Libnames.Ident (loc,c)), NoBindings) in + let c = (CRef (Ident (loc,c)), NoBindings) in (RepeatStar, c) | n = natural; c = pattern_ident -> - let c = (CRef (Libnames.Ident (loc,c)), NoBindings) in + let c = (CRef (Ident (loc,c)), NoBindings) in (UpTo n, c) | "!"; c = constr_with_bindings -> (RepeatPlus,c) | "?"; c = constr_with_bindings -> (RepeatStar,c) @@ -402,14 +457,10 @@ GEXTEND Gram | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> TacMutualCofix (false,id,List.map mk_cofix_tac fd) - | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" -> - TacLetTac (Names.Name id,b,nowhere) - | IDENT "pose"; b = constr -> - TacLetTac (Names.Anonymous,b,nowhere) - | IDENT "set"; id = lpar_id_coloneq; c = lconstr; ")"; p = clause -> - TacLetTac (Names.Name id,c,p) - | IDENT "set"; c = constr; p = clause -> - TacLetTac (Names.Anonymous,c,p) + | IDENT "pose"; (na,c) = constr_or_decl -> + TacLetTac (na,c,nowhere) + | IDENT "set"; (na,c) = constr_or_decl; p = clause -> + TacLetTac (na,c,p) (* Begin compatibility *) | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 9976e07cc..0d73b1e3d 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -439,6 +439,7 @@ module Constr = let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot" let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let" let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint" + let appl_arg = Gram.Entry.create "constr:appl_arg" end module Module = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 4fb9d0359..63090b146 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -168,6 +168,7 @@ module Constr : val binders_let_fixannot : (local_binder list * (name located option * recursion_order_expr)) Gram.Entry.e val delimited_binders_let : local_binder list Gram.Entry.e val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e + val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e end module Module : |