--- a/src/Tools/Code/code_haskell.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML Sat Jan 25 23:50:49 2014 +0100
@@ -25,6 +25,7 @@
val language_params =
space_implode " " (map (prefix "-X") language_extensions);
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
open Code_Printer;
@@ -37,9 +38,9 @@
fun print_haskell_stmt class_syntax tyco_syntax const_syntax
reserved deresolve deriving_show =
let
- val deresolve_const = deresolve o Code_Symbol.Constant;
- val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
- val deresolve_class = deresolve o Code_Symbol.Type_Class;
+ val deresolve_const = deresolve o Constant;
+ val deresolve_tyco = deresolve o Type_Constructor;
+ val deresolve_class = deresolve o Type_Class;
fun class_name class = case class_syntax class
of NONE => deresolve_class class
| SOME class => class;
@@ -84,7 +85,7 @@
in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
| print_term tyvars some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+ of SOME (app as ({ sym = Constant const, ... }, _)) =>
if is_none (const_syntax const)
then print_case tyvars some_thm vars fxy case_expr
else print_app tyvars some_thm vars fxy app
@@ -126,7 +127,7 @@
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
(map print_select clauses)
end;
- fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
+ fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_err n =
@@ -163,7 +164,7 @@
| eqs => map print_eqn eqs)
)
end
- | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
+ | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
let
val tyvars = intro_vars vs reserved;
in
@@ -172,7 +173,7 @@
print_typdecl tyvars (deresolve_tyco tyco, vs)
]
end
- | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
+ | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
let
val tyvars = intro_vars vs reserved;
in
@@ -185,7 +186,7 @@
:: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
+ | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
let
val tyvars = intro_vars vs reserved;
fun print_co ((co, _), tys) =
@@ -203,7 +204,7 @@
@ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
+ | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
let
val tyvars = intro_vars [v] reserved;
fun print_classparam (classparam, ty) =
@@ -239,14 +240,14 @@
]
| SOME k =>
let
- val { sym = Code_Symbol.Constant c, dom, range, ... } = const;
+ val { sym = Constant c, dom, range, ... } = const;
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
val s = if (is_some o const_syntax) c
then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
- val lhs = IConst { sym = Code_Symbol.Constant classparam, typargs = [],
+ val lhs = IConst { sym = Constant classparam, typargs = [],
dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
(*dictionaries are not relevant at this late stage,
and these consts never need type annotations for disambiguation *)
@@ -340,7 +341,7 @@
let
fun deriv _ "fun" = false
| deriv tycos tyco = member (op =) tycos tyco
- orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco)
+ orelse case try (Code_Symbol.Graph.get_node program) (Type_Constructor tyco)
of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
(maps snd cs)
| NONE => true
@@ -432,7 +433,7 @@
of SOME ((pat, ty), t') =>
SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
- fun dest_monad (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
+ fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) =
if c = c_bind then dest_bind t1 t2
else NONE
| dest_monad t = case Code_Thingol.split_let t
@@ -467,7 +468,7 @@
in
if target = target' then
thy
- |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
+ |> Code_Target.set_printings (Constant (c_bind, [(target,
SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
else error "Only Haskell target allows for monad syntax"
end;
@@ -487,7 +488,7 @@
make_command = fn module_name =>
"\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^
module_name ^ ".hs" } })
- #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ #> Code_Target.set_printings (Type_Constructor ("fun",
[(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/code_ml.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_ml.ML Sat Jan 25 23:50:49 2014 +0100
@@ -14,6 +14,7 @@
structure Code_ML : CODE_ML =
struct
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
open Code_Printer;
@@ -36,7 +37,7 @@
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
| ML_Val of ml_binding
- | ML_Funs of ml_binding list * Code_Symbol.symbol list
+ | ML_Funs of ml_binding list * Code_Symbol.T list
| ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
| ML_Class of string * (vname * ((class * class) list * (string * itype) list));
@@ -53,21 +54,21 @@
fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
- val deresolve_const = deresolve o Code_Symbol.Constant;
- val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
- val deresolve_class = deresolve o Code_Symbol.Type_Class;
- val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
- val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
+ val deresolve_const = deresolve o Constant;
+ val deresolve_tyco = deresolve o Type_Constructor;
+ val deresolve_class = deresolve o Type_Class;
+ val deresolve_classrel = deresolve o Class_Relation;
+ val deresolve_inst = deresolve o Class_Instance;
fun print_tyco_expr (sym, []) = (str o deresolve) sym
| print_tyco_expr (sym, [ty]) =
concat [print_typ BR ty, (str o deresolve) sym]
| print_tyco_expr (sym, tys) =
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
+ of NONE => print_tyco_expr (Type_Constructor tyco, tys)
| SOME (_, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
- fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
+ fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
(map_filter (fn (v, sort) =>
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
@@ -81,7 +82,7 @@
print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
((str o deresolve_inst) inst ::
- (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+ (if is_pseudo_fun (Class_Instance inst) then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
[str (if k = 1 then first_upper v ^ "_"
@@ -110,7 +111,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 case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+ of SOME (app as ({ sym = Constant const, ... }, _)) =>
if is_none (const_syntax const)
then print_case is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
@@ -174,7 +175,7 @@
in
concat (
str definer
- :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
+ :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
@@ -195,7 +196,7 @@
in
concat (
prolog
- :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
+ :: (if is_pseudo_fun (Constant const) then [str "()"]
else print_dict_args vs
@ map (print_term is_pseudo_fun some_thm vars BR) ts)
@ str "="
@@ -205,7 +206,7 @@
val shift = if null eqs then I else
map (Pretty.block o single o Pretty.block o single);
in pair
- (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
+ (print_val_decl print_typscheme (Constant const, vs_ty))
((Pretty.block o Pretty.fbreaks o shift) (
print_eqn definer eq
:: map (print_eqn "|") eqs
@@ -228,11 +229,11 @@
];
in pair
(print_val_decl print_dicttypscheme
- (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+ (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
str definer
:: (str o deresolve_inst) inst
- :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+ :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
else print_dict_args vs)
@ str "="
:: enum "," "{" "}"
@@ -243,7 +244,7 @@
))
end;
fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
- [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
+ [print_val_decl print_typscheme (Constant const, vs_ty)]
((semicolon o map str) (
(if n = 0 then "val" else "fun")
:: deresolve_const const
@@ -279,7 +280,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
+ val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -301,7 +302,7 @@
(map str ["val", s, "=", "#" ^ s, ":"] @| p);
fun print_super_class_decl (classrel as (_, super_class)) =
print_val_decl print_dicttypscheme
- (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
+ (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
fun print_super_class_field (classrel as (_, super_class)) =
print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
fun print_super_class_proj (classrel as (_, super_class)) =
@@ -309,7 +310,7 @@
(print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
- (Code_Symbol.Constant classparam, ([(v, [class])], ty));
+ (Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
print_field (deresolve_const classparam) (print_typ NOBR ty);
fun print_classparam_proj (classparam, ty) =
@@ -359,21 +360,21 @@
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
- val deresolve_const = deresolve o Code_Symbol.Constant;
- val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
- val deresolve_class = deresolve o Code_Symbol.Type_Class;
- val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
- val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
+ val deresolve_const = deresolve o Constant;
+ val deresolve_tyco = deresolve o Type_Constructor;
+ val deresolve_class = deresolve o Type_Class;
+ val deresolve_classrel = deresolve o Class_Relation;
+ val deresolve_inst = deresolve o Class_Instance;
fun print_tyco_expr (sym, []) = (str o deresolve) sym
| print_tyco_expr (sym, [ty]) =
concat [print_typ BR ty, (str o deresolve) sym]
| print_tyco_expr (sym, tys) =
concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
+ of NONE => print_tyco_expr (Type_Constructor tyco, tys)
| SOME (_, print) => print print_typ fxy tys)
| print_typ fxy (ITyVar v) = str ("'" ^ v);
- fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
+ fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
(map_filter (fn (v, sort) =>
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
@@ -386,7 +387,7 @@
|> print_classrels classrels
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
brackify BR ((str o deresolve_inst) inst ::
- (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+ (if is_pseudo_fun (Class_Instance inst) then [str "()"]
else map_filter (print_dicts is_pseudo_fun BR) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
str (if k = 1 then "_" ^ first_upper v
@@ -412,7 +413,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 case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+ of SOME (app as ({ sym = Constant const, ... }, _)) =>
if is_none (const_syntax const)
then print_case is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
@@ -471,7 +472,7 @@
in
concat (
str definer
- :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
+ :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
@@ -544,11 +545,11 @@
concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
else (concat o map str) [definer, deresolve_const const];
in pair
- (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
+ (print_val_decl print_typscheme (Constant const, vs_ty))
(concat (
prolog
:: print_dict_args vs
- @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
+ @| print_eqns (is_pseudo_fun (Constant const)) eqs
))
end
| print_def is_pseudo_fun _ definer
@@ -568,11 +569,11 @@
];
in pair
(print_val_decl print_dicttypscheme
- (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+ (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
str definer
:: (str o deresolve_inst) inst
- :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+ :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
else print_dict_args vs)
@ str "="
@@ brackets [
@@ -584,7 +585,7 @@
))
end;
fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
- [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
+ [print_val_decl print_typscheme (Constant const, vs_ty)]
((doublesemicolon o map str) (
"let"
:: deresolve_const const
@@ -619,7 +620,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
+ val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -641,7 +642,7 @@
print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
- (Code_Symbol.Constant classparam, ([(v, [class])], ty));
+ (Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
print_field (deresolve_const classparam) (print_typ NOBR ty);
val w = "_" ^ first_upper v;
@@ -724,7 +725,7 @@
| namify_stmt (Code_Thingol.Classrel _) = namify_const false
| namify_stmt (Code_Thingol.Classparam _) = namify_const false
| namify_stmt (Code_Thingol.Classinst _) = namify_const false;
- fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
+ fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
let
val eqs = filter (snd o snd) raw_eqs;
val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
@@ -734,7 +735,7 @@
| _ => (eqs, NONE)
else (eqs, NONE)
in (ML_Function (const, (tysm, eqs')), some_sym) end
- | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
+ | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
(ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
| ml_binding_of_stmt (sym, _) =
error ("Binding block containing illegal statement: " ^
@@ -755,10 +756,10 @@
(ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
fun modify_datatypes stmts = single (SOME
(ML_Datas (map_filter
- (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
+ (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
fun modify_class stmts = single (SOME
(ML_Class (the_single (map_filter
- (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
+ (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
| modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
@@ -850,7 +851,7 @@
check = { env_var = "ISABELLE_OCAML",
make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
- #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ #> Code_Target.set_printings (Type_Constructor ("fun",
[(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
#> fold (Code_Target.add_reserved target_SML)
--- a/src/Tools/Code/code_namespace.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_namespace.ML Sat Jan 25 23:50:49 2014 +0100
@@ -13,7 +13,7 @@
namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
-> Code_Thingol.program
- -> { deresolver: string -> Code_Symbol.symbol -> string,
+ -> { deresolver: string -> Code_Symbol.T -> string,
flat_program: flat_program }
datatype ('a, 'b) node =
@@ -26,13 +26,13 @@
reserved: Name.context, identifiers: Code_Target.identifier_data,
empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
- cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.symbol -> 'b -> 'b,
- modify_stmts: (Code_Symbol.symbol * Code_Thingol.stmt) list -> 'a option list }
+ cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
+ modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list }
-> Code_Thingol.program
- -> { deresolver: string list -> Code_Symbol.symbol -> string,
+ -> { deresolver: string list -> Code_Symbol.T -> string,
hierarchical_program: ('a, 'b) hierarchical_program }
val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
- print_stmt: string list -> Code_Symbol.symbol * 'a -> 'c,
+ print_stmt: string list -> Code_Symbol.T * 'a -> 'c,
lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
-> ('a, 'b) hierarchical_program -> 'c list
end;
@@ -48,7 +48,7 @@
fun force_identifier ctxt fragments_tab force_module identifiers sym =
case lookup_identifier identifiers sym of
- NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.namespace_prefix ctxt) sym, Code_Symbol.base_name sym)
+ NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
| SOME prefix_name => if null force_module then prefix_name
else (force_module, snd prefix_name);
@@ -57,7 +57,7 @@
fun alias_fragments name = case module_identifiers name
of SOME name' => Long_Name.explode name'
| NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
- val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.namespace_prefix ctxt o fst) program [];
+ val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
in
fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
module_names Symtab.empty
@@ -66,7 +66,7 @@
(** flat program structure **)
-type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.symbol list) list) Graph.T;
+type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
fun flat_program ctxt { module_prefix, module_name, reserved,
identifiers, empty_nsp, namify_stmt, modify_stmt } program =
--- a/src/Tools/Code/code_printer.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_printer.ML Sat Jan 25 23:50:49 2014 +0100
@@ -25,8 +25,8 @@
val semicolon: Pretty.T list -> Pretty.T
val doublesemicolon: Pretty.T list -> Pretty.T
val indent: int -> Pretty.T -> Pretty.T
- val markup_stmt: Code_Symbol.symbol -> Pretty.T -> Pretty.T
- val format: Code_Symbol.symbol list -> int -> Pretty.T -> string
+ val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
+ val format: Code_Symbol.T list -> int -> Pretty.T -> string
val first_upper: string -> string
val first_lower: string -> string
@@ -36,7 +36,7 @@
val lookup_var: var_ctxt -> string -> string
val intro_base_names: (string -> bool) -> (string -> string)
-> string list -> var_ctxt -> var_ctxt
- val intro_base_names_for: (string -> bool) -> (Code_Symbol.symbol -> string)
+ val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string)
-> iterm list -> var_ctxt -> var_ctxt
val aux_params: var_ctxt -> iterm list list -> string list
@@ -94,6 +94,7 @@
structure Code_Printer : CODE_PRINTER =
struct
+open Basic_Code_Symbol;
open Code_Thingol;
(** generic nonsense *)
@@ -200,7 +201,7 @@
fun intro_base_names_for no_syntax deresolve ts =
[]
|> fold Code_Thingol.add_constsyms ts
- |> intro_base_names (fn Code_Symbol.Constant const => no_syntax const | _ => true) deresolve;
+ |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve;
(** pretty literals **)
@@ -313,7 +314,7 @@
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
(app as ({ sym, dom, ... }, ts)) =
case sym of
- Code_Symbol.Constant const => (case const_syntax const of
+ Constant const => (case const_syntax const 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)
--- a/src/Tools/Code/code_runtime.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML Sat Jan 25 23:50:49 2014 +0100
@@ -36,6 +36,7 @@
structure Code_Runtime : CODE_RUNTIME =
struct
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
(** evaluation **)
@@ -53,9 +54,9 @@
val _ = Theory.setup
(Code_Target.extend_target (target, (Code_ML.target_SML, I))
- #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
+ #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
[(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
- #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
+ #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},
[(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
#> Code_Target.add_reserved target this
#> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
@@ -92,7 +93,7 @@
|> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
fun obtain_evaluator' thy some_target program =
- obtain_evaluator thy some_target program o map Code_Symbol.Constant;
+ obtain_evaluator thy some_target program o map Constant;
fun evaluation cookie thy evaluator vs_t args =
let
@@ -198,7 +199,7 @@
val program = Code_Thingol.consts_program thy false consts;
val (ml_modules, target_names) =
Code_Target.produce_code_for thy
- target NONE module_name [] program (map Code_Symbol.Constant consts @ map Code_Symbol.Type_Constructor tycos);
+ target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);
val ml_code = space_implode "\n\n" (map snd ml_modules);
val (consts', tycos') = chop (length consts) target_names;
val consts_map = map2 (fn const =>
@@ -292,7 +293,7 @@
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
in
thy
- |> Code_Target.set_printings (Code_Symbol.Type_Constructor (tyco, [(target, SOME (k, pr))]))
+ |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))]))
end;
fun add_eval_constr (const, const') thy =
@@ -302,11 +303,11 @@
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
in
thy
- |> Code_Target.set_printings (Code_Symbol.Constant (const,
+ |> Code_Target.set_printings (Constant (const,
[(target, SOME (Code_Printer.simple_const_syntax (k, pr)))]))
end;
-fun add_eval_const (const, const') = Code_Target.set_printings (Code_Symbol.Constant
+fun add_eval_const (const, const') = Code_Target.set_printings (Constant
(const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))]));
fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
@@ -437,7 +438,7 @@
|> Code_Target.add_reserved target ml_name
|> Specification.axiomatization [(b, SOME T, NoSyn)] []
|-> (fn ([Const (const, _)], _) =>
- Code_Target.set_printings (Code_Symbol.Constant (const,
+ Code_Target.set_printings (Constant (const,
[(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
#> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
--- a/src/Tools/Code/code_scala.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_scala.ML Sat Jan 25 23:50:49 2014 +0100
@@ -15,6 +15,7 @@
val target = "Scala";
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
open Code_Printer;
@@ -27,18 +28,18 @@
fun print_scala_stmt tyco_syntax const_syntax reserved
args_num is_constr (deresolve, deresolve_full) =
let
- val deresolve_const = deresolve o Code_Symbol.Constant;
- val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
- val deresolve_class = deresolve o Code_Symbol.Type_Class;
+ val deresolve_const = deresolve o Constant;
+ val deresolve_tyco = deresolve o Type_Constructor;
+ val deresolve_class = deresolve o Type_Class;
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 (sym, tys) = applify "[" "]"
(print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr tyvars fxy (Code_Symbol.Type_Constructor tyco, tys)
+ of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys)
| SOME (_, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
- fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Code_Symbol.Type_Class class, [ty]);
+ fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]);
fun print_tupled_typ tyvars ([], ty) =
print_typ tyvars NOBR ty
| print_tupled_typ tyvars ([ty1], ty2) =
@@ -70,7 +71,7 @@
end
| print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
- of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+ of SOME (app as ({ sym = Constant const, ... }, _)) =>
if is_none (const_syntax const)
then print_case tyvars some_thm vars fxy case_expr
else print_app tyvars is_pat some_thm vars fxy app
@@ -81,7 +82,7 @@
val k = length ts;
val typargs' = if is_pat then [] else typargs;
val syntax = case sym of
- Code_Symbol.Constant const => const_syntax const
+ Constant const => const_syntax const
| _ => NONE;
val (l, print') = case syntax of
NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")"
@@ -151,7 +152,7 @@
fun print_defhead tyvars vars const vs params tys ty =
Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
- NOBR (print_context tyvars vs (Code_Symbol.Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
+ NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
str " ="];
fun print_def const (vs, ty) [] =
let
@@ -204,10 +205,10 @@
str "match", str "{"], str "}")
(map print_clause eqs)
end;
- val print_method = str o Library.enclose "`" "`" o deresolve_full o Code_Symbol.Constant;
- fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
+ val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
+ fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
print_def const (vs, ty) (filter (snd o snd) raw_eqs)
- | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
+ | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
let
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, vs_args), tys) =
@@ -224,7 +225,7 @@
NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
:: map print_co cos)
end
- | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
+ | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
let
val tyvars = intro_tyvars [(v, [class])] reserved;
fun add_typarg s = Pretty.block
@@ -349,12 +350,12 @@
scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
(* print statements *)
- fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Constructor tyco)
+ fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)
of Code_Thingol.Datatype (_, constrs) =>
the (AList.lookup (op = o apsnd fst) constrs constr);
- fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Class class)
+ fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class)
of Code_Thingol.Class (_, (_, classparams)) => classparams;
- fun args_num (sym as Code_Symbol.Constant const) = case Code_Symbol.Graph.get_node program sym
+ fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym
of Code_Thingol.Fun (((_, ty), []), _) =>
(length o fst o Code_Thingol.unfold_fun) ty
| Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
@@ -422,7 +423,7 @@
make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn _ =>
"env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
- #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ #> Code_Target.set_printings (Type_Constructor ("fun",
[(target, 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_symbol.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_symbol.ML Sat Jan 25 23:50:49 2014 +0100
@@ -5,20 +5,25 @@
class relations, class instances, modules.
*)
-signature CODE_SYMBOL =
+signature BASIC_CODE_SYMBOL =
sig
datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c |
Class_Relation of 'd | Class_Instance of 'e | Module of 'f
- type symbol = (string, string, class, class * class, string * class, string) attr
- structure Table: TABLE;
- structure Graph: GRAPH;
- val namespace_prefix: Proof.context -> symbol -> string
- val base_name: symbol -> string
- val quote: Proof.context -> symbol -> string
- val marker: symbol -> string
- val value: symbol
- val is_value: symbol -> bool
+end
+
+signature CODE_SYMBOL =
+sig
+ include BASIC_CODE_SYMBOL
+ type T = (string, string, class, class * class, string * class, string) attr
+ structure Table: TABLE
+ structure Graph: GRAPH
+ val default_base: T -> string
+ val default_prefix: Proof.context -> T -> string
+ val quote: Proof.context -> T -> string
+ val marker: T -> string
+ val value: T
+ val is_value: T -> bool
val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l)
-> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr
val maps_attr: ('a -> 'g list) -> ('b -> 'h list)
@@ -40,8 +45,8 @@
val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option
val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option
val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option
- val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option
- val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> symbol list
+ val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> T -> 'a option
+ val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> T list
val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list
end;
@@ -53,7 +58,7 @@
datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd | Class_Instance of 'e | Module of 'f;
-type symbol = (string, string, class, string * class, class * class, string) attr;
+type T = (string, string, class, string * class, class * class, string) attr;
fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2)
| symbol_ord (Constant _, _) = GREATER
@@ -74,8 +79,24 @@
| symbol_ord (_, Class_Instance _) = LESS
| symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2);
-structure Table = Table(type key = symbol val ord = symbol_ord);
-structure Graph = Graph(type key = symbol val ord = symbol_ord);
+structure Table = Table(type key = T val ord = symbol_ord);
+structure Graph = Graph(type key = T val ord = symbol_ord);
+
+local
+ val base = Name.desymbolize false o Long_Name.base_name;
+ fun base_rel (x, y) = base y ^ "_" ^ base x;
+in
+
+fun default_base (Constant "") = "value"
+ | default_base (Constant "==>") = "follows"
+ | default_base (Constant "==") = "meta_eq"
+ | default_base (Constant c) = base c
+ | default_base (Type_Constructor tyco) = base tyco
+ | default_base (Type_Class class) = base class
+ | default_base (Class_Relation classrel) = base_rel classrel
+ | default_base (Class_Instance inst) = base_rel inst;
+
+end;
local
fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
@@ -94,29 +115,16 @@
| prefix thy (Type_Class class) = thyname_of_class thy class
| prefix thy (Class_Relation (class, _)) = thyname_of_class thy class
| prefix thy (Class_Instance inst) = thyname_of_instance thy inst;
- val base = Name.desymbolize false o Long_Name.base_name;
- fun base_rel (x, y) = base y ^ "_" ^ base x;
in
-fun base_name (Constant "") = "value"
- | base_name (Constant "==>") = "follows"
- | base_name (Constant "==") = "meta_eq"
- | base_name (Constant c) = base c
- | base_name (Type_Constructor tyco) = base tyco
- | base_name (Type_Class class) = base class
- | base_name (Class_Relation classrel) = base_rel classrel
- | base_name (Class_Instance inst) = base_rel inst;
+fun default_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
-fun namespace_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
-
-fun default_name ctxt sym = (namespace_prefix ctxt sym, base_name sym);
+end;
val value = Constant "";
fun is_value (Constant "") = true
| is_value _ = false;
-end;
-
fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
| quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco)
| quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class)
@@ -216,3 +224,6 @@
fun dest_module_data x = (Symtab.dest o #module o dest_data) x;
end;
+
+
+structure Basic_Code_Symbol: BASIC_CODE_SYMBOL = Code_Symbol;
--- a/src/Tools/Code/code_target.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_target.ML Sat Jan 25 23:50:49 2014 +0100
@@ -11,26 +11,26 @@
val read_const_exprs: theory -> string list -> string list
val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
- -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
+ -> Code_Thingol.program -> Code_Symbol.T list -> unit
val produce_code_for: theory -> string -> int option -> string -> Token.T list
- -> Code_Thingol.program -> Code_Symbol.symbol list -> (string * string) list * string option list
+ -> Code_Thingol.program -> Code_Symbol.T list -> (string * string) list * string option list
val present_code_for: theory -> string -> int option -> string -> Token.T list
- -> Code_Thingol.program -> Code_Symbol.symbol list * Code_Symbol.symbol list -> string
+ -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
val check_code_for: theory -> string -> bool -> Token.T list
- -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
+ -> Code_Thingol.program -> Code_Symbol.T list -> unit
val export_code: theory -> string list
-> (((string * string) * Path.T option) * Token.T list) list -> unit
val produce_code: theory -> string list
-> string -> int option -> string -> Token.T list -> (string * string) list * string option list
- val present_code: theory -> string list -> Code_Symbol.symbol list
+ val present_code: theory -> string list -> Code_Symbol.T list
-> string -> int option -> string -> Token.T list -> string
val check_code: theory -> string list
-> ((string * bool) * Token.T list) list -> unit
val generatedN: string
val evaluator: theory -> string -> Code_Thingol.program
- -> Code_Symbol.symbol list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
+ -> Code_Symbol.T list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-> (string * string) list * string
type serializer
@@ -46,7 +46,7 @@
type serialization
val parse_args: 'a parser -> Token.T list -> 'a
val serialization: (int -> Path.T option -> 'a -> unit)
- -> (Code_Symbol.symbol list -> int -> 'a -> (string * string) list * (Code_Symbol.symbol -> string option))
+ -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
-> 'a -> serialization
val set_default_code_width: int -> theory -> theory
@@ -73,6 +73,7 @@
structure Code_Target : CODE_TARGET =
struct
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
type literals = Code_Printer.literals;
@@ -154,8 +155,8 @@
(* serialization: abstract nonsense to cover different destinies for generated code *)
-datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.symbol list;
-type serialization = int -> destination -> ((string * string) list * (Code_Symbol.symbol -> string option)) option;
+datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
+type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
fun serialization output _ content width (Export some_path) =
(output width some_path content; NONE)
@@ -345,7 +346,7 @@
val syms_hidden = Code_Symbol.symbols_of printings;
val (syms_all, program) = project_program thy syms_hidden syms proto_program;
fun select_include (name, (content, cs)) =
- if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs
+ if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
then SOME (name, content) else NONE;
val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
in
@@ -471,7 +472,7 @@
let
val program = Code_Thingol.consts_program thy false cs;
val _ = map (fn (((target, module_name), some_path), args) =>
- export_code_for thy some_path target NONE module_name args program (map Code_Symbol.Constant cs)) seris;
+ export_code_for thy some_path target NONE module_name args program (map Constant cs)) seris;
in () end;
fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
@@ -480,18 +481,18 @@
fun produce_code thy cs target some_width some_module_name args =
let
val program = Code_Thingol.consts_program thy false cs;
- in produce_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs) end;
+ in produce_code_for thy target some_width some_module_name args program (map Constant cs) end;
fun present_code thy cs syms target some_width some_module_name args =
let
val program = Code_Thingol.consts_program thy false cs;
- in present_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs, syms) end;
+ in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
fun check_code thy cs seris =
let
val program = Code_Thingol.consts_program thy false cs;
val _ = map (fn ((target, strict), args) =>
- check_code_for thy target strict args program (map Code_Symbol.Constant cs)) seris;
+ check_code_for thy target strict args program (map Constant cs)) seris;
in () end;
fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
@@ -506,17 +507,17 @@
>> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
val parse_consts = parse_names "consts" Args.term
- Code.check_const Code_Symbol.Constant;
+ Code.check_const Constant;
val parse_types = parse_names "types" (Scan.lift Args.name)
- Sign.intern_type Code_Symbol.Type_Constructor;
+ Sign.intern_type Type_Constructor;
val parse_classes = parse_names "classes" (Scan.lift Args.name)
- Sign.intern_class Code_Symbol.Type_Class;
+ Sign.intern_class Type_Class;
val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
(fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
- Code_Symbol.Class_Instance;
+ Class_Instance;
in
@@ -630,19 +631,19 @@
in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end;
fun gen_add_const_syntax prep_const =
- gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax;
+ gen_add_syntax Constant prep_const check_const_syntax;
fun gen_add_tyco_syntax prep_tyco =
- gen_add_syntax Code_Symbol.Type_Constructor prep_tyco check_tyco_syntax;
+ gen_add_syntax Type_Constructor prep_tyco check_tyco_syntax;
fun gen_add_class_syntax prep_class =
- gen_add_syntax Code_Symbol.Type_Class prep_class ((K o K o K) I);
+ gen_add_syntax Type_Class prep_class ((K o K o K) I);
fun gen_add_instance_syntax prep_inst =
- gen_add_syntax Code_Symbol.Class_Instance prep_inst ((K o K o K) I);
+ gen_add_syntax Class_Instance prep_inst ((K o K o K) I);
fun gen_add_include prep_const target (name, some_content) thy =
- gen_add_syntax Code_Symbol.Module (K I)
+ gen_add_syntax Module (K I)
(fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
target name some_content thy;
@@ -693,15 +694,15 @@
fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const
- >> Code_Symbol.Constant
+ >> Constant
|| parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
- >> Code_Symbol.Type_Constructor
+ >> Type_Constructor
|| parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class
- >> Code_Symbol.Type_Class
+ >> Type_Class
|| parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
- >> Code_Symbol.Class_Relation
+ >> Class_Relation
|| parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst
- >> Code_Symbol.Class_Instance
+ >> Class_Instance
|| parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module
>> Code_Symbol.Module;
--- a/src/Tools/Code/code_thingol.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML Sat Jan 25 23:50:49 2014 +0100
@@ -23,7 +23,7 @@
datatype itype =
`%% of string * itype list
| ITyVar of vname;
- type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
+ type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
dom: itype list, range: itype, annotate: bool };
datatype iterm =
IConst of const
@@ -55,7 +55,7 @@
val is_IAbs: iterm -> bool
val eta_expand: int -> const * iterm list -> iterm
val contains_dict_var: iterm -> bool
- val add_constsyms: iterm -> Code_Symbol.symbol list -> Code_Symbol.symbol list
+ val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
val add_tyconames: iterm -> string list -> string list
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
@@ -77,34 +77,36 @@
val implemented_deps: program -> string list
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
- val is_constr: program -> Code_Symbol.symbol -> bool
+ val is_constr: program -> Code_Symbol.T -> bool
val is_case: stmt -> bool
val group_stmts: theory -> program
- -> ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list
- * ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list)) list
+ -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
+ * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
val read_const_exprs: theory -> string list -> string list * string list
val consts_program: theory -> bool -> string list -> program
val dynamic_conv: theory -> (program
- -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
-> conv
val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
- -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
-> term -> 'a
val static_conv: theory -> string list -> (program -> string list
- -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
-> conv
val static_conv_simple: theory -> string list
-> (program -> (string * sort) list -> term -> conv) -> conv
val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
(program -> string list
- -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
-> term -> 'a
end;
structure Code_Thingol: CODE_THINGOL =
struct
+open Basic_Code_Symbol;
+
(** auxiliary **)
fun unfoldl dest x =
@@ -147,7 +149,7 @@
val ty3 = Library.foldr (op `->) (tys2, ty1);
in (tys3, ty3) end;
-type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
+type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
dom: itype list, range: itype, annotate: bool };
datatype iterm =
@@ -286,12 +288,12 @@
type program = stmt Code_Symbol.Graph.T;
fun unimplemented program =
- Code_Symbol.Graph.fold (fn (Code_Symbol.Constant c, (NoStmt, _)) => cons c | _ => I) program [];
+ Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I) program [];
fun implemented_deps program =
Code_Symbol.Graph.keys program
- |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Code_Symbol.Constant (unimplemented program)))
- |> map_filter (fn Code_Symbol.Constant c => SOME c | _ => NONE);
+ |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program)))
+ |> map_filter (fn Constant c => SOME c | _ => NONE);
fun map_terms_bottom_up f (t as IConst _) = f t
| map_terms_bottom_up f (t as IVar _) = f t
@@ -466,7 +468,7 @@
##>> pair (map (unprefix "'" o fst) vs)
##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
#>> Datatype;
- in ensure_stmt Code_Symbol.Type_Constructor stmt_datatype tyco end
+ in ensure_stmt Type_Constructor stmt_datatype tyco end
and ensure_const thy algbr eqngr permissive c =
let
fun stmt_datatypecons tyco =
@@ -494,7 +496,7 @@
| NONE => (case Axclass.class_of_param thy c
of SOME class => stmt_classparam class
| NONE => stmt_fun (Code_Preproc.cert eqngr c))
- in ensure_stmt Code_Symbol.Constant stmt_const c end
+ in ensure_stmt Constant stmt_const c end
and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
let
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -505,14 +507,14 @@
##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
##>> translate_typ thy algbr eqngr permissive ty) cs
#>> (fn info => Class (unprefix "'" Name.aT, info))
- in ensure_stmt Code_Symbol.Type_Class stmt_class class end
+ in ensure_stmt Type_Class stmt_class class end
and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
let
val stmt_classrel =
ensure_class thy algbr eqngr permissive sub_class
##>> ensure_class thy algbr eqngr permissive super_class
#>> Classrel;
- in ensure_stmt Code_Symbol.Class_Relation stmt_classrel (sub_class, super_class) end
+ in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end
and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) =
let
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -552,7 +554,7 @@
#>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
Classinst { class = class, tyco = tyco, vs = vs,
superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
- in ensure_stmt Code_Symbol.Class_Instance stmt_inst (tyco, class) end
+ in ensure_stmt Class_Instance stmt_inst (tyco, class) end
and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
pair (ITyVar (unprefix "'" v))
| translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
@@ -604,7 +606,7 @@
##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
#>> (fn (((c, typargs), dss), range :: dom) =>
- IConst { sym = Code_Symbol.Constant c, typargs = typargs, dicts = dss,
+ IConst { sym = Constant c, typargs = typargs, dicts = dss,
dom = dom, range = range, annotate = annotate })
end
and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
@@ -629,7 +631,7 @@
let
fun collapse_clause vs_map ts body =
case body
- of IConst { sym = Code_Symbol.Constant c, ... } => if member (op =) undefineds c
+ of IConst { sym = Constant c, ... } => if member (op =) undefineds c
then []
else [(ts, body)]
| ICase { term = IVar (SOME v), clauses = clauses, ... } =>
@@ -747,7 +749,7 @@
if permissive then program
else Code_Symbol.Graph.restrict
(member (op =) (Code_Symbol.Graph.all_succs program
- (map Code_Symbol.Constant consts))) program;
+ (map Constant consts))) program;
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr permissive);
in
@@ -766,7 +768,7 @@
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
o dest_TFree))) t [];
val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
- val dummy_constant = Code_Symbol.Constant @{const_name dummy_pattern};
+ val dummy_constant = Constant @{const_name dummy_pattern};
val stmt_value =
fold_map (translate_tyvar_sort thy algbr eqngr false) vs
##>> translate_typ thy algbr eqngr false ty
@@ -783,7 +785,7 @@
val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
in ((program3, ((vs_ty, t), deps)), (dep, program2)) end;
in
- ensure_stmt Code_Symbol.Constant stmt_value @{const_name dummy_pattern}
+ ensure_stmt Constant stmt_value @{const_name dummy_pattern}
#> snd
#> term_value
end;
--- a/src/Tools/nbe.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/nbe.ML Sat Jan 25 23:50:49 2014 +0100
@@ -249,11 +249,9 @@
val univs_cookie = (Univs.get, put_result, name_put);
-val sloppy_name = Code_Symbol.base_name;
-
fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value"
| nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym)
- ^ "_" ^ sloppy_name sym ^ "_" ^ string_of_int i;
+ ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i;
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
fun nbe_bound v = "v_" ^ v;
fun nbe_bound_optional NONE = "_"
@@ -266,7 +264,7 @@
fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts);
fun nbe_apps_constr idx_of c ts =
let
- val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ sloppy_name c ^ "*)"
+ val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
else string_of_int (idx_of c);
in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
@@ -277,6 +275,7 @@
end;
+open Basic_Code_Symbol;
open Basic_Code_Thingol;
@@ -304,11 +303,11 @@
else nbe_apps_constr idx_of sym ts'
end
and assemble_classrels classrels =
- fold_rev (fn classrel => assemble_constapp (Code_Symbol.Class_Relation classrel) [] o single) classrels
+ fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels
and assemble_dict (Dict (classrels, x)) =
assemble_classrels classrels (assemble_plain_dict x)
and assemble_plain_dict (Dict_Const (inst, dss)) =
- assemble_constapp (Code_Symbol.Class_Instance inst) dss []
+ assemble_constapp (Class_Instance inst) dss []
| assemble_plain_dict (Dict_Var (v, (n, _))) =
nbe_dict v n
@@ -429,7 +428,7 @@
[]
| eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) =
let
- val syms = map Code_Symbol.Class_Relation classrels @ map (Code_Symbol.Constant o fst) classparams;
+ val syms = map Class_Relation classrels @ map (Constant o fst) classparams;
val params = Name.invent Name.context "d" (length syms);
fun mk (k, sym) =
(sym, ([(v, [])],
@@ -441,8 +440,8 @@
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
| eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) =
- [(sym_inst, (vs, [([], dummy_const (Code_Symbol.Type_Class class) [] `$$
- map (fn (class, dss) => dummy_const (Code_Symbol.Class_Instance (tyco, class)) dss) superinsts
+ [(sym_inst, (vs, [([], dummy_const (Type_Class class) [] `$$
+ map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) dss) superinsts
@ map (IConst o fst o snd o fst) inst_params)]))];
@@ -513,12 +512,12 @@
| take_until f (x :: xs) = if f x then [] else x :: take_until f xs;
fun is_dict (Const (idx, _)) =
(case Inttab.lookup idx_tab idx of
- SOME (Code_Symbol.Constant _) => false
+ SOME (Constant _) => false
| _ => true)
| is_dict (DFree _) = true
| is_dict _ = false;
fun const_of_idx idx =
- case Inttab.lookup idx_tab idx of SOME (Code_Symbol.Constant const) => const;
+ case Inttab.lookup idx_tab idx of SOME (Constant const) => const;
fun of_apps bounds (t, ts) =
fold_map (of_univ bounds) ts
#>> (fn ts' => list_comb (t, rev ts'))
@@ -568,7 +567,7 @@
structure Nbe_Functions = Code_Data
(
- type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.symbol Inttab.table);
+ type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.T Inttab.table);
val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
);