Allowing (Co)Fixpoint to be defined local and Let-style.

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

11 files changed, 68 insertions, 51 deletions

diff --git a/CHANGES b/CHANGES
index 6e4e9188b..39d9ae874 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,7 @@ Vernacular commands
   The tactic "induction" on a record is now actually doing "destruct".
 - The "Open Scope" command can now be given also a delimiter (e.g. Z).
 - The "Definition" command now allows the "Local" modifier.
+- The "Let" command can now define local (co)fixpoints.
 
 Specification Language
 
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 64afc1aed..f7a631d9c 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -913,6 +913,8 @@ section and depending on {\ident} are prefixed by the let-in definition
 
 \begin{Variants}
 \item {\tt Let {\ident} : {\term$_1$} := {\term$_2$}.}
+\item {\tt Let Fixpoint {\ident} \nelist{\fixpointbody}{with} {\tt .}.}
+\item {\tt Let CoFixpoint {\ident} \nelist{\cofixpointbody}{with} {\tt .}.}
 \end{Variants}
 
 \SeeAlso Sections \ref{Section} (section mechanism), \ref{Opaque},
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index a1eca85bc..cb6b74bcc 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -240,8 +240,8 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list
   | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of (fixpoint_expr * decl_notation list) list
-  | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list
+  | VernacFixpoint of locality * (fixpoint_expr * decl_notation list) list
+  | VernacCoFixpoint of locality * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e6f7480b6..c3d9438de 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -161,6 +161,8 @@ GEXTEND Gram
 	  VernacAssumption (stre, nl, bl)
       | d = def_token; id = identref; b = def_body ->
           VernacDefinition (d, id, b)
+      | IDENT "Let"; id = identref; b = def_body ->
+          VernacDefinition ((Discharge, Definition), id, b)
       (* Gallina inductive declarations *)
       | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
