--- a/src/HOL/HOL.thy Wed Oct 22 14:15:44 2008 +0200
+++ b/src/HOL/HOL.thy Wed Oct 22 14:15:45 2008 +0200
@@ -1692,8 +1692,7 @@
use "~~/src/HOL/Tools/recfun_codegen.ML"
setup {*
- Code_Name.setup
- #> Code_ML.setup
+ Code_ML.setup
#> Code_Haskell.setup
#> Nbe.setup
#> Codegen.setup
--- a/src/HOL/Library/Heap_Monad.thy Wed Oct 22 14:15:44 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy Wed Oct 22 14:15:45 2008 +0200
@@ -296,66 +296,66 @@
code_const "Heap_Monad.Fail" (OCaml "Failure")
code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
-ML {*
-local
+setup {* let
+ open Code_Thingol;
-open Code_Thingol;
-
-val bind' = Code_Name.const @{theory} @{const_name bindM};
-val return' = Code_Name.const @{theory} @{const_name return};
-val unit' = Code_Name.const @{theory} @{const_name Unity};
+ fun lookup naming = the o Code_Thingol.lookup_const naming;
-fun imp_monad_bind'' ts =
- let
- val dummy_name = "";
- val dummy_type = ITyVar dummy_name;
- val dummy_case_term = IVar dummy_name;
- (*assumption: dummy values are not relevant for serialization*)
- val unitt = IConst (unit', ([], []));
- fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
- | dest_abs (t, ty) =
- let
- val vs = Code_Thingol.fold_varnames cons t [];
- val v = Name.variant vs "x";
- val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
- in ((v, ty'), t `$ IVar v) end;
- fun force (t as IConst (c, _) `$ t') = if c = return'
- then t' else t `$ unitt
- | force t = t `$ unitt;
- fun tr_bind' [(t1, _), (t2, ty2)] =
- let
- val ((v, ty), t) = dest_abs (t2, ty2);
- in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
- and tr_bind'' t = case Code_Thingol.unfold_app t
- of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
- then tr_bind' [(x1, ty1), (x2, ty2)]
- else force t
- | _ => force t;
- in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
- [(unitt, tr_bind' ts)]), dummy_case_term) end
-and imp_monad_bind' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
- 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))
- else IConst const `$$ map imp_monad_bind ts
-and imp_monad_bind (IConst const) = imp_monad_bind' const []
- | imp_monad_bind (t as IVar _) = t
- | imp_monad_bind (t as _ `$ _) = (case unfold_app t
- of (IConst const, ts) => imp_monad_bind' const ts
- | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
- | imp_monad_bind (v_ty `|-> t) = v_ty `|-> imp_monad_bind t
- | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
- (((imp_monad_bind t, ty), (map o pairself) imp_monad_bind pats), imp_monad_bind t0);
+ fun imp_monad_bind'' bind' return' unit' ts =
+ let
+ val dummy_name = "";
+ val dummy_type = ITyVar dummy_name;
+ val dummy_case_term = IVar dummy_name;
+ (*assumption: dummy values are not relevant for serialization*)
+ val unitt = IConst (unit', ([], []));
+ fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
+ | dest_abs (t, ty) =
+ let
+ val vs = Code_Thingol.fold_varnames cons t [];
+ val v = Name.variant vs "x";
+ val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
+ in ((v, ty'), t `$ IVar v) end;
+ fun force (t as IConst (c, _) `$ t') = if c = return'
+ then t' else t `$ unitt
+ | force t = t `$ unitt;
+ fun tr_bind' [(t1, _), (t2, ty2)] =
+ let
+ val ((v, ty), t) = dest_abs (t2, ty2);
+ in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
+ and tr_bind'' t = case Code_Thingol.unfold_app t
+ of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
+ then tr_bind' [(x1, ty1), (x2, ty2)]
+ else force t
+ | _ => force t;
+ in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
+ [(unitt, tr_bind' ts)]), dummy_case_term) end
+ and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
+ of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
+ | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
+ | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
+ else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
+ and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
+ | imp_monad_bind bind' return' unit' (t as IVar _) = t
+ | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
+ of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
+ | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
+ | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t
+ | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
+ (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
+
+ fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
+ (imp_monad_bind (lookup naming @{const_name bindM})
+ (lookup naming @{const_name return})
+ (lookup naming @{const_name Unity}));
in
-val imp_program = (Graph.map_nodes o map_terms_stmt) imp_monad_bind;
+ Code_Target.extend_target ("SML_imp", ("SML", imp_program))
+ #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
end
*}
-setup {* Code_Target.extend_target ("SML_imp", ("SML", imp_program)) *}
-setup {* Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) *}
code_reserved OCaml Failure raise
--- a/src/HOL/List.thy Wed Oct 22 14:15:44 2008 +0200
+++ b/src/HOL/List.thy Wed Oct 22 14:15:45 2008 +0200
@@ -3520,20 +3520,8 @@
local
open Basic_Code_Thingol;
-val nil' = Code_Name.const @{theory} @{const_name Nil};
-val cons' = Code_Name.const @{theory} @{const_name Cons};
-val char' = Code_Name.const @{theory} @{const_name Char}
-val nibbles' = map (Code_Name.const @{theory})
- [@{const_name Nibble0}, @{const_name Nibble1},
- @{const_name Nibble2}, @{const_name Nibble3},
- @{const_name Nibble4}, @{const_name Nibble5},
- @{const_name Nibble6}, @{const_name Nibble7},
- @{const_name Nibble8}, @{const_name Nibble9},
- @{const_name NibbleA}, @{const_name NibbleB},
- @{const_name NibbleC}, @{const_name NibbleD},
- @{const_name NibbleE}, @{const_name NibbleF}];
-
-fun implode_list t =
+
+fun implode_list (nil', cons') t =
let
fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
if c = cons'
@@ -3546,19 +3534,19 @@
| _ => NONE
end;
-fun decode_char (IConst (c1, _), IConst (c2, _)) =
+fun decode_char nibbles' (IConst (c1, _), IConst (c2, _)) =
let
fun idx c = find_index (curry (op =) c) nibbles';
fun decode ~1 _ = NONE
| decode _ ~1 = NONE
| decode n m = SOME (chr (n * 16 + m));
in decode (idx c1) (idx c2) end
- | decode_char _ = NONE;
-
-fun implode_string mk_char mk_string ts =
+ | decode_char _ _ = NONE;
+
+fun implode_string (char', nibbles') mk_char mk_string ts =
let
fun implode_char (IConst (c, _) `$ t1 `$ t2) =
- if c = char' then decode_char (t1, t2) else NONE
+ if c = char' then decode_char nibbles' (t1, t2) else NONE
| implode_char _ = NONE;
val ts' = map implode_char ts;
in if forall is_some ts'
@@ -3566,6 +3554,20 @@
else NONE
end;
+fun list_names naming = pairself (the o Code_Thingol.lookup_const naming)
+ (@{const_name Nil}, @{const_name Cons});
+fun char_name naming = (the o Code_Thingol.lookup_const naming)
+ @{const_name Char}
+fun nibble_names naming = map (the o Code_Thingol.lookup_const naming)
+ [@{const_name Nibble0}, @{const_name Nibble1},
+ @{const_name Nibble2}, @{const_name Nibble3},
+ @{const_name Nibble4}, @{const_name Nibble5},
+ @{const_name Nibble6}, @{const_name Nibble7},
+ @{const_name Nibble8}, @{const_name Nibble9},
+ @{const_name NibbleA}, @{const_name NibbleB},
+ @{const_name NibbleC}, @{const_name NibbleD},
+ @{const_name NibbleE}, @{const_name NibbleF}];
+
fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
@@ -3576,8 +3578,8 @@
fun pretty_list literals =
let
val mk_list = Code_Printer.literal_list literals;
- fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list t2)
+ fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
+ case Option.map (cons t1) (implode_list (list_names naming) t2)
of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
| NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
in (2, pretty) end;
@@ -3587,9 +3589,9 @@
val mk_list = Code_Printer.literal_list literals;
val mk_char = Code_Printer.literal_char literals;
val mk_string = Code_Printer.literal_string literals;
- fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list t2)
- of SOME ts => (case implode_string mk_char mk_string ts
+ fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
+ case Option.map (cons t1) (implode_list (list_names naming) t2)
+ of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
of SOME p => p
| NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
| NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
@@ -3598,8 +3600,8 @@
fun pretty_char literals =
let
val mk_char = Code_Printer.literal_char literals;
- fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
- case decode_char (t1, t2)
+ fun pretty _ naming thm _ _ _ [(t1, _), (t2, _)] =
+ case decode_char (nibble_names naming) (t1, t2)
of SOME c => (Code_Printer.str o mk_char) c
| NONE => Code_Printer.nerror thm "Illegal character expression";
in (2, pretty) end;
@@ -3608,9 +3610,9 @@
let
val mk_char = Code_Printer.literal_char literals;
val mk_string = Code_Printer.literal_string literals;
- fun pretty _ thm _ _ _ [(t, _)] =
- case implode_list t
- of SOME ts => (case implode_string mk_char mk_string ts
+ fun pretty _ naming thm _ _ _ [(t, _)] =
+ case implode_list (list_names naming) t
+ of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
of SOME p => p
| NONE => Code_Printer.nerror thm "Illegal message expression")
| NONE => Code_Printer.nerror thm "Illegal message expression";
--- a/src/HOL/Tools/numeral.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/HOL/Tools/numeral.ML Wed Oct 22 14:15:45 2008 +0200
@@ -59,25 +59,28 @@
fun add_code number_of negative unbounded target thy =
let
- val pls' = Code_Name.const thy @{const_name Int.Pls};
- val min' = Code_Name.const thy @{const_name Int.Min};
- val bit0' = Code_Name.const thy @{const_name Int.Bit0};
- val bit1' = Code_Name.const thy @{const_name Int.Bit1};
val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
- fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0
- else if c = bit1' then 1
- else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
- | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
- fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0
- else if c = min' then
- if negative then SOME ~1 else NONE
- else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
- | dest_numeral thm (t1 `$ t2) =
- let val (n, b) = (dest_numeral thm t2, dest_bit thm t1)
- in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
- | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
- fun pretty _ thm _ _ _ [(t, _)] =
- (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t;
+ fun dest_numeral naming thm =
+ let
+ val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls};
+ val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min};
+ val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0};
+ val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1};
+ fun dest_bit (IConst (c, _)) = if c = bit0' then 0
+ else if c = bit1' then 1
+ else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
+ | dest_bit _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
+ fun dest_num (IConst (c, _)) = if c = pls' then SOME 0
+ else if c = min' then
+ if negative then SOME ~1 else NONE
+ else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
+ | dest_num (t1 `$ t2) =
+ let val (n, b) = (dest_num t2, dest_bit t1)
+ in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
+ | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
+ in dest_num end;
+ fun pretty _ naming thm _ _ _ [(t, _)] =
+ (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
in
thy
|> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
--- a/src/HOL/ex/Codegenerator_Pretty.thy Wed Oct 22 14:15:44 2008 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy Wed Oct 22 14:15:45 2008 +0200
@@ -17,7 +17,6 @@
nonfix upto;
*}
-export_code "RType.*" -- "workaround for cache problem"
export_code * in SML module_name CodegenTest
in OCaml module_name CodegenTest file -
in Haskell file -
--- a/src/Tools/code/code_haskell.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/Tools/code/code_haskell.ML Wed Oct 22 14:15:45 2008 +0200
@@ -32,7 +32,7 @@
| pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
in gen_pr_bind pr_bind pr_term end;
-fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
+fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
init_syms deresolve is_cons contr_classparam_typs deriving_show =
let
val deresolve_base = NameSpace.base o deresolve;
@@ -42,24 +42,24 @@
fun classparam_name class classparam = case syntax_class class
of NONE => deresolve_base classparam
| SOME (_, classparam_syntax) => case classparam_syntax classparam
- of NONE => (snd o dest_name) classparam
+ of NONE => (snd o Code_Name.dest_name) classparam
| SOME classparam => classparam;
fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
of [] => []
| classbinds => Pretty.enum "," "(" ")" (
map (fn (v, class) =>
- str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
+ str (class_name class ^ " " ^ Code_Name.lookup_var tyvars v)) classbinds)
@@ str " => ";
fun pr_typforall tyvars vs = case map fst vs
of [] => []
| vnames => str "forall " :: Pretty.breaks
- (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+ (map (str o Code_Name.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
fun pr_tycoexpr tyvars fxy (tyco, tys) =
brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
| SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
- | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
+ | pr_typ tyvars fxy (ITyVar v) = (str o Code_Name.lookup_var tyvars) v;
fun pr_typdecl tyvars (vs, tycoexpr) =
Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
fun pr_typscheme tyvars (vs, ty) =
@@ -75,7 +75,7 @@
pr_term tyvars thm pat vars BR t2
])
| pr_term tyvars thm pat vars fxy (IVar v) =
- (str o lookup_var vars) v
+ (str o Code_Name.lookup_var vars) v
| pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
let
val (binds, t') = Code_Thingol.unfold_abs t;
@@ -102,7 +102,7 @@
(str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
end
- and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
+ and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons naming
and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -131,9 +131,9 @@
) (map pr bs)
end
| pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
- fun pr_stmt (name, Code_Thingol.Fun ((vs, ty), [])) =
+ fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
let
- val tyvars = intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
val n = (length o fst o Code_Thingol.unfold_fun) ty;
in
Pretty.chunks [
@@ -153,10 +153,10 @@
)
]
end
- | pr_stmt (name, Code_Thingol.Fun ((vs, ty), raw_eqs)) =
+ | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
let
val eqs = filter (snd o snd) raw_eqs;
- val tyvars = intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
fun pr_eq ((ts, t), (thm, _)) =
let
val consts = map_filter
@@ -164,8 +164,8 @@
then NONE else (SOME o NameSpace.base o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = init_syms
- |> intro_vars consts
- |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Name.intro_vars consts
+ |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
semicolon (
@@ -186,18 +186,18 @@
:: map pr_eq eqs
)
end
- | pr_stmt (name, Code_Thingol.Datatype (vs, [])) =
+ | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
let
- val tyvars = intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
in
semicolon [
str "data",
pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
]
end
- | pr_stmt (name, Code_Thingol.Datatype (vs, [(co, [ty])])) =
+ | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
let
- val tyvars = intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
in
semicolon (
str "newtype"
@@ -208,9 +208,9 @@
:: (if deriving_show name then [str "deriving (Read, Show)"] else [])
)
end
- | pr_stmt (name, Code_Thingol.Datatype (vs, co :: cos)) =
+ | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
let
- val tyvars = intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
fun pr_co (co, tys) =
concat (
(str o deresolve_base) co
@@ -226,9 +226,9 @@
@ (if deriving_show name then [str "deriving (Read, Show)"] else [])
)
end
- | pr_stmt (name, Code_Thingol.Class (v, (superclasses, classparams))) =
+ | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
let
- val tyvars = intro_vars [v] init_syms;
+ val tyvars = Code_Name.intro_vars [v] init_syms;
fun pr_classparam (classparam, ty) =
semicolon [
(str o classparam_name name) classparam,
@@ -240,7 +240,7 @@
Pretty.block [
str "class ",
Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
- str (deresolve_base name ^ " " ^ lookup_var tyvars v),
+ str (deresolve_base name ^ " " ^ Code_Name.lookup_var tyvars v),
str " where {"
],
str "};"
@@ -248,7 +248,7 @@
end
| pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
let
- val tyvars = intro_vars (map fst vs) init_syms;
+ val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
fun pr_instdef ((classparam, c_inst), (thm, _)) =
semicolon [
(str o classparam_name class) classparam,
@@ -273,20 +273,20 @@
let
val module_alias = if is_some module_name then K module_name else raw_module_alias;
val reserved_names = Name.make_context reserved_names;
- val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
+ val mk_name_module = Code_Name.mk_name_module reserved_names module_prefix module_alias program;
fun add_stmt (name, (stmt, deps)) =
let
- val (module_name, base) = dest_name name;
+ val (module_name, base) = Code_Name.dest_name name;
val module_name' = mk_name_module module_name;
val mk_name_stmt = yield_singleton Name.variants;
fun add_fun upper (nsp_fun, nsp_typ) =
let
val (base', nsp_fun') =
- mk_name_stmt (if upper then first_upper base else base) nsp_fun
+ mk_name_stmt (if upper then Code_Name.first_upper base else base) nsp_fun
in (base', (nsp_fun', nsp_typ)) end;
fun add_typ (nsp_fun, nsp_typ) =
let
- val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
+ val (base', nsp_typ') = mk_name_stmt (Code_Name.first_upper base) nsp_typ
in (base', (nsp_fun, nsp_typ')) end;
val add_name = case stmt
of Code_Thingol.Fun _ => add_fun false
@@ -314,15 +314,14 @@
val hs_program = fold add_stmt (AList.make (fn name =>
(Graph.get_node program name, Graph.imm_succs program name))
(Graph.strong_conn program |> flat)) Symtab.empty;
- fun deresolver name =
- (fst o the o AList.lookup (op =) ((fst o snd o the
- o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
- handle Option => error ("Unknown statement name: " ^ labelled_name name);
+ fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
+ o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Name.dest_name) name))) name
+ handle Option => error ("Unknown statement name: " ^ labelled_name name);
in (deresolver, hs_program) end;
fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
reserved_names includes raw_module_alias
- syntax_class syntax_tyco syntax_const program cs destination =
+ syntax_class syntax_tyco syntax_const naming program cs destination =
let
val stmt_names = Code_Target.stmt_names_of_destination destination;
val module_name = if null stmt_names then raw_module_name else SOME "Code";
@@ -335,16 +334,16 @@
fun deriv _ "fun" = false
| deriv tycos tyco = member (op =) tycos tyco orelse
case try (Graph.get_node program) tyco
- of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
+ of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
(maps snd cs)
| NONE => true
and deriv' tycos (tyco `%% tys) = deriv tycos tyco
andalso forall (deriv' tycos) tys
| deriv' _ (ITyVar _) = true
in deriv [] tyco end;
- val reserved_names = make_vars reserved_names;
- fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
- syntax_const labelled_name reserved_names
+ val reserved_names = Code_Name.make_vars reserved_names;
+ fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
+ syntax_class syntax_tyco syntax_const reserved_names
(if qualified then deresolver else NameSpace.base o deresolver)
is_cons contr_classparam_typs
(if string_classes then deriving_show else K false);
@@ -432,14 +431,14 @@
of SOME (((v, pat), ty), t') =>
SOME ((SOME (((SOME v, pat), ty), true), t1), t')
| NONE => NONE;
- fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
- if c = c_bind then dest_bind t1 t2
+ fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
+ if c = c_bind_name then dest_bind t1 t2
else NONE
- | dest_monad t = case Code_Thingol.split_let t
+ | dest_monad _ t = case Code_Thingol.split_let t
of SOME (((pat, ty), tbind), t') =>
SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
| NONE => NONE;
- val implode_monad = Code_Thingol.unfoldr dest_monad;
+ fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
fun pr_monad pr_bind pr (NONE, t) vars =
(semicolon [pr vars NOBR t], vars)
| pr_monad pr_bind pr (SOME (bind, true), t) vars = vars
@@ -448,9 +447,9 @@
| pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
|> pr_bind NOBR bind
|>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
- fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
+ fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
- val (binds, t'') = implode_monad t'
+ val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars;
in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
| NONE => brackify_infix (1, L) fxy
@@ -460,11 +459,10 @@
fun add_monad target' raw_c_bind thy =
let
val c_bind = Code_Unit.read_const thy raw_c_bind;
- val c_bind' = Code_Name.const thy c_bind;
in if target = target' then
thy
|> Code_Target.add_syntax_const target c_bind
- (SOME (pretty_haskell_monad c_bind'))
+ (SOME (pretty_haskell_monad c_bind))
else error "Only Haskell target allows for monad syntax" end;
--- a/src/Tools/code/code_ml.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/Tools/code/code_ml.ML Wed Oct 22 14:15:45 2008 +0200
@@ -42,15 +42,15 @@
(** SML serailizer **)
-fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
+fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
let
val pr_label_classrel = translate_string (fn "." => "__" | c => c)
o NameSpace.qualifier;
val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
- | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
+ fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
+ | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";
fun pr_proj [] p =
p
| pr_proj [p'] p =
@@ -86,7 +86,7 @@
fun pr_term thm pat vars fxy (IConst c) =
pr_app thm pat vars fxy (c, [])
| pr_term thm pat vars fxy (IVar v) =
- str (lookup_var vars v)
+ str (Code_Name.lookup_var vars v)
| pr_term thm pat vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME c_ts => pr_app thm pat vars fxy c_ts
@@ -116,7 +116,7 @@
else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
(str o deresolve) c
:: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
- and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
+ and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
@@ -199,8 +199,8 @@
then NONE else (SOME o NameSpace.base o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> intro_vars consts
- |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Name.intro_vars consts
+ |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
concat (
@@ -250,7 +250,7 @@
in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = first_upper v ^ "_";
+ val w = Code_Name.first_upper v ^ "_";
fun pr_superclass_field (class, classrel) =
(concat o map str) [
pr_label_classrel classrel, ":", "'" ^ v, deresolve class
@@ -342,12 +342,12 @@
(** OCaml serializer **)
-fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
+fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
let
fun pr_dicts fxy ds =
let
- fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
- | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
+ fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v
+ | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);
fun pr_proj ps p =
fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
fun pr_dict fxy (DictConst (inst, dss)) =
@@ -379,7 +379,7 @@
fun pr_term thm pat vars fxy (IConst c) =
pr_app thm pat vars fxy (c, [])
| pr_term thm pat vars fxy (IVar v) =
- str (lookup_var vars v)
+ str (Code_Name.lookup_var vars v)
| pr_term thm pat vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME c_ts => pr_app thm pat vars fxy c_ts
@@ -407,7 +407,7 @@
else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
else (str o deresolve) c
:: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
- and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
+ and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
@@ -449,8 +449,8 @@
val x = Name.variant (map_filter I fished1) "x";
val fished2 = map_index (fillup_param x) fished1;
val (fished3, _) = Name.variants fished2 Name.context;
- val vars' = intro_vars fished3 vars;
- in map (lookup_var vars') fished3 end;
+ val vars' = Code_Name.intro_vars fished3 vars;
+ in map (Code_Name.lookup_var vars') fished3 end;
fun pr_stmt (MLFuns (funns as funn :: funns')) =
let
fun pr_eq ((ts, t), (thm, _)) =
@@ -460,8 +460,8 @@
then NONE else (SOME o NameSpace.base o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> intro_vars consts
- |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Name.intro_vars consts
+ |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in concat [
(Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
@@ -488,8 +488,8 @@
then NONE else (SOME o NameSpace.base o deresolve) c)
((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = reserved_names
- |> intro_vars consts
- |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ |> Code_Name.intro_vars consts
+ |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
(insert (op =)) ts []);
in
concat (
@@ -516,7 +516,7 @@
((fold o Code_Thingol.fold_constnames)
(insert (op =)) (map (snd o fst) eqs) []);
val vars = reserved_names
- |> intro_vars consts;
+ |> Code_Name.intro_vars consts;
val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
in
Pretty.block (
@@ -574,7 +574,7 @@
in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
| pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
let
- val w = "_" ^ first_upper v;
+ val w = "_" ^ Code_Name.first_upper v;
fun pr_superclass_field (class, classrel) =
(concat o map str) [
deresolve classrel, ":", "'" ^ v, deresolve class
@@ -716,16 +716,16 @@
let
val (x, nsp_typ') = f nsp_typ
in (x, (nsp_fun, nsp_typ')) end;
- val mk_name_module = mk_name_module reserved_names NONE module_alias program;
+ val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;
fun mk_name_stmt upper name nsp =
let
- val (_, base) = dest_name name;
- val base' = if upper then first_upper base else base;
+ val (_, base) = Code_Name.dest_name name;
+ val base' = if upper then Code_Name.first_upper base else base;
val ([base''], nsp') = Name.variants [base'] nsp;
in (base'', nsp') end;
fun add_funs stmts =
fold_map
- (fn (name, Code_Thingol.Fun stmt) =>
+ (fn (name, Code_Thingol.Fun (_, stmt)) =>
map_nsp_fun_yield (mk_name_stmt false name) #>>
rpair (name, stmt |> apsnd (filter (snd o snd)))
| (name, _) =>
@@ -734,7 +734,7 @@
#>> (split_list #> apsnd MLFuns);
fun add_datatypes stmts =
fold_map
- (fn (name, Code_Thingol.Datatype stmt) =>
+ (fn (name, Code_Thingol.Datatype (_, stmt)) =>
map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
| (name, Code_Thingol.Datatypecons _) =>
map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
@@ -747,8 +747,8 @@
| stmts => MLDatas stmts)));
fun add_class stmts =
fold_map
- (fn (name, Code_Thingol.Class info) =>
- map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
+ (fn (name, Code_Thingol.Class (_, stmt)) =>
+ map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
| (name, Code_Thingol.Classrel _) =>
map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
| (name, Code_Thingol.Classparam _) =>
@@ -786,7 +786,7 @@
[]
|> fold (fold (insert (op =)) o Graph.imm_succs program) names
|> subtract (op =) names;
- val (module_names, _) = (split_list o map dest_name) names;
+ val (module_names, _) = (split_list o map Code_Name.dest_name) names;
val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
handle Empty =>
error ("Different namespace prefixes for mutual dependencies:\n"
@@ -796,7 +796,7 @@
val module_name_path = NameSpace.explode module_name;
fun add_dep name name' =
let
- val module_name' = (mk_name_module o fst o dest_name) name';
+ val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
in if module_name = module_name' then
map_node module_name_path (Graph.add_edge (name, name'))
else let
@@ -824,7 +824,7 @@
(rev (Graph.strong_conn program)));
fun deresolver prefix name =
let
- val module_name = (fst o dest_name) name;
+ val module_name = (fst o Code_Name.dest_name) name;
val module_name' = (NameSpace.explode o mk_name_module) module_name;
val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
val stmt_name =
@@ -840,19 +840,19 @@
in (deresolver, nodes) end;
fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
- _ syntax_tyco syntax_const program cs destination =
+ _ syntax_tyco syntax_const naming program cs destination =
let
val is_cons = Code_Thingol.is_cons program;
val stmt_names = Code_Target.stmt_names_of_destination destination;
val module_name = if null stmt_names then raw_module_name else SOME "Code";
val (deresolver, nodes) = ml_node_of_program labelled_name module_name
reserved_names raw_module_alias program;
- val reserved_names = make_vars reserved_names;
+ val reserved_names = Code_Name.make_vars reserved_names;
fun pr_node prefix (Dummy _) =
NONE
| pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
(not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
- (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
+ (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names
(deresolver prefix) is_cons stmt)
else NONE
| pr_node prefix (Module (module_name, (_, nodes))) =
@@ -861,8 +861,8 @@
o rev o flat o Graph.strong_conn) nodes)
|> (if null stmt_names then pr_module module_name else Pretty.chunks)
|> SOME;
- val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
- cs;
+ val cs' = (map o try)
+ (deresolver (if is_some module_name then the_list module_name else [])) cs;
val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
(pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
in
@@ -877,8 +877,8 @@
(** ML (system language) code for evaluation and instrumentalization **)
-fun ml_code_of thy = Code_Target.serialize_custom thy
- (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
+fun ml_code_of thy = Code_Target.serialize_custom thy (target_SML,
+ (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),
literals_sml));
@@ -890,15 +890,16 @@
val _ = if null (term_frees (term_of ct)) then () else error ("Term "
^ quote (Syntax.string_of_term_global thy (term_of ct))
^ " to be evaluated contains free variables");
- fun eval' program ((vs, ty), t) deps =
+ fun eval' naming program ((vs, ty), t) deps =
let
val _ = if Code_Thingol.contains_dictvar t then
error "Term to be evaluated constains free dictionaries" else ();
+ val value_name = "Value.VALUE.value"
val program' = program
- |> Graph.new_node (Code_Name.value_name,
- Code_Thingol.Fun (([], ty), [(([], t), (Drule.dummy_thm, true))]))
- |> fold (curry Graph.add_edge Code_Name.value_name) deps;
- val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name];
+ |> Graph.new_node (value_name,
+ Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
+ |> fold (curry Graph.add_edge value_name) deps;
+ val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
^ space_implode " " (map (enclose "(" ")") args) ^ " end";
in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
@@ -922,12 +923,13 @@
fun delayed_code thy consts () =
let
- val (consts', program) = Code_Thingol.consts_program thy consts;
- val (ml_code, consts'') = ml_code_of thy program consts';
- val _ = if length consts <> length consts'' then
- error ("One of the constants " ^ commas (map (quote o Code_Unit.string_of_const thy) consts)
- ^ "\nhas a user-defined serialization") else ();
- in (ml_code, consts ~~ consts'') end;
+ val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
+ val (ml_code, consts'') = ml_code_of thy naming program consts';
+ val const_tab = map2 (fn const => fn NONE =>
+ error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const
+ ^ "\nhas a user-defined serialization")
+ | SOME const' => (const, const')) consts consts''
+ in (ml_code, const_tab) end;
fun register_const const ctxt =
let
--- a/src/Tools/code/code_name.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/Tools/code/code_name.ML Wed Oct 22 14:15:45 2008 +0200
@@ -2,62 +2,45 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Naming policies for code generation: prefixing any name by corresponding
-theory name, conversion to alphanumeric representation.
-Mappings are incrementally cached. Assumes non-concurrent processing
-inside a single theory.
+Some code generator infrastructure concerning names.
*)
signature CODE_NAME =
sig
- val read_const_exprs: theory -> string list -> string list * string list
+ structure StringPairTab: TABLE
+ val first_upper: string -> string
+ val first_lower: string -> string
+ val dest_name: string -> string * string
val purify_var: string -> string
val purify_tvar: string -> string
val purify_sym: string -> string
+ val purify_base: bool -> string -> string
val check_modulename: string -> string
- val class: theory -> class -> class
- val class_rev: theory -> class -> class option
- val classrel: theory -> class * class -> string
- val classrel_rev: theory -> string -> (class * class) option
- val tyco: theory -> string -> string
- val tyco_rev: theory -> string -> string option
- val instance: theory -> class * string -> string
- val instance_rev: theory -> string -> (class * string) option
- val const: theory -> string -> string
- val const_rev: theory -> string -> string option
- val value_name: string
- val labelled_name: theory -> string -> string
+ type var_ctxt
+ val make_vars: string list -> var_ctxt
+ val intro_vars: string list -> var_ctxt -> var_ctxt
+ val lookup_var: var_ctxt -> string -> string
- val setup: theory -> theory
+ val read_const_exprs: theory -> string list -> string list * string list
+ val mk_name_module: Name.context -> string option -> (string -> string option)
+ -> 'a Graph.T -> string -> string
end;
structure Code_Name: CODE_NAME =
struct
-(** constant expressions **)
+(** auxiliary **)
+
+structure StringPairTab =
+ TableFun(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
-fun read_const_exprs thy =
- let
- fun consts_of some_thyname =
- let
- val thy' = case some_thyname
- of SOME thyname => ThyInfo.the_theory thyname thy
- | NONE => thy;
- val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
- ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
- fun belongs_here c =
- not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
- in case some_thyname
- of NONE => cs
- | SOME thyname => filter belongs_here cs
- end;
- fun read_const_expr "*" = ([], consts_of NONE)
- | read_const_expr s = if String.isSuffix ".*" s
- then ([], consts_of (SOME (unsuffix ".*" s)))
- else ([Code_Unit.read_const thy s], []);
- in pairself flat o split_list o map read_const_expr end;
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+
+val dest_name =
+ apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
(** purification **)
@@ -92,82 +75,16 @@
| purify_tvar v =
(unprefix "'" #> explode #> filter Symbol.is_ascii_letter #> cons "'" #> implode) v;
-fun check_modulename mn =
- let
- val mns = NameSpace.explode mn;
- val mns' = map (purify_name true false) mns;
- in
- if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
- ^ "perhaps try " ^ quote (NameSpace.implode mns'))
- end;
-
-
-(** global names (identifiers) **)
-
-(* identifier categories *)
-
-val suffix_class = "class";
-val suffix_classrel = "classrel"
-val suffix_tyco = "tyco";
-val suffix_instance = "inst";
-val suffix_const = "const";
-
-fun string_of_classrel (class, superclass) = class ^ " < " ^ superclass;
-fun string_of_instance (class, tyco) = tyco ^ " :: " ^ class;
-
-fun add_suffix nsp name =
- NameSpace.append name nsp;
-
-fun dest_suffix nsp name =
- if NameSpace.base name = nsp
- then SOME (NameSpace.qualifier name)
- else NONE;
-
-local
-
-val name_mapping = [
- (suffix_class, "class"),
- (suffix_classrel, "subclass relation"),
- (suffix_tyco, "type constructor"),
- (suffix_instance, "instance"),
- (suffix_const, "constant")
-]
-
-in
-
-val category_of = the o AList.lookup (op =) name_mapping o NameSpace.base;
-
-end;
-
-
-(* theory name lookup *)
-
-local
- fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
-in
- fun thyname_of_class thy =
- thyname_of thy (ProofContext.query_class (ProofContext.init thy));
- fun thyname_of_tyco thy =
- thyname_of thy (Type.the_tags (Sign.tsig_of thy));
- fun thyname_of_instance thy a = case AxClass.arity_property thy a Markup.theory_nameN
- of [] => error ("no such instance: " ^ (quote o string_of_instance) a)
- | thyname :: _ => thyname;
- fun thyname_of_const thy =
- thyname_of thy (Consts.the_tags (Sign.consts_of thy));
-end;
-
-
-(* naming policies *)
-
val purify_prefix =
explode
- (*should disappear as soon as hierarchical theory name spaces are available*)
+ (*FIMXE should disappear as soon as hierarchical theory name spaces are available*)
#> Symbol.scanner "Malformed name"
(Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
#> implode
#> NameSpace.explode
#> map (purify_name true false);
+(*FIMXE non-canonical function treating non-canonical names*)
fun purify_base _ "op &" = "and"
| purify_base _ "op |" = "or"
| purify_base _ "op -->" = "implies"
@@ -183,227 +100,73 @@
val purify_sym = purify_base false;
-fun default_policy thy get_basename get_thyname name =
+fun check_modulename mn =
let
- val prefix = (purify_prefix o get_thyname thy) name;
- val base = (purify_base true o get_basename) name;
- in NameSpace.implode (prefix @ [base]) end;
-
-fun class_policy thy = default_policy thy NameSpace.base thyname_of_class;
-fun classrel_policy thy = default_policy thy (fn (class1, class2) =>
- NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
- (*order fits nicely with composed projections*)
-fun tyco_policy thy = default_policy thy NameSpace.base thyname_of_tyco;
-fun instance_policy thy = default_policy thy (fn (class, tyco) =>
- NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
-
-fun force_thyname thy c = case Code.get_datatype_of_constr thy c
- of SOME dtco => SOME (thyname_of_tyco thy dtco)
- | NONE => (case AxClass.class_of_param thy c
- of SOME class => SOME (thyname_of_class thy class)
- | NONE => (case AxClass.inst_of_param thy c
- of SOME (c, tyco) => SOME (thyname_of_instance thy
- ((the o AxClass.class_of_param thy) c, tyco))
- | NONE => NONE));
-
-fun const_policy thy c =
- case force_thyname thy c
- of NONE => default_policy thy NameSpace.base thyname_of_const c
- | SOME thyname => let
- val prefix = purify_prefix thyname;
- val base = (purify_base true o NameSpace.base) c;
- in NameSpace.implode (prefix @ [base]) end;
-
-
-(* theory and code data *)
-
-type tyco = string;
-type const = string;
-
-structure StringPairTab =
- TableFun(
- type key = string * string;
- val ord = prod_ord fast_string_ord fast_string_ord;
- );
-
-datatype names = Names of {
- class: class Symtab.table * class Symtab.table,
- classrel: string StringPairTab.table * (class * class) Symtab.table,
- tyco: tyco Symtab.table * tyco Symtab.table,
- instance: string StringPairTab.table * (class * tyco) Symtab.table
-}
-
-val empty_names = Names {
- class = (Symtab.empty, Symtab.empty),
- classrel = (StringPairTab.empty, Symtab.empty),
- tyco = (Symtab.empty, Symtab.empty),
- instance = (StringPairTab.empty, Symtab.empty)
-};
-
-local
- fun mk_names (class, classrel, tyco, instance) =
- Names { class = class, classrel = classrel, tyco = tyco, instance = instance };
- fun map_names f (Names { class, classrel, tyco, instance }) =
- mk_names (f (class, classrel, tyco, instance));
-in
- fun merge_names (Names { class = (class1, classrev1),
- classrel = (classrel1, classrelrev1), tyco = (tyco1, tycorev1),
- instance = (instance1, instancerev1) },
- Names { class = (class2, classrev2),
- classrel = (classrel2, classrelrev2), tyco = (tyco2, tycorev2),
- instance = (instance2, instancerev2) }) =
- mk_names ((Symtab.merge (op =) (class1, class2), Symtab.merge (op =) (classrev1, classrev2)),
- (StringPairTab.merge (op =) (classrel1, classrel2), Symtab.merge (op =) (classrelrev1, classrelrev2)),
- (Symtab.merge (op =) (tyco1, tyco2), Symtab.merge (op =) (tycorev1, tycorev2)),
- (StringPairTab.merge (op =) (instance1, instance2), Symtab.merge (op =) (instancerev1, instancerev2)));
- fun map_class f = map_names
- (fn (class, classrel, tyco, inst) => (f class, classrel, tyco, inst));
- fun map_classrel f = map_names
- (fn (class, classrel, tyco, inst) => (class, f classrel, tyco, inst));
- fun map_tyco f = map_names
- (fn (class, classrel, tyco, inst) => (class, classrel, f tyco, inst));
- fun map_instance f = map_names
- (fn (class, classrel, tyco, inst) => (class, classrel, tyco, f inst));
-end; (*local*)
-
-structure Code_Name = TheoryDataFun
-(
- type T = names ref;
- val empty = ref empty_names;
- fun copy (ref names) = ref names;
- val extend = copy;
- fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
-);
-
-structure ConstName = CodeDataFun
-(
- type T = const Symtab.table * string Symtab.table;
- val empty = (Symtab.empty, Symtab.empty);
- fun purge _ cs (const, constrev) = (fold Symtab.delete_safe cs const,
- fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
-);
-
-val setup = Code_Name.init;
-
-
-(* forward lookup with cache update *)
-
-fun get thy get_tabs get upd_names upd policy x =
- let
- val names_ref = Code_Name.get thy;
- val (Names names) = ! names_ref;
- val tabs = get_tabs names;
- fun declare name =
- let
- val names' = upd_names (K (upd (x, name) (fst tabs),
- Symtab.update_new (name, x) (snd tabs))) (Names names)
- in (names_ref := names'; name) end;
- in case get (fst tabs) x
- of SOME name => name
- | NONE =>
- x
- |> policy thy
- |> Name.variant (Symtab.keys (snd tabs))
- |> declare
- end;
-
-fun get_const thy const =
- let
- val tabs = ConstName.get thy;
- fun declare name =
- let
- val names' = (Symtab.update (const, name) (fst tabs),
- Symtab.update_new (name, const) (snd tabs))
- in (ConstName.change thy (K names'); name) end;
- in case Symtab.lookup (fst tabs) const
- of SOME name => name
- | NONE =>
- const
- |> const_policy thy
- |> Name.variant (Symtab.keys (snd tabs))
- |> declare
+ val mns = NameSpace.explode mn;
+ val mns' = map (purify_name true false) mns;
+ in
+ if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
+ ^ "perhaps try " ^ quote (NameSpace.implode mns'))
end;
-(* backward lookup *)
+(** variable name contexts **)
+
+type var_ctxt = string Symtab.table * Name.context;
-fun rev thy get_tabs name =
+fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
+ Name.make_context names);
+
+fun intro_vars names (namemap, namectxt) =
let
- val names_ref = Code_Name.get thy
- val (Names names) = ! names_ref;
- val tab = (snd o get_tabs) names;
- in case Symtab.lookup tab name
- of SOME x => x
- | NONE => error ("No such " ^ category_of name ^ ": " ^ quote name)
- end;
+ val (names', namectxt') = Name.variants names namectxt;
+ val namemap' = fold2 (curry Symtab.update) names names' namemap;
+ in (namemap', namectxt') end;
-fun rev_const thy name =
- let
- val tab = snd (ConstName.get thy);
- in case Symtab.lookup tab name
- of SOME const => const
- | NONE => error ("No such " ^ category_of name ^ ": " ^ quote name)
- end;
+fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
+ of SOME name' => name'
+ | NONE => error ("Invalid name in context: " ^ quote name);
-(* external interfaces *)
-
-fun class thy =
- get thy #class Symtab.lookup map_class Symtab.update class_policy
- #> add_suffix suffix_class;
-fun classrel thy =
- get thy #classrel StringPairTab.lookup map_classrel StringPairTab.update classrel_policy
- #> add_suffix suffix_classrel;
-fun tyco thy =
- get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy
- #> add_suffix suffix_tyco;
-fun instance thy =
- get thy #instance StringPairTab.lookup map_instance StringPairTab.update instance_policy
- #> add_suffix suffix_instance;
-fun const thy =
- get_const thy
- #> add_suffix suffix_const;
+(** misc **)
-fun class_rev thy =
- dest_suffix suffix_class
- #> Option.map (rev thy #class);
-fun classrel_rev thy =
- dest_suffix suffix_classrel
- #> Option.map (rev thy #classrel);
-fun tyco_rev thy =
- dest_suffix suffix_tyco
- #> Option.map (rev thy #tyco);
-fun instance_rev thy =
- dest_suffix suffix_instance
- #> Option.map (rev thy #instance);
-fun const_rev thy =
- dest_suffix suffix_const
- #> Option.map (rev_const thy);
-
-local
+fun read_const_exprs thy =
+ let
+ fun consts_of some_thyname =
+ let
+ val thy' = case some_thyname
+ of SOME thyname => ThyInfo.the_theory thyname thy
+ | NONE => thy;
+ val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+ ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
+ fun belongs_here c =
+ not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
+ in case some_thyname
+ of NONE => cs
+ | SOME thyname => filter belongs_here cs
+ end;
+ fun read_const_expr "*" = ([], consts_of NONE)
+ | read_const_expr s = if String.isSuffix ".*" s
+ then ([], consts_of (SOME (unsuffix ".*" s)))
+ else ([Code_Unit.read_const thy s], []);
+ in pairself flat o split_list o map read_const_expr end;
-val f_mapping = [
- (suffix_class, class_rev),
- (suffix_classrel, Option.map string_of_classrel oo classrel_rev),
- (suffix_tyco, tyco_rev),
- (suffix_instance, Option.map string_of_instance oo instance_rev),
- (suffix_const, fn thy => Option.map (Code_Unit.string_of_const thy) o const_rev thy)
-];
-
-in
-
-val value_name = "Isabelle_Eval.EVAL.EVAL"
-
-fun labelled_name thy suffix_name = if suffix_name = value_name then "<term>" else
+fun mk_name_module reserved_names module_prefix module_alias program =
let
- val category = category_of suffix_name;
- val name = NameSpace.qualifier suffix_name;
- val suffix = NameSpace.base suffix_name
- in case (the o AList.lookup (op =) f_mapping) suffix thy suffix_name
- of SOME thing => category ^ " " ^ quote thing
- | NONE => error ("Unknown name: " ^ quote name)
- end;
+ fun mk_alias name = case module_alias name
+ of SOME name' => name'
+ | NONE => name
+ |> NameSpace.explode
+ |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
+ |> NameSpace.implode;
+ fun mk_prefix name = case module_prefix
+ of SOME module_prefix => NameSpace.append module_prefix name
+ | NONE => name;
+ val tab =
+ Symtab.empty
+ |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
+ o fst o dest_name o fst)
+ program
+ in the o Symtab.lookup tab end;
end;
-
-end;
--- a/src/Tools/code/code_printer.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/Tools/code/code_printer.ML Wed Oct 22 14:15:45 2008 +0200
@@ -7,15 +7,7 @@
signature CODE_PRINTER =
sig
- val first_upper: string -> string
- val first_lower: string -> string
- val dest_name: string -> string * string
- val mk_name_module: Name.context -> string option -> (string -> string option)
- -> 'a Graph.T -> string -> string
- type var_ctxt;
- val make_vars: string list -> var_ctxt;
- val intro_vars: string list -> var_ctxt -> var_ctxt;
- val lookup_var: var_ctxt -> string -> string;
+ val nerror: thm -> string -> 'a
val @@ : 'a * 'a -> 'a list
val @| : 'a list * 'a -> 'a list
@@ -45,19 +37,21 @@
type tyco_syntax
type const_syntax
val parse_infix: ('a -> 'b) -> lrx * int -> string
- -> int * ((fixity -> 'b -> Pretty.T) -> fixity -> 'a list -> Pretty.T)
+ -> int * ((fixity -> 'b -> Pretty.T)
+ -> fixity -> 'a list -> Pretty.T)
val parse_syntax: ('a -> 'b) -> OuterParse.token list
- -> (int * ((fixity -> 'b -> Pretty.T) -> fixity -> 'a list -> Pretty.T)) option
- * OuterParse.token list
- val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T) -> fixity
- -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
- val gen_pr_app: (thm -> bool -> var_ctxt -> const * iterm list -> Pretty.T list)
- -> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T)
- -> (string -> const_syntax option) -> (string -> bool)
- -> thm -> bool -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
+ -> (int * ((fixity -> 'b -> Pretty.T)
+ -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
+ val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
+ -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
+ val gen_pr_app: (thm -> bool -> Code_Name.var_ctxt -> const * iterm list -> Pretty.T list)
+ -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> (string -> const_syntax option) -> (string -> bool) -> Code_Thingol.naming
+ -> thm -> bool -> Code_Name.var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
- -> (thm -> bool -> var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm -> fixity -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
+ -> (thm -> bool -> Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> thm -> fixity
+ -> (string option * iterm option) * itype -> Code_Name.var_ctxt -> Pretty.T * Code_Name.var_ctxt
type literals
val Literals: { literal_char: string -> string, literal_string: string -> string,
@@ -68,8 +62,6 @@
val literal_numeral: literals -> bool -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
val infix_cons: literals -> int * string
-
- val nerror: thm -> string -> 'a
end;
structure Code_Printer : CODE_PRINTER =
@@ -79,52 +71,6 @@
fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
-(** names and naming **)
-
-(* auxiliary *)
-
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
-
-val dest_name =
- apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
-
-fun mk_name_module reserved_names module_prefix module_alias program =
- let
- fun mk_alias name = case module_alias name
- of SOME name' => name'
- | NONE => name
- |> NameSpace.explode
- |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
- |> NameSpace.implode;
- fun mk_prefix name = case module_prefix
- of SOME module_prefix => NameSpace.append module_prefix name
- | NONE => name;
- val tab =
- Symtab.empty
- |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
- o fst o dest_name o fst)
- program
- in the o Symtab.lookup tab end;
-
-(* variable name contexts *)
-
-type var_ctxt = string Symtab.table * Name.context;
-
-fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
- Name.make_context names);
-
-fun intro_vars names (namemap, namectxt) =
- let
- val (names', namectxt') = Name.variants names namectxt;
- val namemap' = fold2 (curry Symtab.update) names names' namemap;
- in (namemap', namectxt') end;
-
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
- | NONE => error ("Invalid name in context: " ^ quote name);
-
-
(** assembling text pieces **)
infixr 5 @@;
@@ -182,19 +128,13 @@
type class_syntax = string * (string -> string option);
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
-> fixity -> itype list -> Pretty.T);
-type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm -> bool -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> Code_Thingol.naming -> thm -> bool -> Code_Name.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
fun simple_const_syntax x = (Option.map o apsnd)
- (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
-
-(*int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
- -> )
+ (fn pretty => fn pr => fn naming => fn thm => fn pat => fn vars => pretty (pr vars)) x;
-('a * ('b -> thm -> bool -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)) option
-*** -> ('a * (('d -> 'b) -> 'e -> 'f -> 'd -> 'c)) option*)
-
-fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
+fun gen_pr_app pr_app pr_term syntax_const is_cons naming thm pat
vars fxy (app as ((c, (_, tys)), ts)) =
case syntax_const c
of NONE => if pat andalso not (is_cons c) then
@@ -202,7 +142,7 @@
else brackify fxy (pr_app thm pat vars app)
| SOME (k, pr) =>
let
- fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
+ fun pr' fxy ts = pr (pr_term thm pat) naming thm pat vars fxy (ts ~~ curry Library.take k tys);
in if k = length ts
then pr' fxy ts
else if k < length ts
@@ -216,9 +156,9 @@
val vs = case pat
of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
| NONE => [];
- val vars' = intro_vars (the_list v) vars;
- val vars'' = intro_vars vs vars';
- val v' = Option.map (lookup_var vars') v;
+ val vars' = Code_Name.intro_vars (the_list v) vars;
+ val vars'' = Code_Name.intro_vars vs vars';
+ val v' = Option.map (Code_Name.lookup_var vars') v;
val pat' = Option.map (pr_term thm true vars'' fxy) pat;
in (pr_bind ((v', pat'), ty), vars'') end;
--- a/src/Tools/code/code_target.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/Tools/code/code_target.ML Wed Oct 22 14:15:45 2008 +0200
@@ -11,7 +11,8 @@
type serializer
val add_target: string * (serializer * literals) -> theory -> theory
- val extend_target: string * (string * (Code_Thingol.program -> Code_Thingol.program))
+ val extend_target: string *
+ (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
val assert_target: theory -> string -> string
@@ -24,20 +25,18 @@
val code_writeln: Pretty.T -> unit
val mk_serialization: string -> ('a -> unit) option
-> (Path.T option -> 'a -> unit)
- -> ('a -> string * string list)
+ -> ('a -> string * string option list)
-> 'a -> serialization
val serialize: theory -> string -> string option -> Args.T list
- -> Code_Thingol.program -> string list -> serialization
+ -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
val serialize_custom: theory -> string * (serializer * literals)
- -> Code_Thingol.program -> string list -> string * string list
+ -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
val the_literals: theory -> string -> literals
val compile: serialization -> unit
val export: serialization -> unit
val file: Path.T -> serialization -> unit
val string: string list -> serialization -> string
-
val code_of: theory -> string -> string -> string list -> string list -> string
- val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
val code_width: int ref
val allow_abort: string -> theory -> theory
@@ -45,11 +44,7 @@
-> (string * (string * string) list) option -> theory -> theory
val add_syntax_inst: string -> string * class -> bool -> theory -> theory
val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
- val add_syntax_tycoP: string -> string -> OuterParse.token list
- -> (theory -> theory) * OuterParse.token list
val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
- val add_syntax_constP: string -> string -> OuterParse.token list
- -> (theory -> theory) * OuterParse.token list
val add_reserved: string -> string -> theory -> theory
end;
@@ -62,7 +57,7 @@
(** basics **)
datatype destination = Compile | Export | File of Path.T | String of string list;
-type serialization = destination -> (string * string list) option;
+type serialization = destination -> (string * string option list) option;
val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
@@ -87,22 +82,24 @@
(** theory data **)
+structure StringPairTab = Code_Name.StringPairTab;
+
datatype name_syntax_table = NameSyntaxTable of {
class: class_syntax Symtab.table,
- inst: unit Symtab.table,
+ instance: unit StringPairTab.table,
tyco: tyco_syntax Symtab.table,
const: const_syntax Symtab.table
};
-fun mk_name_syntax_table ((class, inst), (tyco, const)) =
- NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
-fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
- mk_name_syntax_table (f ((class, inst), (tyco, const)));
-fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
- NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
+fun mk_name_syntax_table ((class, instance), (tyco, const)) =
+ NameSyntaxTable { class = class, instance = instance, tyco = tyco, const = const };
+fun map_name_syntax_table f (NameSyntaxTable { class, instance, tyco, const }) =
+ mk_name_syntax_table (f ((class, instance), (tyco, const)));
+fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
+ NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
mk_name_syntax_table (
(Symtab.join (K snd) (class1, class2),
- Symtab.join (K snd) (inst1, inst2)),
+ StringPairTab.join (K snd) (instance1, instance2)),
(Symtab.join (K snd) (tyco1, tyco2),
Symtab.join (K snd) (const1, const2))
);
@@ -117,12 +114,13 @@
-> (string -> class_syntax option)
-> (string -> tyco_syntax option)
-> (string -> const_syntax option)
+ -> Code_Thingol.naming
-> Code_Thingol.program
-> string list (*selected statements*)
-> serialization;
datatype serializer_entry = Serializer of serializer * literals
- | Extends of string * (Code_Thingol.program -> Code_Thingol.program);
+ | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
datatype target = Target of {
serial: serial,
@@ -178,19 +176,25 @@
fun put_target (target, seri) thy =
let
- val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
+ val lookup_target = Symtab.lookup (fst (CodeTargetData.get thy));
val _ = case seri
- of Extends (super, _) => if defined_target super then ()
+ of Extends (super, _) => if is_some (lookup_target super) then ()
else error ("Unknown code target language: " ^ quote super)
| _ => ();
- val _ = if defined_target target
+ val overwriting = case (Option.map the_serializer o lookup_target) target
+ of NONE => false
+ | SOME (Extends _) => true
+ | SOME (Serializer _) => (case seri
+ of Extends _ => error ("Will not overwrite existing target " ^ quote target)
+ | _ => true);
+ val _ = if overwriting
then warning ("Overwriting existing target " ^ quote target)
- else ();
+ else ();
in
thy
|> (CodeTargetData.map o apfst oo Symtab.map_default)
(target, mk_target ((serial (), seri), (([], Symtab.empty),
- (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
+ (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)),
Symtab.empty))))
((map_target o apfst o apsnd o K) seri)
end;
@@ -241,9 +245,8 @@
fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
let
val class = prep_class thy raw_class;
- val class' = Code_Name.class thy class;
fun mk_classparam c = case AxClass.class_of_param thy c
- of SOME class'' => if class = class'' then Code_Name.const thy c
+ of SOME class' => if class = class' then c
else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
| NONE => error ("Not a class operation: " ^ quote c);
fun mk_syntax_params raw_params = AList.lookup (op =)
@@ -252,30 +255,29 @@
of SOME (syntax, raw_params) =>
thy
|> (map_name_syntax target o apfst o apfst)
- (Symtab.update (class', (syntax, mk_syntax_params raw_params)))
+ (Symtab.update (class, (syntax, mk_syntax_params raw_params)))
| NONE =>
thy
|> (map_name_syntax target o apfst o apfst)
- (Symtab.delete_safe class')
+ (Symtab.delete_safe class)
end;
fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
let
- val inst = Code_Name.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
+ val inst = (prep_class thy raw_class, prep_tyco thy raw_tyco);
in if add_del then
thy
|> (map_name_syntax target o apfst o apsnd)
- (Symtab.update (inst, ()))
+ (StringPairTab.update (inst, ()))
else
thy
|> (map_name_syntax target o apfst o apsnd)
- (Symtab.delete_safe inst)
+ (StringPairTab.delete_safe inst)
end;
fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
let
val tyco = prep_tyco thy raw_tyco;
- val tyco' = if tyco = "fun" then "fun" else Code_Name.tyco thy tyco;
fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syntax
@@ -283,17 +285,16 @@
of SOME syntax =>
thy
|> (map_name_syntax target o apsnd o apfst)
- (Symtab.update (tyco', check_args syntax))
+ (Symtab.update (tyco, check_args syntax))
| NONE =>
thy
|> (map_name_syntax target o apsnd o apfst)
- (Symtab.delete_safe tyco')
+ (Symtab.delete_safe tyco)
end;
fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
let
val c = prep_const thy raw_c;
- val c' = Code_Name.const thy c;
fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c
then error ("Too many arguments in syntax for constant " ^ quote c)
else syntax;
@@ -301,11 +302,11 @@
of SOME syntax =>
thy
|> (map_name_syntax target o apsnd o apsnd)
- (Symtab.update (c', check_args syntax))
+ (Symtab.update (c, check_args syntax))
| NONE =>
thy
|> (map_name_syntax target o apsnd o apsnd)
- (Symtab.delete_safe c')
+ (Symtab.delete_safe c)
end;
fun add_reserved target =
@@ -330,11 +331,10 @@
fun add_module_alias target =
map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename;
-fun gen_allow_abort prep_cs raw_c thy =
+fun gen_allow_abort prep_const raw_c thy =
let
- val c = prep_cs thy raw_c;
- val c' = Code_Name.const thy c;
- in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
+ val c = prep_const thy raw_c;
+ in thy |> (CodeTargetData.map o apsnd) (insert (op =) c) end;
fun zip_list (x::xs) f g =
f
@@ -355,8 +355,6 @@
in
-val parse_syntax = parse_syntax;
-
val add_syntax_class = gen_add_syntax_class cert_class (K I);
val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
@@ -370,11 +368,6 @@
val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const;
val allow_abort_cmd = gen_allow_abort Code_Unit.read_const;
-fun add_syntax_tycoP target tyco = parse_syntax I
- >> add_syntax_tyco_cmd target tyco;
-fun add_syntax_constP target c = parse_syntax fst
- >> (add_syntax_const_cmd target c o Code_Printer.simple_const_syntax);
-
fun the_literals thy =
let
val (targets, _) = CodeTargetData.get thy;
@@ -390,27 +383,63 @@
(* montage *)
-fun invoke_serializer thy modify abortable serializer reserved includes
- module_alias class inst tyco const module args program1 cs1 =
+local
+
+fun labelled_name thy program name = case Graph.get_node program name
+ of Code_Thingol.Fun (c, _) => quote (Code_Unit.string_of_const thy c)
+ | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
+ | Code_Thingol.Datatypecons (c, _) => quote (Code_Unit.string_of_const thy c)
+ | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
+ | Code_Thingol.Classrel (sub, super) => let
+ val Code_Thingol.Class (sub, _) = Graph.get_node program sub
+ val Code_Thingol.Class (super, _) = Graph.get_node program super
+ in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
+ | Code_Thingol.Classparam (c, _) => quote (Code_Unit.string_of_const thy c)
+ | Code_Thingol.Classinst ((class, (tyco, _)), _) => let
+ val Code_Thingol.Class (class, _) = Graph.get_node program class
+ val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
+ in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
+
+fun invoke_serializer thy abortable serializer reserved includes
+ module_alias class instance tyco const module args naming program2 names1 =
let
- val program2 = modify program1;
- val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
- val cs2 = subtract (op =) hidden cs1;
- val program3 = Graph.subgraph (not o member (op =) hidden) program2;
- val all_cs = Graph.all_succs program2 cs2;
- val program4 = Graph.subgraph (member (op =) all_cs) program3;
+ fun distill_names lookup_name src_tab = Symtab.empty
+ |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier
+ of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
+ | NONE => (NONE, tab)) (Symtab.keys src_tab)
+ |>> map_filter I;
+ fun lookup_classparam_rev c' = case try (Graph.get_node program2) c'
+ of SOME (Code_Thingol.Classparam (c, _)) => SOME c
+ | NONE => NONE;
+ fun lookup_tyco_fun naming "fun" = SOME "fun"
+ | lookup_tyco_fun naming tyco = Code_Thingol.lookup_tyco naming tyco;
+ val (names_class, class') = distill_names Code_Thingol.lookup_class class;
+ val class'' = class'
+ |> (Symtab.map o apsnd) (fn class_params => fn c' =>
+ case lookup_classparam_rev c'
+ of SOME c => class_params c
+ | NONE => NONE)
+ val names_inst = map_filter (Code_Thingol.lookup_instance naming)
+ (StringPairTab.keys instance);
+ val (names_tyco, tyco') = distill_names lookup_tyco_fun tyco;
+ val (names_const, const') = distill_names Code_Thingol.lookup_const const;
+ val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
+ val names2 = subtract (op =) names_hidden names1;
+ val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
+ val names_all = Graph.all_succs program2 names2;
+ val program4 = Graph.subgraph (member (op =) names_all) program3;
val empty_funs = filter_out (member (op =) abortable)
(Code_Thingol.empty_funs program3);
val _ = if null empty_funs then () else error ("No defining equations for "
- ^ commas (map (Code_Name.labelled_name thy) empty_funs));
+ ^ commas (map (Sign.extern_const thy) empty_funs));
in
- serializer module args (Code_Name.labelled_name thy) reserved includes
- (Symtab.lookup module_alias) (Symtab.lookup class)
- (Symtab.lookup tyco) (Symtab.lookup const)
- program4 cs2
+ serializer module args (labelled_name thy program2) reserved includes
+ (Symtab.lookup module_alias) (Symtab.lookup class'')
+ (Symtab.lookup tyco') (Symtab.lookup const')
+ naming program4 names2
end;
-fun mount_serializer thy alt_serializer target =
+fun mount_serializer thy alt_serializer target module args naming program =
let
val (targets, abortable) = CodeTargetData.get thy;
fun collapse_hierarchy target =
@@ -422,7 +451,7 @@
of Serializer _ => (I, data)
| Extends (super, modify) => let
val (modify', data') = collapse_hierarchy super
- in (modify' #> modify, merge_target false target (data', data)) end
+ in (modify' #> modify naming, merge_target false target (data', data)) end
end;
val (modify, data) = collapse_hierarchy target;
val (serializer, _) = the_default (case the_serializer data
@@ -430,18 +459,22 @@
val reserved = the_reserved data;
val includes = Symtab.dest (the_includes data);
val module_alias = the_module_alias data;
- val { class, inst, tyco, const } = the_name_syntax data;
+ val { class, instance, tyco, const } = the_name_syntax data;
in
- invoke_serializer thy modify abortable serializer reserved
- includes module_alias class inst tyco const
+ invoke_serializer thy abortable serializer reserved
+ includes module_alias class instance tyco const module args naming (modify program)
end;
+in
+
fun serialize thy = mount_serializer thy NONE;
-fun serialize_custom thy (target_name, seri) program cs =
- mount_serializer thy (SOME seri) target_name NONE [] program cs (String [])
+fun serialize_custom thy (target_name, seri) naming program cs =
+ mount_serializer thy (SOME seri) target_name NONE [] naming program cs (String [])
|> the;
+end; (* local *)
+
fun parse_args f args =
case Scan.read OuterLex.stopper f args
of SOME x => x
@@ -450,40 +483,47 @@
(* code presentation *)
-fun code_of thy target module_name cs stmt_names =
+fun code_of thy target module_name cs names_stmt =
let
- val (cs', program) = Code_Thingol.consts_program thy cs;
+ val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
in
- string stmt_names (serialize thy target (SOME module_name) [] program cs')
+ string names_stmt (serialize thy target (SOME module_name) []
+ naming program names_cs)
end;
(* code generation *)
+fun transitivly_non_empty_funs thy naming program =
+ let
+ val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs 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_Name.read_const_exprs thy cs;
- val (cs3, program) = Code_Thingol.consts_program thy cs2;
- val cs4 = Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy);
+ val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
+ val names4 = transitivly_non_empty_funs thy naming program;
val cs5 = map_filter
- (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
+ (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
in fold (insert (op =)) cs5 cs1 end;
fun cached_program thy =
let
- val program = Code_Thingol.cached_program thy;
- in (Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
+ val (naming, program) = Code_Thingol.cached_program thy;
+ in (transitivly_non_empty_funs thy naming program, (naming, program)) end
fun export_code thy cs seris =
let
- val (cs', program) = if null cs then cached_program thy
+ val (cs', (naming, program)) = if null cs then cached_program thy
else Code_Thingol.consts_program thy cs;
fun mk_seri_dest dest = case dest
of NONE => compile
| SOME "-" => export
| SOME f => file (Path.explode f)
val _ = map (fn (((target, module), dest), args) =>
- (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
+ (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris;
in () end;
fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
@@ -563,13 +603,6 @@
OuterSyntax.command "export_code" "generate executable code for constants"
K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
-fun shell_command thyname cmd = Toplevel.program (fn _ =>
- (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd))
- ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
- of SOME f => (writeln "Now generating code..."; f (theory thyname))
- | NONE => error ("Bad directive " ^ quote cmd)))
- handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
-
end; (*local*)
end; (*struct*)
--- a/src/Tools/code/code_thingol.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/Tools/code/code_thingol.ML Wed Oct 22 14:15:45 2008 +0200
@@ -40,53 +40,59 @@
signature CODE_THINGOL =
sig
- include BASIC_CODE_THINGOL;
- 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;
- val unfold_app: iterm -> iterm * iterm list;
- val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option;
- val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm;
- val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option;
- val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
+ include BASIC_CODE_THINGOL
+ 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
+ val unfold_app: iterm -> iterm * iterm list
+ val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option
+ val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
+ val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
+ val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
val unfold_const_app: iterm ->
- ((string * (dict list list * itype list)) * iterm list) option;
+ ((string * (dict list list * itype list)) * iterm list) option
val collapse_let: ((vname * itype) * iterm) * iterm
- -> (iterm * itype) * (iterm * iterm) list;
- val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm;
- val contains_dictvar: iterm -> bool;
- val locally_monomorphic: iterm -> bool;
- val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
- val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
- val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
+ -> (iterm * itype) * (iterm * iterm) list
+ val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm
+ val contains_dictvar: iterm -> bool
+ val locally_monomorphic: iterm -> bool
+ val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
+ val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
+ val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
+
+ type 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
datatype stmt =
NoStmt
- | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list
- | Datatype of (vname * sort) list * (string * itype list) list
- | Datatypecons of string
- | Class of vname * ((class * string) list * (string * itype) list)
+ | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
+ | Datatype of string * ((vname * sort) list * (string * itype list) list)
+ | Datatypecons of string * string
+ | Class of class * (vname * ((class * string) list * (string * itype) list))
| Classrel of class * class
- | Classparam of class
+ | Classparam of string * class
| Classinst of (class * (string * (vname * sort) list))
* ((class * (string * (string * dict list list))) list
- * ((string * const) * (thm * bool)) list);
- type program = stmt Graph.T;
- val empty_funs: program -> string list;
- val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm;
- val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt;
- val transitivly_non_empty_funs: program -> string list -> string list;
- val is_cons: program -> string -> bool;
- val contr_classparam_typs: program -> string -> itype option list;
+ * ((string * const) * (thm * bool)) list)
+ type program = stmt Graph.T
+ val empty_funs: program -> string list
+ val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
+ val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
+ val is_cons: program -> string -> bool
+ val contr_classparam_typs: program -> string -> itype option list
- val consts_program: theory -> string list -> string list * program;
- val cached_program: theory -> program;
+ val consts_program: theory -> string list -> string list * (naming * program)
+ val cached_program: theory -> naming * program
val eval_conv: theory
- -> (term -> term * (program -> typscheme * iterm -> string list -> thm))
- -> cterm -> thm;
+ -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> thm))
+ -> cterm -> thm
val eval_term: theory
- -> (term -> term * (program -> typscheme * iterm -> string list -> 'a))
- -> term -> 'a;
+ -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> 'a))
+ -> term -> 'a
end;
structure Code_Thingol: CODE_THINGOL =
@@ -109,8 +115,6 @@
(** language core - types, patterns, expressions **)
-(* language representation *)
-
type vname = string;
datatype dict =
@@ -252,18 +256,148 @@
| locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
+(** naming policies **)
+
+(* identifier categories *)
+
+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 (NameSpace.append name nsp);
+
+
+(* policies *)
+
+local
+ fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
+ fun thyname_of_class thy =
+ thyname_of thy (ProofContext.query_class (ProofContext.init thy));
+ fun thyname_of_tyco thy =
+ thyname_of thy (Type.the_tags (Sign.tsig_of thy));
+ fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN
+ of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
+ | thyname :: _ => thyname;
+ fun thyname_of_const thy c = case Code.get_datatype_of_constr thy c
+ of SOME dtco => thyname_of_tyco thy dtco
+ | NONE => (case AxClass.class_of_param thy c
+ of SOME class => thyname_of_class thy class
+ | NONE => (case AxClass.inst_of_param thy c
+ of SOME (c, tyco) => thyname_of_instance thy
+ ((the o AxClass.class_of_param thy) c, tyco)
+ | NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c));
+ fun namify thy get_basename get_thyname name =
+ let
+ val prefix = get_thyname thy name;
+ val base = (Code_Name.purify_base true o get_basename) name;
+ in NameSpace.append prefix base end;
+in
+
+fun namify_class thy = namify thy NameSpace.base thyname_of_class;
+fun namify_classrel thy = namify thy (fn (class1, class2) =>
+ NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
+ (*order fits nicely with composed projections*)
+fun namify_tyco thy = namify thy NameSpace.base thyname_of_tyco;
+fun namify_instance thy = namify thy (fn (class, tyco) =>
+ NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
+fun namify_const thy = namify thy NameSpace.base thyname_of_const;
+
+end; (* local *)
+
+
+(* naming data with lookup and declare *)
+
+structure StringPairTab = Code_Name.StringPairTab;
+
+datatype naming = Naming of {
+ class: class Symtab.table * Name.context,
+ classrel: string StringPairTab.table * Name.context,
+ tyco: string Symtab.table * Name.context,
+ instance: string StringPairTab.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 = (StringPairTab.empty, Name.context),
+ tyco = (Symtab.empty, Name.context),
+ instance = (StringPairTab.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') = yield_singleton Name.variants 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));
+
+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 StringPairTab.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 StringPairTab.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 StringPairTab.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 StringPairTab.update_new namify_instance;
+fun declare_const thy = declare thy map_const
+ lookup_const Symtab.update_new namify_const;
+
(** statements, abstract programs **)
type typscheme = (vname * sort) list * itype;
datatype stmt =
NoStmt
- | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list
- | Datatype of (vname * sort) list * (string * itype list) list
- | Datatypecons of string
- | Class of vname * ((class * string) list * (string * itype) list)
+ | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
+ | Datatype of string * ((vname * sort) list * (string * itype list) list)
+ | Datatypecons of string * string
+ | Class of class * (vname * ((class * string) list * (string * itype) list))
| Classrel of class * class
- | Classparam of class
+ | Classparam of string * class
| Classinst of (class * (string * (vname * sort) list))
* ((class * (string * (string * dict list list))) list
* ((string * const) * (thm * bool)) list);
@@ -271,7 +405,7 @@
type program = stmt Graph.T;
fun empty_funs program =
- Graph.fold (fn (name, (Fun (_, []), _)) => cons name
+ Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c
| _ => I) program [];
fun map_terms_bottom_up f (t as IConst _) = f t
@@ -285,8 +419,8 @@
(map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
fun map_terms_stmt f NoStmt = NoStmt
- | map_terms_stmt f (Fun (tysm, eqs)) = Fun (tysm, (map o apfst)
- (fn (ts, t) => (map f ts, f t)) eqs)
+ | map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst)
+ (fn (ts, t) => (map f ts, f t)) eqs))
| map_terms_stmt f (stmt as Datatype _) = stmt
| map_terms_stmt f (stmt as Datatypecons _) = stmt
| map_terms_stmt f (stmt as Class _) = stmt
@@ -296,19 +430,13 @@
Classinst (arity, (superarities, (map o apfst o apsnd) (fn const =>
case f (IConst const) of IConst const' => const') classparms));
-fun transitivly_non_empty_funs program names_ignored =
- let
- val names_empty = empty_funs program;
- val names_delete = Graph.all_preds program (subtract (op =) names_ignored names_empty)
- in subtract (op =) names_delete (Graph.keys program) end;
-
fun is_cons program name = case Graph.get_node program name
of Datatypecons _ => true
| _ => false;
fun contr_classparam_typs program name = case Graph.get_node program name
- of Classparam class => let
- val Class (_, (_, params)) = Graph.get_node program class;
+ of Classparam (_, class) => let
+ val Class (_, (_, (_, params))) = Graph.get_node program class;
val SOME ty = AList.lookup (op =) params name;
val (tys, res_ty) = unfold_fun ty;
fun no_tyvar (_ `%% tys) = forall no_tyvar tys
@@ -322,22 +450,29 @@
(** translation kernel **)
-fun ensure_stmt stmtgen name (dep, program) =
+fun ensure_stmt lookup declare generate thing (dep, (naming, program)) =
let
- val add_dep = case dep of NONE => I | SOME dep => Graph.add_edge (dep, name);
- fun add_stmt false =
- Graph.default_node (name, NoStmt)
- #> add_dep
- #> curry stmtgen (SOME name)
- ##> snd
- #-> (fn stmt => Graph.map_node name (K stmt))
- | add_stmt true =
- add_dep;
- in
- program
- |> add_stmt (can (Graph.get_node program) name)
- |> pair dep
- |> pair name
+ fun add_dep name = case dep
+ of NONE => I | SOME dep => Graph.add_edge (dep, name);
+ in case lookup naming thing
+ of SOME name => program
+ |> add_dep name
+ |> pair naming
+ |> pair dep
+ |> pair name
+ | NONE => let
+ val (name, naming') = declare thing naming;
+ in
+ program
+ |> Graph.default_node (name, NoStmt)
+ |> add_dep name
+ |> pair naming'
+ |> curry generate (SOME name)
+ ||> snd
+ |-> (fn stmt => (apsnd o Graph.map_node name) (K stmt))
+ |> pair dep
+ |> pair name
+ end
end;
fun not_wellsorted thy thm ty sort e =
@@ -353,22 +488,20 @@
let
val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
val cs = #params (AxClass.get_info thy class);
- val class' = Code_Name.class thy class;
val stmt_class =
fold_map (fn superclass => ensure_class thy algbr funcgr superclass
##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
##>> exprgen_typ thy algbr funcgr ty) cs
- #>> (fn info => Class (unprefix "'" Name.aT, info))
- in ensure_stmt stmt_class class' end
+ #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
+ in ensure_stmt lookup_class (declare_class thy) stmt_class class end
and ensure_classrel thy algbr funcgr (subclass, superclass) =
let
- val classrel' = Code_Name.classrel thy (subclass, superclass);
val stmt_classrel =
ensure_class thy algbr funcgr subclass
##>> ensure_class thy algbr funcgr superclass
#>> Classrel;
- in ensure_stmt stmt_classrel classrel' end
+ in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
and ensure_tyco thy algbr funcgr "fun" =
pair "fun"
| ensure_tyco thy algbr funcgr tyco =
@@ -381,10 +514,9 @@
##>> fold_map (fn (c, tys) =>
ensure_const thy algbr funcgr c
##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
- #>> Datatype
+ #>> (fn info => Datatype (tyco, info))
end;
- val tyco' = Code_Name.tyco thy tyco;
- in ensure_stmt stmt_datatype tyco' end
+ in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
#>> (fn sort => (unprefix "'" v, sort))
@@ -467,38 +599,33 @@
##>> fold_map exprgen_classparam_inst classparams
#>> (fn ((((class, tyco), arity), superarities), classparams) =>
Classinst ((class, (tyco, arity)), (superarities, classparams)));
- val inst = Code_Name.instance thy (class, tyco);
- in ensure_stmt stmt_inst inst end
+ in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
and ensure_const thy algbr funcgr c =
let
- val c' = Code_Name.const thy c;
fun stmt_datatypecons tyco =
ensure_tyco thy algbr funcgr tyco
- #>> Datatypecons;
+ #>> (fn tyco => Datatypecons (c, tyco));
fun stmt_classparam class =
ensure_class thy algbr funcgr class
- #>> Classparam;
- fun stmt_fun trns =
+ #>> (fn class => Classparam (c, class));
+ fun stmt_fun ((vs, raw_ty), raw_thms) =
let
- val raw_thms = Code_Funcgr.eqns funcgr c;
- val (vs, raw_ty) = Code_Funcgr.typ funcgr c;
val ty = Logic.unvarifyT raw_ty;
val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
then raw_thms
else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
in
- trns
- |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
- ||>> exprgen_typ thy algbr funcgr ty
- ||>> fold_map (exprgen_eq thy algbr funcgr) thms
- |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
+ fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+ ##>> exprgen_typ thy algbr funcgr ty
+ ##>> fold_map (exprgen_eq thy algbr funcgr) thms
+ #>> (fn info => Fun (c, info))
end;
- val stmtgen = case Code.get_datatype_of_constr thy c
+ val stmt_const = case Code.get_datatype_of_constr 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)
- in ensure_stmt stmtgen c' end
+ | NONE => stmt_fun (Code_Funcgr.typ funcgr c, Code_Funcgr.eqns funcgr c))
+ in ensure_stmt lookup_const (declare_const thy) stmt_const c end
and exprgen_term thy algbr funcgr thm (Const (c, ty)) =
exprgen_app thy algbr funcgr thm ((c, ty), [])
| exprgen_term thy algbr funcgr thm (Free (v, _)) =
@@ -591,9 +718,9 @@
structure Program = CodeDataFun
(
- type T = program;
- val empty = Graph.empty;
- fun purge thy cs program =
+ type T = naming * program;
+ val empty = (empty_naming, Graph.empty);
+ fun purge thy cs (naming, program) = empty (*FIXME: problem: un-declaration of names
let
val cs_exisiting =
map_filter (Code_Name.const_rev thy) (Graph.keys program);
@@ -601,28 +728,25 @@
o map (Code_Name.const thy)
o filter (member (op =) cs_exisiting)
) cs;
- in Graph.del_nodes dels program end;
+ in Graph.del_nodes dels program end;*)
);
val cached_program = Program.get;
-fun transact f program =
- (NONE, program)
- |> f
- |-> (fn x => fn (_, program) => (x, program));
-
-fun generate thy funcgr f x =
- Program.change_yield thy (transact (f thy (Code.operational_algebra thy) funcgr x));
+fun generate thy funcgr f name =
+ Program.change_yield thy (fn naming_program => (NONE, naming_program)
+ |> f thy (Code.operational_algebra thy) funcgr name
+ |-> (fn name => fn (_, naming_program) => (name, naming_program)));
(* program generation *)
fun consts_program thy cs =
let
- fun project_consts cs program =
+ fun project_consts cs (naming, program) =
let
val cs_all = Graph.all_succs program cs;
- in (cs, Graph.subgraph (member (op =) cs_all) program) end;
+ in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
fun generate_consts thy algebra funcgr =
fold_map (ensure_const thy algebra funcgr);
in
@@ -642,18 +766,19 @@
fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
##>> exprgen_typ thy algbr funcgr ty
##>> exprgen_term thy algbr funcgr NONE t
- #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), (Drule.dummy_thm, true))]));
- fun term_value (dep, program1) =
+ #>> (fn ((vs, ty), t) => Fun
+ (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
+ fun term_value (dep, (naming, program1)) =
let
- val Fun ((vs, ty), [(([], t), _)]) =
- Graph.get_node program1 Code_Name.value_name;
- val deps = Graph.imm_succs program1 Code_Name.value_name;
- val program2 = Graph.del_nodes [Code_Name.value_name] program1;
+ val Fun (_, ((vs, ty), [(([], t), _)])) =
+ Graph.get_node program1 Term.dummy_patternN;
+ val deps = Graph.imm_succs program1 Term.dummy_patternN;
+ val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
val deps_all = Graph.all_succs program2 deps;
val program3 = Graph.subgraph (member (op =) deps_all) program2;
- in ((program3, (((vs, ty), t), deps)), (dep, program2)) end;
+ in (((naming, program3), (((vs, ty), t), deps)), (dep, (naming, program2))) end;
in
- ensure_stmt stmt_value Code_Name.value_name
+ ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
#> snd
#> term_value
end;
@@ -662,8 +787,8 @@
let
fun evaluator'' evaluator''' funcgr t =
let
- val ((program, (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
- in evaluator''' program vs_ty_t deps end;
+ val (((naming, program), (vs_ty_t, deps)), _) = generate thy funcgr ensure_value t;
+ in evaluator''' naming program vs_ty_t deps end;
fun evaluator' t =
let
val (t', evaluator''') = evaluator t;
--- a/src/Tools/nbe.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/Tools/nbe.ML Wed Oct 22 14:15:45 2008 +0200
@@ -288,15 +288,15 @@
(* preparing function equations *)
-fun eqns_of_stmt (_, Code_Thingol.Fun (_, [])) =
+fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) =
[]
- | eqns_of_stmt (const, Code_Thingol.Fun ((vs, _), eqns)) =
+ | eqns_of_stmt (const, Code_Thingol.Fun (_, ((vs, _), eqns))) =
[(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, (superclasses, classops))) =
+ | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (superclasses, classops)))) =
let
val names = map snd superclasses @ map fst classops;
val params = Name.invent_list [] "d" (length names);
@@ -364,27 +364,28 @@
(* reification *)
-fun term_of_univ thy idx_tab t =
+fun term_of_univ thy program 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, _)) =
- let
- val c = the (Inttab.lookup idx_tab idx);
- in
- (is_some o Code_Name.class_rev thy) c
- orelse (is_some o Code_Name.classrel_rev thy) c
- orelse (is_some o Code_Name.instance_rev thy) c
- end
+ 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)
| 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.Fun (c, _) => c
+ | Code_Thingol.Datatypecons (c, _) => c
+ | Code_Thingol.Classparam (c, _) => c);
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 = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx;
+ val c = const_of_idx idx;
val (_, T) = Code.default_typscheme thy c;
val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
val typidx' = typidx + maxidx_of_typ T' + 1;
@@ -405,7 +406,7 @@
(
type T = (Univ option * int) Graph.T * (int * string Inttab.table);
val empty = (Graph.empty, (0, Inttab.empty));
- fun purge thy cs (gr, (maxidx, idx_tab)) =
+ fun purge thy cs (gr, (maxidx, idx_tab)) = empty (*FIXME
let
val cs_exisiting =
map_filter (Code_Name.const_rev thy) (Graph.keys gr);
@@ -413,7 +414,7 @@
o map (Code_Name.const thy)
o filter (member (op =) cs_exisiting)
) cs;
- in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
+ in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end*);
);
(* compilation, evaluation and reification *)
@@ -425,7 +426,7 @@
in
vs_ty_t
|> eval_term ctxt gr deps
- |> term_of_univ thy idx_tab
+ |> term_of_univ thy program idx_tab
end;
(* evaluation with type reconstruction *)
@@ -478,13 +479,13 @@
fun norm_conv ct =
let
val thy = Thm.theory_of_cterm ct;
- fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
+ fun evaluator' t naming program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
fun evaluator t = (add_triv_classes thy t, evaluator' t);
in Code_Thingol.eval_conv thy evaluator ct end;
fun norm_term thy t =
let
- fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps;
+ fun evaluator' t naming program vs_ty_t deps = eval thy t program vs_ty_t deps;
fun evaluator t = (add_triv_classes thy t, evaluator' t);
in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;