diff options
| -rw-r--r-- | pretyping/detyping.ml | 21 | ||||
| -rw-r--r-- | pretyping/termops.ml | 39 | ||||
| -rw-r--r-- | pretyping/termops.mli | 41 |
3 files changed, 76 insertions, 25 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1fcc6d8b7..8de9e2abe 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -174,17 +174,18 @@ let computable p k = let _,ccl = decompose_lam p in noccur_between 1 (k+1) ccl - +let avoid_flag isgoal = if isgoal then Some true else None + 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 true avoid env_names name c' with + (match concrete_name (Some 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' | (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c')) | LetIn (name,_,_,c') -> - (match concrete_name true avoid env_names name c' with + (match concrete_name (Some 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' @@ -196,11 +197,11 @@ 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 true [] empty_names_context name c' with + (match concrete_name (Some 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 true [] empty_names_context name c' with + (match concrete_name (Some 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 @@ -227,7 +228,7 @@ let rec decomp_branch n nal b (avoid,env as e) c = | _ -> Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])), concrete_name in - let na',avoid' = f b avoid env na c in + let na',avoid' = f (Some b) avoid env na c in decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c let rec build_tree na isgoal e ci cl = @@ -355,7 +356,7 @@ let detype_sort = function (**********************************************************************) (* Main detyping function *) -let rec detype isgoal avoid env t = +let rec detype (isgoal:bool) avoid env t = match kind_of_term (collapse_appl t) with | Rel n -> (try match lookup_name_of_rel n env with @@ -484,7 +485,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch = if force_wildcard () & noccurn 1 b then PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids else - let id = next_name_away_with_default "x" x avoid in + let id = next_name_away_in_cases_pattern x avoid in PatVar (dl,Name id),id::avoid,(add_name (Name id) env),id::ids in let rec buildrec ids patlist avoid env n b = @@ -519,9 +520,9 @@ and detype_eqn isgoal avoid env constr construct_nargs branch = and detype_binder isgoal bk avoid env na ty c = let na',avoid' = if bk = BLetIn then - concrete_let_name isgoal avoid env na c + concrete_let_name (avoid_flag isgoal) avoid env na c else - concrete_name isgoal avoid env na c in + concrete_name (avoid_flag isgoal) avoid env na c in let r = detype isgoal avoid' (add_name na' env) c in match bk with | BProd -> RProd (dl, na',detype isgoal avoid env ty, r) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 08c38f1b1..d3283164b 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -834,6 +834,14 @@ let is_global id = with Not_found -> false +let is_constructor id = + try + match locate (make_short_qualid id) with + | ConstructRef _ as ref -> not (is_imported_ref ref) + | _ -> false + with Not_found -> + false + let is_section_variable id = try let _ = Global.lookup_named id in true with Not_found -> false @@ -898,11 +906,19 @@ let occur_id nenv id0 c = with Occur -> true | Not_found -> false (* Case when a global is not in the env *) -let next_name_not_occuring is_goal_ccl name l env_names t = +type avoid_flags = bool option + +let next_name_not_occuring avoid_flags name l env_names t = let rec next id = if List.mem id l or occur_id env_names id t or - (* To be consistent with intro mechanism *) - (is_goal_ccl & is_global id & not (is_section_variable id)) + (* Further restrictions ? *) + match avoid_flags with None -> false | Some not_only_cstr -> + (if not_only_cstr then + (* To be consistent with the intro mechanism *) + is_global id & not (is_section_variable id) + else + (* To avoid constructors in pattern-matchings *) + is_constructor id) then next (lift_ident id) else id in @@ -996,17 +1012,26 @@ let global_vars_set_of_decl env = function Idset.union (global_vars_set env t) (global_vars_set env c) +let default_x = id_of_string "x" + +let rec next_name_away_in_cases_pattern id avoid = + let id = match id with Name id -> id | Anonymous -> default_x in + let rec next id = + if List.mem id avoid or is_constructor id then next (lift_ident id) + else id in + next id + (* Remark: Anonymous var may be dependent in Evar's contexts *) -let concrete_name is_goal_ccl l env_names n c = +let concrete_name avoid_flags l env_names n c = if n = Anonymous & noccurn 1 c then (Anonymous,l) else - let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in + let fresh_id = next_name_not_occuring avoid_flags 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 is_goal_ccl l env_names n c = - let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in +let concrete_let_name avoid_flags l env_names n c = + let fresh_id = next_name_not_occuring avoid_flags 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 d461498d9..37667f741 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -100,6 +100,7 @@ val occur_var_in_decl : identifier -> 'a * types option * types -> bool val occur_term : constr -> constr -> bool val free_rels : constr -> Intset.t +val dependent : constr -> constr -> bool (* Substitution of metavariables *) type metamap = (metavariable * constr) list @@ -108,19 +109,36 @@ val subst_meta : metamap -> constr -> constr (* [pop c] lifts by -1 the positive indexes in [c] *) val pop : constr -> constr -(* bindings of an arbitrary large term. Uses equality modulo +(*s Substitution of an arbitrary large term. Uses equality modulo reduction of let *) -val dependent : constr -> constr -> bool + +(* [subst_term_gen eq d c] replaces [Rel 1] by [d] in [c] using [eq] + as equality *) val subst_term_gen : (constr -> constr -> bool) -> constr -> constr -> constr + +(* [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] + as equality *) val replace_term_gen : (constr -> constr -> bool) -> constr -> constr -> constr -> constr + +(* [subst_term d c] replaces [Rel 1] by [d] in [c] *) val subst_term : constr -> constr -> constr + +(* [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : constr -> constr -> constr -> constr -val subst_term_occ_gen : - int list -> int -> constr -> types -> int * types -val subst_term_occ : int list -> constr -> types -> types + +(* [subst_term_occ occl c d] replaces occurrences of [Rel 1] at + positions [occl] by [c] in [d] *) +val subst_term_occ_gen : int list -> int -> constr -> types -> int * types + +(* [subst_term_occ occl c d] replaces occurrences of [Rel 1] at + positions [occl] by [c] in [d] (see also Note OCC) *) +val subst_term_occ : int list -> constr -> constr -> constr + +(* [subst_term_occ_decl occl c decl] replaces occurrences of [Rel 1] at + positions [occl] by [c] in [decl] *) val subst_term_occ_decl : int list -> constr -> named_declaration -> named_declaration @@ -177,15 +195,22 @@ type used_idents = identifier list val occur_rel : int -> name list -> identifier -> bool val occur_id : name list -> identifier -> constr -> bool +type avoid_flags = bool option + (* Some true = avoid all globals (as in intro); + Some false = avoid only global constructors; None = don't avoid globals *) + +val next_name_away_in_cases_pattern : + name -> identifier list -> identifier val next_global_ident_away : (*allow section vars:*) bool -> identifier -> identifier list -> identifier val next_name_not_occuring : - bool -> name -> identifier list -> name list -> constr -> identifier + avoid_flags -> name -> identifier list -> name list -> constr -> identifier val concrete_name : - bool -> identifier list -> name list -> name -> constr -> + avoid_flags -> identifier list -> name list -> name -> constr -> name * identifier list val concrete_let_name : - bool -> identifier list -> name list -> name -> constr -> name * identifier list + avoid_flags -> identifier list -> name list -> name -> constr -> + name * identifier list val rename_bound_var : env -> identifier list -> types -> types (* other signature iterators *) |