diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 3 | ||||
| -rw-r--r-- | kernel/environ.mli | 3 | ||||
| -rw-r--r-- | kernel/sign.ml | 1 | ||||
| -rw-r--r-- | kernel/sign.mli | 1 | ||||
| -rw-r--r-- | kernel/term.ml | 11 | ||||
| -rw-r--r-- | kernel/term.mli | 5 |
6 files changed, 24 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 100db950f0..0c6167a15c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -88,6 +88,9 @@ let fold_var_context f env a = (fun d (env,e) -> (push_var d env, f env d e)) (var_context env) (reset_context env,a)) +let fold_var_context_reverse f a env = + Sign.fold_var_context_reverse f a (var_context env) + let process_var_context f env = Sign.fold_var_context (fun d env -> f env d) (var_context env) (reset_context env) diff --git a/kernel/environ.mli b/kernel/environ.mli index 42d560ec90..dc733b3b44 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -56,6 +56,9 @@ val map_context : (constr -> constr) -> env -> env val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a val process_var_context : (env -> var_declaration -> env) -> env -> env +(* Recurrence on [var_context] starting from younger decl *) +val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> env -> 'a + (* [process_var_context_both_sides f env] iters [f] on the var declarations of [env] taking as argument both the initial segment, the middle value and the tail segment *) diff --git a/kernel/sign.ml b/kernel/sign.ml index 27aa150e62..d9438eb98a 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -43,6 +43,7 @@ let rec mem_var_context id = function | _ :: sign -> mem_var_context id sign | [] -> false let fold_var_context = List.fold_right +let fold_var_context_reverse = List.fold_left let fold_var_context_both_sides = list_fold_right_and_left let it_var_context_quantifier f = List.fold_left (fun c d -> f d c) diff --git a/kernel/sign.mli b/kernel/sign.mli index bb2e083de7..30e1dae28d 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -25,6 +25,7 @@ val ids_of_var_context : var_context -> identifier list val map_var_context : (constr -> constr) -> var_context -> var_context val mem_var_context : identifier -> var_context -> bool val fold_var_context : (var_declaration -> 'a -> 'a) -> var_context -> 'a -> 'a +val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> var_context -> 'a val fold_var_context_both_sides : ('a -> var_declaration -> var_context -> 'a) -> var_context -> 'a -> 'a val it_var_context_quantifier : diff --git a/kernel/term.ml b/kernel/term.ml index 9829c1154f..9e3ed34797 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -957,6 +957,12 @@ let substl laml = substn_many (Array.map make_substituend (Array.of_list laml)) 0 let subst1 lam = substl [lam] +let substl_decl laml (id,bodyopt,typ as d) = + match bodyopt with + | None -> (id,None,substl laml typ) + | Some body -> (id, Some (substl laml body), typed_app (substl laml) typ) +let subst1_decl lam = substl_decl [lam] + (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function @@ -1425,6 +1431,11 @@ let occur_var s c = in try occur_rec c; false with Occur -> true +let occur_var_in_decl hyp (_,c,typ) = + match c with + | None -> occur_var hyp (body_of_type typ) + | Some body -> occur_var hyp (body_of_type typ) || occur_var hyp body + (***************************************) (* alpha and eta conversion functions *) (***************************************) diff --git a/kernel/term.mli b/kernel/term.mli index fe26462dec..7bba6d924e 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -478,6 +478,9 @@ val substnl : constr list -> int -> constr -> constr val substl : constr list -> constr -> constr val subst1 : constr -> constr -> constr +val substl_decl : constr list -> var_declaration -> var_declaration +val subst1_decl : constr -> var_declaration -> var_declaration + (* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *) val global_vars : constr -> identifier list @@ -526,6 +529,8 @@ val occur_evar : existential_key -> constr -> bool in c, [false] otherwise *) val occur_var : identifier -> constr -> bool +val occur_var_in_decl : identifier -> var_declaration -> bool + (* [dependent M N] is true iff M is eq\_constr with a subterm of N M is appropriately lifted through abstractions of N *) val dependent : constr -> constr -> bool |