Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

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

1 files changed, 33 insertions, 50 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9caab6bcc..ff10083ff 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -95,10 +95,10 @@ let ctxt_of_ids cl = cl
 
 let mt_evd = Evd.empty
 
-let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
 let j_nf_ise sigma {uj_val=v;uj_type=t} =
-  {uj_val=nf_ise1 sigma v;uj_type=typed_app (nf_ise1 sigma) t}
+  {uj_val=nf_ise1 sigma v;uj_type=type_app (nf_ise1 sigma) t}
 
 let jv_nf_ise sigma = Array.map (j_nf_ise sigma)
 
@@ -112,23 +112,13 @@ let evar_type_fixpoint env isevars lna lar vdefj =
     if Array.length lar = lt then 
       for i = 0 to lt-1 do 
         if not (the_conv_x_leq env isevars
-		  (body_of_type (vdefj.(i)).uj_type)
-		  (lift lt (body_of_type lar.(i)))) then
+		  (vdefj.(i)).uj_type
+		  (lift lt lar.(i))) then
           error_ill_typed_rec_body CCI env i lna 
 	    (jv_nf_ise !isevars vdefj) 
-	    (Array.map (typed_app (nf_ise1 !isevars)) lar)
+	    (Array.map (type_app (nf_ise1 !isevars)) lar)
       done
 
-
-(* Inutile ?
-let cast_rel isevars env cj tj =
-    if the_conv_x_leq isevars env cj.uj_type tj.uj_val then
-        {uj_val=j_val_only cj;
-         uj_type=tj.uj_val;
-         uj_kind = hnf_constr !isevars tj.uj_type}
-   else error_actual_type CCI env (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)
-
-*)
 let let_path = make_path ["Core"] (id_of_string "let") CCI
 
 let wrong_number_of_cases_message loc env isevars (c,ct) expn = 
@@ -156,7 +146,7 @@ let pretype_id loc env lvar id =
   with Not_found ->
   try
     let (n,typ) = lookup_rel_id id (rel_context env) in
-    { uj_val  = mkRel n; uj_type = typed_app (lift n) typ }
+    { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
   with Not_found ->
   try
     let typ = lookup_id_type id (named_context env) in
@@ -183,7 +173,7 @@ let pretype_ref pretype loc isevars env lvar = function
 	mkEvar ev
     in
     let typ = existential_type !isevars ev in
-    make_judge body (Retyping.get_assumption_of env !isevars typ)
+    make_judge body typ
 
 | RInd (ind_sp,ctxt) ->
     let ind = (ind_sp,Array.map pretype ctxt) in
@@ -198,7 +188,7 @@ let pretype_sort = function
   | RProp c -> judge_of_prop_contents c
   | RType ->
       { uj_val = dummy_sort;
-	uj_type = make_typed dummy_sort (Type Univ.dummy_univ) }
+	uj_type = dummy_sort }
 
 (* pretype tycon isevars env constr tries to solve the *)
 (* existential variables in constr in environment env with the *)
