X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=f3dd386a91540b15c729dbf22a0b4c7c25fcaf4a;hb=68d46ac40a575f3fce5958fb2776b38739703951;hp=ab15311dfd219c09bb7af3cc51b920724b62f071;hpb=070e79b6e7ec986dd5fcdee24857956f6a4a9221;p=helm.git diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index ab15311df..f3dd386a9 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -35,7 +35,8 @@ type 'a localized_option = type ast_statement = (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + CicNotationPt.term GrafiteAst.reduction, + CicNotationPt.term CicNotationPt.obj, string) GrafiteAst.statement type statement = @@ -55,18 +56,16 @@ let default_associativity = Gramext.NonA type by_continuation = BYC_done - | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option + | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term +let out = ref ignore + +let set_callback f = out := f + EXTEND GLOBAL: term statement; - arg: [ - [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; - SYMBOL ":"; ty = term; RPAREN -> names,ty - | name = IDENT -> [name],Ast.Implicit - ] - ]; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; tactic_term: [ [ t = term LEVEL "90N" -> t ] ]; ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ]; @@ -121,9 +120,15 @@ EXTEND | SYMBOL "<" -> `RightToLeft ] ]; int: [ [ num = NUMBER -> int_of_string num ] ]; + intros_names: [ + [ idents = OPT ident_list0 -> + match idents with None -> [] | Some idents -> idents + ] + ]; intros_spec: [ - [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in + [ OPT [ IDENT "names" ]; + num = OPT [ num = int -> num ]; + idents = intros_names -> num, idents ] ]; @@ -133,14 +138,17 @@ 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"; params = + | IDENT "applyS"; t = tactic_term ; params = LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> string_of_int v | v = IDENT -> v ] -> i,v ] -> + GrafiteAst.ApplyS (loc, t, params) + | IDENT "assumption" -> + GrafiteAst.Assumption loc + | IDENT "auto"; params = auto_params -> GrafiteAst.Auto (loc,params) + | IDENT "cases"; what = tactic_term; + (num, idents) = intros_spec -> + GrafiteAst.Cases (loc, what, idents) | IDENT "clear"; ids = LIST1 IDENT -> GrafiteAst.Clear (loc, ids) | IDENT "clearbody"; id = IDENT -> @@ -216,7 +224,8 @@ EXTEND GrafiteAst.Reflexivity loc | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> GrafiteAst.Replace (loc, p, t) - | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> + | 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 @@ -224,7 +233,8 @@ EXTEND (CicNotationParser.Parse_error "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) else - GrafiteAst.Rewrite (loc, d, t, p) + let n = match xnames with None -> [] | Some names -> names in + GrafiteAst.Rewrite (loc, d, t, p, n) | IDENT "right" -> GrafiteAst.Right loc | IDENT "ring" -> @@ -263,8 +273,10 @@ EXTEND (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']-> + | 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']-> GrafiteAst.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 -> + GrafiteAst.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 -> 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 -> @@ -274,27 +286,39 @@ EXTEND | 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 -> + | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; cont=rewriting_step_continuation -> + GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont) + | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; + cont=rewriting_step_continuation -> GrafiteAst.RewritingStep(loc, None, t1, t2, cont) ] +]; + auto_params: [ + [ params = + LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> + string_of_int v | v = IDENT -> v ] -> i,v ] -> + params + ] +]; + auto_params': [ + [ LPAREN; params = auto_params; RPAREN -> params + | -> [] + ] ]; 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 "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,Some id,t1) + | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; + IDENT "done" -> BYC_weproved (ty,None,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) + 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 + [ IDENT "done" -> true + | -> false ] ]; atomic_tactical: @@ -358,7 +382,7 @@ EXTEND ] ]; inductive_spec: [ [ - fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; + fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars; SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; fst_constructors = LIST0 constructor SEP SYMBOL "|"; tl = OPT [ "with"; @@ -380,7 +404,7 @@ EXTEND ] ]; record_spec: [ [ - name = IDENT; params = LIST0 [ arg = arg -> arg ] ; + name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ; SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; fields = LIST0 [ name = IDENT ; @@ -405,6 +429,15 @@ EXTEND macro: [ [ [ IDENT "check" ]; t = term -> GrafiteAst.Check (loc, t) + | [ IDENT "inline"]; + style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; + suri = QSTRING; prefix = OPT QSTRING -> + 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) | [ IDENT "hint" ] -> GrafiteAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> GrafiteAst.WMatch (loc,t) @@ -545,16 +578,33 @@ EXTEND GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = CicNotationParser.let_defs -> + (* 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 - | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty - | ((Ast.Ident (name, None), None),_,_) :: _ -> + | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ -> + let ty = + List.fold_right + (fun var ty -> Ast.Binder (`Pi,var,ty) + ) params ty + in + name,ty + | (_,(Ast.Ident (name, None), None),_,_) :: _ -> name, Ast.Implicit | _ -> assert false in let body = Ast.Ident (name,None) in - GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty, - Some (Ast.LetRec (ind_kind, defs, body)))) + let flavour = + if List.length defs = 1 then + `Definition + else + `MutualDefinition + in + GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty, + Some (Ast.LetRec (ind_kind, defs, body)))) | IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) @@ -573,6 +623,15 @@ EXTEND | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> let uris = List.map UriManager.uri_of_string uris in GrafiteAst.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 -> + GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ]]; lexicon_command: [ [ IDENT "alias" ; spec = alias_spec -> @@ -619,7 +678,8 @@ EXTEND (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> fun ~include_paths status -> - let status = LexiconEngine.eval_command status scom in + !out scom; + let status = LexiconEngine.eval_command status scom in status,LNone loc | EOI -> raise End_of_file ]