@@ -168,9 +170,13 @@ GEXTEND Gram
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
           VernacInductive (f,false,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint recs
+          VernacFixpoint (use_locality_exp (), recs)
+      | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint (Discharge, recs)
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint corecs
+          VernacCoFixpoint (use_locality_exp (), corecs)
+      | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+          VernacCoFixpoint (Discharge, corecs)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ]
@@ -197,8 +203,6 @@ GEXTEND Gram
   def_token:
     [ [ "Definition" ->
 	(use_locality_exp (), Definition)
-      | IDENT "Let" ->
-	(Discharge, Definition)
       | IDENT "Example" ->
 	(use_locality_exp (), Example)
       | IDENT "SubClass"  ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index fd4e23de7..131b4c0e2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -364,7 +364,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
 	  bl None body (Some ret_type) (fun _ _ -> ())
     | _ ->
-	Command.do_fixpoint fixpoint_exprl
+	Command.do_fixpoint Global fixpoint_exprl
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 850ad2b75..3fe522113 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -668,7 +668,12 @@ let rec pr_vernac = function
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
 
-  | VernacFixpoint recs ->
+  | VernacFixpoint (local, recs) ->
+      let local = match local with
+      | Discharge -> "Let "
+      | Local -> "Local "
+      | Global -> ""
+      in
       let pr_onerec = function
         | ((loc,id),ro,bl,type_,def),ntn ->
             let annot = pr_guard_annot pr_lconstr_expr bl ro in
@@ -677,17 +682,22 @@ let rec pr_vernac = function
             ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	    prlist (pr_decl_notation pr_constr) ntn
       in
-      hov 0 (str "Fixpoint" ++ spc() ++
+      hov 0 (str local ++ str "Fixpoint" ++ spc() ++
         prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
 
-  | VernacCoFixpoint corecs ->
+  | VernacCoFixpoint (local, corecs) ->
+      let local = match local with
+      | Discharge -> "Let "
+      | Local -> "Local "
+      | Global -> ""
+      in
       let pr_onecorec (((loc,id),bl,c,def),ntn) =
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_lconstr_expr c ++
         pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	prlist (pr_decl_notation pr_constr) ntn
       in
-      hov 0 (str "CoFixpoint" ++ spc() ++
+      hov 0 (str local ++ str "CoFixpoint" ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)
   | VernacScheme l ->
       hov 2 (str"Scheme" ++ spc() ++
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 21bb963db..a98daf709 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -515,12 +515,7 @@ let declare_fix kind f def t imps =
     const_entry_opaque = false;
     const_entry_inline_code = false
   } in
-  (** FIXME: include locality *)
-  let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
-  let gr = ConstRef kn in
-  Autoinstance.search_declaration (ConstRef kn);
-  maybe_declare_manual_implicits false gr imps;
-  gr
+  declare_definition f kind ce imps (fun _ r -> r)
 
 let _ = Obligations.declare_fix_ref := declare_fix
 
@@ -798,7 +793,7 @@ let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info)
 let interp_fixpoint l ntns = check_recursive true (interp_recursive true l ntns)
 let interp_cofixpoint l ntns = check_recursive false (interp_recursive false l ntns)
     
-let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
+let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -816,14 +811,14 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    ignore (List.map4 (declare_fix Fixpoint) fixnames fixdecls fixtypes fiximps);
+    ignore (List.map4 (declare_fix (local, Fixpoint)) fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
   end;
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns =
+let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -839,7 +834,7 @@ let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns =
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-    ignore (List.map4 (declare_fix CoFixpoint) fixnames fixdecls fixtypes fiximps);
+    ignore (List.map4 (declare_fix (local, CoFixpoint)) fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
   end;
@@ -874,7 +869,7 @@ let collect_evars_of_term evd c ty =
     Int.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
       evars Evd.empty
       
-let do_program_recursive fixkind fixl ntns =
+let do_program_recursive local fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
   let (env, rec_sign, evd), fix, info = 
     interp_recursive isfix fixl ntns 
@@ -901,7 +896,7 @@ let do_program_recursive fixkind fixl ntns =
   let fiximps = List.map pi2 info in
   let fixdefs = List.map Option.get fixdefs in
   let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
-    if isfix then begin
+  let () = if isfix then begin
       let possible_indexes = List.map compute_possible_guardness_evidences info in
       let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
 	Array.of_list fixtypes,
@@ -910,10 +905,14 @@ let do_program_recursive fixkind fixl ntns =
       let indexes = 
 	Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
 	List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
-    end;
-    Obligations.add_mutual_definitions defs ntns fixkind
+  end in
+  let kind = match fixkind with
+  | Obligations.IsFixpoint _ -> (local, Fixpoint)
+  | Obligations.IsCoFixpoint -> (local, CoFixpoint)
+  in
+  Obligations.add_mutual_definitions defs ~kind ntns fixkind
 
-let do_program_fixpoint l =
+let do_program_fixpoint local l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
     | [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
@@ -932,24 +931,25 @@ let do_program_fixpoint l =
     | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
 	let fixl,ntns = extract_fixpoint_components true l in
 	let fixkind = Obligations.IsFixpoint g in
-	  do_program_recursive fixkind fixl ntns
+	  do_program_recursive local fixkind fixl ntns
 
     | _, _ ->
 	errorlabstrm "do_program_fixpoint"
 	  (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_fixpoint l =
-  if Flags.is_program_mode () then do_program_fixpoint l else
-  let fixl,ntns = extract_fixpoint_components true l in
-  let fix = interp_fixpoint fixl ntns in
-  let possible_indexes =
-    List.map compute_possible_guardness_evidences (snd fix) in
-  declare_fixpoint fix possible_indexes ntns
+let do_fixpoint local l =
+  if Flags.is_program_mode () then do_program_fixpoint local l
+  else
+    let fixl, ntns = extract_fixpoint_components true l in
+    let fix = interp_fixpoint fixl ntns in
+    let possible_indexes =
+      List.map compute_possible_guardness_evidences (snd fix) in
+    declare_fixpoint local fix possible_indexes ntns
 
-let do_cofixpoint l =
+let do_cofixpoint local l =
   let fixl,ntns = extract_cofixpoint_components l in
     if Flags.is_program_mode () then
-      do_program_recursive Obligations.IsCoFixpoint fixl ntns
+      do_program_recursive local Obligations.IsCoFixpoint fixl ntns
     else
       let cofix = interp_cofixpoint fixl ntns in
-	declare_cofixpoint cofix ntns
+	declare_cofixpoint local cofix ntns
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 618dd2019..eb0eef38f 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -134,24 +134,24 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list ->
+  locality -> recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list ->
+  locality -> recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list ->
     decl_notation list -> unit
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
-  (fixpoint_expr * decl_notation list) list -> unit
+  locality -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
-  (cofixpoint_expr * decl_notation list) list -> unit
+  locality -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
 
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : definition_object_kind -> Id.t ->
+val declare_fix : definition_kind -> Id.t ->
   constr -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index a088fa153..6fb8a86cc 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -567,7 +567,7 @@ let declare_mutual_definition l =
 	  None, List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
   in
   (* Declare the recursive definitions *)
-  let kns = List.map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in
+  let kns = List.map4 (!declare_fix_ref (local, kind)) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 428d7e321..bc092a1ce 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -21,11 +21,11 @@ open Decl_kinds
 open Tacexpr
 
 (** Forward declaration. *)
-val declare_fix_ref : (definition_object_kind -> Id.t ->
+val declare_fix_ref : (definition_kind -> Id.t ->
   constr -> types -> Impargs.manual_implicits -> global_reference) ref
 
 val declare_definition_ref :
-  (Id.t -> locality * definition_object_kind ->
+  (Id.t -> definition_kind ->
      Entries.definition_entry -> Impargs.manual_implicits
        -> global_reference declaration_hook -> global_reference) ref
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4c5e07a54..3eb33dce1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -574,15 +574,15 @@ let vernac_inductive finite infer indl =
     let indl = List.map unpack indl in
     do_mutual_inductive indl (finite != CoFinite)
 
-let vernac_fixpoint l =
+let vernac_fixpoint local l =
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_fixpoint l
+  do_fixpoint local l
 
-let vernac_cofixpoint l =
+let vernac_cofixpoint local l =
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_cofixpoint l
+  do_cofixpoint local l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1683,8 +1683,8 @@ let interp c = match c with
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
   | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l
-  | VernacFixpoint l -> vernac_fixpoint l
-  | VernacCoFixpoint l -> vernac_cofixpoint l
+  | VernacFixpoint (local, l) -> vernac_fixpoint local l
+  | VernacCoFixpoint (local, l) -> vernac_cofixpoint local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l