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
17 (* the delift function takes in input a metavariable index, a local_context
18 * and a term t, and substitutes every Rel in t with its position in
19 * the local_context (which is the Rel moved to the canonical context).
20 * Typically, the list of optional terms is the explicit
21 * substitution that is applied to a metavariable occurrence and the result of
22 * the delift function is a term the implicit variable can be substituted with
23 * to make the term [t] unifiable with the metavariable occurrence. In general,
24 * the problem is undecidable if we consider equivalence in place of alpha
25 * convertibility. Our implementation, though, is even weaker than alpha
26 * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
27 * (missing all the other cases). Does this matter in practice?
28 * The metavariable index is the index of the metavariable that must not occur
29 * in the term (for occur check).
32 unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
33 NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
34 NCic.metasenv -> NCic.substitution -> NCic.context ->
35 int -> NCic.local_context -> NCic.term ->
36 (NCic.metasenv * NCic.substitution) * NCic.term
41 int -> int list -> NCic.metasenv * NCic.substitution * int
43 (* bool = true if the type of the new meta is closed *)
46 NCic.metasenv -> NCic.context ->
47 [ `WithType of NCic.term | `Term | `Type | `Sort ] ->
48 NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
50 (* returns the resulting type, the metasenv and the arguments *)
52 ?delta:int -> NCic.metasenv -> NCic.substitution ->
53 NCic.context -> NCic.term -> int ->
54 NCic.term * NCic.metasenv * NCic.term list
56 val flexible: NCic.substitution -> NCic.term list -> bool
58 val in_scope_tag : string
59 val out_scope_tag : int -> string
60 val is_out_scope_tag : string -> bool
61 val int_of_out_scope_tag : string -> int