module N = NotationPt
module G = GrafiteAst
-module L = LexiconAst
-module LE = LexiconEngine
-exception NoInclusionPerformed of string (* full path *)
-
-type 'a localized_option =
- LSome of 'a
- | LNone of G.loc
-
-type ast_statement = G.statement
-
-type 'status statement =
- ?never_include:bool ->
- (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *)
- include_paths:string list -> (#LE.status as 'status) ->
- 'status * ast_statement localized_option
-
-type 'status parser_status = {
- grammar : Grammar.g;
- term : N.term Grammar.Entry.e;
- statement : #LE.status as 'status statement Grammar.Entry.e;
-}
-
-let grafite_callback = ref (fun _ -> ())
-let set_grafite_callback cb = grafite_callback := cb
-
-let lexicon_callback = ref (fun _ -> ())
-let set_lexicon_callback cb = lexicon_callback := cb
-
-let initial_parser () =
- let grammar = CicNotationParser.level2_ast_grammar () in
- let term = CicNotationParser.term () in
- let statement = Grammar.Entry.create grammar "statement" in
- { grammar = grammar; term = term; statement = statement }
-;;
+let exc_located_wrapper f =
+ try
+ f ()
+ with
+ | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
+ | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
+ | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
+ raise (HExtlib.Localized
+ (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
+ | Stdpp.Exc_located (floc, exn) ->
+ raise (HExtlib.Localized
+ (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
-let grafite_parser = ref (initial_parser ())
+let parse_statement grafite_parser lexbuf =
+ exc_located_wrapper
+ (fun () -> (Grammar.Entry.parse (Obj.magic grafite_parser) (Obj.magic lexbuf)))
let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
| BYC_letsuchthat of string * N.term * string * N.term
| BYC_wehaveand of string * N.term * string * N.term
-let initialize_parser () =
+let mk_parser statement lstatus =
+(* let grammar = CicNotationParser.level2_ast_grammar lstatus in *)
+ let term = CicNotationParser.term lstatus in
+ let let_defs = CicNotationParser.let_defs lstatus in
+ let protected_binder_vars = CicNotationParser.protected_binder_vars lstatus in
(* {{{ parser initialization *)
- let term = !grafite_parser.term in
- let statement = !grafite_parser.statement in
- let let_defs = CicNotationParser.let_defs () in
- let protected_binder_vars = CicNotationParser.protected_binder_vars () in
EXTEND
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90" -> t ] ];
+(* MATITA 1.0
new_name: [
[ SYMBOL "_" -> None
| id = IDENT -> Some id ]
];
- ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
+*)
ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
tactic_term_list1: [
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
- reduction_kind: [
- [ IDENT "normalize" -> `Normalize
- | IDENT "simplify" -> `Simpl
- | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
- | IDENT "whd" -> `Whd ]
- ];
nreduction_kind: [
[ IDENT "normalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
let delta = match delta with None -> true | _ -> false in
| SYMBOL "<" -> `RightToLeft ]
];
int: [ [ num = NUMBER -> int_of_string num ] ];
- intros_names: [
- [ idents = OPT ident_list0 ->
- match idents with None -> [] | Some idents -> idents
- ]
- ];
+(* MATITA 1.0
intros_spec: [
[ OPT [ IDENT "names" ];
num = OPT [ num = int -> num ];
num, idents
]
];
- using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
+*)
+(* MATITA 1.0 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; *)
ntactic: [
[ SYMBOL "@"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
| IDENT "apply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
]
];
+(* MATITA 1.0
by_continuation: [
[ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
| WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
BYC_wehaveand (id1,t1,id2,t2)
]
];
+*)
+(* MATITA 1.0
rewriting_step_continuation : [
[ "done" -> true
| -> false
]
];
+*)
(* MATITA 1.0
atomic_tactical:
[ "sequence" LEFTA
if (try ignore (NReference.reference_of_string uri); true
with NReference.IllFormedReference _ -> false)
then
- L.Ident_alias (id, uri)
+ G.Ident_alias (id, uri)
else
raise
(HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
let instance =
match instance with Some i -> i | None -> 0
in
- L.Symbol_alias (symbol, instance, dsc)
+ G.Symbol_alias (symbol, instance, dsc)
| IDENT "num";
instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
SYMBOL "="; dsc = QSTRING ->
let instance =
match instance with Some i -> i | None -> 0
in
- L.Number_alias (instance, dsc)
+ G.Number_alias (instance, dsc)
]
];
argument: [
p2 =
[ blob = UNPARSED_AST ->
add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
- (CicNotationParser.parse_level2_ast
+ (CicNotationParser.parse_level2_ast lstatus
(Ulexing.from_utf8_string blob))
| blob = UNPARSED_META ->
add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
- (CicNotationParser.parse_level2_meta
+ (CicNotationParser.parse_level2_meta lstatus
(Ulexing.from_utf8_string blob))
] ->
let assoc =
in
let p1 =
add_raw_attribute ~text:s
- (CicNotationParser.parse_level1_pattern prec
+ (CicNotationParser.parse_level1_pattern lstatus prec
(Ulexing.from_utf8_string s))
in
(dir, p1, assoc, prec, p2)
include_command: [ [
IDENT "include" ; path = QSTRING ->
- loc,path,true,L.WithPreferences
- | IDENT "include" ; IDENT "source" ; path = QSTRING ->
- loc,path,false,L.WithPreferences
+ loc,path,G.WithPreferences
| IDENT "include'" ; path = QSTRING ->
- loc,path,true,L.WithoutPreferences
+ loc,path,G.WithoutPreferences
]];
grafite_ncommand: [ [
m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
G.NCopy (loc,s,NUri.uri_of_string u,
List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
+ | lc = lexicon_command -> lc
]];
lexicon_command: [ [
IDENT "alias" ; spec = alias_spec ->
- L.Alias (loc, spec)
+ G.Alias (loc, spec)
| IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
- L.Notation (loc, dir, l1, assoc, prec, l2)
+ G.Notation (loc, dir, l1, assoc, prec, l2)
| IDENT "interpretation"; id = QSTRING;
(symbol, args, l3) = interpretation ->
- L.Interpretation (loc, id, (symbol, args), l3)
+ G.Interpretation (loc, id, (symbol, args), l3)
]];
executable: [
[ ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
]
];
statement: [
- [ ex = executable ->
- fun ?(never_include=false) ~include_paths status ->
- let stm = G.Executable (loc, ex) in
- !grafite_callback stm;
- status, LSome stm
- | com = comment ->
- fun ?(never_include=false) ~include_paths status ->
- let stm = G.Comment (loc, com) in
- !grafite_callback stm;
- status, LSome stm
- | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
- fun ?(never_include=false) ~include_paths status ->
- let _root, buri, fullpath, _rrelpath =
- Librarian.baseuri_of_script ~include_paths fname in
- if never_include then raise (NoInclusionPerformed fullpath)
- else
- begin
- let stm =
- G.Executable
- (loc, G.Command (loc, G.Include (iloc,fname))) in
- !grafite_callback stm;
- let status =
- LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
- let stm =
- G.Executable
- (loc,G.Command (loc,G.Include (iloc,buri)))
- in
- status, LSome stm
- end
- | scom = lexicon_command ; SYMBOL "." ->
- fun ?(never_include=false) ~include_paths status ->
- !lexicon_callback scom;
- let status = LE.eval_command status scom in
- status, LNone loc
+ [ ex = executable -> G.Executable (loc, ex)
+ | com = comment -> G.Comment (loc, com)
+ | (iloc,fname,mode) = include_command ; SYMBOL "." ->
+ G.Executable (loc,G.NCommand (loc,G.Include (iloc,mode,fname)))
| EOI -> raise End_of_file
]
];
-END
+ END;
(* }}} *)
+ statement
;;
-let _ = initialize_parser () ;;
+type db = GrafiteAst.statement Grammar.Entry.e ;;
-let exc_located_wrapper f =
- try
- f ()
- with
- | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
- | Stdpp.Exc_located (floc, Stream.Error msg) ->
- raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
- | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
- raise
- (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
- | Stdpp.Exc_located (floc, exn) ->
- raise
- (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
-
-let parse_statement lexbuf =
- exc_located_wrapper
- (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
+class type g_status =
+ object
+ inherit CicNotationParser.g_status
+ method parser_db: db
+ end
-let statement () = Obj.magic !grafite_parser.statement
+class status =
+ object(self)
+ inherit CicNotationParser.status ~keywords:[]
+ val mutable db = None
+ method parser_db = match db with None -> assert false | Some x -> x
+ method set_parser_db v = {< db = Some v >}
+ method set_parser_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< db = Some o#parser_db >}#set_notation_parser_status o
+ initializer
+ let grammar = CicNotationParser.level2_ast_grammar self in
+ db <- Some (mk_parser (Grammar.Entry.create grammar "statement") self)
+ end
-let history = ref [] ;;
-
-let push () =
- LexiconSync.push ();
- history := !grafite_parser :: !history;
- grafite_parser := initial_parser ();
- initialize_parser ()
+let extend status l1 action =
+ let status = CicNotationParser.extend status l1 action in
+ let grammar = CicNotationParser.level2_ast_grammar status in
+ status#set_parser_db
+ (mk_parser (Grammar.Entry.create grammar "statement") status)
;;
-let pop () =
- LexiconSync.pop ();
- match !history with
- | [] -> assert false
- | gp :: tail ->
- grafite_parser := gp;
- history := tail
-;;
-
-(* vim:set foldmethod=marker: *)
+let parse_statement status =
+ parse_statement status#parser_db
+(* vim:set foldmethod=marker: *)
projects / helm.git / blobdiff