* 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_defs:[
[ defs = LIST1 [
- var = typed_name;
+ name = IDENT;
args = LIST1 [
PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
ty = term; PAREN ")" ->
(names, ty)
];
index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
+ ty = OPT [ SYMBOL ":" ; t = term -> t ];
SYMBOL <:unicode<def>> (* ≝ *);
t1 = term ->
- let rec list_of_lambda ty final_term = function
+ let rec list_of_binder binder ty final_term = function
| [] -> final_term
| name::tl ->
- CicAst.Binder (`Lambda, (Cic.Name name, Some ty),
- list_of_lambda ty final_term tl)
+ CicAst.Binder (binder, (Cic.Name name, Some ty),
+ list_of_binder binder ty final_term tl)
in
- let rec lambda_of_arg_list final_term = function
+ let rec binder_of_arg_list binder final_term = function
| [] -> final_term
| (l,ty)::tl ->
- list_of_lambda ty (lambda_of_arg_list final_term tl) l
+ list_of_binder binder ty
+ (binder_of_arg_list binder final_term tl) l
+ in
+ let t1' = binder_of_arg_list `Lambda t1 args in
+ let ty' =
+ match ty with
+ | None -> None
+ | Some ty -> Some (binder_of_arg_list `Pi ty args)
in
- let t1' = lambda_of_arg_list t1 args in
let rec get_position_of name n = function
| [] -> (None,n)
| nam::tl ->
| None -> 0
| (Some name) -> find_arg name 0 args)
in
- (var, t1', index)
+ ((Cic.Name name,ty'), t1', index)
] SEP "and" -> defs
]];
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
print_kind: [
[ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
-> `Env
+ | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ]
+ -> `Coer
] ];
command: [
return_command loc (TacticAst.Redo (int_opt steps))
| [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING ->
return_command loc (TacticAst.Baseuri uri)
+ | [ IDENT "basedir" | IDENT "Basedir" ]; uri = OPT QSTRING ->
+ return_command loc (TacticAst.Basedir uri)
| [ IDENT "check" | IDENT "Check" ]; t = term ->
return_command loc (TacticAst.Check t)
(*
];
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 =