Prelude.sawcore

-- Copyright   : Galois, Inc. 2012-2014
-- License     : BSD3
-- Maintainer  : jhendrix@galois.com

module Prelude where

-- Grammar for the core prelude types.
--
-- We use single colons ":" to represent the type constraint on the core symbols.
--   e.g., "Bool : sort 0" indicates "Bool" has type "sort 0".
-- Functions use "->" to separate arguments from result.
--   e.g., "f : Bool -> Bool -> Bool" indicates "f" is a binary operation on Booleans.


id : (a : sort 0) -> a -> a;
id _ x = x;

-- FIXME: We eventually need to remove this, as it violates soundness...
primitive fix : (a : sort 1) -> (a -> a) -> a;

sawLet : (a b : sort 1) -> a -> (a -> b) -> b;
sawLet _ _ x f = f x;


-- FIXME: below are some defined data-types that could be used in place of
-- the SAW primitive types

--------------------------------------------------------------------------------
-- The Unit type

data UnitType : sort 0 where {
    Unit : UnitType;
  }

-- The recursor for the Unit type at sort 0
-- UnitType__rec : (p : UnitType -> sort 0) -> p Unit -> (u : UnitType) -> p u;
-- UnitType__rec p f1 u = UnitType#rec p f1 u;
UnitType__rec (p : UnitType -> sort 0) (f1 : p Unit) (u : UnitType) : p u
  = UnitType#rec p f1 u;

--------------------------------------------------------------------------------
-- Pair types

data PairType (a b : sort 0) : sort 0 where {
  PairValue : a -> b -> PairType a b;
}

pair_example : (a b : sort 0) -> a -> b -> PairType a b;
pair_example a b x y = PairValue a b x y;

-- The recursor for primitive pair types at sort 1
Pair__rec
  (a b : sort 0)
  (p : PairType a b -> sort 0)
  (f : (x:a) -> (y:b) -> p (PairValue a b x y))
  (pair : PairType a b)
  : p pair
  = PairType#rec a b p f pair;

Pair_fst : (a b : sort 0) -> PairType a b -> a;
Pair_fst a b = Pair__rec a b (\ (p:PairType a b) -> a)
                             (\ (x:a) -> \ (y: b) -> x);

Pair_snd : (a b : sort 0) -> PairType a b -> b;
Pair_snd a b = Pair__rec a b (\ (p:PairType a b) -> b)
                             (\ (x:a) -> \ (y:b) -> y);

fst : (a b : sort 0) -> a * b -> a;
fst a b tup = tup.(1);

snd : (a b : sort 0) -> a * b -> b;
snd a b tup = tup.(2);

uncurry (a b c : sort 0) (f : a -> b -> c) : a * b -> c
  = (\ (x : a * b) -> f x.(1) x.(2));

--------------------------------------------------------------------------------
-- String values

primitive String : sort 0;

primitive error : (a : isort 1) -> String -> a;


--------------------------------------------------------------------------------
-- Record types

-- The empty record
data EmptyType : sort 0 where {
  Empty : EmptyType;
}

-- The recursor for the empty type at sort 0
EmptyType__rec : (p : EmptyType -> sort 0) -> p Empty ->
                  (emp : EmptyType) -> p emp;
EmptyType__rec p f1 emp = EmptyType#rec p f1 emp;

-- Add a named field to a record type
data RecordType (s:String) (a b :sort 0) : sort 0 where {
  RecordValue : a -> b -> RecordType s a b;
}

-- The recursor for record types at sort 0
RecordType__rec
  (s : String)
  (a b :sort 0)
  (p : RecordType s a b -> sort 1)
  (f1 : (x:a) -> (y:b) -> p (RecordValue s a b x y))
  (r : RecordType s a b)
  : p r
  = RecordType#rec s a b p f1 r;


--------------------------------------------------------------------------------
-- The Void type

data Void : sort 0 where { }

-- Eliminate a Void to any type
elimVoid : (a:sort 1) -> Void -> a;
elimVoid a v = Void#rec (\ (_:Void) -> a) v;


--------------------------------------------------------------------------------
-- Equality proofs.

data Eq (t : sort 1) (x : t) : t -> Prop where {
    Refl : Eq t x x;
  }


-- The eliminator for the Eq type at sort 1, assuming the usual parameter-index
-- structure of the Eq type
Eq__rec : (t : sort 1) -> (x : t) -> (p : (y : t) -> Eq t x y -> sort 1) ->
           p x (Refl t x) -> (y : t) -> (pf : Eq t x y) -> p y pf;
Eq__rec t x p f1 y pf = Eq#rec t x p f1 y pf;

-- Congruence closure for equality
eq_cong : (t : sort 1) -> (x : t) -> (y : t) -> Eq t x y ->
           (u : sort 1) -> (f : t -> u) -> Eq u (f x) (f y);
eq_cong t x y eq u f =
  Eq__rec t x (\ (y':t) -> \ (eq':Eq t x y') -> Eq u (f x) (f y'))
          (Refl u (f x)) y eq;

