combine check_and_sort_domain with main function; rewrite much of the error-checking code
(* Title: HOLCF/Tools/Domain/domain.ML
Author: David von Oheimb
Author: Brian Huffman
Theory extender for domain command, including theory syntax.
*)
signature DOMAIN =
sig
val add_domain_cmd:
binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
val add_domain:
binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
val add_new_domain_cmd:
binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list
-> theory -> theory
val add_new_domain:
binding ->
((string * string option) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
end;
structure Domain :> DOMAIN =
struct
open HOLCF_Library;
fun first (x,_,_) = x;
fun second (_,x,_) = x;
fun third (_,_,x) = x;
(* ----- calls for building new thy and thms -------------------------------- *)
type info =
Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info;
fun gen_add_domain
(prep_typ : theory -> (string * sort) list -> 'a -> typ)
(add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
(arg_sort : bool -> sort)
(comp_dbind : binding)
(raw_specs : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * 'a) list * mixfix) list) list)
(thy : theory) =
let
val dtnvs : (binding * typ list * mixfix) list =
let
fun readS (SOME s) = Syntax.read_sort_global thy s
| readS NONE = Sign.defaultS thy;
fun readTFree (a, s) = TFree (a, readS s);
in
map (fn (vs, dbind, mx, _) =>
(dbind, map readTFree vs, mx)) raw_specs
end;
fun thy_type (dbind, tvars, mx) = (dbind, length tvars, mx);
fun thy_arity (dbind, tvars, mx) =
(Sign.full_name thy dbind, map (snd o dest_TFree) tvars, arg_sort false);
(* this theory is used just for parsing and error checking *)
val tmp_thy = thy
|> Theory.copy
|> Sign.add_types (map thy_type dtnvs)
|> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
val dbinds : binding list =
map (fn (_,dbind,_,_) => dbind) raw_specs;
val raw_rhss :
(binding * (bool * binding option * 'a) list * mixfix) list list =
map (fn (_,_,_,cons) => cons) raw_specs;
val dtnvs' : (string * typ list) list =
map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs;
val all_cons = map (Binding.name_of o first) (flat raw_rhss);
val test_dupl_cons =
case duplicates (op =) all_cons of
[] => false | dups => error ("Duplicate constructors: "
^ commas_quote dups);
val all_sels =
(map Binding.name_of o map_filter second o maps second) (flat raw_rhss);
val test_dupl_sels =
case duplicates (op =) all_sels of
[] => false | dups => error("Duplicate selectors: "^commas_quote dups);
fun test_dupl_tvars s =
case duplicates (op =) (map(fst o dest_TFree)s) of
[] => false | dups => error("Duplicate type arguments: "
^commas_quote dups);
val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs');
val sorts : (string * sort) list =
let val all_sorts = map (map dest_TFree o snd) dtnvs';
in
case distinct (eq_set (op =)) all_sorts of
[sorts] => sorts
| _ => error "Mutually recursive domains must have same type parameters"
end;
(* a lazy argument may have an unpointed type *)
(* unless the argument has a selector function *)
fun check_pcpo (lazy, sel, T) =
let val sort = arg_sort (lazy andalso is_none sel) in
if Sign.of_sort tmp_thy (T, sort) then ()
else error ("Constructor argument type is not of sort " ^
Syntax.string_of_sort_global tmp_thy sort ^ ": " ^
Syntax.string_of_typ_global tmp_thy T)
end;
(* test for free type variables, illegal sort constraints on rhs,
non-pcpo-types and invalid use of recursive type;
replace sorts in type variables on rhs *)
val map_tab = Domain_Take_Proofs.get_map_tab thy;
fun check_rec rec_ok (T as TFree (v,_)) =
if AList.defined (op =) sorts v then T
else error ("Free type variable " ^ quote v ^ " on rhs.")
| check_rec rec_ok (T as Type (s, Ts)) =
(case AList.lookup (op =) dtnvs' s of
NONE =>
let val rec_ok' = rec_ok andalso Symtab.defined map_tab s;
in Type (s, map (check_rec rec_ok') Ts) end
| SOME typevars =>
if typevars <> Ts
then error ("Recursion of type " ^
quote (Syntax.string_of_typ_global tmp_thy T) ^
" with different arguments")
else if rec_ok then T
else error ("Illegal indirect recursion of type " ^
quote (Syntax.string_of_typ_global tmp_thy T)))
| check_rec rec_ok (TVar _) = error "extender:check_rec";
fun prep_arg (lazy, sel, raw_T) =
let
val T = prep_typ tmp_thy sorts raw_T;
val _ = check_rec true T;
val _ = check_pcpo (lazy, sel, T);
in (lazy, sel, T) end;
fun prep_con (b, args, mx) = (b, map prep_arg args, mx);
fun prep_rhs cons = map prep_con cons;
val rhss : (binding * (bool * binding option * typ) list * mixfix) list list =
map prep_rhs raw_rhss;
fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T;
fun mk_con_typ (bind, args, mx) =
if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons);
val absTs : typ list = map Type dtnvs';
val repTs : typ list = map mk_rhs_typ rhss;
val iso_spec : (binding * mixfix * (typ * typ)) list =
map (fn ((dbind, _, mx), eq) => (dbind, mx, eq))
(dtnvs ~~ (absTs ~~ repTs));
val ((iso_infos, take_info), thy) = add_isos iso_spec thy;
val (constr_infos, thy) =
thy
|> fold_map (fn ((dbind, cons), info) =>
Domain_Constructors.add_domain_constructors dbind cons info)
(dbinds ~~ rhss ~~ iso_infos);
val (take_rews, thy) =
Domain_Induction.comp_theorems comp_dbind
dbinds take_info constr_infos thy;
in
thy
end;
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
let
fun prep (dbind, mx, (lhsT, rhsT)) =
let val (dname, vs) = dest_Type lhsT;
in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end;
in
Domain_Isomorphism.domain_isomorphism (map prep spec)
end;
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
fun rep_arg lazy = @{sort bifinite};
(* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *)
fun read_typ thy sorts str =
let
val ctxt = ProofContext.init_global thy
|> fold (Variable.declare_typ o TFree) sorts;
in Syntax.read_typ ctxt str end;
fun cert_typ sign sorts raw_T =
let
val T = Type.no_tvars (Sign.certify_typ sign raw_T)
handle TYPE (msg, _, _) => error msg;
val sorts' = Term.add_tfreesT T sorts;
val _ =
case duplicates (op =) (map fst sorts') of
[] => ()
| dups => error ("Inconsistent sort constraints for " ^ commas dups)
in T end;
val add_domain =
gen_add_domain cert_typ Domain_Axioms.add_axioms pcpo_arg;
val add_new_domain =
gen_add_domain cert_typ define_isos rep_arg;
val add_domain_cmd =
gen_add_domain read_typ Domain_Axioms.add_axioms pcpo_arg;
val add_new_domain_cmd =
gen_add_domain read_typ define_isos rep_arg;
(** outer syntax **)
val _ = Keyword.keyword "lazy";
val dest_decl : (bool * binding option * string) parser =
Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
(Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1
|| Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
>> (fn t => (true,NONE,t))
|| Parse.typ >> (fn t => (false,NONE,t));
val cons_decl =
Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix;
val domain_decl =
(Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
(Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
val domains_decl =
Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
Parse.and_list1 domain_decl;
fun mk_domain
(definitional : bool)
(opt_name : binding option,
doms : ((((string * string option) list * binding) * mixfix) *
((binding * (bool * binding option * string) list) * mixfix) list) list ) =
let
val names = map (fn (((_, t), _), _) => Binding.name_of t) doms;
val specs : ((string * string option) list * binding * mixfix *
(binding * (bool * binding option * string) list * mixfix) list) list =
map (fn (((vs, t), mx), cons) =>
(vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms;
val comp_dbind =
case opt_name of NONE => Binding.name (space_implode "_" names)
| SOME s => s;
in
if definitional
then add_new_domain_cmd comp_dbind specs
else add_domain_cmd comp_dbind specs
end;
val _ =
Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
val _ =
Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
end;