Sterling Example: simple_imp:host

File: syntax.sos

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

/*Expressions*/
e ::= num(int)
    | plus(e, e)
    | name(string)
    | greater(e, e)
    | eq(e, e)
    | and(e, e)
    | or(e, e)
    | true
    | false
    | recBuild(recFieldExprs)
    | recFieldAccess(e, string)
Projection e :

recFieldExprs ::= endRecFieldExprs
                | addRecFieldExprs(string, e, recFieldExprs)
Projection recFieldExprs :


/*Statement Commands*/
c ::= noop
    | seq(c, c)
    | declare(string, ty, e)
    | assign(string, e)
    | ifThenElse(e, c, c)
    | while(e, c)
    | recUpdate(string, recFields, e) /*rec.field = e*/
Projection c :

recFields ::= oneField(string)
            | addField(string, recFields)
Projection recFields :


/*Types*/
ty ::= intTy
     | boolTy
     | recTy([(string, ty)])
Projection ty :


/*Evaluation Values*/
value ::= intVal(int)
        | trueVal
        | falseVal
        | recVal([(string, value)])
Projection value :

File: vars.sos

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


Judgment vars : e* [string]
Judgment vars_rf : recFieldExprs* [string]


/*Vars in Expressions*/

-------------- [V-Num]
vars num(I) []


vars E1 D1
vars E2 D2
D1 ++ D2 = D
------------------- [V-Plus]
vars plus(E1, E2) D


---------------- [V-Name]
vars name(X) [X]


vars E1 D1
vars E2 D2
D1 ++ D2 = D
---------------------- [V-Greater]
vars greater(E1, E2) D


vars E1 D1
vars E2 D2
D1 ++ D2 = D
------------------- [V-Eq]
vars eq(E1, E2) D


vars E1 D1
vars E2 D2
D1 ++ D2 = D
------------------- [V-And]
vars and(E1, E2) D


vars E1 D1
vars E2 D2
D1 ++ D2 = D
------------------- [V-Or]
vars or(E1, E2) D


------------ [V-True]
vars true []


------------- [V-False]
vars false []


vars_rf Fields D
----------------------- [V-RecBuild]
vars recBuild(Fields) D


vars Rec D
--------------------------------- [V-RecAccess]
vars recFieldAccess(Rec, Field) D



/*Vars in Record Fields*/

--------------------------- [VRF-Empty]
vars_rf endRecFieldExprs []


vars_rf Rest DRest
vars E DE
DE ++ DRest = D
-------------------------------------- [VRF-Add]
vars_rf addRecFieldExprs(X, E, Rest) D

File: typing.sos

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

Judgment typeOf : [(string, ty)] e* ty
Judgment typeRecFields : [(string, ty)] recFieldExprs* [(string, ty)]
Judgment typeOK : [(string, ty)] c* [(string, ty)]


/*Expression Typing*/

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


typeOf G E1 intTy
typeOf G E2 intTy
--------------------------- [T-Plus]
typeOf G plus(E1, E2) intTy


lookup G X Ty
------------------- [T-Name]
typeOf G name(X) Ty


typeOf G E1 intTy
typeOf G E2 intTy
------------------------------- [T-Greater]
typeOf G greater(E1, E2) boolTy


typeOf G E1 Ty
typeOf G E2 Ty
-------------------------- [T-Eq]
typeOf G eq(E1, E2) boolTy


typeOf G E1 boolTy
typeOf G E2 boolTy
--------------------------- [T-And]
typeOf G and(E1, E2) boolTy


typeOf G E1 boolTy
typeOf G E2 boolTy
-------------------------- [T-Or]
typeOf G or(E1, E2) boolTy


-------------------- [T-True]
typeOf G true boolTy


--------------------- [T-False]
typeOf G false boolTy


typeRecFields G Fields FTys
------------------------------------- [T-RecBuild]
typeOf G recBuild(Fields) recTy(FTys)


typeOf G Rec recTy(Fields)
lookup Fields Field FTy
--------------------------------------- [T-RecField]
typeOf G recFieldAccess(Rec, Field) FTy



/*Record Field Typing*/

----------------------------------- [TRF-End]
typeRecFields G endRecFieldExprs []


