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