--- a/src/Doc/Codegen/Adaptation.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Doc/Codegen/Adaptation.thy Sat Jan 25 23:50:49 2014 +0100
@@ -2,8 +2,8 @@
imports Setup
begin
-setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I))
- #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", K I)) *}
+setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", I))
+ #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", I)) *}
section {* Adaptation to target languages \label{sec:adaptation} *}
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Jan 25 23:50:49 2014 +0100
@@ -671,25 +671,17 @@
open Code_Thingol;
-fun imp_program naming =
+val imp_program =
let
- fun is_const c = case lookup_const naming c
- of SOME c' => (fn c'' => c' = c'')
- | NONE => K false;
- val is_bind = is_const @{const_name bind};
- val is_return = is_const @{const_name return};
+ val is_bind = curry (op =) @{const_name bind};
+ val is_return = curry (op =) @{const_name return};
val dummy_name = "";
val dummy_case_term = IVar NONE;
(*assumption: dummy values are not relevant for serialization*)
- val (unitt, unitT) = case lookup_const naming @{const_name Unity}
- of SOME unit' =>
- let
- val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
- in
- (IConst { name = unit', typargs = [], dicts = [], dom = [],
- range = unitT, annotate = false }, unitT)
- end
- | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
+ val unitT = @{type_name unit} `%% [];
+ val unitt =
+ IConst { sym = Code_Symbol.Constant @{const_name Unity}, typargs = [], dicts = [], dom = [],
+ range = unitT, annotate = false };
fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
let
@@ -697,7 +689,7 @@
val v = singleton (Name.variant_list vs) "x";
val ty' = (hd o fst o unfold_fun) ty;
in ((SOME v, ty'), t `$ IVar (SOME v)) end;
- fun force (t as IConst { name = c, ... } `$ t') = if is_return c
+ fun force (t as IConst { sym = Code_Symbol.Constant c, ... } `$ t') = if is_return c
then t' else t `$ unitt
| force t = t `$ unitt;
fun tr_bind'' [(t1, _), (t2, ty2)] =
@@ -705,13 +697,13 @@
val ((v, ty), t) = dest_abs (t2, ty2);
in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
and tr_bind' t = case unfold_app t
- of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
+ of (IConst { sym = Code_Symbol.Constant c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
then tr_bind'' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
- fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
+ fun imp_monad_bind' (const as { sym = Code_Symbol.Constant c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
| ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
| (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
@@ -726,7 +718,7 @@
ICase { term = imp_monad_bind t, typ = ty,
clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
- in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
+ in (Code_Symbol.Graph.map o K o map_terms_stmt) imp_monad_bind end;
in
--- a/src/HOL/List.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/List.thy Sat Jan 25 23:50:49 2014 +0100
@@ -6318,14 +6318,14 @@
fun implode_list nil' cons' t =
let
- fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
+ fun dest_cons (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
if c = cons'
then SOME (t1, t2)
else NONE
| dest_cons _ = NONE;
val (ts, t') = Code_Thingol.unfoldr dest_cons t;
in case t'
- of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
+ of IConst { sym = Code_Symbol.Constant c, ... } => if c = nil' then SOME ts else NONE
| _ => NONE
end;
--- a/src/HOL/Quickcheck_Narrowing.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Sat Jan 25 23:50:49 2014 +0100
@@ -11,7 +11,7 @@
subsubsection {* Code generation setup *}
-setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
+setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *}
code_printing
type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
--- a/src/HOL/Quickcheck_Random.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Quickcheck_Random.thy Sat Jan 25 23:50:49 2014 +0100
@@ -9,7 +9,7 @@
notation fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "\<circ>\<rightarrow>" 60)
-setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
+setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, I)) *}
subsection {* Catching Match exceptions *}
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Jan 25 23:50:49 2014 +0100
@@ -309,9 +309,9 @@
fun dynamic_value_strict opts cookie thy postproc t =
let
val ctxt = Proof_Context.init_global thy
- fun evaluator naming program ((_, vs_ty), t) deps =
+ fun evaluator program ((_, vs_ty), t) deps =
Exn.interruptible_capture (value opts ctxt cookie)
- (Code_Target.evaluator thy target naming program deps (vs_ty, t));
+ (Code_Target.evaluator thy target program deps (vs_ty, t));
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
(** counterexample generator **)
--- a/src/HOL/Tools/numeral.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Tools/numeral.ML Sat Jan 25 23:50:49 2014 +0100
@@ -69,11 +69,11 @@
let
fun dest_numeral one' bit0' bit1' thm t =
let
- fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
+ fun dest_bit (IConst { sym = Code_Symbol.Constant c, ... }) = if c = bit0' then 0
else if c = bit1' then 1
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
| dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
- fun dest_num (IConst { name = c, ... }) = if c = one' then 1
+ fun dest_num (IConst { sym = Code_Symbol.Constant c, ... }) = if c = one' then 1
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
| dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
--- a/src/HOL/Tools/string_code.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Tools/string_code.ML Sat Jan 25 23:50:49 2014 +0100
@@ -23,13 +23,13 @@
| decode _ ~1 = NONE
| decode n m = SOME (chr (n * 16 + m));
in case tt
- of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
+ of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
| _ => NONE
end;
fun implode_string literals char' nibbles' ts =
let
- fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
+ fun implode_char (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
if c = char' then decode_char nibbles' (t1, t2) else NONE
| implode_char _ = NONE;
val ts' = map_filter implode_char ts;
--- 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
@@ -37,8 +37,11 @@
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;
fun class_name class = case class_syntax class
- of NONE => deresolve class
+ of NONE => deresolve_class class
| SOME class => class;
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
of [] => []
@@ -53,7 +56,7 @@
fun print_tyco_expr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
- of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
+ of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys)
| SOME (_, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
fun print_typdecl tyvars (tyco, vs) =
@@ -81,18 +84,19 @@
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 ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Code_Symbol.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
| NONE => print_case tyvars some_thm vars fxy case_expr)
- and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
+ and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =
let
- val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
+ val ty = Library.foldr (op `->) (dom, range)
val printed_const =
if annotate then
- brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
+ brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
else
- (str o deresolve) c
+ (str o deresolve) sym
in
printed_const :: map (print_term tyvars some_thm vars BR) ts
end
@@ -122,17 +126,16 @@
(concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
(map print_select clauses)
end;
- fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
+ fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_err n =
- semicolon (
- (str o deresolve) name
- :: map str (replicate n "_")
- @ str "="
- :: str "error"
- @@ (str o ML_Syntax.print_string
- o Long_Name.base_name o Long_Name.qualifier) name
+ (semicolon o map str) (
+ deresolve_const const
+ :: replicate n "_"
+ @ "="
+ :: "error"
+ @@ ML_Syntax.print_string const
);
fun print_eqn ((ts, t), (some_thm, _)) =
let
@@ -143,7 +146,7 @@
(insert (op =)) ts []);
in
semicolon (
- (str o deresolve) name
+ (str o deresolve_const) const
:: map (print_term tyvars some_thm vars BR) ts
@ str "="
@@ print_term tyvars some_thm vars NOBR t
@@ -152,7 +155,7 @@
in
Pretty.chunks (
semicolon [
- (str o suffix " ::" o deresolve) name,
+ (str o suffix " ::" o deresolve_const) const,
print_typscheme tyvars (vs, ty)
]
:: (case filter (snd o snd) raw_eqs
@@ -160,52 +163,52 @@
| eqs => map print_eqn eqs)
)
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
+ | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
let
val tyvars = intro_vars vs reserved;
in
semicolon [
str "data",
- print_typdecl tyvars (deresolve name, vs)
+ print_typdecl tyvars (deresolve_tyco tyco, vs)
]
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
+ | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
let
val tyvars = intro_vars vs reserved;
in
semicolon (
str "newtype"
- :: print_typdecl tyvars (deresolve name, vs)
+ :: print_typdecl tyvars (deresolve_tyco tyco, vs)
:: str "="
- :: (str o deresolve) co
+ :: (str o deresolve_const) co
:: print_typ tyvars BR ty
- :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
+ :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
+ | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
let
val tyvars = intro_vars vs reserved;
fun print_co ((co, _), tys) =
concat (
- (str o deresolve) co
+ (str o deresolve_const) co
:: map (print_typ tyvars BR) tys
)
in
semicolon (
str "data"
- :: print_typdecl tyvars (deresolve name, vs)
+ :: print_typdecl tyvars (deresolve_tyco tyco, vs)
:: str "="
:: print_co co
:: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
- @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
+ @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
)
end
- | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
+ | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
let
val tyvars = intro_vars [v] reserved;
fun print_classparam (classparam, ty) =
semicolon [
- (str o deresolve) classparam,
+ (str o deresolve_const) classparam,
str "::",
print_typ tyvars NOBR ty
]
@@ -213,8 +216,8 @@
Pretty.block_enclose (
Pretty.block [
str "class ",
- Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
- str (deresolve name ^ " " ^ lookup_var tyvars v),
+ Pretty.block (print_typcontext tyvars [(v, map snd classrels)]),
+ str (deresolve_class class ^ " " ^ lookup_var tyvars v),
str " where {"
],
str "};"
@@ -230,20 +233,20 @@
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
case requires_args classparam
of NONE => semicolon [
- (str o Long_Name.base_name o deresolve) classparam,
+ (str o Long_Name.base_name o deresolve_const) classparam,
str "=",
print_app tyvars (SOME thm) reserved NOBR (const, [])
]
| SOME k =>
let
- val { name = c, dom, range, ... } = const;
+ val { sym = Code_Symbol.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) 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 { name = classparam, typargs = [],
+ val lhs = IConst { sym = Code_Symbol.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 *)
@@ -268,7 +271,7 @@
end;
in print_stmt end;
-fun haskell_program_of_program ctxt symbol_of module_prefix module_name reserved identifiers =
+fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers =
let
fun namify_fun upper base (nsp_fun, nsp_typ) =
let
@@ -279,7 +282,7 @@
let
val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
in (base', (nsp_fun, nsp_typ')) end;
- fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
+ fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair
| namify_stmt (Code_Thingol.Fun _) = namify_fun false
| namify_stmt (Code_Thingol.Datatype _) = namify_typ
| namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
@@ -287,7 +290,7 @@
| namify_stmt (Code_Thingol.Classrel _) = pair
| namify_stmt (Code_Thingol.Classparam _) = namify_fun false
| namify_stmt (Code_Thingol.Classinst _) = pair;
- fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
+ fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false
| select_stmt (Code_Thingol.Fun _) = true
| select_stmt (Code_Thingol.Datatype _) = true
| select_stmt (Code_Thingol.Datatypecons _) = false
@@ -296,7 +299,7 @@
| select_stmt (Code_Thingol.Classparam _) = false
| select_stmt (Code_Thingol.Classinst _) = true;
in
- Code_Namespace.flat_program ctxt symbol_of
+ Code_Namespace.flat_program ctxt
{ module_prefix = module_prefix, module_name = module_name, reserved = reserved,
identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
@@ -323,25 +326,24 @@
("Maybe", ["Nothing", "Just"])
];
-fun serialize_haskell module_prefix string_classes ctxt { symbol_of, module_name,
+fun serialize_haskell module_prefix string_classes ctxt { module_name,
reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program =
let
(* build program *)
val reserved = fold (insert (op =) o fst) includes reserved_syms;
val { deresolver, flat_program = haskell_program } = haskell_program_of_program
- ctxt symbol_of module_prefix module_name (Name.make_context reserved) identifiers program;
+ ctxt module_prefix module_name (Name.make_context reserved) identifiers program;
(* print statements *)
fun deriving_show tyco =
let
fun deriv _ "fun" = false
- | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
- andalso (member (op =) tycos tyco
- orelse case try (Graph.get_node program) tyco
- of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
+ | deriv tycos tyco = member (op =) tycos tyco
+ orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco)
+ of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
(maps snd cs)
- | NONE => true)
+ | NONE => true
and deriv' tycos (tyco `%% tys) = deriv tycos tyco
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
@@ -369,10 +371,10 @@
val deresolve = deresolver module_name;
fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
- fun print_stmt' name = case Graph.get_node gr name
+ fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
of (_, NONE) => NONE
- | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
- val body_ps = map_filter print_stmt' ((flat o rev o Graph.strong_conn) gr);
+ | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt)));
+ val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr);
in
print_module_frame module_name
((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
@@ -430,7 +432,7 @@
of SOME ((pat, ty), t') =>
SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
- fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
+ fun dest_monad c_bind_name (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
if c = c_bind_name then dest_bind t1 t2
else NONE
| dest_monad _ t = case Code_Thingol.split_let t
--- 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
@@ -28,17 +28,17 @@
datatype ml_binding =
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
- | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
- superinsts: (class * (string * (string * dict list list))) list,
+ | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list,
+ superinsts: (class * dict list list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
datatype ml_stmt =
ML_Exc of string * (typscheme * int)
| ML_Val of ml_binding
- | ML_Funs of ml_binding list * string list
+ | ML_Funs of ml_binding list * Code_Symbol.symbol list
| ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
- | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
+ | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
fun print_product _ [] = NONE
| print_product print [x] = SOME (print x)
@@ -53,30 +53,35 @@
fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
- fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
- | print_tyco_expr (tyco, [ty]) =
- concat [print_typ BR ty, (str o deresolve) tyco]
- | print_tyco_expr (tyco, tys) =
- concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
+ 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;
+ 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 (tyco, tys)
+ of NONE => print_tyco_expr (Code_Symbol.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 (class, [ty]);
+ fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.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);
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
fun print_classrels fxy [] ps = brackify fxy ps
- | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
+ | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps]
| print_classrels fxy classrels ps =
- brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
+ brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
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 ::
- (if is_pseudo_fun inst then [str "()"]
+ ((str o deresolve_inst) inst ::
+ (if is_pseudo_fun (Code_Symbol.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 ^ "_"
@@ -105,21 +110,22 @@
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 ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Code_Symbol.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
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
- if is_constr c then
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+ if is_constr sym then
let val k = length dom in
if k < 2 orelse length ts = k
- then (str o deresolve) c
+ then (str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
- else if is_pseudo_fun c
- then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
+ else if is_pseudo_fun sym
+ then (str o deresolve) sym @@ str "()"
+ else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
@ 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) const_syntax some_thm vars
@@ -158,23 +164,23 @@
:: map (print_select "|") clauses
)
end;
- fun print_val_decl print_typscheme (name, typscheme) = concat
- [str "val", str (deresolve name), str ":", print_typscheme typscheme];
+ fun print_val_decl print_typscheme (sym, typscheme) = concat
+ [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co ((co, _), []) = str (deresolve co)
- | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve_const co)
+ | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
str definer
- :: print_tyco_expr (tyco, map ITyVar vs)
+ :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
end;
fun print_def is_pseudo_fun needs_typ definer
- (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
+ (ML_Function (const, (vs_ty as (vs, ty), eq :: eqs))) =
let
fun print_eqn definer ((ts, t), (some_thm, _)) =
let
@@ -184,12 +190,12 @@
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
val prolog = if needs_typ then
- concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
- else (concat o map str) [definer, deresolve name];
+ concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
+ else (concat o map str) [definer, deresolve_const const];
in
concat (
prolog
- :: (if is_pseudo_fun name then [str "()"]
+ :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
else print_dict_args vs
@ map (print_term is_pseudo_fun some_thm vars BR) ts)
@ str "="
@@ -199,53 +205,53 @@
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 (name, vs_ty))
+ (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
((Pretty.block o Pretty.fbreaks o shift) (
print_eqn definer eq
:: map (print_eqn "|") eqs
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
+ (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
let
- fun print_super_instance (_, (classrel, x)) =
+ fun print_super_instance (super_class, x) =
concat [
- (str o Long_Name.base_name o deresolve) classrel,
+ (str o Long_Name.base_name o deresolve_classrel) (class, super_class),
str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
- (str o Long_Name.base_name o deresolve) classparam,
+ (str o Long_Name.base_name o deresolve_const) classparam,
str "=",
print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
- (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+ (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
str definer
- :: (str o deresolve) inst
- :: (if is_pseudo_fun inst then [str "()"]
+ :: (str o deresolve_inst) inst
+ :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
else print_dict_args vs)
@ str "="
:: enum "," "{" "}"
(map print_super_instance superinsts
@ map print_classparam_instance inst_params)
:: str ":"
- @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
+ @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
))
end;
- fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
- [print_val_decl print_typscheme (name, vs_ty)]
+ fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
+ [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
((semicolon o map str) (
(if n = 0 then "val" else "fun")
- :: deresolve name
+ :: deresolve_const const
:: replicate n "_"
@ "="
:: "raise"
:: "Fail"
- @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
+ @@ ML_Syntax.print_string const
))
| print_stmt (ML_Val binding) =
let
@@ -257,11 +263,11 @@
| print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
let
val print_def' = print_def (member (op =) pseudo_funs) false;
- fun print_pseudo_fun name = concat [
+ fun print_pseudo_fun sym = concat [
str "val",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "=",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "();"
];
val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
@@ -273,7 +279,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (tyco, map ITyVar vs);
+ val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -288,42 +294,42 @@
sig_ps
(Pretty.chunks (ps @| semicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
+ | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
fun print_proj s p = semicolon
(map str ["val", s, "=", "#" ^ s, ":"] @| p);
- fun print_super_class_decl (super_class, classrel) =
+ fun print_super_class_decl (classrel as (_, super_class)) =
print_val_decl print_dicttypscheme
- (classrel, ([(v, [class])], (super_class, ITyVar v)));
- fun print_super_class_field (super_class, classrel) =
- print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
- fun print_super_class_proj (super_class, classrel) =
- print_proj (deresolve classrel)
+ (Code_Symbol.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)) =
+ print_proj (deresolve_classrel classrel)
(print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
fun print_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
- (classparam, ([(v, [class])], ty));
+ (Code_Symbol.Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
- print_field (deresolve classparam) (print_typ NOBR ty);
+ print_field (deresolve_const classparam) (print_typ NOBR ty);
fun print_classparam_proj (classparam, ty) =
- print_proj (deresolve classparam)
+ print_proj (deresolve_const classparam)
(print_typscheme ([(v, [class])], ty));
in pair
(concat [str "type", print_dicttyp (class, ITyVar v)]
- :: map print_super_class_decl super_classes
+ :: map print_super_class_decl classrels
@ map print_classparam_decl classparams)
(Pretty.chunks (
concat [
str ("type '" ^ v),
- (str o deresolve) class,
+ (str o deresolve_class) class,
str "=",
enum "," "{" "};" (
- map print_super_class_field super_classes
+ map print_super_class_field classrels
@ map print_classparam_field classparams
)
]
- :: map print_super_class_proj super_classes
+ :: map print_super_class_proj classrels
@ map print_classparam_proj classparams
))
end;
@@ -353,29 +359,34 @@
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
- fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
- | print_tyco_expr (tyco, [ty]) =
- concat [print_typ BR ty, (str o deresolve) tyco]
- | print_tyco_expr (tyco, tys) =
- concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
+ 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;
+ 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 (tyco, tys)
+ of NONE => print_tyco_expr (Code_Symbol.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 (class, [ty]);
+ fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.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);
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
val print_classrels =
- fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
+ fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
print_plain_dict is_pseudo_fun fxy x
|> print_classrels classrels
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
- brackify BR ((str o deresolve) inst ::
- (if is_pseudo_fun inst then [str "()"]
+ brackify BR ((str o deresolve_inst) inst ::
+ (if is_pseudo_fun (Code_Symbol.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
@@ -401,21 +412,22 @@
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 ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Code_Symbol.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
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
- if is_constr c then
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+ if is_constr sym then
let val k = length dom in
if length ts = k
- then (str o deresolve) c
+ then (str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
- else if is_pseudo_fun c
- then (str o deresolve) c @@ str "()"
- else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
+ else if is_pseudo_fun sym
+ then (str o deresolve) sym @@ str "()"
+ else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
@ 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) const_syntax some_thm vars
@@ -449,23 +461,23 @@
:: map (print_select "|") clauses
)
end;
- fun print_val_decl print_typscheme (name, typscheme) = concat
- [str "val", str (deresolve name), str ":", print_typscheme typscheme];
+ fun print_val_decl print_typscheme (sym, typscheme) = concat
+ [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co ((co, _), []) = str (deresolve co)
- | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
+ fun print_co ((co, _), []) = str (deresolve_const co)
+ | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
str definer
- :: print_tyco_expr (tyco, map ITyVar vs)
+ :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
:: str "="
:: separate (str "|") (map print_co cos)
)
end;
fun print_def is_pseudo_fun needs_typ definer
- (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
+ (ML_Function (const, (vs_ty as (vs, ty), eqs))) =
let
fun print_eqn ((ts, t), (some_thm, _)) =
let
@@ -529,57 +541,57 @@
)
end;
val prolog = if needs_typ then
- concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
- else (concat o map str) [definer, deresolve name];
+ 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 (name, vs_ty))
+ (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
(concat (
prolog
:: print_dict_args vs
- @| print_eqns (is_pseudo_fun name) eqs
+ @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
))
end
| print_def is_pseudo_fun _ definer
- (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
+ (ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
let
- fun print_super_instance (_, (classrel, x)) =
+ fun print_super_instance (super_class, x) =
concat [
- (str o deresolve) classrel,
+ (str o deresolve_classrel) (class, super_class),
str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
- (str o deresolve) classparam,
+ (str o deresolve_const) classparam,
str "=",
print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
- (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+ (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
str definer
- :: (str o deresolve) inst
- :: (if is_pseudo_fun inst then [str "()"]
+ :: (str o deresolve_inst) inst
+ :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
else print_dict_args vs)
@ str "="
@@ brackets [
enum_default "()" ";" "{" "}" (map print_super_instance superinsts
@ map print_classparam_instance inst_params),
str ":",
- print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
+ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
]
))
end;
- fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
- [print_val_decl print_typscheme (name, vs_ty)]
+ fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
+ [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
((doublesemicolon o map str) (
"let"
- :: deresolve name
+ :: deresolve_const const
:: replicate n "_"
@ "="
:: "failwith"
- @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
+ @@ ML_Syntax.print_string const
))
| print_stmt (ML_Val binding) =
let
@@ -591,11 +603,11 @@
| print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
let
val print_def' = print_def (member (op =) pseudo_funs) false;
- fun print_pseudo_fun name = concat [
+ fun print_pseudo_fun sym = concat [
str "let",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "=",
- (str o deresolve) name,
+ (str o deresolve) sym,
str "();;"
];
val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
@@ -607,7 +619,7 @@
end
| print_stmt (ML_Datas [(tyco, (vs, []))]) =
let
- val ty_p = print_tyco_expr (tyco, map ITyVar vs);
+ val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
in
pair
[concat [str "type", ty_p]]
@@ -622,26 +634,26 @@
sig_ps
(Pretty.chunks (ps @| doublesemicolon [p]))
end
- | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
+ | print_stmt (ML_Class (class, (v, (classrels, classparams)))) =
let
fun print_field s p = concat [str s, str ":", p];
- fun print_super_class_field (super_class, classrel) =
- print_field (deresolve classrel) (print_dicttyp (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_classparam_decl (classparam, ty) =
print_val_decl print_typscheme
- (classparam, ([(v, [class])], ty));
+ (Code_Symbol.Constant classparam, ([(v, [class])], ty));
fun print_classparam_field (classparam, ty) =
- print_field (deresolve classparam) (print_typ NOBR ty);
+ print_field (deresolve_const classparam) (print_typ NOBR ty);
val w = "_" ^ first_upper v;
fun print_classparam_proj (classparam, _) =
- (concat o map str) ["let", deresolve classparam, w, "=",
- w ^ "." ^ deresolve classparam ^ ";;"];
+ (concat o map str) ["let", deresolve_const classparam, w, "=",
+ w ^ "." ^ deresolve_const classparam ^ ";;"];
val type_decl_p = concat [
str ("type '" ^ v),
- (str o deresolve) class,
+ (str o deresolve_class) class,
str "=",
enum_default "unit" ";" "{" "}" (
- map print_super_class_field super_classes
+ map print_super_class_field classrels
@ map print_classparam_field classparams
)
];
@@ -694,7 +706,7 @@
(** SML/OCaml generic part **)
-fun ml_program_of_program ctxt symbol_of module_name reserved identifiers program =
+fun ml_program_of_program ctxt module_name reserved identifiers program =
let
fun namify_const upper base (nsp_const, nsp_type) =
let
@@ -712,76 +724,76 @@
| 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 (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
+ fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
let
val eqs = filter (snd o snd) raw_eqs;
- val (eqs', some_value_name) = if null (filter_out (null o snd) vs) then case eqs
+ val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
- else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
+ else (eqs, SOME (sym, member (op =) (Code_Thingol.add_constsyms t []) sym))
| _ => (eqs, NONE)
else (eqs, NONE)
- in (ML_Function (name, (tysm, eqs')), some_value_name) end
- | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
- (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
- | ml_binding_of_stmt (name, _) =
+ 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_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: " ^
- (Code_Symbol.quote_symbol ctxt o symbol_of) name)
- fun modify_fun (name, stmt) =
+ Code_Symbol.quote ctxt sym)
+ fun modify_fun (sym, stmt) =
let
- val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
+ val (binding, some_value_sym) = ml_binding_of_stmt (sym, stmt);
val ml_stmt = case binding
- of ML_Function (name, ((vs, ty), [])) =>
- ML_Exc (name, ((vs, ty),
+ of ML_Function (const, ((vs, ty), [])) =>
+ ML_Exc (const, ((vs, ty),
(length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
- | _ => case some_value_name
+ | _ => case some_value_sym
of NONE => ML_Funs ([binding], [])
- | SOME (name, true) => ML_Funs ([binding], [name])
- | SOME (name, false) => ML_Val binding
+ | SOME (sym, true) => ML_Funs ([binding], [sym])
+ | SOME (sym, false) => ML_Val binding
in SOME ml_stmt end;
fun modify_funs stmts = single (SOME
(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 (name, Code_Thingol.Datatype (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts)))
+ (fn (Code_Symbol.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 (name, Code_Thingol.Class (_, stmt)) => SOME (name, stmt) | _ => NONE) stmts))))
+ (fn (Code_Symbol.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 _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
modify_funs (filter_out (Code_Thingol.is_case o snd) stmts)
- | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Datatypecons _) :: _)) =
modify_datatypes stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Datatype _) :: _)) =
modify_datatypes stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Class _) :: _)) =
modify_class stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classrel _) :: _)) =
modify_class stmts
- | modify_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classparam _) :: _)) =
modify_class stmts
| modify_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
[modify_fun stmt]
- | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
+ | modify_stmts ((stmts as (_, Code_Thingol.Classinst _) :: _)) =
modify_funs stmts
| modify_stmts stmts = error ("Illegal mutual dependencies: " ^
- (Library.commas o map (Code_Symbol.quote_symbol ctxt o symbol_of o fst)) stmts);
+ (Library.commas o map (Code_Symbol.quote ctxt o fst)) stmts);
in
- Code_Namespace.hierarchical_program ctxt symbol_of {
+ Code_Namespace.hierarchical_program ctxt {
module_name = module_name, reserved = reserved, identifiers = identifiers,
empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
end;
fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
- { symbol_of, module_name, reserved_syms, identifiers, includes,
+ { module_name, reserved_syms, identifiers, includes,
class_syntax, tyco_syntax, const_syntax } program =
let
(* build program *)
val { deresolver, hierarchical_program = ml_program } =
- ml_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
+ ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
(* print statements *)
fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
@@ -803,7 +815,7 @@
lift_markup = apsnd } ml_program));
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
- fun prepare names width p = ([("", format names width p)], try (deresolver []));
+ fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
in
Code_Target.serialization write prepare p
end;
--- 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
@@ -7,32 +7,32 @@
signature CODE_NAMESPACE =
sig
type flat_program
- val flat_program: Proof.context -> (string -> Code_Symbol.symbol)
+ val flat_program: Proof.context
-> { module_prefix: string, module_name: string,
reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a,
namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
-> Code_Thingol.program
- -> { deresolver: string -> string -> string,
+ -> { deresolver: string -> Code_Symbol.symbol -> string,
flat_program: flat_program }
datatype ('a, 'b) node =
Dummy
| Stmt of 'a
- | Module of ('b * (string * ('a, 'b) node) Graph.T)
+ | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
type ('a, 'b) hierarchical_program
- val hierarchical_program: Proof.context -> (string -> Code_Symbol.symbol)
+ val hierarchical_program: Proof.context
-> { module_name: string,
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: string -> 'b -> 'b,
- modify_stmts: (string * Code_Thingol.stmt) list -> 'a option list }
+ 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 }
-> Code_Thingol.program
- -> { deresolver: string list -> string -> string,
+ -> { deresolver: string list -> Code_Symbol.symbol -> string,
hierarchical_program: ('a, 'b) hierarchical_program }
val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
- print_stmt: string list -> string * 'a -> 'c,
+ print_stmt: string list -> Code_Symbol.symbol * 'a -> 'c,
lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
-> ('a, 'b) hierarchical_program -> 'c list
end;
@@ -42,24 +42,22 @@
(** fundamental module name hierarchy **)
-val split_name = apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-fun lookup_identifier symbol_of identifiers name =
- Code_Symbol.lookup identifiers (symbol_of name)
+fun lookup_identifier identifiers sym =
+ Code_Symbol.lookup identifiers sym
|> Option.map (split_last o Long_Name.explode);
-fun force_identifier symbol_of fragments_tab force_module identifiers name =
- case lookup_identifier symbol_of identifiers name of
- NONE => (apfst (the o Symtab.lookup fragments_tab) o split_name) name
+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)
| SOME prefix_name => if null force_module then prefix_name
else (force_module, snd prefix_name);
-fun build_module_namespace { module_prefix, module_identifiers, reserved } program =
+fun build_module_namespace ctxt { module_prefix, module_identifiers, reserved } program =
let
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 = Graph.fold (insert (op =) o fst o split_name o fst) program [];
+ val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.namespace_prefix ctxt o fst) program [];
in
fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
module_names Symtab.empty
@@ -68,9 +66,9 @@
(** flat program structure **)
-type flat_program = ((string * Code_Thingol.stmt option) Graph.T * (string * string list) list) Graph.T;
+type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.symbol list) list) Graph.T;
-fun flat_program ctxt symbol_of { module_prefix, module_name, reserved,
+fun flat_program ctxt { module_prefix, module_name, reserved,
identifiers, empty_nsp, namify_stmt, modify_stmt } program =
let
@@ -78,70 +76,70 @@
val module_identifiers = if module_name = ""
then Code_Symbol.lookup_module_data identifiers
else K (SOME module_name);
- val fragments_tab = build_module_namespace { module_prefix = module_prefix,
+ val fragments_tab = build_module_namespace ctxt { module_prefix = module_prefix,
module_identifiers = module_identifiers, reserved = reserved } program;
- val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers
+ val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers
#>> Long_Name.implode;
(* distribute statements over hierarchy *)
- fun add_stmt name stmt =
+ fun add_stmt sym stmt =
let
- val (module_name, base) = prep_name name;
+ val (module_name, base) = prep_sym sym;
in
- Graph.default_node (module_name, (Graph.empty, []))
- #> (Graph.map_node module_name o apfst) (Graph.new_node (name, (base, stmt)))
+ Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
+ #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt)))
end;
- fun add_dependency name name' =
+ fun add_dependency sym sym' =
let
- val (module_name, _) = prep_name name;
- val (module_name', _) = prep_name name';
+ val (module_name, _) = prep_sym sym;
+ val (module_name', _) = prep_sym sym';
in if module_name = module_name'
- then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
- else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
+ then (Graph.map_node module_name o apfst) (Code_Symbol.Graph.add_edge (sym, sym'))
+ else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) sym'))
end;
val proto_program = Graph.empty
- |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
- |> Graph.fold (fn (name, (_, (_, names))) =>
- Graph.Keys.fold (add_dependency name) names) program;
+ |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
+ |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
+ Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
(* name declarations and statement modifications *)
- fun declare name (base, stmt) (gr, nsp) =
+ fun declare sym (base, stmt) (gr, nsp) =
let
val (base', nsp') = namify_stmt stmt base nsp;
- val gr' = (Graph.map_node name o apfst) (K base') gr;
+ val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
in (gr', nsp') end;
fun declarations gr = (gr, empty_nsp)
- |> fold (fn name => declare name (Graph.get_node gr name)) (Graph.keys gr)
+ |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (Code_Symbol.Graph.keys gr)
|> fst
- |> (Graph.map o K o apsnd) modify_stmt;
+ |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
val flat_program = proto_program
|> (Graph.map o K o apfst) declarations;
(* qualified and unqualified imports, deresolving *)
- fun base_deresolver name = fst (Graph.get_node
- (fst (Graph.get_node flat_program (fst (prep_name name)))) name);
+ fun base_deresolver sym = fst (Code_Symbol.Graph.get_node
+ (fst (Graph.get_node flat_program (fst (prep_sym sym)))) sym);
fun classify_names gr imports =
let
val import_tab = maps
- (fn (module_name, names) => map (rpair module_name) names) imports;
- val imported_names = map fst import_tab;
- val here_names = Graph.keys gr;
+ (fn (module_name, syms) => map (rpair module_name) syms) imports;
+ val imported_syms = map fst import_tab;
+ val here_syms = Code_Symbol.Graph.keys gr;
in
- Symtab.empty
- |> fold (fn name => Symtab.update (name, base_deresolver name)) here_names
- |> fold (fn name => Symtab.update (name,
- Long_Name.append (the (AList.lookup (op =) import_tab name))
- (base_deresolver name))) imported_names
+ Code_Symbol.Table.empty
+ |> fold (fn sym => Code_Symbol.Table.update (sym, base_deresolver sym)) here_syms
+ |> fold (fn sym => Code_Symbol.Table.update (sym,
+ Long_Name.append (the (AList.lookup (op =) import_tab sym))
+ (base_deresolver sym))) imported_syms
end;
val deresolver_tab = Symtab.make (AList.make
(uncurry classify_names o Graph.get_node flat_program)
(Graph.keys flat_program));
- fun deresolver "" name =
- Long_Name.append (fst (prep_name name)) (base_deresolver name)
- | deresolver module_name name =
- the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
+ fun deresolver "" sym =
+ Long_Name.append (fst (prep_sym sym)) (base_deresolver sym)
+ | deresolver module_name sym =
+ the (Code_Symbol.Table.lookup (the (Symtab.lookup deresolver_tab module_name)) sym)
handle Option.Option => error ("Unknown statement name: "
- ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name);
+ ^ Code_Symbol.quote ctxt sym);
in { deresolver = deresolver, flat_program = flat_program } end;
@@ -151,18 +149,18 @@
datatype ('a, 'b) node =
Dummy
| Stmt of 'a
- | Module of ('b * (string * ('a, 'b) node) Graph.T);
+ | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
-type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Graph.T;
+type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
fun map_module_content f (Module content) = Module (f content);
fun map_module [] = I
| map_module (name_fragment :: name_fragments) =
- apsnd o Graph.map_node name_fragment o apsnd o map_module_content
+ apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content
o map_module name_fragments;
-fun hierarchical_program ctxt symbol_of { module_name, reserved, identifiers, empty_nsp,
+fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp,
namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program =
let
@@ -170,95 +168,95 @@
val module_identifiers = if module_name = ""
then Code_Symbol.lookup_module_data identifiers
else K (SOME module_name);
- val fragments_tab = build_module_namespace { module_prefix = "",
+ val fragments_tab = build_module_namespace ctxt { module_prefix = "",
module_identifiers = module_identifiers, reserved = reserved } program;
- val prep_name = force_identifier symbol_of fragments_tab (Long_Name.explode module_name) identifiers;
+ val prep_sym = force_identifier ctxt fragments_tab (Long_Name.explode module_name) identifiers;
(* building empty module hierarchy *)
- val empty_module = (empty_data, Graph.empty);
+ val empty_module = (empty_data, Code_Symbol.Graph.empty);
fun ensure_module name_fragment (data, nodes) =
- if can (Graph.get_node nodes) name_fragment then (data, nodes)
+ if can (Code_Symbol.Graph.get_node nodes) (Code_Symbol.Module name_fragment) then (data, nodes)
else (data,
- nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
+ nodes |> Code_Symbol.Graph.new_node (Code_Symbol.Module name_fragment, (name_fragment, Module empty_module)));
fun allocate_module [] = I
| allocate_module (name_fragment :: name_fragments) =
ensure_module name_fragment
- #> (apsnd o Graph.map_node name_fragment o apsnd o map_module_content o allocate_module) name_fragments;
+ #> (apsnd o Code_Symbol.Graph.map_node (Code_Symbol.Module name_fragment) o apsnd o map_module_content o allocate_module) name_fragments;
val empty_program =
empty_module
|> Symtab.fold (fn (_, fragments) => allocate_module fragments) fragments_tab
- |> Graph.fold (allocate_module o these o Option.map fst
- o lookup_identifier symbol_of identifiers o fst) program;
+ |> Code_Symbol.Graph.fold (allocate_module o these o Option.map fst
+ o lookup_identifier identifiers o fst) program;
(* distribute statements over hierarchy *)
- fun add_stmt name stmt =
+ fun add_stmt sym stmt =
let
- val (name_fragments, base) = prep_name name;
+ val (name_fragments, base) = prep_sym sym;
in
- (map_module name_fragments o apsnd) (Graph.new_node (name, (base, Stmt stmt)))
+ (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt)))
end;
- fun add_dependency name name' =
+ fun add_dependency sym sym' =
let
- val (name_fragments, _) = prep_name name;
- val (name_fragments', _) = prep_name name';
+ val (name_fragments, _) = prep_sym sym;
+ val (name_fragments', _) = prep_sym sym';
val (name_fragments_common, (diff, diff')) =
chop_prefix (op =) (name_fragments, name_fragments');
val is_module = not (null diff andalso null diff');
- val dep = pairself hd (diff @ [name], diff' @ [name']);
+ val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
val add_edge = if is_module andalso not cyclic_modules
- then (fn node => Graph.add_edge_acyclic dep node
+ then (fn node => Code_Symbol.Graph.add_edge_acyclic dep node
handle Graph.CYCLES _ => error ("Dependency "
- ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name ^ " -> "
- ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name'
+ ^ Code_Symbol.quote ctxt sym ^ " -> "
+ ^ Code_Symbol.quote ctxt sym'
^ " would result in module dependency cycle"))
- else Graph.add_edge dep
+ else Code_Symbol.Graph.add_edge dep
in (map_module name_fragments_common o apsnd) add_edge end;
val proto_program = empty_program
- |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
- |> Graph.fold (fn (name, (_, (_, names))) =>
- Graph.Keys.fold (add_dependency name) names) program;
+ |> Code_Symbol.Graph.fold (fn (sym, (stmt, _)) => add_stmt sym stmt) program
+ |> Code_Symbol.Graph.fold (fn (sym, (_, (_, syms))) =>
+ Code_Symbol.Graph.Keys.fold (add_dependency sym) syms) program;
(* name declarations, data and statement modifications *)
fun make_declarations nsps (data, nodes) =
let
- val (module_fragments, stmt_names) = List.partition
- (fn name_fragment => case Graph.get_node nodes name_fragment
- of (_, Module _) => true | _ => false) (Graph.keys nodes);
- fun declare namify name (nsps, nodes) =
+ val (module_fragments, stmt_syms) = List.partition
+ (fn sym => case Code_Symbol.Graph.get_node nodes sym
+ of (_, Module _) => true | _ => false) (Code_Symbol.Graph.keys nodes);
+ fun declare namify sym (nsps, nodes) =
let
- val (base, node) = Graph.get_node nodes name;
+ val (base, node) = Code_Symbol.Graph.get_node nodes sym;
val (base', nsps') = namify node base nsps;
- val nodes' = Graph.map_node name (K (base', node)) nodes;
+ val nodes' = Code_Symbol.Graph.map_node sym (K (base', node)) nodes;
in (nsps', nodes') end;
val (nsps', nodes') = (nsps, nodes)
|> fold (declare (K namify_module)) module_fragments
- |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names;
+ |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms;
fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE;
- fun select_names names = case filter (member (op =) stmt_names) names
+ fun select_syms syms = case filter (member (op =) stmt_syms) syms
of [] => NONE
- | xs => SOME xs;
- val modify_stmts' = AList.make (snd o Graph.get_node nodes)
+ | syms => SOME syms;
+ val modify_stmts' = AList.make (snd o Code_Symbol.Graph.get_node nodes)
#> split_list
##> map (fn Stmt stmt => stmt)
- #> (fn (names, stmts) => zip_fillup names (modify_stmts (names ~~ stmts)));
- val stmtss' = (maps modify_stmts' o map_filter select_names o Graph.strong_conn) nodes;
- val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content)
- | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
- val data' = fold memorize_data stmt_names data;
+ #> (fn (syms, stmts) => zip_fillup syms (modify_stmts (syms ~~ stmts)));
+ val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
+ val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
+ | _ => case AList.lookup (op =) stmtss' sym of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
+ val data' = fold memorize_data stmt_syms data;
in (data', nodes'') end;
val (_, hierarchical_program) = make_declarations empty_nsp proto_program;
(* deresolving *)
- fun deresolver prefix_fragments name =
+ fun deresolver prefix_fragments sym =
let
- val (name_fragments, _) = prep_name name;
+ val (name_fragments, _) = prep_sym sym;
val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
- val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
+ val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment)
of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
- val (base', _) = Graph.get_node nodes name;
+ val (base', _) = Code_Symbol.Graph.get_node nodes sym;
in Long_Name.implode (remainder @ [base']) end
- handle Graph.UNDEF _ => error ("Unknown statement name: "
- ^ (Code_Symbol.quote_symbol ctxt o symbol_of) name);
+ handle Code_Symbol.Graph.UNDEF _ => error ("Unknown statement name: "
+ ^ Code_Symbol.quote ctxt sym);
in { deresolver = deresolver, hierarchical_program = hierarchical_program } end;
@@ -266,10 +264,10 @@
let
fun print_node _ (_, Dummy) =
NONE
- | print_node prefix_fragments (name, Stmt stmt) =
- SOME (lift_markup (Code_Printer.markup_stmt name)
- (print_stmt prefix_fragments (name, stmt)))
- | print_node prefix_fragments (name_fragment, Module (data, nodes)) =
+ | print_node prefix_fragments (sym, Stmt stmt) =
+ SOME (lift_markup (Code_Printer.markup_stmt sym)
+ (print_stmt prefix_fragments (sym, stmt)))
+ | print_node prefix_fragments (Code_Symbol.Module name_fragment, Module (data, nodes)) =
let
val prefix_fragments' = prefix_fragments @ [name_fragment]
in
@@ -278,9 +276,9 @@
end
and print_nodes prefix_fragments nodes =
let
- val xs = (map_filter (fn name => print_node prefix_fragments
- (name, snd (Graph.get_node nodes name))) o rev o flat o Graph.strong_conn) nodes
+ val xs = (map_filter (fn sym => print_node prefix_fragments
+ (sym, snd (Code_Symbol.Graph.get_node nodes sym))) o rev o flat o Code_Symbol.Graph.strong_conn) nodes
in if null xs then NONE else SOME xs end;
in these o print_nodes [] end;
-end;
\ No newline at end of file
+end;
--- 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: string -> Pretty.T -> Pretty.T
- val format: string list -> int -> Pretty.T -> string
+ val markup_stmt: Code_Symbol.symbol -> Pretty.T -> Pretty.T
+ val format: Code_Symbol.symbol 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) -> (string -> string)
+ val intro_base_names_for: (string -> bool) -> (Code_Symbol.symbol -> string)
-> iterm list -> var_ctxt -> var_ctxt
val aux_params: var_ctxt -> iterm list list -> string list
@@ -81,7 +81,7 @@
val simple_const_syntax: simple_const_syntax -> const_syntax
val complex_const_syntax: complex_const_syntax -> const_syntax
val activate_const_syntax: theory -> literals
- -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
+ -> string -> const_syntax -> activated_const_syntax
val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
-> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> activated_const_syntax option)
@@ -125,17 +125,18 @@
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
fun indent i = Print_Mode.setmp [] (Pretty.indent i);
-fun markup_stmt name = Print_Mode.setmp [code_presentationN]
- (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
+fun markup_stmt sym = Print_Mode.setmp [code_presentationN]
+ (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
fun filter_presentation [] tree =
Buffer.empty
|> fold XML.add_content tree
- | filter_presentation presentation_names tree =
+ | filter_presentation presentation_syms tree =
let
+ val presentation_idents = map Code_Symbol.marker presentation_syms
fun is_selected (name, attrs) =
name = code_presentationN
- andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
+ andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
fun add_content_with_space tree (is_first, buf) =
buf
|> not is_first ? Buffer.add "\n\n"
@@ -198,8 +199,8 @@
fun intro_base_names_for no_syntax deresolve ts =
[]
- |> fold Code_Thingol.add_constnames ts
- |> intro_base_names no_syntax deresolve;
+ |> fold Code_Thingol.add_constsyms ts
+ |> intro_base_names (fn Code_Symbol.Constant const => no_syntax const | _ => true) deresolve;
(** pretty literals **)
@@ -304,30 +305,31 @@
datatype activated_const_syntax = Plain_const_syntax of int * string
| Complex_const_syntax of activated_complex_const_syntax;
-fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
- (Plain_const_syntax (Code.args_number thy c, s), naming)
- | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
- fold_map (Code_Thingol.ensure_declared_const thy) cs naming
- |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
+fun activate_const_syntax thy literals c (plain_const_syntax s) =
+ Plain_const_syntax (Code.args_number thy c, s)
+ | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f)))=
+ Complex_const_syntax (n, f literals cs);
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
- (app as ({ name = c, dom, ... }, 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)) =>
- let
- fun print' fxy ts =
- print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
- in
- if k = length ts
- then print' fxy ts
- else if k < length ts
- then case chop k ts of (ts1, ts2) =>
- brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
- else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
- end;
+ (app as ({ sym, dom, ... }, ts)) =
+ case sym of
+ Code_Symbol.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)
+ | SOME (Complex_const_syntax (k, print)) =>
+ let
+ fun print' fxy ts =
+ print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
+ in
+ if k = length ts
+ then print' fxy ts
+ else if k < length ts
+ then case chop k ts of (ts1, ts2) =>
+ brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
+ else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
+ end)
+ | _ => brackify fxy (print_app_expr some_thm vars app);
fun gen_print_bind print_term thm (fxy : fixity) pat vars =
let
--- 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
@@ -52,7 +52,7 @@
datatype truth = Holds;
val _ = Theory.setup
- (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
+ (Code_Target.extend_target (target, (Code_ML.target_SML, I))
#> Code_Target.set_printings (Code_Symbol.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},
@@ -87,10 +87,13 @@
val ctxt = Proof_Context.init_global thy;
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
-fun obtain_evaluator thy some_target naming program consts expr =
- Code_Target.evaluator thy (the_default target some_target) naming program consts expr
+fun obtain_evaluator thy some_target program consts expr =
+ Code_Target.evaluator thy (the_default target some_target) program consts expr
|> 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;
+
fun evaluation cookie thy evaluator vs_t args =
let
val ctxt = Proof_Context.init_global thy;
@@ -110,8 +113,8 @@
val _ = if ! trace
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
else ()
- fun evaluator naming program ((_, vs_ty), t) deps =
- evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
+ fun evaluator program ((_, vs_ty), t) deps =
+ evaluation cookie thy (obtain_evaluator thy some_target program deps) (vs_ty, t) args;
in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
fun dynamic_value_strict cookie thy some_target postproc t args =
@@ -120,9 +123,9 @@
fun dynamic_value cookie thy some_target postproc t args =
partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
-fun static_evaluator cookie thy some_target naming program consts' =
+fun static_evaluator cookie thy some_target program consts' =
let
- val evaluator = obtain_evaluator thy some_target naming program consts'
+ val evaluator = obtain_evaluator' thy some_target program consts'
in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
fun static_value_exn cookie thy some_target postproc consts =
@@ -175,13 +178,13 @@
in
fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
- (fn naming => fn program => fn vs_t => fn deps =>
- check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
+ (fn program => fn vs_t => fn deps =>
+ check_holds_oracle thy (obtain_evaluator thy NONE program deps) vs_t deps)
o reject_vars thy;
fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
- (fn naming => fn program => fn consts' =>
- check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
+ (fn program => fn consts' =>
+ check_holds_oracle thy (obtain_evaluator' thy NONE program consts'))
o reject_vars thy;
end; (*local*)
@@ -192,23 +195,22 @@
fun evaluation_code thy module_name tycos consts =
let
val ctxt = Proof_Context.init_global thy;
- val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
- val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
+ val program = Code_Thingol.consts_program thy false consts;
val (ml_modules, target_names) =
Code_Target.produce_code_for thy
- target NONE module_name [] naming program (consts' @ tycos');
+ target NONE module_name [] program (map Code_Symbol.Constant consts @ map Code_Symbol.Type_Constructor tycos);
val ml_code = space_implode "\n\n" (map snd ml_modules);
- val (consts'', tycos'') = chop (length consts') target_names;
+ val (consts', tycos') = chop (length consts) target_names;
val consts_map = map2 (fn const =>
fn NONE =>
error ("Constant " ^ (quote o Code.string_of_const thy) const ^
"\nhas a user-defined serialization")
- | SOME const'' => (const, const'')) consts consts''
+ | SOME const' => (const, const')) consts consts'
val tycos_map = map2 (fn tyco =>
fn NONE =>
error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^
"\nhas a user-defined serialization")
- | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
+ | SOME tyco' => (tyco, tyco')) tycos tycos';
in (ml_code, (tycos_map, consts_map)) end;
--- 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
@@ -27,15 +27,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;
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
+ 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 (tyco, tys)
+ of NONE => print_tyco_expr tyvars fxy (Code_Symbol.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 (class, [ty]);
+ fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Code_Symbol.Type_Class class, [ty]);
fun print_tupled_typ tyvars ([], ty) =
print_typ tyvars NOBR ty
| print_tupled_typ tyvars ([ty1], ty2) =
@@ -67,20 +70,24 @@
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 ({ name = c, ... }, _)) => if is_none (const_syntax c)
+ of SOME (app as ({ sym = Code_Symbol.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
| NONE => print_case tyvars some_thm vars fxy case_expr)
and print_app tyvars is_pat some_thm vars fxy
- (app as ({ name = c, typargs, dom, ... }, ts)) =
+ (app as ({ sym, typargs, dom, ... }, ts)) =
let
val k = length ts;
val typargs' = if is_pat then [] else typargs;
- val (l, print') = case const_syntax c
- of NONE => (args_num c, fn fxy => fn ts => gen_applify (is_constr c ) "(" ")"
+ val syntax = case sym of
+ Code_Symbol.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) "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
- NOBR ((str o deresolve) c) typargs') ts)
+ NOBR ((str o deresolve) sym) typargs') ts)
| SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
@@ -137,32 +144,32 @@
|> single
|> enclose "(" ")"
end;
- fun print_context tyvars vs name = applify "[" "]"
+ fun print_context tyvars vs sym = applify "[" "]"
(fn (v, sort) => (Pretty.block o map str)
- (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
- NOBR ((str o deresolve) name) vs;
- fun print_defhead tyvars vars name vs params tys ty =
+ (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
+ NOBR ((str o deresolve) sym) vs;
+ 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 name) (params ~~ tys)) (print_typ tyvars NOBR ty),
+ NOBR (print_context tyvars vs (Code_Symbol.Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
str " ="];
- fun print_def name (vs, ty) [] =
+ fun print_def const (vs, ty) [] =
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
val params = Name.invent (snd reserved) "a" (length tys);
val tyvars = intro_tyvars vs reserved;
val vars = intro_vars params reserved;
in
- concat [print_defhead tyvars vars name vs params tys ty',
- str ("sys.error(\"" ^ name ^ "\")")]
+ concat [print_defhead tyvars vars const vs params tys ty',
+ str ("sys.error(\"" ^ const ^ "\")")]
end
- | print_def name (vs, ty) eqs =
+ | print_def const (vs, ty) eqs =
let
val tycos = fold (fn ((ts, t), _) =>
fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
val tyvars = reserved
|> intro_base_names
- (is_none o tyco_syntax) deresolve tycos
+ (is_none o tyco_syntax) deresolve_tyco tycos
|> intro_tyvars vs;
val simple = case eqs
of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
@@ -188,7 +195,7 @@
tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
str "=>", print_rhs vars' eq]
end;
- val head = print_defhead tyvars vars2 name vs params tys' ty';
+ val head = print_defhead tyvars vars2 const vs params tys' ty';
in if simple then
concat [head, print_rhs vars2 (hd eqs)]
else
@@ -197,34 +204,34 @@
str "match", str "{"], str "}")
(map print_clause eqs)
end;
- val print_method = str o Library.enclose "`" "`" o deresolve_full;
- fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
- print_def name (vs, ty) (filter (snd o snd) raw_eqs)
- | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
+ 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), _)) =
+ print_def const (vs, ty) (filter (snd o snd) raw_eqs)
+ | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
let
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, vs_args), tys) =
concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((concat o map str) ["final", "case", "class", deresolve co]) vs_args)
+ ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
@@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
(Name.invent_names (snd reserved) "a" tys))),
str "extends",
applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((str o deresolve) name) vs
+ ((str o deresolve_tyco) tyco) vs
];
in
Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
- NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
+ NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
:: map print_co cos)
end
- | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
+ | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
let
- val tyvars = intro_tyvars [(v, [name])] reserved;
+ val tyvars = intro_tyvars [(v, [class])] reserved;
fun add_typarg s = Pretty.block
[str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
fun print_super_classes [] = NONE
- | print_super_classes classes = SOME (concat (str "extends"
- :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
+ | print_super_classes classrels = SOME (concat (str "extends"
+ :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels)));
fun print_classparam_val (classparam, ty) =
concat [str "val", constraint (print_method classparam)
((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
@@ -238,22 +245,22 @@
in
concat [str "def", constraint (Pretty.block [applify "(" ")"
(fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
+ (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
(auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
- add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
+ add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=",
applify "(" ")" (str o lookup_var vars) NOBR
(Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
end;
in
Pretty.chunks (
(Pretty.block_enclose
- (concat ([str "trait", (add_typarg o deresolve) name]
- @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
+ (concat ([str "trait", (add_typarg o deresolve_class) class]
+ @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
(map print_classparam_val classparams))
:: map print_classparam_def classparams
)
end
- | print_stmt (name, Code_Thingol.Classinst
+ | print_stmt (sym, Code_Thingol.Classinst
{ class, tyco, vs, inst_params, superinst_params, ... }) =
let
val tyvars = intro_tyvars vs reserved;
@@ -277,13 +284,13 @@
end;
in
Pretty.block_enclose (concat [str "implicit def",
- constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
+ constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
(map print_classparam_instance (inst_params @ superinst_params))
end;
in print_stmt end;
-fun scala_program_of_program ctxt symbol_of module_name reserved identifiers program =
+fun scala_program_of_program ctxt module_name reserved identifiers program =
let
fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
let
@@ -312,49 +319,49 @@
| namify_stmt (Code_Thingol.Classrel _) = namify_object
| namify_stmt (Code_Thingol.Classparam _) = namify_object
| namify_stmt (Code_Thingol.Classinst _) = namify_common false;
- fun memorize_implicits name =
+ fun memorize_implicits sym =
let
fun is_classinst stmt = case stmt
of Code_Thingol.Classinst _ => true
| _ => false;
- val implicits = filter (is_classinst o Graph.get_node program)
- (Graph.immediate_succs program name);
+ val implicits = filter (is_classinst o Code_Symbol.Graph.get_node program)
+ (Code_Symbol.Graph.immediate_succs program sym);
in union (op =) implicits end;
- fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
+ fun modify_stmt (_, Code_Thingol.Fun (_, SOME _)) = NONE
| modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
| modify_stmt (_, Code_Thingol.Classrel _) = NONE
| modify_stmt (_, Code_Thingol.Classparam _) = NONE
| modify_stmt (_, stmt) = SOME stmt;
in
- Code_Namespace.hierarchical_program ctxt symbol_of
+ Code_Namespace.hierarchical_program ctxt
{ module_name = module_name, reserved = reserved, identifiers = identifiers,
empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [],
memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
end;
-fun serialize_scala ctxt { symbol_of, module_name, reserved_syms, identifiers,
+fun serialize_scala ctxt { module_name, reserved_syms, identifiers,
includes, class_syntax, tyco_syntax, const_syntax } program =
let
(* build program *)
val { deresolver, hierarchical_program = scala_program } =
- scala_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
+ scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
(* print statements *)
- fun lookup_constr tyco constr = case Graph.get_node program tyco
- of Code_Thingol.Datatype (_, (_, constrs)) =>
+ fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Constructor tyco)
+ of Code_Thingol.Datatype (_, constrs) =>
the (AList.lookup (op = o apsnd fst) constrs constr);
- fun classparams_of_class class = case Graph.get_node program class
- of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
- fun args_num c = case Graph.get_node program c
- of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
+ fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Code_Symbol.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
+ of Code_Thingol.Fun (((_, ty), []), _) =>
(length o fst o Code_Thingol.unfold_fun) ty
- | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
- | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
- | Code_Thingol.Classparam (_, class) =>
+ | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
+ | Code_Thingol.Datatypecons tyco => length (lookup_constr tyco const)
+ | Code_Thingol.Classparam class =>
(length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
- (classparams_of_class class)) c;
+ (classparams_of_class class)) const;
fun print_stmt prefix_fragments = print_scala_stmt
tyco_syntax const_syntax (make_vars reserved_syms) args_num
(Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []);
@@ -378,7 +385,7 @@
lift_markup = I } scala_program);
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
- fun prepare names width p = ([("", format names width p)], try (deresolver []));
+ fun prepare syms width p = ([("", format syms width p)], try (deresolver []));
in
Code_Target.serialization write prepare p
end;
--- a/src/Tools/Code/code_simp.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_simp.ML Sat Jan 25 23:50:49 2014 +0100
@@ -52,7 +52,7 @@
(* build simpset and conversion from program *)
-fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
+fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss =
ss
|> fold Simplifier.add_simp ((map_filter (fst o snd)) eqs)
|> fold Simplifier.add_cong (the_list some_cong)
@@ -61,7 +61,7 @@
|> fold Simplifier.add_simp (map (fst o snd) inst_params)
| add_stmt _ ss = ss;
-val add_program = Graph.fold (add_stmt o fst o snd);
+val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
fun simp_ctxt_program thy some_ss program =
simp_ctxt_default thy some_ss
@@ -77,7 +77,7 @@
(* evaluation with dynamic code context *)
fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
- (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
+ (fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy);
--- 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
@@ -13,9 +13,12 @@
type symbol = (string, string, class, class * class, string * class, string) attr
structure Table: TABLE;
structure Graph: GRAPH;
- val default_name: Proof.context -> symbol -> string * string
- val quote_symbol: Proof.context -> symbol -> string
- val tyco_fun: string
+ 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
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)
@@ -38,6 +41,8 @@
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 mapped_const_data: (string -> 'a -> 'g) -> ('a, 'b, 'c, 'd, 'e, 'f) data -> 'g Symtab.table
val dest_constant_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'a) list
val dest_type_constructor_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'b) list
val dest_type_class_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (class * 'c) list
@@ -89,40 +94,48 @@
| NONE => (case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => thyname_of_type thy tyco
| NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
- fun base_rel (x, y) = Long_Name.base_name y ^ "_" ^ Long_Name.base_name x;
- fun plainify ctxt get_prefix get_basename thing =
- (get_prefix (Proof_Context.theory_of ctxt) thing,
- Name.desymbolize false (get_basename thing));
+ fun prefix thy (Constant "") = "Code"
+ | prefix thy (Constant c) = thyname_of_const thy c
+ | prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco
+ | 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 default_name ctxt (Constant "==>") =
- plainify ctxt thyname_of_const (K "follows") "==>"
- | default_name ctxt (Constant "==") =
- plainify ctxt thyname_of_const (K "meta_eq") "=="
- | default_name ctxt (Constant c) =
- plainify ctxt thyname_of_const Long_Name.base_name c
- | default_name ctxt (Type_Constructor "fun") =
- plainify ctxt thyname_of_type (K "fun") "fun"
- | default_name ctxt (Type_Constructor tyco) =
- plainify ctxt thyname_of_type Long_Name.base_name tyco
- | default_name ctxt (Type_Class class) =
- plainify ctxt thyname_of_class Long_Name.base_name class
- | default_name ctxt (Class_Relation classrel) =
- plainify ctxt (fn thy => fn (class, _) => thyname_of_class thy class) base_rel classrel
- | default_name ctxt (Class_Instance inst) =
- plainify ctxt thyname_of_instance base_rel inst;
+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;
-val tyco_fun = (uncurry Long_Name.append o default_name @{context}) (Type_Constructor "fun");
+fun namespace_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
+
+fun default_name ctxt sym = (namespace_prefix ctxt sym, base_name sym);
+
+val value = Constant "";
+fun is_value (Constant "") = true
+ | is_value _ = false;
end;
-fun quote_symbol ctxt (Constant c) = quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
- | quote_symbol ctxt (Type_Constructor tyco) = "type " ^ quote (Proof_Context.extern_type ctxt tyco)
- | quote_symbol ctxt (Type_Class class) = "class " ^ quote (Proof_Context.extern_class ctxt class)
- | quote_symbol ctxt (Class_Relation (sub, super)) =
- quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ quote (Proof_Context.extern_class ctxt super)
- | quote_symbol ctxt (Class_Instance (tyco, class)) =
- quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ quote (Proof_Context.extern_class ctxt class);
+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)
+ | quote ctxt (Class_Relation (sub, super)) =
+ Library.quote (Proof_Context.extern_class ctxt sub) ^ " < " ^ Library.quote (Proof_Context.extern_class ctxt super)
+ | quote ctxt (Class_Instance (tyco, class)) =
+ Library.quote (Proof_Context.extern_type ctxt tyco) ^ " :: " ^ Library.quote (Proof_Context.extern_class ctxt class);
+
+fun marker (Constant c) = "CONST " ^ c
+ | marker (Type_Constructor tyco) = "TYPE " ^ tyco
+ | marker (Type_Class class) = "CLASS " ^ class
+ | marker (Class_Relation (sub, super)) = "CLASSREL " ^ sub ^ " < " ^ super
+ | marker (Class_Instance (tyco, class)) = "INSTANCE " ^ tyco ^ " :: " ^ class;
fun map_attr const tyco class classrel inst module (Constant x) = Constant (const x)
| map_attr const tyco class classrel inst module (Type_Constructor x) = Type_Constructor (tyco x)
@@ -199,6 +212,15 @@
| lookup data (Class_Instance x) = lookup_class_instance_data data x
| lookup data (Module x) = lookup_module_data data x;
+fun symbols_of x = (map Constant o Symtab.keys o #constant o dest_data) x
+ @ (map Type_Constructor o Symtab.keys o #type_constructor o dest_data) x
+ @ (map Type_Class o Symtab.keys o #type_class o dest_data) x
+ @ (map Class_Relation o Symreltab.keys o #class_relation o dest_data) x
+ @ (map Class_Instance o Symreltab.keys o #class_instance o dest_data) x
+ @ (map Module o Symtab.keys o #module o dest_data) x;
+
+fun mapped_const_data f x = Symtab.map f ((#constant o dest_data) x);
+
fun dest_constant_data x = (Symtab.dest o #constant o dest_data) x;
fun dest_type_constructor_data x = (Symtab.dest o #type_constructor o dest_data) x;
fun dest_type_class_data x = (Symtab.dest o #type_class o dest_data) x;
--- 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.naming -> Code_Thingol.program -> string list -> unit
+ -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
val produce_code_for: theory -> string -> int option -> string -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list
+ -> Code_Thingol.program -> Code_Symbol.symbol list -> (string * string) list * string option list
val present_code_for: theory -> string -> int option -> string -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
+ -> Code_Thingol.program -> Code_Symbol.symbol list * Code_Symbol.symbol list -> string
val check_code_for: theory -> string -> bool -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
+ -> Code_Thingol.program -> Code_Symbol.symbol 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_Thingol.naming -> string list)
+ val present_code: theory -> string list -> Code_Symbol.symbol 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.naming -> Code_Thingol.program
- -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
+ val evaluator: theory -> string -> Code_Thingol.program
+ -> Code_Symbol.symbol list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-> (string * string) list * string
type serializer
@@ -39,14 +39,14 @@
check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
-> theory -> theory
val extend_target: string *
- (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
+ (string * (Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
val assert_target: theory -> string -> string
val the_literals: theory -> string -> literals
type serialization
val parse_args: 'a parser -> Token.T list -> 'a
val serialization: (int -> Path.T option -> 'a -> unit)
- -> (string list -> int -> 'a -> (string * string) list * (string -> string option))
+ -> (Code_Symbol.symbol list -> int -> 'a -> (string * string) list * (Code_Symbol.symbol -> string option))
-> 'a -> serialization
val set_default_code_width: int -> theory -> theory
@@ -117,7 +117,7 @@
(cert_class thy class, cert_tyco thy tyco);
fun read_inst thy (raw_tyco, raw_class) =
- (read_class thy raw_class, read_tyco thy raw_tyco);
+ (read_tyco thy raw_tyco, read_class thy raw_class);
val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class;
@@ -154,21 +154,21 @@
(* serialization: abstract nonsense to cover different destinies for generated code *)
-datatype destination = Export of Path.T option | Produce | Present of string list;
-type serialization = int -> destination -> ((string * string) list * (string -> string option)) option;
+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;
fun serialization output _ content width (Export some_path) =
(output width some_path content; NONE)
| serialization _ string content width Produce =
string [] width content |> SOME
- | serialization _ string content width (Present stmt_names) =
- string stmt_names width content
+ | serialization _ string content width (Present syms) =
+ string syms width content
|> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str)
|> SOME;
fun export some_path f = (f (Export some_path); ());
fun produce f = the (f Produce);
-fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names)))));
+fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms)))));
(* serializers: functions producing serializations *)
@@ -176,7 +176,6 @@
type serializer = Token.T list
-> Proof.context
-> {
- symbol_of: string -> Code_Symbol.symbol,
module_name: string,
reserved_syms: string list,
identifiers: identifier_data,
@@ -193,7 +192,7 @@
check: { env_var: string, make_destination: Path.T -> Path.T,
make_command: string -> string } }
| Extension of string *
- (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
+ (Code_Thingol.program -> Code_Thingol.program);
(** theory data **)
@@ -311,10 +310,10 @@
of SOME data => data
| NONE => error ("Unknown code target language: " ^ quote target);
in case the_description data
- of Fundamental _ => (K I, data)
+ of Fundamental _ => (I, data)
| Extension (super, modify) => let
val (modify', data') = collapse super
- in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end
+ in (modify' #> modify, merge_target false target (data', data)) end
end;
in collapse end;
@@ -326,68 +325,37 @@
val (modify, data) = collapse_hierarchy thy target;
in (default_width, data, modify) end;
-fun activate_const_syntax thy literals cs_data naming =
- (Symtab.empty, naming)
- |> fold_map (fn (c, data) => fn (tab, naming) =>
- case Code_Thingol.lookup_const naming c
- of SOME name => let
- val (syn, naming') =
- Code_Printer.activate_const_syntax thy literals c data naming
- in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
- | NONE => (NONE, (tab, naming))) cs_data
- |>> map_filter I;
+fun activate_symbol_syntax thy literals printings =
+ (Code_Symbol.symbols_of printings,
+ (Symtab.lookup (Code_Symbol.mapped_const_data (Code_Printer.activate_const_syntax thy literals) printings),
+ Code_Symbol.lookup_type_constructor_data printings, Code_Symbol.lookup_type_class_data printings))
-fun activate_syntax lookup_name things =
- Symtab.empty
- |> fold_map (fn (thing_identifier, data) => fn tab => case lookup_name thing_identifier
- of SOME name => (SOME name, Symtab.update_new (name, data) tab)
- | NONE => (NONE, tab)) things
- |>> map_filter I;
-
-fun activate_symbol_syntax thy literals naming printings =
- let
- val (names_const, (const_syntax, _)) =
- activate_const_syntax thy literals (Code_Symbol.dest_constant_data printings) naming;
- val (names_tyco, tyco_syntax) =
- activate_syntax (Code_Thingol.lookup_tyco naming) (Code_Symbol.dest_type_constructor_data printings);
- val (names_class, class_syntax) =
- activate_syntax (Code_Thingol.lookup_class naming) (Code_Symbol.dest_type_class_data printings);
- val names_inst = map_filter (Code_Thingol.lookup_instance naming o fst)
- (Code_Symbol.dest_class_instance_data printings);
- in
- (names_const @ names_tyco @ names_class @ names_inst,
- (Symtab.lookup const_syntax, Symtab.lookup tyco_syntax, Symtab.lookup class_syntax))
- end;
-
-fun project_program thy names_hidden names1 program2 =
+fun project_program thy syms_hidden syms1 program2 =
let
val ctxt = Proof_Context.init_global thy;
- val names2 = subtract (op =) names_hidden names1;
- val program3 = Graph.restrict (not o member (op =) names_hidden) program2;
- val names4 = Graph.all_succs program3 names2;
+ val syms2 = subtract (op =) syms_hidden syms1;
+ val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
+ val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
val unimplemented = Code_Thingol.unimplemented program3;
val _ =
if null unimplemented then ()
else error ("No code equations for " ^
commas (map (Proof_Context.extern_const ctxt) unimplemented));
- val program4 = Graph.restrict (member (op =) names4) program3;
- in (names4, program4) end;
+ val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
+ in (syms4, program4) end;
fun prepare_serializer thy (serializer : serializer) literals reserved identifiers
- printings module_name args naming proto_program names =
+ printings module_name args proto_program syms =
let
- val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) =
- activate_symbol_syntax thy literals naming printings;
- val (names_all, program) = project_program thy names_hidden names proto_program;
+ val (syms_hidden, (const_syntax, tyco_syntax, class_syntax)) =
+ activate_symbol_syntax thy literals 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 => case Code_Thingol.lookup_const naming c
- of SOME name => member (op =) names_all name
- | NONE => false) cs
+ if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs
then SOME (name, content) else NONE;
val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
in
(serializer args (Proof_Context.init_global thy) {
- symbol_of = Code_Thingol.symbol_of proto_program,
module_name = module_name,
reserved_syms = reserved,
identifiers = identifiers,
@@ -398,7 +366,7 @@
program)
end;
-fun mount_serializer thy target some_width module_name args naming program names =
+fun mount_serializer thy target some_width module_name args program syms =
let
val (default_width, data, modify) = activate_target thy target;
val serializer = case the_description data
@@ -406,15 +374,15 @@
val (prepared_serializer, prepared_program) =
prepare_serializer thy serializer (the_literals thy target)
(the_reserved data) (the_identifiers data) (the_printings data)
- module_name args naming (modify naming program) names
+ module_name args (modify program) syms
val width = the_default default_width some_width;
in (fn program => prepared_serializer program width, prepared_program) end;
-fun invoke_serializer thy target some_width module_name args naming program names =
+fun invoke_serializer thy target some_width module_name args program syms =
let
val check = if module_name = "" then I else check_name true;
val (mounted_serializer, prepared_program) = mount_serializer thy
- target some_width (check module_name) args naming program names;
+ target some_width (check module_name) args program syms;
in mounted_serializer prepared_program end;
fun assert_module_name "" = error "Empty module name not allowed here"
@@ -429,23 +397,23 @@
fun export_code_for thy some_path target some_width module_name args =
export (using_master_directory thy some_path)
- ooo invoke_serializer thy target some_width module_name args;
+ oo invoke_serializer thy target some_width module_name args;
fun produce_code_for thy target some_width module_name args =
let
val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
- in fn naming => fn program => fn names =>
- produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
+ in fn program => fn syms =>
+ produce (serializer program syms) |> apsnd (fn deresolve => map deresolve syms)
end;
fun present_code_for thy target some_width module_name args =
let
val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
- in fn naming => fn program => fn (names, selects) =>
- present selects (serializer naming program names)
+ in fn program => fn (syms, selects) =>
+ present selects (serializer program syms)
end;
-fun check_code_for thy target strict args naming program names_cs =
+fun check_code_for thy target strict args program syms =
let
val { env_var, make_destination, make_command } =
(#check o the_fundamental thy) target;
@@ -453,7 +421,7 @@
let
val destination = make_destination p;
val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
- generatedN args naming program names_cs);
+ generatedN args program syms);
val cmd = make_command generatedN;
in
if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
@@ -468,46 +436,38 @@
else Isabelle_System.with_tmp_dir "Code_Test" ext_check
end;
-fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =
+fun evaluation mounted_serializer prepared_program syms ((vs, ty), t) =
let
val _ = if Code_Thingol.contains_dict_var t then
error "Term to be evaluated contains free dictionaries" else ();
val v' = singleton (Name.variant_list (map fst vs)) "a";
val vs' = (v', []) :: vs;
- val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
- val value_name = "Value.value.value"
+ val ty' = ITyVar v' `-> ty;
val program = prepared_program
- |> Graph.new_node (value_name,
- Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
- |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
+ |> Code_Symbol.Graph.new_node (Code_Symbol.value,
+ Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))
+ |> fold (curry (perhaps o try o
+ Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
val (program_code, deresolve) = produce (mounted_serializer program);
- val value_name' = the (deresolve value_name);
- in (program_code, value_name') end;
+ val value_name = the (deresolve Code_Symbol.value);
+ in (program_code, value_name) end;
-fun evaluator thy target naming program consts =
+fun evaluator thy target program syms =
let
- val (mounted_serializer, prepared_program) = mount_serializer thy
- target NONE generatedN [] naming program consts;
- in evaluation mounted_serializer prepared_program consts end;
+ val (mounted_serializer, prepared_program) =
+ mount_serializer thy target NONE generatedN [] program syms;
+ in evaluation mounted_serializer prepared_program syms end;
end; (* local *)
(* code generation *)
-fun implemented_functions thy naming program =
+fun read_const_exprs thy const_exprs =
let
- val cs = Code_Thingol.unimplemented program;
- val names = map_filter (Code_Thingol.lookup_const naming) cs;
- in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
-
-fun read_const_exprs thy cs =
- let
- val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
- val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2;
- val names3 = implemented_functions thy naming program;
- val cs3 = map_filter (fn (c, name) =>
- if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
+ val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs;
+ val program = Code_Thingol.consts_program thy true cs2;
+ val cs3 = Code_Thingol.implemented_deps program;
in union (op =) cs3 cs1 end;
fun prep_destination "" = NONE
@@ -515,9 +475,9 @@
fun export_code thy cs seris =
let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
+ 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 naming program names_cs) seris;
+ export_code_for thy some_path target NONE module_name args program (map Code_Symbol.Constant cs)) seris;
in () end;
fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
@@ -525,19 +485,19 @@
fun produce_code thy cs target some_width some_module_name args =
let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
- in produce_code_for thy target some_width some_module_name args naming program names_cs end;
+ 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;
-fun present_code thy cs names_stmt target some_width some_module_name args =
+fun present_code thy cs syms target some_width some_module_name args =
let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
- in present_code_for thy target some_width some_module_name args naming program (names_cs, names_stmt naming) end;
+ 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;
fun check_code thy cs seris =
let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
+ val program = Code_Thingol.consts_program thy false cs;
val _ = map (fn ((target, strict), args) =>
- check_code_for thy target strict args naming program names_cs) seris;
+ check_code_for thy target strict args program (map Code_Symbol.Constant cs)) seris;
in () end;
fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
@@ -547,22 +507,22 @@
val parse_const_terms = Scan.repeat1 Args.term
>> (fn ts => fn thy => map (Code.check_const thy) ts);
-fun parse_names category parse internalize lookup =
+fun parse_names category parse internalize mark_symbol =
Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
- >> (fn xs => fn thy => fn naming => map_filter (lookup naming o internalize thy) xs);
+ >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
val parse_consts = parse_names "consts" Args.term
- Code.check_const Code_Thingol.lookup_const;
+ Code.check_const Code_Symbol.Constant;
val parse_types = parse_names "types" (Scan.lift Args.name)
- Sign.intern_type Code_Thingol.lookup_tyco;
+ Sign.intern_type Code_Symbol.Type_Constructor;
val parse_classes = parse_names "classes" (Scan.lift Args.name)
- Sign.intern_class Code_Thingol.lookup_class;
+ Sign.intern_class Code_Symbol.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_class, Sign.intern_type thy raw_tyco))
- Code_Thingol.lookup_instance;
+ (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
+ Code_Symbol.Class_Instance;
in
@@ -574,7 +534,7 @@
(fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
let val thy = Proof_Context.theory_of ctxt in
present_code thy (mk_cs thy)
- (fn naming => maps (fn f => f thy naming) mk_stmtss)
+ (maps (fn f => f thy) mk_stmtss)
target some_width "Example" []
end);
--- 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
@@ -8,6 +8,7 @@
infix 8 `%%;
infix 4 `$;
infix 4 `$$;
+infixr 3 `->;
infixr 3 `|=>;
infixr 3 `|==>;
@@ -15,14 +16,14 @@
sig
type vname = string;
datatype dict =
- Dict of string list * plain_dict
+ Dict of (class * class) list * plain_dict
and plain_dict =
- Dict_Const of string * dict list list
+ Dict_Const of (string * class) * dict list list
| Dict_Var of vname * (int * int);
datatype itype =
`%% of string * itype list
| ITyVar of vname;
- type const = { name: string, typargs: itype list, dicts: dict list list,
+ type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
dom: itype list, range: itype, annotate: bool };
datatype iterm =
IConst of const
@@ -30,6 +31,7 @@
| `$ of iterm * iterm
| `|=> of (vname option * itype) * iterm
| ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
+ val `-> : itype * itype -> itype;
val `$$ : iterm * iterm list -> iterm;
val `|==> : (vname option * itype) list * iterm -> iterm;
type typscheme = (vname * sort) list * itype;
@@ -38,7 +40,6 @@
signature CODE_THINGOL =
sig
include BASIC_CODE_THINGOL
- val fun_tyco: string
val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
val unfold_fun: itype -> itype list * itype
@@ -54,59 +55,50 @@
val is_IAbs: iterm -> bool
val eta_expand: int -> const * iterm list -> iterm
val contains_dict_var: iterm -> bool
- val add_constnames: iterm -> string list -> string list
+ val add_constsyms: iterm -> Code_Symbol.symbol list -> Code_Symbol.symbol list
val add_tyconames: iterm -> string list -> string list
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
- type naming
- val empty_naming: naming
- val lookup_class: naming -> class -> string option
- val lookup_classrel: naming -> class * class -> string option
- val lookup_tyco: naming -> string -> string option
- val lookup_instance: naming -> class * string -> string option
- val lookup_const: naming -> string -> string option
- val ensure_declared_const: theory -> string -> naming -> string * naming
-
datatype stmt =
- NoStmt of string
- | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
- | Datatype of string * (vname list *
- ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
- | Datatypecons of string * string
- | Class of class * (vname * ((class * string) list * (string * itype) list))
+ NoStmt
+ | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
+ | Datatype of vname list *
+ ((string * vname list (*type argument wrt. canonical order*)) * itype list) list
+ | Datatypecons of string
+ | Class of vname * ((class * class) list * (string * itype) list)
| Classrel of class * class
- | Classparam of string * class
+ | Classparam of class
| Classinst of { class: string, tyco: string, vs: (vname * sort) list,
- superinsts: (class * (string * (string * dict list list))) list,
+ superinsts: (class * dict list list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
- type program = stmt Graph.T
+ type program = stmt Code_Symbol.Graph.T
val unimplemented: program -> string list
+ 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 -> string -> bool
+ val is_constr: program -> Code_Symbol.symbol -> bool
val is_case: stmt -> bool
- val symbol_of: program -> string -> Code_Symbol.symbol;
val group_stmts: theory -> program
- -> ((string * stmt) list * (string * stmt) list
- * ((string * stmt) list * (string * stmt) list)) list
+ -> ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list
+ * ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list)) list
val read_const_exprs: theory -> string list -> string list * string list
- val consts_program: theory -> bool -> string list -> string list * (naming * program)
- val dynamic_conv: theory -> (naming -> program
- -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ val consts_program: theory -> bool -> string list -> program
+ val dynamic_conv: theory -> (program
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
-> conv
- val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
- -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+ val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
-> term -> 'a
- val static_conv: theory -> string list -> (naming -> program -> string list
- -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ val static_conv: theory -> string list -> (program -> string list
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol 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 ->
- (naming -> program -> string list
- -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+ (program -> string list
+ -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
-> term -> 'a
end;
@@ -133,16 +125,29 @@
type vname = string;
datatype dict =
- Dict of string list * plain_dict
+ Dict of (class * class) list * plain_dict
and plain_dict =
- Dict_Const of string * dict list list
+ Dict_Const of (string * class) * dict list list
| Dict_Var of vname * (int * int);
datatype itype =
`%% of string * itype list
| ITyVar of vname;
-type const = { name: string, typargs: itype list, dicts: dict list list,
+fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
+
+val unfold_fun = unfoldr
+ (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
+ | _ => NONE);
+
+fun unfold_fun_n n ty =
+ let
+ val (tys1, ty1) = unfold_fun ty;
+ val (tys3, tys2) = chop n tys1;
+ val ty3 = Library.foldr (op `->) (tys2, ty1);
+ in (tys3, ty3) end;
+
+type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
dom: itype list, range: itype, annotate: bool };
datatype iterm =
@@ -191,7 +196,7 @@
#> fold (fn (p, body) => fold' p #> fold' body) clauses
in fold' end;
-val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
+val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym);
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
| add_tycos (ITyVar _) = I;
@@ -238,15 +243,15 @@
val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
-fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
+fun eta_expand k (const as { dom = tys, ... }, ts) =
let
val j = length ts;
val l = k - j;
val _ = if l > length tys
- then error ("Impossible eta-expansion for constant " ^ quote c) else ();
- val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
+ then error "Impossible eta-expansion" else ();
+ val vars = (fold o fold_varnames) Name.declare ts Name.context;
val vs_tys = (map o apfst) SOME
- (Name.invent_names ctxt "a" ((take l o drop j) tys));
+ (Name.invent_names vars "a" ((take l o drop j) tys));
in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
fun contains_dict_var t =
@@ -262,178 +267,31 @@
in cont_term t end;
-(** namings **)
-
-(* policies *)
-
-local
- fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
- fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
- fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy (swap inst)
- of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
- | thyname :: _ => thyname;
- fun thyname_of_const thy c = case Axclass.class_of_param thy c
- of SOME class => thyname_of_class thy class
- | NONE => (case Code.get_type_of_constr_or_abstr thy c
- of SOME (tyco, _) => thyname_of_type thy tyco
- | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
- fun namify thy get_basename get_thyname name =
- let
- val prefix = get_thyname thy name;
- val base = (Name.desymbolize false o get_basename) name;
- in Long_Name.append prefix base end;
-in
-
-fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
-fun namify_classrel thy = namify thy (fn (sub_class, super_class) =>
- Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class)
- (fn thy => thyname_of_class thy o fst);
- (*order fits nicely with composed projections*)
-fun namify_tyco thy "fun" = "Pure.fun"
- | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_type tyco;
-fun namify_instance thy = namify thy (fn (class, tyco) =>
- Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
-fun namify_const thy "==>" = "Pure.follows"
- | namify_const thy "==" = "Pure.meta_eq"
- | namify_const thy c = namify thy Long_Name.base_name thyname_of_const c;
-
-end; (* local *)
-
-
-(* data *)
-
-datatype naming = Naming of {
- class: class Symtab.table * Name.context,
- classrel: string Symreltab.table * Name.context,
- tyco: string Symtab.table * Name.context,
- instance: string Symreltab.table * Name.context,
- const: string Symtab.table * Name.context
-}
-
-fun dest_Naming (Naming naming) = naming;
-
-val empty_naming = Naming {
- class = (Symtab.empty, Name.context),
- classrel = (Symreltab.empty, Name.context),
- tyco = (Symtab.empty, Name.context),
- instance = (Symreltab.empty, Name.context),
- const = (Symtab.empty, Name.context)
-};
-
-local
- fun mk_naming (class, classrel, tyco, instance, const) =
- Naming { class = class, classrel = classrel,
- tyco = tyco, instance = instance, const = const };
- fun map_naming f (Naming { class, classrel, tyco, instance, const }) =
- mk_naming (f (class, classrel, tyco, instance, const));
-in
- fun map_class f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (f class, classrel, tyco, inst, const));
- fun map_classrel f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (class, f classrel, tyco, inst, const));
- fun map_tyco f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (class, classrel, f tyco, inst, const));
- fun map_instance f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (class, classrel, tyco, f inst, const));
- fun map_const f = map_naming
- (fn (class, classrel, tyco, inst, const) =>
- (class, classrel, tyco, inst, f const));
-end; (*local*)
-
-fun add_variant update (thing, name) (tab, used) =
- let
- val (name', used') = Name.variant name used;
- val tab' = update (thing, name') tab;
- in (tab', used') end;
-
-fun declare thy mapp lookup update namify thing =
- mapp (add_variant update (thing, namify thy thing))
- #> `(fn naming => the (lookup naming thing));
-
-
-(* lookup and declare *)
-
-local
-
-val suffix_class = "class";
-val suffix_classrel = "classrel"
-val suffix_tyco = "tyco";
-val suffix_instance = "inst";
-val suffix_const = "const";
-
-fun add_suffix nsp NONE = NONE
- | add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp);
-
-in
-
-val lookup_class = add_suffix suffix_class
- oo Symtab.lookup o fst o #class o dest_Naming;
-val lookup_classrel = add_suffix suffix_classrel
- oo Symreltab.lookup o fst o #classrel o dest_Naming;
-val lookup_tyco = add_suffix suffix_tyco
- oo Symtab.lookup o fst o #tyco o dest_Naming;
-val lookup_instance = add_suffix suffix_instance
- oo Symreltab.lookup o fst o #instance o dest_Naming;
-val lookup_const = add_suffix suffix_const
- oo Symtab.lookup o fst o #const o dest_Naming;
-
-fun declare_class thy = declare thy map_class
- lookup_class Symtab.update_new namify_class;
-fun declare_classrel thy = declare thy map_classrel
- lookup_classrel Symreltab.update_new namify_classrel;
-fun declare_tyco thy = declare thy map_tyco
- lookup_tyco Symtab.update_new namify_tyco;
-fun declare_instance thy = declare thy map_instance
- lookup_instance Symreltab.update_new namify_instance;
-fun declare_const thy = declare thy map_const
- lookup_const Symtab.update_new namify_const;
-
-fun ensure_declared_const thy const naming =
- case lookup_const naming const
- of SOME const' => (const', naming)
- | NONE => declare_const thy const naming;
-
-val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco
- (*depends on add_suffix*);
-
-val unfold_fun = unfoldr
- (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
- | _ => NONE);
-
-fun unfold_fun_n n ty =
- let
- val (tys1, ty1) = unfold_fun ty;
- val (tys3, tys2) = chop n tys1;
- val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1);
- in (tys3, ty3) end;
-
-end; (* local *)
-
-
(** statements, abstract programs **)
type typscheme = (vname * sort) list * itype;
datatype stmt =
- NoStmt of string
- | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
- | Datatype of string * (vname list * ((string * vname list) * itype list) list)
- | Datatypecons of string * string
- | Class of class * (vname * ((class * string) list * (string * itype) list))
+ NoStmt
+ | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
+ | Datatype of vname list * ((string * vname list) * itype list) list
+ | Datatypecons of string
+ | Class of vname * ((class * class) list * (string * itype) list)
| Classrel of class * class
- | Classparam of string * class
+ | Classparam of class
| Classinst of { class: string, tyco: string, vs: (vname * sort) list,
- superinsts: (class * (string * (string * dict list list))) list,
+ superinsts: (class * dict list list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
-type program = stmt Graph.T;
+type program = stmt Code_Symbol.Graph.T;
fun unimplemented program =
- Graph.fold (fn (_, (NoStmt c, _)) => cons c | _ => I) program [];
+ Code_Symbol.Graph.fold (fn (Code_Symbol.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);
fun map_terms_bottom_up f (t as IConst _) = f t
| map_terms_bottom_up f (t as IVar _) = f t
@@ -449,9 +307,9 @@
fun map_classparam_instances_as_term f =
(map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
-fun map_terms_stmt f (NoStmt c) = (NoStmt c)
- | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
- (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
+fun map_terms_stmt f NoStmt = NoStmt
+ | map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst)
+ (fn (ts, t) => (map f ts, f t)) eqs), case_cong)
| map_terms_stmt f (stmt as Datatype _) = stmt
| map_terms_stmt f (stmt as Datatypecons _) = stmt
| map_terms_stmt f (stmt as Class _) = stmt
@@ -463,41 +321,16 @@
inst_params = map_classparam_instances_as_term f inst_params,
superinst_params = map_classparam_instances_as_term f superinst_params };
-fun is_constr program name = case Graph.get_node program name
+fun is_constr program sym = case Code_Symbol.Graph.get_node program sym
of Datatypecons _ => true
| _ => false;
-fun is_case (Fun (_, (_, SOME _))) = true
+fun is_case (Fun (_, SOME _)) = true
| is_case _ = false;
-fun symbol_of program name =
- case try (Graph.get_node program) name of
- NONE => Code_Symbol.Module "(unknown)"
- (*FIXME: need to be liberal due to ad-hoc introduction of value for evaluation*)
- | SOME stmt => case stmt of
- Fun (c, _) => Code_Symbol.Constant c
- | Datatype (tyco, _) => Code_Symbol.Type_Constructor tyco
- | Datatypecons (c, _) => Code_Symbol.Constant c
- | Class (class, _) => Code_Symbol.Type_Class class
- | Classrel (sub, super) =>
- let
- val Class (sub, _) = Graph.get_node program sub;
- val Class (super, _) = Graph.get_node program super;
- in
- Code_Symbol.Class_Relation (sub, super)
- end
- | Classparam (c, _) => Code_Symbol.Constant c
- | Classinst { class, tyco, ... } =>
- let
- val Class (class, _) = Graph.get_node program class;
- val Datatype (tyco, _) = Graph.get_node program tyco;
- in
- Code_Symbol.Class_Instance (tyco, class)
- end;
-
fun linear_stmts program =
- rev (Graph.strong_conn program)
- |> map (AList.make (Graph.get_node program));
+ rev (Code_Symbol.Graph.strong_conn program)
+ |> map (AList.make (Code_Symbol.Graph.get_node program));
fun group_stmts thy program =
let
@@ -516,8 +349,8 @@
else if forall (is_fun orf is_classinst) stmts
then ([], [], List.partition is_fun stmts)
else error ("Illegal mutual dependencies: " ^ (commas
- o map (Code_Symbol.quote_symbol (Proof_Context.init_global thy)
- o symbol_of program o fst)) stmts);
+ o map (Code_Symbol.quote (Proof_Context.init_global thy)
+ o fst)) stmts);
in
linear_stmts program
|> map group
@@ -528,31 +361,27 @@
(* generic mechanisms *)
-fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
+fun ensure_stmt symbolize generate x (dep, program) =
let
- fun add_dep name = case dep of NONE => I
- | SOME dep => Graph.add_edge (dep, name);
- val (name, naming') = case lookup naming thing
- of SOME name => (name, naming)
- | NONE => declare thing naming;
+ val sym = symbolize x;
+ val add_dep = case dep of NONE => I
+ | SOME dep => Code_Symbol.Graph.add_edge (dep, sym);
in
- if can (Graph.get_node program) name
+ if can (Code_Symbol.Graph.get_node program) sym
then
program
- |> add_dep name
- |> pair naming'
+ |> add_dep
|> pair dep
- |> pair name
+ |> pair x
else
program
- |> Graph.default_node (name, NoStmt "")
- |> add_dep name
- |> pair naming'
- |> curry generate (SOME name)
+ |> Code_Symbol.Graph.default_node (sym, NoStmt)
+ |> add_dep
+ |> curry generate (SOME sym)
||> snd
- |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
+ |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt))
|> pair dep
- |> pair name
+ |> pair x
end;
exception PERMISSIVE of unit;
@@ -582,10 +411,6 @@
(err_typ ^ "\n" ^ err_class)
end;
-fun undefineds thy (dep, (naming, program)) =
- (map_filter (lookup_const naming) (Code.undefineds thy),
- (dep, (naming, program)));
-
(* inference of type annotations for disambiguation with type classes *)
@@ -640,18 +465,18 @@
ensure_const thy algbr eqngr permissive c
##>> pair (map (unprefix "'" o fst) vs)
##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
- #>> (fn info => Datatype (tyco, info));
- in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
+ #>> Datatype;
+ in ensure_stmt Code_Symbol.Type_Constructor stmt_datatype tyco end
and ensure_const thy algbr eqngr permissive c =
let
fun stmt_datatypecons tyco =
ensure_tyco thy algbr eqngr permissive tyco
- #>> (fn tyco => Datatypecons (c, tyco));
+ #>> Datatypecons;
fun stmt_classparam class =
ensure_class thy algbr eqngr permissive class
- #>> (fn class => Classparam (c, class));
+ #>> Classparam;
fun stmt_fun cert = case Code.equations_of_cert thy cert
- of (_, NONE) => pair (NoStmt c)
+ of (_, NONE) => pair NoStmt
| ((vs, ty), SOME eqns) =>
let
val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
@@ -661,34 +486,34 @@
##>> translate_typ thy algbr eqngr permissive ty
##>> translate_eqns thy algbr eqngr permissive eqns'
#>>
- (fn (_, NONE) => NoStmt c
- | (tyscm, SOME eqns) => Fun (c, ((tyscm, eqns), some_case_cong)))
+ (fn (_, NONE) => NoStmt
+ | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong))
end;
val stmt_const = case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => stmt_datatypecons tyco
| 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 lookup_const (declare_const thy) stmt_const c end
+ in ensure_stmt Code_Symbol.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;
val cs = #params (Axclass.get_info thy class);
val stmt_class =
- fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
- ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
+ fold_map (fn super_class =>
+ ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
##>> translate_typ thy algbr eqngr permissive ty) cs
- #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
- in ensure_stmt lookup_class (declare_class thy) stmt_class class end
+ #>> (fn info => Class (unprefix "'" Name.aT, info))
+ in ensure_stmt Code_Symbol.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 lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end
-and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
+ in ensure_stmt Code_Symbol.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;
val these_class_params = these o try (#params o Axclass.get_info thy);
@@ -703,10 +528,8 @@
val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
fun translate_super_instance super_class =
ensure_class thy algbr eqngr permissive super_class
- ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
- #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) =>
- (super_class, (classrel, (inst, dss))));
+ #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss));
fun translate_classparam_instance (c, ty) =
let
val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
@@ -729,7 +552,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 lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
+ in ensure_stmt Code_Symbol.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)) =
@@ -781,7 +604,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 { name = c, typargs = typargs, dicts = dss,
+ IConst { sym = Code_Symbol.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) =
@@ -790,6 +613,7 @@
#>> (fn (t, ts) => t `$$ ts)
and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
+ val undefineds = Code.undefineds thy;
fun arg_types num_args ty = fst (chop num_args (binder_types ty));
val tys = arg_types num_args (snd c_ty);
val ty = nth tys t_pos;
@@ -801,11 +625,11 @@
val constrs =
if null case_pats then []
else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
- fun casify undefineds constrs ty t_app ts =
+ fun casify constrs ty t_app ts =
let
fun collapse_clause vs_map ts body =
case body
- of IConst { name = c, ... } => if member (op =) undefineds c
+ of IConst { sym = Code_Symbol.Constant c, ... } => if member (op =) undefineds c
then []
else [(ts, body)]
| ICase { term = IVar (SOME v), clauses = clauses, ... } =>
@@ -839,9 +663,8 @@
#>> rpair n) constrs
##>> translate_typ thy algbr eqngr permissive ty
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
- ##>> undefineds thy
- #>> (fn ((((t, constrs), ty), ts), undefineds) =>
- casify undefineds constrs ty t ts)
+ #>> (fn (((t, constrs), ty), ts) =>
+ casify constrs ty t ts)
end
and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
if length ts < num_args then
@@ -873,12 +696,12 @@
datatype typarg_witness =
Weakening of (class * class) list * plain_typarg_witness
and plain_typarg_witness =
- Global of (class * string) * typarg_witness list list
+ Global of (string * class) * typarg_witness list list
| Local of string * (int * sort);
fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
Weakening ((sub_class, super_class) :: classrels, x);
fun type_constructor (tyco, _) dss class =
- Weakening ([], Global ((class, tyco), (map o map) fst dss));
+ Weakening ([], Global ((tyco, class), (map o map) fst dss));
fun type_variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
@@ -905,31 +728,33 @@
structure Program = Code_Data
(
- type T = naming * program;
- val empty = (empty_naming, Graph.empty);
+ type T = program;
+ val empty = Code_Symbol.Graph.empty;
);
fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
Program.change_yield (if ignore_cache then NONE else SOME thy)
- (fn naming_program => (NONE, naming_program)
+ (fn program => (NONE, program)
|> generate thy algebra eqngr thing
- |-> (fn thing => fn (_, naming_program) => (thing, naming_program)));
+ |-> (fn thing => fn (_, program) => (thing, program)));
(* program generation *)
fun consts_program thy permissive consts =
let
- fun project_consts consts (naming, program) =
- if permissive then (consts, (naming, program))
- else (consts, (naming, Graph.restrict
- (member (op =) (Graph.all_succs program consts)) program));
+ fun project program =
+ if permissive then program
+ else Code_Symbol.Graph.restrict
+ (member (op =) (Code_Symbol.Graph.all_succs program
+ (map Code_Symbol.Constant consts))) program;
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr permissive);
in
invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
generate_consts consts
- |-> project_consts
+ |> snd
+ |> project
end;
@@ -941,23 +766,24 @@
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 stmt_value =
fold_map (translate_tyvar_sort thy algbr eqngr false) vs
##>> translate_typ thy algbr eqngr false ty
##>> translate_term thy algbr eqngr false NONE (t', NONE)
#>> (fn ((vs, ty), t) => Fun
- (@{const_name dummy_pattern}, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
- fun term_value (dep, (naming, program1)) =
+ (((vs, ty), [(([], t), (NONE, true))]), NONE));
+ fun term_value (dep, program1) =
let
- val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
- Graph.get_node program1 @{const_name dummy_pattern};
- val deps = Graph.immediate_succs program1 @{const_name dummy_pattern};
- val program2 = Graph.del_node @{const_name dummy_pattern} program1;
- val deps_all = Graph.all_succs program2 deps;
- val program3 = Graph.restrict (member (op =) deps_all) program2;
- in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
+ val Fun ((vs_ty, [(([], t), _)]), _) =
+ Code_Symbol.Graph.get_node program1 dummy_constant;
+ val deps = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
+ val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
+ val deps_all = Code_Symbol.Graph.all_succs program2 deps;
+ val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
+ in ((program3, ((vs_ty, t), deps)), (dep, program2)) end;
in
- ensure_stmt ((K o K) NONE) pair stmt_value @{const_name dummy_pattern}
+ ensure_stmt Code_Symbol.Constant stmt_value @{const_name dummy_pattern}
#> snd
#> term_value
end;
@@ -967,9 +793,9 @@
fun dynamic_evaluator thy evaluator algebra eqngr vs t =
let
- val (((naming, program), (((vs', ty'), t'), deps)), _) =
+ val ((program, (((vs', ty'), t'), deps)), _) =
invoke_generation false thy (algebra, eqngr) ensure_value t;
- in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end;
+ in evaluator program ((original_sorts vs vs', (vs', ty')), t') deps end;
fun dynamic_conv thy evaluator =
Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator);
@@ -977,26 +803,26 @@
fun dynamic_value thy postproc evaluator =
Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
-fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
+fun lift_evaluation thy evaluation' algebra eqngr program vs t =
let
- val (((_, _), (((vs', ty'), t'), deps)), _) =
- ensure_value thy algebra eqngr t (NONE, (naming, program));
+ val ((_, (((vs', ty'), t'), deps)), _) =
+ ensure_value thy algebra eqngr t (NONE, program);
in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
fun lift_evaluator thy evaluator' consts algebra eqngr =
let
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr false);
- val (consts', (naming, program)) =
+ val (consts', program) =
invoke_generation true thy (algebra, eqngr) generate_consts consts;
- val evaluation' = evaluator' naming program consts';
- in lift_evaluation thy evaluation' algebra eqngr naming program end;
+ val evaluation' = evaluator' program consts';
+ in lift_evaluation thy evaluation' algebra eqngr program end;
fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
let
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr false);
- val (_, (_, program)) =
+ val (_, program) =
invoke_generation true thy (algebra, eqngr) generate_consts consts;
in evaluator' program 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,11 @@
val univs_cookie = (Univs.get, put_result, name_put);
-val sloppy_name = Long_Name.base_name o Long_Name.qualifier
+val sloppy_name = Code_Symbol.base_name;
-fun nbe_fun idx_of 0 "" = "nbe_value"
- | nbe_fun idx_of i c = "c_" ^ string_of_int (idx_of c)
- ^ "_" ^ sloppy_name c ^ "_" ^ string_of_int i;
+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;
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
fun nbe_bound v = "v_" ^ v;
fun nbe_bound_optional NONE = "_"
@@ -291,24 +291,24 @@
in (c, (num_args, (dicts, eqns))) end;
val eqnss' = map prep_eqns eqnss;
- fun assemble_constapp c dss ts =
+ fun assemble_constapp sym dss ts =
let
val ts' = (maps o map) assemble_dict dss @ ts;
- in case AList.lookup (op =) eqnss' c
+ in case AList.lookup (op =) eqnss' sym
of SOME (num_args, _) => if num_args <= length ts'
then let val (ts1, ts2) = chop num_args ts'
- in nbe_apps (nbe_apps_local idx_of 0 c ts1) ts2
- end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 c)) ts'
- | NONE => if member (op =) deps c
- then nbe_apps (nbe_fun idx_of 0 c) ts'
- else nbe_apps_constr idx_of c ts'
+ in nbe_apps (nbe_apps_local idx_of 0 sym ts1) ts2
+ end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts'
+ | NONE => if member (op =) deps sym
+ then nbe_apps (nbe_fun idx_of 0 sym) ts'
+ else nbe_apps_constr idx_of sym ts'
end
and assemble_classrels classrels =
- fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
+ fold_rev (fn classrel => assemble_constapp (Code_Symbol.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 inst dss []
+ assemble_constapp (Code_Symbol.Class_Instance inst) dss []
| assemble_plain_dict (Dict_Var (v, (n, _))) =
nbe_dict v n
@@ -318,7 +318,7 @@
let
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
- and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts
+ and of_iapp match_cont (IConst { sym, dicts = dss, ... }) ts = constapp sym dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
@@ -353,12 +353,12 @@
val (args', _) = fold_map subst_vars args samepairs;
in (samepairs, args') end;
- fun assemble_eqn c dicts default_args (i, (args, rhs)) =
+ fun assemble_eqn sym dicts default_args (i, (args, rhs)) =
let
- val match_cont = if c = "" then NONE
- else SOME (nbe_apps_local idx_of (i + 1) c (dicts @ default_args));
+ val match_cont = if Code_Symbol.is_value sym then NONE
+ else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args));
val assemble_arg = assemble_iterm
- (fn c => fn dss => fn ts => nbe_apps_constr idx_of c ((maps o map) (K "_") dss @ ts)) NONE;
+ (fn sym' => fn dss => fn ts => nbe_apps_constr idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE;
val assemble_rhs = assemble_iterm assemble_constapp match_cont;
val (samepairs, args') = subst_nonlin_vars args;
val s_args = map assemble_arg args';
@@ -370,17 +370,17 @@
| SOME default_rhs =>
[([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),
([ml_list (rev (dicts @ default_args))], default_rhs)]
- in (nbe_fun idx_of i c, eqns) end;
+ in (nbe_fun idx_of i sym, eqns) end;
- fun assemble_eqns (c, (num_args, (dicts, eqns))) =
+ fun assemble_eqns (sym, (num_args, (dicts, eqns))) =
let
val default_args = map nbe_default
(Name.invent Name.context "a" (num_args - length dicts));
- val eqns' = map_index (assemble_eqn c dicts default_args) eqns
- @ (if c = "" then [] else [(nbe_fun idx_of (length eqns) c,
+ val eqns' = map_index (assemble_eqn sym dicts default_args) eqns
+ @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym,
[([ml_list (rev (dicts @ default_args))],
- nbe_apps_constr idx_of c (dicts @ default_args))])]);
- in (eqns', nbe_abss num_args (nbe_fun idx_of 0 c)) end;
+ nbe_apps_constr idx_of sym (dicts @ default_args))])]);
+ in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end;
val (fun_vars, fun_vals) = map_split assemble_eqns eqnss';
val deps_vars = ml_list (map (nbe_fun idx_of 0) deps);
@@ -394,9 +394,9 @@
let
val ctxt = Proof_Context.init_global thy;
val (deps, deps_vals) = split_list (map_filter
- (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps);
+ (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Code_Symbol.Graph.get_node nbe_program dep)))) raw_deps);
val idx_of = raw_deps
- |> map (fn dep => (dep, snd (Graph.get_node nbe_program dep)))
+ |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep)))
|> AList.lookup (op =)
|> (fn f => the o f);
val s = assemble_eqnss idx_of deps eqnss;
@@ -413,45 +413,45 @@
(* extract equations from statements *)
-fun dummy_const c dss =
- IConst { name = c, typargs = [], dicts = dss,
+fun dummy_const sym dss =
+ IConst { sym = sym, typargs = [], dicts = dss,
dom = [], range = ITyVar "", annotate = false };
-fun eqns_of_stmt (_, Code_Thingol.NoStmt _) =
+fun eqns_of_stmt (_, Code_Thingol.NoStmt) =
[]
- | eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
+ | eqns_of_stmt (_, Code_Thingol.Fun ((_, []), _)) =
[]
- | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
- [(const, (vs, map fst eqns))]
+ | eqns_of_stmt (sym_const, Code_Thingol.Fun (((vs, _), eqns), _)) =
+ [(sym_const, (vs, map fst eqns))]
| eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
[]
| eqns_of_stmt (_, Code_Thingol.Datatype _) =
[]
- | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
+ | eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) =
let
- val names = map snd super_classes @ map fst classparams;
- val params = Name.invent Name.context "d" (length names);
- fun mk (k, name) =
- (name, ([(v, [])],
- [([dummy_const class [] `$$ map (IVar o SOME) params],
+ val syms = map Code_Symbol.Class_Relation classrels @ map (Code_Symbol.Constant o fst) classparams;
+ val params = Name.invent Name.context "d" (length syms);
+ fun mk (k, sym) =
+ (sym, ([(v, [])],
+ [([dummy_const sym_class [] `$$ map (IVar o SOME) params],
IVar (SOME (nth params k)))]));
- in map_index mk names end
+ in map_index mk syms end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
[]
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
- | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
- [(inst, (vs, [([], dummy_const class [] `$$
- map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
+ | 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
@ map (IConst o fst o snd o fst) inst_params)]))];
(* compile whole programs *)
fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) =
- if can (Graph.get_node nbe_program) name
+ if can (Code_Symbol.Graph.get_node nbe_program) name
then (nbe_program, (maxidx, idx_tab))
- else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
+ else (Code_Symbol.Graph.new_node (name, (NONE, maxidx)) nbe_program,
(maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
fun compile_stmts thy stmts_deps =
@@ -468,20 +468,20 @@
|> rpair nbe_program;
in
fold ensure_const_idx refl_deps
- #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
+ #> apfst (fold (fn (name, deps) => fold (curry Code_Symbol.Graph.add_edge name) deps) names_deps
#> compile
- #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
+ #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ))))
end;
fun compile_program thy program =
let
- fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) nbe_program) names
+ fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names
then (nbe_program, (maxidx, idx_tab))
else (nbe_program, (maxidx, idx_tab))
- |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
- Graph.immediate_succs program name)) names);
+ |> compile_stmts thy (map (fn name => ((name, Code_Symbol.Graph.get_node program name),
+ Code_Symbol.Graph.immediate_succs program name)) names);
in
- fold_rev add_stmts (Graph.strong_conn program)
+ fold_rev add_stmts (Code_Symbol.Graph.strong_conn program)
end;
@@ -493,7 +493,7 @@
let
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
in
- ("", (vs, [([], t)]))
+ (Code_Symbol.value, (vs, [([], t)]))
|> singleton (compile_eqnss thy nbe_program deps)
|> snd
|> (fn t => apps t (rev dict_frees))
@@ -502,43 +502,35 @@
(* reconstruction *)
-fun typ_of_itype program vs (ityco `%% itys) =
- let
- val Code_Thingol.Datatype (tyco, _) = Graph.get_node program ityco;
- in Type (tyco, map (typ_of_itype program vs) itys) end
- | typ_of_itype program vs (ITyVar v) =
- let
- val sort = (the o AList.lookup (op =) vs) v;
- in TFree ("'" ^ v, sort) end;
+fun typ_of_itype vs (tyco `%% itys) =
+ Type (tyco, map (typ_of_itype vs) itys)
+ | typ_of_itype vs (ITyVar v) =
+ TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
-fun term_of_univ thy program idx_tab t =
+fun term_of_univ thy idx_tab t =
let
fun take_until f [] = []
- | take_until f (x::xs) = if f x then [] else x :: take_until f xs;
- fun is_dict (Const (idx, _)) = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
- of Code_Thingol.Class _ => true
- | Code_Thingol.Classrel _ => true
- | Code_Thingol.Classinst _ => true
- | _ => false)
+ | 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
+ | _ => true)
| is_dict (DFree _) = true
| is_dict _ = false;
- fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx
- of Code_Thingol.NoStmt c => c
- | Code_Thingol.Fun (c, _) => c
- | Code_Thingol.Datatypecons (c, _) => c
- | Code_Thingol.Classparam (c, _) => c);
+ fun const_of_idx idx =
+ case Inttab.lookup idx_tab idx of SOME (Code_Symbol.Constant const) => const;
fun of_apps bounds (t, ts) =
fold_map (of_univ bounds) ts
#>> (fn ts' => list_comb (t, rev ts'))
and of_univ bounds (Const (idx, ts)) typidx =
let
val ts' = take_until is_dict ts;
- val c = const_of_idx idx;
+ val const = const_of_idx idx;
val T = map_type_tvar (fn ((v, i), _) =>
Type_Infer.param typidx (v ^ string_of_int i, []))
- (Sign.the_const_type thy c);
+ (Sign.the_const_type thy const);
val typidx' = typidx + 1;
- in of_apps bounds (Term.Const (c, T), ts') typidx' end
+ in of_apps bounds (Term.Const (const, T), ts') typidx' end
| of_univ bounds (BVar (n, ts)) typidx =
of_apps bounds (Bound (bounds - n - 1), ts) typidx
| of_univ bounds (t as Abs _) typidx =
@@ -550,11 +542,11 @@
(* evaluation with type reconstruction *)
-fun eval_term thy program (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+fun eval_term thy (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
let
val ctxt = Syntax.init_pretty_global thy;
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
- val ty' = typ_of_itype program vs0 ty;
+ val ty' = typ_of_itype vs0 ty;
fun type_infer t =
Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
(Type.constraint ty' t);
@@ -563,7 +555,7 @@
else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
in
compile_term thy nbe_program deps (vs, t)
- |> term_of_univ thy program idx_tab
+ |> term_of_univ thy idx_tab
|> traced (fn t => "Normalized:\n" ^ string_of_term t)
|> type_infer
|> traced (fn t => "Types inferred:\n" ^ string_of_term t)
@@ -576,8 +568,8 @@
structure Nbe_Functions = Code_Data
(
- type T = (Univ option * int) Graph.T * (int * string Inttab.table);
- val empty = (Graph.empty, (0, Inttab.empty));
+ type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.symbol Inttab.table);
+ val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
);
fun compile ignore_cache thy program =
@@ -599,26 +591,23 @@
val (_, raw_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (@{binding normalization_by_evaluation},
- fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
- mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
+ fn (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
+ mk_equals thy ct (eval_term thy nbe_program_idx_tab vsp_ty_t deps))));
-fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
- raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
+fun oracle thy nbe_program_idx_tab vsp_ty_t deps ct =
+ raw_oracle (thy, nbe_program_idx_tab, vsp_ty_t, deps, ct);
-fun dynamic_conv thy = lift_triv_classes_conv thy (Code_Thingol.dynamic_conv thy
- (K (fn program => oracle thy program (compile false thy program))));
+fun dynamic_conv thy = lift_triv_classes_conv thy
+ (Code_Thingol.dynamic_conv thy (oracle thy o compile false thy));
fun dynamic_value thy = lift_triv_classes_rew thy
- (Code_Thingol.dynamic_value thy I
- (K (fn program => eval_term thy program (compile false thy program))));
+ (Code_Thingol.dynamic_value thy I (eval_term thy o compile false thy));
-fun static_conv thy consts =
- lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
- (K (fn program => fn _ => oracle thy program (compile true thy program))));
+fun static_conv thy consts = lift_triv_classes_conv thy
+ (Code_Thingol.static_conv thy consts (K o oracle thy o compile true thy));
fun static_value thy consts = lift_triv_classes_rew thy
- (Code_Thingol.static_value thy I consts
- (K (fn program => fn _ => eval_term thy program (compile true thy program))));
+ (Code_Thingol.static_value thy I consts (K o eval_term thy o compile true thy));
(** setup **)