Extensibella Example: soundX:host

Language Specification

File: def.sos

[Reduce File] [Raw File] 
Module soundX:host

tm ::= var(string)
     | abs(string, ty, tm)
     | app(tm, tm)
     | num(int)
     | plus(tm, tm)

Projection tm : [(string, ty)]

ty ::= arrowTy(ty, ty)
     | intTy

Projection ty :



Judgment typeOf : [(string, ty)] tm* ty

lookup Ctx X Ty
-------------------- [T-Var]
typeOf Ctx var(X) Ty


typeOf (X, Ty1)::Ctx Body Ty2
---------------------------------------------- [T-Abs]
typeOf Ctx abs(X, Ty1, Body) arrowTy(Ty1, Ty2)


typeOf Ctx T1 arrowTy(Ty1, Ty2)
typeOf Ctx T2 Ty1
------------------------------- [T-App]
typeOf Ctx app(T1, T2) Ty2


----------------------- [T-Num]
typeOf Ctx num(I) intTy


typeOf Ctx T1 intTy
typeOf Ctx T2 intTy
----------------------------- [T-Plus]
typeOf Ctx plus(T1, T2) intTy





/*
  Desugaring removes all the extension-introduced syntax constructors
  by desugaring sub-terms of known constructors and projecting terms
  built by extension-introduced constructors, then desugaring their
  projections.
*/
Fixed Judgment desugar_tm : [(string, ty)] tm tm
Fixed Judgment desugar_ty : ty ty
Fixed Judgment desugar_ctx : [(string, ty)] [(string, ty)]

============================ [DTm-Var]
desugar_tm Ctx var(X) var(X)


desugar_ty Ty DTy
desugar_tm (X, Ty)::Ctx Tm DTm
============================================== [DTm-Abs]
desugar_tm Ctx abs(X, Ty, Tm) abs(X, DTy, DTm)


desugar_tm Ctx A DA
desugar_tm Ctx B DB
==================================== [DTm-App]
desugar_tm Ctx app(A, B) app(DA, DB)


============================ [DTm-Num]
desugar_tm Ctx num(I) num(I)


desugar_tm Ctx A DA
desugar_tm Ctx B DB
====================================== [DTm-Plus]
desugar_tm Ctx plus(A, B) plus(DA, DB)


Ctx |{tm}- T ~~> T_P
desugar_tm Ctx T_P DT
===================== [DTm-Proj]
desugar_tm Ctx T DT



desugar_ty A DA
desugar_ty B DB
======================================== [DTy-Arrow]
desugar_ty arrowTy(A, B) arrowTy(DA, DB)


====================== [DTy-Int]
desugar_ty intTy intTy


|{ty}- Ty ~~> Ty_P
desugar_ty Ty_P DTy
=================== [DTy-Proj]
desugar_ty Ty DTy



================= [DCtx-Nil]
desugar_ctx [] []


desugar_ty Ty DTy
desugar_ctx Rest DRest
========================================= [DCtx-Cons]
desugar_ctx (X, Ty)::Rest (X, DTy)::DRest





/*
  Because extensions can only add new constructs and typing rules,
  evaluation and related judgments are defined as fixed.
*/
Fixed Judgment eval : tm tm
Fixed Judgment subst : string tm tm tm
Fixed Judgment value : tm

eval T1 T11
============================= [E-App-Step1]
eval app(T1, T2) app(T11, T2)


value T1
eval T2 T21
============================= [E-App-Step2]
eval app(T1, T2) app(T1, T21)


value T2
subst X T2 Body V
================================ [E-App-Subst]
eval app(abs(X, Ty, Body), T2) V


eval T1 T11
=============================== [E-Plus-Step1]
eval plus(T1, T2) plus(T11, T2)


value T1
eval T2 T21
=============================== [E-Plus-Step2]
eval plus(T1, T2) plus(T1, T21)


I1 + I2 = I
================================== [E-Plus-Add]
eval plus(num(I1), num(I2)) num(I)



X != Y
======================= [S-Var-NEq]
subst X R var(Y) var(Y)


