2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 exception MetaSubstFailure of string Lazy.t
15 exception Uncertain of string Lazy.t
19 (* the index of the last created meta *)
20 val maxmeta: unit -> int
22 (* the delift function takes in input a metavariable index, a local_context
23 * and a term t, and substitutes every subterm t' of t with its position
24 * (searched up-to unification) in
25 * the local_context (which is the Rel moved to the canonical context).
26 * Typically, the list of optional terms is the explicit
27 * substitution that is applied to a metavariable occurrence and the result of
28 * the delift function is a term the implicit variable can be substituted with
29 * to make the term [t] unifiable with the metavariable occurrence. In general,
30 * the problem is undecidable if we consider equivalence in place of alpha
31 * convertibility. Our implementation, though, is even weaker than alpha
32 * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
33 * (missing all the other cases). Does this matter in practice?
34 * The metavariable index is the index of the metavariable that must not occur
35 * in the term (for occur check).
38 unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
39 NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
40 NCic.metasenv -> NCic.substitution -> NCic.context ->
41 int -> NCic.local_context -> NCic.term ->
42 (NCic.metasenv * NCic.substitution) * NCic.term
47 int -> int list -> NCic.metasenv * NCic.substitution * int
49 (* bool = true if the type of the new meta is closed *)
51 ?attrs:NCic.meta_attrs ->
52 NCic.metasenv -> NCic.context ->
53 ?with_type:NCic.term -> NCicUntrusted.meta_kind ->
54 NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
56 (* extend_meta m n: n must be in m *)
57 val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
59 (* returns the resulting type, the metasenv and the arguments *)
61 ?delta:int -> NCic.metasenv -> NCic.substitution ->
62 NCic.context -> NCic.term -> int ->
63 NCic.term * NCic.metasenv * NCic.term list
65 val is_out_scope_tag : NCic.meta_attrs -> bool
66 val int_of_out_scope_tag : NCic.meta_attrs -> int