(* the index of the last created meta *)
val maxmeta: unit -> int
+(* Bad, this should be made functional and put in the status! *)
+val pushmaxmeta: unit -> unit
+val popmaxmeta: unit -> unit
+
(* the delift function takes in input a metavariable index, a local_context
* and a term t, and substitutes every subterm t' of t with its position
* (searched up-to unification) in
* the delift function is a term the implicit variable can be substituted with
* to make the term [t] unifiable with the metavariable occurrence. In general,
* the problem is undecidable if we consider equivalence in place of alpha
- * convertibility. Our implementation, though, is even weaker than alpha
+ * convertibility.
+ * The old implementation, though, is even weaker than alpha
* convertibility, since it replace the term [tk] if and only if [tk] is a Rel
* (missing all the other cases). Does this matter in practice?
+ * The new experimental implementation, instead, works up to unification.
* The metavariable index is the index of the metavariable that must not occur
* in the term (for occur check).
*)
val delift :
+ #NCic.status ->
unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
additional (i.e. l' does not intersects l) positions whose restriction was
forced because of type dependencies *)
val restrict:
+ #NCic.status ->
NCic.metasenv ->
NCic.substitution ->
int -> int list ->
(* returns the resulting type, the metasenv and the arguments *)
val saturate:
+ #NCic.status ->
?delta:int -> NCic.metasenv -> NCic.substitution ->
NCic.context -> NCic.term -> int ->
NCic.term * NCic.metasenv * NCic.term list
val is_out_scope_tag : NCic.meta_attrs -> bool
val int_of_out_scope_tag : NCic.meta_attrs -> int
+
+val is_flexible:
+ #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool