Extensibella Example: library:host

Language Specification

File: syntax.sos

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

s ::= skipS /*just "skip" is a bad idea for Extensibella*/
    | decl(string, ty, e)
    | assign(string, e)
    | seq(s, s)
    | ifte(e, s, s)
    | while(e, s)

e ::= var(string)
    | intlit(int)
    | trueE | falseE /*just "true" and "false" are bad for Extensibella*/
    | add(e, e)
    | eq(e, e)
    | gt(e, e)
    | not(e)

ty ::= intTy /*just "int" is built-in*/
     | bool

Projection s :
Projection e :
Projection ty :

File: vars.sos

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

/*We don't have a built-in set type, so we use a list instead*/
Judgment vars: e* [string]

--------------- [VR-var]
vars var(N) [N]


----------------- [VR-intlit]
vars intlit(I) []


------------- [VR-true]
vars trueE []


-------------- [VR-false]
vars falseE []


vars E1 Vr1
vars E2 Vr2
Vr1 ++ Vr2 = V
------------------ [VR-add]
vars add(E1, E2) V


vars E1 Vr1
vars E2 Vr2
Vr1 ++ Vr2 = V
----------------- [VR-eq]
vars eq(E1, E2) V


vars E1 Vr1
vars E2 Vr2
Vr1 ++ Vr2 = V
----------------- [VR-gt]
vars gt(E1, E2) V


vars E Vr
-------------- [VR-not]
vars not(E) Vr

File: typing.sos

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

/*We use the standard library's lookup and no_lookup relations rather
  than writing our own here.*/

/*Gamma |- e* : ty*/
Judgment ty_e : [(string, ty)] e* ty
/*Gamma |- s* -| Gamma*/
Judgment ty_s : [(string, ty)] s* [(string, ty)]

lookup G N Ty
---------------- [T-var]
ty_e G var(N) Ty


---------------------- [T-intlit]
ty_e G intlit(I) intTy


----------------- [T-true]
ty_e G trueE bool


------------------ [T-false]
ty_e G falseE bool


ty_e G E1 intTy
ty_e G E2 intTy
------------------------ [T-add]
ty_e G add(E1, E2) intTy


ty_e G E1 intTy
ty_e G E2 intTy
---------------------- [T-eq]
ty_e G eq(E1, E2) bool


ty_e G E1 intTy
ty_e G E2 intTy
---------------------- [T-gt]
ty_e G gt(E1, E2) bool


ty_e G E bool
------------------ [T-not]
ty_e G not(E) bool





-------------- [TS-skip]
ty_s G skipS G


ty_s G S1 G1
ty_s G1 S2 G2
--------------------- [TS-seq]
ty_s G seq(S1, S2) G2


ty_e G E Ty
no_lookup G N
-------------------------------- [TS-decl]
ty_s G decl(N, Ty, E) (N, Ty)::G


ty_e G E Ty
lookup G N Ty
--------------------- [TS-assign]
ty_s G assign(N, E) G


ty_e G E bool
ty_s G S1 G1
ty_s G S2 G2
------------------------ [TS-ifte]
ty_s G ifte(E, S1, S2) G


ty_e G E bool
ty_s G S G1
-------------------- [TS-while]
ty_s G while(E, S) G

File: eval.sos

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

Judgment value: e*

--------------- [V-Int]
value intlit(I)


----------- [V-True]
value trueE


------------ [V-False]
value falseE

/*We use the standard library's lookup and select relations rather
  than writing our own here.*/

/*gamma |- e* \Downarrow e*/
Judgment eval_e : [(string, e)] e* e
/*gamma |- s* -| gamma*/
Judgment eval_s : [(string, e)] s* [(string, e)]

lookup G N V
----------------- [E-var]
eval_e G var(N) V


---------------------------- [E-intlit]
eval_e G intlit(I) intlit(I)


-------------------- [E-true]
eval_e G trueE trueE


---------------------- [E-false]
eval_e G falseE falseE


eval_e G E1 intlit(I1)
eval_e G E2 intlit(I2)
I1 + I2 = I
------------------------------ [E-add]
eval_e G add(E1, E2) intlit(I)


eval_e G E1 V1
eval_e G E2 V2
V1 = V2
------------------------- [E-eq-True]
eval_e G eq(E1, E2) trueE


eval_e G E1 V1
eval_e G E2 V2
V1 != V2
-------------------------- [E-eq-False]
eval_e G eq(E1, E2) falseE


eval_e G E1 intlit(I1)
eval_e G E2 intlit(I2)
I1 > I2
------------------------- [E-gt-True]
eval_e G gt(E1, E2) trueE


eval_e G E1 intlit(I1)
eval_e G E2 intlit(I2)
I1 <= I2
-------------------------- [E-gt-False]
eval_e G gt(E1, E2) falseE


eval_e G E falseE
--------------------- [E-not-True]
eval_e G not(E) trueE


eval_e G E trueE
---------------------- [E-not-False]
eval_e G not(E) falseE





