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 (* Bad, this should be made functional and put in the status! *)
  23 val pushmaxmeta: unit -> unit
  24 val popmaxmeta: unit -> unit
  25
  26 (* the delift function takes in input a metavariable index, a local_context
  27  * and a term t, and substitutes every subterm t' of t with its position
  28  * (searched up-to unification) in
  29  * the local_context (which is the Rel moved to the canonical context).
  30  * Typically, the list of optional terms is the explicit
  31  * substitution that is applied to a metavariable occurrence and the result of
  32  * the delift function is a term the implicit variable can be substituted with
  33  * to make the term [t] unifiable with the metavariable occurrence.  In general,
  34  * the problem is undecidable if we consider equivalence in place of alpha
  35  * convertibility.
  36  * The old implementation, though, is even weaker than alpha
  37  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
  38  * (missing all the other cases). Does this matter in practice?
  39  * The new experimental implementation, instead, works up to unification.
  40  * The metavariable index is the index of the metavariable that must not occur
  41  * in the term (for occur check).
  42  *)
  43 val delift :
  44   #NCic.status ->
  45   unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
  46     NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
  47   NCic.metasenv -> NCic.substitution -> NCic.context ->
  48   int -> NCic.local_context -> NCic.term ->
  49     (NCic.metasenv * NCic.substitution) * NCic.term
  50
  51 (* restrict metasenv subst n l
  52    returns metasenv, subst, created meta and l' where l' is the list of
  53    additional (i.e. l' does not intersects l) positions whose restriction was
  54    forced because of type dependencies *)
  55 val restrict:
  56    #NCic.status ->
  57     NCic.metasenv ->
  58     NCic.substitution ->
  59     int -> int list ->
  60      NCic.metasenv * NCic.substitution * int * int list
  61
  62 (* bool = true if the type of the new meta is closed *)
  63 val mk_meta:
  64    ?attrs:NCic.meta_attrs ->
  65    NCic.metasenv -> NCic.context ->
  66     ?with_type:NCic.term -> NCicUntrusted.meta_kind ->
  67     NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
  68
  69 (* extend_meta m n: n must be in m *)
  70 val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
  71
  72 (* returns the resulting type, the metasenv and the arguments *)
  73 val saturate:
  74    #NCic.status ->
  75     ?delta:int -> NCic.metasenv -> NCic.substitution ->
  76     NCic.context -> NCic.term -> int ->
  77        NCic.term * NCic.metasenv * NCic.term list
  78
  79 val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind
  80
  81 val is_out_scope_tag : NCic.meta_attrs -> bool
  82 val int_of_out_scope_tag : NCic.meta_attrs -> int
  83
  84 val is_flexible:
  85  #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool