helm/software/components/ng_tactics/nTacStatus.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: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 exception Error of string lazy_t
  15 val fail: string lazy_t -> 'a
  16
  17 type lowtac_status = {
  18         pstatus : NCic.obj;
  19         lstatus : LexiconEngine.status
  20 }
  21
  22 type lowtactic = lowtac_status -> int -> lowtac_status
  23
  24 type tac_status = {
  25         gstatus : Continuationals.Stack.t;
  26         istatus : lowtac_status;
  27 }
  28
  29 type tactic = tac_status -> tac_status
  30
  31 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
  32 type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
  33
  34 type cic_term
  35 val ctx_of : cic_term -> NCic.context
  36 val term_of_cic_term :
  37       lowtac_status -> cic_term -> NCic.context -> lowtac_status * NCic.term
  38
  39 val mk_cic_term : NCic.context -> NCic.term -> cic_term
  40 val disambiguate:
  41   lowtac_status -> tactic_term -> cic_term option -> NCic.context ->
  42     lowtac_status * cic_term (* * cic_term XXX *)
  43
  44 val analyse_indty:
  45   lowtac_status -> cic_term ->
  46     lowtac_status *
  47       (NReference.reference * int * NCic.term list * NCic.term list)
  48
  49 val ppterm: lowtac_status -> cic_term -> string
  50 val whd:
  51       lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
  52         lowtac_status * cic_term
  53 val normalize:
  54       lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
  55         lowtac_status * cic_term
  56 val typeof:
  57       lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
  58 val unify:
  59   lowtac_status -> NCic.context -> cic_term -> cic_term -> lowtac_status
  60 val refine:
  61   lowtac_status -> NCic.context -> cic_term -> cic_term option ->
  62     lowtac_status * cic_term * cic_term (* status, term, type *)
  63 val apply_subst:
  64   lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
  65
  66 val get_goalty: lowtac_status -> int -> cic_term
  67 val mk_meta:
  68    lowtac_status -> ?name:string -> NCic.context ->
  69    [ `Decl of cic_term | `Def of cic_term ] ->
  70      lowtac_status * cic_term
  71 val instantiate: lowtac_status -> int -> cic_term -> lowtac_status
  72
  73 val select_term:
  74   lowtac_status ->
  75   found: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
  76   postprocess: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
  77   cic_term -> tactic_term option * NCic.term ->
  78     lowtac_status * cic_term
  79
  80 val mk_in_scope: lowtac_status -> cic_term -> lowtac_status * cic_term
  81 val mk_out_scope: int -> lowtac_status -> cic_term -> lowtac_status * cic_term
  82
  83 val pp_tac_status: tac_status -> unit
  84
  85 (* end *)