--- 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;
--- 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
--- 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";
--- /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;
--- /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;
--- 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";
--- 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;