--- a/src/Pure/Isar/code.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/Isar/code.ML Mon Jan 04 14:10:13 2010 +0100
@@ -76,8 +76,8 @@
signature CODE_DATA =
sig
type T
- val change: theory -> (T -> T) -> T
- val change_yield: theory -> (T -> 'a * T) -> 'a * T
+ val change: theory -> (theory -> T -> T) -> T
+ val change_yield: theory -> (theory -> T -> 'a * T) -> 'a * T
end;
signature PRIVATE_CODE =
@@ -85,9 +85,9 @@
include CODE
val declare_data: Object.T -> serial
val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
- -> theory -> ('a -> 'a) -> 'a
+ -> theory -> (theory -> 'a -> 'a) -> 'a
val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
- -> theory -> ('a -> 'b * 'a) -> 'b * 'a
+ -> theory -> (theory -> 'a -> 'b * 'a) -> 'b * 'a
end;
structure Code : PRIVATE_CODE =
@@ -234,53 +234,35 @@
local
type data = Object.T Datatab.table;
-fun create_data data = Synchronized.var "code data" data;
-fun empty_data () = create_data Datatab.empty : data Synchronized.var;
+fun empty_dataref () = Synchronized.var "code data" (NONE : (data * theory_ref) option);
-structure Code_Data = TheoryDataFun
+structure Code_Data = Theory_Data
(
- type T = spec * data Synchronized.var;
+ type T = spec * (data * theory_ref) option Synchronized.var;
val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
- (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_data ());
- fun copy (spec, data) = (spec, create_data (Synchronized.value data));
- val extend = copy;
- fun merge _ ((spec1, _), (spec2, _)) =
- (merge_spec (spec1, spec2), empty_data ());
+ (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
+ val extend = I
+ fun merge ((spec1, _), (spec2, _)) =
+ (merge_spec (spec1, spec2), empty_dataref ());
);
-fun thy_data f thy = f ((snd o Code_Data.get) thy);
-
-fun get_ensure_init kind data =
- case Datatab.lookup (Synchronized.value data) kind
- of SOME x => x
- | NONE => let val y = invoke_init kind
- in (Synchronized.change data (Datatab.update (kind, y)); y) end;
-
in
(* access to executable code *)
val the_exec = fst o Code_Data.get;
-fun map_exec_purge f =
- Code_Data.map (fn (exec, data) => (f exec, empty_data ()));
+fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
-val purge_data = (Code_Data.map o apsnd) (fn _ => empty_data ());
+val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
fun change_eqns delete c f = (map_exec_purge o map_eqns
o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
o apfst) (fn (_, eqns) => (true, f eqns));
-fun del_eqns c = change_eqns true c (K (false, []));
-
(* tackling equation history *)
-fun get_eqns thy c =
- Symtab.lookup ((the_eqns o the_exec) thy) c
- |> Option.map (snd o snd o fst)
- |> these;
-
fun continue_history thy = if (history_concluded o the_exec) thy
then thy
|> (Code_Data.map o apfst o map_history_concluded) (K false)
@@ -297,30 +279,26 @@
#> map_history_concluded (K true))
|> SOME;
-val _ = Context.>> (Context.map_theory (Code_Data.init
- #> Theory.at_begin continue_history
- #> Theory.at_end conclude_history));
+val _ = Context.>> (Context.map_theory (Theory.at_begin continue_history #> Theory.at_end conclude_history));
(* access to data dependent on abstract executable code *)
-fun change_data (kind, mk, dest) =
+fun change_yield_data (kind, mk, dest) theory f =
let
- fun chnge data_ref f =
- let
- val data = get_ensure_init kind data_ref;
- val data' = f (dest data);
- in (Synchronized.change data_ref (Datatab.update (kind, mk data')); data') end;
- in thy_data chnge end;
+ val dataref = (snd o Code_Data.get) theory;
+ val (datatab, thy, thy_ref) = case Synchronized.value dataref
+ of SOME (datatab, thy_ref) => (datatab, Theory.deref thy_ref, thy_ref)
+ | NONE => (Datatab.empty, theory, Theory.check_thy theory)
+ val data = case Datatab.lookup datatab kind
+ of SOME data => data
+ | NONE => invoke_init kind;
+ val result as (x, data') = f thy (dest data);
+ val _ = Synchronized.change dataref
+ ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
+ in result end;
-fun change_yield_data (kind, mk, dest) =
- let
- fun chnge data_ref f =
- let
- val data = get_ensure_init kind data_ref;
- val (x, data') = f (dest data);
- in (x, (Synchronized.change data_ref (Datatab.update (kind, mk data')); data')) end;
- in thy_data chnge end;
+fun change_data ops theory f = change_yield_data ops theory (pair () oo f) |> snd;
end; (*local*)
@@ -574,7 +552,9 @@
in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
fun these_eqns thy c =
- get_eqns thy c
+ Symtab.lookup ((the_eqns o the_exec) thy) c
+ |> Option.map (snd o snd o fst)
+ |> these
|> (map o apfst) (Thm.transfer thy)
|> burrow_fst (standard_typscheme thy);
@@ -709,38 +689,6 @@
val add_signature_cmd = gen_add_signature read_const read_signature;
-(* datatypes *)
-
-structure Type_Interpretation =
- Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
-
-fun add_datatype raw_cs thy =
- let
- val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
- val (tyco, vs_cos) = constrset_of_consts thy cs;
- val old_cs = (map fst o snd o get_datatype thy) tyco;
- fun drop_outdated_cases cases = fold Symtab.delete_safe
- (Symtab.fold (fn (c, (_, (_, cos))) =>
- if exists (member (op =) old_cs) cos
- then insert (op =) c else I) cases []) cases;
- in
- thy
- |> fold (del_eqns o fst) cs
- |> map_exec_purge
- ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
- #> (map_cases o apfst) drop_outdated_cases)
- |> Type_Interpretation.data (tyco, serial ())
- end;
-
-fun type_interpretation f = Type_Interpretation.interpretation
- (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
-
-fun add_datatype_cmd raw_cs thy =
- let
- val cs = map (read_bare_const thy) raw_cs;
- in add_datatype cs thy end;
-
-
(* code equations *)
fun gen_add_eqn default (thm, proper) thy =
@@ -773,6 +721,56 @@
of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
| NONE => thy;
+fun del_eqns c = change_eqns true c (K (false, []));
+
+
+(* cases *)
+
+fun add_case thm thy =
+ let
+ val (c, (k, case_pats)) = case_cert thm;
+ val _ = case filter_out (is_constr thy) case_pats
+ of [] => ()
+ | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
+ val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
+ in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
+
+fun add_undefined c thy =
+ (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
+
+
+(* datatypes *)
+
+structure Type_Interpretation =
+ Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+
+fun add_datatype raw_cs thy =
+ let
+ val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
+ val (tyco, vs_cos) = constrset_of_consts thy cs;
+ val old_cs = (map fst o snd o get_datatype thy) tyco;
+ fun drop_outdated_cases cases = fold Symtab.delete_safe
+ (Symtab.fold (fn (c, (_, (_, cos))) =>
+ if exists (member (op =) old_cs) cos
+ then insert (op =) c else I) cases []) cases;
+ in
+ thy
+ |> fold (del_eqns o fst) cs
+ |> map_exec_purge
+ ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
+ #> (map_cases o apfst) drop_outdated_cases)
+ |> Type_Interpretation.data (tyco, serial ())
+ end;
+
+fun type_interpretation f = Type_Interpretation.interpretation
+ (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
+
+fun add_datatype_cmd raw_cs thy =
+ let
+ val cs = map (read_bare_const thy) raw_cs;
+ in add_datatype cs thy end;
+
+
(* c.f. src/HOL/Tools/recfun_codegen.ML *)
structure Code_Target_Attr = Theory_Data
@@ -789,7 +787,6 @@
let
val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
in thy |> add_warning_eqn thm |> attr prefix thm end;
-
(* setup *)
val _ = Context.>> (Context.map_theory
@@ -807,21 +804,6 @@
"declare theorems for code generation"
end));
-
-(* cases *)
-
-fun add_case thm thy =
- let
- val (c, (k, case_pats)) = case_cert thm;
- val _ = case filter_out (is_constr thy) case_pats
- of [] => ()
- | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs));
- val entry = (1 + Int.max (1, length case_pats), (k, case_pats))
- in (map_exec_purge o map_cases o apfst) (Symtab.update (c, entry)) thy end;
-
-fun add_undefined c thy =
- (map_exec_purge o map_cases o apsnd) (Symtab.update (c, ())) thy;
-
end; (*struct*)
--- a/src/Pure/axclass.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/axclass.ML Mon Jan 04 14:10:13 2010 +0100
@@ -118,7 +118,6 @@
(
type T = axclasses * (instances * inst_params);
val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
- val copy = I;
val extend = I;
fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
(merge_axclasses pp (axclasses1, axclasses2),
--- a/src/Pure/context.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/context.ML Mon Jan 04 14:10:13 2010 +0100
@@ -83,7 +83,7 @@
include CONTEXT
structure Theory_Data:
sig
- val declare: Object.T -> (Object.T -> Object.T) -> (Object.T -> Object.T) ->
+ val declare: Object.T -> (Object.T -> Object.T) ->
(Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
val get: serial -> (Object.T -> 'a) -> theory -> 'a
val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
@@ -112,7 +112,6 @@
type kind =
{empty: Object.T,
- copy: Object.T -> Object.T,
extend: Object.T -> Object.T,
merge: Pretty.pp -> Object.T * Object.T -> Object.T};
@@ -126,18 +125,16 @@
in
fun invoke_empty k = invoke (K o #empty) k ();
-val invoke_copy = invoke #copy;
val invoke_extend = invoke #extend;
fun invoke_merge pp = invoke (fn kind => #merge kind pp);
-fun declare_theory_data empty copy extend merge =
+fun declare_theory_data empty extend merge =
let
val k = serial ();
- val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
+ val kind = {empty = empty, extend = extend, merge = merge};
val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
in k end;
-val copy_data = Datatab.map' invoke_copy;
val extend_data = Datatab.map' invoke_extend;
fun merge_data pp (data1, data2) =
@@ -341,7 +338,7 @@
val (self', data', ancestry') =
if draft then (self, data, ancestry) (*destructive change!*)
else if #stage history > 0
- then (NONE, copy_data data, ancestry)
+ then (NONE, data, ancestry)
else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
val ids' = insert_id draft id ids;
val data'' = f data';
@@ -357,9 +354,8 @@
let
val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
val ids' = insert_id draft id ids;
- val data' = copy_data data;
val thy' = SYNCHRONIZED (fn () =>
- (check_thy thy; create_thy NONE true ids' data' ancestry history));
+ (check_thy thy; create_thy NONE true ids' data ancestry history));
in thy' end;
val pre_pure_thy = create_thy NONE true Inttab.empty
@@ -430,9 +426,9 @@
val declare = declare_theory_data;
fun get k dest thy =
- dest ((case Datatab.lookup (data_of thy) k of
+ dest (case Datatab.lookup (data_of thy) k of
SOME x => x
- | NONE => invoke_copy k (invoke_empty k))); (*adhoc value*)
+ | NONE => invoke_empty k); (*adhoc value*)
fun put k mk x = modify_thy (Datatab.update (k, mk x));
@@ -582,7 +578,6 @@
sig
type T
val empty: T
- val copy: T -> T
val extend: T -> T
val merge: Pretty.pp -> T * T -> T
end;
@@ -604,7 +599,6 @@
val kind = Context.Theory_Data.declare
(Data Data.empty)
- (fn Data x => Data (Data.copy x))
(fn Data x => Data (Data.extend x))
(fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
@@ -639,7 +633,6 @@
(
type T = Data.T;
val empty = Data.empty;
- val copy = I;
val extend = Data.extend;
fun merge _ = Data.merge;
);
--- a/src/Pure/sign.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/sign.ML Mon Jan 04 14:10:13 2010 +0100
@@ -151,7 +151,6 @@
structure SignData = TheoryDataFun
(
type T = sign;
- val copy = I;
fun extend (Sign {syn, tsig, consts, ...}) =
make_sign (Name_Space.default_naming, syn, tsig, consts);
--- a/src/Pure/theory.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/theory.ML Mon Jan 04 14:10:13 2010 +0100
@@ -91,7 +91,6 @@
type T = thy;
val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
val empty = make_thy (empty_axioms, Defs.empty, ([], []));
- val copy = I;
fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
--- a/src/Tools/Code/code_ml.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_ml.ML Mon Jan 04 14:10:13 2010 +0100
@@ -481,8 +481,6 @@
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
- |> intro_base_names
- (is_none o syntax_const) deresolve consts
|> intro_vars ((fold o Code_Thingol.fold_varnames)
(insert (op =)) ts []);
in concat [
--- a/src/Tools/Code/code_preproc.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML Mon Jan 04 14:10:13 2010 +0100
@@ -454,8 +454,8 @@
(** retrieval and evaluation interfaces **)
-fun obtain thy cs ts = apsnd snd
- (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
+fun obtain theory cs ts = apsnd snd
+ (Wellsorted.change_yield theory (fn thy => extend_arities_eqngr thy cs ts));
fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
let
--- a/src/Tools/Code/code_printer.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_printer.ML Mon Jan 04 14:10:13 2010 +0100
@@ -60,6 +60,7 @@
val brackify: fixity -> Pretty.T list -> Pretty.T
val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
+ val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
type tyco_syntax
type simple_const_syntax
@@ -220,6 +221,11 @@
else p
end;
+fun applify opn cls fxy_ctxt p [] = p
+ | applify opn cls fxy_ctxt p ps =
+ (if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
+ (p @@ enum "," opn cls ps);
+
(* generic syntax *)
--- a/src/Tools/Code/code_target.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_target.ML Mon Jan 04 14:10:13 2010 +0100
@@ -153,7 +153,7 @@
fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
fun the_module_alias (Target { module_alias , ... }) = module_alias;
-structure CodeTargetData = Theory_Data
+structure Targets = Theory_Data
(
type T = (target Symtab.table * string list) * int;
val empty = ((Symtab.empty, []), 80);
@@ -163,17 +163,17 @@
Library.merge (op =) (exc1, exc2)), Int.max (width1, width2));
);
-val abort_allowed = snd o fst o CodeTargetData.get;
+val abort_allowed = snd o fst o Targets.get;
-val the_default_width = snd o CodeTargetData.get;
+val the_default_width = snd o Targets.get;
-fun assert_target thy target = if Symtab.defined ((fst o fst) (CodeTargetData.get thy)) target
+fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target
then target
else error ("Unknown code target language: " ^ quote target);
fun put_target (target, seri) thy =
let
- val lookup_target = Symtab.lookup ((fst o fst) (CodeTargetData.get thy));
+ val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
val _ = case seri
of Extends (super, _) => if is_some (lookup_target super) then ()
else error ("Unknown code target language: " ^ quote super)
@@ -189,11 +189,10 @@
else ();
in
thy
- |> (CodeTargetData.map o apfst o apfst oo Symtab.map_default)
+ |> (Targets.map o apfst o apfst o Symtab.update)
(target, make_target ((serial (), seri), (([], Symtab.empty),
(mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
Symtab.empty))))
- ((map_target o apfst o apsnd o K) seri)
end;
fun add_target (target, seri) = put_target (target, Serializer seri);
@@ -205,7 +204,7 @@
val _ = assert_target thy target;
in
thy
- |> (CodeTargetData.map o apfst o apfst o Symtab.map_entry target o map_target) f
+ |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target) f
end;
fun map_reserved target =
@@ -217,7 +216,7 @@
fun map_module_alias target =
map_target_data target o apsnd o apsnd o apsnd;
-fun set_default_code_width k = (CodeTargetData.map o apsnd) (K k);
+fun set_default_code_width k = (Targets.map o apsnd) (K k);
(** serializer usage **)
@@ -226,7 +225,7 @@
fun the_literals thy =
let
- val ((targets, _), _) = CodeTargetData.get thy;
+ val ((targets, _), _) = Targets.get thy;
fun literals target = case Symtab.lookup targets target
of SOME data => (case the_serializer data
of Serializer (_, literals) => literals
@@ -284,7 +283,7 @@
fun mount_serializer thy alt_serializer target some_width module args naming program names =
let
- val ((targets, abortable), default_width) = CodeTargetData.get thy;
+ val ((targets, abortable), default_width) = Targets.get thy;
fun collapse_hierarchy target =
let
val data = case Symtab.lookup targets target
@@ -457,7 +456,7 @@
fun gen_allow_abort prep_const raw_c thy =
let
val c = prep_const thy raw_c;
- in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
+ in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end;
(* concrete syntax *)
--- a/src/Tools/Code/code_thingol.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon Jan 04 14:10:13 2010 +0100
@@ -848,8 +848,8 @@
val empty = (empty_naming, Graph.empty);
);
-fun invoke_generation thy (algebra, eqngr) f name =
- Program.change_yield thy (fn naming_program => (NONE, naming_program)
+fun invoke_generation theory (algebra, eqngr) f name =
+ Program.change_yield theory (fn thy => fn naming_program => (NONE, naming_program)
|> f thy algebra eqngr name
|-> (fn name => fn (_, naming_program) => (name, naming_program)));
--- a/src/Tools/nbe.ML Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Tools/nbe.ML Mon Jan 04 14:10:13 2010 +0100
@@ -513,15 +513,14 @@
(* compilation, evaluation and reification *)
-fun compile_eval thy naming program vs_t deps =
+fun compile_eval theory naming program vs_t deps =
let
- val ctxt = ProofContext.init thy;
val (_, (gr, (_, idx_tab))) =
- Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
+ Nbe_Functions.change theory (fn thy => ensure_stmts (ProofContext.init thy) naming program o snd);
in
vs_t
- |> eval_term ctxt gr deps
- |> term_of_univ thy program idx_tab
+ |> eval_term (ProofContext.init theory) gr deps
+ |> term_of_univ theory program idx_tab
end;
(* evaluation with type reconstruction *)