src/HOL/HOLCF/Tools/Domain/domain.ML
author huffman
Sun Dec 19 18:15:21 2010 -0800 (2010-12-19)
changeset 41296 6aaf80ea9715
parent 40832 4352ca878c41
child 42151 4da4fc77664b
permissions -rw-r--r--
switch to transparent ascription, to avoid warning messages
huffman@40040
     1
(*  Title:      HOLCF/Tools/Domain/domain.ML
wenzelm@23152
     2
    Author:     David von Oheimb
huffman@35794
     3
    Author:     Brian Huffman
wenzelm@23152
     4
wenzelm@23152
     5
Theory extender for domain command, including theory syntax.
wenzelm@23152
     6
*)
wenzelm@23152
     7
huffman@40040
     8
signature DOMAIN =
wenzelm@23152
     9
sig
huffman@33796
    10
  val add_domain_cmd:
huffman@33796
    11
      ((string * string option) list * binding * mixfix *
huffman@33796
    12
       (binding * (bool * binding option * string) list * mixfix) list) list
huffman@33796
    13
      -> theory -> theory
huffman@33796
    14
huffman@33796
    15
  val add_domain:
huffman@40215
    16
      ((string * sort) list * binding * mixfix *
huffman@33796
    17
       (binding * (bool * binding option * typ) list * mixfix) list) list
huffman@33796
    18
      -> theory -> theory
huffman@33798
    19
huffman@33798
    20
  val add_new_domain_cmd:
huffman@33798
    21
      ((string * string option) list * binding * mixfix *
huffman@33798
    22
       (binding * (bool * binding option * string) list * mixfix) list) list
huffman@33798
    23
      -> theory -> theory
huffman@33798
    24
huffman@33798
    25
  val add_new_domain:
huffman@40215
    26
      ((string * sort) list * binding * mixfix *
huffman@33798
    27
       (binding * (bool * binding option * typ) list * mixfix) list) list
huffman@33798
    28
      -> theory -> theory
huffman@40832
    29
end
wenzelm@23152
    30
huffman@41296
    31
structure Domain : DOMAIN =
wenzelm@23152
    32
struct
wenzelm@23152
    33
huffman@40832
    34
open HOLCF_Library
huffman@40026
    35
huffman@40832
    36
fun first  (x,_,_) = x
huffman@40832
    37
fun second (_,x,_) = x
huffman@40832
    38
fun third  (_,_,x) = x
huffman@40026
    39
wenzelm@23152
    40
(* ----- calls for building new thy and thms -------------------------------- *)
wenzelm@23152
    41
huffman@36118
    42
type info =
huffman@40832
    43
     Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info
huffman@36118
    44
huffman@40485
    45
fun add_arity ((b, sorts, mx), sort) thy : theory =
huffman@40485
    46
  thy
huffman@40485
    47
  |> Sign.add_types [(b, length sorts, mx)]
huffman@40832
    48
  |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
huffman@40485
    49
huffman@30919
    50
