]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_refiner/nCicMetaSubst.mli
freescale porting, work in progress
[helm.git] / helm / software / 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 (* the index of the last created meta *)
18 val maxmeta: unit -> int
19
20 (* the delift function takes in input a metavariable index, a local_context
21  * and a term t, and substitutes every subterm t' of t with its position 
22  * (searched up-to unification) in
23  * the local_context (which is the Rel moved to the canonical context).
24  * Typically, the list of optional terms is the explicit
25  * substitution that is applied to a metavariable occurrence and the result of
26  * the delift function is a term the implicit variable can be substituted with
27  * to make the term [t] unifiable with the metavariable occurrence.  In general,
28  * the problem is undecidable if we consider equivalence in place of alpha
29  * convertibility. Our implementation, though, is even weaker than alpha
30  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
31  * (missing all the other cases). Does this matter in practice?
32  * The metavariable index is the index of the metavariable that must not occur
33  * in the term (for occur check).
34  *)
35 val delift : 
36   unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
37     NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) -> 
38   NCic.metasenv -> NCic.substitution -> NCic.context -> 
39   int -> NCic.local_context -> NCic.term ->
40     (NCic.metasenv * NCic.substitution) * NCic.term
41
42 val restrict: 
43     NCic.metasenv ->
44     NCic.substitution ->
45       int -> int list -> NCic.metasenv * NCic.substitution * int
46
47 (* bool = true if the type of the new meta is closed *)
48 val mk_meta: 
49    ?name:string -> 
50    NCic.metasenv -> NCic.context -> 
51     [ `WithType of NCic.term | `Term | `Type | `Sort ] -> 
52     NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
53
54 (* returns the resulting type, the metasenv and the arguments *)
55 val saturate:
56     ?delta:int -> NCic.metasenv -> NCic.substitution -> 
57     NCic.context -> NCic.term -> int ->
58        NCic.term * NCic.metasenv * NCic.term list
59
60 val in_scope_tag : string
61 val out_scope_tag : int -> string
62 val is_out_scope_tag : string -> bool
63 val int_of_out_scope_tag : string -> int