Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en interp_constr etc.

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

6 files changed, 102 insertions, 130 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index af24760fc9..cf68a472b4 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -379,8 +379,9 @@ let dbize_fw  sigma env com = dbize FW sigma env com
 (* constr_of_com takes an environment of typing assumptions,
  * and translates a command to a constr. *)
 
-let raw_constr_of_com sigma env com = dbize_cci sigma (unitize_env env) com
-let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env env) com
+let interp_rawconstr sigma env com = dbize_cci sigma (unitize_env (context env)) com
+
+let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env (context env)) com
 let raw_constr_of_compattern sigma env com = 
   dbize_cci sigma (unitize_env env) com
 
@@ -461,73 +462,51 @@ let _ =
 
 
 (*********************************************************************)
-(* Functions before in ex-trad                                       *)
-
-(* Endless list of alternative ways to call Trad *)
+(* V6 compat: Functions before in ex-trad                            *)
 
-(* With dB *)
+(* Endless^H^H^H^H^H^H^HShort list of alternative ways to call pretyping *)
 
-let constr_of_com_env1 is_ass sigma env com = 
-  let c = raw_constr_of_com sigma (context env) com in
+let interp_constr_gen is_ass sigma env com = 
+  let c = interp_rawconstr sigma env com in
   try 
     ise_resolve1 is_ass sigma env c
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
-let constr_of_com_env sigma env com =
-  constr_of_com_env1 false sigma env com
-    
-let fconstr_of_com_env1 is_ass sigma env com = 
-  let c = raw_fconstr_of_com sigma (context env) com in
-  try 
-    ise_resolve1 is_ass sigma env c
-  with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e
- 
-let fconstr_of_com_env sigma hyps com =
-  fconstr_of_com_env1 false sigma hyps com 
-    
-let judgment_of_com1 is_ass sigma env com = 
-  let c = raw_constr_of_com sigma (context env) com in
-  try 
-    ise_resolve is_ass sigma [] env c
+let interp_constr sigma env c = interp_constr_gen false sigma env c
+let interp_type sigma env   c = interp_constr_gen true sigma env c
+
+
+let judgment_of_com sigma env com = 
+  let c = interp_rawconstr sigma env com in
+  try
+    ise_resolve false sigma [] env c
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
-let judgment_of_com sigma env com =
-  judgment_of_com1 false sigma env com
-
-(* Without dB *)
-let type_of_com env com =
-  let sign = context env in
-  let c = raw_constr_of_com Evd.empty sign com in
+let typed_type_of_com sigma env com =
+  let c = interp_rawconstr sigma env com in
   try 
-    ise_resolve_type true Evd.empty [] env c
+    ise_resolve_type true sigma [] env c
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
-let constr_of_com1 is_ass sigma env com = 
-  constr_of_com_env1 is_ass sigma env com
-    
-let constr_of_com sigma env com =
-  constr_of_com1 false sigma env com
-
-let constr_of_com_sort sigma sign com =
-  constr_of_com1 true sigma sign com
+(* Note: typ is retyped *)
 
-let fconstr_of_com1 is_ass sigma env com = 
-  fconstr_of_com_env1 is_ass sigma env com
+let interp_casted_constr sigma env com typ = 
+  ise_resolve_casted sigma env typ (interp_rawconstr sigma env com)
 
-let fconstr_of_com sigma sign com  =
-  fconstr_of_com1 false sigma sign com
-let fconstr_of_com_sort sigma sign com  =
-  fconstr_of_com1 true sigma sign com
 
-(* Note: typ is retyped *)
+let fconstr_of_com1 is_ass sigma env com = 
+  let c = raw_fconstr_of_com sigma env com in
+  try 
+    ise_resolve1 is_ass sigma env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
+ 
+let fconstr_of_com sigma hyps com =
+  fconstr_of_com1 false sigma hyps com 
 
