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 #NCicEnvironment.status ->
39 unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
40 NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
41 NCic.metasenv -> NCic.substitution -> NCic.context ->
42 int -> NCic.local_context -> NCic.term ->
43 (NCic.metasenv * NCic.substitution) * NCic.term
45 (* restrict metasenv subst n l
46 returns metasenv, subst, created meta and l' where l' is the list of
47 additional (i.e. l' does not intersects l) positions whose restriction was
48 forced because of type dependencies *)
50 #NCicEnvironment.status ->
54 NCic.metasenv * NCic.substitution * int * int list
56 (* bool = true if the type of the new meta is closed *)
58 ?attrs:NCic.meta_attrs ->
59 NCic.metasenv -> NCic.context ->
60 ?with_type:NCic.term -> NCicUntrusted.meta_kind ->
61 NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
63 (* extend_meta m n: n must be in m *)
64 val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
66 (* returns the resulting type, the metasenv and the arguments *)
68 #NCicEnvironment.status ->
69 ?delta:int -> NCic.metasenv -> NCic.substitution ->
70 NCic.context -> NCic.term -> int ->
71 NCic.term * NCic.metasenv * NCic.term list
73 val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind
75 val is_out_scope_tag : NCic.meta_attrs -> bool
76 val int_of_out_scope_tag : NCic.meta_attrs -> int
79 #NCicEnvironment.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool