## highcode-type.pkg
#
# See overview comments in:
#
# src/lib/compiler/back/top/highcode/highcode-type.api# Compiled by:
# src/lib/compiler/core.sublib### "One should expect that the expected
### can be prevented, but the unexpected
### should have been expected."
###
### -- Norman Augustine
stipulate
package di = debruijn_index; # debruijn_index is from src/lib/compiler/front/typer/basics/debruijn-index.pkg package err = error_message; # error_message is from src/lib/compiler/front/basics/errormsg/error-message.pkg package hbt = highcode_basetypes; # highcode_basetypes is from src/lib/compiler/back/top/highcode/highcode-basetypes.pkg package tmp = highcode_codetemp; # highcode_codetemp is from src/lib/compiler/back/top/highcode/highcode-codetemp.pkg package hut = highcode_uniq_types; # highcode_uniq_types is from src/lib/compiler/back/top/highcode/highcode-uniq-types.pkg fun bug msg
=
err::impossible("highcode_type: " + msg);
say = global_controls::print::say;
herein
# We get 'included' by:
#
# src/lib/compiler/back/top/highcode/highcode-form.pkg package highcode_type
: (weak) Highcode_Type # Highcode_Type is from src/lib/compiler/back/top/highcode/highcode-type.api {
# highcode hut::Uniqkind is roughly equivalent to:
#
# hut::Kind
# = TYPE
# | BOXED_TYPE
# | TYPESEQ List( hut::Kind )
# | TYPEFUN (List( hut::Kind ), hut::Kind)
# ;
#
# We treat Uniqkind as an abstract type
# to isolate clients from the complexity of the
# hashconsing machinery; this has the downside
# of preventing them from using pattern matching.
# Some hut::Uniqkind constructors:
#
my plaintype_uniqkind: hut::Uniqkind = hut::kind_to_uniqkind hut::kind::PLAINTYPE;
my boxedtype_uniqkind: hut::Uniqkind = hut::kind_to_uniqkind hut::kind::BOXEDTYPE;
#
my make_kindseq_uniqkind: List(hut::Uniqkind) -> hut::Uniqkind = hut::kind_to_uniqkind o hut::kind::KINDSEQ;
my make_kindfun_uniqkind: (List(hut::Uniqkind), hut::Uniqkind) -> hut::Uniqkind = hut::kind_to_uniqkind o hut::kind::KINDFUN;
# Matching hut::Uniqkind deconstructors:
#
my unpack_plaintype_uniqkind: hut::Uniqkind -> Void = fn _ = ();
my unpack_boxedtype_uniqkind: hut::Uniqkind -> Void = fn _ = ();
#
my unpack_kindseq_uniqkind: hut::Uniqkind -> List( hut::Uniqkind )
=
fn tk
=>
case (hut::uniqkind_to_kind tk)
#
hut::kind::KINDSEQ x => x;
_ => bug "unexpected hut::Kind in unpack_kindseq_uniqkind";
esac;
end;
my unpack_kindfun_uniqkind: hut::Uniqkind -> (List( hut::Uniqkind ), hut::Uniqkind)
=
fn tk
=
case (hut::uniqkind_to_kind tk)
#
hut::kind::KINDFUN x => x;
_ => bug "unexpected hut::Kind in unpack_kindfun_uniqkind";
esac;
# Some hut::Uniqkind predicates:
#
my uniqkind_is_plaintype: hut::Uniqkind -> Bool = fn tk = hut::same_uniqkind (tk, plaintype_uniqkind);
my uniqkind_is_boxedtype: hut::Uniqkind -> Bool = fn tk = hut::same_uniqkind (tk, boxedtype_uniqkind);
#
my uniqkind_is_kindseq: hut::Uniqkind -> Bool = fn tk = case (hut::uniqkind_to_kind tk) hut::kind::KINDSEQ _ => TRUE; _ => FALSE; esac;
my uniqkind_is_kindfun: hut::Uniqkind -> Bool = fn tk = case (hut::uniqkind_to_kind tk) hut::kind::KINDFUN _ => TRUE; _ => FALSE; esac;
# Some hut::Uniqkind one-arm switches:
#
fun if_uniqkind_is_plaintype (tk, f, g) = if (hut::same_uniqkind (tk, plaintype_uniqkind)) f (); else g tk; fi;
fun if_uniqkind_is_boxedtype (tk, f, g) = if (hut::same_uniqkind (tk, boxedtype_uniqkind )) f (); else g tk; fi;
#
fun if_uniqkind_is_kindseq (tk, f, g) = case (hut::uniqkind_to_kind tk) hut::kind::KINDSEQ x => f x; _ => g tk; esac;
fun if_uniqkind_is_kindfun (tk, f, g) = case (hut::uniqkind_to_kind tk) hut::kind::KINDFUN x => f x; _ => g tk; esac;
# Highcode Calling_Convention and Useless_Recordflag are used to classify different kinds of typelocked
# functions and records. As of now, they are roughly equivalent to:
#
# Calling_Convention
# = FIXED_CALLING_CONVENTION
# | VARIABLE_CALLING_CONVENTION { arg_is_raw: Bool,
# body_is_raw: Bool
# }
#
# Useless_Recordflag = USELESS_RECORDFLAG
#
# We treat both as abstract types so pattern matching no longer applies.
# NOTE: VARIABLE_CALLING_CONVENTION flags are used by HIGHCODEs before we perform representation
# analysis while FIXED_CALLING_CONVENTION is used by HIGHCODEs after we perform representation
# analysis.
# Calling_Convention and record_flag constructors:
#
my fixed_calling_convention: hut::Calling_Convention = hut::FIXED_CALLING_CONVENTION;
my useless_recordflag: hut::Useless_Recordflag = hut::USELESS_RECORDFLAG;
#
my make_variable_calling_convention: { arg_is_raw: Bool, body_is_raw: Bool } -> hut::Calling_Convention
=
fn arg_is_raw__body_is_raw
=
hut::VARIABLE_CALLING_CONVENTION arg_is_raw__body_is_raw;
# Calling_Convention and Useless_Recordflag deconstructors:
#
my unpack_variable_calling_convention: hut::Calling_Convention -> { arg_is_raw: Bool, body_is_raw: Bool } # This function is never used.
=
fn x = case x
#
hut::VARIABLE_CALLING_CONVENTION arg_is_raw__body_is_raw
=> arg_is_raw__body_is_raw;
_ => bug "unexpected Calling_Convention in unpack_variable_calling_convention";
esac;
my unpack_fixed_calling_convention: hut::Calling_Convention -> Void
=
fn x = case x hut::FIXED_CALLING_CONVENTION => ();
_ => bug "unexpected Calling_Convention in unpack_fixed_calling_convention";
esac;
my unpack_useless_recordflag: hut::Useless_Recordflag -> Void
=
fn (hut::USELESS_RECORDFLAG) = ();
# Calling_Convention and Useless_Recordflag predicates:
#
my calling_convention_is_variable: hut::Calling_Convention -> Bool
=
fn x = case x hut::VARIABLE_CALLING_CONVENTION _ => TRUE;
_ => FALSE;
esac;
my calling_convention_is_fixed: hut::Calling_Convention -> Bool
=
fn x = case x hut::FIXED_CALLING_CONVENTION => TRUE;
_ => FALSE;
esac;
my useless_recordflag_is: hut::Useless_Recordflag -> Bool
=
fn (hut::USELESS_RECORDFLAG) = TRUE;
# Calling_Convention and Useless_Recordflag one-arm switches:
#
fun if_calling_convention_is_variable (calling_convention, then_fn, else_fn)
=
case calling_convention
#
hut::VARIABLE_CALLING_CONVENTION arg_is_raw__body_is_raw => then_fn arg_is_raw__body_is_raw;
_ => else_fn calling_convention;
esac;
fun if_calling_convention_is_fixed (calling_convention, then_fn, else_fn)
=
case calling_convention
#
hut::FIXED_CALLING_CONVENTION => then_fn ();
_ => else_fn calling_convention;
esac;
fun if_useless_recordflag_is (rf, then_fn, else_fn) # Useless fn on a useless value. :-)
=
then_fn ();
# highcode hut::Uniqtyp is roughly equivalent
# to the following Mythryl datatype:
#
# Uniqtyp
# = TYPEVAR (Debruijn_Index, Int)
# | NAMED_TYPEVAR tmp::Codetemp
# | BASETYPE hut::Basetype
# | TYPEFUN (List( hut::Uniqkind ), hut::Uniqtyp)
# | APPLY_TYPEFUN (hut::Uniqtyp, List( hut::Uniqtyp ))
# | TYPESEQ List( hut::Uniqtyp )
# | TYPE_PROJECTION (hut::Uniqtyp, Int)
# | SUM_TYPE List( hut::Uniqtyp )
# | RECURSIVE_TYPE (hut::Uniqtyp, Int)
# | TUPLE_TYPE List( hut::Uniqtyp ) # record_flag hidden
# | ARROW_TYPE (hut::Calling_Convention, List(hut::Uniqtyp), List(hut::Uniqtyp))
# | BOXED_TYPE hut::Uniqtyp
# | ABSTRACT_TYPE hut::Uniqtyp
# | EXTENSIBLE_TOKEN_TYPE (Token, hut::Uniqtyp)
# | FATE_TYPE List(hut::Uniqtyp)
# | INDIRECT_TYPE_THUNK (hut::Uniqtyp, hut::Uniqtype)
# | TYPE_CLOSURE (Uniqtyp, Int, Int, Uniqtyp_Dictionary)
# ;
#
# We treat Uniqtyp as an abstract type
# to isolate clients from the complexity of the
# hashconsing machinery; this has the downside
# of preventing them from using pattern matching.
#
# hut::Uniqtyp applications (TC_APPLY) and projections
# (TC_PROJ) are automatically reduced as needed, that is, the
# client does not need to worry about whether a hut::Uniqtyp is in the
# normal form or not, all functions defined here automatically
# take care of this.
# Some hut::Uniqtyp constructors
#
my make_debruijn_typevar_uniqtyp: (di::Debruijn_Index, Int) -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::DEBRUIJN_TYPEVAR;
my make_named_typevar_uniqtyp: tmp::Codetemp -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::NAMED_TYPEVAR;
my make_basetype_uniqtyp: hbt::Basetype -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::BASETYPE;
#
my make_typefun_uniqtyp: ( List(hut::Uniqkind),
hut::Uniqtyp
) -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::TYPEFUN;
my make_apply_typefun_uniqtyp: ( hut::Uniqtyp,
List(hut::Uniqtyp)
) -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::APPLY_TYPEFUN;
my make_typeseq_uniqtyp: List(hut::Uniqtyp) -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::TYPESEQ;
my make_ith_in_typeseq_uniqtyp: (hut::Uniqtyp, Int) -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::ITH_IN_TYPESEQ;
#
my make_sum_uniqtyp: List(hut::Uniqtyp) -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::SUM;
my make_abstract_uniqtyp: hut::Uniqtyp -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::ABSTRACT;
my make_boxed_uniqtyp: hut::Uniqtyp -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::BOXED;
#
my make_tuple_uniqtyp: List(hut::Uniqtyp) -> hut::Uniqtyp = fn ts = hut::typ_to_uniqtyp (hut::typ::TUPLE (useless_recordflag, ts));
my make_extensible_token_uniqtyp: hut::Uniqtyp -> hut::Uniqtyp = fn tc = hut::typ_to_uniqtyp (hut::typ::EXTENSIBLE_TOKEN (hut::wrap_token, tc));
#
my make_arrow_uniqtyp: (hut::Calling_Convention, List(hut::Uniqtyp), List(hut::Uniqtyp)) -> hut::Uniqtyp = hut::make_arrow_uniqtyp;
my make_recursive_uniqtyp: ((Int, hut::Uniqtyp, List(hut::Uniqtyp)), Int) -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::RECURSIVE;
# hut::Uniqtyp deconstructors -- these are
# basically inverse to the above functions:
#
my unpack_debruijn_typevar_uniqtyp: hut::Uniqtyp -> (di::Debruijn_Index, Int)
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::DEBRUIJN_TYPEVAR x => x;
_ => bug "unexpected typ in unpack_debruijn_typevar_uniqtyp";
esac;
my unpack_named_typevar_uniqtyp: hut::Uniqtyp -> tmp::Codetemp
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::NAMED_TYPEVAR x => x;
_ => bug "unexpected typ in unpack_named_typevar_uniqtyp";
esac;
my unpack_basetype_uniqtyp: hut::Uniqtyp -> hbt::Basetype
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::BASETYPE x => x;
_ => bug "unexpected typ in unpack_basetype_uniqtyp";
esac;
my unpack_typefun_uniqtyp: hut::Uniqtyp -> (List( hut::Uniqkind ), hut::Uniqtyp)
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::TYPEFUN x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_typefun_uniqtyp";
esac;
my unpack_apply_typefun_uniqtyp: hut::Uniqtyp -> (hut::Uniqtyp, List( hut::Uniqtyp ))
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::APPLY_TYPEFUN x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_apply_typefun_uniqtyp";
esac;
my unpack_typeseq_uniqtyp: hut::Uniqtyp -> List( hut::Uniqtyp )
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::TYPESEQ x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_typeseq_uniqtyp";
esac;
my unpack_ith_in_typeseq_uniqtyp: hut::Uniqtyp -> (hut::Uniqtyp, Int)
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::ITH_IN_TYPESEQ x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_ith_in_typeseq_uniqtyp";
esac;
my unpack_sum_uniqtyp: hut::Uniqtyp -> List( hut::Uniqtyp )
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::SUM x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_sum_uniqtyp";
esac;
my unpack_recursive_uniqtyp: hut::Uniqtyp -> (((Int, hut::Uniqtyp, List( hut::Uniqtyp)) ), Int)
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::RECURSIVE x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_recursive_uniqtyp";
esac;
my unpack_extensible_token_uniqtyp: hut::Uniqtyp -> hut::Uniqtyp
=
fn tc = case (hut::uniqtyp_to_typ tc)
hut::typ::EXTENSIBLE_TOKEN (tk, x)
=>
if (hut::same_token (tk, hut::wrap_token)) x;
else bug "unexpected token hut::Uniqtyp in unpack_extensible_token_uniqtyp";
fi;
_ => bug "unexpected regular hut::Uniqtyp in unpack_extensible_token_uniqtyp";
esac;
my unpack_abstract_uniqtyp: hut::Uniqtyp -> hut::Uniqtyp
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::ABSTRACT x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_abstract_uniqtyp";
esac;
my unpack_boxed_uniqtyp: hut::Uniqtyp -> hut::Uniqtyp
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::BOXED x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_boxed_uniqtyp";
esac;
my unpack_tuple_uniqtyp: hut::Uniqtyp -> List( hut::Uniqtyp )
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::TUPLE (_, x) => x;
_ => bug "unexpected hut::Uniqtyp in unpack_tuple_uniqtyp";
esac;
my unpack_arrow_uniqtyp: hut::Uniqtyp -> (hut::Calling_Convention, List( hut::Uniqtyp ), List( hut::Uniqtyp ))
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::ARROW x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_arrow_uniqtyp";
esac;
# Some hut::Uniqtyp predicates:
#
my uniqtyp_is_debruijn_typevar: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::DEBRUIJN_TYPEVAR _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_named_typevar: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::NAMED_TYPEVAR _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_basetype: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::BASETYPE _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_typefun: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::TYPEFUN _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_apply_typefun: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::APPLY_TYPEFUN _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_typeseq: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::TYPESEQ _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_ith_in_typeseq: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::ITH_IN_TYPESEQ _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_sum: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::SUM _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_recursive: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::RECURSIVE _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_extensible_token: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::EXTENSIBLE_TOKEN (tk, _) => hut::same_token (tk, hut::wrap_token);
_ => FALSE;
esac;
my uniqtyp_is_abstract: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::ABSTRACT _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_boxed: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::BOXED _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_tuple: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::TUPLE _ => TRUE;
_ => FALSE;
esac;
my uniqtyp_is_arrow: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::ARROW _ => TRUE;
_ => FALSE;
esac;
# Some hut::Uniqtyp one-arm switches:
#
fun if_uniqtyp_is_debruijn_typevar (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::DEBRUIJN_TYPEVAR x => f x; _ => g tc; esac;
fun if_uniqtyp_is_named_typevar (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::NAMED_TYPEVAR x => f x; _ => g tc; esac;
fun if_uniqtyp_is_basetype (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::BASETYPE x => f x; _ => g tc; esac;
fun if_uniqtyp_is_typefun (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::TYPEFUN x => f x; _ => g tc; esac;
fun if_uniqtyp_is_apply_typefun (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::APPLY_TYPEFUN x => f x; _ => g tc; esac;
fun if_uniqtyp_is_typeseq (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::TYPESEQ x => f x; _ => g tc; esac;
fun if_uniqtyp_is_ith_in_typeseq (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::ITH_IN_TYPESEQ x => f x; _ => g tc; esac;
fun if_uniqtyp_is_sum (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::SUM x => f x; _ => g tc; esac;
fun if_uniqtyp_is_recursive (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::RECURSIVE x => f x; _ => g tc; esac;
fun if_uniqtyp_is_abstract (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::ABSTRACT x => f x; _ => g tc; esac;
fun if_uniqtyp_is_boxed (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::BOXED x => f x; _ => g tc; esac;
fun if_uniqtyp_is_tuple (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::TUPLE (_, x) => f x; _ => g tc; esac;
fun if_uniqtyp_is_arrow (tc, f, g) = case (hut::uniqtyp_to_typ tc) hut::typ::ARROW x => f x; _ => g tc; esac;
fun if_uniqtyp_is_extensible_token (tc, f, g)
=
case (hut::uniqtyp_to_typ tc)
#
hut::typ::EXTENSIBLE_TOKEN (rk, x)
=>
if (hut::same_token (rk, hut::wrap_token)) f x;
else g tc;
fi;
_ => g tc;
esac;
# highcode hut::Uniqtype is roughly equivalent to:
#
# Type
# = TYP hut::Uniqtyp
# | PACKAGE List(hut::Uniqtype)
# | GENERIC_PACKAGE (List(hut::Uniqtype), List(hut::Uniqtype))
# | TYPEAGNOSTIC (List(hut::Uniqkind), List(hut::Uniqtype))
#
# We treat Uniqtype as an abstract type
# to isolate clients from the complexity of the
# hashconsing machinery; this has the downside
# of preventing them from using pattern matching.
#
# Clients do not need to worry about whether an
# hut::Uniqtype is in normal form or not.
# hut::Uniqtype constructors
#
my make_typ_uniqtype: hut::Uniqtyp -> hut::Uniqtype = hut::type_to_uniqtype o hut::type::TYP;
my make_package_uniqtype: List(hut::Uniqtype) -> hut::Uniqtype = hut::type_to_uniqtype o hut::type::PACKAGE;
my make_generic_package_uniqtype: (List(hut::Uniqtype), List(hut::Uniqtype)) -> hut::Uniqtype = hut::type_to_uniqtype o hut::type::GENERIC_PACKAGE;
my make_typeagnostic_uniqtype: (List(hut::Uniqkind), List(hut::Uniqtype)) -> hut::Uniqtype = hut::type_to_uniqtype o hut::type::TYPEAGNOSTIC;
# hut::Uniqtype deconstructors
#
my unpack_typ_uniqtype: hut::Uniqtype -> hut::Uniqtyp
=
fn lt = case (hut::uniqtype_to_type lt) hut::type::TYP x => x;
hut::type::PACKAGE _ => bug "hut::type::PACKAGE unsupported in unpack_typ_uniqtype";
hut::type::GENERIC_PACKAGE _ => bug "hut::type::GENERIC unsupported in unpack_typ_uniqtype";
hut::type::TYPEAGNOSTIC _ => bug "hut::type::TYPEAGNOSTIC unsupported in unpack_typ_uniqtype";
_ => bug "Unexpected hut::Uniqtype in unpack_typ_uniqtype";
esac;
my unpack_package_uniqtype: hut::Uniqtype -> List( hut::Uniqtype )
=
fn lt = case (hut::uniqtype_to_type lt)
#
hut::type::PACKAGE x => x;
_ => bug "unexpected hut::Uniqtype in unpack_package_uniqtype";
esac;
my unpack_generic_package_uniqtype: hut::Uniqtype -> (List( hut::Uniqtype ), List( hut::Uniqtype ))
=
fn lt = case (hut::uniqtype_to_type lt)
#
hut::type::GENERIC_PACKAGE x => x;
_ => bug "unexpected hut::Uniqtype in unpack_generic_package_uniqtype";
esac;
my unpack_typeagnostic_uniqtype: hut::Uniqtype -> (List( hut::Uniqkind ), List( hut::Uniqtype ))
=
fn lt = case (hut::uniqtype_to_type lt)
#
hut::type::TYPEAGNOSTIC x => x;
_ => bug "unexpected hut::Uniqtype in unpack_typeagnostic_uniqtype";
esac;
# hut::Uniqtype predicates
#
my uniqtype_is_typ: hut::Uniqtype -> Bool
=
fn lt = case (hut::uniqtype_to_type lt)
#
hut::type::TYP _ => TRUE;
_ => FALSE;
esac;
my uniqtype_is_package: hut::Uniqtype -> Bool
=
fn lt = case (hut::uniqtype_to_type lt)
#
hut::type::PACKAGE _ => TRUE;
_ => FALSE;
esac;
my uniqtype_is_generic_package: hut::Uniqtype -> Bool
=
fn lt = case (hut::uniqtype_to_type lt)
#
hut::type::GENERIC_PACKAGE _ => TRUE;
_ => FALSE;
esac;
my uniqtype_is_typeagnostic: hut::Uniqtype -> Bool
=
fn lt = case (hut::uniqtype_to_type lt)
#
hut::type::TYPEAGNOSTIC _ => TRUE;
_ => FALSE;
esac;
# hut::Uniqtype one-arm switches.
# These are if-then-else constructs which may be
# daisy-chained to implement a complete 'case' statement:
#
fun if_uniqtype_is_typ (lt, f, g) = case (hut::uniqtype_to_type lt) hut::type::TYP x => f x; _ => g lt; esac;
fun if_uniqtype_is_package (lt, f, g) = case (hut::uniqtype_to_type lt) hut::type::PACKAGE x => f x; _ => g lt; esac;
fun if_uniqtype_is_generic_package (lt, f, g) = case (hut::uniqtype_to_type lt) hut::type::GENERIC_PACKAGE x => f x; _ => g lt; esac;
fun if_uniqtype_is_typeagnostic (lt, f, g) = case (hut::uniqtype_to_type lt) hut::type::TYPEAGNOSTIC x => f x; _ => g lt; esac;
# Because highcode hut::Uniqtyp is embedded inside
# highcode hut::Uniqtype, we supply the the following
# utility functions for building types that are based
# on simple typelocked typs.
# hut::Uniqtyp-hut::Uniqtype constructors
#
my make_debruijn_typevar_uniqtype: (di::Debruijn_Index, Int) -> hut::Uniqtype = make_typ_uniqtype o make_debruijn_typevar_uniqtyp;
my make_basetype_uniqtype: hbt::Basetype -> hut::Uniqtype = make_typ_uniqtype o make_basetype_uniqtyp;
my make_tuple_uniqtype: List(hut::Uniqtype) -> hut::Uniqtype = make_typ_uniqtype o (make_tuple_uniqtyp o (map unpack_typ_uniqtype));
#
my make_arrow_uniqtype: (hut::Calling_Convention, List( hut::Uniqtype ), List( hut::Uniqtype )) -> hut::Uniqtype
=
fn (r, t1, t2)
=
{ ts1 = map unpack_typ_uniqtype t1;
ts2 = map unpack_typ_uniqtype t2;
#
make_typ_uniqtype (make_arrow_uniqtyp (r, ts1, ts2));
};
# Some hut::Uniqtyp-hut::Uniqtype deconstructors
#
my unpack_debruijn_typevar_uniqtype: hut::Uniqtype -> (di::Debruijn_Index, Int) = unpack_debruijn_typevar_uniqtyp o unpack_typ_uniqtype;
my unpack_basetype_uniqtype: hut::Uniqtype -> hbt::Basetype = unpack_basetype_uniqtyp o unpack_typ_uniqtype;
my unpack_tuple_uniqtype: hut::Uniqtype -> List( hut::Uniqtype ) = (map make_typ_uniqtype) o (unpack_tuple_uniqtyp o unpack_typ_uniqtype);
#
my unpack_arrow_uniqtype: hut::Uniqtype -> (hut::Calling_Convention, List(hut::Uniqtype), List(hut::Uniqtype))
=
fn t = { my (r, ts1, ts2) = unpack_arrow_uniqtyp (unpack_typ_uniqtype t);
(r, map make_typ_uniqtype ts1, map make_typ_uniqtype ts2);
};
# Some hut::Uniqtyp-hut::Uniqtype predicates
my uniqtype_is_debruijn_typevar: hut::Uniqtype -> Bool
=
fn t = case (hut::uniqtype_to_type t) hut::type::TYP x => uniqtyp_is_debruijn_typevar x;
_ => FALSE;
esac;
my uniqtype_is_basetype: hut::Uniqtype -> Bool
=
fn t = case (hut::uniqtype_to_type t) hut::type::TYP x => uniqtyp_is_basetype x;
_ => FALSE;
esac;
my uniqtype_is_tuple_type: hut::Uniqtype -> Bool
=
fn t = case (hut::uniqtype_to_type t) hut::type::TYP x => uniqtyp_is_tuple x;
_ => FALSE;
esac;
my uniqtype_is_arrow_type: hut::Uniqtype -> Bool
=
fn t = case (hut::uniqtype_to_type t) hut::type::TYP x => uniqtyp_is_arrow x;
_ => FALSE;
esac;
# Some hut::Uniqtyp-hut::Uniqtype one-arm switches:
#
fun if_uniqtype_is_debruijn_typevar (lt, f, g)
=
case (hut::uniqtype_to_type lt)
hut::type::TYP tc
=>
case (hut::uniqtyp_to_typ tc) hut::typ::DEBRUIJN_TYPEVAR x => f x;
_ => g lt;
esac;
_ => g lt;
esac;
fun if_uniqtype_is_basetype (lt, f, g)
=
case (hut::uniqtype_to_type lt)
hut::type::TYP tc
=>
case (hut::uniqtyp_to_typ tc) hut::typ::BASETYPE x => f x;
_ => g lt;
esac;
_ => g lt;
esac;
fun if_uniqtype_is_tuple_type (lt, f, g)
=
case (hut::uniqtype_to_type lt)
hut::type::TYP tc
=>
case (hut::uniqtyp_to_typ tc) hut::typ::TUPLE (_, x) => f x;
_ => g lt;
esac;
_ => g lt;
esac;
fun if_uniqtype_is_arrow_type (lt, f, g)
=
case (hut::uniqtype_to_type lt)
#
hut::type::TYP tc
=>
case (hut::uniqtyp_to_typ tc)
#
hut::typ::ARROW x => f x;
_ => g lt;
esac;
_ => g lt;
esac;
#########################################################################3
# The following functions are written for nextcode only.
# If you are writing writing code for highcode,
# you should not use any of these functions.
#
# The fate referred here is the internal
# fate introduced via nextcode conversion;
# it is different from the source-level fate
# (Fate(X)) or control fate (Control_Fate(X))
# where are represented hbt::primTypeCon_fate and
# hbt::primTypeCon_control_fate respectively.
# Our fate-hut::Uniqtyp-hut::Uniqtype constructors
#
my make_uniqtyp_fate: List( hut::Uniqtyp ) -> hut::Uniqtyp = hut::typ_to_uniqtyp o hut::typ::FATE;
my make_uniqtype_fate: List( hut::Uniqtype) -> hut::Uniqtype = hut::type_to_uniqtype o hut::type::FATE;
# Our fate-hut::Uniqtyp-hut::Uniqtype deconstructors.
# These are inverse to the above two:
#
my unpack_uniqtyp_fate: hut::Uniqtyp -> List( hut::Uniqtyp )
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::FATE x => x;
_ => bug "unexpected hut::Uniqtyp in unpack_uniqtyp_fate";
esac;
my unpack_uniqtype_fate: hut::Uniqtype -> List( hut::Uniqtype )
=
fn lt = case (hut::uniqtype_to_type lt) hut::type::FATE x => x;
_ => bug "unexpected hut::Uniqtype in unpack_uniqtype_fate";
esac;
# Our fate-hut::Uniqtyp-hut::Uniqtype predicates
#
my uniqtyp_is_fate: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::FATE _ => TRUE;
_ => FALSE;
esac;
my uniqtype_is_fate: hut::Uniqtype -> Bool
=
fn lt = case (hut::uniqtype_to_type lt) hut::type::FATE _ => TRUE;
_ => FALSE;
esac;
# Our fate-hut::Uniqtyp-hut::Uniqtype one-arm switches
fun if_uniqtyp_is_fate (tc, f, g)
=
case (hut::uniqtyp_to_typ tc) hut::typ::FATE x => f x;
_ => g tc;
esac;
fun if_uniqtype_is_fate (lt, f, g)
=
case (hut::uniqtype_to_type lt) hut::type::FATE x => f x;
_ => g lt;
esac;
################################################################################################
# The following functions are written for lambdacode_type only. If you
# are writing code for highcode only, don't use any of these functions.
# The idea is that in lambdacode, all (value or type) functions have single
# argument and single return-result. Ideally, we should define
# another sets of datatypes for typs and ltys. But we want to avoid
# the translation from lambdacode_type to highcode types, so we let them
# share the same representations as much as possible.
#
# Ultimately, highcode_type should be separated into two files: one for
# highcode, another for lambdacode, but we will see if this is necessary.
# The implementation here is TEMPORARY; Stefan needs to take a look at XXX BUGGO FIXME
# this. Note parrow could share the representation with arrow if there
# is one-to-one mapping between parrow and arrow.
# plambda hut::Uniqtyp-hut::Uniqtype constructors
#
my make_lambdacode_arrow_uniqtyp: (hut::Uniqtyp, hut::Uniqtyp) -> hut::Uniqtyp
=
fn (x, y) = make_arrow_uniqtyp (make_variable_calling_convention { arg_is_raw => FALSE, body_is_raw => FALSE }, [x], [y]);
my make_lambdacode_arrow_uniqtype: (hut::Uniqtype, hut::Uniqtype) -> hut::Uniqtype
=
fn (x, y) = make_typ_uniqtype (make_lambdacode_arrow_uniqtyp (unpack_typ_uniqtype x, unpack_typ_uniqtype y));
my make_lambdacode_typeagnostic_uniqtype: (List( hut::Uniqkind ), hut::Uniqtype) -> hut::Uniqtype
=
fn (ks, t) = make_typeagnostic_uniqtype (ks, [t]);
my make_lambdacode_generic_package_uniqtype: (hut::Uniqtype, hut::Uniqtype) -> hut::Uniqtype
=
fn (x, y) = make_generic_package_uniqtype ([x], [y]);
# Our* plambda hut::Uniqtyp-hut::Uniqtype deconstructors:
#
my unpack_lambdacode_arrow_uniqtyp: hut::Uniqtyp -> (hut::Uniqtyp, hut::Uniqtyp)
=
fn tc = case (hut::uniqtyp_to_typ tc)
#
hut::typ::ARROW (_, xs, ys) => (hut::uniqtyp_list_to_uniqtyp_tuple xs, hut::uniqtyp_list_to_uniqtyp_tuple ys);
_ => bug "unexpected hut::Uniqtyp in unpack_lambdacode_arrow_uniqtyp";
esac;
my unpack_lambdacode_arrow_uniqtype: hut::Uniqtype -> (hut::Uniqtype, hut::Uniqtype)
=
fn t = { my (t1, t2)
=
unpack_lambdacode_arrow_uniqtyp (unpack_typ_uniqtype t);
( make_typ_uniqtype t1,
make_typ_uniqtype t2
);
};
my unpack_lambdacode_typeagnostic_uniqtype: hut::Uniqtype -> (List( hut::Uniqkind ), hut::Uniqtype)
=
fn t = { my (ks, ts)
=
unpack_typeagnostic_uniqtype t;
case ts [x] => (ks, x);
_ => bug "unexpected case in unpack_lambdacode_typeagnostic_uniqtype";
esac;
};
my unpack_lambdacode_generic_package_uniqtype: hut::Uniqtype -> (hut::Uniqtype, hut::Uniqtype)
=
fn t = { my (ts1, ts2)
=
unpack_generic_package_uniqtype t;
case (ts1, ts2) ([x], [y]) => (x, y);
_ => bug "unexpected case in unpack_lambdacode_generic_package_uniqtype";
esac;
};
# Our plambda hut::Uniqtyp-hut::Uniqtype predicates
#
my uniqtyp_is_lambdacode_arrow: hut::Uniqtyp -> Bool
=
fn tc = case (hut::uniqtyp_to_typ tc) hut::typ::ARROW (_, [x], [y]) => TRUE;
_ => FALSE;
esac;
my uniqtype_is_lambdacode_arrow: hut::Uniqtype -> Bool
=
fn t = case (hut::uniqtype_to_type t) hut::type::TYP x => uniqtyp_is_lambdacode_arrow x;
_ => FALSE;
esac;
my uniqtype_is_lambdacode_typeagnostic: hut::Uniqtype -> Bool
=
fn t = case (hut::uniqtype_to_type t) hut::type::TYPEAGNOSTIC (_, [x]) => TRUE;
_ => FALSE;
esac;
my uniqtype_is_lambdacode_generic_package: hut::Uniqtype -> Bool
=
fn t = case (hut::uniqtype_to_type t) hut::type::GENERIC_PACKAGE ([x], [y]) => TRUE;
_ => FALSE;
esac;
# Our plambda hut::Uniqtyp-hut::Uniqtype one-arm switches
#
fun if_uniqtyp_is_lambdacode_arrow (tc, f, g)
=
case (hut::uniqtyp_to_typ tc) hut::typ::ARROW (_,[x],[y]) => f (x, y);
_ => g tc;
esac;
fun if_uniqtype_is_lambdacode_arrow (lt, f, g)
=
case (hut::uniqtype_to_type lt)
#
hut::type::TYP tc
=>
case (hut::uniqtyp_to_typ tc) hut::typ::ARROW (_,[x],[y]) => f (x, y);
_ => g lt;
esac;
_ => g lt;
esac;
fun if_uniqtype_is_lambdacode_typeagnostic (lt, f, g)
=
case (hut::uniqtype_to_type lt) hut::type::TYPEAGNOSTIC (ks,[x]) => f (ks, x);
_ => g lt;
esac;
fun if_uniqtype_is_lambdacode_generic_package (lt, f, g)
=
case (hut::uniqtype_to_type lt)
#
hut::type::GENERIC_PACKAGE ([x],[y]) => f (x, y);
_ => g lt;
esac;
}; # package highcode_type
end; # top-level stipulate