X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=b3bbaf3f8d94d68d3a6cfe6c8b4b90597273f744;hb=9c2f282765ec75a3c9aafc9e73e6626588891abe;hp=0dd5c0885e7a1ce6636cd6d765c4fb530b1d5e21;hpb=7e79f902b0fea9afb02576b653b384bc512b2264;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 0dd5c0885..b3bbaf3f8 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -48,10 +48,20 @@ type statement = LexiconEngine.status -> LexiconEngine.status * ast_statement localized_option -let grammar = CicNotationParser.level2_ast_grammar +type parser_status = { + grammar : Grammar.g; + term : CicNotationPt.term Grammar.Entry.e; + statement : statement Grammar.Entry.e; +} -let term = CicNotationParser.term -let statement = Grammar.Entry.create grammar "statement" +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 grafite_parser = ref (initial_parser ()) let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) @@ -92,6 +102,12 @@ type by_continuation = | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term +let initialize_parser () = + (* {{{ 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) ] ]; @@ -164,9 +180,20 @@ EXTEND ] ]; using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; + ntactic: [ + [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t) + | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> + GrafiteAst.NChange (loc, what, with_what) + | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> + GrafiteAst.NElim (loc, what, where) + | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n) + ] + ]; tactic: [ [ IDENT "absurd"; t = tactic_term -> GrafiteAst.Absurd (loc, t) + | IDENT "apply"; IDENT "rule"; t = tactic_term -> + GrafiteAst.ApplyRule (loc, t) | IDENT "apply"; t = tactic_term -> GrafiteAst.Apply (loc, t) | IDENT "applyP"; t = tactic_term -> @@ -209,12 +236,12 @@ EXTEND GrafiteAst.Destruct (loc, xts) | IDENT "elim"; what = tactic_term; using = using; pattern = OPT pattern_spec; - (num, idents) = intros_spec -> + ispecs = intros_spec -> let pattern = match pattern with | None -> None, [], Some Ast.UserInput | Some pattern -> pattern in - GrafiteAst.Elim (loc, what, using, pattern, (num, idents)) + GrafiteAst.Elim (loc, what, using, pattern, ispecs) | IDENT "elimType"; what = tactic_term; using = using; (num, idents) = intros_spec -> GrafiteAst.ElimType (loc, what, using, (num, idents)) @@ -444,6 +471,10 @@ EXTEND | IDENT "skip" -> GrafiteAst.Skip loc ] ]; + ntheorem_flavour: [ + [ [ IDENT "ntheorem" ] -> `Theorem + ] + ]; theorem_flavour: [ [ [ IDENT "definition" ] -> `Definition | [ IDENT "fact" ] -> `Fact @@ -459,7 +490,8 @@ EXTEND ] ]; inductive_spec: [ [ - fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars; + fst_name = IDENT; + params = LIST0 protected_binder_vars; SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; fst_constructors = LIST0 constructor SEP SYMBOL "|"; tl = OPT [ "with"; @@ -481,7 +513,8 @@ EXTEND ] ]; record_spec: [ [ - name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ; + name = IDENT; + params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; fields = LIST0 [ name = IDENT ; @@ -506,6 +539,8 @@ EXTEND macro: [ [ [ IDENT "check" ]; t = term -> GrafiteAst.Check (loc, t) + | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term -> + GrafiteAst.Eval (loc, kind, t) | [ IDENT "inline"]; style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; suri = QSTRING; prefix = OPT QSTRING; @@ -644,6 +679,9 @@ EXTEND GrafiteAst.Obj (loc, Ast.Theorem (`Variant,name,typ,Some (Ast.Ident (newname, None)))) + | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body)) | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body)) @@ -653,9 +691,9 @@ EXTEND Ast.Theorem (flavour, name, Ast.Implicit, Some body)) | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None)) - | LETCOREC ; defs = CicNotationParser.let_defs -> + | LETCOREC ; defs = let_defs -> mk_rec_corec `CoInductive defs loc - | LETREC ; defs = CicNotationParser.let_defs -> + | LETREC ; defs = let_defs -> mk_rec_corec `Inductive defs loc | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in @@ -676,6 +714,10 @@ EXTEND let composites = match composites with None -> true | Some _ -> false in GrafiteAst.Coercion (loc, t, composites, arity, saturations) + | IDENT "prefer" ; IDENT "coercion"; t = tactic_term -> + GrafiteAst.PreferCoercion (loc, t) + | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> + GrafiteAst.UnificationHint (loc, t, n) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> @@ -705,6 +747,10 @@ EXTEND | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical -> GrafiteAst.Tactic (loc, Some tac, punct) | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct) + | tac = ntactic; punct = punctuation_tactical -> + GrafiteAst.NTactic (loc, tac, punct) + | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical -> + GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct) | tac = non_punctuation_tactical; punct = punctuation_tactical -> GrafiteAst.NonPunctuationTactical (loc, tac, punct) | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac) @@ -721,7 +767,8 @@ EXTEND [ ex = executable -> fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex)) | com = comment -> - fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) + fun ?(never_include=false) ~include_paths status -> + status,LSome (GrafiteAst.Comment (loc, com)) | (iloc,fname,mode) = include_command ; SYMBOL "." -> !out fname; fun ?(never_include=false) ~include_paths status -> @@ -746,6 +793,10 @@ EXTEND ] ]; END +(* }}} *) +;; + +let _ = initialize_parser () ;; let exc_located_wrapper f = try @@ -763,5 +814,28 @@ let exc_located_wrapper f = let parse_statement lexbuf = exc_located_wrapper - (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf))) + (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf))) + +let statement () = !grafite_parser.statement + +let history = ref [] ;; + +let push () = + LexiconSync.push (); + history := !grafite_parser :: !history; + grafite_parser := initial_parser (); + initialize_parser () +;; + +let pop () = + LexiconSync.pop (); + match !history with + | [] -> assert false + | gp :: tail -> + grafite_parser := gp; + history := tail +;; + +(* vim:set foldmethod=marker: *) +