Initial implementation of statuses using objects in place of nested records.

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.mli

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index b04aa3cde54530fea0e1c1419a9cda97aa8c9bb8..11fcbab1dd785294af545ba9745ddb5135d53276 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,24 +25,54 @@
 
 exception BaseUriNotSetYet
 
+type tactic = 
+ (CicNotationPt.term, CicNotationPt.term, 
+  CicNotationPt.term GrafiteAst.reduction, string) 
+   GrafiteAst.tactic
+
+type lazy_tactic = 
+  (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
+    GrafiteAst.tactic
+
 val disambiguate_tactic:
  LexiconEngine.status ref ->
  Cic.context ->
- Cic.metasenv ->
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic ->
-  Cic.metasenv *
-   (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic
+ Cic.metasenv -> int option ->
+ tactic Disambiguate.disambiguator_input ->
+  Cic.metasenv * lazy_tactic
 
 val disambiguate_command: 
- LexiconEngine.status ->
- baseuri:string option ->
+ NEstatus.extra_status ->
+ ?baseuri:string ->
  Cic.metasenv ->
-  CicNotationPt.obj GrafiteAst.command ->
-  LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command
+ ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
+  NEstatus.extra_status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_macro:
  LexiconEngine.status ref ->
  Cic.metasenv ->
  Cic.context ->
-  CicNotationPt.term GrafiteAst.macro ->
-  Cic.metasenv * Cic.term GrafiteAst.macro
+ ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->
+  Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro
+
+val disambiguate_nterm :
+ NCic.term option -> 
+ NEstatus.extra_status ->
+ NCic.context -> NCic.metasenv -> NCic.substitution ->
+ CicNotationPt.term Disambiguate.disambiguator_input ->
+   NCic.metasenv * NCic.substitution * NEstatus.extra_status * NCic.term
+
+val disambiguate_nobj :
+ NEstatus.extra_status ->
+ ?baseuri:string ->
+ (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
+  NEstatus.extra_status * NCic.obj
+
+type pattern = 
+  CicNotationPt.term Disambiguate.disambiguator_input option * 
+  (string * NCic.term) list * NCic.term option
+
+val disambiguate_npattern:
+  GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
+    
+