## 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 pp = standard_prettyprinter; # standard_prettyprinter is from src/lib/prettyprint/big/src/standard-prettyprinter.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);
Pp = pp::Pp;
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 (\\ 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 ) => "argRaw/bodyRaw"; # "r"=="raw", "c"=="cooked".
callnotes_to_string' (TRUE, FALSE) => "argRaw/bodyCooked";
callnotes_to_string' (FALSE, TRUE ) => "argCooked/bodyRaw";
callnotes_to_string' (FALSE, FALSE) => "argCooked/bodyCooked";
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 package 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_typefun_uniqkind 0 => plaintype_uniqkind;
make_n_arg_typefun_uniqkind 1 => one___arg_fn;
make_n_arg_typefun_uniqkind 2 => two___arg_fn;
make_n_arg_typefun_uniqkind 3 => three_arg_fn;
make_n_arg_typefun_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 uniqtypes:
#
int_uniqtype = make_basetype_uniqtype hbt::basetype_tagged_int;
int1_uniqtype = make_basetype_uniqtype hbt::basetype_int1;
float64_uniqtype = make_basetype_uniqtype hbt::basetype_float64;
string_uniqtype = make_basetype_uniqtype hbt::basetype_string;
exception_uniqtype = make_basetype_uniqtype hbt::basetype_exception;
truevoid_uniqtype = make_basetype_uniqtype hbt::basetype_truevoid;
#
void_uniqtype = make_tuple_uniqtype [];
#
bool_uniqtype
=
{ tbool = make_sum_uniqtype [void_uniqtype, void_uniqtype];
tsig_bool = make_typefun_uniqtype ([plaintype_uniqkind], tbool);
make_recursive_uniqtype((1, tsig_bool, []), 0);
};
#
list_uniqtype # Not exported -- used for printing.
=
{ alpha = make_debruijn_typevar_uniqtype (di::innermost, 0);
tlist = make_debruijn_typevar_uniqtype (di::innersnd, 0);
alist = make_apply_typefun_uniqtype (tlist, [alpha]);
tcc_cons = make_tuple_uniqtype [alpha, alist];
tlist = make_typefun_uniqtype([plaintype_uniqkind], make_sum_uniqtype [tcc_cons, void_uniqtype]);
# The order here should be consistent with that in
# src/lib/compiler/front/typer/types/more-type-types.pkg tsig_list = make_typefun_uniqtype([make_n_arg_typefun_uniqkind 1], tlist);
make_recursive_uniqtype((1, tsig_list, []), 0);
};
#
fun make_typevar_i_uniqtype i = make_debruijn_typevar_uniqtype (di::innermost, i);
#
fun make_ref_uniqtype x = make_apply_typefun_uniqtype (make_basetype_uniqtype hbt::basetype_ref, [x]);
fun make_rw_vector_uniqtype x = make_apply_typefun_uniqtype (make_basetype_uniqtype hbt::basetype_rw_vector, [x]);
fun make_ro_vector_uniqtype x = make_apply_typefun_uniqtype (make_basetype_uniqtype hbt::basetype_vector, [x]);
fun make_exception_tag_uniqtype x = make_apply_typefun_uniqtype (make_basetype_uniqtype hbt::basetype_exception_tag, [x]);
# Prebuilt basetype uniqtypoids:
#
int_uniqtypoid = make_type_uniqtypoid int_uniqtype;
int1_uniqtypoid = make_type_uniqtypoid int1_uniqtype;
float64_uniqtypoid = make_type_uniqtypoid float64_uniqtype;
string_uniqtypoid = make_type_uniqtypoid string_uniqtype;
exception_uniqtypoid = make_type_uniqtypoid exception_uniqtype;
truevoid_uniqtypoid = make_type_uniqtypoid truevoid_uniqtype;
void_uniqtypoid = make_type_uniqtypoid void_uniqtype;
bool_uniqtypoid = make_type_uniqtypoid bool_uniqtype;
# Uniqtypoid constructors:
#
make_typevar_i_uniqtypoid = make_type_uniqtypoid o make_typevar_i_uniqtype;
make_ref_uniqtypoid = make_type_uniqtypoid o make_ref_uniqtype o unpack_type_uniqtypoid;
make_rw_vector_uniqtypoid = make_type_uniqtypoid o make_rw_vector_uniqtype o unpack_type_uniqtypoid;
make_ro_vector_uniqtypoid = make_type_uniqtypoid o make_ro_vector_uniqtype o unpack_type_uniqtypoid;
make_exception_tag_uniqtypoid = make_type_uniqtypoid o make_exception_tag_uniqtype o unpack_type_uniqtypoid;
############################################################################
# UTILITY FUNCTIONS FOR TESTING EQUIVALENCE
############################################################################
# Testing equivalence of tkinds,
# types, ltys, fflags, and rflags:
#
my same_uniqkind: (hut::Uniqkind, hut::Uniqkind) -> Bool = hut::same_uniqkind;
my same_uniqtype: (hut::Uniqtype, hut::Uniqtype) -> Bool = hut::same_uniqtype;
my same_uniqtypoid: (hut::Uniqtypoid, hut::Uniqtypoid) -> Bool = hut::same_uniqtypoid;
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 types and
# ltys with relaxed constraints:
#
my similar_uniqtypes: (hut::Uniqtype, hut::Uniqtype) -> Bool = hut::similar_uniqtypes;
my similar_uniqtypoids: (hut::Uniqtypoid, hut::Uniqtypoid) -> Bool = hut::similar_uniqtypoids;
############################################################################
# UTILITY FUNCTIONS FOR PRETTY PRINTING
############################################################################
# Prettyprinting of tkinds, types, 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 uniqtype_to_string (x: hut::Uniqtype)
=
g (hut::uniqtype_to_type x)
where
fun g (hut::type::DEBRUIJN_TYPEVAR (i, j)) => "DEBRUIJN_TYPEVAR(" + (di::di_print i) + ", " + (int::to_string j) + ")";
g (hut::type::NAMED_TYPEVAR v) => "NAMED_TYPEVAR (v" + (int::to_string v) + ")";
g (hut::type::BASETYPE pt)
=>
hbt::basetype_to_string pt;
g (hut::type::TYPEFUN (ks, t))
=>
"(\\[" + plist (uniqkind_to_string, ks) + "]." + (uniqtype_to_string t) + ")";
g (hut::type::APPLY_TYPEFUN (t, [])) => uniqtype_to_string t + "[]";
g (hut::type::APPLY_TYPEFUN (t, zs)) => (uniqtype_to_string t) + "[" + (plist (uniqtype_to_string, zs)) + "]";
g (hut::type::TYPESEQ zs) => "TYPESEQ(" + (plist (uniqtype_to_string, zs)) + ")";
g (hut::type::ITH_IN_TYPESEQ (t, i)) => "ITH_IN_TYPESEQ(" + (uniqtype_to_string t) + ", " + (int::to_string i) + ")";
g (hut::type::SUM tcs) => "SUM(" + (plist (uniqtype_to_string, tcs)) + ")";
g (hut::type::RECURSIVE ((_, tc, ts), i))
=>
if (same_uniqtype (x, bool_uniqtype)) "BOOL";
elif (same_uniqtype (x, list_uniqtype)) "LIST";
else
# ntc = case ts
# [] => tc;
# _ => make_apply_typefun_uniqtype (tc, ts);
# esac;
"DATA { " + "DATA" +
# "[" +
# (uniqtype_to_string tc) +
# "] &&" +
# (plist (uniqtype_to_string, ts)) +
# "&&"
"====" +
(int::to_string i) +
"}";
fi;
g (hut::type::ABSTRACT t) => "ABSTRACT(" + (uniqtype_to_string t) + ")";
g (hut::type::BOXED t) => "BOXED(" + (uniqtype_to_string t) + ")";
g (hut::type::TUPLE(_, zs)) => "TUPLE<" + (plist (uniqtype_to_string, zs)) + ">";
g (hut::type::ARROW (ff, z1, z2)) => parw (\\ u = plist (uniqtype_to_string, u), (ff, z1, z2));
g (hut::type::PARROW _) => bug "unexpected TC_PARROW in uniqtype_to_string";
g (hut::type::EXTENSIBLE_TOKEN (k, t))
=>
if (hut::token_is_valid k) (hut::token_abbreviation k) + "(" + (uniqtype_to_string t) + ")";
else bug "unexpected TC_EXTENSIBLE_TOKEN type in uniqtype_to_string";
fi;
g (hut::type::FATE ts)
=>
"Count(" + (plist (uniqtype_to_string, ts)) + ")";
g (hut::type::INDIRECT_TYPE_THUNK _) => bug "unexpected TC_INDIRECT in uniqtype_to_string";
g (hut::type::TYPE_CLOSURE _) => bug "unexpected TC_CLOSURE in uniqtype_to_string";
end;
end; # fun uniqtype_to_string
#
fun uniqtypoid_to_string (x: hut::Uniqtypoid)
=
g (hut::uniqtypoid_to_typoid x)
where
fun h (i, t)
=
"(" + (int::to_string i) + ", " + (uniqtypoid_to_string t) + ")";
#
fun g (hut::typoid::TYPE t) => uniqtype_to_string t;
g (hut::typoid::PACKAGE zs) => "PACKAGE { " + (plist (uniqtypoid_to_string, zs)) + "}";
g (hut::typoid::GENERIC_PACKAGE (ts1, ts2))
=>
"(" + (plist (uniqtypoid_to_string, ts1)) + ") ==> ("
+ (plist (uniqtypoid_to_string, ts2)) + ")";
g (hut::typoid::TYPEAGNOSTIC (ks, ts))
=>
"(TYPEAGNOSTIC[" + plist (uniqkind_to_string, ks) + "]."
+ (plist (uniqtypoid_to_string, ts)) + ")";
g (hut::typoid::FATE ts)
=>
"FATE(" + (plist (uniqtypoid_to_string, ts)) + ")";
g (hut::typoid::INDIRECT_TYPE_THUNK _) => bug "unexpected INDIRECT_TYPE_THUNK in uniqtypoid_to_string";
g (hut::typoid::TYPE_CLOSURE _) => bug "unexpected TYPE_CLOSURE in uniqtypoid_to_string";
end;
end; # fun uniqtypoid_to_string
fun prettyprint_uniqkind (pp:Pp) (x: hut::Uniqkind)
=
g (hut::uniqkind_to_kind x)
where
fun g hut::kind::PLAINTYPE => pp.lit "hut::kind::PLAINTYPE";
g hut::kind::BOXEDTYPE => pp.lit "hut::kind::BOXEDTYPE";
g (hut::kind::KINDFUN (ks, k))
=>
pp.box' 0 0 {.
pp.lit "hut::kind::KINDFUN (";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqkind pp) ks;
pp.ind 0;
pp.cut ();
pp.lit "->";
pp.ind 4;
pp.txt " ";
prettyprint_uniqkind pp k;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::kind::KINDSEQ zs)
=>
pp.box' 0 0 {.
pp.lit "hut::kind::KINDSEQ (";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqkind pp) zs;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
end;
end;
#
fun prettyprint_uniqtype (pp:Pp) (x: hut::Uniqtype)
=
g (hut::uniqtype_to_type x)
where
fun g (hut::type::DEBRUIJN_TYPEVAR (i, j))
=>
pp.lit ("hut::type::DEBRUIJN_TYPEVAR(" + (di::di_print i) + ", " + (int::to_string j) + ")");
g (hut::type::NAMED_TYPEVAR v)
=>
pp.lit ("hut::type::NAMED_TYPEVAR (v" + (int::to_string v) + ")");
g (hut::type::BASETYPE pt)
=>
pp.lit ("hut::type::BASETYPE " + (hbt::basetype_to_string pt));
g (hut::type::TYPEFUN (ks, t))
=>
pp.box' 0 0 {.
pp.lit "hut::type::TYPEFUN (";
pp.ind 4;
pp.txt " ";
pp.box' 0 2 {.
pp.lit "kinds => [";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqkind pp) ks;
pp.ind 0;
pp.txt " ";
pp.lit "]";
};
pp.endlit ",";
pp.txt " ";
pp.box' 0 2 {.
pp.lit "type =>";
pp.ind 4;
pp.txt " ";
prettyprint_uniqtype pp t;
pp.ind 0;
pp.txt " ";
pp.lit "]";
};
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::APPLY_TYPEFUN (t, []))
=>
pp.box' 0 0 {.
pp.lit "hut::type::APPLY_TYPEFUN (";
pp.ind 4;
pp.txt " ";
pp.lit "t =>";
pp.txt " ";
prettyprint_uniqtype pp t;
pp.txt " ";
pp.lit "[]";
pp.txt " ";
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::APPLY_TYPEFUN (t, zs))
=>
pp.box' 0 0 {.
pp.lit "hut::type::APPLY_TYPEFUN (";
pp.ind 4;
pp.txt " ";
pp.box' 0 -1 {.
pp.lit "t =>";
pp.ind 4;
pp.txt " ";
prettyprint_uniqtype pp t;
};
pp.endlit ",";
pp.txt " ";
pp.box' 0 2 {.
pp.lit "zs => [";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtype pp) zs;
pp.ind 0;
pp.txt " ";
pp.lit "]";
};
pp.txt " ";
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::TYPESEQ zs)
=>
pp.box' 0 0 {.
pp.lit "hut::type::TYPESEQ(";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtype pp) zs;
pp.txt " ";
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::ITH_IN_TYPESEQ (t, i))
=>
pp.box' 0 0 {.
pp.lit "hut::type::ITH_IN_TYPESEQ(";
pp.ind 4;
pp.txt " ";
prettyprint_uniqtype pp t;
pp.endlit ",";
pp.txt " ";
pp.lit (int::to_string i);
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::SUM tcs)
=>
pp.box' 0 0 {.
pp.lit "hut::type::SUM(";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtype pp) tcs;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::RECURSIVE ((_, tc, ts), i))
=>
if (same_uniqtype (x, bool_uniqtype)) pp.lit "BOOL";
elif (same_uniqtype (x, list_uniqtype)) pp.lit "LIST";
else
# ntc = case ts
# [] => tc;
# _ => make_apply_typefun_uniqtype (tc, ts);
# esac;
pp.box' 0 0 {.
pp.lit "DATA {";
pp.ind 4;
pp.txt " ";
pp.lit "DATA";
pp.box' 0 0 {.
pp.lit "[";
pp.ind 4;
pp.txt " ";
prettyprint_uniqtype pp tc;
pp.txt " ";
pp.ind 0;
pp.txt " ";
pp.lit "]";
};
pp.ind 0;
pp.cut ();
pp.lit "&&";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtype pp) ts;
pp.ind 0;
pp.cut ();
pp.lit "&&";
pp.ind 4;
pp.txt " ";
pp.lit "====";
pp.lit (int::to_string i);
pp.ind 0;
pp.txt " ";
pp.lit "}";
};
fi;
g (hut::type::ABSTRACT t)
=>
pp.box' 0 0 {.
pp.lit "hut::type::ABSTRACT(";
pp.ind 4;
pp.txt " ";
prettyprint_uniqtype pp t;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::BOXED t)
=>
pp.box' 0 0 {.
pp.lit "hut::type::BOXED(";
pp.ind 4;
pp.txt " ";
prettyprint_uniqtype pp t;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::TUPLE(_, zs))
=>
pp.box' 0 0 {.
pp.lit "hut::type::TUPLE(";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtype pp) zs;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::ARROW (ff, z1, z2))
=>
pp.box' 0 0 {.
pp.lit "hut::type::ARROW(";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtype pp) z1;
pp.txt " ";
pp.lit (callnotes_to_string ff);
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtype pp) z2;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::PARROW _) => bug "unexpected TC_PARROW in uniqtype_to_string";
g (hut::type::EXTENSIBLE_TOKEN (k, t))
=>
if (hut::token_is_valid k)
pp.box' 0 0 {.
pp.lit "hut::type::EXTENSIBLE_TOKEN(";
pp.ind 4;
pp.txt " ";
pp.lit (hut::token_abbreviation k);
pp.box' 0 2 {.
pp.lit "(";
pp.ind 4;
pp.txt " ";
prettyprint_uniqtype pp t;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
pp.ind 0;
pp.cut ();
pp.lit ")";
};
else
bug "unexpected TC_EXTENSIBLE_TOKEN type in uniqtype_to_string";
fi;
g (hut::type::FATE ts)
=>
pp.box' 0 0 {.
pp.lit "hut::type::FATE(";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtype pp) ts;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::type::INDIRECT_TYPE_THUNK _) => bug "unexpected TC_INDIRECT in uniqtype_to_string";
g (hut::type::TYPE_CLOSURE _) => bug "unexpected TC_CLOSURE in uniqtype_to_string";
end;
end; # fun prettyprint_uniqtype
fun prettyprint_uniqtypoid (pp:Pp) (x: hut::Uniqtypoid)
=
g (hut::uniqtypoid_to_typoid x)
where
fun h (i, t)
=
pp.box' 0 0 {.
pp.lit "(";
pp.ind 4;
pp.lit (int::to_string i);
pp.endlit ",";
pp.txt " ";
prettyprint_uniqtypoid pp t;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
#
fun g (hut::typoid::TYPE t)
=>
{
prettyprint_uniqtype pp t;
};
g (hut::typoid::PACKAGE zs)
=>
pp.box' 0 0 {.
pp.lit "PACKAGE {";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtypoid pp) zs;
pp.ind 0;
pp.txt " ";
pp.lit "}";
};
g (hut::typoid::GENERIC_PACKAGE (ts1, ts2))
=>
pp.box' 0 0 {.
pp.lit "GENERIC_PACKAGE (";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtypoid pp) ts1;
pp.ind 0;
pp.cut ();
pp.lit ") ==> (";
pp.ind 4;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtypoid pp) ts2;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::typoid::TYPEAGNOSTIC (ks, ts))
=>
pp.box' 0 0 {.
pp.lit "TYPEAGNOSTIC(";
pp.ind 2;
pp.txt " ";
pp.box' 1 0 {.
pp.lit "kinds =>";
pp.txt " ";
pp.box' 1 2 {.
pp.lit "[";
pp.ind 2;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqkind pp) ks;
pp.ind 0;
pp.txt " ";
pp.lit "]";
};
};
pp.endlit ",";
pp.txt " ";
pp.box' 1 0 {.
pp.lit "typoids =>";
pp.txt " ";
pp.box' 1 2 {.
pp.lit "[";
pp.ind 2;
pp.txt " ";
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtypoid pp) ts;
pp.ind 0;
pp.txt " ";
pp.lit "]";
};
};
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::typoid::FATE ts)
=>
pp.box' 0 0 {.
pp.lit "FATE(";
pp.ind 4;
pp::seqx {. pp.txt ", "; } (prettyprint_uniqtypoid pp) ts;
pp.ind 0;
pp.cut ();
pp.lit ")";
};
g (hut::typoid::INDIRECT_TYPE_THUNK _) => bug "unexpected INDIRECT_TYPE_THUNK in prettyprint_uniqtypoid";
g (hut::typoid::TYPE_CLOSURE _) => bug "unexpected TYPE_CLOSURE in prettyprint_uniqtypoid";
end;
end; # fun prettyprint_uniqtypoid
# Finding out the depth for a type's
# innermost-bound free variables
#
my max_freevar_depth_in_uniqtype: ( hut::Uniqtype, di::Debruijn_Depth) -> di::Debruijn_Depth = hut::max_freevar_depth_in_uniqtype;
my max_freevar_depth_in_uniqtypes: (List( hut::Uniqtype ), di::Debruijn_Depth) -> di::Debruijn_Depth = hut::max_freevar_depth_in_uniqtypes;
# Adjusting an hut::Uniqtypoid or hut::Uniqtype
# from one depth to another
#
fun change_depth_of_uniqtypoid (lt, d, nd)
=
if (d == nd) lt;
else hut::make_type_closure_uniqtypoid (lt, 0, nd - d, hut::empty_uniqtype_dictionary);
fi;
#
fun change_depth_of_uniqtype (tc, d, nd)
=
if (d == nd) tc;
else hut::make_type_closure_uniqtype (tc, 0, nd - d, hut::empty_uniqtype_dictionary);
fi;
stipulate
fun make_type_dictionary (i, k, dd, e)
=
if (i >= k) e;
else make_type_dictionary (i+1, k, dd, hut::cons_entry_onto_uniqtype_dictionary (e, (NULL, dd+i)));
fi;
herein
#
fun change_k_depth_of_uniqtypoid (lt, d, nd, k)
=
if (d == nd) lt;
else hut::make_type_closure_uniqtypoid (lt, k, nd-d+k, make_type_dictionary (0, k, nd-d, hut::empty_uniqtype_dictionary));
fi;
#
fun change_k_depth_of_uniqtype (tc, d, nd, k)
=
if (d == nd) tc;
else hut::make_type_closure_uniqtype (tc, k, nd-d+k, make_type_dictionary (0, k, nd-d, hut::empty_uniqtype_dictionary));
fi;
end;
############################################################################
# UTILITY FUNCTIONS ON LTY DICTIONARY
############################################################################
# Utility values and functions on lty_env
#
Highcode_Variable_To_Uniqtypoid_Map
=
int_red_black_map::Map( (hut::Uniqtypoid, di::Debruijn_Depth) );
exception HIGHCODE_VARIABLE_NOT_FOUND;
empty_highcode_variable_to_uniqtypoid_map
=
int_red_black_map::empty
:
Highcode_Variable_To_Uniqtypoid_Map;
#
fun get_uniqtypoid_for_var (venv, lv, nd)
=
case (int_red_black_map::get (venv, lv))
#
THE (lt, d)
=>
if (d == nd) lt;
elif (d > nd) bug "unexpected depth info in ltLookup";
else hut::make_type_closure_uniqtypoid (lt, 0, nd - d, hut::empty_uniqtype_dictionary);
fi;
NULL => { say "**** hmmm, I didn't find the variable ";
say (int::to_string lv); say "\n";
raise exception HIGHCODE_VARIABLE_NOT_FOUND;
};
esac;
#
fun set_uniqtypoid_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::Uniqtypoid, # typefun
ts: List( hut::Uniqtype ) # arglist for typefun.
)
=
{ nt = hut::reduce_uniqtypoid_to_weak_head_normal_form lt;
case (/* lt_outX */ hut::uniqtypoid_to_typoid nt, ts)
(hut::typoid::TYPEAGNOSTIC (ks, b), ts)
=>
{ nenv = hut::cons_entry_onto_uniqtype_dictionary (hut::empty_uniqtype_dictionary, (THE ts, 0));
#
map (\\ x = hut::make_type_closure_uniqtypoid (x, 1, 0, nenv))
b;
};
(_, []) => [nt]; # This requires further clarifications !!! XXX FIXME BUGGO
_ => bug "incorrect hut::Uniqtypoid instantiation in apply_typeagnsotic_type_to_arglist";
esac;
};
#
fun apply_typeagnostic_type_to_arglist_with_single_result
(
lt: hut::Uniqtypoid,
ts: List( hut::Uniqtype )
)
=
case (apply_typeagnostic_type_to_arglist (lt, ts))
#
[y] => y;
_ => bug "unexpected pmacroExpandTypeagnosticLambdaTypeOrHOC";
esac;
############################################################################
# KIND-CHECKING ROUTINES
############################################################################
exception KIND_TYPE_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 types (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_TYPE_CHECK_FAILED; fi;
# Assert that a kind is typelocked:
#
fun tk_assert_is_mono k
=
if (not (tk_is_mono k)) raise exception KIND_TYPE_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_TYPE_CHECK_FAILED;
_ => raise exception KIND_TYPE_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_TYPE_CHECK_FAILED;
fi;
_ => raise exception KIND_TYPE_CHECK_FAILED;
esac;
# Check the application of types 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_TYPE_CHECK_FAILED;
fi;
_ => raise exception KIND_TYPE_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::Uniqtype we process.
#
# One problem is that a hut::Uniqtype can have different kinds,
# depending on the valuations of its free variables.
#
# So this dictionary maps a hut::Uniqtype to an association list
# that maps the kinds of the free variables in the hut::Uniqtype
# (represented as a TYPEKIND_TYPESEQ) to the hut::Uniqtype's kind.
#
package uniqtype_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::Uniqtype;
compare = hut::compare_uniqtypes;
);
package memo:
api {
Dictionary;
#
make_dictionary: Void -> Dictionary;
#
recall_or_compute_uniqkind_of_uniqtype
:
( Dictionary,
hut::Debruijn_To_Uniqkind_Listlist,
hut::Uniqtype,
(Void -> hut::Uniqkind)
)
->
hut::Uniqkind;
}
{
package uniqtype_dictionary
=
red_black_map_g ( # red_black_map_g is from src/lib/src/red-black-map-g.pkg #
Key = hut::Uniqtype;
compare = hut::compare_uniqtypes;
);
Dictionary
=
Ref( uniqtype_dictionary::Map( List ( (hut::Uniqkind, hut::Uniqkind) ) ) ); # XXX BUGGO FIXME More icky thread-hostile global mutable state.
my make_dictionary: Void -> Dictionary
=
REF o (\\ () = uniqtype_dictionary::empty);
#
fun recall_or_compute_uniqkind_of_uniqtype
(
dictionary: Dictionary,
debruijn_to_uniqkind_listlist: hut::Debruijn_To_Uniqkind_Listlist, # Maps typevars to their Uniqkinds.
uniqtype: hut::Uniqtype, # Our primary input.
uniqkind_of_uniqtype_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_uniqtype (debruijn_to_uniqkind_listlist, uniqtype))
#
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 (uniqtype_dictionary::get (*dictionary, uniqtype))
#
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 type's kind.
uniqkind
where
#
uniqkind = uniqkind_of_uniqtype_thunk ();
#
kci' = (typevars_kindseq, uniqkind) ! kci;
dictionary := uniqtype_dictionary::set (*dictionary, uniqtype, kci');
end;
esac;
};
NULL =>
# freevars were not available.
# We'll have to recompute and
# cannot cache the result.
#
uniqkind_of_uniqtype_thunk ();
esac;
}; # package memo
# Return the kind of a given type
# in the given kind dictionary
#
fun get_uniqkind_of_uniqtype_thunk () # Evaluating the thunk allocates a fresh memo dictionary.
=
get_uniqkind_of_uniqtype
where
dictionary = memo::make_dictionary ();
#
fun get_uniqkind_of_uniqtype debruijn_to_uniqkind_listlist (uniqtype: hut::Uniqtype)
=
memo::recall_or_compute_uniqkind_of_uniqtype (dictionary, debruijn_to_uniqkind_listlist, uniqtype, uniqkind_of_uniqtype_thunk)
where
g = get_uniqkind_of_uniqtype debruijn_to_uniqkind_listlist; # Default recursive invocation.
# How to compute the kind of a type
#
fun uniqkind_of_uniqtype_thunk ()
=
case (hut::uniqtype_to_type uniqtype)
#
hut::type::DEBRUIJN_TYPEVAR (depth, index) => hut::debruijn_to_uniqkind (debruijn_to_uniqkind_listlist, depth, index);
hut::type::NAMED_TYPEVAR _ => bug "TC_NAMED_VAR not supported yet in get_uniqkind_of_uniqtype";
hut::type::BASETYPE pt => make_n_arg_typefun_uniqkind (highcode_basetypes::basetype_arity pt);
hut::type::TYPEFUN (ks, tc) => make_kindfun_uniqkind (ks, get_uniqkind_of_uniqtype (hut::prepend_uniqkind_list_to_map (debruijn_to_uniqkind_listlist, ks)) tc);
hut::type::APPLY_TYPEFUN (tc, tcs) => tk_app (g tc, map g tcs);
hut::type::TYPESEQ tcs => make_kindseq_uniqkind (map g tcs);
hut::type::ITH_IN_TYPESEQ (tc, i) => select_ith_in_type_sequence (g tc, i);
hut::type::SUM tcs
=>
{ list::apply (tk_assert_is_mono o g) tcs;
plaintype_uniqkind;
};
hut::type::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_TYPE_CHECK_FAILED;
fi;
};
_ => raise exception KIND_TYPE_CHECK_FAILED;
esac;
};
hut::type::ABSTRACT tc
=>
{ tk_assert_is_mono (g tc);
plaintype_uniqkind;
};
hut::type::BOXED tc
=>
{ tk_assert_is_mono (g tc);
plaintype_uniqkind;
};
hut::type::TUPLE (_, tcs)
=>
{ list::apply (tk_assert_is_mono o g) tcs;
plaintype_uniqkind;
};
hut::type::ARROW (_, ts1, ts2)
=>
{ list::apply (tk_assert_is_mono o g) ts1;
list::apply (tk_assert_is_mono o g) ts2;
plaintype_uniqkind;
};
hut::type::EXTENSIBLE_TOKEN(_, tc)
=>
{ tk_assert_is_mono (g tc);
plaintype_uniqkind;
};
hut::type::PARROW _ => bug "unexpected TC_PARROW in tkTypeConstructor";
hut::type::TYPE_CLOSURE _ => bug "unexpected TC_CLOSURE in tkTypeConstructor";
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected TC_INDIRECT in tkTypeConstructor";
hut::type::FATE _ => bug "unexpected TC_FATE in tkTypeConstructor";
esac;
end; # fun get_uniqkind_of_uniqtype
end; # fun get_uniqkind_of_uniqtype_thunk
# Assert that the kind of `type'
# is a subkind of `kind' in `debruijn_to_uniqkind_listlist':
#
fun assert_type_has_subkind_of_kind_thunk () # Evaluating the thunk allocates a new memo dictionary.
=
assert_type_has_subkind_of_kind
where
get_uniqkind_of_uniqtype = get_uniqkind_of_uniqtype_thunk (); # Allocate a fresh memo dictionary.
#
fun assert_type_has_subkind_of_kind debruijn_to_uniqkind_listlist (kind, type)
=
assert_this_is_a_subkind_of_that
{
this => get_uniqkind_of_uniqtype debruijn_to_uniqkind_listlist type,
that => kind
};
end;
# hut::Uniqtypoid 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_type_has_subkind_of_kind =
assert_type_has_subkind_of_kind_thunk (); # Evaluating the thunk allocates a new memo dictionary.
#
fun apply_typeagnostic_type_to_arglist_with_checking
(
fn_type: hut::Uniqtypoid, # Fn type.
fn_arg_types: List(hut::Uniqtype), # Types of args to which fn is being applied.
debruijn_to_uniqkind_listlist: hut::Debruijn_To_Uniqkind_Listlist
)
=
{ fn_type_in_whnf = hut::reduce_uniqtypoid_to_weak_head_normal_form fn_type;
case (/* lt_outX */ hut::uniqtypoid_to_typoid fn_type_in_whnf, fn_arg_types)
#
(hut::typoid::TYPEAGNOSTIC (fn_parameter_kinds, b), fn_arg_types) # 'b' == 'body type(s)'...? It has type List(Uniqtypoid)
=>
{ paired_lists::apply (assert_type_has_subkind_of_kind debruijn_to_uniqkind_listlist) (fn_parameter_kinds, fn_arg_types);
#
fun h x
=
hut::make_type_closure_uniqtypoid (x, 1, 0, hut::cons_entry_onto_uniqtype_dictionary (hut::empty_uniqtype_dictionary, (THE fn_arg_types, 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::Uniqtypoid 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_uniqtype_dictionary (hut::empty_uniqtype_dictionary, (THE ts, 0));
#
fun h (abslevel, ol, nl, tenv)
=
if (abslevel == 0)
#
hut::make_type_closure_uniqtypoid (lt, ol, nl, tenv);
#
elif (abslevel > 0)
#
h (abslevel - 1, ol+1, nl+1, hut::cons_entry_onto_uniqtype_dictionary (tenv, (NULL, nl)));
else
bug "unexpected cases in ltAdjSt";
fi;
end;
# A special type 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_uniqtype_dictionary (hut::empty_uniqtype_dictionary, (THE ts, 0));
#
fun h (abslevel, ol, nl, tenv)
=
if (abslevel == 0) hut::make_type_closure_uniqtype (tc, ol, nl, tenv);
elif (abslevel > 0) h (abslevel - 1, ol+1, nl+1, hut::cons_entry_onto_uniqtype_dictionary (tenv, (NULL, nl)));
else bug "unexpected cases in tcAdjSt";
fi;
end;
# * Sinking the hut::Uniqtypoid 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_uniqtypoid (lt, ol, nl, tenv);
#
elif (abslevel > 0)
#
h (abslevel - 1, ol+1, nl+1, hut::cons_entry_onto_uniqtype_dictionary(tenv, (NULL, nl)));
else
bug "unexpected cases in ltSinkSt";
fi;
nt = h (nd-d, 0, 1, hut::empty_uniqtype_dictionary);
nt; # was reduceLambdaTypeToNormalForm nt
};
# * Sinking the type 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_uniqtype (tc, ol, nl, tenv);
elif (abslevel > 0) h (abslevel - 1, ol+1, nl+1, hut::cons_entry_onto_uniqtype_dictionary (tenv, (NULL, nl)));
else bug "unexpected cases in ltSinkSt";
fi;
nt = h (nd-d, 0, 1, hut::empty_uniqtype_dictionary);
nt; # was reduceTypeConstructorToNormalForm nt
};
# Utility functions used in nextcode:
#
fun lt_is_fate lt
=
case (hut::uniqtypoid_to_typoid lt)
#
hut::typoid::FATE _
=>
TRUE;
hut::typoid::TYPE tc
=>
case (hut::uniqtype_to_type tc) hut::type::FATE _ => TRUE;
_ => FALSE;
esac;
_ => FALSE;
esac;
#
fun ltw_is_fate (lt, f, g, h)
=
case (hut::uniqtypoid_to_typoid lt)
#
hut::typoid::FATE t
=>
f t;
hut::typoid::TYPE tc
=>
case (hut::uniqtype_to_type tc) hut::type::FATE x => g x;
_ => h lt;
esac;
_ => h lt;
esac;
#
fun tc_bug tc s = bug (s + "\n\n" + (uniqtype_to_string tc) + "\n\n");
fun lt_bug lt s = bug (s + "\n\n" + (uniqtypoid_to_string lt) + "\n\n");
# Other misc utility functions:
#
fun tc_get_field (tc, i)
=
case (hut::uniqtype_to_type tc)
#
hut::type::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::uniqtypoid_to_typoid t)
#
hut::typoid::PACKAGE ts
=>
(list::nth (ts, i))
except
_ = bug "incorrect PACKAGE in lt_get_field";
#
hut::typoid::TYPE tc
=>
make_type_uniqtypoid (tc_get_field (tc, i));
_ => bug "incorrect lambda types in lt_get_field";
esac;
#
fun tc_swap t
=
case (hut::uniqtype_to_type t)
#
hut::type::ARROW (hut::VARIABLE_CALLING_CONVENTION { arg_is_raw => r1, body_is_raw => r2 }, [s1], [s2])
=> make_arrow_uniqtype (hut::VARIABLE_CALLING_CONVENTION { arg_is_raw => r2, body_is_raw => r1 }, [s2], [s1]);
#
hut::type::ARROW (hut::FIXED_CALLING_CONVENTION, [s1], [s2])
=> make_arrow_uniqtype (hut::FIXED_CALLING_CONVENTION, [s2], [s1]);
_ => bug "unexpected types in tc_swap";
esac;
#
fun lt_swap t
=
case (hut::uniqtypoid_to_typoid t)
#
(hut::typoid::TYPEAGNOSTIC (ks, [x]))
=>
make_typeagnostic_uniqtypoid (ks, [lt_swap x]);
(hut::typoid::TYPE x)
=>
make_type_uniqtypoid (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_uniqtypoid ( atys, rtys);
ltc_fkfun ( { call_as=>acf::CALL_AS_FUNCTION fixed, ... }, atys, rtys)
=>
make_arrow_uniqtypoid (fixed, atys, rtys);
end;
#
fun ltd_fkfun lambda_type
=
if (uniqtypoid_is_generic_package lambda_type)
unpack_generic_package_uniqtypoid lambda_type;
else
my (_, atys, rtys) = unpack_arrow_uniqtypoid lambda_type;
(atys, rtys);
fi;
#
fun ltc_rkind (acf::RK_TUPLE _, lts) => make_tuple_uniqtypoid lts;
ltc_rkind (acf::RK_PACKAGE, lts) => make_package_uniqtypoid lts;
ltc_rkind (acf::RK_VECTOR t, _) => make_ro_vector_uniqtypoid (make_type_uniqtypoid 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 type:
#
fun tc_upd_prim tc
=
h (hut::uniqtype_to_type tc)
where
fun h (hut::type::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::RW_VECTOR_SET; # Int1, Float64, List, Null_Or, Generic_Machine_Word, Single_Word, Tagged_Int, Untagged_Int, Boxed, Dynamically_Typed.
fi;
h (hut::type::TUPLE _ | hut::type::ARROW _)
=>
hbo::SET_VECSLOT_TO_BOXED_VALUE;
h (hut::type::RECURSIVE ((1, tc, ts), 0))
=>
{ ntc = case ts [] => tc;
_ => make_apply_typefun_uniqtype (tc, ts);
esac;
case (hut::uniqtype_to_type ntc)
#
hut::type::TYPEFUN([k], b) => h (hut::uniqtype_to_type b);
_ => hbo::RW_VECTOR_SET;
esac;
};
h (hut::type::SUM tcs)
=>
{ fun g (a ! r) => same_uniqtype (a, void_uniqtype)
?? g r
:: FALSE;
g [] => TRUE;
end;
if (g tcs) hbo::SET_VECSLOT_TO_TAGGED_INT_VALUE;
else hbo::RW_VECTOR_SET;
fi;
};
h _ => hbo::RW_VECTOR_SET;
end;
end;
fun uniqkind_to_uniqtypoid (uniqkind: hut::Uniqkind) : hut::Uniqtypoid
=
case (hut::uniqkind_to_kind uniqkind)
#
hut::kind::PLAINTYPE => int_uniqtypoid;
hut::kind::BOXEDTYPE => int_uniqtypoid;
hut::kind::KINDSEQ ks => make_tuple_uniqtypoid (map uniqkind_to_uniqtypoid ks);
hut::kind::KINDFUN (ks, k) => make_arrow_uniqtypoid (fixed_calling_convention, [make_tuple_uniqtypoid (map uniqkind_to_uniqtypoid ks)], [uniqkind_to_uniqtypoid k]);
esac;
# tnarrow_fn: Void -> ((hut::Uniqtype -> hut::Uniqtype) * (hut::Uniqtypoid -> hut::Uniqtypoid) * (Void->Void))
#
fun tnarrow_fn ()
=
( tc_map o hut::reduce_uniqtype_to_normal_form,
lt_map o hut::reduce_uniqtypoid_to_normal_form,
\\ () = ()
)
where
fun tc_narrow tcf t
=
case (hut::uniqtype_to_type t)
#
hut::type::BASETYPE pt
=>
if (hbt::isvoid pt) truevoid_uniqtype;
else t;
fi;
hut::type::TUPLE (_, tcs)
=>
make_tuple_uniqtype (map tcf tcs);
hut::type::ARROW (r, ts1, ts2)
=>
make_arrow_uniqtype (fixed_calling_convention, map tcf ts1, map tcf ts2);
_ => truevoid_uniqtype;
esac;
#
fun lt_narrow (tcf, ltf) t
=
case (hut::uniqtypoid_to_typoid t)
#
hut::typoid::TYPE tc => make_type_uniqtypoid (tcf tc);
hut::typoid::PACKAGE ts => make_package_uniqtypoid (map ltf ts);
#
hut::typoid::GENERIC_PACKAGE (ts1, ts2) => make_generic_package_uniqtypoid (map ltf ts1, map ltf ts2);
hut::typoid::TYPEAGNOSTIC (ks, xs) => make_generic_package_uniqtypoid([make_package_uniqtypoid (map uniqkind_to_uniqtypoid ks)], map ltf xs);
hut::typoid::FATE _ => bug "unexpected hut::typoid::FATE in ltNarrow";
hut::typoid::INDIRECT_TYPE_THUNK _ => bug "unexpected hut::typoid::INDIRECT_TYPE_THUNK in ltNarrow";
hut::typoid::TYPE_CLOSURE _ => bug "unexpected hut::typoid::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::Uniqtype -> hut::Uniqtype,
# hut::Uniqtypoid -> hut::Uniqtypoid,
# hut::Uniqtype -> hut::Uniqtype,
# hut::Uniqtypoid -> hut::Uniqtypoid,
# Void -> Void
# )
#
fun twrap_fn bbb
=
{ fun tc_wmap (w, u) t
=
case (hut::uniqtype_to_type t)
#
(hut::type::DEBRUIJN_TYPEVAR _ | hut::type::NAMED_TYPEVAR _) => t;
hut::type::BASETYPE bt => if (hbt::basetype_is_unboxed bt) make_extensible_token_uniqtype t; else t;fi;
hut::type::TYPEFUN (ks, tc) => make_typefun_uniqtype (ks, w tc); # impossible case
hut::type::APPLY_TYPEFUN (tc, tcs) => make_apply_typefun_uniqtype (w tc, map w tcs);
hut::type::TYPESEQ tcs => make_typeseq_uniqtype (map w tcs);
hut::type::ITH_IN_TYPESEQ (tc, i) => make_ith_in_typeseq_uniqtype (w tc, i);
hut::type::SUM tcs => make_sum_uniqtype (map w tcs);
#
hut::type::RECURSIVE ((n, tc, ts), i)
=>
make_recursive_uniqtype((n, hut::reduce_uniqtype_to_normal_form (u tc), map w ts), i);
#
hut::type::TUPLE (_, ts) => make_extensible_token_uniqtype (make_tuple_uniqtype (map w ts)); # ?
hut::type::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::uniqtype_list_to_uniqtype_tuple ts1)];
esac;
nts2 = [w (hut::uniqtype_list_to_uniqtype_tuple ts2)];
nt = make_arrow_uniqtype (fixed_calling_convention, nts1, nts2);
if b1 nt;
else make_extensible_token_uniqtype nt;
fi;
};
#
hut::type::ARROW (hut::FIXED_CALLING_CONVENTION, _, _)
=>
bug "unexpected TC_FIXED_ARROW in tc_umap";
hut::type::EXTENSIBLE_TOKEN (k, t) => bug "unexpected token hut::Uniqtype in tc_wmap";
hut::type::BOXED _ => bug "unexpected TC_BOXED in tc_wmap";
hut::type::ABSTRACT _ => bug "unexpected TC_ABSTRACT in tc_wmap";
_ => bug "unexpected other types in tc_wmap";
esac;
#
fun tc_umap (u, w) t
=
case (hut::uniqtype_to_type t)
#
(hut::type::DEBRUIJN_TYPEVAR _ | hut::type::NAMED_TYPEVAR _ | hut::type::BASETYPE _) => t;
hut::type::TYPEFUN (ks, tc) => make_typefun_uniqtype (ks, u tc); /* impossible case */
hut::type::APPLY_TYPEFUN (tc, tcs) => make_apply_typefun_uniqtype (u tc, map w tcs);
hut::type::TYPESEQ tcs => make_typeseq_uniqtype (map u tcs);
hut::type::ITH_IN_TYPESEQ (tc, i) => make_ith_in_typeseq_uniqtype (u tc, i);
hut::type::SUM tcs => make_sum_uniqtype (map u tcs);
#
hut::type::RECURSIVE ((n, tc, ts), i)
=>
make_recursive_uniqtype((n, hut::reduce_uniqtype_to_normal_form (u tc), map w ts), i);
#
hut::type::TUPLE (rk, tcs) => make_tuple_uniqtype (map u tcs);
#
hut::type::ARROW (hut::VARIABLE_CALLING_CONVENTION { arg_is_raw => b1, body_is_raw => b2 }, ts1, ts2)
=>
make_arrow_uniqtype (fixed_calling_convention, map u ts1, map u ts2);
#
hut::type::ARROW (hut::FIXED_CALLING_CONVENTION, _, _)
=>
bug "unexpected TC_FIXED_ARROW in tc_umap";
#
hut::type::PARROW _ => bug "unexpected TC_PARROW in tc_umap";
hut::type::BOXED _ => bug "unexpected TC_BOXED in tc_umap";
hut::type::ABSTRACT _ => bug "unexpected TC_ABSTRACT in tc_umap";
#
hut::type::EXTENSIBLE_TOKEN (k, t)
=>
if (hut::same_token (k, hut::wrap_token))
bug "unexpected TC_WRAP in tc_umap";
else
hut::type_to_uniqtype (hut::type::EXTENSIBLE_TOKEN (k, u t));
fi;
_ => bug "unexpected other types in tc_umap";
esac;
#
fun lt_umap (tcf, ltf) t
=
case (hut::uniqtypoid_to_typoid t)
#
hut::typoid::TYPE tc => make_type_uniqtypoid (tcf tc);
hut::typoid::PACKAGE ts => make_package_uniqtypoid (map ltf ts);
hut::typoid::GENERIC_PACKAGE (ts1, ts2) => make_generic_package_uniqtypoid (map ltf ts1, map ltf ts2);
hut::typoid::TYPEAGNOSTIC (ks, xs) => make_typeagnostic_uniqtypoid (ks, map ltf xs);
hut::typoid::FATE _ => bug "unexpected CNTs in lt_umap";
hut::typoid::INDIRECT_TYPE_THUNK _ => bug "unexpected INDs in lt_umap";
hut::typoid::TYPE_CLOSURE _ => bug "unexpected ENVs in lt_umap";
esac;
(highcode_dictionary::wmemo_fn { tc_wmap, tc_umap, lt_umap })
->
{ tc_wmap=>tc_wrap, tc_umap=>tc_map, lt_umap=>lt_map, cleanup };
#
fun lt_wrap x
=
if_uniqtypoid_is_type ( x,
(\\ tc = make_type_uniqtypoid (tc_wrap tc)),
\\ _ = bug "unexpected case in ltWrap"
);
( tc_wrap o hut::reduce_uniqtype_to_normal_form,
lt_wrap o hut::reduce_uniqtypoid_to_normal_form,
tc_map o hut::reduce_uniqtype_to_normal_form,
lt_map o hut::reduce_uniqtypoid_to_normal_form,
cleanup
);
};
#########################################################################
# SUBSTITION OF NAMED VARS IN A TYC/LTY
#########################################################################
package uniqtypoid_dictionary
=
binary_map_g (
#
Key = hut::Uniqtypoid;
compare = hut::compare_uniqtypoids;
);
# 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 (uniqtype_dictionary::empty);
#
fun tc_named_typevar_elimination s depth type
=
case (hut::get_free_named_variables_in_uniqtype type)
#
[] => type; # nothing to elim
#
_ =>
{ # Encode the type and
# the depth for memoization
# using make_ith_in_typeseq_uniqtype:
#
tycdepth = make_ith_in_typeseq_uniqtype (type, depth);
case (uniqtype_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::uniqtype_to_type type)
#
hut::type::DEBRUIJN_TYPEVAR _ => type;
hut::type::BASETYPE _ => type;
#
hut::type::TYPEFUN (tks, t) => make_typefun_uniqtype (tks, tc_named_typevar_elimination s (di::next depth) t);
hut::type::APPLY_TYPEFUN (t, ts) => make_apply_typefun_uniqtype (r t, rs ts);
hut::type::TYPESEQ ts => make_typeseq_uniqtype (rs ts);
#
hut::type::ITH_IN_TYPESEQ (t, i) => make_ith_in_typeseq_uniqtype (r t, i);
hut::type::SUM ts => make_sum_uniqtype (rs ts);
#
hut::type::TUPLE (rf, ts) => make_tuple_uniqtype (rs ts);
hut::type::ARROW (ff, ts, ts') => make_arrow_uniqtype (ff, rs ts, rs ts');
hut::type::PARROW (t, t') => make_lambdacode_arrow_uniqtype (r t, r t');
#
hut::type::BOXED t => make_boxed_uniqtype (r t);
hut::type::ABSTRACT t => make_abstract_uniqtype (r t);
hut::type::FATE ts => make_uniqtype_fate (rs ts);
#
hut::type::RECURSIVE ((i, t, ts), j)
=>
make_recursive_uniqtype ((i, r t, rs ts), j);
hut::type::NAMED_TYPEVAR tvar
=>
case (s (tvar, depth))
#
THE t => t;
NULL => type;
esac;
hut::type::EXTENSIBLE_TOKEN (tok, t)
=>
hut::type_to_uniqtype (hut::type::EXTENSIBLE_TOKEN (tok, r t));
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected TC_INDIRECT in tc_named_typevar_elimination";
hut::type::TYPE_CLOSURE _ => bug "unexpected TC_CLOSURE in tc_named_typevar_elimination";
esac;
dictionary := uniqtype_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 (uniqtypoid_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_uniqtypoid lambda_type)
#
[] => lambda_type; # nothing to elim
#
_ => {
# Encode the hut::Uniqtypoid and depth info
# using TYPE_CLOSURE
# (only first 2 args are useful)
#
ltydepth
=
hut::typoid_to_uniqtypoid
(
hut::typoid::TYPE_CLOSURE (lambda_type, depth, 0, hut::empty_uniqtype_dictionary)
);
case (uniqtypoid_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::uniqtypoid_to_typoid lambda_type)
#
hut::typoid::TYPE t => make_type_uniqtypoid (tc_named_typevar_elimination s depth t);
hut::typoid::PACKAGE ts => make_package_uniqtypoid (rs ts);
#
hut::typoid::GENERIC_PACKAGE (ts, ts') => make_generic_package_uniqtypoid (rs ts, rs ts');
hut::typoid::TYPEAGNOSTIC (tks, ts) => make_typeagnostic_uniqtypoid (tks, map (lt_named_typevar_elimination s (di::next depth)) ts);
hut::typoid::FATE ts => make_uniqtypoid_fate (rs ts);
#
hut::typoid::INDIRECT_TYPE_THUNK _ => bug "unexpected INDIRECT_TYPE_THUNK in lt_named_typevar_elimination";
hut::typoid::TYPE_CLOSURE _ => bug "unexpected TYPE_CLOSURE in lt_named_typevar_elimination";
esac;
dictionary := uniqtypoid_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::Uniqtype));
# 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, type) ! s)
=>
case (int::compare (tv, tv'))
#
LESS => NULL;
GREATER => h s;
EQUAL => THE type;
esac;
end;
end;
#
fun tc_nvar_subst_fn ()
=
tc_nvar_subst
where
dictionary = REF (uniqtype_dictionary::empty);
#
fun tc_nvar_subst subst
=
loop
where
fun loop type
=
# Check if substitution overlaps
# with free vars list:
#
case (intersection_non_empty (subst, hut::get_free_named_variables_in_uniqtype type))
#
FALSE => type; # nothing to subst
#
TRUE =>
# Next check the memoization table:
#
case (uniqtype_dictionary::get (*dictionary, type))
#
THE t => t; # Hit.
#
NULL => # Must recompute.
t
where
t = case (hut::uniqtype_to_type type)
#
hut::type::NAMED_TYPEVAR tv
=>
case (search_subst (tv, subst))
#
THE t => t;
NULL => type;
esac;
#
hut::type::DEBRUIJN_TYPEVAR _ => type;
hut::type::BASETYPE _ => type;
#
hut::type::TYPEFUN (tks, t) => make_typefun_uniqtype (tks, loop t);
hut::type::APPLY_TYPEFUN (t, ts) => make_apply_typefun_uniqtype (loop t, map loop ts);
#
hut::type::TYPESEQ ts => make_typeseq_uniqtype (map loop ts);
hut::type::ITH_IN_TYPESEQ (t, i) => make_ith_in_typeseq_uniqtype (loop t, i);
hut::type::SUM ts => make_sum_uniqtype (map loop ts);
#
hut::type::RECURSIVE ((i, t, ts), j)
=>
make_recursive_uniqtype ((i, loop t, map loop ts), j);
#
hut::type::TUPLE (rf, ts) => make_tuple_uniqtype (map loop ts);
hut::type::ARROW (ff, ts, ts') => make_arrow_uniqtype (ff, map loop ts, map loop ts');
hut::type::PARROW (t, t') => make_lambdacode_arrow_uniqtype (loop t, loop t');
#
hut::type::BOXED t => make_boxed_uniqtype (loop t);
hut::type::ABSTRACT t => make_abstract_uniqtype (loop t);
hut::type::FATE ts => make_uniqtype_fate (map loop ts);
hut::type::EXTENSIBLE_TOKEN (tok, t)
=>
hut::type_to_uniqtype (hut::type::EXTENSIBLE_TOKEN (tok, loop t));
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected TC_INDIRECT in substTypeConstructor";
hut::type::TYPE_CLOSURE _ => bug "unexpected TC_CLOSURE in substTypeConstructor";
esac;
# Update memoization table:
#
dictionary := uniqtype_dictionary::set (*dictionary, type, 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 (uniqtypoid_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_uniqtypoid lambda_type))
#
FALSE => lambda_type; # nothing to subst
#
TRUE =>
# Next, check the memoization table:
#
case (uniqtypoid_dictionary::get (*dictionary, lambda_type))
#
THE t => t; # A hit!
#
NULL => # Must recompute>
t
where
t = case (hut::uniqtypoid_to_typoid lambda_type)
#
hut::typoid::TYPE t => make_type_uniqtypoid (tc_nvar_subst t);
#
hut::typoid::PACKAGE ts => make_package_uniqtypoid (map loop ts);
hut::typoid::GENERIC_PACKAGE (ts, ts') => make_generic_package_uniqtypoid (map loop ts, map loop ts');
#
hut::typoid::TYPEAGNOSTIC (tks, ts) => make_typeagnostic_uniqtypoid (tks, map loop ts);
hut::typoid::FATE ts => make_uniqtypoid_fate (map loop ts);
#
hut::typoid::INDIRECT_TYPE_THUNK _ => bug "unexpected INDIRECT_TYPE_THUNK in lt_named_typevar_elimination";
hut::typoid::TYPE_CLOSURE _ => bug "unexpected TYPE_CLOSURE in lt_named_typevar_elimination";
esac;
# Update memoization table:
#
dictionary := uniqtypoid_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 (uniqtype_dictionary::empty);
#
fun tc_nvar_cvt (tvoffs: Tvoffs) d type
=
# Compile_statistics::addStat s_iter 1;
# Compile_statistics::addStat s_tvoffs (length tvoffs);
# Compile_statistics::addStat s_nvars (length (hut::freeNamedVariablesInTypeConstructor type));
# Check if substitution overlaps with free vars list
#
case (intersect (tvoffs, hut::get_free_named_variables_in_uniqtype type))
#
[] => (# Compile_statistics::addStat s_cuts 1;
type # nothing to convert
);
tvoffs
=>
{
# Encode the type
# and the depth for memoization
# using make_ith_in_typeseq_uniqtype:
#
tycdepth = make_ith_in_typeseq_uniqtype (type, d);
case (uniqtype_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::uniqtype_to_type type)
#
hut::type::NAMED_TYPEVAR tvar
=>
case (search_subst (tvar, tvoffs))
#
THE i => make_debruijn_typevar_uniqtype (d, i);
NULL => type;
esac;
#
hut::type::DEBRUIJN_TYPEVAR _ => type;
hut::type::BASETYPE _ => type;
hut::type::TYPEFUN (tks, t) => make_typefun_uniqtype (tks, tc_nvar_cvt tvoffs (di::next d) t);
#
hut::type::APPLY_TYPEFUN (t, ts) => make_apply_typefun_uniqtype (r t, rs ts);
hut::type::TYPESEQ ts => make_typeseq_uniqtype (rs ts);
hut::type::ITH_IN_TYPESEQ (t, i) => make_ith_in_typeseq_uniqtype (r t, i);
hut::type::SUM ts => make_sum_uniqtype (rs ts);
hut::type::RECURSIVE ((i, t, ts), j) => make_recursive_uniqtype ((i, r t, rs ts), j);
hut::type::TUPLE (rf, ts) => make_tuple_uniqtype (rs ts);
hut::type::ARROW (ff, ts, ts') => make_arrow_uniqtype (ff, rs ts, rs ts');
hut::type::PARROW (t, t') => make_lambdacode_arrow_uniqtype (r t, r t');
hut::type::BOXED t => make_boxed_uniqtype (r t);
hut::type::ABSTRACT t => make_abstract_uniqtype (r t);
hut::type::EXTENSIBLE_TOKEN (tok, t) => hut::type_to_uniqtype (hut::type::EXTENSIBLE_TOKEN (tok, r t));
hut::type::FATE ts => make_uniqtype_fate (rs ts);
hut::type::INDIRECT_TYPE_THUNK _ => bug "unexpected TC_INDIRECT in tc_nvar_cvt";
hut::type::TYPE_CLOSURE _ => bug "unexpected TC_CLOSURE in tc_nvar_cvt";
esac;
dictionary := uniqtype_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 (uniqtypoid_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_uniqtypoid 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::typoid_to_uniqtypoid (hut::typoid::TYPE_CLOSURE (lambda_type, d, 0, hut::empty_uniqtype_dictionary));
case (uniqtypoid_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::uniqtypoid_to_typoid lambda_type)
#
hut::typoid::TYPE t
=>
make_type_uniqtypoid (tc_nvar_cvt tvoffs d t);
#
hut::typoid::PACKAGE ts => make_package_uniqtypoid (rs ts);
hut::typoid::GENERIC_PACKAGE (ts, ts') => make_generic_package_uniqtypoid (rs ts, rs ts');
#
hut::typoid::TYPEAGNOSTIC (tks, ts)
=>
make_typeagnostic_uniqtypoid (tks,
map (lt_nvar_cvt tvoffs (di::next d)) ts);
#
hut::typoid::FATE ts
=>
make_uniqtypoid_fate (rs ts);
#
hut::typoid::INDIRECT_TYPE_THUNK _ => bug "unexpected INDIRECT_TYPE_THUNK in lt_nvar_cvt";
hut::typoid::TYPE_CLOSURE _ => bug "unexpected TYPE_CLOSURE in lt_nvar_cvt";
esac;
dictionary := uniqtypoid_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_uniqtypoid (ks, map lt_subst lt);
};
}; # package highcode
end; # top-level stipulate