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=20aad1cd3a19c16788264e634cb95028cca31c89;hpb=63ed9d3148199584ae8b238f018e0f9883768ada;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 20aad1cd3..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,10 +102,16 @@ 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) ] ]; - tactic_term: [ [ t = term LEVEL "90N" -> t ] ]; + tactic_term: [ [ t = term LEVEL "90" -> t ] ]; new_name: [ [ id = IDENT -> Some id | SYMBOL "_" -> None ] @@ -164,11 +180,24 @@ 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 -> + GrafiteAst.ApplyP (loc, t) | IDENT "applyS"; t = tactic_term ; params = auto_params -> GrafiteAst.ApplyS (loc, t, params) | IDENT "assumption" -> @@ -207,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)) @@ -442,6 +471,10 @@ EXTEND | IDENT "skip" -> GrafiteAst.Skip loc ] ]; + ntheorem_flavour: [ + [ [ IDENT "ntheorem" ] -> `Theorem + ] + ]; theorem_flavour: [ [ [ IDENT "definition" ] -> `Definition | [ IDENT "fact" ] -> `Fact @@ -450,8 +483,15 @@ EXTEND | [ IDENT "theorem" ] -> `Theorem ] ]; + inline_flavour: [ + [ attr = theorem_flavour -> attr + | [ IDENT "axiom" ] -> `Axiom + | [ IDENT "mutual" ] -> `MutualDefinition + ] + ]; 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"; @@ -473,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 ; @@ -498,15 +539,18 @@ 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 -> + suri = QSTRING; prefix = OPT QSTRING; + flavour = OPT [ "as"; attr = inline_flavour -> attr ] -> let style = match style with | None -> GrafiteAst.Declarative | Some depth -> GrafiteAst.Procedural depth in let prefix = match prefix with None -> "" | Some prefix -> prefix in - GrafiteAst.Inline (loc,style,suri,prefix) + GrafiteAst.Inline (loc,style,suri,prefix, flavour) | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true) | IDENT "auto"; params = auto_params -> @@ -528,7 +572,8 @@ EXTEND let alpha = "[a-zA-Z]" in let num = "[0-9]+" in let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in - let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in + let decoration = "\\'" in + let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in let rex = Str.regexp ("^"^ident^"$") in if Str.string_match rex id 0 then if (try ignore (UriManager.uri_of_string uri); true @@ -593,7 +638,7 @@ EXTEND in let p1 = add_raw_attribute ~text:s - (CicNotationParser.parse_level1_pattern + (CicNotationParser.parse_level1_pattern prec (Ulexing.from_utf8_string s)) in (dir, p1, assoc, prec, p2) @@ -634,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)) @@ -643,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 @@ -657,13 +705,19 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; suri = URI ; arity = OPT int ; - saturations = OPT int; composites = OPT (IDENT "nocomposites") -> + | IDENT "coercion" ; + t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ; + arity = OPT int ; saturations = OPT int; + composites = OPT (IDENT "nocomposites") -> let arity = match arity with None -> 0 | Some x -> x in let saturations = match saturations with None -> 0 | Some x -> x in let composites = match composites with None -> true | Some _ -> false in GrafiteAst.Coercion - (loc, UriManager.uri_of_string suri, composites, arity, saturations) + (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 -> @@ -693,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) @@ -709,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 -> @@ -734,6 +793,10 @@ EXTEND ] ]; END +(* }}} *) +;; + +let _ = initialize_parser () ;; let exc_located_wrapper f = try @@ -751,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: *) +