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.
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_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
14 exception Error of string lazy_t
15 val fail: string lazy_t -> 'a
17 type lowtac_status = {
19 lstatus : LexiconEngine.status
22 type lowtactic = lowtac_status -> int -> lowtac_status
25 gstatus : Continuationals.Stack.t;
26 istatus : lowtac_status;
29 type tactic = tac_status -> tac_status
31 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
32 type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
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
39 val mk_cic_term : NCic.context -> NCic.term -> cic_term
41 lowtac_status -> tactic_term -> cic_term option -> NCic.context ->
42 lowtac_status * cic_term (* * cic_term XXX *)
45 lowtac_status -> cic_term ->
47 (NReference.reference * int * NCic.term list * NCic.term list)
49 val ppterm: lowtac_status -> cic_term -> string
51 lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
52 lowtac_status * cic_term
54 lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
55 lowtac_status * cic_term
57 lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
59 lowtac_status -> NCic.context -> cic_term -> cic_term -> lowtac_status
61 lowtac_status -> NCic.context -> cic_term -> cic_term option ->
62 lowtac_status * cic_term * cic_term (* status, term, type *)
64 lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
66 val get_goalty: lowtac_status -> int -> cic_term
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
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
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
83 val pp_tac_status: tac_status -> unit