X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=9373e54b43a1de051f743a2581220677abaf4df8;hb=92081320b50b03d6bf296552d2cae9e4b398f1be;hp=8848efad6ce3865660fd2b4ed797ab050bf001d9;hpb=351cacd582f87110b1ff710ca44ed649f90fbd32;p=helm.git diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 8848efad6..9373e54b4 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -53,6 +53,12 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) let default_precedence = 50 let default_associativity = Gramext.NonA +type by_continuation = + BYC_done + | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option + | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term + | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term + EXTEND GLOBAL: term statement; arg: [ @@ -68,11 +74,10 @@ EXTEND [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] ]; reduction_kind: [ - [ IDENT "demodulate" -> `Demodulate - | IDENT "normalize" -> `Normalize + [ IDENT "normalize" -> `Normalize | IDENT "reduce" -> `Reduce | IDENT "simplify" -> `Simpl - | IDENT "unfold"; t = OPT term -> `Unfold t + | IDENT "unfold"; t = OPT tactic_term -> `Unfold t | IDENT "whd" -> `Whd ] ]; sequent_pattern_spec: [ @@ -128,16 +133,16 @@ EXTEND GrafiteAst.Absurd (loc, t) | IDENT "apply"; t = tactic_term -> GrafiteAst.Apply (loc, t) + | IDENT "applyS"; t = tactic_term -> + GrafiteAst.ApplyS (loc, t) | IDENT "assumption" -> GrafiteAst.Assumption loc - | IDENT "auto"; - depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; - width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ]; - paramodulation = OPT [ IDENT "paramodulation" ]; - full = OPT [ IDENT "full" ] -> (* ALB *) - GrafiteAst.Auto (loc,depth,width,paramodulation,full) - | IDENT "clear"; id = IDENT -> - GrafiteAst.Clear (loc,id) + | IDENT "auto"; params = + LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> + string_of_int v | v = IDENT -> v ] -> i,v ] -> + GrafiteAst.Auto (loc,params) + | IDENT "clear"; ids = LIST1 IDENT -> + GrafiteAst.Clear (loc, ids) | IDENT "clearbody"; id = IDENT -> GrafiteAst.ClearBody (loc,id) | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> @@ -148,11 +153,13 @@ EXTEND GrafiteAst.Contradiction loc | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> GrafiteAst.Cut (loc, ident, t) - | IDENT "decompose"; types = OPT ident_list0; what = IDENT; - (num, idents) = intros_spec -> + | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT; + idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] -> let types = match types with None -> [] | Some types -> types in + let idents = match idents with None -> [] | Some idents -> idents in let to_spec id = GrafiteAst.Ident id in GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents) + | IDENT "demodulate" -> GrafiteAst.Demodulate loc | IDENT "discriminate"; t = tactic_term -> GrafiteAst.Discriminate (loc, t) | IDENT "elim"; what = tactic_term; using = using; @@ -176,7 +183,7 @@ EXTEND GrafiteAst.Fold (loc, kind, t, p) | IDENT "fourier" -> GrafiteAst.Fourier loc - | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> + | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] -> let idents = match idents with None -> [] | Some idents -> idents in GrafiteAst.FwdSimpl (loc, hyp, idents) | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> @@ -194,12 +201,14 @@ EXTEND | IDENT "inversion"; t = tactic_term -> GrafiteAst.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 [ IDENT "using" ; ident = IDENT -> ident ] -> - let to_what = match to_what with None -> [] | Some to_what -> to_what in - GrafiteAst.LApply (loc, depth, to_what, what, ident) + 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 + GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) | IDENT "left" -> GrafiteAst.Left loc | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> GrafiteAst.LetIn (loc, t, where) @@ -224,12 +233,72 @@ EXTEND GrafiteAst.Ring loc | IDENT "split" -> GrafiteAst.Split loc + | IDENT "subst" -> + GrafiteAst.Subst loc | IDENT "symmetry" -> GrafiteAst.Symmetry loc | IDENT "transitivity"; t = tactic_term -> GrafiteAst.Transitivity (loc, t) + (* Produzioni Aggiunte *) + | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> + GrafiteAst.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']-> + GrafiteAst.Suppose (loc, t, id, t1) + | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc]; + cont=by_continuation -> + let t' = match t with LNone _ -> None | LSome t -> Some t in + (match cont with + BYC_done -> GrafiteAst.Bydone (loc, t') + | BYC_weproved (ty,id,t1) -> + GrafiteAst.By_term_we_proved(loc, t', ty, id, t1) + | BYC_letsuchthat (id1,t1,id2,t2) -> + (match t with + LNone floc -> + raise (HExtlib.Localized + (floc,CicNotationParser.Parse_error + "tactic_term expected here")) + | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2)) + | BYC_wehaveand (id1,t1,id2,t2) -> + (match t with + LNone floc -> + raise (HExtlib.Localized + (floc,CicNotationParser.Parse_error + "tactic_term expected here")) + | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2))) + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> + GrafiteAst.We_need_to_prove (loc, t, id, t1) + | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> + GrafiteAst.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 -> + GrafiteAst.Byinduction(loc, t, id) + | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term -> + GrafiteAst.Thesisbecomes(loc, t) + | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; + SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> + GrafiteAst.Case(loc,id,params) + | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont) + | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, None, t1, t2, cont) + ] +]; + by_continuation: [ + [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,id,t1) + | IDENT "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) + | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ; + "and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN -> + BYC_wehaveand (id1,t1,id2,t2) ] - ]; +]; + rewriting_step_continuation : [ + [ IDENT "done" -> None + | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id) + | -> Some Cic.Anonymous + ] +]; atomic_tactical: [ "sequence" LEFTA [ t1 = SELF; SYMBOL ";"; t2 = SELF -> @@ -258,6 +327,7 @@ EXTEND | IDENT "solve"; SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> GrafiteAst.Solve (loc, tacs) + | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac) | LPAREN; tac = SELF; RPAREN -> tac | tac = tactic -> GrafiteAst.Tactic (loc, tac) ] @@ -266,7 +336,8 @@ EXTEND [ [ SYMBOL "[" -> GrafiteAst.Branch loc | SYMBOL "|" -> GrafiteAst.Shift loc - | i = int; SYMBOL ":" -> GrafiteAst.Pos (loc, i) + | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i) + | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc | SYMBOL "]" -> GrafiteAst.Merge loc | SYMBOL ";" -> GrafiteAst.Semicolon loc | SYMBOL "." -> GrafiteAst.Dot loc @@ -315,8 +386,14 @@ EXTEND SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; fields = LIST0 [ name = IDENT ; - coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; - ty = term -> (name,ty,coercion) + 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 @@ -328,13 +405,7 @@ EXTEND ] ]; macro: [ - [ [ IDENT "quit" ] -> GrafiteAst.Quit loc -(* | [ IDENT "abort" ] -> GrafiteAst.Abort loc *) -(* | [ IDENT "undo" ]; steps = OPT NUMBER -> - GrafiteAst.Undo (loc, int_opt steps) - | [ IDENT "redo" ]; steps = OPT NUMBER -> - GrafiteAst.Redo (loc, int_opt steps) *) - | [ IDENT "check" ]; t = term -> + [ [ IDENT "check" ]; t = term -> GrafiteAst.Check (loc, t) | [ IDENT "hint" ] -> GrafiteAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> @@ -347,7 +418,6 @@ EXTEND GrafiteAst.WElim (loc, t) | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> GrafiteAst.WHint (loc,t) - | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name) ] ]; alias_spec: [ @@ -449,13 +519,17 @@ EXTEND ]; include_command: [ [ - IDENT "include" ; path = QSTRING -> loc,path + IDENT "include" ; path = QSTRING -> + loc,path,LexiconAst.WithPreferences + | IDENT "include'" ; path = QSTRING -> + loc,path,LexiconAst.WithoutPreferences ]]; grafite_command: [ [ IDENT "set"; n = QSTRING; v = QSTRING -> GrafiteAst.Set (loc, n, v) | IDENT "drop" -> GrafiteAst.Drop loc + | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s) | IDENT "qed" -> GrafiteAst.Qed loc | IDENT "variant" ; name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode> ; newname = IDENT -> @@ -469,6 +543,8 @@ EXTEND body = term -> GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, Ast.Implicit, Some body)) + | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> + GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = CicNotationParser.let_defs -> let name,ty = @@ -491,8 +567,9 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; suri = URI -> - GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true) + | IDENT "coercion" ; suri = URI ; arity = OPT int -> + let arity = match arity with None -> 0 | Some x -> x in + GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> @@ -528,17 +605,20 @@ EXTEND fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex)) | com = comment -> fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) - | (iloc,fname) = include_command ; SYMBOL "." -> + | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ~include_paths status -> - let path = DependenciesParser.baseuri_of_script ~include_paths fname in + let buri, fullpath = + DependenciesParser.baseuri_of_script ~include_paths fname + in let status = - LexiconEngine.eval_command status (LexiconAst.Include (iloc,path)) + LexiconEngine.eval_command status + (LexiconAst.Include (iloc,buri,mode,fullpath)) in status, LSome (GrafiteAst.Executable (loc,GrafiteAst.Command - (loc,GrafiteAst.Include (iloc,path)))) + (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> fun ~include_paths status -> let status = LexiconEngine.eval_command status scom in