---------------- [X-skip]
eval_s G skipS G


eval_e G E V
--------------------------------- [X-decl]
eval_s G decl(N, Ty, E) (N, V)::G


eval_e G E V
select (N, VOld) NewG G
---------------------------------- [X-assign]
eval_s G assign(N, E) (N, V)::NewG


eval_s G S1 G1
eval_s G1 S2 G2
----------------------- [X-seq]
eval_s G seq(S1, S2) G2


eval_e G E trueE
eval_s G S1 G1
--------------------------- [X-ifte-True]
eval_s G ifte(E, S1, S2) G1


eval_e G E falseE
eval_s G S2 G1
--------------------------- [X-ifte-False]
eval_s G ifte(E, S1, S2) G1


eval_e G E trueE
eval_s G S G1
eval_s G1 while(E, S) G2
------------------------ [X-while-True]
eval_s G while(E, S) G2


eval_e G E falseE
---------------------- [X-while-False]
eval_s G while(E, S) G


Extensibella_Stand_In {
  |{s}- S ~~> T
  eval_s G T G1
  ------------- [X-Q]
  eval_s G S G1
}

Reasoning

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

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

Module library:host.

Projection_Constraint proj_e_unique : forall E E1 E2,
  |{e}- E ~~> E1 -> |{e}- E ~~> E2 -> E1 = E2.
Projection_Constraint proj_e_is : forall E E',
  |{e}- E ~~> E' -> is_e E -> is_e E'.

Projection_Constraint proj_s_unique : forall S S1 S2,
  |{s}- S ~~> S1 -> |{s}- S ~~> S2 -> S1 = S2.
Projection_Constraint proj_s_is : forall S S',
  |{s}- S ~~> S' -> is_s S -> is_s S'.

Projection_Constraint proj_ty_unique : forall Ty Ty1 Ty2,
  |{ty}- Ty ~~> Ty1 -> |{ty}- Ty ~~> Ty2 -> Ty1 = Ty2.
Projection_Constraint proj_ty_is : forall Ty Ty',
  |{ty}- Ty ~~> Ty' -> is_ty Ty -> is_ty Ty'.


Proj_Rel is_e E.


Ext_Ind forall E, is_e E. [Show Proof]



