Suites modifs du noyau. Univ devient purement fonctionnel.

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

9 files changed, 88 insertions, 170 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ea3a4fdb8e..b08286ef35 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -97,7 +97,7 @@ let new_evar =
 let make_evar_instance env =
   fold_named_context
     (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*))
-    env []
+    env ~init:[]
 
 (* create an untyped existential variable *)
 let new_evar_in_sign env =
@@ -124,7 +124,7 @@ let new_Type () = mkType (new_univ ())
 
 let new_Type_sort () = Type (new_univ ())
 
-let judge_of_new_Type () = fst (Typeops.judge_of_type (new_univ ()))
+let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
 (*
 let new_Type () = mkType dummy_univ
 
@@ -304,7 +304,7 @@ let make_evar_instance_with_rel env =
   let vars = 
     fold_named_context
       (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*))
-      env [] in
+      env ~init:[] in
   snd (fold_rel_context
     (fun env (_,b,_) (i,l) -> (i-1, (*if b=None then *) mkRel i :: l (*else l*)))
     env (n,vars))
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 066df12096..c8cbf31a62 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -18,126 +18,36 @@ open Declarations
 open Environ
 open Reductionops
 
-(*
-type inductive_instance = {
-  mis_sp : section_path;
-  mis_mib : mutual_inductive_body;
-  mis_tyi : int;
-  mis_mip : one_inductive_body }
-
-
-let build_mis (sp,tyi) mib =
-  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi;
-    mis_mip = mind_nth_type_packet mib tyi }
-
-let mis_ntypes mis = mis.mis_mib.mind_ntypes
-let mis_nparams mis = mis.mis_mip.mind_nparams
-
-let mis_index mis = mis.mis_tyi
-
-let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
-let mis_nrealargs mis = mis.mis_mip.mind_nrealargs
-let mis_kelim mis = mis.mis_mip.mind_kelim
-let mis_recargs mis =
-  Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
-let mis_recarg mis = mis.mis_mip.mind_listrec
-let mis_typename mis = mis.mis_mip.mind_typename
-let mis_typepath mis =
-  make_path (dirpath mis.mis_sp) mis.mis_mip.mind_typename CCI
-let mis_consnames mis = mis.mis_mip.mind_consnames
-let mis_conspaths mis =
-  let dir = dirpath mis.mis_sp in
-  Array.map (fun id -> make_path dir id CCI) mis.mis_mip.mind_consnames
-let mis_inductive mis = (mis.mis_sp,mis.mis_tyi)
-let mis_finite mis = mis.mis_mip.mind_finite
-
-let mis_typed_nf_lc mis =
-  let sign = mis.mis_mib.mind_hyps in
-  mis.mis_mip.mind_nf_lc
-
-let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
-
-let mis_user_lc mis = 
-  let sign = mis.mis_mib.mind_hyps in
-  (mind_user_lc mis.mis_mip)
-
-(* gives the vector of constructors and of 
-   types of constructors of an inductive definition 
-   correctly instanciated *)
-
-let mis_type_mconstructs mispec =
-  let specif = Array.map body_of_type (mis_user_lc mispec)
-  and ntypes = mis_ntypes mispec
-  and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) 
-  and make_Ck k =
-     mkMutConstruct ((mispec.mis_sp,mispec.mis_tyi),k+1) in
-  (Array.init nconstr make_Ck, 
-   Array.map (substl (list_tabulate make_Ik ntypes)) specif)
-*)
-let mis_nf_constructor_type (ind,mib,mip) j =
-  let specif = mip.mind_nf_lc
-  and ntypes = mib.mind_ntypes
-  and nconstr = Array.length mip.mind_consnames in
-  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
-  if j > nconstr then error "Not enough constructors in the type";
-  substl (list_tabulate make_Ik ntypes) specif.(j-1)
-(*
-let mis_constructor_type i mispec = 
-  let specif = mis_user_lc mispec
-  and ntypes = mis_ntypes mispec
-  and nconstr = mis_nconstr mispec in
-  let make_Ik k = mkMutInd (mispec.mis_sp,ntypes-k-1) in 
-  if i > nconstr then error "Not enough constructors in the type";
-  substl (list_tabulate make_Ik ntypes) specif.(i-1)
-
-let mis_arity mis =
-  let hyps = mis.mis_mib.mind_hyps  in
-  mind_user_arity mis.mis_mip
-
-let mis_nf_arity mis =
-  let hyps = mis.mis_mib.mind_hyps in
-  mis.mis_mip.mind_nf_arity
-
-let mis_params_ctxt mis = mis.mis_mip.mind_params_ctxt
-(*
-  let paramsign,_ =
-    decompose_prod_n_assum mis.mis_mip.mind_nparams
-      (body_of_type (mis_nf_arity mis))
-  in paramsign
-*)
-
-let mis_sort mispec = mispec.mis_mip.mind_sort
-*)
-
 (* [inductive_family] = [inductive_instance] applied to global parameters *)
 type inductive_family = inductive * constr list
 
