src/HOL/Statespace/state_space.ML
author haftmann
Sat Nov 14 08:45:51 2015 +0100 (2015-11-14)
changeset 61669 27ca6147e3b3
parent 61606 6d5213bd9709
child 61673 fd4ac1530d63
permissions -rw-r--r--
separate ML module for interpretation
haftmann@28308
     1
(*  Title:      HOL/Statespace/state_space.ML
schirmer@25171
     2
    Author:     Norbert Schirmer, TU Muenchen
schirmer@25171
     3
*)
schirmer@25171
     4
schirmer@25408
     5
signature STATE_SPACE =
wenzelm@45362
     6
sig
wenzelm@45362
     7
  val distinct_compsN : string
wenzelm@45362
     8
  val getN : string
wenzelm@45362
     9
  val putN : string
wenzelm@45362
    10
  val injectN : string
wenzelm@45362
    11
  val namespaceN : string
wenzelm@45362
    12
  val projectN : string
wenzelm@45362
    13
  val valuetypesN : string
schirmer@25408
    14
wenzelm@45362
    15
  val namespace_definition :
wenzelm@45362
    16
     bstring ->
wenzelm@45362
    17
     typ ->
wenzelm@46925
    18
     (xstring, string) Expression.expr * (binding * string option * mixfix) list ->
wenzelm@45362
    19
     string list -> string list -> theory -> theory
schirmer@25408
    20
wenzelm@45362
    21
  val define_statespace :
wenzelm@45362
    22
     string list ->
wenzelm@45362
    23
     string ->
wenzelm@49754
    24
     ((string * bool) * (string list * bstring * (string * string) list)) list ->
wenzelm@45362
    25
     (string * string) list -> theory -> theory
wenzelm@45362
    26
  val define_statespace_i :
wenzelm@45362
    27
     string option ->
wenzelm@45362
    28
     string list ->
wenzelm@45362
    29
     string ->
wenzelm@49754
    30
     ((string * bool) * (typ list * bstring * (string * string) list)) list ->
wenzelm@45362
    31
     (string * typ) list -> theory -> theory
schirmer@25408
    32
wenzelm@45362
    33
  val statespace_decl :
wenzelm@45362
    34
     ((string list * bstring) *
wenzelm@49754
    35
       (((string * bool) * (string list * xstring * (bstring * bstring) list)) list *
wenzelm@45362
    36
        (bstring * string) list)) parser
schirmer@25408
    37
schirmer@25408
    38
wenzelm@45362
    39
  val neq_x_y : Proof.context -> term -> term -> thm option
wenzelm@45362
    40
  val distinctNameSolver : Simplifier.solver
wenzelm@45362
    41
  val distinctTree_tac : Proof.context -> int -> tactic
wenzelm@45362
    42
  val distinct_simproc : Simplifier.simproc
schirmer@25408
    43
schirmer@25408
    44
wenzelm@48741
    45
  val get_comp : Context.generic -> string -> (typ * string) option
wenzelm@45362
    46
  val get_silent : Context.generic -> bool
wenzelm@45362
    47
  val set_silent : bool -> Context.generic -> Context.generic
schirmer@25408
    48
wenzelm@45362
    49
  val gen_lookup_tr : Proof.context -> term -> string -> term
wenzelm@45362
    50
  val lookup_swap_tr : Proof.context -> term list -> term
wenzelm@45362
    51
  val lookup_tr : Proof.context -> term list -> term
wenzelm@45362
    52
  val lookup_tr' : Proof.context -> term list -> term
schirmer@25408
    53
wenzelm@45362
    54
  val gen_update_tr :
wenzelm@45362
    55
     bool -> Proof.context -> string -> term -> term -> term
wenzelm@45362
    56
  val update_tr : Proof.context -> term list -> term
wenzelm@45362
    57
  val update_tr' : Proof.context -> term list -> term
wenzelm@45362
    58
end;
schirmer@25408
    59
norbert@29247
    60
structure StateSpace : STATE_SPACE =
schirmer@25171
    61
struct
schirmer@25171
    62
wenzelm@45362
    63
(* Names *)
schirmer@25171
    64
schirmer@25171
    65
val distinct_compsN = "distinct_names"
schirmer@25171
    66
val namespaceN = "_namespace"
schirmer@25171
    67
val valuetypesN = "_valuetypes"
schirmer@25171
    68
val projectN = "project"
schirmer@25171
    69
val injectN = "inject"
schirmer@25171
    70
val getN = "get"
schirmer@25171
    71
val putN = "put"
schirmer@25171
    72
val project_injectL = "StateSpaceLocale.project_inject";
schirmer@25171
    73
schirmer@25171
    74
schirmer@25171
    75
(* Library *)
schirmer@25171
    76
schirmer@25171
    77
fun fold1 f xs = fold f (tl xs) (hd xs)
schirmer@25171
    78
fun fold1' f [] x = x
schirmer@25171
    79
  | fold1' f xs _ = fold1 f xs
wenzelm@26478
    80
schirmer@25171
    81
fun sorted_subset eq [] ys = true
schirmer@25171
    82
  | sorted_subset eq (x::xs) [] = false
schirmer@25171
    83
  | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys
schirmer@25171
    84
                                       else sorted_subset eq (x::xs) ys;
