--- a/src/HOL/Tools/list_code.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/HOL/Tools/list_code.ML Tue Aug 31 13:29:38 2010 +0200
@@ -46,7 +46,7 @@
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
| NONE =>
default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_syntax_const target @{const_name Cons}
+ in Code_Target.add_const_syntax target @{const_name Cons}
(SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
end
--- a/src/HOL/Tools/numeral.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/HOL/Tools/numeral.ML Tue Aug 31 13:29:38 2010 +0200
@@ -76,7 +76,7 @@
fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
(Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
in
- thy |> Code_Target.add_syntax_const target number_of
+ thy |> Code_Target.add_const_syntax target number_of
(SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
@{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
end;
--- a/src/HOL/Tools/string_code.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/HOL/Tools/string_code.ML Tue Aug 31 13:29:38 2010 +0200
@@ -59,7 +59,7 @@
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
| NONE =>
List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_syntax_const target
+ in Code_Target.add_const_syntax target
@{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
end;
@@ -69,7 +69,7 @@
case decode_char nibbles' (t1, t2)
of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
| NONE => Code_Printer.eqn_error thm "Illegal character expression";
- in Code_Target.add_syntax_const target
+ in Code_Target.add_const_syntax target
@{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
end;
@@ -82,7 +82,7 @@
of SOME p => p
| NONE => Code_Printer.eqn_error thm "Illegal message expression")
| NONE => Code_Printer.eqn_error thm "Illegal message expression";
- in Code_Target.add_syntax_const target
+ in Code_Target.add_const_syntax target
@{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
end;
--- a/src/HOL/ex/Numeral.thy Tue Aug 31 13:15:35 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Tue Aug 31 13:29:38 2010 +0200
@@ -989,7 +989,7 @@
in dest_num end;
fun pretty sgn literals [one', dig0', dig1'] _ thm _ _ [(t, _)] =
(Code_Printer.str o print literals o sgn o dest_num one' dig0' dig1' thm) t
- fun add_syntax (c, sgn) = Code_Target.add_syntax_const target c
+ fun add_syntax (c, sgn) = Code_Target.add_const_syntax target c
(SOME (Code_Printer.complex_const_syntax
(1, ([@{const_name One}, @{const_name Dig0}, @{const_name Dig1}],
pretty sgn))));
--- a/src/Tools/Code/code_eval.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Tue Aug 31 13:29:38 2010 +0200
@@ -143,7 +143,7 @@
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
in
thy
- |> Code_Target.add_syntax_tyco target tyco (SOME (k, pr))
+ |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
end;
fun add_eval_constr (const, const') thy =
@@ -153,10 +153,10 @@
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
in
thy
- |> Code_Target.add_syntax_const target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
+ |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
end;
-fun add_eval_const (const, const') = Code_Target.add_syntax_const target
+fun add_eval_const (const, const') = Code_Target.add_const_syntax target
const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
--- a/src/Tools/Code/code_haskell.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Tue Aug 31 13:29:38 2010 +0200
@@ -24,11 +24,11 @@
(** Haskell serializer **)
-fun print_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
+fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
reserved deresolve contr_classparam_typs deriving_show =
let
val deresolve_base = Long_Name.base_name o deresolve;
- fun class_name class = case syntax_class class
+ fun class_name class = case class_syntax class
of NONE => deresolve class
| SOME class => class;
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
@@ -43,7 +43,7 @@
(map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
fun print_tyco_expr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
- and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
+ and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
| SOME (i, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
@@ -72,7 +72,7 @@
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
| print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
then print_case tyvars some_thm vars fxy cases
else print_app tyvars some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
@@ -90,7 +90,7 @@
(str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
end
- and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
+ and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -133,7 +133,7 @@
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts
+ (is_none o const_syntax) deresolve consts
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
@@ -218,7 +218,7 @@
| print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun requires_args classparam = case syntax_const classparam
+ fun requires_args classparam = case const_syntax classparam
of NONE => 0
| SOME (Code_Printer.Plain_const_syntax _) => 0
| SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
@@ -234,7 +234,7 @@
val (c, (_, tys)) = const;
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
- val s = if (is_some o syntax_const) c
+ val s = if (is_some o const_syntax) c
then NONE else (SOME o Long_Name.base_name o deresolve) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
@@ -315,7 +315,7 @@
fun serialize_haskell module_prefix module_name string_classes labelled_name
raw_reserved includes module_alias
- syntax_class syntax_tyco syntax_const program
+ class_syntax tyco_syntax const_syntax program
(stmt_names, presentation_stmt_names) =
let
val reserved = fold (insert (op =) o fst) includes raw_reserved;
@@ -337,7 +337,7 @@
in deriv [] tyco end;
val reserved = make_vars reserved;
fun print_stmt qualified = print_haskell_stmt labelled_name
- syntax_class syntax_tyco syntax_const reserved
+ class_syntax tyco_syntax const_syntax reserved
(if qualified then deresolver else Long_Name.base_name o deresolver)
contr_classparam_typs
(if string_classes then deriving_show else K false);
@@ -458,7 +458,7 @@
val c_bind = Code.read_const thy raw_c_bind;
in if target = target' then
thy
- |> Code_Target.add_syntax_const target c_bind
+ |> Code_Target.add_const_syntax target c_bind
(SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
else error "Only Haskell target allows for monad syntax" end;
@@ -483,7 +483,7 @@
check = { env_var = "EXEC_GHC", make_destination = I,
make_command = fn ghc => fn module_name =>
ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
- #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+ #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
--- a/src/Tools/Code/code_ml.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Tue Aug 31 13:29:38 2010 +0200
@@ -59,14 +59,14 @@
(** SML serializer **)
-fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
+fun print_sml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
let
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
| print_tyco_expr fxy (tyco, [ty]) =
concat [print_typ BR ty, (str o deresolve) tyco]
| print_tyco_expr fxy (tyco, tys) =
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
- and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
+ and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr fxy (tyco, tys)
| SOME (i, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
@@ -114,7 +114,7 @@
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
| print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
@@ -131,7 +131,7 @@
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
- (print_term is_pseudo_fun) syntax_const some_thm vars
+ (print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -190,7 +190,7 @@
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts
+ (is_none o const_syntax) deresolve consts
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
val prolog = if needs_typ then
@@ -365,14 +365,14 @@
(** OCaml serializer **)
-fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
+fun print_ocaml_stmt labelled_name tyco_syntax const_syntax reserved is_cons deresolve =
let
fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
| print_tyco_expr fxy (tyco, [ty]) =
concat [print_typ BR ty, (str o deresolve) tyco]
| print_tyco_expr fxy (tyco, tys) =
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
- and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
+ and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr fxy (tyco, tys)
| SOME (i, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
@@ -412,7 +412,7 @@
in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
| print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
@@ -429,7 +429,7 @@
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
- (print_term is_pseudo_fun) syntax_const some_thm vars
+ (print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -495,7 +495,7 @@
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts
+ (is_none o const_syntax) deresolve consts
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in
@@ -521,7 +521,7 @@
val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
val vars = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts;
+ (is_none o const_syntax) deresolve consts;
val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
in
Pretty.block (
@@ -903,7 +903,7 @@
in (deresolver, nodes) end;
fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
- reserved includes module_alias _ syntax_tyco syntax_const program
+ reserved includes module_alias _ tyco_syntax const_syntax program
(stmt_names, presentation_stmt_names) =
let
val is_cons = Code_Thingol.is_cons program;
@@ -916,7 +916,7 @@
| print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
(null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
then NONE
- else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt)
+ else SOME (print_stmt labelled_name tyco_syntax const_syntax reserved is_cons (deresolver prefix) stmt)
| print_node prefix (Module (module_name, (_, nodes))) =
let
val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
@@ -960,13 +960,13 @@
(target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
- #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+ #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
)))
- #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+ #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
--- a/src/Tools/Code/code_printer.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Aug 31 13:29:38 2010 +0200
@@ -284,8 +284,8 @@
fold_map (Code_Thingol.ensure_declared_const thy) cs naming
|-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
-fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
- case syntax_const c
+fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
+ case const_syntax c
of NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
| SOME (Complex_const_syntax (k, print)) =>
--- a/src/Tools/Code/code_scala.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Tue Aug 31 13:29:38 2010 +0200
@@ -24,14 +24,14 @@
(** Scala serializer **)
-fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
+fun print_scala_stmt labelled_name tyco_syntax const_syntax reserved
args_num is_singleton_constr (deresolve, deresolve_full) =
let
fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
(print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
- and print_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
+ and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr tyvars fxy (tyco, tys)
| SOME (i, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
@@ -67,7 +67,7 @@
end
| print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
then print_case tyvars some_thm vars fxy cases
else print_app tyvars is_pat some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
@@ -76,8 +76,8 @@
let
val k = length ts;
val arg_typs' = if is_pat orelse
- (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
- val (l, print') = case syntax_const c
+ (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
+ val (l, print') = case const_syntax c
of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
@@ -156,7 +156,7 @@
fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
val tyvars = reserved
|> intro_base_names
- (is_none o syntax_tyco) deresolve tycos
+ (is_none o tyco_syntax) deresolve tycos
|> intro_tyvars vs;
val simple = case eqs
of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
@@ -165,7 +165,7 @@
(map (snd o fst) eqs) [];
val vars1 = reserved
|> intro_base_names
- (is_none o syntax_const) deresolve consts
+ (is_none o const_syntax) deresolve consts
val params = if simple
then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
else aux_params vars1 (map (fst o fst) eqs);
@@ -414,7 +414,7 @@
in (deresolver, sca_program) end;
fun serialize_scala labelled_name raw_reserved includes module_alias
- _ syntax_tyco syntax_const
+ _ tyco_syntax const_syntax
program (stmt_names, presentation_stmt_names) =
let
@@ -440,7 +440,7 @@
fun is_singleton_constr c = case Graph.get_node program c
of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
- val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
+ val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
(make_vars reserved) args_num is_singleton_constr;
(* print nodes *)
@@ -524,7 +524,7 @@
make_command = fn scala_home => fn _ =>
"export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
- #> Code_Target.add_syntax_tyco target "fun"
+ #> Code_Target.add_tyco_syntax target "fun"
(SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ BR ty1 (*product type vs. tupled arguments!*),
--- a/src/Tools/Code/code_target.ML Tue Aug 31 13:15:35 2010 +0200
+++ b/src/Tools/Code/code_target.ML Tue Aug 31 13:29:38 2010 +0200
@@ -45,10 +45,10 @@
val allow_abort: string -> theory -> theory
type tyco_syntax = Code_Printer.tyco_syntax
type const_syntax = Code_Printer.const_syntax
- val add_syntax_class: string -> class -> string option -> theory -> theory
- val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
- val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
- val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
+ val add_class_syntax: string -> class -> string option -> theory -> theory
+ val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
+ val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
+ val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
val add_reserved: string -> string -> theory -> theory
val add_include: string -> string * (string * string list) option -> theory -> theory
end;
@@ -63,7 +63,7 @@
type const_syntax = Code_Printer.const_syntax;
-(** basics **)
+(** abstract nonsense **)
datatype destination = File of Path.T option | String of string list;
type serialization = destination -> (string * string option list) option;
@@ -80,21 +80,21 @@
(** theory data **)
-datatype name_syntax_table = NameSyntaxTable of {
+datatype symbol_syntax_data = Symbol_Syntax_Data of {
class: string Symtab.table,
instance: unit Symreltab.table,
tyco: Code_Printer.tyco_syntax Symtab.table,
const: Code_Printer.const_syntax Symtab.table
};
-fun mk_name_syntax_table ((class, instance), (tyco, const)) =
- NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
-fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
- mk_name_syntax_table (f ((class, instance), (tyco, const)));
-fun merge_name_syntax_table
- (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
- NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
- mk_name_syntax_table (
+fun make_symbol_syntax_data ((class, instance), (tyco, const)) =
+ Symbol_Syntax_Data { class = class, instance = instance, tyco = tyco, const = const };
+fun map_symbol_syntax_data f (Symbol_Syntax_Data { class, instance, tyco, const }) =
+ make_symbol_syntax_data (f ((class, instance), (tyco, const)));
+fun merge_symbol_syntax_data
+ (Symbol_Syntax_Data { class = class1, instance = instance1, tyco = tyco1, const = const1 },
+ Symbol_Syntax_Data { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
+ make_symbol_syntax_data (
(Symtab.join (K snd) (class1, class2),
Symreltab.join (K snd) (instance1, instance2)),
(Symtab.join (K snd) (tyco1, tyco2),
@@ -128,25 +128,25 @@
description: description,
reserved: string list,
includes: (Pretty.T * string list) Symtab.table,
- name_syntax_table: name_syntax_table,
+ symbol_syntax_data: symbol_syntax_data,
module_alias: string Symtab.table
};
-fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))) =
+fun make_target ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))) =
Target { serial = serial, description = description, reserved = reserved,
- includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
-fun map_target f ( Target { serial, description, reserved, includes, name_syntax_table, module_alias } ) =
- make_target (f ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))));
+ includes = includes, symbol_syntax_data = symbol_syntax_data, module_alias = module_alias };
+fun map_target f ( Target { serial, description, reserved, includes, symbol_syntax_data, module_alias } ) =
+ make_target (f ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))));
fun merge_target strict target (Target { serial = serial1, description = description,
reserved = reserved1, includes = includes1,
- name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
+ symbol_syntax_data = symbol_syntax_data1, module_alias = module_alias1 },
Target { serial = serial2, description = _,
reserved = reserved2, includes = includes2,
- name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
+ symbol_syntax_data = symbol_syntax_data2, module_alias = module_alias2 }) =
if serial1 = serial2 orelse not strict then
make_target ((serial1, description),
((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
- (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
+ (merge_symbol_syntax_data (symbol_syntax_data1, symbol_syntax_data2),
Symtab.join (K snd) (module_alias1, module_alias2))
))
else
@@ -155,7 +155,7 @@
fun the_description (Target { description, ... }) = description;
fun the_reserved (Target { reserved, ... }) = reserved;
fun the_includes (Target { includes, ... }) = includes;
-fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
+fun the_symbol_syntax_data (Target { symbol_syntax_data = Symbol_Syntax_Data x, ... }) = x;
fun the_module_alias (Target { module_alias , ... }) = module_alias;
structure Targets = Theory_Data
@@ -194,7 +194,7 @@
thy
|> (Targets.map o apfst o apfst o Symtab.update)
(target, make_target ((serial (), seri), (([], Symtab.empty),
- (mk_name_syntax_table ((Symtab.empty, Symreltab.empty),
+ (make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
(Symtab.empty, Symtab.empty)), Symtab.empty))))
end;
@@ -215,7 +215,7 @@
fun map_includes target =
map_target_data target o apsnd o apfst o apsnd;
fun map_name_syntax target =
- map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
+ map_target_data target o apsnd o apsnd o apfst o map_symbol_syntax_data;
fun map_module_alias target =
map_target_data target o apsnd o apsnd o apsnd;
@@ -315,7 +315,7 @@
fun includes names_all = map_filter (select_include names_all)
((Symtab.dest o the_includes) data);
val module_alias = the_module_alias data
- val { class, instance, tyco, const } = the_name_syntax data;
+ val { class, instance, tyco, const } = the_symbol_syntax_data data;
val literals = the_literals thy target;
val width = the_default default_width some_width;
in
@@ -437,19 +437,19 @@
| NONE => del x;
in (map_name_syntax target o mapp) change thy end;
-fun gen_add_syntax_class prep_class =
+fun gen_add_class_syntax prep_class =
gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);
-fun gen_add_syntax_inst prep_inst =
+fun gen_add_instance_syntax prep_inst =
gen_add_syntax (apfst o apsnd, Symreltab.update, Symreltab.delete_safe) prep_inst ((K o K) I);
-fun gen_add_syntax_tyco prep_tyco =
+fun gen_add_tyco_syntax prep_tyco =
gen_add_syntax (apsnd o apfst, Symtab.update, Symtab.delete_safe) prep_tyco
(fn thy => fn tyco => fn syn => if fst syn <> Sign.arity_number thy tyco
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syn);
-fun gen_add_syntax_const prep_const =
+fun gen_add_const_syntax prep_const =
gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
(fn thy => fn c => fn syn =>
if Code_Printer.requires_args syn > Code.args_number thy c
@@ -513,18 +513,18 @@
in
-val add_syntax_class = gen_add_syntax_class cert_class;
-val add_syntax_inst = gen_add_syntax_inst cert_inst;
-val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const = gen_add_syntax_const (K I);
+val add_class_syntax = gen_add_class_syntax cert_class;
+val add_instance_syntax = gen_add_instance_syntax cert_inst;
+val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
+val add_const_syntax = gen_add_const_syntax (K I);
val allow_abort = gen_allow_abort (K I);
val add_reserved = add_reserved;
val add_include = add_include;
-val add_syntax_class_cmd = gen_add_syntax_class read_class;
-val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
-val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
+val add_class_syntax_cmd = gen_add_class_syntax read_class;
+val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
+val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
+val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
val allow_abort_cmd = gen_allow_abort Code.read_const;
fun parse_args f args =
@@ -554,23 +554,23 @@
val _ =
Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
process_multi_syntax Parse.xname (Scan.option Parse.string)
- add_syntax_class_cmd);
+ add_class_syntax_cmd);
val _ =
Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
(Scan.option (Parse.minus >> K ()))
- add_syntax_inst_cmd);
+ add_instance_syntax_cmd);
val _ =
Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
- add_syntax_tyco_cmd);
+ add_tyco_syntax_cmd);
val _ =
Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
- add_syntax_const_cmd);
+ add_const_syntax_cmd);
val _ =
Outer_Syntax.command "code_reserved" "declare words as reserved for target language"