| Low-level lambda calculus with imperative memory access |
Require Import Arith List.
Require Import Binding.
Require Import MemMonad.
Set Implicit Arguments.
The language |
There's nothing new here compared to PSLC. The definitions follow the
challenge statement.
|
Inductive idty : Set :=
| IUnit : idty
| INat : idty.
Inductive ity : Set :=
| IData : idty -> ity
| IArrow : ity -> ity -> ity.
Inductive iterm : list ity -> ity -> Set :=
| IVar : forall G t,
Var G t
-> iterm G t
| ILam : forall G dom ran,
iterm (dom :: G) ran
-> iterm G (IArrow dom ran)
| IApp : forall G dom ran,
iterm G (IArrow dom ran)
-> iterm G dom
-> iterm G ran
| IUnitE : forall G,
iterm G (IData IUnit)
| IConst : forall G,
nat
-> iterm G (IData INat)
| ISucc : forall G,
iterm G (IData INat)
-> iterm G (IData INat)
| IWrite : forall G,
iterm G (IData INat)
-> iterm G (IData INat)
-> iterm G (IData IUnit)
| IRead : forall G,
iterm G (IData INat)
-> iterm G (IData INat)
| ISeq : forall G t,
iterm G (IData IUnit)
-> iterm G t
-> iterm G t
| IIf : forall G t,
iterm G (IData INat)
-> iterm G t
-> iterm G t
-> iterm G t.
Denotational semantics |
For Imp, we give separate meta-language types for values and expressions
of an object-language type.
Values represent finished computations, while the type of every expression
reflects that it is a monadic computation that may have side effects.
|
Definition idvalDenote (t : idty) : Set :=
match t with
| IUnit => unit
| INat => nat
end.
| The main interesting aspect below is that, even though we're considering values, we give functions monadic types. |
Fixpoint ivalDenote (t : ity) : Set :=
match t with
| IData t => idvalDenote t
| IArrow t1 t2 => ivalDenote t1 -> memM (ivalDenote t2)
end.
| This is the type schema of expressions; each is a monadic computation. |
Definition ityDenote t := memM (ivalDenote t).
The semantics of expressions should be unsurprising. Note that the
substitutions associate values with free variables, while the
result type of itermDenote expresses that we are returning
expressions.
The syntactic shorthands for monadic bind operations are put to good use here.
Note that, like in the Haskell IO monad, arbitrary Coq computations are
allowed inside monadic values, as seen in the IIf case.
|
Fixpoint itermDenote (G : list ity) (t : ity) (e : iterm G t) {struct e}
: Subst ivalDenote G -> ityDenote t :=
match e in (iterm G t) return (Subst ivalDenote G -> ityDenote t) with
| IVar _ _ v => fun s => Return (VarDenote v s)
| ILam _ _ _ e' => fun s => Return (fun x => itermDenote e' (SCons _ x s))
| IApp _ _ _ e1 e2 => fun s =>
v1 <- itermDenote e1 s;
v2 <- itermDenote e2 s;
v1 v2
| IUnitE _ => fun _ => Return tt
| IConst _ n => fun _ => Return n
| ISucc _ e => fun s =>
v <- itermDenote e s;
Return (S v)
| IWrite _ dst src => fun s =>
vDst <- itermDenote dst s;
vSrc <- itermDenote src s;
Write vDst vSrc
| IRead _ src => fun s =>
vSrc <- itermDenote src s;
Read vSrc
| ISeq _ _ e1 e2 => fun s =>
itermDenote e1 s;;
itermDenote e2 s
| IIf _ _ e e1 e2 => fun s =>
v <- itermDenote e s;
match v with
| S _ => itermDenote e1 s
| _ => itermDenote e2 s
end
end.