src/HOLCF/Tools/domain/domain_extender.ML
changeset 31163 19c2f68ae23d
parent 31161 a27d4254ff4c
child 31228 bcacfd816d28
equal deleted inserted replaced
31162:6dc708ca4a8f 31163:19c2f68ae23d
    22 open Domain_Library;
    22 open Domain_Library;
    23 
    23 
    24 (* ----- general testing and preprocessing of constructor list -------------- *)
    24 (* ----- general testing and preprocessing of constructor list -------------- *)
    25 fun check_and_sort_domain
    25 fun check_and_sort_domain
    26   (dtnvs : (string * typ list) list)
    26   (dtnvs : (string * typ list) list)
    27   (cons'' : ((binding * (bool * binding option * typ) list * mixfix) list) list)
    27   (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
    28   (sg : theory)
    28   (sg : theory)
    29   : ((string * typ list) *
    29   : ((string * typ list) *
    30       (binding * (bool * binding option * typ) list * mixfix) list) list =
    30       (binding * (bool * binding option * typ) list * mixfix) list) list =
    31   let
    31   let
    32     val defaultS = Sign.defaultS sg;
    32     val defaultS = Sign.defaultS sg;
    73 				then Type(s,map (analyse true) typl)
    73 				then Type(s,map (analyse true) typl)
    74 				else error ("Direct recursion of type " ^ 
    74 				else error ("Direct recursion of type " ^ 
    75 					     quote (string_of_typ sg t) ^ 
    75 					     quote (string_of_typ sg t) ^ 
    76 					    " with different arguments"))
    76 					    " with different arguments"))
    77         |   analyse indirect (TVar _) = Imposs "extender:analyse";
    77         |   analyse indirect (TVar _) = Imposs "extender:analyse";
    78 	fun check_pcpo T = if pcpo_type sg T then T
    78         fun check_pcpo lazy T =
    79           else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
    79           let val ok = if lazy then cpo_type else pcpo_type
    80 	val analyse_con = upd_second (map (upd_third (check_pcpo o analyse false)));
    80           in if ok sg T then T else error
       
    81             ("Constructor argument type is not of sort pcpo: " ^
       
    82               string_of_typ sg T)
       
    83           end;
       
    84         fun analyse_arg (lazy, sel, T) =
       
    85           (lazy, sel, check_pcpo lazy (analyse false T));
       
    86         fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx);
    81       in ((dname,distinct_typevars), map analyse_con cons') end; 
    87       in ((dname,distinct_typevars), map analyse_con cons') end; 
    82   in ListPair.map analyse_equation (dtnvs,cons'')
    88   in ListPair.map analyse_equation (dtnvs,cons'')
    83   end; (* let *)
    89   end; (* let *)
    84 
    90 
    85 (* ----- calls for building new thy and thms -------------------------------- *)
    91 (* ----- calls for building new thy and thms -------------------------------- *)