diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 293 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 12 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 54 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 13 | ||||
| -rw-r--r-- | pretyping/typing.ml | 155 | ||||
| -rw-r--r-- | pretyping/typing.mli | 18 |
7 files changed, 376 insertions, 171 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 7959b5c7c2..f7096f2682 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,64 +1,77 @@ (* $Id$ *) -open Util;; -open Generic;; -open Names;; -open Term;; -open Reduction;; -open Environ;; -open Typeops;; -open Type_errors;; -open Classops;; -open Recordops;; -open Evarconv;; +open Util +open Generic +open Names +open Term +open Reduction +open Environ +open Typeops +open Type_errors +open Classops +open Recordops +open Evarconv +open Retyping (* Typing operations dealing with coercions *) -let class_of1 env sigma t = class_of sigma (nf_ise1 env sigma t);; +let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t) let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} = - {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k} + { uj_val = nf_ise1 sigma v; + uj_type = nf_ise1 sigma t; + uj_kind = k } + let jl_nf_ise env sigma = List.map (j_nf_ise env sigma) (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function - [] -> {uj_val=applist(j_val_only funj,argl); - uj_type= typ; - uj_kind = funj.uj_kind} + | [] -> { uj_val=applist(j_val_only funj,argl); + uj_type= typ; + uj_kind = funj.uj_kind } | h::restl -> - (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *) - match whd_betadeltaiota env Evd.empty typ with - DOP2(Prod,c1,DLAM(_,c2)) -> (* Typage garanti par l'appel a app_coercion*) - apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly "apply_coercion_args" - in apply_rec [] funj.uj_type argl;; + (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *) + match whd_betadeltaiota env Evd.empty typ with + | DOP2(Prod,c1,DLAM(_,c2)) -> + (* Typage garanti par l'appel a app_coercion*) + apply_rec (h::acc) (subst1 h c2) restl + | _ -> anomaly "apply_coercion_args" + in + apply_rec [] funj.uj_type argl (* appliquer le chemin de coercions p a` hj *) let apply_pcoercion env p hj typ_cl = - if !compter then - (nbpathc := !nbpathc +1; nbcoer := !nbcoer + (List.length p)); - try fst (List.fold_left - (fun (ja,typ_cl) i -> - let fv,b= coe_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] in - let jres = apply_coercion_args env argl fv in - (if b then {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val} - else jres),jres.uj_type) - (hj,typ_cl) p) - with _ -> failwith "apply_pcoercion" + if !compter then begin + nbpathc := !nbpathc +1; + nbcoer := !nbcoer + (List.length p) + end; + try + fst (List.fold_left + (fun (ja,typ_cl) i -> + let fv,b= coe_value i in + let argl = (class_args_of typ_cl)@[ja.uj_val] in + let jres = apply_coercion_args env argl fv in + (if b then + {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val} + else + jres), + jres.uj_type) + (hj,typ_cl) p) + with _ -> + failwith "apply_pcoercion" let inh_app_fun env isevars j = - match whd_betadeltaiota env !isevars j.uj_type with - DOP2(Prod,_,DLAM(_,_)) -> j - | _ -> - (try - let t,i1 = class_of1 env !isevars j.uj_type in - let p = lookup_path_to_fun_from i1 in - apply_pcoercion env p j t - with _ -> j) + match whd_betadeltaiota env !isevars j.uj_type with + | DOP2(Prod,_,DLAM(_,_)) -> j + | _ -> + (try + let t,i1 = class_of1 env !isevars j.uj_type in + let p = lookup_path_to_fun_from i1 in + apply_pcoercion env p j t + with _ -> j) (* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *) let inh_tosort_force env isevars j = @@ -69,110 +82,126 @@ let inh_tosort_force env isevars j = let inh_tosort env isevars j = let typ = whd_betadeltaiota env !isevars j.uj_type in match typ with - DOP0(Sort(_)) -> j (* idem inh_app_fun *) - | _ -> (try inh_tosort_force env isevars j with _ -> j) + | DOP0(Sort(_)) -> j (* idem inh_app_fun *) + | _ -> (try inh_tosort_force env isevars j with _ -> j) let inh_ass_of_j env isevars j = - let typ = whd_betadeltaiota env !isevars j.uj_type in - match typ with - DOP0(Sort s) -> {body=j.uj_val;typ=s} - | _ -> - (try - let j1 = inh_tosort_force env isevars j - in assumption_of_judgment env !isevars j1 - with _ -> error_assumption CCI env (nf_ise1 env !isevars j.uj_val)) - (* try ... with _ -> ... is BAD *) + let typ = whd_betadeltaiota env !isevars j.uj_type in + match typ with + | DOP0(Sort s) -> {body=j.uj_val;typ=s} + | _ -> + (try + let j1 = inh_tosort_force env isevars j in + assumption_of_judgment env !isevars j1 + with _ -> + error_assumption CCI env (nf_ise1 !isevars j.uj_val)) + (* try ... with _ -> ... is BAD *) let inh_coerce_to1 env isevars c1 v t k = - let t1,i1 = class_of1 env !isevars c1 in - let t2,i2 = class_of1 env !isevars t in - let p = lookup_path_between (i2,i1) in - let hj = {uj_val=v;uj_type=t;uj_kind=k} in - let hj' = apply_pcoercion env p hj t2 in - if the_conv_x_leq env isevars hj'.uj_type c1 then hj' - else failwith "inh_coerce_to" + let t1,i1 = class_of1 env !isevars c1 in + let t2,i2 = class_of1 env !isevars t in + let p = lookup_path_between (i2,i1) in + let hj = {uj_val=v;uj_type=t;uj_kind=k} in + let hj' = apply_pcoercion env p hj t2 in + if the_conv_x_leq env isevars hj'.uj_type c1 then + hj' + else + failwith "inh_coerce_to" let inh_coerce_to env isevars c1 hj = inh_coerce_to1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind - + let rec inh_conv_coerce1 env isevars c1 v t k = - if the_conv_x_leq env isevars t c1 - then {uj_val=v; uj_type=t; uj_kind=k} - else try inh_coerce_to1 env isevars c1 v t k - with _ -> (* try ... with _ -> ... is BAD *) - -(* (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*) - (match (whd_betadeltaiota env !isevars t, - whd_betadeltaiota env !isevars c1) with - | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> -(* let v' = hnf_constr !isevars v in*) - let v' = whd_betadeltaiota env !isevars v in - if (match v' with - DOP2(Lambda,v1,DLAM(_,v2)) -> - the_conv_x env isevars v1 u1 (* leq v1 u1? *) - | _ -> false) - then - let (x,v1,v2) = destLambda v' in -(* let jv1 = exemeta_rec def_vty_con env isevars v1 in - let assv1 = assumption_of_judgement env !isevars jv1 in - *) - let assv1 = outcast_type v1 in - let env1 = push_rel (x,assv1) env in - let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 (mkSort (sort_of env !isevars1 t2)) in - abs_rel !isevars x assv1 h2 - else -(* - let ju1 = exemeta_rec def_vty_con env isevars u1 in - let assu1 = assumption_of_judgement env !isevars ju1 in - *) - let assu1 = outcast_type u1 in - let name = (match name with Anonymous -> Name (id_of_string "x") - | _ -> name) in - let env1 = add_rel (name,assu1) env in - let h1 = - inh_conv_coerce1 env isevars1 t1 (Rel 1) u1 (mkSort (level_of_type assu1)) in - let h2 = inh_conv_coerce1 env isevars1 u2 - (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) - (subst1 h1.uj_val t2) - (mkSort (sort_of env !isevars1 t2)) in - abs_rel !isevars name assu1 h2 - | _ -> failwith "inh_coerce_to") + if the_conv_x_leq env isevars t c1 then + {uj_val=v; uj_type=t; uj_kind=k} + else + try + inh_coerce_to1 env isevars c1 v t k + with _ -> (* try ... with _ -> ... is BAD *) + (* (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*) + (match (whd_betadeltaiota env !isevars t, + whd_betadeltaiota env !isevars c1) with + | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> + (* let v' = hnf_constr !isevars v in *) + let v' = whd_betadeltaiota env !isevars v in + if (match v' with + | DOP2(Lambda,v1,DLAM(_,v2)) -> + the_conv_x env isevars v1 u1 (* leq v1 u1? *) + | _ -> false) + then + let (x,v1,v2) = destLambda v' in + (* let jv1 = exemeta_rec def_vty_con env isevars v1 in + let assv1 = assumption_of_judgement env !isevars jv1 in *) + let assv1 = outcast_type v1 in + let env1 = push_rel (x,assv1) env in + let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 + (mkSort (get_sort_of env !isevars t2)) in + abs_rel env !isevars x assv1 h2 + else + (* let ju1 = exemeta_rec def_vty_con env isevars u1 in + let assu1 = assumption_of_judgement env !isevars ju1 in *) + let assu1 = outcast_type u1 in + let name = (match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name) in + let env1 = push_rel (name,assu1) env in + let h1 = + inh_conv_coerce1 env isevars t1 (Rel 1) u1 + (mkSort (level_of_type assu1)) in + let h2 = inh_conv_coerce1 env isevars1 u2 + (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) + (subst1 h1.uj_val t2) + (mkSort (sort_of env !isevars1 t2)) + in + abs_rel !isevars name assu1 h2 + | _ -> failwith "inh_coerce_to") let inh_conv_coerce env isevars c1 hj = inh_conv_coerce1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind let inh_cast_rel env isevars cj tj = - let cj' = (try inh_conv_coerce env isevars tj.uj_val cj - with Not_found | Failure _ -> error_actual_type CCI env - (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)) in - { uj_val = mkCast cj'.uj_val tj.uj_val; - uj_type = tj.uj_val; - uj_kind = whd_betadeltaiota env !isevars tj.uj_type} + let cj' = + try + inh_conv_coerce env isevars tj.uj_val cj + with Not_found | Failure _ -> + error_actual_type CCI env + (j_nf_ise !isevars cj) (j_nf_ise !isevars tj) + in + { uj_val = mkCast cj'.uj_val tj.uj_val; + uj_type = tj.uj_val; + uj_kind = whd_betadeltaiota env !isevars tj.uj_type } let inh_apply_rel_list nocheck env isevars argjl funj vtcon = let rec apply_rec acc typ = function - [] -> let resj = - {uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc)); - uj_type= typ; - uj_kind = funj.uj_kind} in - (match vtcon with - | (_,(_,Some typ')) -> - (try inh_conv_coerce env isevars typ' resj - with _ -> resj) (* try ... with _ -> ... is BAD *) - | (_,(_,None)) -> resj) - - | hj::restjl -> - match whd_betadeltaiota env !isevars typ with - DOP2(Prod,c1,DLAM(_,c2)) -> - let hj' = - if nocheck then hj else - (try inh_conv_coerce env isevars c1 hj - with (Failure _ | Not_found) -> - error_cant_apply "Type Error" CCI env - (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) in - apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl - | _ -> - error_cant_apply "Non-functional construction" CCI env - (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl) - in apply_rec [] funj.uj_type argjl -;; + | [] -> + let resj = + { uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc)); + uj_type= typ; + uj_kind = funj.uj_kind } + in + (match vtcon with + | (_,(_,Some typ')) -> + (try inh_conv_coerce env isevars typ' resj + with _ -> resj) (* try ... with _ -> ... is BAD *) + | (_,(_,None)) -> resj) + + | hj::restjl -> + match whd_betadeltaiota env !isevars typ with + | DOP2(Prod,c1,DLAM(_,c2)) -> + let hj' = + if nocheck then + hj + else + (try + inh_conv_coerce env isevars c1 hj + with Failure _ | Not_found -> + error_cant_apply "Type Error" CCI env + (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) + in + apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl + | _ -> + error_cant_apply "Non-functional construction" CCI env + (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl) + in + apply_rec [] funj.uj_type argjl + diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cd9e6d9211..5af5fb9156 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -8,7 +8,7 @@ open Term open Reduction open Instantiate open Environ -open Typing_ev +open Typing open Classops open Recordops open Evarutil diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 43653f80d4..226b6ff0de 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -45,7 +45,7 @@ let filter_sign p sign x = (* All ids of sign must be distincts! *) let new_isevar_sign env sigma typ args = - let sign = get_globals (context env) in + let sign = var_context env in if not (list_distinct (ids_of_sign sign)) then error "new_isevar_sign: two vars have the same name"; let newev = Evd.new_evar() in @@ -60,7 +60,7 @@ let dummy_sort = mkType dummy_univ (* Declaring any type to be in the sort Type shouldn't be harmful since cumulativity now includes Prop and Set in Type. *) let new_type_var env sigma = - let sign = get_globals (context env) in + let sign = var_context env in let args = (Array.of_list (List.map mkVar (ids_of_sign sign))) in let (sigma',c) = new_isevar_sign env sigma dummy_sort args in (sigma', make_typed c (Type dummy_univ)) @@ -70,7 +70,7 @@ let split_evar_to_arrow sigma c = let evd = Evd.map sigma ev in let evenv = evd.evar_env in let (sigma1,dom) = new_type_var evenv sigma in - let hyps = get_globals (context evenv) in + let hyps = var_context evenv in let nvar = next_ident_away (id_of_string "x") (ids_of_sign hyps) in let nevenv = push_var (nvar,dom) evenv in let (sigma2,rng) = new_type_var nevenv sigma1 in @@ -97,7 +97,7 @@ let do_restrict_hyps sigma c = let args = Array.to_list args in let evd = Evd.map sigma ev in let env = evd.evar_env in - let hyps = get_globals (context env) in + let hyps = var_context env in let (_,(rsign,ncargs)) = List.fold_left (fun (sign,(rs,na)) a -> @@ -244,7 +244,7 @@ let evar_define isevars lhs rhs = let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit) (Array.to_list argsv) in let evd = ise_map isevars ev in - let hyps = get_globals (context evd.evar_env) in + let hyps = var_context evd.evar_env in (* the substitution to invert *) let worklist = List.combine (ids_of_sign hyps) args in let body = real_clean isevars ev worklist rhs in @@ -263,7 +263,7 @@ let solve_refl conv_algo isevars c1 c2 = and (_,argsv2) = destEvar c2 in let evd = Evd.map !isevars ev in let env = evd.evar_env in - let hyps = get_globals (context env) in + let hyps = var_context env in let (_,rsign) = array_fold_left2 (fun (sgn,rsgn) a1 a2 -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1e6245a471..500e6bfe74 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -146,17 +146,17 @@ let mt_evd = Evd.empty let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) -let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} = - {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k} +let j_nf_ise sigma {uj_val=v;uj_type=t;uj_kind=k} = + {uj_val=nf_ise1 sigma v;uj_type=nf_ise1 sigma t;uj_kind=k} -let jv_nf_ise env sigma = Array.map (j_nf_ise env sigma) +let jv_nf_ise sigma = Array.map (j_nf_ise sigma) (* Utilisé pour inférer le prédicat des Cases *) (* Semble exagérement fort *) (* Faudra préférer une unification entre les types de toutes les clauses *) (* et autoriser des ? à rester dans le résultat de l'unification *) -let has_ise env sigma t = - try let _ = whd_ise env sigma t in true +let has_ise sigma t = + try let _ = whd_ise sigma t in true with UserError _ -> false let evar_type_fixpoint env isevars lna lar vdefj = @@ -166,8 +166,8 @@ let evar_type_fixpoint env isevars lna lar vdefj = if not (the_conv_x_leq env isevars (vdefj.(i)).uj_type (lift lt (body_of_type lar.(i)))) then error_ill_typed_rec_body CCI env i lna - (jv_nf_ise env !isevars vdefj) - (Array.map (typed_app (nf_ise1 env !isevars)) lar) + (jv_nf_ise !isevars vdefj) + (Array.map (typed_app (nf_ise1 !isevars)) lar) done @@ -183,7 +183,7 @@ let cast_rel isevars env cj tj = let let_path = make_path ["Core"] (id_of_string "let") CCI let wrong_number_of_cases_message loc env isevars (c,ct) expn = - let c = nf_ise1 env !isevars c and ct = nf_ise1 env !isevars ct in + let c = nf_ise1 !isevars c and ct = nf_ise1 !isevars ct in error_number_branches_loc loc CCI env c ct expn let check_branches_message loc env isevars (c,ct) (explft,lft) = @@ -191,10 +191,11 @@ let check_branches_message loc env isevars (c,ct) (explft,lft) = if n<>expn then wrong_number_of_cases_message loc env isevars (c,ct) expn; for i = 0 to n-1 do if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then - let c = nf_ise1 env !isevars c - and ct = nf_ise1 env !isevars ct - and lfi = nf_betaiota env !isevars (nf_ise1 env !isevars lft.(i)) in - error_ill_formed_branch_loc loc CCI env c i lfi (nf_betaiota env !isevars explft.(i)) + let c = nf_ise1 !isevars c + and ct = nf_ise1 !isevars ct + and lfi = nf_betaiota env !isevars (nf_ise1 !isevars lft.(i)) in + error_ill_formed_branch_loc loc CCI env c i lfi + (nf_betaiota env !isevars explft.(i)) done (* @@ -287,10 +288,10 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let (valc,typc) = destCast v in {uj_val=valc; uj_type=typc; uj_kind=dummy_sort} | (false,(None,Some ty)) -> - let (c,ty) = new_isevar env isevars ty CCI in + let (c,ty) = new_isevar isevars env ty CCI in {uj_val=c;uj_type=ty;uj_kind = dummy_sort} | (true,(None,None)) -> - let (c,ty) = new_isevar env isevars (mkCast dummy_sort dummy_sort) CCI in + let (c,ty) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in {uj_val=c;uj_type=ty;uj_kind = dummy_sort} | (false,(None,None)) -> (match loc with @@ -336,19 +337,20 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let j = pretype mt_tycon env isevars f in let j = inh_app_fun env isevars j in let apply_one_arg (tycon,jl) c = - let cj = pretype (app_dom_tycon isevars tycon) env isevars c in - let rtc = app_rng_tycon isevars cj.uj_val tycon in + let cj = pretype (app_dom_tycon env isevars tycon) env isevars c in + let rtc = app_rng_tycon env isevars cj.uj_val tycon in (rtc,cj::jl) in let jl = List.rev (snd (List.fold_left apply_one_arg (mk_tycon j.uj_type,[]) args)) in inh_apply_rel_list !trad_nocheck env isevars jl j vtcon | RBinder(loc,BLambda,name,c1,c2) -> - let j = pretype (abs_dom_valcon isevars vtcon) env isevars c1 in + let j = pretype (abs_dom_valcon env isevars vtcon) env isevars c1 in let assum = inh_ass_of_j env isevars j in let var = (name,assum) in let j' = - pretype (abs_rng_tycon isevars vtcon) (push_rel var env) isevars c2 in + pretype (abs_rng_tycon env isevars vtcon) (push_rel var env) isevars c2 + in fst (abs_rel env !isevars name assum j') | RBinder(loc,BProd,name,c1,c2) -> @@ -364,7 +366,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let (mind,_) = try find_mrectype env !isevars cj.uj_type with Induc -> error_case_not_inductive CCI env - (nf_ise1 env !isevars cj.uj_val) (nf_ise1 env !isevars 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 mt_tycon env isevars p | None -> @@ -382,11 +384,11 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) try let expti = Indrec.branch_scheme env !isevars isrec i cj.uj_type in let fj = pretype (mk_tycon expti) env isevars lf.(i-1) in - let efjt = nf_ise1 env !isevars fj.uj_type in + let efjt = nf_ise1 !isevars fj.uj_type in let pred = Indrec.pred_case_ml_onebranch env !isevars isrec (cj.uj_val,cj.uj_type) (i,fj.uj_val,efjt) in - if has_ise env !isevars pred then findtype (i+1) + if has_ise !isevars pred then findtype (i+1) else let pty = Retyping.get_type_of env !isevars pred in let k = Retyping.get_type_of env !isevars pty in @@ -394,8 +396,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) with UserError _ -> findtype (i+1) in findtype 1 in - let evalct = nf_ise1 env !isevars cj.uj_type - and evalPt = nf_ise1 env !isevars pj.uj_type in + let evalct = nf_ise1 !isevars cj.uj_type + and evalPt = nf_ise1 !isevars pj.uj_type in let (mind,bty,rsty) = Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in @@ -474,20 +476,20 @@ let j_apply f env sigma j = let ise_resolve fail_evar sigma metamap env c = let isevars = ref sigma in let j = unsafe_fmachine mt_tycon false isevars metamap env c in - j_apply (process_evars fail_evar) env !isevars j + 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 (process_evars fail_evar) env !isevars) tj + 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 mt_tycon true isevars metamap env c in - j_apply (process_evars true) env !isevars j + j_apply (fun _ -> process_evars true) env !isevars j let ise_resolve1 is_ass sigma env c = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index b4fee1cd29..84097f8581 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -40,24 +40,25 @@ 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 -> 'c evar_map -> (int * constr) list -> +val ise_resolve : bool -> unit evar_map -> (int * constr) list -> unsafe_env -> rawconstr -> unsafe_judgment -val ise_resolve_type : bool -> 'c evar_map -> (int * constr) list -> +val ise_resolve_type : bool -> unit evar_map -> (int * constr) list -> unsafe_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 -> 'c evar_map -> unsafe_env -> rawconstr -> constr +val ise_resolve1 : bool -> unit evar_map -> unsafe_env -> rawconstr -> constr (* progmach.ml tries to type ill-typed terms: does not perform the conversion * test in application. *) -val ise_resolve_nocheck : 'c evar_map -> (int * constr) list -> +val ise_resolve_nocheck : unit evar_map -> (int * constr) list -> unsafe_env -> rawconstr -> unsafe_judgment (* Internal of Trad... * Unused outside Trad, but useful for debugging *) -val pretype : bool * (constr option * constr option) - -> unsafe_env -> 'c evar_defs -> rawconstr -> unsafe_judgment +val pretype : + trad_constraint -> unsafe_env -> unit evar_defs -> rawconstr + -> unsafe_judgment diff --git a/pretyping/typing.ml b/pretyping/typing.ml new file mode 100644 index 0000000000..c12f9bb34f --- /dev/null +++ b/pretyping/typing.ml @@ -0,0 +1,155 @@ + +(* $Id$ *) + +open Util +open Names +open Generic +open Term +open Environ +open Reduction +open Type_errors +open Typeops + +let vect_lift = Array.mapi lift +let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) + +type 'a mach_flags = { + fix : bool; + nocheck : bool } + +(* The typing machine without information, without universes but with + existential variables. *) + +let rec execute mf env sigma cstr = + match kind_of_term cstr with + | IsMeta n -> + error "execute: found a non-instanciated goal" + + | IsEvar _ -> + let ty = type_of_existential env sigma cstr in + let jty = execute mf env sigma ty in + { uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type } + + | IsRel n -> + relative env n + + | IsVar id -> + make_judge cstr (snd (lookup_var id env)) + + | IsAbst _ -> + if evaluable_abst env cstr then + execute mf env sigma (abst_value env cstr) + else + error "Cannot typecheck an unevaluable abstraction" + + | IsConst _ -> + make_judge cstr (type_of_constant env sigma cstr) + + | IsMutInd _ -> + make_judge cstr (type_of_inductive env sigma cstr) + + | IsMutConstruct _ -> + let (typ,kind) = destCast (type_of_constructor env sigma cstr) in + { uj_val = cstr; uj_type = typ; uj_kind = kind } + + | IsMutCase (_,p,c,lf) -> + let cj = execute mf env sigma c in + let pj = execute mf env sigma p in + let lfj = execute_array mf env sigma lf in + type_of_case env sigma pj cj lfj + + | 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 = execute_fix mf env sigma lar lfi vdef in + let fix = mkFix vn i larv lfi vdefv in + check_fix env sigma fix; + make_judge fix larv.(i) + + | IsCoFix (i,lar,lfi,vdef) -> + let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in + let cofix = mkCoFix i larv lfi vdefv in + check_cofix env sigma cofix; + make_judge cofix larv.(i) + + | IsSort (Prop c) -> + make_judge_of_prop_contents c + + | IsSort (Type u) -> + let (j,_) = make_judge_of_type u in j + + | IsAppL (f,args) -> + let j = execute mf env sigma f in + let jl = execute_list mf env sigma args in + let (j,_) = apply_rel_list env sigma mf.nocheck jl j in + j + + | IsLambda (name,c1,c2) -> + let j = execute mf env sigma c1 in + let var = assumption_of_judgment env sigma j in + let env1 = push_rel (name,var) env in + let j' = execute mf env1 sigma c2 in + let (j,_) = abs_rel env1 sigma name var j' in + j + + | IsProd (name,c1,c2) -> + let j = execute mf env sigma c1 in + let var = assumption_of_judgment env sigma j in + let env1 = push_rel (name,var) env in + let j' = execute mf env1 sigma c2 in + let (j,_) = gen_rel env1 sigma name var j' in + j + + | IsCast (c,t) -> + let cj = execute mf env sigma c in + let tj = execute mf env sigma t in + cast_rel env sigma cj tj + + | _ -> error_cant_execute CCI env cstr + +and execute_fix mf env sigma lar lfi vdef = + let larj = execute_array mf env sigma lar in + let lara = Array.map (assumption_of_judgment env sigma) larj in + let nlara = + List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in + let env1 = + List.fold_left (fun env nvar -> push_rel nvar env) env nlara in + let vdefj = execute_array mf env1 sigma vdef in + let vdefv = Array.map j_val_only vdefj in + let cst3 = type_fixpoint env1 sigma lfi lara vdefj in + (lara,vdefv) + +and execute_array mf env sigma v = + let jl = execute_list mf env sigma (Array.to_list v) in + Array.of_list jl + +and execute_list mf env sigma = function + | [] -> + [] + | c::r -> + let j = execute mf env sigma c in + let jr = execute_list mf env sigma r in + j::jr + + +let safe_machine env sigma constr = + let mf = { fix = false; nocheck = false } in + execute mf env sigma constr + + +(* Type of a constr *) + +let type_of env sigma c = + let j = safe_machine env sigma c in + nf_betaiota env sigma j.uj_type + +(* The typed type of a judgment. *) + +let execute_type env sigma constr = + let j = execute { fix=false; nocheck=true } env sigma constr in + assumption_of_judgment env sigma j + +let execute_rec_type env sigma constr = + let j = execute { fix=false; nocheck=false } env sigma constr in + assumption_of_judgment env sigma j + diff --git a/pretyping/typing.mli b/pretyping/typing.mli new file mode 100644 index 0000000000..b12cd369d3 --- /dev/null +++ b/pretyping/typing.mli @@ -0,0 +1,18 @@ + +(* $Id$ *) + +(*i*) +open Term +open Environ +open Evd +(*i*) + +(* This module provides the typing machine with existential variables + (but without universes). *) + +val type_of : unsafe_env -> 'a evar_map -> constr -> constr + +val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type + +val execute_rec_type : unsafe_env -> 'a evar_map -> constr -> typed_type + |