diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | pretyping/coercionops.ml (renamed from pretyping/classops.ml) | 28 | ||||
| -rw-r--r-- | pretyping/coercionops.mli (renamed from pretyping/classops.mli) | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 383 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 43 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 11 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 1 |
8 files changed, 340 insertions, 132 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f0e73bdb29..c980d204ca 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -27,7 +27,7 @@ open EConstr open Vars open Reductionops open Pretype_errors -open Classops +open Coercionops open Evarutil open Evarconv open Evd diff --git a/pretyping/classops.ml b/pretyping/coercionops.ml index c12a236d8e..16021b66f8 100644 --- a/pretyping/classops.ml +++ b/pretyping/coercionops.ml @@ -297,15 +297,15 @@ let lookup_pattern_path_between env (s,t) = (* rajouter une coercion dans le graphe *) -let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = +let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref = ref (fun _ -> str "<a class path>") let install_path_printer f = path_printer := f let print_path x = !path_printer x -let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref = - ref (fun _ _ _ _ -> false) +let path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) ref = + ref (fun _ _ _ _ _ -> false) let install_path_comparator f = path_comparator := f @@ -315,7 +315,10 @@ let warn_ambiguous_path = CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker" (fun l -> prlist_with_sep fnl (fun (c,p,q) -> str"New coercion path " ++ print_path (c,p) ++ - str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l) + if List.is_empty q then + str" is not definitionally an identity function." + else + str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l) (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -334,10 +337,23 @@ let add_coercion_in_graph env sigma (ic,source,target) = let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in let try_add_new_path (i,j as ij) p = + (* If p is a cycle, we check whether p is definitionally an identity + function or not. If it is not, we report p as an ambiguous inheritance + path. *) + if Bijint.Index.equal i j && not (compare_path env sigma i p []) then + ambig_paths := (ij,p,[])::!ambig_paths; if not (Bijint.Index.equal i j) || different_class_params env i then match lookup_path_between_class ij with | q -> - if not (compare_path env sigma p q) then + (* p has the same source and target classes as an existing path q. We + report them as ambiguous inheritance paths if + 1. p and q have no common element, and + 2. p and q are not convertible. + If 1 does not hold, say p = p1 @ [c] @ p2 and q = q1 @ [c] @ q2, + convertibility of p1 and q1, also, p2 and q2 should be checked; thus, + checking the ambiguity of p and q is redundant with them. *) + if not (List.exists (fun c -> List.exists (coe_info_typ_equal c) q) p || + compare_path env sigma i p q) then ambig_paths := (ij,p,q)::!ambig_paths; false | exception Not_found -> (add_new_path ij p; true) @@ -355,7 +371,7 @@ let add_coercion_in_graph env sigma (ic,source,target) = try_add_new_path1 (s,target) (p@[ic]); ClPairMap.iter (fun (u,v) q -> - if not (Bijint.Index.equal u v) && Bijint.Index.equal u target && not (List.equal coe_info_typ_equal p q) then + if not (Bijint.Index.equal u v) && Bijint.Index.equal u target then try_add_new_path1 (s,v) (p@[ic]@q)) old_inheritance_graph end; diff --git a/pretyping/classops.mli b/pretyping/coercionops.mli index 9c5274286e..9f633843eb 100644 --- a/pretyping/classops.mli +++ b/pretyping/coercionops.mli @@ -111,7 +111,7 @@ val lookup_pattern_path_between : val install_path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit val install_path_comparator : - (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit + (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4925f3e5fa..bfdb471c46 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -288,16 +288,18 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with (* [check_evars] fails if some unresolved evar remains *) -let check_evars env initial_sigma sigma c = +let check_evars env ?initial sigma c = let rec proc_rec c = match EConstr.kind sigma c with | Evar (evk, _) -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in - begin match k with - | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None - end + (match initial with + | Some initial when Evd.mem initial evk -> () + | _ -> + let (loc,k) = evar_source evk sigma in + begin match k with + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () + | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None + end) | _ -> EConstr.iter sigma proc_rec c in proc_rec c @@ -478,26 +480,142 @@ let mark_obligation_evar sigma k evc = Evd.set_obligation_evar sigma (fst (destEvar sigma evc)) | _ -> sigma -(* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *) -(* in environment [env], with existential variables [sigma] and *) -(* the type constraint tycon *) +type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> type_constraint -> GlobEnv.t -> evar_map -> evar_map * 'a + +type pretyper = { + pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun; + pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun; + pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun; + pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun; + pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun; + pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; + pretype_prod : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; + pretype_letin : pretyper -> Name.t * glob_constr * glob_constr option * glob_constr -> unsafe_judgment pretype_fun; + pretype_cases : pretyper -> Constr.case_style * glob_constr option * tomatch_tuples * cases_clauses -> unsafe_judgment pretype_fun; + pretype_lettuple : pretyper -> Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr -> unsafe_judgment pretype_fun; + pretype_if : pretyper -> glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr -> unsafe_judgment pretype_fun; + pretype_rec : pretyper -> glob_fix_kind * Id.t array * glob_decl list array * glob_constr array * glob_constr array -> unsafe_judgment pretype_fun; + pretype_sort : pretyper -> glob_sort -> unsafe_judgment pretype_fun; + pretype_hole : pretyper -> Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option -> unsafe_judgment pretype_fun; + pretype_cast : pretyper -> glob_constr * glob_constr cast_type -> unsafe_judgment pretype_fun; + pretype_int : pretyper -> Uint63.t -> unsafe_judgment pretype_fun; + pretype_float : pretyper -> Float64.t -> unsafe_judgment pretype_fun; + pretype_type : pretyper -> glob_constr -> unsafe_type_judgment pretype_fun; +} -let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t = - let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in - let pretype_type = pretype_type ~program_mode ~poly resolve_tc in - let pretype = pretype ~program_mode ~poly resolve_tc in - let open Context.Rel.Declaration in +(** Tie the loop *) +let eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t = let loc = t.CAst.loc in match DAst.get t with | GRef (ref,u) -> + self.pretype_ref self (ref, u) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GVar id -> + self.pretype_var self id ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GEvar (evk, args) -> + self.pretype_evar self (evk, args) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GPatVar knd -> + self.pretype_patvar self knd ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GApp (c, args) -> + self.pretype_app self (c, args) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GLambda (na, bk, t, c) -> + self.pretype_lambda self (na, bk, t, c) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GProd (na, bk, t, c) -> + self.pretype_prod self (na, bk, t, c) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GLetIn (na, b, t, c) -> + self.pretype_letin self (na, b, t, c) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GCases (st, c, tm, cl) -> + self.pretype_cases self (st, c, tm, cl) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GLetTuple (na, b, t, c) -> + self.pretype_lettuple self (na, b, t, c) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GIf (c, r, t1, t2) -> + self.pretype_if self (c, r, t1, t2) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GRec (knd, nas, decl, c, t) -> + self.pretype_rec self (knd, nas, decl, c, t) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GSort s -> + self.pretype_sort self s ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GHole (knd, nam, arg) -> + self.pretype_hole self (knd, nam, arg) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GCast (c, t) -> + self.pretype_cast self (c, t) ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GInt n -> + self.pretype_int self n ?loc ~program_mode ~poly resolve_tc tycon env sigma + | GFloat f -> + self.pretype_float self f ?loc ~program_mode ~poly resolve_tc tycon env sigma + +let eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t = + self.pretype_type self t ~program_mode ~poly resolve_tc tycon env sigma + +let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk update = + let f decl (subst,update,sigma) = + let id = NamedDecl.get_id decl in + let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in + let t = replace_vars subst (NamedDecl.get_type decl) in + let check_body sigma id c = + match b, c with + | Some b, Some c -> + if not (is_conv !!env sigma b c) then + user_err ?loc (str "Cannot interpret " ++ + pr_existential_key sigma evk ++ + strbrk " in current context: binding for " ++ Id.print id ++ + strbrk " is not convertible to its expected definition (cannot unify " ++ + quote (Termops.Internal.print_constr_env !!env sigma b) ++ + strbrk " and " ++ + quote (Termops.Internal.print_constr_env !!env sigma c) ++ + str ").") + | Some b, None -> + user_err ?loc (str "Cannot interpret " ++ + pr_existential_key sigma evk ++ + strbrk " in current context: " ++ Id.print id ++ + strbrk " should be bound to a local definition.") + | None, _ -> () in + let check_type sigma id t' = + if not (is_conv !!env sigma t t') then + user_err ?loc (str "Cannot interpret " ++ + pr_existential_key sigma evk ++ + strbrk " in current context: binding for " ++ Id.print id ++ + strbrk " is not well-typed.") in + let sigma, c, update = + try + let c = List.assoc id update in + let sigma, c = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in + check_body sigma id (Some c.uj_val); + sigma, c.uj_val, List.remove_assoc id update + with Not_found -> + try + let (n,b',t') = lookup_rel_id id (rel_context !!env) in + check_type sigma id (lift n t'); + check_body sigma id (Option.map (lift n) b'); + sigma, mkRel n, update + with Not_found -> + try + let decl = lookup_named id !!env in + check_type sigma id (NamedDecl.get_type decl); + check_body sigma id (NamedDecl.get_value decl); + sigma, mkVar id, update + with Not_found -> + user_err ?loc (str "Cannot interpret " ++ + pr_existential_key sigma evk ++ + str " in current context: no binding for " ++ Id.print id ++ str ".") in + ((id,c)::subst, update, sigma) in + let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in + check_instance loc subst inst; + sigma, Array.map_of_list snd subst + +module Default = +struct + + let pretype_ref self (ref, u) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let sigma, t_ref = pretype_ref ?loc sigma env ref u in - inh_conv_coerce_to_tycon ?loc env sigma t_ref tycon + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon - | GVar id -> + let pretype_var self id = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let pretype tycon env sigma t = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t in let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in - inh_conv_coerce_to_tycon ?loc env sigma t_id tycon + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon - | GEvar (id, inst) -> + let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma = (* 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 id = interp_ltac_id env id in @@ -505,12 +623,12 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : try Evd.evar_key id sigma with Not_found -> error_evar_not_found ?loc !!env sigma id in let hyps = evar_filtered_context (Evd.find sigma evk) in - let sigma, args = pretype_instance ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in + let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in let c = mkEvar (evk, args) in let j = Retyping.get_judgment_of !!env sigma c in - inh_conv_coerce_to_tycon ?loc env sigma j tycon + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon - | GPatVar kind -> + let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma = let sigma, ty = match tycon with | Some ty -> sigma, ty @@ -519,7 +637,10 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let sigma, uj_val = new_evar env sigma ~src:(loc,k) ty in sigma, { uj_val; uj_type = ty } - | GHole (k, naming, None) -> + let pretype_hole self (k, naming, ext) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + match ext with + | None -> let open Namegen in let naming = match naming with | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id) @@ -533,7 +654,7 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let sigma = if program_mode then mark_obligation_evar sigma k uj_val else sigma in sigma, { uj_val; uj_type = ty } - | GHole (k, _naming, Some arg) -> + | Some arg -> let sigma, ty = match tycon with | Some ty -> sigma, ty @@ -541,7 +662,11 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in sigma, { uj_val = c; uj_type = ty } - | GRec (fixkind,names,bl,lar,vdef) -> + let pretype_rec self (fixkind, names, bl, lar, vdef) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let open Context.Rel.Declaration in + let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in + let pretype_type tycon env sigma c = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let rec type_bl env sigma ctxt = function | [] -> sigma, ctxt @@ -632,13 +757,16 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon ?loc env sigma fixj tycon + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon - | GSort s -> + let pretype_sort self s = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let sigma, j = pretype_sort ?loc sigma s in - inh_conv_coerce_to_tycon ?loc env sigma j tycon + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon - | GApp (f,args) -> + let pretype_app self (f, args) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, fj = pretype empty_tycon env sigma f in let floc = loc_of_glob_constr f in let length = List.length args in @@ -738,7 +866,7 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : else sigma, resj | _ -> sigma, resj in - let sigma, t = inh_conv_coerce_to_tycon ?loc env sigma resj tycon in + let sigma, t = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in let refine_arg sigma (newarg,origarg) = (* Refine an argument (originally `origarg`) represented by an evar (`newarg`) to use typing information from the context *) @@ -755,7 +883,9 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let sigma = List.fold_left refine_arg sigma bidiargs in (sigma, t) - | GLambda(name,bk,c1,c2) -> + let pretype_lambda self (name, bk, c1, c2) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let open Context.Rel.Declaration in let sigma, tycon' = match tycon with | None -> sigma, tycon @@ -765,17 +895,20 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : in let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in let dom_valcon = valcon_of_tycon dom in - let sigma, j = pretype_type dom_valcon env sigma c1 in + let sigma, j = eval_type_pretyper self ~program_mode ~poly resolve_tc dom_valcon env sigma c1 in let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in let var = LocalAssum (name, j.utj_val) in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let var',env' = push_rel ~hypnaming sigma var env in - let sigma, j' = pretype rng env' sigma c2 in + let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in let name = get_name var' in let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in - inh_conv_coerce_to_tycon ?loc env sigma resj tycon + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon - | GProd(name,bk,c1,c2) -> + let pretype_prod self (name, bk, c1, c2) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let open Context.Rel.Declaration in + let pretype_type tycon env sigma c = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, j = pretype_type empty_valcon env sigma c1 in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let sigma, name, j' = match name with @@ -796,9 +929,13 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let (e, info) = CErrors.push e in let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info) in - inh_conv_coerce_to_tycon ?loc env sigma resj tycon + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon - | GLetIn(name,c1,t,c2) -> + let pretype_letin self (name, c1, t, c2) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let open Context.Rel.Declaration in + let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in + let pretype_type tycon env sigma c = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, tycon1 = match t with | Some t -> @@ -819,7 +956,11 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : sigma, { uj_val = mkLetIn (make_annot name r, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } - | GLetTuple (nal,(na,po),c,d) -> + let pretype_lettuple self (nal, (na, po), c, d) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let open Context.Rel.Declaration in + let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in + let pretype_type tycon env sigma c = eval_type_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = pretype empty_tycon env sigma c in let (IndType (indf,realargs)) = try find_rectype !!env sigma cj.uj_type @@ -912,7 +1053,15 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : obj ind rci p cj.uj_val fj.uj_val in sigma, { uj_val = v; uj_type = ccl }) - | GIf (c,(na,po),b1,b2) -> + let pretype_cases self (sty, po, tml, eqns) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in + Cases.compile_cases ?loc ~program_mode sty (pretype, sigma) tycon env (po,tml,eqns) + + let pretype_if self (c, (na, po), b1, b2) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let open Context.Rel.Declaration in + let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = pretype empty_tycon env sigma c in let (IndType (indf,realargs)) = try find_rectype !!env sigma cj.uj_type @@ -938,7 +1087,7 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in let sigma, pred, p = match po with | Some p -> - let sigma, pj = pretype_type empty_valcon env_p sigma p in + let sigma, pj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env_p sigma p in let ccl = nf_evar sigma pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist sigma (pred,[cj.uj_val])) in @@ -973,12 +1122,11 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in - inh_conv_coerce_to_tycon ?loc env sigma cj tycon + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon - | GCases (sty,po,tml,eqns) -> - Cases.compile_cases ?loc ~program_mode sty (pretype, sigma) tycon env (po,tml,eqns) - - | GCast (c,k) -> + let pretype_cast self (c, k) = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> + let pretype tycon env sigma c = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma c in let sigma, cj = match k with | CastCoerce -> @@ -986,7 +1134,7 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in - let sigma, tj = pretype_type empty_valcon env sigma t in + let sigma, tj = eval_type_pretyper self ~program_mode ~poly resolve_tc empty_valcon env sigma t in let sigma, tval = Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma tj.utj_val in let tval = nf_evar sigma tval in @@ -1017,81 +1165,28 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : in let v = mkCast (cj.uj_val, k, tval) in sigma, { uj_val = v; uj_type = tval } - in inh_conv_coerce_to_tycon ?loc env sigma cj tycon + in inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon - | GInt i -> + let pretype_int self i = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let resj = try Typing.judge_of_int !!env i with Invalid_argument _ -> user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.") in - inh_conv_coerce_to_tycon ?loc env sigma resj tycon - | GFloat f -> + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + + let pretype_float self f = + fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let resj = try Typing.judge_of_float !!env f with Invalid_argument _ -> user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.") in - inh_conv_coerce_to_tycon ?loc env sigma resj tycon - -and pretype_instance ~program_mode ~poly resolve_tc env sigma loc hyps evk update = - let f decl (subst,update,sigma) = - let id = NamedDecl.get_id decl in - let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in - let t = replace_vars subst (NamedDecl.get_type decl) in - let check_body sigma id c = - match b, c with - | Some b, Some c -> - if not (is_conv !!env sigma b c) then - user_err ?loc (str "Cannot interpret " ++ - pr_existential_key sigma evk ++ - strbrk " in current context: binding for " ++ Id.print id ++ - strbrk " is not convertible to its expected definition (cannot unify " ++ - quote (Termops.Internal.print_constr_env !!env sigma b) ++ - strbrk " and " ++ - quote (Termops.Internal.print_constr_env !!env sigma c) ++ - str ").") - | Some b, None -> - user_err ?loc (str "Cannot interpret " ++ - pr_existential_key sigma evk ++ - strbrk " in current context: " ++ Id.print id ++ - strbrk " should be bound to a local definition.") - | None, _ -> () in - let check_type sigma id t' = - if not (is_conv !!env sigma t t') then - user_err ?loc (str "Cannot interpret " ++ - pr_existential_key sigma evk ++ - strbrk " in current context: binding for " ++ Id.print id ++ - strbrk " is not well-typed.") in - let sigma, c, update = - try - let c = List.assoc id update in - let sigma, c = pretype ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in - check_body sigma id (Some c.uj_val); - sigma, c.uj_val, List.remove_assoc id update - with Not_found -> - try - let (n,b',t') = lookup_rel_id id (rel_context !!env) in - check_type sigma id (lift n t'); - check_body sigma id (Option.map (lift n) b'); - sigma, mkRel n, update - with Not_found -> - try - let decl = lookup_named id !!env in - check_type sigma id (NamedDecl.get_type decl); - check_body sigma id (NamedDecl.get_value decl); - sigma, mkVar id, update - with Not_found -> - user_err ?loc (str "Cannot interpret " ++ - pr_existential_key sigma evk ++ - str " in current context: no binding for " ++ Id.print id ++ str ".") in - ((id,c)::subst, update, sigma) in - let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in - check_instance loc subst inst; - sigma, Array.map_of_list snd subst + inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon (* [pretype_type valcon env sigma c] coerces [c] into a type *) -and pretype_type ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with +let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma = match DAst.get c with | GHole (knd, naming, None) -> let loc = loc_of_glob_constr c in (match valcon with @@ -1118,7 +1213,7 @@ and pretype_type ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma c let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in sigma, { utj_val; utj_type = s}) | _ -> - let sigma, j = pretype ~program_mode ~poly resolve_tc empty_tycon env sigma c in + let sigma, j = eval_pretyper self ~program_mode ~poly resolve_tc empty_tycon env sigma c in let loc = loc_of_glob_constr c in let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in match valcon with @@ -1131,6 +1226,41 @@ and pretype_type ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma c ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v end +end + +(* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *) +(* in environment [env], with existential variables [sigma] and *) +(* the type constraint tycon *) + +let default_pretyper = + let open Default in + { + pretype_ref = pretype_ref; + pretype_var = pretype_var; + pretype_evar = pretype_evar; + pretype_patvar = pretype_patvar; + pretype_app = pretype_app; + pretype_lambda = pretype_lambda; + pretype_prod = pretype_prod; + pretype_letin = pretype_letin; + pretype_cases = pretype_cases; + pretype_lettuple = pretype_lettuple; + pretype_if = pretype_if; + pretype_rec = pretype_rec; + pretype_sort = pretype_sort; + pretype_hole = pretype_hole; + pretype_cast = pretype_cast; + pretype_int = pretype_int; + pretype_float = pretype_float; + pretype_type = pretype_type; + } + +let pretype ~program_mode ~poly resolve_tc tycon env sigma c = + eval_pretyper default_pretyper ~program_mode ~poly resolve_tc tycon env sigma c + +let pretype_type ~program_mode ~poly resolve_tc tycon env sigma c = + eval_type_pretyper default_pretyper ~program_mode ~poly resolve_tc tycon env sigma c + let ise_pretype_gen flags env sigma lvar kind c = let program_mode = flags.program_mode in let poly = flags.polymorphic in @@ -1195,19 +1325,20 @@ let understand_ltac flags env sigma lvar kind c = let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let path_convertible env sigma p q = - let open Classops in +let path_convertible env sigma i p q = + let open Coercionops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Explicit,t,b) in + let mkGSort u = DAst.make @@ Glob_term.GSort u in let mkGHole () = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in let path_to_gterm p = match p with | ic :: p' -> let names = - List.map (fun n -> Id.of_string ("x" ^ string_of_int n)) - (List.interval 0 ic.coe_param) + List.init (ic.coe_param + 1) + (fun n -> Id.of_string ("x" ^ string_of_int n)) in List.fold_right (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ @@ -1215,9 +1346,29 @@ let path_convertible env sigma p q = (fun t ic -> mkGApp (mkGRef ic.coe_value, List.make ic.coe_param (mkGHole ()) @ [t])) - (mkGApp (mkGRef ic.coe_value, List.map (fun i -> mkGVar i) names)) + (mkGApp (mkGRef ic.coe_value, List.map mkGVar names)) p' - | [] -> anomaly (str "A coercion path shouldn't be empty.") + | [] -> + (* identity function for the class [i]. *) + let cl,params = class_info_from_index i in + let clty = + match cl with + | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false}) + | CL_FUN -> anomaly (str "A source class must not be Funclass.") + | CL_SECVAR v -> mkGRef (GlobRef.VarRef v) + | CL_CONST c -> mkGRef (GlobRef.ConstRef c) + | CL_IND i -> mkGRef (GlobRef.IndRef i) + | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p)) + in + let names = + List.init params.cl_param + (fun n -> Id.of_string ("x" ^ string_of_int n)) + in + List.fold_right + (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ + mkGLambda (Name (Id.of_string "x"), + mkGApp (clty, List.map mkGVar names), + mkGVar (Id.of_string "x")) in try let sigma,tp = understand_tcc env sigma (path_to_gterm p) in @@ -1228,4 +1379,4 @@ let path_convertible env sigma p q = let _ = Evarconv.unify_delay env sigma tp tq in true with Evarconv.UnableToUnify _ | PretypeError _ -> false -let _ = Classops.install_path_comparator path_convertible +let _ = Coercionops.install_path_comparator path_convertible diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f9da568c75..18e416596e 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -115,12 +115,49 @@ val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> val check_evars_are_solved : program_mode:bool -> env -> ?initial:evar_map -> (* current map: *) evar_map -> unit -(** [check_evars env initial_sigma extended_sigma c] fails if some - new unresolved evar remains in [c] *) -val check_evars : env -> evar_map -> evar_map -> constr -> unit +(** [check_evars env ?initial sigma c] fails if some unresolved evar + remains in [c] which isn't in [initial] (any unresolved evar if + [initial] not provided) *) +val check_evars : env -> ?initial:evar_map -> evar_map -> constr -> unit (**/**) (** Internal of Pretyping... *) val ise_pretype_gen : inference_flags -> env -> evar_map -> ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types + +(** {6 Open-recursion style pretyper} *) + +type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> Evardefine.type_constraint -> GlobEnv.t -> evar_map -> evar_map * 'a + +type pretyper = { + pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun; + pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun; + pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun; + pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun; + pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun; + pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; + pretype_prod : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; + pretype_letin : pretyper -> Name.t * glob_constr * glob_constr option * glob_constr -> unsafe_judgment pretype_fun; + pretype_cases : pretyper -> Constr.case_style * glob_constr option * tomatch_tuples * cases_clauses -> unsafe_judgment pretype_fun; + pretype_lettuple : pretyper -> Name.t list * (Name.t * glob_constr option) * glob_constr * glob_constr -> unsafe_judgment pretype_fun; + pretype_if : pretyper -> glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr -> unsafe_judgment pretype_fun; + pretype_rec : pretyper -> glob_fix_kind * Id.t array * glob_decl list array * glob_constr array * glob_constr array -> unsafe_judgment pretype_fun; + pretype_sort : pretyper -> glob_sort -> unsafe_judgment pretype_fun; + pretype_hole : pretyper -> Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option -> unsafe_judgment pretype_fun; + pretype_cast : pretyper -> glob_constr * glob_constr cast_type -> unsafe_judgment pretype_fun; + pretype_int : pretyper -> Uint63.t -> unsafe_judgment pretype_fun; + pretype_float : pretyper -> Float64.t -> unsafe_judgment pretype_fun; + pretype_type : pretyper -> glob_constr -> unsafe_type_judgment pretype_fun; +} +(** Type of pretyping algorithms in open-recursion style. A typical way to + implement a pretyping variant is to inherit from some pretyper using + record inheritance and replacing particular fields with the [where] clause. + Recursive calls to the subterms should call the [pretyper] provided as the + first argument to the function. This object can be turned in an actual + pretyping function through the {!eval_pretyper} function below. *) + +val default_pretyper : pretyper +(** Coq vanilla pretyper. *) + +val eval_pretyper : pretyper -> program_mode:bool -> poly:bool -> bool -> Evardefine.type_constraint -> GlobEnv.t -> evar_map -> glob_constr -> evar_map * unsafe_judgment diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 7e140f4399..07154d4e03 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -26,7 +26,7 @@ Constr_matching Tacred Typeclasses_errors Typeclasses -Classops +Coercionops Program Coercion Detyping diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5b416a99f9..35e182840b 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -114,7 +114,7 @@ let find_primitive_projection c = (* the effective components of a structure and the projections of the *) (* structure *) -(* Table des definitions "object" : pour chaque object c, +(* Table of "object" definitions: for each object c, c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n) @@ -127,16 +127,19 @@ let find_primitive_projection c = that maps the pair (Li,ci) to the following data + o_ORIGIN = c (the constant name which this conversion rule is + synthesized from) o_DEF = c o_TABS = B1...Bk o_INJ = Some n (when ci is a reference to the parameter xi) - o_PARAMS = a1...am - o_NARAMS = m + o_TPARAMS = a1...am + o_NPARAMS = m o_TCOMP = ui1...uir *) type obj_typ = { + o_ORIGIN : Constant.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) @@ -224,7 +227,7 @@ let compute_canonical_projections env ~warn (con,ind) = match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> ((GlobRef.ConstRef proji_sp, (patt, t)), - { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) + { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index e8b0d771aa..aaba7cc3e5 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -73,6 +73,7 @@ type cs_pattern = | Default_cs type obj_typ = { + o_ORIGIN : Constant.t; o_DEF : constr; o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) |