-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
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 \
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
helm-cic \
helm-utf8_macros \
camlp4.gramlib \
- helm-cic_proof_checking \
helm-cic_transformations\
+ helm-cic_proof_checking \
ulex \
$(NULL)
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)
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
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
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";
("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)
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
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 ->
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
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
List.map2
(fun p t ->
match p with
- | Pt.VarPattern name -> name, t
+ | GrafiteAst.VarPattern name -> name, t
| _ -> assert false)
pl matched_terms
in
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
+
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 =
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
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: [
[ 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: [
| SYMBOL <:unicode<lambda>> (* λ *) -> `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: [
];
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<def>> (* ≝ *); body = term ->
let body = fold_binder `Lambda args body in
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<def>> (* ≝ *);
];
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 *)
| 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<Rightarrow>> (* ⇒ *);
]
];
(* }}} *)
-(* {{{ Grammar for interpretation, notation level 3 *)
- argument: [
- [ id = IDENT -> IdentArg (0, id)
- | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] 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} *)
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;
(** 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} *)
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 *)
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
(* 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 *)
-
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 []
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
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
| _ -> 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
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:
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
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
--- /dev/null
+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 }.
+
"\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 ; ) ]"
rec acc
@{ 'cons $a $acc }
}.
-print [1;2;3;4].
+check [1;2;3;4].
notation
"[ list1 a sep ; | b ]"
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 }.
"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"
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}
# 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 \] .
# 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.
notation \[ \LIST \NUM a \] for \FOLD left \[ 'a \] \LAMBDA acc \[ 'b \NUM a \].
+
--- /dev/null
+(* 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
+
+ (** <name, inductive/coinductive, type, constructor list>
+ * 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
+
--- /dev/null
+(* 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<vdash>>; 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<def>> ; 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<def>>; OPT SYMBOL "|";
+ fst_constructors = LIST0 constructor SEP SYMBOL "|";
+ tl = OPT [ "with";
+ types = LIST1 [
+ name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
+ 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<def>>; 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<eta>> (* η *) -> () ] 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<def>> ; 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<def>> (* ≝ *); body = term -> body ] ->
+ GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body))
+ | flavour = theorem_flavour; name = IDENT;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); 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))
+
--- /dev/null
+(* 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
+
file:///projects/helm/library/coq_contribs/
</key>
</section>
+ <section name="notation">
+ <key name="core_file">doc/core_notation.ma</key>
+ </section>
</helm_registry>
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\e[01;31m%s\e[00m%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\e[01;31m%s\e[00m%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)
+
projects / helm.git / commitdiff