-let constr_of_com_casted sigma env com typ = 
-  let sign = context env in
-  ise_resolve_casted sigma env typ (raw_constr_of_com sigma sign com)
 
 (* Typing with Trad, and re-checking with Mach *)
 (* Should be done in two passes by library commands ...
@@ -600,7 +579,7 @@ let constr_of_rawconstr c =
   glob [] c
 
 let constr_of_com_pattern sigma env com = 
-  let c = raw_constr_of_com sigma (context env) com in
+  let c = interp_rawconstr sigma env com in
   try 
     constr_of_rawconstr c
   with e -> 
@@ -624,7 +603,7 @@ let glob_nvar com =
 let cvt_pattern sigma env = function
   | Node(_,"PATTERN", Node(_,"COMMAND",[com])::nums) ->
       let occs = List.map num_of_ast nums in
-      let c = constr_of_com sigma env com in
+      let c = interp_constr sigma env com in
       let j = Typing.unsafe_machine env sigma c in
       (occs, j.uj_val, j.uj_type)
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
@@ -634,7 +613,7 @@ let cvt_unfold = function
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold")
 
 let cvt_fold sigma sign = function
-  | Node(_,"COMMAND",[c]) -> constr_of_com sigma sign c
+  | Node(_,"COMMAND",[c]) -> interp_constr sigma sign c
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold")
 
 let flag_of_ast lf =
@@ -687,7 +666,7 @@ let flag_of_ast lf =
       | (false,_) -> (fun _ -> false)
       | (true,None) -> (fun _ -> true)
       | (true,Some p) -> p }
-  
+
 let redexp_of_ast sigma sign = function
   | ("Red", []) -> Red
   | ("Hnf", []) -> Hnf
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index d762faba10..54c1ce5c20 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -12,52 +12,48 @@ open Rawterm
 
 (* Translation from AST to terms. *)
 
