# HG changeset patch # User huffman # Date 1289320896 28800 # Node ID 05be0c37db1d72b8baf667f484cd945c06710caf # Parent 0f37a553bc1a2ace9c6bc130fd9b8ee00af36fa2 add bifiniteness check for domain_isomorphism command diff -r 0f37a553bc1a -r 05be0c37db1d src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Nov 09 05:23:34 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Nov 09 08:41:36 2010 -0800 @@ -407,7 +407,7 @@ (* lookup function for sorts of type variables *) fun the_sort v = the (AList.lookup (op =) sorts v); - (* temporary arities for rewriting *) + (* declare arities in temporary theory *) val tmp_thy = let fun arity (vs, tbind, mx, _, _) = @@ -416,6 +416,13 @@ fold AxClass.axiomatize_arity (map arity doms) tmp_thy end; + (* check bifiniteness of right-hand sides *) + fun check_rhs (vs, tbind, mx, rhs, morphs) = + if Sign.of_sort tmp_thy (rhs, @{sort bifinite}) then () + else error ("Type not of sort bifinite: " ^ + quote (Syntax.string_of_typ_global tmp_thy rhs)); + val _ = map check_rhs doms; + (* domain equations *) fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) = let fun arg v = TFree (v, the_sort v);