Due to space restrictions we only present the crucial components of the system: the part that contains effect handling using monads and the partial evaluator that makes use of it.
The whole framework consists of currently 20 modules that contain about 2000 lines of code (including many comments and empty lines).
The implementation will be available from the Department of Artificial Intelligence at the University of Edinburgh.
sig effect_monad. % EFFECT MONAD % The effect monad guarantees that computational effects are hidden from % predicates to which "bind" passes terms: in other terms, these terms % are guaranteed to be values. The specific implementation here makes % a distinction between values (do not require computation) possibly % non-terminating computations and other computations. The reason for % the latter is that "computations" that cannot be done statically % (reduced to a value) might induce non-linearity if they are applied % without restrictions. kind effM type -> type. % kind of effect monads % MONAD REPRESENTATION type value_effM A -> effM A. type mnont_effM A -> (A -> effM A) -> effM A. type comp_effM A -> (A -> effM A) -> effM A. % MONAD OPERATORS % [unit_value_effM +T ?M] lifts term [T] to the computation (value of % monadic type) [M], indicating that [T] is a value. type unit_value_effM A -> effM A -> o. % [unit_mnont_effM +T ?M] lifts term [T] to the computation [M], % indicating that evaluating it may cause non-termination. type unit_mnont_effM A -> effM A -> o. % [unit_comp_effM +T ?M] lifts term [T] to the computation [M], indicating % that it still requires (terminating) computation to become completely % reduced. type unit_comp_effM A -> effM A -> o. % [bind_effM +MA +P ?MB] binds the computation [MA] to predicate [P], % returning the resulting value of monadic type in [MB]. type bind_effM effM A -> (A -> effM B -> o) -> effM B -> o. % ADDITIONAL FUNCTIONS % [show_effM +MA ?A] converts the representation of computation [MA] % to a value [A] of the type on which the effect monad operates. Has to % be provided by the user! type show_effM effM A -> A -> o. % [lifted_term +V ?T] gets the term [T] that has been lifted out of a % computation using variable [V] in its place. type lifted_term A -> A -> o.
module effect_monad.
unit_value_effM T (value_effM T).
unit_mnont_effM T (mnont_effM T value_effM).
unit_comp_effM T (comp_effM T value_effM).
bind_effM (value_effM T) K Res :- K T Res.
bind_effM (mnont_effM T F1) K (mnont_effM T Res) :-
pi lt\ sigma R\
lifted_term lt T =>
bind_effM (F1 lt) K R,
( % CASE: result of binding is a value
value_effM (F2 lt) = R,
Res = (t\ value_effM (F2 t))
; % CASE: result of binding maybe non-termination or computation
C (F2 lt) (F3 lt) = R,
Res = (t\ C (F2 t) (F3 t))
).
bind_effM (comp_effM T F1) K Res :-
pi lt\ sigma R\
lifted_term lt T =>
bind_effM (F1 lt) K R,
( % CASE: R does not contain lifted term
Res = R
; % CASE: R contains lifted term
( % CASE: result of binding is a value
value_effM (F2 lt) = R,
Res = comp_effM T (t\ value_effM (F2 t))
; % CASE: result of binding maybe non-termination or computation
C (F2 lt) (F3 lt) = R,
Res = comp_effM T (t\ C (F2 t) (F3 t))
)
).
sig part_eval. accum_sig let_ext. accum_sig effect_monad. % PARTIAL EVALUATION WITH EFFECT ANALYSIS % [part_eval +T1 ?T2] partially evaluates term [T1] to [T2]. The % effect behaviour (non-termination, impureness) of [T1] is % preserved. Side-effecting terms are lifted to the outermost level % (toplevel or function abstractions). See module "let_ext" for additional % terms associated with lifting out side effects. type part_eval tm -> tm -> o. % [part_eval_fun +F1 ?F2] partially evaluates term function [F1] to % [F2]. The effect behaviour (non-termination, impureness) of [F1] % is preserved. type part_eval_fun (tm -> tm) -> (tm -> tm) -> o. % [funcall_terminates +F +T] checks whether function [F] (in term % representation) terminates when applied to term [T]. There are % no defaults for this, of course, but you may "plug in" your own % termination analyser. type funcall_terminates tm -> tm -> o.
module part_eval.
accumulate utils.
accumulate let_ext.
accumulate effect_monad.
% PART_EVAL
part_eval T1 T2 :-
part_evalM T1 M,
show_effM M T2.
% PART_EVALM
type part_evalM tm -> effM tm -> o.
part_evalM T Res :-
T = u,
unit_value_effM T Res.
part_evalM (pair T1 T2) Res :-
part_evalM T1 M1,
part_evalM T2 M2,
bind_effM M1 (V1\ bind_effM M2 (simplify_pair V1)) Res.
part_evalM (fst T) Res :-
part_evalM T M,
bind_effM M simplify_fst Res.
part_evalM (snd T) Res :-
part_evalM T M,
bind_effM M simplify_snd Res.
part_evalM (inl T) Res :-
part_evalM T M,
bind_effM M (V\ unit_value_effM (inl V)) Res.
part_evalM (inr T) Res :-
part_evalM T M,
bind_effM M (V\ unit_value_effM (inr V)) Res.
part_evalM (case CT LF RF) Res :-
part_evalM CT M,
bind_effM M (CV\ simplify_case CV LF RF) Res.
part_evalM (lam F1) Res :-
part_eval_fun F1 F2,
unit_value_effM (lam F2) Res.
part_evalM (rec F1) Res :-
pi f\ sigma Mf\
unit_comp_effM f Mf,
part_evalM f Mf =>
sigma Fx\
part_eval_fun (F1 f) Fx,
( % CASE: function not recursive anymore -> normal function
unit_value_effM (lam Fx) Res
; % CASE: function still potentially recursive
F2 f = Fx,
unit_comp_effM (rec F2) Res
).
part_evalM (app T1 T2) Res :-
part_evalM T1 M1,
part_evalM T2 M2,
bind_effM M1 (V1\ bind_effM M2 (simplify_app V1)) Res.
part_evalM (abs_rtp T) Res :-
part_evalM T M,
bind_effM M (V\ unit_value_effM (abs_rtp V)) Res.
part_evalM (rep_rtp T) Res :-
part_evalM T M,
bind_effM M simplify_rep_rtp Res.
% PART_EVAL_FUN
part_eval_fun F1 F2 :-
pi x\ sigma Mx\
unit_value_effM x Mx,
part_evalM x Mx =>
sigma M\
part_evalM (F1 x) M,
show_effM M (F2 x).
% SIMPLIFICATION RULES
type simplify_pair tm -> tm -> effM tm -> o.
type simplify_fst tm -> effM tm -> o.
type simplify_snd tm -> effM tm -> o.
type simplify_case tm -> (tm -> tm) -> (tm -> tm) -> effM tm -> o.
type simplify_case_arm tm -> (tm -> tm) -> (tm -> tm) -> (tm -> tm) -> o.
type simplify_case_arms tm -> (tm -> tm) -> (tm -> tm) -> effM tm -> o.
type simplify_app tm -> tm -> effM tm -> o.
type simplify_term_app tm -> tm -> effM tm -> o.
type simplify_rep_rtp tm -> effM tm -> o.
% Pair reconstructs its destructed form -> simplify.
% This is safe, because V, too, is guaranteed to be a value!
simplify_pair V1 V2 Res :-
lifted_term V1 (fst V),
lifted_term V2 (snd V),
!,
unit_value_effM V Res.
simplify_pair V1 V2 Res :- unit_value_effM (pair V1 V2) Res.
simplify_fst (pair V1 _V2) Res :- !, unit_value_effM V1 Res.
simplify_fst V Res :- unit_comp_effM (fst V) Res.
simplify_snd (pair _V1 V2) Res :- !, unit_value_effM V2 Res.
simplify_snd V Res :- unit_comp_effM (snd V) Res.
simplify_case (inl V) LF _RF Res :- !, part_evalM (LF V) Res.
simplify_case (inr V) _LF RF Res :- !, part_evalM (RF V) Res.
% Condition not reducable to choice.
simplify_case CV LF1 RF1 Res :-
part_eval_fun LF1 LF2,
part_eval_fun RF1 RF2,
simplify_case_arm CV LF2 inl LF3,
simplify_case_arm CV RF2 inr RF3,
simplify_case_arms CV LF3 RF3 Res.
% Case arm a function of condition.
simplify_case_arm CV F1 Make F2 :-
pi x\ sigma Mx\
unit_value_effM x Mx,
part_evalM x Mx =>
sigma F\ sigma M\
elim_sub_term (F1 x) (Make x) F,
!,
part_evalM (F CV) M,
show_effM M (F2 x).
% Case arm not a function of condition.
simplify_case_arm _CV F _Make F.
% Left and right case arm equivalent.
simplify_case_arms CV LF RF Res :-
pi l\ pi r\
EQ = LF l,
EQ = RF r,
!,
part_evalM EQ Res.
% Case arms not equivalent.
simplify_case_arms CV LF RF Res :- unit_comp_effM (case CV LF RF) Res.
% Application of simple lambda abstraction.
simplify_app (lam F) V Res :- !, part_evalM (F V) Res.
% Terminating function applications.
simplify_app FV V Res :-
funcall_terminates FV V,
!,
simplify_term_app FV V Res.
% Maybe non-terminating function applications.
simplify_app FV V Res :- unit_mnont_effM (app FV V) Res.
% Terminating recursive function application.
simplify_term_app FV V Res :-
FV = rec F,
!,
part_evalM (F FV V) Res.
% Terminating unknown function.
simplify_term_app FV V Res :- unit_comp_effM (app FV V) Res.
simplify_rep_rtp (abs_rtp V) Res :- !, unit_value_effM V Res.
simplify_rep_rtp V Res :- unit_comp_effM (rep_rtp V) Res.
% SHOW_EFFM
show_effM (value_effM T) T.
show_effM (mnont_effM T F) (let_mnont T G) :- pi t\ show_effM (F t) (G t).
show_effM (comp_effM T F) (let_comp T G) :- pi t\ show_effM (F t) (G t).
% SPECIAL RULES FOR LIFTED TERMS
part_evalM LT Res :-
(
let T F = LT
;
let_mnont T F = LT
;
let_comp T F = LT
),
part_evalM T M,
bind_effM M (V\ part_evalM (F V)) Res.
part_evalM LT Res :-
lifted_term LT _T,
unit_value_effM LT Res.