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