-(*
+val interp_rawconstr     : 'a evar_map -> env -> Coqast.t -> rawconstr
+val interp_constr        : 'a evar_map -> env -> Coqast.t -> constr
+val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr
+val interp_type          : 'a evar_map -> env -> Coqast.t -> constr
+val typed_type_of_com    : 'a evar_map -> env -> Coqast.t -> typed_type
+val judgment_of_com      : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+
+val constr_of_com_pattern : 'a evar_map -> env -> Coqast.t -> constr
+val redexp_of_ast : 
+  'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr
+
+(* Translation rules from V6 to V7:
+
+constr_of_com_casted -> interp_casted_constr
+constr_of_com_sort   -> interp_type
+constr_of_com        -> interp_constr
+rawconstr_of_com     -> interp_rawconstr  [+ env instead of sign]
+type_of_com          -> typed_type_of_com Evd.empty
+constr_of_com1 true  -> interp_type
+*)
+
+(*i For debug (or obsolete)
 val dbize_op : CoqAst.loc -> string -> CoqAst.t list -> constr list -> constr
 val dbize    : unit assumptions -> CoqAst.t -> constr
 
-val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
-*)
 val dbize_cci      : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
+val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
 
-(*
-val absolutize_fw  : 'c evar_map -> unit assumptions -> constr -> constr
-*)
 val dbize_fw       : 'c evar_map -> unit assumptions -> Coqast.t -> rawconstr
-
-val raw_constr_of_com :
-  'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
+val absolutize_fw  : 'c evar_map -> unit assumptions -> constr -> constr
 val raw_fconstr_of_com :
   'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
+val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
+val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
+
 val raw_constr_of_compattern :
   'c evar_map -> 'a assumptions -> Coqast.t -> rawconstr
 
 val globalize_command : Coqast.t -> Coqast.t
 val globalize_ast     : Coqast.t -> Coqast.t
 
-(*i Ceci était avant dans Trad
-    Maintenant elles sont là car relève des ast i*)
-
-val type_of_com : env -> Coqast.t -> typed_type
-
-val constr_of_com_casted : 'a evar_map -> env -> Coqast.t -> constr ->
-  constr
-
-val constr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
-val constr_of_com : 'a evar_map -> env -> Coqast.t -> constr
-val constr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
-val constr_of_com_pattern : 'a evar_map -> env -> Coqast.t -> constr
-
-val fconstr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
-val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
-
-val judgment_of_com1 : 
-  bool -> 'a evar_map -> env -> Coqast.t -> unsafe_judgment
-val judgment_of_com : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
-
 (* Typing with Trad, and re-checking with Mach *)
-(*i
 val fconstruct :'c evar_map -> context -> Coqast.t -> unsafe_judgment
 val fconstruct_type : 'c evar_map -> context -> Coqast.t -> typed_type
 
@@ -67,5 +63,3 @@ val fconstruct_with_univ :
 
 i*)
 
-val redexp_of_ast : 
-  'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 29d02b0138..f7b1c51cc6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -457,7 +457,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 *)
 
 
-let unsafe_fmachine vtcon nocheck isevars metamap env constr = 
+let unsafe_fmachine vtcon nocheck isevars metamap env constr =
   trad_metamap := metamap;
   trad_nocheck := nocheck;
   reset_problems ();
@@ -499,26 +499,24 @@ let ise_resolve fail_evar sigma metamap env c =
   let j = unsafe_fmachine empty_tycon false isevars metamap env c in
   j_apply (fun _ -> process_evars fail_evar) env !isevars j
 
-
 let ise_resolve_type fail_evar sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine def_vty_con false isevars metamap env c in
   let tj = inh_ass_of_j env isevars j in
   typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj
 
-
 let ise_resolve_nocheck sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine empty_tycon true isevars metamap env c in
   j_apply (fun _ -> process_evars true) env !isevars j
 
-
 let ise_resolve1 is_ass sigma env c =
   if is_ass then 
     body_of_type (ise_resolve_type true sigma [] env c)
   else 
     (ise_resolve true sigma [] env c).uj_val
 
+
 (* Keeping universe constraints *)
 (*
 let fconstruct_type_with_univ_sp sigma sign sp c =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c4af6472d3..a20b1eb3f4 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -11,6 +11,25 @@ open Rawterm
 open Evarutil
 (*i*)
 
+(* Raw calls to the inference machine of Trad: boolean says if we must fail
+ * on unresolved evars, or replace them by Metas *)
+val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
+  env -> rawconstr -> unsafe_judgment
+val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list ->
+  env -> rawconstr -> typed_type
+
+(* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
+ * if we must coerce to a type *)
+val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr
+
+val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
+
+(* progmach.ml tries to type ill-typed terms: does not perform the conversion
+ * test in application.
+ *)
+val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
+  env -> rawconstr -> unsafe_judgment
+
 (* Typing with Trad, and re-checking with Mach *)
 (*i
 val infconstruct_type :
@@ -36,30 +55,11 @@ val infconstruct_type_with_univ_sp :
   -> Impuniv.universes * (typed_type * information)
 i*)
 
-(* Low level typing functions, for terms with de Bruijn indices and Metas *)
-
-(* Raw calls to the inference machine of Trad: boolean says if we must fail
- * on unresolved evars, or replace them by Metas *)
-val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
-  env -> rawconstr -> unsafe_judgment
-val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list ->
-  env -> rawconstr -> typed_type
-
-(* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
- * if we must coerce to a type *)
-val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr
-
-val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
-
-(* progmach.ml tries to type ill-typed terms: does not perform the conversion
- * test in application.
- *)
-val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
-  env -> rawconstr -> unsafe_judgment
-
-
+(*i*)
 (* Internal of Trad...
  * Unused outside Trad, but useful for debugging
  *)
 val pretype : 
   trad_constraint -> env -> 'a evar_defs -> rawconstr -> unsafe_judgment
+
+(*i*)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f73fc4f078..91bab946e0 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -33,11 +33,11 @@ let constant_entry_of_com (com,comtypopt) =
   let env = Global.env() in
   match comtypopt with
       None -> 
-	{ const_entry_body = Cooked (constr_of_com sigma env com);
+	{ const_entry_body = Cooked (interp_constr sigma env com);
 	  const_entry_type = None }
     | Some comtyp ->
-	let typ = constr_of_com_sort sigma env comtyp in
-	{ const_entry_body = Cooked (constr_of_com_casted sigma env com typ);
+	let typ = interp_type sigma env comtyp in
+	{ const_entry_body = Cooked (interp_casted_constr sigma env com typ);
 	  const_entry_type = Some typ }
 
 let red_constant_entry ce = function
@@ -61,21 +61,21 @@ let definition_body_red ident n com comtypeopt red_option =
 let definition_body ident n com typ = definition_body_red ident n com typ None
 
 let syntax_definition ident com =
-  let c = raw_constr_of_com Evd.empty (Global.context()) com in 
+  let c = interp_rawconstr Evd.empty (Global.env()) com in 
   Syntax_def.declare_syntactic_definition ident c;
   if is_verbose() then 
     message ((string_of_id ident) ^ " is now a syntax macro")
 
 (***TODO
 let abstraction_definition ident arity com =
-  let c = raw_constr_of_compattern Evd.empty (Global.env()) com in 
+  let c = raw_interp_constrpattern Evd.empty (Global.env()) com in 
   machine_abstraction ident arity c
 ***)
 
 (* 2| Variable definitions *)
 
 let parameter_def_var ident c =
-  let c = constr_of_com1 true Evd.empty (Global.env()) c in
+  let c = interp_type Evd.empty (Global.env()) c in
   declare_parameter (id_of_string ident) c;
   if is_verbose() then message (ident ^ " is assumed")
     
@@ -92,7 +92,7 @@ let hypothesis_def_var is_refining ident n c =
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
           declare_variable (id_of_string ident)
-             (constr_of_com1 true Evd.empty (Global.env()) c,n,false);
+             (interp_type Evd.empty (Global.env()) c,n,false);
 	  if is_verbose() then message (ident ^ " is assumed");
           if is_refining then 
             mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
@@ -138,7 +138,8 @@ let build_mutual lparams lnamearconstrs finite =
       let (ind_env,arityl) =
       	List.fold_left 
 	  (fun (env,arl) (recname,arityc,_) -> 
-             let arity = type_of_com env (mkProdCit lparams arityc) in
+             let arity =
+	       typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
 	     let env' = Environ.push_var (recname,arity) env in
 (*	A quoi cela sert ?
 	declare_variable recname (arity.body,NeverDischarge,false);*)
@@ -149,7 +150,7 @@ let build_mutual lparams lnamearconstrs finite =
         (fun ar (name,_,lname_constr) -> 
            let consconstrl =
              List.map 
-               (fun (_,constr) -> constr_of_com sigma ind_env
+               (fun (_,constr) -> interp_constr sigma ind_env
                     (mkProdCit lparams constr))
                lname_constr 
 	   in
@@ -217,7 +218,7 @@ let build_recursive lnameargsardef =
     try 
       List.fold_left 
         (fun (env,arl) (recname,lparams,arityc,_) -> 
-           let arity = type_of_com env (mkProdCit lparams arityc) in
+           let arity = typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
            declare_variable recname (arity.body,NeverDischarge,false);
            (Environ.push_var (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
@@ -227,7 +228,7 @@ let build_recursive lnameargsardef =
   let recdef = 
     try 
       List.map (fun (_,lparams,arityc,def) -> 
-                  constr_of_com sigma rec_sign 
+                  interp_constr sigma rec_sign 
                     (mkLambdaCit lparams (mkCastC(def,arityc))))
         lnameargsardef
     with e -> 
@@ -280,7 +281,7 @@ let build_corecursive lnameardef =
     try 
       List.fold_left 
         (fun (env,arl) (recname,arityc,_) -> 
-           let arity = type_of_com env0 arityc in
+           let arity = typed_type_of_com Evd.empty env0 arityc in
            declare_variable recname (arity.body,NeverDischarge,false);
            (Environ.push_var (recname,arity) env, (arity::arl)))
         (env0,[]) lnameardef
@@ -290,7 +291,7 @@ let build_corecursive lnameardef =
   let recdef =
     try 
       List.map (fun (_,arityc,def) -> 
-                  constr_of_com sigma rec_sign
+                  interp_constr sigma rec_sign
                     (mkCastC(def,arityc)))
         lnameardef
     with e -> 
@@ -354,7 +355,7 @@ let build_scheme lnamedepindsort =
   and env0 = Global.env() in
   let lrecspec =
     List.map (fun (_,dep,indid,sort) -> 
-                let s = destSort (constr_of_com sigma env0 sort) in
+                let s = destSort (interp_constr sigma env0 sort) in
                 (inductive_of_ident indid,dep,s)) lnamedepindsort
   in
   let n = NeverDischarge in 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 79ccb76111..673f4a4f61 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -70,14 +70,14 @@ let typecheck_params_and_field ps fs =
   let env1,newps =
     List.fold_left
       (fun (env,newps) (id,t) -> 
-         let tj = type_of_com env t in
+         let tj = typed_type_of_com Evd.empty env t in
          (Environ.push_var (id,tj) env,(id,tj.body)::newps))
       (env0,[]) ps
   in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) (id,t) -> 
-         let tj = type_of_com env t in
+         let tj = typed_type_of_com Evd.empty env t in
          (Environ.push_var (id,tj) env,(id,tj.body)::newfs)) (env1,[]) fs
   in
   List.rev(newps),List.rev(newfs)