Extensible_Theorem
  is_e_var_or_not : forall E,
    IsE: is_e E ->
    (exists N, E = var N) \/ ((exists N, E = var N) -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_intlit_or_not : forall E,
    IsE: is_e E ->
    (exists I, E = intlit I) \/ ((exists I, E = intlit I) -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_trueE_or_not : forall E,
    IsE: is_e E ->
    E = trueE \/ (E = trueE -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_falseE_or_not : forall E,
    IsE: is_e E ->
    E = falseE \/ (E = falseE -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_add_or_not : forall E,
    IsE: is_e E ->
    (exists E1 E2, E = add E1 E2) \/
    ((exists E1 E2, E = add E1 E2) -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_eqC_or_not : forall E,
    IsE: is_e E ->
    (exists E1 E2, E = eq E1 E2) \/
    ((exists E1 E2, E = eq E1 E2) -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_gt_or_not : forall E,
    IsE: is_e E ->
    (exists E1 E2, E = gt E1 E2) \/
    ((exists E1 E2, E = gt E1 E2) -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_not_or_not : forall E,
    IsE: is_e E ->
    (exists E', E = not E') \/
    ((exists E', E = not E') -> false)
  on IsE. [Show Proof]

Extensible_Theorem
  is_e_eq_or_not : forall E1 E2,
    IsE1: is_e E1 ->
    IsE2: is_e E2 ->
    E1 = E2 \/ (E1 = E2 -> false)
  on IsE1. [Show Proof]



Extensible_Theorem
  vars_unique : forall E V1 V2,
    Vars1 : vars E V1 ->
    Vars2 : vars E V2 ->
    V1 = V2
  on Vars1. [Show Proof]



Projection_Constraint proj_e_vars_exist : forall E E' V,
  |{e}- E ~~> E' -> vars E V -> exists V', vars E' V'.

%Rationale for TC:
%Evaluation depends on the variables in an expression.  In fact, by
%the property vars_eval_same_result below, evaluation is determined
%*entirely* by the variables in an expression.  Therefore making the
%variables in an expression be a subset of those in its projection
%gives other extensions a handle on understanding the behavior of an
%unknown expression in particular contexts.
Projection_Constraint proj_e_vars : forall E E' V V' X,
  |{e}- E ~~> E' -> vars E V -> vars E' V' ->
  mem X V -> mem X V'.


Theorem append__is_list__is_string : forall L1 L2 L,
  is_list is_string L1 -> is_list is_string L2 -> L1 ++ L2 = L ->
  is_list is_string L. [Show Proof]


Extensible_Theorem
  vars_is : forall E V,
    IsE : is_e E ->
    Vars : vars E V ->
    is_list is_string V
  on Vars. [Show Proof]



Theorem append__is_list__is_string__total : forall L1 L2,
  is_list is_string L1 -> is_list is_string L2 ->
  exists L, L1 ++ L2 = L. [Show Proof]


Extensible_Theorem
  vars_exist : forall E,
    IsE : is_e E ->
    exists V, vars E V
  on IsE. [Show Proof]



Extensible_Theorem
  value_empty_typable : forall V G Ty,
    Value: value V ->
    Ty: ty_e G V Ty ->
    ty_e [] V Ty
  on Value. [Show Proof]



Theorem lookup_is : forall G X V,
  is_list (is_pair is_string is_e) G -> lookup G X V -> is_e V. [Show Proof]



Extensible_Theorem
  eval_e_is : forall G E V,
    IsE : is_e E ->
    IsCtx : is_list (is_pair is_string is_e) G ->
    Ev : eval_e G E V ->
    is_e V
  on Ev. [Show Proof]



Extensible_Theorem
  type_preservation_e : forall TG EG E Ty V,
    Ty: ty_e TG E Ty ->
    Ev: eval_e EG E V ->
    Rel: (forall X Ty V,
             lookup TG X Ty -> lookup EG X V -> ty_e [] V Ty) ->
    ty_e [] V Ty
  on Ev. [Show Proof]



%lemma for type_preservation_s
Extensible_Theorem
  var_types_maintained : forall G S G' X Ty,
    Ty: ty_s G S G' ->
    Lkp: lookup G X Ty ->
    lookup G' X Ty
  on Ty. [Show Proof]



Extensible_Theorem
  type_preservation_s : forall TG EG S TG' EG' X Ty V,
    Ty: ty_s TG S TG' ->
    Ev: eval_s EG S EG' ->
    Rel: (forall X Ty V,
             lookup TG X Ty -> lookup EG X V -> ty_e [] V Ty) ->
    LkpTy: lookup TG' X Ty ->
    LkpV: lookup EG' X V ->
    ty_e [] V Ty
  on Ev. [Show Proof]



Projection_Constraint proj_eval_e : forall G E E' V,
  |{e}- E ~~> E' -> eval_e G E V ->
  is_list (is_pair is_string is_e) G -> is_e E ->
  exists V', eval_e G E' V'.


Extensible_Theorem
  eval_e_unique : forall G E V1 V2,
    Ev1: eval_e G E V1 ->
    Ev2: eval_e G E V2 ->
    V1 = V2
  on Ev1. [Show Proof]



Projection_Constraint proj_s_eval : forall S S' G G2,
  |{s}- S ~~> S' -> eval_s G S G2 -> exists G', eval_s G S' G'.


Ext_Size eval_s G S G1.
Proj_Rel eval_s G S G1.


Ext_Ind forall G S G1, eval_s G S G1. [Show Proof]



Projection_Constraint proj_s_eval_results :
  forall S S' G G1 G2 X V,
    |{s}- S ~~> S' -> eval_s G S G1 -> eval_s G S' G2 ->
    lookup G1 X V -> lookup G2 X V.
Projection_Constraint proj_s_eval_results_back :
  forall S S' G G1 G2 X V,
    |{s}- S ~~> S' -> eval_s G S G1 -> eval_s G S' G2 ->
    lookup G2 X V -> lookup G1 X V.


Extensible_Theorem
  eval_e_value : forall G E V,
    Ev: eval_e G E V ->
    AllVal: (forall X XV, mem (X, XV) G -> value XV) ->
    value V
  on Ev. [Show Proof]



Extensible_Theorem
  eval_s_value : forall G S G' Y YV,
    Ev: eval_s G S G' ->
    AllVal: (forall X XV, mem (X, XV) G -> value XV) ->
    Mem: mem (Y, YV) G' ->
    value YV
  on Ev. [Show Proof]



%helpers for vars_eval_same_result
Theorem vars_equiv_left :
  forall (G1 : list (pair string e)) G2 D D1 D2,
    (forall X U1 U2, mem X D -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2) ->
    D1 ++ D2 = D ->
    (forall X U1 U2, mem X D1 -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2). [Show Proof]

Theorem vars_equiv_right :
  forall (G1 : list (pair string e)) G2 D D1 D2,
    (forall X U1 U2, mem X D -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2) ->
    D1 ++ D2 = D ->
    (forall X U1 U2, mem X D2 -> lookup G1 X U1 ->
                     lookup G2 X U2 -> U1 = U2). [Show Proof]



Extensible_Theorem
  vars_eval_same_result : forall G1 G2 E D V1 V2,
    Equiv : (forall X U1 U2,
                mem X D ->
                lookup G1 X U1 ->
                lookup G2 X U2 -> U1 = U2) ->
    Vars : vars E D ->
    Ev1 : eval_e G1 E V1 ->
    Ev2 : eval_e G2 E V2 ->
    V1 = V2
  on Ev1. [Show Proof]
Back to example home