typeOf G E Ty
typeRecFields G Rest FTys
no_lookup FTys L /*each label only occurs once*/
---------------------------------------------------------- [TRF-Add]
typeRecFields G addRecFieldExprs(L, E, Rest) (L, Ty)::FTys



/*Statement Typing*/

--------------- [T-Noop]
typeOK G noop G


typeOK G C1 G1
typeOK G1 C2 G2
----------------------- [T-Seq]
typeOK G seq(C1, C2) G2


no_lookup G X /*can't overwrite existing decls*/
typeOf G E Ty
------------------------------------- [T-Declare]
typeOK G declare(X, Ty, E) (X, Ty)::G


typeOf G E Ty
lookup G X Ty
----------------------- [T-Assign]
typeOK G assign(X, E) G


typeOf G Cond boolTy
typeOK G Then GT
typeOK G Else GE
--------------------------------------- [T-IfThenElse]
typeOK G ifThenElse(Cond, Then, Else) G
/*branches open new scopes*/


typeOf G Cond boolTy
typeOK G Body GB
---------------------------- [T-While]
typeOK G while(Cond, Body) G
/*body opens a new scope*/


lookup G Rec recTy(FFields)
checkRecUpdate Fields FFields Ty
typeOf G E Ty
------------------------------------ [T-RecUpdate]
typeOK G recUpdate(Rec, Fields, E) G



/*Check whether the update to the nested fields is valid
  The tyctx is the fields of the record*/
Judgment checkRecUpdate : recFields* [(string, ty)] ty

lookup RecFieldTys F Ty
----------------------------------------- [CRU-OneField]
checkRecUpdate oneField(F) RecFieldTys Ty


lookup RecFieldTys F recTy(FFieldTys)
checkRecUpdate Rest FFieldTys Ty
----------------------------------------------- [CRU-AddField]
checkRecUpdate addField(F, Rest) RecFieldTys Ty




/*Typing for values to allow type soundness*/
Judgment typeOfVal : value* ty

------------------------- [TV-Int]
typeOfVal intVal(I) intTy


------------------------ [TV-True]
typeOfVal trueVal boolTy


------------------------- [TV-False]
typeOfVal falseVal boolTy


typeOfEvalctx Fields FTys
------------------------------------ [TV-Rec]
typeOfVal recVal(Fields) recTy(FTys)




/*Typing for evaluation contexts to allow recVal typing*/
Fixed Judgment typeOfEvalctx : [(string, value)] [(string, ty)]

=================== [TEC-Empty]
typeOfEvalctx [] []


typeOfVal V Ty
typeOfEvalctx Rest RestTys
=========================================== [TEC-Add]
typeOfEvalctx (X, V)::Rest (X, Ty)::RestTys

File: eval.sos

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

Judgment eval_e : [(string, value)] e* value
Judgment eval_rf : [(string, value)] recFieldExprs* [(string, value)]
Judgment eval_c : [(string, value)] c* [(string, value)]


/*Expression Evaluation*/

------------------------- [E-Num]
eval_e G num(I) intVal(I)


eval_e G E1 intVal(I1)
eval_e G E2 intVal(I2)
I1 + I2 = I
------------------------------- [E-Plus]
eval_e G plus(E1, E2) intVal(I)


lookup G X V
------------------ [E-Name]
eval_e G name(X) V


eval_e G E1 intVal(I1)
eval_e G E2 intVal(I2)
I1 > I2
-------------------------------- [E-GreaterTrue]
eval_e G greater(E1, E2) trueVal


eval_e G E1 intVal(I1)
eval_e G E2 intVal(I2)
I1 <= I2
--------------------------------- [E-GreaterFalse]
eval_e G greater(E1, E2) falseVal


eval_e G E1 V1
eval_e G E2 V2
val_eq V1 V2
--------------------------- [E-EqTrue]
eval_e G eq(E1, E2) trueVal


eval_e G E1 V1
eval_e G E2 V2
! val_eq V1 V2
---------------------------- [E-EqFalse]
eval_e G eq(E1, E2) falseVal


eval_e G E1 trueVal
eval_e G E2 trueVal
---------------------------- [E-AndTrue]
eval_e G and(E1, E2) trueVal


