Extensibella Example: simple_imp:list

Language Specification

File: list.sos

Module simple_imp:list

Builds on simple_imp:host

/*New Expressions and Projections*/
e ::= ...
    | nil(ty) /*we need the type to satisfy a host property*/
    | cons(e, e)
    | null(e)
    | head(e)
    | tail(e)
    | index(e, e) /*lst[i]*/
    | length(e)


--------------------------------------------- [Proj-Nil]
|{e}- nil(Ty) ~~>
      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


/*Actually computing the length or index from records would require
  conditionals, so we'll take advantage of the lax projection
  constraints and translate to something unrelated to the actual
  value.*/
-------------------------------------------------- [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)


/*Strictly speaking, an empty list doesn't have the head or tail
  fields.  However, we don't have any projection constraints on types,
  so we can do whatever we want, and this is close.*/
----------------------------------------------- [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

Module simple_imp:list

/*Expression Vars*/

--------------- [V-Nil]
vars nil(Ty) []


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

Module simple_imp:list

/*Expression Typing*/

--------------------------- [T-Nil]
typeOf G nil(Ty) 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

Module simple_imp:list

/*Expression Evaluation*/

----------------------- [E-Nil]
eval_e G nil(Ty) 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


/*To address proof problems, explicitly make indexing H::T
  We need this form in order for indexing to succeed anyway
  Another option would be to make indexRel fixed*/
eval_e G E1 consVal(Hd, Tl)
eval_e G E2 intVal(I)
indexRel consVal(Hd, Tl) 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)