File ‹Dataspace.ML›
structure Dataspace =
struct
val achanT = TFree ("'ch", ["HOL.type"])
fun mk_constant_elements cds =
let val cfixes = map (fn (n, t) => (Binding.name n, SOME t, NoSyn)) cds
in [ Element.Fixes cfixes ] end;
fun mk_channel_elements exts chds thy =
let
val ctx = Named_Target.theory_init thy
val chns = map fst chds
val chfixes = map (fn (n, t) => (Binding.name n, SOME (Prism_Lib.prismT t achanT), NoSyn)) chds
val wbs = map (Prism_Lib.mk_wb_prism o Syntax.free) chns;
val simp = Attrib.check_src ctx (Token.make_src ("simp", Position.none) [])
val imps = map (fn e => Locale.check thy (e, Position.none)) exts
val ilnsls = map (filter (Prism_Lib.isPrismT o snd) o map fst o Locale.params_of thy) imps
val impind = List.concat (map (Lens_Lib.pairsWith chns) (map (map fst) ilnsls))
val codeps = map (fn (x, y) => Prism_Lib.mk_codep (Syntax.free x) (Syntax.free y))
(Lens_Lib.pairings (chns) @ impind)
in
[ Element.Fixes chfixes
, Element.Assumes [((Binding.name "prisms", [simp])
, map (fn wb => (wb, [])) wbs),
((Binding.name "codeps", [simp])
, map (fn dp => (dp, [])) codeps)]
]
end
val STATE = "STATE_TYPE"
val CHAN = "CHAN_TYPE"
fun compile_dataspace nm exts cds assms vds chds thy =
let
val imps = map (fn e => Locale.check thy (e, Position.none)) exts
val pinsts = Expression.Named
[(STATE, Logic.mk_type Lens_Lib.astateT)
,(CHAN, Logic.mk_type achanT)]
val locexs = map (fn i => (i, (("", false), (pinsts, [])))) imps
val st_par = (Binding.name STATE, SOME (Term.itselfT Lens_Lib.astateT), NoSyn)
val ch_par = (Binding.name CHAN, SOME (Term.itselfT achanT), NoSyn)
in
(Local_Theory.exit_global o snd o
Expression.add_locale (Binding.name nm) Binding.empty [] (locexs, [])
(mk_constant_elements cds
@ [Element.Assumes assms]
@ Lens_Statespace.mk_statespace_elements vds exts thy
@ mk_channel_elements exts chds thy
@ [Element.Fixes [st_par, ch_par]])) thy
end
fun dataspace_cmd nm exts cds rassms vds chds thy =
let
val ctx = Named_Target.theory_init thy
val assms =
map (fn (b, td) => (b, map (fn (t, ts) =>
(HOLogic.mk_Trueprop (Syntax.parse_term ctx t),
map (HOLogic.mk_Trueprop o Syntax.parse_term ctx) ts)) td)) rassms
in
compile_dataspace nm exts (map (fn (n, t) =>
(n, Syntax.read_typ ctx t)) cds) assms (map (fn (n, t) =>
(n, Syntax.read_typ ctx t)) vds) (map (fn (n, t) => (n, Syntax.read_typ ctx t)) chds) thy
end
val _ =
Outer_Syntax.command @{command_keyword dataspace} "define reactive contexts"
((Parse.name --
((@{keyword "="} |-- Scan.repeat (Parse.name --| @{keyword "+"}))
-- Scan.optional (@{keyword "constants"} |-- Scan.repeat1 (Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ))) []
-- Scan.optional (@{keyword "assumes"} |-- Parse.!!! (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.propp))) []
-- Scan.optional (@{keyword "variables"} |-- Scan.repeat1 (Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ))) []
-- Scan.optional (@{keyword "channels"} |-- Scan.repeat1 (Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ))) [])
>> (fn (nm, ((((exts, cds), assms), vds), chds)) => Toplevel.theory (dataspace_cmd nm exts cds assms vds chds))))
end;