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