# HG changeset patch # User haftmann # Date 1283254178 -7200 # Node ID 79d7f2b4cf713ca8321845f65987f3101d293488 # Parent ec2a8efd8990cea6162b2f089ef4e3701cf48704 more coherent naming of syntax data structures diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/HOL/Tools/list_code.ML --- 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 diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/HOL/Tools/numeral.ML --- 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; diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/HOL/Tools/string_code.ML --- 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; diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/HOL/ex/Numeral.thy --- 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)))); diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/Tools/Code/code_eval.ML --- 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 = diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/Tools/Code/code_haskell.ML --- 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 "->", diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/Tools/Code/code_ml.ML --- 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 "->", diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/Tools/Code/code_printer.ML --- 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)) => diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/Tools/Code/code_scala.ML --- 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!*), diff -r ec2a8efd8990 -r 79d7f2b4cf71 src/Tools/Code/code_target.ML --- 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"