-type inductive_type = IndType of inductive_family * constr list
+let make_ind_family (mis, params) = (mis,params)
+let dest_ind_family (mis,params) = (mis,params)
 
 let liftn_inductive_family n d (mis,params) =
   (mis, List.map (liftn n d) params)
 let lift_inductive_family n = liftn_inductive_family n 1
 
-let liftn_inductive_type n d (IndType (indf, realargs)) =
-  IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
-let lift_inductive_type n = liftn_inductive_type n 1
-
 let substnl_ind_family l n (mis,params) =
   (mis, List.map (substnl l n) params)
 
-let substnl_ind_type l n (IndType (indf,realargs)) =
-  IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs)
 
-let make_ind_family (mis, params) = (mis,params)
-let dest_ind_family (mis,params) = (mis,params)
+type inductive_type = IndType of inductive_family * constr list
 
 let make_ind_type (indf, realargs) = IndType (indf,realargs)
 let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
 
+let liftn_inductive_type n d (IndType (indf, realargs)) =
+  IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
+let lift_inductive_type n = liftn_inductive_type n 1
+
+let substnl_ind_type l n (IndType (indf,realargs)) =
+  IndType (substnl_ind_family l n indf, List.map (substnl l n) realargs)
+
 let mkAppliedInd (IndType ((ind,params), realargs)) =
   applist (mkInd ind,params@realargs)
 
+
 let mis_is_recursive_subset listind mip = 
   let rec one_is_rec rvec = 
     List.exists
@@ -152,6 +62,14 @@ let mis_is_recursive_subset listind mip =
 let mis_is_recursive (mib,mip) =
   mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) mip
 
+let mis_nf_constructor_type (ind,mib,mip) j =
+  let specif = mip.mind_nf_lc
+  and ntypes = mib.mind_ntypes
+  and nconstr = Array.length mip.mind_consnames in
+  let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
+  if j > nconstr then error "Not enough constructors in the type";
+  substl (list_tabulate make_Ik ntypes) specif.(j-1)
+
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -200,15 +118,7 @@ let instantiate_params t args sign =
     | [], [] -> substl s t
     | _ -> anomaly"instantiate_params: type, ctxt and args mismatch"
   in inst [] t (List.rev sign,args)
-(*
-let get_constructor_type (IndFamily (mispec,params)) j =
-  assert (j <= mis_nconstr mispec);
-  let typi = mis_constructor_type j mispec in
-  instantiate_params typi params (mis_params_ctxt mispec)
-
-let get_constructors_types (IndFamily (mispec,params) as indf) =
-  Array.init (mis_nconstr mispec) (fun j -> get_constructor_type indf (j+1))
-*)
+
 let get_constructor (ind,mib,mip,params) j =
   assert (j <= Array.length mip.mind_consnames);
   let typi = mis_nf_constructor_type (ind,mib,mip) j in
@@ -340,10 +250,8 @@ let is_dep env predty (ind,args) =
   is_dep_arity env kelim predty glob_t
 
 
-
 let set_names env n brty =
-  let (args,cl) = decompose_prod_n n brty in
-  let ctxt = List.map (fun (x,ty) -> (x,None,ty)) args in
+  let (ctxt,cl) = decompose_prod_n_assum n brty in
   it_mkProd_or_LetIn_name env cl ctxt
 
 let set_pattern_names env ind brv =
@@ -365,7 +273,7 @@ let type_case_branches_with_names env indspec pj c =
 (* Guard condition *)
 
 (* A function which checks that a term well typed verifies both
-   syntaxic conditions *)
+   syntactic conditions *)
 
 let control_only_guard env = 
   let rec control_rec c = match kind_of_term c with
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 2174bf0e96..ef72ab7a35 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -11,46 +11,38 @@
 open Names
 open Term
 open Declarations