schirmer@25171
    85
schirmer@25171
    86
schirmer@25171
    87
schirmer@25171
    88
type namespace_info =
schirmer@25171
    89
 {declinfo: (typ*string) Termtab.table, (* type, name of statespace *)
schirmer@25171
    90
  distinctthm: thm Symtab.table,
schirmer@25171
    91
  silent: bool
schirmer@25171
    92
 };
wenzelm@26478
    93
wenzelm@33519
    94
structure NameSpaceData = Generic_Data
wenzelm@33519
    95
(
wenzelm@26478
    96
  type T = namespace_info;
schirmer@25171
    97
  val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false};
schirmer@25171
    98
  val extend = I;
wenzelm@33519
    99
  fun merge
wenzelm@33519
   100
    ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
wenzelm@33519
   101
      {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
wenzelm@33519
   102
    {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
wenzelm@33519
   103
     distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
wenzelm@41472
   104
     silent = silent1 andalso silent2 (* FIXME odd merge *)}
wenzelm@33519
   105
);
schirmer@25171
   106
schirmer@25171
   107
fun make_namespace_data declinfo distinctthm silent =
schirmer@25171
   108
     {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
schirmer@25171
   109
schirmer@25171
   110
schirmer@25171
   111
fun update_declinfo (n,v) ctxt =
schirmer@25171
   112
  let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
wenzelm@26478
   113
  in NameSpaceData.put
schirmer@25171
   114
      (make_namespace_data (Termtab.update (n,v) declinfo) distinctthm silent) ctxt
schirmer@25171
   115
  end;
schirmer@25171
   116
schirmer@25171
   117
fun set_silent silent ctxt =
schirmer@25171
   118
  let val {declinfo,distinctthm,...} = NameSpaceData.get ctxt;
wenzelm@26478
   119
  in NameSpaceData.put
schirmer@25171
   120
      (make_namespace_data declinfo distinctthm silent) ctxt
schirmer@25171
   121
  end;
schirmer@25171
   122
schirmer@25171
   123
val get_silent = #silent o NameSpaceData.get;
wenzelm@26478
   124
wenzelm@46925
   125
fun expression_no_pos (expr, fixes) : Expression.expression =
wenzelm@46925
   126
  (map (fn (name, inst) => ((name, Position.none), inst)) expr, fixes);
wenzelm@46925
   127
schirmer@25171
   128
fun prove_interpretation_in ctxt_tac (name, expr) thy =
schirmer@25171
   129
   thy
haftmann@61669
   130
   |> Interpretation.sublocale_global_cmd (name, Position.none) (expression_no_pos expr) []
wenzelm@26478
   131
   |> Proof.global_terminal_proof
wenzelm@49889
   132
         ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
wenzelm@42361
   133
   |> Proof_Context.theory_of
schirmer@25171
   134
norbert@29247
   135
fun add_locale name expr elems thy =
wenzelm@45362
   136
  thy
haftmann@57181
   137
  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
haftmann@29362
   138
  |> snd
wenzelm@33671
   139
  |> Local_Theory.exit;
norbert@29247
   140
norbert@29247
   141
fun add_locale_cmd name expr elems thy =
wenzelm@45362
   142
  thy
haftmann@57181
   143
  |> Expression.add_locale_cmd (Binding.name name) Binding.empty (expression_no_pos expr) elems
haftmann@29362
   144
  |> snd
wenzelm@33671
   145
  |> Local_Theory.exit;
norbert@29247
   146
schirmer@25171
   147
type statespace_info =
schirmer@25171
   148
 {args: (string * sort) list, (* type arguments *)
schirmer@25171
   149
  parents: (typ list * string * string option list) list,
schirmer@25171
   150
             (* type instantiation, state-space name, component renamings *)
schirmer@25171
   151
  components: (string * typ) list,
schirmer@25171
   152
  types: typ list (* range types of state space *)
schirmer@25171
   153
 };
schirmer@25171
   154
wenzelm@33519
   155
structure StateSpaceData = Generic_Data
wenzelm@33519
   156
(
schirmer@25171
   157
  type T = statespace_info Symtab.table;
schirmer@25171
   158
  val empty = Symtab.empty;
schirmer@25171
   159
  val extend = I;
wenzelm@33519
   160
  fun merge data : T = Symtab.merge (K true) data;
wenzelm@33519
   161
);
schirmer@25171
   162
schirmer@25171
   163
fun add_statespace name args parents components types ctxt =
wenzelm@26478
   164
     StateSpaceData.put
schirmer@25171
   165
      (Symtab.update_new (name, {args=args,parents=parents,
schirmer@25171
   166
                                components=components,types=types}) (StateSpaceData.get ctxt))
wenzelm@26478
   167
      ctxt;
schirmer@25171
   168
schirmer@25171
   169
fun get_statespace ctxt name =
schirmer@25171
   170
      Symtab.lookup (StateSpaceData.get ctxt) name;
schirmer@25171
   171
schirmer@25171
   172
schirmer@25171
   173
fun mk_free ctxt name =
wenzelm@26478
   174
  if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
schirmer@25171
   175
  then
wenzelm@59900
   176
    let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden;
wenzelm@42488
   177
    in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
schirmer@25171
   178
  else NONE
wenzelm@26478
   179
wenzelm@26478
   180
schirmer@25171
   181
fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name;
wenzelm@26478
   182
fun get_comp ctxt name =
wenzelm@26478
   183
     Option.mapPartial
wenzelm@26478
   184
       (Termtab.lookup (#declinfo (NameSpaceData.get ctxt)))
schirmer@25171
   185
       (mk_free (Context.proof_of ctxt) name);
schirmer@25171
   186
schirmer@25171
   187
schirmer@25171
   188
(*** Tactics ***)
schirmer@25171
   189
schirmer@25171
   190
fun neq_x_y ctxt x y =
schirmer@25171
   191
  (let
wenzelm@26478
   192
    val dist_thm = the (get_dist_thm (Context.Proof ctxt) (#1 (dest_Free x)));
wenzelm@59582
   193
    val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
wenzelm@59582
   194
    val tree = Thm.term_of ctree;
schirmer@25171
   195
    val x_path = the (DistinctTreeProver.find_tree x tree);
schirmer@25171
   196
    val y_path = the (DistinctTreeProver.find_tree y tree);
wenzelm@60327
   197
    val thm = DistinctTreeProver.distinctTreeProver ctxt dist_thm x_path y_path;
wenzelm@26478
   198
  in SOME thm
wenzelm@45361
   199
  end handle Option.Option => NONE)
schirmer@25171
   200
wenzelm@42368
   201
fun distinctTree_tac ctxt = SUBGOAL (fn (goal, i) =>
wenzelm@42368
   202
  (case goal of
wenzelm@42368
   203
    Const (@{const_name Trueprop}, _) $
wenzelm@42368
   204
      (Const (@{const_name Not}, _) $
wenzelm@42368
   205
        (Const (@{const_name HOL.eq}, _) $ (x as Free _) $ (y as Free _))) =>
wenzelm@42368
   206
      (case neq_x_y ctxt x y of
wenzelm@60754
   207
        SOME neq => resolve_tac ctxt [neq] i
wenzelm@42368
   208
      | NONE => no_tac)
wenzelm@42368
   209
  | _ => no_tac));
schirmer@25171
   210
wenzelm@51717
   211
val distinctNameSolver = mk_solver "distinctNameSolver" distinctTree_tac;
schirmer@25171
   212
schirmer@25171
   213
val distinct_simproc =
wenzelm@61144
   214
  Simplifier.make_simproc @{context} "StateSpace.distinct_simproc"
wenzelm@61144
   215
   {lhss = [@{term "x = y"}],
wenzelm@61144
   216
    proc = fn _ => fn ctxt => fn ct =>
wenzelm@61144
   217
      (case Thm.term_of ct of
wenzelm@61144
   218
        Const (@{const_name HOL.eq},_) $ (x as Free _) $ (y as Free _) =>
wenzelm@61144
   219
          Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
wenzelm@61144
   220
            (neq_x_y ctxt x y)
wenzelm@61144
   221
      | _ => NONE),
wenzelm@61144
   222
    identifier = []};
schirmer@25171
   223
wenzelm@26478
   224
fun interprete_parent name dist_thm_name parent_expr thy =
schirmer@25171
   225
  let
wenzelm@42368
   226
    fun solve_tac ctxt = CSUBGOAL (fn (goal, i) =>
schirmer@25171
   227
      let
wenzelm@42361
   228
        val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name;
wenzelm@60327
   229
        val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal;
wenzelm@60754
   230
      in resolve_tac ctxt [rule] i end);
wenzelm@26478
   231
wenzelm@42368
   232
    fun tac ctxt =
wenzelm@42368
   233
      Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt);
wenzelm@26478
   234
wenzelm@45362
   235
  in
wenzelm@45362
   236
    thy |> prove_interpretation_in tac (name, parent_expr)
wenzelm@26478
   237
  end;
schirmer@25171
   238
wenzelm@26478
   239
fun namespace_definition name nameT parent_expr parent_comps new_comps thy =
schirmer@25171
   240
  let
schirmer@25171
   241
    val all_comps = parent_comps @ new_comps;
norbert@29247
   242
    val vars = (map (fn n => (Binding.name n, NONE, NoSyn)) all_comps);
schirmer@25171
   243
    val dist_thm_name = distinct_compsN;
schirmer@25171
   244
norbert@29247
   245
    val dist_thm_full_name = dist_thm_name;
wenzelm@59582
   246
    fun comps_of_thm thm = Thm.prop_of thm
schirmer@25171
   247
             |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free);
wenzelm@26478
   248
wenzelm@38835
   249
    fun type_attr phi = Thm.declaration_attribute (fn thm => fn context =>
wenzelm@38835
   250
      (case context of
wenzelm@38835
   251
        Context.Theory _ => context
wenzelm@38835
   252
      | Context.Proof ctxt =>
wenzelm@26478
   253
        let
wenzelm@38835
   254
          val {declinfo,distinctthm=tt,silent} = NameSpaceData.get context;
wenzelm@32960
   255
          val all_names = comps_of_thm thm;
schirmer@25171
   256
          fun upd name tt =
wenzelm@38835
   257
               (case Symtab.lookup tt name of
schirmer@25171
   258
                 SOME dthm => if sorted_subset (op =) (comps_of_thm dthm) all_names
schirmer@25171
   259
                              then Symtab.update (name,thm) tt else tt
wenzelm@38835
   260
               | NONE => Symtab.update (name,thm) tt)
schirmer@25171
   261
schirmer@25171
   262
          val tt' = tt |> fold upd all_names;
wenzelm@38835
   263
          val context' =
wenzelm@51717
   264
              Context_Position.set_visible false ctxt
wenzelm@51717
   265
              addsimprocs [distinct_simproc]
wenzelm@51717
   266
              |> Context_Position.restore_visible ctxt
wenzelm@51717
   267
              |> Context.Proof
wenzelm@51717
   268
              |> NameSpaceData.put {declinfo=declinfo,distinctthm=tt',silent=silent};
wenzelm@38835
   269
        in context' end));
wenzelm@26478
   270
schirmer@25171
   271
    val attr = Attrib.internal type_attr;
schirmer@25171
   272
wenzelm@45362
   273
    val assume =
wenzelm@45362
   274
      ((Binding.name dist_thm_name, [attr]),
wenzelm@45362
   275
        [(HOLogic.Trueprop $
wenzelm@45362
   276
          (Const (@{const_name all_distinct}, Type (@{type_name tree}, [nameT]) --> HOLogic.boolT) $
wenzelm@45362
   277
            DistinctTreeProver.mk_tree (fn n => Free (n, nameT)) nameT
wenzelm@45362
   278
              (sort fast_string_ord all_comps)), [])]);
wenzelm@45362
   279
  in
wenzelm@45362
   280
    thy
wenzelm@45362
   281
    |> add_locale name ([], vars) [Element.Assumes [assume]]
wenzelm@45362
   282
    |> Proof_Context.theory_of
wenzelm@45362
   283
    |> interprete_parent name dist_thm_full_name parent_expr
schirmer@25171
   284
  end;
schirmer@25171
   285
wenzelm@55972
   286
fun encode_dot x = if x = #"." then #"_" else x;
schirmer@25171
   287
schirmer@25171
   288
fun encode_type (TFree (s, _)) = s
schirmer@25171
   289
  | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
wenzelm@26478
   290
  | encode_type (Type (n,Ts)) =
schirmer@25171
   291
      let
schirmer@25171
   292
        val Ts' = fold1' (fn x => fn y => x ^ "_" ^ y) (map encode_type Ts) "";
hoelzl@32651
   293
        val n' = String.map encode_dot n;
schirmer@25171
   294
      in if Ts'="" then n' else Ts' ^ "_" ^ n' end;
schirmer@25171
   295
schirmer@25171
   296
fun project_name T = projectN ^"_"^encode_type T;
schirmer@25171
   297
fun inject_name T = injectN ^"_"^encode_type T;
schirmer@25171
   298
schirmer@25171
   299
schirmer@25171
   300
fun add_declaration name decl thy =
schirmer@25171
   301
  thy
haftmann@57181
   302
  |> Named_Target.init name
wenzelm@45291
   303
  |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
wenzelm@33671
   304
  |> Local_Theory.exit_global;
schirmer@25171
   305
schirmer@25171
   306
fun parent_components thy (Ts, pname, renaming) =
schirmer@25171
   307
  let
schirmer@25171
   308
    val ctxt = Context.Theory thy;
schirmer@25171
   309
    fun rename [] xs = xs
schirmer@25171
   310
      | rename (NONE::rs)  (x::xs) = x::rename rs xs
schirmer@25171
   311
      | rename (SOME r::rs) ((x,T)::xs) = (r,T)::rename rs xs;
wenzelm@45362
   312
    val {args, parents, components, ...} = the (Symtab.lookup (StateSpaceData.get ctxt) pname);
schirmer@25171
   313
    val inst = map fst args ~~ Ts;
schirmer@25171
   314
    val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
wenzelm@26478
   315
    val parent_comps =
wenzelm@49754
   316
      maps (fn (Ts',n,rs) => parent_components thy (map subst Ts', n, rs)) parents;
schirmer@25171
   317
    val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
schirmer@25171
   318
  in all_comps end;
schirmer@25171
   319
schirmer@25171
   320
fun statespace_definition state_type args name parents parent_comps components thy =
wenzelm@26478
   321
  let
haftmann@28965
   322
    val full_name = Sign.full_bname thy name;
schirmer@25171
   323
    val all_comps = parent_comps @ components;
schirmer@25171
   324
schirmer@25171
   325
    val components' = map (fn (n,T) => (n,(T,full_name))) components;
schirmer@25171
   326
wenzelm@49754
   327
    fun parent_expr (prefix, (_, n, rs)) =
wenzelm@49754
   328
      (suffix namespaceN n, (prefix, Expression.Positional rs));
norbert@29247
   329
    val parents_expr = map parent_expr parents;
schirmer@25171
   330
    fun distinct_types Ts =
wenzelm@27276
   331
      let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty;
wenzelm@27276
   332
      in map fst (Typtab.dest tab) end;
schirmer@25171
   333
schirmer@25171
   334
    val Ts = distinct_types (map snd all_comps);
schirmer@25171
   335
    val arg_names = map fst args;
wenzelm@43324
   336
    val valueN = singleton (Name.variant_list arg_names) "'value";
wenzelm@43324
   337
    val nameN = singleton (Name.variant_list (valueN :: arg_names)) "'name";
schirmer@25171
   338
    val valueT = TFree (valueN, Sign.defaultS thy);
schirmer@25171
   339
    val nameT = TFree (nameN, Sign.defaultS thy);
schirmer@25171
   340
    val stateT = nameT --> valueT;
schirmer@25171
   341
    fun projectT T = valueT --> T;
wenzelm@26478
   342
    fun injectT T = T --> valueT;
norbert@29247
   343
    val locinsts = map (fn T => (project_injectL,
wenzelm@49754
   344
                    ((encode_type T,false),Expression.Positional
wenzelm@45362
   345
                             [SOME (Free (project_name T,projectT T)),
norbert@29247
   346
                              SOME (Free ((inject_name T,injectT T)))]))) Ts;
wenzelm@32952
   347
    val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn),
wenzelm@32952
   348
                                     (Binding.name (inject_name T),NONE,NoSyn)]) Ts;
wenzelm@32952
   349
    val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts;
schirmer@25171
   350
wenzelm@49754
   351
    fun interprete_parent_valuetypes (prefix, (Ts, pname, _)) thy =
schirmer@25171
   352
      let
wenzelm@26478
   353
        val {args,types,...} =
schirmer@25171
   354
             the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
schirmer@25171
   355
        val inst = map fst args ~~ Ts;
schirmer@25171
   356
        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
wenzelm@32952
   357
        val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
norbert@29247
   358
wenzelm@45362
   359
        val expr = ([(suffix valuetypesN name,
wenzelm@49754
   360
                     (prefix, Expression.Positional (map SOME pars)))],[]);
wenzelm@29291
   361
      in
wenzelm@59498
   362
        prove_interpretation_in (fn ctxt => ALLGOALS (solve_tac ctxt (Assumption.all_prems_of ctxt)))
wenzelm@29291
   363
          (suffix valuetypesN name, expr) thy
wenzelm@29291
   364
      end;
schirmer@25171
   365
wenzelm@49754
   366
    fun interprete_parent (prefix, (_, pname, rs)) =
schirmer@25171
   367
      let
wenzelm@49754
   368
        val expr = ([(pname, (prefix, Expression.Positional rs))],[])
wenzelm@26478
   369
      in prove_interpretation_in
haftmann@29360
   370
           (fn ctxt => Locale.intro_locales_tac false ctxt [])
schirmer@25171
   371
           (full_name, expr) end;
schirmer@25171
   372
schirmer@25171
   373
    fun declare_declinfo updates lthy phi ctxt =
schirmer@25171
   374
      let
wenzelm@26478
   375
        fun upd_prf ctxt =
schirmer@25171
   376
          let
schirmer@25171
   377
            fun upd (n,v) =
schirmer@25171
   378
              let
wenzelm@42361
   379
                val nT = Proof_Context.infer_type (Local_Theory.target_of lthy) (n, dummyT)
wenzelm@26478
   380
              in Context.proof_map
wenzelm@26478
   381
                  (update_declinfo (Morphism.term phi (Free (n,nT)),v))
schirmer@25171
   382
              end;
schirmer@25171
   383
          in ctxt |> fold upd updates end;
schirmer@25171
   384
schirmer@25171
   385
      in Context.mapping I upd_prf ctxt end;
schirmer@25171
   386
wenzelm@26478
   387
   fun string_of_typ T =
wenzelm@39134
   388
      Print_Mode.setmp []
wenzelm@39134
   389
        (Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy))) T;
schirmer@25171
   390
   val fixestate = (case state_type of
schirmer@25171
   391
         NONE => []
wenzelm@26478
   392
       | SOME s =>
wenzelm@26478
   393
          let
wenzelm@32960
   394
            val fx = Element.Fixes [(Binding.name s,SOME (string_of_typ stateT),NoSyn)];
wenzelm@26478
   395
            val cs = Element.Constrains
schirmer@25171
   396
                       (map (fn (n,T) =>  (n,string_of_typ T))
schirmer@25171
   397
                         ((map (fn (n,_) => (n,nameT)) all_comps) @
schirmer@25171
   398
                          constrains))
schirmer@25171
   399
          in [fx,cs] end
schirmer@25171
   400
       )
schirmer@25171
   401
wenzelm@26478
   402
wenzelm@26478
   403
  in thy
wenzelm@26478
   404
     |> namespace_definition
norbert@29247
   405
           (suffix namespaceN name) nameT (parents_expr,[])
schirmer@25171
   406
           (map fst parent_comps) (map fst components)
wenzelm@49754
   407
     |> Context.theory_map (add_statespace full_name args (map snd parents) components [])
norbert@29247
   408
     |> add_locale (suffix valuetypesN name) (locinsts,locs) []
wenzelm@45362
   409
     |> Proof_Context.theory_of
wenzelm@26478
   410
     |> fold interprete_parent_valuetypes parents
norbert@29247
   411
     |> add_locale_cmd name
norbert@29247
   412
              ([(suffix namespaceN full_name ,(("",false),Expression.Named [])),
norbert@29247
   413
                (suffix valuetypesN full_name,(("",false),Expression.Named  []))],[]) fixestate
wenzelm@45362
   414
     |> Proof_Context.theory_of
schirmer@25171
   415
     |> fold interprete_parent parents
haftmann@38389
   416
     |> add_declaration full_name (declare_declinfo components')
schirmer@25171
   417
  end;
schirmer@25171
   418
schirmer@25171
   419
schirmer@25171
   420
(* prepare arguments *)
schirmer@25171
   421
wenzelm@36149
   422
fun read_typ ctxt raw_T env =
wenzelm@36149
   423
  let
wenzelm@36149
   424
    val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
wenzelm@36149
   425
    val T = Syntax.read_typ ctxt' raw_T;
wenzelm@45741
   426
    val env' = Term.add_tfreesT T env;
wenzelm@36149
   427
  in (T, env') end;
wenzelm@36149
   428
wenzelm@36149
   429
fun cert_typ ctxt raw_T env =
wenzelm@36149
   430
  let
wenzelm@42361
   431
    val thy = Proof_Context.theory_of ctxt;
wenzelm@36149
   432
    val T = Type.no_tvars (Sign.certify_typ thy raw_T)
wenzelm@36149
   433
      handle TYPE (msg, _, _) => error msg;
wenzelm@45741
   434
    val env' = Term.add_tfreesT T env;
wenzelm@36149
   435
  in (T, env') end;
wenzelm@36149
   436
schirmer@25171
   437
fun gen_define_statespace prep_typ state_space args name parents comps thy =
schirmer@25171
   438
  let (* - args distinct
schirmer@25171
   439
         - only args may occur in comps and parent-instantiations
wenzelm@26478
   440
         - number of insts must match parent args
schirmer@25171
   441
         - no duplicate renamings
schirmer@25171
   442
         - renaming should occur in namespace
schirmer@25171
   443
      *)
wenzelm@26478
   444
    val _ = writeln ("Defining statespace " ^ quote name ^ " ...");
schirmer@25171
   445
wenzelm@42361
   446
    val ctxt = Proof_Context.init_global thy;
wenzelm@27283
   447
wenzelm@49754
   448
    fun add_parent (prefix, (Ts, pname, rs)) env =
schirmer@25171
   449
      let
wenzelm@49754
   450
        val prefix' =
wenzelm@49754
   451
          (case prefix of
wenzelm@49754
   452
            ("", mandatory) => (pname, mandatory)
wenzelm@49754
   453
          | _ => prefix);
wenzelm@49754
   454
haftmann@28965
   455
        val full_pname = Sign.full_bname thy pname;
wenzelm@26478
   456
        val {args,components,...} =
schirmer@25171
   457
              (case get_statespace (Context.Theory thy) full_pname of
schirmer@25171
   458
                SOME r => r
schirmer@25171
   459
               | NONE => error ("Undefined statespace " ^ quote pname));
schirmer@25171
   460
schirmer@25171
   461
wenzelm@27283
   462
        val (Ts',env') = fold_map (prep_typ ctxt) Ts env
wenzelm@26478
   463
            handle ERROR msg => cat_error msg
wenzelm@36149
   464
                    ("The error(s) above occurred in parent statespace specification "
schirmer@25171
   465
                    ^ quote pname);
schirmer@25171
   466
        val err_insts = if length args <> length Ts' then
schirmer@25171
   467
            ["number of type instantiation(s) does not match arguments of parent statespace "
schirmer@25171
   468
              ^ quote pname]
schirmer@25171
   469
            else [];
wenzelm@26478
   470
schirmer@25171
   471
        val rnames = map fst rs
schirmer@25171
   472
        val err_dup_renamings = (case duplicates (op =) rnames of
schirmer@25171
   473
             [] => []
schirmer@25171
   474
            | dups => ["Duplicate renaming(s) for " ^ commas dups])
schirmer@25171
   475
schirmer@25171
   476
        val cnames = map fst components;
haftmann@36692
   477
        val err_rename_unknowns = (case subtract (op =) cnames rnames of
schirmer@25171
   478
              [] => []
schirmer@25171
   479
             | rs => ["Unknown components " ^ commas rs]);
wenzelm@26478
   480
schirmer@25171
   481
schirmer@25171
   482
        val rs' = map (AList.lookup (op =) rs o fst) components;
schirmer@25171
   483
        val errs =err_insts @ err_dup_renamings @ err_rename_unknowns
wenzelm@49754
   484
      in
wenzelm@49754
   485
        if null errs then ((prefix', (Ts', full_pname, rs')), env')
wenzelm@49754
   486
        else error (cat_lines (errs @ ["in parent statespace " ^ quote pname]))
schirmer@25171
   487
      end;
wenzelm@26478
   488
schirmer@25171
   489
    val (parents',env) = fold_map add_parent parents [];
schirmer@25171
   490
schirmer@25171
   491
    val err_dup_args =
schirmer@25171
   492
         (case duplicates (op =) args of
schirmer@25171
   493
            [] => []
schirmer@25171
   494
          | dups => ["Duplicate type argument(s) " ^ commas dups]);
wenzelm@26478
   495
schirmer@25171
   496
wenzelm@26478
   497
    val err_dup_components =
schirmer@25171
   498
         (case duplicates (op =) (map fst comps) of
schirmer@25171
   499
           [] => []
schirmer@25171
   500
          | dups => ["Duplicate state-space components " ^ commas dups]);
schirmer@25171
   501
schirmer@25171
   502
    fun prep_comp (n,T) env =
wenzelm@27283
   503
      let val (T', env') = prep_typ ctxt T env handle ERROR msg =>
wenzelm@36149
   504
       cat_error msg ("The error(s) above occurred in component " ^ quote n)
schirmer@25171
   505
      in ((n,T'), env') end;
schirmer@25171
   506
schirmer@25171
   507
    val (comps',env') = fold_map prep_comp comps env;
schirmer@25171
   508
schirmer@25171
   509
    val err_extra_frees =
schirmer@25171
   510
      (case subtract (op =) args (map fst env') of
schirmer@25171
   511
        [] => []
schirmer@25171
   512
      | extras => ["Extra free type variable(s) " ^ commas extras]);
schirmer@25171
   513
schirmer@25171
   514
    val defaultS = Sign.defaultS thy;
schirmer@25171
   515
    val args' = map (fn x => (x, AList.lookup (op =) env x |> the_default defaultS)) args;
schirmer@25171
   516
schirmer@25171
   517
schirmer@25171
   518
    fun fst_eq ((x:string,_),(y,_)) = x = y;
wenzelm@26478
   519
    fun snd_eq ((_,t:typ),(_,u)) = t = u;
schirmer@25171
   520
wenzelm@49754
   521
    val raw_parent_comps = maps (parent_components thy o snd) parents';
wenzelm@26478
   522
    fun check_type (n,T) =
schirmer@25171
   523
          (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
schirmer@25171
   524
             []  => []
schirmer@25171
   525
           | [_] => []
wenzelm@45660
   526
           | rs  => ["Different types for component " ^ quote n ^ ": " ^
wenzelm@32432
   527
                commas (map (Syntax.string_of_typ ctxt o snd) rs)])
wenzelm@26478
   528
wenzelm@32952
   529
    val err_dup_types = maps check_type (duplicates fst_eq raw_parent_comps)
schirmer@25171
   530
schirmer@25171
   531
    val parent_comps = distinct (fst_eq) raw_parent_comps;
schirmer@25171
   532
    val all_comps = parent_comps @ comps';
schirmer@25171
   533
    val err_comp_in_parent = (case duplicates (op =) (map fst all_comps) of
schirmer@25171
   534
               [] => []
wenzelm@45660
   535
             | xs => ["Components already defined in parents: " ^ commas_quote xs]);
schirmer@25171
   536
    val errs = err_dup_args @ err_dup_components @ err_extra_frees @
schirmer@25171
   537
               err_dup_types @ err_comp_in_parent;
wenzelm@26478
   538
  in if null errs
schirmer@25171
   539
     then thy |> statespace_definition state_space args' name parents' parent_comps comps'
wenzelm@26478
   540
     else error (cat_lines errs)
schirmer@25171
   541
  end
schirmer@25171
   542
  handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name);
wenzelm@26478
   543
wenzelm@36149
   544
val define_statespace = gen_define_statespace read_typ NONE;
wenzelm@36149
   545
val define_statespace_i = gen_define_statespace cert_typ;
wenzelm@26478
   546
schirmer@25171
   547
wenzelm@45362
   548
schirmer@25171
   549
(*** parse/print - translations ***)
schirmer@25171
   550
schirmer@25171
   551
local
wenzelm@55972
   552
wenzelm@26478
   553
fun map_get_comp f ctxt (Free (name,_)) =
wenzelm@26478
   554
      (case (get_comp ctxt name) of
wenzelm@26478
   555
        SOME (T,_) => f T T dummyT
schirmer@25171
   556
      | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*)))
schirmer@25171
   557
  | map_get_comp _ _ _ = Syntax.free "arbitrary";
schirmer@25171
   558
wenzelm@55972
   559
fun name_of (Free (n,_)) = n;
schirmer@25171
   560
schirmer@25171
   561
in
schirmer@25171
   562
wenzelm@26478
   563
fun gen_lookup_tr ctxt s n =
wenzelm@45362
   564
  (case get_comp (Context.Proof ctxt) n of
wenzelm@45362
   565
    SOME (T, _) =>
wenzelm@45362
   566
      Syntax.const @{const_name StateFun.lookup} $
wenzelm@45362
   567
        Syntax.free (project_name T) $ Syntax.free n $ s
wenzelm@45362
   568
  | NONE =>
wenzelm@45362
   569
      if get_silent (Context.Proof ctxt)
wenzelm@45362
   570
      then Syntax.const @{const_name StateFun.lookup} $
wenzelm@45362
   571
        Syntax.const @{const_syntax undefined} $ Syntax.free n $ s
wenzelm@45660
   572
      else raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", []));
schirmer@25171
   573
wenzelm@42052
   574
fun lookup_tr ctxt [s, x] =
wenzelm@42264
   575
  (case Term_Position.strip_positions x of
wenzelm@42052
   576
    Free (n,_) => gen_lookup_tr ctxt s n
wenzelm@42052
   577
  | _ => raise Match);
wenzelm@42052
   578
schirmer@25171
   579
fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n;
schirmer@25171
   580
wenzelm@45362
   581
fun lookup_tr' ctxt [_ $ Free (prj, _), n as (_ $ Free (name, _)), s] =
wenzelm@45362
   582
      (case get_comp (Context.Proof ctxt) name of
wenzelm@45362
   583
        SOME (T, _) =>
wenzelm@45362
   584
          if prj = project_name T
wenzelm@45362
   585
          then Syntax.const "_statespace_lookup" $ s $ n
wenzelm@45362
   586
          else raise Match
schirmer@25171
   587
      | NONE => raise Match)
wenzelm@55972
   588
  | lookup_tr' _ _ = raise Match;
schirmer@25171
   589
wenzelm@26478
   590
fun gen_update_tr id ctxt n v s =
schirmer@25171
   591
  let
wenzelm@45362
   592
    fun pname T = if id then @{const_name Fun.id} else project_name T;
wenzelm@45362
   593
    fun iname T = if id then @{const_name Fun.id} else inject_name T;
wenzelm@45362
   594
  in
wenzelm@45362
   595
    (case get_comp (Context.Proof ctxt) n of
wenzelm@45362
   596
      SOME (T, _) =>
wenzelm@45362
   597
        Syntax.const @{const_name StateFun.update} $
wenzelm@45362
   598
          Syntax.free (pname T) $ Syntax.free (iname T) $
wenzelm@45362
   599
          Syntax.free n $ (Syntax.const @{const_name K_statefun} $ v) $ s
wenzelm@45362
   600
    | NONE =>
wenzelm@45362
   601
        if get_silent (Context.Proof ctxt) then
wenzelm@45362
   602
          Syntax.const @{const_name StateFun.update} $
wenzelm@45362
   603
            Syntax.const @{const_syntax undefined} $ Syntax.const @{const_syntax undefined} $
wenzelm@45362
   604
            Syntax.free n $ (Syntax.const @{const_name K_statefun} $ v) $ s
wenzelm@45362
   605
       else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined", []))
schirmer@25171
   606
   end;
schirmer@25171
   607
wenzelm@42052
   608
fun update_tr ctxt [s, x, v] =
wenzelm@42264
   609
  (case Term_Position.strip_positions x of
wenzelm@42052
   610
    Free (n, _) => gen_update_tr false ctxt n v s
wenzelm@42052
   611
  | _ => raise Match);
schirmer@25171
   612
wenzelm@45362
   613
fun update_tr' ctxt
wenzelm@45362
   614
        [_ $ Free (prj, _), _ $ Free (inj, _), n as (_ $ Free (name, _)), (Const (k, _) $ v), s] =
wenzelm@45362
   615
      if Long_Name.base_name k = Long_Name.base_name @{const_name K_statefun} then
schirmer@25171
   616
        (case get_comp (Context.Proof ctxt) name of
wenzelm@45362
   617
          SOME (T, _) =>
wenzelm@45362
   618
            if inj = inject_name T andalso prj = project_name T then
wenzelm@45362
   619
              Syntax.const "_statespace_update" $ s $ n $ v
wenzelm@45362
   620
            else raise Match
wenzelm@45362
   621
        | NONE => raise Match)
schirmer@25171
   622
     else raise Match
schirmer@25171
   623
  | update_tr' _ _ = raise Match;
schirmer@25171
   624
schirmer@25171
   625
end;
schirmer@25171
   626
schirmer@25171
   627
schirmer@25171
   628
(*** outer syntax *)
schirmer@25171
   629
wenzelm@45362
   630
local
wenzelm@45362
   631
schirmer@25171
   632
val type_insts =
wenzelm@36960
   633
  Parse.typ >> single ||
wenzelm@46949
   634
  @{keyword "("} |-- Parse.!!! (Parse.list1 Parse.typ --| @{keyword ")"})
schirmer@25171
   635
wenzelm@46949
   636
val comp = Parse.name -- (@{keyword "::"} |-- Parse.!!! Parse.typ);
schirmer@25171
   637
fun plus1_unless test scan =
wenzelm@46949
   638
  scan ::: Scan.repeat (@{keyword "+"} |-- Scan.unless test (Parse.!!! scan));
schirmer@25171
   639
wenzelm@46949
   640
val mapsto = @{keyword "="};
wenzelm@36960
   641
val rename = Parse.name -- (mapsto |-- Parse.name);
wenzelm@46949
   642
val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
schirmer@25171
   643
wenzelm@45362
   644
val parent =
wenzelm@61606
   645
  Parse_Spec.locale_prefix --
wenzelm@45362
   646
  ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
wenzelm@49754
   647
    >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
schirmer@25171
   648
wenzelm@45362
   649
in
schirmer@25171
   650
schirmer@25171
   651
val statespace_decl =
wenzelm@45362
   652
  Parse.type_args -- Parse.name --
wenzelm@46949
   653
    (@{keyword "="} |--
wenzelm@45362
   654
      ((Scan.repeat1 comp >> pair []) ||
wenzelm@45362
   655
        (plus1_unless comp parent --
wenzelm@46949
   656
          Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
wenzelm@45362
   657
val _ =
wenzelm@59936
   658
  Outer_Syntax.command @{command_keyword statespace} "define state-space as locale context"
wenzelm@45362
   659
    (statespace_decl >> (fn ((args, name), (parents, comps)) =>
wenzelm@45362
   660
      Toplevel.theory (define_statespace args name parents comps)));
schirmer@25171
   661
wenzelm@45362
   662
end;
schirmer@25171
   663
wenzelm@45362
   664
end;