sym : (a : sort 1) -> (x y : a) -> Eq a x y -> Eq a y x;
sym a x y eq =
  Eq__rec a x (\ (y':a) -> \ (eq':Eq a x y') -> Eq a y' x) (Refl a x) y eq;

trans : (a : sort 1) -> (x y z : a) -> Eq a x y -> Eq a y z -> Eq a x z;
trans a x y z eq1 eq2 =
  Eq__rec a y (\ (y':a) -> \ (eq':Eq a y y') -> Eq a x y') eq1 z eq2;

trans2 : (a : sort 1) -> (x y z : a) -> Eq a x z -> Eq a y z -> Eq a x y;
trans2 a x y z eq1 eq2 = trans a x z y eq1 (sym a y z eq2);

trans4 : (a : sort 1) -> (w x y z : a) ->
          Eq a w x -> Eq a x y -> Eq a y z -> Eq a w z;
trans4 a w x y z eq1 eq2 eq3 =
  trans a w x z eq1 (trans a x y z eq2 eq3);

eq_inv_map : (a b : sort 1) -> (a1 a2 : a) -> Eq a a1 a2 ->
              (f1 f2 : a -> b) -> Eq b (f1 a2) (f2 a2) ->
              Eq b (f1 a1) (f2 a1);
eq_inv_map a b a1 a2 eq_a f1 f2 eq_f =
  trans
    b (f1 a1) (f1 a2) (f2 a1)
    (eq_cong a a1 a2 eq_a b f1)
    (trans b (f1 a2) (f2 a2) (f2 a1) eq_f
           (eq_cong a a2 a1 (sym a a1 a2 eq_a) b f2));


-- Basic axiom about the behavior of "fix"
axiom fix_unfold :
  (a : sort 1) ->
  (f : a -> a) ->
  Eq a (fix a f) (f (fix a f));

inverse_eta_rule :
  (a : sort 1) ->
  (b : sort 1) ->
  (f : a -> b) ->
  (g : a -> b) ->
  (Eq (a -> b) f g) ->
  (x : a) ->
  Eq b (f x) (g x);
inverse_eta_rule a b f g H =
  Eq__rec (a -> b) f
    ( \ (g' : a -> b) -> \ (H':Eq (a -> b) f g') ->
        ( x : a ) -> Eq b (f x) (g' x))
    (\ (x:a) -> Refl b (f x))
    g H;


-- Unchecked assertion that two types are equal.
axiom unsafeAssert : (a : sort 1) -> (x : a) -> (y : a) -> Eq a x y;


primitive coerce : (a b : sort 0) -> Eq (sort 0) a b -> a -> b;

coerce__def : (a b : sort 0) -> Eq (sort 0) a b -> a -> b;
coerce__def a b eq x =
   Eq__rec (sort 0) a (\ (b':sort 0) -> \ (eq':Eq (sort 0) a b') -> b') x b eq;

axiom coerce__eq :
  Eq ((a b : sort 0) -> Eq (sort 0) a b -> a -> b) coerce coerce__def;


-- NOTE: this is equivalent to UIP / Axiom K
{-
coerce_same : (a : sort 0) -> (q : Eq (sort 0) a a) -> (x : a) -> Eq a (coerce a a q x) x;
coerce_same a (Refl _ _) x = Refl a x;
-}

rcoerce : (a b : sort 0) -> Eq (sort 0) a b -> b -> a;
rcoerce a b q = coerce b a (sym (sort 0) a b q);

-- NOTE: this is equivalent to UIP / Axiom K
{-
rcoerce_same : (a : sort 0) -> (q : Eq (sort 0) a a) -> (x : a) -> Eq a (rcoerce a a q x) x;
rcoerce_same a q x = coerce_same a (sym (sort 0) a a q) x;
-}

unsafeCoerce : (a b : sort 0) -> a -> b;
unsafeCoerce a b = coerce a b (unsafeAssert (sort 0) a b);

axiom unsafeCoerce_same : (a : sort 0) -> (x : a) ->
                           Eq a (unsafeCoerce a a x) x;

-- NOTE: We could prove unsafeCoerce_same if we were willing to allow UIP...
{-
unsafeCoerce_same : (a : sort 0) -> (x : a) -> Eq a (unsafeCoerce a a x) x;
unsafeCoerce_same a x = coerce_same a (unsafeAssert (sort 0) a a) x;
-}

piCong0 : (r x y : sort 0) -> Eq (sort 0) x y -> (Eq (sort 0) (x -> r) (y -> r));
piCong0 r x y eq =
  Eq__rec
    (sort 0) x
    (\ (y': sort 0) -> \ (eq': Eq (sort 0) x y') ->
       Eq (sort 0) (x -> r) (y' -> r))
    (Refl (sort 0) (x -> r)) y eq;

piCong1 : (r x y : sort 0) -> Eq (sort 0) x y -> (Eq (sort 0) (r -> x) (r -> y));
piCong1 r x y eq =
  Eq__rec
    (sort 0) x
    (\ (y': sort 0) -> \ (eq': Eq (sort 0) x y') ->
       Eq (sort 0) (r -> x) (r -> y'))
    (Refl (sort 0) (r -> x)) y eq;


--------------------------------------------------------------------------------
-- Bits

data Bit : sort 0 where {
    Bit1 : Bit;
    Bit0 : Bit;
  }

Bit__rec : (p : Bit -> sort 1) -> (p Bit1) -> (p Bit0) -> (b:Bit) -> p b;
Bit__rec p f1 f2 b = Bit#rec p f1 f2 b;


--------------------------------------------------------------------------------
-- Booleans

-- Boolean is a primitive type, because it is handled specially by some of the
-- back-ends (e.g., the SAT/SMT solvers)
primitive Bool : sort 0;
primitive True : Bool;
primitive False : Bool;

-- Elimination form for Bool is dependent if-then-else. This is exactly the same
-- as the recursor for Bit, but it is declared as a primitive because Bool is.
-- It also rearranges the arguments to look more like normal if-then-else.
primitive iteDep : (p : Bool -> sort 1) -> (b:Bool) ->
                    p True -> p False -> p b;

-- Reduction rules for iteDep
axiom iteDep_True : (p : Bool -> sort 1) -> (f1:p True) -> (f2:p False) ->
                     Eq (p True) (iteDep p True f1 f2) f1;
axiom iteDep_False : (p : Bool -> sort 1) -> (f1:p True) -> (f2:p False) ->
                      Eq (p False) (iteDep p False f1 f2) f2;

-- Non-dependent if-then-else; this is a primitive because it is handled
-- specially by some of the back-ends (e.g., the SAT/SMT solvers)
primitive ite : (a : sort 1) -> Bool -> a -> a -> a;

-- ite should be the same as iteDep
axiom ite_eq_iteDep : (a:sort 1) -> (b:Bool) -> (x y:a) ->
                       Eq a (ite a b x y) (iteDep (\ (_:Bool) -> a) b x y);

ite_true (a : sort 1) (x y : a) : Eq a (ite a True x y) x =
  trans a (ite a True x y) (iteDep (\ (b:Bool) -> a) True x y) x
        (ite_eq_iteDep a True x y) (iteDep_True (\ (_:Bool) -> a) x y);

ite_false (a : sort 1) (x y : a) : Eq a (ite a False x y) y =
  trans a (ite a False x y) (iteDep (\ (b:Bool) -> a) False x y) y
        (ite_eq_iteDep a False x y) (iteDep_False (\ (_:Bool) -> a) x y);

--
-- Converting between Bools and Bits (cause why not?)
--

bool2bit : Bool -> Bit;
bool2bit b = iteDep (\ (_:Bool) -> Bit) b Bit1 Bit0;

bool2bit_True : Eq Bit (bool2bit True) Bit1;
bool2bit_True = iteDep_True (\ (_:Bool) -> Bit) Bit1 Bit0;

bool2bit_False : Eq Bit (bool2bit False) Bit0;
bool2bit_False = iteDep_False (\ (_:Bool) -> Bit) Bit1 Bit0;

bit2bool : Bit -> Bool;
bit2bool = Bit__rec (\ (_:Bit) -> Bool) True False;

bit2bool_Bit1 : Eq Bool (bit2bool Bit1) True;
bit2bool_Bit1 = Refl Bool True;

bit2bool_Bit0 : Eq Bool (bit2bool Bit0) False;
bit2bool_Bit0 = Refl Bool False;


--
-- The Boolean operations
--

primitive not : Bool -> Bool;
axiom not__eq : (b:Bool) -> Eq Bool (not b) (ite Bool b False True);

primitive and : Bool -> Bool -> Bool;
axiom and__eq : (b1 b2:Bool) -> Eq Bool (and b1 b2) (ite Bool b1 b2 False);

primitive or : Bool -> Bool -> Bool;
axiom or__eq : (b1 b2:Bool) -> Eq Bool (or b1 b2) (ite Bool b1 True b2);

primitive xor : Bool -> Bool -> Bool;
axiom xor__eq : (b1 b2:Bool) ->
                 Eq Bool (xor b1 b2) (ite Bool b1 (not b2) b2);

-- Decidable Boolean equality, also known as iff
primitive boolEq : Bool -> Bool -> Bool;
axiom boolEq__eq : (b1 b2:Bool) ->
                    Eq Bool (boolEq b1 b2) (ite Bool b1 b2 (not b2));

-- Implies is not a primitive, as it is not mapped by any of the simulator
-- back-ends; instead, it is just defined in terms of or and not
implies : Bool -> Bool -> Bool;
implies = \ (a:Bool) (b:Bool) -> or (not a) b;

-- FIXME: this rule should be derived by scDefRewriteRules
implies__eq : (a b:Bool) -> Eq Bool (implies a b) (or (not a) b);
implies__eq a b = Refl Bool (implies a b);



unitEq : UnitType -> UnitType -> Bool;
unitEq _ _ = True;

pairEq : (a b : sort 0) -> (a -> a -> Bool) -> (b -> b -> Bool) -> a * b -> a * b -> Bool;
pairEq a b f g x y = and ( f x.(1) y.(1) ) ( g x.(2) y.(2) );


--
-- Rewrite rules for booleans
--

not_True : Eq Bool (not True) False;
not_True =
  trans Bool (not True) (ite Bool True False True) False
        (not__eq True) (ite_true Bool False True);

not_False : Eq Bool (not False) True;
not_False =
  trans Bool (not False) (ite Bool False False True) True
        (not__eq False) (ite_false Bool False True);

not_not (x : Bool) : Eq Bool (not (not x)) x =
  iteDep (\ (b:Bool) -> Eq Bool (not (not b)) b) x
         (trans Bool (not (not True)) (not False) True
                (eq_cong Bool (not True) False not_True Bool not)
                not_False)
         (trans Bool (not (not False)) (not True) False
                (eq_cong Bool (not False) True not_False Bool not)
                not_True);


and_True1 (x : Bool) : Eq Bool (and True x) x =
  trans Bool (and True x) (ite Bool True x False) x
        (and__eq True x) (ite_true Bool x False);

and_False1 (x : Bool) : Eq Bool (and False x) False =
  trans Bool (and False x) (ite Bool False x False) False
        (and__eq False x) (ite_false Bool x False);

and_True2 (x : Bool) : Eq Bool (and x True) x =
  iteDep (\ (b:Bool) -> Eq Bool (and b True) b) x
         (and_True1 True) (and_False1 True);

and_False2 (x : Bool) : Eq Bool (and x False) False =
  iteDep (\ (b:Bool) -> Eq Bool (and b False) False) x
         (and_True1 False) (and_False1 False);

and_assoc (x y z : Bool) : Eq Bool (and x (and y z)) (and (and x y) z) =
  iteDep (\ (b:Bool) -> Eq Bool (and x (and y b)) (and (and x y) b)) z
         (trans2 Bool (and x (and y True)) (and (and x y) True) (and x y)
                 (eq_cong Bool (and y True) y (and_True2 y) Bool (and x))
                 (and_True2 (and x y)))
         (trans2 Bool (and x (and y False)) (and (and x y) False) False
                 (trans Bool (and x (and y False)) (and x False) False
                        (eq_cong Bool (and y False) False (and_False2 y) Bool (and x))
                        (and_False2 x))
                 (and_False2 (and x y)));

and_idem (x : Bool) : Eq Bool (and x x) x =
  iteDep (\ (b:Bool) -> Eq Bool (and b b) b) x
         (and_True1 True) (and_False1 False);


or_True1 (x : Bool) : Eq Bool (or True x) True =
  trans Bool (or True x) (ite Bool True True x) True
        (or__eq True x) (ite_true Bool True x);

or_False1 (x : Bool) : Eq Bool (or False x) x =
  trans Bool (or False x) (ite Bool False True x) x
        (or__eq False x) (ite_false Bool True x);

or_True2 (x : Bool) : Eq Bool (or x True) True =
  iteDep (\ (b:Bool) -> Eq Bool (or b True) True) x
         (or_True1 True) (or_False1 True);

or_False2 (x : Bool) : Eq Bool (or x False) x =
  iteDep (\ (b:Bool) -> Eq Bool (or b False) b) x
         (or_True1 False) (or_False1 False);

or_assoc (x y z : Bool) : Eq Bool (or x (or y z)) (or (or x y) z) =
  iteDep (\ (b:Bool) -> Eq Bool (or x (or y b)) (or (or x y) b)) z
         (trans2 Bool (or x (or y True)) (or (or x y) True) True
                 (trans Bool (or x (or y True)) (or x True) True
                        (eq_cong Bool (or y True) True (or_True2 y) Bool (or x))
                        (or_True2 x))
                 (or_True2 (or x y)))
         (trans2 Bool (or x (or y False)) (or (or x y) False) (or x y)
                 (eq_cong Bool (or y False) y (or_False2 y) Bool (or x))
                 (or_False2 (or x y)));

or_idem (x : Bool) : Eq Bool (or x x) x =
  iteDep (\ (b:Bool) -> Eq Bool (or b b) b) x
         (or_True1 True) (or_False1 False);


implies_True1 (x : Bool) : Eq Bool (implies True x) x =
  trans
    Bool (or (not True) x) (or False x) x
    (eq_cong Bool (not True) False not_True
             Bool (\ (y:Bool) -> or y x))
    (or_False1 x);

implies_False1 (x : Bool) : Eq Bool (implies False x) True =
  trans
    Bool (or (not False) x) (or True x) True
    (eq_cong Bool (not False) True not_False
             Bool (\ (y:Bool) -> or y x))
    (or_True1 x);

-- Legacy name
true_implies (x : Bool) : Eq Bool (implies True x) x = implies_True1 x;

xor_True1 (x : Bool) : Eq Bool (xor True x) (not x) =
  trans Bool (xor True x) (ite Bool True (not x) x) (not x)
        (xor__eq True x) (ite_true Bool (not x) x);

xor_False1 (x : Bool) : Eq Bool (xor False x) x =
  trans Bool (xor False x) (ite Bool False (not x) x) x
        (xor__eq False x) (ite_false Bool (not x) x);

xor_False2 (x : Bool) : Eq Bool (xor x False) x =
  iteDep (\ (b:Bool) -> Eq Bool (xor b False) b) x
         (trans Bool (xor True False) (not False) True (xor_True1 False) not_False)
         (xor_False1 False);

xor_True2 (x : Bool) : Eq Bool (xor x True) (not x) =
  iteDep (\ (b:Bool) -> Eq Bool (xor b True) (not b)) x
         (xor_True1 True)
         (trans2 Bool (xor False True) (not False) True (xor_False1 True) not_False);

xor_same (x : Bool) : Eq Bool (xor x x) False =
  iteDep (\ (b:Bool) -> Eq Bool (xor b b) False) x
         (trans Bool (xor True True) (not True) False (xor_True1 True) not_True)
         (xor_False1 False);

boolEq_True1 (x : Bool) : Eq Bool (boolEq True x) x =
  trans Bool (boolEq True x) (ite Bool True x (not x)) x
        (boolEq__eq True x) (ite_true Bool x (not x));

boolEq_False1 (x : Bool) : Eq Bool (boolEq False x) (not x) =
  trans Bool (boolEq False x) (ite Bool False x (not x)) (not x)
        (boolEq__eq False x) (ite_false Bool x (not x));

boolEq_True2 (x : Bool) : Eq Bool (boolEq x True) x =
  iteDep (\ (b:Bool) -> Eq Bool (boolEq b True) b) x
         (boolEq_True1 True)
         (trans Bool (boolEq False True) (not True) False (boolEq_False1 True) not_True);

boolEq_False2 (x : Bool) : Eq Bool (boolEq x False) (not x) =
  iteDep (\ (b:Bool) -> Eq Bool (boolEq b False) (not b)) x
         (trans2 Bool (boolEq True False) (not True) False (boolEq_True1 False) not_True)
         (boolEq_False1 False);

boolEq_same (x : Bool) : Eq Bool (boolEq x x) True =
  iteDep (\ (b:Bool) -> Eq Bool (boolEq b b) True) x
         (boolEq_True1 True)
         (trans Bool (boolEq False False) (not False) True (boolEq_False1 False) not_False);

not_or (x y : Bool) : Eq Bool (not (or x y)) (and (not x) (not y)) =
  iteDep (\ (b:Bool) -> Eq Bool (not (or b y)) (and (not b) (not y)))
         x
         (trans Bool (not (or True y)) False (and (not True) (not y))
                (trans Bool (not (or True y)) (not True) False
                       (eq_cong Bool (or True y) True (or_True1 y)
                                Bool not)
                       not_True)
                (trans Bool False (and False (not y)) (and (not True) (not y))
                       (sym Bool (and False (not y)) False (and_False1 (not y)))
                       (eq_cong Bool False (not True)
                                (sym Bool (not True) False not_True)
                                Bool (\ (z:Bool) -> (and z (not y))))))
         (trans Bool (not (or False y)) (not y) (and (not False) (not y))
                (eq_cong Bool (or False y) y (or_False1 y) Bool not)
                (sym Bool (and (not False) (not y)) (not y)
                     (trans Bool (and (not False) (not y)) (and True (not y))
                            (not y)
                            (eq_cong Bool (not False) True not_False Bool
                                     (\ (z:Bool) -> (and z (not y))))
                            (and_True1 (not y)))));

not_and (x y : Bool)
  : Eq Bool (not (and x y)) (or (not x) (not y)) =
  iteDep (\ (b:Bool) -> Eq Bool (not (and b y)) (or (not b) (not y)))
         x
         (trans Bool (not (and True y)) (not y) (or (not True) (not y))
                (eq_cong Bool (and True y) y (and_True1 y) Bool not)
                (sym Bool (or (not True) (not y)) (not y)
                     (trans Bool (or (not True) (not y)) (or False (not y))
                            (not y)
                            (eq_cong Bool (not True) False not_True Bool
                                     (\ (z:Bool) -> (or z (not y))))
                            (or_False1 (not y)))))
         (trans Bool (not (and False y)) True (or (not False) (not y))
                (trans Bool (not (and False y)) (not False) True
                       (eq_cong Bool (and False y) False (and_False1 y)
                                Bool not)
                       not_False)
                (trans Bool True (or True (not y)) (or (not False) (not y))
                       (sym Bool (or True (not y)) True (or_True1 (not y)))
                       (eq_cong Bool True (not False)
                                (sym Bool (not False) True not_False)
                                Bool (\ (z:Bool) -> (or z (not y))))));

ite_not (a : sort 1) (b : Bool) (x y : a)
  : Eq a (ite a (not b) x y) (ite a b y x) =
  iteDep (\ (b':Bool) -> Eq a (ite a (not b') x y) (ite a b' y x))
         b
         (trans a (ite a (not True) x y) y (ite a True y x)
                (trans a (ite a (not True) x y) (ite a False x y) y
                       (eq_cong Bool (not True) False not_True a
                                (\ (z:Bool) -> ite a z x y))
                       (ite_false a x y))
                (sym a (ite a True y x) y (ite_true a y x)))
         (trans a (ite a (not False) x y) x (ite a False y x)
                (trans a (ite a (not False) x y) (ite a True x y) x
                       (eq_cong Bool (not False) True not_False a
                                (\ (z:Bool) -> ite a z x y))
                       (ite_true a x y))
                (sym a (ite a False y x) x (ite_false a y x)));

ite_nest1 (a : sort 1) (b : Bool) (x y z : a)
  : Eq a (ite a b (ite a b x y) z) (ite a b x z) =
  iteDep (\ (b':Bool) -> Eq a (ite a b' (ite a b' x y) z) (ite a b' x z))
         b
         (trans a (ite a True (ite a True x y) z) x (ite a True x z)
                (trans a (ite a True (ite a True x y) z) (ite a True x y) x
                       (ite_true a (ite a True x y) z)
                       (ite_true a x y))
                (sym a (ite a True x z) x (ite_true a x z)))
         (trans a (ite a False (ite a False x y) z) z (ite a False x z)
                (ite_false a (ite a False x y) z)
                (sym a (ite a False x z) z (ite_false a x z)));

ite_nest2 (a : sort 1) (b : Bool) (x y z : a)
  : Eq a (ite a b x (ite a b y z)) (ite a b x z) =
  iteDep (\ (b':Bool) -> Eq a (ite a b' x (ite a b' y z)) (ite a b' x z))
         b
         (trans a (ite a True x (ite a True y z)) x (ite a True x z)
                (ite_true a x (ite a True y z))
                (sym a (ite a True x z) x (ite_true a x z)))
         (trans a (ite a False x (ite a False y z)) z (ite a False x z)
                (trans a (ite a False x (ite a False y z)) (ite a False y z) z
                       (ite_false a x (ite a False y z))
                       (ite_false a y z))
                (sym a (ite a False x z) z (ite_false a x z)));

-- This is provable with iteDep on b, but yuck!
axiom ite_bit : (b : Bool) -> (c : Bool) -> (d : Bool) ->
                 Eq Bool (ite Bool b c d) (and (or (not b) c) (or b d));

ite_bit_false_1 (b c : Bool)
  : Eq Bool (ite Bool b False c) (and (not b) c) =
  iteDep (\ (b':Bool) -> Eq Bool (ite Bool b' False c) (and (not b') c)) b
         (trans Bool (ite Bool True False c) False (and (not True) c)
                (ite_true Bool False c)
                (sym Bool (and (not True) c) False
                     (trans Bool (and (not True) c) (and False c) False
                            (eq_cong Bool (not True) False not_True
                                     Bool (\ (z:Bool) -> (and z c)))
                            (and_False1 c))))
         (trans Bool (ite Bool False False c) c (and (not False) c)
                (ite_false Bool False c)
                (sym Bool (and (not False) c) c
                     (trans Bool (and (not False) c) (and True c) c
                            (eq_cong Bool (not False) True not_False
                                     Bool (\ (z:Bool) -> (and z c)))
                            (and_True1 c))));

ite_bit_true_1 (b c : Bool) : Eq Bool (ite Bool b True c) (or b c) =
  iteDep (\ (b':Bool) -> Eq Bool (ite Bool b' True c) (or b' c))
         b
         (trans Bool (ite Bool True True c) True (or True c)
                (ite_true Bool True c)
                (sym Bool (or True c) True (or_True1 c)))
         (trans Bool (ite Bool False True c) c (or False c)
                (ite_false Bool True c)
                (sym Bool (or False c) c (or_False1 c)));

ite_fold_not (b : Bool) : Eq Bool (ite Bool b False True) (not b) =
  iteDep (\ (b':Bool) -> Eq Bool (ite Bool b' False True) (not b'))
         b
         (trans Bool (ite Bool True False True) False (not True)
                (ite_true Bool False True)
                (sym Bool (not True) False not_True))
         (trans Bool (ite Bool False False True) True (not False)
                (ite_false Bool False True)
                (sym Bool (not False) True not_False));

ite_eq (a : sort 1) (b : Bool) (x : a) : Eq a (ite a b x x) x =
  iteDep (\ (b':Bool) -> Eq a (ite a b' x x) x)
         b (ite_true a x x) (ite_false a x x);

or_triv1 (x : Bool) : Eq Bool (or x (not x)) True =
  iteDep (\ (b:Bool) -> Eq Bool (or b (not b)) True)
         x
         (or_True1 (not True))
         (trans Bool (or False (not False)) (not False) True
                (or_False1 (not False)) not_False);

or_triv2 (x : Bool) : Eq Bool (or (not x) x) True =
  iteDep (\ (b:Bool) -> Eq Bool (or (not b) b) True)
         x
         (or_True2 (not True))
         (trans Bool (or (not False) False) (not False) True
                (or_False2 (not False)) not_False);

and_triv1 (x : Bool) : Eq Bool (and x (not x)) False =
  iteDep (\ (b:Bool) -> Eq Bool (and b (not b)) False)
         x
         (trans Bool (and True (not True)) (not True) False
                (and_True1 (not True)) not_True)
         (and_False1 (not False));

and_triv2 (x : Bool) : Eq Bool (and (not x) x) False =
  iteDep (\ (b:Bool) -> Eq Bool (and (not b) b) False)
         x
         (trans Bool (and (not True) True) (not True) False
                (and_True2 (not True)) not_True)
         (and_False2 (not False));


--------------------------------------------------------------------------------
-- Converting Booleans to Propositions

EqTrue : Bool -> Prop;
EqTrue x = Eq Bool x True;

TrueProp : Prop;
TrueProp = EqTrue True;

TrueI : EqTrue True;
TrueI = Refl Bool True;

andI : (x y : Bool) -> EqTrue x -> EqTrue y -> EqTrue (and x y);
andI x y p q =
  trans4 Bool (and x y) (and x True) x True
  (eq_cong Bool y True q Bool (and x)) (and_True2 x) p;

impliesI (x y : Bool) : (EqTrue x -> EqTrue y) -> EqTrue (implies x y) =
  iteDep (\ (x : Bool) -> (EqTrue x -> EqTrue y) -> EqTrue (implies x y)) x
         (\ (H : EqTrue True -> EqTrue y) ->
           trans Bool (implies True y) y True (implies_True1 y) (H TrueI))
         (\ (_ : EqTrue False -> EqTrue y) -> implies_False1 y);


--------------------------------------------------------------------------------
-- Either

data Either (s t : sort 0) : sort 0 where {
    Left  : s -> Either s t;
    Right : t -> Either s t;
  }

Either__rec : (s t : sort 0) -> (p : Either s t -> sort 0) ->
               ((l : s) -> p (Left s t l)) ->
               ((r : t) -> p (Right s t r)) ->
               (e : Either s t) -> p e;
Either__rec s t p f1 f2 e = Either#rec s t p f1 f2 e;

-- The eliminator for the Either type
either : (a b c : sort 0) -> (a -> c) -> (b -> c) -> Either a b -> c;
either a b c f g e =
  Either__rec a b (\ (p: Either a b) -> c) f g e;

-- Eta-expanded version of the Left constructor
left : (a b : sort 0) -> a -> Either a b;
left a b x = Left a b x;

-- Eta-expanded version of the Right constructor
right : (a b : sort 0) -> b -> Either a b;
right a b x = Right a b x;

eitherCong0 : (t x y : sort 0) -> Eq (sort 0) x y ->
               Eq (sort 0) (Either x t) (Either y t);
eitherCong0 t x y eq =
  eq_cong (sort 0) x y eq (sort 0) (\ (y':sort 0) -> Either y' t);

eitherCong1 : (t x y : sort 0) -> Eq (sort 0) x y ->
               Eq (sort 0) (Either t x) (Either t y);
eitherCong1 t x y eq =
  eq_cong (sort 0) x y eq (sort 0) (\ (y':sort 0) -> Either t y');

boolToEither : Bool -> Either #() #();
boolToEither b = ite (Either #() #()) b (Left #() #() ()) (Right #() #() ());


--------------------------------------------------------------------------------
-- Maybe

data Maybe (a : sort 0) : sort 0 where {
    Nothing : Maybe a;
    Just : a -> Maybe a;
  }

Maybe__rec : (a : sort 0) -> (p : (Maybe a) -> sort 0) ->
              p (Nothing a) -> ((x:a) -> p (Just a x)) -> (m : Maybe a) -> p m;
Maybe__rec a p f1 f2 m = Maybe#rec a p f1 f2 m;

maybe : (a b : sort 0) -> b -> (a -> b) -> Maybe a -> b;
maybe a b f1 f2 m = Maybe__rec a (\ (m':Maybe a) -> b) f1 f2 m;


--------------------------------------------------------------------------------
-- Nat

data Nat : sort 0 where {
    Zero : Nat;
    Succ : Nat -> Nat;
  }

Nat__rec : (p : Nat -> sort 1) -> p Zero -> ((n:Nat) -> p n -> p (Succ n)) ->
            (n:Nat) -> p n;
Nat__rec p f1 f2 n = Nat#rec p f1 f2 n;

Nat_cases : (a:sort 1) -> a -> (Nat -> a -> a) -> Nat -> a;
Nat_cases a f1 f2 n = Nat__rec (\ (n:Nat) -> a) f1 f2 n;

-- Build a binary function for Nats that satisfies:
--   Nat_cases2 a f1 f2 f3 Zero y = f1 y
--   Nat_cases2 a f1 f2 f3 (Succ x) Zero = f2 x
--   Nat_cases2 a f1 f2 f3 (Succ x) (Succ y) = f3 x y (Nat_cases2 ... x y)
Nat_cases2 : (a:sort 1) -> (Nat -> a) -> (Nat -> a) ->
              (Nat -> Nat -> a -> a) -> Nat -> Nat -> a;
Nat_cases2 a f1 f2 f3 n m =
  Nat__rec (\ (n:Nat) -> Nat -> a) f1
          (\ (n:Nat) -> \ (f_rec : Nat -> a) -> \ (m:Nat) ->
             Nat__rec (\ (m':Nat) -> a) (f2 n)
                      (\ (m':Nat) -> \ (frec':a) -> f3 n m' (f_rec m')) m) n m;

eqNat : Nat -> Nat -> sort 1;
eqNat x y = Eq Nat x y;

eqNatSucc : (x y : Nat) -> eqNat x y -> eqNat (Succ x) (Succ y);
eqNatSucc x y eq = eq_cong Nat x y eq Nat (\ (n:Nat) -> Succ n);

-- Predecessor
pred : Nat -> Nat;
pred x = Nat_cases Nat Zero (\ (n:Nat) -> \ (m:Nat) -> n) x;

eqNatPrec : (x y : Nat) -> eqNat (Succ x) (Succ y) -> eqNat x y;
eqNatPrec x y eq' =
  eq_cong Nat (Succ x) (Succ y) eq' Nat pred;

-- | Propositional less than or equal to; defined the same way as in Coq
data IsLeNat (n:Nat) : Nat -> Prop where {
  IsLeNat_base : IsLeNat n n;
  IsLeNat_succ : (m:Nat) -> IsLeNat n m -> IsLeNat n (Succ m);
}

-- | m < n is defined as m+1 <= n (as in Coq)
IsLtNat : Nat -> Nat -> Prop;
IsLtNat m n = IsLeNat (Succ m) n;

-- | Restate the recursor on IsLeNat
IsLeNat__rec :
  (n  : Nat) ->
  (p  : (x : Nat) -> IsLeNat n x -> Prop) ->
  (Hbase : p n (IsLeNat_base n)) ->
  (Hstep : (x : Nat) -> (H : IsLeNat n x) -> p x H -> p (Succ x) (IsLeNat_succ n x H)) ->
  (m : Nat) -> (Hm : IsLeNat n m) -> p m Hm;
IsLeNat__rec n p Hbase Hstep m Hm = IsLeNat#rec n p Hbase Hstep m Hm;

-- | Test if m < n or n <= m
-- FIXME: implement this!
primitive natCompareLe : (m n : Nat) -> Either (IsLtNat m n) (IsLeNat n m);

-- | Test if m = n
-- FIXME: implement this!
primitive proveEqNat : (m n : Nat) -> Maybe (Eq Nat m n);

-- | Try to prove x <= y (FIXME: implement this from natCompareLe!)
primitive proveLeNat : (x y : Nat) -> Maybe (IsLeNat x y);

-- | Try to prove x < y
proveLtNat : (x y : Nat) -> Maybe (IsLtNat x y);
proveLtNat x y = proveLeNat (Succ x) y;


-- | Addition
addNat : Nat -> Nat -> Nat;
addNat x y =
  Nat_cases Nat y (\ (_:Nat) -> \ (prev_sum:Nat) -> Succ prev_sum) x;

eqNatAdd0 (x : Nat) : eqNat (addNat x 0) x =
  Nat__rec (\ (n:Nat) -> eqNat (addNat n 0) n)
           (Refl Nat 0)
           (\ (n:Nat) -> eqNatSucc (addNat n 0) n)
           x;

eqNatAddS (x y : Nat) : eqNat (addNat x (Succ y)) (Succ (addNat x y)) =
  Nat__rec (\ (x':Nat) -> (y':Nat) ->
              eqNat (addNat x' (Succ y')) (Succ (addNat x' y')))
           (\ (y':Nat) -> Refl Nat (Succ y'))
           (\ (x':Nat) ->
            \ (eqF : (y':Nat) ->
                      eqNat (addNat x' (Succ y')) (Succ (addNat x' y'))) ->
            \ (y':Nat) ->
              eqNatSucc (addNat x' (Succ y')) (Succ (addNat x' y')) (eqF y'))
           x y;

eqNatAddComm (x y : Nat) : eqNat (addNat x y) (addNat y x) =
  Nat__rec (\ (y':Nat) -> (x':Nat) -> eqNat (addNat x' y') (addNat y' x'))
           (\ (x':Nat) -> eqNatAdd0 x')
           (\ (y':Nat) ->
            \ (eqF : (x':Nat) -> eqNat (addNat x' y') (addNat y' x')) ->
            \ (x':Nat) ->
              trans Nat
                    (addNat x' (Succ y'))
                    (Succ (addNat x' y'))
                    (Succ (addNat y' x'))
                    (eqNatAddS x' y')
                    (eqNatSucc (addNat x' y') (addNat y' x') (eqF x')))
           y x;

addNat_assoc (x y z : Nat) : eqNat (addNat x (addNat y z)) (addNat (addNat x y) z) =
  Nat__rec (\ (x':Nat) -> eqNat (addNat x' (addNat y z)) (addNat (addNat x' y) z))
           (Refl Nat (addNat y z))
           (\ (x':Nat) ->
            \ (eq : eqNat (addNat x' (addNat y z)) (addNat (addNat x' y) z)) ->
              eqNatSucc (addNat x' (addNat y z)) (addNat (addNat x' y) z) eq)
           x;

-- | Multiplication
mulNat : Nat -> Nat -> Nat;
mulNat x y =
  Nat__rec (\ (x':Nat) -> Nat) 0
           (\ (x':Nat) -> \ (prod:Nat) -> addNat y prod) x;

equal0Nat : Nat -> Bool;
equal0Nat n =
  Nat_cases Bool True (\ (n:Nat) -> \ (b:Bool) -> False) n;

equalNat : Nat -> Nat -> Bool;
equalNat x y =
  Nat_cases (Nat -> Bool) equal0Nat
            (\ (n':Nat) -> \ (eqN : Nat -> Bool) -> \ (m:Nat) ->
               Nat_cases Bool False
                         (\ (m':Nat) -> \ (b:Bool) -> eqN m') m) x y;

ltNat : Nat -> Nat -> Bool;
ltNat x y =
  Nat_cases2 Bool (\ (x':Nat) -> False)
             (\ (y':Nat) -> True)
             (\ (y':Nat) -> \ (x':Nat) -> \ (lt_mn:Bool) -> lt_mn) y x;

-- | Subtraction
subNat : Nat -> Nat -> Nat;
subNat x y =
  Nat_cases2 Nat (\ (x':Nat) -> x')
             (\ (y':Nat) -> Zero)
             (\ (y':Nat) -> \ (x':Nat) -> \ (sub_xy:Nat) -> sub_xy) y x;

-- | Minimum
minNat : Nat -> Nat -> Nat;
minNat x y =
  Nat_cases2 Nat (\ (y':Nat) -> Zero)
             (\ (x':Nat) -> Zero)
             (\ (x':Nat) -> \ (y':Nat) -> \ (min_xy:Nat) -> Succ min_xy) x y;

-- | Maximum
maxNat : Nat -> Nat -> Nat;
maxNat x y =
  Nat_cases2 Nat (\ (y':Nat) -> y')
             (\ (x':Nat) -> Succ x')
             (\ (x':Nat) -> \ (y':Nat) -> \ (max_xy:Nat) -> Succ max_xy) x y;

-- | Width(n) = 1 + floor(log_2(n))
primitive widthNat : Nat -> Nat;

-- | Natural exponentiation
expNat : Nat -> Nat -> Nat;
expNat b e =
  Nat_cases Nat 1 (\ (e':Nat) -> \ (exp_b_e:Nat) -> mulNat b exp_b_e) e;

-- | Natural division and modulus
primitive divModNat : Nat -> Nat -> Nat * Nat;

divNat : Nat -> Nat -> Nat;
divNat x y = (divModNat x y).(1);

modNat : Nat -> Nat -> Nat;
modNat x y = (divModNat x y).(2);

-- There are implicit constructors from integer literals.

-- Dependent, non-recursive pattern matching combinator for natural numbers
natCase : (p : Nat -> sort 0) -> p Zero -> ((n : Nat) -> p (Succ n)) ->
           (n : Nat) -> p n;
natCase p z s = Nat__rec p z (\ (n:Nat) -> \ (r:p n) -> s n);

-- An if-then-else for whether a Nat = 0
if0Nat : (a : sort 0) -> Nat -> a -> a -> a;
if0Nat a n x y = natCase (\ (_:Nat) -> a) x (\ (_:Nat) -> y) n;

-- An exponentation operation on arbitrary types.
--
-- The arguments are: the 1 value for a;
-- the multiplication operation, the base of the exponent
-- and the number of times to multiply.
primitive expByNat : (a:sort 0) -> a -> (a -> a -> a) -> a -> Nat -> a;


-- | LeNat is transitive
IsLeNat_transitive :
  (n m o:Nat) ->
  IsLeNat n m ->
  IsLeNat m o ->
  IsLeNat n o;
IsLeNat_transitive n m o Hnm Hmo =
  IsLeNat__rec m
    (\ (x:Nat) -> \(H:IsLeNat m x) -> IsLeNat n x)
    Hnm
    (\ (x:Nat) -> \ (H1:IsLeNat m x) -> \ (H2:IsLeNat n x) -> IsLeNat_succ n x H2)
  o Hmo;

-- No Nat is strictly less than zero
IsLtNat_Zero_absurd :
  (p:Prop) ->
  (m:Nat) ->
  IsLtNat m Zero ->
  p;
IsLtNat_Zero_absurd p m HSmZ =
  IsLeNat__rec (Succ m)
    ( \ (x : Nat) -> \ (H:IsLeNat (Succ m) x) -> if0Nat Prop x p TrueProp)
    TrueI
    ( \ (x : Nat) -> \ (H1:IsLeNat (Succ m) x) -> \ (H2 : if0Nat Prop x p TrueProp) -> TrueI)
    Zero HSmZ;

IsLeNat_SuccSucc :
  (n m:Nat) ->
  IsLeNat (Succ n) (Succ m) ->
  IsLeNat n m;
IsLeNat_SuccSucc n m HSS =
  IsLeNat__rec (Succ n)
    ( \ (x : Nat) -> \ (H:IsLeNat (Succ n) x) -> IsLeNat n (pred x))
    (IsLeNat_base n)
    (Nat__rec
      ( \ (x : Nat) -> IsLeNat (Succ n) x -> IsLeNat n (pred x) -> IsLeNat n x)
      ( \ (H1 : IsLeNat (Succ n) Zero) -> \ (H2 : IsLeNat n (pred Zero)) -> H2)
      ( \ (x : Nat) ->
        \ (Hind : IsLeNat (Succ n) x -> IsLeNat n (pred x) -> IsLeNat n x) ->
        \ (H1 : IsLeNat (Succ n) (Succ x)) ->
	\ (H2 : IsLeNat n (pred (Succ x))) ->
	IsLeNat_succ n x H2)
    )
  (Succ m) HSS;

-- | The complete induction principle on natural numbers
Nat_complete_induction :
  (p : Nat -> Prop) ->
  ((n : Nat) -> ((m : Nat) -> IsLtNat m n -> p m) -> p n) ->
  (n : Nat) -> p n;

Nat_complete_induction p f n0 =
  Nat__rec ( \ (n:Nat) -> (m:Nat) -> IsLeNat m n -> p m)
    (\ (n:Nat) ->
     \ (Hn:IsLeNat n 0) ->
     f n (\ (m:Nat) -> \ (Hm : IsLeNat (Succ m) n) ->
            IsLtNat_Zero_absurd (p m) m (IsLeNat_transitive (Succ m) n 0 Hm Hn))
    )
   (\ (n:Nat) ->
     \ (Hind : (m:Nat) -> IsLeNat m n -> p m) ->
     \ (r:Nat) ->
     \ (Hr:IsLeNat r (Succ n)) ->
       f r (\ (m:Nat) -> \ (Hm: IsLeNat (Succ m) r) ->
             Hind m (IsLeNat_SuccSucc m n (IsLeNat_transitive (Succ m) r (Succ n) Hm Hr)))
    )
    n0 n0 (IsLeNat_base n0);




--------------------------------------------------------------------------------
-- Operations on string values

primitive equalString : String -> String -> Bool;


--------------------------------------------------------------------------------
-- "Vec n a" is an array of n elements, each with type "a".
primitive Vec : Nat -> sort 0 -> sort 0;

-- Primitive function for generating an array.
primitive gen : (n : Nat) -> (a : sort 0) -> (Nat -> a) -> Vec n a;

-- Primitive eliminators for arrays
primitive head : (n : Nat) -> (a : sort 0) -> Vec (Succ n) a -> a;
primitive tail : (n : Nat) -> (a : sort 0) -> Vec (Succ n) a -> Vec n a;

-- An implementation for atWithDefault
--
-- FIXME: can we replace atWithDefault with this implementation? Or does some
-- automation rely on atWithDefault being a primitive?
atWithDefault' : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> a;
atWithDefault' n_top a d =
  Nat__rec
    (\ (n:Nat) -> Vec n a -> Nat -> a)
    (\ (_:Vec 0 a) (_:Nat) -> d)
    (\ (n:Nat) (rec_f: Vec n a -> Nat -> a) (v:Vec (Succ n) a) (i:Nat) ->
       Nat_cases a (head n a v)
                 (\ (i_prev:Nat) (_:a) -> rec_f (tail n a v) i_prev) i)
    n_top;

primitive atWithDefault : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> a;

at : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a;
at n a v i = atWithDefault n a (error a "at: index out of bounds") v i;
-- `at n a v i` has the precondition `ltNat i n`

primitive EmptyVec : (a : sort 0) -> Vec 0 a;

ConsVec : (a : isort 0) -> a -> (n : Nat) -> Vec n a -> Vec (Succ n) a;
ConsVec a x n v =
  gen (Succ n) a (Nat_cases a x (\ (i:Nat) -> \ (a':a) -> at n a v i));

upd : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a -> Vec n a;
upd n a v j x = gen n a (\ (i : Nat) -> ite a (equalNat i j) x (at n a v i));
-- TODO: assertion that j < n

-- | Defines a function that maps array elements from one range to another.
map : (a : isort 0) -> (b : sort 0) -> (a -> b) -> (n : Nat) -> Vec n a -> Vec n b;
map a b f n v = gen n b (\ (i : Nat) -> f (at n a v i));

-- | Defines a function that maps array elements from one range to another.
zipWith : (a b : isort 0) -> (c : sort 0)
        -> (a -> b -> c)
        -> (n : Nat) -> Vec n a -> Vec n b -> Vec n c;
zipWith a b c f n x y = gen n c (\ (i : Nat) -> f (at n a x i) (at n b y i));

-- replicate n x returns an array with n copies of x.
replicate : (n : Nat) -> (a : sort 0) -> a -> Vec n a;
replicate n a x = gen n a (\ (_ : Nat) -> x);

-- | Create a vector of length 1.
single : (a : sort 0) -> a -> Vec 1 a;
single = replicate 1;

axiom at_single : (a : sort 0) -> (x : a) -> (i : Nat) -> Eq a (at 1 a (single a x) i) x;

-- Zip together two lists (truncating the longer of the two).
primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);

primitive foldr : (a b : sort 0) -> (n : Nat) -> (a -> b -> b) -> b -> Vec n a -> b;
primitive foldl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> b;
primitive scanl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> Vec (addNat 1 n) b;

reverse : (n : Nat) -> (a : isort 0) -> Vec n a -> Vec n a;
reverse n a xs = gen n a (\ (i : Nat) -> at n a xs (subNat (subNat n 1) i));

transpose : (m n : Nat) -> (a : isort 0) -> Vec m (Vec n a) -> Vec n (Vec m a);
transpose m n a xss =
  gen n (Vec m a) (\ (j : Nat) ->
    gen m a (\ (i : Nat) -> at n a (at m (Vec n a) xss i) j));

-- | Return true if two vectors are equal, given a comparison function
-- for elements.
vecEq : (n : Nat) -> (a : isort 0) -> (a -> a -> Bool)
      -> Vec n a -> Vec n a -> Bool;
vecEq n a eqFn x y =
  foldr Bool Bool n and True (zipWith a a Bool eqFn n x y);

-- | Take a prefix of a vector.
take : (a : isort 0) -> (m n : Nat) -> Vec (addNat m n) a -> Vec m a;
take a m n v = gen m a (\ (i : Nat) -> at (addNat m n) a v i);

vecCong : (a : sort 0) -> (m n : Nat) -> Eq Nat m n ->
           Eq (sort 0) (Vec m a) (Vec n a);
vecCong a m n eq = eq_cong Nat m n eq (sort 0) (\ (i:Nat) -> Vec i a);

coerceVec : (a : sort 0) -> (m n : Nat) -> Eq Nat m n -> Vec m a -> Vec n a;
coerceVec a m n q = coerce (Vec m a) (Vec n a) (vecCong a m n q);

-- | Simplify take  all elements from a vector.
axiom take0 : (a : sort 0)
       -> (m : Nat)
       -> (v : Vec (addNat m 0) a)
       -> Eq (Vec m a)
             (take a m 0 v)
             (coerceVec a (addNat m 0) m (eqNatAdd0 m) v);

-- | Returns a suffix of a vector after a given number of elements.
drop : (a : isort 0) -> (m n : Nat) -> Vec (addNat m n) a -> Vec n a;
drop a m n v = gen n a (\ (i : Nat) -> at (addNat m n) a v (addNat m i));

-- | Simplify drop 0-elements from a vector.
axiom drop0 : (a : sort 0)
       -> (n : Nat)
       -> (v : Vec (addNat 0 n) a)
       -> Eq (Vec n a) (drop a 0 n v) v;

-- | Select a range [i,..,i+n] of values from the array.
slice : (a : isort 0)
      -> (m n o : Nat)
      -> Vec (addNat (addNat m n) o) a -> Vec n a;
slice a m n o v = drop a m n (take a (addNat m n) o v);

-- Concatenate arrays together.
join  : (m n : Nat)
       -> (a : isort 0)
       -> Vec m (Vec n a)
       -> Vec (mulNat m n) a;
join m n a v =
  gen (mulNat m n) a (\ (i : Nat) ->
    at n a (at m (Vec n a) v (divNat i n)) (modNat i n));

-- Split array into list
split : (m n : Nat) -> (a : isort 0) -> Vec (mulNat m n) a -> Vec m (Vec n a);
split m n a v =
  gen m (Vec n a) (\ (i : Nat) ->
    gen n a (\ (j : Nat) ->
      at (mulNat m n) a v (addNat (mulNat i n) j)));

-- Append two arrays together.
append : (m n : Nat) -> (a : isort 0) -> Vec m a -> Vec n a -> Vec (addNat m n) a;
append m n a x y =
  gen (addNat m n) a
    (\ (i : Nat) ->
      ite a (ltNat i m) (at m a x i) (at n a y (subNat i m)));

-- Rotate array to the left.
primitive rotateL : (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> Vec n a;
-- rotateL n a v i = gen n a (\ (j:Nat) -> at n a v (modNat (addNat i j) n));

-- Rotate array to the right.
primitive rotateR : (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> Vec n a;
-- rotateR n a v i = gen n a (\ (j:Nat) -> at n a v (modNat (addNat (subNat n i) j) n));

-- Shift array to the left.
primitive shiftL : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> Vec n a;

-- Shift array to the right.
primitive shiftR : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> Vec n a;

joinLittleEndian  : (m n : Nat)
                  -> (a : isort 0)
                  -> Vec m (Vec n a)
                  -> Vec (mulNat m n) a;
joinLittleEndian m n a v = join m n a (reverse m (Vec n a) v);

splitLittleEndian : (m n : Nat)
                  -> (a : isort 0)
                  -> Vec (mulNat m n) a
                  -> Vec m (Vec n a);
splitLittleEndian m n a v = reverse m (Vec n a) (split m n a v);

--------------------------------------------------------------------------------
-- Bitvectors

-- Bitvector operations expect the most-significant bit first.

-- | Returns most-significant bit in a signed bitvector.
msb : (n : Nat) -> Vec (Succ n) Bool -> Bool;
msb n v = at (Succ n) Bool v 0;

-- | Returns least-significant bit in a bitvector.
lsb : (n : Nat) -> Vec (Succ n) Bool -> Bool;
lsb n v = at (Succ n) Bool v n;

-- | (bvNat n x) yields (x mod 2^n) as an n-bit vector.
primitive bvNat : (n : Nat) -> Nat -> Vec n Bool;

-- | Satisfies @bvNat n (bvToNat n x) = x@.
primitive bvToNat : (n : Nat) -> Vec n Bool -> Nat;

axiom bvNat_bvToNat_id : (n : Nat) -> (x : Vec n Bool) ->
                         Eq (Vec n Bool) (bvNat n (bvToNat n x)) x;

bvAt : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool
     -> a;
bvAt n a w xs i = at n a xs (bvToNat w i);

bvUpd : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool
      -> a -> Vec n a;
bvUpd n a w xs i y = upd n a xs (bvToNat w i) y;

bvRotateL : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool -> Vec n a;
bvRotateL n a w xs i = rotateL n a xs (bvToNat w i);

bvRotateR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool -> Vec n a;
bvRotateR n a w xs i = rotateR n a xs (bvToNat w i);

bvShiftL : (n : Nat) -> (a : isort 0) -> (w : Nat) -> a -> Vec n a -> Vec w Bool -> Vec n a;
bvShiftL n a w z xs i = shiftL n a z xs (bvToNat w i);

bvShiftR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> a -> Vec n a -> Vec w Bool -> Vec n a;
bvShiftR n a w z xs i = shiftR n a z xs (bvToNat w i);

-- A version of bvShiftR that uses the 0th element of the input Vec as the default shift value
bvSShiftR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec (Succ n) a -> Vec w Bool -> Vec (Succ n) a;
bvSShiftR n a w xs i = bvShiftR (Succ n) a w (at (Succ n) a xs 0) xs i;

primitive bvAdd : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;

-- | Unsigned and signed comparison functions.
primitive bvugt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
primitive bvuge : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
primitive bvult : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
primitive bvule : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;

primitive bvsgt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
primitive bvsge : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
primitive bvslt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
primitive bvsle : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;

primitive bvPopcount : (n : Nat) -> Vec n Bool -> Vec n Bool;
primitive bvCountLeadingZeros : (n : Nat) -> Vec n Bool -> Vec n Bool;
primitive bvCountTrailingZeros : (n : Nat) -> Vec n Bool -> Vec n Bool;

-- Universal quantification over bitvectors
primitive bvForall : (n : Nat) -> (Vec n Bool -> Bool) -> Bool;

bvCarry : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
bvCarry n x y = bvult n (bvAdd n x y) x;

bvSCarry : (n : Nat) -> Vec (Succ n) Bool -> Vec (Succ n) Bool -> Bool;
bvSCarry n x y = and (boolEq (msb n x) (msb n y)) (xor (msb n x) (msb n (bvAdd (Succ n) x y)));

bvAddWithCarry : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool * Vec n Bool;
bvAddWithCarry n x y = (bvCarry n x y, bvAdd n x y);

axiom bvAddZeroL : (n : Nat) -> (x : Vec n Bool) -> Eq (Vec n Bool) (bvAdd n (bvNat n 0) x) x;
axiom bvAddZeroR : (n : Nat) -> (x : Vec n Bool) -> Eq (Vec n Bool) (bvAdd n x (bvNat n 0)) x;

primitive bvNeg : (n : Nat) -> Vec n Bool -> Vec n Bool;

primitive bvSub : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;

bvSBorrow : (n : Nat) -> Vec (Succ n) Bool -> Vec (Succ n) Bool -> Bool;
bvSBorrow n x y = and (xor (msb n x) (msb n y)) (xor (msb n x) (msb n (bvSub (Succ n) x y)));

primitive bvMul : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
primitive bvLg2 : (n : Nat) -> Vec n Bool -> Vec n Bool;

-- Unsigned division and remainder.
--
-- When the divisor is 0, bvUDiv returns a vector with all bits set.
-- (Equal to 2^x - 1), and bvURem returns the divident unchanged.
--
-- These two functions satisfy the property that:
--   bvAdd x (bvMul x (bvUDiv x u v) v) (bvURem x u v) == u
primitive bvUDiv : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
primitive bvURem : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;


-- Signed division.
-- When the divisor is 0, bvSDiv returns 2^x - 1 when the dividend
-- is non-negative, and -1 when the dividend is negative; bvSRem
-- returns the dividend unchanged.
--
-- Otherwise, the sign of the quotient is the exclusive xor of
-- the sign bit of the dividend and divisor; the remainder is negative
-- if the dividend is negative.

-- bvSDiv and bvSRem satisfy the property that:
--
--   bvAdd x (bvMul x (bvSDiv x u v) v) (bvSRem x u v) == u
primitive bvSDiv : (n : Nat) -> Vec (Succ n) Bool -> Vec (Succ n) Bool -> Vec (Succ n) Bool;
primitive bvSRem : (n : Nat) -> Vec (Succ n) Bool -> Vec (Succ n) Bool -> Vec (Succ n) Bool;
--TODO:

-- | Shift left by the given number of bits.
-- New bits are False.
primitive bvShl : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;

-- Logical right shift.  New bits are False.
primitive bvShr : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;

-- | Signed right shift.  New bits are equal to most-significant bit.
primitive bvSShr : (w : Nat) -> Vec (Succ w) Bool -> Nat -> Vec (Succ w) Bool;

axiom bvShiftL_bvShl :
  (n : Nat) -> (w : Nat) -> (x : Vec n Bool) -> (i : Vec w Bool) ->
  Eq (Vec n Bool) (bvShiftL n Bool w False x i) (bvShl n x (bvToNat w i));

axiom bvShiftR_bvShr :
  (n : Nat) -> (w : Nat) -> (x : Vec n Bool) -> (i : Vec w Bool) ->
  Eq (Vec n Bool) (bvShiftR n Bool w False x i) (bvShr n x (bvToNat w i));

-- | Zipwith specialized to bitvectors.
bvZipWith : (Bool -> Bool -> Bool)
          -> (n : Nat)
          -> Vec n Bool -> Vec n Bool -> Vec n Bool;
bvZipWith = zipWith Bool Bool Bool;

-- | Bitwise complement.
bvNot : (n : Nat) -> Vec n Bool -> Vec n Bool;
bvNot = map Bool Bool not;

-- | Pairwise conjunction
bvAnd : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
bvAnd = bvZipWith and;

-- | Pairwise disjunction
bvOr : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
bvOr  = bvZipWith or;

-- | Pairwise exclusive or
bvXor : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
bvXor = bvZipWith xor;

-- | Return true if two bitvectors are equal.
bvEq : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
bvEq n x y = vecEq n Bool boolEq x y;

axiom bvEq_refl : (n : Nat) -> (x : Vec n Bool) -> Eq Bool (bvEq n x x) True;

axiom equalNat_bv : (n : Nat) -> (x : Vec n Bool) -> (i : Nat) ->
               Eq Bool (equalNat i (bvToNat n x)) (bvEq n (bvNat n i) x);

-- | Returns the bitvector 1 if the boolean is true,
--   and returns 0 otherwise
bvBool : (n : Nat) -> Bool -> Vec n Bool;
bvBool n b = ite (Vec n Bool) b (bvNat n 1) (bvNat n 0);

-- | Return true if two bitvectors are not equal.
bvNe : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
bvNe n x y = not (bvEq n x y);

-- | Return true if the bitvector is nonzero
bvNonzero : (n : Nat) -> Vec n Bool -> Bool;
bvNonzero n x = bvNe n x (bvNat n 0);

-- | Truncates a vector a smaller size.
-- msb implementation:
bvTrunc : (m n : Nat) -> Vec (addNat m n) Bool -> Vec n Bool;
bvTrunc = drop Bool;
-- lsb implementation:
-- bvTrunc : (m n : Nat) -> Vec (addNat n m) Bool -> Vec n Bool;
-- bvTrunc m n = take Bool n m;

-- | Perform a unsigned extension of the bitvector.
-- @bvUExt m n x@ adds m bits of zeros to the most-significant bits of
-- the n-bit vector x.
-- msb implementation:
bvUExt : (m n : Nat) -> Vec n Bool -> Vec (addNat m n) Bool;
bvUExt m n x = append m n Bool (bvNat m 0) x;
-- lsb implementation:
-- bvUExt : (m n : Nat) -> Vec n Bool -> Vec (addNat n m) Bool;
-- bvUExt m n a = append n m Bool x (bvNat m 0);

-- | 'replicateBool' is an version of 'replicate' optimized for type Bool.
replicateBool : (n : Nat) -> Bool -> Vec n Bool;
replicateBool n b = ite (Vec n Bool) b (bvNot n (bvNat n 0)) (bvNat n 0);

-- | Perform a signed extension of the bitvector.
-- msb implementation:
bvSExt : (m n : Nat) -> Vec (Succ n) Bool -> Vec (addNat m (Succ n)) Bool;
bvSExt m n x = append m (Succ n) Bool (replicateBool m (msb n x)) x;
-- lsb implementation:
-- bvSExt : (m n : Nat) -> Vec (Succ n) Bool -> Vec (addNat (Succ n) m) Bool;
-- bvSExt m n x = append (Succ n) m Bool x (replicateBool m (msb n x));

--------------------------------------------------------------------------------
-- Infinite streams

data Stream (a : sort 0) : sort 0 where {
    MkStream : (Nat -> a) -> Stream a;
  }

injectCode "Coq"
  "Instance Inhabited_Stream (a:Type) (Ha:Inhabited a) : Inhabited (Stream a) := MkInhabited (Stream a) (MkStream a (fun _ => inhabitant)).";

Stream__rec : (a:sort 0) -> (p:Stream a -> sort 0) ->
               ((f:Nat -> a) -> p (MkStream a f)) -> (str:Stream a) -> p str;
Stream__rec a p f1 str = Stream#rec a p f1 str;

streamUpd : (a : sort 0) -> Stream a -> Nat -> a -> Stream a;
streamUpd a strm i y =
  Stream__rec a (\ (strm':Stream a) -> Stream a)
              (\ (s:Nat -> a) ->
                 MkStream a (\ (j : Nat) -> ite a (equalNat i j) y (s j))) strm;

bvStreamUpd : (a : sort 0) -> (w : Nat) ->
     Stream a -> Vec w Bool -> a -> Stream a;
bvStreamUpd a w xs i y = streamUpd a xs (bvToNat w i) y;

streamGet : (a : sort 0) -> Stream a -> Nat -> a;
streamGet a strm i =
  Stream__rec a (\ (strm':Stream a) -> a) (\ (s:Nat -> a) -> s i) strm;

streamConst : (a : sort 0) -> a -> Stream a;
streamConst a x = MkStream a (\ (i : Nat) -> x);

streamMap : (a b : sort 0) -> (a -> b) -> Stream a -> Stream b;
streamMap a b f xs = MkStream b (\ (i : Nat) -> f (streamGet a xs i));

streamMap2 : (a b c : sort 0) -> (a -> b -> c) ->
              Stream a -> Stream b -> Stream c;
streamMap2 a b c f xs ys =
  MkStream c (\ (i : Nat) -> f (streamGet a xs i) (streamGet b ys i));

streamTake : (a : sort 0) -> (n : Nat) -> Stream a -> Vec n a;
streamTake a n xs = gen n a (\ (i : Nat) -> streamGet a xs i);

streamDrop : (a : sort 0) -> (n : Nat) -> Stream a -> Stream a;
streamDrop a n xs = MkStream a (\ (i : Nat) -> streamGet a xs (addNat n i));

streamAppend : (a : sort 0) -> (n : Nat) -> Vec n a -> Stream a -> Stream a;
streamAppend a n xs ys =
  MkStream a (\ (i : Nat) ->
    atWithDefault n a (streamGet a ys (subNat i n)) xs i);

streamJoin : (a : isort 0) -> (n : Nat)
           -> Stream (Vec (Succ n) a)
           -> (Stream a);
streamJoin a n s =
  MkStream a (\ (i:Nat) ->
     at (Succ n) a (streamGet (Vec (Succ n) a) s (divNat i (Succ n)))
                   (modNat i (Succ n)) );

streamSplit : (a : sort 0) -> (n : Nat) -> Stream a -> Stream (Vec n a);
streamSplit a n xs =
  MkStream (Vec n a) (\ (i : Nat) ->
    gen n a (\ (j : Nat) ->
      streamGet a xs (addNat (mulNat i n) j)));

streamShiftL : (a : sort 0) -> Stream a -> Nat -> Stream a;
streamShiftL a xs i = streamDrop a i xs;

streamShiftR : (a : sort 0) -> a -> Stream a -> Nat -> Stream a;
streamShiftR a z xs i = streamAppend a i (replicate i a z) xs;

-- TODO "streamScanl" should probably be a primitive.  However, stream
-- primitives are complicated to implement because the backends have different
-- implementations for streams, and there is no uniform place to implement them.
--
-- We explicitly use "fix" here to implement sharing in the stream.  A naive
-- implementation that just iterates "f" separate for each index would waste work.
-- The fixpoint is well founded because each element only refers to elements with
-- smaller indices.
--
-- For Coq support, this definition is replaced with a naive implementation
-- that performs independent iterations for each location.
streamScanl : (a b : sort 0) -> (b -> a -> b) -> b -> Stream a -> Stream b;
streamScanl a b f z as =
  fix (Stream b)
    (\ (bs : Stream b) -> MkStream b
      (natCase (\ (n : Nat) -> b)
         -- zero case
         z
	 -- successor case
	 (\ (n : Nat) -> f (streamGet b bs n) (streamGet a as n)))
    );

--------------------------------------------------------------------------------
-- Integer values
--   integer values of unbounded precision

primitive Integer : sort 0;

primitive intAdd : Integer -> Integer -> Integer;
primitive intSub : Integer -> Integer -> Integer;
primitive intMul : Integer -> Integer -> Integer;
primitive intDiv : Integer -> Integer -> Integer;
primitive intMod : Integer -> Integer -> Integer;
primitive intMin : Integer -> Integer -> Integer;
primitive intMax : Integer -> Integer -> Integer;
primitive intNeg : Integer -> Integer;
primitive intAbs : Integer -> Integer;
primitive intEq  : Integer -> Integer -> Bool;
primitive intLe  : Integer -> Integer -> Bool;
primitive intLt  : Integer -> Integer -> Bool;

-- intToNat x == max 0 x
primitive intToNat : Integer -> Nat;
primitive natToInt : Nat -> Integer;

-- for x >= 0, intToBv n x = x `mod` 2^n
-- for x <  0, intToBv n x = bvNeg n (-x `mod` 2^n)
primitive intToBv : (n:Nat) -> Integer -> Vec n Bool;

-- return the unsigned value of the bitvector as an integer
primitive bvToInt : (n:Nat) -> Vec n Bool -> Integer;

-- return the 2's complement signed value of the bitvector as an integer
primitive sbvToInt : (n:Nat) -> Vec n Bool -> Integer;


--------------------------------------------------------------------------------
-- Integers mod n

primitive IntMod : Nat -> sort 0;

primitive toIntMod : (n : Nat) -> Integer -> IntMod n;
primitive fromIntMod : (n : Nat) -> IntMod n -> Integer;

primitive intModEq  : (n : Nat) -> IntMod n -> IntMod n -> Bool;
primitive intModAdd : (n : Nat) -> IntMod n -> IntMod n -> IntMod n;
primitive intModSub : (n : Nat) -> IntMod n -> IntMod n -> IntMod n;
primitive intModMul : (n : Nat) -> IntMod n -> IntMod n -> IntMod n;
primitive intModNeg : (n : Nat) -> IntMod n -> IntMod n;


--------------------------------------------------------------------------------
-- Point-update functions

updNatFun : (a:sort 0)
	  -> (Nat -> a) -> Nat -> a -> (Nat -> a);
updNatFun a f i v x = ite a (equalNat i x) v (f x);

updBvFun : (n:Nat) -> (a:sort 0)
	 -> (Vec n Bool -> a) -> Vec n Bool -> a -> (Vec n Bool -> a);
updBvFun n a f i v x = ite a (bvEq n i x) v (f x);

--------------------------------------------------------------------------------
-- Floating-point values
--    Currently commented out because they are not implemented...

primitive Float : sort 0;

-- mkFloat m e = m * 2^^e
primitive mkFloat : Integer -> Integer -> Float;
-- primitive bvToFloat : Vec 32 Bool -> Float;
-- primitive floatToBV : Float -> Vec 32 Bool;

primitive Double : sort 0;

-- mkDouble m e = m * 2^^e
primitive mkDouble : Integer -> Integer -> Float;
-- primitive bvToDouble : Vec 64 Bool -> Double;
-- primitive doubleToBV : Double -> Vec 64 Bool;


-------------------------------------------------------------------------------
-- Dependent sums

data Sigma (a : sort 0) (b : a -> sort 0) : sort 0
  where {
    exists : (pa : a) -> b pa -> Sigma a b;
  }

Sigma__rec
  (a : sort 0) (b : a -> sort 0) (p : Sigma a b -> sort 0)
  (f1 : (pa : a) -> (pb : b pa) -> p (exists a b pa pb)) (u : Sigma a b) : p u
  = Sigma#rec a b p f1 u;

Sigma_proj1 (a : sort 0) (b : a -> sort 0) : Sigma a b -> a
  = Sigma__rec a b (\ (_ : Sigma a b) -> a) (\ (pa : a) (_ : b pa) -> pa);

Sigma_proj2 (a : sort 0) (b : a -> sort 0)
  : (p : Sigma a b) -> b (Sigma_proj1 a b p)
  = Sigma__rec a b
      (\ (p : Sigma a b) -> b (Sigma_proj1 a b p))
      (\ (pa : a) (pb : b pa) -> pb);

uncurrySigma : (a : sort 0) -> (b : a -> sort 0) -> (c : sort 0) ->
               ((pa : a) -> b pa -> c) -> Sigma a b -> c;
uncurrySigma a b c = Sigma__rec a b (\ (_:Sigma a b) -> c);


--------------------------------------------------------------------------------
-- Lists

data List (a : sort 0) : sort 0
  where {
    Nil : List a;
    Cons : a -> List a -> List a;
  }

List__rec :
  (a : sort 0) -> (P : List a -> sort 0) -> P (Nil a) ->
  ((x : a) -> (l : List a) -> P l -> P (Cons a x l)) ->
  (l : List a) -> P l;
List__rec a P f1 f2 l = List#rec a P f1 f2 l;

unfoldList : (a:sort 0) -> List a -> Either #() (a * List a);
unfoldList a l =
  List__rec a (\ (_:List a) -> Either #() (a * List a))
  (Left #() (a * List a) ())
  (\ (x:a) (l:List a) (_:Either #() (a * List a)) ->
     Right #() (a * List a) (x, l))
  l;

foldList : (a:sort 0) -> Either #() (a * List a) -> List a;
foldList a =
  either #() (a * List a) (List a)
         (\ (_ : #()) -> Nil a)
         (\ (tup : (a * List a)) ->
            Cons a tup.(1) tup.(2));

-- A list of types, i.e. `List (sort 0)` if `List` was universe polymorphic
data ListSort : sort 1
  where {
    LS_Nil : ListSort;
    LS_Cons : sort 0 -> ListSort -> ListSort;
  }

ListSort__rec : (P : ListSort -> sort 1) -> P LS_Nil ->
                ((A:sort 0) -> (l:ListSort) -> P l -> P (LS_Cons A l)) ->
                (l:ListSort) -> P l;
ListSort__rec P f1 f2 l = ListSort#rec P f1 f2 l;

-- The sort at the given index in a ListSort or `Eq Bool True False` if
--  the index is out of bounds
listSortGet : ListSort -> Nat -> sort 0;
listSortGet = ListSort__rec (\ (_:ListSort) -> Nat -> sort 0)
  (\ (_:Nat) -> Eq Bool True False)
  (\ (A:sort 0) (_:ListSort) (rec : Nat -> sort 0) ->
     Nat_cases (sort 0) A (\ (n:Nat) (_:sort 0) -> rec n));

-- A ListSort with the first n (or all, if n > length) entries removed
listSortDrop : ListSort -> Nat -> ListSort;
listSortDrop = ListSort__rec (\ (_:ListSort) -> Nat -> ListSort)
  (\ (_:Nat) -> LS_Nil)
  (\ (_:sort 0) (Ds:ListSort) (rec : Nat -> ListSort) ->
     Nat_cases ListSort Ds (\ (n:Nat) (_ : ListSort) -> rec n));


--------------------------------------------------------------------------------
-- Nested Either types

-- The false proposition
FalseProp : Prop;
FalseProp = Eq Bool True False;

-- Ex Falso Quodlibet: if True = False then anything is possible
efq : (a : sort 0) -> FalseProp -> a;
efq a contra =
  coerce
    #() a
    (trans
     (sort 0) #() (ite (sort 0) True #() a) a
     (sym (sort 0) (ite (sort 0) True #() a) #()
           (ite_true (sort 0) #() a))
     (trans
      (sort 0) (ite (sort 0) True #() a) (ite (sort 0) False #() a) a
      (eq_cong Bool True False contra (sort 0)
               (\ (b:Bool) -> ite (sort 0) b #() a))
      (ite_false (sort 0) #() a)
      ))
    ();

-- Ex Falso Quodlibet at sort 1
efq1 : (a : sort 1) -> Eq Bool True False -> a;
efq1 a contra =
  Eq__rec Bit Bit1
          (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b)
          () Bit0 (efq (Eq Bit Bit1 Bit0) contra);

-- An if-then-else that tests if a ListSort is nil
ifLSNil : (a : sort 1) -> ListSort -> a -> a -> a;
ifLSNil a l x y =
  ListSort__rec (\ (_:ListSort) -> a) x (\ (_:sort 0) (_:ListSort) (_:a) -> y) l;

-- A right-nested sequence of Eithers, defined as
--   Eithers [] = FalseProp
--   Eithers [tp] = tp
--   Eithers (tp:tps) = Either tp (Eithers tps)
Eithers : ListSort -> sort 0;
Eithers = ListSort__rec
            (\ (_:ListSort) -> sort 0)
            FalseProp
            (\ (tp:sort 0) (tail:ListSort) (rec:sort 0) ->
               ifLSNil (sort 0) tail tp (Either tp rec));

-- Eliminate the outermost either of an Eithers of cons shape
eithers1 : (tp:sort 0) -> (tps:ListSort) -> (a:sort 0) ->
           Eithers (LS_Cons tp tps) -> (tp -> a) -> (Eithers tps -> a) -> a;
eithers1 tp tps_in a =
  ListSort__rec
    (\ (tps:ListSort) ->
       Eithers (LS_Cons tp tps) -> (tp -> a) -> (Eithers tps -> a) -> a)
    (\ (eiths:tp) (f:tp -> a) (_:FalseProp -> a) -> f eiths)
    (\ (tp2:sort 0) (tail:ListSort)
       (_:Eithers (LS_Cons tp tail) -> (tp -> a) -> (Eithers tail -> a) -> a)
       (eiths:Either tp (Eithers (LS_Cons tp2 tail)))
       (f1:tp -> a) (f2:Eithers (LS_Cons tp2 tail) -> a) ->
       either tp (Eithers (LS_Cons tp2 tail)) a f1 f2 eiths)
    tps_in;

-- The type of a list of functions to a particular output type a
data FunsTo (a:sort 0) : sort 1 where {
  FunsTo_Nil : FunsTo a;
  FunsTo_Cons : (tp:sort 0) -> (tp -> a) -> FunsTo a -> FunsTo a;
}

-- The recursor for FunsTo
FunsTo__rec : (a:sort 0) -> (P : FunsTo a -> sort 1) -> P (FunsTo_Nil a) ->
              ((tp:sort 0) -> (f:tp -> a) -> (es:FunsTo a) ->
               P es -> P (FunsTo_Cons a tp f es)) ->
              (es:FunsTo a) -> P es;
FunsTo__rec a P f1 f2 es = FunsTo#rec a P f1 f2 es;

-- Extract the input types of the functions in a FunsTo list
FunsToIns : (a:sort 0) -> FunsTo a -> ListSort;
FunsToIns a =
  FunsTo__rec
    a (\ (_:FunsTo a) -> ListSort) LS_Nil
    (\ (tp:sort 0) (_:tp -> a) (_:FunsTo a) (rec:ListSort) -> LS_Cons tp rec);

-- An eliminator for the Eithers type
eithers : (a:sort 0) -> (elims:FunsTo a) -> Eithers (FunsToIns a elims) -> a;
eithers a =
  FunsTo__rec
    a
    (\ (elims:FunsTo a) -> Eithers (FunsToIns a elims) -> a)
    (\ (contra:FalseProp) -> efq a contra)
    (\ (tp:sort 0) (f:tp -> a) (elims:FunsTo a)
       (rec:Eithers (FunsToIns a elims) -> a)
       (eiths:Eithers (LS_Cons tp (FunsToIns a elims))) ->
       eithers1 tp (FunsToIns a elims) a eiths f rec);


--------------------------------------------------------------------------------
-- Lists of 64-bit words (for testing Heapster)

data W64List : sort 0 where {
  W64Nil : W64List;
  W64Cons : Vec 64 Bool -> W64List -> W64List;
}

unfoldedW64List : sort 0;
unfoldedW64List =
  Either #()
  (Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #()) * W64List * #());

unfoldW64List : W64List -> unfoldedW64List;
unfoldW64List l =
  W64List#rec (\ (_:W64List) -> unfoldedW64List)
  (Left #() (Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #()) * W64List * #()) ())
  (\ (bv:Vec 64 Bool) (l':W64List) (_:unfoldedW64List) ->
     Right #() (Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #()) * W64List * #())
               (exists (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #()) bv (),
                l', ()))
  l;

foldW64List : unfoldedW64List -> W64List;
foldW64List =
  either #() (Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #()) * W64List * #())
         W64List
         (\ (_:#()) -> W64Nil)
         (\ (bv_l:(Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #())
                   * W64List * #())) ->
            W64Cons (Sigma_proj1 (Vec 64 Bool)
                                 (\ (_:Vec 64 Bool) -> #()) bv_l.(1))
                    bv_l.(2).(1));


--------------------------------------------------------------------------------
-- Vector operations with built-in casts of their resulting lengths

-- Specialized version of unsafeAssert for bitvector inequalities
axiom unsafeAssertBVULt : (n : Nat) -> (x : Vec n Bool) -> (y : Vec n Bool) ->
                          Eq Bool (bvult n x y) True;
axiom unsafeAssertBVULe : (n : Nat) -> (x : Vec n Bool) -> (y : Vec n Bool) ->
                          Eq Bool (bvule n x y) True;

-- Decide equality on two bitvectors, returning a proof if they are equal
primitive bvEqWithProof : (n : Nat) -> (v1 v2 : Vec n Bool) ->
                          Maybe (Eq (Vec n Bool) v1 v2);

-- Compare two bitvectors with bvult, returning a proof if bvult succeeds
bvultWithProof : (n : Nat) -> (v1 v2 : Vec n Bool) ->
                 Maybe (Eq Bool (bvult n v1 v2) True);
bvultWithProof n v1 v2 =
  iteDep (\ (b:Bool) -> Maybe (Eq Bool b True)) (bvult n v1 v2)
         (Just (Eq Bool True True) (Refl Bool True))
         (Nothing (Eq Bool False True));

-- Compare two bitvectors with bvule, returning a proof if bvule succeeds
bvuleWithProof : (n : Nat) -> (v1 v2 : Vec n Bool) ->
                 Maybe (Eq Bool (bvule n v1 v2) True);
bvuleWithProof n v1 v2 =
  iteDep (\ (b:Bool) -> Maybe (Eq Bool b True)) (bvule n v1 v2)
         (Just (Eq Bool True True) (Refl Bool True))
         (Nothing (Eq Bool False True));

-- Convert a proof of bitvector equality to one of Nat equality
primitive bvEqToEqNat : (n : Nat) -> (v1 v2 : Vec n Bool) ->
                        Eq (Vec n Bool) v1 v2 ->
                        eqNat (bvToNat n v1) (bvToNat n v2);

-- Convert a proof of bitvector less-than to one of Nat less-than
primitive bvultToIsLtNat : (n : Nat) -> (v1 v2 : Vec n Bool) ->
                           Eq Bool (bvult n v1 v2) True ->
                           IsLtNat (bvToNat n v1) (bvToNat n v2);

-- Generate a vector using a proof that the index is in the range of the vector
-- FIXME: Like the below, gen should maybe use this...?
primitive genWithProof : (n : Nat) -> (a : sort 0) ->
                         ((i : Nat) -> IsLtNat i n -> a) -> Vec n a;

-- | Index a vector using a proof that the index is in the range of the vector
-- FIXME: atWithDefault should maybe use this...?
primitive atWithProof : (n : Nat) -> (a : sort 0) -> Vec n a ->
                        (i : Nat) -> IsLtNat i n -> a;

-- Set the value at index i in a vector using a proof that i is in range
primitive updWithProof : (n : Nat) -> (a : sort 0) -> Vec n a ->
                         (i : Nat) -> a -> IsLtNat i n -> Vec n a;

-- Take a slice of a vector using a proof that the slice is in range
primitive sliceWithProof : (a : sort 0) -> (n off len : Nat) ->
                           IsLeNat (addNat off len) n -> Vec n a -> Vec len a;

-- Update a slice of a vector using a proof that the slice is in range
primitive updSliceWithProof : (a : sort 0) -> (n off len : Nat) ->
                              IsLeNat (addNat off len) n ->
                              Vec n a -> Vec len a -> Vec n a;


--------------------------------------------------------------------------------
-- Vectors indexed by bitvectors

-- Helper definition to write the proposition that x <u y
is_bvult : (n:Nat) -> (x y:Vec n Bool) -> Prop;
is_bvult n x y = Eq Bool (bvult n x y) True;

-- Helper definition to write the proposition that x <=u y
is_bvule : (n:Nat) -> (x y:Vec n Bool) -> Prop;
is_bvule n x y = Eq Bool (bvule n x y) True;

-- Axiom: x <u 0 never hold
axiom not_bvult_zero : (n:Nat) -> (x:Vec n Bool) ->
                       Eq Bool (bvult n x (bvNat n 0)) False;

-- Axiom: x <=u y <u z implies x <u z
axiom trans_bvult_bvule : (n:Nat) -> (x y z:Vec n Bool) ->
                          is_bvult n x y -> is_bvule n y z -> is_bvult n x z;

axiom bvult_sub_add_bvult : (n:Nat) -> (x y z:Vec n Bool) ->
                            is_bvule n y z -> is_bvult n x (bvSub n z y) ->
                            is_bvult n (bvAdd n y x) z;

-- Axiom: x <u y+z and y <=u x implies (x-y) <u z
axiom bvult_sum_bvult_sub : (n:Nat) -> (x y z:Vec n Bool) ->
                            is_bvult n x (bvAdd n y z) ->
                            Eq Bool (bvult n x y) False ->
                            is_bvult n (bvSub n x y) z;

-- When comparing a nat and a bitvector, IsLtNat and is_bvult are equivalent
axiom IsLtNat_to_bvult : (n : Nat) -> (x : Vec n Bool) -> (i : Nat) ->
                         IsLtNat i (bvToNat n x) -> is_bvult n (bvNat n i) x;
axiom bvult_to_IsLtNat : (n : Nat) -> (x : Vec n Bool) -> (i : Nat) ->
                         is_bvult n (bvNat n i) x -> IsLtNat i (bvToNat n x);

-- The type of a bitvector-indexed array of length len : Vec n Bool
BVVec : (n:Nat) -> Vec n Bool -> sort 0 -> sort 0;
BVVec n len = Vec (bvToNat n len);

-- Generate a BVVec of length len whose elements are given by a function
genBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
           ((i:Vec n Bool) -> is_bvult n i len -> a) ->
           BVVec n len a;
genBVVec n len a f =
  genWithProof (bvToNat n len) a
    (\ (i:Nat) (pf:IsLtNat i (bvToNat n len)) ->
       f (bvNat n i) (IsLtNat_to_bvult n len i pf));

-- Generate a BVVec from the elements of an existing vector, using a default
-- value when we run out of the existing vector
genBVVecFromVec : (m : Nat) -> (a : sort 0) -> Vec m a -> a ->
                  (n : Nat) -> (len : Vec n Bool) -> BVVec n len a;
genBVVecFromVec m a v def n len =
  genBVVec n len a (\ (i:Vec n Bool) (_:is_bvult n i len) ->
                      atWithDefault m a def v (bvToNat n i));

-- Generate a vector from the elements of an existing BVVec, using a default
-- value when we run out of the existing BVVec - the inverse of genBVVecFromVec
genFromBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
               BVVec n len a -> a -> (m : Nat) -> Vec m a;
genFromBVVec n len a v def m =
  gen m a (\ (i:Nat) -> atWithDefault (bvToNat n len) a def v i);

-- Generate an empty BVVec
emptyBVVec : (n : Nat) -> (a : sort 0) -> BVVec n (bvNat n 0) a;
emptyBVVec n a =
  genBVVec n (bvNat n 0) a
           (\ (i:Vec n Bool) (pf:is_bvult n i (bvNat n 0)) ->
              efq a (trans Bool True (bvult n i (bvNat n 0)) False
                            (sym Bool (bvult n i (bvNat n 0)) True pf)
                            (not_bvult_zero n i)));

-- Generate a BVVec by repeating a single element
repeatBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) -> a ->
              BVVec n len a;
repeatBVVec n len a x =
  genBVVec n len a (\ (i:Vec n Bool) (_:is_bvult n i len) -> x);

-- Generate a BVVec with 1 element
singletonBVVec : (n : Nat) -> (a : sort 0) -> a -> BVVec n (bvNat n 1) a;
singletonBVVec n a x = repeatBVVec n (bvNat n 1) a x;

-- Read the ixth element of a BVVec, assuming that ix < len
atBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
          BVVec n len a -> (ix : Vec n Bool) ->
          is_bvult n ix len -> a;
atBVVec n len a x ix pf =
  atWithProof (bvToNat n len) a x (bvToNat n ix)
    (bvult_to_IsLtNat n len (bvToNat n ix)
      (trans Bool (bvult n (bvNat n (bvToNat n ix)) len) (bvult n ix len) True
        (eq_cong (Vec n Bool) (bvNat n (bvToNat n ix)) ix
          (bvNat_bvToNat_id n ix) Bool (\ (y:Vec n Bool) -> bvult n y len))
        pf));

-- Indexing a generated BVVec just returns the generating function
axiom at_gen_BVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
                     (f : (i:Vec n Bool) -> is_bvult n i len -> a) ->
                     (ix : Vec n Bool) -> (pf : is_bvult n ix len) ->
                     Eq a (atBVVec n len a (genBVVec n len a f) ix pf) (f ix pf);

-- Generating a BVVec by indexing another just returns the other BVVec
axiom gen_at_BVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
                     (x : BVVec n len a) ->
                     Eq (BVVec n len a) (genBVVec n len a (atBVVec n len a x)) x;

-- Update the value at a specific index in a BVVec if it is in range, otherwise
-- do nothing
updBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
           BVVec n len a -> (ix : Vec n Bool) ->
           a -> BVVec n len a;
updBVVec n len a v ix elem =
  genBVVec n len a (\ (i:Vec n Bool) (pf:is_bvult n i len) ->
                      ite a (bvEq n i ix) elem (atBVVec n len a v i pf));

-- Adjust the value at a specific index in a BVVec by applying a function
adjustBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
              BVVec n len a -> (a -> a) -> Vec n Bool ->
              BVVec n len a;
adjustBVVec n len a v f ix =
  genBVVec n len a (\ (i:Vec n Bool) (pf:is_bvult n i len) ->
                      ite a (bvEq n i ix)
                          (f (atBVVec n len a v i pf))
                          (atBVVec n len a v i pf));

-- Take the first i elements of a BVVec, assuming i <= len
takeBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
            (i : Vec n Bool) -> is_bvule n i len ->
            BVVec n len a -> BVVec n i a;
takeBVVec n len a i pf v =
  genBVVec n i a
    (\ (j:Vec n Bool) (pf2:is_bvult n j i) ->
       atBVVec n len a v j (trans_bvult_bvule n j i len pf2 pf));

-- Drop the first i elements of a BVVec, assuming i <= len
dropBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
            (i : Vec n Bool) -> is_bvule n i len ->
            BVVec n len a -> BVVec n (bvSub n len i) a;
dropBVVec n len a i pf v =
  genBVVec n (bvSub n len i) a
    (\ (j:Vec n Bool) (pf2:is_bvult n j (bvSub n len i)) ->
       atBVVec n len a v (bvAdd n i j) (bvult_sub_add_bvult n j i len pf pf2));

-- Combined drop and take
sliceBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
             (start' len' : Vec n Bool) -> is_bvule n start' len ->
             is_bvule n len' (bvSub n len start') ->
             BVVec n len a -> BVVec n len' a;
sliceBVVec n len a start' len' pf1 pf2 v =
  takeBVVec n (bvSub n len start') a len' pf2
    (dropBVVec n len a start' pf1 v);

-- Update a slice of a BVVec
updSliceBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
                BVVec n len a -> (start' len' : Vec n Bool) ->
                BVVec n len' a -> BVVec n len a;
updSliceBVVec n len a v start' len' v_sub =
  genBVVec n len a
    (\ (i:Vec n Bool) (pf:is_bvult n i len) ->
       ite a (bvule n start' i)
           (maybe (is_bvult n (bvSub n i start') len') a
              (atBVVec n len a v i pf)
              (\ (pf_sub:is_bvult n (bvSub n i start') len') ->
                 atBVVec n len' a v_sub (bvSub n i start') pf_sub)
              (bvultWithProof n (bvSub n i start') len'))
           (atBVVec n len a v i pf));

-- Append two BVVecs
appendBVVec : (n : Nat) -> (len1 len2 : Vec n Bool) -> (a : sort 0) ->
              BVVec n len1 a -> BVVec n len2 a -> BVVec n (bvAdd n len1 len2) a;
appendBVVec n len1 len2 a v1 v2 =
  genBVVec n (bvAdd n len1 len2) a
    (\ (i:Vec n Bool) (pf12:is_bvult n i (bvAdd n len1 len2)) ->
       iteDep
         (\ (b:Bool) -> Eq Bool (bvult n i len1) b -> a)
         (bvult n i len1)
         (\ (pf1:is_bvult n i len1) -> atBVVec n len1 a v1 i pf1)
         (\ (not_pf1:Eq Bool (bvult n i len1) False) ->
            atBVVec n len2 a v2 (bvSub n i len1)
                    (bvult_sum_bvult_sub n i len1 len2 pf12 not_pf1))
         (Refl Bool (bvult n i len1)));


-- | The complete induction principle on bitvectors
BV_complete_induction :
  (w: Nat) ->
  (p: Vec w Bool -> Prop) ->
  ((x : Vec w Bool) -> ((y: Vec w Bool) -> is_bvult w y x -> p y) -> p x) ->
  (x : Vec w Bool) -> p x;
BV_complete_induction w p f x0 =
  Nat_complete_induction
    (\ (n:Nat) -> (x:Vec w Bool) -> IsLeNat (bvToNat w x) n -> p x)
    (\ (n:Nat) ->
     \ (Hind : (m : Nat) -> (Hm : IsLtNat m n) -> (y : Vec w Bool) ->
               (Hy : IsLeNat (bvToNat w y) m) -> p y) ->
     \ (x : Vec w Bool) ->
     \ (Hx : IsLeNat (bvToNat w x) n) ->
       f x (\ (y:Vec w Bool) -> \ (Hult : is_bvult w y x) ->
              Hind (bvToNat w y)
	        (IsLeNat_transitive (Succ (bvToNat w y)) (bvToNat w x) n (bvultToIsLtNat w y x Hult) Hx)
	        y (IsLeNat_base (bvToNat w y))
	   )
    )
    (bvToNat w x0) x0 (IsLeNat_base (bvToNat w x0));


--------------------------------------------------------------------------------
-- Iso-recursive types

data IRTDesc (As:ListSort) : sort 0 where {
  IRT_varD   : Nat -> IRTDesc As; -- an IRTDesc var
  IRT_mu     : IRTDesc As -> IRTDesc As; -- binds a varD
  IRT_Either : IRTDesc As -> IRTDesc As -> IRTDesc As;
  IRT_prod   : IRTDesc As -> IRTDesc As -> IRTDesc As;
  IRT_sigT   : (i:Nat) -> (listSortGet As i -> IRTDesc As) -> IRTDesc As;
  IRT_BVVec  : (n:Nat) -> Vec n Bool -> (D:IRTDesc As) -> IRTDesc As;
  IRT_unit   : IRTDesc As;
  IRT_empty  : IRTDesc As;
  IRT_varT   : (i:Nat) -> IRTDesc As; -- a sort var, i.e. an index into `As`
}

IRTDesc__rec : (As:ListSort) -> (P : IRTDesc As -> sort 1) ->
               ((i:Nat) -> P (IRT_varD As i)) ->
               ((D:IRTDesc As) -> P D -> P (IRT_mu As D)) ->
               ((Dl:IRTDesc As) -> P Dl -> (Dr:IRTDesc As) -> P Dr ->
                  P (IRT_Either As Dl Dr)) ->
               ((Dl:IRTDesc As) -> P Dl -> (Dr:IRTDesc As) -> P Dr ->
                  P (IRT_prod As Dl Dr)) ->
               ((i:Nat) -> (Df : listSortGet As i -> IRTDesc As) ->
                  ((a:listSortGet As i) -> P (Df a)) -> P (IRT_sigT As i Df)) ->
               ((n:Nat) -> (len:Vec n Bool) -> (D:IRTDesc As) -> P D ->
                  P (IRT_BVVec As n len D)) ->
               P (IRT_unit As) -> P (IRT_empty As) ->
               ((i:Nat) -> P (IRT_varT As i)) ->
               (D:IRTDesc As) -> P D;
IRTDesc__rec As P f1 f2 f3 f4 f5 f6 f7 f8 f9 D = IRTDesc#rec As P f1 f2 f3 f4 f5 f6 f7 f8 f9 D;

-- A list of substitutions for a context of iso-recursive type descriptions
data IRTSubsts (As:ListSort) : sort 0 where {
  IRTs_Nil : IRTSubsts As;
  IRTs_Cons : IRTDesc As -> IRTSubsts As -> IRTSubsts As;
}

IRTSubsts__rec : (As:ListSort) -> (P : IRTSubsts As -> sort 1) -> P (IRTs_Nil As) ->
                 ((D:IRTDesc As) -> (Ds:IRTSubsts As) -> P Ds -> P (IRTs_Cons As D Ds)) ->
                 (Ds:IRTSubsts As) -> P Ds;
IRTSubsts__rec As P f1 f2 Ds = IRTSubsts#rec As P f1 f2 Ds;

-- The IRTDesc at the given index in an IRTSubsts or IRT_empty if the
-- index is out of bounds
atIRTs : (As:ListSort) -> IRTSubsts As -> Nat -> IRTDesc As;
atIRTs As = IRTSubsts__rec As (\ (_:IRTSubsts As) -> Nat -> IRTDesc As)
  (\ (_:Nat) -> IRT_empty As)
  (\ (D:IRTDesc As) (_:IRTSubsts As) (rec : Nat -> IRTDesc As) ->
     Nat_cases (IRTDesc As) D (\ (n:Nat) (_:IRTDesc As) -> rec n));

-- A IRTSubsts with the first n (or all, if n > length) entries removed
dropIRTs : (As:ListSort) -> IRTSubsts As -> Nat -> IRTSubsts As;
dropIRTs As = IRTSubsts__rec As (\ (_:IRTSubsts As) -> Nat -> IRTSubsts As)
  (\ (_:Nat) -> IRTs_Nil As)
  (\ (_:IRTDesc As) (Ds:IRTSubsts As) (rec : Nat -> IRTSubsts As) ->
     Nat_cases (IRTSubsts As) Ds (\ (n:Nat) (_ : IRTSubsts As) -> rec n));

-- The type corresponding to an iso-recursive type description
data IRT (As:ListSort) : IRTSubsts As -> IRTDesc As -> sort 0 where {
  IRT_elemD    : (Ds:IRTSubsts As) -> (i:Nat) ->
                 IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i) ->
                 IRT As Ds (IRT_varD As i);
  IRT_fold     : (Ds:IRTSubsts As) -> (D:IRTDesc As) ->
                 IRT As (IRTs_Cons As (IRT_mu As D) Ds) D -> IRT As Ds (IRT_mu As D);
  IRT_Left     : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
                 IRT As Ds Dl -> IRT As Ds (IRT_Either As Dl Dr);
  IRT_Right    : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
                 IRT As Ds Dr -> IRT As Ds (IRT_Either As Dl Dr);
  IRT_pair     : (Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
                 IRT As Ds Dl -> IRT As Ds Dr -> IRT As Ds (IRT_prod As Dl Dr);
  IRT_existT   : (Ds:IRTSubsts As) -> (i:Nat) -> (Df : listSortGet As i -> IRTDesc As) ->
                 (a:listSortGet As i) -> IRT As Ds (Df a) -> IRT As Ds (IRT_sigT As i Df);
  IRT_genBVVec : (Ds:IRTSubsts As) -> (n:Nat) -> (len:Vec n Bool) -> (D:IRTDesc As) ->
                 ((i:Vec n Bool) -> is_bvult n i len -> IRT As Ds D) -> IRT As Ds (IRT_BVVec As n len D);
  IRT_tt       : (Ds:IRTSubsts As) -> IRT As Ds (IRT_unit As);
  IRT_elemT    : (Ds:IRTSubsts As) -> (i:Nat) ->
                 listSortGet As i -> IRT As Ds (IRT_varT As i);
}

IRT__rec : (As:ListSort) -> (P : (Ds:IRTSubsts As) -> (D:IRTDesc As) -> IRT As Ds D -> sort 1) ->
           ((Ds:IRTSubsts As) -> (i:Nat) ->
              (x:IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i)) ->
              P (dropIRTs As Ds (Succ i)) (atIRTs As Ds i) x ->
              P Ds (IRT_varD As i) (IRT_elemD As Ds i x)) ->
           ((Ds:IRTSubsts As) -> (D:IRTDesc As) ->
              (x:IRT As (IRTs_Cons As (IRT_mu As D) Ds) D) ->
              P (IRTs_Cons As (IRT_mu As D) Ds) D x ->
              P Ds (IRT_mu As D) (IRT_fold As Ds D x)) ->
           ((Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) -> (xl:IRT As Ds Dl) ->
              P Ds Dl xl -> P Ds (IRT_Either As Dl Dr) (IRT_Left As Ds Dl Dr xl)) ->
           ((Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) -> (xr:IRT As Ds Dr) ->
              P Ds Dr xr -> P Ds (IRT_Either As Dl Dr) (IRT_Right As Ds Dl Dr xr)) ->
           ((Ds:IRTSubsts As) -> (Dl:IRTDesc As) -> (Dr:IRTDesc As) ->
              (xl:IRT As Ds Dl) -> P Ds Dl xl ->
              (xr:IRT As Ds Dr) -> P Ds Dr xr ->
              P Ds (IRT_prod As Dl Dr) (IRT_pair As Ds Dl Dr xl xr)) ->
           ((Ds:IRTSubsts As) -> (i:Nat) -> (Df : listSortGet As i -> IRTDesc As) ->
              (a:listSortGet As i) -> (xf:IRT As Ds (Df a)) -> P Ds (Df a) xf ->
              P Ds (IRT_sigT As i Df) (IRT_existT As Ds i Df a xf)) ->
           ((Ds:IRTSubsts As) -> (n:Nat) -> (len:Vec n Bool) -> (D:IRTDesc As) ->
              (xg : (i:Vec n Bool) -> is_bvult n i len -> IRT As Ds D) ->
              ((i:Vec n Bool) -> (pf:is_bvult n i len) -> P Ds D (xg i pf)) ->
              P Ds (IRT_BVVec As n len D) (IRT_genBVVec As Ds n len D xg)) ->
           ((Ds:IRTSubsts As) -> P Ds (IRT_unit As) (IRT_tt As Ds)) ->
           ((Ds:IRTSubsts As) -> (i:Nat) -> (a:listSortGet As i) ->
              P Ds (IRT_varT As i) (IRT_elemT As Ds i a)) ->
           (Ds:IRTSubsts As) -> (D:IRTDesc As) -> (x:IRT As Ds D) -> P Ds D x;
IRT__rec As P f1 f2 f3 f4 f5 f6 f7 f8 f9 Ds D x = IRT#rec As P f1 f2 f3 f4 f5 f6 f7 f8 f9 Ds D x;

-- The type of a once-unfolded iso-recursive type
UnfoldedIRT : (As:ListSort) -> IRTSubsts As -> IRTDesc As -> sort 0;
UnfoldedIRT As Ds D = IRTDesc__rec As (\ (_:IRTDesc As) -> IRTSubsts As -> sort 0)
  (\ (i:Nat) (Ds:IRTSubsts As) ->
      IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i))
  (\ (D:IRTDesc As) (rec : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
      rec (IRTs_Cons As (IRT_mu As D) Ds))
  (\ (_:IRTDesc As) (recl : IRTSubsts As -> sort 0)
     (_:IRTDesc As) (recr : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
      Either (recl Ds) (recr Ds))
  (\ (_:IRTDesc As) (recl : IRTSubsts As -> sort 0)
     (_:IRTDesc As) (recr : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
      recl Ds * recr Ds)
  (\ (i:Nat) (_ : listSortGet As i -> IRTDesc As)
     (recf : listSortGet As i -> IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
      Sigma (listSortGet As i) (\ (a:listSortGet As i) -> recf a Ds))
  (\ (n:Nat) (len:Vec n Bool) (_:IRTDesc As)
     (rec : IRTSubsts As -> sort 0) (Ds:IRTSubsts As) ->
      BVVec n len (rec Ds))
  (\ (_:IRTSubsts As) -> #())
  (\ (_:IRTSubsts As) -> Eq Bool True False)
  (\ (i:Nat) (_:IRTSubsts As) -> listSortGet As i) D Ds;

-- `fold` and `unfold` for IRTs

unfoldIRT : (As:ListSort) -> (Ds:IRTSubsts As) -> (D:IRTDesc As) ->
            IRT As Ds D -> UnfoldedIRT As Ds D;
unfoldIRT As = IRT__rec As (\ (Ds:IRTSubsts As) (D:IRTDesc As) (_:IRT As Ds D) -> UnfoldedIRT As Ds D)
  (\ (Ds:IRTSubsts As) (i:Nat) (x:IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i))
     (_:UnfoldedIRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i)) -> x)
  (\ (Ds:IRTSubsts As) (D:IRTDesc As) (_:IRT As (IRTs_Cons As (IRT_mu As D) Ds) D)
     (rec: UnfoldedIRT As (IRTs_Cons As (IRT_mu As D) Ds) D) -> rec)
  (\ (Ds:IRTSubsts As) (Dl:IRTDesc As) (Dr:IRTDesc As)
     (_:IRT As Ds Dl) (recl:UnfoldedIRT As Ds Dl) ->
      Left (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) recl)
  (\ (Ds:IRTSubsts As) (Dl:IRTDesc As) (Dr:IRTDesc As)
     (_:IRT As Ds Dr) (recr:UnfoldedIRT As Ds Dr) ->
      Right (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) recr)
  (\ (Ds:IRTSubsts As) (Dl:IRTDesc As) (Dr:IRTDesc As)
     (_:IRT As Ds Dl) (recl:UnfoldedIRT As Ds Dl)
     (_:IRT As Ds Dr) (recr:UnfoldedIRT As Ds Dr) ->
      (recl, recr))
  (\ (Ds:IRTSubsts As) (i:Nat) (Df : listSortGet As i -> IRTDesc As) (a:listSortGet As i)
     (_:IRT As Ds (Df a)) (recf:UnfoldedIRT As Ds (Df a)) ->
      exists (listSortGet As i) (\ (a:listSortGet As i) -> UnfoldedIRT As Ds (Df a)) a recf)
  (\ (Ds:IRTSubsts As) (n:Nat) (len:Vec n Bool) (D:IRTDesc As)
     (_ : (i:Vec n Bool) -> is_bvult n i len -> IRT As Ds D)
     (recg : (i:Vec n Bool) -> is_bvult n i len -> UnfoldedIRT As Ds D) ->
      genBVVec n len (UnfoldedIRT As Ds D) recg)
  (\ (Ds:IRTSubsts As) -> ())
  (\ (Ds:IRTSubsts As) (i:Nat) (a:listSortGet As i) -> a);

foldIRT : (As:ListSort) -> (Ds:IRTSubsts As) -> (D:IRTDesc As) ->
          UnfoldedIRT As Ds D -> IRT As Ds D;
foldIRT As Ds D = IRTDesc__rec As (\ (D:IRTDesc As) -> (Ds:IRTSubsts As) -> UnfoldedIRT As Ds D -> IRT As Ds D)
  (\ (i:Nat) (Ds:IRTSubsts As) (x:IRT As (dropIRTs As Ds (Succ i)) (atIRTs As Ds i)) ->
      IRT_elemD As Ds i x)
  (\ (D:IRTDesc As) (rec : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds D -> IRT As Ds D)
     (Ds:IRTSubsts As) (x:UnfoldedIRT As (IRTs_Cons As (IRT_mu As D) Ds) D) ->
      IRT_fold As Ds D (rec (IRTs_Cons As (IRT_mu As D) Ds) x))
  (\ (Dl:IRTDesc As) (recl : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds Dl -> IRT As Ds Dl)
     (Dr:IRTDesc As) (recr : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds Dr -> IRT As Ds Dr)
     (Ds:IRTSubsts As) (x:Either (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr)) ->
      either (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) (IRT As Ds (IRT_Either As Dl Dr))
             (\ (xl:UnfoldedIRT As Ds Dl) -> IRT_Left  As Ds Dl Dr (recl Ds xl))
             (\ (xr:UnfoldedIRT As Ds Dr) -> IRT_Right As Ds Dl Dr (recr Ds xr)) x)
  (\ (Dl:IRTDesc As) (recl : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds Dl -> IRT As Ds Dl)
     (Dr:IRTDesc As) (recr : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds Dr -> IRT As Ds Dr)
     (Ds:IRTSubsts As) (x:UnfoldedIRT As Ds Dl * UnfoldedIRT As Ds Dr) ->
      uncurry (UnfoldedIRT As Ds Dl) (UnfoldedIRT As Ds Dr) (IRT As Ds (IRT_prod As Dl Dr))
              (\ (xl:UnfoldedIRT As Ds Dl) (xr:UnfoldedIRT As Ds Dr) ->
                  IRT_pair As Ds Dl Dr (recl Ds xl) (recr Ds xr)) x)
  (\ (i:Nat) (Df : listSortGet As i -> IRTDesc As)
     (recf : (a:listSortGet As i) -> (Ds:IRTSubsts As) -> UnfoldedIRT As Ds (Df a) -> IRT As Ds (Df a))
     (Ds:IRTSubsts As) (x:Sigma (listSortGet As i) (\ (a:listSortGet As i) -> UnfoldedIRT As Ds (Df a))) ->
      uncurrySigma (listSortGet As i) (\ (a:listSortGet As i) -> UnfoldedIRT As Ds (Df a)) (IRT As Ds (IRT_sigT As i Df))
                   (\ (a:listSortGet As i) (xf:UnfoldedIRT As Ds (Df a)) ->
                       IRT_existT As Ds i Df a (recf a Ds xf)) x)
  (\ (n:Nat) (len:Vec n Bool) (D:IRTDesc As) (recg : (Ds:IRTSubsts As) -> UnfoldedIRT As Ds D -> IRT As Ds D)
     (Ds:IRTSubsts As) (x : BVVec n len (UnfoldedIRT As Ds D)) ->
      IRT_genBVVec As Ds n len D (\ (i:Vec n Bool) (pf:is_bvult n i len) ->
                                     recg Ds (atBVVec n len (UnfoldedIRT As Ds D) x i pf)))
  (\ (Ds:IRTSubsts As) (x:#()) -> IRT_tt As Ds)
  (\ (Ds:IRTSubsts As) (x:Eq Bool True False) -> efq (IRT As Ds (IRT_empty As)) x)
  (\ (i:Nat) (Ds:IRTSubsts As) (x:listSortGet As i) -> IRT_elemT As Ds i x) D Ds;


--------------------------------------------------------------------------------
-- Computation monad

primitive CompM : sort 0 -> sort 0;

primitive returnM : (a:sort 0) -> a -> CompM a;
primitive bindM : (a b:sort 0) -> CompM a -> (a -> CompM b) -> CompM b;

-- Raise an error in the computation monad
primitive errorM : (a:sort 0) -> String -> CompM a;

-- Apply a pure function to a computation
fmapM : (a b: sort 0) -> (a -> b) -> CompM a -> CompM b;
fmapM a b f m = bindM a b m (\ (x:a) -> returnM b (f x));

-- Apply a computation of a function to a computation of an argument
applyM : (a b: sort 0) -> CompM (a -> b) -> CompM a -> CompM b;
applyM a b f m =
  bindM (a -> b) b f (\ (f:a->b) -> bindM a b m (\ (x:a) -> returnM b (f x)));

-- Apply a binary pure function to a computation
fmapM2 : (a b c: sort 0) -> (a -> b -> c) -> CompM a -> CompM b -> CompM c;
fmapM2 a b c f m1 m2 = applyM b c (fmapM a (b -> c) f m1) m2;

-- Apply a trinary pure function to a computation
fmapM3 : (a b c d: sort 0) -> (a -> b -> c -> d) ->
         CompM a -> CompM b -> CompM c -> CompM d;
fmapM3 a b c d f m1 m2 m3 = applyM c d (fmapM2 a b (c -> d) f m1 m2) m3;

-- Bind two values and pass them to a binary function
bindM2 : (a b c: sort 0) -> CompM a -> CompM b -> (a -> b -> CompM c) -> CompM c;
bindM2 a b c m1 m2 f = bindM a c m1 (\ (x:a) -> bindM b c m2 (f x));

-- Bind three values and pass them to a trinary function
bindM3 : (a b c d: sort 0) -> CompM a -> CompM b -> CompM c ->
         (a -> b -> c -> CompM d) -> CompM d;
bindM3 a b c d m1 m2 m3 f = bindM a d m1 (\ (x:a) -> bindM2 b c d m2 m3 (f x));

-- A version of bind that takes the function first
bindApplyM : (a b : sort 0) -> (a -> CompM b) -> CompM a -> CompM b;
bindApplyM a b f m = bindM a b m f;

-- A version of bindM2 that takes the function first
bindApplyM2 : (a b c: sort 0) -> (a -> b -> CompM c) -> CompM a -> CompM b -> CompM c;
bindApplyM2 a b c f m1 m2 = bindM a c m1 (\ (x:a) -> bindM b c m2 (f x));

-- A version of bindM3 that takes the function first
bindApplyM3 : (a b c d: sort 0) -> (a -> b -> c -> CompM d) ->
              CompM a -> CompM b -> CompM c -> CompM d;
bindApplyM3 a b c d f m1 m2 m3 = bindM3 a b c d m1 m2 m3 f;

-- Compose two monadic functions
composeM : (a b c: sort 0) -> (a -> CompM b) -> (b -> CompM c) -> a -> CompM c;
composeM a b c f g x = bindM b c (f x) g;

-- Tuple a type onto the input and output types of a monadic function
tupleCompMFunBoth : (a b c: sort 0) -> (a -> CompM b) -> (c * a -> CompM (c * b));
tupleCompMFunBoth a b c f =
  \ (x:c * a) ->
    bindM b (c * b) (f x.(2)) (\ (y:b) -> returnM (c*b) (x.(1), y));

-- Tuple a valu onto the output of a monadic function
tupleCompMFunOut : (a b c: sort 0) -> c -> (a -> CompM b) -> (a -> CompM (c * b));
tupleCompMFunOut a b c x f =
  \ (y:a) -> bindM b (c*b) (f y) (\ (z:b) -> returnM (c*b) (x,z));

-- Map a monadic function across a vector
mapM : (a :sort 0) -> (b : isort 0) -> (a -> CompM b) -> (n : Nat) -> Vec n a -> CompM (Vec n b);
mapM a b f =
  Nat__rec
    (\ (n:Nat) -> Vec n a -> CompM (Vec n b))
    (\ (_:Vec 0 a) -> returnM (Vec 0 b) (EmptyVec b))
    (\ (n:Nat) (rec_f:Vec n a -> CompM (Vec n b)) (v:Vec (Succ n) a) ->
       fmapM2 b (Vec n b) (Vec (Succ n) b)
              (\ (hd:b) (tl:Vec n b) -> ConsVec b hd n tl)
              (f (head n a v))
              (rec_f (tail n a v)));

-- Map a monadic function across a BVVec
mapBVVecM : (a : sort 0) -> (b : isort 0) -> (a -> CompM b) ->
            (n : Nat) -> (len : Vec n Bool) -> BVVec n len a ->
            CompM (BVVec n len b);
mapBVVecM a b f n len = mapM a b f (bvToNat n len);

-- Append two BVVecs and cast the resulting size, if possible
appendCastBVVecM : (n : Nat) -> (len1 len2 len3 : Vec n Bool) -> (a : sort 0) ->
                   BVVec n len1 a -> BVVec n len2 a ->
                   CompM (BVVec n len3 a);
appendCastBVVecM n len1 len2 len3 a v1 v2 =
  maybe
    (Eq (Vec n Bool) (bvAdd n len1 len2) len3) (CompM (BVVec n len3 a))
    (errorM (BVVec n len3 a) "Could not cast BVVec")
    (\ (pf:Eq (Vec n Bool) (bvAdd n len1 len2) len3) ->
       returnM
         (BVVec n len3 a)
         (coerce (BVVec n (bvAdd n len1 len2) a) (BVVec n len3 a)
                 (eq_cong (Vec n Bool) (bvAdd n len1 len2) len3 pf
                          (sort 0) (\ (l:Vec n Bool) -> BVVec n l a))
                 (appendBVVec n len1 len2 a v1 v2)))
    (bvEqWithProof n (bvAdd n len1 len2) len3);

-- Run the first computation, and, if it raises an error, catch the error and
-- run the second computation
-- primitive catchM : (a:sort 0) -> CompM a -> CompM a -> CompM a;

-- The computation that nondeterministically chooses a value of type a and
-- passes it to the supplied function f to get a computation of type b. As a
-- specification, this is the union of computations f x.
primitive existsM : (a b:sort 0) -> (a -> CompM b) -> CompM b;

-- The computation that nondeterministically chooses one computation or another.
-- As a specification, represents the disjunction of two specifications.
orM : (a : sort 0) -> CompM a -> CompM a -> CompM a;
orM a m1 m2 = existsM Bool a (\ (b:Bool) -> ite (CompM a) b m1 m2);

-- The specification that matches any computation
anySpec : (a : sort 0) -> CompM a;
anySpec a = existsM (CompM a) a (\ (m:CompM a) -> m);

-- The specification formed from the intersection of all computations f x for
-- all possible inputs x. Computationally, this is sort of like running f for
-- all possible inputs x at the same time and then raising an error if any of
-- those computations diverge from each other.
primitive forallM : (a b:sort 0) -> (a -> CompM b) -> CompM b;

-- The specification which asserts that the first argument is True and then
-- runs the second argument
assertingM : (a : sort 0) -> Bool -> CompM a -> CompM a;
assertingM a b m = ite (CompM a) b m (errorM a "Assertion failed");

-- The specification which assumes that the first argument is True and then
-- runs the second argument
assumingM : (a : sort 0) -> Bool -> CompM a -> CompM a;
assumingM a b m = ite (CompM a) b m (anySpec a);

-- A hint to Mr Solver that a recursive function has the given loop invariant
invariantHint : (a : sort 0) -> Bool -> a -> a;
invariantHint _ _ a = a;

-- The version of assertingM which appears in un-monadified Cryptol (this gets
-- converted to assertingM during monadification, see assertingOrAssumingMacro)
asserting : (a : isort 0) -> Bool -> a -> a;
asserting a b x = ite a b x (error a "Assertion failed");

-- The version of assumingM which appears in un-monadified Cryptol (this gets
-- converted to assumingM during monadification, see assertingOrAssumingMacro)
assuming : (a : isort 0) -> Bool -> a -> a;
assuming a b x = ite a b x (error a "Assuming failed");

-- NOTE: for the simplicity and efficiency of MR solver, we define all
-- fixed-point computations in CompM via a primitive multiFixM, defined below.
-- Thus, even though fixM is really the primitive operation, we write this file
-- as if multiFixM is, but I am leaving this version of fixM commented out here
-- to keep this decision explicitly documented and to make it easier to switch
-- back to having fixM be primitive if we decide to do so later.
--
{-
primitive fixM : (a:sort 0) -> (b:a -> sort 0) ->
                 (((x:a) -> CompM (b x)) -> ((x:a) -> CompM (b x))) ->
                 (x:a) -> CompM (b x);
-}

-- A representation of the type (x1:A1) -> ... -> (xn:An) -> CompM (B x1 ... xn)
data LetRecType : sort 1 where {
  LRT_Ret : sort 0 -> LetRecType;
  LRT_Fun : (a:sort 0) -> (a -> LetRecType) -> LetRecType;
}

-- Convert a LetRecType to the type it represents
lrtToType : LetRecType -> sort 0;
lrtToType lrt =
  LetRecType#rec
  (\ (lrt:LetRecType) -> sort 0)
  (\ (b:sort 0) -> CompM b)
  (\ (a:sort 0) (_: a -> LetRecType) (b: a -> sort 0) -> (x:a) -> b x)
  lrt;

-- NOTE: the following are needed to define multiFixM instead of making it a
-- primitive, which we are keeping commented here in case that is needed
{-
-- Convert the argument types of a LetRecType to their "flat" version of the
-- form { x1:A1 & { x2:A2 & ... { xn:An & unit } ... }}
lrtToFlatArgs : LetRecType -> sort 0;
lrtToFlatArgs lrt =
  LetRecType#rec
  (\ (lrt:LetRecType) -> sort 0)
  (\ (_:sort 0) -> #())
  (\ (a:sort 0) (_: a -> LetRecType) (b: a -> sort 0) -> Sigma a b)
  lrt;

-- Get the dependent return type fun (args:lrtToFlatArgs) => B x.1 ... of a
-- LetRecType in terms of the flat arguments
lrtToFlatRet : (lrt:LetRecType) -> lrtToFlatArgs lrt -> sort 0;
lrtToFlatRet lrt =
  LetRecType#rec
  (\ (lrt:LetRecType) -> lrtToFlatArgs lrt -> sort 0)
  (\ (a:sort 0) (_:#()) -> a)
  (\ (a:sort 0) (lrtF: a -> LetRecType)
      (retF: (x:a) -> lrtToFlatArgs (lrtF x) -> sort 0)
      (args: Sigma a (\ (x:a) -> lrtToFlatArgs (lrtF x))) ->
      retF (Sigma_proj1 a (\ (x:a) -> lrtToFlatArgs (lrtF x)) args)
           (Sigma_proj2 a (\ (x:a) -> lrtToFlatArgs (lrtF x)) args))
  lrt;

-- Extract out the "flat" version of a LetRecType
lrtToFlatType : LetRecType -> sort 0;
lrtToFlatType lrt = (args:lrtToFlatArgs lrt) -> CompM (lrtToFlatRet lrt args);


-- "Flatten" a function described by a LetRecType
flattenLRTFun : (lrt:LetRecType) -> lrtToType lrt -> lrtToFlatType lrt;
flattenLRTFun lrt =
  LetRecType#rec
  (\ (lrt:LetRecType) -> lrtToType lrt -> lrtToFlatType lrt)
  (\ (b:sort 0) (f:CompM b) (_:#()) -> f)
  (\ (a:sort 0) (lrtF: a -> LetRecType)
     (restF: (x:a) -> lrtToType (lrtF x) -> lrtToFlatType (lrtF x))
     (f: lrtToType (LRT_Fun a lrtF)) (args:lrtToFlatArgs (LRT_Fun a lrtF)) ->
     restF (Sigma_proj1 a (\ (x:a) -> lrtToFlatArgs (lrtF x)) args)
           (f (Sigma_proj1 a (\ (x:a) -> lrtToFlatArgs (lrtF x)) args))
           (Sigma_proj2 a (\ (x:a) -> lrtToFlatArgs (lrtF x)) args))
  lrt;

-- "Unflatten" a function described by a LetRecType
unflattenLRTFun : (lrt:LetRecType) -> lrtToFlatType lrt -> lrtToType lrt;
unflattenLRTFun lrt =
  LetRecType#rec
  (\ (lrt:LetRecType) -> lrtToFlatType lrt -> lrtToType lrt)
  (\ (b:sort 0) (f:#() -> CompM b) -> f ())
  (\ (a:sort 0) (lrtF: a -> LetRecType)
     (restF: (x:a) -> lrtToFlatType (lrtF x) -> lrtToType (lrtF x))
     (f: lrtToFlatType (LRT_Fun a lrtF)) (x:a) ->
     restF x (\ (args:lrtToFlatArgs (lrtF x)) ->
                f (exists a (\ (y:a) -> lrtToFlatArgs (lrtF y)) x args)))
  lrt;
-}

-- A list of 0 or more LetRecTypes
data LetRecTypes : sort 1 where {
  LRT_Nil : LetRecTypes;
  LRT_Cons : LetRecType -> LetRecTypes -> LetRecTypes;
}

-- Build the function type lrtToType lrt1 -> ... -> lrtToType lrtn -> b from the
-- LetRecTypes list [lrt1, ..., lrtn]
lrtPi : LetRecTypes -> sort 0 -> sort 0;
lrtPi lrts b =
  LetRecTypes#rec
  (\ (lrts:LetRecTypes) -> sort 0)
  b
  (\ (lrt:LetRecType) (_:LetRecTypes) (rest:sort 0) -> lrtToType lrt -> rest)
  lrts;

-- Build the product type (lrtToType lrt1, ..., lrtToType lrtn) from the
-- LetRecTypes list [lrt1, ..., lrtn]
lrtTupleType : LetRecTypes -> sort 0;
lrtTupleType lrts =
  LetRecTypes#rec
  (\ (lrts:LetRecTypes) -> sort 0)
  #()
  (\ (lrt:LetRecType) (_:LetRecTypes) (rest:sort 0) -> #(lrtToType lrt, rest))
  lrts;

-- NOTE: the following are needed to define letRecM instead of making it a
-- primitive, which we are keeping commented here in case that is needed
{-
-- Apply a multi-arity function of type lrtPi lrts B to an lrtTupleType lrts
lrtApply : (lrts:LetRecTypes) -> (B:sort 0) -> lrtPi lrts B -> lrtTupleType lrts -> B;
lrtApply top_lrts B =
  LetRecTypes#rec
  (\ (lrts:LetRecTypes) -> lrtPi lrts B -> lrtTupleType lrts -> B)
  (\ (F:B) (_:#()) -> F)
  (\ (lrt:LetRecType) (lrts:LetRecTypes) (rest:lrtPi lrts B -> lrtTupleType lrts -> B)
      (F:lrtPi (LRT_Cons lrt lrts) B) (fs:lrtTupleType (LRT_Cons lrt lrts)) ->
    rest (F fs.(1)) fs.(2))
  top_lrts;

-- Construct a multi-arity function of type lrtPi lrts B from one of type
-- lrtTupleType lrts -> B
lrtLambda : (lrts:LetRecTypes) -> (B:sort 0) -> (lrtTupleType lrts -> B) -> lrtPi lrts B;
lrtLambda top_lrts B =
  LetRecTypes#rec
  (\ (lrts:LetRecTypes) -> (lrtTupleType lrts -> B) -> lrtPi lrts B)
  (\ (F:#() -> B) -> F ())
  (\ (lrt:LetRecType) (lrts:LetRecTypes)
     (rest:(lrtTupleType lrts -> B) -> lrtPi lrts B)
     (F:lrtTupleType (LRT_Cons lrt lrts) -> B) (f:lrtToType lrt) ->
    rest (\ (fs:lrtTupleType lrts) -> F (f, fs)))
  top_lrts;

-- Build a multi-argument fixed-point of type A1 -> ... -> An -> CompM B
multiArgFixM : (lrt:LetRecType) -> (lrtToType lrt -> lrtToType lrt) ->
               lrtToType lrt;
multiArgFixM lrt F =
  unflattenLRTFun
    lrt
    (fixM (lrtToFlatArgs lrt) (lrtToFlatRet lrt)
          (\ (f:lrtToFlatType lrt) ->
             flattenLRTFun lrt (F (unflattenLRTFun lrt f))));

-- Construct a mutual fixed-point over tuples of LRT functions
multiTupleFixM : (lrts:LetRecTypes) -> (lrtTupleType lrts -> lrtTupleType lrts) ->
                 lrtTupleType lrts;
multiTupleFixM top_lrts =
  LetRecTypes#rec
  (\ (lrts:LetRecTypes) -> (lrtTupleType lrts -> lrtTupleType lrts) -> lrtTupleType lrts)
  (\ (_:#() -> #()) -> ())
  (\ (lrt:LetRecType) (lrts:LetRecTypes)
     (restF: (lrtTupleType lrts -> lrtTupleType lrts) -> lrtTupleType lrts)
     (F:lrtTupleType (LRT_Cons lrt lrts) -> lrtTupleType (LRT_Cons lrt lrts)) ->
     (multiArgFixM lrt (\ (f:lrtToType lrt) ->
                          (F (f, restF (\ (fs:lrtTupleType lrts) ->
                                          (F (f, fs)).(2)))).(1)),
      restF (\ (fs:lrtTupleType lrts) ->
               (F (multiArgFixM lrt
                     (\ (f:lrtToType lrt) ->
                        (F (f, restF (\ (fs:lrtTupleType lrts) ->
                                        (F (f, fs)).(2)))).(1)),
                   fs)).(2))))
  top_lrts;

-- A nicer version of multiTupleFixM that abstracts the functions one at a time
multiFixM : (lrts:LetRecTypes) -> lrtPi lrts (lrtTupleType lrts) ->
            lrtTupleType lrts;
multiFixM lrts F =
  multiTupleFixM lrts (\ (fs:lrtTupleType lrts) -> lrtApply lrts (lrtTupleType lrts) F fs);
-}

-- This is like let rec in ML: letRecM defs body defines N recursive functions
-- in terms of themselves using defs, and then passes them to body. We use this
-- instead of the more standard fixM because it offers a more compact
-- representation, and because fixM messes with functional extensionality by
-- introducing an irreducible term at function type.
primitive letRecM : (lrts : LetRecTypes) -> (B:sort 0) ->
                    lrtPi lrts (lrtTupleType lrts) ->
                    lrtPi lrts (CompM B) -> CompM B;
-- letRecM lrts B F body = lrtApply lrts (CompM B) body (multiFixM lrts F);

-- This is let rec with exactly one binding
letRecM1 : (a b c : sort 0) -> ((a -> CompM b) -> (a -> CompM b)) ->
           ((a -> CompM b) -> CompM c) -> CompM c;
letRecM1 a b c fn body =
  letRecM
    (LRT_Cons (LRT_Fun a (\ (_:a) -> LRT_Ret b)) LRT_Nil) c
    (\ (f:a -> CompM b) -> (fn f, ()))
    (\ (f:a -> CompM b) -> body f);

-- A single-argument fixed-point function
fixM : (a:sort 0) -> (b:a -> sort 0) ->
       (((x:a) -> CompM (b x)) -> ((x:a) -> CompM (b x))) ->
       (x:a) -> CompM (b x);
fixM a b f x =
  letRecM (LRT_Cons (LRT_Fun a (\ (y:a) -> LRT_Ret (b y))) LRT_Nil)
          (b x)
          (\ (g: (y:a) -> CompM (b y)) -> (f g, ()))
          (\ (g: (y:a) -> CompM (b y)) -> g x);


-- The following commented block allows multiFixM to be defined in terms of and
-- to reduce to letRecM, which is useful if we want to define all our automated
-- reasoning in terms of letRecM instead of multiFixM

-- Apply a function the the body of a multi-arity lrtPi function
{-
lrtPiMap : (a b : sort 0) -> (f : a -> b) -> (lrts : LetRecTypes) ->
           lrtPi lrts a -> lrtPi lrts b;
lrtPiMap a b f lrts_top =
  LetRecTypes#rec
  (\ (lrts:LetRecTypes) -> lrtPi lrts a -> lrtPi lrts b)
  (\ (x:a) -> f x)
  (\ (lrt:LetRecType) (lrts:LetRecTypes) (rec:lrtPi lrts a -> lrtPi lrts b)
     (f:lrtToType lrt -> lrtPi lrts a) (g:lrtToType lrt) ->
     rec (f g))
  lrts_top;

-- Convert a multi-arity lrtPi that returns a pair to a pair of lrtPi functions
-- that return the individual arguments
lrtPiPair : (a b:sort 0) -> (lrts : LetRecTypes) -> lrtPi lrts #(a,b) ->
            #(lrtPi lrts a, lrtPi lrts b);
lrtPiPair a b lrts f =
  (lrtPiMap #(a,b) a (\ (tup:#(a,b)) -> tup.(1)) lrts f,
   lrtPiMap #(a,b) b (\ (tup:#(a,b)) -> tup.(2)) lrts f);

-- Build a monadic function that takes in its arguments and then calls letRecM.
-- That is, build a function
--
-- \x1 ... xn -> letRecM lrts F (\f1 ... fm -> body f1 ... fm x1 ... xn)
--
-- where F recursively defines the fi functions and body defines the computation
-- for the function we are defining in terms of the fi and the xj arguments.
letRecFun : (lrts : LetRecTypes) -> lrtPi lrts (lrtTupleType lrts) ->
            (lrt : LetRecType) -> lrtPi lrts (lrtToType lrt) -> lrtToType lrt;
letRecFun lrts F lrt_top =
  LetRecType#rec
  (\ (lrt:LetRecType) -> lrtPi lrts (lrtToType lrt) -> lrtToType lrt)
  (\ (b:sort 0) (body:lrtPi lrts (CompM b)) ->
     letRecM lrts b F body)
  (\ (a:sort 0) (lrtF: a -> LetRecType)
     (rec: (x:a) -> lrtPi lrts (lrtToType (lrtF x)) -> lrtToType (lrtF x))
     (body:lrtPi lrts ((x:a) -> lrtToType (lrtF x)))
     (x:a) ->
     rec x (lrtPiMap ((y:a) -> lrtToType (lrtF y))
                     (lrtToType (lrtF x))
                     (\ (g:(y:a) -> lrtToType (lrtF y)) -> g x)
                     lrts
                     body))
  lrt_top;

-- Build a multi-argument fixed-point of type A1 -> ... -> An -> CompM B
multiArgFixM : (lrt:LetRecType) -> (lrtToType lrt -> lrtToType lrt) ->
               lrtToType lrt;
multiArgFixM lrt F =
  letRecFun (LRT_Cons lrt LRT_Nil)
            (\ (f:lrtToType lrt) -> (F f, ()))
            lrt
            (\ (f:lrtToType lrt) -> f);

-- Construct a fixed-point for a tuple of mutually-recursive functions
multiFixM : (lrts:LetRecTypes) -> lrtPi lrts (lrtTupleType lrts) ->
            lrtTupleType lrts;
multiFixM lrts_top F_top =
  LetRecTypes#rec
  (\ (lrts:LetRecTypes) -> lrtPi lrts_top (lrtTupleType lrts) ->
     lrtTupleType lrts)
  (\ (_:lrtPi lrts_top #()) -> ())
  (\ (lrt:LetRecType) (lrts:LetRecTypes)
     (rec: lrtPi lrts_top (lrtTupleType lrts) -> lrtTupleType lrts)
     (F: lrtPi lrts_top #(lrtToType lrt, lrtTupleType lrts)) ->
     (letRecFun
        lrts_top F_top lrt
        (lrtPiPair (lrtToType lrt) (lrtTupleType lrts) lrts_top F).(1)
      ,
      rec (lrtPiPair (lrtToType lrt) (lrtTupleType lrts) lrts_top F).(2)))
  lrts_top
  F_top;
-}

-- Construct a fixed-point for a tuple of mutually-recursive functions
--
-- NOTE: Currently, Mr Solver actually works better with a primitive multiFixM,
-- so that's what we are going to do for now...
primitive
multiFixM : (lrts:LetRecTypes) -> lrtPi lrts (lrtTupleType lrts) ->
            lrtTupleType lrts;

-- Build a multi-argument fixed-point of type A1 -> ... -> An -> CompM B
multiArgFixM : (lrt:LetRecType) -> (lrtToType lrt -> lrtToType lrt) ->
               lrtToType lrt;
multiArgFixM lrt F =
  (multiFixM (LRT_Cons lrt LRT_Nil) (\ (f:lrtToType lrt) -> (F f, ()))).(1);


-- Test computations
test_fun0 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun0 _ = returnM (Vec 64 Bool) (bvNat 64 0);

test_fun1 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun1 _ = returnM (Vec 64 Bool) (bvNat 64 1);

test_fun2 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun2 x = returnM (Vec 64 Bool) x;

-- If x == 0 then x else 0; should be equal to 0
test_fun3 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun3 x =
  ite (CompM (Vec 64 Bool)) (bvEq 64 x (bvNat 64 0))
      (returnM (Vec 64 Bool) x)
      (returnM (Vec 64 Bool) (bvNat 64 0));

-- let rec f x = 0 in f x
test_fun4 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun4 x =
  letRecM1
    (Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (y:Vec 64 Bool) ->
      returnM (Vec 64 Bool) (bvNat 64 0))
    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) ->
      f x);

{- Alternate version of test_fun4 that uses letRecM directly
test_fun4 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun4 x =
  letRecM
    (LRT_Cons (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool))
     LRT_Nil)
    (Vec 64 Bool)
    (\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
      ((\ (y:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 0)), ()))
    (\ (f:(Vec 64 Bool -> CompM (Vec 64 Bool))) -> f x);
-}

-- let rec f = f in f x
test_fun5 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun5 x =
  letRecM1
    (Vec 64 Bool) (Vec 64 Bool) (Vec 64 Bool)
    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f)
    (\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) -> f x);

-- let rec f = g and g = f in f x
test_fun6 : Vec 64 Bool -> CompM (Vec 64 Bool);
test_fun6 x =
  letRecM
    (LRT_Cons
      (LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
      (LRT_Cons
        (LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) -> LRT_Ret (Vec 64 Bool)))
        LRT_Nil))
    (Vec 64 Bool)
    (\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
       (f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
      (f2, (f1, ())))
    (\ (f1:(Vec 64 Bool -> CompM (Vec 64 Bool)))
       (f2:(Vec 64 Bool -> CompM (Vec 64 Bool))) ->
      f1 x);


--------------------------------------------------------------------------------
-- ITree Specification monad

-- Lists at sort 1
data List1 (a:sort 1) : sort 1 where {
  Nil1 : List1 a;
  Cons1 : a -> List1 a -> List1 a;
}

-- An event type is a type of events plus a mapping from events to their return
-- types
data EvType : sort 1 where {
   Build_EvType : (E:sort 0) -> (E -> sort 0) -> EvType;
}

-- Get the type for an EvType
evTypeType : EvType -> sort 0;
evTypeType e =
  EvType#rec (\ (_:EvType) -> sort 0) (\ (E:sort 0) (_:E -> sort 0) -> E) e;

-- Get the return type for an event
evRetType : (E:EvType) -> evTypeType E -> sort 0;
evRetType e =
  EvType#rec (\ (E:EvType) -> evTypeType E -> sort 0)
             (\ (E:sort 0) (evTypeEnc:E -> sort 0) -> evTypeEnc) e;

-- The EvType with Void as the event type
VoidEv : EvType;
VoidEv = Build_EvType Void (elimVoid (sort 0));

-- Build the dependent type { a1:A1 & { a2:A2 & ... { an:An & unit } ... }} of
-- inputs to the LetRecType (LRT_Fun A1 (\ a1 -> ...))
LRTInput : LetRecType -> sort 0;
LRTInput lrt =
  LetRecType#rec
  (\ (lrt:LetRecType) -> sort 0)
  (\ (_:sort 0) -> #())
  (\ (a:sort 0) (_: a -> LetRecType) (b: a -> sort 0) -> Sigma a b)
  lrt;

-- Build the output type (R a1 ... an) of the application of a LetRecType
-- (LRT_Fun A1 (\ a1 -> ... (LRT_Fun An (\ an -> LRT_Ret R a1 ... an))))
-- function to the arguments a1 ... an in an LRTInput
LRTOutput : (lrt:LetRecType) -> LRTInput lrt -> sort 0;
LRTOutput lrt =
  LetRecType#rec
  (\ (lrt:LetRecType) -> LRTInput lrt -> sort 0)
  (\ (R:sort 0) (_:LRTInput (LRT_Ret R)) -> R)
  (\ (a:sort 0) (lrtF : a -> LetRecType)
     (rec : (x:a) -> LRTInput (lrtF x) -> sort 0)
     (args: Sigma a (\ (x:a) -> LRTInput (lrtF x))) ->
     rec (Sigma_proj1 a (\ (x:a) -> LRTInput (lrtF x)) args)
         (Sigma_proj2 a (\ (x:a) -> LRTInput (lrtF x)) args))
  lrt;

-- Build the function type (a1:A1) -> ... -> (an:An) -> B from the LetRecType
-- (LRT_Fun A1 (\ a1 -> ...))
lrt1Pi : (lrt:LetRecType) -> (LRTInput lrt -> sort 0) -> sort 0;
lrt1Pi lrt_top =
  LetRecType#rec
  (\ (lrt:LetRecType) -> (LRTInput lrt -> sort 0) -> sort 0)
  (\ (_:sort 0) (F:#() -> sort 0) -> F ())
  (\ (a:sort 0) (lrtF: a -> LetRecType)
     (rec: (x:a) -> (LRTInput (lrtF x) -> sort 0) -> sort 0)
     (F : LRTInput (LRT_Fun a lrtF) -> sort 0) ->
     (x:a) -> rec x (\ (args : LRTInput (lrtF x)) ->
                       F (exists a (\ (y:a) -> LRTInput (lrtF y)) x args)))
  lrt_top;

-- Build an lrtPi function from a unary function on an LRTInput
lrtLambda : (lrt:LetRecType) -> (F: LRTInput lrt -> sort 0) ->
            ((args: LRTInput lrt) -> F args) -> lrt1Pi lrt F;
lrtLambda lrt_top =
  LetRecType#rec
  (\ (lrt:LetRecType) -> (F: LRTInput lrt -> sort 0) ->
                         ((args: LRTInput lrt) -> F args) -> lrt1Pi lrt F)
  (\ (_:sort 0) -> \ (F: #() -> sort 0) (f : (args:#()) -> F args) -> f ())
  (\ (a:sort 0) (lrtF: a -> LetRecType)
     (rec: (x:a) -> (F: LRTInput (lrtF x) -> sort 0) ->
                    ((args: LRTInput (lrtF x)) -> F args) -> lrt1Pi (lrtF x) F)
     (F: LRTInput (LRT_Fun a lrtF) -> sort 0)
     (f : (args: LRTInput (LRT_Fun a lrtF)) -> F args) (x:a) ->
     rec x (\ (args:LRTInput (lrtF x)) ->
              F (exists a (\ (y:a) -> LRTInput (lrtF y)) x args))
           (\ (args:LRTInput (lrtF x)) ->
              f (exists a (\ (y:a) -> LRTInput (lrtF y)) x args)))
  lrt_top;

-- A recursive frame is a list of types for recursive functions all bound
-- same time
RecFrame : sort 1;
RecFrame = (List1 LetRecType);

-- Get the nth element of a RecFrame, or void -> void if n is too big
nthLRT : List1 LetRecType -> Nat -> LetRecType;
nthLRT lrts =
  List1#rec
  LetRecType
  (\ (lrts:List1 LetRecType) -> Nat -> LetRecType)
  (\ (_:Nat) -> LRT_Fun Void (\ (_:Void) -> LRT_Ret Void))
  (\ (lrt:LetRecType) (_:List1 LetRecType) (rec:Nat -> LetRecType) (n:Nat) ->
     Nat#rec (\ (_:Nat) -> LetRecType) lrt (\ (m:Nat) (_:LetRecType) -> rec m) n)
  lrts;

-- A recursive call to one of the functions in a RecFrame
data FrameCall (frame : RecFrame) : sort 0 where {
  FrameCallOfArgs : (n:Nat) -> LRTInput (nthLRT frame n) -> FrameCall frame;
}

-- Make a recursive call from its individual arguments
mkFrameCall : (frame:RecFrame) -> (n:Nat) ->
              lrt1Pi (nthLRT frame n) (\ (_:LRTInput (nthLRT frame n)) ->
                                         FrameCall frame);
mkFrameCall frame n =
  lrtLambda (nthLRT frame n) (\ (_:LRTInput (nthLRT frame n)) -> FrameCall frame)
            (\ (args:LRTInput (nthLRT frame n)) -> FrameCallOfArgs frame n args);

-- The return type for calling a recursive function in a RecFrame
FrameCallRet : (frame:RecFrame) -> FrameCall frame -> sort 0;
FrameCallRet frame call =
  FrameCall#rec
  frame
  (\ (_:FrameCall frame) -> sort 0)
  (\ (n:Nat) (args:LRTInput (nthLRT frame n)) -> LRTOutput (nthLRT frame n) args)
  call;

-- A function stack is a list of values of type LetRecTypes, which intuitively
-- represents a stack of bindings of mutually recursive functions
FunStack : sort 1;
FunStack = List1 (List1 LetRecType);

-- The empty FunStack
emptyFunStack : FunStack;
emptyFunStack = Nil1 (List1 LetRecType);

-- Push a frame, represented by a LetRecTypes list, onto the top of a FunStack
pushFunStack : List1 LetRecType -> FunStack -> FunStack;
pushFunStack frame stack = Cons1 (List1 LetRecType) frame stack;

-- The monad for specifications (FIXME: document this!)
primitive SpecM : (E:EvType) -> FunStack -> sort 0 -> sort 0;


-- Return for SpecM
primitive retS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> a ->
                 SpecM E stack a;

-- Bind for SpecM
primitive bindS : (E:EvType) -> (stack:FunStack) ->
                  (a b:sort 0) -> SpecM E stack a ->
                  (a -> SpecM E stack b) -> SpecM E stack b;

-- Trigger an event in type E, returning its return type
primitive triggerS : (E:EvType) -> (stack:FunStack) -> (e:evTypeType E) ->
                     SpecM E stack (evRetType E e);

-- Signal an error in SpecM
primitive errorS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> String ->
                   SpecM E stack a;

-- The spec that universally quantifies over all return values of type a
primitive forallS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) ->
                    SpecM E stack a;

-- The spec that existentially quantifies over all return values of type a
primitive existsS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) ->
                    SpecM E stack a;

primitive assumeS : (E:EvType) -> (stack:FunStack) ->
                    (p:Prop) -> SpecM E stack #();
primitive assertS : (E:EvType) -> (stack:FunStack) ->
                    (p:Prop) -> SpecM E stack #();

primitive liftStackS : (E:EvType) -> (stack:FunStack) -> (A:sort 0) ->
                       SpecM E emptyFunStack A -> SpecM E stack A;

-- Return the type represented by a LetRecType
LRTType : (E:EvType) -> FunStack -> LetRecType -> sort 0;
LRTType E stack lrt =
  LetRecType#rec
  (\ (lrt:LetRecType) -> sort 0)
  (\ (r:sort 0) -> SpecM E stack r)
  (\ (a:sort 0) (_:a -> LetRecType) (b:a -> sort 0) -> (x:a) -> b x)
  lrt;

-- Build the right-nested tuple type (T1 * (T2 * ... (Tn * #()))) where each Ti
-- is the result of calling LRTType on the ith LetRecType in a list
FrameTuple : (E:EvType) -> FunStack -> List1 LetRecType -> sort 0;
FrameTuple E stack lrts =
  List1#rec
  LetRecType
  (\ (_:List1 LetRecType) -> sort 0)
  #()
  (\ (lrt:LetRecType) (_:List1 LetRecType) (rest:sort 0) ->
     (LRTType E stack lrt) * rest)
  lrts;

-- A recursive call to a function in the top frame of a function stack
primitive callS :
  (E:EvType) -> (stack:FunStack) -> (frame:List1 LetRecType) ->
  (call : FrameCall frame) ->
  SpecM E (pushFunStack frame stack) (FrameCallRet frame call);

-- Bind a collection of recursive functions whose types are given by a frame of
-- LetRecTypes and whose bodies are given by an FrameTuple, and call the nth one
primitive multiFixS :
  (E:EvType) -> (stack:FunStack) -> (frame:List1 LetRecType) ->
  FrameTuple E (pushFunStack frame stack) frame ->
  (call : FrameCall frame) ->
  SpecM E stack (FrameCallRet frame call);

-- Apply a pure function to the result of a computation
fmapS : (E:EvType) -> (stack:FunStack) -> (a b:sort 0) -> (a -> b) ->
        SpecM E stack a ->
        SpecM E stack b;
fmapS E stack a b f m =
      bindS E stack a b m (\ (x:a) -> retS E stack b (f x));

-- Apply a computation of a function to a computation of an argument
applyS : (E:EvType) -> (stack:FunStack) -> (a b:sort 0) ->
         SpecM E stack (a -> b) ->
         SpecM E stack a -> SpecM E stack b;
applyS E stack a b fm m =
  bindS E stack (a -> b) b fm (\ (f:a -> b) ->
    bindS E stack a b m (\ (x:a) -> retS E stack b (f x)));

-- Apply a binary pure function to a computation
fmapS2 : (E:EvType) -> (stack:FunStack) -> (a b c:sort 0) -> (a -> b -> c) ->
         SpecM E stack a -> SpecM E stack b ->
         SpecM E stack c;
fmapS2 E stack a b c f m1 m2 =
  applyS E stack b c (fmapS E stack a (b -> c) f m1) m2;

-- Apply a trinary pure function to a computation
fmapS3 : (E:EvType) -> (stack:FunStack) ->
         (a b c d:sort 0) -> (a -> b -> c -> d) ->
         SpecM E stack a -> SpecM E stack b ->
         SpecM E stack c -> SpecM E stack d;
fmapS3 E stack a b c d f m1 m2 m3 =
  applyS E stack c d (fmapS2 E stack a b (c -> d) f m1 m2) m3;

-- Bind two values and pass them to a binary function
bindS2 : (E:EvType) -> (stack:FunStack) -> (a b c:sort 0) ->
         SpecM E stack a ->
         SpecM E stack b -> (a -> b -> SpecM E stack c) ->
         SpecM E stack c;
bindS2 E stack a b c m1 m2 k =
  bindS E stack a c m1
  (\ (x:a) -> bindS E stack b c m2 (\ (y:b) -> k x y));

-- Bind three values and pass them to a trinary function
bindS3 : (E:EvType) -> (stack:FunStack) ->
         (a b c d:sort 0) -> SpecM E stack a ->
         SpecM E stack b -> SpecM E stack c ->
         (a -> b -> c -> SpecM E stack d) -> SpecM E stack d;
bindS3 E stack a b c d m1 m2 m3 k =
  bindS E stack a d m1
        (\ (x:a) -> bindS2 E stack b c d m2 m3 (k x));

-- A version of bind that takes the function first
bindApplyS : (E:EvType) -> (stack:FunStack) ->
             (a b:sort 0) -> (a -> SpecM E stack b) ->
             SpecM E stack a -> SpecM E stack b;
bindApplyS E stack a b k m =
  bindS E stack a b m k;

-- A version of bindS2 that takes the function first
bindApplyS2 : (E:EvType) -> (stack:FunStack) ->
              (a b c:sort 0) -> (a -> b -> SpecM E stack c) ->
              SpecM E stack a -> SpecM E stack b ->
              SpecM E stack c;
bindApplyS2 E stack a b c k m1 m2 =
  bindS2 E stack a b c m1 m2 k;

-- A version of bindS3 that takes the function first
bindApplyS3 : (E:EvType) -> (stack:FunStack) ->
              (a b c d:sort 0) -> (a -> b -> c -> SpecM E stack d) ->
              SpecM E stack a -> SpecM E stack b ->
              SpecM E stack c -> SpecM E stack d;
bindApplyS3 E stack a b c d k m1 m2 m3 =
  bindS3 E stack a b c d m1 m2 m3 k;

-- Compose two monadic functions
composeS : (E:EvType) -> (stack:FunStack) ->
           (a b c:sort 0) -> (a -> SpecM E stack b) ->
           (b -> SpecM E stack c) -> a -> SpecM E stack c;
composeS E stack a b c k1 k2 x =
  bindS E stack b c (k1 x) k2;

-- Tuple a type onto the input and output types of a monadic function
tupleSpecMFunBoth : (E:EvType) -> (stack:FunStack) ->
                    (a b c:sort 0) -> (a -> SpecM E stack b) ->
                    (c * a -> SpecM E stack (c * b));
tupleSpecMFunBoth E stack a b c k =
  \ (x: c * a) ->
    bindS E stack b (c * b) (k x.(2))
          (\ (y:b) -> retS E stack (c*b) (x.(1), y));

-- Tuple a value onto the output of a monadic function
tupleSpecMFunOut : (E:EvType) -> (stack:FunStack) -> (a b c:sort 0) ->
  c -> (a -> SpecM E stack b) -> (a -> SpecM E stack (c*b));
tupleSpecMFunOut E stack a b c x f =
  \ (y:a) -> bindS E stack b (c*b) (f y)
             (\ (z:b) -> retS E stack (c*b) (x,z));

-- Map a monadic function across a vector
mapS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) ->
       (b:isort 0) -> (a -> SpecM E stack b) -> (n:Nat) -> Vec n a ->
       SpecM E stack (Vec n b);
mapS E stack a b f =
  Nat__rec
    (\ (n:Nat) -> Vec n a -> SpecM E stack (Vec n b))
    (\ (_:Vec 0 a) -> retS E stack (Vec 0 b) (EmptyVec b))
    (\ (n:Nat) (rec_f:Vec n a -> SpecM E stack (Vec n b))
       (v:Vec (Succ n) a) ->
      fmapS2 E stack b (Vec n b) (Vec (Succ n) b)
        (\ (hd:b) (tl:Vec n b) -> ConsVec b hd n tl)
        (f (head n a v))
        (rec_f (tail n a v)));

-- Map a monadic function across a BVVec
mapBVVecS : (E:EvType) -> (stack:FunStack) ->
            (a : sort 0) -> (b : isort 0) -> (a -> SpecM E stack b) ->
            (n : Nat) -> (len : Vec n Bool) -> BVVec n len a ->
            SpecM E stack (BVVec n len b);
mapBVVecS E stack a b f n len = mapS E stack a b f (bvToNat n len);

-- Append two BVVecs and cast the resulting size, if possible
appendCastBVVecS : (E:EvType) -> (stack:FunStack) ->
                   (n : Nat) -> (len1 len2 len3 : Vec n Bool) -> (a : sort 0) ->
                   BVVec n len1 a -> BVVec n len2 a ->
                   SpecM E stack (BVVec n len3 a);
appendCastBVVecS E stack n len1 len2 len3 a v1 v2 =
  maybe
    (Eq (Vec n Bool) (bvAdd n len1 len2) len3) (SpecM E stack (BVVec n len3 a))
    (errorS E stack (BVVec n len3 a) "Could not cast BVVec")
    (\ (pf:Eq (Vec n Bool) (bvAdd n len1 len2) len3) ->
       retS
         E stack (BVVec n len3 a)
         (coerce (BVVec n (bvAdd n len1 len2) a) (BVVec n len3 a)
                 (eq_cong (Vec n Bool) (bvAdd n len1 len2) len3 pf
                          (sort 0) (\ (l:Vec n Bool) -> BVVec n l a))
                 (appendBVVec n len1 len2 a v1 v2)))
    (bvEqWithProof n (bvAdd n len1 len2) len3);


--------------------------------------------------------------------------------
-- SMT Array

primitive Array : sort 0 -> sort 0 -> sort 0;

primitive arrayConstant : (a b : sort 0) -> b -> (Array a b);
primitive arrayLookup : (a b : sort 0) -> (Array a b) -> a -> b;
primitive arrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
primitive arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Array (Vec n Bool) a;
primitive arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> a -> Vec n Bool -> Array (Vec n Bool) a;
primitive arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Bool;
primitive arrayEq     : (a b : sort 0) -> (Array a b) -> (Array a b) -> Bool;

--------------------------------------------------------------------------------
-- General axioms

axiom bveq_sameL : (n : Nat)
           -> (x z : Vec n Bool)
           -> Eq Bool
                 (bvEq n x (bvAdd n x z))
                 (bvEq n (bvNat n 0) z);

axiom bveq_sameR : (n : Nat)
           -> (x y : Vec n Bool)
           -> Eq Bool
                 (bvEq n (bvAdd n x y) x)
                 (bvEq n y (bvNat n 0));

axiom bveq_same2 : (n : Nat)
           -> (x y z : Vec n Bool)
           -> Eq Bool
                 (bvEq n (bvAdd n x y) (bvAdd n x z))
                 (bvEq n y z);

axiom bvNat_bvToNat : (n : Nat)
              -> (x : Vec n Bool)
              -> Eq (Vec n Bool)
                    (bvNat n (bvToNat n x))
                    x;

axiom ite_split_cong : (b : Bool) -> (x : Vec 384 Bool) -> (y : Vec 384 Bool)
               -> Eq (Vec 12 (Vec 32 Bool))
                     (split 12 32 Bool (ite (Vec 384 Bool) b x y))
                     (ite (Vec 12 (Vec 32 Bool)) b (split 12 32 Bool x) (split 12 32 Bool y));

axiom ite_join_cong : (b : Bool)
              -> (x : Vec 12 (Vec 32 Bool))
              -> (y : Vec 12 (Vec 32 Bool))
              -> Eq (Vec 384 Bool)
                    (join 12 32 Bool (ite (Vec 12 (Vec 32 Bool)) b x y))
                    (ite (Vec 384 Bool) b (join 12 32 Bool x) (join 12 32 Bool y));

axiom map_map : (a b c : sort 0) -> (f : a -> b) -> (g : b -> c) ->
                 (n : Nat) -> (xs : Vec n a) ->
                 Eq (Vec n c) (map b c g n (map a b f n xs))
                              (map a c (\ (x:a) -> g (f x)) n xs);