From: Stefano Zacchiroli Date: Thu, 14 Jul 2005 16:38:04 +0000 (+0000) Subject: snapshot, notably: X-Git-Tag: pre_notation~11 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=34113d572c334c351ba66f4b05db503eed4d48f2;p=helm.git snapshot, notably: - started merge with cic_transformations, ATM all available matita scripts are parseable with test_parser fed with doc/core_notation.ma --- diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index 6eae806d5..00d1f6fed 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -1,14 +1,17 @@ -cicNotationUtil.cmi: cicNotationPt.cmo +cicNotationUtil.cmi: grafiteAst.cmo cicNotationPt.cmo cicNotationTag.cmi: cicNotationPt.cmo cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi -cicNotationMatcher.cmi: cicNotationPt.cmo cicNotationEnv.cmi +cicNotationMatcher.cmi: grafiteAst.cmo cicNotationPt.cmo cicNotationEnv.cmi cicNotationFwd.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi -cicNotationRew.cmi: cicNotationPt.cmo +grafiteParser.cmi: grafiteAst.cmo cicNotationPt.cmo +cicNotationRew.cmi: grafiteAst.cmo cicNotationPt.cmo cicNotationPres.cmi: cicNotationPt.cmo -cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi -cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi +grafiteAst.cmo: cicNotationPt.cmo +grafiteAst.cmx: cicNotationPt.cmx +cicNotationUtil.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationUtil.cmi +cicNotationUtil.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationUtil.cmi cicNotationTag.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationTag.cmi cicNotationTag.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationTag.cmi cicNotationLexer.cmo: cicNotationLexer.cmi @@ -17,10 +20,10 @@ cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi -cicNotationMatcher.cmo: cicNotationUtil.cmi cicNotationTag.cmi \ +cicNotationMatcher.cmo: grafiteAst.cmo cicNotationUtil.cmi cicNotationTag.cmi \ cicNotationPt.cmo cicNotationPp.cmi cicNotationEnv.cmi \ cicNotationMatcher.cmi -cicNotationMatcher.cmx: cicNotationUtil.cmx cicNotationTag.cmx \ +cicNotationMatcher.cmx: grafiteAst.cmx cicNotationUtil.cmx cicNotationTag.cmx \ cicNotationPt.cmx cicNotationPp.cmx cicNotationEnv.cmx \ cicNotationMatcher.cmi cicNotationFwd.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi \ @@ -33,13 +36,17 @@ cicNotationParser.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ cicNotationParser.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ cicNotationPp.cmx cicNotationLexer.cmx cicNotationEnv.cmx \ cicNotationParser.cmi -cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ +grafiteParser.cmo: grafiteAst.cmo cicNotationPt.cmo cicNotationParser.cmi \ + grafiteParser.cmi +grafiteParser.cmx: grafiteAst.cmx cicNotationPt.cmx cicNotationParser.cmx \ + grafiteParser.cmi +cicNotationRew.cmo: grafiteAst.cmo cicNotationUtil.cmi cicNotationPt.cmo \ cicNotationParser.cmi cicNotationMatcher.cmi cicNotationEnv.cmi \ cicNotationRew.cmi -cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ +cicNotationRew.cmx: grafiteAst.cmx cicNotationUtil.cmx cicNotationPt.cmx \ cicNotationParser.cmx cicNotationMatcher.cmx cicNotationEnv.cmx \ cicNotationRew.cmi -cicNotationPres.cmo: cicNotationPt.cmo cicNotationPres.cmi cicNotationPp.cmi \ - cicNotationPres.cmi -cicNotationPres.cmx: cicNotationPt.cmx cicNotationPres.cmx cicNotationPp.cmx \ - cicNotationPres.cmi +cicNotationPres.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ + cicNotationPres.cmi cicNotationPp.cmi cicNotationPres.cmi +cicNotationPres.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ + cicNotationPres.cmx cicNotationPp.cmx cicNotationPres.cmi diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index ea2f30449..38859414d 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -5,8 +5,8 @@ REQUIRES = \ helm-cic \ helm-utf8_macros \ camlp4.gramlib \ - helm-cic_proof_checking \ helm-cic_transformations\ + helm-cic_proof_checking \ ulex \ $(NULL) INTERFACE_FILES = \ @@ -18,11 +18,13 @@ INTERFACE_FILES = \ cicNotationMatcher.mli \ cicNotationFwd.mli \ cicNotationParser.mli \ + grafiteParser.mli \ cicNotationRew.mli \ cicNotationPres.mli \ $(NULL) IMPLEMENTATION_FILES = \ cicNotationPt.ml \ + grafiteAst.ml \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ $(NULL) @@ -38,9 +40,12 @@ test_parser: test_parser.ml $(PACKAGE).cma cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4) cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) +grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) cicNotationLexer.cmx: OCAMLOPT = $(OCAMLOPT_P4) cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) +grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) cicNotationParser.ml.annot: OCAMLC = $(OCAMLC_P4) +grafiteParser.ml.annot: OCAMLC = $(OCAMLC_P4) cicNotationLexer.ml.annot: OCAMLC = $(OCAMLC_P4) cicNotationPres.cmi: OCAMLOPTIONS += -rectypes cicNotationPres.cmo: OCAMLOPTIONS += -rectypes diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 92204cfb7..b5cd026d6 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -29,19 +29,24 @@ exception Error of int * int * string let regexp number = xml_digit+ + (* ZACK: breaks unicode's binder followed by an ascii letter without blank *) +(* let regexp ident_letter = xml_letter *) + +let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ] + let regexp ident_decoration = '\'' | '!' | '?' | '`' -let regexp ident_cont = xml_letter | xml_digit | '_' -let regexp ident = xml_letter ident_cont* ident_decoration* +let regexp ident_cont = ident_letter | xml_digit | '_' +let regexp ident = ident_letter ident_cont* ident_decoration* let regexp tex_token = '\\' ident let regexp delim_begin = "\\[" let regexp delim_end = "\\]" -let regexp keyword = '"' ident '"' let regexp qkeyword = "'" ident "'" let regexp implicit = '?' +let regexp placeholder = '%' let regexp meta = implicit number let regexp csymbol = '\'' ident @@ -55,6 +60,11 @@ let regexp meta_ident = "$" ident let regexp meta_anonymous = "$_" let regexp qstring = '"' [^ '"']* '"' +let regexp begincomment = "(**" xml_blank +let regexp endcomment = "*)" +let regexp comment_char = [^'*'] | '*'[^')'] +let regexp note = "(*" ([^'*'] | "**") comment_char* "*)" + let level1_layouts = [ "sub"; "sup"; "below"; "above"; @@ -150,8 +160,6 @@ let expand_macro lexbuf = ("SYMBOL", Utf8Macro.expand macro) with Utf8Macro.Macro_not_found _ -> "SYMBOL", Ulexing.utf8_lexeme lexbuf -let keyword lexbuf = "KEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf) - let remove_quotes s = String.sub s 1 (String.length s - 2) let remove_left_quote s = String.sub s 1 (String.length s - 1) @@ -196,7 +204,8 @@ let rec level2_meta_token = lexer let rec level2_ast_token = lexer | xml_blank+ -> level2_ast_token lexbuf | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) - | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf) + | implicit -> return lexbuf ("IMPLICIT", "") + | placeholder -> return lexbuf ("PLACEHOLDER", "") | ident -> let lexeme = Ulexing.utf8_lexeme lexbuf in if Hashtbl.mem level2_ast_keywords lexeme then @@ -204,7 +213,6 @@ let rec level2_ast_token = lexer else return lexbuf ("IDENT", lexeme) | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) - | keyword -> return lexbuf (keyword lexbuf) | tex_token -> return lexbuf (expand_macro lexbuf) | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) | qstring -> @@ -218,8 +226,15 @@ let rec level2_ast_token = lexer return lexbuf ("UNPARSED_META", remove_left_quote (Ulexing.utf8_lexeme lexbuf)) | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous") - | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) + | note -> + let comment = + Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4) + in + return lexbuf ("NOTE", comment) + | begincomment -> return lexbuf ("BEGINCOMMENT","") + | endcomment -> return lexbuf ("ENDCOMMENT","") | eof -> return lexbuf ("EOI", "") + | _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf) let rec level1_pattern_token = lexer | xml_blank+ -> level1_pattern_token lexbuf diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 9d879db5e..2ae4fd00e 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -373,19 +373,19 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Pt.UriPattern uri -> Uri uri, [] - | Pt.VarPattern _ -> Blob, [] - | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl + | GrafiteAst.UriPattern uri -> Uri uri, [] + | GrafiteAst.VarPattern _ -> Blob, [] + | GrafiteAst.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl let tag_of_pattern p = let mask, pl = mask_of_appl_pattern p in Hashtbl.hash mask, pl - type pattern_t = Pt.cic_appl_pattern + type pattern_t = GrafiteAst.cic_appl_pattern type term_t = Cic.annterm let classify = function - | Pt.VarPattern _ -> Variable + | GrafiteAst.VarPattern _ -> Variable | _ -> Constructor end @@ -399,7 +399,7 @@ struct List.map2 (fun p t -> match p with - | Pt.VarPattern name -> name, t + | GrafiteAst.VarPattern name -> name, t | _ -> assert false) pl matched_terms in diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli index 4abb5b8bc..3846bf528 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.mli +++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli @@ -54,6 +54,7 @@ end module Matcher32: sig val compiler : - (CicNotationPt.cic_appl_pattern * int) list -> + (GrafiteAst.cic_appl_pattern * int) list -> (Cic.annterm -> ((string * Cic.annterm) list * int) option) end + diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 472389de3..e52baffdd 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -54,15 +54,9 @@ let level1_pattern = Grammar.Entry.create level1_pattern_grammar "level1_pattern" let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" let term = Grammar.Entry.create level2_ast_grammar "term" +let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" -let level3_term = Grammar.Entry.create level2_ast_grammar "level3_term" -let notation = (* level1 <-> level 2 *) - Grammar.Entry.create level2_ast_grammar "notation" -let interpretation = (* level2 <-> level 3 *) - Grammar.Entry.create level2_ast_grammar "interpretation" -let phrase = Grammar.Entry.create level2_ast_grammar "phrase" - let return_term loc term = () let fail floc msg = @@ -280,12 +274,12 @@ let parse_level1_pattern_ref = ref (fun _ -> assert false) let parse_level2_ast_ref = ref (fun _ -> assert false) let parse_level2_meta_ref = ref (fun _ -> assert false) +let fold_cluster binder terms ty body = + List.fold_right + (fun term body -> Binder (binder, (term, ty), body)) + terms body (* terms are names: either Ident or FreshVar *) + let fold_binder binder pt_names body = - let fold_cluster binder terms ty body = - List.fold_right - (fun term body -> Binder (binder, (term, ty), body)) - terms body (* terms are names: either Ident or FreshVar *) - in List.fold_right (fun (names, ty) body -> fold_cluster binder names ty body) pt_names body @@ -409,10 +403,7 @@ EXTEND END EXTEND - GLOBAL: level2_ast term - level3_term - notation interpretation - phrase; + GLOBAL: level2_ast term let_defs; (* {{{ Grammar for ast patterns, notation level 2 *) level2_ast: [ [ p = term -> p ] ]; sort: [ @@ -439,9 +430,9 @@ EXTEND [ SYMBOL "["; substs = LIST0 meta_subst; SYMBOL "]" -> substs ] ]; possibly_typed_name: [ - [ LPAREN; id = bound_name; SYMBOL ":"; typ = term; RPAREN -> + [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN -> id, Some typ - | id = bound_name -> id, None + | arg = single_arg -> arg, None ] ]; match_pattern: [ @@ -457,23 +448,27 @@ EXTEND | SYMBOL <:unicode> (* λ *) -> `Lambda ] ]; - bound_name: [ - [ i = IDENT -> Ident (i, None) - | SYMBOL "\\FRESH"; i = IDENT -> Variable (FreshVar i) - ] + arg: [ + [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; + SYMBOL ":"; ty = term; RPAREN -> + List.map (fun n -> Ident (n, None)) names, Some ty + | name = IDENT -> [Ident (name, None)], None + | blob = UNPARSED_META -> + let meta = !parse_level2_meta_ref (Stream.of_string blob) in + match meta with + | Variable (FreshVar _) -> [meta], None + | Variable (TermVar "_") -> [Ident ("_", None)], None + | _ -> failwith "Invalid bound name." + ] ]; - bound_names: [ - [ vars = LIST1 bound_name SEP SYMBOL ","; - ty = OPT [ SYMBOL ":"; p = term -> p ] -> - [ vars, ty ] - | clusters = LIST1 [ - LPAREN; - vars = LIST1 bound_name SEP SYMBOL ","; - ty = OPT [ SYMBOL ":"; p = term -> p ]; - RPAREN -> - vars, ty - ] -> - clusters + single_arg: [ + [ name = IDENT -> Ident (name, None) + | blob = UNPARSED_META -> + let meta = !parse_level2_meta_ref (Stream.of_string blob) in + match meta with + | Variable (FreshVar _) -> meta + | Variable (TermVar "_") -> Ident ("_", None) + | _ -> failwith "Invalid index name." ] ]; induction_kind: [ @@ -483,8 +478,9 @@ EXTEND ]; let_defs: [ [ defs = LIST1 [ - name = bound_name; args = bound_names; - index_name = OPT [ "on"; id = bound_name -> id ]; + name = single_arg; + args = LIST1 arg; + index_name = OPT [ "on"; id = single_arg -> id ]; ty = OPT [ SYMBOL ":" ; p = term -> p ]; SYMBOL <:unicode> (* ≝ *); body = term -> let body = fold_binder `Lambda args body in @@ -510,13 +506,26 @@ EXTEND let index = match index_name with | None -> 0 - | Some name -> find_arg name 0 args + | Some index_name -> find_arg index_name 0 args in (name, ty), body, index ] SEP "and" -> defs ] ]; + binder_vars: [ + [ vars = [ + l = LIST1 single_arg SEP SYMBOL "," -> l + | SYMBOL "_" -> [Ident ("_", None)] ]; + typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) + | LPAREN; + vars = [ + l = LIST1 single_arg SEP SYMBOL "," -> l + | SYMBOL "_" -> [Ident ("_", None)] ]; + typ = OPT [ SYMBOL ":"; t = term -> t ]; + RPAREN -> (vars, typ) + ] + ]; term: LEVEL "10" (* let in *) [ "10" NONA [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); @@ -529,8 +538,8 @@ EXTEND ]; term: LEVEL "20" (* binder *) [ "20" RIGHTA - [ b = binder; names = bound_names; SYMBOL "."; body = term -> - return_term loc (fold_binder b names body) + [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term -> + return_term loc (fold_cluster b vars typ body) ] ]; term: LEVEL "70" (* apply *) @@ -553,12 +562,13 @@ EXTEND | u = URI -> return_term loc (Uri (u, None)) | n = NUMBER -> return_term loc (Num (n, 0)) | IMPLICIT -> return_term loc (Implicit) + | PLACEHOLDER -> return_term loc UserInput | m = META -> return_term loc (Meta (int_of_string m, [])) | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s)) | s = sort -> return_term loc (Sort s) | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ]; "match"; t = term; - indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; + indty_ident = OPT [ "in"; id = IDENT -> id ]; "with"; SYMBOL "["; patterns = LIST0 [ lhs = match_pattern; SYMBOL <:unicode> (* ⇒ *); @@ -574,65 +584,6 @@ EXTEND ] ]; (* }}} *) -(* {{{ Grammar for interpretation, notation level 3 *) - argument: [ - [ id = IDENT -> IdentArg (0, id) - | l = LIST1 [ SYMBOL <:unicode> (* η *) -> () ] SEP SYMBOL "."; - SYMBOL "."; id = IDENT -> - IdentArg (List.length l, id) - ] - ]; - level3_term: [ - [ u = URI -> UriPattern (UriManager.uri_of_string u) - | id = IDENT -> VarPattern id - | LPAREN; terms = LIST1 SELF; RPAREN -> - (match terms with - | [] -> assert false - | [term] -> term - | terms -> ApplPattern terms) - ] - ]; -(* }}} *) -(* {{{ Notation glues *) - 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: [ - [ s = QSTRING; - assoc = OPT associativity; prec = OPT precedence; - IDENT "for"; - p2 = - [ blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob) - | blob = UNPARSED_META -> - !parse_level2_meta_ref (Stream.of_string blob) ] - -> - (!parse_level1_pattern_ref (Stream.of_string s), assoc, prec, p2) - ] - ]; - interpretation: [ - [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term -> - (s, args, t) - ] - ]; -(* }}} *) -(* {{{ Top-level phrases *) - phrase: [ - [ IDENT "print"; t = term; SYMBOL "." -> Print t - | IDENT "notation"; (l1, assoc, prec, l2) = notation; SYMBOL "." -> - Notation (l1, assoc, prec, l2) - | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." -> - Interpretation ((symbol, args), l3) - | IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u) - | IDENT "dump"; SYMBOL "." -> Dump - ] - ]; -(* }}} *) END (** {2 API implementation} *) @@ -652,10 +603,6 @@ let parse_level2_ast stream = exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast stream) let parse_level2_meta stream = exc_located_wrapper (fun () -> Grammar.Entry.parse level2_meta stream) -let parse_interpretation stream = - exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream) -let parse_phrase stream = - exc_located_wrapper (fun () -> Grammar.Entry.parse phrase stream) let _ = parse_level1_pattern_ref := parse_level1_pattern; diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 73627cd0a..2819f4d9d 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -33,12 +33,7 @@ val parse_level1_pattern: char Stream.t -> CicNotationPt.term (** AST pattern: notation level 2 *) val parse_level2_ast: char Stream.t -> CicNotationPt.term - - (** interpretation: notation level 3 *) -val parse_interpretation: char Stream.t -> CicNotationPt.cic_appl_pattern - - (** top level phrases *) -val parse_phrase: char Stream.t -> CicNotationPt.phrase +val parse_level2_meta: char Stream.t -> CicNotationPt.term (** {2 Grammar extension} *) @@ -65,6 +60,15 @@ val binder_assoc: Gramext.g_assoc val apply_assoc: Gramext.g_assoc val simple_assoc: Gramext.g_assoc +(** {2 Grammar entries} + * needed by grafite parser *) + +val level2_ast_grammar: Grammar.g + +val term : CicNotationPt.term Grammar.Entry.e +val let_defs : + (CicNotationPt.capture_variable * CicNotationPt.term * int) list Grammar.Entry.e + (** {2 Debugging} *) (** print "level2_pattern" entry on stdout, flushing afterwards *) diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index 4b47b9014..c6b006f42 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -33,10 +33,6 @@ let binder_attributes = [None, "mathcolor", "blue"] let indent_attributes = [None, "indent", "1em"] let keyword_attributes = [None, "mathcolor", "blue"] -let mpres_arrow = Mpresentation.Mo (binder_attributes, "->") - (* TODO unicode symbol "to" *) -let mpres_implicit = Mpresentation.Mtext ([], "?") - let to_unicode s = try if s.[0] = '\\' then diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 322ce401b..56272ebed 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -136,19 +136,3 @@ and pattern_variable = (* level 2 variables *) | FreshVar of string -type argument_pattern = - | IdentArg of int * string (* eta-depth, name *) - -type cic_appl_pattern = - | UriPattern of UriManager.uri - | VarPattern of string - | ApplPattern of cic_appl_pattern list - -type phrase = (* TODO hackish: replace with TacticAst.statement or similar *) - | Print of term - | Notation of term * Gramext.g_assoc option * int option * term - (* level 1 pattern, associativity, precedence, level 2 pattern *) - | Interpretation of (string * argument_pattern list) * cic_appl_pattern - | Render of UriManager.uri - | Dump (* dump grammar *) - diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 436a40571..15947f3f2 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -244,12 +244,8 @@ let ast_of_acic0 term_info acic k = let level1_patterns21 = Hashtbl.create 211 let level2_patterns32 = Hashtbl.create 211 -let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option) -option ref) = - ref None -let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option) -option ref) = - ref None +let compiled21 = ref None +let compiled32 = ref None let pattern21_matrix = ref [] let pattern32_matrix = ref [] @@ -257,11 +253,11 @@ let pattern32_matrix = ref [] let get_compiled21 () = match !compiled21 with | None -> assert false - | Some f -> f + | Some f -> Lazy.force f let get_compiled32 () = match !compiled32 with | None -> assert false - | Some f -> f + | Some f -> Lazy.force f let set_compiled21 f = compiled21 := Some f let set_compiled32 f = compiled32 := Some f @@ -371,7 +367,7 @@ let rec pp_ast1 term = let instantiate32 term_info env symbol args = let rec instantiate_arg = function - | Ast.IdentArg (n, name) -> + | GrafiteAst.IdentArg (n, name) -> let t = (try List.assoc name env with Not_found -> assert false) in let rec count_lambda = function | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body @@ -408,10 +404,10 @@ let rec ast_of_acic1 term_info annterm = | _ -> Ast.AttributedTerm (`Href uris, ast) let load_patterns32 t = - set_compiled32 (CicNotationMatcher.Matcher32.compiler t) + set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t)) let load_patterns21 t = - set_compiled21 (CicNotationMatcher.Matcher21.compiler t) + set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t)) let ast_of_acic id_to_sort annterm = let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index cb43b3099..7c2415a73 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -39,8 +39,8 @@ type interpretation_id type pretty_printer_id val add_interpretation: - string * CicNotationPt.argument_pattern list -> (* level 2 pattern *) - CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) + string * GrafiteAst.argument_pattern list -> (* level 2 pattern *) + GrafiteAst.cic_appl_pattern -> (* level 3 pattern *) interpretation_id val add_pretty_printer: diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index d3a87dfc1..4dbc83f9e 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -350,13 +350,13 @@ let dress sauce = let find_appl_pattern_uris ap = let rec aux acc = function - | UriPattern uri -> + | GrafiteAst.UriPattern uri -> (try ignore (List.find (fun uri' -> UriManager.eq uri uri') acc); acc with Not_found -> uri :: acc) - | VarPattern _ -> acc - | ApplPattern apl -> List.fold_left aux acc apl + | GrafiteAst.VarPattern _ -> acc + | GrafiteAst.ApplPattern apl -> List.fold_left aux acc apl in aux [] ap diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index 080bbfa36..6661245af 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -55,8 +55,7 @@ val boxify: CicNotationPt.term list -> CicNotationPt.term val group: CicNotationPt.term list -> CicNotationPt.term val ungroup: CicNotationPt.term list -> CicNotationPt.term list -val find_appl_pattern_uris: - CicNotationPt.cic_appl_pattern -> UriManager.uri list +val find_appl_pattern_uris: GrafiteAst.cic_appl_pattern -> UriManager.uri list val find_branch: CicNotationPt.term -> CicNotationPt.term diff --git a/helm/ocaml/cic_notation/doc/core_notation.ma b/helm/ocaml/cic_notation/doc/core_notation.ma new file mode 100644 index 000000000..bb62bd372 --- /dev/null +++ b/helm/ocaml/cic_notation/doc/core_notation.ma @@ -0,0 +1,72 @@ +notation "hvbox(a break \to b)" + right associative with precedence 20 +for @{ \forall $_:$a.$b }. + +notation "hvbox(a break = b)" + non associative with precedence 45 +for @{ 'eq $a $b }. + +notation "hvbox(a break \leq b)" + non associative with precedence 45 +for @{ 'leq $a $b }. + +notation "hvbox(a break \geq b)" + non associative with precedence 45 +for @{ 'geq $a $b }. + +notation "hvbox(a break \lt b)" + non associative with precedence 45 +for @{ 'lt $a $b }. + +notation "hvbox(a break \gt b)" + non associative with precedence 45 +for @{ 'gt $a $b }. + +notation "hvbox(a break \neq b)" + non associative with precedence 45 +for @{ 'neq $a $b }. + +notation "hvbox(a break + b)" + left associative with precedence 50 +for @{ 'plus $a $b }. + +notation "hvbox(a break - b)" + left associative with precedence 50 +for @{ 'minus $a $b }. + +notation "hvbox(a break * b)" + left associative with precedence 55 +for @{ 'times $a $b }. + +notation "hvbox(a break / b)" + left associative with precedence 55 +for @{ 'divide $a $b }. + +notation "\frac a b" + non associative with precedence 90 +for @{ 'divide $a $b }. + +notation "a \over b" + non associative with precedence 55 +for @{ 'divide $a $b }. + +notation "- a" + non associative with precedence 60 +for @{ 'uminus $a }. + +notation "\sqrt a" + non associative with precedence 60 +for @{ 'sqrt $a }. + +notation "hvbox(a break \lor b)" + left associative with precedence 30 +for @{ 'or $a $b }. + +notation "hvbox(a break \land b)" + left associative with precedence 35 +for @{ 'or $a $b }. + +notation "hvbox(a break \lnot b)" + left associative with precedence 40 +for @{ 'or $a $b }. + diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma index 493db5958..803d624c0 100644 --- a/helm/ocaml/cic_notation/doc/samples.ma +++ b/helm/ocaml/cic_notation/doc/samples.ma @@ -3,14 +3,11 @@ notation "\langle a , b \rangle" for @{ 'pair $a $b }. -print \langle 1, \langle 2, 3 \rangle \rangle. -print 'pair 1 ('pair 2 ('pair 3 4)). +check \langle 1, \langle 2, 3 \rangle \rangle. +check 'pair 1 ('pair 2 ('pair 3 4)). -notation - "a :: b" -for - @{ 'cons $a $b }. -print 1 :: 2 :: 'ugo. +notation "a :: b" for @{ 'cons $a $b }. +check 1 :: 2 :: 'ugo. notation "[ hovbox (list0 a sep ; ) ]" @@ -20,7 +17,7 @@ for ${ rec acc @{ 'cons $a $acc } }. -print [1;2;3;4]. +check [1;2;3;4]. notation "[ list1 a sep ; | b ]" @@ -38,14 +35,14 @@ for ${ else fail }. -print 'cons 1 ('cons 2 ('cons 3 'ugo)). -print 'cons 1 ('cons 2 ('cons 3 'nil)). -print [1;2;3;4]. -print [1;2;3;4|5]. +check 'cons 1 ('cons 2 ('cons 3 'ugo)). +check 'cons 1 ('cons 2 ('cons 3 'nil)). +check [1;2;3;4]. +check [1;2;3;4|5]. notation "a + b" left associative for @{ 'plus $a $b }. -print 1 + 2 + 3. -print 1 + (2 + 3). +check 1 + 2 + 3. +check 1 + (2 + 3). notation "a + b" left associative for @{ 'plus $a $b }. notation "a * b" left associative for @{ 'mult $a $b }. @@ -57,7 +54,7 @@ notation "hvbox ('if' a 'then' break b break 'else' break c)" for @{ 'ifthenelse $a $b $c }. -print if even then \forall x:nat.x else bump x. +check if even then \forall x:nat.x else bump x. notation "a \vee b" @@ -70,6 +67,12 @@ notation for @{ 'lambda ${ident x} $a }. +notation + "hvbox(a break \to b)" +for + @{ \forall $_:$a.$b }. +check nat \to nat. + NOTES @a e' un'abbreviazione per @{term a} @@ -86,19 +89,19 @@ OLD SAMPLES # sample mappings level 1 <--> level 2 notation \[ \TERM a ++ \OPT \NUM i \] for 'assign \TERM a ('plus \TERM a \DEFAULT \[\NUM i\] \[1\]). -print 1 ++ 2. +check 1 ++ 2. notation \[ + \LIST0 \NUM a \] for \FOLD right \[ 'zero \] \LAMBDA acc \[ 'plus \NUM a \TERM acc \]. -print + 1 2 3 4. +check + 1 2 3 4. notation \[ [ \HOVBOX\[ \LIST0 \TERM a \SEP ; \] ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a \TERM acc \]. -print []. -print [1;2;3;4]. +check []. +check [1;2;3;4]. notation \[ [ \LIST0 \[ \TERM a ; \TERM b \] \SEP ; ] \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \TERM a ( 'cons \TERM b \TERM acc) \] . -print []. -print [1;2]. -print [1;2;3;4]. +check []. +check [1;2]. +check [1;2;3;4]. notation \[ | \LIST0 \[ \TERM a \OPT \[ , \TERM b \] \] \SEP ; | \] for \FOLD right \[ 'nil \] \LAMBDA acc \[ 'cons \DEFAULT \[ \TERM a \] \[ ('pair \TERM a \TERM b) \] \TERM acc \] . @@ -117,7 +120,7 @@ render cic:/Coq/Arith/Plus/plus_comm.con. # full samples notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b. -print 1 + 2. +check 1 + 2. interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y). render cic:/Coq/Arith/Plus/plus_comm.con. @@ -129,3 +132,4 @@ render cic:/Coq/Arith/Mult/mult_plus_distr_r.con. notation \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \]. + diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml new file mode 100644 index 000000000..5117fd493 --- /dev/null +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -0,0 +1,177 @@ +(* Copyright (C) 2004, 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/ + *) + +type direction = [ `LeftToRight | `RightToLeft ] +type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ] + +type loc = CicNotationPt.location + +type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term + +type ('term, 'ident) tactic = + | Absurd of loc * 'term + | Apply of loc * 'term + | Assumption of loc + | Auto of loc * int option * int option (* depth, width *) + | Change of loc * ('term,'ident) pattern * 'term + | Clear of loc * 'ident + | ClearBody of loc * 'ident + | Compare of loc * 'term + | Constructor of loc * int + | Contradiction of loc + | Cut of loc * 'ident option * 'term + | DecideEquality of loc + | Decompose of loc * 'term + | Discriminate of loc * 'term + | Elim of loc * 'term * 'term option * int option * 'ident list + | ElimType of loc * 'term * 'term option * int option * 'ident list + | Exact of loc * 'term + | Exists of loc + | Fail of loc + | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern + | Fourier of loc + | FwdSimpl of loc * string * 'ident list + | Generalize of loc * ('term, 'ident) pattern * 'ident option + | Goal of loc * int (* change current goal, argument is goal number 1-based *) + | IdTac of loc + | Injection of loc * 'term + | Intros of loc * int option * 'ident list + | LApply of loc * int option * 'term list * 'term * 'ident option + | Left of loc + | LetIn of loc * 'term * 'ident + | Reduce of loc * reduction_kind * ('term, 'ident) pattern + | Reflexivity of loc + | Replace of loc * ('term, 'ident) pattern * 'term + | Rewrite of loc * direction * 'term * ('term, 'ident) pattern + | Right of loc + | Ring of loc + | Split of loc + | Symmetry of loc + | Transitivity of loc * 'term + +type thm_flavour = Cic.object_flavour + + (** + * true means inductive, false coinductive *) +type 'term inductive_type = string * bool * 'term * (string * 'term) list + +type search_kind = [ `Locate | `Hint | `Match | `Elim ] + +type print_kind = [ `Env | `Coer ] + +type 'term macro = + (* Whelp's stuff *) + | WHint of loc * 'term + | WMatch of loc * 'term + | WInstance of loc * 'term + | WLocate of loc * string + | WElim of loc * 'term + (* real macros *) +(* | Abort of loc *) + | Print of loc * string + | Check of loc * 'term + | Hint of loc + | Quit of loc +(* | Redo of loc * int option + | Undo of loc * int option *) +(* | Print of loc * print_kind *) + | Search_pat of loc * search_kind * string (* searches with string pattern *) + | Search_term of loc * search_kind * 'term (* searches with term pattern *) + +type alias_spec = + | Ident_alias of string * string (* identifier, uri *) + | Symbol_alias of string * int * string (* name, instance no, description *) + | Number_alias of int * string (* instance no, description *) + +type obj = + | Inductive of (string * CicNotationPt.term) list * + CicNotationPt.term inductive_type list + (** parameters, list of loc * mutual inductive types *) + | Theorem of thm_flavour * string * CicNotationPt.term * CicNotationPt.term option + (** flavour, name, type, body + * - name is absent when an unnamed theorem is being proved, tipically in + * interactive usage + * - body is present when its given along with the command, otherwise it + * will be given in proof editing mode using the tactical language + *) + | Record of + (string * CicNotationPt.term) list * string * CicNotationPt.term * + (string * CicNotationPt.term) list + +type argument_pattern = + | IdentArg of int * string (* eta-depth, name *) + +type cic_appl_pattern = + | UriPattern of UriManager.uri + | VarPattern of string + | ApplPattern of cic_appl_pattern list + +type ('term,'obj) command = + | Default of loc * string * UriManager.uri list + | Include of loc * string + | Set of loc * string * string + | Drop of loc + | Qed of loc + (** name. + * Name is needed when theorem was started without providing a name + *) + | Coercion of loc * 'term + | Alias of loc * alias_spec + (** parameters, name, type, fields *) + | Obj of loc * 'obj + | Notation of loc * 'term * Gramext.g_assoc option * int option * 'term + (* level 1 pattern, associativity, precedence, level 2 pattern *) + | Interpretation of loc * (string * argument_pattern list) * cic_appl_pattern + + (* DEBUGGING *) + | Dump of loc (* dump grammar on stdout *) + (* DEBUGGING *) + | Render of loc * UriManager.uri (* render library object *) + +type ('term, 'ident) tactical = + | Tactic of loc * ('term, 'ident) tactic + | Do of loc * int * ('term, 'ident) tactical + | Repeat of loc * ('term, 'ident) tactical + | Seq of loc * ('term, 'ident) tactical list (* sequential composition *) + | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list + | First of loc * ('term, 'ident) tactical list + (* try a sequence of loc * tacticals until one succeeds, fail otherwise *) + | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *) + | Solve of loc * ('term, 'ident) tactical list + + +type ('term, 'obj, 'ident) code = + | Command of loc * ('term,'obj) command + | Macro of loc * 'term macro + | Tactical of loc * ('term, 'ident) tactical + +type ('term, 'obj, 'ident) comment = + | Note of loc * string + | Code of loc * ('term, 'obj, 'ident) code + +type ('term, 'obj, 'ident) statement = + | Executable of loc * ('term, 'obj, 'ident) code + | Comment of loc * ('term, 'obj, 'ident) comment + diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml new file mode 100644 index 000000000..41c3fd054 --- /dev/null +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -0,0 +1,481 @@ +(* 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/ + *) + +open Printf + +let grammar = CicNotationParser.level2_ast_grammar + +let term = CicNotationParser.term +let statement = Grammar.Entry.create grammar "statement" +let statements = Grammar.Entry.create grammar "statements" + +EXTEND + GLOBAL: term statement statements; + arg: [ + [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; + SYMBOL ":"; ty = term; RPAREN -> names,ty + | name = IDENT -> [name],CicNotationPt.Implicit + ] + ]; + constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; + tactic_term: [ [ t = term -> t ] ]; + ident_list0: [ + [ SYMBOL "["; idents = LIST0 IDENT SEP SYMBOL ";"; SYMBOL "]" -> idents ] + ]; + tactic_term_list1: [ + [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] + ]; + reduction_kind: [ + [ IDENT "reduce" -> `Reduce + | IDENT "simplify" -> `Simpl + | IDENT "whd" -> `Whd + | IDENT "normalize" -> `Normalize ] + ]; + sequent_pattern_spec: [ + [ hyp_paths = + LIST0 + [ id = IDENT ; + path = OPT [SYMBOL ":" ; path = term -> path ] -> + (id,match path with Some p -> p | None -> CicNotationPt.UserInput) ] + SEP SYMBOL ";"; + goal_path = OPT [ SYMBOL <:unicode>; term = term -> term ] -> + let goal_path = + match goal_path with + None -> CicNotationPt.UserInput + | Some goal_path -> goal_path + in + hyp_paths,goal_path + ] + ]; + pattern_spec: [ + [ res = OPT [ + "in"; + wanted_and_sps = + [ "match" ; wanted = 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, [], CicNotationPt.UserInput + | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path + in + wanted, hyp_paths, goal_path ] -> + match res with + None -> None,[],CicNotationPt.UserInput + | Some ps -> ps] + ]; + direction: [ + [ SYMBOL ">" -> `LeftToRight + | SYMBOL "<" -> `RightToLeft ] + ]; + int: [ [ num = NUMBER -> int_of_string num ] ]; + tactic: [ + [ IDENT "absurd"; t = tactic_term -> + GrafiteAst.Absurd (loc, t) + | IDENT "apply"; t = tactic_term -> + GrafiteAst.Apply (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 ] -> + GrafiteAst.Auto (loc,depth,width) + | IDENT "clear"; id = IDENT -> + GrafiteAst.Clear (loc,id) + | IDENT "clearbody"; id = IDENT -> + GrafiteAst.ClearBody (loc,id) + | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> + GrafiteAst.Change (loc, what, t) + | IDENT "compare"; t = tactic_term -> + GrafiteAst.Compare (loc,t) + | IDENT "constructor"; n = int -> + GrafiteAst.Constructor (loc, n) + | IDENT "contradiction" -> + GrafiteAst.Contradiction loc + | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> + GrafiteAst.Cut (loc, ident, t) + | IDENT "decide"; IDENT "equality" -> + GrafiteAst.DecideEquality loc + | IDENT "decompose"; where = tactic_term -> + GrafiteAst.Decompose (loc, where) + | IDENT "discriminate"; t = tactic_term -> + GrafiteAst.Discriminate (loc, t) + | IDENT "elim"; what = tactic_term; + using = OPT [ "using"; using = tactic_term -> using ]; + OPT "names"; num = OPT [num = int -> num]; + idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + GrafiteAst.Elim (loc, what, using, num, idents) + | IDENT "elimType"; what = tactic_term; + using = OPT [ "using"; using = tactic_term -> using ]; + OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + GrafiteAst.ElimType (loc, what, using, num, idents) + | IDENT "exact"; t = tactic_term -> + GrafiteAst.Exact (loc, t) + | IDENT "exists" -> + GrafiteAst.Exists loc + | IDENT "fail" -> GrafiteAst.Fail loc + | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> + let (pt,_,_) = p in + if pt <> None then + raise (CicNotationParser.Parse_error + (loc, "the pattern cannot specify the term to replace, only its" + ^ " paths in the hypotheses and in the conclusion")) + else + GrafiteAst.Fold (loc, kind, t, p) + | IDENT "fourier" -> + GrafiteAst.Fourier loc + | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> + 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] -> + GrafiteAst.Generalize (loc,p,id) + | IDENT "goal"; n = int -> + GrafiteAst.Goal (loc, n) + | IDENT "id" -> GrafiteAst.IdTac loc + | IDENT "injection"; t = tactic_term -> + GrafiteAst.Injection (loc, t) + | IDENT "intro"; ident = OPT IDENT -> + let idents = match ident with None -> [] | Some id -> [id] in + GrafiteAst.Intros (loc, Some 1, idents) + | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + GrafiteAst.Intros (loc, num, idents) + | IDENT "lapply"; + depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; + what = tactic_term; + to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; + ident = OPT [ "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 "left" -> GrafiteAst.Left loc + | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> + GrafiteAst.LetIn (loc, t, where) + | kind = reduction_kind; p = pattern_spec -> + GrafiteAst.Reduce (loc, kind, p) + | IDENT "reflexivity" -> + 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 -> + let (pt,_,_) = p in + if pt <> None then + raise + (CicNotationParser.Parse_error + (loc,"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) + | IDENT "right" -> + GrafiteAst.Right loc + | IDENT "ring" -> + GrafiteAst.Ring loc + | IDENT "split" -> + GrafiteAst.Split loc + | IDENT "symmetry" -> + GrafiteAst.Symmetry loc + | IDENT "transitivity"; t = tactic_term -> + GrafiteAst.Transitivity (loc, t) + ] + ]; + tactical: + [ "sequence" LEFTA + [ tacticals = LIST1 NEXT SEP SYMBOL ";" -> + match tacticals with + [] -> assert false + | [tac] -> tac + | l -> GrafiteAst.Seq (loc, l) + ] + | "then" NONA + [ tac = tactical; SYMBOL ";"; + SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" -> + (GrafiteAst.Then (loc, tac, tacs)) + ] + | "loops" RIGHTA + [ IDENT "do"; count = int; tac = tactical -> + GrafiteAst.Do (loc, count, tac) + | IDENT "repeat"; tac = tactical -> + GrafiteAst.Repeat (loc, tac) + ] + | "simple" NONA + [ IDENT "first"; + SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" -> + GrafiteAst.First (loc, tacs) + | IDENT "try"; tac = NEXT -> + GrafiteAst.Try (loc, tac) + | IDENT "solve"; + SYMBOL "["; tacs = LIST0 tactical SEP SYMBOL "|"; SYMBOL "]" -> + GrafiteAst.Solve (loc, tacs) + | LPAREN; tac = tactical; RPAREN -> tac + | tac = tactic -> GrafiteAst.Tactic (loc, tac) + ] + ]; + theorem_flavour: [ + [ [ IDENT "definition" ] -> `Definition + | [ IDENT "fact" ] -> `Fact + | [ IDENT "lemma" ] -> `Lemma + | [ IDENT "remark" ] -> `Remark + | [ IDENT "theorem" ] -> `Theorem + ] + ]; + inductive_spec: [ [ + fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; + 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 [ arg = arg -> arg ] ; + SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; + fields = LIST0 [ + name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) + ] 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 "quit" ] -> GrafiteAst.Quit loc +(* | [ IDENT "abort" ] -> GrafiteAst.Abort loc *) + | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name) +(* | [ 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 -> + GrafiteAst.Check (loc, t) + | [ IDENT "hint" ] -> GrafiteAst.Hint loc + | [ IDENT "whelp"; "match" ] ; t = term -> + GrafiteAst.WMatch (loc,t) + | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> + GrafiteAst.WInstance (loc,t) + | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> + GrafiteAst.WLocate (loc,id) + | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> + GrafiteAst.WElim (loc, t) + | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> + GrafiteAst.WHint (loc,t) + | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name) + ] + ]; + 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 ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" 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) + then + GrafiteAst.Ident_alias (id, uri) + else + raise (CicNotationParser.Parse_error (loc,sprintf "Not a valid uri: %s" uri)) + else + raise (CicNotationParser.Parse_error (loc, + 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 + GrafiteAst.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 + GrafiteAst.Number_alias (instance, dsc) + ] + ]; + argument: [ + [ id = IDENT -> GrafiteAst.IdentArg (0, id) + | l = LIST1 [ SYMBOL <:unicode> (* η *) -> () ] SEP SYMBOL "."; + SYMBOL "."; id = IDENT -> + GrafiteAst.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: [ + [ s = QSTRING; + assoc = OPT associativity; prec = OPT precedence; + IDENT "for"; + p2 = + [ blob = UNPARSED_AST -> + CicNotationParser.parse_level2_ast (Stream.of_string blob) + | blob = UNPARSED_META -> + CicNotationParser.parse_level2_meta (Stream.of_string blob) ] + -> + (CicNotationParser.parse_level1_pattern (Stream.of_string s), assoc, prec, p2) + ] + ]; + level3_term: [ + [ u = URI -> GrafiteAst.UriPattern (UriManager.uri_of_string u) + | id = IDENT -> GrafiteAst.VarPattern id + | LPAREN; terms = LIST1 SELF; RPAREN -> + (match terms with + | [] -> assert false + | [term] -> term + | terms -> GrafiteAst.ApplPattern terms) + ] + ]; + interpretation: [ + [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term -> + (s, args, t) + ] + ]; + command: [ [ + IDENT "set"; n = QSTRING; v = QSTRING -> + GrafiteAst.Set (loc, n, v) + | IDENT "drop" -> GrafiteAst.Drop loc + | IDENT "qed" -> GrafiteAst.Qed loc + | IDENT "variant" ; name = IDENT; SYMBOL ":"; + typ = term; SYMBOL <:unicode> ; newname = IDENT -> + GrafiteAst.Obj (loc, + GrafiteAst.Theorem + (`Variant,name,typ,Some (CicNotationPt.Ident (newname, None)))) + | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body)) + | flavour = theorem_flavour; name = IDENT; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + GrafiteAst.Obj (loc, + GrafiteAst.Theorem (flavour, name, CicNotationPt.Implicit, body)) + | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; + defs = CicNotationParser.let_defs -> + let name,ty = + match defs with + | ((CicNotationPt.Ident (name, None), Some ty),_,_) :: _ -> name,ty + | ((CicNotationPt.Ident (name, None), None),_,_) :: _ -> + name, CicNotationPt.Implicit + | _ -> assert false + in + let body = CicNotationPt.Ident (name,None) in + GrafiteAst.Obj (loc,GrafiteAst.Theorem(`Definition, name, ty, + Some (CicNotationPt.LetRec (ind_kind, defs, body)))) + | [ IDENT "inductive" ]; spec = inductive_spec -> + let (params, ind_types) = spec in + GrafiteAst.Obj (loc,GrafiteAst.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 + GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types)) + | IDENT "coercion" ; name = IDENT -> + GrafiteAst.Coercion (loc, CicNotationPt.Ident (name,Some [])) + | IDENT "coercion" ; name = URI -> + GrafiteAst.Coercion (loc, CicNotationPt.Uri (name,Some [])) + | IDENT "alias" ; spec = alias_spec -> + GrafiteAst.Alias (loc, spec) + | IDENT "record" ; (params,name,ty,fields) = record_spec -> + GrafiteAst.Obj (loc,GrafiteAst.Record (params,name,ty,fields)) + | IDENT "include" ; path = QSTRING -> + GrafiteAst.Include (loc,path) + | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> + let uris = List.map UriManager.uri_of_string uris in + GrafiteAst.Default (loc,what,uris) + | IDENT "notation"; (l1, assoc, prec, l2) = notation -> + GrafiteAst.Notation (loc, l1, assoc, prec, l2) + | IDENT "interpretation"; (symbol, args, l3) = interpretation -> + GrafiteAst.Interpretation (loc, (symbol, args), l3) + + | IDENT "dump" -> GrafiteAst.Dump loc + | IDENT "render"; u = URI -> GrafiteAst.Render (loc, UriManager.uri_of_string u) + ]]; + executable: [ + [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) + | tac = tactical; SYMBOL "." -> GrafiteAst.Tactical (loc, tac) + | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac) + ] + ]; + comment: [ + [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> + GrafiteAst.Code (loc, ex) + | str = NOTE -> + GrafiteAst.Note (loc, str) + ] + ]; + statement: [ + [ ex = executable -> GrafiteAst.Executable (loc,ex) + | com = comment -> GrafiteAst.Comment (loc, com) + ] + ]; + statements: [ + [ l = LIST0 statement ; EOI -> l + ] + ]; +END + +let exc_located_wrapper f = + try + f () + with + | Stdpp.Exc_located (floc, Stream.Error msg) -> + raise (CicNotationParser.Parse_error (floc, msg)) + | Stdpp.Exc_located (floc, exn) -> + raise (CicNotationParser.Parse_error (floc, (Printexc.to_string exn))) + +let parse_statement stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream)) +let parse_statements stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream)) + diff --git a/helm/ocaml/cic_notation/grafiteParser.mli b/helm/ocaml/cic_notation/grafiteParser.mli new file mode 100644 index 000000000..e769a5bfb --- /dev/null +++ b/helm/ocaml/cic_notation/grafiteParser.mli @@ -0,0 +1,32 @@ +(* 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/ + *) + +val parse_statement: + char Stream.t -> (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement + +val parse_statements: + char Stream.t -> + (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement list + diff --git a/helm/ocaml/cic_notation/test_parser.conf.xml b/helm/ocaml/cic_notation/test_parser.conf.xml index 119a45f57..eca4f2d8c 100644 --- a/helm/ocaml/cic_notation/test_parser.conf.xml +++ b/helm/ocaml/cic_notation/test_parser.conf.xml @@ -5,4 +5,7 @@ file:///projects/helm/library/coq_contribs/ +
+ doc/core_notation.ma +
diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 1673db6f4..22d5c09ff 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -42,86 +42,124 @@ let dump_xml t id_to_uri fname = Xml.pp_to_outchan (CicNotationPres.render_to_boxml id_to_uri t) oc; close_out oc -let _ = +let extract_loc = + function + | GrafiteAst.Executable (loc, _) + | GrafiteAst.Comment (loc, _) -> loc + +let errquit ignore_exn = + if not ignore_exn then begin + prerr_endline "Error, exiting!"; + exit 2 + end + +let process_stream ?(ignore_exn = false) istream = + let char_count = ref 0 in let module P = CicNotationPt in - let arg_spec = [ ] in - let usage = "" in - Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; + let module G = GrafiteAst in try - let istream = Stream.of_channel stdin in - while Stream.peek istream <> None do - try - match CicNotationParser.parse_phrase istream with - | P.Print t -> - prerr_endline "===="; - prerr_endline (CicNotationPp.pp_term t); flush stdout; - let t' = CicNotationRew.pp_ast t in - prerr_endline (CicNotationPp.pp_term t'); flush stdout; - let tbl = Hashtbl.create 0 in - dump_xml t' tbl "out.xml" - | P.Notation (l1, associativity, precedence, l2) -> - prerr_endline "Extending parser ..."; flush stdout; - prerr_endline (CicNotationPp.pp_term l1) ; - prerr_endline (sprintf "Found keywords: %s" - (String.concat " " (CicNotationUtil.keywords_of_term l1))); - let time1 = Unix.gettimeofday () in - ignore (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); - let time2 = Unix.gettimeofday () in - prerr_endline "Extending pretty printer ..."; flush stdout; - let time3 = Unix.gettimeofday () in - ignore (CicNotationRew.add_pretty_printer - ?precedence ?associativity l2 l1); - let time4 = Unix.gettimeofday () in - printf "done (extending parser took %f, extending pretty printer took %f)\n" - (time2 -. time1) (time4 -. time3); - flush stdout - | P.Interpretation (l2, l3) -> - prerr_endline "Adding interpretation ..."; flush stdout; - let time1 = Unix.gettimeofday () in - ignore (CicNotationRew.add_interpretation l2 l3); - let time2 = Unix.gettimeofday () in - printf "done (patterns compilation took %f seconds)\n" - (time2 -. time1); - flush stdout - | P.Dump -> CicNotationParser.print_l2_pattern (); print_newline () - | P.Render uri -> - let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - let annobj, _, _, id_to_sort, _, _, _ = - Cic2acic.acic_object_of_cic_object obj - in - let annterm = - match annobj with - | Cic.AConstant (_, _, _, _, ty, _, _) - | Cic.AVariable (_, _, _, ty, _, _) -> ty - | _ -> assert false - in - let time1 = Unix.gettimeofday () in - let t, id_to_uri = - CicNotationRew.ast_of_acic id_to_sort annterm - in + while Stream.peek istream <> None do + try + let statement = GrafiteParser.parse_statement istream in + let floc = extract_loc statement in + let (_, y) = P.loc_of_floc floc in + char_count := y + !char_count; + match statement with + | G.Executable (_, G.Macro (_, G.Check (_, t))) -> + prerr_endline "===="; + prerr_endline (CicNotationPp.pp_term t); flush stdout; + let t' = CicNotationRew.pp_ast t in + prerr_endline (CicNotationPp.pp_term t'); flush stdout; + let tbl = Hashtbl.create 0 in + dump_xml t' tbl "out.xml" + | G.Executable (_, G.Command (_, + G.Notation (_, l1, associativity, precedence, l2))) -> + prerr_endline "Extending parser ..."; flush stdout; + prerr_endline (CicNotationPp.pp_term l1) ; + prerr_endline (sprintf "Found keywords: %s" + (String.concat " " (CicNotationUtil.keywords_of_term l1))); + let time1 = Unix.gettimeofday () in + ignore (CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); let time2 = Unix.gettimeofday () in - prerr_endline (sprintf "ast creation took %f seconds\n" (time2 -. time1)); - prerr_endline "AST"; - prerr_endline (CicNotationPp.pp_term t); - flush stdout; + prerr_endline "Extending pretty printer ..."; flush stdout; let time3 = Unix.gettimeofday () in - let t' = CicNotationRew.pp_ast t in - let time4 = Unix.gettimeofday () in - prerr_endline (sprintf "pretty printing took %f seconds\n" (time4 -. time3)); - prerr_endline (CicNotationPp.pp_term t'); - dump_xml t' id_to_uri "out.xml" - (* let (x, y) = P.loc_of_floc floc in *) - (* let before = String.sub line 0 x in *) - (* let error = String.sub line x (y - x) in *) - (* let after = String.sub line y (String.length line - y) in *) - (* eprintf "%s%s%s\n" before error after; *) - (* prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) + ignore (CicNotationRew.add_pretty_printer + ?precedence ?associativity l2 l1); + let time4 = Unix.gettimeofday () in + printf ("done (extending parser took %f, " ^^ + "extending pretty printer took %f)\n") + (time2 -. time1) (time4 -. time3); + flush stdout + | G.Executable (_, G.Command (_, G.Interpretation (_, l2, l3))) -> + prerr_endline "Adding interpretation ..."; flush stdout; + let time1 = Unix.gettimeofday () in + ignore (CicNotationRew.add_interpretation l2 l3); + let time2 = Unix.gettimeofday () in + printf "done (patterns compilation took %f seconds)\n" + (time2 -. time1); + flush stdout + | G.Executable (_, G.Command (_, G.Dump _)) -> + CicNotationParser.print_l2_pattern (); print_newline () + | G.Executable (_, G.Command (_, G.Render (_, uri))) -> + let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let annobj, _, _, id_to_sort, _, _, _ = + Cic2acic.acic_object_of_cic_object obj + in + let annterm = + match annobj with + | Cic.AConstant (_, _, _, _, ty, _, _) + | Cic.AVariable (_, _, _, ty, _, _) -> ty + | _ -> assert false + in + let time1 = Unix.gettimeofday () in + let t, id_to_uri = + CicNotationRew.ast_of_acic id_to_sort annterm + in + let time2 = Unix.gettimeofday () in + prerr_endline (sprintf "ast creation took %f seconds\n" + (time2 -. time1)); + prerr_endline "AST"; + prerr_endline (CicNotationPp.pp_term t); + flush stdout; + let time3 = Unix.gettimeofday () in + let t' = CicNotationRew.pp_ast t in + let time4 = Unix.gettimeofday () in + prerr_endline (sprintf "pretty printing took %f seconds\n" + (time4 -. time3)); + prerr_endline (CicNotationPp.pp_term t'); + dump_xml t' id_to_uri "out.xml" + | _ -> + prerr_endline "Unsupported statement" with | End_of_file -> raise End_of_file + | CicNotationParser.Parse_error (floc, msg) -> + let (x, y) = P.loc_of_floc floc in +(* let before = String.sub line 0 x in + let error = String.sub line x (y - x) in + let after = String.sub line y (String.length line - y) in + eprintf "%s%s%s\n" before error after; + prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) + prerr_endline (sprintf "Parse error at character %d-%d: %s" + (!char_count + x) (!char_count + y) msg); + errquit ignore_exn | exn -> prerr_endline - (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) + (sprintf "Uncaught exception: %s" (Printexc.to_string exn)); + errquit ignore_exn done with End_of_file -> () + +let _ = + let arg_spec = [ ] in + let usage = "" in + Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; + print_endline "Loading builtin notation ..."; + let ic = open_in (Helm_registry.get "notation.core_file") in + process_stream ~ignore_exn:true (Stream.of_channel ic); + close_in ic; + print_endline "done."; + flush stdout; + process_stream ~ignore_exn:false (Stream.of_channel stdin) +