(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) (* $Id$ *) module N = CicNotationPt 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 = (N.term, N.term, N.term G.reduction, N.term N.obj, string) G.statement type statement = ?never_include:bool -> include_paths:string list -> LE.status -> LE.status * ast_statement localized_option type parser_status = { grammar : Grammar.g; term : N.term Grammar.Entry.e; statement : 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 grafite_parser = ref (initial_parser ()) let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t) let default_associativity = Gramext.NonA let mk_rec_corec ng ind_kind defs loc = (* In case of mutual definitions here we produce just the syntax tree for the first one. The others will be generated from the completely specified term just before insertion in the environment. We use the flavour `MutualDefinition to rememer this. *) let name,ty = match defs with | (params,(N.Ident (name, None), Some ty),_,_) :: _ -> let ty = List.fold_right (fun var ty -> N.Binder (`Pi,var,ty) ) params ty in name,ty | (_,(N.Ident (name, None), None),_,_) :: _ -> name, N.Implicit | _ -> assert false in let body = N.Ident (name,None) in let flavour = if List.length defs = 1 then `Definition else `MutualDefinition in if ng then G.NObj (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)))) else G.Obj (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)))) type by_continuation = BYC_done | BYC_weproved of N.term * string option * N.term option | BYC_letsuchthat of string * N.term * string * N.term | BYC_wehaveand of string * N.term * string * N.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 "90" -> t ] ]; new_name: [ [ id = IDENT -> Some id | SYMBOL "_" -> None ] ]; ident_list0: [ [ LPAREN; idents = LIST0 new_name; 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 ] ]; sequent_pattern_spec: [ [ hyp_paths = LIST0 [ id = IDENT ; path = OPT [SYMBOL ":" ; path = tactic_term -> path ] -> (id,match path with Some p -> p | None -> N.UserInput) ]; goal_path = OPT [ SYMBOL <:unicode>; term = tactic_term -> term ] -> let goal_path = match goal_path, hyp_paths with None, [] -> Some N.UserInput | None, _::_ -> None | Some goal_path, _ -> Some goal_path in hyp_paths,goal_path ] ]; pattern_spec: [ [ res = OPT [ "in"; wanted_and_sps = [ "match" ; wanted = tactic_term ; sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> Some wanted,sps | sps = sequent_pattern_spec -> None,Some sps ] -> let wanted,hyp_paths,goal_path = match wanted_and_sps with wanted,None -> wanted, [], Some N.UserInput | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path in wanted, hyp_paths, goal_path ] -> match res with None -> None,[],Some N.UserInput | Some ps -> ps] ]; inverter_param_list: [ [ params = tactic_term -> let deannotate = function | N.AttributedTerm (_,t) | t -> t in match deannotate params with | N.Implicit -> [false] | N.UserInput -> [true] | N.Appl l -> List.map (fun x -> match deannotate x with | N.Implicit -> false | N.UserInput -> true | _ -> raise (Invalid_argument "malformed target parameter list 1")) l | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ] ]; direction: [ [ SYMBOL ">" -> `LeftToRight | SYMBOL "<" -> `RightToLeft ] ]; int: [ [ num = NUMBER -> int_of_string num ] ]; intros_names: [ [ idents = OPT ident_list0 -> match idents with None -> [] | Some idents -> idents ] ]; intros_spec: [ [ OPT [ IDENT "names" ]; num = OPT [ num = int -> num ]; idents = intros_names -> num, idents ] ]; using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; ntactic: [ [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t) | IDENT "nassert"; seqs = LIST0 [ hyps = LIST0 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty | id = IDENT ; SYMBOL ":" ; ty = tactic_term ; SYMBOL <:unicode> ; bo = tactic_term -> id,`Def (bo,ty)]; SYMBOL <:unicode>; concl = tactic_term -> (List.rev hyps,concl) ] -> G.NAssert (loc, seqs) | IDENT "ncases"; what = tactic_term ; where = pattern_spec -> G.NCases (loc, what, where) | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> G.NChange (loc, what, with_what) | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> G.NElim (loc, what, where) | IDENT "ngeneralize"; p=pattern_spec -> G.NGeneralize (loc, p) | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode> ; t = tactic_term; where = pattern_spec -> G.NLetIn (loc,where,t,name) | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec -> G.NRewrite (loc, dir, what, where) | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ]; where = pattern_spec -> let delta = match delta with None -> true | _ -> false in G.NEval (loc, where, `Whd delta) | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n) | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_") | SYMBOL "*" -> G.NCase1 (loc,"_") | SYMBOL "*"; n=IDENT -> G.NCase1 (loc,n) ] ]; tactic: [ [ IDENT "absurd"; t = tactic_term -> G.Absurd (loc, t) | IDENT "apply"; IDENT "rule"; t = tactic_term -> G.ApplyRule (loc, t) | IDENT "apply"; t = tactic_term -> G.Apply (loc, t) | IDENT "applyP"; t = tactic_term -> G.ApplyP (loc, t) | IDENT "applyS"; t = tactic_term ; params = auto_params -> G.ApplyS (loc, t, params) | IDENT "assumption" -> G.Assumption loc | IDENT "autobatch"; params = auto_params -> G.AutoBatch (loc,params) | IDENT "cases"; what = tactic_term; pattern = OPT pattern_spec; specs = intros_spec -> let pattern = match pattern with | None -> None, [], Some N.UserInput | Some pattern -> pattern in G.Cases (loc, what, pattern, specs) | IDENT "clear"; ids = LIST1 IDENT -> G.Clear (loc, ids) | IDENT "clearbody"; id = IDENT -> G.ClearBody (loc,id) | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> G.Change (loc, what, t) | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec -> let times = match times with None -> 1 | Some i -> i in G.Compose (loc, t1, t2, times, specs) | IDENT "constructor"; n = int -> G.Constructor (loc, n) | IDENT "contradiction" -> G.Contradiction loc | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> G.Cut (loc, ident, t) | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] -> let idents = match idents with None -> [] | Some idents -> idents in G.Decompose (loc, idents) | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p) | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] -> G.Destruct (loc, xts) | IDENT "elim"; what = tactic_term; using = using; pattern = OPT pattern_spec; ispecs = intros_spec -> let pattern = match pattern with | None -> None, [], Some N.UserInput | Some pattern -> pattern in G.Elim (loc, what, using, pattern, ispecs) | IDENT "elimType"; what = tactic_term; using = using; (num, idents) = intros_spec -> G.ElimType (loc, what, using, (num, idents)) | IDENT "exact"; t = tactic_term -> G.Exact (loc, t) | IDENT "exists" -> G.Exists loc | IDENT "fail" -> G.Fail loc | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> let (pt,_,_) = p in if pt <> None then raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ("the pattern cannot specify the term to replace, only its" ^ " paths in the hypotheses and in the conclusion"))) else G.Fold (loc, kind, t, p) | IDENT "fourier" -> G.Fourier loc | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] -> let idents = match idents with None -> [] | Some idents -> idents in G.FwdSimpl (loc, hyp, idents) | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> G.Generalize (loc,p,id) | IDENT "id" -> G.IdTac loc | IDENT "intro"; ident = OPT IDENT -> let idents = match ident with None -> [] | Some id -> [Some id] in G.Intros (loc, (Some 1, idents)) | IDENT "intros"; specs = intros_spec -> G.Intros (loc, specs) | IDENT "inversion"; t = tactic_term -> G.Inversion (loc, t) | IDENT "lapply"; linear = OPT [ IDENT "linear" ]; depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; what = tactic_term; to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; ident = OPT [ "as" ; ident = IDENT -> ident ] -> let linear = match linear with None -> false | Some _ -> true in let to_what = match to_what with None -> [] | Some to_what -> to_what in G.LApply (loc, linear, depth, to_what, what, ident) | IDENT "left" -> G.Left loc | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> G.LetIn (loc, t, where) | kind = reduction_kind; p = pattern_spec -> G.Reduce (loc, kind, p) | IDENT "reflexivity" -> G.Reflexivity loc | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> G.Replace (loc, p, t) | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec; xnames = OPT [ "as"; n = ident_list0 -> n ] -> let (pt,_,_) = p in if pt <> None then raise (HExtlib.Localized (loc, (CicNotationParser.Parse_error "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) else let n = match xnames with None -> [] | Some names -> names in G.Rewrite (loc, d, t, p, n) | IDENT "right" -> G.Right loc | IDENT "ring" -> G.Ring loc | IDENT "split" -> G.Split loc | IDENT "symmetry" -> G.Symmetry loc | IDENT "transitivity"; t = tactic_term -> G.Transitivity (loc, t) (* Produzioni Aggiunte *) | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> G.Assume (loc, id, t) | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']-> G.Suppose (loc, t, id, t1) | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2) | just = [ IDENT "using"; t=tactic_term -> `Term t | params = auto_params -> `Auto params] ; cont=by_continuation -> (match cont with BYC_done -> G.Bydone (loc, just) | BYC_weproved (ty,id,t1) -> G.By_just_we_proved(loc, just, ty, id, t1) | BYC_letsuchthat (id1,t1,id2,t2) -> G.ExistsElim (loc, just, id1, t1, id2, t2) | BYC_wehaveand (id1,t1,id2,t2) -> G.AndElim (loc, just, id1, t1, id2, t2)) | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> G.We_need_to_prove (loc, t, id, t1) | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> G.We_proceed_by_cases_on (loc, t, t1) | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> G.We_proceed_by_induction_on (loc, t, t1) | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN -> G.Byinduction(loc, t, id) | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term -> G.Thesisbecomes(loc, t) | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> G.Case(loc,id,params) (* DO NOT FACTORIZE with the two following, camlp5 sucks*) | IDENT "conclude"; termine = tactic_term; SYMBOL "=" ; t1=tactic_term ; t2 = [ IDENT "using"; t=tactic_term -> `Term t | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term | IDENT "proof" -> `Proof | params = auto_params -> `Auto params]; cont = rewriting_step_continuation -> G.RewritingStep(loc, Some (None,termine), t1, t2, cont) | IDENT "obtain" ; name = IDENT; termine = tactic_term; SYMBOL "=" ; t1=tactic_term ; t2 = [ IDENT "using"; t=tactic_term -> `Term t | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term | IDENT "proof" -> `Proof | params = auto_params -> `Auto params]; cont = rewriting_step_continuation -> G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont) | SYMBOL "=" ; t1=tactic_term ; t2 = [ IDENT "using"; t=tactic_term -> `Term t | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term | IDENT "proof" -> `Proof | params = auto_params -> `Auto params]; cont = rewriting_step_continuation -> G.RewritingStep(loc, None, t1, t2, cont) ] ]; auto_fixed_param: [ [ IDENT "paramodulation" | IDENT "depth" | IDENT "width" | IDENT "size" | IDENT "timeout" | IDENT "library" | IDENT "type" | IDENT "all" ] ]; auto_params: [ [ params = LIST0 [ i = auto_fixed_param -> i,"" | i = auto_fixed_param ; SYMBOL "="; v = [ v = int -> string_of_int v | v = IDENT -> v ] -> i,v ]; tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> (match tl with Some l -> l | None -> []), params ] ]; 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] ; "done" -> BYC_weproved (ty,None,t1) | "done" -> BYC_done | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2) | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> BYC_wehaveand (id1,t1,id2,t2) ] ]; rewriting_step_continuation : [ [ "done" -> true | -> false ] ]; atomic_tactical: [ "sequence" LEFTA [ t1 = SELF; SYMBOL ";"; t2 = SELF -> let ts = match t1 with | G.Seq (_, l) -> l @ [ t2 ] | _ -> [ t1; t2 ] in G.Seq (loc, ts) ] | "then" NONA [ tac = SELF; SYMBOL ";"; SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> (G.Then (loc, tac, tacs)) ] | "loops" RIGHTA [ IDENT "do"; count = int; tac = SELF -> G.Do (loc, count, tac) | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac) ] | "simple" NONA [ IDENT "first"; SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> G.First (loc, tacs) | IDENT "try"; tac = SELF -> G.Try (loc, tac) | IDENT "solve"; SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> G.Solve (loc, tacs) | IDENT "progress"; tac = SELF -> G.Progress (loc, tac) | LPAREN; tac = SELF; RPAREN -> tac | tac = tactic -> tac ] ]; punctuation_tactical: [ [ SYMBOL "[" -> G.Branch loc | SYMBOL "|" -> G.Shift loc | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i) | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc | SYMBOL "]" -> G.Merge loc | SYMBOL ";" -> G.Semicolon loc | SYMBOL "." -> G.Dot loc ] ]; non_punctuation_tactical: [ "simple" NONA [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals) | IDENT "unfocus" -> G.Unfocus loc | IDENT "skip" -> G.Skip loc ] ]; ntheorem_flavour: [ [ [ IDENT "ndefinition" ] -> `Definition | [ IDENT "nfact" ] -> `Fact | [ IDENT "nlemma" ] -> `Lemma | [ IDENT "nremark" ] -> `Remark | [ IDENT "ntheorem" ] -> `Theorem ] ]; theorem_flavour: [ [ [ IDENT "definition" ] -> `Definition | [ IDENT "fact" ] -> `Fact | [ IDENT "lemma" ] -> `Lemma | [ IDENT "remark" ] -> `Remark | [ IDENT "theorem" ] -> `Theorem ] ]; inline_flavour: [ [ attr = theorem_flavour -> attr | [ IDENT "axiom" ] -> `Axiom | [ IDENT "mutual" ] -> `MutualDefinition ] ]; inductive_spec: [ [ 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"; types = LIST1 [ name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> (name, true, typ, constructors) ] SEP "with" -> types ] -> let params = List.fold_right (fun (names, typ) acc -> (List.map (fun name -> (name, typ)) names) @ acc) params [] in let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in let tl_ind_types = match tl with None -> [] | Some types -> types in let ind_types = fst_ind_type :: tl_ind_types in (params, ind_types) ] ]; record_spec: [ [ name = IDENT; params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; fields = LIST0 [ name = IDENT ; coercion = [ SYMBOL ":" -> false,0 | SYMBOL ":"; SYMBOL ">" -> true,0 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity ]; ty = term -> let b,n = coercion in (name,ty,b,n) ] SEP SYMBOL ";"; SYMBOL "}" -> let params = List.fold_right (fun (names, typ) acc -> (List.map (fun name -> (name, typ)) names) @ acc) params [] in (params,name,typ,fields) ] ]; macro: [ [ [ IDENT "check" ]; t = term -> G.Check (loc, t) | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term -> G.Eval (loc, kind, t) | [ IDENT "inline"]; style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; suri = QSTRING; prefix = OPT QSTRING; flavour = OPT [ "as"; attr = inline_flavour -> attr ] -> let style = match style with | None -> G.Declarative | Some depth -> G.Procedural depth in let prefix = match prefix with None -> "" | Some prefix -> prefix in G.Inline (loc,style,suri,prefix, flavour) | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> if rew = None then G.Hint (loc, false) else G.Hint (loc,true) | IDENT "auto"; params = auto_params -> G.AutoInteractive (loc,params) | [ IDENT "whelp"; "match" ] ; t = term -> G.WMatch (loc,t) | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> G.WInstance (loc,t) | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> G.WLocate (loc,id) | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> G.WElim (loc, t) | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> G.WHint (loc,t) ] ]; alias_spec: [ [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> let alpha = "[a-zA-Z]" in let num = "[0-9]+" in let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" 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 with UriManager.IllFormedUri _ -> false) || (try ignore (NReference.reference_of_string uri); true with NReference.IllFormedReference _ -> false) then L.Ident_alias (id, uri) else raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri))) else raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ( Printf.sprintf "Not a valid identifier: %s" id))) | IDENT "symbol"; symbol = QSTRING; instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; SYMBOL "="; dsc = QSTRING -> let instance = match instance with Some i -> i | None -> 0 in L.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) ] ]; argument: [ [ l = LIST0 [ SYMBOL <:unicode> (* η *); SYMBOL "." -> () ]; id = IDENT -> N.IdentArg (List.length l, id) ] ]; associativity: [ [ IDENT "left"; IDENT "associative" -> Gramext.LeftA | IDENT "right"; IDENT "associative" -> Gramext.RightA | IDENT "non"; IDENT "associative" -> Gramext.NonA ] ]; precedence: [ [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] ]; notation: [ [ dir = OPT direction; s = QSTRING; assoc = OPT associativity; prec = precedence; IDENT "for"; p2 = [ blob = UNPARSED_AST -> add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob) (CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string blob)) | blob = UNPARSED_META -> add_raw_attribute ~text:(Printf.sprintf "${%s}" blob) (CicNotationParser.parse_level2_meta (Ulexing.from_utf8_string blob)) ] -> let assoc = match assoc with | None -> default_associativity | Some assoc -> assoc in let p1 = add_raw_attribute ~text:s (CicNotationParser.parse_level1_pattern prec (Ulexing.from_utf8_string s)) in (dir, p1, assoc, prec, p2) ] ]; level3_term: [ [ u = URI -> N.UriPattern (UriManager.uri_of_string u) | id = IDENT -> N.VarPattern id | SYMBOL "_" -> N.ImplicitPattern | LPAREN; terms = LIST1 SELF; RPAREN -> (match terms with | [] -> assert false | [term] -> term | terms -> N.ApplPattern terms) ] ]; interpretation: [ [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term -> (s, args, t) ] ]; include_command: [ [ IDENT "include" ; path = QSTRING -> loc,path,L.WithPreferences | IDENT "include'" ; path = QSTRING -> loc,path,L.WithoutPreferences ]]; grafite_command: [ [ IDENT "set"; n = QSTRING; v = QSTRING -> G.Set (loc, n, v) | IDENT "drop" -> G.Drop loc | IDENT "print"; s = IDENT -> G.Print (loc,s) | IDENT "qed" -> G.Qed loc | IDENT "nqed" -> G.NQed loc | IDENT "variant" ; name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode> ; newname = IDENT -> G.Obj (loc, N.Theorem (`Variant,name,typ,Some (N.Ident (newname, None)))) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> G.NObj (loc, N.Theorem (nflavour, name, typ, body)) | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> G.Obj (loc, N.Theorem (flavour, name, typ, body)) | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); body = term -> G.Obj (loc, N.Theorem (flavour, name, N.Implicit, Some body)) | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> G.Obj (loc, N.Theorem (`Axiom, name, typ, None)) | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term -> G.NObj (loc, N.Theorem (`Axiom, name, typ, None)) | LETCOREC ; defs = let_defs -> mk_rec_corec false `CoInductive defs loc | LETREC ; defs = let_defs -> mk_rec_corec false `Inductive defs loc | NLETCOREC ; defs = let_defs -> mk_rec_corec true `CoInductive defs loc | NLETREC ; defs = let_defs -> mk_rec_corec true `Inductive defs loc | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in G.Obj (loc, N.Inductive (params, ind_types)) | IDENT "ninductive"; spec = inductive_spec -> let (params, ind_types) = spec in G.NObj (loc, N.Inductive (params, ind_types)) | IDENT "coinductive"; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) ind_types in G.Obj (loc, N.Inductive (params, ind_types)) | IDENT "ncoinductive"; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) ind_types in G.NObj (loc, N.Inductive (params, ind_types)) | IDENT "coercion" ; t = [ u = URI -> N.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 G.Coercion (loc, t, composites, arity, saturations) | IDENT "prefer" ; IDENT "coercion"; t = tactic_term -> G.PreferCoercion (loc, t) | IDENT "pump" ; steps = int -> G.Pump(loc,steps) | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> G.UnificationHint (loc, t, n) | IDENT "inverter"; name = IDENT; IDENT "for"; indty = tactic_term; paramspec = inverter_param_list -> G.Inverter (loc, name, indty, paramspec) | IDENT "record" ; (params,name,ty,fields) = record_spec -> G.Obj (loc, N.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> let uris = List.map UriManager.uri_of_string uris in G.Default (loc,what,uris) | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ; refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ; refl = tactic_term -> refl ] ; sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ; sym = tactic_term -> sym ] ; trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ; trans = tactic_term -> trans ] ; "as" ; id = IDENT -> G.Relation (loc,id,a,aeq,refl,sym,trans) ]]; lexicon_command: [ [ IDENT "alias" ; spec = alias_spec -> L.Alias (loc, spec) | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation -> L.Notation (loc, dir, l1, assoc, prec, l2) | IDENT "interpretation"; id = QSTRING; (symbol, args, l3) = interpretation -> L.Interpretation (loc, id, (symbol, args), l3) ]]; executable: [ [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd) | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical -> G.Tactic (loc, Some tac, punct) | punct = punctuation_tactical -> G.Tactic (loc, None, punct) | tac = ntactic; punct = punctuation_tactical -> G.NTactic (loc, tac, punct) | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical -> G.NTactic (loc, G.NId loc, punct) | tac = non_punctuation_tactical; punct = punctuation_tactical -> G.NonPunctuationTactical (loc, tac, punct) | mac = macro; SYMBOL "." -> G.Macro (loc, mac) ] ]; comment: [ [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> G.Code (loc, ex) | str = NOTE -> G.Note (loc, str) ] ]; statement: [ [ ex = executable -> fun ?(never_include=false) ~include_paths status -> let stm = G.Executable (loc, ex) in !grafite_callback status stm; status, LSome stm | com = comment -> fun ?(never_include=false) ~include_paths status -> let stm = G.Comment (loc, com) in !grafite_callback status stm; status, LSome stm | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> let stm = G.Executable (loc, G.Command (loc, G.Include (iloc, fname))) in !grafite_callback status stm; let _root, buri, fullpath, _rrelpath = Librarian.baseuri_of_script ~include_paths fname in let stm = G.Executable (loc, G.Command (loc, G.Include (iloc, buri))) in let status = if never_include then raise (NoInclusionPerformed fullpath) else LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in status, LSome stm | scom = lexicon_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> !lexicon_callback status scom; let status = LE.eval_command status scom in status, LNone loc | EOI -> raise End_of_file ] ]; END (* }}} *) ;; let _ = initialize_parser () ;; 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 !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: *)