]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_refiner/nCicMetaSubst.mli
Sig in Prop
[helm.git] / matita / components / ng_refiner / nCicMetaSubst.mli
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 (* $Id$ *)
13
14 exception MetaSubstFailure of string Lazy.t
15 exception Uncertain of string Lazy.t
16
17 val debug: bool ref
18
19 (* the index of the last created meta *)
20 val maxmeta: unit -> int
21
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.
32  * The old implementation, though, is even weaker than alpha
33  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
34  * (missing all the other cases). Does this matter in practice?
35  * The new experimental implementation, instead, works up to unification.
36  * The metavariable index is the index of the metavariable that must not occur
37  * in the term (for occur check).
38  *)
39 val delift : 
40   #NCic.status ->
41   unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
42     NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) -> 
43   NCic.metasenv -> NCic.substitution -> NCic.context -> 
44   int -> NCic.local_context -> NCic.term ->
45     (NCic.metasenv * NCic.substitution) * NCic.term
46
47 (* restrict metasenv subst n l
48    returns metasenv, subst, created meta and l' where l' is the list of
49    additional (i.e. l' does not intersects l) positions whose restriction was
50    forced because of type dependencies *)
51 val restrict: 
52    #NCic.status ->
53     NCic.metasenv ->
54     NCic.substitution ->
55     int -> int list ->
56      NCic.metasenv * NCic.substitution * int * int list
57
58 (* bool = true if the type of the new meta is closed *)
59 val mk_meta: 
60    ?attrs:NCic.meta_attrs -> 
61    NCic.metasenv -> NCic.context -> 
62     ?with_type:NCic.term -> NCicUntrusted.meta_kind ->
63     NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
64
65 (* extend_meta m n: n must be in m *)
66 val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
67
68 (* returns the resulting type, the metasenv and the arguments *)
69 val saturate:
70    #NCic.status ->
71     ?delta:int -> NCic.metasenv -> NCic.substitution -> 
72     NCic.context -> NCic.term -> int ->
73        NCic.term * NCic.metasenv * NCic.term list
74
75 val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind
76
77 val is_out_scope_tag : NCic.meta_attrs -> bool
78 val int_of_out_scope_tag : NCic.meta_attrs -> int
79
80 val is_flexible:
81  #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool