Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour

les définitions


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

4 files changed, 72 insertions, 31 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index c6a038c3b..34adc0587 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -33,30 +33,44 @@ open Safe_typing
 open Nametab
 open Typeops
 open Indtypes
+open Vernacexpr
 
-let mkCastC(a,b) = ope("CAST",[a;b])
-let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)])
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
-let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)])
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 
+let rec abstract_rawconstr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC(x,t,b)) idl
+        (abstract_rawconstr c bl)
+
+let rec destSubCast c = match kind_of_term c with
+  | Lambda (x,t,c) -> 
+      let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u)
+  | LetIn (x,b,t,c) ->
+      let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u)
+  | Cast (b,u) -> (b,u)
+  | _ -> assert false
+
 (* Commands of the interface *)
 
 (* 1| Constant definitions *)
 
-let constant_entry_of_com (com,comtypopt,opacity) =
+let constant_entry_of_com (bl,com,comtypopt,opacity) =
   let sigma = Evd.empty in
   let env = Global.env() in
   match comtypopt with
       None -> 
-	{ const_entry_body = interp_constr sigma env com;
+	let b = abstract_rawconstr com bl in
+	{ const_entry_body = interp_constr sigma env b;
 	  const_entry_type = None;
           const_entry_opaque = opacity }
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
-	let b = mkCastC (com,comtyp) in
-	let (body,typ) = destCast (interp_constr sigma env b) in
+	let b = abstract_rawconstr (mkCastC (com,comtyp)) bl in
+	let (body,typ) = destSubCast (interp_constr sigma env b) in
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
           const_entry_opaque = opacity }
@@ -75,8 +89,10 @@ let declare_global_definition ident ce n local =
   if_verbose message ((string_of_id ident) ^ " is defined");
   ConstRef sp
 
-let declare_definition red_option ident (local,n) c typopt = 
-  let ce = constant_entry_of_com (c,typopt,false) in
+let declare_definition ident (local,n) bl red_option c typopt = 
+  let ce = constant_entry_of_com (bl,c,typopt,false) in
+  if bl<>[] && red_option <> None then 
+    error "Evaluation under a local context not supported";
   let ce' = red_constant_entry ce red_option in
   match n with
     | NeverDischarge -> declare_global_definition ident ce' n local
diff --git a/toplevel/command.mli b/toplevel/command.mli
index ea6c97e0e..1b8cbe49a 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -14,6 +14,7 @@ open Names
 open Term
 open Nametab
 open Library
+open Vernacexpr
 (*i*)
 
 (*s Declaration functions. The following functions take ASTs,
@@ -21,8 +22,9 @@ open Library
    functions of [Declare]; they return an absolute reference to the
    defined object *)
 
-val declare_definition : Tacred.red_expr option -> identifier
-  -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference
+val declare_definition : identifier -> bool * strength ->
+  local_binder list -> Tacred.red_expr option -> Coqast.t -> Coqast.t option
+    -> global_reference
 
 val syntax_definition : identifier -> Coqast.t -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 68ab00755..3852ba7fe 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -267,15 +267,33 @@ let interp_goal = function
   | StartTheoremProof x -> (false, interp_theorem x)
   | StartDefinitionBody x -> interp_definition x
 
