ProofEngineTypes.proof * Cic.metasenv
val subst_meta_and_metasenv_in_proof :
ProofEngineTypes.proof ->
- int -> (Cic.term -> Cic.term) -> Cic.metasenv ->
+ int -> Cic.substitution -> Cic.metasenv ->
ProofEngineTypes.proof * Cic.metasenv
(* returns the list of goals that are in newmetasenv and were not in
* *)
val select:
metasenv:Cic.metasenv ->
+ subst:Cic.substitution ->
ugraph:CicUniv.universe_graph ->
conjecture:Cic.conjecture ->
pattern:ProofEngineTypes.lazy_pattern ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph *
[ `Decl of (Cic.context * Cic.term) list
- | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option
+ | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list
] option list *
(Cic.context * Cic.term) list
?equality:(Cic.context -> Cic.term -> Cic.term -> bool) ->
Cic.term -> Cic.conjecture -> (Cic.context * Cic.term) list
-(* saturate_term newmeta metasenv context ty goal_arity *)
-(* Given a type [ty] (a backbone), it returns its suffix of length *)
-(* [goal_arity] head and a new metasenv in which there is new a META for each *)
-(* hypothesis, a list of arguments for the new applications and the index of *)
-(* the last new META introduced. The nth argument in the list of arguments is *)
-(* just the nth new META. *)
-val saturate_term:
- int -> Cic.metasenv -> Cic.context -> Cic.term -> int ->
- Cic.term * Cic.metasenv * Cic.term list * int
-
(* returns the index and the type of a premise in a context *)
val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
+(* orders a metasenv w.r.t. dependency among metas *)
+val sort_metasenv: Cic.metasenv -> Cic.metasenv
+
+(* finds an hypothesis by name in the context *)
+val find_hyp: string -> Cic.context -> Cic.term * Cic.term
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+val sort_pattern_hyps:
+ Cic.context -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.lazy_pattern
+
+
+(* FG: some helper functions ************************************************)
+
+val get_name: Cic.context -> int -> string option
+
+val get_rel: Cic.context -> string -> Cic.term option
+
+(* split_with_whd (c, t) takes a type t typed in the context c and returns
+ [(c_0, t_0); (c_1, t_1); ...; (c_n, t_n)], n where t_0 is the conclusion of
+ t and t_i is the premise of t accessed by Rel i in t_0.
+ Performes a whd on the conclusion before giving up.
+ Each t_i is returned with a context c_i in wich it is typed
+ split_with_normalize (c, t) normalizes t before operating the split
+ whd is useless here
+*)
+val split_with_whd: Cic.context * Cic.term ->
+ (Cic.context * Cic.term) list * int
+val split_with_normalize: Cic.context * Cic.term ->
+ (Cic.context * Cic.term) list * int