diff options
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r-- | pretyping/pretyping.ml | 83 |
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 = |