diff options
37 files changed, 1662 insertions, 1636 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d56a375bf..6b221ecd8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1742,7 +1742,7 @@ let interp_gen kind sigma env ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in - Default.understand_gen kind sigma env c + understand_gen kind sigma env c let interp_constr sigma env c = interp_gen (OfType None) sigma env c @@ -1754,7 +1754,7 @@ let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ = interp_gen (OfType (Some typ)) sigma env ~impls c let interp_open_constr sigma env c = - Default.understand_tcc sigma env (intern_constr sigma env c) + understand_tcc sigma env (intern_constr sigma env c) let interp_open_constr_patvar sigma env c = let raw = intern_gen false sigma env c ~allow_patvar:true in @@ -1772,10 +1772,10 @@ let interp_open_constr_patvar sigma env c = ) | _ -> map_glob_constr patvar_to_evar r in let raw = patvar_to_evar raw in - Default.understand_tcc !sigma env raw + understand_tcc !sigma env raw let interp_constr_judgment sigma env c = - Default.understand_judgment sigma env (intern_constr sigma env c) + understand_judgment sigma env (intern_constr sigma env c) let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) kind c = @@ -1787,7 +1787,7 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) let istype = kind = IsType in let c = intern_gen istype ~impls !evdref env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in - Default.understand_tcc_evars ~fail_evar evdref env kind c, imps + understand_tcc_evars ~fail_evar evdref env kind c, imps let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c typ = @@ -1801,7 +1801,7 @@ let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_intern let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c = let c = intern_gen (kind=IsType) ~impls !evdref env c in - Default.understand_tcc_evars evdref env kind c + understand_tcc_evars evdref env kind c let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c @@ -1836,12 +1836,12 @@ let interp_aconstr ?(impls=empty_internalization_env) vars recvars a = let interp_binder sigma env na t = let t = intern_gen true sigma env t in let t' = locate_if_isevar (loc_of_glob_constr t) na t in - Default.understand_type sigma env t' + understand_type sigma env t' let interp_binder_evars evdref env na t = let t = intern_gen true !evdref env t in let t' = locate_if_isevar (loc_of_glob_constr t) na t in - Default.understand_tcc_evars evdref env IsType t' + understand_tcc_evars evdref env IsType t' open Environ open Term @@ -1886,10 +1886,10 @@ let interp_context_gen understand_type understand_judgment ?(global_level=false) int_env, interp_rawcontext_gen understand_type understand_judgment env bl let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params = - interp_context_gen (Default.understand_type sigma) - (Default.understand_judgment sigma) ~global_level ~impl_env sigma env params + interp_context_gen (understand_type sigma) + (understand_judgment sigma) ~global_level ~impl_env sigma env params let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params = - interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) - (Default.understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params + interp_context_gen (fun env t -> understand_tcc_evars evdref env IsType t) + (understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params diff --git a/lib/flags.ml b/lib/flags.ml index 470cf81f1..29e01bac3 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -66,6 +66,9 @@ let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros +let program_mode = ref false +let is_program_mode () = !program_mode + let hash_cons_proofs = ref true let warn = ref true diff --git a/lib/flags.mli b/lib/flags.mli index da43c8678..94c8795d4 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -47,6 +47,9 @@ val if_verbose : ('a -> unit) -> 'a -> unit val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool +val program_mode : bool ref +val is_program_mode : unit -> bool + val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit diff --git a/lib/util.ml b/lib/util.ml index 879884283..c4229fd32 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1211,6 +1211,11 @@ let iterate_for a b f x = let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in iterate a x +let app_opt f x = + match f with + | Some f -> f x + | None -> x + (* Delayed computations *) type 'a delayed = unit -> 'a diff --git a/lib/util.mli b/lib/util.mli index caf1723b3..868a76711 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -261,6 +261,7 @@ val const : 'a -> 'b -> 'a val iterate : ('a -> 'a) -> int -> 'a -> 'a val repeat : int -> ('a -> unit) -> 'a -> unit val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a +val app_opt : ('a -> 'a) option -> 'a -> 'a (** {6 Delayed computations. } *) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 512269e55..21d2b125e 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -14,7 +14,7 @@ open Tacinterp open Tacmach open Decl_expr open Decl_mode -open Pretyping.Default +open Pretyping open Glob_term open Term open Pp diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e3a95fb4f..c848faaa7 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1289,7 +1289,7 @@ let understand_my_constr c gls = let nc = names_of_rel_context env in let rawc = Detyping.detype false [] nc c in let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc -> map_glob_constr frob rc in - Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) + Pretyping.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) let my_refine c gls = let oc = understand_my_constr c gls in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 8d4b0eee1..a955891f8 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -130,7 +130,7 @@ let mk_open_instance id gl m t= GLambda(loc,name,k,GHole (dummy_loc,Evd.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=try - Pretyping.Default.understand evmap env (raux m rawt) + Pretyping.understand evmap env (raux m rawt) with _ -> error "Untypable instance, maybe higher-order non-prenex quantification" in decompose_lam_n_assum m ntt diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6a5888874..a7298095e 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -368,8 +368,8 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in - let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in + let value = Option.map (Pretyping.understand Evd.empty env) raw_value in + let typ = Pretyping.understand_type Evd.empty env raw_typ in Environ.push_named (id,value,typ) env @@ -521,7 +521,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = a pseudo value "v1 ... vn". The "value" of this branch is then simply [res] *) - let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in + let rt_as_constr = Pretyping.understand Evd.empty env rt in let rt_typ = Typing.type_of env Evd.empty rt_as_constr in let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in let res = fresh_id args_res.to_avoid "res" in @@ -629,7 +629,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = and combine the two result *) let v_res = build_entry_lc env funnames avoid v in - let v_as_constr = Pretyping.Default.understand Evd.empty env v in + let v_as_constr = Pretyping.understand Evd.empty env v in let v_type = Typing.type_of env Evd.empty v_as_constr in let new_env = match n with @@ -645,7 +645,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let make_discr = make_discr_match brl in build_entry_lc_from_case env funnames make_discr el brl avoid | GIf(_,b,(na,e_option),lhs,rhs) -> - let b_as_constr = Pretyping.Default.understand Evd.empty env b in + let b_as_constr = Pretyping.understand Evd.empty env b in let b_typ = Typing.type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ @@ -677,7 +677,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = ) nal in - let b_as_constr = Pretyping.Default.understand Evd.empty env b in + let b_as_constr = Pretyping.understand Evd.empty env b in let b_typ = Typing.type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ @@ -724,7 +724,7 @@ and build_entry_lc_from_case env funname make_discr in let types = List.map (fun (case_arg,_) -> - let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in + let case_arg_as_constr = Pretyping.understand Evd.empty env case_arg in Typing.type_of env Evd.empty case_arg_as_constr ) el in @@ -928,7 +928,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_t = mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) in - let t' = Pretyping.Default.understand Evd.empty env new_t in + let t' = Pretyping.understand Evd.empty env new_t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -948,7 +948,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = try observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = - try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue + try Pretyping.understand Evd.empty env t with _ -> raise Continue in let is_in_b = is_free_in id b in let _keep_eq = @@ -970,7 +970,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude with Continue -> let jmeq = Libnames.IndRef (destInd (jmeq ())) in - let ty' = Pretyping.Default.understand Evd.empty env ty in + let ty' = Pretyping.understand Evd.empty env ty in let ind,args' = Inductive.find_inductive env ty' in let mib,_ = Global.lookup_inductive ind in let nparam = mib.Declarations.mind_nparams in @@ -992,7 +992,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); - let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in + let eq'_as_constr = Pretyping.understand Evd.empty env eq' in observe (str " computing new type for jmeq : done") ; let new_args = match kind_of_term eq'_as_constr with @@ -1040,7 +1040,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = if is_in_b then b else replace_var_by_term id rt b in let new_env = - let t' = Pretyping.Default.understand Evd.empty env eq' in + let t' = Pretyping.understand Evd.empty env eq' in Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = @@ -1078,7 +1078,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else raise Continue with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t' = Pretyping.Default.understand Evd.empty env t in + let t' = Pretyping.understand Evd.empty env t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1094,7 +1094,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = end | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t' = Pretyping.Default.understand Evd.empty env t in + let t' = Pretyping.understand Evd.empty env t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1113,7 +1113,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in observe (str "computing new type for lambda : " ++ pr_glob_constr rt); - let t' = Pretyping.Default.understand Evd.empty env t in + let t' = Pretyping.understand Evd.empty env t in match n with | Name id -> let new_env = Environ.push_rel (n,None,t') env in @@ -1135,7 +1135,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | GLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in - let t' = Pretyping.Default.understand Evd.empty env t in + let t' = Pretyping.understand Evd.empty env t in let type_t' = Typing.type_of env Evd.empty t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = @@ -1160,7 +1160,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = args (crossed_types) depth t in - let t' = Pretyping.Default.understand Evd.empty env new_t in + let t' = Pretyping.understand Evd.empty env new_t in let new_env = Environ.push_rel (na,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 3b3f3057b..3ea9c3d3e 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -49,7 +49,7 @@ let rec substitterm prof t by_t in_u = let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl -let understand = Pretyping.Default.understand Evd.empty (Global.env()) +let understand = Pretyping.understand Evd.empty (Global.env()) (** Operations on names and identifiers *) let id_of_name = function diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c37de6e4a..0f92378d6 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -36,7 +36,6 @@ open Pfedit open Topconstr open Glob_term open Pretyping -open Pretyping.Default open Safe_typing open Constrintern open Hiddentac diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index cccb12e41..ffcd40f94 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -142,6 +142,7 @@ let subtac (loc, command) = (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) + | VernacFixpoint l -> List.iter (fun ((lid, _, _, _, _), _) -> check_fresh lid; @@ -177,9 +178,6 @@ let subtac (loc, command) = List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; ignore(Subtac_command.build_corecursive l) - (*| VernacEndProof e -> - subtac_end_proof e*) - | _ -> user_err_loc (loc,"", str ("Invalid Program command")) with | Typing_error e -> @@ -227,3 +225,5 @@ let subtac (loc, command) = | e -> (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *) raise e + +let subtac c = Program.with_program subtac c diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 279e4d87a..3b740f161 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -345,7 +345,6 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c = ignore(Typing.sort_of env' evm pred); pred with _ -> lift nar c -module Cases_F(Coercion : Coercion.S) : S = struct let inh_coerce_to_ind isevars env ty tyi = let expected_typ = inductive_template isevars env None tyi in @@ -1481,8 +1480,6 @@ let inh_conv_coerce_to_tycon loc env isevars j tycon = j | None -> j -let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false) - let string_of_name name = match name with | Anonymous -> "anonymous" @@ -1919,7 +1916,7 @@ let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon in Some (build_initial_predicate true allnames pred) | None -> None -let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = +let compile_program_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = let typing_fun tycon env = typing_fun tycon env isevars in @@ -2016,6 +2013,3 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; inh_conv_coerce_to_tycon loc env isevars j tycon - -end - diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli index 11a811597..b7e78f6d2 100644 --- a/plugins/subtac/subtac_cases.mli +++ b/plugins/subtac/subtac_cases.mli @@ -19,4 +19,3 @@ open Evarutil (*i*) (*s Compilation of pattern-matching, subtac style. *) -module Cases_F(C : Coercion.S) : Cases.S diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index a81243f73..75d0f3429 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -25,10 +25,8 @@ open Entries open Errors open Util -module SPretyping = Subtac_pretyping.Pretyping - let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c = - SPretyping.understand_tcc_evars evdref env kind + understand_tcc_evars evdref env kind (intern_gen (kind=IsType) ~impls !evdref env c) let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ = @@ -36,13 +34,13 @@ let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internaliza let interp_context_evars evdref env params = let impls_env, bl = Constrintern.interp_context_gen - (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t) - (SPretyping.understand_judgment_tcc evdref) !evdref env params in bl + (fun env t -> understand_tcc_evars evdref env IsType t) + (understand_judgment_tcc evdref) !evdref env params in bl let interp_type_evars_impls ~evdref ?(impls=empty_internalization_env) env c = let c = intern_gen true ~impls !evdref env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in - SPretyping.understand_tcc_evars ~fail_evar:false evdref env IsType c, imps + understand_tcc_evars ~fail_evar:false evdref env IsType c, imps let type_ctx_instance evars env ctx inst subst = let rec aux (subst, instctx) l = function diff --git a/plugins/subtac/subtac_coercion.mli b/plugins/subtac/subtac_coercion.mli index 5678c10e6..b872c99d5 100644 --- a/plugins/subtac/subtac_coercion.mli +++ b/plugins/subtac/subtac_coercion.mli @@ -1,4 +1,2 @@ open Term -val disc_subset : types -> (types * types) option -module Coercion : Coercion.S diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index e5d93ace2..6e6f42308 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -41,7 +41,6 @@ open Notation open Evd open Evarutil -module SPretyping = Subtac_pretyping.Pretyping open Subtac_utils open Pretyping open Subtac_obligations @@ -56,7 +55,7 @@ let interp_gen kind isevars env ?(impls=Constrintern.empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in - let c' = SPretyping.understand_tcc_evars isevars env kind c' in + let c' = understand_tcc_evars isevars env kind c' in evar_nf isevars c' let interp_constr isevars env c = @@ -74,12 +73,12 @@ let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internaliz let interp_open_constr isevars env c = msgnl (str "Pretyping " ++ my_print_constr_expr c); let c = Constrintern.intern_constr ( !isevars) env c in - let c' = SPretyping.understand_tcc_evars isevars env (OfType None) c in + let c' = understand_tcc_evars isevars env (OfType None) c in evar_nf isevars c' let interp_constr_judgment isevars env c = let j = - SPretyping.understand_judgment_tcc isevars env + understand_judgment_tcc isevars env (Constrintern.intern_constr ( !isevars) env c) in { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type } @@ -94,7 +93,7 @@ let locate_if_isevar loc na = function let interp_binder sigma env na t = let t = Constrintern.intern_gen true ( !sigma) env t in - SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t) + understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t) let interp_context_evars evdref env params = let int_env, bl = Constrintern.intern_context false !evdref env Constrintern.empty_internalization_env params in @@ -104,7 +103,7 @@ let interp_context_evars evdref env params = match b with None -> let t' = locate_if_isevar (loc_of_glob_constr t) na t in - let t = SPretyping.understand_tcc_evars evdref env IsType t' in + let t = understand_tcc_evars evdref env IsType t' in let d = (na,None,t) in let impls = if k = Implicit then @@ -114,7 +113,7 @@ let interp_context_evars evdref env params = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = SPretyping.understand_judgment_tcc evdref env b in + let c = understand_judgment_tcc evdref env b in let d = (na, Some c.uj_val, c.uj_type) in (push_rel d env,d::params, succ n, impls)) (env,[],1,[]) (List.rev bl) diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index b83057ac8..f64c1ae2f 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -36,8 +36,6 @@ open Printer open Subtac_errors open Eterm -module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion) - open Pretyping let _ = Pretyping.allow_anonymous_refs := true diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli index fa767790d..e999f1710 100644 --- a/plugins/subtac/subtac_pretyping.mli +++ b/plugins/subtac/subtac_pretyping.mli @@ -8,8 +8,6 @@ open Topconstr open Implicit_quantifiers open Impargs -module Pretyping : Pretyping.S - val interp : Environ.env -> Evd.evar_map ref -> diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 43182765d..464bb8639 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -36,628 +36,3 @@ open Declarations open Inductive open Inductiveops -module SubtacPretyping_F (Coercion : Coercion.S) = struct - - module Cases = Subtac_cases.Cases_F(Coercion) - - (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) - let allow_anonymous_refs = ref true - - 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 - - let evd_comb3 f evdref x y z = - let (evd',t) = f !evdref x y z in - evdref := evd'; - t - - let mt_evd = Evd.empty - - (* Utilisé pour inférer le prédicat des Cases *) - (* Semble exagérement fort *) - (* Faudra préférer une unification entre les types de toutes les clauses *) - (* et autoriser des ? à rester dans le résultat de l'unification *) - - let evar_type_fixpoint loc env evdref lna lar vdefj = - let lt = Array.length vdefj in - if Array.length lar = lt then - for i = 0 to lt-1 do - if not (e_cumul env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env !evdref - i lna vdefj lar - done - - let check_branches_message loc env evdref ind 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 (ind,i) lft.(i) explft.(i) - done - - (* coerce to tycon if any *) - let inh_conv_coerce_to_tycon loc env evdref j = function - | None -> j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t - - let push_rels vars env = List.fold_right push_rel vars env - - (* - let evar_type_case evdref env ct pt lft p c = - let (mind,bty,rslty) = type_case_branches env ( evdref) ct pt p c - in check_branches_message evdref env mind (c,ct) (bty,lft); (mind,rslty) - *) - - let strip_meta id = (* For Grammar v7 compatibility *) - let s = string_of_id id in - if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1)) - else id - - let invert_ltac_bound_name env id0 id = - try mkRel (pi1 (Termops.lookup_rel_id id (rel_context env))) - with Not_found -> - errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++ - str " depends on pattern variable name " ++ pr_id id ++ - str " which is not bound in current context") - - let pretype_id loc env sigma (lvar,unbndltacvars) id = - let id = strip_meta id in (* May happen in tactics defined by Grammar *) - try - let (n,_,typ) = Termops.lookup_rel_id id (rel_context env) in - { uj_val = mkRel n; uj_type = lift n typ } - with Not_found -> - 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 = Retyping.get_type_of env sigma c } - with Not_found -> - 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 *) - 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 -> - 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=Termops.it_mkLambda ccl' sign; uj_type=Termops.it_mkProd s' sign} - - (*************************************************************************) - (* Main pretyping function *) - - let pretype_ref evdref env ref = - let c = constr_of_global ref in - make_judge c (Retyping.get_type_of env Evd.empty c) - - let pretype_sort evdref = function - | GProp c -> judge_of_prop_contents c - | GType _ -> evd_comb0 judge_of_new_Type evdref - - let split_tycon_lam loc env evd tycon = - let rec real_split evd c = - let t = whd_betadeltaiota env evd c in - match kind_of_term t with - | Prod (na,dom,rng) -> evd, (na, dom, rng) - | Evar ev when not (Evd.is_defined_evar evd ev) -> - let (evd',prod) = define_evar_as_product evd ev in - let (_,dom,rng) = destProd prod in - evd',(Anonymous, dom, rng) - | _ -> error_not_product_loc loc env evd c - in - match tycon with - | None -> evd,(Anonymous,None,None) - | Some c -> - let evd', (n, dom, rng) = real_split evd c in - evd', (n, mk_tycon dom, mk_tycon rng) - - - (* [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 c = -(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *) -(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) -(* with _ -> () *) -(* in *) - match c with - | GRef (loc,ref) -> - inh_conv_coerce_to_tycon loc env evdref - (pretype_ref evdref env ref) - tycon - - | GVar (loc, id) -> - inh_conv_coerce_to_tycon loc env evdref - (pretype_id loc env !evdref lvar id) - tycon - - | GEvar (loc, ev, instopt) -> - (* Ne faudrait-il pas s'assurer que hyps est bien un - sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = evar_context (Evd.find !evdref ev) in - let args = match instopt with - | None -> instance_from_named_context hyps - | Some inst -> failwith "Evar subtitutions not implemented" in - let c = mkEvar (ev, args) in - let j = (Retyping.get_judgment_of env !evdref c) in - inh_conv_coerce_to_tycon loc env evdref j tycon - - | GPatVar (loc,(someta,n)) -> - anomaly "Found a pattern variable in a glob_constr to type" - - | GHole (loc,k) -> - let ty = - match tycon with - | Some ty -> ty - | None -> - e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in - { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } - - | GRec (loc,fixkind,names,bl,lar,vdef) -> - let rec type_bl env ctxt = function - [] -> ctxt - | (na,k,None,ty)::bl -> - let ty' = pretype_type empty_valcon env evdref lvar ty in - let dcl = (na,None,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl - | (na,k,Some bd,ty)::bl -> - let ty' = pretype_type empty_valcon env 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 - (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let newenv = - let marked_ftys = - Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in - mkApp (delayed_force Subtac_utils.fix_proto, [| sort; ty |])) - ftys - in - push_rec_types (names,marked_ftys,[||]) env - in - let fixi = match fixkind with GFix (vn, i) -> i | GCoFix i -> i in - let vdefj = - array_map2_i - (fun i ctxt def -> - let fty = - let ty = ftys.(i) in - if i = fixi then ( - Option.iter (fun tycon -> - evdref := Coercion.inh_conv_coerces_to loc env !evdref ftys.(i) tycon) - tycon; - nf_evar !evdref ty) - else ty - in - (* 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 fty) 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 e -> 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 s' = pretype_sort evdref s in - inh_conv_coerce_to_tycon loc env evdref s' 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 = - (* Bidirectional typechecking hint: - parameters of a constructor are completely determined - by a typing constraint *) - if 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 npars = 0 then [] - else - try - (* Does not treat partially applied constructors. *) - let IndType (indf, args) = find_rectype env !evdref ty in - let (ind',pars) = dest_ind_family indf in - if 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 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 - (join_loc floc argloc) env !evdref - resj [hj] - in - let resj = apply_rec env 1 fj candargs args in - let resj = - match kind_of_term (whd_evar !evdref resj.uj_val) with - | App (f,args) when isInd f or isConst 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 t - | _ -> resj in - inh_conv_coerce_to_tycon loc env evdref resj tycon - - | GLambda(loc,name,k,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_lam 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 name j j' in - inh_conv_coerce_to_tycon loc env evdref resj tycon - - | GProd(loc,name,k,c1,c2) -> - let j = pretype_type empty_valcon env evdref lvar c1 in - let var = (name,j.utj_val) in - let env' = Termops.push_rel_assum var env in - let j' = pretype_type empty_valcon env' evdref lvar c2 in - let resj = - try judge_of_product env name j j' - with TypeError _ as e -> Loc.raise loc e in - inh_conv_coerce_to_tycon loc env evdref resj tycon - - | GLetIn(loc,name,c1,c2) -> - let j = pretype empty_tycon env evdref lvar c1 in - let t = Termops.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 } - - | 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 Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); - let cs = cstrs.(0) in - if 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_rels 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_rels 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 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 } - - | 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 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 }) - - | 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 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_rels 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 - let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred; - uj_type = typ} tycon - in - jtyp.uj_val, jtyp.uj_type - | None -> - let p = match tycon with - | Some ty -> ty - | None -> - e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ()) - 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 - 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 - let env_c = push_rels 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 mis,_ = dest_ind_family indf in - let ci = make_case_info env mis IfStyle in - 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) - - | 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 (k,t) -> - let tj = pretype_type empty_valcon env evdref lvar t in - let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in - let v = mkCast (cj.uj_val, k, tj.utj_val) in - { uj_val = v; uj_type = tj.utj_val } - in - inh_conv_coerce_to_tycon loc env evdref cj tycon - - (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type valcon env evdref lvar = function - | GHole loc -> - (match valcon with - | Some v -> - let s = - let sigma = !evdref in - let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_betadeltaiota env sigma t) with - | Sort s -> s - | Evar ev when is_Type (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort) evdref ev - | _ -> anomaly "Found a type constraint which is not a type" - in - { utj_val = v; - utj_type = s } - | None -> - let s = Termops.new_Type_sort () 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_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in - match valcon with - | None -> tj - | Some v -> - if e_cumul env evdref v tj.utj_val then tj - else - error_unexpected_type_loc - (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 - | OfType exptyp -> - 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 - (try - evdref := Typeclasses.resolve_typeclasses ~onlyargs:true - ~split:true ~fail:true env !evdref; - evdref := Typeclasses.resolve_typeclasses ~onlyargs:false - ~split:true ~fail:false env !evdref - with e -> if fail_evar then raise e else ()); - evdref := consider_remaining_unif_problems 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 - - (* 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 understand_judgment sigma env c = - let evdref = ref (create_evar_defs sigma) in - let j = pretype empty_tycon env evdref ([],[]) c in - let evd = consider_remaining_unif_problems env !evdref in - let j = j_nf_evar evd j in - check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); - j - - let understand_judgment_tcc evdref env c = - let j = pretype empty_tycon env evdref ([],[]) c in - j_nf_evar !evdref j - - (* Raw calls to the unsafe inference machine: boolean says if we must - fail on unresolved evars; the unsafe_judgment list allows us to - extend env with some bindings *) - - let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c = - let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in - !evdref, c - - (** Entry points of the high-level type synthesis algorithm *) - - let understand_gen kind sigma env c = - snd (ise_pretype_gen true true true sigma env ([],[]) kind c) - - let understand sigma env ?expected_type:exptyp c = - snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c) - - let understand_type sigma env c = - snd (ise_pretype_gen true false true sigma env ([],[]) IsType c) - - let understand_ltac expand_evar sigma env lvar kind c = - ise_pretype_gen expand_evar false true sigma env lvar kind c - - let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = - ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c - - let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c = - pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c -end - -module Default : S = SubtacPretyping_F(Coercion.Default) diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index 719b87952..5cbb307db 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -79,7 +79,6 @@ val trace : std_ppcmds -> unit val wf_relations : (constr, constr delayed) Hashtbl.t type binders = local_binder list -val app_opt : ('a -> 'a) option -> 'a -> 'a val print_args : env -> constr array -> std_ppcmds val make_existential : loc -> ?opaque:obligation_definition_status -> env -> evar_map ref -> types -> constr diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 2883df6d7..8652dbd03 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -362,9 +362,6 @@ let evd_comb2 f evdref x y = evdref := evd'; y - -module Cases_F(Coercion : Coercion.S) : S = struct - let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (* Ideally, we could find a common inductive type to which both the term to match and the patterns coerce *) @@ -1642,7 +1639,8 @@ let build_initial_predicate arsign pred = | _ -> assert false in buildrec 0 pred [] (List.rev arsign) -let extract_arity_signature env0 tomatchl tmsign = +let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = + let lift = if dolift then lift else fun n t -> t in let get_one_sign n tm (na,t) = match tm with | NotInd (bo,typ) -> @@ -1652,7 +1650,7 @@ let extract_arity_signature env0 tomatchl tmsign = user_err_loc (loc,"", str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> - let indf' = lift_inductive_family n indf in + let indf' = if dolift then lift_inductive_family n indf else indf in let (ind,_) = dest_ind_family indf' in let nparams_ctxt,nrealargs_ctxt = inductive_nargs_env env0 ind in let arsign = fst (get_arity env0 indf') in @@ -1786,11 +1784,511 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred = sigma,nal,pred) preds +module ProgramCases = struct + +open Program + +let ($) f x = f x + +let string_of_name name = + match name with + | Anonymous -> "anonymous" + | Name n -> string_of_id n + +let id_of_name n = id_of_string (string_of_name n) + +let make_prime_id name = + let str = string_of_name name in + id_of_string str, id_of_string (str ^ "'") + +let prime avoid name = + let previd, id = make_prime_id name in + previd, next_ident_away id avoid + +let make_prime avoid prevname = + let previd, id = prime !avoid prevname in + avoid := id :: !avoid; + previd, id + +let eq_id avoid id = + let hid = id_of_string ("Heq_" ^ string_of_id id) in + let hid' = next_ident_away hid avoid in + hid' + +let mk_eq typ x y = mkApp (delayed_force coq_eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (delayed_force coq_eq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = + mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |]) + +let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) + +let constr_of_pat env isevars arsign pat avoid = + let rec typ env (ty, realargs) pat avoid = + match pat with + | PatVar (l,name) -> + let name, avoid = match name with + Name n -> name, avoid + | Anonymous -> + let previd, id = prime avoid (Name (id_of_string "wildcard")) in + Name id, id :: avoid + in + PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid + | PatCstr (l,((_, i) as cstr),args,alias) -> + let cind = inductive_of_constructor cstr in + let IndType (indf, _) = + try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) + with Not_found -> error_case_not_inductive env + {uj_val = ty; uj_type = Typing.type_of env !isevars ty} + in + let ind, params = dest_ind_family indf in + if ind <> cind then error_bad_constructor_loc l cstr ind; + let cstrs = get_constructors env indf in + let ci = cstrs.(i-1) in + let nb_args_constr = ci.cs_nargs in + assert(nb_args_constr = List.length args); + let patargs, args, sign, env, n, m, avoid = + List.fold_right2 + (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) -> + let pat', sign', arg', typ', argtypargs, n', avoid = + typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid + in + let args' = arg' :: List.map (lift n') args in + let env' = push_rels sign' env in + (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid)) + ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid) + in + let args = List.rev args in + let patargs = List.rev patargs in + let pat' = PatCstr (l, cstr, patargs, alias) in + let cstr = mkConstruct ci.cs_cstr in + let app = applistc cstr (List.map (lift (List.length sign)) params) in + let app = applistc app args in + let apptype = Retyping.get_type_of env ( !isevars) app in + let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in + match alias with + Anonymous -> + pat', sign, app, apptype, realargs, n, avoid + | Name id -> + let sign = (alias, None, lift m ty) :: sign in + let avoid = id :: avoid in + let sign, i, avoid = + try + let env = push_rels sign env in + isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars; + let eq_t = mk_eq (lift (succ m) ty) + (mkRel 1) (* alias *) + (lift 1 app) (* aliased term *) + in + let neq = eq_id avoid id in + (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid + with Reduction.NotConvertible -> sign, 1, avoid + in + (* Mark the equality as a hole *) + pat', sign, lift i app, lift i apptype, realargs, n + i, avoid + in + let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in + pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid + + +(* shadows functional version *) +let eq_id avoid id = + let hid = id_of_string ("Heq_" ^ string_of_id id) in + let hid' = next_ident_away hid !avoid in + avoid := hid' :: !avoid; + hid' + +let rels_of_patsign = + List.map (fun ((na, b, t) as x) -> + match b with + | Some t' when kind_of_term t' = Rel 0 -> (na, None, t) + | _ -> x) + +let vars_of_ctx ctx = + let _, y = + List.fold_right (fun (na, b, t) (prev, vars) -> + match b with + | Some t' when kind_of_term t' = Rel 0 -> + prev, + (GApp (dummy_loc, + (GRef (dummy_loc, delayed_force coq_eq_refl_ref)), + [hole; GVar (dummy_loc, prev)])) :: vars + | _ -> + match na with + Anonymous -> raise (Invalid_argument "vars_of_ctx") + | Name n -> n, GVar (dummy_loc, n) :: vars) + ctx (id_of_string "vars_of_ctx_error", []) + in List.rev y + +let rec is_included x y = + match x, y with + | PatVar _, _ -> true + | _, PatVar _ -> true + | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') -> + if i = i' then List.for_all2 is_included args args' + else false + +(* liftsign is the current pattern's complete signature length. Hence pats is already typed in its + full signature. However prevpatterns are in the original one signature per pattern form. + *) +let build_ineqs prevpatterns pats liftsign = + let _tomatchs = List.length pats in + let diffs = + List.fold_left + (fun c eqnpats -> + let acc = List.fold_left2 + (* ppat is the pattern we are discriminating against, curpat is the current one. *) + (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) + (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) -> + match acc with + None -> None + | Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *) + if is_included curpat ppat then + (* Length of previous pattern's signature *) + let lens = List.length ppat_sign in + (* Accumulated length of previous pattern's signatures *) + let len' = lens + len in + let acc = + ((* Jump over previous prevpat signs *) + lift_rel_context len ppat_sign @ sign, + len', + succ n, (* nth pattern *) + mkApp (delayed_force coq_eq_ind, + [| lift (len' + liftsign) curpat_ty; + liftn (len + liftsign) (succ lens) ppat_c ; + lift len' curpat_c |]) :: + List.map (lift lens (* Jump over this prevpat signature *)) c) + in Some acc + else None) + (Some ([], 0, 0, [])) eqnpats pats + in match acc with + None -> c + | Some (sign, len, _, c') -> + let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_conj c')) + (lift_rel_context liftsign sign) + in + conj :: c) + [] prevpatterns + in match diffs with [] -> None + | _ -> Some (mk_coq_conj diffs) + +let subst_rel_context k ctx subst = + let (_, ctx') = + List.fold_right + (fun (n, b, t) (k, acc) -> + (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc)) + ctx (k, []) + in ctx' + +let lift_rel_contextn n k sign = + let rec liftrec k = function + | (na,c,t)::sign -> + (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) + | [] -> [] + in + liftrec (rel_context_length sign + k) sign + +let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = + let i = ref 0 in + let (x, y, z) = + List.fold_left + (fun (branches, eqns, prevpatterns) eqn -> + let _, newpatterns, pats = + List.fold_left2 + (fun (idents, newpatterns, pats) pat arsign -> + let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in + (idents, pat' :: newpatterns, cpat :: pats)) + ([], [], []) eqn.patterns sign + in + let newpatterns = List.rev newpatterns and opats = List.rev pats in + let rhs_rels, pats, signlen = + List.fold_left + (fun (renv, pats, n) (sign,c, (s, args), p) -> + (* Recombine signatures and terms of all of the row's patterns *) + let sign' = lift_rel_context n sign in + let len = List.length sign' in + (sign' @ renv, + (* lift to get outside of previous pattern's signatures. *) + (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats, + len + n)) + ([], [], 0) opats in + let pats, _ = List.fold_left + (* lift to get outside of past patterns to get terms in the combined environment. *) + (fun (pats, n) (sign, c, (s, args), p) -> + let len = List.length sign in + ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n)) + ([], 0) pats + in + let ineqs = build_ineqs prevpatterns pats signlen in + let rhs_rels' = rels_of_patsign rhs_rels in + let _signenv = push_rel_context rhs_rels' env in + let arity = + let args, nargs = + List.fold_right (fun (sign, c, (_, args), _) (allargs,n) -> + (args @ c :: allargs, List.length args + succ n)) + pats ([], 0) + in + let args = List.rev args in + substl args (liftn signlen (succ nargs) arity) + in + let rhs_rels', tycon = + let neqs_rels, arity = + match ineqs with + | None -> [], arity + | Some ineqs -> + [Anonymous, None, ineqs], lift 1 arity + in + let eqs_rels, arity = decompose_prod_n_assum neqs arity in + eqs_rels @ neqs_rels @ rhs_rels', arity + in + let rhs_env = push_rels rhs_rels' env in + let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in + let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' + and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in + let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in + let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in + let branch = + let bref = GVar (dummy_loc, branch_name) in + match vars_of_ctx rhs_rels with + [] -> bref + | l -> GApp (dummy_loc, bref, l) + in + let branch = match ineqs with + Some _ -> GApp (dummy_loc, branch, [ hole ]) + | None -> branch + in + incr i; + let rhs = { eqn.rhs with it = Some branch } in + (branch_decl :: branches, + { eqn with patterns = newpatterns; rhs = rhs } :: eqns, + opats :: prevpatterns)) + ([], [], []) eqns + in x, y + +(* Builds the predicate. If the predicate is dependent, its context is + * made of 1+nrealargs assumptions for each matched term in an inductive + * type and 1 assumption for each term not _syntactically_ in an + * inductive type. + + * Each matched terms are independently considered dependent or not. + + * A type constraint but no annotation case: it is assumed non dependent. + *) + +let lift_ctx n ctx = + let ctx', _ = + List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0) + in ctx' + +(* Turn matched terms into variables. *) +let abstract_tomatch env tomatchs tycon = + let prev, ctx, names, tycon = + List.fold_left + (fun (prev, ctx, names, tycon) (c, t) -> + let lenctx = List.length ctx in + match kind_of_term c with + Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon + | _ -> + let tycon = Option.map + (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in + let name = next_ident_away (id_of_string "filtered_var") names in + (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, + (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, + name :: names, tycon) + ([], [], [], tycon) tomatchs + in List.rev prev, ctx, tycon + +let is_dependent_ind = function + IsInd (_, IndType (indf, args), _) when List.length args > 0 -> true + | _ -> false + +let build_dependent_signature env evars avoid tomatchs arsign = + let avoid = ref avoid in + let arsign = List.rev arsign in + let allnames = List.rev (List.map (List.map pi1) arsign) in + let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in + let eqs, neqs, refls, slift, arsign' = + List.fold_left2 + (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign -> + (* The accumulator: + previous eqs, + number of previous eqs, + lift to get outside eqs and in the introduced variables ('as' and 'in'), + new arity signatures + *) + match ty with + IsInd (ty, IndType (indf, args), _) when List.length args > 0 -> + (* Build the arity signature following the names in matched terms as much as possible *) + let argsign = List.tl arsign in (* arguments in inverse application order *) + let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *) + let argsign = List.rev argsign in (* arguments in application order *) + let env', nargeqs, argeqs, refl_args, slift, argsign' = + List.fold_left2 + (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) -> + let argt = Retyping.get_type_of env evars arg in + let eq, refl_arg = + if Reductionops.is_conv env evars argt t then + (mk_eq (lift (nargeqs + slift) argt) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) arg), + mk_eq_refl argt arg) + else + (mk_JMeq (lift (nargeqs + slift) t) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) argt) + (lift (nargeqs + nar) arg), + mk_JMeq_refl argt arg) + in + let previd, id = + let name = + match kind_of_term arg with + Rel n -> pi1 (lookup_rel n env) + | _ -> name + in + make_prime avoid name + in + (env, succ nargeqs, + (Name (eq_id avoid previd), None, eq) :: argeqs, + refl_arg :: refl_args, + pred slift, + (Name id, b, t) :: argsign')) + (env, neqs, [], [], slift, []) args argsign + in + let eq = mk_JMeq + (lift (nargeqs + slift) appt) + (mkRel (nargeqs + slift)) + (lift (nargeqs + nar) ty) + (lift (nargeqs + nar) tm) + in + let refl_eq = mk_JMeq_refl ty tm in + let previd, id = make_prime avoid appn in + (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs, + succ nargeqs, + refl_eq :: refl_args, + pred slift, + (((Name id, appb, appt) :: argsign') :: arsigns)) + + | _ -> + (* Non dependent inductive or not inductive, just use a regular equality *) + let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in + let previd, id = make_prime avoid name in + let arsign' = (Name id, b, typ) in + let tomatch_ty = type_of_tomatch ty in + let eq = + mk_eq (lift nar tomatch_ty) + (mkRel slift) (lift nar tm) + in + ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs, + (mk_eq_refl tomatch_ty tm) :: refl_args, + pred slift, (arsign' :: []) :: arsigns)) + ([], 0, [], nar, []) tomatchs arsign + in + let arsign'' = List.rev arsign' in + assert(slift = 0); (* we must have folded over all elements of the arity signature *) + arsign'', allnames, nar, eqs, neqs, refls + +let context_of_arsign l = + let (x, _) = List.fold_right + (fun c (x, n) -> + (lift_rel_context n c @ x, List.length c + n)) + l ([], 0) + in x + +let compile_program_cases loc style (typing_function, evdref) tycon env (predopt, tomatchl, eqns) = + let typing_fun tycon env = function + | Some t -> typing_function tycon env evdref t + | None -> coq_unit_judge () in + + (* We build the matrix of patterns and right-hand side *) + let matx = matx_of_eqns env eqns in + + (* We build the vector of terms to match consistently with the *) + (* constructors found in patterns *) + let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in + let tycon = valcon_of_tycon tycon in + let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env tomatchs tycon in + let env = push_rel_context tomatchs_lets env in + let len = List.length eqns in + let sign, allnames, signlen, eqs, neqs, args = + (* The arity signature *) + let arsign = extract_arity_signature ~dolift:false env tomatchs tomatchl in + (* Build the dependent arity signature, the equalities which makes + the first part of the predicate and their instantiations. *) + let avoid = [] in + build_dependent_signature env ( !evdref) avoid tomatchs arsign + + in + let tycon, arity = + match tycon' with + | None -> let ev = mkExistential env evdref in ev, ev + | Some t -> + let pred = + try + let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in + (* The tycon may be ill-typed after abstraction. *) + let env' = push_rel_context (context_of_arsign sign) env in + ignore(Typing.sort_of env' !evdref pred); pred + with _ -> + let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in + lift nar t + in Option.get tycon, pred + in + let neqs, arity = + let ctx = context_of_arsign eqs in + let neqs = List.length ctx in + neqs, it_mkProd_or_LetIn (lift neqs arity) ctx + in + let lets, matx = + (* Type the rhs under the assumption of equations *) + constrs_of_pats typing_fun env evdref matx tomatchs sign neqs arity + in + let matx = List.rev matx in + let _ = assert(len = List.length lets) in + let env = push_rels lets env in + let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in + let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in + let args = List.rev_map (lift len) args in + let pred = liftn len (succ signlen) arity in + let nal, pred = build_initial_predicate sign pred in + + (* We push the initial terms to match and push their alias to rhs' envs *) + (* names of aliases will be recovered from patterns (hence Anonymous here) *) + let initial_pushed = List.map (fun tm -> Pushed (tm,[],Anonymous)) tomatchs in + + let typing_function tycon env evdref = function + | Some t -> typing_function tycon env evdref t + | None -> coq_unit_judge () in + + let pb = + { env = env; + evdref = evdref; + pred = pred; + tomatch = initial_pushed; + history = start_history (List.length initial_pushed); + mat = matx; + caseloc = loc; + casestyle= style; + typing_function = typing_function } in + + let j = compile pb in + (* We check for unused patterns *) + List.iter (check_unused_pattern env) matx; + let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in + let j = + { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; + uj_type = nf_evar !evdref tycon; } + in j +end + (**************************************************************************) (* Main entry of the matching compilation *) let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = - + if predopt = None && Flags.is_program_mode () then + ProgramCases.compile_program_cases loc style (typing_fun, evdref) + tycon env (predopt, tomatchl, eqns) + else + (* We build the matrix of patterns and right-hand side *) let matx = matx_of_eqns env eqns in @@ -1798,6 +2296,8 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* constructors found in patterns *) let tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in + + (* If an elimination predicate is provided, we check it is compatible with the type of arguments to match; if none is provided, we build alternative possible predicates *) @@ -1861,4 +2361,3 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* We coerce to the tycon (if an elim predicate was provided) *) inh_conv_coerce_to_tycon loc env evdref j tycon -end diff --git a/pretyping/cases.mli b/pretyping/cases.mli index fcfee055c..39677f38b 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -48,13 +48,10 @@ val error_needs_inversion : env -> constr -> types -> 'a (** {6 Compilation primitive. } *) -module type S = sig - val compile_cases : - loc -> case_style -> - (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> - type_constraint -> - env -> glob_constr option * tomatch_tuples * cases_clauses -> - unsafe_judgment -end - -module Cases_F(C : Coercion.S) : S +val compile_cases : + loc -> case_style -> + (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> + type_constraint -> + env -> glob_constr option * tomatch_tuples * cases_clauses -> + unsafe_judgment + diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index eb014af46..2b93a5fca 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -31,219 +31,456 @@ open Retyping open Evd open Termops -module type S = sig - (*s Coercions. *) - - (* [inh_app_fun env evd j] coerces [j] to a function; i.e. it - inserts a coercion into [j], if needed, in such a way it gets as - type a product; it returns [j] if no coercion is applicable *) - val inh_app_fun : - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment - - (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it - inserts a coercion into [j], if needed, in such a way it gets as - type a sort; it fails if no coercion is applicable *) - val inh_coerce_to_sort : loc -> - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment - - (* [inh_coerce_to_base env evd j] coerces [j] to its base type; i.e. it - inserts a coercion into [j], if needed, in such a way it gets as - type its base type (the notion depends on the coercion system) *) - val inh_coerce_to_base : loc -> - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment - - (* [inh_coerce_to_prod env evars t] coerces [t] to a product type *) - val inh_coerce_to_prod : loc -> - env -> evar_map -> types -> evar_map * types - - (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type - [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and - [j.uj_type] are convertible; it fails if no coercion is applicable *) - val inh_conv_coerce_to : loc -> - env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment - - val inh_conv_coerce_rigid_to : loc -> - env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment - - (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] - is coercible to an object of type [t'] adding evar constraints if needed; - it fails if no coercion exists *) - val inh_conv_coerces_to : loc -> - env -> evar_map -> types -> types -> evar_map - - (* [inh_pattern_coerce_to loc env evd pat ind1 ind2] coerces the Cases - pattern [pat] typed in [ind1] into a pattern typed in [ind2]; - raises [Not_found] if no coercion found *) - val inh_pattern_coerce_to : - loc -> Glob_term.cases_pattern -> inductive -> inductive -> Glob_term.cases_pattern -end - -module Default = struct - (* Typing operations dealing with coercions *) - exception NoCoercion - - (* Here, funj is a coercion therefore already typed in global context *) - let apply_coercion_args env argl funj = - let rec apply_rec acc typ = function - | [] -> { uj_val = applist (j_val funj,argl); - uj_type = typ } - | h::restl -> - (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *) - match kind_of_term (whd_betadeltaiota env Evd.empty typ) with - | Prod (_,c1,c2) -> - (* Typage garanti par l'appel à app_coercion*) - apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly "apply_coercion_args" +(* Typing operations dealing with coercions *) +exception NoCoercion + +(* Here, funj is a coercion therefore already typed in global context *) +let apply_coercion_args env argl funj = + let rec apply_rec acc typ = function + | [] -> { uj_val = applist (j_val funj,argl); + uj_type = typ } + | h::restl -> + (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *) + match kind_of_term (whd_betadeltaiota env Evd.empty typ) with + | Prod (_,c1,c2) -> + (* Typage garanti par l'appel à app_coercion*) + apply_rec (h::acc) (subst1 h c2) restl + | _ -> anomaly "apply_coercion_args" + in + apply_rec [] funj.uj_type argl + +(* appliquer le chemin de coercions de patterns p *) +let apply_pattern_coercion loc pat p = + List.fold_left + (fun pat (co,n) -> + let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in + Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) + pat p + +(* raise Not_found if no coercion found *) +let inh_pattern_coerce_to loc pat ind1 ind2 = + let p = lookup_pattern_path_between (ind1,ind2) in + apply_pattern_coercion loc pat p + +(* Program coercions *) + +open Program + +let make_existential loc ?(opaque = Define true) env isevars c = + Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c + +let app_opt env evars f t = + whd_betaiota !evars (app_opt f t) + +let pair_of_array a = (a.(0), a.(1)) +let make_name s = Name (id_of_string s) + +let rec disc_subset x = + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Ind i -> + let len = Array.length l in + let sigty = delayed_force sig_typ in + if len = 2 && i = Term.destInd sigty + then + let (a, b) = pair_of_array l in + Some (a, b) + else None + | _ -> None) + | _ -> None + +exception NoSubtacCoercion + +let hnf env isevars c = whd_betadeltaiota env isevars c +let hnf_nodelta env evars c = whd_betaiota evars c + +let lift_args n sign = + let rec liftrec k = function + | t::sign -> liftn n k t :: (liftrec (k-1) sign) + | [] -> [] + in + liftrec (List.length sign) sign + +let rec mu env isevars t = + let rec aux v = + let v = hnf env !isevars v in + match disc_subset v with + Some (u, p) -> + let f, ct = aux u in + let p = hnf env !isevars p in + (Some (fun x -> + app_opt env isevars + f (mkApp (delayed_force sig_proj1, + [| u; p; x |]))), + ct) + | None -> (None, v) + in aux t + +and coerce loc env isevars (x : Term.constr) (y : Term.constr) + : (Term.constr -> Term.constr) option + = + let rec coerce_unify env x y = + let x = hnf env !isevars x and y = hnf env !isevars y in + try + isevars := the_conv_x_leq env x y !isevars; + None + with Reduction.NotConvertible -> coerce' env x y + and coerce' env x y : (Term.constr -> Term.constr) option = + let subco () = subset_coerce env isevars x y in + let dest_prod c = + match Reductionops.splay_prod_n env ( !isevars) 1 c with + | [(na,b,t)], c -> (na,t), c + | _ -> raise NoSubtacCoercion in - apply_rec [] funj.uj_type argl - - (* appliquer le chemin de coercions de patterns p *) - let apply_pattern_coercion loc pat p = - List.fold_left - (fun pat (co,n) -> - let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in - Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) - pat p - - (* raise Not_found if no coercion found *) - let inh_pattern_coerce_to loc pat ind1 ind2 = - let p = lookup_pattern_path_between (ind1,ind2) in - apply_pattern_coercion loc pat p - - let saturate_evd env evd = - Typeclasses.resolve_typeclasses - ~onlyargs:true ~split:true ~fail:false env evd - - (* appliquer le chemin de coercions p à hj *) - let apply_coercion env sigma p hj typ_cl = - try - fst (List.fold_left - (fun (ja,typ_cl) i -> - let fv,isid = coercion_value i in - let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in - let jres = apply_coercion_args env argl fv in - (if isid then - { uj_val = ja.uj_val; uj_type = jres.uj_type } - else - jres), - jres.uj_type) - (hj,typ_cl) p) - with _ -> anomaly "apply_coercion" - - let inh_app_fun env evd j = - let t = whd_betadeltaiota env evd j.uj_type in - match kind_of_term t with - | Prod (_,_,_) -> (evd,j) - | Evar ev -> - let (evd',t) = define_evar_as_product evd ev in - (evd',{ uj_val = j.uj_val; uj_type = t }) - | _ -> - let t,p = - lookup_path_to_fun_from env evd j.uj_type in - (evd,apply_coercion env evd p j t) - - let inh_app_fun env evd j = - try inh_app_fun env evd j - with Not_found -> - try inh_app_fun env (saturate_evd env evd) j - with Not_found -> (evd, j) - - let inh_tosort_force loc env evd j = - try - let t,p = lookup_path_to_sort_from env evd j.uj_type in - let j1 = apply_coercion env evd p j t in - let j2 = on_judgment_type (whd_evar evd) j1 in - (evd,type_judgment env j2) - with Not_found -> - error_not_a_type_loc loc env evd j - - let inh_coerce_to_sort loc env evd j = - let typ = whd_betadeltaiota env evd j.uj_type in - match kind_of_term typ with - | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) - | Evar ev when not (is_defined_evar evd ev) -> - let (evd',s) = define_evar_as_sort evd ev in - (evd',{ utj_val = j.uj_val; utj_type = s }) - | _ -> - inh_tosort_force loc env evd j - - let inh_coerce_to_base loc env evd j = (evd, j) - let inh_coerce_to_prod loc env evd t = (evd, t) - - let inh_coerce_to_fail env evd rigidonly v t c1 = - if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) - then - raise NoCoercion - else + let rec coerce_application typ typ' c c' l l' = + let len = Array.length l in + let rec aux tele typ typ' i co = + if i < len then + let hdx = l.(i) and hdy = l'.(i) in + try isevars := the_conv_x_leq env hdx hdy !isevars; + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in + aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co + with Reduction.NotConvertible -> + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in + let _ = + try isevars := the_conv_x_leq env eqT eqT' !isevars + with Reduction.NotConvertible -> raise NoSubtacCoercion + in + (* Disallow equalities on arities *) + if Reduction.is_arity env eqT then raise NoSubtacCoercion; + let restargs = lift_args 1 + (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) + in + let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in + let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in + let eq = mkApp (delayed_force coq_eq_ind, [| eqT; hdx; hdy |]) in + let evar = make_existential loc env isevars eq in + let eq_app x = mkApp (delayed_force coq_eq_rect, + [| eqT; hdx; pred; x; hdy; evar|]) in + aux (hdy :: tele) (subst1 hdx restT) + (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) + else Some co + in + if isEvar c || isEvar c' then + (* Second-order unification needed. *) + raise NoSubtacCoercion; + aux [] typ typ' 0 (fun x -> x) + in + match (kind_of_term x, kind_of_term y) with + | Sort s, Sort s' -> + (match s, s' with + Prop x, Prop y when x = y -> None + | Prop _, Type _ -> None + | Type x, Type y when x = y -> None (* false *) + | _ -> subco ()) + | Prod (name, a, b), Prod (name', a', b') -> + let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in + let env' = push_rel (name', None, a') env in + let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in + (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) + let coec1 = app_opt env' isevars c1 (mkRel 1) in + (* env, x : a' |- c1[x] : lift 1 a *) + let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in + (* env, x : a' |- c2 : b[c1[x]/x]] > b' *) + (match c1, c2 with + | None, None -> None + | _, _ -> + Some + (fun f -> + mkLambda (name', a', + app_opt env' isevars c2 + (mkApp (Term.lift 1 f, [| coec1 |]))))) + + | App (c, l), App (c', l') -> + (match kind_of_term c, kind_of_term c' with + Ind i, Ind i' -> (* Inductive types *) + let len = Array.length l in + let sigT = delayed_force sigT_typ in + let prod = delayed_force prod_typ in + (* Sigma types *) + if len = Array.length l' && len = 2 && i = i' + && (i = Term.destInd sigT || i = Term.destInd prod) + then + if i = Term.destInd sigT + then + begin + let (a, pb), (a', pb') = + pair_of_array l, pair_of_array l' + in + let c1 = coerce_unify env a a' in + let rec remove_head a c = + match kind_of_term c with + | Lambda (n, t, t') -> c, t' + (*| Prod (n, t, t') -> t'*) + | Evar (k, args) -> + let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in + isevars := evs; + let (n, dom, rng) = destLambda t in + let (domk, args) = destEvar dom in + isevars := define domk a !isevars; + t, rng + | _ -> raise NoSubtacCoercion + in + let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in + let env' = push_rel (make_name "x", None, a) env in + let c2 = coerce_unify env' b b' in + match c1, c2 with + None, None -> + None + | _, _ -> + Some + (fun x -> + let x, y = + app_opt env' isevars c1 (mkApp (delayed_force sigT_proj1, + [| a; pb; x |])), + app_opt env' isevars c2 (mkApp (delayed_force sigT_proj2, + [| a; pb; x |])) + in + mkApp (delayed_force sigT_intro, [| a'; pb'; x ; y |])) + end + else + begin + let (a, b), (a', b') = + pair_of_array l, pair_of_array l' + in + let c1 = coerce_unify env a a' in + let c2 = coerce_unify env b b' in + match c1, c2 with + None, None -> None + | _, _ -> + Some + (fun x -> + let x, y = + app_opt env isevars c1 (mkApp (delayed_force prod_proj1, + [| a; b; x |])), + app_opt env isevars c2 (mkApp (delayed_force prod_proj2, + [| a; b; x |])) + in + mkApp (delayed_force prod_intro, [| a'; b'; x ; y |])) + end + else + if i = i' && len = Array.length l' then + let evm = !isevars in + (try subco () + with NoSubtacCoercion -> + let typ = Typing.type_of env evm c in + let typ' = Typing.type_of env evm c' in + (* if not (is_arity env evm typ) then *) + coerce_application typ typ' c c' l l') + (* else subco () *) + else + subco () + | x, y when x = y -> + if Array.length l = Array.length l' then + let evm = !isevars in + let lam_type = Typing.type_of env evm c in + let lam_type' = Typing.type_of env evm c' in + (* if not (is_arity env evm lam_type) then ( *) + coerce_application lam_type lam_type' c c' l l' + (* ) else subco () *) + else subco () + | _ -> subco ()) + | _, _ -> subco () + + and subset_coerce env isevars x y = + match disc_subset x with + Some (u, p) -> + let c = coerce_unify env u y in + let f x = + app_opt env isevars c (mkApp (delayed_force sig_proj1, + [| u; p; x |])) + in Some f + | None -> + match disc_subset y with + Some (u, p) -> + let c = coerce_unify env x u in + Some + (fun x -> + let cx = app_opt env isevars c x in + let evar = make_existential loc env isevars (mkApp (p, [| cx |])) + in + (mkApp + (delayed_force sig_intro, + [| u; p; cx; evar |]))) + | None -> + raise NoSubtacCoercion + (*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars; + None*) + in coerce_unify env x y + +let coerce_itf loc env isevars v t c1 = + let evars = ref isevars in + let coercion = coerce loc env evars t c1 in + let t = Option.map (app_opt env evars coercion) v in + !evars, t + + + +let saturate_evd env evd = + Typeclasses.resolve_typeclasses + ~onlyargs:true ~split:true ~fail:false env evd + +(* appliquer le chemin de coercions p à hj *) +let apply_coercion env sigma p hj typ_cl = + try + fst (List.fold_left + (fun (ja,typ_cl) i -> + let fv,isid = coercion_value i in + let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in + let jres = apply_coercion_args env argl fv in + (if isid then + { uj_val = ja.uj_val; uj_type = jres.uj_type } + else + jres), + jres.uj_type) + (hj,typ_cl) p) + with _ -> anomaly "apply_coercion" + +let inh_app_fun env evd j = + let t = whd_betadeltaiota env evd j.uj_type in + match kind_of_term t with + | Prod (_,_,_) -> (evd,j) + | Evar ev -> + let (evd',t) = define_evar_as_product evd ev in + (evd',{ uj_val = j.uj_val; uj_type = t }) + | _ -> + try let t,p = + lookup_path_to_fun_from env evd j.uj_type in + (evd,apply_coercion env evd p j t) + with Not_found when Flags.is_program_mode () -> + try + let isevars = ref evd in + let coercef, t = mu env isevars t in + let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in + (!isevars, res) + with NoSubtacCoercion | NoCoercion -> + (evd,j) + +let inh_app_fun env evd j = + try inh_app_fun env evd j + with Not_found -> + try inh_app_fun env (saturate_evd env evd) j + with Not_found -> (evd, j) + +let inh_tosort_force loc env evd j = + try + let t,p = lookup_path_to_sort_from env evd j.uj_type in + let j1 = apply_coercion env evd p j t in + let j2 = on_judgment_type (whd_evar evd) j1 in + (evd,type_judgment env j2) + with Not_found -> + error_not_a_type_loc loc env evd j + +let inh_coerce_to_sort loc env evd j = + let typ = whd_betadeltaiota env evd j.uj_type in + match kind_of_term typ with + | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) + | Evar ev when not (is_defined_evar evd ev) -> + let (evd',s) = define_evar_as_sort evd ev in + (evd',{ utj_val = j.uj_val; utj_type = s }) + | _ -> + inh_tosort_force loc env evd j + +let inh_coerce_to_base loc env evd j = + if Flags.is_program_mode () then + let isevars = ref evd in + let typ = hnf env !isevars j.uj_type in + let ct, typ' = mu env isevars typ in + let res = + { uj_val = app_opt env isevars ct j.uj_val; + uj_type = typ' } + in !isevars, res + else (evd, j) + +let inh_coerce_to_prod loc env evd t = + if Flags.is_program_mode () then + let isevars = ref evd in + let typ = hnf env !isevars t in + let _, typ' = mu env isevars typ in + !isevars, typ' + else (evd, t) + +let inh_coerce_to_fail env evd rigidonly v t c1 = + if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) + then + raise NoCoercion + else let v', t' = try let t2,t1,p = lookup_path_between env evd (t,c1) in match v with - Some v -> - let j = - apply_coercion env evd p - {uj_val = v; uj_type = t} t2 in - Some j.uj_val, j.uj_type - | None -> None, t + Some v -> + let j = + apply_coercion env evd p + {uj_val = v; uj_type = t} t2 in + Some j.uj_val, j.uj_type + | None -> None, t with Not_found -> raise NoCoercion in try (the_conv_x_leq env t' c1 evd, v') with Reduction.NotConvertible -> raise NoCoercion - let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = - try (the_conv_x_leq env t c1 evd, v) - with Reduction.NotConvertible -> +let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = + try (the_conv_x_leq env t c1 evd, v) + with Reduction.NotConvertible -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> - match + match kind_of_term (whd_betadeltaiota env evd t), kind_of_term (whd_betadeltaiota env evd c1) - with - | Prod (name,t1,t2), Prod (_,u1,u2) -> - (* Conversion did not work, we may succeed with a coercion. *) - (* We eta-expand (hence possibly modifying the original term!) *) - (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) - (* has type forall (x:u1), u2 (with v' recursively obtained) *) - (* Note: we retype the term because sort-polymorphism may have *) - (* weaken its type *) - let name = match name with - | Anonymous -> Name (id_of_string "x") - | _ -> name in - let env1 = push_rel (name,None,u1) env in - let (evd', v1) = - inh_conv_coerce_to_fail loc env1 evd rigidonly - (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in - let v1 = Option.get v1 in - let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in - let t2 = match v2 with - | None -> subst_term v1 t2 - | Some v2 -> Retyping.get_type_of env1 evd' v2 in - let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in - (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') - | _ -> raise NoCoercion - - (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to_gen rigidonly loc env evd cj t = - let (evd', val') = - try - inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercion -> - let evd = saturate_evd env evd in - try - inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercion -> - error_actual_type_loc loc env evd cj t - in - let val' = match val' with Some v -> v | None -> assert(false) in - (evd',{ uj_val = val'; uj_type = t }) - - let inh_conv_coerce_to = inh_conv_coerce_to_gen false - let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + with + | Prod (name,t1,t2), Prod (_,u1,u2) -> + (* Conversion did not work, we may succeed with a coercion. *) + (* We eta-expand (hence possibly modifying the original term!) *) + (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) + (* has type forall (x:u1), u2 (with v' recursively obtained) *) + (* Note: we retype the term because sort-polymorphism may have *) + (* weaken its type *) + let name = match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name in + let env1 = push_rel (name,None,u1) env in + let (evd', v1) = + inh_conv_coerce_to_fail loc env1 evd rigidonly + (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in + let v1 = Option.get v1 in + let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in + let t2 = match v2 with + | None -> subst_term v1 t2 + | Some v2 -> Retyping.get_type_of env1 evd' v2 in + let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') + | _ -> raise NoCoercion - let inh_conv_coerces_to loc env evd t t' = +(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) +let inh_conv_coerce_to_gen rigidonly loc env evd cj t = + let (evd', val') = try - fst (inh_conv_coerce_to_fail loc env evd true None t t') + inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercion -> - evd (* Maybe not enough information to unify *) - -end + let evd = saturate_evd env evd in + try + inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t + with NoCoercion -> + (if Flags.is_program_mode () then + try + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + with NoSubtacCoercion -> + error_actual_type_loc loc env evd cj t + else error_actual_type_loc loc env evd cj t) + in + let val' = match val' with Some v -> v | None -> assert(false) in + (evd',{ uj_val = val'; uj_type = t }) + +let inh_conv_coerce_to = inh_conv_coerce_to_gen false +let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + +let inh_conv_coerces_to loc env evd t t' = + try + fst (inh_conv_coerce_to_fail loc env evd true None t t') + with NoCoercion -> + evd (* Maybe not enough information to unify *) + diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 91cb693ab..45566e9fb 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -16,51 +16,47 @@ open Environ open Evarutil open Glob_term -module type S = sig - (** {6 Coercions. } *) - - (** [inh_app_fun env isevars j] coerces [j] to a function; i.e. it - inserts a coercion into [j], if needed, in such a way it gets as - type a product; it returns [j] if no coercion is applicable *) - val inh_app_fun : - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment - - (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it - inserts a coercion into [j], if needed, in such a way it gets as - type a sort; it fails if no coercion is applicable *) - val inh_coerce_to_sort : loc -> - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment - - (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it - inserts a coercion into [j], if needed, in such a way it gets as - type its base type (the notion depends on the coercion system) *) - val inh_coerce_to_base : loc -> - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment - - (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) - val inh_coerce_to_prod : loc -> - env -> evar_map -> types -> evar_map * types - - (** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type - [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and - [j.uj_type] are convertible; it fails if no coercion is applicable *) - val inh_conv_coerce_to : loc -> - env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment - - val inh_conv_coerce_rigid_to : loc -> - env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment - - (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] - is coercible to an object of type [t'] adding evar constraints if needed; - it fails if no coercion exists *) - val inh_conv_coerces_to : loc -> - env -> evar_map -> types -> types -> evar_map - - (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases - pattern [pat] typed in [ind1] into a pattern typed in [ind2]; - raises [Not_found] if no coercion found *) - val inh_pattern_coerce_to : - loc -> cases_pattern -> inductive -> inductive -> cases_pattern -end - -module Default : S +(** {6 Coercions. } *) + +(** [inh_app_fun env isevars j] coerces [j] to a function; i.e. it + inserts a coercion into [j], if needed, in such a way it gets as + type a product; it returns [j] if no coercion is applicable *) +val inh_app_fun : + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + +(** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it + inserts a coercion into [j], if needed, in such a way it gets as + type a sort; it fails if no coercion is applicable *) +val inh_coerce_to_sort : loc -> + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment + +(** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it + inserts a coercion into [j], if needed, in such a way it gets as + type its base type (the notion depends on the coercion system) *) +val inh_coerce_to_base : loc -> + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + +(** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) +val inh_coerce_to_prod : loc -> + env -> evar_map -> types -> evar_map * types + +(** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type + [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and + [j.uj_type] are convertible; it fails if no coercion is applicable *) +val inh_conv_coerce_to : loc -> + env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment + +val inh_conv_coerce_rigid_to : loc -> + env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment + +(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] + is coercible to an object of type [t'] adding evar constraints if needed; + it fails if no coercion exists *) +val inh_conv_coerces_to : loc -> + env -> evar_map -> types -> types -> evar_map + +(** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases + pattern [pat] typed in [ind1] into a pattern typed in [ind2]; + raises [Not_found] if no coercion found *) +val inh_pattern_coerce_to : + loc -> cases_pattern -> inductive -> inductive -> cases_pattern diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4f286efe7..e75dfcca8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -105,8 +105,10 @@ let interp_elimination_sort = function 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); + (evdref := Typeclasses.resolve_typeclasses ~onlyargs:true + ~split:true ~fail:true env !evdref; + 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 @@ -136,277 +138,198 @@ let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) = (* Side-effect *) !evdref,c -module type S = -sig - - module Cases : Cases.S - - (* 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 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 -> glob_constr -> open_constr - - val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_map ref -> env -> typing_constraint -> glob_constr -> constr - - (* More general entry point with evars from ltac *) - - (* 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], - - expand_evars : expand inferred evars by their value if any - sigma : initial set of existential variables (typically dependent subgoals) - ltac_env : partial substitution of variables (used for the tactic language) - constraint : tell if interpreted as a possibly constrained term or a type - *) - - val understand_ltac : - bool -> evar_map -> env -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr - - (* Standard call to get a constr from a glob_constr, resolving implicit args *) - - val understand : evar_map -> env -> ?expected_type:Term.types -> - glob_constr -> constr - - (* Idem but the glob_constr is intended to be a type *) - - val understand_type : evar_map -> env -> glob_constr -> constr - - (* A generalization of the two previous case *) - - val understand_gen : typing_constraint -> evar_map -> env -> - glob_constr -> constr - - (* Idem but returns the judgment of the understood term *) - - 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 -> glob_constr -> unsafe_judgment - - (*i*) - (* Internal of Pretyping... - * Unused outside, but useful for debugging - *) - val pretype : - type_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_judgment - - val pretype_type : - val_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_type_judgment - - val pretype_gen : - bool -> bool -> bool -> evar_map ref -> env -> - ltac_var_map -> typing_constraint -> glob_constr -> constr - - (*i*) -end - -module Pretyping_F (Coercion : Coercion.S) = struct - - module Cases = Cases.Cases_F(Coercion) - - (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) - let allow_anonymous_refs = ref false - - let program_mode = 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 - - let evd_comb3 f evdref x y z = - let (evd',t) = f !evdref x y z in - evdref := evd'; - t - - let mt_evd = Evd.empty - - (* Utilisé pour inférer le prédicat des Cases *) - (* Semble exagérement fort *) - (* Faudra préférer une unification entre les types de toutes les clauses *) - (* et autoriser des ? à rester dans le résultat de l'unification *) - - let evar_type_fixpoint loc env evdref lna lar vdefj = - let lt = Array.length vdefj in - if Array.length lar = lt then - for i = 0 to lt-1 do - if not (e_cumul env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env !evdref - i lna vdefj lar - done - - (* coerce to tycon if any *) - let inh_conv_coerce_to_tycon loc env evdref j = function - | None -> j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t - - (* used to enforce a name in Lambda when the type constraints itself - is named, hence possibly dependent *) - - let orelse_name name name' = match name with - | Anonymous -> name' - | _ -> name - - let invert_ltac_bound_name env id0 id = - try mkRel (pi1 (lookup_rel_id id (rel_context env))) - with Not_found -> - errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++ - str " depends on pattern variable name " ++ pr_id id ++ - str " which is not bound in current context.") - - let protected_get_type_of env sigma c = - try Retyping.get_type_of env sigma c - with Anomaly _ -> - 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 +(* 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 + +let evd_comb3 f evdref x y z = + let (evd',t) = f !evdref x y z in + evdref := evd'; + t + +let mt_evd = Evd.empty + +(* Utilisé pour inférer le prédicat des Cases *) +(* Semble exagérement fort *) +(* Faudra préférer une unification entre les types de toutes les clauses *) +(* et autoriser des ? à rester dans le résultat de l'unification *) + +let evar_type_fixpoint loc env evdref lna lar vdefj = + let lt = Array.length vdefj in + if Array.length lar = lt then + for i = 0 to lt-1 do + if not (e_cumul env evdref (vdefj.(i)).uj_type + (lift lt lar.(i))) then + error_ill_typed_rec_body_loc loc env !evdref + i lna vdefj lar + done + +(* coerce to tycon if any *) +let inh_conv_coerce_to_tycon loc env evdref j = function + | None -> j + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t + +let push_rels vars env = List.fold_right push_rel vars env + +(* used to enforce a name in Lambda when the type constraints itself + is named, hence possibly dependent *) + +let orelse_name name name' = match name with + | Anonymous -> name' + | _ -> name + +let invert_ltac_bound_name env id0 id = + try mkRel (pi1 (lookup_rel_id id (rel_context env))) + with Not_found -> + errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++ + str " depends on pattern variable name " ++ pr_id id ++ + str " which is not bound in current context.") + +let protected_get_type_of env sigma c = + try Retyping.get_type_of env sigma c + with Anomaly _ -> + 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 +>>>>>>> Second step of integration of Program: { uj_val = mkRel n; uj_type = lift n typ } - with Not_found -> + 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 -> - (* [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 + { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> - (* [id] not found, standard error message *) - error_var_not_found_loc loc id - - let evar_kind_of_term sigma c = - kind_of_term (whd_evar sigma c) - - (*************************************************************************) - (* Main pretyping function *) - - let pretype_ref evdref env ref = - let c = constr_of_global ref in - make_judge c (Retyping.get_type_of env Evd.empty c) - - 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 - | GRef (loc,ref) -> - inh_conv_coerce_to_tycon loc env evdref - (pretype_ref evdref env ref) - tycon - - | GVar (loc, id) -> - 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 - 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 - let args = match instopt with - | None -> instance_from_named_context hyps - | Some inst -> failwith "Evar subtitutions not implemented" in - let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env !evdref c) in - 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 = MatchingVar (someta,n) in + (* 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 -> + (* [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 + +let evar_kind_of_term sigma c = + kind_of_term (whd_evar sigma c) + +(*************************************************************************) +(* Main pretyping function *) + +let pretype_ref evdref env ref = + let c = constr_of_global ref in + make_judge c (Retyping.get_type_of env Evd.empty c) + +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 + | GRef (loc,ref) -> + inh_conv_coerce_to_tycon loc env evdref + (pretype_ref evdref env ref) + tycon + + | GVar (loc, id) -> + 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 + 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 + let args = match instopt with + | None -> instance_from_named_context hyps + | Some inst -> failwith "Evar subtitutions not implemented" in + let c = mkEvar (evk, args) in + let j = (Retyping.get_judgment_of env !evdref c) in + 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 = MatchingVar (someta,n) in + { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } + + | GHole (loc,k) -> + let ty = + match tycon with + | Some ty -> ty + | None -> + new_type_evar evdref env loc in { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } - | GHole (loc,k) -> - let ty = - match tycon with - | Some ty -> ty - | None -> - new_type_evar evdref env loc in - { uj_val = e_new_evar evdref env ~src:(loc,k) ty; 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 - (* 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 + | 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 + (* 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 @@ -419,389 +342,395 @@ module Pretyping_F (Coercion : Coercion.S) = struct 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) + (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) + make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (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 - - | GSort (loc,s) -> - let j = pretype_sort evdref s 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 = - (* Bidirectional typechecking hint: - parameters of a constructor are completely determined - by a typing constraint *) - if !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 npars = 0 then [] - else - try - (* Does not treat partially applied constructors. *) - let IndType (indf, args) = find_rectype env !evdref ty in - let (ind',pars) = dest_ind_family indf in - if 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 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 - (join_loc 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 + (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 + + | GSort (loc,s) -> + let j = pretype_sort evdref s 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 = + (* 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 npars = 0 then [] + else + try + (* Does not treat partially applied constructors. *) + let IndType (indf, args) = find_rectype env !evdref ty in + let (ind',pars) = dest_ind_family indf in + if 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 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 + (join_loc 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 or has_polymorphic_type (destConst f) - -> + when isInd f or 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 + make_judge c (* use this for keeping evars: resj.uj_val *) t | _ -> resj end - | _ -> resj in + | _ -> resj in inh_conv_coerce_to_tycon loc env evdref resj tycon - | 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 - let var = (name,None,j.utj_val) in - let j' = pretype rng (push_rel var env) evdref lvar c2 in - judge_of_abstraction env (orelse_name name name') j j' - - | GProd(loc,name,bk,c1,c2) -> - let j = pretype_type empty_valcon env evdref lvar c1 in - let j' = - if name = Anonymous then - let j = pretype_type empty_valcon env evdref lvar c2 in - { j with utj_val = lift 1 j.utj_val } - else - 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 -> 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 (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 - 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 } - - | 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 Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor."); - let cs = cstrs.(0) in - if 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 Array.length cstrs <> 2 then - user_err_loc (loc,"", - str "If is only for inductive types with two constructors."); + | 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 + judge_of_abstraction env (orelse_name name name') j j' + + | GProd(loc,name,bk,c1,c2) -> + let j = pretype_type empty_valcon env evdref lvar c1 in + let j' = + if name = Anonymous then + let j = pretype_type empty_valcon env evdref lvar c2 in + { j with utj_val = lift 1 j.utj_val } + else + 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 -> 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 (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 + 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 } + + | 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 Array.length cstrs <> 1 then + user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor."); + let cs = cstrs.(0) in + if 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_rels 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 - | 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 + let nar = List.length arsgn in + (match po with + | Some p -> + let env_p = push_rels psign env in + let pj = pretype_type empty_valcon env_p evdref lvar p in + let ccl = nf_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 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_rels 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 - 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)) + | 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 - 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 + in + let env_c = push_rels 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|]) - 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) - - | 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 (k,t) -> - let tj = pretype_type empty_valcon env evdref lvar t in - let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in - let cj = match k with - | 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 - - (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type valcon env evdref lvar = function - | GHole loc -> - (match valcon with - | Some v -> - let s = - let sigma = !evdref in - let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_betadeltaiota env sigma t) with - | Sort s -> s - | Evar ev when is_Type (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort) evdref ev - | _ -> anomaly "Found a type constraint which is not a type" - in - { utj_val = v; - utj_type = s } - | None -> - let s = 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_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in - match valcon with - | None -> tj - | Some v -> - if e_cumul env evdref v tj.utj_val then tj - else - error_unexpected_type_loc - (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 - | OfType exptyp -> - let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in + 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) + + | 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 (k,t) -> + let tj = pretype_type empty_valcon env evdref lvar t in + let cj = pretype empty_tycon env evdref lvar c in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cj = match k with + | 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 + +(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) +and pretype_type valcon env evdref lvar = function + | GHole loc -> + (match valcon with + | Some v -> + let s = + let sigma = !evdref in + let t = Retyping.get_type_of env sigma v in + match kind_of_term (whd_betadeltaiota env sigma t) with + | Sort s -> s + | Evar ev when is_Type (existential_type sigma ev) -> + evd_comb1 (define_evar_as_sort) evdref ev + | _ -> anomaly "Found a type constraint which is not a type" + in + { utj_val = v; + utj_type = s } + | None -> + let s = 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_glob_constr c in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in + match valcon with + | None -> tj + | Some v -> + if e_cumul env evdref v tj.utj_val then tj + else + error_unexpected_type_loc + (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 + | OfType exptyp -> + 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 - 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 - retourne aussi le nouveau sigma... - *) - - let understand_judgment sigma env c = - let evdref = ref sigma in - let j = pretype empty_tycon env evdref ([],[]) c in - 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 - 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 sigma in - let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in + | IsType -> + (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 + retourne aussi le nouveau sigma... +*) + +let understand_judgment sigma env c = + let evdref = ref sigma in + let j = pretype empty_tycon env evdref ([],[]) c in + 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 + 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 sigma in + let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in !evdref, c - (** Entry points of the high-level type synthesis algorithm *) - - let understand_gen kind sigma env c = - snd (ise_pretype_gen true true true sigma env ([],[]) kind c) +(** Entry points of the high-level type synthesis algorithm *) - let understand sigma env ?expected_type:exptyp c = - snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c) +let understand_gen kind sigma env c = + snd (ise_pretype_gen true true true sigma env ([],[]) kind c) - let understand_type sigma env c = - snd (ise_pretype_gen true true true sigma env ([],[]) IsType c) +let understand sigma env ?expected_type:exptyp c = + snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c) - let understand_ltac expand_evar sigma env lvar kind c = - ise_pretype_gen expand_evar false false sigma env lvar kind c +let understand_type sigma env c = + snd (ise_pretype_gen true true true sigma env ([],[]) IsType c) - let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = - ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c +let understand_ltac expand_evar sigma env lvar kind c = + ise_pretype_gen expand_evar false false sigma env lvar kind c - let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c = - pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c -end +let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = + ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c -module Default : S = Pretyping_F(Coercion.Default) +let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c = + pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index cf47d194e..34bafdb23 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -23,7 +23,7 @@ open Evarutil (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : - Pp.loc -> env -> int list list -> rec_declaration -> int array + Pp.loc -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types option | IsType @@ -33,82 +33,72 @@ type ltac_var_map = var_map * unbound_ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr -module type S = -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 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. *) - module Cases : Cases.S +val understand_tcc : ?resolve_classes:bool -> + evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr - (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) - val allow_anonymous_refs : bool ref +val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> + evar_map ref -> env -> typing_constraint -> glob_constr -> constr - (** 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. *) +(** More general entry point with evars from ltac *) - val understand_tcc : ?resolve_classes:bool -> - evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr +(** Generic call to the interpreter from glob_constr to constr, failing + unresolved holes in the glob_constr cannot be instantiated. - val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_map ref -> env -> typing_constraint -> glob_constr -> constr + In [understand_ltac expand_evars sigma env ltac_env constraint c], - (** More general entry point with evars from ltac *) + expand_evars : expand inferred evars by their value if any + sigma : initial set of existential variables (typically dependent subgoals) + ltac_env : partial substitution of variables (used for the tactic language) + constraint : tell if interpreted as a possibly constrained term or a type +*) - (** Generic call to the interpreter from glob_constr to constr, failing - unresolved holes in the glob_constr cannot be instantiated. +val understand_ltac : + bool -> evar_map -> env -> ltac_var_map -> + typing_constraint -> glob_constr -> pure_open_constr - In [understand_ltac expand_evars sigma env ltac_env constraint c], +(** Standard call to get a constr from a glob_constr, resolving implicit args *) - expand_evars : expand inferred evars by their value if any - sigma : initial set of existential variables (typically dependent subgoals) - ltac_env : partial substitution of variables (used for the tactic language) - constraint : tell if interpreted as a possibly constrained term or a type - *) +val understand : evar_map -> env -> ?expected_type:Term.types -> + glob_constr -> constr - val understand_ltac : - bool -> evar_map -> env -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr +(** Idem but the glob_constr is intended to be a type *) - (** Standard call to get a constr from a glob_constr, resolving implicit args *) +val understand_type : evar_map -> env -> glob_constr -> constr - val understand : evar_map -> env -> ?expected_type:Term.types -> - glob_constr -> constr +(** A generalization of the two previous case *) - (** Idem but the glob_constr is intended to be a type *) +val understand_gen : typing_constraint -> evar_map -> env -> + glob_constr -> constr - val understand_type : evar_map -> env -> glob_constr -> constr +(** Idem but returns the judgment of the understood term *) - (** A generalization of the two previous case *) +val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment - val understand_gen : typing_constraint -> evar_map -> env -> - glob_constr -> constr +(** Idem but do not fail on unresolved evars *) +val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment - (** Idem but returns the judgment of the understood term *) +(**/**) +(** Internal of Pretyping... *) +val pretype : + type_constraint -> env -> evar_map ref -> + ltac_var_map -> glob_constr -> unsafe_judgment - val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment +val pretype_type : + val_constraint -> env -> evar_map ref -> + ltac_var_map -> glob_constr -> unsafe_type_judgment - (** Idem but do not fail on unresolved evars *) - val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment +val pretype_gen : + bool -> bool -> bool -> evar_map ref -> env -> + ltac_var_map -> typing_constraint -> glob_constr -> constr - (**/**) - (** Internal of Pretyping... *) - val pretype : - type_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_judgment - - val pretype_type : - val_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_type_judgment - - val pretype_gen : - bool -> bool -> bool -> evar_map ref -> env -> - ltac_var_map -> typing_constraint -> glob_constr -> constr - - (**/**) - -end - -module Pretyping_F (C : Coercion.S) : S -module Default : S +(**/**) (** To embed constr in glob_constr *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 9eec94146..199adf6a7 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -20,6 +20,7 @@ Tacred Typeclasses_errors Typeclasses Classops +Program Coercion Unification Detyping diff --git a/pretyping/unification.ml b/pretyping/unification.ml index be6d90a26..983b9fd61 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -23,7 +23,7 @@ open Glob_term open Evarutil open Pretype_errors open Retyping -open Coercion.Default +open Coercion open Recordops let occur_meta_or_undefined_evar evd c = diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 9d2c1c7ab..417818abf 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -26,7 +26,7 @@ open Pretype_errors open Evarutil open Unification open Mod_subst -open Coercion.Default +open Coercion (* Abbreviations *) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index c606600d7..3e6300e09 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -41,7 +41,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = error "Instantiate called on already-defined evar"; let env = Evd.evar_env evi in let sigma',typed_c = - try Pretyping.Default.understand_ltac true sigma env ltac_var + try Pretyping.understand_ltac true sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc with _ -> let loc = Glob_term.loc_of_glob_constr rawc in diff --git a/proofs/goal.ml b/proofs/goal.ml index 4d65b636c..68f49d900 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -154,7 +154,7 @@ module Refinable = struct let my_type = Retyping.get_type_of env !rdefs t in let j = Environ.make_judge t my_type in let (new_defs,j') = - Coercion.Default.inh_conv_coerce_to (Pp.dummy_loc) env !rdefs j typ + Coercion.inh_conv_coerce_to (Pp.dummy_loc) env !rdefs j typ in rdefs := new_defs; j'.Environ.uj_val @@ -219,7 +219,7 @@ module Refinable = struct (* call to [understand_tcc_evars] returns a constr with undefined evars these evars will be our new goals *) let open_constr = - Pretyping.Default.understand_tcc_evars ~resolve_classes rdefs env tycon rawc + Pretyping.understand_tcc_evars ~resolve_classes rdefs env tycon rawc in ignore(update_handle handle init_defs !rdefs); open_constr diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index f8cca076f..c4cf7b62f 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -22,7 +22,7 @@ open Glob_term let absurd c gls = let env = pf_env gls and sigma = project gls in - let _,j = Coercion.Default.inh_coerce_to_sort dummy_loc env + let _,j = Coercion.inh_coerce_to_sort dummy_loc env (Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in let c = j.Environ.utj_val in (tclTHENS diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 9c0d5db2c..66c59ec36 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -588,7 +588,7 @@ let hResolve id c occ t gl = let t_raw = Detyping.detype true env_ids env_names t in let rec resolve_hole t_hole = try - Pretyping.Default.understand sigma env t_hole + Pretyping.understand sigma env t_hole with | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) -> resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d4a7be4ec..cf93a66cf 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,7 +44,6 @@ open Printer open Inductiveops open Syntax_def open Pretyping -open Pretyping.Default open Extrawit open Pcoq open Compat diff --git a/toplevel/record.ml b/toplevel/record.ml index 0ddc59c50..5ed6c45c5 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -32,7 +32,7 @@ open Topconstr let interp_evars evdref env impls k typ = let typ' = intern_gen true ~impls !evdref env typ in let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in - imps, Pretyping.Default.understand_tcc_evars evdref env k typ' + imps, Pretyping.understand_tcc_evars evdref env k typ' let interp_fields_evars evars env impls_env nots l = List.fold_left2 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a7b4a175f..7a7246733 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1026,6 +1026,15 @@ let _ = declare_bool_option { optsync = true; optdepr = false; + optname = "use of the program extension"; + optkey = ["Program"]; + optread = (fun () -> !Flags.program_mode); + optwrite = (fun b -> Flags.program_mode:=b) } + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; optname = "use of virtual machine inside the kernel"; optkey = ["Virtual";"Machine"]; optread = (fun () -> Vconv.use_vm ()); |