diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 814 |
1 files changed, 430 insertions, 384 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c66221e5f..7777de514 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -93,10 +93,10 @@ let ((constr_in : constr -> Dyn.t), (** Miscellaneous interpretation functions *) -let interp_sort = function - | GProp -> Prop Null - | GSet -> Prop Pos - | GType _ -> new_Type_sort () +let interp_sort evd = function + | GProp -> evd, Prop Null + | GSet -> evd, Prop Pos + | GType _ -> new_sort_variable univ_rigid evd let interp_elimination_sort = function | GProp -> InProp @@ -157,7 +157,7 @@ let check_extra_evars_are_solved env initial_sigma sigma = let check_evars_are_solved env initial_sigma sigma = check_typeclasses_instances_are_solved env sigma; - check_problems_are_solved sigma; + check_problems_are_solved env sigma; check_extra_evars_are_solved env initial_sigma sigma (* Try typeclasses, hooks, unification heuristics ... *) @@ -179,21 +179,6 @@ let process_inference_flags flags env initial_sigma (sigma,c) = (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false -let evd_comb0 f evdref = - let (evd',x) = f !evdref in - evdref := evd'; - x - -let evd_comb1 f evdref x = - let (evd',y) = f !evdref x in - evdref := evd'; - y - -let evd_comb2 f evdref x y = - let (evd',z) = f !evdref x y in - evdref := evd'; - z - (* 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 *) @@ -236,7 +221,8 @@ let protected_get_type_of env sigma c = (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") -let pretype_id loc env sigma (lvar,unbndltacvars) id = +let pretype_id loc env evdref (lvar,unbndltacvars) id = + let sigma = !evdref in (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in @@ -257,6 +243,12 @@ let pretype_id loc env sigma (lvar,unbndltacvars) id = (* Check if [id] is a section or goal variable *) try let (_,_,typ) = lookup_named id env in + (* let _ = *) + (* try *) + (* let ctx = Decls.variable_context id in *) + (* evdref := Evd.merge_context_set univ_rigid !evdref ctx; *) + (* with Not_found -> () *) + (* in *) { uj_val = mkVar id; uj_type = typ } with Not_found -> (* [id] not found, standard error message *) @@ -268,18 +260,26 @@ let evar_kind_of_term sigma c = (*************************************************************************) (* Main pretyping function *) -let pretype_ref loc evdref env = function +(* Check with universe list? *) +let pretype_global rigid env evd gr us = Evd.fresh_global ~rigid env evd gr + +let pretype_ref loc evdref env ref us = + match ref with | VarRef id -> (* Section variable *) - (try let (_,_,ty) = lookup_named id env in make_judge (mkVar id) ty + (try let (_,_,ty) = lookup_named id env in + (* let ctx = Decls.variable_context id in *) + (* evdref := Evd.merge_context_set univ_rigid !evdref ctx; *) + make_judge (mkVar id) ty with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal variables *) Pretype_errors.error_var_not_found_loc loc id) | ref -> - let c = constr_of_global ref in - make_judge c (Retyping.get_type_of env Evd.empty c) + let evd, c = pretype_global univ_flexible env !evdref ref us in + evdref := evd; + make_judge c (Retyping.get_type_of env evd c) let pretype_sort evdref = function | GProp -> judge_of_prop @@ -287,27 +287,37 @@ let pretype_sort evdref = function | GType _ -> evd_comb0 judge_of_new_Type evdref let new_type_evar evdref env loc = - evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,Evar_kinds.InternalHole)) evdref + let e, s = + evd_comb0 (fun evd -> Evarutil.new_type_evar univ_flexible_alg evd env ~src:(loc,Evar_kinds.InternalHole)) evdref + in e + +let get_projection env cst = + let cb = lookup_constant cst env in + match cb.Declarations.const_proj with + | Some {Declarations.proj_ind = mind; proj_npars = n; proj_arg = m; proj_type = ty} -> + (cst,mind,n,m,ty) + | None -> raise Not_found let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* [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 resolve_tc (tycon : type_constraint) env evdref lvar t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type resolve_tc in let pretype = pretype resolve_tc in match t with - | GRef (loc,ref) -> + | GRef (loc,ref,u) -> inh_conv_coerce_to_tycon loc env evdref - (pretype_ref loc evdref env ref) + (pretype_ref loc evdref env ref u) tycon | GVar (loc, id) -> - inh_conv_coerce_to_tycon loc env evdref - (pretype_id loc env !evdref lvar id) - tycon + inh_conv_coerce_to_tycon loc env evdref + (pretype_id loc env evdref lvar id) + tycon | GEvar (loc, evk, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un @@ -321,12 +331,12 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> - let ty = - match tycon with - | Some ty -> ty - | None -> new_type_evar evdref env loc in - let k = Evar_kinds.MatchingVar (someta,n) in - { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } + let ty = + match tycon with + | Some ty -> ty + | None -> new_type_evar evdref env loc in + let k = Evar_kinds.MatchingVar (someta,n) in + { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } | GHole (loc, k, None) -> let ty = @@ -348,178 +358,216 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = { uj_val = c; uj_type = ty } | GRec (loc,fixkind,names,bl,lar,vdef) -> - let rec type_bl env ctxt = function - [] -> ctxt - | (na,bk,None,ty)::bl -> - 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,bk,Some bd,ty)::bl -> - 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) 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 - let nbfix = Array.length lar in - let names = Array.map (fun id -> Name id) names in - let _ = - match tycon with - | Some t -> - let fixi = match fixkind with - | GFix (vn,i) -> i - | GCoFix i -> i - in e_conv env evdref ftys.(fixi) t - | None -> true - in - (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let newenv = push_rec_types (names,ftys,[||]) env in - let vdefj = - Array.map2_i - (fun i ctxt def -> + let rec type_bl env ctxt = function + [] -> ctxt + | (na,bk,None,ty)::bl -> + 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,bk,Some bd,ty)::bl -> + 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) 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 + let nbfix = Array.length lar in + let names = Array.map (fun id -> Name id) names in + let _ = + match tycon with + | Some t -> + let fixi = match fixkind with + | GFix (vn,i) -> i + | GCoFix i -> i + in e_conv env evdref ftys.(fixi) t + | None -> true + in + (* Note: bodies are not used by push_rec_types, so [||] is safe *) + let newenv = push_rec_types (names,ftys,[||]) env in + let vdefj = + Array.map2_i + (fun i ctxt def -> (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) - let (ctxt,ty) = - decompose_prod_n_assum (rel_context_length ctxt) - (lift nbfix ftys.(i)) in - let nenv = push_rel_context ctxt newenv 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 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 - | GFix (vn,i) -> + let (ctxt,ty) = + decompose_prod_n_assum (rel_context_length ctxt) + (lift nbfix ftys.(i)) in + let nenv = push_rel_context ctxt newenv 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 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 + | 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, but doing it properly involves delta-reduction, and it finally doesn't seem worth the effort (except for huge mutual fixpoints ?) *) - let possible_indexes = - Array.to_list (Array.mapi - (fun i (n,_) -> match n with - | Some n -> [n] - | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) - vn) - in - let fixdecls = (names,ftys,fdefs) in - let indexes = search_guard loc env possible_indexes fixdecls in - make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) - | GCoFix i -> - let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix - with reraise -> - let e = Errors.push reraise in Loc.raise loc e); - make_judge (mkCoFix cofix) ftys.(i) - in + let possible_indexes = + Array.to_list (Array.mapi + (fun i (n,_) -> match n with + | Some n -> [n] + | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) + vn) + in + let fixdecls = (names,ftys,fdefs) in + let indexes = search_guard loc env possible_indexes fixdecls in + make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) + | GCoFix i -> + let cofix = (i,(names,ftys,fdefs)) in + (try check_cofix env cofix + with reraise -> + let e = Errors.push reraise in Loc.raise loc e); + make_judge (mkCoFix cofix) ftys.(i) + in inh_conv_coerce_to_tycon loc env evdref fixj tycon | GSort (loc,s) -> - let j = pretype_sort evdref s in - inh_conv_coerce_to_tycon loc env evdref j tycon + let j = pretype_sort evdref s in + inh_conv_coerce_to_tycon loc env evdref j tycon + + | GProj (loc, p, arg) -> + let (cst, mind, n, m, ty) = + try get_projection env p + with Not_found -> + user_err_loc (loc,"",str "Not a projection") + in + let mk_ty k = + let ind = + Evarutil.evd_comb1 (Evd.fresh_inductive_instance env) evdref (mind,0) + in + let args = + let ctx = smash_rel_context (Inductiveops.inductive_params_ctxt ind) in + List.fold_right (fun (n, b, ty) (* par *)args -> + let ty = substl args ty in + let ev = e_new_evar evdref env ~src:(loc,k) ty in + ev :: args) ctx [] + (* let j = pretype (mk_tycon ty) env evdref lvar par in *) + (* j.uj_val :: args) ctx pars [] *) + in (ind, List.rev args) + in + let argtycon = + match arg with + (** FIXME ? *) + | GHole (loc, k, _) -> (* Typeclass projection application: + create the necessary type constraint *) + let ind, args = mk_ty k in + mk_tycon (applist (mkIndU ind, args)) + | _ -> empty_tycon + in + let recty = pretype argtycon env evdref lvar arg in + let recty, ((ind,u), pars) = + try + let IndType (indf, _ (*[]*)) = + find_rectype env !evdref recty.uj_type + in recty, dest_ind_family indf + with Not_found -> + (match argtycon with + | Some ty -> assert false + (* let IndType (indf, _) = find_rectype env !evdref ty in *) + (* recty, dest_ind_family indf *) + | None -> + let ind, args = mk_ty Evar_kinds.InternalHole in + let j' = + inh_conv_coerce_to_tycon loc env evdref recty + (mk_tycon (applist (mkIndU ind, args))) in + j', (ind, args)) + in + let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in + let ty = Vars.subst_univs_constr usubst ty in + let ty = substl (recty.uj_val :: List.rev pars) ty in + let j = {uj_val = mkProj (cst,recty.uj_val); uj_type = ty} in + inh_conv_coerce_to_tycon loc env evdref j tycon | GApp (loc,f,args) -> - let fj = pretype empty_tycon env evdref lvar f in - let floc = loc_of_glob_constr f in - let length = List.length args in - let candargs = + let fj = pretype empty_tycon env evdref lvar f in + let floc = loc_of_glob_constr f in + let length = List.length args in + let candargs = (* Bidirectional typechecking hint: parameters of a constructor are completely determined by a typing constraint *) - if Flags.is_program_mode () && length > 0 && isConstruct fj.uj_val then - match tycon with - | None -> [] - | Some ty -> - let (ind, i) = destConstruct fj.uj_val in - let npars = inductive_nparams ind in - if Int.equal npars 0 then [] - else - try - (* Does not treat partially applied constructors. *) - let ty = evd_comb1 (Coercion.inh_coerce_to_prod loc env) evdref ty in - let IndType (indf, args) = find_rectype env !evdref ty in - let (ind',pars) = dest_ind_family indf in - if eq_ind ind ind' then pars - else (* Let the usual code throw an error *) [] - with Not_found -> [] - else [] - in - let rec apply_rec env n resj candargs = function - | [] -> resj - | c::rest -> - let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in - let resty = whd_betadeltaiota env !evdref resj.uj_type in - match kind_of_term resty with - | Prod (na,c1,c2) -> - let hj = pretype (mk_tycon c1) env evdref lvar c in - let candargs, ujval = - match candargs with - | [] -> [], j_val hj - | arg :: args -> - if e_conv env evdref (j_val hj) arg then - args, nf_evar !evdref (j_val hj) - else [], j_val hj - in - let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in - apply_rec env (n+1) - { uj_val = value; - uj_type = typ } - candargs rest - - | _ -> - let hj = pretype empty_tycon env evdref lvar c in - error_cant_apply_not_functional_loc - (Loc.merge floc argloc) env !evdref - resj [hj] - in - let resj = apply_rec env 1 fj candargs args in - let resj = - match evar_kind_of_term !evdref resj.uj_val with - | App (f,args) -> - let f = whd_evar !evdref f in - begin match kind_of_term f with - | Ind _ | Const _ - when isInd f || has_polymorphic_type (destConst f) - -> - 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 (* use this for keeping evars: resj.uj_val *) t - | _ -> resj end - | _ -> resj in - inh_conv_coerce_to_tycon loc env evdref resj tycon + if Flags.is_program_mode () && length > 0 && isConstruct fj.uj_val then + match tycon with + | None -> [] + | Some ty -> + let ((ind, i), u) = destConstruct fj.uj_val in + let npars = inductive_nparams ind in + if Int.equal npars 0 then [] + else + try + let ty = evd_comb1 (Coercion.inh_coerce_to_prod loc env) evdref ty in + let IndType (indf, args) = find_rectype env !evdref ty in + let ((ind',u'),pars) = dest_ind_family indf in + if eq_ind ind ind' then pars + else (* Let the usual code throw an error *) [] + with Not_found -> [] + else [] + in + let rec apply_rec env n resj candargs = function + | [] -> resj + | c::rest -> + let argloc = loc_of_glob_constr c in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in + let resty = whd_betadeltaiota env !evdref resj.uj_type in + match kind_of_term resty with + | Prod (na,c1,c2) -> + let hj = pretype (mk_tycon c1) env evdref lvar c in + let candargs, ujval = + match candargs with + | [] -> [], j_val hj + | arg :: args -> + if e_conv env evdref (j_val hj) arg then + args, nf_evar !evdref (j_val hj) + else [], j_val hj + in + let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in + apply_rec env (n+1) + { uj_val = value; + uj_type = typ } + candargs rest + + | _ -> + let hj = pretype empty_tycon env evdref lvar c in + error_cant_apply_not_functional_loc + (Loc.merge floc argloc) env !evdref + resj [hj] + in + let resj = apply_rec env 1 fj candargs args in + inh_conv_coerce_to_tycon loc env evdref resj tycon | GLambda(loc,name,bk,c1,c2) -> - let tycon' = evd_comb1 - (fun evd tycon -> - match tycon with - | None -> evd, tycon - | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in - evd, Some ty') - evdref 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 evdref lvar c1 in - let var = (name,None,j.utj_val) in - let j' = pretype rng (push_rel var env) evdref lvar c2 in - let resj = judge_of_abstraction env (orelse_name name name') j j' in - inh_conv_coerce_to_tycon loc env evdref resj tycon + let tycon' = evd_comb1 + (fun evd tycon -> + match tycon with + | None -> evd, tycon + | Some ty -> + let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in + evd, Some ty') + evdref 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 evdref lvar c1 in + let var = (name,None,j.utj_val) in + let j' = pretype rng (push_rel var env) evdref lvar c2 in + let resj = judge_of_abstraction env (orelse_name name name') j j' in + inh_conv_coerce_to_tycon loc env evdref resj tycon | GProd(loc,name,bk,c1,c2) -> - let j = pretype_type empty_valcon env evdref lvar c1 in - let j' = match name with + let j = pretype_type empty_valcon env evdref lvar c1 in + let j' = match name with | Anonymous -> let j = pretype_type empty_valcon env evdref lvar c2 in { j with utj_val = lift 1 j.utj_val } @@ -527,212 +575,208 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = let var = (name,j.utj_val) in let env' = push_rel_assum var env in pretype_type empty_valcon env' evdref lvar c2 - in - let resj = - try judge_of_product env name j j' - with TypeError _ as e -> let e = Errors.push e in Loc.raise loc e in - inh_conv_coerce_to_tycon loc env evdref resj tycon + in + let resj = + try judge_of_product env name j j' + with TypeError _ as e -> let e = Errors.push e in Loc.raise loc e in + inh_conv_coerce_to_tycon loc env evdref resj tycon | GLetIn(loc,name,c1,c2) -> - let j = - match c1 with - | GCast (loc, c, CastConv 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 - 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) evdref lvar c2 in - { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; - uj_type = subst1 j.uj_val j'.uj_type } + let j = + match c1 with + | GCast (loc, c, CastConv 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 + in + let t = 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) evdref lvar c2 in + { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; + uj_type = subst1 j.uj_val j'.uj_type } | 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_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj - in - let cstrs = get_constructors env indf in - if not (Int.equal (Array.length cstrs) 1) then - user_err_loc (loc,"",str "Destructing let is only for inductive types" ++ - str " with one constructor."); - let cs = cstrs.(0) in - if not (Int.equal (List.length nal) cs.cs_nargs) then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ - int cs.cs_nargs ++ str " variables."); - let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args in - let env_f = push_rel_context fsign env in - (* Make dependencies from arity signature impossible *) - let arsgn = - let arsgn,_ = get_arity env indf in - if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn - else arsgn - in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in - let nar = List.length arsgn in - (match po with - | Some p -> - let env_p = push_rel_context psign env 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 !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 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 - 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 !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 !evdref - cj.uj_val in - let ccl = refresh_universes ccl in - let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in - let v = - 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 }) - - | 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_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj in - let cstrs = get_constructors env indf in - if not (Int.equal (Array.length cstrs) 2) then - user_err_loc (loc,"", - str "If is only for inductive types with two constructors."); - + 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_glob_constr c in + error_case_not_inductive_loc cloc env !evdref cj + in + let cstrs = get_constructors env indf in + if not (Int.equal (Array.length cstrs) 1) then + user_err_loc (loc,"",str "Destructing let is only for inductive types" ++ + str " with one constructor."); + let cs = cstrs.(0) in + if not (Int.equal (List.length nal) cs.cs_nargs) then + user_err_loc (loc,"", str "Destructing let on this type expects " ++ + int cs.cs_nargs ++ str " variables."); + let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) + (List.rev nal) cs.cs_args in + let env_f = push_rel_context fsign env in + (* Make dependencies from arity signature impossible *) let arsgn = let arsgn,_ = get_arity env indf in if not !allow_anonymous_refs then - (* Make dependencies from arity signature impossible *) List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn else arsgn in - let nar = List.length arsgn in let psign = (na,None,build_dependent_inductive env indf)::arsgn in - let pred,p = match po with + let nar = List.length arsgn in + (match po with | Some p -> - let env_p = push_rel_context psign env 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 - pred, typ + let env_p = push_rel_context psign env 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 !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 ind,_ = dest_ind_family indf in + let ci = make_case_info env (fst 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 p = match tycon with - | Some ty -> ty - | None -> 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 - let p = nf_evar !evdref p in - let f cs b = - let n = rel_context_length cs.cs_args in - let pi = lift n pred in (* liftn n 2 pred ? *) - let pi = beta_applist (pi, [build_dependent_constructor cs]) in - let csgn = - if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args - else - List.map - (fun (n, b, t) -> - match n with - Name _ -> (n, b, t) - | Anonymous -> (Name (Id.of_string "H"), b, t)) - cs.cs_args + 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_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 !evdref + cj.uj_val in + (* let ccl = refresh_universes ccl in *) + let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in + let v = + let ind,_ = dest_ind_family indf in + let ci = make_case_info env (fst 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 }) + + | 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_glob_constr c in + error_case_not_inductive_loc cloc env !evdref cj in + let cstrs = get_constructors env indf in + if not (Int.equal (Array.length cstrs) 2) then + user_err_loc (loc,"", + str "If is only for inductive types with two constructors."); + + let arsgn = + let arsgn,_ = get_arity env indf in + if not !allow_anonymous_refs then + (* Make dependencies from arity signature impossible *) + List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + else arsgn + in + let nar = List.length arsgn in + let psign = (na,None,build_dependent_inductive env indf)::arsgn in + let pred,p = match po with + | Some p -> + let env_p = push_rel_context psign env 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 + pred, typ + | None -> + let p = match tycon with + | Some ty -> ty + | None -> new_type_evar evdref env loc in - let env_c = push_rel_context csgn env 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 - let v = - 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|]) + it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in + let pred = nf_evar !evdref pred in + let p = nf_evar !evdref p in + let f cs b = + let n = rel_context_length cs.cs_args in + let pi = lift n pred in (* liftn n 2 pred ? *) + let pi = beta_applist (pi, [build_dependent_constructor cs]) in + let csgn = + if not !allow_anonymous_refs then + List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args + else + List.map + (fun (n, b, t) -> + match n with + Name _ -> (n, b, t) + | Anonymous -> (Name (Id.of_string "H"), b, t)) + cs.cs_args in - { uj_val = v; uj_type = p } + let env_c = push_rel_context csgn env 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 + let v = + let ind,_ = dest_ind_family indf in + let ci = make_case_info env (fst 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 } | 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) + Cases.compile_cases loc sty + ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) + tycon env (* loc *) (po,tml,eqns) | GCast (loc,c,k) -> - let cj = - match k with - | CastCoerce -> - let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj - | CastConv t | CastVM t | CastNative t -> - let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in - let tj = pretype_type empty_valcon env evdref lvar t in - let tval = nf_evar !evdref tj.utj_val in - let cj = match k with - | VMcast -> - 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 - 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 - (ConversionFailed (env,cty,tval)) - end - else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ - str "unresolved arguments remain.") - | NATIVEcast -> - 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 evars = Nativenorm.evars_of_evar_map !evdref in - begin - try - ignore - (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); - cj - with Reduction.NotConvertible -> - error_actual_type_loc loc env !evdref cj tval + let cj = + match k with + | CastCoerce -> + let cj = pretype empty_tycon env evdref lvar c in + evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj + | CastConv t | CastVM t | CastNative t -> + let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in + let tj = pretype_type empty_valcon env evdref lvar t in + let tval = nf_evar !evdref tj.utj_val in + let cj = match k with + | VMcast -> + 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 + 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 + (ConversionFailed (env,cty,tval)) + end + else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ + str "unresolved arguments remain.") + | NATIVEcast -> + 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 evars = Nativenorm.evars_of_evar_map !evdref in + begin + try + ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj + with Reduction.NotConvertible -> + error_actual_type_loc loc env !evdref cj tval (ConversionFailed (env,cty,tval)) - end - - | _ -> - pretype (mk_tycon tval) env evdref lvar c - 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 + end + | _ -> + pretype (mk_tycon tval) env evdref lvar c + 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 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type resolve_tc valcon env evdref lvar = function @@ -751,7 +795,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function { utj_val = v; utj_type = s } | None -> - let s = evd_comb0 new_sort_variable evdref in + let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar evdref env ~src:(loc, knd) (mkSort s); utj_type = s}) | c -> @@ -778,11 +822,6 @@ let ise_pretype_gen flags sigma env lvar kind c = in process_inference_flags flags env sigma (!evdref,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... -*) - let default_inference_flags fail = { use_typeclasses = true; use_unif_heuristics = true; @@ -810,8 +849,10 @@ let on_judgment f j = let understand_judgment sigma env c = let evdref = ref sigma in let j = pretype true empty_tycon env evdref empty_lvar c in - on_judgment (fun c -> - snd (process_inference_flags all_and_fail_flags env sigma (!evdref,c))) j + let j = on_judgment (fun c -> + let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in + evdref := evd; c) j + in j, Evd.evar_universe_context !evdref let understand_judgment_tcc evdref env c = let j = pretype true empty_tycon env evdref empty_lvar c in @@ -819,13 +860,18 @@ let understand_judgment_tcc evdref env c = let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in evdref := evd; c) j +let ise_pretype_gen_ctx flags sigma env lvar kind c = + let evd, c = ise_pretype_gen flags sigma env lvar kind c in + let evd, f = Evarutil.nf_evars_and_universes evd in + f c, Evd.get_universe_context_set evd + (** Entry points of the high-level type synthesis algorithm *) let understand ?(flags=all_and_fail_flags) ?(expected_type=WithoutTypeConstraint) sigma env c = - snd (ise_pretype_gen flags sigma env empty_lvar expected_type c) + ise_pretype_gen_ctx flags sigma env empty_lvar expected_type c let understand_tcc ?(flags=all_no_fail_flags) sigma env ?(expected_type=WithoutTypeConstraint) c = ise_pretype_gen flags sigma env empty_lvar expected_type c |