eval_e G E1 falseVal
----------------------------- [E-AndFalse1]
eval_e G and(E1, E2) falseVal


eval_e G E1 trueVal
eval_e G E2 falseVal
----------------------------- [E-AndFalse2]
eval_e G and(E1, E2) falseVal


eval_e G E1 trueVal
--------------------------- [E-OrTrue1]
eval_e G or(E1, E2) trueVal


eval_e G E1 falseVal
eval_e G E2 trueVal
--------------------------- [E-OrTrue2]
eval_e G or(E1, E2) trueVal


eval_e G E1 falseVal
eval_e G E2 falseVal
---------------------------- [E-OrFalse]
eval_e G or(E1, E2) falseVal


--------------------- [E-True]
eval_e G true trueVal


----------------------- [E-False]
eval_e G false falseVal


eval_rf G Fields FieldVals
------------------------------------------- [E-RecBuild]
eval_e G recBuild(Fields) recVal(FieldVals)


eval_e G Rec recVal(Fields)
lookup Fields Field V
------------------------------------- [E-RecField]
eval_e G recFieldAccess(Rec, Field) V



/*Record Field Evaluation*/

----------------------------- [ERF-End]
eval_rf G endRecFieldExprs []


eval_e G E V
eval_rf G Rest FVs
-------------------------------------------------- [ERF-Add]
eval_rf G addRecFieldExprs(L, E, Rest) (L, V)::FVs



/*Command Evaluation*/

--------------- [E-Noop]
eval_c G noop G


eval_c G C1 G1
eval_c G1 C2 G2
----------------------- [E-Seq]
eval_c G seq(C1, C2) G2


eval_e G E V
------------------------------------ [E-Declare]
eval_c G declare(X, Ty, E) (X, V)::G


eval_e G E V
------------------------------- [E-Assign]
eval_c G assign(X, E) (X, V)::G


eval_e G Cond trueVal
eval_c G Then G1
---------------------------------------- [E-IfThenElseTrue]
eval_c G ifThenElse(Cond, Then, Else) G1


eval_e G Cond falseVal
eval_c G Else G1
---------------------------------------- [E-IfThenElseFalse]
eval_c G ifThenElse(Cond, Then, Else) G1


eval_e G Cond falseVal
---------------------------- [E-WhileFalse]
eval_c G while(Cond, Body) G


eval_e G Cond trueVal
eval_c G Body G1
eval_c G1 while(Cond, Body) G2
------------------------------ [E-WhileTrue]
eval_c G while(Cond, Body) G2


eval_e G E V
lookup G Rec recVal(Fields)
update_rec_fields RecFields Fields V Result
------------------------------------------- [E-RecUpdate]
{eval_c G recUpdate(Rec, RecFields, E)
             (Rec, recVal(Result))::G}


/*Update the associations in the first tyCtx for the fields,
  descending through it to place the value in the final one, producing
  the ending tyCtx*/
Judgment update_rec_fields : recFields* [(string, value)] value [(string, value)]

------------------------------------------------- [URF-One]
update_rec_fields oneField(F) Init V (F, V)::Init


lookup Init F recVal(FFields)
update_rec_fields Rest FFields V UpdatedFFields
----------------------------------------------- [URF-Step]
{update_rec_fields addField(F, Rest) Init V
    (F, recVal(UpdatedFFields))::Init}



/*Check equality in a way appropriate to each value type*/
Judgment val_eq : value* value

-------------------------- [VE-Int]
val_eq intVal(I) intVal(I)


---------------------- [VE-True]
val_eq trueVal trueVal


------------------------ [VE-False]
val_eq falseVal falseVal


evalctx_eq Fields1 Fields2
-------------------------------------- [VE-Rec]
val_eq recVal(Fields1) recVal(Fields2)



Fixed Judgment evalctx_eq : [(string, value)] [(string, value)]

================ [ECEq-Empty]
evalctx_eq [] []


select (X, V2) EC2 Rest2
val_eq V1 V2
evalctx_eq Rest1 Rest2
============================= [ECEq-Add]
evalctx_eq (X, V1)::Rest1 EC2