aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r--pretyping/detyping.ml127
1 files changed, 67 insertions, 60 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0b5ea86d5..8ba408679 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,14 +6,17 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+module CVars = Vars
+
open Pp
open CErrors
open Util
open Names
open Term
+open Environ
+open EConstr
open Vars
open Inductiveops
-open Environ
open Glob_term
open Glob_ops
open Termops
@@ -188,7 +191,7 @@ let _ = declare_bool_option
(* Auxiliary function for MutCase printing *)
(* [computable] tries to tell if the predicate typing the result is inferable*)
-let computable p k =
+let computable sigma p k =
(* We first remove as many lambda as the arity, then we look
if it remains a lambda for a dependent elimination. This function
works for normal eta-expanded term. For non eta-expanded or
@@ -205,29 +208,29 @@ let computable p k =
sinon on perd la réciprocité de la synthèse (qui, lui,
engendrera un prédicat non dépendant) *)
- let sign,ccl = decompose_lam_assum p in
+ let sign,ccl = decompose_lam_assum sigma p in
Int.equal (Context.Rel.length sign) (k + 1)
&&
- noccur_between 1 (k+1) ccl
+ noccur_between sigma 1 (k+1) ccl
-let lookup_name_as_displayed env t s =
- let rec lookup avoid n c = match kind_of_term c with
+let lookup_name_as_displayed env sigma t s =
+ let rec lookup avoid n c = match EConstr.kind sigma c with
| Prod (name,_,c') ->
- (match compute_displayed_name_in RenamingForGoal avoid name c' with
+ (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with
| (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
| (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
| LetIn (name,_,_,c') ->
- (match compute_displayed_name_in RenamingForGoal avoid name c' with
+ (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with
| (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
| (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
| Cast (c,_,_) -> lookup avoid n c
| _ -> None
in lookup (ids_of_named_context (named_context env)) 1 t
-let lookup_index_as_renamed env t n =
- let rec lookup n d c = match kind_of_term c with
+let lookup_index_as_renamed env sigma t n =
+ let rec lookup n d c = match EConstr.kind sigma c with
| Prod (name,_,c') ->
- (match compute_displayed_name_in RenamingForGoal [] name c' with
+ (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
(Name _,_) -> lookup n (d+1) c'
| (Anonymous,_) ->
if Int.equal n 0 then
@@ -237,7 +240,7 @@ let lookup_index_as_renamed env t n =
else
lookup (n-1) (d+1) c')
| LetIn (name,_,_,c') ->
- (match compute_displayed_name_in RenamingForGoal [] name c' with
+ (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
| (Name _,_) -> lookup n (d+1) c'
| (Anonymous,_) ->
if Int.equal n 0 then
@@ -254,20 +257,20 @@ let lookup_index_as_renamed env t n =
(**********************************************************************)
(* Fragile algorithm to reverse pattern-matching compilation *)
-let update_name na ((_,(e,_)),c) =
+let update_name sigma na ((_,(e,_)),c) =
match na with
- | Name _ when force_wildcard () && noccurn (List.index Name.equal na e) c ->
+ | Name _ when force_wildcard () && noccurn sigma (List.index Name.equal na e) c ->
Anonymous
| _ ->
na
-let rec decomp_branch tags nal b (avoid,env as e) c =
+let rec decomp_branch tags nal b (avoid,env as e) sigma c =
let flag = if b then RenamingForGoal else RenamingForCasesPattern (fst env,c) in
match tags with
| [] -> (List.rev nal,(e,c))
| b::tags ->
let na,c,f,body,t =
- match kind_of_term (strip_outer_cast c), b with
+ match EConstr.kind sigma (strip_outer_cast sigma c), b with
| Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t
| LetIn (na,b,t,c),true ->
na,c,compute_displayed_name_in,Some b,Some t
@@ -277,52 +280,52 @@ let rec decomp_branch tags nal b (avoid,env as e) c =
| _, true ->
Anonymous,lift 1 c,compute_displayed_name_in,None,None
in
- let na',avoid' = f flag avoid na c in
+ let na',avoid' = f sigma flag avoid na c in
decomp_branch tags (na'::nal) b
- (avoid', add_name_opt na' body t env) c
+ (avoid', add_name_opt na' body t env) sigma c
-let rec build_tree na isgoal e ci cl =
- let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
+let rec build_tree na isgoal e sigma ci cl =
+ let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name sigma na rhs) in
let cnl = ci.ci_pp_info.cstr_tags in
let cna = ci.ci_cstr_nargs in
List.flatten
(List.init (Array.length cl)
- (fun i -> contract_branch isgoal e (cnl.(i),cna.(i),mkpat i,cl.(i))))
+ (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i))))
-and align_tree nal isgoal (e,c as rhs) = match nal with
+and align_tree nal isgoal (e,c as rhs) sigma = match nal with
| [] -> [[],rhs]
| na::nal ->
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Case (ci,p,c,cl) when
- eq_constr c (mkRel (List.index Name.equal na (fst (snd e))))
+ eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e))))
&& not (Int.equal (Array.length cl) 0)
&& (* don't contract if p dependent *)
- computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
- let clauses = build_tree na isgoal e ci cl in
+ computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
+ let clauses = build_tree na isgoal e sigma ci cl in
List.flatten
(List.map (fun (pat,rhs) ->
- let lines = align_tree nal isgoal rhs in
+ let lines = align_tree nal isgoal rhs sigma in
List.map (fun (hd,rest) -> pat::hd,rest) lines)
clauses)
| _ ->
- let pat = PatVar(dl,update_name na rhs) in
- let mat = align_tree nal isgoal rhs in
+ let pat = PatVar(dl,update_name sigma na rhs) in
+ let mat = align_tree nal isgoal rhs sigma in
List.map (fun (hd,rest) -> pat::hd,rest) mat
-and contract_branch isgoal e (cdn,can,mkpat,b) =
- let nal,rhs = decomp_branch cdn [] isgoal e b in
- let mat = align_tree nal isgoal rhs in
+and contract_branch isgoal e sigma (cdn,can,mkpat,b) =
+ let nal,rhs = decomp_branch cdn [] isgoal e sigma b in
+ let mat = align_tree nal isgoal rhs sigma in
List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat
(**********************************************************************)
(* Transform internal representation of pattern-matching into list of *)
(* clauses *)
-let is_nondep_branch c l =
+let is_nondep_branch sigma c l =
try
(* FIXME: do better using tags from l *)
- let sign,ccl = decompose_lam_n_decls (List.length l) c in
- noccur_between 1 (Context.Rel.length sign) ccl
+ let sign,ccl = decompose_lam_n_decls sigma (List.length l) c in
+ noccur_between sigma 1 (Context.Rel.length sign) ccl
with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *)
false
@@ -420,7 +423,7 @@ let detype_sort sigma = function
| Type u ->
GType
(if !print_universes
- then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
+ then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
else [])
type binder_kind = BProd | BLambda | BLetIn
@@ -432,14 +435,15 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
let set_detype_anonymous f = detype_anonymous := f
let detype_level sigma l =
- GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
+ GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
let detype_instance sigma l =
+ let l = EInstance.kind sigma l in
if Univ.Instance.is_empty l then None
else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
let rec detype flags avoid env sigma t =
- match kind_of_term (collapse_appl t) with
+ match EConstr.kind sigma (collapse_appl sigma t) with
| Rel n ->
(try match lookup_name_of_rel n (fst env) with
| Name id -> GVar (dl, id)
@@ -454,7 +458,7 @@ let rec detype flags avoid env sigma t =
| Var id ->
(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
with Not_found -> GVar (dl, id))
- | Sort s -> GSort (dl,detype_sort sigma s)
+ | Sort s -> GSort (dl,detype_sort sigma (ESorts.kind sigma s))
| Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
detype flags avoid env sigma c1
| Cast (c1,k,c2) ->
@@ -504,7 +508,9 @@ let rec detype flags avoid env sigma t =
let ty = Retyping.get_type_of (snd env) sigma c in
let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
let body' = strip_lam_assum body in
- let body' = subst_instance_constr u body' in
+ let u = EInstance.kind sigma u in
+ let body' = CVars.subst_instance_constr u body' in
+ let body' = EConstr.of_constr body' in
substl (c :: List.rev args) body'
with Retyping.RetypeError _ | Not_found ->
anomaly (str"Cannot detype an unfolded primitive projection.")
@@ -523,18 +529,18 @@ let rec detype flags avoid env sigma t =
| LocalDef _ -> true
| LocalAssum (id,_) ->
try let n = List.index Name.equal (Name id) (fst env) in
- isRelN n c
- with Not_found -> isVarId id c
+ isRelN sigma n c
+ with Not_found -> isVarId sigma id c
in
let id,l =
try
let id = match Evd.evar_ident evk sigma with
- | None -> Evd.pr_evar_suggested_name evk sigma
+ | None -> Termops.pr_evar_suggested_name evk sigma
| Some id -> id
in
let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
- let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
- let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
+ let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
+ let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in
id,l
with Not_found ->
Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
@@ -547,10 +553,10 @@ let rec detype flags avoid env sigma t =
| Construct (cstr_sp,u) ->
GRef (dl, ConstructRef cstr_sp, detype_instance sigma u)
| Case (ci,p,c,bl) ->
- let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in
+ let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
detype_case comp (detype flags avoid env sigma)
(detype_eqns flags avoid env sigma ci comp)
- is_nondep_branch avoid
+ (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
@@ -590,7 +596,7 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) =
Array.map (fun (_,bd,_) -> bd) v)
and share_names flags n l avoid env sigma c t =
- match kind_of_term c, kind_of_term t with
+ match EConstr.kind sigma c, EConstr.kind sigma t with
(* factorize even when not necessary to have better presentation *)
| Lambda (na,t,c), Prod (na',t',c') ->
let na = match (na,na') with
@@ -628,7 +634,7 @@ and share_names flags n l avoid env sigma c t =
and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
try
if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
- let mat = build_tree Anonymous (snd flags) (avoid,env) ci bl in
+ let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in
List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c))
mat
with e when CErrors.noncritical e ->
@@ -637,15 +643,15 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
let make_pat x avoid env b body ty ids =
- if force_wildcard () && noccurn 1 b then
+ if force_wildcard () && noccurn sigma 1 b then
PatVar (dl,Anonymous),avoid,(add_name Anonymous body ty env),ids
else
let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
- let na,avoid' = compute_displayed_name_in flag avoid x b in
+ let na,avoid' = compute_displayed_name_in sigma flag avoid x b in
PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na
in
let rec buildrec ids patlist avoid env l b =
- match kind_of_term b, l with
+ match EConstr.kind sigma b, l with
| _, [] ->
(dl, Id.Set.elements ids,
[PatCstr(dl, constr, List.rev patlist,Anonymous)],
@@ -680,8 +686,8 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in
let na',avoid' = match bk with
- | BLetIn -> compute_displayed_let_name_in flag avoid na c
- | _ -> compute_displayed_name_in flag avoid na c in
+ | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c
+ | _ -> compute_displayed_name_in sigma flag avoid na c in
let r = detype flags avoid' (add_name na' body ty env) sigma c in
match bk with
| BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
@@ -694,7 +700,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
GLetIn (dl, na', c, t, r)
let detype_rel_context ?(lax=false) where avoid env sigma sign =
- let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
+ let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
let rec aux avoid env = function
| [] -> []
| decl::rest ->
@@ -706,10 +712,10 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign =
| None -> na,avoid
| Some c ->
if is_local_def decl then
- compute_displayed_let_name_in
+ compute_displayed_let_name_in sigma
(RenamingElsewhereFor (fst env,c)) avoid na c
else
- compute_displayed_name_in
+ compute_displayed_name_in sigma
(RenamingElsewhereFor (fst env,c)) avoid na c in
let b = match decl with
| LocalAssum _ -> None
@@ -726,6 +732,7 @@ let detype ?(lax=false) isgoal avoid env sigma t =
detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t
let detype_closed_glob ?lax isgoal avoid env sigma t =
+ let open Context.Rel.Declaration in
let convert_id cl id =
try Id.Map.find id cl.idents
with Not_found -> id
@@ -746,8 +753,8 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
(* spiwack: I'm not sure it is the right thing to do,
but I'm computing the detyping environment like
[Printer.pr_constr_under_binders_env] does. *)
- let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) b in
- let env = Termops.push_rels_assum assums env in
+ let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in
+ let env = push_rel_context assums env in
detype ?lax isgoal avoid env sigma c
(* if [id] is bound to a [closed_glob_constr]. *)
with Not_found -> try
@@ -802,7 +809,7 @@ let rec subst_glob_constr subst raw =
| GRef (loc,ref,u) ->
let ref',t = subst_global subst ref in
if ref' == ref then raw else
- detype false [] (Global.env()) Evd.empty t
+ detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)
| GVar _ -> raw
| GEvar _ -> raw
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 17:42:59 +0000