aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/decl_mode/decl_interp.ml2
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml2
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml34
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/recdef.ml1
-rw-r--r--plugins/subtac/subtac.ml6
-rw-r--r--plugins/subtac/subtac_cases.ml8
-rw-r--r--plugins/subtac/subtac_cases.mli1
-rw-r--r--plugins/subtac/subtac_classes.ml10
-rw-r--r--plugins/subtac/subtac_coercion.mli2
-rw-r--r--plugins/subtac/subtac_command.ml13
-rw-r--r--plugins/subtac/subtac_pretyping.ml2
-rw-r--r--plugins/subtac/subtac_pretyping.mli2
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml625
-rw-r--r--plugins/subtac/subtac_utils.mli1
16 files changed, 35 insertions, 678 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 512269e559..21d2b125e2 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 e3a95fb4fa..c848faaa74 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 8d4b0eee1c..a955891f83 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 6a58888743..a7298095ea 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 3b3f3057b6..3ea9c3d3e7 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 c37de6e4a6..0f92378d68 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 cccb12e418..ffcd40f94b 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 279e4d87a3..3b740f1618 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 11a8115971..b7e78f6d28 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 a81243f73f..75d0f3429e 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 5678c10e69..b872c99d5f 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 e5d93ace26..6e6f42308f 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 b83057ac8b..f64c1ae2f2 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 fa767790d0..e999f1710c 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 43182765df..464bb8639f 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 719b87952a..5cbb307db3 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:26:35 +0000