aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml5
-rw-r--r--pretyping/glob_ops.ml38
-rw-r--r--pretyping/glob_ops.mli10
-rw-r--r--pretyping/pretyping.ml30
-rw-r--r--pretyping/pretyping.mli7
-rw-r--r--pretyping/typing.ml44
-rw-r--r--pretyping/univdecls.ml7
-rw-r--r--pretyping/univdecls.mli2
8 files changed, 103 insertions, 40 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 311c1c09ec..a0434f9279 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -450,11 +450,6 @@ let current_pattern eqn =
| pat::_ -> pat
| [] -> anomaly (Pp.str "Empty list of patterns.")
-let alias_of_pat = DAst.with_val (function
- | PatVar name -> name
- | PatCstr(_,_,name) -> name
- )
-
let remove_current_pattern eqn =
match eqn.patterns with
| pat::pats ->
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index a21137a05c..25817478e7 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -19,6 +19,16 @@ open Ltac_pretype
let cases_pattern_loc c = c.CAst.loc
+let alias_of_pat pat = DAst.with_val (function
+ | PatVar name -> name
+ | PatCstr(_,_,name) -> name
+ ) pat
+
+let set_pat_alias id = DAst.map (function
+ | PatVar Anonymous -> PatVar (Name id)
+ | PatCstr (cstr,patl,Anonymous) -> PatCstr (cstr,patl,Name id)
+ | pat -> assert false)
+
let cases_predicate_names tml =
List.flatten (List.map (function
| (tm,(na,None)) -> [na]
@@ -452,6 +462,10 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
(**********************************************************************)
(* Conversion from glob_constr to cases pattern, if possible *)
+let is_gvar id c = match DAst.get c with
+| GVar id' -> Id.equal id id'
+| _ -> false
+
let rec cases_pattern_of_glob_constr na = DAst.map (function
| GVar id ->
begin match na with
@@ -468,6 +482,9 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
| _ -> raise Not_found
end
+ | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous ->
+ (* A canonical encoding of aliases *)
+ DAst.get (cases_pattern_of_glob_constr na' b)
| _ -> raise Not_found
)
@@ -503,23 +520,34 @@ let add_patterns_for_params_remove_local_defs (ind,j) l =
drop_local_defs typi l in
Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l
+let add_alias ?loc na c =
+ match na with
+ | Anonymous -> c
+ | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id))
+
(* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux x = DAst.map_with_loc (fun ?loc -> function
- | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
- | PatCstr (cstr,l,Anonymous) ->
+let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function
+ | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None))
+ | PatCstr (cstr,l,na) ->
let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in
let l = add_patterns_for_params_remove_local_defs cstr l in
- GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
+ add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l))
+ | PatVar (Name id) when not isclosed ->
+ GVar id
+ | PatVar Anonymous when not isclosed ->
+ GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None)
| _ -> raise Not_found
) x
let glob_constr_of_closed_cases_pattern p = match DAst.get p with
| PatCstr (cstr,l,na) ->
let loc = p.CAst.loc in
- na,glob_constr_of_closed_cases_pattern_aux (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
+ na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
| _ ->
raise Not_found
+let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p
+
(**********************************************************************)
(* Interpreting ltac variables *)
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 9dd7068cbc..0d9fb1f453 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,10 @@ open Glob_term
val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
+val alias_of_pat : 'a cases_pattern_g -> Name.t
+
+val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
+
val cast_type_eq : ('a -> 'a -> bool) ->
'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
@@ -78,10 +82,14 @@ val map_pattern : (glob_constr -> glob_constr) ->
Take the current alias as parameter,
@raise Not_found if translation is impossible *)
-val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
+val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g
+(** A canonical encoding of cases pattern into constr such that
+ composed with [cases_pattern_of_glob_constr Anonymous] gives identity *)
+val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g
+
val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8809558ff7..6700748ebc 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -378,10 +378,10 @@ let check_evars_are_solved env current_sigma init_sigma =
let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
check_evars_are_solved env current_sigma frozen
-let process_inference_flags flags env initial_sigma (sigma,c) =
+let process_inference_flags flags env initial_sigma (sigma,c,cty) =
let sigma = solve_remaining_evars flags env sigma initial_sigma in
let c = if flags.expand_evars then nf_evar sigma c else c in
- sigma,c
+ sigma,c,cty
let adjust_evar_source evdref na c =
match na, kind !evdref c with
@@ -1173,15 +1173,18 @@ let ise_pretype_gen flags env sigma lvar kind c =
let env = make_env env sigma in
let evdref = ref sigma in
let k0 = Context.Rel.length (rel_context env) in
- let c' = match kind with
+ let c', c'_ty = match kind with
| WithoutTypeConstraint ->
- (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
+ let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in
+ j.uj_val, j.uj_type
| OfType exptyp ->
- (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
+ let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in
+ j.uj_val, j.uj_type
| IsType ->
- (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val
+ let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in
+ tj.utj_val, mkSort tj.utj_type
in
- process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c')
+ process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty)
let default_inference_flags fail = {
use_typeclasses = true;
@@ -1201,7 +1204,7 @@ let all_and_fail_flags = default_inference_flags true
let all_no_fail_flags = default_inference_flags false
let ise_pretype_gen_ctx flags env sigma lvar kind c =
- let evd, c = ise_pretype_gen flags env sigma lvar kind c in
+ let evd, c, _ = ise_pretype_gen flags env sigma lvar kind c in
let evd, f = Evarutil.nf_evars_and_universes evd in
f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd
@@ -1213,12 +1216,15 @@ let understand
env sigma c =
ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c
-let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c =
- let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in
- (sigma, c)
+let understand_tcc_ty ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c =
+ ise_pretype_gen flags env sigma empty_lvar expected_type c
+
+let understand_tcc ?flags env sigma ?expected_type c =
+ let sigma, c, _ = understand_tcc_ty ?flags env sigma ?expected_type c in
+ sigma, c
let understand_ltac flags env sigma lvar kind c =
- let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in
+ let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
(sigma, c)
let pretype k0 resolve_tc typcon env evdref lvar t =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index fe10be9e7c..864768fe56 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -58,6 +58,11 @@ val all_and_fail_flags : inference_flags
val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
?expected_type:typing_constraint -> glob_constr -> evar_map * constr
+(** As [understand_tcc] but also returns the type of the elaborated term.
+ The [expand_evars] flag is not applied to the type (only to the term). *)
+val understand_tcc_ty : ?flags:inference_flags -> env -> evar_map ->
+ ?expected_type:typing_constraint -> glob_constr -> evar_map * constr * types
+
(** More general entry point with evars from ltac *)
(** Generic call to the interpreter from glob_constr to constr
@@ -116,7 +121,7 @@ val pretype_type :
val ise_pretype_gen :
inference_flags -> env -> evar_map ->
- ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr
+ ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types
(**/**)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 3132d2ad53..3cc1520179 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -34,7 +34,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
let mspec = lookup_mind_specif env ind in
let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
- EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
+ Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
let e_type_judgment env evdref j =
match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with
@@ -49,6 +49,30 @@ let e_assumption_of_judgment env evdref j =
with Type_errors.TypeError _ | PretypeError _ ->
error_assumption env !evdref j
+let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv =
+ let rec apply_rec n typ = function
+ | [] ->
+ { uj_val = mkApp (j_val funj, Array.map j_val argjv);
+ uj_type =
+ let ar = inductive_type_knowing_parameters env !evdref ind argjv in
+ hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) }
+ | hj::restjl ->
+ match EConstr.kind !evdref (whd_all env !evdref typ) with
+ | Prod (_,c1,c2) ->
+ if Evarconv.e_cumul env evdref hj.uj_type c1 then
+ apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+ else
+ error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
+ | Evar ev ->
+ let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
+ evdref := evd';
+ let (_,_,c2) = destProd evd' t in
+ apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+ | _ ->
+ error_cant_apply_not_functional env !evdref funj argjv
+ in
+ apply_rec 1 funj.uj_type (Array.to_list argjv)
+
let e_judge_of_apply env evdref funj argjv =
let rec apply_rec n typ = function
| [] ->
@@ -300,16 +324,14 @@ let rec execute env evdref cstr =
| App (f,args) ->
let jl = execute_array env evdref args in
- let j =
- match EConstr.kind !evdref f with
- | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
- make_judge f
- (inductive_type_knowing_parameters env !evdref (ind, u) jl)
- | _ ->
- (* No template polymorphism *)
- execute env evdref f
- in
- e_judge_of_apply env evdref j jl
+ (match EConstr.kind !evdref f with
+ | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
+ let fj = execute env evdref f in
+ e_judge_of_applied_inductive_knowing_parameters env evdref fj (ind, u) jl
+ | _ ->
+ (* No template polymorphism *)
+ let fj = execute env evdref f in
+ e_judge_of_apply env evdref fj jl)
| Lambda (name,c1,c2) ->
let j = execute env evdref c1 in
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index 3cf32d7ff0..89f1185a99 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -6,12 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open CErrors
(** Local universes and constraints declarations *)
type universe_decl =
- (Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
let default_univ_decl =
let open Misctypes in
@@ -34,9 +33,9 @@ let interp_univ_constraints env evd cstrs =
in
List.fold_left interp (evd,Univ.Constraint.empty) cstrs
-let interp_univ_decl env decl =
+let interp_univ_decl env decl =
let open Misctypes in
- let pl = decl.univdecl_instance in
+ let pl : lident list = decl.univdecl_instance in
let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in
let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
let decl = { univdecl_instance = pl;
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
index 0c3b749cbf..706d3a157f 100644
--- a/pretyping/univdecls.mli
+++ b/pretyping/univdecls.mli
@@ -8,7 +8,7 @@
(** Local universe and constraint declarations. *)
type universe_decl =
- (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
val default_univ_decl : universe_decl
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:15:20 +0000