From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- pretyping/pretyping.ml | 300 ++++++++++++++++++++++++++----------------------- 1 file changed, 159 insertions(+), 141 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a3b1dd18..901936f3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,13 +1,27 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* if loc = dummy_loc then raise e else Stdpp.raise_with_loc loc e); + | e -> if loc = dummy_loc then raise e else Loc.raise loc e); indexes else (* we now search recursively amoungst all combinations *) @@ -72,20 +87,53 @@ let search_guard loc env possible_indexes fixdefs = user_err_loc (loc,"search_guard", Pp.str errmsg) with Found indexes -> indexes) -(* To embed constr in rawconstr *) +(* To embed constr in glob_constr *) let ((constr_in : constr -> Dyn.t), (constr_out : Dyn.t -> constr)) = Dyn.create "constr" (** Miscellaneous interpretation functions *) let interp_sort = function - | RProp c -> Prop c - | RType _ -> new_Type_sort () + | GProp c -> Prop c + | GType _ -> new_Type_sort () let interp_elimination_sort = function - | RProp Null -> InProp - | RProp Pos -> InSet - | RType _ -> InType + | GProp Null -> InProp + | GProp Pos -> InSet + | GType _ -> InType + +let resolve_evars env evdref fail_evar resolve_classes = + if resolve_classes then + evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false + ~split:true ~fail:fail_evar env !evdref); + (* Resolve eagerly, potentially making wrong choices *) + evdref := (try consider_remaining_unif_problems + ~ts:(Typeclasses.classes_transparent_state ()) env !evdref + with e -> if fail_evar then raise e else !evdref) + +let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) = + let evdref = ref evd in + resolve_evars env evdref fail_evar use_classes; + let rec proc_rec c = + let c = Reductionops.whd_evar !evdref c in + match kind_of_term c with + | Evar (evk,args as ev) when not (Evd.mem initial_sigma evk) -> + let sigma = !evdref in + (try + let c = hook env sigma ev in + evdref := Evd.define evk c !evdref; + c + with Exit -> + if fail_evar then + let evi = Evd.find_undefined sigma evk in + let (loc,src) = evar_source evk !evdref in + Pretype_errors.error_unsolvable_implicit loc env sigma evi src None + else + c) + | _ -> map_constr proc_rec c in + let c = proc_rec c in + (* Side-effect *) + !evdref,c module type S = sig @@ -95,20 +143,20 @@ sig (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) val allow_anonymous_refs : bool ref - (* Generic call to the interpreter from rawconstr to open_constr, leaving + (* Generic call to the interpreter from glob_constr to open_constr, leaving unresolved holes as evars and returning the typing contexts of these evars. Work as [understand_gen] for the rest. *) val understand_tcc : ?resolve_classes:bool -> - evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr + evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_map ref -> env -> typing_constraint -> rawconstr -> constr + evar_map ref -> env -> typing_constraint -> glob_constr -> constr (* More general entry point with evars from ltac *) - (* Generic call to the interpreter from rawconstr to constr, failing - unresolved holes in the rawterm cannot be instantiated. + (* Generic call to the interpreter from glob_constr to constr, failing + unresolved holes in the glob_constr cannot be instantiated. In [understand_ltac expand_evars sigma env ltac_env constraint c], @@ -120,29 +168,29 @@ sig val understand_ltac : bool -> evar_map -> env -> ltac_var_map -> - typing_constraint -> rawconstr -> evar_map * constr + typing_constraint -> glob_constr -> pure_open_constr - (* Standard call to get a constr from a rawconstr, resolving implicit args *) + (* Standard call to get a constr from a glob_constr, resolving implicit args *) val understand : evar_map -> env -> ?expected_type:Term.types -> - rawconstr -> constr + glob_constr -> constr - (* Idem but the rawconstr is intended to be a type *) + (* Idem but the glob_constr is intended to be a type *) - val understand_type : evar_map -> env -> rawconstr -> constr + val understand_type : evar_map -> env -> glob_constr -> constr (* A generalization of the two previous case *) val understand_gen : typing_constraint -> evar_map -> env -> - rawconstr -> constr + glob_constr -> constr (* Idem but returns the judgment of the understood term *) - val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment + val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment (* Idem but do not fail on unresolved evars *) - val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment + val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment (*i*) (* Internal of Pretyping... @@ -150,15 +198,15 @@ sig *) val pretype : type_constraint -> env -> evar_map ref -> - ltac_var_map -> rawconstr -> unsafe_judgment + ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : val_constraint -> env -> evar_map ref -> - ltac_var_map -> rawconstr -> unsafe_type_judgment + ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : bool -> bool -> bool -> evar_map ref -> env -> - ltac_var_map -> typing_constraint -> rawconstr -> constr + ltac_var_map -> typing_constraint -> glob_constr -> constr (*i*) end @@ -207,13 +255,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct i lna vdefj lar done - let check_branches_message loc env evdref c (explft,lft) = - for i = 0 to Array.length explft - 1 do - 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 evdref j = function | None -> j @@ -241,45 +282,33 @@ module Pretyping_F (Coercion : Coercion.S) = struct errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") let pretype_id loc env sigma (lvar,unbndltacvars) id = + (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> + (* Check if [id] is an ltac variable *) try let (ids,c) = List.assoc id lvar in let subst = List.map (invert_ltac_bound_name env id) ids in let c = substl subst c in { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> + (* Check if [id] is a section or goal variable *) try let (_,_,typ) = lookup_named id env in { uj_val = mkVar id; uj_type = typ } with Not_found -> - try (* To build a nicer ltac error message *) + (* [id] not found, build nice error message if [id] yet known from ltac *) + try match List.assoc id unbndltacvars with | None -> user_err_loc (loc,"", str "Variable " ++ pr_id id ++ str " should be bound to a term.") | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> + (* [id] not found, standard error message *) error_var_not_found_loc loc id - (* make a dependent predicate from an undependent one *) - - let make_dep_of_undep env (IndType (indf,realargs)) pj = - let n = List.length realargs in - let rec decomp n p = - if n=0 then p else - match kind_of_term p with - | Lambda (_,_,c) -> decomp (n-1) c - | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) - in - let sign,s = decompose_prod_n n pj.uj_type in - let ind = build_dependent_inductive env indf in - let s' = mkProd (Anonymous, ind, s) in - let ccl = lift 1 (decomp n pj.uj_val) in - let ccl' = mkLambda (Anonymous, ind, ccl) in - {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign} - let evar_kind_of_term sigma c = kind_of_term (whd_evar sigma c) @@ -290,27 +319,30 @@ module Pretyping_F (Coercion : Coercion.S) = struct let c = constr_of_global ref in make_judge c (Retyping.get_type_of env Evd.empty c) - let pretype_sort = function - | RProp c -> judge_of_prop_contents c - | RType _ -> judge_of_new_Type () + let pretype_sort evdref = function + | GProp c -> judge_of_prop_contents c + | GType _ -> evd_comb0 judge_of_new_Type evdref exception Found of fixpoint + let new_type_evar evdref env loc = + evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,InternalHole)) evdref + (* [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 evdref lvar = function - | RRef (loc,ref) -> + | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref (pretype_ref evdref env ref) tycon - | RVar (loc, id) -> + | GVar (loc, id) -> inh_conv_coerce_to_tycon loc env evdref (pretype_id loc env !evdref lvar id) tycon - | REvar (loc, evk, instopt) -> + | GEvar (loc, evk, 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_filtered_context (Evd.find !evdref evk) in @@ -321,24 +353,23 @@ module Pretyping_F (Coercion : Coercion.S) = struct let j = (Retyping.get_judgment_of env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon - | RPatVar (loc,(someta,n)) -> + | GPatVar (loc,(someta,n)) -> let ty = match tycon with | Some (None, ty) -> ty - | None | Some _ -> - e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in + | None | Some _ -> new_type_evar evdref env loc in let k = MatchingVar (someta,n) in { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } - | RHole (loc,k) -> + | GHole (loc,k) -> let ty = match tycon with | Some (None, ty) -> ty | None | Some _ -> - e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in + new_type_evar evdref env loc in { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } - | RRec (loc,fixkind,names,bl,lar,vdef) -> + | GRec (loc,fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt | (na,bk,None,ty)::bl -> @@ -379,7 +410,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct 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) -> + | GFix (vn,i) -> (* First, let's find the guard indexes. *) (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, @@ -395,22 +426,23 @@ module Pretyping_F (Coercion : Coercion.S) = struct let fixdecls = (names,ftys,fdefs) in let indexes = search_guard loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) - | RCoFix i -> + | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); + (try check_cofix env cofix with e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon - | RSort (loc,s) -> - inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon + | GSort (loc,s) -> + let j = pretype_sort evdref s in + inh_conv_coerce_to_tycon loc env evdref j tycon - | RApp (loc,f,args) -> + | GApp (loc,f,args) -> let fj = pretype empty_tycon env evdref lvar f in - let floc = loc_of_rawconstr f in + let floc = loc_of_glob_constr f in let rec apply_rec env n resj = function | [] -> resj | c::rest -> - let argloc = loc_of_rawconstr c in + let argloc = loc_of_glob_constr c 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 @@ -444,7 +476,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | _ -> resj in inh_conv_coerce_to_tycon loc env evdref resj tycon - | RLambda(loc,name,bk,c1,c2) -> + | GLambda(loc,name,bk,c1,c2) -> 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 evdref lvar c1 in @@ -452,7 +484,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let j' = pretype rng (push_rel var env) evdref lvar c2 in judge_of_abstraction env (orelse_name name name') j j' - | RProd(loc,name,bk,c1,c2) -> + | GProd(loc,name,bk,c1,c2) -> let j = pretype_type empty_valcon env evdref lvar c1 in let j' = if name = Anonymous then @@ -465,13 +497,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct in let resj = try judge_of_product env name j j' - with TypeError _ as e -> Stdpp.raise_with_loc loc e in + with TypeError _ as e -> Loc.raise loc e in inh_conv_coerce_to_tycon loc env evdref resj tycon - | RLetIn(loc,name,c1,c2) -> + | GLetIn(loc,name,c1,c2) -> let j = match c1 with - | RCast (loc, c, CastConv (DEFAULTcast, t)) -> + | GCast (loc, c, CastConv (DEFAULTcast, t)) -> let tj = pretype_type empty_valcon env evdref lvar t in pretype (mk_tycon tj.utj_val) env evdref lvar c | _ -> pretype empty_tycon env evdref lvar c1 @@ -483,12 +515,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct { 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) -> + | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env !evdref cj.uj_type with Not_found -> - let cloc = loc_of_rawconstr c in + let cloc = loc_of_glob_constr c in error_case_not_inductive_loc cloc env !evdref cj in let cstrs = get_constructors env indf in @@ -524,10 +556,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct 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 - let ci = make_case_info env mis LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) in - { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } + let ind,_ = dest_ind_family indf in + let ci = make_case_info env ind LetStyle in + Typing.check_allowed_sort env !evdref ind cj.uj_val p; + mkCase (ci, p, cj.uj_val,[|f|]) in + { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } | None -> let tycon = lift_tycon cs.cs_nargs tycon in @@ -543,18 +576,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ccl = refresh_universes ccl in let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = - let mis,_ = dest_ind_family indf in - let ci = make_case_info env mis LetStyle in - mkCase (ci, p, cj.uj_val,[|f|] ) - in - { uj_val = v; uj_type = ccl }) + let ind,_ = dest_ind_family indf in + let ci = make_case_info env ind LetStyle in + Typing.check_allowed_sort env !evdref ind cj.uj_val p; + mkCase (ci, p, cj.uj_val,[|f|]) + in { uj_val = v; uj_type = ccl }) - | RIf (loc,c,(na,po),b1,b2) -> + | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env !evdref cj.uj_type with Not_found -> - let cloc = loc_of_rawconstr c in + let cloc = loc_of_glob_constr c in error_case_not_inductive_loc cloc env !evdref cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 2 then @@ -577,15 +610,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct 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 evdref {uj_val = pred; - uj_type = typ} tycon - in - jtyp.uj_val, jtyp.uj_type + pred, typ | None -> let p = match tycon with | Some (None, ty) -> ty - | None | Some _ -> - e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) + | None | Some _ -> new_type_evar evdref env loc in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in @@ -611,18 +640,20 @@ module Pretyping_F (Coercion : Coercion.S) = struct let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = - let mis,_ = dest_ind_family indf in - let ci = make_case_info env mis IfStyle in - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) + let ind,_ = dest_ind_family indf in + let ci = make_case_info env ind IfStyle in + let pred = nf_evar !evdref pred in + Typing.check_allowed_sort env !evdref ind cj.uj_val pred; + mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in { uj_val = v; uj_type = p } - | RCases (loc,sty,po,tml,eqns) -> + | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) - | RCast (loc,c,k) -> + | GCast (loc,c,k) -> let cj = match k with CastCoerce -> @@ -633,29 +664,24 @@ module Pretyping_F (Coercion : Coercion.S) = struct let cj = pretype empty_tycon env evdref lvar c 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) -> - (try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj - with Reduction.NotConvertible -> - error_actual_type_loc loc env !evdref cj tval) - + | VMcast -> + if not (occur_existential cty || occur_existential tval) then + begin + try + ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj + with Reduction.NotConvertible -> + error_actual_type_loc loc env !evdref cj tval + end + else user_err_loc (loc,"",str "Cannot check cast with vm: unresolved arguments remain.") | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval) in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon - | RDynamic (loc,d) -> - if (Dyn.tag d) = "constr" then - let c = constr_out d in - let j = (Retyping.get_judgment_of env !evdref c) in - j - (*inh_conv_coerce_to_tycon loc env evdref j tycon*) - else - user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic.")) - (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type valcon env evdref lvar = function - | RHole loc -> + | GHole loc -> (match valcon with | Some v -> let s = @@ -670,12 +696,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct { utj_val = v; utj_type = s } | None -> - let s = new_Type_sort () in + let s = evd_comb0 new_sort_variable evdref in { utj_val = e_new_evar evdref env ~src:loc (mkSort s); utj_type = s}) | c -> let j = pretype empty_tycon env evdref lvar c in - let loc = loc_of_rawconstr c in + let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with | None -> tj @@ -683,7 +709,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct if e_cumul env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_rawconstr c) env !evdref tj.utj_val v + (loc_of_glob_constr c) env !evdref tj.utj_val v let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c = let c' = match kind with @@ -691,18 +717,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in (pretype tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val in - if resolve_classes then ( - evdref := Typeclasses.resolve_typeclasses ~onlyargs:false - ~split:true ~fail:fail_evar env !evdref); - evdref := (try consider_remaining_unif_problems env !evdref - with e when not resolve_classes -> - consider_remaining_unif_problems env - (Typeclasses.resolve_typeclasses ~onlyargs:false - ~split:true ~fail:fail_evar env !evdref)); - let c = if expand_evar then nf_evar !evdref c' else c' in - if fail_evar then check_evars env Evd.empty !evdref c; - c + (pretype_type empty_valcon env evdref lvar c).utj_val + in + resolve_evars env evdref fail_evar resolve_classes; + let c = if expand_evar then nf_evar !evdref c' else 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 @@ -710,26 +730,24 @@ module Pretyping_F (Coercion : Coercion.S) = struct *) let understand_judgment sigma env c = - let evdref = ref (create_evar_defs sigma) in + let evdref = ref sigma in let j = pretype empty_tycon env evdref ([],[]) c in - let evd = consider_remaining_unif_problems env !evdref in - let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:false - ~fail:true env evd - in - let j = j_nf_evar evd j in - check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); - j + resolve_evars env evdref true true; + let j = j_nf_evar !evdref j in + check_evars env sigma !evdref (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 + resolve_evars env evdref false true; + 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 expand_evar fail_evar resolve_classes sigma env lvar kind c = - let evdref = ref (Evd.create_evar_defs sigma) in + let evdref = ref sigma in let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in !evdref, c -- cgit v1.2.3