(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)

exception Error of string lazy_t
val fail: string lazy_t -> 'a

type lowtac_status = {
        pstatus : NCic.obj;
        lstatus : LexiconEngine.status
}

type lowtactic = lowtac_status -> int -> lowtac_status 

type tac_status = {
        gstatus : Continuationals.Stack.t; 
        istatus : lowtac_status;
} 

type tactic = tac_status -> tac_status

type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input

type cic_term 
val ctx_of : cic_term -> NCic.context
val term_of_cic_term : 
      lowtac_status -> cic_term -> NCic.context -> lowtac_status * NCic.term

val mk_cic_term : NCic.context -> NCic.term -> cic_term
val disambiguate:
  lowtac_status -> tactic_term -> cic_term option -> NCic.context -> 
    lowtac_status * cic_term (* * cic_term XXX *)

val analyse_indty: 
  lowtac_status -> cic_term -> 
    lowtac_status * 
      (NReference.reference * int * NCic.term list * NCic.term list)

val ppterm: lowtac_status -> cic_term -> string
val whd: 
      lowtac_status -> ?delta:int -> NCic.context -> cic_term -> 
        lowtac_status * cic_term 
val normalize: 
      lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
        lowtac_status * cic_term 
val typeof: 
      lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
val unify: 
  lowtac_status -> NCic.context -> cic_term -> cic_term -> lowtac_status
val refine: 
  lowtac_status -> NCic.context -> cic_term -> cic_term option -> 
    lowtac_status * cic_term * cic_term (* status, term, type *)
val apply_subst:
  lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term

val get_goalty: lowtac_status -> int -> cic_term
val mk_meta: 
   lowtac_status -> ?name:string -> NCic.context ->
   [ `Decl of cic_term | `Def of cic_term ] ->
     lowtac_status * cic_term
val instantiate: lowtac_status -> int -> cic_term -> lowtac_status

val select_term:
  lowtac_status -> 
  found: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
  postprocess: (lowtac_status -> cic_term -> lowtac_status * cic_term) ->
  cic_term -> tactic_term option * NCic.term ->
    lowtac_status * cic_term

val mk_in_scope: lowtac_status -> cic_term -> lowtac_status * cic_term
val mk_out_scope: int -> lowtac_status -> cic_term -> lowtac_status * cic_term

val pp_tac_status: tac_status -> unit

(* end *)