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