-open Sign
 open Environ
 open Evd
 
-val mis_nf_constructor_type :
-  (section_path * 'a) * mutual_inductive_body *
-  one_inductive_body -> int -> constr
-
+(* An inductive type with its parameters *)
 type inductive_family = inductive * constr list
-and inductive_type = IndType of inductive_family * constr list
-val liftn_inductive_family :
-  int -> int -> 'a * constr list -> 'a * constr list
-val lift_inductive_family :
-  int -> 'a * constr list -> 'a * constr list
-val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
-val lift_inductive_type : int -> inductive_type -> inductive_type
-val substnl_ind_family :
-  constr list -> int -> 'a * constr list -> 'a * constr list
-val substnl_ind_type :
-  constr list -> int -> inductive_type -> inductive_type
 val make_ind_family : 'a * 'b -> 'a * 'b
 val dest_ind_family : 'a * 'b -> 'a * 'b
+val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
+val lift_inductive_family  : int -> inductive_family -> inductive_family
+val substnl_ind_family :
+  constr list -> int -> inductive_family -> inductive_family
+
+(* An inductive type with its parameters and real arguments *)
+type inductive_type = IndType of inductive_family * constr list
 val make_ind_type : inductive_family * constr list -> inductive_type
 val dest_ind_type : inductive_type -> inductive_family * constr list
+val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
+val lift_inductive_type  : int -> inductive_type -> inductive_type
+val substnl_ind_type :
+  constr list -> int -> inductive_type -> inductive_type
+
 val mkAppliedInd : inductive_type -> constr
-val mis_is_recursive_subset :
-  int list -> one_inductive_body -> bool
-val mis_is_recursive :
-  mutual_inductive_body * one_inductive_body ->
-  bool
-val make_case_info :
-  env -> inductive ->
-  case_style option -> pattern_source array -> case_info
-val make_default_case_info : env -> inductive -> case_info
+val mis_is_recursive_subset : int list -> one_inductive_body -> bool
+val mis_is_recursive : mutual_inductive_body * one_inductive_body -> bool
+val mis_nf_constructor_type :
+  inductive * mutual_inductive_body * one_inductive_body -> int -> constr
 
 type constructor_summary = {
   cs_cstr : constructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : rel_context;
+  cs_args : Sign.rel_context;
   cs_concl_realargs : constr array;
 } 
 val lift_constructor : int -> constructor_summary -> constructor_summary
@@ -59,28 +51,24 @@ val get_constructor :
   int -> constructor_summary
 val get_constructors :
   env -> inductive * constr list -> constructor_summary array
-val get_arity :
-  env -> inductive * constr list -> arity
-val local_rels : rel_context -> constr list
+val get_arity : env -> inductive * constr list -> Sign.arity
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive * constr list -> constr
-val make_arity :
-  env -> bool -> inductive * constr list -> sorts -> types
-val build_branch_type :
-  env -> bool -> constr -> constructor_summary -> types
+val make_arity : env -> bool -> inductive * constr list -> sorts -> types
+val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
 exception Induc
 val extract_mrectype : constr -> inductive * constr list
-val find_mrectype :
-  env -> evar_map -> constr -> inductive * constr list
-val find_rectype :
-  env -> evar_map -> constr -> inductive_type
-val find_inductive :
-  env -> evar_map -> constr -> inductive * constr list
-val find_coinductive :
-  env ->
-  evar_map -> constr -> inductive * constr list
+val find_mrectype    : env -> evar_map -> constr -> inductive * constr list
+val find_rectype     : env -> evar_map -> constr -> inductive_type
+val find_inductive   : env -> evar_map -> constr -> inductive * constr list
+val find_coinductive : env -> evar_map -> constr -> inductive * constr list
+
 val type_case_branches_with_names :
   env -> inductive * constr list -> unsafe_judgment -> constr ->
     types array * types
+val make_case_info :
+  env -> inductive -> case_style option -> pattern_source array -> case_info
+val make_default_case_info : env -> inductive -> case_info
+
 val control_only_guard : env -> types -> unit
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index fd42ca0ba9..034597a713 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -55,7 +55,7 @@ let env_ise sigma env =
         (na, option_app (nf_evar sigma) b, nf_evar sigma ty)
         e)
     ctxt
