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