Sterling Example: simple_imp:list

File: list.sos

[Reduce File] [Raw File]

Module simple_imp:list

Builds on simple_imp:host

/*New Expressions and Projections*/
e ::= ...
    | nil
    | cons(e, e)
    | null(e)
    | head(e)
    | tail(e)
    | index(e, e) /*lst[i]*/
    | length(e)


--------------------------------------------- [Proj-Nil]
|{e}- nil ~~>
      recBuild(addRecFieldExprs("null", true,
               endRecFieldExprs))


---------------------------------------------------------- [Proj-Cons]
|{e}- cons(E1, E2) ~~>
      recBuild(
         addRecFieldExprs("null", false,
         addRecFieldExprs("head", E1,
         addRecFieldExprs("tail", E2, endRecFieldExprs))))


------------------- [Proj-Null]
|{e}- null(E) ~~> E


------------------- [Proj-Head]
|{e}- head(E) ~~> E


------------------- [Proj-Tail]
|{e}- tail(E) ~~> E


-------------------------------------------------- [Proj-Index]
|{e}- index(Lst, Index) ~~> and(null(Lst),
                                eq(num(0), Index))


--------------------- [Proj-Length]
|{e}- length(E) ~~> E



/*New Type and Projection*/
ty ::= ...
     | listTy(ty)


----------------------------------------------- [Proj-ListTy]
|{ty}- listTy(T) ~~>
       recTy([("head", T), ("tail", listTy(T)),
              ("null", boolTy)])



/*New Value and Projection*/
value ::= ...
        | nilVal
        | consVal(value, value)


------------------------------------------------ [Proj-NilVal]
|{value}- nilVal ~~> recVal([("null", trueVal)])


--------------------------------------------- [Proj-ConsVal]
|{value}- consVal(Hd, Tl) ~~>
          recVal([("head", Hd), ("tail", Tl),
                  ("null", falseVal)])

File: list_vars.sos

[Reduce File] [Raw File]

Module simple_imp:list

/*Expression Vars*/

----------- [V-Nil]
vars nil []


vars E1 D1
vars E2 D2
D1 ++ D2 = D
------------------- [V-Cons]
vars cons(E1, E2) D


vars E D
-------------- [V-Null]
vars null(E) D


vars E D
-------------- [V-Head]
vars head(E) D


vars E D
-------------- [V-Tail]
vars tail(E) D


vars E1 D1
vars E2 D2
D1 ++ D2 = D
-------------------- [V-Index]
vars index(E1, E2) D


vars E D
---------------- [V-Length]
vars length(E) D

File: list_typing.sos

[Reduce File] [Raw File]

Module simple_imp:list

/*Expression Typing*/

----------------------- [T-Nil]
typeOf G nil listTy(Ty)


typeOf G E1 Ty
typeOf G E2 listTy(Ty)
-------------------------------- [T-Cons]
typeOf G cons(E1, E2) listTy(Ty)


typeOf G E listTy(Ty)
----------------------- [T-Null]
typeOf G null(E) boolTy


typeOf G E listTy(Ty)
--------------------- [T-Head]
typeOf G head(E) Ty


typeOf G E listTy(Ty)
--------------------------- [T-Tail]
typeOf G tail(E) listTy(Ty)


typeOf G List listTy(Ty)
typeOf G Index intTy
------------------------------ [T-Index]
typeOf G index(List, Index) Ty


typeOf G Lst listTy(Ty)
-------------------------- [T-Length]
typeOf G length(Lst) intTy




/*Value Typing*/

--------------------------- [TV-Nil]
typeOfVal nilVal listTy(Ty)


typeOfVal V1 Ty
typeOfVal V2 listTy(Ty)
------------------------------------ [TV-Cons]
typeOfVal consVal(V1, V2) listTy(Ty)

File: list_eval.sos

[Reduce File] [Raw File]

Module simple_imp:list

/*Expression Evaluation*/

------------------- [E-Nil]
eval_e G nil nilVal


eval_e G E1 V1
eval_e G E2 V2
------------------------------------- [E-Cons]
eval_e G cons(E1, E2) consVal(V1, V2)


eval_e G E nilVal
---------------------- [E-NullTrue]
eval_e G null(E) trueVal


eval_e G E consVal(V1, V2)
-------------------------- [E-NullFalse]
eval_e G null(E) falseVal


eval_e G E consVal(V1, V2)
-------------------------- [E-Head]
eval_e G head(E) V1


eval_e G E consVal(V1, V2)
-------------------------- [E-Tail]
eval_e G tail(E) V2


eval_e G E1 VL
eval_e G E2 intVal(I)
indexRel VL I V
------------------------ [E-Index]
eval_e G index(E1, E2) V


eval_e G E ListVal
lengthRel ListVal Length
--------------------------------- [E-Length]
eval_e G length(E) intVal(Length)


/*Support for list expression evaluation*/
Judgment indexRel : value* int value

----------------------------- [Index-0]
indexRel consVal(Hd, Tl) 0 Hd


Index - 1 = SubIndex
indexRel Tl SubIndex V
-------------------------------- [Index-Step]
indexRel consVal(Hd, Tl) Index V


|{value}- V ~~> VT
indexRel VT I Result
-------------------- [Index-D]*
indexRel V I Result


Judgment lengthRel : value* int

--------------- [Len-Nil]
lengthRel nilVal 0


lengthRel Tl SubLen
SubLen + 1 = Len
----------------------------- [Len-Cons]
lengthRel consVal(Hd, Tl) Len


|{value}- V ~~> VT
lengthRel VT Len
------------------ [Len-D]*
lengthRel V Len




/*Value Equality*/

-------------------- [VE-NilVal]
val_eq nilVal nilVal


val_eq V11 V21
val_eq V12 V22
------------------------------------------ [VE-ConsVal]
val_eq consVal(V11, V12) consVal(V21, V22)