ensembles de contraintes d'univers

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

1 files changed, 107 insertions, 108 deletions

diff --git a/kernel/typing.ml b/kernel/typing.ml
index 4a029dfe32..dfce2e4427 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -38,7 +38,7 @@ type 'a mach_flags = {
 (* The typing machine without information. *)
 
 let rec execute mf env cstr =
-  let u0 = universes env in
+  let cst0 = Constraint.empty in
   match kind_of_term cstr with
     | IsMeta n ->
        	let metaty =
@@ -47,17 +47,17 @@ let rec execute mf env cstr =
 	in
         (match kind_of_term metaty with
            | IsCast (typ,kind) -> 
-	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, u0)
+	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0)
            | _ ->
-	       let (jty,u1) = execute mf env metaty in
+	       let (jty,cst) = execute mf env metaty in
 	       let k = whd_betadeltaiotaeta env jty.uj_type in
-	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, u1))
+	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst))
 	
     | IsRel n -> 
-	(relative env n, u0)
+	(relative env n, cst0)
 
     | IsVar id -> 
-	(make_judge cstr (snd (lookup_var id env)), u0)
+	(make_judge cstr (snd (lookup_var id env)), cst0)
 	  
     | IsAbst _ ->
         if evaluable_abst env cstr then 
@@ -66,93 +66,91 @@ let rec execute mf env cstr =
 	  error "Cannot typecheck an unevaluable abstraction"
 	      
     | IsConst _ ->
-        (make_judge cstr (type_of_constant_or_existential env cstr), u0)
+        (make_judge cstr (type_of_constant_or_existential env cstr), cst0)
 	  
     | IsMutInd _ ->
-	(make_judge cstr (type_of_inductive env cstr), u0)
+	(make_judge cstr (type_of_inductive env cstr), cst0)
 	  
     | IsMutConstruct _ -> 
 	let (typ,kind) = destCast (type_of_constructor env cstr) in
-        ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , u0)
+        ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0)
 	  
     | IsMutCase (_,p,c,lf) ->
-        let (cj,u1) = execute mf env c in
-	let env1 = set_universes u1 env in
-        let (pj,u2) = execute mf env1 p in
-	let env2 = set_universes u2 env1 in
-        let (lfj,u3) = execute_array mf env2 lf in
-	let env3 = set_universes u3 env2 in
-        (type_of_case env3 pj cj lfj, u3)
+        let (cj,cst1) = execute mf env c in
+        let (pj,cst2) = execute mf env p in
+        let (lfj,cst3) = execute_array mf env lf in
+	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+        (type_of_case env pj cj lfj, cst)
   
     | IsFix (vn,i,lar,lfi,vdef) ->
         if (not mf.fix) && array_exists (fun n -> n < 0) vn then
           error "General Fixpoints not allowed";
-        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
+        let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let fix = mkFix vn i larv lfi vdefv in
         check_fix env fix;
-	(make_judge fix larv.(i), u1)
+	(make_judge fix larv.(i), cst)
 	  
     | IsCoFix (i,lar,lfi,vdef) ->
-        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
+        let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
         let cofix = mkCoFix i larv lfi vdefv in
         check_cofix env cofix;
-	(make_judge cofix larv.(i), u1)
+	(make_judge cofix larv.(i), cst)
 	  
     | IsSort (Prop c) -> 
-	(type_of_prop_or_set c, u0)
+	(type_of_prop_or_set c, cst0)
 
     | IsSort (Type u) ->
-	type_of_type u u0
+	type_of_type u
 	  
     | IsAppL a ->
 	let la = Array.length a in
 	if la = 0 then error_cant_execute CCI env cstr;
 	let hd = a.(0)
 	and tl = Array.to_list (Array.sub a 1 (la - 1)) in
