src/HOLCF/Tools/Domain/domain_extender.ML
author haftmann
Tue Jul 21 16:14:56 2009 +0200 (2009-07-21)
changeset 32126 a5042f260440
parent 31986 src/HOLCF/Tools/domain/domain_extender.ML@a68f88d264f7
child 32952 aeb1e44fbc19
permissions -rw-r--r--
obey captialized directory names convention
haftmann@32126
     1
(*  Title:      HOLCF/Tools/Domain/domain_extender.ML
wenzelm@23152
     2
    Author:     David von Oheimb
wenzelm@23152
     3
wenzelm@23152
     4
Theory extender for domain command, including theory syntax.
wenzelm@23152
     5
*)
wenzelm@23152
     6
wenzelm@23152
     7
signature DOMAIN_EXTENDER =
wenzelm@23152
     8
sig
huffman@31161
     9
  val add_domain_cmd: string ->
huffman@31288
    10
                      ((string * string option) list * binding * mixfix *
huffman@31288
    11
                       (binding * (bool * binding option * string) list * mixfix) list) list
huffman@31288
    12
                      -> theory -> theory
huffman@31161
    13
  val add_domain: string ->
huffman@31288
    14
                  ((string * string option) list * binding * mixfix *
huffman@31288
    15
                   (binding * (bool * binding option * typ) list * mixfix) list) list
huffman@31288
    16
                  -> theory -> theory
wenzelm@23152
    17
end;
wenzelm@23152
    18
huffman@31023
    19
structure Domain_Extender :> DOMAIN_EXTENDER =
wenzelm@23152
    20
struct
wenzelm@23152
    21
wenzelm@23152
    22
open Domain_Library;
wenzelm@23152
    23
wenzelm@23152
    24
(* ----- general testing and preprocessing of constructor list -------------- *)
huffman@30919
    25
fun check_and_sort_domain
huffman@31288
    26
      (dtnvs : (string * typ list) list)
