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 (*
  15
  16 exception MetaSubstFailure of string Lazy.t
  17 exception Uncertain of string Lazy.t
  18 exception AssertFailure of string Lazy.t
  19 exception DeliftingARelWouldCaptureAFreeVariable;;
  20
  21 (* The entry (i,t) in a substitution means that *)
  22 (* (META i) have been instantiated with t.      *)
  23 (* type substitution = (int * (Cic.context * Cic.term)) list *)
  24
  25   (** @raise SubstNotFound *)
  26
  27 (* apply_subst subst t                     *)
  28 (* applies the substitution [subst] to [t] *)
  29 (* [subst] must be already unwinded        *)
  30
  31 val apply_subst : Cic.substitution -> Cic.term -> Cic.term
  32 val apply_subst_context : Cic.substitution -> Cic.context -> Cic.context
  33 val apply_subst_metasenv: Cic.substitution -> Cic.metasenv -> Cic.metasenv
  34
  35 (*** delifting ***)
  36
  37 val delift :
  38   int -> Cic.substitution -> Cic.context -> Cic.metasenv ->
  39   (Cic.term option) list -> Cic.term ->
  40     Cic.term * Cic.metasenv * Cic.substitution
  41 val restrict :
  42   Cic.substitution -> (int * int) list -> Cic.metasenv ->
  43   Cic.metasenv * Cic.substitution
  44
  45 (** delifts the Rels in t of n
  46  *  @raise DeliftingARelWouldCaptureAFreeVariable
  47  *)
  48 val delift_rels :
  49  Cic.substitution -> Cic.metasenv -> int -> Cic.term ->
  50   Cic.term * Cic.substitution * Cic.metasenv
  51
  52 (** {2 Pretty printers} *)
  53 val use_low_level_ppterm_in_context : bool ref
  54 val set_ppterm_in_context :
  55  (metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context ->
  56    string) -> unit
  57
  58 val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string
  59 val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string
  60 val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string
  61 val ppcontext:
  62  metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context ->
  63    string
  64 val ppterm_in_name_context:
  65  metasenv:Cic.metasenv -> Cic.substitution -> Cic.term ->
  66   (Cic.name option) list -> string
  67 val ppterm_in_context:
  68  metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string
  69 val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string
  70
  71 (** {2 Format-like pretty printers}
  72  * As above with prototypes suitable for toplevel/ocamldebug printers. No
  73  * subsitutions are applied here since such printers are required to be invoked
  74  * with only one argument.
  75  *)
  76
  77 val fppsubst: Format.formatter -> Cic.substitution -> unit
  78 val fppterm: Format.formatter -> Cic.term -> unit
  79 val fppmetasenv: Format.formatter -> Cic.metasenv -> unit
  80
  81 (*
  82 (* DEBUG *)
  83 val print_counters: unit -> unit
  84 val reset_counters: unit -> unit
  85 *)
  86
  87 (* val clean_up_meta :
  88   Cic.substitution -> Cic.metasenv -> Cic.term -> Cic.term
  89 *)
  90 *)