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 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. Our implementation, though, is even weaker than alpha
  32  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
  33  * (missing all the other cases). Does this matter in practice?
  34  * The metavariable index is the index of the metavariable that must not occur
  35  * in the term (for occur check).
  36  *)
  37 val delift :
  38   unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
  39     NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
  40   NCic.metasenv -> NCic.substitution -> NCic.context ->
  41   int -> NCic.local_context -> NCic.term ->
  42     (NCic.metasenv * NCic.substitution) * NCic.term
  43
  44 (* restrict metasenv subst n l
  45    returns metasenv, subst, created meta and l' where l' is the list of
  46    additional (i.e. l' does not intersects l) positions whose restriction was
  47    forced because of type dependencies *)
  48 val restrict:
  49     NCic.metasenv ->
  50     NCic.substitution ->
  51     int -> int list ->
  52      NCic.metasenv * NCic.substitution * int * int list
  53
  54 (* bool = true if the type of the new meta is closed *)
  55 val mk_meta:
  56    ?attrs:NCic.meta_attrs ->
  57    NCic.metasenv -> NCic.context ->
  58     ?with_type:NCic.term -> NCicUntrusted.meta_kind ->
  59     NCic.metasenv * int * NCic.term * NCic.term (* menv,metano,instance,type *)
  60
  61 (* extend_meta m n: n must be in m *)
  62 val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
  63
  64 (* returns the resulting type, the metasenv and the arguments *)
  65 val saturate:
  66     ?delta:int -> NCic.metasenv -> NCic.substitution ->
  67     NCic.context -> NCic.term -> int ->
  68        NCic.term * NCic.metasenv * NCic.term list
  69
  70 val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind
  71
  72 val is_out_scope_tag : NCic.meta_attrs -> bool
  73 val int_of_out_scope_tag : NCic.meta_attrs -> int
  74
  75 val is_flexible : NCic.context -> subst:NCic.substitution -> NCic.term -> bool