## type-anormcode.pkg
# Compiled by:
# src/lib/compiler/core.sublib# highcode Type Checker
stipulate
package acf = anormcode_form; # anormcode_form is from src/lib/compiler/back/top/anormcode/anormcode-form.pkgherein
api Type_Anormcode {
#
# Which set of typing rules to use while doing the typecheck
Typesys; # Currently very crude
check_top: (acf::Function, Typesys) -> Bool;
check_expression: (acf::Expression, Typesys) -> Bool;
};
end;
stipulate
package acf = anormcode_form; # anormcode_form is from src/lib/compiler/back/top/anormcode/anormcode-form.pkg package cos = compile_statistics; # compile_statistics is from src/lib/compiler/front/basics/stats/compile-statistics.pkg package di = debruijn_index; # debruijn_index is from src/lib/compiler/front/typer/basics/debruijn-index.pkg package hbo = highcode_baseops; # highcode_baseops is from src/lib/compiler/back/top/highcode/highcode-baseops.pkg package hcf = highcode_form; # highcode_form is from src/lib/compiler/back/top/highcode/highcode-form.pkg package tmp = highcode_codetemp; # highcode_codetemp is from src/lib/compiler/back/top/highcode/highcode-codetemp.pkg package hut = highcode_uniq_types; # highcode_uniq_types is from src/lib/compiler/back/top/highcode/highcode-uniq-types.pkg package is = int_red_black_set; # int_red_black_set is from src/lib/src/int-red-black-set.pkg package pp = prettyprint_anormcode; # prettyprint_anormcode is from src/lib/compiler/back/top/anormcode/prettyprint-anormcode.pkg package vh = varhome; # varhome is from src/lib/compiler/front/typer-stuff/basics/varhome.pkgherein
package type_anormcode
: (weak) Type_Anormcode # Type_Anormcode is from src/lib/compiler/back/top/anormcode/type-anormcode.pkg {
# Which set of the typing rules
# to use while doing the typecheck:
#
Typesys = Bool; # Currently very crude
stipulate
fun bug s
=
error_message::impossible ("type_anormcode: " + s);
say = control_print::say;
anyerror = REF FALSE;
###########################################################################
# BASIC UTILITY FUNCTIONS #
###########################################################################
fun foldl2 (f, a, xs, ys, g)
=
loop (a, xs, ys)
where
recursive my loop
=
\\ (a, NIL, NIL) => a;
(a, x ! xs, y ! ys) => loop (f (x, y, a), xs, ys);
(a, xs', _) => g (a, xs', length xs, length ys);
end;
end;
fun simplify (le, 0)
=>
acf::RET [acf::STRING "<...>"];
simplify (le, n)
=>
{ fun h le
=
simplify (le, n - 1);
fun h1 (fk, v, args, le)
=
(fk, v, args, h le);
fun h2 (tfk, v, tvs, le)
=
(tfk, v, tvs, h le);
case le
acf::LET (vs, e1, e2)
=>
acf::LET (vs, h e1, h e2);
acf::MUTUALLY_RECURSIVE_FNS (fdecs, b)
=>
acf::MUTUALLY_RECURSIVE_FNS (map h1 fdecs, h b);
acf::TYPEFUN (tdec, e)
=>
acf::TYPEFUN (h2 tdec, h e);
acf::SWITCH (v, l, dc, opp)
=>
acf::SWITCH (v, l, map g dc, f opp)
where
fun g (c, x)
=
(c, h x);
f =
\\ THE y => THE (h y);
NULL => NULL;
end ;
end;
acf::CONSTRUCTOR (dc, tcs, vs, lv, le) => acf::CONSTRUCTOR (dc, tcs, vs, lv, h le);
acf::RECORD (rk, vs, lv, le) => acf::RECORD (rk, vs, lv, h le);
acf::GET_FIELD (v, n, lv, le) => acf::GET_FIELD (v, n, lv, h le);
acf::EXCEPT (e, v) => acf::EXCEPT (h e, v);
acf::BASEOP (po, vs, lv, le) => acf::BASEOP (po, vs, lv, h le);
_ => le;
esac;
};
end; # fun simplify
# Utility functions for printing:
#
say_uniqkind = say o hcf::uniqkind_to_string;
say_uniqtype = say o hcf::uniqtype_to_string;
say_uniqtypoid = say o hcf::uniqtypoid_to_string;
fun le_print le
=
pp::print_lexp (simplify (le, 3));
sv_print = pp::print_sval;
fun error (le, g)
=
{ anyerror := TRUE;
say "\n************************************************************\
\\n**** highcode type checking failed: ";
g () then { say "\n** term:\n"; le_print le;};
};
fun err_msg (le, s, r)
=
error (le, {. say s; r;} );
fun catch_exn f (le, g)
=
f ()
except
ex = error ( le,
{. g () then say ("\n** exception " + exception_name ex + " raised"); }
);
# A hack for type checkng:
#
fun later_phase post_reify
=
post_reify;
fun check phase dicts lambda_expression
=
{ # Imperative table -- keeps track of already bound variables,
# so we can tell if a variable is re-bound (which should be
# illegal). Note that lvars and tvars actually share the same
# namespace! -- Christopher League, 1998-04-11
defined_lvars
=
REF is::empty;
fun lvar_def le (highcode_variable: tmp::Codetemp)
=
if (is::member (*defined_lvars, highcode_variable))
#
err_msg (le, ("highcode_variable " + (highcode_codetemp::to_string highcode_variable) + " redefined"), ());
else
defined_lvars := is::add (*defined_lvars, highcode_variable);
fi;
lt_equiv
=
hcf::similar_uniqtypoids; # should be hcf::lambda_types_are_equivalent # XXX BUGGO FIXME
lt_tapp_check
=
if *anormcode_sequencer_controls::check_kinds
#
hcf::apply_typeagnostic_type_to_arglist_with_checking_thunk (); # Evaluating the thunk allocates a new memo dictionary.
else
\\ (lt, ts, _) = hcf::apply_typeagnostic_type_to_arglist (lt, ts);
fi;
fun const_truevoid _
=
hcf::truevoid_uniqtypoid;
my (lt_string, lt_exn, lt_etag, lt_vector, lt_wrap, lt_bool)
=
if (later_phase phase)
#
(hcf::string_uniqtypoid, hcf::truevoid_uniqtypoid, const_truevoid, const_truevoid, const_truevoid,
hcf::truevoid_uniqtypoid);
else
(hcf::string_uniqtypoid, hcf::exception_uniqtypoid, hcf::make_exception_tag_uniqtypoid, hcf::make_type_uniqtypoid o hcf::make_ro_vector_uniqtype,
hcf::make_type_uniqtypoid o hcf::make_boxed_uniqtype, hcf::bool_uniqtypoid);
fi;
fun pr_msg_lt (s, lt)
=
{ say s;
say_uniqtypoid lt;
};
fun pr_list f s t
=
{ recursive my loop
=
\\ [] => say "<empty list>\n";
[x] => { f x; say "\n"; };
x ! xs => { f x; say "\n* and\n"; loop xs; };
end;
say s;
loop t;
};
fun print2lts (s, s', lt, lt')
=
{ pr_list say_uniqtypoid s lt;
pr_list say_uniqtypoid s' lt';
};
fun lt_match (le, s) (t, t')
=
if (not (lt_equiv (t, t')))
error (
le,
{. pr_msg_lt (s + ": Lty conflict\n** types:\n", t);
pr_msg_lt ("\n** and\n", t');
}
);
fi;
fun lts_match (le, s) (ts, ts')
=
foldl2 (
\\ (t, t', _)
=
lt_match
(le, s) (t, t'),
(),
ts,
ts',
\\ (_, _, n, n')
=
error (
le,
{. print2lts (
cat [s, ": type list mismatch (", int::to_string n, " vs ",
int::to_string n', ")\n** expected types:\n"
],
"** actual types:\n",
ts,
ts'
);
}
)
);
stipulate
fun lt_fn_app_fn opr (le, s, msg) (t, ts)
=
catch_exn
{. my (xs, ys) = opr (hcf::ltd_fkfun t);
lts_match (le, s) (xs, ts); ys;
}
( le,
{. pr_msg_lt (s + msg + "\n** type:\n", t);
[];
}
);
herein
fun lt_fn_app (le, s)
=
lt_fn_app_fn (\\ x = x) (le, s, ": Applying term of non-arrow type");
fun lt_fn_app_r (le, s)
=
lt_fn_app_fn (\\ (x, y) = (y, x)) (le, s, ": Rev-apply term of non-arrow type");
end;
fun lt_ty_app
(
expression: acf::Expression,
message: String
)
( function_type: hut::Uniqtypoid,
argument_uniqtypes: List( hut::Uniqtype ),
debruijn_to_uniqkind_listlist: hut::Debruijn_To_Uniqkind_Listlist
)
=
catch_exn
{. lt_tapp_check (function_type, argument_uniqtypes, debruijn_to_uniqkind_listlist); }
( expression,
{. pr_msg_lt (message + ": Kind conflict\n** function type:\n", function_type);
pr_list say_uniqtype "\n** argument types:\n" argument_uniqtypes;
[];
}
);
fun lt_arrow (le, s) (call_as, alts, rlts)
=
case call_as
#
acf::CALL_AS_GENERIC_PACKAGE
=>
hcf::make_generic_package_uniqtypoid (alts, rlts);
acf::CALL_AS_FUNCTION raw
=>
catch_exn
#
{. hcf::make_arrow_uniqtypoid (raw, alts, rlts); }
#
( le,
{. print2lts (
s + ": deeply typeagnostic non-generic .\n** parameter types:\n",
"** result types:\n",
alts, rlts
);
hcf::truevoid_uniqtypoid;
}
);
esac;
# typeInDict: hcf::tkindDict * hcf::ltyDict * di::depth -> Expression -> List( Uniqtypoid )
fun type_in_dictionary (kenv, venv, d)
=
{ fun ext_dictionary (lv, lt, ve) = hcf::set_uniqtypoid_for_var (ve, lv, lt, d);
fun bogus_bind (lv, ve) = ext_dictionary (lv, hcf::truevoid_uniqtypoid, ve);
fun type_in venv' = type_in_dictionary (kenv, venv', d);
fun type_with (v, t) = type_in (hcf::set_uniqtypoid_for_var (venv, v, t, d));
fun mismatch (le, s) (a, r, n, n')
=
err_msg
( le,
cat [s, ": naming/result list mismatch\n** expected ",
int::to_string n, " elements, got ", int::to_string n'],
fold_forward bogus_bind a r
);
fun typeof le
=
{ fun typeof_variable lv
=
hcf::get_uniqtypoid_for_var (venv, lv, d)
except
lt_unbound
=
err_msg (le, "Unbound highcode_variable " + tmp::name_of_highcode_codetemp lv, hcf::truevoid_uniqtypoid);
typeof_val
=
\\ acf::VAR lv => typeof_variable lv;
(acf::INT _ | acf::UNT _) => hcf::int_uniqtypoid;
(acf::INT1 _ | acf::UNT1 _) => hcf::int1_uniqtypoid;
acf::FLOAT64 _ => hcf::float64_uniqtypoid;
acf::STRING _ => hcf::string_uniqtypoid;
end;
fun typeof_fn ve (_, highcode_variable, vts, eb)
=
(ts, type_in ve' eb)
where
fun split ((lv, t), (ve, ts))
=
{ lvar_def le lv;
(hcf::set_uniqtypoid_for_var (ve, lv, t, d), t ! ts);
};
my (ve', ts)
=
fold_backward split (ve,[]) vts;
lvar_def le highcode_variable;
end;
# There are lvars hidden in varhome::Valcon_Form, used by valcon.
# These functions just make sure that they are defined in the
# current environemnent; we don't bother to typecheck them properly XXX BUGGO FIXME
# because supposedly Valcon_Form will go away...
fun check_varhome (vh::HIGHCODE_VARIABLE v) => ignore (typeof_variable v);
check_varhome (vh::PATH (a, _)) => check_varhome a;
check_varhome _ => ();
end;
fun check_conrep (vh::EXCEPTION a)
=>
check_varhome a;
check_conrep (vh::SUSPENSION (THE (a1, a2)))
=>
{ check_varhome a1;
check_varhome a2;
};
check_conrep _
=>
();
end;
fun check_single_inst (fp as (le, s)) (lt, ts) # Check that it yields single result.
=
if (null ts)
#
lt;
else
case (lt_ty_app fp (lt, ts, kenv))
#
[] => hcf::void_uniqtypoid;
[lt] => lt;
lts => err_msg
( le,
cat [s, ": inst yields ", int::to_string (length lts),
" results instead of 1"
],
hcf::truevoid_uniqtypoid
);
esac;
fi;
fun type_with_naming_to_single_rslt_of_inst_and_app (s, lt, ts, vs, lv) e
=
type_with (lv, lt) e
where
fp = (le, s);
lt = case (lt_fn_app fp (check_single_inst fp (lt, ts), map typeof_val vs))
#
[lt] => lt;
_ => err_msg ( le,
cat [s, ": baseop/valcon must return single result type "],
hcf::truevoid_uniqtypoid
);
esac;
# [] => hcf::void_uniqtypoid;
# lts => hcf::make_tuple_uniqtypoid lts;
# ** until BASEOPs start returning multiple results... **
end;
fun match_and_type_with (s, v, lt, lt', lv, e)
=
{ lt_match (le, s) (typeof_val v, lt);
type_with (lv, lt') e;
};
case le
#
acf::RET vs
=>
map typeof_val vs;
acf::LET (lvs, e, e')
=>
{ apply (lvar_def le) lvs;
type_in (foldl2 (ext_dictionary, venv, lvs,
typeof e, mismatch (le, "STIPULATE"))) e';
};
acf::MUTUALLY_RECURSIVE_FNS ([], e)
=>
{ say "\n**** Warning: empty declaration list in acf::MUTUALLY_RECURSIVE_FNS\n";
typeof e;
};
acf::MUTUALLY_RECURSIVE_FNS ((fd as (fk as { loop_info=>NULL, call_as, ... },
lv, _, _)) ! fds', e)
=>
{ my (alts, rlts)
=
typeof_fn venv fd;
lt = lt_arrow (le, "non-rec acf::MUTUALLY_RECURSIVE_FNS") (call_as, alts, rlts);
ve = ext_dictionary (lv, lt, venv);
venv'
=
if (null fds')
ve;
else
err_msg
(le,
"multiple namings in acf::MUTUALLY_RECURSIVE_FNS, not all recursive",
fold_forward (\\ ((_, lv, _, _), ve) => bogus_bind (lv, ve); end ) ve fds');
fi;
type_in venv' e;
};
acf::MUTUALLY_RECURSIVE_FNS (fds, e)
=>
{ isfct = FALSE;
fun ext_dictionary (( { call_as=> acf::CALL_AS_GENERIC_PACKAGE, ... }, _, _, _), _)
=>
bug "unexpected case in extDict";
ext_dictionary (( { loop_info, call_as, ... }, lv, vts, _): acf::Function, ve)
=>
case (loop_info, isfct)
#
(THE (lts, _), FALSE)
=>
{ lt = lt_arrow (le, "acf::MUTUALLY_RECURSIVE_FNS") (call_as, map #2 vts, lts);
hcf::set_uniqtypoid_for_var (ve, lv, lt, d);
};
_ =>
{ msg =
if (isfct)
"recursive generic ";
else
"a non-recursive function ";
fi;
err_msg (le, "in MUTUALLY_RECURSIVE_FNS: " + msg + tmp::name_of_highcode_codetemp lv, ve);
};
esac;
end;
venv' = fold_forward ext_dictionary venv fds;
fun check_dcl (( { loop_info => NULL, ... }, _, _, _): acf::Function)
=>
();
check_dcl (fd as ( { loop_info => THE (lts, _), ... }, _, _, _))
=>
{
lts_match (le, "acf::MUTUALLY_RECURSIVE_FNS") (lts, #2 (typeof_fn venv' fd));
};
end;
apply check_dcl fds;
type_in venv' e;
};
acf::APPLY (v, vs)
=>
lt_fn_app (le, "acf::APPLY") (typeof_val v, map typeof_val vs);
acf::TYPEFUN ((tfk, lv, tks, e), e')
=>
{ fun getkind (tv, tk)
=
{ lvar_def le tv;
tk;
};
ks = map getkind tks;
lts = type_in_dictionary (hut::prepend_uniqkind_list_to_map (kenv, ks), venv, di::next d) e;
lvar_def le lv;
type_with (lv, hcf::make_typeagnostic_uniqtypoid (ks, lts)) e';
};
acf::APPLY_TYPEFUN (v, ts)
=>
lt_ty_app (le, "acf::APPLY_TYPEFUN") (typeof_val v, ts, kenv);
acf::SWITCH (_, _,[], _)
=>
err_msg (le, "empty acf::SWITCH",[]);
acf::SWITCH (v, _, ce ! ces, lo)
=>
{ sel_lty = typeof_val v;
fun g lt
=
{ lt_match (le, "acf::SWITCH branch 1") (lt, sel_lty);
venv;
};
fun br_lts (c, e)
=
{ venv' = case c
#
acf::VAL_CASETAG ((_, pick_valcon_form, lt), ts, v)
=>
{ check_conrep pick_valcon_form;
fp = (le, "acf::SWITCH DECON");
ct = check_single_inst fp (lt, ts);
nts = lt_fn_app_r fp (ct, [sel_lty]);
lvar_def le v;
foldl2 (ext_dictionary, venv, [v], nts, mismatch fp);
};
(acf::INT_CASETAG _ | acf::UNT_CASETAG _) => g hcf::int_uniqtypoid;
(acf::INT1_CASETAG _ | acf::UNT1_CASETAG _) => g hcf::int1_uniqtypoid;
acf::FLOAT64_CASETAG _ => g hcf::float64_uniqtypoid;
acf::STRING_CASETAG _ => g lt_string;
acf::VLEN_CASETAG _ => g hcf::int_uniqtypoid; # ?
esac;
type_in venv' e;
};
ts = br_lts ce;
fun check_branch (ce, n)
=
{ lts_match (le, "acf::SWITCH branch " + int::to_string n) (ts, br_lts ce);
n+1;
};
fold_forward check_branch 2 ces;
case lo
THE e => lts_match (le, "acf::SWITCH else") (ts, typeof e);
NULL => ();
esac;
ts;
};
acf::CONSTRUCTOR ((_, pick_valcon_form, lt), ts, u, lv, e)
=>
{ check_conrep pick_valcon_form;
lvar_def le lv;
type_with_naming_to_single_rslt_of_inst_and_app ("acf::CONSTRUCTOR", lt, ts,[u], lv) e;
};
acf::RECORD (rk, vs, lv, e)
=>
{ lt = case rk
#
acf::RK_VECTOR t
=>
{ lt = hcf::make_type_uniqtypoid t;
match = lt_match (le, "VECTOR");
apply (\\ v = match (lt, typeof_val v))
vs;
lt_vector t;
};
acf::RK_TUPLE _
=>
if (null vs)
#
hcf::void_uniqtypoid;
else
hcf::make_tuple_uniqtypoid (map check_mono vs)
where
fun check_mono v
=
{ t = typeof_val v;
if (hcf::uniqtypoid_is_generic_package t or hcf::uniqtypoid_is_typeagnostic t)
#
error (
le,
{. pr_msg_lt ("RECORD: poly type in mono record:\n", t); }
);
fi;
t;
};
end;
fi;
acf::RK_PACKAGE
=>
hcf::make_package_uniqtypoid (map typeof_val vs);
esac;
lvar_def le lv;
type_with (lv, lt) e;
};
acf::GET_FIELD (v, n, lv, e)
=>
{ lt = catch_exn
{. hcf::lt_get_field (typeof_val v, n); }
( le,
{. say "acf::GET_FIELD from wrong type or out of range";
hcf::truevoid_uniqtypoid;
}
);
lvar_def le lv;
type_with (lv, lt) e;
};
acf::RAISE (v, lts)
=>
{ lt_match (le, "acf::RAISE") (typeof_val v, lt_exn);
lts;
};
acf::EXCEPT (e, v)
=>
{ lts = typeof e;
lt_fn_app_r (le, "acf::EXCEPT") (typeof_val v, lts);
lts;
};
acf::BRANCH ((_, _, lt, ts), vs, e1, e2)
=>
{ fp = (le, "acf::BRANCH");
lt = case (lt_fn_app fp (check_single_inst fp (lt, ts), map typeof_val vs))
#
[lt] => lt;
#
_ => err_msg ( le,
"BRANCH: baseop must return single result ",
hcf::truevoid_uniqtypoid
);
esac;
lt_match fp (lt, lt_bool);
lts1 = typeof e1;
lts2 = typeof e2;
lts_match fp (lts1, lts2);
lts1;
};
acf::BASEOP ((_, hbo::WCAST, lt,[]), [u], lv, e)
=>
# A hack: checked only after reify is done
#
if (later_phase phase)
#
lvar_def le lv;
case (hcf::unpack_generic_package_uniqtypoid lt)
#
([argt], [rt])
=>
{ lt_match (le, "WCAST") (typeof_val u, argt);
type_with (lv, rt) e;
};
_ => bug "unexpected WCAST in typecheck";
esac;
else
bug "unexpected WCAST in typecheck";
fi;
acf::BASEOP ((dc, _, lt, ts), vs, lv, e)
=>
{ # There are lvars hidden inside dicts,
# which we didn't check before.
# This is a first-order check that
# they at least are bound to something;
# for now we don't care about their types.
# (I'm not sure what the rules should look like.) XXX BUGGO FIXME
# --league, 10 april 1998.
#
fun check_symbolmapstack (THE { default, table } )
=>
{ typeof_variable default;
apply (ignore o typeof_variable o #2) table;
};
check_symbolmapstack (NULL: Null_Or( acf::Dictionary ))
=>
();
end;
check_symbolmapstack dc;
lvar_def le lv;
type_with_naming_to_single_rslt_of_inst_and_app ("acf::BASEOP", lt, ts, vs, lv) e;
};
esac;
/*
| acf::GENOP (dictionary, (_, lt, ts), vs, lv, e) =>
# verify dictionary ?
typeWithNamingToSingleRsltOfInstAndApp ("acf::GENOP", lt, ts, vs, lv) e
| EXCEPTION_TAG (t, v, lv, e) =>
matchAndTypeWith ("EXCEPTION_TAG", v, ltString, ltEtag (hcf::make_type_uniqtypoid t), lv, e)
| WRAP (t, v, lv, e) =>
matchAndTypeWith ("WRAP", v, hcf::make_type_uniqtypoid t, ltWrap t, lv, e)
| UNWRAP (t, v, lv, e) =>
matchAndTypeWith ("UNWRAP", v, ltWrap t, hcf::make_type_uniqtypoid t, lv, e)
*/
};
typeof;
};
anyerror := FALSE;
ignore (type_in_dictionary dicts lambda_expression);
*anyerror;
};
herein # toplevel 'stipulate'
#############################################################################
# MAIN FUNCTION --- my checkTop: anormcode::Function_Declaration * typesys -> Bool
#############################################################################
fun check_top ((fkind, v, args, lambda_expression): acf::Function, phase)
=
{ ve = fold_forward
(\\ ((v, t), ve) = hcf::set_uniqtypoid_for_var (ve, v, t, di::top))
hcf::empty_highcode_variable_to_uniqtypoid_map
args;
err = check phase
(hut::empty_debruijn_to_uniqkind_listlist, ve, di::top)
lambda_expression;
err = case fkind
#
{ call_as => acf::CALL_AS_GENERIC_PACKAGE, ... }
=>
err;
_ =>
{ say "**** Not a generic package at top level\n";
TRUE;
};
esac;
err;
};
check_top
=
cos::do_compiler_phase (cos::make_compiler_phase "Compiler 051 HIGHCODECheck") check_top;
###############################################################################
# MAIN FUNCTION
# anormcode::Expression * typesys -> Bool
# (currently unused?)
###############################################################################
fun check_expression (le, phase)
=
check phase (hut::empty_debruijn_to_uniqkind_listlist, hcf::empty_highcode_variable_to_uniqtypoid_map, di::top) le;
end; # stipulate
}; # package type_anormcode
end; # stipulate