aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/correctness/pcic.ml10
-rw-r--r--contrib/first-order/instances.ml2
-rw-r--r--interp/constrextern.ml12
-rw-r--r--parsing/termast.ml6
-rw-r--r--pretyping/detyping.ml47
-rw-r--r--pretyping/detyping.mli13
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/termops.ml20
-rw-r--r--pretyping/termops.mli11
9 files changed, 58 insertions, 65 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index bef1e2a23c..db2617da33 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -137,7 +137,7 @@ let tuple_ref dep n =
let trad_binder avoid nenv id = function
| CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id))
- | CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty
+ | CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty
let rec push_vars avoid nenv = function
| [] -> ([],avoid,nenv)
@@ -209,22 +209,22 @@ let rawconstr_of_prog p =
let n = List.length l in
let cl = List.map (trad avoid nenv) l in
let tuple = tuple_ref dep n in
- let tyl = List.map (Detyping.detype (Global.env()) avoid nenv) tyl in
+ let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in
let args = tyl @ cl in
RApp (dummy_loc, RRef (dummy_loc, tuple), args)
| CC_case (ty,b,el) ->
let c = trad avoid nenv b in
let cl = List.map (trad avoid nenv) el in
- let ty = Detyping.detype (Global.env()) avoid nenv ty in
+ let ty = Detyping.detype (false,Global.env()) avoid nenv ty in
ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None)
| CC_expr c ->
- Detyping.detype (Global.env()) avoid nenv c
+ Detyping.detype (false,Global.env()) avoid nenv c
| CC_hole c ->
RCast (dummy_loc, RHole (dummy_loc, QuestionMark),
- Detyping.detype (Global.env()) avoid nenv c)
+ Detyping.detype (false,Global.env()) avoid nenv c)
in
trad [] empty_names_context p
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 1dc72eecb8..423df2f3c7 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -121,7 +121,7 @@ let mk_open_instance id gl m t=
let nid=(fresh_id avoid var_id gl) in
(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
let nt=it_mkLambda_or_LetIn revt (aux m []) in
- let rawt=Detyping.detype env [] [] nt in
+ let rawt=Detyping.detype (false,env) [] [] nt in
let rec raux n t=
if n=0 then t else
match t with
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b34ae524f2..2eae4a51b9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -738,7 +738,7 @@ let extern_constr_gen at_top scopt env t =
let vars = vars_of_env env in
let avoid = if at_top then ids_of_context env else [] in
extern (not at_top) (scopt,Symbols.current_scopes()) vars
- (Detyping.detype env avoid (names_of_rel_context env) t)
+ (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t)
let extern_constr_in_scope at_top scope env t =
extern_constr_gen at_top (Some scope) env t
@@ -782,13 +782,11 @@ let rec raw_of_pat tenv env = function
| PCase ((Some ind,cs),typopt,tm,bv) ->
let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in
- Detyping.detype_case false
- (fun tenv _ -> raw_of_pat tenv)
- (fun tenv _ -> raw_of_eqn tenv)
- tenv avoid env ind cs typopt k tm bv
+ Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env)
+ tenv avoid ind cs typopt k tm bv
| PCase _ -> error "Unsupported case-analysis while printing pattern"
- | PFix f -> Detyping.detype tenv [] env (mkFix f)
- | PCoFix c -> Detyping.detype tenv [] env (mkCoFix c)
+ | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f)
+ | PCoFix c -> Detyping.detype (false,tenv) [] env (mkCoFix c)
| PSort s -> RSort (loc,s)
and raw_of_eqn tenv env constr construct_nargs branch =
diff --git a/parsing/termast.ml b/parsing/termast.ml
index da683e5fa8..3174898c42 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -337,7 +337,7 @@ let ast_of_constr at_top env t =
else Reductionops.local_strong strip_outer_cast t in
let avoid = if at_top then ids_of_context env else [] in
ast_of_raw
- (Detyping.detype env avoid (names_of_rel_context env) t')
+ (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t')
let ast_of_constant env sp =
let a = ast_of_constant_ref sp in
@@ -432,8 +432,8 @@ let rec ast_of_pattern tenv env = function
| PMeta (Some n) -> ope("META",[ast_of_ident n])
| PMeta None -> ope("ISEVAR",[])
- | PFix f -> ast_of_raw (Detyping.detype tenv [] env (mkFix f))
- | PCoFix c -> ast_of_raw (Detyping.detype tenv [] env (mkCoFix c))
+ | PFix f -> ast_of_raw (Detyping.detype (false,tenv) [] env (mkFix f))
+ | PCoFix c -> ast_of_raw (Detyping.detype (false,tenv) [] env (mkCoFix c))
and ast_of_patopt tenv env = function
| None -> (string "SYNTH")
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index acbdd0387e..6b091b9ced 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -164,17 +164,17 @@ let computable p k =
let lookup_name_as_renamed env t s =
let rec lookup avoid env_names n c = match kind_of_term c with
| Prod (name,_,c') ->
- (match concrete_name env avoid env_names name c' with
- | (Some id,avoid') ->
+ (match concrete_name true avoid env_names name c' with
+ | (Name id,avoid') ->
if id=s then (Some n)
else lookup avoid' (add_name (Name id) env_names) (n+1) c'
- | (None,avoid') -> lookup avoid' env_names (n+1) (pop c'))
+ | (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c'))
| LetIn (name,_,_,c') ->
- (match concrete_name env avoid env_names name c' with
- | (Some id,avoid') ->
+ (match concrete_name true avoid env_names name c' with
+ | (Name id,avoid') ->
if id=s then (Some n)
else lookup avoid' (add_name (Name id) env_names) (n+1) c'
- | (None,avoid') -> lookup avoid' env_names (n+1) (pop c'))
+ | (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c'))
| Cast (c,_) -> lookup avoid env_names n c
| _ -> None
in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t
@@ -182,20 +182,20 @@ let lookup_name_as_renamed env t s =
let lookup_index_as_renamed env t n =
let rec lookup n d c = match kind_of_term c with
| Prod (name,_,c') ->
- (match concrete_name env [] empty_names_context name c' with
- (Some _,_) -> lookup n (d+1) c'
- | (None ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+ (match concrete_name true [] empty_names_context name c' with
+ (Name _,_) -> lookup n (d+1) c'
+ | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
| LetIn (name,_,_,c') ->
- (match concrete_name env [] empty_names_context name c' with
- | (Some _,_) -> lookup n (d+1) c'
- | (None ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+ (match concrete_name true [] empty_names_context name c' with
+ | (Name _,_) -> lookup n (d+1) c'
+ | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
| Cast (c,_) -> lookup n d c
| _ -> None
in lookup n 1 t
-let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
+let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl =
let synth_type = synthetize_type () in
- let tomatch = detype tenv avoid env c in
+ let tomatch = detype c in
(* Find constructors arity *)
let (mib,mip) = Inductive.lookup_mind_specif tenv indsp in
@@ -209,13 +209,11 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
if synth_type & computable & bl <> [||] then
Anonymous, None, None, None
else
- let p = option_app (detype tenv avoid env) p in
+ let p = option_app detype p in
match p with
| None -> Anonymous, None, None, None
| Some p ->
let decompose_lam k c =
- let name_cons = function
- Anonymous -> fun l -> l | Name id -> fun l -> id::l in
let rec lamdec_rec l avoid k c =
if k = 0 then l,c else match c with
| RLambda (_,x,t,c) ->
@@ -241,7 +239,7 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
n, aliastyp, Some typ, Some p
in
let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
- let eqnv = array_map3 (detype_eqn tenv avoid env) constructs consnargsl bl in
+ let eqnv = array_map3 detype_eqn constructs consnargsl bl in
let eqnl = Array.to_list eqnv in
let tag =
try
@@ -256,7 +254,7 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
if tag = RegularStyle then
RCases (dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl)
else
- let bl = Array.map (detype tenv avoid env) bl in
+ let bl = Array.map detype bl in
if not !Options.v7 && tag = LetStyle && aliastyp = None then
let rec decomp_lam_force n avoid l p =
if n = 0 then (List.rev l,p) else
@@ -340,8 +338,8 @@ let rec detype tenv avoid env t =
let comp = computable p (annot.ci_pp_info.ind_nargs) in
let ind = annot.ci_ind in
let st = annot.ci_pp_info.style in
- detype_case comp detype detype_eqn tenv avoid env ind st (Some p)
- annot.ci_pp_info.ind_nargs c bl
+ detype_case comp (detype tenv avoid env) (detype_eqn tenv avoid env)
+ (snd tenv) avoid ind st (Some p) annot.ci_pp_info.ind_nargs c bl
| Fix (nvn,recdef) -> detype_fix tenv avoid env nvn recdef
| CoFix (n,recdef) -> detype_cofix tenv avoid env n recdef
@@ -437,11 +435,10 @@ and detype_eqn tenv avoid env constr construct_nargs branch =
and detype_binder tenv bk avoid env na ty c =
let na',avoid' =
- if bk = BLetIn then concrete_let_name tenv avoid env na c
+ if bk = BLetIn then
+ concrete_let_name (fst tenv) avoid env na c
else
- match concrete_name tenv avoid env na c with
- | (Some id,l') -> (Name id), l'
- | (None,l') -> Anonymous, l' in
+ concrete_name (fst tenv) avoid env na c in
let r = detype tenv avoid' (add_name na' env) c in
match bk with
| BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5cf174875a..253e0f51c8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -20,15 +20,14 @@ open Termops
(* [detype env avoid nenv c] turns [c], typed in [env], into a rawconstr. *)
(* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
-val detype : env -> identifier list -> names_context -> constr -> rawconstr
+val detype : bool * env -> identifier list -> names_context -> constr ->
+ rawconstr
val detype_case :
- bool ->
- (env -> identifier list -> names_context -> 'a -> rawconstr) ->
- (env -> identifier list -> names_context -> constructor -> int ->
- 'a -> Rawterm.loc * Names.identifier list * Rawterm.cases_pattern list *
- Rawterm.rawconstr) ->
- env -> identifier list -> names_context -> inductive -> case_style ->
+ bool -> ('a -> rawconstr) ->
+ (constructor -> int -> 'a -> loc * identifier list * cases_pattern list *
+ rawconstr) ->
+ env -> identifier list -> inductive -> case_style ->
'a option -> int -> 'a -> 'a array -> rawconstr
(* look for the index of a named var or a nondep var as it is renamed *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 145dc87202..a0fbb77241 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -759,7 +759,7 @@ let rec pretype tycon env isevars lvar = function
let nconstr = Array.length mip.mind_consnames in
let tyi = snd ind in
if isrec && mis_is_recursive_subset [tyi] recargs then
- Some (Detyping.detype env
+ Some (Detyping.detype (false,env)
(ids_of_context env) (names_of_rel_context env)
(nf_evar (evars_of isevars) v))
else
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 6cf9b4e0db..c7786b2e1c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -714,7 +714,7 @@ let occur_rel p env id =
try lookup_name_of_rel p env = Name id
with Not_found -> false (* Unbound indice : may happen in debug *)
-let occur_id env nenv id0 c =
+let occur_id nenv id0 c =
let rec occur n c = match kind_of_term c with
| Var id when id=id0 -> raise Occur
| Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur
@@ -731,11 +731,11 @@ let occur_id env nenv id0 c =
with Occur -> true
| Not_found -> false (* Case when a global is not in the env *)
-let next_name_not_occuring env name l env_names t =
+let next_name_not_occuring is_goal_ccl name l env_names t =
let rec next id =
- if List.mem id l or occur_id env env_names id t or
+ if List.mem id l or occur_id env_names id t or
(* To be consistent with intro mechanism *)
- (is_global id & not (is_section_variable id))
+ (is_goal_ccl & is_global id & not (is_section_variable id))
then next (lift_ident id)
else id
in
@@ -826,16 +826,16 @@ let global_vars_set_of_decl env = function
(global_vars_set env c)
(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name env l env_names n c =
+let concrete_name is_goal_ccl l env_names n c =
if n = Anonymous & noccurn 1 c then
- (None,l)
+ (Anonymous,l)
else
- let fresh_id = next_name_not_occuring env n l env_names c in
- let idopt = if noccurn 1 c then None else (Some fresh_id) in
+ let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in
+ let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
(idopt, fresh_id::l)
-let concrete_let_name env l env_names n c =
- let fresh_id = next_name_not_occuring env n l env_names c in
+let concrete_let_name is_goal_ccl l env_names n c =
+ let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in
(Name fresh_id, fresh_id::l)
let rec rename_bound_var env l c =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9031ec42de..0f970706a3 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -151,16 +151,15 @@ val add_vname : Idset.t -> name -> Idset.t
(* sets of free identifiers *)
type used_idents = identifier list
val occur_rel : int -> name list -> identifier -> bool
-val occur_id : env -> name list -> identifier -> constr -> bool
+val occur_id : name list -> identifier -> constr -> bool
val next_name_not_occuring :
- env -> name -> identifier list -> name list -> constr -> identifier
+ bool -> name -> identifier list -> name list -> constr -> identifier
val concrete_name :
- env -> identifier list -> name list -> name ->
- constr -> identifier option * identifier list
+ bool -> identifier list -> name list -> name -> constr ->
+ name * identifier list
val concrete_let_name :
- env -> identifier list -> name list ->
- name -> constr -> name * identifier list
+ bool -> identifier list -> name list -> name -> constr -> name * identifier list
val rename_bound_var : env -> identifier list -> types -> types
(* other signature iterators *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 08:54:09 +0000