## highcode-form.pkg # "ltybasic.sml" in SML/NJ
# Compiled by:
# src/lib/compiler/core.sublib### "There are only two kinds of math books:
### Those you cannot read beyond the first sentence,
### and those you cannot read beyond the first page."
###
### -- C.N. Yang, circa 1980 I think.
### [Nobel Prize in theoretical physics, 1957]
### "I like mathematics because it is not human
### and has nothing particular to do with this
### planet or with the whole accidental universe
### -- because like Spinoza's God, it won't love
### us in return."
###
### -- Bertrand Russell, 1912
stipulate
package acf = anormcode_form; # anormcode_form is from src/lib/compiler/back/top/anormcode/anormcode-form.pkg 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 hbo = highcode_baseops; # highcode_baseops is from src/lib/compiler/back/top/highcode/highcode-baseops.pkg package hbt = highcode_basetypes; # highcode_basetypes is from src/lib/compiler/back/top/highcode/highcode-basetypes.pkg package hct = highcode_type; # highcode_type is from src/lib/compiler/back/top/highcode/highcode-type.pkg package hut = highcode_uniq_types; # highcode_uniq_types is from src/lib/compiler/back/top/highcode/highcode-uniq-types.pkg package lms = list_mergesort; # list_mergesort is from src/lib/src/list-mergesort.pkg package tmp = highcode_codetemp; # highcode_codetemp is from src/lib/compiler/back/top/highcode/highcode-codetemp.pkg #
# Really should not refer to this.
fun bug msg = err::impossible ("highcode: " + msg);
say = global_controls::print::say;
herein
package highcode_form
: (weak) Highcode_Form # Highcode_Form is from src/lib/compiler/back/top/highcode/highcode-form.api {
stipulate
fun plist (p, []) => ""; # "plist" might be "print list".
plist (p, x ! xs) => (p x) + (string::cat (map (fn z = (", " + (p z))) xs));
end;
#
fun callnotes_to_string (hut::VARIABLE_CALLING_CONVENTION { arg_is_raw, body_is_raw })
=>
callnotes_to_string' (arg_is_raw, body_is_raw)
where
fun callnotes_to_string' (TRUE, TRUE ) => "rr"; # "r"=="raw", "c"=="cooked".
callnotes_to_string' (TRUE, FALSE) => "rc";
callnotes_to_string' (FALSE, TRUE ) => "cr";
callnotes_to_string' (FALSE, FALSE) => "cc";
end;
end;
callnotes_to_string hut::FIXED_CALLING_CONVENTION
=>
"f";
end;
#
fun parw (p, (callnotes, t1, t2)) # "parw" might be "polylambda arrow"...? or "print arrow"...?
=
"<"
+ (p t1)
+ "> -"
+ callnotes_to_string callnotes
+ "-> <"
+ (p t2)
+ ">";
herein
include highcode_type; # highcode_type is from src/lib/compiler/back/top/highcode/highcode-type.pkg # Utility functions for constructing tkinds
#
#
fun n_plaintype_uniqkinds n # Also used in translate_types and translate_deep_syntax_to_lambdacode
=
h (n, [])
where
fun h (n, results)
=
if (n < 1) results;
else h (n - 1, plaintype_uniqkind ! results);
fi;
end;
stipulate
# Precompute and save the three most
# common cases -- 1, 2 or 3 args:
#
one___arg_fn = make_kindfun_uniqkind (n_plaintype_uniqkinds 1, plaintype_uniqkind);
two___arg_fn = make_kindfun_uniqkind (n_plaintype_uniqkinds 2, plaintype_uniqkind);
three_arg_fn = make_kindfun_uniqkind (n_plaintype_uniqkinds 3, plaintype_uniqkind);
herein
#
fun make_n_arg_typ_fun_uniqkind 0 => plaintype_uniqkind;
make_n_arg_typ_fun_uniqkind 1 => one___arg_fn;
make_n_arg_typ_fun_uniqkind 2 => two___arg_fn;
make_n_arg_typ_fun_uniqkind 3 => three_arg_fn;
make_n_arg_typ_fun_uniqkind i => make_kindfun_uniqkind (n_plaintype_uniqkinds i, plaintype_uniqkind);
end;
end;
# Base Calling_Conventions and Useless_Recordflags:
#
rawraw_variable_calling_convention
=
make_variable_calling_convention
{
arg_is_raw => TRUE,
body_is_raw => TRUE
};
# Called (only) from: src/lib/compiler/back/top/improve/specialize-anormcode-to-least-general-type.pkg #
fun update_calling_convention (x as hut::FIXED_CALLING_CONVENTION, { arg_is_raw => TRUE, body_is_raw => TRUE }) => x;
update_calling_convention (x as hut::VARIABLE_CALLING_CONVENTION _, arg_is_raw__body_is_raw) => make_variable_calling_convention arg_is_raw__body_is_raw;
#
update_calling_convention _ => bug "unexpected case in update_calling_convention";
end;
#
fun unpack_calling_convention (hut::FIXED_CALLING_CONVENTION) => { arg_is_raw => TRUE, body_is_raw => TRUE };
unpack_calling_convention (hut::VARIABLE_CALLING_CONVENTION arg_is_raw__body_is_raw ) => arg_is_raw__body_is_raw;
end;
# Unlike hct::unpack_variable_calling_convention
# and hct::unpack_fixed_calling_convention
# our unpack_calling_convention
# fn returns a usable result for any Calling_Convention arg.
# Precompute various commonly used basetype uniqtyps:
#
int_uniqtyp = make_basetype_uniqtyp hbt::basetype_tagged_int;
int1_uniqtyp = make_basetype_uniqtyp hbt::basetype_int1;
float64_uniqtyp = make_basetype_uniqtyp hbt::basetype_float64;
string_uniqtyp = make_basetype_uniqtyp hbt::basetype_string;
exception_uniqtyp = make_basetype_uniqtyp hbt::basetype_exception;
truevoid_uniqtyp = make_basetype_uniqtyp hbt::basetype_truevoid;
#
void_uniqtyp = make_tuple_uniqtyp [];
#
bool_uniqtyp
=
{ tbool = make_sum_uniqtyp [void_uniqtyp, void_uniqtyp];
tsig_bool = make_typefun_uniqtyp ([plaintype_uniqkind], tbool);
make_recursive_uniqtyp((1, tsig_bool, []), 0);
};
#
list_uniqtyp # Not exported -- used for printing.
=
{ alpha = make_debruijn_typevar_uniqtyp (di::innermost, 0);
tlist = make_debruijn_typevar_uniqtyp (di::innersnd, 0);
alist = make_apply_typefun_uniqtyp (tlist, [alpha]);
tcc_cons = make_tuple_uniqtyp [alpha, alist];
tlist = make_typefun_uniqtyp([plaintype_uniqkind], make_sum_uniqtyp [tcc_cons, void_uniqtyp]);
# The order here should be consistent with that in
# src/lib/compiler/front/typer/types/type-types.pkg tsig_list = make_typefun_uniqtyp([make_n_arg_typ_fun_uniqkind 1], tlist);
make_recursive_uniqtyp((1, tsig_list, []), 0);
};
#
fun make_typevar_i_uniqtyp i = make_debruijn_typevar_uniqtyp (di::innermost, i);
#
fun make_ref_uniqtyp x = make_apply_typefun_uniqtyp (make_basetype_uniqtyp hbt::basetype_ref, [x]);
fun make_rw_vector_uniqtyp x = make_apply_typefun_uniqtyp (make_basetype_uniqtyp hbt::basetype_rw_vector, [x]);
fun make_ro_vector_uniqtyp x = make_apply_typefun_uniqtyp (make_basetype_uniqtyp hbt::basetype_vector, [x]);
fun make_exception_tag_uniqtyp x = make_apply_typefun_uniqtyp (make_basetype_uniqtyp hbt::basetype_exception_tag, [x]);
# Prebuilt basetype uniqtypes:
#
int_uniqtype = make_typ_uniqtype int_uniqtyp;
int1_uniqtype = make_typ_uniqtype int1_uniqtyp;
float64_uniqtype = make_typ_uniqtype float64_uniqtyp;
string_uniqtype = make_typ_uniqtype string_uniqtyp;
exception_uniqtype = make_typ_uniqtype exception_uniqtyp;
truevoid_uniqtype = make_typ_uniqtype truevoid_uniqtyp;
void_uniqtype = make_typ_uniqtype void_uniqtyp;
bool_uniqtype = make_typ_uniqtype bool_uniqtyp;
# Uniqtype constructors:
#
make_typevar_i_uniqtype = make_typ_uniqtype o make_typevar_i_uniqtyp;
make_ref_uniqtype = make_typ_uniqtype o make_ref_uniqtyp o unpack_typ_uniqtype;
make_rw_vector_uniqtype = make_typ_uniqtype o make_rw_vector_uniqtyp o unpack_typ_uniqtype;
make_ro_vector_uniqtype = make_typ_uniqtype o make_ro_vector_uniqtyp o unpack_typ_uniqtype;
make_exception_tag_uniqtype = make_typ_uniqtype o make_exception_tag_uniqtyp o unpack_typ_uniqtype;
############################################################################
# UTILITY FUNCTIONS FOR TESTING EQUIVALENCE
############################################################################
# Testing equivalence of tkinds,
# typs, ltys, fflags, and rflags:
#
my same_uniqkind: (hut::Uniqkind, hut::Uniqkind) -> Bool = hut::same_uniqkind;
my same_uniqtyp: (hut::Uniqtyp, hut::Uniqtyp) -> Bool = hut::same_uniqtyp;
my same_uniqtype: (hut::Uniqtype, hut::Uniqtype) -> Bool = hut::same_uniqtype;
my same_callnotes: (hut::Calling_Convention, hut::Calling_Convention) -> Bool = hut::same_callnotes;
my same_recordflag: (hut::Useless_Recordflag, hut::Useless_Recordflag) -> Bool = hut::same_recordflag;
# Testing the equivalence for typs and
# ltys with relaxed constraints:
#
my similar_uniqtyps: (hut::Uniqtyp, hut::Uniqtyp) -> Bool = hut::similar_uniqtyps;
my similar_uniqtypes: (hut::Uniqtype, hut::Uniqtype) -> Bool = hut::similar_uniqtypes;
############################################################################
# UTILITY FUNCTIONS FOR PRETTY PRINTING
############################################################################
# Prettyprinting of tkinds, typs, and ltys:
#
fun uniqkind_to_string (x: hut::Uniqkind)
=
g (hut::uniqkind_to_kind x)
where
fun g hut::kind::PLAINTYPE => "K0";
g hut::kind::BOXEDTYPE => "KB0";
g (hut::kind::KINDFUN (ks, k))
=>
"<" + (plist (uniqkind_to_string, ks)) + "->" + (uniqkind_to_string k) + ">";
g (hut::kind::KINDSEQ zs)
=>
"KS(" + (plist (uniqkind_to_string, zs)) + ")";
end;
end;
#
fun uniqtyp_to_string (x: hut::Uniqtyp)
=
g (hut::uniqtyp_to_typ x)
where
fun g (hut::typ::DEBRUIJN_TYPEVAR (i, j)) => "TV(" + (di::di_print i) + ", " + (int::to_string j) + ")";
g (hut::typ::NAMED_TYPEVAR v) => "NTV (v" + (int::to_string v) + ")";
g (hut::typ::BASETYPE pt)
=>
hbt::basetype_to_string pt;
g (hut::typ::TYPEFUN (ks, t))
=>
"(\\[" + plist (uniqkind_to_string, ks) + "]." + (uniqtyp_to_string t) + ")";
g (hut::typ::APPLY_TYPEFUN (t, [])) => uniqtyp_to_string t + "[]";
g (hut::typ::APPLY_TYPEFUN (t, zs)) => (uniqtyp_to_string t) + "[" + (plist (uniqtyp_to_string, zs)) + "]";
g (hut::typ::TYPESEQ zs) => "TS(" + (plist (uniqtyp_to_string, zs)) + ")";
g (hut::typ::ITH_IN_TYPESEQ (t, i)) => "TP(" + (uniqtyp_to_string t) + ", " + (int::to_string i) + ")";
g (hut::typ::SUM tcs) => "TSUM(" + (plist (uniqtyp_to_string, tcs)) + ")";
g (hut::typ::RECURSIVE ((_, tc, ts), i))
=>
if (same_uniqtyp (x, bool_uniqtyp)) "B";
elif (same_uniqtyp (x, list_uniqtyp)) "LST";
else
# ntc = case ts
# [] => tc;
# _ => make_apply_typefun_uniqtyp (tc, ts);
# esac;
"DT { " + "DATA" +
# "[" +
# (uniqtyp_to_string tc) +
# "] &&" +
# (plist (uniqtyp_to_string, ts)) +
# "&&"
"====" +
(int::to_string i) +
"}";
fi;
g (hut::typ::ABSTRACT t) => "Ax(" + (uniqtyp_to_string t) + ")";
g (hut::typ::BOXED t) => "Bx(" + (uniqtyp_to_string t) + ")";
g (hut::typ::TUPLE(_, zs)) => "TT<" + (plist (uniqtyp_to_string, zs)) + ">";
g (hut::typ::ARROW (ff, z1, z2)) => parw (fn u = plist (uniqtyp_to_string, u), (ff, z1, z2));
g (hut::typ::PARROW _) => bug "unexpected TC_PARROW in uniqtyp_to_string";
g (hut::typ::EXTENSIBLE_TOKEN (k, t))
=>
if (hut::token_is_valid k) (hut::token_abbreviation k) + "(" + (uniqtyp_to_string t) + ")";
else bug "unexpected TC_EXTENSIBLE_TOKEN typ in uniqtyp_to_string";
fi;
g (hut::typ::FATE ts)
=>
"Count(" + (plist (uniqtyp_to_string, ts)) + ")";
g (hut::typ::INDIRECT_TYPE_THUNK _) => bug "unexpected TC_INDIRECT in uniqtyp_to_string";
g (hut::typ::TYPE_CLOSURE _) => bug "unexpected TC_CLOSURE in uniqtyp_to_string";
end;
end; # fun uniqtyp_to_string
#
fun uniqtype_to_string (x: hut::Uniqtype)
=
g (hut::uniqtype_to_type x)
where
fun h (i, t)
=
"(" + (int::to_string i) + ", " + (uniqtype_to_string t) + ")";
#
fun g (hut::type::TYP t) => uniqtyp_to_string t;
g (hut::type::PACKAGE zs) => "S { " + (plist (uniqtype_to_string, zs)) + "}";
g (hut::type::GENERIC_PACKAGE (ts1, ts2))
=>
"(" + (plist (uniqtype_to_string, ts1)) + ") ==> ("
+ (plist (uniqtype_to_string, ts2)) + ")";
g (hut::type::TYPEAGNOSTIC (ks, ts))
=>
"(Q[" + plist (uniqkind_to_string, ks) + "]."
+ (plist (uniqtype_to_string, ts)) + ")";
g (hut::type::FATE ts)
=>
"COUNT(" + (plist (uniqtype_to_string, ts)) + ")";
g (hut::type::INDIRECT_TYPE_THUNK _) => bug "unexpected INDIRECT_TYPE_THUNK in uniqtype_to_string";
g (hut::type::TYPE_CLOSURE _) => bug "unexpected TYPE_CLOSURE in uniqtype_to_string";
end;
end; # fun uniqtype_to_string
# Finding out the depth for a typ's
# innermost-bound free variables
#
my max_freevar_depth_in_uniqtyp: (hut::Uniqtyp, di::Debruijn_Depth) -> di::Debruijn_Depth = hut::max_freevar_depth_in_uniqtyp;
my max_freevar_depth_in_uniqtyps: (List( hut::Uniqtyp ), di::Debruijn_Depth) -> di::Debruijn_Depth = hut::max_freevar_depth_in_uniqtyps;
# Adjusting an hut::Uniqtype or hut::Uniqtyp
# from one depth to another
#
fun change_depth_of_uniqtype (lt, d, nd)
=
if (d == nd) lt;
else hut::make_type_closure_uniqtype (lt, 0, nd - d, hut::empty_uniqtyp_dictionary);
fi;
#
fun change_depth_of_uniqtyp (tc, d, nd)
=
if (d == nd) tc;
else hut::make_type_closure_uniqtyp (tc, 0, nd - d, hut::empty_uniqtyp_dictionary);
fi;
stipulate
fun make_typ_dictionary (i, k, dd, e)
=
if (i >= k) e;
else make_typ_dictionary (i+1, k, dd, hut::cons_entry_onto_uniqtyp_dictionary (e, (NULL, dd+i)));
fi;
herein
#
fun change_k_depth_of_uniqtype (lt, d, nd, k)
=
if (d == nd) lt;
else hut::make_type_closure_uniqtype (lt, k, nd-d+k, make_typ_dictionary (0, k, nd-d, hut::empty_uniqtyp_dictionary));
fi;
#
fun change_k_depth_of_uniqtyp (tc, d, nd, k)
=
if (d == nd) tc;
else hut::make_type_closure_uniqtyp (tc, k, nd-d+k, make_typ_dictionary (0, k, nd-d, hut::empty_uniqtyp_dictionary));
fi;
end;
############################################################################
# UTILITY FUNCTIONS ON LTY DICTIONARY
############################################################################
# Utility values and functions on lty_env
#
Highcode_Variable_To_Uniqtype_Map = int_red_black_map::Map( (hut::Uniqtype, di::Debruijn_Depth) );
exception HIGHCODE_VARIABLE_NOT_FOUND;
my empty_highcode_variable_to_uniqtype_map: Highcode_Variable_To_Uniqtype_Map
=
int_red_black_map::empty;
#
fun get_uniqtype_for_var (venv, lv, nd)
=
case (int_red_black_map::get (venv, lv))
NULL
=>
{ say "**** hmmm, I didn't find the variable ";
say (int::to_string lv); say "\n";
raise exception HIGHCODE_VARIABLE_NOT_FOUND;
};
THE (lt, d)
=>
if (d == nd) lt;
elif (d > nd) bug "unexpected depth info in ltLookup";
else hut::make_type_closure_uniqtype (lt, 0, nd - d, hut::empty_uniqtyp_dictionary);
fi;
esac;
#
fun set_uniqtype_for_var (venv, lv, lt, d)
=
int_red_black_map::set (venv, lv, (lt, d));
end; # top-level stipulate
# Instantiate a typeagnostic type
# or a higher-order constructor.
#
# Compare with apply_typeagnostic_type_to_arglist_with_checking_thunk() below,
# which does the same thing with more checking.
#
fun apply_typeagnostic_type_to_arglist
(
lt: hut::Uniqtype, # typefun
ts: List( hut::Uniqtyp ) # arglist for typefun.
)
=
{ nt = hut::reduce_uniqtype_to_weak_head_normal_form lt;
case (/* lt_outX */ hut::uniqtype_to_type nt, ts)
(hut::type::TYPEAGNOSTIC (ks, b), ts)
=>
{ nenv = hut::cons_entry_onto_uniqtyp_dictionary (hut::empty_uniqtyp_dictionary, (THE ts, 0));
#
map (fn x = hut::make_type_closure_uniqtype (x, 1, 0, nenv))
b;
};
(_, []) => [nt]; # This requires further clarifications !!! XXX FIXME BUGGO
_ => bug "incorrect hut::Uniqtype instantiation in apply_typeagnsotic_type_to_arglist";
esac;
};
#
fun apply_typeagnostic_type_to_arglist_with_single_result
(
lt: hut::Uniqtype,
ts: List( hut::Uniqtyp )
)
=
case (apply_typeagnostic_type_to_arglist (lt, ts))
#
[y] => y;
_ => bug "unexpected pmacroExpandTypeagnosticLambdaTypeOrHOC";
esac;
############################################################################
# KIND-CHECKING ROUTINES
############################################################################
exception KIND_TYP_CHECK_FAILED;
exception APPLY_TYPEFUN_CHECK_FAILED;
# tk_subkind returns TRUE if k1 is a subkind of k2, or if they are
# equivalent kinds. It is NOT commutative. tks_subkind is the same
# thing, component-wise on lists of kinds.
#
fun are_subkinds (ks1, ks2)
=
paired_lists::all is_subkind (ks1, ks2) # Component-wise
also
fun is_subkind (k1, k2)
=
same_uniqkind (k1, k2) # reflexive
or
case (hut::uniqkind_to_kind k1, hut::uniqkind_to_kind k2)
#
( hut::kind::BOXEDTYPE,
hut::kind::PLAINTYPE
)
=>
TRUE; # ground kinds (base case)
# This next case is WRONG, but necessary until the
# infrastructure is there to give proper boxed kinds to
# certain typs (e.g., REF: Omega -> Omega_b) XXX BUGGO FIXME
#
( hut::kind::PLAINTYPE,
hut::kind::BOXEDTYPE
)
=>
TRUE;
( hut::kind::KINDSEQ ks1,
hut::kind::KINDSEQ ks2
)
=>
are_subkinds (ks1, ks2);
( hut::kind::KINDFUN (ks1, k1'),
hut::kind::KINDFUN (ks2, k2')
)
=>
are_subkinds (ks1, ks2) and # Contravariant
is_subkind (k1', k2');
_ => FALSE;
esac;
# Is kind 'k' typelocked?
#
fun tk_is_mono k
=
is_subkind (k, plaintype_uniqkind);
# Assert that k1 is a subkind of k2:
#
fun assert_this_is_a_subkind_of_that { this, that }
=
if (not (is_subkind (this, that))) raise exception KIND_TYP_CHECK_FAILED; fi;
# Assert that a kind is typelocked:
#
fun tk_assert_is_mono k
=
if (not (tk_is_mono k)) raise exception KIND_TYP_CHECK_FAILED; fi;
# Select the ith element
# from a kind sequence:
#
fun select_ith_in_type_sequence (tk, i)
=
case (hut::uniqkind_to_kind tk)
#
(hut::kind::KINDSEQ ks)
=>
list::nth (ks, i)
except
_ = raise exception KIND_TYP_CHECK_FAILED;
_ => raise exception KIND_TYP_CHECK_FAILED;
esac;
#
fun tks_eqv (ks1, ks2)
=
same_uniqkind (make_kindseq_uniqkind ks1, make_kindseq_uniqkind ks2);
#
fun tk_app (tk, tks)
=
case (hut::uniqkind_to_kind tk)
#
hut::kind::KINDFUN (a, b)
=>
if (tks_eqv (a, tks)) b;
else raise exception KIND_TYP_CHECK_FAILED;
fi;
_ => raise exception KIND_TYP_CHECK_FAILED;
esac;
# Check the application of typs of kinds `tks'
# to a type function of kind `tk':
#
fun tk_app (tk, tks)
=
case (hut::uniqkind_to_kind tk)
#
hut::kind::KINDFUN (a, b)
=>
if (are_subkinds (tks, a)) b;
else raise exception KIND_TYP_CHECK_FAILED;
fi;
_ => raise exception KIND_TYP_CHECK_FAILED;
esac;
# Kind-checking naturally requires traversing type graphs.
#
# To avoid re-traversing bits of the dag, we use a dictionary
# to memoize the kind of each hut::Uniqtyp we process.
#
# One problem is that a hut::Uniqtyp can have different kinds,
# depending on the valuations of its free variables.
#
# So this dictionary maps a hut::Uniqtyp to an association list
# that maps the kinds of the free variables in the hut::Uniqtyp
# (represented as a TYPEKIND_TYPESEQ) to the hut::Uniqtyp's kind.
#
package uniqtyp_dictionary # XXX BUGGO FIXME is there any reason to be using binary_map_g instead of the standard red_black_map_g ?
=
binary_map_g ( # binary_map_g is from src/lib/src/binary-map-g.pkg Key = hut::Uniqtyp;
compare = hut::compare_uniqtyps;
);
package memo:
api {
Dictionary;
#
make_dictionary: Void -> Dictionary;
#
recall_or_compute_uniqkind_of_uniqtyp
:
( Dictionary,
hut::Debruijn_To_Uniqkind_Listlist,
hut::Uniqtyp,
(Void -> hut::Uniqkind)
)
->
hut::Uniqkind;
}
{
package uniqtyp_dictionary
=
red_black_map_g ( # red_black_map_g is from src/lib/src/red-black-map-g.pkg #
Key = hut::Uniqtyp;
compare = hut::compare_uniqtyps;
);
Dictionary
=
Ref( uniqtyp_dictionary::Map( List ( (hut::Uniqkind, hut::Uniqkind) ) ) ); # XXX BUGGO FIXME More icky thread-hostile global mutable state.
my make_dictionary: Void -> Dictionary
=
REF o (fn () = uniqtyp_dictionary::empty);
#
fun recall_or_compute_uniqkind_of_uniqtyp
(
dictionary: Dictionary,
debruijn_to_uniqkind_listlist: hut::Debruijn_To_Uniqkind_Listlist, # Maps typevars to their Uniqkinds.
uniqtyp: hut::Uniqtyp, # Our primary input.
uniqkind_of_uniqtyp_thunk: Void -> hut::Uniqkind # This will compute needed result from first principles, if we don't find it in our cache.
): hut::Uniqkind
=
case (hut::get_uniqkinds_of_free_typevars_of_uniqtyp (debruijn_to_uniqkind_listlist, uniqtyp))
#
THE (uniqkinds_of_free_typevars: List(hut::Uniqkind))
=>
{
# Encode those as a hut::kind::KINDSEQ:
#
typevars_kindseq = make_kindseq_uniqkind uniqkinds_of_free_typevars;
# Query the dictionary:
#
kci = case (uniqtyp_dictionary::get (*dictionary, uniqtyp))
#
THE kci => kci;
NULL => [];
esac;
# Get for an equivalent dictionary:
#
fun same_dictionary_identifier (typevars_kindseq', _)
=
same_uniqkind (typevars_kindseq, typevars_kindseq');
case (list::find same_dictionary_identifier kci)
#
THE (_, uniqkind) # Cache hit -- return cached kind.
=>
uniqkind;
NULL => # Not in the list -- compute and cache typ's kind.
uniqkind
where
#
uniqkind = uniqkind_of_uniqtyp_thunk ();
#
kci' = (typevars_kindseq, uniqkind) ! kci;
dictionary := uniqtyp_dictionary::set (*dictionary, uniqtyp, kci');
end;
esac;
};
NULL =>
# freevars were not available.
# We'll have to recompute and
# cannot cache the result.
#
uniqkind_of_uniqtyp_thunk ();
esac;
}; # package memo
# Return the kind of a given typ
# in the given kind dictionary
#
fun get_uniqkind_of_uniqtyp_thunk () # Evaluating the thunk allocates a fresh memo dictionary.
=
get_uniqkind_of_uniqtyp
where
dictionary = memo::make_dictionary ();
#
fun get_uniqkind_of_uniqtyp debruijn_to_uniqkind_listlist (uniqtyp: hut::Uniqtyp)
=
memo::recall_or_compute_uniqkind_of_uniqtyp (dictionary, debruijn_to_uniqkind_listlist, uniqtyp, uniqkind_of_uniqtyp_thunk)
where
g = get_uniqkind_of_uniqtyp debruijn_to_uniqkind_listlist; # Default recursive invocation.
# How to compute the kind of a typ
#
fun uniqkind_of_uniqtyp_thunk ()
=
case (hut::uniqtyp_to_typ uniqtyp)
#
hut::typ::DEBRUIJN_TYPEVAR (depth, index) => hut::debruijn_to_uniqkind (debruijn_to_uniqkind_listlist, depth, index);
hut::typ::NAMED_TYPEVAR _ => bug "TC_NAMED_VAR not supported yet in get_uniqkind_of_uniqtyp";
hut::typ::BASETYPE pt => make_n_arg_typ_fun_uniqkind (highcode_basetypes::basetype_arity pt);
hut::typ::TYPEFUN (ks, tc) => make_kindfun_uniqkind (ks, get_uniqkind_of_uniqtyp (hut::prepend_uniqkind_list_to_map (debruijn_to_uniqkind_listlist, ks)) tc);
hut::typ::APPLY_TYPEFUN (tc, tcs) => tk_app (g tc, map g tcs);
hut::typ::TYPESEQ tcs => make_kindseq_uniqkind (map g tcs);
hut::typ::ITH_IN_TYPESEQ (tc, i) => select_ith_in_type_sequence (g tc, i);
hut::typ::SUM tcs
=>
{ list::apply (tk_assert_is_mono o g) tcs;
plaintype_uniqkind;
};
hut::typ::RECURSIVE ((n, tc, ts), i)
=>
{ k = g tc;
nk = case ts
[] => k;
_ => tk_app (k, map g ts);
esac;
case (hut::uniqkind_to_kind nk)
#
hut::kind::KINDFUN (a, b)
=>
{ arg = case a [x] => x;
_ => make_kindseq_uniqkind a;
esac;
if (is_subkind (arg, b)) # order?
#
n == 1 ?? b
:: select_ith_in_type_sequence (arg, i);
else
raise exception KIND_TYP_CHECK_FAILED;
fi;
};
_ => raise exception KIND_TYP_CHECK_FAILED;
esac;
};
hut::typ::ABSTRACT tc
=>
{ tk_assert_is_mono (g tc);
plaintype_uniqkind;
};
hut::typ::BOXED tc
=>
{ tk_assert_is_mono (g tc);
plaintype_uniqkind;
};
hut::typ::TUPLE (_, tcs)
=>
{ list::apply (tk_assert_is_mono o g) tcs;
plaintype_uniqkind;
};
hut::typ::ARROW (_, ts1, ts2)
=>
{ list::apply (tk_assert_is_mono o g) ts1;
list::apply (tk_assert_is_mono o g) ts2;
plaintype_uniqkind;
};
hut::typ::EXTENSIBLE_TOKEN(_, tc)
=>
{ tk_assert_is_mono (g tc);
plaintype_uniqkind;
};
hut::typ::PARROW _ => bug "unexpected TC_PARROW in tkTypeConstructor";
hut::typ::TYPE_CLOSURE _ => bug "unexpected TC_CLOSURE in tkTypeConstructor";
hut::typ::INDIRECT_TYPE_THUNK _ => bug "unexpected TC_INDIRECT in tkTypeConstructor";
hut::typ::FATE _ => bug "unexpected TC_FATE in tkTypeConstructor";
esac;
end; # fun get_uniqkind_of_uniqtyp
end; # fun get_uniqkind_of_uniqtyp_thunk
# Assert that the kind of `typ'
# is a subkind of `kind' in `debruijn_to_uniqkind_listlist':
#
fun assert_typ_has_subkind_of_kind_thunk () # Evaluating the thunk allocates a new memo dictionary.
=
assert_typ_has_subkind_of_kind
where
get_uniqkind_of_uniqtyp = get_uniqkind_of_uniqtyp_thunk (); # Allocate a fresh memo dictionary.
#
fun assert_typ_has_subkind_of_kind debruijn_to_uniqkind_listlist (kind, typ)
=
assert_this_is_a_subkind_of_that
{
this => get_uniqkind_of_uniqtyp debruijn_to_uniqkind_listlist typ,
that => kind
};
end;
# hut::Uniqtype application with kind-checking (exported)
#
# Compare with apply_typeagnostic_type_to_arglist
# above, which does the same thing with less checking.
#
fun apply_typeagnostic_type_to_arglist_with_checking_thunk () # Evaluating the thunk allocates a new memo dictionary.
=
apply_typeagnostic_type_to_arglist_with_checking
where
assert_typ_has_subkind_of_kind =
assert_typ_has_subkind_of_kind_thunk (); # Evaluating the thunk allocates a new memo dictionary.
#
fun apply_typeagnostic_type_to_arglist_with_checking
(
fn_type: hut::Uniqtype, # Fn type.
fn_arg_typs: List(hut::Uniqtyp), # Types of args to which fn is being applied.
debruijn_to_uniqkind_listlist: hut::Debruijn_To_Uniqkind_Listlist
)
=
{ fn_type_in_whnf = hut::reduce_uniqtype_to_weak_head_normal_form fn_type;
case (/* lt_outX */ hut::uniqtype_to_type fn_type_in_whnf, fn_arg_typs)
#
(hut::type::TYPEAGNOSTIC (fn_parameter_kinds, b), fn_arg_typs) # 'b' == 'body type(s)'...? It has type List(Uniqtype)
=>
{ paired_lists::apply (assert_typ_has_subkind_of_kind debruijn_to_uniqkind_listlist) (fn_parameter_kinds, fn_arg_typs);
#
fun h x
=
hut::make_type_closure_uniqtype (x, 1, 0, hut::cons_entry_onto_uniqtyp_dictionary (hut::empty_uniqtyp_dictionary, (THE fn_arg_typs, 0)));
map h b;
};
(_, []) => [fn_type_in_whnf]; # ? problematic XXX BUGGO FIXME Appears to say "don't complain about bad fn type if no args".
_ => raise exception APPLY_TYPEFUN_CHECK_FAILED; # This is the only place we raise this exception.
esac;
};
end;
# A special hut::Uniqtype application used inside
#
# src/lib/compiler/back/top/improve/specialize-anormcode-to-least-general-type.pkg #
fun lt_sp_adj (ks, lt, ts, dist, bnl)
=
h (dist, 1, bnl, btenv)
where
btenv = hut::cons_entry_onto_uniqtyp_dictionary (hut::empty_uniqtyp_dictionary, (THE ts, 0));
#
fun h (abslevel, ol, nl, tenv)
=
if (abslevel == 0)
#
hut::make_type_closure_uniqtype (lt, ol, nl, tenv);
#
elif (abslevel > 0)
#
h (abslevel - 1, ol+1, nl+1, hut::cons_entry_onto_uniqtyp_dictionary (tenv, (NULL, nl)));
else
bug "unexpected cases in ltAdjSt";
fi;
end;
# A special typ application used
# inside src/lib/compiler/back/top/improve/specialize-anormcode-to-least-general-type.pkg #
fun tc_sp_adj (ks, tc, ts, dist, bnl)
=
h (dist, 1, bnl, btenv)
where
btenv = hut::cons_entry_onto_uniqtyp_dictionary (hut::empty_uniqtyp_dictionary, (THE ts, 0));
#
fun h (abslevel, ol, nl, tenv)
=
if (abslevel == 0) hut::make_type_closure_uniqtyp (tc, ol, nl, tenv);
elif (abslevel > 0) h (abslevel - 1, ol+1, nl+1, hut::cons_entry_onto_uniqtyp_dictionary (tenv, (NULL, nl)));
else bug "unexpected cases in tcAdjSt";
fi;
end;
# * Sinking the hut::Uniqtype one-level down -- used inside specialize-anormcode-to-least-general-type.pkg
#
fun lt_sp_sink (ks, lt, d, nd)
=
{ fun h (abslevel, ol, nl, tenv)
=
if (abslevel == 0)
#
hut::make_type_closure_uniqtype (lt, ol, nl, tenv);
#
elif (abslevel > 0)
#
h (abslevel - 1, ol+1, nl+1, hut::cons_entry_onto_uniqtyp_dictionary(tenv, (NULL, nl)));
else
bug "unexpected cases in ltSinkSt";
fi;
nt = h (nd-d, 0, 1, hut::empty_uniqtyp_dictionary);
nt; # was reduceLambdaTypeToNormalForm nt
};
# * Sinking the typ one-level down -- used inside specialize-anormcode-to-least-general-type.pkg
#
fun tc_sp_sink (ks, tc, d, nd)
=
{ fun h (abslevel, ol, nl, tenv)
=
if (abslevel == 0) hut::make_type_closure_uniqtyp (tc, ol, nl, tenv);
elif (abslevel > 0) h (abslevel - 1, ol+1, nl+1, hut::cons_entry_onto_uniqtyp_dictionary (tenv, (NULL, nl)));
else bug "unexpected cases in ltSinkSt";
fi;
nt = h (nd-d, 0, 1, hut::empty_uniqtyp_dictionary);
nt; # was reduceTypeConstructorToNormalForm nt
};
# Utility functions used in nextcode:
#
fun lt_is_fate lt
=
case (hut::uniqtype_to_type lt)
#
hut::type::FATE _
=>
TRUE;
hut::type::TYP tc
=>
case (hut::uniqtyp_to_typ tc) hut::typ::FATE _ => TRUE;
_ => FALSE;
esac;
_ => FALSE;
esac;
#
fun ltw_is_fate (lt, f, g, h)
=
case (hut::uniqtype_to_type lt)
#
hut::type::FATE t
=>
f t;
hut::type::TYP tc
=>
case (hut::uniqtyp_to_typ tc) hut::typ::FATE x => g x;
_ => h lt;
esac;
_ => h lt;
esac;
#
fun tc_bug tc s = bug (s + "\n\n" + (uniqtyp_to_string tc) + "\n\n");
fun lt_bug lt s = bug (s + "\n\n" + (uniqtype_to_string lt) + "\n\n");
# Other misc utility functions:
#
fun tc_get_field (tc, i)
=
case (hut::uniqtyp_to_typ tc)
#
hut::typ::TUPLE (_, zs)
=>
(list::nth (zs, i))
except
_ = bug "wrong TC_TUPLE in tc_get_field";
_ => tc_bug tc "wrong TCs in tc_get_field";
esac;
#
fun lt_get_field (t, i)
=
case (hut::uniqtype_to_type t)
#
hut::type::PACKAGE ts
=>
(list::nth (ts, i))
except
_ = bug "incorrect PACKAGE in lt_get_field";
#
hut::type::TYP tc
=>
make_typ_uniqtype (tc_get_field (tc, i));
_ => bug "incorrect lambda types in lt_get_field";
esac;
#
fun tc_swap t
=
case (hut::uniqtyp_to_typ t)
#
hut::typ::ARROW (hut::VARIABLE_CALLING_CONVENTION { arg_is_raw => r1, body_is_raw => r2 }, [s1], [s2])
=> make_arrow_uniqtyp (hut::VARIABLE_CALLING_CONVENTION { arg_is_raw => r2, body_is_raw => r1 }, [s2], [s1]);
#
hut::typ::ARROW (hut::FIXED_CALLING_CONVENTION, [s1], [s2])
=> make_arrow_uniqtyp (hut::FIXED_CALLING_CONVENTION, [s2], [s1]);
_ => bug "unexpected typs in tc_swap";
esac;
#
fun lt_swap t
=
case (hut::uniqtype_to_type t)
#
(hut::type::TYPEAGNOSTIC (ks, [x]))
=>
make_typeagnostic_uniqtype (ks, [lt_swap x]);
(hut::type::TYP x)
=>
make_typ_uniqtype (tc_swap x);
_ => bug "unexpected type in lt_swap";
esac;
# Functions that manipulate the highcode
# function and record types
#
fun ltc_fkfun ( { call_as=>acf::CALL_AS_GENERIC_PACKAGE, ... }: acf::Function_Notes, atys, rtys)
=>
make_generic_package_uniqtype ( atys, rtys);
ltc_fkfun ( { call_as=>acf::CALL_AS_FUNCTION fixed, ... }, atys, rtys)
=>
make_arrow_uniqtype (fixed, atys, rtys);
end;
#
fun ltd_fkfun lambda_type
=
if (uniqtype_is_generic_package lambda_type)
unpack_generic_package_uniqtype lambda_type;
else
my (_, atys, rtys) = unpack_arrow_uniqtype lambda_type;
(atys, rtys);
fi;
#
fun ltc_rkind (acf::RK_TUPLE _, lts) => make_tuple_uniqtype lts;
ltc_rkind (acf::RK_PACKAGE, lts) => make_package_uniqtype lts;
ltc_rkind (acf::RK_VECTOR t, _) => make_ro_vector_uniqtype (make_typ_uniqtype t);
end;
#
fun ltd_rkind (lt, i)
=
lt_get_field (lt, i);
#############################################################################
# UTILITY FUNCTIONS USED BY POST-REPRESENTATION ANALYSIS
#############################################################################
# Figure the appropriate baseop given a typ:
#
fun tc_upd_prim tc
=
h (hut::uniqtyp_to_typ tc)
where
fun h (hut::typ::BASETYPE pt)
=>
if (hbt::ubxupd pt) hbo::SET_VECSLOT_TO_TAGGED_INT_VALUE; # Tagged_Int case.
elif (hbt::bxupd pt) hbo::SET_VECSLOT_TO_BOXED_VALUE; # Everything else.
else hbo::SET_VECSLOT; # Int1, Float64, List, Null_Or, Generic_Machine_Word, Single_Word, Tagged_Int, Untagged_Int, Boxed, Dynamically_Typed.
fi;
h (hut::typ::TUPLE _ | hut::typ::ARROW _)
=>
hbo::SET_VECSLOT_TO_BOXED_VALUE;
h (hut::typ::RECURSIVE ((1, tc, ts), 0))
=>
{ ntc = case ts [] => tc;
_ => make_apply_typefun_uniqtyp (tc, ts);
esac;
case (hut::uniqtyp_to_typ ntc)
#
hut::typ::TYPEFUN([k], b) => h (hut::uniqtyp_to_typ b);
_ => hbo::SET_VECSLOT;
esac;
};
h (hut::typ::SUM tcs)
=>
{ fun g (a ! r) => same_uniqtyp (a, void_uniqtyp)
?? g r
:: FALSE;
g [] => TRUE;
end;
if (g tcs) hbo::SET_VECSLOT_TO_TAGGED_INT_VALUE;
else hbo::SET_VECSLOT;
fi;
};
h _ => hbo::SET_VECSLOT;
end;
end;
fun uniqkind_to_uniqtype (uniqkind: hut::Uniqkind) : hut::Uniqtype
=
case (hut::uniqkind_to_kind uniqkind)
#
hut::kind::PLAINTYPE => int_uniqtype;
hut::kind::BOXEDTYPE => int_uniqtype;
hut::kind::KINDSEQ ks => make_tuple_uniqtype (map uniqkind_to_uniqtype ks);
hut::kind::KINDFUN (ks, k) => make_arrow_uniqtype (fixed_calling_convention, [make_tuple_uniqtype (map uniqkind_to_uniqtype ks)], [uniqkind_to_uniqtype k]);
esac;
# tnarrow_fn: Void -> ((hut::Uniqtyp -> hut::Uniqtyp) * (hut::Uniqtype -> hut::Uniqtype) * (Void->Void))
#
fun tnarrow_fn ()
=
( tc_map o hut::reduce_uniqtyp_to_normal_form,
lt_map o hut::reduce_uniqtype_to_normal_form,
fn () = ()
)
where
fun tc_narrow tcf t
=
case (hut::uniqtyp_to_typ t)
#
hut::typ::BASETYPE pt
=>
if (hbt::isvoid pt) truevoid_uniqtyp;
else t;
fi;
hut::typ::TUPLE (_, tcs)
=>
make_tuple_uniqtyp (map tcf tcs);
hut::typ::ARROW (r, ts1, ts2)
=>
make_arrow_uniqtyp (fixed_calling_convention, map tcf ts1, map tcf ts2);
_ => truevoid_uniqtyp;
esac;
#
fun lt_narrow (tcf, ltf) t
=
case (hut::uniqtype_to_type t)
#
hut::type::TYP tc => make_typ_uniqtype (tcf tc);
hut::type::PACKAGE ts => make_package_uniqtype (map ltf ts);
#
hut::type::GENERIC_PACKAGE (ts1, ts2) => make_generic_package_uniqtype (map ltf ts1, map ltf ts2);
hut::type::TYPEAGNOSTIC (ks, xs) => make_generic_package_uniqtype([make_package_uniqtype (map uniqkind_to_uniqtype ks)], map ltf xs);
hut::type::FATE _ => bug "unexpected hut::type::FATE in ltNarrow";
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected hut::type::INDIRECT_TYPE_THUNK in ltNarrow";
hut::type::TYPE_CLOSURE _ => bug "unexpected hut::type::TYPE_CLOSURE in ltNarrow";
esac;
my { tc_map, lt_map }
=
highcode_dictionary::tmemo_fn
{
tcf => tc_narrow,
ltf => lt_narrow
};
end; # fun tnarrow_fn
# twrap_fn: Bool -> ( hut::Uniqtyp -> hut::Uniqtyp,
# hut::Uniqtype -> hut::Uniqtype,
# hut::Uniqtyp -> hut::Uniqtyp,
# hut::Uniqtype -> hut::Uniqtype,
# Void -> Void
# )
#
fun twrap_fn bbb
=
{ fun tc_wmap (w, u) t
=
case (hut::uniqtyp_to_typ t)
#
(hut::typ::DEBRUIJN_TYPEVAR _ | hut::typ::NAMED_TYPEVAR _) => t;
hut::typ::BASETYPE bt => if (hbt::basetype_is_unboxed bt) make_extensible_token_uniqtyp t; else t;fi;
hut::typ::TYPEFUN (ks, tc) => make_typefun_uniqtyp (ks, w tc); # impossible case
hut::typ::APPLY_TYPEFUN (tc, tcs) => make_apply_typefun_uniqtyp (w tc, map w tcs);
hut::typ::TYPESEQ tcs => make_typeseq_uniqtyp (map w tcs);
hut::typ::ITH_IN_TYPESEQ (tc, i) => make_ith_in_typeseq_uniqtyp (w tc, i);
hut::typ::SUM tcs => make_sum_uniqtyp (map w tcs);
#
hut::typ::RECURSIVE ((n, tc, ts), i)
=>
make_recursive_uniqtyp((n, hut::reduce_uniqtyp_to_normal_form (u tc), map w ts), i);
#
hut::typ::TUPLE (_, ts) => make_extensible_token_uniqtyp (make_tuple_uniqtyp (map w ts)); # ?
hut::typ::ARROW (hut::VARIABLE_CALLING_CONVENTION { arg_is_raw => b1, body_is_raw => b2 }, ts1, ts2)
=>
{ nts1 = case ts1 # Too specific !
[t11, t12] => [w t11, w t12];
_ => [w (hut::uniqtyp_list_to_uniqtyp_tuple ts1)];
esac;
nts2 = [w (hut::uniqtyp_list_to_uniqtyp_tuple ts2)];
nt = make_arrow_uniqtyp (fixed_calling_convention, nts1, nts2);
if b1 nt;
else make_extensible_token_uniqtyp nt;
fi;
};
#
hut::typ::ARROW (hut::FIXED_CALLING_CONVENTION, _, _)
=>
bug "unexpected TC_FIXED_ARROW in tc_umap";
hut::typ::EXTENSIBLE_TOKEN (k, t) => bug "unexpected token hut::Uniqtyp in tc_wmap";
hut::typ::BOXED _ => bug "unexpected TC_BOXED in tc_wmap";
hut::typ::ABSTRACT _ => bug "unexpected TC_ABSTRACT in tc_wmap";
_ => bug "unexpected other typs in tc_wmap";
esac;
#
fun tc_umap (u, w) t
=
case (hut::uniqtyp_to_typ t)
#
(hut::typ::DEBRUIJN_TYPEVAR _ | hut::typ::NAMED_TYPEVAR _ | hut::typ::BASETYPE _) => t;
hut::typ::TYPEFUN (ks, tc) => make_typefun_uniqtyp (ks, u tc); /* impossible case */
hut::typ::APPLY_TYPEFUN (tc, tcs) => make_apply_typefun_uniqtyp (u tc, map w tcs);
hut::typ::TYPESEQ tcs => make_typeseq_uniqtyp (map u tcs);
hut::typ::ITH_IN_TYPESEQ (tc, i) => make_ith_in_typeseq_uniqtyp (u tc, i);
hut::typ::SUM tcs => make_sum_uniqtyp (map u tcs);
#
hut::typ::RECURSIVE ((n, tc, ts), i)
=>
make_recursive_uniqtyp((n, hut::reduce_uniqtyp_to_normal_form (u tc), map w ts), i);
#
hut::typ::TUPLE (rk, tcs) => make_tuple_uniqtyp (map u tcs);
#
hut::typ::ARROW (hut::VARIABLE_CALLING_CONVENTION { arg_is_raw => b1, body_is_raw => b2 }, ts1, ts2)
=>
make_arrow_uniqtyp (fixed_calling_convention, map u ts1, map u ts2);
#
hut::typ::ARROW (hut::FIXED_CALLING_CONVENTION, _, _)
=>
bug "unexpected TC_FIXED_ARROW in tc_umap";
#
hut::typ::PARROW _ => bug "unexpected TC_PARROW in tc_umap";
hut::typ::BOXED _ => bug "unexpected TC_BOXED in tc_umap";
hut::typ::ABSTRACT _ => bug "unexpected TC_ABSTRACT in tc_umap";
#
hut::typ::EXTENSIBLE_TOKEN (k, t)
=>
if (hut::same_token (k, hut::wrap_token))
bug "unexpected TC_WRAP in tc_umap";
else
hut::typ_to_uniqtyp (hut::typ::EXTENSIBLE_TOKEN (k, u t));
fi;
_ => bug "unexpected other typs in tc_umap";
esac;
#
fun lt_umap (tcf, ltf) t
=
case (hut::uniqtype_to_type t)
#
hut::type::TYP tc => make_typ_uniqtype (tcf tc);
hut::type::PACKAGE ts => make_package_uniqtype (map ltf ts);
hut::type::GENERIC_PACKAGE (ts1, ts2) => make_generic_package_uniqtype (map ltf ts1, map ltf ts2);
hut::type::TYPEAGNOSTIC (ks, xs) => make_typeagnostic_uniqtype (ks, map ltf xs);
hut::type::FATE _ => bug "unexpected CNTs in lt_umap";
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected INDs in lt_umap";
hut::type::TYPE_CLOSURE _ => bug "unexpected ENVs in lt_umap";
esac;
my { tc_wmap=>tc_wrap, tc_umap=>tc_map, lt_umap=>lt_map, cleanup }
=
highcode_dictionary::wmemo_fn { tc_wmap, tc_umap, lt_umap };
#
fun lt_wrap x
=
if_uniqtype_is_typ (x, (fn tc = make_typ_uniqtype (tc_wrap tc)),
fn _ = bug "unexpected case in ltWrap");
( tc_wrap o hut::reduce_uniqtyp_to_normal_form,
lt_wrap o hut::reduce_uniqtype_to_normal_form,
tc_map o hut::reduce_uniqtyp_to_normal_form,
lt_map o hut::reduce_uniqtype_to_normal_form,
cleanup
);
};
#########################################################################
# SUBSTITION OF NAMED VARS IN A TYC/LTY
#########################################################################
package uniqtype_dictionary
=
binary_map_g (
#
Key = hut::Uniqtype;
compare = hut::compare_uniqtypes;
);
# Used (only) in src/lib/compiler/back/top/anormcode/anormcode-namedtypevar-vs-debruijntypevar-forms.pkg #
fun tc_named_typevar_elimination_thunk () # Evaluating the thunk allocates a new dictionary.
=
tc_named_typevar_elimination
where
dictionary = REF (uniqtyp_dictionary::empty);
#
fun tc_named_typevar_elimination s depth typ
=
case (hut::get_free_named_variables_in_uniqtyp typ)
#
[] => typ; # nothing to elim
#
_ =>
{ # Encode the typ and
# the depth for memoization
# using make_ith_in_typeseq_uniqtyp:
#
tycdepth = make_ith_in_typeseq_uniqtyp (typ, depth);
case (uniqtyp_dictionary::get (*dictionary, tycdepth))
#
THE t => t; # hit!
#
NULL => # must recompute
{
r = tc_named_typevar_elimination s depth; # Default recursive invoc.
rs = map r; # Recursive invocation on list.
t = case (hut::uniqtyp_to_typ typ)
#
hut::typ::DEBRUIJN_TYPEVAR _ => typ;
hut::typ::BASETYPE _ => typ;
#
hut::typ::TYPEFUN (tks, t) => make_typefun_uniqtyp (tks, tc_named_typevar_elimination s (di::next depth) t);
hut::typ::APPLY_TYPEFUN (t, ts) => make_apply_typefun_uniqtyp (r t, rs ts);
hut::typ::TYPESEQ ts => make_typeseq_uniqtyp (rs ts);
#
hut::typ::ITH_IN_TYPESEQ (t, i) => make_ith_in_typeseq_uniqtyp (r t, i);
hut::typ::SUM ts => make_sum_uniqtyp (rs ts);
#
hut::typ::TUPLE (rf, ts) => make_tuple_uniqtyp (rs ts);
hut::typ::ARROW (ff, ts, ts') => make_arrow_uniqtyp (ff, rs ts, rs ts');
hut::typ::PARROW (t, t') => make_lambdacode_arrow_uniqtyp (r t, r t');
#
hut::typ::BOXED t => make_boxed_uniqtyp (r t);
hut::typ::ABSTRACT t => make_abstract_uniqtyp (r t);
hut::typ::FATE ts => make_uniqtyp_fate (rs ts);
#
hut::typ::RECURSIVE ((i, t, ts), j)
=>
make_recursive_uniqtyp ((i, r t, rs ts), j);
hut::typ::NAMED_TYPEVAR tvar
=>
case (s (tvar, depth))
#
THE t => t;
NULL => typ;
esac;
hut::typ::EXTENSIBLE_TOKEN (tok, t)
=>
hut::typ_to_uniqtyp (hut::typ::EXTENSIBLE_TOKEN (tok, r t));
hut::typ::INDIRECT_TYPE_THUNK _ => bug "unexpected TC_INDIRECT in tc_named_typevar_elimination";
hut::typ::TYPE_CLOSURE _ => bug "unexpected TC_CLOSURE in tc_named_typevar_elimination";
esac;
dictionary := uniqtyp_dictionary::set (*dictionary, tycdepth, t);
t;
};
esac;
};
esac; # tc_named_typevar_elimination
end;
# Used (only) in src/lib/compiler/back/top/anormcode/anormcode-namedtypevar-vs-debruijntypevar-forms.pkg #
fun lt_named_typevar_elimination_thunk () # Evaluating the thunk allocates a new dictionary.
=
lt_named_typevar_elimination
where
dictionary = REF (uniqtype_dictionary::empty);
tc_named_typevar_elimination = tc_named_typevar_elimination_thunk(); # Evaluating the thunk allocates a new dictionary.
#
fun lt_named_typevar_elimination s depth lambda_type
=
case (hut::get_free_named_variables_in_uniqtype lambda_type)
#
[] => lambda_type; # nothing to elim
#
_ => {
# Encode the hut::Uniqtype and depth info
# using TYPE_CLOSURE
# (only first 2 args are useful)
#
ltydepth
=
hut::type_to_uniqtype
(
hut::type::TYPE_CLOSURE (lambda_type, depth, 0, hut::empty_uniqtyp_dictionary)
);
case (uniqtype_dictionary::get (*dictionary, ltydepth))
#
THE t => t; # Hit.
#
NULL => # Must recompute.
t
where
r = lt_named_typevar_elimination s depth; # Default recursive invoc.
rs = map r; # recursive invocation on list
t = case (hut::uniqtype_to_type lambda_type)
#
hut::type::TYP t => make_typ_uniqtype (tc_named_typevar_elimination s depth t);
hut::type::PACKAGE ts => make_package_uniqtype (rs ts);
#
hut::type::GENERIC_PACKAGE (ts, ts') => make_generic_package_uniqtype (rs ts, rs ts');
hut::type::TYPEAGNOSTIC (tks, ts) => make_typeagnostic_uniqtype (tks, map (lt_named_typevar_elimination s (di::next depth)) ts);
hut::type::FATE ts => make_uniqtype_fate (rs ts);
#
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected INDIRECT_TYPE_THUNK in lt_named_typevar_elimination";
hut::type::TYPE_CLOSURE _ => bug "unexpected TYPE_CLOSURE in lt_named_typevar_elimination";
esac;
dictionary := uniqtype_dictionary::set (*dictionary, ltydepth, t);
end;
esac;
};
esac; # fun lt_named_typevar_elimination
end; # fun lt_named_typevar_elimination_thunk
############################################################
Smap = List ((tmp::Codetemp, hut::Uniqtyp));
# Is the intersection of two
# sorted lists non-NIL?
#
fun intersection_non_empty (NIL, _: List( tmp::Codetemp ))
=>
FALSE;
intersection_non_empty(_, NIL)
=>
FALSE;
intersection_non_empty (s1 as (h1: tmp::Codetemp, _) ! t1, s2 as h2 ! t2)
=>
case (int::compare (h1, h2))
#
LESS => intersection_non_empty (t1, s2);
GREATER => intersection_non_empty (s1, t2);
EQUAL => TRUE;
esac;
end;
#
fun search_subst (tv: tmp::Codetemp, s)
=
h s
where
fun h []
=>
NULL;
h ((tv': tmp::Codetemp, typ) ! s)
=>
case (int::compare (tv, tv'))
#
LESS => NULL;
GREATER => h s;
EQUAL => THE typ;
esac;
end;
end;
#
fun tc_nvar_subst_fn ()
=
tc_nvar_subst
where
dictionary = REF (uniqtyp_dictionary::empty);
#
fun tc_nvar_subst subst
=
loop
where
fun loop typ
=
# Check if substitution overlaps
# with free vars list:
#
case (intersection_non_empty (subst, hut::get_free_named_variables_in_uniqtyp typ))
#
FALSE => typ; # nothing to subst
#
TRUE =>
# Next check the memoization table:
#
case (uniqtyp_dictionary::get (*dictionary, typ))
#
THE t => t; # Hit.
#
NULL => # Must recompute.
t
where
t = case (hut::uniqtyp_to_typ typ)
#
hut::typ::NAMED_TYPEVAR tv
=>
case (search_subst (tv, subst))
THE t => t;
NULL => typ;
esac;
#
hut::typ::DEBRUIJN_TYPEVAR _ => typ;
hut::typ::BASETYPE _ => typ;
#
hut::typ::TYPEFUN (tks, t) => make_typefun_uniqtyp (tks, loop t);
hut::typ::APPLY_TYPEFUN (t, ts) => make_apply_typefun_uniqtyp (loop t, map loop ts);
#
hut::typ::TYPESEQ ts => make_typeseq_uniqtyp (map loop ts);
hut::typ::ITH_IN_TYPESEQ (t, i) => make_ith_in_typeseq_uniqtyp (loop t, i);
hut::typ::SUM ts => make_sum_uniqtyp (map loop ts);
#
hut::typ::RECURSIVE ((i, t, ts), j)
=>
make_recursive_uniqtyp ((i, loop t, map loop ts), j);
#
hut::typ::TUPLE (rf, ts) => make_tuple_uniqtyp (map loop ts);
hut::typ::ARROW (ff, ts, ts') => make_arrow_uniqtyp (ff, map loop ts, map loop ts');
hut::typ::PARROW (t, t') => make_lambdacode_arrow_uniqtyp (loop t, loop t');
#
hut::typ::BOXED t => make_boxed_uniqtyp (loop t);
hut::typ::ABSTRACT t => make_abstract_uniqtyp (loop t);
hut::typ::FATE ts => make_uniqtyp_fate (map loop ts);
hut::typ::EXTENSIBLE_TOKEN (tok, t)
=>
hut::typ_to_uniqtyp (hut::typ::EXTENSIBLE_TOKEN (tok, loop t));
hut::typ::INDIRECT_TYPE_THUNK _ => bug "unexpected TC_INDIRECT in substTypeConstructor";
hut::typ::TYPE_CLOSURE _ => bug "unexpected TC_CLOSURE in substTypeConstructor";
esac;
# Update memoization table:
#
dictionary := uniqtyp_dictionary::set (*dictionary, typ, t);
end;
esac;
esac;
end; # fun tc_nvar_subst
end; # fun tc_nvar_subst_fn
#
fun lt_nvar_subst_fn ()
=
lt_nvar_subst
where
dictionary = REF (uniqtype_dictionary::empty);
tc_nvar_subst' = tc_nvar_subst_fn();
#
fun lt_nvar_subst subst
=
loop
where
tc_nvar_subst = tc_nvar_subst' subst;
#
fun loop lambda_type
=
# First check if there are
# any free type variables:
#
case (intersection_non_empty (subst, hut::get_free_named_variables_in_uniqtype lambda_type))
#
FALSE => lambda_type; # nothing to subst
#
TRUE =>
# Next, check the memoization table:
#
case (uniqtype_dictionary::get (*dictionary, lambda_type))
#
THE t => t; # A hit!
#
NULL => # Must recompute>
t
where
t = case (hut::uniqtype_to_type lambda_type)
#
hut::type::TYP t => make_typ_uniqtype (tc_nvar_subst t);
#
hut::type::PACKAGE ts => make_package_uniqtype (map loop ts);
hut::type::GENERIC_PACKAGE (ts, ts') => make_generic_package_uniqtype (map loop ts, map loop ts');
#
hut::type::TYPEAGNOSTIC (tks, ts) => make_typeagnostic_uniqtype (tks, map loop ts);
hut::type::FATE ts => make_uniqtype_fate (map loop ts);
#
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected INDIRECT_TYPE_THUNK in lt_named_typevar_elimination";
hut::type::TYPE_CLOSURE _ => bug "unexpected TYPE_CLOSURE in lt_named_typevar_elimination";
esac;
# Update memoization table:
#
dictionary := uniqtype_dictionary::set (*dictionary, lambda_type, t);
end;
esac;
esac;
end; # fun lt_nvar_subst
end; # fun lt_nvar_subst_fn
############################################################
# Building up a typeagnostic type by abstracting over a
# list of named vars
Tvoffs = List ((tmp::Codetemp, Int));
#
fun intersect (NIL, _: List( tmp::Codetemp ))
=>
NIL;
intersect(_, NIL)
=>
NIL;
intersect (s1 as (h1: tmp::Codetemp, n) ! t1, s2 as h2 ! t2)
=>
case (int::compare (h1, h2))
#
LESS => intersect (t1, s2);
GREATER => intersect (s1, t2);
EQUAL => (h1, n) ! intersect (t1, t2);
esac;
end;
# s_iter = compile_statistics::makeStat "Cvt Iterations"
# s_hits = compile_statistics::makeStat "Cvt Hits in dictionary"
# s_cuts = compile_statistics::makeStat "Cvt Freevar cutoffs"
# s_tvoffs = compile_statistics::makeStat "Cvt tvoffs length"
# s_nvars = compile_statistics::makeStat "Cvt free nvars length"
#
fun tc_nvar_cvt_fn ()
=
tc_nvar_cvt
where
dictionary = REF (uniqtyp_dictionary::empty);
#
fun tc_nvar_cvt (tvoffs: Tvoffs) d typ
=
# Compile_statistics::addStat s_iter 1;
# Compile_statistics::addStat s_tvoffs (length tvoffs);
# Compile_statistics::addStat s_nvars (length (hut::freeNamedVariablesInTypeConstructor typ));
# Check if substitution overlaps with free vars list
#
case (intersect (tvoffs, hut::get_free_named_variables_in_uniqtyp typ))
#
[] => (# Compile_statistics::addStat s_cuts 1;
typ # nothing to convert
);
tvoffs
=>
{
# Encode the typ
# and the depth for memoization
# using make_ith_in_typeseq_uniqtyp:
#
tycdepth = make_ith_in_typeseq_uniqtyp (typ, d);
case (uniqtyp_dictionary::get (*dictionary, tycdepth))
#
THE t => (# Compile_statistics::addStat s_hits 1;
t # Hit.
);
#
NULL => # Must recompute.
t
where
r = tc_nvar_cvt tvoffs d; # Default recursive invoc.
rs = map r; # recursive invocation on list
t = case (hut::uniqtyp_to_typ typ)
#
hut::typ::NAMED_TYPEVAR tvar
=>
case (search_subst (tvar, tvoffs))
#
THE i => make_debruijn_typevar_uniqtyp (d, i);
NULL => typ;
esac;
#
hut::typ::DEBRUIJN_TYPEVAR _ => typ;
hut::typ::BASETYPE _ => typ;
hut::typ::TYPEFUN (tks, t) => make_typefun_uniqtyp (tks, tc_nvar_cvt tvoffs (di::next d) t);
#
hut::typ::APPLY_TYPEFUN (t, ts) => make_apply_typefun_uniqtyp (r t, rs ts);
hut::typ::TYPESEQ ts => make_typeseq_uniqtyp (rs ts);
hut::typ::ITH_IN_TYPESEQ (t, i) => make_ith_in_typeseq_uniqtyp (r t, i);
hut::typ::SUM ts => make_sum_uniqtyp (rs ts);
hut::typ::RECURSIVE ((i, t, ts), j) => make_recursive_uniqtyp ((i, r t, rs ts), j);
hut::typ::TUPLE (rf, ts) => make_tuple_uniqtyp (rs ts);
hut::typ::ARROW (ff, ts, ts') => make_arrow_uniqtyp (ff, rs ts, rs ts');
hut::typ::PARROW (t, t') => make_lambdacode_arrow_uniqtyp (r t, r t');
hut::typ::BOXED t => make_boxed_uniqtyp (r t);
hut::typ::ABSTRACT t => make_abstract_uniqtyp (r t);
hut::typ::EXTENSIBLE_TOKEN (tok, t) => hut::typ_to_uniqtyp (hut::typ::EXTENSIBLE_TOKEN (tok, r t));
hut::typ::FATE ts => make_uniqtyp_fate (rs ts);
hut::typ::INDIRECT_TYPE_THUNK _ => bug "unexpected TC_INDIRECT in tc_nvar_cvt";
hut::typ::TYPE_CLOSURE _ => bug "unexpected TC_CLOSURE in tc_nvar_cvt";
esac;
dictionary := uniqtyp_dictionary::set (*dictionary, tycdepth, t);
end;
esac;
};
esac; # fun tc_nvar_cvt
end; # fun tc_nvar_cvt_fn
#
fun lt_nvar_cvt_fn ()
=
lt_nvar_cvt
where
dictionary = REF (uniqtype_dictionary::empty);
tc_nvar_cvt = tc_nvar_cvt_fn();
#
fun lt_nvar_cvt tvoffs d lambda_type
=
# Check if substitution overlaps
# with free vars list:
#
case (intersect (tvoffs, hut::get_free_named_variables_in_uniqtype lambda_type))
#
[] => lambda_type; # nothing to convert
#
tvoffs => {
# encode the lambdaType and depth info using TYPE_CLOSURE
# (only first 2 args are useful)
ltydepth = hut::type_to_uniqtype (hut::type::TYPE_CLOSURE (lambda_type, d, 0, hut::empty_uniqtyp_dictionary));
case (uniqtype_dictionary::get (*dictionary, ltydepth))
#
THE t => t; # hit!
#
NULL => # must recompute
t
where
r = lt_nvar_cvt tvoffs d; # Default recursive invoc.
rs = map r; # Recursive invocation on list.
t = case (hut::uniqtype_to_type lambda_type)
#
hut::type::TYP t
=>
make_typ_uniqtype (tc_nvar_cvt tvoffs d t);
#
hut::type::PACKAGE ts => make_package_uniqtype (rs ts);
hut::type::GENERIC_PACKAGE (ts, ts') => make_generic_package_uniqtype (rs ts, rs ts');
#
hut::type::TYPEAGNOSTIC (tks, ts)
=>
make_typeagnostic_uniqtype (tks,
map (lt_nvar_cvt tvoffs (di::next d)) ts);
#
hut::type::FATE ts
=>
make_uniqtype_fate (rs ts);
#
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected INDIRECT_TYPE_THUNK in lt_nvar_cvt";
hut::type::TYPE_CLOSURE _ => bug "unexpected TYPE_CLOSURE in lt_nvar_cvt";
esac;
dictionary := uniqtype_dictionary::set (*dictionary, ltydepth, t);
end;
esac;
};
esac; # fun lt_nvar_cvt
end; # fun lt_nvar_cvt_fn
# Make a type abstraction
# from nvar to lambda type:
#
fun lt_nvpoly (tvks, lt)
=
{ fun frob ((tv, k) ! tvks, n, ks, tvoffs)
=>
frob (tvks, n+1, k ! ks, (tv, n) ! tvoffs);
frob ([], _, ks, tvoffs)
=>
(reverse ks, reverse tvoffs);
end;
my (ks, tvoffs)
=
frob (tvks, 0, [], []);
#
fun cmp ((tvar1, _), (tvar2, _))
=
tvar1 > tvar2;
tvoffs = lms::sort_list cmp tvoffs;
# Temporarily gen()
#
lt_subst = lt_nvar_cvt_fn() tvoffs (di::next di::top);
make_typeagnostic_uniqtype (ks, map lt_subst lt);
};
}; # package highcode
end; # top-level stipulate