aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml5
-rw-r--r--pretyping/detyping.ml22
-rw-r--r--pretyping/glob_ops.ml38
-rw-r--r--pretyping/glob_ops.mli10
-rw-r--r--pretyping/inferCumulativity.ml34
-rw-r--r--pretyping/pretyping.ml30
-rw-r--r--pretyping/pretyping.mli7
7 files changed, 85 insertions, 61 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 311c1c09e..a0434f927 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/detyping.ml b/pretyping/detyping.ml
index 754e88139..18ecbf8ed 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -451,17 +451,15 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
then
Anonymous, None, None
else
- match Option.map detype p with
- | None -> Anonymous, None, None
- | Some p ->
- let nl,typ = it_destRLambda_or_LetIn_names k p in
- let n,typ = match DAst.get typ with
- | GLambda (x,_,t,c) -> x, c
- | _ -> Anonymous, typ in
- let aliastyp =
- if List.for_all (Name.equal Anonymous) nl then None
- else Some (Loc.tag (indsp,nl)) in
- n, aliastyp, Some typ
+ let p = detype p in
+ let nl,typ = it_destRLambda_or_LetIn_names k p in
+ let n,typ = match DAst.get typ with
+ | GLambda (x,_,t,c) -> x, c
+ | _ -> Anonymous, typ in
+ let aliastyp =
+ if List.for_all (Name.equal Anonymous) nl then None
+ else Some (Loc.tag (indsp,nl)) in
+ n, aliastyp, Some typ
in
let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
let tag =
@@ -650,7 +648,7 @@ and detype_r d flags avoid env sigma t =
(is_nondep_branch sigma) avoid
(ci.ci_ind,ci.ci_pp_info.style,
ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
- (Some p) c bl
+ p c bl
| Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef
| CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index a21137a05..25817478e 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 9dd7068cb..0d9fb1f45 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/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index a0a8276c5..a4097237f 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -159,34 +159,21 @@ and infer_vect infos variances v =
let infer_term cv_pb env variances c =
let open CClosure in
- let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in
- let infos = create_clos_infos reds env in
+ let infos = create_clos_infos all env in
infer_fterm cv_pb infos variances (CClosure.inject c) []
-let infer_arity_constructor env variances arcn is_arity params =
- let numchecked = ref 0 in
- let numparams = Context.Rel.nhyps params in
- let basic_check env variances tp =
- let variances =
- if !numchecked >= numparams then
- infer_term CUMUL env variances tp
- else
- variances
- in
- numchecked := !numchecked + 1; variances
- in
+let infer_arity_constructor is_arity env variances arcn =
let infer_typ typ (env,variances) =
match typ with
| Context.Rel.Declaration.LocalAssum (_, typ') ->
- (Environ.push_rel typ env, basic_check env variances typ')
+ (Environ.push_rel typ env, infer_term CUMUL env variances typ')
| Context.Rel.Declaration.LocalDef _ -> assert false
in
- let arcn' = Term.it_mkProd_or_LetIn arcn params in
- let typs, codom = Reduction.dest_prod env arcn' in
+ let typs, codom = Reduction.dest_prod env arcn in
let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in
(* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j}
i is irrelevant, j is invariant. *)
- if not is_arity then basic_check env variances codom else variances
+ if not is_arity then infer_term CUMUL env variances codom else variances
let infer_inductive env mie =
let open Entries in
@@ -205,15 +192,12 @@ let infer_inductive env mie =
Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
LMap.empty uarray
in
+ let env, _ = Typeops.infer_local_decls env params in
let variances = List.fold_left (fun variances entry ->
- let _, params = Typeops.infer_local_decls env params in
- let variances = infer_arity_constructor
- env variances entry.mind_entry_arity true params
+ let variances = infer_arity_constructor true
+ env variances entry.mind_entry_arity
in
- List.fold_left
- (fun variances cons ->
- infer_arity_constructor
- env variances cons false params)
+ List.fold_left (infer_arity_constructor false env)
variances entry.mind_entry_lc)
variances
entries
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8809558ff..6700748eb 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 fe10be9e7..864768fe5 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
(**/**)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 19:25:59 +0000