Sterling Example: functions:list

File: list.sos

[Reduce File] [Raw File]

Module functions:list

Builds on functions: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) ~~> recFieldAccess(E, "null")


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


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


-------------------------------------------- [Proj-Index]
|{e}- index(Lst, Index) ~~> plus(Lst, 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 functions: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 functions:list

/*Expression Typing*/

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


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


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


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


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


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


typeOf FG G Lst listTy(Ty)
----------------------------- [T-Length]
typeOf FG 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 functions:list

/*Expression Evaluation*/

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


eval_e FG G E1 V1 O1
eval_e FG G E2 V2 O2
appendOutput O1 O2 O
------------------------------------------ [E-Cons]
eval_e FG G cons(E1, E2) consVal(V1, V2) O


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


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


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


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


eval_e FG G E1 ListVal O1
eval_e FG G E2 intVal(I) O2
index ListVal I V
appendOutput O1 O2 O
----------------------------- [E-Index]
eval_e FG G index(E1, E2) V O


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


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

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


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


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


Judgment length : value* int

--------------- [Len-Nil]
length nilVal 0


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


|{value}- V ~~> VT
length VT Len
------------------ [Len-D]*
length 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)