================== [S-Var-Eq]
subst X R var(X) R


X != Y
subst X R B S
===================================== [S-Abs-NEq]
subst X R abs(Y, Ty, B) abs(Y, Ty, S)


===================================== [S-Abs-Eq]
subst X R abs(X, Ty, B) abs(X, Ty, B)


subst X R T1 S1
subst X R T2 S2
================================= [S-App]
subst X R app(T1, T2) app(S1, S2)


======================= [S-Num]
subst X R num(I) num(I)


subst X R T1 S1
subst X R T2 S2
=================================== [S-Plus]
subst X R plus(T1, T2) plus(S1, S2)



=================== [V-Abs]
value abs(X, Ty, T)


============ [V-Num]
value num(I)

Reasoning

[Show All Proofs] [Hide All Proofs] [Raw File]

Click on a command or tactic to see a detailed view of its use.

Module soundX:host.

/********************************************************************
 We prove properties about typing, as well as projection constraints,
 for all constructs, regardless of which module is introducing them.
 ********************************************************************/
Theorem lookup_ty_is : forall Ctx X Ty,
  is_list (is_pair is_string is_ty) Ctx -> lookup Ctx X Ty ->
  is_ty Ty. [Show Proof]



Projection_Constraint
  proj_ty_is : forall Ty Ty',
    Proj : |{ty}- Ty ~~> Ty' ->
    IsTy : is_ty Ty ->
    is_ty Ty'.


/*
  This goes before proj_is because projection might depend on the
  context, and thus the type, so we might need this to prove that.
*/
Extensible_Theorem
  type_is : forall Ctx T Ty,
    IsCtx : is_list (is_pair is_string is_ty) Ctx ->
    IsT : is_tm T ->
    Ty : typeOf Ctx T Ty ->
    is_ty Ty
  on Ty. [Show Proof]



Projection_Constraint
  proj_is : forall Ctx T T',
    Proj : Ctx |{tm}- T ~~> T' ->
    IsCtx : is_list (is_pair is_string is_ty) Ctx ->
    IsT : is_tm T ->
    is_tm T'.


Extensible_Theorem
  type_unique : forall Ctx T TyA TyB,
    IsCtx : is_list (is_pair is_string is_ty) Ctx ->
    IsT : is_tm T ->
    TyA : typeOf Ctx T TyA ->
    TyB : typeOf Ctx T TyB ->
    TyA = TyB
  on TyA. [Show Proof]



Extensible_Theorem
  ty_lookup : forall Ctx1 Ctx2 T Ty,
    Ty : typeOf Ctx1 T Ty ->
    L : (forall X XTy, lookup Ctx1 X XTy -> lookup Ctx2 X XTy) ->
    typeOf Ctx2 T Ty
  on Ty. [Show Proof]



Theorem empty_ty_any : forall T Ty Ctx,
  typeOf [] T Ty -> typeOf Ctx T Ty. [Show Proof]



Projection_Constraint proj_ty_unique : forall Ty TyA TyB,
  |{ty}- Ty ~~> TyA -> |{ty}- Ty ~~> TyB -> is_ty Ty -> TyA = TyB.


Projection_Constraint proj_tm_unique : forall Ctx T TA TB,
  Ctx |{tm}- T ~~> TA -> Ctx |{tm}- T ~~> TB ->
  is_tm T -> is_list (is_pair is_string is_ty) Ctx -> TA = TB.



/********************************************************************
 Everything is desugared before we get to evaluation, and we need
 some properties about desugarings.
 ********************************************************************/
Theorem lookup_desugar_ctx : forall Ctx X Ty Ctx',
  lookup Ctx X Ty -> desugar_ctx Ctx Ctx' ->
  exists Ty', lookup Ctx' X Ty' /\ desugar_ty Ty Ty'. [Show Proof]


Theorem desugar_ty_unique : forall Ty TyA TyB,
  is_ty Ty -> desugar_ty Ty TyA -> desugar_ty Ty TyB -> TyA = TyB. [Show Proof]