-    env0
+    ~init:env0
 
 (* This simplify the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a601d6397d..a98cc3e81d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -305,7 +305,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       let env' = push_rel_assum var env in
       let j' = pretype_type empty_valcon env' isevars lvar lmeta c2 in
       let resj =
-	try fst (judge_of_product env name j j')
+	try judge_of_product env name j j'
 	with TypeError _ as e -> Stdpp.raise_with_loc loc e in
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 	
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index bb6948767b..da12c6449c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -90,7 +90,7 @@ let typeur sigma metamap =
     match kind_of_term t with
     | Cast (c,s) when isSort s -> destSort s
     | Sort (Prop c) -> type_0
-    | Sort (Type u) -> Type (fst (Univ.super u))
+    | Sort (Type u) -> Type (Univ.super u)
     | Prod (name,t,c2) ->
         (match (sort_of (push_rel (name,None,t) env) c2) with
 	  | Prop _ as s -> s
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f8dd8ce154..04cbd0d19e 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -23,6 +23,23 @@ let print_sort = function
 (*  | Type _ -> [< 'sTR "Type" >] *)
   | Type u -> [< 'sTR "Type("; Univ.pr_uni u; 'sTR ")" >]
 
+let current_module = ref empty_dirpath
+
+let set_module m = current_module := m
+
+let new_univ = 
+  let univ_gen = ref 0 in
+  (fun sp ->
+    incr univ_gen; 
+    Univ.make_univ (!current_module,!univ_gen))
+
+let new_sort_in_family = function 
+  | InProp -> mk_Prop
+  | InSet -> mk_Set
+  | InType -> Type (new_univ ())
+
+
+
 (* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
 let prod_it = List.fold_left (fun c (n,t)  -> mkProd (n, t, c))
 
@@ -580,9 +597,9 @@ let empty_names_context = []
 let ids_of_rel_context sign =
   Sign.fold_rel_context
     (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
-    sign []
+    sign ~init:[]
 let ids_of_named_context sign =
-  Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign []
+  Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
 
 let ids_of_context env = 
   (ids_of_rel_context (rel_context env))
@@ -673,7 +690,7 @@ let process_rel_context f env =
   let sign = named_context env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
-  Sign.fold_rel_context f rels env0
+  Sign.fold_rel_context f rels ~init:env0
 
 let assums_of_rel_context sign =
   Sign.fold_rel_context
@@ -681,7 +698,7 @@ let assums_of_rel_context sign =
       match c with
           Some _ -> l
         | None -> (na,body_of_type t)::l)
-    sign []
+    sign ~init:[]
 
 let lift_rel_context n sign =
   let rec liftrec k = function
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 30a7fa8ca4..5e32cef35a 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -15,6 +15,12 @@ open Term
 open Sign
 open Environ
 
+(* Universes *)
+val set_module : Names.dir_path -> unit
+val new_univ : unit -> Univ.universe
+val new_sort_in_family : sorts_family -> sorts
+
+(* iterators on terms *)
 val print_sort : sorts -> std_ppcmds
 val prod_it : init:types -> (name * types) list -> types
 val lam_it : init:constr -> (name * types) list -> constr
@@ -138,6 +144,6 @@ val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val fold_named_context_both_sides :
   ('a -> named_declaration -> named_context -> 'a) ->
-    named_context -> 'a -> 'a
+    named_context -> init:'a -> 'a
 val mem_named_context : identifier -> named_context -> bool
 val make_all_name_different : env -> env
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b36c032046..5b759e74c6 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -86,7 +86,7 @@ let rec execute mf env sigma cstr =
 	judge_of_prop_contents c
 
     | Sort (Type u) ->
-	let (j,_) = judge_of_type u in j
+	judge_of_type u
 	  
     | App (f,args) ->
 	let j = execute mf env sigma f in
@@ -107,8 +107,7 @@ let rec execute mf env sigma cstr =
 	let env1 = push_rel (name,None,varj.utj_val) env in
         let j' = execute mf env1 sigma c2 in
         let varj' = type_judgment env sigma j' in
-	let (j,_) = judge_of_product env1 name varj varj' in
-	j
+	judge_of_product env1 name varj varj'
 
      | LetIn (name,c1,c2,c3) ->
         let j1 = execute mf env sigma c1 in