@@ -223,9 +213,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 | RHole loc ->
   if !compter then nbimpl:=!nbimpl+1;
   (match tycon with
-  | Some ty ->
-      let c = new_isevar isevars env ty CCI in
-      {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
+  | Some ty -> { uj_val = new_isevar isevars env ty CCI; uj_type = ty }
   | None ->
       (match loc with
 	   None -> anomaly "There is an implicit argument I cannot solve"
@@ -249,14 +237,13 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
         pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars lvar
           lmeta def) vdef in
   (evar_type_fixpoint env isevars lfi lara vdefj;
-   let larav = Array.map body_of_type lara in
    match fixkind with
      | RFix (vn,i as vni) ->
-	 let fix = (vni,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+	 let fix = (vni,(lara,List.rev lfi,Array.map j_val vdefj)) in
 	 check_fix env !isevars fix;
 	 make_judge (mkFix fix) lara.(i)
      | RCoFix i -> 
-	 let cofix = (i,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+	 let cofix = (i,(lara,List.rev lfi,Array.map j_val vdefj)) in
 	 check_cofix env !isevars cofix;
 	 make_judge (mkCoFix cofix) lara.(i))
 
@@ -271,14 +258,14 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       let rng_tycon = option_app (subst1 cj.uj_val) rng in
       (rng_tycon,cj::jl)  in
     let jl = List.rev (snd (List.fold_left apply_one_arg
-			      (mk_tycon (body_of_type j.uj_type),[]) args)) in
-    inh_apply_rel_list false loc env isevars jl j tycon
+			      (mk_tycon j.uj_type,[]) args)) in
+    inh_apply_rel_list loc env isevars jl j tycon
 
 | RBinder(loc,BLambda,name,c1,c2)      ->
     let (dom,rng) = split_tycon loc env isevars tycon in
     let dom_valcon = valcon_of_tycon dom in
     let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
-    let assum = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
+    let assum = (inh_ass_of_j env isevars j).utj_val in
     let var = (name,assum) in
     let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2 
     in 
@@ -287,7 +274,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 | RBinder(loc,BProd,name,c1,c2)        ->
     let j = pretype empty_tycon env isevars lvar lmeta c1 in
     let assum = inh_ass_of_j env isevars j in
-    let var = (name,assumption_of_type_judgment assum) in
+    let var = (name,assum.utj_val) in
     let j' = pretype empty_tycon (push_rel_assum var env) isevars lvar lmeta c2 in
     (try fst (gen_rel env !isevars name assum j')
      with TypeError _ as e -> Stdpp.raise_with_loc loc e)
@@ -296,15 +283,15 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
     let j = pretype empty_tycon env isevars lvar lmeta c1 in
     let var = (name,j.uj_val,j.uj_type) in
     let j' = pretype tycon (push_rel_def var env) isevars lvar lmeta c2 in
-    { uj_val = mkLetIn (name, j.uj_val, body_of_type j.uj_type, j'.uj_val) ;
-      uj_type = typed_app (subst1 j.uj_val) j'.uj_type }
+    { uj_val = mkLetIn (name, j.uj_val, j.uj_type, j'.uj_val) ;
+      uj_type = type_app (subst1 j.uj_val) j'.uj_type }
 
 | ROldCase (loc,isrec,po,c,lf) ->
   let cj = pretype empty_tycon env isevars lvar lmeta c in
   let (IndType (indf,realargs) as indt) = 
-    try find_rectype env !isevars (body_of_type cj.uj_type)
+    try find_rectype env !isevars cj.uj_type
     with Induc -> error_case_not_inductive CCI env
-	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars (body_of_type cj.uj_type)) in
+	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
   let pj = match po with
     | Some p -> pretype empty_tycon env isevars lvar lmeta p
     | None -> 
@@ -323,34 +310,34 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 		let expti = expbr.(i) in
 		let fj =
                   pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
-		let efjt = nf_ise1 !isevars (body_of_type fj.uj_type) in 
+		let efjt = nf_ise1 !isevars fj.uj_type in 
 		let pred = 
 		  Cases.pred_case_ml_onebranch env !isevars isrec indt
 		    (i,fj.uj_val,efjt) in
 		if has_ise !isevars pred then findtype (i+1)
 		else 
 		  let pty = Retyping.get_type_of env !isevars pred in
-		  { uj_val=pred; 
-		    uj_type = Retyping.get_assumption_of env !isevars pty }
+		  { uj_val = pred; 
+		    uj_type = pty }
 	      with UserError _ -> findtype (i+1) in
 	    findtype 0 in
 
-  let evalct = find_rectype env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
-  and evalPt = nf_ise1 !isevars (body_of_type pj.uj_type) in
+  let evalct = find_rectype env !isevars cj.uj_type (*Pour normaliser evars*)
+  and evalPt = nf_ise1 !isevars pj.uj_type in
 
   let (bty,rsty) =
     Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
   if Array.length bty <> Array.length lf then
     wrong_number_of_cases_message loc env isevars 
-      (cj.uj_val,nf_ise1 !isevars (body_of_type cj.uj_type))
+      (cj.uj_val,nf_ise1 !isevars cj.uj_type)
       (Array.length bty)
   else
     let lfj =
       array_map2
         (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar lmeta f) bty
           lf in
-    let lfv = (Array.map (fun j -> j.uj_val) lfj) in
-    let lft = (Array.map (fun j -> body_of_type j.uj_type) lfj) in
+    let lfv = Array.map j_val lfj in
+    let lft = Array.map (fun j -> j.uj_type) lfj in
     check_branches_message loc env isevars cj.uj_val (bty,lft);
     let v =
       if isrec
@@ -361,9 +348,8 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	let ci = make_default_case_info mis in
 	mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map (fun j-> j.uj_val) lfj)
     in
-    let s = snd (splay_arity env !isevars evalPt) in
     {uj_val = v;
-     uj_type = make_typed rsty s }
+     uj_type = rsty }
 
 | RCases (loc,prinfo,po,tml,eqns) ->
     Cases.compile_cases loc
@@ -376,9 +362,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
   let cj = pretype (mk_tycon tj.utj_val) env isevars lvar lmeta c in
   match tycon with
     | None  -> cj
-    | Some t' -> 
-	let tj' = Retyping.get_assumption_of env !isevars t' in
-	inh_conv_coerce_to loc env isevars cj tj'
+    | Some t' -> inh_conv_coerce_to loc env isevars cj t'
 
 and pretype_type valcon env isevars lvar lmeta = function
 | RHole loc ->
@@ -386,9 +370,8 @@ and pretype_type valcon env isevars lvar lmeta = function
     (match valcon with
        | Some v -> Retyping.get_judgment_of env !isevars v
        | None ->
-	   let ty = dummy_sort in
-	   let c = new_isevar isevars env ty CCI in
-	   { uj_val = c ; uj_type = make_typed ty (Type Univ.dummy_univ) })
+	   { uj_val = new_isevar isevars env dummy_sort CCI;
+	     uj_type = dummy_sort })
 | c ->
   let j = pretype empty_tycon env isevars lvar lmeta c in
   let tj = inh_tosort env isevars j in
@@ -453,7 +436,7 @@ let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
   let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in
   let metamap = ref [] in
   let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
-  let t = typed_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
+  let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
   !metamap, {uj_val = v; uj_type = t }
 
 let ise_resolve_casted sigma env typ c =
@@ -468,7 +451,7 @@ let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c =
   let j = unsafe_infer tycon isevars env lvar lmeta c in
   let metamap = ref [] in
   let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
-  let t = typed_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
+  let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
   !metamap, {uj_val = v; uj_type = t }
 
 let ise_infer_type_gen fail_evar sigma env lvar lmeta c =