-	let (j,u1) = execute mf env hd in
-	let env1 = set_universes u1 env in
-        let (jl,u2) = execute_list mf env1 tl in
-	let env2 = set_universes u2 env1 in
-	apply_rel_list env2 mf.nocheck jl j
+	let (j,cst1) = execute mf env hd in
+        let (jl,cst2) = execute_list mf env tl in
+	let (j,cst3) = apply_rel_list env mf.nocheck jl j in
+	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+	(j, cst)
 	    
     | IsLambda (name,c1,c2) -> 
-        let (j,u1) = execute mf env c1 in
+        let (j,cst1) = execute mf env c1 in
         let var = assumption_of_judgment env j in
-	let env1 = push_rel (name,var) (set_universes u1 env) in
-        let (j',u2) = execute mf env1 c2 in 
-	let env2 = set_universes u2 env1 in
-        abs_rel env2 name var j'
+	let env1 = push_rel (name,var) env in
+        let (j',cst2) = execute mf env1 c2 in 
+        let (j,cst3) = abs_rel env1 name var j' in
+	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+	(j, cst)
 	  
     | IsProd (name,c1,c2) ->
-        let (j,u1) = execute mf env c1 in
+        let (j,cst1) = execute mf env c1 in
         let var = assumption_of_judgment env j in
-	let env1 = push_rel (name,var) (set_universes u1 env) in
-        let (j',u2) = execute mf env1 c2 in
-	let env2 = set_universes u2 env1 in
-        gen_rel env2 name var j'
+	let env1 = push_rel (name,var) env in
+        let (j',cst2) = execute mf env1 c2 in
+	let (j,cst3) = gen_rel env1 name var j' in
+	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+	(j, cst)
 	  
     | IsCast (c,t) ->
-        let (cj,u1) = execute mf env c in
-	let env1 = set_universes u1 env in
-        let (tj,u2) = execute mf env1 t in
-	let env2 = set_universes u2 env1 in
-        (cast_rel env2 cj tj, u2)
+        let (cj,cst1) = execute mf env c in
+        let (tj,cst2) = execute mf env t in
+	let cst = Constraint.union cst1 cst2 in
+        (cast_rel env cj tj, cst)
 	  
       | _ -> error_cant_execute CCI env cstr
 	  
 and execute_fix mf env lar lfi vdef =
-  let (larj,u1) = execute_array mf env lar in
-  let env1 = set_universes u1 env in
-  let lara = Array.map (assumption_of_judgment env1) larj in
+  let (larj,cst1) = execute_array mf env lar in
+  let lara = Array.map (assumption_of_judgment env) larj in
   let nlara = 
     List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
-  let env2 = 
-    List.fold_left (fun env nvar -> push_rel nvar env) env1 nlara in
-  let (vdefj,u2) = execute_array mf env2 vdef in
-  let env3 = set_universes u2 env2 in
+  let env1 = 
+    List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
+  let (vdefj,cst2) = execute_array mf env1 vdef in
   let vdefv = Array.map j_val_only vdefj in
-  let u3 = type_fixpoint env3 lfi lara vdefj in
-  (lara,vdefv,u3)
+  let cst3 = type_fixpoint env1 lfi lara vdefj in
+  let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
+  (lara,vdefv,cst)
 
 and execute_array mf env v =
   let (jl,u1) = execute_list mf env (Array.to_list v) in
@@ -160,11 +158,11 @@ and execute_array mf env v =
 
 and execute_list mf env = function
   | [] -> 
-      ([], universes env)
+      ([], Constraint.empty)
   | c::r -> 
-      let (j,u') = execute mf env c in 
-      let (jr,u'') = execute_list mf (set_universes u' env) r in
-      (j::jr, u'')
+      let (j,cst1) = execute mf env c in 
+      let (jr,cst2) = execute_list mf env r in
+      (j::jr, Constraint.union cst1 cst2)
 
 
 (* The typed type of a judgment. *)
@@ -224,19 +222,19 @@ let unsafe_type_of_type env c =
 (* Typing of several terms. *)
 
 let safe_machine_l env cl =
-  let type_one (env,l) c =
-    let (j,u) = safe_machine env c in
-    (set_universes u env, j::l)
+  let type_one (cst,l) c =
+    let (j,cst') = safe_machine env c in
+    (Constraint.union cst cst', j::l)
   in
-  List.fold_left type_one (env,[]) cl
+  List.fold_left type_one (Constraint.empty,[]) cl
 
 let safe_machine_v env cv =
-  let type_one (env,l) c =
-    let (j,u) = safe_machine env c in
-    (set_universes u env, j::l)
+  let type_one (cst,l) c =
+    let (j,cst') = safe_machine env c in
+    (Constraint.union cst cst', j::l)
   in
-  let env',l = Array.fold_left type_one (env,[]) cv in
-  (env', Array.of_list l)
+  let cst',l = Array.fold_left type_one (Constraint.empty,[]) cv in
+  (cst', Array.of_list l)
  
 
 (*s Safe environments. *)
@@ -261,8 +259,8 @@ let lookup_meta = lookup_meta
    being added to the environment. *)
 
 let push_rel_or_var push (id,c) env =
-  let (j,u) = safe_machine env c in
-  let env' = set_universes u env in
+  let (j,cst) = safe_machine env c in
+  let env' = add_constraints cst env in
   let var = assumption_of_judgment env' j in
   push (id,var) env'
 
@@ -279,39 +277,41 @@ let push_rels vars env =
 (* Insertion of constants and parameters in environment. *)
 
 let add_constant sp ce env =
-  let (jb,u) = safe_machine env ce.const_entry_body in
-  let env' = set_universes u env in
-  let (env'',ty) = 
+  let (jb,cst) = safe_machine env ce.const_entry_body in
+  let env' = add_constraints cst env in
+  let (env'',ty,cst') = 
     match ce.const_entry_type with
       | None -> 
-	  env', typed_type_of_judgment env' jb
+	  env', typed_type_of_judgment env' jb, Constraint.empty
       | Some ty -> 
-	  let (jt,u') = safe_machine env ty in
-	  let env'' = set_universes u' env' in
-	  match conv env'' jb.uj_type jt.uj_val with
-	    | Convertible u'' -> 
-		let env'' = set_universes u'' env' in
-		env'', assumption_of_judgment env'' jt
-	    | NotConvertible -> 
-		error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+	  let (jt,cst') = safe_machine env ty in
+	  let env'' = add_constraints cst' env' in
+	  try
+	    let cst'' = conv env'' jb.uj_type jt.uj_val in
+	    let env'' = add_constraints cst'' env'' in
+	    env'', assumption_of_judgment env'' jt, Constraint.union cst' cst''
+	  with NotConvertible -> 
+	    error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
   in
   let cb = { 
     const_kind = kind_of_path sp;
     const_body = Some (ref (Cooked ce.const_entry_body));
     const_type = ty;
     const_hyps = get_globals (context env);
+    const_constraints = Constraint.union cst cst';
     const_opaque = false } 
   in
   add_constant sp cb env''
 
 let add_parameter sp t env =
-  let (jt,u) = safe_machine env t in
-  let env' = set_universes u env in
+  let (jt,cst) = safe_machine env t in
+  let env' = add_constraints cst env in
   let cb = {
     const_kind = kind_of_path sp;
     const_body = None;
     const_type = assumption_of_judgment env' jt;
     const_hyps = get_globals (context env);
+    const_constraints = cst;
     const_opaque = false } 
   in
   Environ.add_constant sp cb env'
@@ -330,35 +330,32 @@ let rec for_all_prods p env c =
 	 let env' = Environ.push_rel (name,ty) env in
 	 for_all_prods p env' c)
     | DOP2(Prod, b, DLAM(name,c)) -> 
-	let (jb,u) = unsafe_machine env b in
+	let (jb,cst) = unsafe_machine env b in
 	let var = assumption_of_judgment env jb in
 	(p var) &&
-	(let env' = Environ.push_rel (name,var) (set_universes u env) in
+	(let env' = Environ.push_rel (name,var) (add_constraints cst env) in
 	 for_all_prods p env' c)
     | _ -> true
 
 let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c
 
-let enforce_type_constructor env univ j =
+let enforce_type_constructor env univ j cst =
   match whd_betadeltaiota env j.uj_type with
     | DOP0 (Sort (Type uc)) -> 
-	let u = universes env in
-	set_universes (enforce_geq univ uc u) env
+	Constraint.add (univ,Geq,uc) cst
     | _ -> error "Type of Constructor not well-formed"
 
 let type_one_constructor env_ar nparams ar c =
   let (params,dc) = decompose_prod_n nparams c in
   let env_par = push_rels params env_ar in
-  let (jc,u) = safe_machine env_par dc in
-  let env_par' = set_universes u env_par in
-  let env_par'' = match sort_of_arity env_ar ar with
-    | Type u -> enforce_type_constructor env_par' u jc
-    | Prop _ -> env_par'
+  let (jc,cst) = safe_machine env_par dc in
+  let cst' = match sort_of_arity env_ar ar with
+    | Type u -> enforce_type_constructor env_par u jc cst
+    | Prop _ -> cst
   in
-  let env_ar' = set_universes (universes env_par'') env_ar in
-  let (j,u) = safe_machine env_ar' c in
+  let (j,cst'') = safe_machine env_ar c in
   let issmall = is_small_type env_par c in
-  (set_universes u env_ar', (issmall,j))
+  ((issmall,j), Constraint.union cst' cst'')
 
 let logic_constr env c =
   for_all_prods (fun t -> not (is_info_type env t)) env c
@@ -376,18 +373,19 @@ let is_unit env_par nparams ar spec =
 
 let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) =
   let (lna,vc) = decomp_all_DLAMV_name spec in
-  let (env',(issmall,jlc)) = 
+  let ((issmall,jlc),cst') = 
     List.fold_right
-      (fun c (env,(small,jl)) -> 
-	 let (env',(sm,jc)) = type_one_constructor env nparams ar c in
-	 (env', (small && sm,jc::jl)))
-       (Array.to_list vc) (env_ar,(true,[]))
+      (fun c ((small,jl),cst) -> 
+	 let ((sm,jc),cst') = type_one_constructor env_ar nparams ar c in
+	 ((small && sm,jc::jl), Constraint.union cst cst'))
+      (Array.to_list vc) 
+      ((true,[]),Constraint.empty)
   in
   let castlc = List.map cast_of_judgment jlc in
   let spec' = put_DLAMSV lna (Array.of_list castlc) in
   let isunit = is_unit env_par nparams ar spec in
-  let (_,tyar) = lookup_rel (ninds+1-i) env' in
-  (env', (id,tyar,cnames,issmall,isunit,spec'))
+  let (_,tyar) = lookup_rel (ninds+1-i) env_ar in
+  ((id,tyar,cnames,issmall,isunit,spec'), cst')
 
 let add_mind sp mie env =
   mind_check_names mie;
@@ -401,20 +399,21 @@ let add_mind sp mie env =
   in
   let env_arities = push_rels types_sign env in
   let env_params = push_rels params env_arities in
-  let env_arities',_,inds =
+  let _,inds,cst =
     List.fold_left 
-      (fun (env,i,inds) ind -> 
-	 let (env',ind') = 
-	   type_one_inductive i env env_params nparams ninds ind 
+      (fun (i,inds,cst) ind -> 
+	 let (ind',cst') = 
+	   type_one_inductive i env_arities env_params nparams ninds ind 
 	 in
-	 (env',succ i,ind'::inds))
-      (env_arities,1,[]) mie.mind_entry_inds
+	 (succ i,ind'::inds, Constraint.union cst cst'))
+      (1,[],Constraint.empty) 
+      mie.mind_entry_inds
   in
   let kind = kind_of_path sp in
   let mib = 
-    cci_inductive env env_arities' kind nparams mie.mind_entry_finite inds
+    cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst
   in
-  add_mind sp mib (set_universes (universes env_arities') env)
+  add_mind sp mib (add_constraints cst env)
 
 let export = export
 let import = import