Theory Execute
theory Execute
imports POPLmarkRecord "HOL-Library.Code_Target_Numeral"
begin
section ‹Executing the specification›
text ‹
\label{sec:exec}
An important criterion that a solution to the {\sc PoplMark} Challenge should
fulfill is the possibility to {\it animate} the specification. For example,
it should be possible to apply the reduction relation for the calculus to
example terms. Since the reduction relations are defined inductively, they can
be interpreted as a logic program in the style of {\sc Prolog}.
The definition of the single-step evaluation relation presented in \secref{sec:evaluation}
and \secref{sec:evaluation-rcd} is directly executable.
In order to compute the normal form of a term using the one-step evaluation
relation ‹⟼›, we introduce the inductive predicate ‹t ⇓ u›,
denoting that ‹u› is a normal form of ‹t›.
›
inductive norm :: "trm ⇒ trm ⇒ bool" (infixl "⇓" 50)
where
"t ∈ value ⟹ t ⇓ t"
| "t ⟼ s ⟹ s ⇓ u ⟹ t ⇓ u"
definition normal_forms where
"normal_forms t ≡ {u. t ⇓ u}"
lemma [code_pred_intro Rcd_Nil]: "valuep (Rcd [])"
by (auto intro: valuep.intros)
lemma [code_pred_intro Rcd_Cons]: "valuep t ⟹ valuep (Rcd fs) ⟹ valuep (Rcd ((l, t) # fs))"
by (auto intro!: valuep.intros elim!: valuep.cases)
lemmas valuep.intros(1)[code_pred_intro Abs'] valuep.intros(2)[code_pred_intro TAbs']
code_pred (modes: i => bool) valuep
proof -
case valuep
from valuep.prems show thesis
proof (cases rule: valuep.cases)
case (Rcd fs)
from this valuep.Rcd_Nil valuep.Rcd_Cons show thesis
by (cases fs) (auto intro: valuep.intros)
next
case Abs
with valuep.Abs' show thesis .
next
case TAbs
with valuep.TAbs' show thesis .
qed
qed
thm valuep.equation
code_pred (modes: i => i => bool, i => o => bool as normalize) norm .
thm norm.equation
lemma [code]:
"normal_forms = set_of_pred o normalize"
unfolding set_of_pred_def o_def normal_forms_def [abs_def]
by (auto intro: set_eqI normalizeI elim: normalizeE)
lemma [code_unfold]: "x ∈ value ⟷ valuep x"
by (simp add: value_def)
definition
natT :: type where
"natT ≡ ∀<:Top. (∀<:TVar 0. (∀<:TVar 1. (TVar 2 → TVar 1) → TVar 0 → TVar 1))"
definition
fact2 :: trm where
"fact2 ≡
LET PVar natT =
(λ<:Top. λ<:TVar 0. λ<:TVar 1. λ:TVar 2 → TVar 1. λ: TVar 1. Var 1 ∙ Var 0)
IN
LET PRcd
[(''pluspp'', PVar (natT → natT → natT)),
(''multpp'', PVar (natT → natT → natT))] = Rcd
[(''multpp'', λ:natT. λ:natT. λ<:Top. λ<:TVar 0. λ<:TVar 1. λ:TVar 2 → TVar 1.
Var 5 ∙⇩τ TVar 3 ∙⇩τ TVar 2 ∙⇩τ TVar 1 ∙ (Var 4 ∙⇩τ TVar 3 ∙⇩τ TVar 2 ∙⇩τ TVar 1) ∙ Var 0),
(''pluspp'', λ:natT. λ:natT. λ<:Top. λ<:TVar 0. λ<:TVar 1. λ:TVar 2 → TVar 1. λ:TVar 1.
Var 6 ∙⇩τ TVar 4 ∙⇩τ TVar 3 ∙⇩τ TVar 3 ∙ Var 1 ∙
(Var 5 ∙⇩τ TVar 4 ∙⇩τ TVar 3 ∙⇩τ TVar 2 ∙ Var 1 ∙ Var 0))]
IN
Var 0 ∙ (Var 1 ∙ Var 2 ∙ Var 2) ∙ Var 2"
value "normal_forms fact2"
text ‹
Unfortunately, the definition based
on evaluation contexts from \secref{sec:evaluation-ctxt} is not directly executable.
The reason is that from the definition of evaluation contexts, the code generator
cannot immediately read off an algorithm that, given a term ‹t›, computes a context
‹E› and a term ‹t⇩0› such that ‹t = E t⇩0›. In order to do this, one
would have to extract the algorithm contained in the proof of the {\it decomposition lemma}
from \secref{sec:evaluation-ctxt}.
›
values "{u. norm fact2 u}"
end