diff --git a/src/HOL/SPARK/Tools/fdl_lexer.ML b/src/HOL/SPARK/Tools/fdl_lexer.ML --- a/src/HOL/SPARK/Tools/fdl_lexer.ML +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML @@ -1,279 +1,279 @@ (* Title: HOL/SPARK/Tools/fdl_lexer.ML Author: Stefan Berghofer Copyright: secunet Security Networks AG Lexical analyzer for fdl files. *) signature FDL_LEXER = sig type T type chars type banner type date type time datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF val tokenize: (chars -> 'a * chars) -> (chars -> T * chars) -> Position.T -> string -> 'a * T list val position_of: T -> Position.T val pos_of: T -> string val is_eof: T -> bool val stopper: T Scan.stopper val kind_of: T -> kind val content_of: T -> string val unparse: T -> string val is_proper: T -> bool val is_digit: string -> bool val c_comment: chars -> T * chars val curly_comment: chars -> T * chars val percent_comment: chars -> T * chars val vcg_header: chars -> (banner * (date * time) option) * chars val siv_header: chars -> (banner * (date * time) * (date * time) * (string * string)) * chars end; structure Fdl_Lexer: FDL_LEXER = struct (** tokens **) datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF; datatype T = Token of kind * string * Position.T; fun make_token k xs = Token (k, implode (map fst xs), case xs of [] => Position.none | (_, p) :: _ => p); fun kind_of (Token (k, _, _)) = k; fun is_proper (Token (Comment, _, _)) = false | is_proper _ = true; fun content_of (Token (_, s, _)) = s; fun unparse (Token (Traceability, s, _)) = "For " ^ s ^ ":" | unparse (Token (_, s, _)) = s; fun position_of (Token (_, _, pos)) = pos; val pos_of = Position.here o position_of; fun is_eof (Token (EOF, _, _)) = true | is_eof _ = false; fun mk_eof pos = Token (EOF, "", pos); val eof = mk_eof Position.none; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (position_of (List.last toks))) is_eof; fun leq_token (Token (_, s, _), Token (_, s', _)) = size s <= size s'; (** split up a string into a list of characters (with positions) **) type chars = (string * Position.T) list; fun is_char_eof ("", _) = true | is_char_eof _ = false; val char_stopper = Scan.stopper (K ("", Position.none)) is_char_eof; fun symbol (x : string, _ : Position.T) = x; fun explode_pos s pos = fst (fold_map (fn x => fn pos => - ((x, pos), Position.advance_symbol x pos)) (raw_explode s) pos); + ((x, pos), Position.symbol x pos)) (raw_explode s) pos); (** scanners **) val any = Scan.one (not o Scan.is_stopper char_stopper); fun prfx [] = Scan.succeed [] | prfx (x :: xs) = Scan.one (equal x o symbol) ::: prfx xs; val $$$ = prfx o raw_explode; val lexicon = Scan.make_lexicon (map raw_explode ["rule_family", "For", ":", "[", "]", "(", ")", ",", "&", ";", "=", ".", "..", "requires", "may_be_replaced_by", "may_be_deduced", "may_be_deduced_from", "are_interchangeable", "if", "end", "function", "procedure", "type", "var", "const", "array", "record", ":=", "of", "**", "*", "/", "div", "mod", "+", "-", "<>", "<", ">", "<=", ">=", "<->", "->", "not", "and", "or", "for_some", "for_all", "***", "!!!", "element", "update", "pending"]); fun keyword s = Scan.literal lexicon :|-- (fn xs => if map symbol xs = raw_explode s then Scan.succeed xs else Scan.fail); fun is_digit x = "0" <= x andalso x <= "9"; fun is_alpha x = "a" <= x andalso x <= "z" orelse "A" <= x andalso x <= "Z"; val is_underscore = equal "_"; val is_tilde = equal "~"; val is_newline = equal "\n"; val is_tab = equal "\t"; val is_space = equal " "; val is_whitespace = is_space orf is_tab orf is_newline; val is_whitespace' = is_space orf is_tab; val number = Scan.many1 (is_digit o symbol); val identifier = Scan.one (is_alpha o symbol) ::: Scan.many ((is_alpha orf is_digit orf is_underscore) o symbol) @@@ Scan.optional (Scan.one (is_tilde o symbol) >> single) []; val long_identifier = identifier @@@ Scan.repeats1 ($$$ "." @@@ identifier); val whitespace = Scan.many (is_whitespace o symbol); val whitespace1 = Scan.many1 (is_whitespace o symbol); val whitespace' = Scan.many (is_whitespace' o symbol); val newline = Scan.one (is_newline o symbol); fun beginning n cs = let val drop_blanks = drop_suffix is_whitespace; val all_cs = drop_blanks cs; val dots = if length all_cs > n then " ..." else ""; in (drop_blanks (take n all_cs) |> map (fn c => if is_whitespace c then " " else c) |> implode) ^ dots end; fun !!! text scan = let fun get_pos [] = " (end-of-input)" | get_pos ((_, pos) :: _) = Position.here pos; fun err (syms, msg) = fn () => text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^ (case msg of NONE => "" | SOME m => "\n" ^ m ()); in Scan.!! err scan end; val any_line' = Scan.many (not o (Scan.is_stopper char_stopper orf (is_newline o symbol))); val any_line = whitespace' |-- any_line' --| newline >> (implode o map symbol); fun gen_comment a b = $$$ a |-- !!! "unclosed comment" (Scan.repeat (Scan.unless ($$$ b) any) --| $$$ b) >> make_token Comment; val c_comment = gen_comment "/*" "*/"; val curly_comment = gen_comment "{" "}"; val percent_comment = $$$ "%" |-- any_line' >> make_token Comment; fun repeatn 0 _ = Scan.succeed [] | repeatn n p = Scan.one p ::: repeatn (n-1) p; (** header of *.vcg and *.siv files (see simplifier/load_provenance.pro) **) type banner = string * string * string; type date = string * string * string; type time = string * string * string * string option; val asterisks = Scan.repeat1 (Scan.one (equal "*" o symbol)); fun alphan n = repeatn n (is_alpha o symbol) >> (implode o map symbol); fun digitn n = repeatn n (is_digit o symbol) >> (implode o map symbol); val time = digitn 2 --| $$$ ":" -- digitn 2 --| $$$ ":" -- digitn 2 -- Scan.option ($$$ "." |-- digitn 2) >> (fn (((hr, mi), s), ms) => (hr, mi, s, ms)); val date = digitn 2 --| $$$ "-" -- alphan 3 --| $$$ "-" -- digitn 4 >> (fn ((d, m), y) => (d, m, y)); val banner = whitespace' |-- asterisks --| whitespace' --| newline :|-- (fn xs => (any_line -- any_line -- any_line >> (fn ((l1, l2), l3) => (l1, l2, l3))) --| whitespace' --| prfx (map symbol xs) --| whitespace' --| newline); val vcg_header = banner -- Scan.option (whitespace |-- $$$ "DATE :" |-- whitespace |-- date --| whitespace --| Scan.option ($$$ "TIME :" -- whitespace) -- time); val siv_header = banner --| whitespace -- ($$$ "CREATED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --| whitespace -- ($$$ "SIMPLIFIED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --| newline --| newline -- (any_line -- any_line) >> (fn (((b, c), s), ls) => (b, c, s, ls)); (** the main tokenizer **) fun scan header comment = !!! "bad header" header --| whitespace -- Scan.repeat (Scan.unless (Scan.one is_char_eof) (!!! "bad input" ( comment || (keyword "For" -- whitespace1) |-- Scan.repeat1 (Scan.unless (keyword ":") any) --| keyword ":" >> make_token Traceability || Scan.max leq_token (Scan.literal lexicon >> make_token Keyword) ( long_identifier >> make_token Long_Ident || identifier >> make_token Ident) || number >> make_token Number) --| whitespace)); fun tokenize header comment pos s = fst (Scan.finite char_stopper (Scan.error (scan header comment)) (explode_pos s pos)); end; diff --git a/src/Pure/General/position.ML b/src/Pure/General/position.ML --- a/src/Pure/General/position.ML +++ b/src/Pure/General/position.ML @@ -1,299 +1,299 @@ (* Title: Pure/General/position.ML Author: Makarius Source positions starting from 1; values <= 0 mean "absent". Count Isabelle symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a right-open interval offset .. end_offset (exclusive). *) signature POSITION = sig eqtype T val ord: T ord val make: Thread_Position.T -> T val dest: T -> Thread_Position.T val line_of: T -> int option val offset_of: T -> int option val end_offset_of: T -> int option val file_of: T -> string option val id_of: T -> string option - val advance_symbol: Symbol.symbol -> T -> T - val advance_symbol_explode: string -> T -> T + val symbol: Symbol.symbol -> T -> T + val symbol_explode: string -> T -> T val advance_offsets: int -> T -> T val distance_of: T * T -> int option val none: T val start: T val file_name: string -> Properties.T val file_only: string -> T val file: string -> T val line_file_only: int -> string -> T val line_file: int -> string -> T val line: int -> T val get_props: T -> Properties.T val id: string -> T val id_only: string -> T val put_id: string -> T -> T val copy_id: T -> T -> T val id_properties_of: T -> Properties.T val parse_id: T -> int option val adjust_offsets: (int -> int option) -> T -> T val of_properties: Properties.T -> T val properties_of: T -> Properties.T val offset_properties_of: T -> Properties.T val def_properties_of: T -> Properties.T val entity_markup: string -> string * T -> Markup.T val entity_properties_of: bool -> serial -> T -> Properties.T val markup: T -> Markup.T -> Markup.T val is_reported: T -> bool val is_reported_range: T -> bool val reported_text: T -> Markup.T -> string -> string val report_text: T -> Markup.T -> string -> unit val report: T -> Markup.T -> unit type report = T * Markup.T type report_text = report * string val reports_text: report_text list -> unit val reports: report list -> unit val store_reports: report_text list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit val append_reports: report_text list Unsynchronized.ref -> report list -> unit val here_strs: T -> string * string val here: T -> string val here_list: T list -> string type range = T * T val no_range: range val no_range_position: T -> T val range_position: range -> T val range: T * T -> range val range_of_properties: Properties.T -> range val properties_of_range: range -> Properties.T val thread_data: unit -> T val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b val default: T -> bool * T end; structure Position: POSITION = struct (* datatype position *) datatype T = Pos of (int * int * int) * Properties.T; fun dest2 f = apply2 (fn Pos p => f p); val ord = pointer_eq_ord (int_ord o dest2 (#1 o #1) ||| int_ord o dest2 (#2 o #1) ||| int_ord o dest2 (#3 o #1) ||| Properties.ord o dest2 #2); fun norm_props (props: Properties.T) = maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) [Markup.fileN, Markup.idN]; fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props); fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props}; fun valid (i: int) = i > 0; fun maybe_valid i = if valid i then SOME i else NONE; fun if_valid i i' = if valid i then i' else i; (* fields *) fun line_of (Pos ((i, _, _), _)) = maybe_valid i; fun offset_of (Pos ((_, j, _), _)) = maybe_valid j; fun end_offset_of (Pos ((_, _, k), _)) = maybe_valid k; fun file_of (Pos (_, props)) = Properties.get props Markup.fileN; fun id_of (Pos (_, props)) = Properties.get props Markup.idN; (* advance *) fun advance_count "\n" (i: int, j: int, k: int) = (if_valid i (i + 1), if_valid j (j + 1), k) | advance_count s (i, j, k) = if Symbol.not_eof s then (i, if_valid j (j + 1), k) else (i, j, k); fun invalid_count (i, j, _: int) = not (valid i orelse valid j); -fun advance_symbol sym (pos as (Pos (count, props))) = +fun symbol sym (pos as (Pos (count, props))) = if invalid_count count then pos else Pos (advance_count sym count, props); -val advance_symbol_explode = fold advance_symbol o Symbol.explode; +val symbol_explode = fold symbol o Symbol.explode; fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) = if offset = 0 orelse invalid_count count then pos else if offset < 0 then raise Fail "Illegal offset" else if valid i then raise Fail "Illegal line position" else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props); (* distance of adjacent positions *) fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) = if valid j andalso valid j' then SOME (j' - j) else NONE; (* make position *) val none = Pos ((0, 0, 0), []); val start = Pos ((1, 1, 0), []); fun file_name "" = [] | file_name name = [(Markup.fileN, name)]; fun file_only name = Pos ((0, 0, 0), file_name name); fun file name = Pos ((1, 1, 0), file_name name); fun line_file_only i name = Pos ((i, 0, 0), file_name name); fun line_file i name = Pos ((i, 1, 0), file_name name); fun line i = line_file i ""; fun get_props (Pos (_, props)) = props; fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]); fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]); fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props)); fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id); fun parse_id pos = Option.map Value.parse_int (id_of pos); fun id_properties_of pos = (case id_of pos of SOME id => [(Markup.idN, id)] | NONE => []); fun adjust_offsets adjust (pos as Pos (_, props)) = if is_none (file_of pos) then (case parse_id pos of SOME id => (case adjust id of SOME offset => let val Pos (count, _) = advance_offsets offset pos in Pos (count, Properties.remove Markup.idN props) end | NONE => pos) | NONE => pos) else pos; (* markup properties *) fun get props name = (case Properties.get props name of NONE => 0 | SOME s => Value.parse_int s); fun of_properties props = make {line = get props Markup.lineN, offset = get props Markup.offsetN, end_offset = get props Markup.end_offsetN, props = props}; fun value k i = if valid i then [(k, Value.print_int i)] else []; fun properties_of (Pos ((i, j, k), props)) = value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props; fun offset_properties_of (Pos ((_, j, k), _)) = value Markup.offsetN j @ value Markup.end_offsetN k; val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y)); fun entity_markup kind (name, pos) = Markup.entity kind name |> Markup.properties (def_properties_of pos); fun entity_properties_of def serial pos = if def then (Markup.defN, Value.print_int serial) :: properties_of pos else (Markup.refN, Value.print_int serial) :: def_properties_of pos; val markup = Markup.properties o properties_of; (* reports *) fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos); fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos); fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else ""; fun report_text pos markup txt = Output.report [reported_text pos markup txt]; fun report pos markup = report_text pos markup ""; type report = T * Markup.T; type report_text = report * string; val reports_text = map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "") #> Output.report; val reports = map (rpair "") #> reports_text; fun store_reports _ [] _ _ = () | store_reports (r: report_text list Unsynchronized.ref) ps markup x = let val ms = markup x in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end; fun append_reports (r: report_text list Unsynchronized.ref) reports = Unsynchronized.change r (append (map (rpair "") reports)); (* here: user output *) fun here_strs pos = (case (line_of pos, file_of pos) of (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")") | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")") | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")") | _ => if is_reported pos then ("", "\092<^here>") else ("", "")); fun here pos = let val props = properties_of pos; val (s1, s2) = here_strs pos; in if s2 = "" then "" else s1 ^ Markup.markup (Markup.properties props Markup.position) s2 end; val here_list = map here #> distinct (op =) #> implode; (* range *) type range = T * T; val no_range = (none, none); fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props); fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props); fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos'); fun range_of_properties props = let val pos = of_properties props; val pos' = make {line = get props Markup.end_lineN, offset = get props Markup.end_offsetN, end_offset = 0, props = props}; in (pos, pos') end; fun properties_of_range (pos, pos') = properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos')); (* thread data *) val thread_data = make o Thread_Position.get; fun setmp_thread_data pos = Thread_Position.setmp (dest pos); fun default pos = if pos = none then (false, thread_data ()) else (true, pos); end; diff --git a/src/Pure/General/symbol_pos.ML b/src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML +++ b/src/Pure/General/symbol_pos.ML @@ -1,308 +1,308 @@ (* Title: Pure/General/symbol_pos.ML Author: Makarius Symbols with explicit position information. *) signature SYMBOL_POS = sig type T = Symbol.symbol * Position.T type 'a scanner = T list -> 'a * T list val symbol: T -> Symbol.symbol val content: T list -> string val range: T list -> Position.range val is_eof: T -> bool val stopper: T Scan.stopper val !!! : Scan.message -> 'a scanner -> 'a scanner val $$ : Symbol.symbol -> T scanner val ~$$ : Symbol.symbol -> T scanner val $$$ : Symbol.symbol -> T list scanner val ~$$$ : Symbol.symbol -> T list scanner val scan_pos: Position.T scanner val scan_string_q: string -> (Position.T * (T list * Position.T)) scanner val scan_string_qq: string -> (Position.T * (T list * Position.T)) scanner val scan_string_bq: string -> (Position.T * (T list * Position.T)) scanner val recover_string_q: T list scanner val recover_string_qq: T list scanner val recover_string_bq: T list scanner val quote_string_q: string -> string val quote_string_qq: string -> string val quote_string_bq: string -> string val cartouche_content: T list -> T list val scan_cartouche: string -> T list scanner val scan_cartouche_content: string -> T list scanner val recover_cartouche: T list scanner val scan_comment: string -> T list scanner val scan_comment_body: string -> T list scanner val recover_comment: T list scanner val source: Position.T -> (Symbol.symbol, 'a) Source.source -> (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source type text = string val implode: T list -> text val implode_range: Position.range -> T list -> text * Position.range val explode_delete: text * Position.T -> T list * Position.T list val explode: text * Position.T -> T list val explode0: string -> T list val scan_ident: T list scanner val is_identifier: string -> bool val scan_nat: T list scanner val scan_float: T list scanner end; structure Symbol_Pos: SYMBOL_POS = struct (* type T *) type T = Symbol.symbol * Position.T; type 'a scanner = T list -> 'a * T list; fun symbol ((s, _): T) = s; val content = implode o map symbol; fun range (syms as (_, pos) :: _) = - let val pos' = List.last syms |-> Position.advance_symbol + let val pos' = List.last syms |-> Position.symbol in Position.range (pos, pos') end | range [] = Position.no_range; (* stopper *) fun mk_eof pos = (Symbol.eof, pos); val eof = mk_eof Position.none; val is_eof = Symbol.is_eof o symbol; val stopper = - Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance_symbol)) is_eof; + Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.symbol)) is_eof; (* basic scanners *) fun !!! text (scan: 'a scanner) = let fun get_pos [] = " (end-of-input)" | get_pos ((_, pos) :: _) = Position.here pos; fun err (syms, msg) = fn () => text () ^ get_pos syms ^ Markup.markup Markup.no_report (" at " ^ Symbol.beginning 10 (map symbol syms)) ^ (case msg of NONE => "" | SOME m => "\n" ^ m ()); in Scan.!! err scan end; fun $$ s = Scan.one (fn x => symbol x = s); fun ~$$ s = Scan.one (fn x => symbol x <> s); fun $$$ s = Scan.one (fn x => symbol x = s) >> single; fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single; val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos); (* scan string literals *) local val char_code = Scan.one (Symbol.is_ascii_digit o symbol) -- Scan.one (Symbol.is_ascii_digit o symbol) -- Scan.one (Symbol.is_ascii_digit o symbol) :|-- (fn (((a, pos), (b, _)), (c, _)) => let val (n, _) = Library.read_int [a, b, c] in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end); fun scan_str q err_prefix = $$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string") ($$$ q || $$$ "\\" || char_code) || Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.not_eof s) >> single; fun scan_strs q err_prefix = Scan.ahead ($$ q) |-- !!! (fn () => err_prefix ^ "unclosed string literal") ((scan_pos --| $$$ q) -- (Scan.repeats (scan_str q err_prefix) -- ($$$ q |-- scan_pos))); fun recover_strs q = $$$ q @@@ Scan.repeats (Scan.permissive (scan_str q "")); in val scan_string_q = scan_strs "'"; val scan_string_qq = scan_strs "\""; val scan_string_bq = scan_strs "`"; val recover_string_q = recover_strs "'"; val recover_string_qq = recover_strs "\""; val recover_string_bq = recover_strs "`"; end; (* quote string literals *) local fun char_code i = (if i < 10 then "00" else if i < 100 then "0" else "") ^ string_of_int i; fun quote_str q s = if Symbol.is_ascii_control s then "\\" ^ char_code (ord s) else if s = q orelse s = "\\" then "\\" ^ s else s; fun quote_string q = enclose q q o implode o map (quote_str q) o Symbol.explode; in val quote_string_q = quote_string "'"; val quote_string_qq = quote_string "\""; val quote_string_bq = quote_string "`"; end; (* nested text cartouches *) fun cartouche_content syms = let fun err () = error ("Malformed text cartouche: " ^ quote (content syms) ^ Position.here (#1 (range syms))); in (case syms of ("\", _) :: rest => (case rev rest of ("\", _) :: rrest => rev rrest | _ => err ()) | _ => err ()) end; val scan_cartouche_depth = Scan.repeat1 (Scan.depend (fn (depth: int option) => (case depth of SOME d => $$ Symbol.open_ >> pair (SOME (d + 1)) || (if d > 0 then Scan.one (fn (s, _) => s <> Symbol.close andalso Symbol.not_eof s) >> pair depth || $$ Symbol.close >> pair (if d = 1 then NONE else SOME (d - 1)) else Scan.fail) | NONE => Scan.fail))); fun scan_cartouche err_prefix = Scan.ahead ($$ Symbol.open_) |-- !!! (fn () => err_prefix ^ "unclosed text cartouche") (Scan.provide is_none (SOME 0) scan_cartouche_depth); fun scan_cartouche_content err_prefix = scan_cartouche err_prefix >> cartouche_content; val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth; (* ML-style comments *) local val scan_cmt = Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) || Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) || Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) || Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single; val scan_cmts = Scan.pass 0 (Scan.repeats scan_cmt); in fun scan_comment err_prefix = Scan.ahead ($$ "(" -- $$ "*") |-- !!! (fn () => err_prefix ^ "unclosed comment") ($$$ "(" @@@ $$$ "*" @@@ scan_cmts @@@ $$$ "*" @@@ $$$ ")"); fun scan_comment_body err_prefix = Scan.ahead ($$ "(" -- $$ "*") |-- !!! (fn () => err_prefix ^ "unclosed comment") ($$ "(" |-- $$ "*" |-- scan_cmts --| $$ "*" --| $$ ")"); val recover_comment = $$$ "(" @@@ $$$ "*" @@@ scan_cmts; end; (* source *) fun source pos = Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos => - Scan.one Symbol.not_eof >> (fn s => (Position.advance_symbol s pos, (s, pos)))))); + Scan.one Symbol.not_eof >> (fn s => (Position.symbol s pos, (s, pos)))))); (* compact representation -- with Symbol.DEL padding *) type text = string; fun pad [] = [] | pad [(s, _)] = [s] | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) = let - val end_pos1 = Position.advance_symbol s1 pos1; + val end_pos1 = Position.symbol s1 pos1; val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2))); in s1 :: replicate d Symbol.DEL @ pad rest end; val implode = implode o pad; fun implode_range (pos1, pos2) syms = let val syms' = (("", pos1) :: syms @ [("", pos2)]) in (implode syms', range syms') end; fun explode_delete (str, pos) = let val (res, _) = - fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance_symbol s p)) + fold (fn s => fn (res, p) => ((s, p) :: res, Position.symbol s p)) (Symbol.explode str) ([], Position.no_range_position pos); in fold (fn (s, p) => if s = Symbol.DEL then apsnd (cons p) else apfst (cons (s, p))) res ([], []) end; val explode = explode_delete #> #1; fun explode0 str = explode (str, Position.none); (* identifiers *) local val letter = Scan.one (symbol #> Symbol.is_letter); val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig); val sub = Scan.one (symbol #> (fn s => s = "\<^sub>")); in val scan_ident = letter ::: Scan.repeats (letdigs1 || sub ::: letdigs1); end; fun is_identifier s = Symbol.is_ascii_identifier s orelse (case try (Scan.finite stopper scan_ident) (explode0 s) of SOME (_, []) => true | _ => false); (* numerals *) val scan_nat = Scan.many1 (Symbol.is_digit o symbol); val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat; end; structure Basic_Symbol_Pos = (*not open by default*) struct val $$ = Symbol_Pos.$$; val ~$$ = Symbol_Pos.~$$; val $$$ = Symbol_Pos.$$$; val ~$$$ = Symbol_Pos.~$$$; end; type 'a scanner = 'a Symbol_Pos.scanner; diff --git a/src/Pure/Isar/token.ML b/src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML +++ b/src/Pure/Isar/token.ML @@ -1,802 +1,802 @@ (* Title: Pure/Isar/token.ML Author: Markus Wenzel, TU Muenchen Outer token syntax for Isabelle/Isar. *) signature TOKEN = sig datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option | (*special content*) Error of string | EOF val str_of_kind: kind -> string type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} type T type src = T list type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring} datatype value = Source of src | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | Attribute of morphism -> attribute | Declaration of declaration | Files of file Exn.result list val pos_of: T -> Position.T val adjust_offsets: (int -> int option) -> T -> T val eof: T val is_eof: T -> bool val not_eof: T -> bool val stopper: T Scan.stopper val kind_of: T -> kind val is_kind: kind -> T -> bool val is_command: T -> bool val keyword_with: (string -> bool) -> T -> bool val is_command_modifier: T -> bool val ident_with: (string -> bool) -> T -> bool val is_proper: T -> bool val is_comment: T -> bool val is_informal_comment: T -> bool val is_formal_comment: T -> bool val is_document_marker: T -> bool val is_ignored: T -> bool val is_begin_ignore: T -> bool val is_end_ignore: T -> bool val is_error: T -> bool val is_space: T -> bool val is_blank: T -> bool val is_newline: T -> bool val range_of: T list -> Position.range val core_range_of: T list -> Position.range val content_of: T -> string val source_of: T -> string val input_of: T -> Input.source val inner_syntax_of: T -> string val keyword_markup: bool * Markup.T -> string -> Markup.T val completion_report: T -> Position.report_text list val reports: Keyword.keywords -> T -> Position.report_text list val markups: Keyword.keywords -> T -> Markup.T list val unparse: T -> string val print: T -> string val text_of: T -> string * string val file_source: file -> Input.source val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T val get_value: T -> value option val reports_of_value: T -> Position.report list val name_value: name_value -> value val get_name: T -> name_value option val declare_maxidx: T -> Proof.context -> Proof.context val map_facts: (string option -> thm list -> thm list) -> T -> T val trim_context_src: src -> src val transform: morphism -> T -> T val init_assignable: T -> T val assign: value option -> T -> T val evaluate: ('a -> value) -> (T -> 'a) -> T -> 'a val closure: T -> T val pretty_value: Proof.context -> T -> Pretty.T val name_of_src: src -> string * Position.T val args_of_src: src -> T list val checked_src: src -> bool val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a val pretty_src: Proof.context -> src -> Pretty.T val ident_or_symbolic: string -> bool val read_cartouche: Symbol_Pos.T list -> T val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list val explode: Keyword.keywords -> Position.T -> string -> T list val explode0: Keyword.keywords -> string -> T list val print_name: Keyword.keywords -> string -> string val print_properties: Keyword.keywords -> Properties.T -> string val make: (int * int) * string -> Position.T -> T * Position.T val make_string: string * Position.T -> T val make_int: int -> T list val make_src: string * Position.T -> T list -> src type 'a parser = T list -> 'a * T list type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) val read_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a option val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context end; structure Token: TOKEN = struct (** tokens **) (* token kind *) datatype kind = (*immediate source*) Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | Float | Space | (*delimited content*) String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option | (*special content*) Error of string | EOF; val str_of_kind = fn Command => "command" | Keyword => "keyword" | Ident => "identifier" | Long_Ident => "long identifier" | Sym_Ident => "symbolic identifier" | Var => "schematic variable" | Type_Ident => "type variable" | Type_Var => "schematic type variable" | Nat => "natural number" | Float => "floating-point number" | Space => "white space" | String => "quoted string" | Alt_String => "back-quoted string" | Verbatim => "verbatim text" | Cartouche => "text cartouche" | Comment NONE => "informal comment" | Comment (SOME _) => "formal comment" | Error _ => "bad input" | EOF => "end-of-input"; val immediate_kinds = Vector.fromList [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space]; val delimited_kind = (fn String => true | Alt_String => true | Verbatim => true | Cartouche => true | Comment _ => true | _ => false); (* datatype token *) (*The value slot assigns an (optional) internal value to a token, usually as a side-effect of special scanner setup (see also args.ML). Note that an assignable ref designates an intermediate state of internalization -- it is NOT meant to persist.*) type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}; type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}; datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot and slot = Slot | Value of value option | Assignable of value option Unsynchronized.ref and value = Source of T list | Literal of bool * Markup.T | Name of name_value * morphism | Typ of typ | Term of term | Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of morphism -> attribute | Declaration of declaration | Files of file Exn.result list; type src = T list; (* position *) fun pos_of (Token ((_, (pos, _)), _, _)) = pos; fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos; fun adjust_offsets adjust (Token ((x, range), y, z)) = Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z); (* stopper *) fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _), _)) = true | is_eof _ = false; val not_eof = not o is_eof; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* kind of token *) fun kind_of (Token (_, (k, _), _)) = k; fun is_kind k (Token (_, (k', _), _)) = k = k'; val is_command = is_kind Command; fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x | keyword_with _ _ = false; val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified"); fun ident_with pred (Token (_, (Ident, x), _)) = pred x | ident_with _ _ = false; fun is_ignored (Token (_, (Space, _), _)) = true | is_ignored (Token (_, (Comment NONE, _), _)) = true | is_ignored _ = false; fun is_proper (Token (_, (Space, _), _)) = false | is_proper (Token (_, (Comment _, _), _)) = false | is_proper _ = true; fun is_comment (Token (_, (Comment _, _), _)) = true | is_comment _ = false; fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true | is_informal_comment _ = false; fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true | is_formal_comment _ = false; fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true | is_document_marker _ = false; fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true | is_begin_ignore _ = false; fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true | is_end_ignore _ = false; fun is_error (Token (_, (Error _, _), _)) = true | is_error _ = false; (* blanks and newlines -- space tokens obey lines *) fun is_space (Token (_, (Space, _), _)) = true | is_space _ = false; fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x) | is_blank _ = false; fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x | is_newline _ = false; (* range of tokens *) fun range_of (toks as tok :: _) = let val pos' = end_pos_of (List.last toks) in Position.range (pos_of tok, pos') end | range_of [] = Position.no_range; val core_range_of = drop_prefix is_ignored #> drop_suffix is_ignored #> range_of; (* token content *) fun content_of (Token (_, (_, x), _)) = x; fun source_of (Token ((source, _), _, _)) = source; fun input_of (Token ((source, range), (kind, _), _)) = Input.source (delimited_kind kind) source range; fun inner_syntax_of tok = let val x = content_of tok in if YXML.detect x then x else Syntax.implode_input (input_of tok) end; (* markup reports *) local val token_kind_markup = fn Var => (Markup.var, "") | Type_Ident => (Markup.tfree, "") | Type_Var => (Markup.tvar, "") | String => (Markup.string, "") | Alt_String => (Markup.alt_string, "") | Verbatim => (Markup.verbatim, "") | Cartouche => (Markup.cartouche, "") | Comment _ => (Markup.comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), "")); fun command_markups keywords x = if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties] else (if Keyword.is_proof_asm keywords x then [Markup.keyword3] else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper] else [Markup.keyword1]) |> map Markup.command_properties; in fun keyword_markup (important, keyword) x = if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter; fun completion_report tok = if is_kind Keyword tok then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok)) else []; fun reports keywords tok = if is_command tok then keyword_reports tok (command_markups keywords (content_of tok)) else if is_kind Keyword tok then keyword_reports tok [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)] else let val pos = pos_of tok; val (m, text) = token_kind_markup (kind_of tok); val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos)); in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end; fun markups keywords = map (#2 o #1) o reports keywords; end; (* unparse *) fun unparse (Token (_, (kind, x), _)) = (case kind of String => Symbol_Pos.quote_string_qq x | Alt_String => Symbol_Pos.quote_string_bq x | Verbatim => enclose "{*" "*}" x | Cartouche => cartouche x | Comment NONE => enclose "(*" "*)" x | EOF => "" | _ => x); fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok); fun text_of tok = let val k = str_of_kind (kind_of tok); val ms = markups Keyword.empty_keywords tok; val s = unparse tok; in if s = "" then (k, "") else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ Markup.markups ms s, "") else (k, Markup.markups ms s) end; (** associated values **) (* inlined file content *) fun file_source (file: file) = let val text = cat_lines (#lines file); - val end_pos = Position.advance_symbol_explode text (#pos file); + val end_pos = Position.symbol_explode text (#pos file); in Input.source true text (Position.range (#pos file, end_pos)) end; fun get_files (Token (_, _, Value (SOME (Files files)))) = files | get_files _ = []; fun put_files [] tok = tok | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files))) | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); (* access values *) fun get_value (Token (_, _, Value v)) = v | get_value _ = NONE; fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v))) | map_value _ tok = tok; (* reports of value *) fun get_assignable_value (Token (_, _, Assignable r)) = ! r | get_assignable_value (Token (_, _, Value v)) = v | get_assignable_value _ = NONE; fun reports_of_value tok = (case get_assignable_value tok of SOME (Literal markup) => let val pos = pos_of tok; val x = content_of tok; in if Position.is_reported pos then map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x) else [] end | _ => []); (* name value *) fun name_value a = Name (a, Morphism.identity); fun get_name tok = (case get_assignable_value tok of SOME (Name (a, _)) => SOME a | _ => NONE); (* maxidx *) fun declare_maxidx tok = (case get_value tok of SOME (Source src) => fold declare_maxidx src | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T) | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t) | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths | SOME (Attribute _) => I (* FIXME !? *) | SOME (Declaration decl) => (fn ctxt => let val ctxt' = Context.proof_map (Morphism.form decl) ctxt in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end) | _ => I); (* fact values *) fun map_facts f = map_value (fn v => (case v of Source src => Source (map (map_facts f) src) | Fact (a, ths) => Fact (a, f a ths) | _ => v)); val trim_context_src = (map o map_facts) (K (map Thm.trim_context)); (* transform *) fun transform phi = map_value (fn v => (case v of Source src => Source (map (transform phi) src) | Literal _ => v | Name (a, psi) => Name (a, psi $> phi) | Typ T => Typ (Morphism.typ phi T) | Term t => Term (Morphism.term phi t) | Fact (a, ths) => Fact (a, Morphism.fact phi ths) | Attribute att => Attribute (Morphism.transform phi att) | Declaration decl => Declaration (Morphism.transform phi decl) | Files _ => v)); (* static binding *) (*1st stage: initialize assignable slots*) fun init_assignable tok = (case tok of Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE)) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := NONE; tok)); (*2nd stage: assign values as side-effect of scanning*) fun assign v tok = (case tok of Token (x, y, Slot) => Token (x, y, Value v) | Token (_, _, Value _) => tok | Token (_, _, Assignable r) => (r := v; tok)); fun evaluate mk eval arg = let val x = eval arg in (assign (SOME (mk x)) arg; x) end; (*3rd stage: static closure of final values*) fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v) | closure tok = tok; (* pretty *) fun pretty_value ctxt tok = (case get_value tok of SOME (Literal markup) => let val x = content_of tok in Pretty.mark_str (keyword_markup markup x, x) end | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt)) | SOME (Typ T) => Syntax.pretty_typ ctxt T | SOME (Term t) => Syntax.pretty_term ctxt t | SOME (Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths)) | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok)); (* src *) fun dest_src ([]: src) = raise Fail "Empty token source" | dest_src (head :: args) = (head, args); fun name_of_src src = let val head = #1 (dest_src src); val name = (case get_name head of SOME {name, ...} => name | NONE => content_of head); in (name, pos_of head) end; val args_of_src = #2 o dest_src; fun pretty_src ctxt src = let val (head, args) = dest_src src; val prt_name = (case get_name head of SOME {print, ...} => Pretty.mark_str (print ctxt) | NONE => Pretty.str (content_of head)); in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end; fun checked_src (head :: _) = is_some (get_name head) | checked_src [] = true; fun check_src ctxt get_table src = let val (head, args) = dest_src src; val table = get_table ctxt; in (case get_name head of SOME {name, ...} => (src, Name_Space.get table name) | NONE => let val pos = pos_of head; val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos); val _ = Context_Position.report ctxt pos Markup.operator; val kind = Name_Space.kind_of (Name_Space.space_of_table table); fun print ctxt' = Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name; val value = name_value {name = name, kind = kind, print = print}; val head' = closure (assign (SOME value) head); in (head' :: args, x) end) end; (** scanners **) open Basic_Symbol_Pos; val err_prefix = "Outer lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* scan symbolic idents *) val scan_symid = Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) || Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single; fun is_symid str = (case try Symbol.explode str of SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s | SOME ss => forall Symbol.is_symbolic_char ss | _ => false); fun ident_or_symbolic "begin" = false | ident_or_symbolic ":" = true | ident_or_symbolic "::" = true | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; (* scan verbatim text *) val scan_verb = $$$ "*" --| Scan.ahead (~$$ "}") || Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single; val scan_verbatim = Scan.ahead ($$ "{" -- $$ "*") |-- !!! "unclosed verbatim text" ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); val recover_verbatim = $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb; (* scan cartouche *) val scan_cartouche = Symbol_Pos.scan_pos -- ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos); (* scan space *) fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n"; val scan_space = Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] || Scan.many space_symbol @@@ $$$ "\n"; (* scan comment *) val scan_comment = Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos); (** token sources **) local fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2; fun token k ss = Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot); fun token_range k (pos1, (ss, pos2)) = Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot); fun scan_token keywords = !!! "bad input" (Symbol_Pos.scan_string_qq err_prefix >> token_range String || Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String || scan_verbatim >> token_range Verbatim || scan_cartouche >> token_range Cartouche || scan_comment >> token_range (Comment NONE) || Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) || scan_space >> token Space || (Scan.max token_leq (Scan.max token_leq (Scan.literal (Keyword.major_keywords keywords) >> pair Command) (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword)) (Lexicon.scan_longid >> pair Long_Ident || Lexicon.scan_id >> pair Ident || Lexicon.scan_var >> pair Var || Lexicon.scan_tid >> pair Type_Ident || Lexicon.scan_tvar >> pair Type_Var || Symbol_Pos.scan_float >> pair Float || Symbol_Pos.scan_nat >> pair Nat || scan_symid >> pair Sym_Ident) >> uncurry token)); fun recover msg = (Symbol_Pos.recover_string_qq || Symbol_Pos.recover_string_bq || recover_verbatim || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); in fun make_source keywords {strict} = let val scan_strict = Scan.bulk (scan_token keywords); val scan = if strict then scan_strict else Scan.recover scan_strict recover; in Source.source Symbol_Pos.stopper scan end; fun read_cartouche syms = (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of SOME tok => tok | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms)))); end; (* explode *) fun tokenize keywords strict syms = Source.of_list syms |> make_source keywords strict |> Source.exhaust; fun explode keywords pos text = Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false}; fun explode0 keywords = explode keywords Position.none; (* print names in parsable form *) fun print_name keywords name = ((case explode keywords Position.none name of [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok)) | _ => true) ? Symbol_Pos.quote_string_qq) name; fun print_properties keywords = map (apply2 (print_name keywords) #> (fn (a, b) => a ^ " = " ^ b)) #> commas #> enclose "[" "]"; (* make *) fun make ((k, n), s) pos = let val pos' = Position.advance_offsets n pos; val range = Position.range (pos, pos'); val tok = if 0 <= k andalso k < Vector.length immediate_kinds then Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot) else (case explode Keyword.empty_keywords pos s of [tok] => tok | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot)) in (tok, pos') end; fun make_string (s, pos) = let val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none); val pos' = Position.no_range_position pos; in Token ((x, (pos', pos')), y, z) end; val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int; fun make_src a args = make_string a :: args; (** parsers **) type 'a parser = T list -> 'a * T list; type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list); (* read body -- e.g. antiquotation source *) fun read_body keywords scan = tokenize (Keyword.no_command_keywords keywords) {strict = true} #> filter is_proper #> Scan.read stopper scan; fun read_antiq keywords scan (syms, pos) = (case read_body keywords scan syms of SOME x => x | NONE => error ("Malformed antiquotation" ^ Position.here pos)); (* wrapped syntax *) fun syntax_generic scan src context = let val (name, pos) = name_of_src src; val old_reports = maps reports_of_value src; val args1 = map init_assignable (args_of_src src); fun reported_text () = if Context_Position.reports_enabled_generic context then let val new_reports = maps (reports_of_value o closure) args1 in if old_reports <> new_reports then map (fn (p, m) => Position.reported_text p m "") new_reports else [] end else []; in (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of (SOME x, (context', [])) => let val _ = Output.report (reported_text ()) in (x, context') end | (_, (context', args2)) => let val print_name = (case get_name (hd src) of NONE => quote name | SOME {kind, print, ...} => let val ctxt' = Context.proof_of context'; val (markup, xname) = print ctxt'; in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end); val print_args = if null args2 then "" else ":\n " ^ space_implode " " (map print args2); in error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^ Markup.markup_report (implode (reported_text ()))) end) end; fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof; end; type 'a parser = 'a Token.parser; type 'a context_parser = 'a Token.context_parser; diff --git a/src/Pure/ML/ml_lex.ML b/src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML +++ b/src/Pure/ML/ml_lex.ML @@ -1,394 +1,394 @@ (* Title: Pure/ML/ml_lex.ML Author: Makarius Lexical syntax for Isabelle/ML and Standard ML. *) signature ML_LEX = sig val keywords: string list datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | Space | Comment of Comment.kind option | Error of string | EOF eqtype token val stopper: token Scan.stopper val is_regular: token -> bool val is_improper: token -> bool val is_comment: token -> bool val set_range: Position.range -> token -> token val range_of: token -> Position.range val pos_of: token -> Position.T val end_pos_of: token -> Position.T val kind_of: token -> token_kind val content_of: token -> string val check_content_of: token -> string val flatten: token list -> string val source: (Symbol.symbol, 'a) Source.source -> (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source val tokenize: string -> token list val tokenize_range: Position.range -> string -> token list val read_text: Symbol_Pos.text * Position.T -> token Antiquote.antiquote list val read: Symbol_Pos.text -> token Antiquote.antiquote list val read_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list val read_source': {language: bool -> Markup.T, opaque_warning: bool, symbols: bool} -> token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list val read_source: Input.source -> token Antiquote.antiquote list val read_source_sml: Input.source -> token Antiquote.antiquote list val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list end; structure ML_Lex: ML_LEX = struct (** keywords **) val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as", "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn", "fun", "functor", "handle", "if", "in", "include", "infix", "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec", "sharing", "sig", "signature", "struct", "structure", "then", "type", "val", "where", "while", "with", "withtype"]; val keywords2 = ["and", "case", "do", "else", "end", "if", "in", "let", "local", "of", "sig", "struct", "then", "while", "with"]; val keywords3 = ["handle", "open", "raise"]; val lexicon = Scan.make_lexicon (map raw_explode keywords); (** tokens **) (* datatype token *) datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | Space | Comment of Comment.kind option | Error of string | EOF; datatype token = Token of Position.range * (token_kind * string); (* position *) fun set_range range (Token (_, x)) = Token (range, x); fun range_of (Token (range, _)) = range; val pos_of = #1 o range_of; val end_pos_of = #2 o range_of; (* stopper *) fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _))) = true | is_eof _ = false; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* token content *) fun kind_of (Token (_, (k, _))) = k; fun content_of (Token (_, (_, x))) = x; fun token_leq (tok, tok') = content_of tok <= content_of tok'; fun is_keyword (Token (_, (Keyword, _))) = true | is_keyword _ = false; fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x) | is_delimiter _ = false; fun is_regular (Token (_, (Error _, _))) = false | is_regular (Token (_, (EOF, _))) = false | is_regular _ = true; fun is_improper (Token (_, (Space, _))) = true | is_improper (Token (_, (Comment _, _))) = true | is_improper _ = false; fun is_comment (Token (_, (Comment _, _))) = true | is_comment _ = false; fun warning_opaque tok = (case tok of Token (_, (Keyword, ":>")) => warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\ \prefer non-opaque matching (:) possibly with abstype" ^ Position.here (pos_of tok)) | _ => ()); fun check_content_of tok = (case kind_of tok of Error msg => error msg | _ => content_of tok); (* flatten *) fun flatten_content (tok :: (toks as tok' :: _)) = Symbol.escape (check_content_of tok) :: (if is_improper tok orelse is_improper tok' then flatten_content toks else Symbol.space :: flatten_content toks) | flatten_content toks = map (Symbol.escape o check_content_of) toks; val flatten = implode o flatten_content; (* markup *) local val token_kind_markup = fn Type_Var => (Markup.ML_tvar, "") | Word => (Markup.ML_numeral, "") | Int => (Markup.ML_numeral, "") | Real => (Markup.ML_numeral, "") | Char => (Markup.ML_char, "") | String => (Markup.ML_string, "") | Comment _ => (Markup.ML_comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); in fun token_report (tok as Token ((pos, _), (kind, x))) = let val (markup, txt) = if not (is_keyword tok) then token_kind_markup kind else if is_delimiter tok then (Markup.ML_delimiter, "") else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "") else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "") else (Markup.ML_keyword1 |> Markup.keyword_properties, ""); in ((pos, markup), txt) end; end; (** scanners **) open Basic_Symbol_Pos; val err_prefix = "SML lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* identifiers *) local val scan_letdigs = Scan.many (Symbol.is_ascii_letdig o Symbol_Pos.symbol); val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) ::: scan_letdigs; val scan_symbolic = Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol); in val scan_ident = scan_alphanumeric || scan_symbolic; val scan_long_ident = Scan.repeats1 (scan_alphanumeric @@@ $$$ ".") @@@ (scan_ident || $$$ "="); val scan_type_var = $$$ "'" @@@ scan_letdigs; end; (* numerals *) local val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol); val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); val scan_sign = Scan.optional ($$$ "~") []; val scan_decint = scan_sign @@@ scan_dec; val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint; in val scan_word = $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex || $$$ "0" @@@ $$$ "w" @@@ scan_dec; val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec); val scan_rat = scan_decint @@@ Scan.optional ($$$ "/" @@@ scan_dec) []; val scan_real = scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] || scan_decint @@@ scan_exp; end; (* chars and strings *) val scan_blanks1 = Scan.many1 (Symbol.is_ascii_blank o Symbol_Pos.symbol); local val scan_escape = Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single || $$$ "^" @@@ (Scan.one (fn (s, _) => Char.ord #"@" <= ord s andalso ord s <= Char.ord #"_") >> single) || Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]); val scan_str = Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; val scan_gaps = Scan.repeats scan_gap; in val scan_char = $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\""; val recover_char = $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) []; val scan_string = Scan.ahead ($$ "\"") |-- !!! "unclosed string literal" ($$$ "\"" @@@ Scan.repeats (scan_gap || scan_str) @@@ $$$ "\""); val recover_string = $$$ "\"" @@@ Scan.repeats (scan_gap || Scan.permissive scan_str); end; (* rat antiquotation *) val rat_name = Symbol_Pos.explode ("Pure.rat ", Position.none); val scan_rat_antiq = Symbol_Pos.scan_pos -- ($$ "@" |-- Symbol_Pos.scan_pos -- scan_rat) -- Symbol_Pos.scan_pos >> (fn ((pos1, (pos2, body)), pos3) => {start = Position.range_position (pos1, pos2), stop = Position.none, range = Position.range (pos1, pos3), body = rat_name @ body}); (* scan tokens *) local fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss)); val scan_sml = scan_char >> token Char || scan_string >> token String || scan_blanks1 >> token Space || Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) || Scan.max token_leq (Scan.literal lexicon >> token Keyword) (scan_word >> token Word || scan_real >> token Real || scan_int >> token Int || scan_long_ident >> token Long_Ident || scan_ident >> token Ident || scan_type_var >> token Type_Var); val scan_sml_antiq = scan_sml >> Antiquote.Text; val scan_ml_antiq = Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) || Antiquote.scan_control >> Antiquote.Control || Antiquote.scan_antiq >> Antiquote.Antiq || scan_rat_antiq >> Antiquote.Antiq || scan_sml_antiq; fun recover msg = (recover_char || recover_string || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); fun reader {opaque_warning} scan syms = let val termination = if null syms then [] else let - val pos1 = List.last syms |-> Position.advance_symbol; - val pos2 = Position.advance_symbol Symbol.space pos1; + val pos1 = List.last syms |-> Position.symbol; + val pos2 = Position.symbol Symbol.space pos1; in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end; fun check (Antiquote.Text tok) = (check_content_of tok; if opaque_warning then warning_opaque tok else ()) | check _ = (); val input = Source.of_list syms |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan)) (fn msg => recover msg >> map Antiquote.Text)) |> Source.exhaust; val _ = Position.reports (Antiquote.antiq_reports input); val _ = Position.reports_text (maps (fn Antiquote.Text t => [token_report t] | _ => []) input); val _ = List.app check input; in input @ termination end; in fun source src = Symbol_Pos.source (Position.line 1) src |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_sml)) recover); val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust; fun tokenize_range range = tokenize #> map (set_range range); val read_text = reader {opaque_warning = true} scan_ml_antiq o Symbol_Pos.explode; fun read text = read_text (text, Position.none); fun read_range range = read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq); fun read_source' {language, symbols, opaque_warning} scan source = let val pos = Input.pos_of source; val _ = if Position.is_reported_range pos then Position.report pos (language (Input.is_delimited source)) else (); in Input.source_explode source |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p)) |> reader {opaque_warning = opaque_warning} scan end; val read_source = read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true} scan_ml_antiq; val read_source_sml = read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false} scan_sml_antiq; val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq; end; end; diff --git a/src/Pure/Pure.thy b/src/Pure/Pure.thy --- a/src/Pure/Pure.thy +++ b/src/Pure/Pure.thy @@ -1,1540 +1,1540 @@ (* Title: Pure/Pure.thy Author: Makarius The Pure theory, with definitions of Isar commands and some lemmas. *) theory Pure keywords "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites" "obtains" "shows" "when" "where" "|" :: quasi_command and "text" "txt" :: document_body and "text_raw" :: document_raw and "default_sort" :: thy_decl and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations" "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias" "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn and "axiomatization" :: thy_stmt and "external_file" "bibtex_file" "ROOTS_file" :: thy_load and "generate_file" :: thy_decl and "export_generated_files" :: diag and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix" and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML" and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) and "ML_val" "ML_command" :: diag % "ML" and "simproc_setup" :: thy_decl % "ML" and "setup" "local_setup" "attribute_setup" "method_setup" "declaration" "syntax_declaration" "parse_ast_translation" "parse_translation" "print_translation" "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" and "bundle" :: thy_decl_block and "unbundle" :: thy_decl and "include" "including" :: prf_decl and "print_bundles" :: diag and "context" "locale" "experiment" :: thy_decl_block and "interpret" :: prf_goal % "proof" and "interpretation" "global_interpretation" "sublocale" :: thy_goal and "class" :: thy_decl_block and "subclass" :: thy_goal and "instantiation" :: thy_decl_block and "instance" :: thy_goal and "overloading" :: thy_decl_block and "opening" :: quasi_command and "code_datatype" :: thy_decl and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt and "schematic_goal" :: thy_goal_stmt and "notepad" :: thy_decl_block and "have" :: prf_goal % "proof" and "hence" :: prf_goal % "proof" and "show" :: prf_asm_goal % "proof" and "thus" :: prf_asm_goal % "proof" and "then" "from" "with" :: prf_chain % "proof" and "note" :: prf_decl % "proof" and "supply" :: prf_script % "proof" and "using" "unfolding" :: prf_decl % "proof" and "fix" "assume" "presume" "define" :: prf_asm % "proof" and "consider" :: prf_goal % "proof" and "obtain" :: prf_asm_goal % "proof" and "guess" :: prf_script_asm_goal % "proof" and "let" "write" :: prf_decl % "proof" and "case" :: prf_asm % "proof" and "{" :: prf_open % "proof" and "}" :: prf_close % "proof" and "next" :: next_block % "proof" and "qed" :: qed_block % "proof" and "by" ".." "." "sorry" "\" :: "qed" % "proof" and "done" :: "qed_script" % "proof" and "oops" :: qed_global % "proof" and "defer" "prefer" "apply" :: prf_script % "proof" and "apply_end" :: prf_script % "proof" and "subgoal" :: prf_script_goal % "proof" and "proof" :: prf_block % "proof" and "also" "moreover" :: prf_decl % "proof" and "finally" "ultimately" :: prf_chain % "proof" and "back" :: prf_script % "proof" and "help" "print_commands" "print_options" "print_context" "print_theory" "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules" "print_theorems" "print_locales" "print_classes" "print_locale" "print_interps" "print_attributes" "print_simpset" "print_rules" "print_trans_rules" "print_methods" "print_antiquotations" "print_ML_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings" "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag and "print_state" :: diag and "welcome" :: diag and "end" :: thy_end and "realizers" :: thy_decl and "realizability" :: thy_decl and "extract_type" "extract" :: thy_decl and "find_theorems" "find_consts" :: diag and "named_theorems" :: thy_decl abbrevs "\\tag" = "\<^marker>\tag \" and "===>" = "===>" (*prevent replacement of very long arrows*) and "--->" = "\\" and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = "" and "hence" = "then have" and "thus" = "then show" begin section \Isar commands\ subsection \Other files\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\external_file\ "formal dependency on external file" (Resources.provide_parse_file >> (fn get_file => Toplevel.theory (#2 o get_file))); val _ = Outer_Syntax.command \<^command_keyword>\bibtex_file\ "check bibtex database file in Prover IDE" (Resources.provide_parse_file >> (fn get_file => Toplevel.theory (fn thy => let val ({lines, pos, ...}, thy') = get_file thy; val _ = Bibtex.check_database_output pos (cat_lines lines); in thy' end))); val _ = Outer_Syntax.command \<^command_keyword>\ROOTS_file\ "session ROOTS file" (Resources.provide_parse_file >> (fn get_file => Toplevel.theory (fn thy => let val ({src_path, lines, pos = pos0, ...}, thy') = get_file thy; val ctxt = Proof_Context.init_global thy'; val dir = Path.dir (Path.expand (Resources.master_directory thy' + src_path)); val _ = (lines, pos0) |-> fold (fn line => fn pos1 => let - val pos2 = Position.advance_symbol_explode line pos1; + val pos2 = Position.symbol_explode line pos1; val range = Position.range (pos1, pos2); val source = Input.source true line range; val _ = if line = "" then () else if String.isPrefix "#" line then Context_Position.report ctxt (#1 range) Markup.comment else (ignore (Resources.check_session_dir ctxt (SOME dir) source) handle ERROR msg => Output.error_message msg); - in pos2 |> Position.advance_symbol "\n" end); + in pos2 |> Position.symbol "\n" end); in thy' end))); val _ = Outer_Syntax.local_theory \<^command_keyword>\generate_file\ "generate source file, with antiquotations" (Parse.path_binding -- (\<^keyword>\=\ |-- Parse.embedded_input) >> Generated_Files.generate_file_cmd); val files_in_theory = (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) -- Scan.option (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.theory_name --| \<^keyword>\)\)); val _ = Outer_Syntax.command \<^command_keyword>\export_generated_files\ "export generated files from given theories" (Parse.and_list1 files_in_theory >> (fn args => Toplevel.keep (fn st => Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args))); val base_dir = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.path_input --| \<^keyword>\)\)) (Input.string ""); val external_files = Scan.repeat1 Parse.path_input -- base_dir; val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false; val executable = \<^keyword>\(\ |-- Parse.!!! (exe --| \<^keyword>\)\) >> SOME || Scan.succeed NONE; val export_files = Scan.repeat1 Parse.path_binding -- executable; val _ = Outer_Syntax.command \<^command_keyword>\compile_generated_files\ "compile generated files and export results" (Parse.and_list files_in_theory -- Scan.optional (\<^keyword>\external_files\ |-- Parse.!!! (Parse.and_list1 external_files)) [] -- Scan.optional (\<^keyword>\export_files\ |-- Parse.!!! (Parse.and_list1 export_files)) [] -- Scan.optional (\<^keyword>\export_prefix\ |-- Parse.path_binding) ("", Position.none) -- (Parse.where_ |-- Parse.!!! Parse.ML_source) >> (fn ((((args, external), export), export_prefix), source) => Toplevel.keep (fn st => Generated_Files.compile_generated_files_cmd (Toplevel.context_of st) args external export export_prefix source))); in end\ external_file "ROOT0.ML" external_file "ROOT.ML" subsection \Embedded ML text\ ML \ local val semi = Scan.option \<^keyword>\;\; val _ = Outer_Syntax.command \<^command_keyword>\ML_file\ "read and evaluate Isabelle/ML file" (Resources.parse_file --| semi >> ML_File.ML NONE); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_debug\ "read and evaluate Isabelle/ML file (with debugger information)" (Resources.parse_file --| semi >> ML_File.ML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_no_debug\ "read and evaluate Isabelle/ML file (no debugger information)" (Resources.parse_file --| semi >> ML_File.ML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file\ "read and evaluate Standard ML file" (Resources.parse_file --| semi >> ML_File.SML NONE); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_debug\ "read and evaluate Standard ML file (with debugger information)" (Resources.parse_file --| semi >> ML_File.SML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_no_debug\ "read and evaluate Standard ML file (no debugger information)" (Resources.parse_file --| semi >> ML_File.SML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_export\ "evaluate SML within Isabelle/ML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_export, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.theory (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) end)); val _ = Outer_Syntax.command \<^command_keyword>\SML_import\ "evaluate Isabelle/ML within SML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_import, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval_source flags source) #> Local_Theory.propagate_ml_env) end)); val _ = Outer_Syntax.command ("ML_export", \<^here>) "ML text within theory or local theory, and export to bootstrap environment" (Parse.ML_source >> (fn source => Toplevel.generic_theory (fn context => context |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle |> Config.put_generic ML_Env.ML_write_global true |> ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) |> Config.restore_generic ML_Env.ML_write_global context |> Config.restore_generic ML_Env.ML_environment context |> Local_Theory.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_prf\ "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> Proof.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_val\ "diagnostic ML text" (Parse.ML_source >> Isar_Cmd.ml_diag true); val _ = Outer_Syntax.command \<^command_keyword>\ML_command\ "diagnostic ML text (silent)" (Parse.ML_source >> Isar_Cmd.ml_diag false); val _ = Outer_Syntax.command \<^command_keyword>\setup\ "ML setup for global theory" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); val _ = Outer_Syntax.local_theory \<^command_keyword>\local_setup\ "ML setup for local theory" (Parse.ML_source >> Isar_Cmd.local_setup); val _ = Outer_Syntax.command \<^command_keyword>\oracle\ "declare oracle" (Parse.range Parse.name -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source) >> (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y))); val _ = Outer_Syntax.local_theory \<^command_keyword>\attribute_setup\ "define attribute in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\method_setup\ "define proof method in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\declaration\ "generic ML declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\syntax_declaration\ "generic ML syntax declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\simproc_setup\ "define simproc in ML" (Parse.name_position -- (\<^keyword>\(\ |-- Parse.enum1 "|" Parse.term --| \<^keyword>\)\ --| \<^keyword>\=\) -- Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c)); in end\ subsection \Theory commands\ subsubsection \Sorts and types\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\default_sort\ "declare default sort for explicit type variables" (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); val _ = Outer_Syntax.local_theory \<^command_keyword>\typedecl\ "type declaration" (Parse.type_args -- Parse.binding -- Parse.opt_mixfix >> (fn ((args, a), mx) => Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_synonym\ "declare type abbreviation" (Parse.type_args -- Parse.binding -- (\<^keyword>\=\ |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')) >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); in end\ subsubsection \Consts\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\judgment\ "declare object-logic judgment" (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\consts\ "declare constants" (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); in end\ subsubsection \Syntax and translations\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\nonterminal\ "declare syntactic type constructors (grammar nonterminal symbols)" (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); val _ = Outer_Syntax.command \<^command_keyword>\syntax\ "add raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\no_syntax\ "delete raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); val trans_pat = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\)\)) "logic" -- Parse.inner_syntax Parse.string; fun trans_arrow toks = ((\<^keyword>\\\ || \<^keyword>\=>\) >> K Syntax.Parse_Rule || (\<^keyword>\\\ || \<^keyword>\<=\) >> K Syntax.Print_Rule || (\<^keyword>\\\ || \<^keyword>\==\) >> K Syntax.Parse_Print_Rule) toks; val trans_line = trans_pat -- Parse.!!! (trans_arrow -- trans_pat) >> (fn (left, (arr, right)) => arr (left, right)); val _ = Outer_Syntax.command \<^command_keyword>\translations\ "add syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); val _ = Outer_Syntax.command \<^command_keyword>\no_translations\ "delete syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); in end\ subsubsection \Translation functions\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\parse_ast_translation\ "install parse ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); val _ = Outer_Syntax.command \<^command_keyword>\parse_translation\ "install parse translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_translation\ "install print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\typed_print_translation\ "install typed print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_ast_translation\ "install print ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); in end\ subsubsection \Specifications\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\definition\ "constant definition" (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => #2 oo Specification.definition_cmd decl params prems spec)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\abbreviation\ "constant abbreviation" (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec)); val axiomatization = Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a)); val _ = Outer_Syntax.command \<^command_keyword>\axiomatization\ "axiomatic constant specification" (Scan.optional Parse.vars [] -- Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], []) >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); val _ = Outer_Syntax.local_theory \<^command_keyword>\alias\ "name-space alias for constant" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.alias_cmd); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_alias\ "name-space alias for type constructor" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.type_alias_cmd); in end\ subsubsection \Notation\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\type_notation\ "add concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd true mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\no_type_notation\ "delete concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\notation\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\no_notation\ "delete concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd false mode args)); in end\ subsubsection \Theorems\ ML \ local val long_keyword = Parse_Spec.includes >> K "" || Parse_Spec.long_statement_keyword; val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); val short_statement = Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)); fun theorem spec schematic descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) => ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl))); val _ = theorem \<^command_keyword>\theorem\ false "theorem"; val _ = theorem \<^command_keyword>\lemma\ false "lemma"; val _ = theorem \<^command_keyword>\corollary\ false "corollary"; val _ = theorem \<^command_keyword>\proposition\ false "proposition"; val _ = theorem \<^command_keyword>\schematic_goal\ true "schematic goal"; in end\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\lemmas\ "define theorems" (Parse_Spec.name_facts -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\declare\ "declare theorems" (Parse.and_list1 Parse.thms1 -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes)); val _ = Outer_Syntax.local_theory \<^command_keyword>\named_theorems\ "declare named collection of theorems" (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >> fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); in end\ subsubsection \Hide names\ ML \ local fun hide_names command_keyword what hide parse prep = Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space") ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) => (Toplevel.theory (fn thy => let val ctxt = Proof_Context.init_global thy in fold (hide fully o prep ctxt) args thy end)))); val _ = hide_names \<^command_keyword>\hide_class\ "classes" Sign.hide_class Parse.class Proof_Context.read_class; val _ = hide_names \<^command_keyword>\hide_type\ "types" Sign.hide_type Parse.type_const ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_const\ "consts" Sign.hide_const Parse.const ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_fact\ "facts" Global_Theory.hide_fact Parse.name_position (Global_Theory.check_fact o Proof_Context.theory_of); in end\ subsection \Bundled declarations\ ML \ local val _ = Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\bundle\ "define bundle of declarations" ((Parse.binding --| \<^keyword>\=\) -- Parse.thms1 -- Parse.for_fixes >> (uncurry Bundle.bundle_cmd)) (Parse.binding --| Parse.begin >> Bundle.init); val _ = Outer_Syntax.local_theory \<^command_keyword>\unbundle\ "activate declarations from bundle in local theory" (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd); val _ = Outer_Syntax.command \<^command_keyword>\include\ "activate declarations from bundle in proof body" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\including\ "activate declarations from bundle in goal refinement" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\print_bundles\ "print bundles of declarations" (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of))); in end\ subsection \Local theory specifications\ subsubsection \Specification context\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\context\ "begin local theory context" (((Parse.name_position -- Scan.optional Parse_Spec.opening []) >> (fn (name, incls) => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd incls name)) || Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems))) --| Parse.begin); val _ = Outer_Syntax.command \<^command_keyword>\end\ "end context" (Scan.succeed (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o Toplevel.end_proof (K Proof.end_notepad))); in end\ subsubsection \Locales and interpretation\ ML \ local val locale_context_elements = Scan.repeat1 Parse_Spec.context_element; val locale_val = ((Parse_Spec.locale_expression -- Scan.optional Parse_Spec.opening []) || Parse_Spec.opening >> pair ([], [])) -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! locale_context_elements) [] || locale_context_elements >> pair (([], []), []); val _ = Outer_Syntax.command \<^command_keyword>\locale\ "define named specification context" (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- Parse.!!! locale_val) ((([], []), []), []) -- Parse.opt_begin >> (fn ((name, ((expr, includes), elems)), begin) => Toplevel.begin_main_target begin (Expression.add_locale_cmd name Binding.empty includes expr elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\experiment\ "open private specification context" (Scan.repeat Parse_Spec.context_element --| Parse.begin >> (fn elems => Toplevel.begin_main_target true (Experiment.experiment_cmd elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\interpret\ "prove interpretation of locale expression in proof context" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.proof (Interpretation.interpret_cmd expr))); val interpretation_args_with_defs = Parse.!!! Parse_Spec.locale_expression -- (Scan.optional (\<^keyword>\defines\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\=\ -- Parse.term))) ([])); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\global_interpretation\ "prove interpretation of locale expression into global theory" (interpretation_args_with_defs >> (fn (expr, defs) => Interpretation.global_interpretation_cmd expr defs)); val _ = Outer_Syntax.command \<^command_keyword>\sublocale\ "prove sublocale relation between a locale and a locale expression" ((Parse.name_position --| (\<^keyword>\\\ || \<^keyword>\<\) -- interpretation_args_with_defs >> (fn (loc, (expr, defs)) => Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs))) || interpretation_args_with_defs >> (fn (expr, defs) => Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs))); val _ = Outer_Syntax.command \<^command_keyword>\interpretation\ "prove interpretation of locale expression in local theory or into global theory" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr))); in end\ subsubsection \Type classes\ ML \ local val class_context_elements = Scan.repeat1 Parse_Spec.context_element; val class_val = ((Parse_Spec.class_expression -- Scan.optional Parse_Spec.opening []) || Parse_Spec.opening >> pair []) -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! class_context_elements) [] || class_context_elements >> pair ([], []); val _ = Outer_Syntax.command \<^command_keyword>\class\ "define type class" (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- class_val) (([], []), []) -- Parse.opt_begin >> (fn ((name, ((supclasses, includes), elems)), begin) => Toplevel.begin_main_target begin (Class_Declaration.class_cmd name includes supclasses elems #> snd))); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\subclass\ "prove a subclass relation" (Parse.class >> Class_Declaration.subclass_cmd); val _ = Outer_Syntax.command \<^command_keyword>\instantiation\ "instantiate and prove type arity" (Parse.multi_arity --| Parse.begin >> (fn arities => Toplevel.begin_main_target true (Class.instantiation_cmd arities))); val _ = Outer_Syntax.command \<^command_keyword>\instance\ "prove type arity or subclass relation" ((Parse.class -- ((\<^keyword>\\\ || \<^keyword>\<\) |-- Parse.!!! Parse.class) >> Class.classrel_cmd || Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof || Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I))); in end\ subsubsection \Arbitrary overloading\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\overloading\ "overloaded definitions" (Scan.repeat1 (Parse.name --| (\<^keyword>\==\ || \<^keyword>\\\) -- Parse.term -- Scan.optional (\<^keyword>\(\ |-- (\<^keyword>\unchecked\ >> K false) --| \<^keyword>\)\) true >> Scan.triple1) --| Parse.begin >> (fn operations => Toplevel.begin_main_target true (Overloading.overloading_cmd operations))); in end\ subsection \Proof commands\ ML \ local val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\notepad\ "begin proof context" (Parse.begin >> K Proof.begin_notepad); in end\ subsubsection \Statements\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\have\ "state local goal" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\show\ "state local goal, to refine pending subgoals" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\hence\ "old-style alias of \"then have\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\thus\ "old-style alias of \"then show\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2))); in end\ subsubsection \Local facts\ ML \ local val facts = Parse.and_list1 Parse.thms1; val _ = Outer_Syntax.command \<^command_keyword>\then\ "forward chaining" (Scan.succeed (Toplevel.proof Proof.chain)); val _ = Outer_Syntax.command \<^command_keyword>\from\ "forward chaining from given facts" (facts >> (Toplevel.proof o Proof.from_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\with\ "forward chaining from given and current facts" (facts >> (Toplevel.proof o Proof.with_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\note\ "define facts" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\supply\ "define facts during goal refinement (unstructured)" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\using\ "augment goal facts" (facts >> (Toplevel.proof o Proof.using_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\unfolding\ "unfold definitions in goal and facts" (facts >> (Toplevel.proof o Proof.unfolding_cmd)); in end\ subsubsection \Proof context\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\fix\ "fix local variables (Skolem constants)" (Parse.vars >> (Toplevel.proof o Proof.fix_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\assume\ "assume propositions" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\presume\ "assume propositions, to be established later" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\define\ "local definition (non-polymorphic)" ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b))); val _ = Outer_Syntax.command \<^command_keyword>\consider\ "state cases rule" (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\obtain\ "generalized elimination" (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); val _ = Outer_Syntax.command \<^command_keyword>\guess\ "wild guessing (unstructured)" (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\let\ "bind text variables" (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\=\ |-- Parse.term)) >> (Toplevel.proof o Proof.let_bind_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\write\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args))); val _ = Outer_Syntax.command \<^command_keyword>\case\ "invoke local context" (Parse_Spec.opt_thm_name ":" -- (\<^keyword>\(\ |-- Parse.!!! (Parse.name_position -- Scan.repeat (Parse.maybe Parse.binding) --| \<^keyword>\)\) || Parse.name_position >> rpair []) >> (Toplevel.proof o Proof.case_cmd)); in end\ subsubsection \Proof structure\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\{\ "begin explicit proof block" (Scan.succeed (Toplevel.proof Proof.begin_block)); val _ = Outer_Syntax.command \<^command_keyword>\}\ "end explicit proof block" (Scan.succeed (Toplevel.proof Proof.end_block)); val _ = Outer_Syntax.command \<^command_keyword>\next\ "enter next proof block" (Scan.succeed (Toplevel.proof Proof.next_block)); in end\ subsubsection \End proof\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\qed\ "conclude proof" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m))); val _ = Outer_Syntax.command \<^command_keyword>\by\ "terminal backward proof" (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) => (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2)))); val _ = Outer_Syntax.command \<^command_keyword>\..\ "default proof" (Scan.succeed Isar_Cmd.default_proof); val _ = Outer_Syntax.command \<^command_keyword>\.\ "immediate proof" (Scan.succeed Isar_Cmd.immediate_proof); val _ = Outer_Syntax.command \<^command_keyword>\done\ "done proof" (Scan.succeed Isar_Cmd.done_proof); val _ = Outer_Syntax.command \<^command_keyword>\sorry\ "skip proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\\\ "dummy proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\oops\ "forget proof" (Scan.succeed Toplevel.forget_proof); in end\ subsubsection \Proof steps\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\defer\ "shuffle internal proof state" (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer)); val _ = Outer_Syntax.command \<^command_keyword>\prefer\ "shuffle internal proof state" (Parse.nat >> (Toplevel.proof o Proof.prefer)); val _ = Outer_Syntax.command \<^command_keyword>\apply\ "initial goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m)))); val _ = Outer_Syntax.command \<^command_keyword>\apply_end\ "terminal goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m)))); val _ = Outer_Syntax.command \<^command_keyword>\proof\ "backward proof step" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Toplevel.proof (fn state => let val state' = state |> Proof.proof m |> Seq.the_result ""; val _ = Output.information (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state')); in state' end)))) in end\ subsubsection \Subgoal focus\ ML \ local val opt_fact_binding = Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) Binding.empty_atts; val for_params = Scan.optional (\<^keyword>\for\ |-- Parse.!!! ((Scan.option Parse.dots >> is_some) -- (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) (false, []); val _ = Outer_Syntax.command \<^command_keyword>\subgoal\ "focus on first subgoal within backward refinement" (opt_fact_binding -- (Scan.option (\<^keyword>\premises\ |-- Parse.!!! opt_fact_binding)) -- for_params >> (fn ((a, b), c) => Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c))); in end\ subsubsection \Calculation\ ML \ local val calculation_args = Scan.option (\<^keyword>\(\ |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\)\))); val _ = Outer_Syntax.command \<^command_keyword>\also\ "combine calculation and current facts" (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\finally\ "combine calculation and current facts, exhibit result" (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\moreover\ "augment calculation by current facts" (Scan.succeed (Toplevel.proof' Calculation.moreover)); val _ = Outer_Syntax.command \<^command_keyword>\ultimately\ "augment calculation by current facts, exhibit result" (Scan.succeed (Toplevel.proof' Calculation.ultimately)); val _ = Outer_Syntax.command \<^command_keyword>\print_trans_rules\ "print transitivity rules" (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); in end\ subsubsection \Proof navigation\ ML \ local fun report_back () = Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"]; val _ = Outer_Syntax.command \<^command_keyword>\back\ "explicit backtracking of proof command" (Scan.succeed (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o Toplevel.skip_proof report_back)); in end\ subsection \Diagnostic commands (for interactive mode only)\ ML \ local val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val _ = Outer_Syntax.command \<^command_keyword>\help\ "retrieve outer syntax commands according to name patterns" (Scan.repeat Parse.name >> (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats))); val _ = Outer_Syntax.command \<^command_keyword>\print_commands\ "print outer syntax commands" (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_options\ "print configuration options" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_context\ "print context of local theory target" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context))); val _ = Outer_Syntax.command \<^command_keyword>\print_theory\ "print logical theory contents" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_definitions\ "print dependencies of definitional theory content" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_syntax\ "print inner syntax of context" (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_defn_rules\ "print definitional rewrite rules of context" (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_abbrevs\ "print constant abbreviations of context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_theorems\ "print theorems of local theory or proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b))); val _ = Outer_Syntax.command \<^command_keyword>\print_locales\ "print locales of this theory" (Parse.opt_bang >> (fn verbose => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in Pretty.writeln (Locale.pretty_locales thy verbose) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_classes\ "print classes of this theory" (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_locale\ "print locale of this theory" (Parse.opt_bang -- Parse.name_position >> (fn (show_facts, raw_name) => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_locale thy show_facts name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_interps\ "print interpretations of locale for this theory or proof context" (Parse.name_position >> (fn raw_name => Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state; val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_registrations ctxt name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_attributes\ "print attributes of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_simpset\ "print context of Simplifier" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_rules\ "print intro/elim rules" (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_methods\ "print methods of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_antiquotations\ "print document antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_ML_antiquotations\ "print ML antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\locale_deps\ "visualize locale dependencies" (Scan.succeed (Toplevel.keep (Toplevel.theory_of #> (fn thy => Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) |> Graph_Display.display_graph_old)))); val _ = Outer_Syntax.command \<^command_keyword>\print_term_bindings\ "print term bindings of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_facts\ "print facts of proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_cases\ "print cases of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_statement\ "print theorems as long statements" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts); val _ = Outer_Syntax.command \<^command_keyword>\thm\ "print theorems" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms); val _ = Outer_Syntax.command \<^command_keyword>\prf\ "print proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false); val _ = Outer_Syntax.command \<^command_keyword>\full_prf\ "print full proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true); val _ = Outer_Syntax.command \<^command_keyword>\prop\ "read and print proposition" (opt_modes -- Parse.term >> Isar_Cmd.print_prop); val _ = Outer_Syntax.command \<^command_keyword>\term\ "read and print term" (opt_modes -- Parse.term >> Isar_Cmd.print_term); val _ = Outer_Syntax.command \<^command_keyword>\typ\ "read and print type" (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\::\ |-- Parse.!!! Parse.sort)) >> Isar_Cmd.print_type); val _ = Outer_Syntax.command \<^command_keyword>\print_codesetup\ "print code generator setup" (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_state\ "print current proof state (if present)" (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state)))); val _ = Outer_Syntax.command \<^command_keyword>\welcome\ "print welcome message" (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ())))); in end\ subsection \Dependencies\ ML \ local val theory_bounds = Parse.theory_name >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.theory_name --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\thy_deps\ "visualize theory dependencies" (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args))); val class_bounds = Parse.sort >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.sort --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\class_deps\ "visualize class dependencies" (Scan.option class_bounds -- Scan.option class_bounds >> (fn args => Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args))); val _ = Outer_Syntax.command \<^command_keyword>\thm_deps\ "print theorem dependencies (immediate non-transitive)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\ "print all oracles used in theorems (full graph of transitive dependencies)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val ctxt = Toplevel.context_of st; val thms = Attrib.eval_thms ctxt args; in Pretty.writeln (Thm_Deps.pretty_thm_oracles ctxt thms) end))); val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name); val _ = Outer_Syntax.command \<^command_keyword>\unused_thms\ "find unused theorems" (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); val check = Theory.check {long = false} ctxt; in Thm_Deps.unused_thms_cmd (case opt_range of NONE => (Theory.parents_of thy, [thy]) | SOME (xs, NONE) => (map check xs, [thy]) | SOME (xs, SOME ys) => (map check xs, map check ys)) |> map pretty_thm |> Pretty.writeln_chunks end))); in end\ subsubsection \Find consts and theorems\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\find_consts\ "find constants by name / type patterns" (Find_Consts.query_parser >> (fn spec => Toplevel.keep (fn st => Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec)))); val options = Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")")) (NONE, true); val _ = Outer_Syntax.command \<^command_keyword>\find_theorems\ "find theorems meeting specified criteria" (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) => Toplevel.keep (fn st => Pretty.writeln (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec)))); in end\ subsection \Code generation\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\code_datatype\ "define set of code datatype constructors" (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd)); in end\ subsection \Extraction of programs from proofs\ ML \ local val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") []; val _ = Outer_Syntax.command \<^command_keyword>\realizers\ "specify realizers for primitive axioms / theorems, together with correctness proof" (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >> (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); val _ = Outer_Syntax.command \<^command_keyword>\realizability\ "add equations characterizing realizability" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract_type\ "add equations characterizing type of extracted program" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract\ "extract terms from proofs" (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); in end\ section \Auxiliary lemmas\ subsection \Meta-level connectives in assumptions\ lemma meta_mp: assumes "PROP P \ PROP Q" and "PROP P" shows "PROP Q" by (rule \PROP P \ PROP Q\ [OF \PROP P\]) lemmas meta_impE = meta_mp [elim_format] lemma meta_spec: assumes "\x. PROP P x" shows "PROP P x" by (rule \\x. PROP P x\) lemmas meta_allE = meta_spec [elim_format] lemma swap_params: "(\x y. PROP P x y) \ (\y x. PROP P x y)" .. lemma equal_allI: \(\x. PROP P x) \ (\x. PROP Q x)\ if \\x. PROP P x \ PROP Q x\ by (simp only: that) subsection \Meta-level conjunction\ lemma all_conjunction: "(\x. PROP A x &&& PROP B x) \ ((\x. PROP A x) &&& (\x. PROP B x))" proof assume conj: "\x. PROP A x &&& PROP B x" show "(\x. PROP A x) &&& (\x. PROP B x)" proof - fix x from conj show "PROP A x" by (rule conjunctionD1) from conj show "PROP B x" by (rule conjunctionD2) qed next assume conj: "(\x. PROP A x) &&& (\x. PROP B x)" fix x show "PROP A x &&& PROP B x" proof - show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) qed qed lemma imp_conjunction: "(PROP A \ PROP B &&& PROP C) \ ((PROP A \ PROP B) &&& (PROP A \ PROP C))" proof assume conj: "PROP A \ PROP B &&& PROP C" show "(PROP A \ PROP B) &&& (PROP A \ PROP C)" proof - assume "PROP A" from conj [OF \PROP A\] show "PROP B" by (rule conjunctionD1) from conj [OF \PROP A\] show "PROP C" by (rule conjunctionD2) qed next assume conj: "(PROP A \ PROP B) &&& (PROP A \ PROP C)" assume "PROP A" show "PROP B &&& PROP C" proof - from \PROP A\ show "PROP B" by (rule conj [THEN conjunctionD1]) from \PROP A\ show "PROP C" by (rule conj [THEN conjunctionD2]) qed qed lemma conjunction_imp: "(PROP A &&& PROP B \ PROP C) \ (PROP A \ PROP B \ PROP C)" proof assume r: "PROP A &&& PROP B \ PROP C" assume ab: "PROP A" "PROP B" show "PROP C" proof (rule r) from ab show "PROP A &&& PROP B" . qed next assume r: "PROP A \ PROP B \ PROP C" assume conj: "PROP A &&& PROP B" show "PROP C" proof (rule r) from conj show "PROP A" by (rule conjunctionD1) from conj show "PROP B" by (rule conjunctionD2) qed qed declare [[ML_write_global = false]] end diff --git a/src/Tools/Haskell/Haskell.thy b/src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy +++ b/src/Tools/Haskell/Haskell.thy @@ -1,3519 +1,3519 @@ (* Title: Tools/Haskell/Haskell.thy Author: Makarius Support for Isabelle tools in Haskell. *) theory Haskell imports Main begin generate_file "Isabelle/Bytes.hs" = \ {- Title: Isabelle/Bytes.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Compact byte strings. See \<^file>\$ISABELLE_HOME/src/Pure/General/bytes.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/General/bytes.scala\. -} {-# LANGUAGE TypeApplications #-} module Isabelle.Bytes ( Bytes, make, unmake, pack, unpack, empty, null, length, index, all, any, head, last, take, drop, isPrefixOf, isSuffixOf, concat, space, spaces, char, all_char, any_char, byte, singleton ) where import Prelude hiding (null, length, all, any, head, last, take, drop, concat) import qualified Data.ByteString.Short as ShortByteString import Data.ByteString.Short (ShortByteString) import qualified Data.ByteString as ByteString import Data.ByteString (ByteString) import qualified Data.List as List import Data.Word (Word8) import Data.Array (Array, array, (!)) type Bytes = ShortByteString make :: ByteString -> Bytes make = ShortByteString.toShort unmake :: Bytes -> ByteString unmake = ShortByteString.fromShort pack :: [Word8] -> Bytes pack = ShortByteString.pack unpack :: Bytes -> [Word8] unpack = ShortByteString.unpack empty :: Bytes empty = ShortByteString.empty null :: Bytes -> Bool null = ShortByteString.null length :: Bytes -> Int length = ShortByteString.length index :: Bytes -> Int -> Word8 index = ShortByteString.index all :: (Word8 -> Bool) -> Bytes -> Bool all p = List.all p . unpack any :: (Word8 -> Bool) -> Bytes -> Bool any p = List.any p . unpack head :: Bytes -> Word8 head bytes = index bytes 0 last :: Bytes -> Word8 last bytes = index bytes (length bytes - 1) take :: Int -> Bytes -> Bytes take n = pack . List.take n . unpack drop :: Int -> Bytes -> Bytes drop n = pack . List.drop n . unpack isPrefixOf :: Bytes -> Bytes -> Bool isPrefixOf bs1 bs2 = n1 <= n2 && List.all (\i -> index bs1 i == index bs2 i) [0 .. n1 - 1] where n1 = length bs1; n2 = length bs2 isSuffixOf :: Bytes -> Bytes -> Bool isSuffixOf bs1 bs2 = n1 <= n2 && List.all (\i -> index bs1 i == index bs2 (i + k)) [0 .. n1 - 1] where n1 = length bs1; n2 = length bs2; k = n2 - n1 concat :: [Bytes] -> Bytes concat = mconcat space :: Word8 space = 32 small_spaces :: Array Int Bytes small_spaces = array (0, 64) [(i, pack (replicate i space)) | i <- [0 .. 64]] spaces :: Int -> Bytes spaces n = if n < 64 then small_spaces ! n else concat ((small_spaces ! (n `mod` 64)) : replicate (n `div` 64) (small_spaces ! 64)) char :: Word8 -> Char char = toEnum . fromEnum all_char :: (Char -> Bool) -> Bytes -> Bool all_char pred = all (pred . char) any_char :: (Char -> Bool) -> Bytes -> Bool any_char pred = any (pred . char) byte :: Char -> Word8 byte = toEnum . fromEnum singletons :: Array Word8 Bytes singletons = array (minBound, maxBound) [(i, make (ByteString.singleton i)) | i <- [minBound .. maxBound]] singleton :: Word8 -> Bytes singleton b = singletons ! b \ generate_file "Isabelle/UTF8.hs" = \ {- Title: Isabelle/UTF8.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Variations on UTF-8. See \<^file>\$ISABELLE_HOME/src/Pure/General/utf8.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/General/utf8.scala\. -} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} module Isabelle.UTF8 ( setup, setup3, Recode (..) ) where import qualified System.IO as IO import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Text.Encoding as Encoding import qualified Data.Text.Encoding.Error as Error import Data.ByteString (ByteString) import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) setup :: IO.Handle -> IO () setup h = do IO.hSetEncoding h IO.utf8 IO.hSetNewlineMode h IO.noNewlineTranslation setup3 :: IO.Handle -> IO.Handle -> IO.Handle -> IO () setup3 h1 h2 h3 = do setup h1 setup h2 setup h3 class Recode a b where encode :: a -> b decode :: b -> a instance Recode Text ByteString where encode :: Text -> ByteString encode = Encoding.encodeUtf8 decode :: ByteString -> Text decode = Encoding.decodeUtf8With Error.lenientDecode instance Recode Text Bytes where encode :: Text -> Bytes encode = Bytes.make . encode decode :: Bytes -> Text decode = decode . Bytes.unmake instance Recode String ByteString where encode :: String -> ByteString encode = encode . Text.pack decode :: ByteString -> String decode = Text.unpack . decode instance Recode String Bytes where encode :: String -> Bytes encode = encode . Text.pack decode :: Bytes -> String decode = Text.unpack . decode \ generate_file "Isabelle/Library.hs" = \ {- Title: Isabelle/Library.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Basic library of Isabelle idioms. See also \<^file>\$ISABELLE_HOME/src/Pure/General/basics.ML\, \<^file>\$ISABELLE_HOME/src/Pure/library.ML\. -} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} module Isabelle.Library ( (|>), (|->), (#>), (#->), fold, fold_rev, single, map_index, get_index, separate, StringLike, STRING (..), TEXT (..), BYTES (..), show_bytes, show_text, proper_string, quote, space_implode, commas, commas_quote, cat_lines, space_explode, split_lines, trim_line) where import qualified Data.Text as Text import Data.Text (Text) import qualified Data.Text.Lazy as Lazy import Data.String (IsString) import qualified Data.List.Split as Split import qualified Isabelle.Symbol as Symbol import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.UTF8 as UTF8 {- functions -} (|>) :: a -> (a -> b) -> b x |> f = f x (|->) :: (a, b) -> (a -> b -> c) -> c (x, y) |-> f = f x y (#>) :: (a -> b) -> (b -> c) -> a -> c (f #> g) x = x |> f |> g (#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d (f #-> g) x = x |> f |-> g {- lists -} fold :: (a -> b -> b) -> [a] -> b -> b fold _ [] y = y fold f (x : xs) y = fold f xs (f x y) fold_rev :: (a -> b -> b) -> [a] -> b -> b fold_rev _ [] y = y fold_rev f (x : xs) y = f x (fold_rev f xs y) single :: a -> [a] single x = [x] map_index :: ((Int, a) -> b) -> [a] -> [b] map_index f = map_aux 0 where map_aux _ [] = [] map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b) get_index f = get_aux 0 where get_aux _ [] = Nothing get_aux i (x : xs) = case f x of Nothing -> get_aux (i + 1) xs Just y -> Just (i, y) separate :: a -> [a] -> [a] separate s (x : (xs @ (_ : _))) = x : s : separate s xs separate _ xs = xs; {- string-like interfaces -} class (IsString a, Monoid a, Eq a, Ord a) => StringLike a where space_explode :: Char -> a -> [a] trim_line :: a -> a gen_trim_line :: Int -> (Int -> Char) -> (Int -> a -> a) -> a -> a gen_trim_line n at trim s = if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then trim (n - 2) s else if n >= 1 && Symbol.is_ascii_line_terminator (at (n - 1)) then trim (n - 1) s else s instance StringLike String where space_explode :: Char -> String -> [String] space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c))) trim_line :: String -> String trim_line s = gen_trim_line (length s) ((!!) s) take s instance StringLike Text where space_explode :: Char -> Text -> [Text] space_explode c str = if Text.null str then [] else if Text.all (/= c) str then [str] else map Text.pack $ space_explode c $ Text.unpack str trim_line :: Text -> Text trim_line s = gen_trim_line (Text.length s) (Text.index s) Text.take s instance StringLike Lazy.Text where space_explode :: Char -> Lazy.Text -> [Lazy.Text] space_explode c str = if Lazy.null str then [] else if Lazy.all (/= c) str then [str] else map Lazy.pack $ space_explode c $ Lazy.unpack str trim_line :: Lazy.Text -> Lazy.Text trim_line = Lazy.fromStrict . trim_line . Lazy.toStrict instance StringLike Bytes where space_explode :: Char -> Bytes -> [Bytes] space_explode c str = if Bytes.null str then [] else if Bytes.all_char (/= c) str then [str] else explode (Bytes.unpack str) where explode rest = case span (/= (Bytes.byte c)) rest of (_, []) -> [Bytes.pack rest] (prfx, _ : rest') -> Bytes.pack prfx : explode rest' trim_line :: Bytes -> Bytes trim_line s = gen_trim_line (Bytes.length s) (Bytes.char . Bytes.index s) Bytes.take s class StringLike a => STRING a where make_string :: a -> String instance STRING String where make_string = id instance STRING Text where make_string = Text.unpack instance STRING Lazy.Text where make_string = Lazy.unpack instance STRING Bytes where make_string = UTF8.decode class StringLike a => TEXT a where make_text :: a -> Text instance TEXT String where make_text = Text.pack instance TEXT Text where make_text = id instance TEXT Lazy.Text where make_text = Lazy.toStrict instance TEXT Bytes where make_text = UTF8.decode class StringLike a => BYTES a where make_bytes :: a -> Bytes instance BYTES String where make_bytes = UTF8.encode instance BYTES Text where make_bytes = UTF8.encode instance BYTES Lazy.Text where make_bytes = UTF8.encode . Lazy.toStrict instance BYTES Bytes where make_bytes = id show_bytes :: Show a => a -> Bytes show_bytes = make_bytes . show show_text :: Show a => a -> Text show_text = make_text . show {- strings -} proper_string :: StringLike a => a -> Maybe a proper_string s = if s == "" then Nothing else Just s quote :: StringLike a => a -> a quote s = "\"" <> s <> "\"" space_implode :: StringLike a => a -> [a] -> a space_implode s = mconcat . separate s commas, commas_quote :: StringLike a => [a] -> a commas = space_implode ", " commas_quote = commas . map quote split_lines :: StringLike a => a -> [a] split_lines = space_explode '\n' cat_lines :: StringLike a => [a] -> a cat_lines = space_implode "\n" \ generate_file "Isabelle/Symbol.hs" = \ {- Title: Isabelle/Symbols.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Isabelle text symbols. See \<^file>\$ISABELLE_HOME/src/Pure/General/symbol.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/General/symbol_explode.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Symbol ( is_ascii_letter, is_ascii_digit, is_ascii_hex, is_ascii_quasi, is_ascii_blank, is_ascii_line_terminator, is_ascii_letdig, is_ascii_identifier, Symbol, explode ) where import Data.Word (Word8) import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) {- ASCII characters -} is_ascii_letter :: Char -> Bool is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' is_ascii_digit :: Char -> Bool is_ascii_digit c = '0' <= c && c <= '9' is_ascii_hex :: Char -> Bool is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f' is_ascii_quasi :: Char -> Bool is_ascii_quasi c = c == '_' || c == '\'' is_ascii_blank :: Char -> Bool is_ascii_blank c = c `elem` (" \t\n\11\f\r" :: String) is_ascii_line_terminator :: Char -> Bool is_ascii_line_terminator c = c == '\r' || c == '\n' is_ascii_letdig :: Char -> Bool is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c is_ascii_identifier :: String -> Bool is_ascii_identifier s = not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s {- explode symbols: ASCII, UTF8, named -} type Symbol = Bytes is_utf8 :: Word8 -> Bool is_utf8 b = b >= 128 is_utf8_trailer :: Word8 -> Bool is_utf8_trailer b = 128 <= b && b < 192 is_utf8_control :: Word8 -> Bool is_utf8_control b = 128 <= b && b < 160 (|>) :: a -> (a -> b) -> b x |> f = f x explode :: Bytes -> [Symbol] explode string = scan 0 where byte = Bytes.index string substring i j = if i == j - 1 then Bytes.singleton (byte i) else Bytes.pack (map byte [i .. j - 1]) n = Bytes.length string test pred i = i < n && pred (byte i) test_char pred i = i < n && pred (Bytes.char (byte i)) many pred i = if test pred i then many pred (i + 1) else i maybe_char c i = if test_char (== c) i then i + 1 else i maybe_ascii_id i = if test_char is_ascii_letter i then many (is_ascii_letdig . Bytes.char) (i + 1) else i scan i = if i < n then let b = byte i c = Bytes.char b in {-encoded newline-} if c == '\r' then "\n" : scan (maybe_char '\n' (i + 1)) {-pseudo utf8: encoded ascii control-} else if b == 192 && test is_utf8_control (i + 1) && not (test is_utf8 (i + 2)) then Bytes.singleton (byte (i + 1) - 128) : scan (i + 2) {-utf8-} else if is_utf8 b then let j = many is_utf8_trailer (i + 1) in substring i j : scan j {-named symbol-} else if c == '\\' && test_char (== '<') (i + 1) then let j = (i + 2) |> maybe_char '^' |> maybe_ascii_id |> maybe_char '>' in substring i j : scan j {-single character-} else Bytes.singleton b : scan (i + 1) else [] \ generate_file "Isabelle/Buffer.hs" = \ {- Title: Isabelle/Buffer.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Efficient buffer of byte strings. See also \<^file>\$ISABELLE_HOME/src/Pure/General/buffer.ML\. -} module Isabelle.Buffer (T, empty, add, content) where import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) newtype T = Buffer [Bytes] empty :: T empty = Buffer [] add :: Bytes -> T -> T add b (Buffer bs) = Buffer (if Bytes.null b then bs else b : bs) content :: T -> Bytes content (Buffer bs) = Bytes.concat (reverse bs) \ generate_file "Isabelle/Value.hs" = \ {- Title: Isabelle/Value.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Plain values, represented as string. See also \<^file>\$ISABELLE_HOME/src/Pure/General/value.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Value (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real) where import qualified Data.List as List import qualified Text.Read as Read import Isabelle.Bytes (Bytes) import Isabelle.Library {- bool -} print_bool :: Bool -> Bytes print_bool True = "true" print_bool False = "false" parse_bool :: Bytes -> Maybe Bool parse_bool "true" = Just True parse_bool "false" = Just False parse_bool _ = Nothing {- nat -} parse_nat :: Bytes -> Maybe Int parse_nat s = case Read.readMaybe (make_string s) of Just n | n >= 0 -> Just n _ -> Nothing {- int -} print_int :: Int -> Bytes print_int = show_bytes parse_int :: Bytes -> Maybe Int parse_int = Read.readMaybe . make_string {- real -} print_real :: Double -> Bytes print_real x = let s = show x in case span (/= '.') s of (a, '.' : b) | List.all (== '0') b -> make_bytes a _ -> make_bytes s parse_real :: Bytes -> Maybe Double parse_real = Read.readMaybe . make_string \ generate_file "Isabelle/Properties.hs" = \ {- Title: Isabelle/Properties.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Property lists. See also \<^file>\$ISABELLE_HOME/src/Pure/General/properties.ML\. -} module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove) where import qualified Data.List as List import Isabelle.Bytes (Bytes) type Entry = (Bytes, Bytes) type T = [Entry] defined :: T -> Bytes -> Bool defined props name = any (\(a, _) -> a == name) props get :: T -> Bytes -> Maybe Bytes get props name = List.lookup name props get_value :: (Bytes -> Maybe a) -> T -> Bytes -> Maybe a get_value parse props name = case get props name of Nothing -> Nothing Just s -> parse s put :: Entry -> T -> T put entry props = entry : remove (fst entry) props remove :: Bytes -> T -> T remove name props = if defined props name then filter (\(a, _) -> a /= name) props else props \ generate_file "Isabelle/Markup.hs" = \ {- Title: Isabelle/Markup.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Quasi-abstract markup elements. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/markup.ML\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.Markup ( T, empty, is_empty, properties, nameN, name, xnameN, xname, kindN, bindingN, binding, entityN, entity, defN, refN, completionN, completion, no_completionN, no_completion, lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position, expressionN, expression, citationN, citation, pathN, path, urlN, url, docN, doc, markupN, consistentN, unbreakableN, indentN, widthN, blockN, block, breakN, break, fbreakN, fbreak, itemN, item, wordsN, words, tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var, numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string, inner_cartoucheN, inner_cartouche, token_rangeN, token_range, sortingN, sorting, typingN, typing, class_parameterN, class_parameter, antiquotedN, antiquoted, antiquoteN, antiquote, paragraphN, paragraph, text_foldN, text_fold, keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword, improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string, verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1, comment2N, comment2, comment3N, comment3, forkedN, forked, joinedN, joined, runningN, running, finishedN, finished, failedN, failed, canceledN, canceled, initializedN, initialized, finalizedN, finalized, consolidatedN, consolidated, writelnN, writeln, stateN, state, informationN, information, tracingN, tracing, warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report, intensifyN, intensify, Output, no_output) where import Prelude hiding (words, error, break) import Isabelle.Library import qualified Isabelle.Properties as Properties import qualified Isabelle.Value as Value import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) {- basic markup -} type T = (Bytes, Properties.T) empty :: T empty = ("", []) is_empty :: T -> Bool is_empty ("", _) = True is_empty _ = False properties :: Properties.T -> T -> T properties more_props (elem, props) = (elem, fold_rev Properties.put more_props props) markup_elem :: Bytes -> T markup_elem name = (name, []) markup_string :: Bytes -> Bytes -> Bytes -> T markup_string name prop = \s -> (name, [(prop, s)]) {- misc properties -} nameN :: Bytes nameN = \Markup.nameN\ name :: Bytes -> T -> T name a = properties [(nameN, a)] xnameN :: Bytes xnameN = \Markup.xnameN\ xname :: Bytes -> T -> T xname a = properties [(xnameN, a)] kindN :: Bytes kindN = \Markup.kindN\ {- formal entities -} bindingN :: Bytes bindingN = \Markup.bindingN\ binding :: T binding = markup_elem bindingN entityN :: Bytes entityN = \Markup.entityN\ entity :: Bytes -> Bytes -> T entity kind name = (entityN, (if Bytes.null name then [] else [(nameN, name)]) <> (if Bytes.null kind then [] else [(kindN, kind)])) defN :: Bytes defN = \Markup.defN\ refN :: Bytes refN = \Markup.refN\ {- completion -} completionN :: Bytes completionN = \Markup.completionN\ completion :: T completion = markup_elem completionN no_completionN :: Bytes no_completionN = \Markup.no_completionN\ no_completion :: T no_completion = markup_elem no_completionN {- position -} lineN, end_lineN :: Bytes lineN = \Markup.lineN\ end_lineN = \Markup.end_lineN\ offsetN, end_offsetN :: Bytes offsetN = \Markup.offsetN\ end_offsetN = \Markup.end_offsetN\ fileN, idN :: Bytes fileN = \Markup.fileN\ idN = \Markup.idN\ positionN :: Bytes positionN = \Markup.positionN\ position :: T position = markup_elem positionN {- expression -} expressionN :: Bytes expressionN = \Markup.expressionN\ expression :: Bytes -> T expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)]) {- citation -} citationN :: Bytes citationN = \Markup.citationN\ citation :: Bytes -> T citation = markup_string nameN citationN {- external resources -} pathN :: Bytes pathN = \Markup.pathN\ path :: Bytes -> T path = markup_string pathN nameN urlN :: Bytes urlN = \Markup.urlN\ url :: Bytes -> T url = markup_string urlN nameN docN :: Bytes docN = \Markup.docN\ doc :: Bytes -> T doc = markup_string docN nameN {- pretty printing -} markupN, consistentN, unbreakableN, indentN :: Bytes markupN = \Markup.markupN\ consistentN = \Markup.consistentN\ unbreakableN = \Markup.unbreakableN\ indentN = \Markup.indentN\ widthN :: Bytes widthN = \Markup.widthN\ blockN :: Bytes blockN = \Markup.blockN\ block :: Bool -> Int -> T block c i = (blockN, (if c then [(consistentN, Value.print_bool c)] else []) <> (if i /= 0 then [(indentN, Value.print_int i)] else [])) breakN :: Bytes breakN = \Markup.breakN\ break :: Int -> Int -> T break w i = (breakN, (if w /= 0 then [(widthN, Value.print_int w)] else []) <> (if i /= 0 then [(indentN, Value.print_int i)] else [])) fbreakN :: Bytes fbreakN = \Markup.fbreakN\ fbreak :: T fbreak = markup_elem fbreakN itemN :: Bytes itemN = \Markup.itemN\ item :: T item = markup_elem itemN {- text properties -} wordsN :: Bytes wordsN = \Markup.wordsN\ words :: T words = markup_elem wordsN {- inner syntax -} tfreeN :: Bytes tfreeN = \Markup.tfreeN\ tfree :: T tfree = markup_elem tfreeN tvarN :: Bytes tvarN = \Markup.tvarN\ tvar :: T tvar = markup_elem tvarN freeN :: Bytes freeN = \Markup.freeN\ free :: T free = markup_elem freeN skolemN :: Bytes skolemN = \Markup.skolemN\ skolem :: T skolem = markup_elem skolemN boundN :: Bytes boundN = \Markup.boundN\ bound :: T bound = markup_elem boundN varN :: Bytes varN = \Markup.varN\ var :: T var = markup_elem varN numeralN :: Bytes numeralN = \Markup.numeralN\ numeral :: T numeral = markup_elem numeralN literalN :: Bytes literalN = \Markup.literalN\ literal :: T literal = markup_elem literalN delimiterN :: Bytes delimiterN = \Markup.delimiterN\ delimiter :: T delimiter = markup_elem delimiterN inner_stringN :: Bytes inner_stringN = \Markup.inner_stringN\ inner_string :: T inner_string = markup_elem inner_stringN inner_cartoucheN :: Bytes inner_cartoucheN = \Markup.inner_cartoucheN\ inner_cartouche :: T inner_cartouche = markup_elem inner_cartoucheN token_rangeN :: Bytes token_rangeN = \Markup.token_rangeN\ token_range :: T token_range = markup_elem token_rangeN sortingN :: Bytes sortingN = \Markup.sortingN\ sorting :: T sorting = markup_elem sortingN typingN :: Bytes typingN = \Markup.typingN\ typing :: T typing = markup_elem typingN class_parameterN :: Bytes class_parameterN = \Markup.class_parameterN\ class_parameter :: T class_parameter = markup_elem class_parameterN {- antiquotations -} antiquotedN :: Bytes antiquotedN = \Markup.antiquotedN\ antiquoted :: T antiquoted = markup_elem antiquotedN antiquoteN :: Bytes antiquoteN = \Markup.antiquoteN\ antiquote :: T antiquote = markup_elem antiquoteN {- text structure -} paragraphN :: Bytes paragraphN = \Markup.paragraphN\ paragraph :: T paragraph = markup_elem paragraphN text_foldN :: Bytes text_foldN = \Markup.text_foldN\ text_fold :: T text_fold = markup_elem text_foldN {- outer syntax -} keyword1N :: Bytes keyword1N = \Markup.keyword1N\ keyword1 :: T keyword1 = markup_elem keyword1N keyword2N :: Bytes keyword2N = \Markup.keyword2N\ keyword2 :: T keyword2 = markup_elem keyword2N keyword3N :: Bytes keyword3N = \Markup.keyword3N\ keyword3 :: T keyword3 = markup_elem keyword3N quasi_keywordN :: Bytes quasi_keywordN = \Markup.quasi_keywordN\ quasi_keyword :: T quasi_keyword = markup_elem quasi_keywordN improperN :: Bytes improperN = \Markup.improperN\ improper :: T improper = markup_elem improperN operatorN :: Bytes operatorN = \Markup.operatorN\ operator :: T operator = markup_elem operatorN stringN :: Bytes stringN = \Markup.stringN\ string :: T string = markup_elem stringN alt_stringN :: Bytes alt_stringN = \Markup.alt_stringN\ alt_string :: T alt_string = markup_elem alt_stringN verbatimN :: Bytes verbatimN = \Markup.verbatimN\ verbatim :: T verbatim = markup_elem verbatimN cartoucheN :: Bytes cartoucheN = \Markup.cartoucheN\ cartouche :: T cartouche = markup_elem cartoucheN commentN :: Bytes commentN = \Markup.commentN\ comment :: T comment = markup_elem commentN {- comments -} comment1N :: Bytes comment1N = \Markup.comment1N\ comment1 :: T comment1 = markup_elem comment1N comment2N :: Bytes comment2N = \Markup.comment2N\ comment2 :: T comment2 = markup_elem comment2N comment3N :: Bytes comment3N = \Markup.comment3N\ comment3 :: T comment3 = markup_elem comment3N {- command status -} forkedN, joinedN, runningN, finishedN, failedN, canceledN, initializedN, finalizedN, consolidatedN :: Bytes forkedN = \Markup.forkedN\ joinedN = \Markup.joinedN\ runningN = \Markup.runningN\ finishedN = \Markup.finishedN\ failedN = \Markup.failedN\ canceledN = \Markup.canceledN\ initializedN = \Markup.initializedN\ finalizedN = \Markup.finalizedN\ consolidatedN = \Markup.consolidatedN\ forked, joined, running, finished, failed, canceled, initialized, finalized, consolidated :: T forked = markup_elem forkedN joined = markup_elem joinedN running = markup_elem runningN finished = markup_elem finishedN failed = markup_elem failedN canceled = markup_elem canceledN initialized = markup_elem initializedN finalized = markup_elem finalizedN consolidated = markup_elem consolidatedN {- messages -} writelnN :: Bytes writelnN = \Markup.writelnN\ writeln :: T writeln = markup_elem writelnN stateN :: Bytes stateN = \Markup.stateN\ state :: T state = markup_elem stateN informationN :: Bytes informationN = \Markup.informationN\ information :: T information = markup_elem informationN tracingN :: Bytes tracingN = \Markup.tracingN\ tracing :: T tracing = markup_elem tracingN warningN :: Bytes warningN = \Markup.warningN\ warning :: T warning = markup_elem warningN legacyN :: Bytes legacyN = \Markup.legacyN\ legacy :: T legacy = markup_elem legacyN errorN :: Bytes errorN = \Markup.errorN\ error :: T error = markup_elem errorN reportN :: Bytes reportN = \Markup.reportN\ report :: T report = markup_elem reportN no_reportN :: Bytes no_reportN = \Markup.no_reportN\ no_report :: T no_report = markup_elem no_reportN intensifyN :: Bytes intensifyN = \Markup.intensifyN\ intensify :: T intensify = markup_elem intensifyN {- output -} type Output = (Bytes, Bytes) no_output :: Output no_output = ("", "") \ generate_file "Isabelle/Position.hs" = \ {- Title: Isabelle/Position.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Source positions starting from 1; values <= 0 mean "absent". Count Isabelle symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a right-open interval offset .. end_offset (exclusive). See also \<^file>\$ISABELLE_HOME/src/Pure/General/position.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Position ( T, line_of, column_of, offset_of, end_offset_of, file_of, id_of, start, none, put_file, file, file_only, put_id, - advance_symbol, advance_symbol_explode, advance_symbol_explode_string, shift_offsets, + symbol, symbol_explode, symbol_explode_string, shift_offsets, of_properties, properties_of, def_properties_of, entity_markup, entity_properties_of, is_reported, is_reported_range, here, Range, no_range, no_range_position, range_position, range ) where import Data.Maybe (isJust, fromMaybe) import qualified Isabelle.Properties as Properties import qualified Isabelle.Bytes as Bytes import qualified Isabelle.Value as Value import Isabelle.Bytes (Bytes) import qualified Isabelle.Markup as Markup import qualified Isabelle.YXML as YXML import Isabelle.Library import qualified Isabelle.Symbol as Symbol import Isabelle.Symbol (Symbol) {- position -} data T = Position { _line :: Int, _column :: Int, _offset :: Int, _end_offset :: Int, _file :: Bytes, _id :: Bytes } deriving (Eq, Ord) valid, invalid :: Int -> Bool valid i = i > 0 invalid = not . valid maybe_valid :: Int -> Maybe Int maybe_valid i = if valid i then Just i else Nothing if_valid :: Int -> Int -> Int if_valid i i' = if valid i then i' else i {- fields -} line_of, column_of, offset_of, end_offset_of :: T -> Maybe Int line_of = maybe_valid . _line column_of = maybe_valid . _column offset_of = maybe_valid . _offset end_offset_of = maybe_valid . _end_offset file_of :: T -> Maybe Bytes file_of = proper_string . _file id_of :: T -> Maybe Bytes id_of = proper_string . _id {- make position -} start :: T start = Position 1 1 1 0 Bytes.empty Bytes.empty none :: T none = Position 0 0 0 0 Bytes.empty Bytes.empty put_file :: Bytes -> T -> T put_file file pos = pos { _file = file } file :: Bytes -> T file file = put_file file start file_only :: Bytes -> T file_only file = put_file file none put_id :: Bytes -> T -> T put_id id pos = pos { _id = id } {- advance position -} advance_line :: Symbol -> Int -> Int advance_line "\n" line = if_valid line (line + 1) advance_line _ line = line advance_column :: Symbol -> Int -> Int advance_column "\n" column = if_valid column 1 advance_column _ column = if_valid column (column + 1) advance_offset :: Symbol -> Int -> Int advance_offset c offset = if_valid offset (offset + 1) -advance_symbol :: Symbol -> T -> T -advance_symbol s pos = +symbol :: Symbol -> T -> T +symbol s pos = pos { _line = advance_line s (_line pos), _column = advance_column s (_column pos), _offset = advance_offset s (_offset pos) } -advance_symbol_explode :: BYTES a => a -> T -> T -advance_symbol_explode = fold advance_symbol . Symbol.explode . make_bytes - -advance_symbol_explode_string :: String -> T -> T -advance_symbol_explode_string = advance_symbol_explode +symbol_explode :: BYTES a => a -> T -> T +symbol_explode = fold symbol . Symbol.explode . make_bytes + +symbol_explode_string :: String -> T -> T +symbol_explode_string = symbol_explode {- shift offsets -} shift_offsets :: Int -> T -> T shift_offsets shift pos = pos { _offset = offset', _end_offset = end_offset' } where offset = _offset pos end_offset = _end_offset pos offset' = if invalid offset || invalid shift then offset else offset + shift end_offset' = if invalid end_offset || invalid shift then end_offset else end_offset + shift {- markup properties -} get_string :: Properties.T -> Bytes -> Bytes get_string props name = fromMaybe "" (Properties.get_value Just props name) get_int :: Properties.T -> Bytes -> Int get_int props name = fromMaybe 0 (Properties.get_value Value.parse_int props name) of_properties :: Properties.T -> T of_properties props = none { _line = get_int props Markup.lineN, _offset = get_int props Markup.offsetN, _end_offset = get_int props Markup.end_offsetN, _file = get_string props Markup.fileN, _id = get_string props Markup.idN } string_entry :: Bytes -> Bytes -> Properties.T string_entry k s = if Bytes.null s then [] else [(k, s)] int_entry :: Bytes -> Int -> Properties.T int_entry k i = if invalid i then [] else [(k, Value.print_int i)] properties_of :: T -> Properties.T properties_of pos = int_entry Markup.lineN (_line pos) ++ int_entry Markup.offsetN (_offset pos) ++ int_entry Markup.end_offsetN (_end_offset pos) ++ string_entry Markup.fileN (_file pos) ++ string_entry Markup.idN (_id pos) def_properties_of :: T -> Properties.T def_properties_of = properties_of #> map (\(a, b) -> ("def_" <> a, b)) entity_markup :: Bytes -> (Bytes, T) -> Markup.T entity_markup kind (name, pos) = Markup.entity kind name |> Markup.properties (def_properties_of pos) entity_properties_of :: Bool -> Int -> T -> Properties.T entity_properties_of def serial pos = if def then (Markup.defN, Value.print_int serial) : properties_of pos else (Markup.refN, Value.print_int serial) : def_properties_of pos {- reports -} is_reported :: T -> Bool is_reported pos = isJust (offset_of pos) && isJust (id_of pos) is_reported_range :: T -> Bool is_reported_range pos = is_reported pos && isJust (end_offset_of pos) {- here: user output -} here :: T -> Bytes here pos = if Bytes.null s2 then "" else s1 <> m1 <> s2 <> m2 where props = properties_of pos (m1, m2) = YXML.output_markup (Markup.properties props Markup.position) (s1, s2) = case (line_of pos, file_of pos) of (Just i, Nothing) -> (" ", "(line " <> Value.print_int i <> ")") (Just i, Just name) -> (" ", "(line " <> Value.print_int i <> " of " <> quote name <> ")") (Nothing, Just name) -> (" ", "(file " <> quote name <> ")") _ -> if is_reported pos then ("", "\092<^here>") else ("", "") {- range -} type Range = (T, T) no_range :: Range no_range = (none, none) no_range_position :: T -> T no_range_position pos = pos { _end_offset = 0 } range_position :: Range -> T range_position (pos, pos') = pos { _end_offset = _offset pos' } range :: Range -> Range range (pos, pos') = (range_position (pos, pos'), no_range_position pos') \ generate_file "Isabelle/XML.hs" = \ {- Title: Isabelle/XML.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Untyped XML trees and representation of ML values. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of) where import Isabelle.Library import qualified Isabelle.Properties as Properties import qualified Isabelle.Markup as Markup import qualified Isabelle.Buffer as Buffer import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) {- types -} type Attributes = Properties.T type Body = [Tree] data Tree = Elem (Markup.T, Body) | Text Bytes {- wrapped elements -} wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree wrap_elem (((a, atts), body1), body2) = Elem ((\XML.xml_elemN\, (\XML.xml_nameN\, a) : atts), Elem ((\XML.xml_bodyN\, []), body1) : body2) unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree]) unwrap_elem (Elem ((\XML.xml_elemN\, (\XML.xml_nameN\, a) : atts), Elem ((\XML.xml_bodyN\, []), body1) : body2)) = Just (((a, atts), body1), body2) unwrap_elem _ = Nothing {- text content -} add_content :: Tree -> Buffer.T -> Buffer.T add_content tree = case unwrap_elem tree of Just (_, ts) -> fold add_content ts Nothing -> case tree of Elem (_, ts) -> fold add_content ts Text s -> Buffer.add s content_of :: Body -> Bytes content_of body = Buffer.empty |> fold add_content body |> Buffer.content {- string representation -} encode_char :: Char -> String encode_char '<' = "<" encode_char '>' = ">" encode_char '&' = "&" encode_char '\'' = "'" encode_char '\"' = """ encode_char c = [c] encode_text :: Bytes -> Bytes encode_text = make_bytes . concatMap (encode_char . Bytes.char) . Bytes.unpack instance Show Tree where show tree = Buffer.empty |> show_tree tree |> Buffer.content |> make_string where show_tree (Elem ((name, atts), [])) = Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>" show_tree (Elem ((name, atts), ts)) = Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #> fold show_tree ts #> Buffer.add " Buffer.add name #> Buffer.add ">" show_tree (Text s) = Buffer.add (encode_text s) show_elem name atts = space_implode " " (name : map (\(a, x) -> a <> "=\"" <> encode_text x <> "\"") atts) \ generate_file "Isabelle/XML/Encode.hs" = \ {- Title: Isabelle/XML/Encode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML as data representation language. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.XML.Encode ( A, T, V, P, int_atom, bool_atom, unit_atom, tree, properties, string, int, bool, unit, pair, triple, list, option, variant ) where import Data.Maybe (fromJust) import Isabelle.Library import Isabelle.Bytes (Bytes) import qualified Isabelle.Value as Value import qualified Isabelle.Properties as Properties import qualified Isabelle.XML as XML type A a = a -> Bytes type T a = a -> XML.Body type V a = a -> Maybe ([Bytes], XML.Body) type P a = a -> [Bytes] -- atomic values int_atom :: A Int int_atom = Value.print_int bool_atom :: A Bool bool_atom False = "0" bool_atom True = "1" unit_atom :: A () unit_atom () = "" -- structural nodes node ts = XML.Elem ((":", []), ts) vector = map_index (\(i, x) -> (int_atom i, x)) tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts) -- representation of standard types tree :: T XML.Tree tree t = [t] properties :: T Properties.T properties props = [XML.Elem ((":", props), [])] string :: T Bytes string "" = [] string s = [XML.Text s] int :: T Int int = string . int_atom bool :: T Bool bool = string . bool_atom unit :: T () unit = string . unit_atom pair :: T a -> T b -> T (a, b) pair f g (x, y) = [node (f x), node (g y)] triple :: T a -> T b -> T c -> T (a, b, c) triple f g h (x, y, z) = [node (f x), node (g y), node (h z)] list :: T a -> T [a] list f xs = map (node . f) xs option :: T a -> T (Maybe a) option _ Nothing = [] option f (Just x) = [node (f x)] variant :: [V a] -> T a variant fs x = [tagged (fromJust (get_index (\f -> f x) fs))] \ generate_file "Isabelle/XML/Decode.hs" = \ {- Title: Isabelle/XML/Decode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML as data representation language. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.XML.Decode ( A, T, V, P, int_atom, bool_atom, unit_atom, tree, properties, string, int, bool, unit, pair, triple, list, option, variant ) where import Isabelle.Library import Isabelle.Bytes (Bytes) import qualified Isabelle.Value as Value import qualified Isabelle.Properties as Properties import qualified Isabelle.XML as XML type A a = Bytes -> a type T a = XML.Body -> a type V a = ([Bytes], XML.Body) -> a type P a = [Bytes] -> a err_atom = error "Malformed XML atom" err_body = error "Malformed XML body" {- atomic values -} int_atom :: A Int int_atom s = case Value.parse_int s of Just i -> i Nothing -> err_atom bool_atom :: A Bool bool_atom "0" = False bool_atom "1" = True bool_atom _ = err_atom unit_atom :: A () unit_atom "" = () unit_atom _ = err_atom {- structural nodes -} node (XML.Elem ((":", []), ts)) = ts node _ = err_body vector atts = map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts)) tagged _ = err_body {- representation of standard types -} tree :: T XML.Tree tree [t] = t tree _ = err_body properties :: T Properties.T properties [XML.Elem ((":", props), [])] = props properties _ = err_body string :: T Bytes string [] = "" string [XML.Text s] = s string _ = err_body int :: T Int int = int_atom . string bool :: T Bool bool = bool_atom . string unit :: T () unit = unit_atom . string pair :: T a -> T b -> T (a, b) pair f g [t1, t2] = (f (node t1), g (node t2)) pair _ _ _ = err_body triple :: T a -> T b -> T c -> T (a, b, c) triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3)) triple _ _ _ _ = err_body list :: T a -> T [a] list f ts = map (f . node) ts option :: T a -> T (Maybe a) option _ [] = Nothing option f [t] = Just (f (node t)) option _ _ = err_body variant :: [V a] -> T a variant fs [t] = (fs !! tag) (xs, ts) where (tag, (xs, ts)) = tagged t variant _ _ = err_body \ generate_file "Isabelle/YXML.hs" = \ {- Title: Isabelle/YXML.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Efficient text representation of XML trees. Suitable for direct inlining into plain text. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-incomplete-patterns #-} module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup, buffer_body, buffer, string_of_body, string_of, parse_body, parse) where import qualified Data.List as List import Data.Word (Word8) import Isabelle.Library import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.Markup as Markup import qualified Isabelle.XML as XML import qualified Isabelle.Buffer as Buffer {- markers -} charX, charY :: Word8 charX = 5 charY = 6 strX, strY, strXY, strXYX :: Bytes strX = Bytes.singleton charX strY = Bytes.singleton charY strXY = strX <> strY strXYX = strXY <> strX detect :: Bytes -> Bool detect = Bytes.any (\c -> c == charX || c == charY) {- output -} output_markup :: Markup.T -> Markup.Output output_markup markup@(name, atts) = if Markup.is_empty markup then Markup.no_output else (strXY <> name <> Bytes.concat (map (\(a, x) -> strY <> a <> "=" <> x) atts) <> strX, strXYX) buffer_attrib (a, x) = Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x buffer_body :: XML.Body -> Buffer.T -> Buffer.T buffer_body = fold buffer buffer :: XML.Tree -> Buffer.T -> Buffer.T buffer (XML.Elem ((name, atts), ts)) = Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #> buffer_body ts #> Buffer.add strXYX buffer (XML.Text s) = Buffer.add s string_of_body :: XML.Body -> Bytes string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content string_of :: XML.Tree -> Bytes string_of = string_of_body . single {- parse -} -- split: fields or non-empty tokens split :: Bool -> Word8 -> [Word8] -> [[Word8]] split _ _ [] = [] split fields sep str = splitting str where splitting rest = case span (/= sep) rest of (_, []) -> cons rest [] (prfx, _ : rest') -> cons prfx (splitting rest') cons item = if fields || not (null item) then (:) item else id -- structural errors err :: Bytes -> a err msg = error (make_string ("Malformed YXML: " <> msg)) err_attribute = err "bad attribute" err_element = err "bad element" err_unbalanced :: Bytes -> a err_unbalanced name = if Bytes.null name then err "unbalanced element" else err ("unbalanced element " <> quote name) -- stack operations add x ((elem, body) : pending) = (elem, x : body) : pending push name atts pending = if Bytes.null name then err_element else ((name, atts), []) : pending pop (((name, atts), body) : pending) = if Bytes.null name then err_unbalanced name else add (XML.Elem ((name, atts), reverse body)) pending -- parsing parse_attrib s = case List.elemIndex (Bytes.byte '=') s of Just i | i > 0 -> (Bytes.pack $ take i s, Bytes.pack $ drop (i + 1) s) _ -> err_attribute parse_chunk [[], []] = pop parse_chunk ([] : name : atts) = push (Bytes.pack name) (map parse_attrib atts) parse_chunk txts = fold (add . XML.Text . Bytes.pack) txts parse_body :: Bytes -> XML.Body parse_body source = case fold parse_chunk chunks [((Bytes.empty, []), [])] of [((name, _), result)] | Bytes.null name -> reverse result ((name, _), _) : _ -> err_unbalanced name where chunks = source |> Bytes.unpack |> split False charX |> map (split True charY) parse :: Bytes -> XML.Tree parse source = case parse_body source of [result] -> result [] -> XML.Text "" _ -> err "multiple results" \ generate_file "Isabelle/Completion.hs" = \ {- Title: Isabelle/Completion.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Completion of names. See also \<^file>\$ISABELLE_HOME/src/Pure/General/completion.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Completion ( Name, T, names, none, make, markup_element, markup_report, make_report ) where import qualified Isabelle.Bytes as Bytes import qualified Isabelle.Name as Name import Isabelle.Name (Name) import qualified Isabelle.Properties as Properties import qualified Isabelle.Markup as Markup import Isabelle.XML.Classes import qualified Isabelle.XML as XML import qualified Isabelle.YXML as YXML type Names = [(Name, (Name, Name))] -- external name, kind, internal name data T = Completion Properties.T Int Names -- position, total length, names names :: Int -> Properties.T -> Names -> T names limit props names = Completion props (length names) (take limit names) none :: T none = names 0 [] [] make :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> T make limit (name, props) make_names = if name /= "" && name /= "_" then names limit props (make_names (Bytes.isPrefixOf (Name.clean name))) else none markup_element :: T -> (Markup.T, XML.Body) markup_element (Completion props total names) = if not (null names) then (Markup.properties props Markup.completion, encode (total, names)) else (Markup.empty, []) markup_report :: [T] -> Name markup_report [] = Bytes.empty markup_report elems = YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems) make_report :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> Name make_report limit name_props make_names = markup_report [make limit name_props make_names] \ generate_file "Isabelle/File.hs" = \ {- Title: Isabelle/File.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) File-system operations. See also \<^file>\$ISABELLE_HOME/src/Pure/General/file.ML\. -} module Isabelle.File (read, write, append) where import Prelude hiding (read) import qualified System.IO as IO import qualified Data.ByteString as ByteString import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) read :: IO.FilePath -> IO Bytes read path = Bytes.make <$> IO.withFile path IO.ReadMode ByteString.hGetContents write :: IO.FilePath -> Bytes -> IO () write path bs = IO.withFile path IO.WriteMode (\h -> ByteString.hPut h (Bytes.unmake bs)) append :: IO.FilePath -> Bytes -> IO () append path bs = IO.withFile path IO.AppendMode (\h -> ByteString.hPut h (Bytes.unmake bs)) \ generate_file "Isabelle/Pretty.hs" = \ {- Title: Isabelle/Pretty.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Generic pretty printing module. See also \<^file>\$ISABELLE_HOME/src/Pure/General/pretty.ML\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.Pretty ( T, symbolic, formatted, unformatted, str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str, item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate, commas, enclose, enum, list, str_list, big_list) where import qualified Data.List as List import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import Isabelle.Library hiding (quote, separate, commas) import qualified Isabelle.Buffer as Buffer import qualified Isabelle.Markup as Markup import qualified Isabelle.XML as XML import qualified Isabelle.YXML as YXML data T = Block Markup.T Bool Int [T] | Break Int Int | Str Bytes {- output -} symbolic_text s = if Bytes.null s then [] else [XML.Text s] symbolic_markup markup body = if Markup.is_empty markup then body else [XML.Elem (markup, body)] symbolic :: T -> XML.Body symbolic (Block markup consistent indent prts) = concatMap symbolic prts |> symbolic_markup block_markup |> symbolic_markup markup where block_markup = if null prts then Markup.empty else Markup.block consistent indent symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (Bytes.spaces wd))] symbolic (Str s) = symbolic_text s formatted :: T -> Bytes formatted = YXML.string_of_body . symbolic unformatted :: T -> Bytes unformatted prt = Buffer.empty |> out prt |> Buffer.content where out (Block markup _ _ prts) = let (bg, en) = YXML.output_markup markup in Buffer.add bg #> fold out prts #> Buffer.add en out (Break _ wd) = Buffer.add (Bytes.spaces wd) out (Str s) = Buffer.add s {- derived operations to create formatting expressions -} force_nat n | n < 0 = 0 force_nat n = n str :: BYTES a => a -> T str = Str . make_bytes brk_indent :: Int -> Int -> T brk_indent wd ind = Break (force_nat wd) ind brk :: Int -> T brk wd = brk_indent wd 0 fbrk :: T fbrk = Str "\n" breaks, fbreaks :: [T] -> [T] breaks = List.intersperse (brk 1) fbreaks = List.intersperse fbrk blk :: (Int, [T]) -> T blk (indent, es) = Block Markup.empty False (force_nat indent) es block :: [T] -> T block prts = blk (2, prts) strs :: BYTES a => [a] -> T strs = block . breaks . map str markup :: Markup.T -> [T] -> T markup m = Block m False 0 mark :: Markup.T -> T -> T mark m prt = if m == Markup.empty then prt else markup m [prt] mark_str :: BYTES a => (Markup.T, a) -> T mark_str (m, s) = mark m (str s) marks_str :: BYTES a => ([Markup.T], a) -> T marks_str (ms, s) = fold_rev mark ms (str s) item :: [T] -> T item = markup Markup.item text_fold :: [T] -> T text_fold = markup Markup.text_fold keyword1, keyword2 :: BYTES a => a -> T keyword1 name = mark_str (Markup.keyword1, name) keyword2 name = mark_str (Markup.keyword2, name) text :: BYTES a => a -> [T] text = breaks . map str . filter (not . Bytes.null) . space_explode ' ' . make_bytes paragraph :: [T] -> T paragraph = markup Markup.paragraph para :: BYTES a => a -> T para = paragraph . text quote :: T -> T quote prt = blk (1, [Str "\"", prt, Str "\""]) cartouche :: T -> T cartouche prt = blk (1, [Str "\92", prt, Str "\92"]) separate :: BYTES a => a -> [T] -> [T] separate sep = List.intercalate [str sep, brk 1] . map single commas :: [T] -> [T] commas = separate ("," :: Bytes) enclose :: BYTES a => a -> a -> [T] -> T enclose lpar rpar prts = block (str lpar : prts <> [str rpar]) enum :: BYTES a => a -> a -> a -> [T] -> T enum sep lpar rpar = enclose lpar rpar . separate sep list :: BYTES a => a -> a -> [T] -> T list = enum "," str_list :: BYTES a => a -> a -> [a] -> T str_list lpar rpar = list lpar rpar . map str big_list :: BYTES a => a -> [T] -> T big_list name prts = block (fbreaks (str name : prts)) \ generate_file "Isabelle/Name.hs" = \ {- Title: Isabelle/Name.hs Author: Makarius Names of basic logical entities (variables etc.). See also \<^file>\$ISABELLE_HOME/src/Pure/name.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Name ( Name, clean_index, clean, Context, declare, is_declared, context, make_context, variant ) where import Data.Word (Word8) import qualified Data.Set as Set import Data.Set (Set) import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.Symbol as Symbol import Isabelle.Library type Name = Bytes {- suffix for internal names -} underscore :: Word8 underscore = Bytes.byte '_' clean_index :: Name -> (Name, Int) clean_index x = if Bytes.null x || Bytes.last x /= underscore then (x, 0) else let rev = reverse (Bytes.unpack x) n = length (takeWhile (== underscore) rev) y = Bytes.pack (reverse (drop n rev)) in (y, n) clean :: Name -> Name clean = fst . clean_index {- context for used names -} data Context = Context (Set Name) declare :: Name -> Context -> Context declare x (Context names) = Context (Set.insert x names) is_declared :: Context -> Name -> Bool is_declared (Context names) x = Set.member x names context :: Context context = Context (Set.fromList ["", "'"]) make_context :: [Name] -> Context make_context used = fold declare used context {- generating fresh names -} bump_init :: Name -> Name bump_init str = str <> "a" bump_string :: Name -> Name bump_string str = let a = Bytes.byte 'a' z = Bytes.byte 'z' bump (b : bs) | b == z = a : bump bs bump (b : bs) | a <= b && b < z = b + 1 : bs bump bs = a : bs rev = reverse (Bytes.unpack str) part2 = reverse (takeWhile (Symbol.is_ascii_quasi . Bytes.char) rev) part1 = reverse (bump (drop (length part2) rev)) in Bytes.pack (part1 <> part2) variant :: Name -> Context -> (Name, Context) variant name names = let vary bump x = if is_declared names x then bump x |> vary bump_string else x (x, n) = clean_index name x' = x |> vary bump_init names' = declare x' names; in (x' <> Bytes.pack (replicate n underscore), names') \ generate_file "Isabelle/Term.hs" = \ {- Title: Isabelle/Term.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Lambda terms, types, sorts. See also \<^file>\$ISABELLE_HOME/src/Pure/term.scala\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Term ( Indexname, Sort, Typ(..), Term(..), Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs, type_op0, type_op1, op0, op1, op2, typed_op2, binder, dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->), aconv, list_comb, strip_comb, head_of ) where import Isabelle.Library import qualified Isabelle.Name as Name import Isabelle.Name (Name) infixr 5 --> infixr ---> {- types and terms -} type Indexname = (Name, Int) type Sort = [Name] data Typ = Type (Name, [Typ]) | TFree (Name, Sort) | TVar (Indexname, Sort) deriving (Show, Eq, Ord) data Term = Const (Name, [Typ]) | Free (Name, Typ) | Var (Indexname, Typ) | Bound Int | Abs (Name, Typ, Term) | App (Term, Term) deriving (Show, Eq, Ord) {- free and bound variables -} type Free = (Name, Typ) lambda :: Free -> Term -> Term lambda (name, typ) body = Abs (name, typ, abstract 0 body) where abstract lev (Free (x, ty)) | name == x && typ == ty = Bound lev abstract lev (Abs (a, ty, t)) = Abs (a, ty, abstract (lev + 1) t) abstract lev (App (t, u)) = App (abstract lev t, abstract lev u) abstract _ t = t declare_frees :: Term -> Name.Context -> Name.Context declare_frees (Free (x, _)) = Name.declare x declare_frees (Abs (_, _, b)) = declare_frees b declare_frees (App (t, u)) = declare_frees t #> declare_frees u declare_frees _ = id incr_boundvars :: Int -> Term -> Term incr_boundvars inc = if inc == 0 then id else incr 0 where incr lev (Bound i) = if i >= lev then Bound (i + inc) else Bound i incr lev (Abs (a, ty, b)) = Abs (a, ty, incr (lev + 1) b) incr lev (App (t, u)) = App (incr lev t, incr lev u) incr _ t = t subst_bound :: Term -> Term -> Term subst_bound arg = subst 0 where subst lev (Bound i) = if i < lev then Bound i else if i == lev then incr_boundvars lev arg else Bound (i - 1) subst lev (Abs (a, ty, b)) = Abs (a, ty, subst (lev + 1) b) subst lev (App (t, u)) = App (subst lev t, subst lev u) subst _ t = t dest_abs :: Name.Context -> Term -> Maybe (Free, Term) dest_abs names (Abs (x, ty, b)) = let (x', _) = Name.variant x (declare_frees b names) v = (x', ty) in Just (v, subst_bound (Free v) b) dest_abs _ _ = Nothing strip_abs :: Name.Context -> Term -> ([Free], Term) strip_abs names tm = case dest_abs names tm of Just (v, t) -> let (vs, t') = strip_abs names t' in (v : vs, t') Nothing -> ([], tm) {- type and term operators -} type_op0 :: Name -> (Typ, Typ -> Bool) type_op0 name = (mk, is) where mk = Type (name, []) is (Type (name, _)) = True is _ = False type_op1 :: Name -> (Typ -> Typ, Typ -> Maybe Typ) type_op1 name = (mk, dest) where mk ty = Type (name, [ty]) dest (Type (name, [ty])) = Just ty dest _ = Nothing type_op2 :: Name -> (Typ -> Typ -> Typ, Typ -> Maybe (Typ, Typ)) type_op2 name = (mk, dest) where mk ty1 ty2 = Type (name, [ty1, ty2]) dest (Type (name, [ty1, ty2])) = Just (ty1, ty2) dest _ = Nothing op0 :: Name -> (Term, Term -> Bool) op0 name = (mk, is) where mk = Const (name, []) is (Const (c, _)) = c == name is _ = False op1 :: Name -> (Term -> Term, Term -> Maybe Term) op1 name = (mk, dest) where mk t = App (Const (name, []), t) dest (App (Const (c, _), t)) | c == name = Just t dest _ = Nothing op2 :: Name -> (Term -> Term -> Term, Term -> Maybe (Term, Term)) op2 name = (mk, dest) where mk t u = App (App (Const (name, []), t), u) dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u) dest _ = Nothing typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term)) typed_op2 name = (mk, dest) where mk ty t u = App (App (Const (name, [ty]), t), u) dest (App (App (Const (c, [ty]), t), u)) | c == name = Just (ty, t, u) dest _ = Nothing binder :: Name -> (Free -> Term -> Term, Name.Context -> Term -> Maybe (Free, Term)) binder name = (mk, dest) where mk (a, ty) b = App (Const (name, [ty]), lambda (a, ty) b) dest names (App (Const (c, _), t)) | c == name = dest_abs names t dest _ _ = Nothing {- type operations -} dummyS :: Sort dummyS = [""] dummyT :: Typ; is_dummyT :: Typ -> Bool (dummyT, is_dummyT) = type_op0 \\<^type_name>\dummy\\ propT :: Typ; is_propT :: Typ -> Bool (propT, is_propT) = type_op0 \\<^type_name>\prop\\ (-->) :: Typ -> Typ -> Typ; dest_funT :: Typ -> Maybe (Typ, Typ) ((-->), dest_funT) = type_op2 \\<^type_name>\fun\\ (--->) :: [Typ] -> Typ -> Typ [] ---> b = b (a : as) ---> b = a --> (as ---> b) {- term operations -} aconv :: Term -> Term -> Bool aconv (App (t1, u1)) (App (t2, u2)) = aconv t1 t2 && aconv u1 u2 aconv (Abs (_, ty1, t1)) (Abs (_, ty2, t2)) = aconv t1 t2 && ty1 == ty2 aconv a1 a2 = a1 == a2 list_comb :: Term -> [Term] -> Term list_comb f [] = f list_comb f (t : ts) = list_comb (App (f, t)) ts strip_comb :: Term -> (Term, [Term]) strip_comb tm = strip (tm, []) where strip (App (f, t), ts) = strip (f, t : ts) strip x = x head_of :: Term -> Term head_of (App (f, _)) = head_of f head_of u = u \ generate_file "Isabelle/Pure.hs" = \ {- Title: Isabelle/Term.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Support for Isabelle/Pure logic. See also \<^file>\$ISABELLE_HOME/src/Pure/logic.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Pure ( mk_forall, dest_forall, mk_equals, dest_equals, mk_implies, dest_implies ) where import qualified Isabelle.Name as Name import Isabelle.Term mk_forall :: Free -> Term -> Term; dest_forall :: Name.Context -> Term -> Maybe (Free, Term) (mk_forall, dest_forall) = binder \\<^const_name>\Pure.all\\ mk_equals :: Typ -> Term -> Term -> Term; dest_equals :: Term -> Maybe (Typ, Term, Term) (mk_equals, dest_equals) = typed_op2 \\<^const_name>\Pure.eq\\ mk_implies :: Term -> Term -> Term; dest_implies :: Term -> Maybe (Term, Term) (mk_implies, dest_implies) = op2 \\<^const_name>\Pure.imp\\ \ generate_file "Isabelle/HOL.hs" = \ {- Title: Isabelle/Term.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Support for Isabelle/HOL logic. See also \<^file>\$ISABELLE_HOME/src/HOL/Tools/hologic.ML\. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.HOL ( boolT, is_boolT, mk_trueprop, dest_trueprop, mk_setT, dest_setT, mk_mem, dest_mem, mk_eq, dest_eq, true, is_true, false, is_false, mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj, mk_imp, dest_imp, mk_iff, dest_iff, mk_all, dest_all, mk_ex, dest_ex ) where import qualified Isabelle.Name as Name import Isabelle.Term boolT :: Typ; is_boolT :: Typ -> Bool (boolT, is_boolT) = type_op0 \\<^type_name>\bool\\ mk_trueprop :: Term -> Term; dest_trueprop :: Term -> Maybe Term (mk_trueprop, dest_trueprop) = op1 \\<^const_name>\Trueprop\\ mk_setT :: Typ -> Typ; dest_setT :: Typ -> Maybe Typ (mk_setT, dest_setT) = type_op1 \\<^type_name>\set\\ mk_mem :: Typ -> Term -> Term -> Term; dest_mem :: Term -> Maybe (Typ, Term, Term) (mk_mem, dest_mem) = typed_op2 \\<^const_name>\Set.member\\ mk_eq :: Typ -> Term -> Term -> Term; dest_eq :: Term -> Maybe (Typ, Term, Term) (mk_eq, dest_eq) = typed_op2 \\<^const_name>\HOL.eq\\ true :: Term; is_true :: Term -> Bool (true, is_true) = op0 \\<^const_name>\True\\ false :: Term; is_false :: Term -> Bool (false, is_false) = op0 \\<^const_name>\False\\ mk_not :: Term -> Term; dest_not :: Term -> Maybe Term (mk_not, dest_not) = op1 \\<^const_name>\Not\\ mk_conj :: Term -> Term -> Term; dest_conj :: Term -> Maybe (Term, Term) (mk_conj, dest_conj) = op2 \\<^const_name>\conj\\ mk_disj :: Term -> Term -> Term; dest_disj :: Term -> Maybe (Term, Term) (mk_disj, dest_disj) = op2 \\<^const_name>\disj\\ mk_imp :: Term -> Term -> Term; dest_imp :: Term -> Maybe (Term, Term) (mk_imp, dest_imp) = op2 \\<^const_name>\implies\\ mk_iff :: Term -> Term -> Term mk_iff = mk_eq boolT dest_iff :: Term -> Maybe (Term, Term) dest_iff tm = case dest_eq tm of Just (ty, t, u) | ty == boolT -> Just (t, u) _ -> Nothing mk_all :: Free -> Term -> Term; dest_all :: Name.Context -> Term -> Maybe (Free, Term) (mk_all, dest_all) = binder \\<^const_name>\All\\ mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term) (mk_ex, dest_ex) = binder \\<^const_name>\Ex\\ \ generate_file "Isabelle/Term_XML/Encode.hs" = \ {- Title: Isabelle/Term_XML/Encode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. See also \<^file>\$ISABELLE_HOME/src/Pure/term_xml.ML\. -} {-# LANGUAGE LambdaCase #-} module Isabelle.Term_XML.Encode (indexname, sort, typ, typ_body, term) where import Isabelle.Library import Isabelle.XML.Encode import Isabelle.Term indexname :: P Indexname indexname (a, b) = if b == 0 then [a] else [a, int_atom b] sort :: T Sort sort = list string typ :: T Typ typ ty = ty |> variant [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing }, \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing }, \case { TVar (a, b) -> Just (indexname a, sort b); _ -> Nothing }] typ_body :: T Typ typ_body ty = if is_dummyT ty then [] else typ ty term :: T Term term t = t |> variant [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing }, \case { Free (a, b) -> Just ([a], typ_body b); _ -> Nothing }, \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing }, \case { Bound a -> Just ([], int a); _ -> Nothing }, \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing }, \case { App a -> Just ([], pair term term a); _ -> Nothing }] \ generate_file "Isabelle/Term_XML/Decode.hs" = \ {- Title: Isabelle/Term_XML/Decode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. See also \<^file>\$ISABELLE_HOME/src/Pure/term_xml.ML\. -} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term) where import Isabelle.Library import Isabelle.XML.Decode import Isabelle.Term indexname :: P Indexname indexname [a] = (a, 0) indexname [a, b] = (a, int_atom b) sort :: T Sort sort = list string typ :: T Typ typ ty = ty |> variant [\([a], b) -> Type (a, list typ b), \([a], b) -> TFree (a, sort b), \(a, b) -> TVar (indexname a, sort b)] typ_body :: T Typ typ_body [] = dummyT typ_body body = typ body term :: T Term term t = t |> variant [\([a], b) -> Const (a, list typ b), \([a], b) -> Free (a, typ_body b), \(a, b) -> Var (indexname a, typ_body b), \([], a) -> Bound (int a), \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d), \([], a) -> App (pair term term a)] \ generate_file "Isabelle/XML/Classes.hs" = \ {- generated by Isabelle -} {- Title: Isabelle/XML/Classes.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Type classes for XML data representation. -} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} module Isabelle.XML.Classes (Encode_Atom(..), Decode_Atom(..), Encode (..), Decode (..)) where import qualified Isabelle.XML as XML import qualified Isabelle.XML.Encode as Encode import qualified Isabelle.XML.Decode as Decode import qualified Isabelle.Term_XML.Encode as Encode import qualified Isabelle.Term_XML.Decode as Decode import qualified Isabelle.Properties as Properties import Isabelle.Bytes (Bytes) import Isabelle.Term (Typ, Term) class Encode_Atom a where encode_atom :: Encode.A a class Decode_Atom a where decode_atom :: Decode.A a instance Encode_Atom Int where encode_atom = Encode.int_atom instance Decode_Atom Int where decode_atom = Decode.int_atom instance Encode_Atom Bool where encode_atom = Encode.bool_atom instance Decode_Atom Bool where decode_atom = Decode.bool_atom instance Encode_Atom () where encode_atom = Encode.unit_atom instance Decode_Atom () where decode_atom = Decode.unit_atom class Encode a where encode :: Encode.T a class Decode a where decode :: Decode.T a instance Encode Bytes where encode = Encode.string instance Decode Bytes where decode = Decode.string instance Encode Int where encode = Encode.int instance Decode Int where decode = Decode.int instance Encode Bool where encode = Encode.bool instance Decode Bool where decode = Decode.bool instance Encode () where encode = Encode.unit instance Decode () where decode = Decode.unit instance (Encode a, Encode b) => Encode (a, b) where encode = Encode.pair encode encode instance (Decode a, Decode b) => Decode (a, b) where decode = Decode.pair decode decode instance (Encode a, Encode b, Encode c) => Encode (a, b, c) where encode = Encode.triple encode encode encode instance (Decode a, Decode b, Decode c) => Decode (a, b, c) where decode = Decode.triple decode decode decode instance Encode a => Encode [a] where encode = Encode.list encode instance Decode a => Decode [a] where decode = Decode.list decode instance Encode a => Encode (Maybe a) where encode = Encode.option encode instance Decode a => Decode (Maybe a) where decode = Decode.option decode instance Encode XML.Tree where encode = Encode.tree instance Decode XML.Tree where decode = Decode.tree instance Encode Properties.T where encode = Encode.properties instance Decode Properties.T where decode = Decode.properties instance Encode Typ where encode = Encode.typ instance Decode Typ where decode = Decode.typ instance Encode Term where encode = Encode.term instance Decode Term where decode = Decode.term \ generate_file "Isabelle/UUID.hs" = \ {- Title: Isabelle/UUID.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Universally unique identifiers. See \<^file>\$ISABELLE_HOME/src/Pure/General/uuid.scala\. -} module Isabelle.UUID (T, random, print, parse) where import Prelude hiding (print) import Data.UUID (UUID) import qualified Data.UUID as UUID import Data.UUID.V4 (nextRandom) import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) type T = UUID random :: IO T random = nextRandom print :: T -> Bytes print = Bytes.make . UUID.toASCIIBytes parse :: Bytes -> Maybe T parse = UUID.fromASCIIBytes . Bytes.unmake \ generate_file "Isabelle/Byte_Message.hs" = \ {- Title: Isabelle/Byte_Message.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Byte-oriented messages. See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} module Isabelle.Byte_Message ( write, write_line, read, read_block, read_line, make_message, write_message, read_message, make_line_message, write_line_message, read_line_message, read_yxml, write_yxml ) where import Prelude hiding (read) import Data.Maybe import qualified Data.ByteString as ByteString import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.Symbol as Symbol import qualified Isabelle.UTF8 as UTF8 import qualified Isabelle.XML as XML import qualified Isabelle.YXML as YXML import Network.Socket (Socket) import qualified Network.Socket.ByteString as Socket import Isabelle.Library import qualified Isabelle.Value as Value {- output operations -} write :: Socket -> [Bytes] -> IO () write socket = Socket.sendMany socket . map Bytes.unmake write_line :: Socket -> Bytes -> IO () write_line socket s = write socket [s, "\n"] {- input operations -} read :: Socket -> Int -> IO Bytes read socket n = read_body 0 [] where result = Bytes.concat . reverse read_body len ss = if len >= n then return (result ss) else (do s <- Socket.recv socket (min (n - len) 8192) case ByteString.length s of 0 -> return (result ss) m -> read_body (len + m) (Bytes.make s : ss)) read_block :: Socket -> Int -> IO (Maybe Bytes, Int) read_block socket n = do msg <- read socket n let len = Bytes.length msg return (if len == n then Just msg else Nothing, len) read_line :: Socket -> IO (Maybe Bytes) read_line socket = read_body [] where result = trim_line . Bytes.pack . reverse read_body bs = do s <- Socket.recv socket 1 case ByteString.length s of 0 -> return (if null bs then Nothing else Just (result bs)) 1 -> case ByteString.head s of 10 -> return (Just (result bs)) b -> read_body (b : bs) {- messages with multiple chunks (arbitrary content) -} make_header :: [Int] -> [Bytes] make_header ns = [space_implode "," (map Value.print_int ns), "\n"] make_message :: [Bytes] -> [Bytes] make_message chunks = make_header (map Bytes.length chunks) <> chunks write_message :: Socket -> [Bytes] -> IO () write_message socket = write socket . make_message parse_header :: Bytes -> [Int] parse_header line = let res = map Value.parse_nat (space_explode ',' line) in if all isJust res then map fromJust res else error ("Malformed message header: " <> quote (UTF8.decode line)) read_chunk :: Socket -> Int -> IO Bytes read_chunk socket n = do res <- read_block socket n return $ case res of (Just chunk, _) -> chunk (Nothing, len) -> error ("Malformed message chunk: unexpected EOF after " <> show len <> " of " <> show n <> " bytes") read_message :: Socket -> IO (Maybe [Bytes]) read_message socket = do res <- read_line socket case res of Just line -> Just <$> mapM (read_chunk socket) (parse_header line) Nothing -> return Nothing -- hybrid messages: line or length+block (with content restriction) is_length :: Bytes -> Bool is_length msg = not (Bytes.null msg) && Bytes.all_char (\c -> '0' <= c && c <= '9') msg is_terminated :: Bytes -> Bool is_terminated msg = not (Bytes.null msg) && Symbol.is_ascii_line_terminator (Bytes.char $ Bytes.last msg) make_line_message :: Bytes -> [Bytes] make_line_message msg = let n = Bytes.length msg in if is_length msg || is_terminated msg then error ("Bad content for line message:\n" <> take 100 (UTF8.decode msg)) else (if n > 100 || Bytes.any_char (== '\n') msg then make_header [n + 1] else []) <> [msg, "\n"] write_line_message :: Socket -> Bytes -> IO () write_line_message socket = write socket . make_line_message read_line_message :: Socket -> IO (Maybe Bytes) read_line_message socket = do opt_line <- read_line socket case opt_line of Nothing -> return Nothing Just line -> case Value.parse_nat line of Nothing -> return $ Just line Just n -> fmap trim_line . fst <$> read_block socket n read_yxml :: Socket -> IO (Maybe XML.Body) read_yxml socket = do res <- read_line_message socket return (YXML.parse_body <$> res) write_yxml :: Socket -> XML.Body -> IO () write_yxml socket body = write_line_message socket (YXML.string_of_body body) \ generate_file "Isabelle/Isabelle_Thread.hs" = \ {- Title: Isabelle/Isabelle_Thread.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Isabelle-specific thread management. See \<^file>\$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.scala\. -} {-# LANGUAGE NamedFieldPuns #-} module Isabelle.Isabelle_Thread ( ThreadId, Result, find_id, properties, change_properties, add_resource, del_resource, bracket_resource, is_stopped, expose_stopped, stop, my_uuid, stop_uuid, Fork, fork_finally, fork) where import Data.Unique import Data.IORef import System.IO.Unsafe import qualified Data.List as List import Control.Monad (when, forM_) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Control.Exception as Exception import Control.Concurrent (ThreadId) import qualified Control.Concurrent as Concurrent import Control.Concurrent.Thread (Result) import qualified Control.Concurrent.Thread as Thread import qualified Isabelle.UUID as UUID import qualified Isabelle.Properties as Properties {- thread info -} type Resources = Map Unique (IO ()) data Info = Info {uuid :: UUID.T, props :: Properties.T, stopped :: Bool, resources :: Resources} type Infos = Map ThreadId Info lookup_info :: Infos -> ThreadId -> Maybe Info lookup_info infos id = Map.lookup id infos init_info :: ThreadId -> UUID.T -> Infos -> (Infos, ()) init_info id uuid infos = (Map.insert id (Info uuid [] False Map.empty) infos, ()) {- global state -} {-# NOINLINE global_state #-} global_state :: IORef Infos global_state = unsafePerformIO (newIORef Map.empty) find_id :: UUID.T -> IO (Maybe ThreadId) find_id uuid = do state <- readIORef global_state return $ fst <$> List.find (\(_, Info{uuid = uuid'}) -> uuid == uuid') (Map.assocs state) get_info :: ThreadId -> IO (Maybe Info) get_info id = do state <- readIORef global_state return $ lookup_info state id map_info :: ThreadId -> (Info -> Info) -> IO (Maybe Info) map_info id f = atomicModifyIORef' global_state (\infos -> case lookup_info infos id of Nothing -> (infos, Nothing) Just info -> let info' = f info in (Map.insert id info' infos, Just info')) delete_info :: ThreadId -> IO () delete_info id = atomicModifyIORef' global_state (\infos -> (Map.delete id infos, ())) {- thread properties -} my_info :: IO (Maybe Info) my_info = do id <- Concurrent.myThreadId get_info id properties :: IO Properties.T properties = maybe [] props <$> my_info change_properties :: (Properties.T -> Properties.T) -> IO () change_properties f = do id <- Concurrent.myThreadId map_info id (\info -> info {props = f (props info)}) return () {- managed resources -} add_resource :: IO () -> IO Unique add_resource resource = do id <- Concurrent.myThreadId u <- newUnique map_info id (\info -> info {resources = Map.insert u resource (resources info)}) return u del_resource :: Unique -> IO () del_resource u = do id <- Concurrent.myThreadId map_info id (\info -> info {resources = Map.delete u (resources info)}) return () bracket_resource :: IO () -> IO a -> IO a bracket_resource resource body = Exception.bracket (add_resource resource) del_resource (const body) {- stop -} is_stopped :: IO Bool is_stopped = maybe False stopped <$> my_info expose_stopped :: IO () expose_stopped = do stopped <- is_stopped when stopped $ throw ThreadKilled stop :: ThreadId -> IO () stop id = do info <- map_info id (\info -> info {stopped = True}) let ops = case info of Nothing -> []; Just Info{resources} -> map snd (Map.toDescList resources) sequence_ ops {- UUID -} my_uuid :: IO (Maybe UUID.T) my_uuid = fmap uuid <$> my_info stop_uuid :: UUID.T -> IO () stop_uuid uuid = do id <- find_id uuid forM_ id stop {- fork -} type Fork a = (ThreadId, UUID.T, IO (Result a)) fork_finally :: IO a -> (Either SomeException a -> IO b) -> IO (Fork b) fork_finally body finally = do uuid <- UUID.random (id, result) <- Exception.mask (\restore -> Thread.forkIO (Exception.try (do id <- Concurrent.myThreadId atomicModifyIORef' global_state (init_info id uuid) restore body) >>= (\res -> do id <- Concurrent.myThreadId; delete_info id; finally res))) return (id, uuid, result) fork :: IO a -> IO (Fork a) fork body = fork_finally body Thread.result \ generate_file "Isabelle/Server.hs" = \ {- Title: Isabelle/Server.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) TCP server on localhost. -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Server ( localhost_name, localhost, publish_text, publish_stdout, server, connection ) where import Control.Monad (forever, when) import qualified Control.Exception as Exception import Network.Socket (Socket) import qualified Network.Socket as Socket import qualified System.IO as IO import qualified Data.ByteString.Char8 as Char8 import Isabelle.Library import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.UUID as UUID import qualified Isabelle.Byte_Message as Byte_Message import qualified Isabelle.Isabelle_Thread as Isabelle_Thread {- server address -} localhost_name :: Bytes localhost_name = "127.0.0.1" localhost :: Socket.HostAddress localhost = Socket.tupleToHostAddress (127, 0, 0, 1) publish_text :: Bytes -> Bytes -> UUID.T -> Bytes publish_text name address password = "server " <> quote name <> " = " <> address <> " (password " <> quote (show_bytes password) <> ")" publish_stdout :: Bytes -> Bytes -> UUID.T -> IO () publish_stdout name address password = Char8.putStrLn (Bytes.unmake $ publish_text name address password) {- server -} server :: (Bytes -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO () server publish handle = Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop) where open :: IO (Socket, Bytes) open = do server_socket <- Socket.socket Socket.AF_INET Socket.Stream Socket.defaultProtocol Socket.bind server_socket (Socket.SockAddrInet 0 localhost) Socket.listen server_socket 50 port <- Socket.socketPort server_socket let address = localhost_name <> ":" <> show_bytes port password <- UUID.random publish address password return (server_socket, UUID.print password) loop :: Socket -> Bytes -> IO () loop server_socket password = forever $ do (connection, _) <- Socket.accept server_socket Isabelle_Thread.fork_finally (do line <- Byte_Message.read_line connection when (line == Just password) $ handle connection) (\finally -> do Socket.close connection case finally of Left exn -> IO.hPutStrLn IO.stderr $ Exception.displayException exn Right () -> return ()) return () {- client connection -} connection :: String -> Bytes -> (Socket -> IO a) -> IO a connection port password client = Socket.withSocketsDo $ do addr <- resolve Exception.bracket (open addr) Socket.close body where resolve = do let hints = Socket.defaultHints { Socket.addrFlags = [Socket.AI_NUMERICHOST, Socket.AI_NUMERICSERV], Socket.addrSocketType = Socket.Stream } head <$> Socket.getAddrInfo (Just hints) (Just "127.0.0.1") (Just port) open addr = do socket <- Socket.socket (Socket.addrFamily addr) (Socket.addrSocketType addr) (Socket.addrProtocol addr) Socket.connect socket $ Socket.addrAddress addr return socket body socket = do Byte_Message.write_line socket password client socket \ generate_file "Isabelle/Time.hs" = \ {- Title: Isabelle/Time.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Time based on milliseconds. See \<^file>\~~/src/Pure/General/time.scala\ -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Time ( Time, seconds, minutes, ms, zero, is_zero, is_relevant, get_seconds, get_minutes, get_ms, message ) where import Text.Printf (printf) import Isabelle.Bytes (Bytes) import Isabelle.Library data Time = Time Int instance Eq Time where Time ms1 == Time ms2 = ms1 == ms2 instance Ord Time where compare (Time ms1) (Time ms2) = compare ms1 ms2 seconds :: Double -> Time seconds s = Time (round (s * 1000.0)) minutes :: Double -> Time minutes m = Time (round (m * 60000.0)) ms :: Int -> Time ms = Time zero :: Time zero = ms 0 is_zero :: Time -> Bool is_zero (Time ms) = ms == 0 is_relevant :: Time -> Bool is_relevant (Time ms) = ms >= 1 get_seconds :: Time -> Double get_seconds (Time ms) = fromIntegral ms / 1000.0 get_minutes :: Time -> Double get_minutes (Time ms) = fromIntegral ms / 60000.0 get_ms :: Time -> Int get_ms (Time ms) = ms instance Show Time where show t = printf "%.3f" (get_seconds t) message :: Time -> Bytes message t = make_bytes (show t) <> "s" \ generate_file "Isabelle/Timing.hs" = \ {- Title: Isabelle/Timing.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Support for time measurement. See \<^file>\~~/src/Pure/General/timing.ML\ and \<^file>\~~/src/Pure/General/timing.scala\ -} module Isabelle.Timing ( Timing (..), zero, is_zero, is_relevant ) where import qualified Isabelle.Time as Time import Isabelle.Time (Time) data Timing = Timing {elapsed :: Time, cpu :: Time, gc :: Time} deriving (Show, Eq) zero :: Timing zero = Timing Time.zero Time.zero Time.zero is_zero :: Timing -> Bool is_zero t = Time.is_zero (elapsed t) && Time.is_zero (cpu t) && Time.is_zero (gc t) is_relevant :: Timing -> Bool is_relevant t = Time.is_relevant (elapsed t) || Time.is_relevant (cpu t) || Time.is_relevant (gc t) \ generate_file "Isabelle/Bash.hs" = \ {- Title: Isabelle/Bash.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Support for GNU bash. See \<^file>\$ISABELLE_HOME/src/Pure/System/bash.ML\ -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Bash ( string, strings, Params, get_script, get_input, get_cwd, get_putenv, get_redirect, get_timeout, get_description, script, input, cwd, putenv, redirect, timeout, description, ) where import Text.Printf (printf) import qualified Isabelle.Symbol as Symbol import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) import qualified Isabelle.Time as Time import Isabelle.Time (Time) import Isabelle.Library {- concrete syntax -} string :: Bytes -> Bytes string str = if Bytes.null str then "\"\"" else str |> Bytes.unpack |> map trans |> Bytes.concat where trans b = case Bytes.char b of '\t' -> "$'\\t'" '\n' -> "$'\\n'" '\f' -> "$'\\f'" '\r' -> "$'\\r'" c -> if Symbol.is_ascii_letter c || Symbol.is_ascii_digit c || c `elem` ("+,-./:_" :: String) then Bytes.singleton b else if b < 32 || b >= 127 then make_bytes (printf "$'\\x%02x'" b :: String) else "\\" <> Bytes.singleton b strings :: [Bytes] -> Bytes strings = space_implode " " . map string {- server parameters -} data Params = Params { _script :: Bytes, _input :: Bytes, _cwd :: Maybe Bytes, _putenv :: [(Bytes, Bytes)], _redirect :: Bool, _timeout :: Time, _description :: Bytes} deriving (Show, Eq) get_script :: Params -> Bytes get_script = _script get_input :: Params -> Bytes get_input = _input get_cwd :: Params -> Maybe Bytes get_cwd = _cwd get_putenv :: Params -> [(Bytes, Bytes)] get_putenv = _putenv get_redirect :: Params -> Bool get_redirect = _redirect get_timeout :: Params -> Time get_timeout = _timeout get_description :: Params -> Bytes get_description = _description script :: Bytes -> Params script script = Params script "" Nothing [] False Time.zero "" input :: Bytes -> Params -> Params input input params = params { _input = input } cwd :: Bytes -> Params -> Params cwd cwd params = params { _cwd = Just cwd } putenv :: [(Bytes, Bytes)] -> Params -> Params putenv putenv params = params { _putenv = putenv } redirect :: Params -> Params redirect params = params { _redirect = True } timeout :: Time -> Params -> Params timeout timeout params = params { _timeout = timeout } description :: Bytes -> Params -> Params description description params = params { _description = description } \ generate_file "Isabelle/Process_Result.hs" = \ {- Title: Isabelle/Process_Result.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Result of system process. See \<^file>\~~/src/Pure/System/process_result.ML\ and \<^file>\~~/src/Pure/System/process_result.scala\ -} {-# LANGUAGE OverloadedStrings #-} module Isabelle.Process_Result ( interrupt_rc, timeout_rc, T, make, rc, out_lines, err_lines, timing, timing_elapsed, out, err, ok, check ) where import Isabelle.Time (Time) import qualified Isabelle.Timing as Timing import Isabelle.Timing (Timing) import Isabelle.Bytes (Bytes) import Isabelle.Library interrupt_rc :: Int interrupt_rc = 130 timeout_rc :: Int timeout_rc = 142 data T = Process_Result { _rc :: Int, _out_lines :: [Bytes], _err_lines :: [Bytes], _timing :: Timing} deriving (Show, Eq) make :: Int -> [Bytes] -> [Bytes] -> Timing -> T make = Process_Result rc :: T -> Int rc = _rc out_lines :: T -> [Bytes] out_lines = _out_lines err_lines :: T -> [Bytes] err_lines = _err_lines timing :: T -> Timing timing = _timing timing_elapsed :: T -> Time timing_elapsed = Timing.elapsed . timing out :: T -> Bytes out = trim_line . cat_lines . out_lines err :: T -> Bytes err = trim_line . cat_lines . err_lines ok :: T -> Bool ok result = rc result == 0 check :: T -> T check result = if ok result then result else error (make_string $ err result) \ generate_file "Isabelle/Options.hs" = \ {- Title: Isabelle/Options.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) System options with external string representation. See \<^file>\~~/src/Pure/System/options.ML\ and \<^file>\~~/src/Pure/System/options.scala\ -} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE InstanceSigs #-} module Isabelle.Options ( boolT, intT, realT, stringT, unknownT, T, typ, bool, int, real, seconds, string, decode ) where import qualified Data.Map.Strict as Map import Data.Map.Strict (Map) import qualified Isabelle.Properties as Properties import Isabelle.Bytes (Bytes) import qualified Isabelle.Value as Value import qualified Isabelle.Time as Time import Isabelle.Time (Time) import Isabelle.Library import qualified Isabelle.XML.Decode as Decode import Isabelle.XML.Classes (Decode (..)) {- representation -} boolT :: Bytes boolT = "bool" intT :: Bytes intT = "int" realT :: Bytes realT = "real" stringT :: Bytes stringT = "string" unknownT :: Bytes unknownT = "unknown" data Opt = Opt { _pos :: Properties.T, _name :: Bytes, _typ :: Bytes, _value :: Bytes } data T = Options (Map Bytes Opt) {- check -} check_name :: T -> Bytes -> Opt check_name (Options map) name = case Map.lookup name map of Just opt | _typ opt /= unknownT -> opt _ -> error (make_string ("Unknown system option " <> quote name)) check_type :: T -> Bytes -> Bytes -> Opt check_type options name typ = let opt = check_name options name t = _typ opt in if t == typ then opt else error (make_string ("Ill-typed system option " <> quote name <> " : " <> t <> " vs. " <> typ)) {- get typ -} typ :: T -> Bytes -> Bytes typ options name = _typ (check_name options name) {- get value -} get :: Bytes -> (Bytes -> Maybe a) -> T -> Bytes -> a get typ parse options name = let opt = check_type options name typ in case parse (_value opt) of Just x -> x Nothing -> error (make_string ("Malformed value for system option " <> quote name <> " : " <> typ <> " =\n" <> quote (_value opt))) bool :: T -> Bytes -> Bool bool = get boolT Value.parse_bool int :: T -> Bytes -> Int int = get intT Value.parse_int real :: T -> Bytes -> Double real = get realT Value.parse_real seconds :: T -> Bytes -> Time seconds options = Time.seconds . real options string :: T -> Bytes -> Bytes string = get stringT Just {- decode -} instance Decode T where decode :: Decode.T T decode = let decode_entry :: Decode.T (Bytes, Opt) decode_entry body = let (pos, (name, (typ, value))) = Decode.pair Decode.properties (Decode.pair Decode.string (Decode.pair Decode.string Decode.string)) body in (name, Opt { _pos = pos, _name = name, _typ = typ, _value = value }) in Options . Map.fromList . Decode.list decode_entry \ export_generated_files _ end