diff options
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 6 | ||||
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 313 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 76 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 2 |
4 files changed, 184 insertions, 213 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 0bfafa492..6ffb36e41 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -58,7 +58,7 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in - let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in + let c' = SPretyping.understand_tcc_evars isevars env kind c' in evar_nf isevars c' let interp_constr isevars env c = @@ -76,7 +76,7 @@ let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = let interp_open_constr isevars env c = msgnl (str "Pretyping " ++ my_print_constr_expr c); let c = Constrintern.intern_constr ( !isevars) env c in - let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in + let c' = SPretyping.understand_tcc_evars isevars env (OfType None) c in evar_nf isevars c' let interp_constr_judgment isevars env c = @@ -96,7 +96,7 @@ let locate_if_isevar loc na = function let interp_binder sigma env na t = let t = Constrintern.intern_gen true ( !sigma) env t in - SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t) + SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t) let interp_context_evars evdref env params = let bl = Constrintern.intern_context false ( !evdref) env params in diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 5003b60a7..23d845732 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -46,24 +46,24 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref true - let evd_comb0 f isevars = - let (evd',x) = f !isevars in - isevars := evd'; + let evd_comb0 f evdref = + let (evd',x) = f !evdref in + evdref := evd'; x - let evd_comb1 f isevars x = - let (evd',y) = f !isevars x in - isevars := evd'; + let evd_comb1 f evdref x = + let (evd',y) = f !evdref x in + evdref := evd'; y - let evd_comb2 f isevars x y = - let (evd',z) = f !isevars x y in - isevars := evd'; + let evd_comb2 f evdref x y = + let (evd',z) = f !evdref x y in + evdref := evd'; z - let evd_comb3 f isevars x y z = - let (evd',t) = f !isevars x y z in - isevars := evd'; + let evd_comb3 f evdref x y z = + let (evd',t) = f !evdref x y z in + evdref := evd'; t let mt_evd = Evd.empty @@ -73,34 +73,34 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* 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 evar_type_fixpoint loc env isevars lna lar vdefj = + let evar_type_fixpoint loc env evdref lna lar vdefj = let lt = Array.length vdefj in if Array.length lar = lt then for i = 0 to lt-1 do - if not (e_cumul env isevars (vdefj.(i)).uj_type + if not (e_cumul env evdref (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env ( !isevars) + error_ill_typed_rec_body_loc loc env ( !evdref) i lna vdefj lar done - let check_branches_message loc env isevars c (explft,lft) = + let check_branches_message loc env evdref c (explft,lft) = for i = 0 to Array.length explft - 1 do - if not (e_cumul env isevars lft.(i) explft.(i)) then - let sigma = !isevars in + if not (e_cumul env evdref lft.(i) explft.(i)) then + let sigma = !evdref in error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i) done (* coerce to tycon if any *) - let inh_conv_coerce_to_tycon loc env isevars j = function - | None -> j_nf_isevar !isevars j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t + let inh_conv_coerce_to_tycon loc env evdref j = function + | None -> j_nf_evar !evdref j + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t let push_rels vars env = List.fold_right push_rel vars env (* - let evar_type_case isevars env ct pt lft p c = - let (mind,bty,rslty) = type_case_branches env ( isevars) ct pt p c - in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty) + let evar_type_case evdref env ct pt lft p c = + let (mind,bty,rslty) = type_case_branches env ( evdref) ct pt p c + in check_branches_message evdref env (c,ct) (bty,lft); (mind,rslty) *) let strip_meta id = (* For Grammar v7 compatibility *) @@ -149,7 +149,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (*************************************************************************) (* Main pretyping function *) - let pretype_ref isevars env ref = + let pretype_ref evdref env ref = let c = constr_of_global ref in make_judge c (Retyping.get_type_of env Evd.empty c) @@ -157,35 +157,35 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RProp c -> judge_of_prop_contents c | RType _ -> judge_of_new_Type () - (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *) - (* in environment [env], with existential variables [( isevars)] and *) + (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) + (* in environment [env], with existential variables [( evdref)] and *) (* the type constraint tycon *) - let rec pretype (tycon : type_constraint) env isevars lvar c = + let rec pretype (tycon : type_constraint) env evdref lvar c = (* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *) (* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) (* with _ -> () *) (* in *) match c with | RRef (loc,ref) -> - inh_conv_coerce_to_tycon loc env isevars - (pretype_ref isevars env ref) + inh_conv_coerce_to_tycon loc env evdref + (pretype_ref evdref env ref) tycon | RVar (loc, id) -> - inh_conv_coerce_to_tycon loc env isevars + inh_conv_coerce_to_tycon loc env evdref (pretype_id loc env lvar id) tycon | REvar (loc, ev, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = evar_context (Evd.find ( !isevars) ev) in + let hyps = evar_context (Evd.find ( !evdref) ev) in let args = match instopt with | None -> instance_from_named_context hyps | Some inst -> failwith "Evar subtitutions not implemented" in let c = mkEvar (ev, args) in - let j = (Retyping.get_judgment_of env ( !isevars) c) in - inh_conv_coerce_to_tycon loc env isevars j tycon + let j = (Retyping.get_judgment_of env ( !evdref) c) in + inh_conv_coerce_to_tycon loc env evdref j tycon | RPatVar (loc,(someta,n)) -> anomaly "Found a pattern variable in a rawterm to type" @@ -195,26 +195,26 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct match tycon with | Some (None, ty) -> ty | None | Some _ -> - e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in - { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty } + e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in + { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } | RRec (loc,fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt | (na,k,None,ty)::bl -> - let ty' = pretype_type empty_valcon env isevars lvar ty in + let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = (na,None,ty'.utj_val) in type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl | (na,k,Some bd,ty)::bl -> - let ty' = pretype_type empty_valcon env isevars lvar ty in - let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in + let ty' = pretype_type empty_valcon env evdref lvar ty in + let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar ty in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in let ctxtv = Array.map (type_bl env empty_rel_context) bl in let larj = array_map2 (fun e ar -> - pretype_type empty_valcon (push_rel_context e env) isevars lvar ar) + pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in @@ -223,7 +223,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* Note: bodies are not used by push_rec_types, so [||] is safe *) let newenv = let marked_ftys = - Array.map (fun ty -> let sort = Retyping.get_type_of env !isevars ty in + Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in mkApp (Lazy.force Subtac_utils.fix_proto, [| sort; ty |])) ftys in @@ -237,9 +237,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let ty = ftys.(i) in if i = fixi then ( Option.iter (fun tycon -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars ftys.(i) tycon) + evdref := Coercion.inh_conv_coerces_to loc env !evdref ftys.(i) tycon) tycon; - nf_isevar !isevars ty) + nf_evar !evdref ty) else ty in (* we lift nbfix times the type in tycon, because of @@ -248,13 +248,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct decompose_prod_n_assum (rel_context_length ctxt) (lift nbfix fty) in let nenv = push_rel_context ctxt newenv in - let j = pretype (mk_tycon ty) nenv isevars lvar def in + let j = pretype (mk_tycon ty) nenv evdref lvar def in { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - evar_type_fixpoint loc env isevars names ftys vdefj; - let ftys = Array.map (nf_evar ( !isevars)) ftys in - let fdefs = Array.map (fun x -> nf_evar ( !isevars) (j_val x)) vdefj in + evar_type_fixpoint loc env evdref names ftys vdefj; + let ftys = Array.map (nf_evar ( !evdref)) ftys in + let fdefs = Array.map (fun x -> nf_evar ( !evdref) (j_val x)) vdefj in let fixj = match fixkind with | RFix (vn,i) -> (* First, let's find the guard indexes. *) @@ -276,10 +276,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon loc env isevars fixj tycon + inh_conv_coerce_to_tycon loc env evdref fixj tycon | RSort (loc,s) -> - inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon + inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon | RApp (loc,f,args) -> let length = List.length args in @@ -297,44 +297,44 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty | _ -> None in - let fj = pretype ftycon env isevars lvar f in + let fj = pretype ftycon env evdref lvar f in let floc = loc_of_rawconstr f in let rec apply_rec env n resj tycon = function | [] -> resj | c::rest -> let argloc = loc_of_rawconstr c in - let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in - let resty = whd_betadeltaiota env ( !isevars) resj.uj_type in + let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in + let resty = whd_betadeltaiota env ( !evdref) resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> - Option.iter (fun ty -> isevars := - Coercion.inh_conv_coerces_to loc env !isevars resty ty) tycon; - let evd, (_, _, tycon) = split_tycon loc env !isevars tycon in - isevars := evd; - let hj = pretype (mk_tycon (nf_isevar !isevars c1)) env isevars lvar c in + Option.iter (fun ty -> evdref := + Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon; + let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in + evdref := evd; + let hj = pretype (mk_tycon (nf_evar !evdref c1)) env evdref lvar c in let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in - let typ' = nf_isevar !isevars typ in + let typ' = nf_evar !evdref typ in apply_rec env (n+1) - { uj_val = nf_isevar !isevars value; - uj_type = nf_isevar !isevars typ' } - (Option.map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest + { uj_val = nf_evar !evdref value; + uj_type = nf_evar !evdref typ' } + (Option.map (fun (abs, c) -> abs, nf_evar !evdref c) tycon) rest | _ -> - let hj = pretype empty_tycon env isevars lvar c in + let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional_loc - (join_loc floc argloc) env ( !isevars) + (join_loc floc argloc) env ( !evdref) resj [hj] in - let resj = j_nf_evar ( !isevars) (apply_rec env 1 fj ftycon args) in + let resj = j_nf_evar ( !evdref) (apply_rec env 1 fj ftycon args) in let resj = match kind_of_term resj.uj_val with | App (f,args) when isInd f or isConst f -> - let sigma = !isevars in + let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in let t = Retyping.get_type_of env sigma c in make_judge c t | _ -> resj in - inh_conv_coerce_to_tycon loc env isevars resj tycon + inh_conv_coerce_to_tycon loc env evdref resj tycon | RLambda(loc,name,k,c1,c2) -> let tycon' = evd_comb1 @@ -344,42 +344,42 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | Some ty -> let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in evd, Some ty') - isevars tycon + evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in - let j = pretype_type dom_valcon env isevars lvar c1 in + let j = pretype_type dom_valcon env evdref lvar c1 in let var = (name,None,j.utj_val) in - let j' = pretype rng (push_rel var env) isevars lvar c2 in + let j' = pretype rng (push_rel var env) evdref lvar c2 in let resj = judge_of_abstraction env name j j' in - inh_conv_coerce_to_tycon loc env isevars resj tycon + inh_conv_coerce_to_tycon loc env evdref resj tycon | RProd(loc,name,k,c1,c2) -> - let j = pretype_type empty_valcon env isevars lvar c1 in + let j = pretype_type empty_valcon env evdref lvar c1 in let var = (name,j.utj_val) in let env' = push_rel_assum var env in - let j' = pretype_type empty_valcon env' isevars lvar c2 in + let j' = pretype_type empty_valcon env' evdref lvar c2 in let resj = 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 + inh_conv_coerce_to_tycon loc env evdref resj tycon | RLetIn(loc,name,c1,c2) -> - let j = pretype empty_tycon env isevars lvar c1 in + let j = pretype empty_tycon env evdref lvar c1 in let t = refresh_universes j.uj_type in let var = (name,Some j.uj_val,t) in let tycon = lift_tycon 1 tycon in - let j' = pretype tycon (push_rel var env) isevars lvar c2 in + let j' = pretype tycon (push_rel var env) evdref lvar c2 in { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } | RLetTuple (loc,nal,(na,po),c,d) -> - let cj = pretype empty_tycon env isevars lvar c in + let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env ( !isevars) cj.uj_type + try find_rectype env ( !evdref) cj.uj_type with Not_found -> let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env ( !isevars) cj + error_case_not_inductive_loc cloc env ( !evdref) cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 1 then @@ -402,16 +402,16 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (match po with | Some p -> let env_p = push_rels psign env in - let pj = pretype_type empty_valcon env_p isevars lvar p in - let ccl = nf_evar ( !isevars) pj.utj_val in + let pj = pretype_type empty_valcon env_p evdref lvar p in + let ccl = nf_evar ( !evdref) pj.utj_val in let psign = make_arity_signature env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.to_list cs.cs_concl_realargs) @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env ( !isevars) lp inst in - let fj = pretype (mk_tycon fty) env_f isevars lvar d in + let fty = hnf_lam_applist env ( !evdref) lp inst in + let fj = pretype (mk_tycon fty) env_f evdref lvar d in let f = it_mkLambda_or_LetIn fj.uj_val fsign in let v = let mis,_ = dest_ind_family indf in @@ -421,14 +421,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | None -> let tycon = lift_tycon cs.cs_nargs tycon in - let fj = pretype tycon env_f isevars lvar d in + let fj = pretype tycon env_f evdref lvar d in let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let ccl = nf_evar ( !isevars) fj.uj_type in + let ccl = nf_evar ( !evdref) fj.uj_type in let ccl = if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env ( !isevars) + error_cant_find_case_type_loc loc env ( !evdref) cj.uj_val in let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = @@ -439,16 +439,16 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct { uj_val = v; uj_type = ccl }) | RIf (loc,c,(na,po),b1,b2) -> - let cj = pretype empty_tycon env isevars lvar c in + let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env ( !isevars) cj.uj_type + try find_rectype env ( !evdref) cj.uj_type with Not_found -> let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env ( !isevars) cj in + error_case_not_inductive_loc cloc env ( !evdref) cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 2 then user_err_loc (loc,"", - str "If is only for inductive types with two constructors"); + str "If is only for inductive types with two constructors."); let arsgn = let arsgn,_ = get_arity env indf in @@ -462,11 +462,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let pred,p = match po with | Some p -> let env_p = push_rels psign env in - let pj = pretype_type empty_valcon env_p isevars lvar p in - let ccl = nf_evar ( !isevars) pj.utj_val in + let pj = pretype_type empty_valcon env_p evdref lvar p in + let ccl = nf_evar ( !evdref) pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in - let jtyp = inh_conv_coerce_to_tycon loc env isevars {uj_val = pred; + let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred; uj_type = typ} tycon in jtyp.uj_val, jtyp.uj_type @@ -474,11 +474,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let p = match tycon with | Some (None, ty) -> ty | None | Some _ -> - e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) + e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in - let pred = nf_evar ( !isevars) pred in - let p = nf_evar ( !isevars) p in + let pred = nf_evar ( !evdref) pred in + let p = nf_evar ( !evdref) p in (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*) let f cs b = let n = rel_context_length cs.cs_args in @@ -497,7 +497,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct in let env_c = push_rels csgn env in (* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *) - let bj = pretype (mk_tycon pi) env_c isevars lvar b in + let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs.cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in @@ -510,81 +510,80 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty - ((fun vtyc env isevars -> pretype vtyc env isevars lvar),isevars) + ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) - | RCast(loc,c,k) -> + | RCast (loc,c,k) -> let cj = match k with CastCoerce -> - let cj = pretype empty_tycon env isevars lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj + let cj = pretype empty_tycon env evdref lvar c in + evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj | CastConv (k,t) -> - let tj = pretype_type empty_valcon env isevars lvar t in - let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in + let tj = pretype_type empty_valcon env evdref lvar t in + let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in (* User Casts are for helping pretyping, experimentally not to be kept*) (* ... except for Correctness *) let v = mkCast (cj.uj_val, k, tj.utj_val) in { uj_val = v; uj_type = tj.utj_val } in - inh_conv_coerce_to_tycon loc env isevars cj tycon + inh_conv_coerce_to_tycon loc env evdref cj tycon | RDynamic (loc,d) -> if (tag d) = "constr" then let c = constr_out d in - let j = (Retyping.get_judgment_of env ( !isevars) c) in + let j = (Retyping.get_judgment_of env ( !evdref) c) in j - (*inh_conv_coerce_to_tycon loc env isevars j tycon*) + (*inh_conv_coerce_to_tycon loc env evdref j tycon*) else - user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic")) + user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic.")) - (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *) - and pretype_type valcon env isevars lvar = function + (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) + and pretype_type valcon env evdref lvar = function | RHole loc -> (match valcon with | Some v -> let s = - let sigma = !isevars in + let sigma = !evdref in let t = Retyping.get_type_of env sigma v in match kind_of_term (whd_betadeltaiota env sigma t) with | Sort s -> s - | Evar v when is_Type (existential_type sigma v) -> - evd_comb1 (define_evar_as_sort) isevars v + | Evar ev when is_Type (existential_type sigma ev) -> + evd_comb1 (define_evar_as_sort) evdref ev | _ -> anomaly "Found a type constraint which is not a type" in { utj_val = v; utj_type = s } | None -> let s = new_Type_sort () in - { utj_val = e_new_evar isevars env ~src:loc (mkSort s); + { utj_val = e_new_evar evdref env ~src:loc (mkSort s); utj_type = s}) | c -> - let j = pretype empty_tycon env isevars lvar c in + let j = pretype empty_tycon env evdref lvar c in let loc = loc_of_rawconstr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) isevars j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with | None -> tj | Some v -> - if e_cumul env isevars v tj.utj_val then tj + if e_cumul env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_rawconstr c) env ( !isevars) tj.utj_val v + (loc_of_rawconstr c) env ( !evdref) tj.utj_val v - let pretype_gen_aux isevars env lvar kind c = + let pretype_gen fail_evar resolve_classes evdref env lvar kind c = let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env isevars lvar c).uj_val + (pretype tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env isevars lvar c).utj_val in - let evd,_ = consider_remaining_unif_problems env !isevars in - isevars:=evd; - nf_evar ( !isevars) c' - - let pretype_gen isevars env lvar kind c = - let c = pretype_gen_aux isevars env lvar kind c in - isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !isevars; - nf_evar ( !isevars) c + (pretype_type empty_valcon env evdref lvar c).utj_val in + evdref := fst (consider_remaining_unif_problems env !evdref); + if resolve_classes then + evdref := + Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref; + let c = nf_evar !evdref c' in + if fail_evar then check_evars env Evd.empty !evdref c; + c (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage @@ -592,57 +591,45 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct *) let understand_judgment sigma env c = - let isevars = ref (create_evar_defs sigma) in - let j = pretype empty_tycon env isevars ([],[]) c in - let j = j_nf_evar ( !isevars) j in - let isevars,_ = consider_remaining_unif_problems env !isevars in - check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); - j - - let understand_judgment_tcc isevars env c = - let j = pretype empty_tycon env isevars ([],[]) c in - let sigma = !isevars in - let j = j_nf_evar sigma j in - j + let evdref = ref (create_evar_defs sigma) in + let j = pretype empty_tycon env evdref ([],[]) c in + let evd,_ = consider_remaining_unif_problems env !evdref in + let j = j_nf_evar evd j in + check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); + j + + let understand_judgment_tcc evdref env c = + let j = pretype empty_tycon env evdref ([],[]) c in + j_nf_evar !evdref j (* Raw calls to the unsafe inference machine: boolean says if we must fail on unresolved evars; the unsafe_judgment list allows us to extend env with some bindings *) - let ise_pretype_gen fail_evar sigma env lvar kind c = - let isevars = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen isevars env lvar kind c in - let evd = !isevars in - if fail_evar then check_evars env Evd.empty evd c; - evd, c - + let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c = + let evdref = ref (Evd.create_evar_defs sigma) in + let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in + !evdref, c + (** Entry points of the high-level type synthesis algorithm *) let understand_gen kind sigma env c = - snd (ise_pretype_gen true sigma env ([],[]) kind c) + snd (ise_pretype_gen true true sigma env ([],[]) kind c) let understand sigma env ?expected_type:exptyp c = - snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c) + snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c) let understand_type sigma env c = - snd (ise_pretype_gen false sigma env ([],[]) IsType c) + snd (ise_pretype_gen false true sigma env ([],[]) IsType c) let understand_ltac sigma env lvar kind c = - ise_pretype_gen false sigma env lvar kind c - - let understand_tcc_evars evdref env kind c = - pretype_gen evdref env ([],[]) kind c + ise_pretype_gen false true sigma env lvar kind c let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = - let ev, t = - if resolve_classes then - ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c - else - let isevars = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen_aux isevars env ([],[]) (OfType exptyp) c in - !isevars, c - in - ev, t + ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c + + let understand_tcc_evars evdref env kind c = + pretype_gen false true evdref env ([],[]) kind c end module Default : S = SubtacPretyping_F(Coercion.Default) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 562e6ec93..8c06f9bfe 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -157,7 +157,7 @@ sig rawconstr -> unsafe_type_judgment val pretype_gen : - evar_defs ref -> env -> + bool -> bool -> evar_defs ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr @@ -487,7 +487,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | Some p -> let env_p = push_rels psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_isevar !evdref pj.utj_val in + let ccl = nf_evar !evdref pj.utj_val in let psign = make_arity_signature env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = @@ -507,7 +507,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let tycon = lift_tycon cs.cs_nargs tycon in let fj = pretype tycon env_f evdref lvar d in let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let ccl = nf_isevar !evdref fj.uj_type in + let ccl = nf_evar !evdref fj.uj_type in let ccl = if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl @@ -605,7 +605,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | CastConv (k,t) -> let tj = pretype_type empty_valcon env evdref lvar t in let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_isevar !evdref cj.uj_type and tval = nf_isevar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in let cj = match k with | VMcast when not (occur_existential cty || occur_existential tval) -> ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj @@ -656,22 +656,22 @@ module Pretyping_F (Coercion : Coercion.S) = struct error_unexpected_type_loc (loc_of_rawconstr c) env ( !evdref) tj.utj_val v - let pretype_gen_aux evdref env lvar kind c = + let pretype_gen fail_evar resolve_classes evdref env lvar kind c = let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env evdref lvar c).uj_val + (pretype tycon env evdref lvar c).uj_val | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in - let evd,_ = consider_remaining_unif_problems env !evdref in - evdref := evd; - nf_isevar !evdref c' - - let pretype_gen evdref env lvar kind c = - let c = pretype_gen_aux evdref env lvar kind c in - evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref; - nf_isevar !evdref c - + evdref := fst (consider_remaining_unif_problems env !evdref); + if resolve_classes then + evdref := + Typeclasses.resolve_typeclasses ~onlyargs:(not fail_evar) + ~fail:fail_evar env !evdref; + let c = nf_evar !evdref c' in + if fail_evar then check_evars env Evd.empty !evdref c; + c + (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage retourne aussi le nouveau sigma... @@ -681,59 +681,43 @@ module Pretyping_F (Coercion : Coercion.S) = struct let evdref = ref (create_evar_defs sigma) in let j = pretype empty_tycon env evdref ([],[]) c in let evd,_ = consider_remaining_unif_problems env !evdref in - let j = j_nf_evar ( evd) j in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in - let j = j_nf_evar ( evd) j in + let j = j_nf_evar evd j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc evdref env c = let j = pretype empty_tycon env evdref ([],[]) c in - let sigma = !evdref in - let j = j_nf_evar sigma j in - j + j_nf_evar !evdref j (* Raw calls to the unsafe inference machine: boolean says if we must fail on unresolved evars; the unsafe_judgment list allows us to extend env with some bindings *) - let ise_pretype_gen fail_evar sigma env lvar kind c = + let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen_aux evdref env lvar kind c in - if fail_evar then - let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env !evdref in - let c = Evarutil.nf_isevar evd c in - check_evars env Evd.empty evd c; - evd, c - else !evdref, c + let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in + !evdref, c (** Entry points of the high-level type synthesis algorithm *) let understand_gen kind sigma env c = - snd (ise_pretype_gen true sigma env ([],[]) kind c) + snd (ise_pretype_gen true true sigma env ([],[]) kind c) let understand sigma env ?expected_type:exptyp c = - snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c) + snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c) let understand_type sigma env c = - snd (ise_pretype_gen true sigma env ([],[]) IsType c) + snd (ise_pretype_gen true true sigma env ([],[]) IsType c) let understand_ltac sigma env lvar kind c = - ise_pretype_gen false sigma env lvar kind c - - let understand_tcc_evars evdref env kind c = - pretype_gen evdref env ([],[]) kind c - + ise_pretype_gen false false sigma env lvar kind c + let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = - let evd, t = - let evdref = ref (Evd.create_evar_defs sigma) in - let c = - if resolve_classes then - pretype_gen evdref env ([],[]) (OfType exptyp) c - else - pretype_gen_aux evdref env ([],[]) (OfType exptyp) c - in !evdref, c - in evd, t + ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c + + let understand_tcc_evars evdref env kind c = + pretype_gen false true evdref env ([],[]) kind c end - + module Default : S = Pretyping_F(Coercion.Default) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index e7a8374b5..974cba1b4 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -97,7 +97,7 @@ sig rawconstr -> unsafe_type_judgment val pretype_gen : - evar_defs ref -> env -> + bool -> bool -> evar_defs ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr |