Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour

"set (f:=fun n => t)" (et idem pour pose).

Documentation notation Record sans sort et, en passant, "let|" -> "let '".



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10852 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 67 insertions, 14 deletions

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 :