* http://helm.cs.unibo.it/
*)
-let debug = true
+let debug = false
let debug_print s =
if debug then begin
prerr_endline "<NEW_TEXTUAL_PARSER>";
* thus be interpreted differently than others *)
let use_fresh_num_instances = false
+ (** does the lexer return COMMENT tokens? *)
+let return_comments = false
+
open Printf
open DisambiguateTypes
exception Parse_error of Token.flocation * string
+let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments ()
+
let fresh_num_instance =
let n = ref 0 in
if use_fresh_num_instances then
let term = CicUtil.term_of_uri uri in
(uri, (fun _ _ _ -> term))
-let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
+let grammar = Grammar.gcreate cic_lexer
let term = Grammar.Entry.create grammar "term"
let term0 = Grammar.Entry.create grammar "term0"
let idents = match idents with None -> [] | Some idents -> idents in
return_tactic loc (TacticAst.Intros (num, idents))
| [ IDENT "intro" | IDENT "Intro" ] ->
- return_tactic loc (TacticAst.Intros (Some 1, []))
+ return_tactic loc (TacticAst.Intros (None, []))
| [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
| [ "let" | "Let" ];
t = tactic_term; "in"; where = IDENT ->
[ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
| "sequence" LEFTA
[ tactics = LIST1 NEXT SEP SYMBOL ";" ->
- return_tactical loc (TacticAst.Seq tactics)
+ (match tactics with
+ | [tactic] -> tactic
+ | _ -> return_tactical loc (TacticAst.Seq tactics))
]
| "then" NONA
[ tac = tactical;
print_kind: [
[ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
-> `Env
+ | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ]
+ -> `Coer
] ];
command: [
];
script_entry: [
[ cmd = tactical0 -> Command cmd
- | s = COMMENT -> Comment (loc, s)
+(* | s = COMMENT -> Comment (loc, s) *)
]
];
script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ];
let empty = ""
- let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
+ let aliases_grammar = Grammar.gcreate cic_lexer
let aliases = Grammar.Entry.create aliases_grammar "aliases"
let to_string env =