Theorem desugar_tm_unique : forall Ctx T TA TB,
  is_list (is_pair is_string is_ty) Ctx -> is_tm T ->
  desugar_tm Ctx T TA -> desugar_tm Ctx T TB -> TA = TB. [Show Proof]


Extensible_Theorem
  desugar_ty_exists : forall Ty,
    IsTy : is_ty Ty ->
    exists Ty', desugar_ty Ty Ty'
  on IsTy. [Show Proof]



%These are like the is_tm and is_ty predicates Sterling generates, but
%only for the host language's constructs.
Define host_is_ty : ty -> prop by
host_is_ty (arrowTy Ty1 Ty2) := host_is_ty Ty1 /\ host_is_ty Ty2;
host_is_ty intTy.
Define host_is_tm : tm -> prop by
host_is_tm (var X) := is_string X;
host_is_tm (abs X Ty B) :=
  is_string X /\ host_is_ty Ty /\ host_is_tm B;
host_is_tm (app A B) := host_is_tm A /\ host_is_tm B;
host_is_tm (num I) := is_integer I;
host_is_tm (plus A B) := host_is_tm A /\ host_is_tm B.


Theorem desugar_ty_host_is_ty : forall Ty DTy,
  is_ty Ty -> desugar_ty Ty DTy -> host_is_ty DTy. [Show Proof]


Theorem desugar_tm_host_is_tm : forall Ctx T DT,
  is_tm T -> is_list (is_pair is_string is_ty) Ctx ->
  desugar_tm Ctx T DT -> host_is_tm DT. [Show Proof]



/********************************************************************
 SoundX's Property:
 Desugared terms have desugared types
 ********************************************************************/
Extensible_Theorem
  desugar_ty_rel : forall Ctx T Ty T' Ty' Ctx',
    IsT : is_tm T ->
    IsCtx : is_list (is_pair is_string is_ty) Ctx ->
    Ty : typeOf Ctx T Ty ->
    DT : desugar_tm Ctx T T' ->
    DTy : desugar_ty Ty Ty' ->
    DCtx : desugar_ctx Ctx Ctx' ->
    typeOf Ctx' T' Ty'
  on Ty. [Show Proof]



/********************************************************************
 We can prove properties about evaluation and substitution for the
 host language alone because everything is desugared before we
 evaluate it.
 ********************************************************************/
Theorem subst_is : forall X R T S,
  is_tm T -> is_string X -> is_tm R -> subst X R T S -> is_tm S. [Show Proof]



Theorem eval_is : forall T T',
  is_tm T -> eval T T' -> is_tm T'. [Show Proof]



Theorem subst_unique : forall X R T VA VB,
  subst X R T VA -> subst X R T VB -> VA = VB. [Show Proof]



Theorem value_eval_false : forall T V,
  value T -> eval T V -> false. [Show Proof]



Theorem eval_unique : forall T VA VB,
  eval T VA -> eval T VB -> VA = VB. [Show Proof]



Theorem subst_type_preservation : forall T Ctx X XTy Ty R S,
  typeOf ((X, XTy)::Ctx) T Ty -> subst X R T S -> typeOf [] R XTy ->
  typeOf Ctx S Ty. [Show Proof]

  
  
Theorem type_preservation : forall T Ty T',
  typeOf [] T Ty -> eval T T' -> typeOf [] T' Ty. [Show Proof]



Theorem subst_total : forall X R T,
  host_is_tm T -> is_string X -> exists S, subst X R T S. [Show Proof]



Theorem canonical_form_intTy : forall V,
  value V -> typeOf [] V intTy -> exists I, V = num(I). [Show Proof]


Theorem canonical_form_arrowTy : forall V Ty1 Ty2,
  value V -> typeOf [] V (arrowTy Ty1 Ty2) ->
  exists X B, V = abs X Ty1 B. [Show Proof]



Theorem progress : forall T Ty,
  host_is_tm T -> typeOf [] T Ty -> (exists T', eval T T') \/ value T. [Show Proof]
Back to example home