src/HOLCF/Tools/Domain/domain_extender.ML
author huffman
Thu Oct 14 13:46:27 2010 -0700 (2010-10-14)
changeset 40017 575d3aa1f3c5
parent 40016 2eff1cbc1ccb
child 40019 05cda34d36e7
permissions -rw-r--r--
include iso_info as part of constr_info type
haftmann@32126
     1
(*  Title:      HOLCF/Tools/Domain/domain_extender.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
wenzelm@23152
     8
signature DOMAIN_EXTENDER =
wenzelm@23152
     9
sig
huffman@33796
    10
  val add_domain_cmd:
huffman@35774
    11
      binding ->
huffman@33796
    12
      ((string * string option) list * binding * mixfix *
huffman@33796
    13
       (binding * (bool * binding option * string) list * mixfix) list) list
huffman@33796
    14
      -> theory -> theory
huffman@33796
    15
huffman@33796
    16
  val add_domain:
huffman@35774
    17
      binding ->
huffman@33796
    18
      ((string * string option) list * binding * mixfix *
huffman@33796
    19
       (binding * (bool * binding option * typ) list * mixfix) list) list
huffman@33796
    20
      -> theory -> theory
huffman@33798
    21
huffman@33798
    22
  val add_new_domain_cmd:
huffman@35774
    23
      binding ->
huffman@33798
    24
      ((string * string option) list * binding * mixfix *
huffman@33798
    25
       (binding * (bool * binding option * string) list * mixfix) list) list
huffman@33798
    26
      -> theory -> theory
huffman@33798
    27
huffman@33798
    28
  val add_new_domain:
huffman@35774
    29
      binding ->
huffman@33798
    30
      ((string * string option) list * binding * mixfix *
huffman@33798
    31
       (binding * (bool * binding option * typ) list * mixfix) list) list
huffman@33798
    32
      -> theory -> theory
wenzelm@23152
    33
end;
wenzelm@23152
    34
huffman@31023
    35
structure Domain_Extender :> DOMAIN_EXTENDER =
wenzelm@23152
    36
struct
wenzelm@23152
    37
wenzelm@23152
    38
open Domain_Library;
wenzelm@23152
    39
wenzelm@23152
    40
(* ----- general testing and preprocessing of constructor list -------------- *)
huffman@30919
    41
fun check_and_sort_domain
huffman@39965
    42
    (arg_sort : bool -> sort)
huffman@33796
    43
    (dtnvs : (string * typ list) list)
huffman@33796
    44
    (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
huffman@33798
    45
    (thy : theory)
huffman@31288
    46
    : ((string * typ list) *
huffman@31288
    47
       (binding * (bool * binding option * typ) list * mixfix) list) list =
huffman@33796
    48
  let
huffman@33798
    49
    val defaultS = Sign.defaultS thy;
huffman@33796
    50
huffman@33796
    51
    val test_dupl_typs =
huffman@33796
    52
      case duplicates (op =) (map fst dtnvs) of 
huffman@33796
    53
        [] => false | dups => error ("Duplicate types: " ^ commas_quote dups);
huffman@33796
    54
huffman@33796
    55
    val all_cons = map (Binding.name_of o first) (flat cons'');
huffman@33796
    56
    val test_dupl_cons =
huffman@33796
    57
      case duplicates (op =) all_cons of 
huffman@33796
    58
        [] => false | dups => error ("Duplicate constructors: " 
huffman@33796
    59
                                      ^ commas_quote dups);
huffman@33796
    60
    val all_sels =
huffman@33796
    61
      (map Binding.name_of o map_filter second o maps second) (flat cons'');
huffman@33796
    62
    val test_dupl_sels =
huffman@33796
    63
      case duplicates (op =) all_sels of
huffman@33796
    64
        [] => false | dups => error("Duplicate selectors: "^commas_quote dups);
huffman@33796
    65
huffman@33796
    66
    fun test_dupl_tvars s =
huffman@33796
    67
      case duplicates (op =) (map(fst o dest_TFree)s) of
huffman@33796
    68
        [] => false | dups => error("Duplicate type arguments: " 
huffman@33796
    69
                                    ^commas_quote dups);
huffman@33796
    70
    val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs);
huffman@33796
    71
huffman@33796
    72
    (* test for free type variables, illegal sort constraints on rhs,
huffman@33796
    73
       non-pcpo-types and invalid use of recursive type;
huffman@33796
    74
       replace sorts in type variables on rhs *)
huffman@33796
    75
    fun analyse_equation ((dname,typevars),cons') = 
huffman@33796
    76
      let
huffman@33796
    77
        val tvars = map dest_TFree typevars;
huffman@33796
    78
        val distinct_typevars = map TFree tvars;
huffman@33796
    79
        fun rm_sorts (TFree(s,_)) = TFree(s,[])
huffman@33796
    80
          | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
huffman@33796
    81
          | rm_sorts (TVar(s,_))  = TVar(s,[])
huffman@33796
    82
        and remove_sorts l = map rm_sorts l;
huffman@33796
    83
        fun analyse indirect (TFree(v,s))  =
huffman@33796
    84
            (case AList.lookup (op =) tvars v of 
huffman@33796
    85
               NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
huffman@33796
    86
             | SOME sort => if eq_set (op =) (s, defaultS) orelse
huffman@33796
    87
                               eq_set (op =) (s, sort)
huffman@33796
    88
                            then TFree(v,sort)
huffman@33796
    89
                            else error ("Inconsistent sort constraint" ^
huffman@33796
    90
                                        " for type variable " ^ quote v))
huffman@33796
    91
          | analyse indirect (t as Type(s,typl)) =
huffman@33796
    92
            (case AList.lookup (op =) dtnvs s of
huffman@36119
    93
               NONE => Type (s, map (analyse false) typl)
huffman@33796
    94
             | SOME typevars =>
huffman@33796
    95
                 if indirect 
huffman@33796
    96
                 then error ("Indirect recursion of type " ^ 
huffman@33798
    97
                             quote (string_of_typ thy t))
huffman@33796
    98
                 else if dname <> s orelse
huffman@33796
    99
                         (** BUG OR FEATURE?:
huffman@33796
   100
                             mutual recursion may use different arguments **)
huffman@33796
   101
                         remove_sorts typevars = remove_sorts typl 
huffman@33796
   102
                 then Type(s,map (analyse true) typl)
huffman@33796
   103
                 else error ("Direct recursion of type " ^ 
huffman@33798
   104
                             quote (string_of_typ thy t) ^ 
huffman@33796
   105
                             " with different arguments"))
huffman@33796
   106
          | analyse indirect (TVar _) = Imposs "extender:analyse";
huffman@33796
   107
        fun check_pcpo lazy T =
huffman@39965
   108
            let val sort = arg_sort lazy in
huffman@39965
   109
              if Sign.of_sort thy (T, sort) then T
huffman@39965
   110
              else error ("Constructor argument type is not of sort " ^
huffman@39965
   111
                          Syntax.string_of_sort_global thy sort ^ ": " ^
huffman@39965
   112
                          string_of_typ thy T)
huffman@33796
   113
            end;
huffman@33796
   114
        fun analyse_arg (lazy, sel, T) =
huffman@33796
   115
            (lazy, sel, check_pcpo lazy (analyse false T));
huffman@33796
   116
        fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
huffman@33796
   117
      in ((dname,distinct_typevars), map analyse_con cons') end; 
huffman@33796
   118
  in ListPair.map analyse_equation (dtnvs,cons'')
huffman@33796
   119
  end; (* let *)
wenzelm@23152
   120
wenzelm@23152
   121
(* ----- calls for building new thy and thms -------------------------------- *)
wenzelm@23152
   122
huffman@36118
   123
type info =
huffman@36118
   124
     Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info;
huffman@36118
   125
huffman@30919
   126
fun gen_add_domain
huffman@33796
   127
    (prep_typ : theory -> 'a -> typ)
huffman@36118
   128
    (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
huffman@39965
   129
    (arg_sort : bool -> sort)
huffman@35774
   130
    (comp_dbind : binding)
huffman@33798
   131
    (eqs''' : ((string * string option) list * binding * mixfix *
huffman@33798
   132
               (binding * (bool * binding option * 'a) list * mixfix) list) list)
huffman@35516
   133
    (thy : theory) =
huffman@33798
   134
  let
huffman@35520
   135
    val dtnvs : (binding * typ list * mixfix) list =
huffman@35520
   136
      let
huffman@35520
   137
        fun readS (SOME s) = Syntax.read_sort_global thy s
huffman@35520
   138
          | readS NONE = Sign.defaultS thy;
huffman@35520
   139
        fun readTFree (a, s) = TFree (a, readS s);
huffman@35520
   140
      in
huffman@35520
   141
        map (fn (vs,dname:binding,mx,_) =>
huffman@35520
   142
                (dname, map readTFree vs, mx)) eqs'''
huffman@35520
   143
      end;
huffman@33798
   144
huffman@33798
   145
    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
huffman@33798
   146
    fun thy_arity (dname,tvars,mx) =
huffman@39974
   147
      (Sign.full_name thy dname, map (snd o dest_TFree) tvars, arg_sort false);
huffman@33798
   148
huffman@33798
   149
    (* this theory is used just for parsing and error checking *)
huffman@35516
   150
    val tmp_thy = thy
huffman@33798
   151
      |> Theory.copy
huffman@33798
   152
      |> Sign.add_types (map thy_type dtnvs)
huffman@33798
   153
      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
huffman@33798
   154
huffman@35776
   155
    val dbinds : binding list =
huffman@35776
   156
        map (fn (_,dbind,_,_) => dbind) eqs''';
huffman@35520
   157
    val cons''' :
huffman@35520
   158
        (binding * (bool * binding option * 'a) list * mixfix) list list =
huffman@35520
   159
        map (fn (_,_,_,cons) => cons) eqs''';
huffman@35520
   160
    val cons'' :
huffman@35520
   161
        (binding * (bool * binding option * typ) list * mixfix) list list =
huffman@35520
   162
        map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
huffman@33798
   163
    val dtnvs' : (string * typ list) list =
huffman@35520
   164
        map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
huffman@33798
   165
    val eqs' : ((string * typ list) *
huffman@33798
   166
        (binding * (bool * binding option * typ) list * mixfix) list) list =
huffman@39965
   167
        check_and_sort_domain arg_sort dtnvs' cons'' tmp_thy;
huffman@36118
   168
    val dts : typ list = map (Type o fst) eqs';
huffman@33798
   169
huffman@33798
   170
    fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
huffman@33798
   171
    fun mk_con_typ (bind, args, mx) =
huffman@33798
   172
        if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
huffman@33798
   173
    fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
huffman@36118
   174
    val repTs : typ list = map mk_eq_typ eqs';
huffman@33798
   175
huffman@36118
   176
    val iso_spec : (binding * mixfix * (typ * typ)) list =
huffman@36118
   177
        map (fn ((dbind, _, mx), eq) => (dbind, mx, eq))
huffman@36118
   178
          (dtnvs ~~ (dts ~~ repTs));
huffman@36118
   179
huffman@36118
   180
    val ((iso_infos, take_info), thy) = add_isos iso_spec thy;
huffman@36118
   181
huffman@35520
   182
    val new_dts : (string * string list) list =
huffman@35520
   183
        map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
huffman@35520
   184
    fun one_con (con,args,mx) : cons =
huffman@36118
   185
        (Binding.name_of con,  (* FIXME preverse binding (!?) *)
huffman@33798
   186
         ListPair.map (fn ((lazy,sel,tp),vn) =>
huffman@35519
   187
           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
huffman@36118
   188
                      (args, Datatype_Prop.make_tnames (map third args)));
huffman@33798
   189
    val eqs : eq list =
huffman@33798
   190
        map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
huffman@36118
   191
huffman@40016
   192
    val (constr_infos, thy) =
huffman@33796
   193
        thy
huffman@40016
   194
          |> fold_map (fn ((dbind, (_,cs)), info) =>
huffman@40016
   195
                Domain_Constructors.add_domain_constructors dbind cs info)
huffman@40016
   196
             (dbinds ~~ eqs' ~~ iso_infos);
huffman@40016
   197
huffman@40016
   198
    val (take_rews, theorems_thy) =
huffman@40016
   199
        thy
huffman@40016
   200
          |> Domain_Theorems.comp_theorems (comp_dbind, eqs)
huffman@40017
   201
              (dbinds ~~ map snd eqs') take_info constr_infos;
huffman@33796
   202
  in
huffman@33796
   203
    theorems_thy
huffman@33796
   204
  end;
wenzelm@23152
   205
huffman@36118
   206
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
huffman@36118
   207
  let
huffman@36118
   208
    fun prep (dbind, mx, (lhsT, rhsT)) =
huffman@36118
   209
      let val (dname, vs) = dest_Type lhsT;
huffman@36118
   210
      in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end;
huffman@36118
   211
  in
huffman@36118
   212
    Domain_Isomorphism.domain_isomorphism (map prep spec)
huffman@36118
   213
  end;
wenzelm@23152
   214
huffman@39965
   215
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
huffman@39986
   216
fun rep_arg lazy = @{sort bifinite};
huffman@39965
   217
huffman@36118
   218
val add_domain =
huffman@39965
   219
    gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg;
huffman@36118
   220
huffman@36118
   221
val add_new_domain =
huffman@39965
   222
    gen_add_domain Sign.certify_typ define_isos rep_arg;
huffman@36118
   223
huffman@36118
   224
val add_domain_cmd =
huffman@39965
   225
    gen_add_domain Syntax.read_typ_global Domain_Axioms.add_axioms pcpo_arg;
huffman@36118
   226
huffman@36118
   227
val add_new_domain_cmd =
huffman@39965
   228
    gen_add_domain Syntax.read_typ_global define_isos rep_arg;
huffman@33798
   229
wenzelm@23152
   230
wenzelm@23152
   231
(** outer syntax **)
wenzelm@23152
   232
wenzelm@36960
   233
val _ = Keyword.keyword "lazy";
wenzelm@24867
   234
huffman@30919
   235
val dest_decl : (bool * binding option * string) parser =
wenzelm@36960
   236
  Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
wenzelm@36960
   237
    (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ)  --| Parse.$$$ ")" >> Parse.triple1
wenzelm@36960
   238
    || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
huffman@33796
   239
    >> (fn t => (true,NONE,t))
wenzelm@36960
   240
    || Parse.typ >> (fn t => (false,NONE,t));
wenzelm@23152
   241
wenzelm@23152
   242
val cons_decl =
wenzelm@36960
   243
  Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix;
huffman@30916
   244
huffman@30916
   245
val domain_decl =
wenzelm@36960
   246
  (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
wenzelm@36960
   247
    (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
wenzelm@23152
   248
huffman@30916
   249
val domains_decl =
wenzelm@36960
   250
  Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
wenzelm@36960
   251
    Parse.and_list1 domain_decl;
wenzelm@23152
   252
huffman@33796
   253
fun mk_domain
huffman@33798
   254
    (definitional : bool)
huffman@35774
   255
    (opt_name : binding option,
huffman@33796
   256
     doms : ((((string * string option) list * binding) * mixfix) *
huffman@33796
   257
             ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
huffman@33796
   258
  let
huffman@33796
   259
    val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
huffman@33796
   260
    val specs : ((string * string option) list * binding * mixfix *
huffman@33796
   261
                 (binding * (bool * binding option * string) list * mixfix) list) list =
huffman@33796
   262
        map (fn (((vs, t), mx), cons) =>
huffman@33796
   263
                (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
huffman@35774
   264
    val comp_dbind =
huffman@35774
   265
        case opt_name of NONE => Binding.name (space_implode "_" names)
huffman@35774
   266
                       | SOME s => s;
huffman@33798
   267
  in
huffman@33798
   268
    if definitional 
huffman@35774
   269
    then add_new_domain_cmd comp_dbind specs
huffman@35774
   270
    else add_domain_cmd comp_dbind specs
huffman@33798
   271
  end;
wenzelm@23152
   272
wenzelm@24867
   273
val _ =
wenzelm@36960
   274
  Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
wenzelm@36960
   275
    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
huffman@33798
   276
huffman@33798
   277
val _ =
wenzelm@36960
   278
  Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
wenzelm@36960
   279
    Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
wenzelm@23152
   280
wenzelm@24867
   281
end;