-- File: stack

-- Gives the example of the ADT of stacks.
-- This file is divided into two parts.
-- 1) Without existential types.
-- 2) With existential types.

Path "../lol"
Path "../lolExtra"
Load "lambdaLplus"
Load "logic2"
Load "list2"


------------------------------------------------------------
------------------------------------------------------------
--                                                        --
--  1. W I T H O U T   E X I S T E N T I A L   T Y P E S  --
--                                                        --
------------------------------------------------------------
------------------------------------------------------------

Def StackI := \Rep:*s. {| empty : Rep, 
                          push : Nat -> Rep -> Rep,
                          pop : Rep -> Rep,
                          top : Rep -> Nat,
                          isEmpty : Rep -> Bool |}

Def Rep1 := List Nat
Def ops1 := {empty = nil Nat,
              push = (;) Nat,
              pop = tail Nat,
              top = head O,
              isEmpty = null Nat} :
             StackI Rep1

Def Spec := \Rep:*s. \ops:StackI Rep.
                   ops`isEmpty ops`empty = true /\
                   (@s:Rep. @n:Nat. ops`isEmpty (ops`push n s) = false) /\
                   (@s:Rep. @n:Nat. ops`top (ops`push n s) = n) /\
                   (@s:Rep. @n:Nat. ops`pop (ops`push n s) = s) :
            @Rep:*s. StackI Rep -> *p

Prove Spec_ops1 : Spec Rep1 ops1

-- 'wprinciple' is called 'principle' in my thesis
Prove wprinciple : @Rep1:*s. @ops1: StackI Rep1. Spec Rep1 ops1 ->
                   @A:*s. @body:(@X:*s.StackI X -> A). @Q:A->*p.
                 (@X:*s.@ops:StackI X. Spec X ops -> Q (body X ops)) ->
                 Q ((\X:*s.\ops:StackI X. body X ops) Rep1 ops1)

Def prog1 := (\X:*s.\ops : StackI X.
                  ops`isEmpty (ops`pop (ops`push O ops`empty))) Rep1 ops1

Prove prog1_is_true : prog1 = true



------------------------------------------------------
------------------------------------------------------
--                                                  --
--  2. W I T H   E X I S T E N T I A L   T Y P E S  --
--                                                  --
------------------------------------------------------
------------------------------------------------------

Def imp1 := pack StackI Rep1 ops1 : Sig Rep:*s. StackI Rep

Def StackImp := Sig Rep:*s. StackI Rep

Def prog1' := unpack imp1 (\X:*s. \ops:StackI X.
                              ops`isEmpty (ops`pop (ops`push O ops`empty))) :
              Bool

Def Rep2 := List Nat
Def ops2 := {empty = nil Nat,
              push = snoc Nat,
              pop = init Nat,
              top = last O,
              isEmpty = null Nat} :
             StackI Rep2
Def imp2 := pack StackI Rep2 ops2 : StackImp

Def UserSpec := \imp:StackImp. ExK Rep:*s. Ex ops:StackI Rep.
                     imp = pack StackI Rep ops /\ Spec Rep ops :
                StackImp -> *p

Prove UserSpec_imp1 : UserSpec imp1

Prove principle : @imp:StackImp. UserSpec imp ->
                  @A:*s. @body:(@X:*s.StackI X -> A). @Q:A->*p.
                 (@X:*s.@ops:StackI X. Spec X ops -> Q (body X ops)) ->
                 Q (unpack imp (\X:*s.\ops:StackI X. body X ops))

Prove prog1'_is_true : prog1'=true