-let vernac_definition kind id red_option c typ_opt hook = 
-  let red_option = match red_option with
-    | None -> None 
-    | Some r -> 
-	let (evc,env)= Command.get_current_context () in
-	Some (interp_redexp env evc r) in
-  let (local,stre as x) = interp_definition kind in
-  let ref = declare_definition red_option id x c typ_opt in
-  hook stre ref
+let start_proof_and_print idopt k t hook =
+  start_proof_com idopt k t hook;
+  print_subgoals ();
+  if !pcoq <> None then (out_some !pcoq).start_proof ()
+
+let rec generalize_rawconstr c = function
+  | [] -> c
+  | LocalRawDef (id,b)::bl -> Ast.mkLetInC(id,b,generalize_rawconstr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> Ast.mkProdC(x,t,b)) idl
+        (generalize_rawconstr c bl)
+
+let vernac_definition kind id def hook =
+  let (local,stre as k) = interp_definition kind in
+  match def with
+  | ProveBody (bl,t) ->
+      let hook _ _ = () in
+      let t = generalize_rawconstr t bl in
+      start_proof_and_print (Some id) k t hook
+  | DefineBody (bl,red_option,c,typ_opt) ->
+      let red_option = match red_option with
+        | None -> None
+        | Some r -> 
+	    let (evc,env)= Command.get_current_context () in
+	    Some (interp_redexp env evc r) in
+      let ref = declare_definition id k bl red_option c typ_opt in
+      hook stre ref
 
 let vernac_start_proof kind sopt t lettop hook =
   if not(refining ()) then
@@ -284,9 +302,7 @@ let vernac_start_proof kind sopt t lettop hook =
 	(str "Let declarations can only be used in proof editing mode")
 (*    else if s = None then
       error "repeated Goal not permitted in refining mode"*);
-  start_proof_com sopt (interp_goal kind) t hook;
-  print_subgoals ();
-  if !pcoq <> None then (out_some !pcoq).start_proof ()
+  start_proof_and_print sopt (false, interp_theorem kind) t hook
 
 let vernac_end_proof is_opaque idopt =
   if_verbose show_script ();
@@ -866,8 +882,9 @@ let interp c = match c with
   | VernacDistfix (assoc,n,inf,qid) -> vernac_distfix assoc n inf qid
 
   (* Gallina *)
-  | VernacDefinition (k,id,red,t,otyp,f) -> vernac_definition k id red t otyp f
-  | VernacStartProof (k,id,t,top,f) -> vernac_start_proof k id t top f
+  | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
+  | VernacStartTheoremProof (k,id,t,top,f) ->
+      vernac_start_proof k (Some id) t top f
   | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,l) -> vernac_assumption stre l
@@ -929,7 +946,7 @@ let interp c = match c with
   | VernacNop -> ()
 
   (* Proof management *)
-(*  | VernacGoal c -> vernac_goal c*)
+  | VernacGoal t -> vernac_start_proof Theorem None t false (fun _ _ -> ())
   | VernacAbort id -> vernac_abort id
   | VernacAbortAll -> vernac_abort_all ()
   | VernacRestart -> vernac_restart ()
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index f1bd6ed52..ace11aee3 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -149,6 +149,13 @@ type fixpoint_expr =
     identifier * simple_binder list * constr_ast * constr_ast
 type cofixpoint_expr =
     identifier * constr_ast * constr_ast
+type local_binder =
+  | LocalRawDef of identifier * constr_ast
+  | LocalRawAssum of identifier list * constr_ast
+type definition_expr =
+  | ProveBody of local_binder list * constr_ast
+  | DefineBody of local_binder list * raw_red_expr option * constr_ast
+      * constr_ast option
 
 type local_decl_expr =
   | AssumExpr of identifier * constr_ast
@@ -174,11 +181,10 @@ type vernac_expr =
   | VernacDistfix of grammar_associativity * int * string * qualid located
 
   (* Gallina *)
-  | VernacDefinition of definition_kind * identifier *
-      raw_red_expr option * constr_ast * constr_ast option *
+  | VernacDefinition of definition_kind * identifier * definition_expr *
+      Proof_type.declaration_hook
+  | VernacStartTheoremProof of theorem_kind * identifier * Coqast.t * bool *
       Proof_type.declaration_hook
-  | VernacStartProof of goal_kind * identifier option *
-      constr_ast * bool * Proof_type.declaration_hook
   | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option
   | VernacExactProof of constr_ast
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
@@ -245,7 +251,7 @@ type vernac_expr =
   | VernacNop
 
   (* Proof management *)
-(*  | VernacGoal of constr_ast option*)
+  | VernacGoal of constr_ast
   | VernacAbort of identifier option
   | VernacAbortAll
   | VernacRestart