huffman@31288
    27
      (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
huffman@31288
    28
      (sg : theory)
huffman@31288
    29
    : ((string * typ list) *
huffman@31288
    30
       (binding * (bool * binding option * typ) list * mixfix) list) list =
huffman@31288
    31
    let
huffman@31288
    32
      val defaultS = Sign.defaultS sg;
huffman@31288
    33
      val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
huffman@31288
    34
                              [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
huffman@31288
    35
      val test_dupl_cons =
huffman@31288
    36
          (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of 
huffman@31288
    37
             [] => false | dups => error ("Duplicate constructors: " 
huffman@31288
    38
                                          ^ commas_quote dups));
huffman@31288
    39
      val test_dupl_sels =
huffman@31288
    40
          (case duplicates (op =) (map Binding.name_of (List.mapPartial second
huffman@31288
    41
                                                                        (List.concat (map second (List.concat cons''))))) of
huffman@31288
    42
             [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
huffman@31288
    43
      val test_dupl_tvars =
huffman@31288
    44
          exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
huffman@31288
    45
                         [] => false | dups => error("Duplicate type arguments: " 
huffman@31288
    46
                                                     ^commas_quote dups)) (map snd dtnvs);
huffman@31288
    47
      (* test for free type variables, illegal sort constraints on rhs,
huffman@31288
    48
         non-pcpo-types and invalid use of recursive type;
huffman@31288
    49
         replace sorts in type variables on rhs *)
huffman@31288
    50
      fun analyse_equation ((dname,typevars),cons') = 
huffman@31288
    51
          let
huffman@31288
    52
            val tvars = map dest_TFree typevars;
huffman@31288
    53
            val distinct_typevars = map TFree tvars;
huffman@31288
    54
            fun rm_sorts (TFree(s,_)) = TFree(s,[])
huffman@31288
    55
              | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
huffman@31288
    56
              | rm_sorts (TVar(s,_))  = TVar(s,[])
huffman@31288
    57
            and remove_sorts l = map rm_sorts l;
huffman@31288
    58
            val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
huffman@31288
    59
            fun analyse indirect (TFree(v,s))  =
huffman@31288
    60
                (case AList.lookup (op =) tvars v of 
huffman@31288
    61
                   NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
huffman@31288
    62
                 | SOME sort => if eq_set_string (s,defaultS) orelse
huffman@31288
    63
                                   eq_set_string (s,sort    )
huffman@31288
    64
                                then TFree(v,sort)
huffman@31288
    65
                                else error ("Inconsistent sort constraint" ^
huffman@31288
    66
                                            " for type variable " ^ quote v))
huffman@31288
    67
              | analyse indirect (t as Type(s,typl)) =
huffman@31288
    68
                (case AList.lookup (op =) dtnvs s of
huffman@31288
    69
                   NONE          => if s mem indirect_ok
huffman@31288
    70
                                    then Type(s,map (analyse false) typl)
huffman@31288
    71
                                    else Type(s,map (analyse true) typl)
huffman@31288
    72
                 | SOME typevars => if indirect 
huffman@31288
    73
                                    then error ("Indirect recursion of type " ^ 
huffman@31288
    74
                                                quote (string_of_typ sg t))
huffman@31288
    75
                                    else if dname <> s orelse
huffman@31288
    76
                                            (** BUG OR FEATURE?:
huffman@31288
    77
                                                mutual recursion may use different arguments **)
huffman@31288
    78
                                            remove_sorts typevars = remove_sorts typl 
huffman@31288
    79
                                    then Type(s,map (analyse true) typl)
huffman@31288
    80
                                    else error ("Direct recursion of type " ^ 
huffman@31288
    81
                                                quote (string_of_typ sg t) ^ 
huffman@31288
    82
                                                " with different arguments"))
huffman@31288
    83
              | analyse indirect (TVar _) = Imposs "extender:analyse";
huffman@31288
    84
            fun check_pcpo lazy T =
huffman@31288
    85
                let val ok = if lazy then cpo_type else pcpo_type
huffman@31288
    86
                in if ok sg T then T else error
huffman@31288
    87
                                            ("Constructor argument type is not of sort pcpo: " ^
huffman@31288
    88
                                             string_of_typ sg T)
huffman@31288
    89
                end;
huffman@31288
    90
            fun analyse_arg (lazy, sel, T) =
huffman@31288
    91
                (lazy, sel, check_pcpo lazy (analyse false T));
huffman@31288
    92
            fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
huffman@31288
    93
          in ((dname,distinct_typevars), map analyse_con cons') end; 
huffman@31288
    94
    in ListPair.map analyse_equation (dtnvs,cons'')
huffman@31288
    95
    end; (* let *)
wenzelm@23152
    96
wenzelm@23152
    97
(* ----- calls for building new thy and thms -------------------------------- *)
wenzelm@23152
    98
huffman@30919
    99
fun gen_add_domain
huffman@31288
   100
      (prep_typ : theory -> 'a -> typ)
huffman@31288
   101
      (comp_dnam : string)
huffman@31288
   102
      (eqs''' : ((string * string option) list * binding * mixfix *
huffman@31288
   103
                 (binding * (bool * binding option * 'a) list * mixfix) list) list)
huffman@31288
   104
      (thy''' : theory) =
huffman@31288
   105
    let
huffman@31288
   106
      fun readS (SOME s) = Syntax.read_sort_global thy''' s
huffman@31288
   107
        | readS NONE = Sign.defaultS thy''';
huffman@31288
   108
      fun readTFree (a, s) = TFree (a, readS s);
huffman@31161
   109
huffman@31288
   110
      val dtnvs = map (fn (vs,dname:binding,mx,_) => 
huffman@31288
   111
                          (dname, map readTFree vs, mx)) eqs''';
huffman@31288
   112
      val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
huffman@31288
   113
      fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
huffman@31288
   114
      fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
huffman@31288
   115
      val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
huffman@31288
   116
                         |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
huffman@31288
   117
      val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
huffman@31288
   118
      val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
huffman@31288
   119
      val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list =
huffman@31288
   120
          check_and_sort_domain dtnvs' cons'' thy'';
huffman@31288
   121
      val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
huffman@31288
   122
      val dts  = map (Type o fst) eqs';
huffman@31288
   123
      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
haftmann@31986
   124
      fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
huffman@31288
   125
      fun typid (Type  (id,_)) =
wenzelm@30364
   126
          let val c = hd (Symbol.explode (Long_Name.base_name id))
wenzelm@23152
   127
          in if Symbol.is_letter c then c else "t" end
huffman@31288
   128
        | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
huffman@31288
   129
        | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
huffman@31288
   130
      fun one_con (con,args,mx) =
huffman@31288
   131
          ((Syntax.const_name mx (Binding.name_of con)),
huffman@31288
   132
           ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
huffman@31288
   133
                                                           DatatypeAux.dtyp_of_typ new_dts tp),
huffman@31288
   134
                                                          Option.map Binding.name_of sel,vn))
huffman@31288
   135
                        (args,(mk_var_names(map (typid o third) args)))
huffman@31288
   136
          ) : cons;
huffman@31288
   137
      val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
huffman@31288
   138
      val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs;
huffman@31288
   139
      val ((rewss, take_rews), theorems_thy) =
huffman@31288
   140
          thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs
huffman@31288
   141
              ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
huffman@31288
   142
    in
huffman@31288
   143
      theorems_thy
huffman@31288
   144
        |> Sign.add_path (Long_Name.base_name comp_dnam)
huffman@31288
   145
        |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
huffman@31288
   146
        |> Sign.parent_path
huffman@31288
   147
    end;
wenzelm@23152
   148
huffman@30919
   149
val add_domain = gen_add_domain Sign.certify_typ;
huffman@30919
   150
val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
wenzelm@23152
   151
wenzelm@23152
   152
wenzelm@23152
   153
(** outer syntax **)
wenzelm@23152
   154
wenzelm@23152
   155
local structure P = OuterParse and K = OuterKeyword in
wenzelm@23152
   156
wenzelm@27353
   157
val _ = OuterKeyword.keyword "lazy";
wenzelm@24867
   158
huffman@30919
   159
val dest_decl : (bool * binding option * string) parser =
huffman@31288
   160
    P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
huffman@31288
   161
      (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ)  --| P.$$$ ")" >> P.triple1
huffman@31288
   162
      || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
huffman@31288
   163
      >> (fn t => (true,NONE,t))
huffman@31288
   164
      || P.typ >> (fn t => (false,NONE,t));
wenzelm@23152
   165
wenzelm@23152
   166
val cons_decl =
huffman@31288
   167
    P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
huffman@30916
   168
huffman@31161
   169
val type_var' : (string * string option) parser =
huffman@31288
   170
    (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
huffman@30916
   171
huffman@31161
   172
val type_args' : (string * string option) list parser =
huffman@31288
   173
    type_var' >> single ||
huffman@31288
   174
              P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") ||
huffman@31288
   175
              Scan.succeed [];
huffman@30916
   176
huffman@30916
   177
val domain_decl =
huffman@31288
   178
    (type_args' -- P.binding -- P.opt_infix) --
huffman@31288
   179
                                             (P.$$$ "=" |-- P.enum1 "|" cons_decl);
wenzelm@23152
   180
huffman@30916
   181
val domains_decl =
huffman@31288
   182
    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
huffman@31288
   183
                P.and_list1 domain_decl;
wenzelm@23152
   184
huffman@31161
   185
fun mk_domain (opt_name : string option,
huffman@31288
   186
               doms : ((((string * string option) list * binding) * mixfix) *
huffman@31288
   187
                       ((binding * (bool * binding option * string) list) * mixfix) list) list ) =
huffman@31288
   188
    let
huffman@31288
   189
      val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
huffman@31288
   190
      val specs : ((string * string option) list * binding * mixfix *
huffman@31288
   191
                   (binding * (bool * binding option * string) list * mixfix) list) list =
huffman@31288
   192
          map (fn (((vs, t), mx), cons) =>
huffman@31288
   193
                  (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
huffman@31288
   194
      val comp_dnam =
huffman@31288
   195
          case opt_name of NONE => space_implode "_" names | SOME s => s;
huffman@31288
   196
    in add_domain_cmd comp_dnam specs end;
wenzelm@23152
   197
wenzelm@24867
   198
val _ =
huffman@31288
   199
    OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl
huffman@31288
   200
                        (domains_decl >> (Toplevel.theory o mk_domain));
wenzelm@23152
   201
wenzelm@24867
   202
end;
wenzelm@23152
   203
wenzelm@23152
   204
end;