bool.ott

% Language additions for booleans

grammar

tm, a , b , A , B  :: '' ::= {{ com terms and types }}

  | Bool                  ::   :: TyBool {{ com boolean type }}
  | True                  ::   :: LitTrue {{ com boolean value true }}
  | False                 ::   :: LitFalse {{ com boolean value false }}
  | if a then b1 else b2  ::   :: If {{ com conditional }}

  | if a then b1 else b2 [ x . B ]  ::   :: IfM {{ com conditional }}

v :: 'v_' ::= 
  | Bool                  ::   :: TyBool 
  | True                  ::   :: LitTrue
  | False                 ::   :: LitFalse

neutral , ne :: 'n_' ::=
  | if ne then a else b    ::   :: If

nf :: 'nf_' ::= 
  | Bool                  ::   :: TyBool 
  | True                  ::   :: LitTrue
  | False                 ::   :: LitFalse
  | if ne then a else b    ::   :: If


defns 
Jwhnf :: '' ::= 

defn
whnf G |-  a ~> nf ::    :: whnf :: 'whnf_' 
by

whnf G |-  a ~> True
whnf G |-  b1 ~> nf
--------------------------- :: if_true
whnf G |-  if a then b1 else b2 ~> nf

whnf G |-  a ~> False
whnf G |-  b2 ~> nf
------------------------------- :: if_false
whnf G |-  if a then b1 else b2 ~> nf

----------------- :: bool
whnf G |-  Bool ~> Bool

---------------- :: true
whnf G |-  True ~> True

------------------- :: false
whnf G |-  False ~> False

whnf G |-  a ~> ne
---------------------------------------------------- :: if_cong
whnf G |-  if a then b1 else b2 ~> if ne then b1 else b2


defns
JOp :: '' ::=

defn
a ~> b ::   :: step :: 's_'
{{ com single-step operational semantics, i. e. head reduction }}
by

---------------------------------- :: if_true
if True then b1 else b2 ~> b1


---------------------------------- :: if_false
if False then b1 else b2 ~> b1

a ~> a'
--------------------------------- :: if
if a then b1 else b2 ~> if a' then b1 else b2


defns 
JEq :: '' ::=

defn
G |- A = B ::  :: eq :: 'e_'
{{ com Definitional equality }}
by

----------------------------- :: if_true
G |- if True then a else b = a

------------------------------- :: if_false
G |- if False then a else b = b


G |- a = a'
G |- b1 = b1'
G |- b2 = b2'
--------------------------------------------------- :: if
G |- if a then b1 else b2 = if a' then b1' else b2'

-------------------------------- :: if_eta
G |- if a then b else b = b


defns
JTyping :: '' ::= 

defn 

G |- a : A   ::   :: typing :: 't_'
{{ com Typing }}
by


---------------- :: bool
G |- Bool : Type

---------------- :: true
G |- True : Bool

---------------- :: false
G |- False : Bool


G |- a : Bool 
G |- b1 : A
G |- b2 : A
---------------------------- :: if_simple
G |- if a then b1 else b2 : A

G |- a : Bool 
G |- b1 : A [ True / x ]
G |- b2 : A [ False / x ]
G, x:Bool |- A : Type
-------------------------------- :: if_full
G |- if a then b1 else b2 : A[a/x]


G |- x : Bool 
G |- b1 : A [ True / x ]
G |- b2 : A [ False / x ]
G |- A : Type
---------------------------- :: if
G |- if x then b1 else b2 : A 


defns
JBidirectional :: '' ::= 

defn 
G |- a => A ::    :: inferType :: 'i_'
{{ com type synthesis (algorithmic) }}
by

---------------- :: bool
G |- Bool => Type

---------------- :: true
G |- True => Bool

---------------- :: false
G |- False => Bool

G |- a <= Bool 
G |- b1 => A1
G |- b2 => A2
G |- A1 <=> A2
---------------------------- :: if_simple
G |- if a then b1 else b2 => A1

G |- a <= Bool 
G |- b1 <= A [ True / x ]
G |- b2 <= A [ False / x ]
G, x:Bool |- A <= Type
-------------------------------- :: if_motive
G |- if a then b1 else b2 [x.A] => A[a/x]


G |- a <= Bool 
G |- b1 => B1
G |- b2 => B2
----------------------------------------------- :: if_alt
G |- if a then b1 else b2 => if a then B1 else B2


defn 
G |- a <= B ::    :: checkType :: 'c_'
{{ com type checking (algorithmic) }}
by

G |- a <= Bool 
G |- b1 <= A
G |- b2 <= A
---------------------------- :: if_simple
G |- if a then b1 else b2 <= A


G |- x <= Bool 
G |- b1 <= A [ True / x ]
G |- b2 <= A [ False / x ]
------------------------------ :: if
G |- if x then b1 else b2 <= A