# HG changeset patch # User wenzelm # Date 1189782154 -7200 # Node ID e840872e9c7cb251ffa43a6cb9f8da8ebc11f613 # Parent 5bbdc9b6064843087e7e7b85b92656c20917a35b moved ML_XXX.ML files to Pure/ML; diff -r 5bbdc9b60648 -r e840872e9c7c src/Pure/General/ml_syntax.ML --- a/src/Pure/General/ml_syntax.ML Fri Sep 14 15:27:12 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -(* Title: Pure/General/ml_syntax.ML - ID: $Id$ - Author: Makarius - -Basic ML syntax operations. -*) - -signature ML_SYNTAX = -sig - val reserved_names: string list - val reserved: Name.context - val is_reserved: string -> bool - val is_identifier: string -> bool - val atomic: string -> string - val print_int: int -> string - val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string - val print_list: ('a -> string) -> 'a list -> string - val print_option: ('a -> string) -> 'a option -> string - val print_char: string -> string - val print_string: string -> string - val print_strings: string list -> string - val print_indexname: indexname -> string - val print_class: class -> string - val print_sort: sort -> string - val print_typ: typ -> string - val print_term: term -> string -end; - -structure ML_Syntax: ML_SYNTAX = -struct - -(* reserved words *) - -val reserved_names = - ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", - "end", "exception", "fn", "fun", "handle", "if", "in", "infix", - "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", - "raise", "rec", "then", "type", "val", "with", "withtype", "while", - "eqtype", "functor", "include", "sharing", "sig", "signature", - "struct", "structure", "where"]; - -val reserved = Name.make_context reserved_names; -val is_reserved = Name.is_declared reserved; - - -(* identifiers *) - -fun is_identifier name = - not (is_reserved name) andalso Syntax.is_ascii_identifier name; - - -(* literal output -- unformatted *) - -val atomic = enclose "(" ")"; - -val print_int = Int.toString; - -fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")"; - -fun print_list f = enclose "[" "]" o commas o map f; - -fun print_option f NONE = "NONE" - | print_option f (SOME x) = "SOME (" ^ f x ^ ")"; - -fun print_char s = - if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s) - else if s = "\"" then "\\\"" - else if s = "\\" then "\\\\" - else - let val c = ord s in - if c < 32 then "\\^" ^ chr (c + ord "@") - else if c < 127 then s - else "\\" ^ string_of_int c - end; - -val print_string = quote o translate_string print_char; -val print_strings = print_list print_string; - -val print_indexname = print_pair print_string print_int; - -val print_class = print_string; -val print_sort = print_list print_class; - -fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg - | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg - | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg; - -fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg - | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg - | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg - | print_term (Bound i) = "Bound " ^ print_int i - | print_term (Abs (s, T, t)) = - "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")" - | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2); - -end; diff -r 5bbdc9b60648 -r e840872e9c7c src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Sep 14 15:27:12 2007 +0200 +++ b/src/Pure/IsaMakefile Fri Sep 14 17:02:34 2007 +0200 @@ -27,33 +27,34 @@ CPure.thy General/ROOT.ML General/alist.ML General/balanced_tree.ML \ General/basics.ML General/buffer.ML General/file.ML General/graph.ML \ General/heap.ML General/history.ML General/markup.ML \ - General/ml_syntax.ML General/name_space.ML General/ord_list.ML \ - General/output.ML General/path.ML General/position.ML \ - General/pretty.ML General/print_mode.ML General/scan.ML \ - General/secure.ML General/seq.ML General/source.ML General/stack.ML \ - General/susp.ML General/symbol.ML General/table.ML General/url.ML \ - General/xml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \ - Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML \ - Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \ - Isar/element.ML Isar/find_theorems.ML Isar/induct_attrib.ML \ - Isar/isar_cmd.ML Isar/isar_syn.ML Isar/local_defs.ML \ - Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ - Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \ - Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ - Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \ - Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML \ - Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML \ - Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \ - Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML \ + General/name_space.ML General/ord_list.ML General/output.ML \ + General/path.ML General/position.ML General/pretty.ML \ + General/print_mode.ML General/scan.ML General/secure.ML General/seq.ML \ + General/source.ML General/stack.ML General/susp.ML General/symbol.ML \ + General/table.ML General/url.ML General/xml.ML Isar/ROOT.ML \ + Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ + Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML \ + Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \ + Isar/find_theorems.ML Isar/induct_attrib.ML Isar/isar_cmd.ML \ + Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \ + Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \ + Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \ + Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \ + Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML \ + Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_insts.ML \ + Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML \ + Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \ + ML-Systems/alice.ML ML-Systems/exn.ML \ ML-Systems/multithreading_dummy.ML ML-Systems/multithreading_polyml.ML \ ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \ ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-5.0.ML \ ML-Systems/polyml-5.1.ML ML-Systems/polyml-interrupt-timeout.ML \ ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML \ ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/proper_int.ML \ - ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \ - Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ - ProofGeneral/ROOT.ML ProofGeneral/parsing.ML ProofGeneral/pgip.ML \ + ML-Systems/smlnj.ML ML/ml_context.ML ML/ml_syntax.ML \ + Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ + Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \ + ProofGeneral/parsing.ML ProofGeneral/pgip.ML \ ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \ ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \ ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \ @@ -61,19 +62,19 @@ ProofGeneral/proof_general_emacs.ML ProofGeneral/proof_general_pgip.ML \ Pure.thy ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML \ Syntax/parser.ML Syntax/printer.ML Syntax/simple_syntax.ML \ - Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \ - Syntax/type_ext.ML Thy/html.ML Thy/latex.ML Thy/ml_context.ML \ - Thy/present.ML Thy/term_style.ML Thy/thm_database.ML Thy/thm_deps.ML \ - Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \ - Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/named_thms.ML \ - Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML \ - compress.ML config.ML conjunction.ML consts.ML context.ML \ - context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML \ - fact_index.ML goal.ML library.ML logic.ML meta_simplifier.ML \ - more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML \ - proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML \ - sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML \ - theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML + Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \ + Syntax/type_ext.ML Thy/html.ML Thy/latex.ML Thy/present.ML \ + Thy/term_style.ML Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_edit.ML \ + Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML \ + Tools/ROOT.ML Tools/invoke.ML Tools/named_thms.ML Tools/xml_syntax.ML \ + assumption.ML axclass.ML codegen.ML compress.ML config.ML \ + conjunction.ML consts.ML context.ML context_position.ML conv.ML \ + defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML library.ML \ + logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \ + old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML \ + pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \ + tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \ + type_infer.ML unify.ML variable.ML @./mk diff -r 5bbdc9b60648 -r e840872e9c7c src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Fri Sep 14 15:27:12 2007 +0200 +++ b/src/Pure/Isar/ROOT.ML Fri Sep 14 17:02:34 2007 +0200 @@ -20,9 +20,9 @@ use "outer_parse.ML"; use "outer_keyword.ML"; use "antiquote.ML"; +use "../ML/ml_context.ML"; (*theory sources*) -use "../Thy/ml_context.ML"; use "../Thy/thy_header.ML"; use "../Thy/thy_load.ML"; use "../Thy/html.ML"; diff -r 5bbdc9b60648 -r e840872e9c7c src/Pure/ML/ml_context.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_context.ML Fri Sep 14 17:02:34 2007 +0200 @@ -0,0 +1,273 @@ +(* Title: Pure/Thy/ml_context.ML + ID: $Id$ + Author: Makarius + +ML context and antiquotations. +*) + +signature BASIC_ML_CONTEXT = +sig + val the_context: unit -> theory + val thm: xstring -> thm + val thms: xstring -> thm list +end; + +signature ML_CONTEXT = +sig + include BASIC_ML_CONTEXT + val get_context: unit -> Context.generic option + val set_context: Context.generic option -> unit + val setmp: Context.generic option -> ('a -> 'b) -> 'a -> 'b + val the_generic_context: unit -> Context.generic + val the_local_context: unit -> Proof.context + val pass: Context.generic option -> ('a -> 'b) -> 'a -> 'b * Context.generic option + val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic + val save: ('a -> 'b) -> 'a -> 'b + val >> : (theory -> theory) -> unit + val add_keywords: string list -> unit + val inline_antiq: string -> + (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit + val value_antiq: string -> + (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit + val proj_value_antiq: string -> (Context.generic * Args.T list -> + (string * string * string) * (Context.generic * Args.T list)) -> unit + val eval_antiquotes_fn: (string -> string * string) ref (* FIXME tmp *) + val trace: bool ref + val use_mltext: string -> bool -> Context.generic option -> unit + val use_mltext_update: string -> bool -> Context.generic -> Context.generic + val use_let: string -> string -> string -> Context.generic -> Context.generic + val use: Path.T -> unit +end; + +structure ML_Context: ML_CONTEXT = +struct + +(** Implicit ML context **) + +local + val current_context = ref (NONE: Context.generic option); +in + fun get_context () = ! current_context; + fun set_context opt_context = current_context := opt_context; + fun setmp opt_context f x = Library.setmp current_context opt_context f x; +end; + +fun the_generic_context () = + (case get_context () of + SOME context => context + | _ => error "Unknown context"); + +val the_local_context = Context.proof_of o the_generic_context; + +val the_context = Context.theory_of o the_generic_context; + +fun pass opt_context f x = + setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x; + +fun pass_context context f x = + (case pass (SOME context) f x of + (y, SOME context') => (y, context') + | (_, NONE) => error "Lost context in ML"); + +fun save f x = CRITICAL (fn () => setmp (get_context ()) f x); + +fun change_theory f = CRITICAL (fn () => + set_context (SOME (Context.map_theory f (the_generic_context ())))); + + + +(** ML antiquotations **) + +(* maintain keywords *) + +val global_lexicon = ref Scan.empty_lexicon; + +fun add_keywords keywords = CRITICAL (fn () => + change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords))); + + +(* maintain commands *) + +datatype antiq = Inline of string | ProjValue of string * string * string; +val global_parsers = ref (Symtab.empty: + (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); + +local + +fun add_item kind name scan = CRITICAL (fn () => + change global_parsers (fn tab => + (if not (Symtab.defined tab name) then () + else warning ("Redefined ML antiquotation: " ^ quote name); + Symtab.update (name, scan >> kind) tab))); + +in + +val inline_antiq = add_item Inline; +val proj_value_antiq = add_item ProjValue; +fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, ""))); + +end; + + +(* command syntax *) + +fun syntax scan src = + #1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ())); + +fun command src = + let val ((name, _), pos) = Args.dest_src src in + (case Symtab.lookup (! global_parsers) name of + NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) + | SOME scan => syntax scan src) + end; + + +(* outer syntax *) + +structure T = OuterLex; +structure P = OuterParse; + +val antiq = + P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) + >> (fn ((x, pos), y) => Args.src ((x, y), pos)); + + +(* input/output wrappers *) + +local + +val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; +val isabelle_struct0 = isabelle_struct ""; + +fun eval_antiquotes txt = CRITICAL (fn () => + let + val ants = Antiquote.scan_antiquotes (txt, Position.line 1); + + fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) + | expand (Antiquote.Antiq x) names = + (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of + Inline s => (("", s), names) + | ProjValue (a, s, f) => + let + val a' = if ML_Syntax.is_identifier a then a else "val"; + val ([b], names') = Name.variants [a'] names; + val binding = "val " ^ b ^ " = " ^ s ^ ";\n"; + val value = + if f = "" then "Isabelle." ^ b + else "(" ^ f ^ " Isabelle." ^ b ^ ")"; + in ((binding, value), names') end); + + val (decls, body) = + fold_map expand ants ML_Syntax.reserved + |> #1 |> split_list |> pairself implode; + in (isabelle_struct decls, body) end); + +fun eval name verbose txt = use_text name Output.ml_output verbose txt; + +in + +val eval_antiquotes_fn = ref eval_antiquotes; + +val trace = ref false; + +fun eval_wrapper name verbose txt = + let + val (txt1, txt2) = ! eval_antiquotes_fn txt; + val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else (); + in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end; + +end; + + +(* ML evaluation *) + +fun use_mltext txt verbose opt_context = + setmp opt_context (fn () => eval_wrapper "ML" verbose txt) (); + +fun use_mltext_update txt verbose context = + #2 (pass_context context (eval_wrapper "ML" verbose) txt); + +fun use_context txt = use_mltext_update + ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false; + +fun use_let bind body txt = + use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); + +fun use path = eval_wrapper (Path.implode path) true (File.read path); + + +(* basic antiquotations *) + +val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); + +val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); +val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); +val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); + +val _ = value_antiq "ctyp" (Args.typ >> (fn T => + ("ctyp", + "Thm.ctyp_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)))); + +val _ = value_antiq "cterm" (Args.term >> (fn t => + ("cterm", + "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); + +val _ = value_antiq "cprop" (Args.prop >> (fn t => + ("cprop", + "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); + + +fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) => + #1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c)) + |> syn ? ProofContext.const_syntax_name ctxt + |> ML_Syntax.print_string); + +val _ = inline_antiq "const_name" (const false); +val _ = inline_antiq "const_syntax" (const true); + + + +(** fact references **) + +fun thm name = ProofContext.get_thm (the_local_context ()) (Name name); +fun thms name = ProofContext.get_thms (the_local_context ()) (Name name); + + +local + +fun print_interval (FromTo arg) = + "PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg + | print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i + | print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i; + +fun thm_sel name = + Args.thm_sel >> (fn is => "PureThy.NameSelection " ^ + ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is)) + || Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name); + +fun thm_antiq kind = value_antiq kind + (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel => + "ProofContext.get_" ^ kind ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel)); + +in + +val _ = add_keywords ["(", ")", "-", ","]; +val _ = thm_antiq "thm"; +val _ = thm_antiq "thms"; + +end; + +val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> + (fn ns => ("cpat", + "((cterm_of (ML_Context.the_context ())) o Library.the_single o " ^ + "(ProofContext.read_term_pats TypeInfer.logicT (ML_Context.the_local_context ())))" + ^ (ML_Syntax.print_list ML_Syntax.print_string [ns]), ""))); + +(*final declarations of this structure!*) +nonfix >>; +fun >> f = change_theory f; + +end; + +structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; +open Basic_ML_Context; diff -r 5bbdc9b60648 -r e840872e9c7c src/Pure/ML/ml_syntax.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_syntax.ML Fri Sep 14 17:02:34 2007 +0200 @@ -0,0 +1,96 @@ +(* Title: Pure/General/ml_syntax.ML + ID: $Id$ + Author: Makarius + +Basic ML syntax operations. +*) + +signature ML_SYNTAX = +sig + val reserved_names: string list + val reserved: Name.context + val is_reserved: string -> bool + val is_identifier: string -> bool + val atomic: string -> string + val print_int: int -> string + val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string + val print_list: ('a -> string) -> 'a list -> string + val print_option: ('a -> string) -> 'a option -> string + val print_char: string -> string + val print_string: string -> string + val print_strings: string list -> string + val print_indexname: indexname -> string + val print_class: class -> string + val print_sort: sort -> string + val print_typ: typ -> string + val print_term: term -> string +end; + +structure ML_Syntax: ML_SYNTAX = +struct + +(* reserved words *) + +val reserved_names = + ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", + "end", "exception", "fn", "fun", "handle", "if", "in", "infix", + "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", + "raise", "rec", "then", "type", "val", "with", "withtype", "while", + "eqtype", "functor", "include", "sharing", "sig", "signature", + "struct", "structure", "where"]; + +val reserved = Name.make_context reserved_names; +val is_reserved = Name.is_declared reserved; + + +(* identifiers *) + +fun is_identifier name = + not (is_reserved name) andalso Syntax.is_ascii_identifier name; + + +(* literal output -- unformatted *) + +val atomic = enclose "(" ")"; + +val print_int = Int.toString; + +fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")"; + +fun print_list f = enclose "[" "]" o commas o map f; + +fun print_option f NONE = "NONE" + | print_option f (SOME x) = "SOME (" ^ f x ^ ")"; + +fun print_char s = + if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s) + else if s = "\"" then "\\\"" + else if s = "\\" then "\\\\" + else + let val c = ord s in + if c < 32 then "\\^" ^ chr (c + ord "@") + else if c < 127 then s + else "\\" ^ string_of_int c + end; + +val print_string = quote o translate_string print_char; +val print_strings = print_list print_string; + +val print_indexname = print_pair print_string print_int; + +val print_class = print_string; +val print_sort = print_list print_class; + +fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg + | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg + | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg; + +fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg + | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg + | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg + | print_term (Bound i) = "Bound " ^ print_int i + | print_term (Abs (s, T, t)) = + "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")" + | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2); + +end; diff -r 5bbdc9b60648 -r e840872e9c7c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Sep 14 15:27:12 2007 +0200 +++ b/src/Pure/ROOT.ML Fri Sep 14 17:02:34 2007 +0200 @@ -44,7 +44,7 @@ use "Syntax/printer.ML"; use "Syntax/syntax.ML"; -use "General/ml_syntax.ML"; +use "ML/ml_syntax.ML"; (*core of tactical proof system*) use "envir.ML"; diff -r 5bbdc9b60648 -r e840872e9c7c src/Pure/Thy/ml_context.ML --- a/src/Pure/Thy/ml_context.ML Fri Sep 14 15:27:12 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,273 +0,0 @@ -(* Title: Pure/Thy/ml_context.ML - ID: $Id$ - Author: Makarius - -ML context and antiquotations. -*) - -signature BASIC_ML_CONTEXT = -sig - val the_context: unit -> theory - val thm: xstring -> thm - val thms: xstring -> thm list -end; - -signature ML_CONTEXT = -sig - include BASIC_ML_CONTEXT - val get_context: unit -> Context.generic option - val set_context: Context.generic option -> unit - val setmp: Context.generic option -> ('a -> 'b) -> 'a -> 'b - val the_generic_context: unit -> Context.generic - val the_local_context: unit -> Proof.context - val pass: Context.generic option -> ('a -> 'b) -> 'a -> 'b * Context.generic option - val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic - val save: ('a -> 'b) -> 'a -> 'b - val >> : (theory -> theory) -> unit - val add_keywords: string list -> unit - val inline_antiq: string -> - (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit - val value_antiq: string -> - (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit - val proj_value_antiq: string -> (Context.generic * Args.T list -> - (string * string * string) * (Context.generic * Args.T list)) -> unit - val eval_antiquotes_fn: (string -> string * string) ref (* FIXME tmp *) - val trace: bool ref - val use_mltext: string -> bool -> Context.generic option -> unit - val use_mltext_update: string -> bool -> Context.generic -> Context.generic - val use_let: string -> string -> string -> Context.generic -> Context.generic - val use: Path.T -> unit -end; - -structure ML_Context: ML_CONTEXT = -struct - -(** Implicit ML context **) - -local - val current_context = ref (NONE: Context.generic option); -in - fun get_context () = ! current_context; - fun set_context opt_context = current_context := opt_context; - fun setmp opt_context f x = Library.setmp current_context opt_context f x; -end; - -fun the_generic_context () = - (case get_context () of - SOME context => context - | _ => error "Unknown context"); - -val the_local_context = Context.proof_of o the_generic_context; - -val the_context = Context.theory_of o the_generic_context; - -fun pass opt_context f x = - setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x; - -fun pass_context context f x = - (case pass (SOME context) f x of - (y, SOME context') => (y, context') - | (_, NONE) => error "Lost context in ML"); - -fun save f x = CRITICAL (fn () => setmp (get_context ()) f x); - -fun change_theory f = CRITICAL (fn () => - set_context (SOME (Context.map_theory f (the_generic_context ())))); - - - -(** ML antiquotations **) - -(* maintain keywords *) - -val global_lexicon = ref Scan.empty_lexicon; - -fun add_keywords keywords = CRITICAL (fn () => - change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords))); - - -(* maintain commands *) - -datatype antiq = Inline of string | ProjValue of string * string * string; -val global_parsers = ref (Symtab.empty: - (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); - -local - -fun add_item kind name scan = CRITICAL (fn () => - change global_parsers (fn tab => - (if not (Symtab.defined tab name) then () - else warning ("Redefined ML antiquotation: " ^ quote name); - Symtab.update (name, scan >> kind) tab))); - -in - -val inline_antiq = add_item Inline; -val proj_value_antiq = add_item ProjValue; -fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, ""))); - -end; - - -(* command syntax *) - -fun syntax scan src = - #1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ())); - -fun command src = - let val ((name, _), pos) = Args.dest_src src in - (case Symtab.lookup (! global_parsers) name of - NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) - | SOME scan => syntax scan src) - end; - - -(* outer syntax *) - -structure T = OuterLex; -structure P = OuterParse; - -val antiq = - P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) - >> (fn ((x, pos), y) => Args.src ((x, y), pos)); - - -(* input/output wrappers *) - -local - -val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; -val isabelle_struct0 = isabelle_struct ""; - -fun eval_antiquotes txt = CRITICAL (fn () => - let - val ants = Antiquote.scan_antiquotes (txt, Position.line 1); - - fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) - | expand (Antiquote.Antiq x) names = - (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of - Inline s => (("", s), names) - | ProjValue (a, s, f) => - let - val a' = if ML_Syntax.is_identifier a then a else "val"; - val ([b], names') = Name.variants [a'] names; - val binding = "val " ^ b ^ " = " ^ s ^ ";\n"; - val value = - if f = "" then "Isabelle." ^ b - else "(" ^ f ^ " Isabelle." ^ b ^ ")"; - in ((binding, value), names') end); - - val (decls, body) = - fold_map expand ants ML_Syntax.reserved - |> #1 |> split_list |> pairself implode; - in (isabelle_struct decls, body) end); - -fun eval name verbose txt = use_text name Output.ml_output verbose txt; - -in - -val eval_antiquotes_fn = ref eval_antiquotes; - -val trace = ref false; - -fun eval_wrapper name verbose txt = - let - val (txt1, txt2) = ! eval_antiquotes_fn txt; - val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else (); - in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end; - -end; - - -(* ML evaluation *) - -fun use_mltext txt verbose opt_context = - setmp opt_context (fn () => eval_wrapper "ML" verbose txt) (); - -fun use_mltext_update txt verbose context = - #2 (pass_context context (eval_wrapper "ML" verbose) txt); - -fun use_context txt = use_mltext_update - ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false; - -fun use_let bind body txt = - use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); - -fun use path = eval_wrapper (Path.implode path) true (File.read path); - - -(* basic antiquotations *) - -val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); - -val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); -val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); -val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); - -val _ = value_antiq "ctyp" (Args.typ >> (fn T => - ("ctyp", - "Thm.ctyp_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)))); - -val _ = value_antiq "cterm" (Args.term >> (fn t => - ("cterm", - "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); - -val _ = value_antiq "cprop" (Args.prop >> (fn t => - ("cprop", - "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); - - -fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) => - #1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c)) - |> syn ? ProofContext.const_syntax_name ctxt - |> ML_Syntax.print_string); - -val _ = inline_antiq "const_name" (const false); -val _ = inline_antiq "const_syntax" (const true); - - - -(** fact references **) - -fun thm name = ProofContext.get_thm (the_local_context ()) (Name name); -fun thms name = ProofContext.get_thms (the_local_context ()) (Name name); - - -local - -fun print_interval (FromTo arg) = - "PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg - | print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i - | print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i; - -fun thm_sel name = - Args.thm_sel >> (fn is => "PureThy.NameSelection " ^ - ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is)) - || Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name); - -fun thm_antiq kind = value_antiq kind - (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel => - "ProofContext.get_" ^ kind ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel)); - -in - -val _ = add_keywords ["(", ")", "-", ","]; -val _ = thm_antiq "thm"; -val _ = thm_antiq "thms"; - -end; - -val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> - (fn ns => ("cpat", - "((cterm_of (ML_Context.the_context ())) o Library.the_single o " ^ - "(ProofContext.read_term_pats TypeInfer.logicT (ML_Context.the_local_context ())))" - ^ (ML_Syntax.print_list ML_Syntax.print_string [ns]), ""))); - -(*final declarations of this structure!*) -nonfix >>; -fun >> f = change_theory f; - -end; - -structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; -open Basic_ML_Context;