Support for implicit formal argument types in Program ; parse types in type scope.

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

7 files changed, 59 insertions, 39 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 09ed69fb4d..c92e719104 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -307,7 +307,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (* 		     ++ str "Coq type: " ++ my_print_constr env fullctyp)  *)
 (*      with _ -> ()  *)
 (*   in *)
-  let evm = non_instanciated_map env isevars in
+  let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in
+  let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in
+  let evm = non_instanciated_map env isevars evm in
+
     (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
   let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in
     (*     (try trace (str "Generated obligations : "); *)
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index e83ee66585..1b4e2f3870 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -89,18 +89,18 @@ let list_split_at index l =
 
 open Vernacexpr
 
-let coqintern evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
-let coqinterp evd env : Topconstr.constr_expr -> Term.constr = Constrintern.interp_constr (evars_of evd) env
+let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
+let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env
 
 let env_with_binders env isevars l =
   let rec aux ((env, rels) as acc) = function
       Topconstr.LocalRawDef ((loc, name), def) :: tl -> 
-	let rawdef = coqintern !isevars env def in
+	let rawdef = coqintern_constr !isevars env def in
 	let coqdef, deftyp = interp env isevars rawdef empty_tycon in
 	let reldecl = (name, Some coqdef, deftyp) in
 	  aux  (push_rel reldecl env, reldecl :: rels) tl
     | Topconstr.LocalRawAssum (bl, typ) :: tl ->
-	let rawtyp = coqintern !isevars env typ in
+	let rawtyp = coqintern_type !isevars env typ in
 	let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
 	let acc = 
 	  List.fold_left (fun (env, rels) (loc, name) -> 
@@ -113,35 +113,37 @@ let env_with_binders env isevars l =
   in aux (env, []) l
 
 let subtac_process env isevars id l c tycon =
-  let env_binders, binders_rel = env_with_binders env isevars l in
+  let c = Command.abstract_constr_expr c l in
+(*   let env_binders, binders_rel = env_with_binders env isevars l in *)
   let tycon = 
     match tycon with
 	None -> empty_tycon
       | Some t -> 
-	  let t = coqintern !isevars env_binders t in
-	  let coqt, ttyp = interp env_binders isevars t empty_tycon in
+	  let t = Command.generalize_constr_expr t l in
+	  let t = coqintern_type !isevars env t in
+	  let coqt, ttyp = interp env isevars t empty_tycon in
 	    mk_tycon coqt
   in    
-  let c = coqintern !isevars env_binders c in
-  let coqc, ctyp = interp env_binders isevars c tycon in
-(*   let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ *)
-(* 		 str "Coq type: " ++ my_print_constr env_binders ctyp) *)
-(*   with _ -> ()  *)
+  let c = coqintern_constr !isevars env c in
+  let coqc, ctyp = interp env isevars c tycon in
+(*   let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *)
+(* 		 str "Coq type: " ++ my_print_constr env ctyp) *)
+(*   with _ -> () *)
 (*   in *)
-(*   let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ()))  with _ -> () in *)
+(*   let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars))  with _ -> () in *)
     
-  let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel 
-  and fullctyp = it_mkProd_or_LetIn ctyp binders_rel
-  in
-  let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in
-  let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp in
-
-  let _ = try trace (str "After evar normalization: " ++ spc () ++
-		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
-		 ++ str "Coq type: " ++ my_print_constr env fullctyp)
-     with _ -> ()
-  in
-  let evm = non_instanciated_map env isevars in
+(*   let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel  *)
+(*   and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *)
+(*   in *)
+  let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in
+  let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in
+(*   let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *)
+(*   let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *)
+(*   let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *)
+(* 		       Evd.pr_evar_map evm) *)
+(*   with _ -> () *)
+(*   in *)
+  let evm = non_instanciated_map env isevars (evars_of !isevars) in
 (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
     evm, fullcoqc, fullctyp
 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 2e362a2107..fb58a14eb7 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -174,20 +174,28 @@ let string_of_hole_kind = function
   | InternalHole -> "InternalHole"
   | TomatchTypeParameter _ -> "TomatchTypeParameter"
       
-let non_instanciated_map env evd =
-  let evm = evars_of !evd in
-    List.fold_left 
-      (fun evm (key, evi) -> 
-	 let (loc,k) = evar_source key !evd in
-	   debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
-		      str (string_of_hole_kind k));
-	   match k with 
-	       QuestionMark _ -> Evd.add evm key evi
-	     | _ ->
+let evars_of_term evc init c = 
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n)
+    | Evar (n, _) -> assert(false)
+    | _ -> fold_constr evrec acc c
+  in 
+    evrec init c
+
+let non_instanciated_map env evd evm =
+  List.fold_left 
+    (fun evm (key, evi) -> 
+       let (loc,k) = evar_source key !evd in
+	 debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
+		    str (string_of_hole_kind k));
+	 match k with 
+	     QuestionMark _ -> Evd.add evm key evi
+	   | _ ->
 	       debug 2 (str " and is an implicit");
 	       Pretype_errors.error_unsolvable_implicit loc env evm k)
-      Evd.empty (Evarutil.non_instantiated evm)
-
+    Evd.empty (Evarutil.non_instantiated evm)
+    
 let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
 let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
 
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 37ee1ac23a..07be96090b 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -85,7 +85,8 @@ val print_args : env -> constr array -> std_ppcmds
 val make_existential : loc -> ?opaque:bool -> env -> evar_defs ref -> types -> constr
 val make_existential_expr : loc -> 'a -> 'b -> constr_expr
 val string_of_hole_kind : hole_kind -> string
-val non_instanciated_map : env -> evar_defs ref -> evar_map
+val evars_of_term : evar_map -> evar_map -> constr -> evar_map
+val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map
 val global_kind : logical_kind
 val goal_kind : locality_flag * goal_object_kind
 val global_proof_kind : logical_kind
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5a41f35086..f067eda6b5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1087,6 +1087,8 @@ let intern_gen isarity sigma env
 
 let intern_constr sigma env c = intern_gen false sigma env c 
 
+let intern_type sigma env c = intern_gen true sigma env c 
+
 let intern_pattern env patt =
   try
     intern_cases_pattern env [] ([],[]) None patt 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 1af6854d3e..edbf9fb62a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -51,6 +51,8 @@ type ltac_sign = identifier list * unbound_ltac_var_map
 
 val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 
+val intern_type : evar_map -> env -> constr_expr -> rawconstr
+
 val intern_gen : bool -> evar_map -> env ->
   ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 9540888dd3..4fae328056 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -57,6 +57,8 @@ val build_combined_scheme : identifier located -> identifier located list -> uni
 
 val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
 
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+
 val start_proof : identifier -> goal_kind -> constr ->
   declaration_hook -> unit