fun gen_add_domain
huffman@40215
    51
    (prep_sort : theory -> 'a -> sort)
huffman@40215
    52
    (prep_typ : theory -> (string * sort) list -> 'b -> typ)
huffman@36118
    53
    (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
huffman@39965
    54
    (arg_sort : bool -> sort)
huffman@40215
    55
    (raw_specs : ((string * 'a) list * binding * mixfix *
huffman@40215
    56
               (binding * (bool * binding option * 'b) list * mixfix) list) list)
huffman@35516
    57
    (thy : theory) =
huffman@33798
    58
  let
huffman@35520
    59
    val dtnvs : (binding * typ list * mixfix) list =
huffman@35520
    60
      let
huffman@40832
    61
        fun prep_tvar (a, s) = TFree (a, prep_sort thy s)
huffman@35520
    62
      in
huffman@40044
    63
        map (fn (vs, dbind, mx, _) =>
huffman@40215
    64
                (dbind, map prep_tvar vs, mx)) raw_specs
huffman@40832
    65
      end
huffman@33798
    66
huffman@40042
    67
    fun thy_arity (dbind, tvars, mx) =
huffman@40832
    68
      ((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false)
huffman@33798
    69
huffman@33798
    70
    (* this theory is used just for parsing and error checking *)
huffman@35516
    71
    val tmp_thy = thy
huffman@33798
    72
      |> Theory.copy
huffman@40832
    73
      |> fold (add_arity o thy_arity) dtnvs
huffman@33798
    74
huffman@35776
    75
    val dbinds : binding list =
huffman@40832
    76
        map (fn (_,dbind,_,_) => dbind) raw_specs
huffman@40044
    77
    val raw_rhss :
huffman@40215
    78
        (binding * (bool * binding option * 'b) list * mixfix) list list =
huffman@40832
    79
        map (fn (_,_,_,cons) => cons) raw_specs
huffman@33798
    80
    val dtnvs' : (string * typ list) list =
huffman@40832
    81
        map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs
huffman@40044
    82
huffman@40832
    83
    val all_cons = map (Binding.name_of o first) (flat raw_rhss)
huffman@40044
    84
    val test_dupl_cons =
huffman@40044
    85
      case duplicates (op =) all_cons of 
huffman@40044
    86
        [] => false | dups => error ("Duplicate constructors: " 
huffman@40832
    87
                                      ^ commas_quote dups)
huffman@40044
    88
    val all_sels =
huffman@40832
    89
      (map Binding.name_of o map_filter second o maps second) (flat raw_rhss)
huffman@40044
    90
    val test_dupl_sels =
huffman@40044
    91
      case duplicates (op =) all_sels of
huffman@40832
    92
        [] => false | dups => error("Duplicate selectors: "^commas_quote dups)
huffman@40044
    93
huffman@40044
    94
    fun test_dupl_tvars s =
huffman@40044
    95
      case duplicates (op =) (map(fst o dest_TFree)s) of
huffman@40044
    96
        [] => false | dups => error("Duplicate type arguments: " 
huffman@40832
    97
                                    ^commas_quote dups)
huffman@40832
    98
    val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs')
huffman@40044
    99
huffman@40044
   100
    val sorts : (string * sort) list =
huffman@40832
   101
      let val all_sorts = map (map dest_TFree o snd) dtnvs'
huffman@40044
   102
      in
huffman@40044
   103
        case distinct (eq_set (op =)) all_sorts of
huffman@40044
   104
          [sorts] => sorts
huffman@40044
   105
        | _ => error "Mutually recursive domains must have same type parameters"
huffman@40832
   106
      end
huffman@40044
   107
huffman@40044
   108
    (* a lazy argument may have an unpointed type *)
huffman@40044
   109
    (* unless the argument has a selector function *)
huffman@40044
   110
    fun check_pcpo (lazy, sel, T) =
huffman@40044
   111
      let val sort = arg_sort (lazy andalso is_none sel) in
huffman@40044
   112
        if Sign.of_sort tmp_thy (T, sort) then ()
huffman@40044
   113
        else error ("Constructor argument type is not of sort " ^
huffman@40044
   114
                    Syntax.string_of_sort_global tmp_thy sort ^ ": " ^
huffman@40044
   115
                    Syntax.string_of_typ_global tmp_thy T)
huffman@40832
   116
      end
huffman@40044
   117
huffman@40044
   118
    (* test for free type variables, illegal sort constraints on rhs,
huffman@40832
   119
       non-pcpo-types and invalid use of recursive type
huffman@40044
   120
       replace sorts in type variables on rhs *)
huffman@40832
   121
    val rec_tab = Domain_Take_Proofs.get_rec_tab thy
huffman@40044
   122
    fun check_rec rec_ok (T as TFree (v,_))  =
huffman@40044
   123
        if AList.defined (op =) sorts v then T
huffman@40044
   124
        else error ("Free type variable " ^ quote v ^ " on rhs.")
huffman@40044
   125
      | check_rec rec_ok (T as Type (s, Ts)) =
huffman@40044
   126
        (case AList.lookup (op =) dtnvs' s of
huffman@40044
   127
          NONE =>
huffman@40832
   128
            let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s
huffman@40044
   129
            in Type (s, map (check_rec rec_ok') Ts) end
huffman@40044
   130
        | SOME typevars =>
huffman@40044
   131
          if typevars <> Ts
huffman@40044
   132
          then error ("Recursion of type " ^ 
huffman@40044
   133
                      quote (Syntax.string_of_typ_global tmp_thy T) ^ 
huffman@40044
   134
                      " with different arguments")
huffman@40044
   135
          else if rec_ok then T
huffman@40044
   136
          else error ("Illegal indirect recursion of type " ^ 
huffman@40044
   137
                      quote (Syntax.string_of_typ_global tmp_thy T)))
huffman@40832
   138
      | check_rec rec_ok (TVar _) = error "extender:check_rec"
huffman@40044
   139
huffman@40044
   140
    fun prep_arg (lazy, sel, raw_T) =
huffman@40044
   141
      let
huffman@40832
   142
        val T = prep_typ tmp_thy sorts raw_T
huffman@40832
   143
        val _ = check_rec true T
huffman@40832
   144
        val _ = check_pcpo (lazy, sel, T)
huffman@40832
   145
      in (lazy, sel, T) end
huffman@40832
   146
    fun prep_con (b, args, mx) = (b, map prep_arg args, mx)
huffman@40832
   147
    fun prep_rhs cons = map prep_con cons
huffman@40044
   148
    val rhss : (binding * (bool * binding option * typ) list * mixfix) list list =
huffman@40832
   149
        map prep_rhs raw_rhss
huffman@33798
   150
huffman@40832
   151
    fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T
huffman@33798
   152
    fun mk_con_typ (bind, args, mx) =
huffman@40832
   153
        if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args)
huffman@40832
   154
    fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons)
huffman@40042
   155
huffman@40832
   156
    val absTs : typ list = map Type dtnvs'
huffman@40832
   157
    val repTs : typ list = map mk_rhs_typ rhss
huffman@33798
   158
huffman@36118
   159
    val iso_spec : (binding * mixfix * (typ * typ)) list =
huffman@36118
   160
        map (fn ((dbind, _, mx), eq) => (dbind, mx, eq))
huffman@40832
   161
          (dtnvs ~~ (absTs ~~ repTs))
huffman@36118
   162
huffman@40832
   163
    val ((iso_infos, take_info), thy) = add_isos iso_spec thy
huffman@36118
   164
huffman@40016
   165
    val (constr_infos, thy) =
huffman@33796
   166
        thy
huffman@40042
   167
          |> fold_map (fn ((dbind, cons), info) =>
huffman@40042
   168
                Domain_Constructors.add_domain_constructors dbind cons info)
huffman@40832
   169
             (dbinds ~~ rhss ~~ iso_infos)
huffman@40016
   170
huffman@40026
   171
    val (take_rews, thy) =
huffman@40097
   172
        Domain_Induction.comp_theorems
huffman@40832
   173
          dbinds take_info constr_infos thy
huffman@33796
   174
  in
huffman@40026
   175
    thy
huffman@40832
   176
  end
wenzelm@23152
   177
huffman@36118
   178
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
huffman@36118
   179
  let
huffman@36118
   180
    fun prep (dbind, mx, (lhsT, rhsT)) =
huffman@40832
   181
      let val (dname, vs) = dest_Type lhsT
huffman@40832
   182
      in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end
huffman@36118
   183
  in
huffman@36118
   184
    Domain_Isomorphism.domain_isomorphism (map prep spec)
huffman@40832
   185
  end
wenzelm@23152
   186
huffman@40832
   187
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo}
huffman@40832
   188
fun rep_arg lazy = if lazy then @{sort predomain} else @{sort "domain"}
huffman@39965
   189
huffman@40215
   190
fun read_sort thy (SOME s) = Syntax.read_sort_global thy s
huffman@40832
   191
  | read_sort thy NONE = Sign.defaultS thy
huffman@40215
   192
huffman@40044
   193
(* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *)
huffman@40044
   194
fun read_typ thy sorts str =
huffman@40044
   195
  let
huffman@40044
   196
    val ctxt = ProofContext.init_global thy
huffman@40832
   197
      |> fold (Variable.declare_typ o TFree) sorts
huffman@40832
   198
  in Syntax.read_typ ctxt str end
huffman@40044
   199
huffman@40044
   200
fun cert_typ sign sorts raw_T =
huffman@40044
   201
  let
huffman@40044
   202
    val T = Type.no_tvars (Sign.certify_typ sign raw_T)
huffman@40832
   203
      handle TYPE (msg, _, _) => error msg
huffman@40832
   204
    val sorts' = Term.add_tfreesT T sorts
huffman@40044
   205
    val _ =
huffman@40044
   206
      case duplicates (op =) (map fst sorts') of
huffman@40044
   207
        [] => ()
huffman@40044
   208
      | dups => error ("Inconsistent sort constraints for " ^ commas dups)
huffman@40832
   209
  in T end
huffman@40044
   210
huffman@36118
   211
val add_domain =
huffman@40832
   212
    gen_add_domain (K I) cert_typ Domain_Axioms.add_axioms pcpo_arg
huffman@36118
   213
huffman@36118
   214
val add_new_domain =
huffman@40832
   215
    gen_add_domain (K I) cert_typ define_isos rep_arg
huffman@36118
   216
huffman@36118
   217
val add_domain_cmd =
huffman@40832
   218
    gen_add_domain read_sort read_typ Domain_Axioms.add_axioms pcpo_arg
huffman@36118
   219
huffman@36118
   220
val add_new_domain_cmd =
huffman@40832
   221
    gen_add_domain read_sort read_typ define_isos rep_arg
huffman@33798
   222
wenzelm@23152
   223
wenzelm@23152
   224
(** outer syntax **)
wenzelm@23152
   225
huffman@40832
   226
val _ = Keyword.keyword "lazy"
huffman@40832
   227
val _ = Keyword.keyword "unsafe"
wenzelm@24867
   228
huffman@30919
   229
val dest_decl : (bool * binding option * string) parser =
wenzelm@36960
   230
  Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
wenzelm@36960
   231
    (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ)  --| Parse.$$$ ")" >> Parse.triple1
wenzelm@36960
   232
    || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
huffman@33796
   233
    >> (fn t => (true,NONE,t))
huffman@40832
   234
    || Parse.typ >> (fn t => (false,NONE,t))
wenzelm@23152
   235
wenzelm@23152
   236
val cons_decl =
huffman@40832
   237
  Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix
huffman@30916
   238
huffman@30916
   239
val domain_decl =
wenzelm@36960
   240
  (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
huffman@40832
   241
    (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl)
wenzelm@23152
   242
huffman@30916
   243
val domains_decl =
huffman@40329
   244
  Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unsafe" >> K true) --| Parse.$$$ ")") false --
huffman@40832
   245
    Parse.and_list1 domain_decl
wenzelm@23152
   246
huffman@33796
   247
fun mk_domain
huffman@40329
   248
    (unsafe : bool,
huffman@40329
   249
     doms : ((((string * string option) list * binding) * mixfix) *
huffman@33796
   250
             ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
huffman@33796
   251
  let
huffman@33796
   252
    val specs : ((string * string option) list * binding * mixfix *
huffman@33796
   253
                 (binding * (bool * binding option * string) list * mixfix) list) list =
huffman@33796
   254
        map (fn (((vs, t), mx), cons) =>
huffman@40832
   255
                (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms
huffman@33798
   256
  in
huffman@40329
   257
    if unsafe
huffman@40329
   258
    then add_domain_cmd specs
huffman@40329
   259
    else add_new_domain_cmd specs
huffman@40832
   260
  end
wenzelm@23152
   261
wenzelm@24867
   262
val _ =
wenzelm@36960
   263
  Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
huffman@40832
   264
    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain))
wenzelm@23152
   265
huffman@40832
   266
end