From 37cd9a179ca8986827dd1ca0a0043e48a108012d Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 8 Apr 2021 18:46:21 -0400 Subject: [PATCH] remove appendString, move Sigma, List, W64List --- .../generated/CryptolToCoq/SAWCorePrelude.v | 106 ++++---- saw-core/prelude/Prelude.sawcore | 249 +++++++++--------- 2 files changed, 175 insertions(+), 180 deletions(-) diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v index d306d938..24e3ed90 100644 --- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v +++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v @@ -43,8 +43,6 @@ Definition uncurry : forall (a : Type), forall (b : Type), forall (c : Type), fo (* Prelude.error was skipped *) -(* Prelude.appendString was skipped *) - (* Prelude.EmptyType was skipped *) (* Prelude.EmptyType__rec was skipped *) @@ -814,6 +812,58 @@ Definition updBvFun : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), ( (* Prelude.mkDouble was skipped *) +(* Prelude.Sigma was skipped *) + +(* Prelude.Sigma__rec was skipped *) + +(* Prelude.Sigma_proj1 was skipped *) + +(* Prelude.Sigma_proj2 was skipped *) + +Definition uncurrySigma : forall (a : Type), forall (b : a -> Type), forall (c : Type), (forall (pa : a), b pa -> c) -> @sigT a b -> c := + fun (a : Type) (b : a -> Type) (c : Type) => @sigT_rect a b (fun (_1 : @sigT a b) => c). + +(* Prelude.List was skipped *) + +Definition List_def : forall (a : Type), Type := + fun (a : Type) => @Datatypes.list a. + +(* Prelude.List__rec was skipped *) + +Definition unfoldList : forall (a : Type), @Datatypes.list a -> @Either unit (prod a (prod (@Datatypes.list a) unit)) := + fun (a : Type) (l : @Datatypes.list a) => @Datatypes.list_rect a (fun (_1 : @Datatypes.list a) => @Either unit (prod a (prod (@Datatypes.list a) unit))) (@Left unit (prod a (prod (@Datatypes.list a) unit)) tt) (fun (x : a) (l1 : @Datatypes.list a) (_1 : @Either unit (prod a (prod (@Datatypes.list a) unit))) => @Right unit (prod a (prod (@Datatypes.list a) unit)) (pair x (pair l1 tt))) l. + +Definition foldList : forall (a : Type), @Either unit (prod a (prod (@Datatypes.list a) unit)) -> @Datatypes.list a := + fun (a : Type) => @either unit (prod a (prod (@Datatypes.list a) unit)) (@Datatypes.list a) (fun (_1 : unit) => @Datatypes.nil a) (fun (tup : prod a (prod (@Datatypes.list a) unit)) => @Datatypes.cons a (SAWCoreScaffolding.fst tup) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd tup))). + +Inductive ListSort : Type := +| LS_Nil : @ListSort +| LS_Cons : Type -> @ListSort -> @ListSort +. + +Definition ListSort__rec : forall (P : @ListSort -> Type), P (@LS_Nil) -> (forall (A : Type), forall (l : @ListSort), P l -> P (@LS_Cons A l)) -> forall (l : @ListSort), P l := + fun (P : @ListSort -> Type) (f1 : P (@LS_Nil)) (f2 : forall (A : Type), forall (l : @ListSort), P l -> P (@LS_Cons A l)) (l : @ListSort) => SAWCorePrelude.ListSort_rect P f1 f2 l. + +Definition listSortGet : @ListSort -> @SAWCoreScaffolding.Nat -> Type := + @ListSort__rec (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)). + +Definition listSortDrop : @ListSort -> @SAWCoreScaffolding.Nat -> @ListSort := + @ListSort__rec (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> @ListSort) (fun (_1 : @SAWCoreScaffolding.Nat) => @LS_Nil) (fun (_1 : Type) (Ds : @ListSort) (rec : @SAWCoreScaffolding.Nat -> @ListSort) => @Nat_cases (@ListSort) Ds (fun (n : @SAWCoreScaffolding.Nat) (_2 : @ListSort) => rec n)). + +Inductive W64List : Type := +| W64Nil : @W64List +| W64Cons : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) -> @W64List -> @W64List +. + +Definition unfoldedW64List : Type := + @Either unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)). + +Definition unfoldW64List : @W64List -> unfoldedW64List := + fun (l : @W64List) => SAWCorePrelude.W64List_rect (fun (_1 : @W64List) => unfoldedW64List) (@Left unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) tt) (fun (bv : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (l' : @W64List) (_1 : @Either unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit))) => @Right unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_2 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) (pair (@existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_2 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) bv tt) (pair l' tt))) l. + +Definition foldW64List : unfoldedW64List -> @W64List := + @either unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) (@W64List) (fun (_1 : unit) => @W64Nil) (fun (bv_l : prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) => @W64Cons (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) (SAWCoreScaffolding.fst bv_l)) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd bv_l))). + Axiom bvEqWithProof : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @Maybe (@SAWCoreScaffolding.Eq (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) v1 v2) . Definition bvultWithProof : forall (n : @SAWCoreScaffolding.Nat), forall (v1 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (v2 : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @Maybe (@SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n v1 v2) (@SAWCoreScaffolding.true)) := @@ -888,58 +938,6 @@ Definition sliceBVVec : forall (n : @SAWCoreScaffolding.Nat), forall (len : @SAW Definition updSliceBVVec : forall (n : @SAWCoreScaffolding.Nat), forall (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (a : Type), @BVVec n len a -> forall (start' : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), forall (len' : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)), @BVVec n len' a -> @BVVec n len a := fun (n : @SAWCoreScaffolding.Nat) (len : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (a : Type) (v : @BVVec n len a) (start' : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (len' : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (v_sub : @BVVec n len' a) => @genBVVec n len a (fun (i : @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) (pf : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n i len) (@SAWCoreScaffolding.true)) => if @SAWCoreVectorsAsCoqVectors.bvule n start' i then @maybe (@is_bvult n (@SAWCoreVectorsAsCoqVectors.bvSub n i start') len') a (@atBVVec n len a v i pf) (fun (pf_sub : @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreVectorsAsCoqVectors.bvult n (@SAWCoreVectorsAsCoqVectors.bvSub n i start') len') (@SAWCoreScaffolding.true)) => @atBVVec n len' a v_sub (@SAWCoreVectorsAsCoqVectors.bvSub n i start') pf_sub) (@bvultWithProof n (@SAWCoreVectorsAsCoqVectors.bvSub n i start') len') else @atBVVec n len a v i pf). -(* Prelude.Sigma was skipped *) - -(* Prelude.Sigma__rec was skipped *) - -(* Prelude.Sigma_proj1 was skipped *) - -(* Prelude.Sigma_proj2 was skipped *) - -Definition uncurrySigma : forall (a : Type), forall (b : a -> Type), forall (c : Type), (forall (pa : a), b pa -> c) -> @sigT a b -> c := - fun (a : Type) (b : a -> Type) (c : Type) => @sigT_rect a b (fun (_1 : @sigT a b) => c). - -(* Prelude.List was skipped *) - -Definition List_def : forall (a : Type), Type := - fun (a : Type) => @Datatypes.list a. - -(* Prelude.List__rec was skipped *) - -Definition unfoldList : forall (a : Type), @Datatypes.list a -> @Either unit (prod a (prod (@Datatypes.list a) unit)) := - fun (a : Type) (l : @Datatypes.list a) => @Datatypes.list_rect a (fun (_1 : @Datatypes.list a) => @Either unit (prod a (prod (@Datatypes.list a) unit))) (@Left unit (prod a (prod (@Datatypes.list a) unit)) tt) (fun (x : a) (l1 : @Datatypes.list a) (_1 : @Either unit (prod a (prod (@Datatypes.list a) unit))) => @Right unit (prod a (prod (@Datatypes.list a) unit)) (pair x (pair l1 tt))) l. - -Definition foldList : forall (a : Type), @Either unit (prod a (prod (@Datatypes.list a) unit)) -> @Datatypes.list a := - fun (a : Type) => @either unit (prod a (prod (@Datatypes.list a) unit)) (@Datatypes.list a) (fun (_1 : unit) => @Datatypes.nil a) (fun (tup : prod a (prod (@Datatypes.list a) unit)) => @Datatypes.cons a (SAWCoreScaffolding.fst tup) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd tup))). - -Inductive ListSort : Type := -| LS_Nil : @ListSort -| LS_Cons : Type -> @ListSort -> @ListSort -. - -Definition ListSort__rec : forall (P : @ListSort -> Type), P (@LS_Nil) -> (forall (A : Type), forall (l : @ListSort), P l -> P (@LS_Cons A l)) -> forall (l : @ListSort), P l := - fun (P : @ListSort -> Type) (f1 : P (@LS_Nil)) (f2 : forall (A : Type), forall (l : @ListSort), P l -> P (@LS_Cons A l)) (l : @ListSort) => SAWCorePrelude.ListSort_rect P f1 f2 l. - -Definition listSortGet : @ListSort -> @SAWCoreScaffolding.Nat -> Type := - @ListSort__rec (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> Type) (fun (_1 : @SAWCoreScaffolding.Nat) => @SAWCoreScaffolding.Eq (@SAWCoreScaffolding.Bool) (@SAWCoreScaffolding.true) (@SAWCoreScaffolding.false)) (fun (A : Type) (_1 : @ListSort) (rec : @SAWCoreScaffolding.Nat -> Type) => @Nat_cases Type A (fun (n : @SAWCoreScaffolding.Nat) (_2 : Type) => rec n)). - -Definition listSortDrop : @ListSort -> @SAWCoreScaffolding.Nat -> @ListSort := - @ListSort__rec (fun (_1 : @ListSort) => @SAWCoreScaffolding.Nat -> @ListSort) (fun (_1 : @SAWCoreScaffolding.Nat) => @LS_Nil) (fun (_1 : Type) (Ds : @ListSort) (rec : @SAWCoreScaffolding.Nat -> @ListSort) => @Nat_cases (@ListSort) Ds (fun (n : @SAWCoreScaffolding.Nat) (_2 : @ListSort) => rec n)). - -Inductive W64List : Type := -| W64Nil : @W64List -| W64Cons : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool) -> @W64List -> @W64List -. - -Definition unfoldedW64List : Type := - @Either unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)). - -Definition unfoldW64List : @W64List -> unfoldedW64List := - fun (l : @W64List) => SAWCorePrelude.W64List_rect (fun (_1 : @W64List) => unfoldedW64List) (@Left unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) tt) (fun (bv : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (l' : @W64List) (_1 : @Either unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit))) => @Right unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_2 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) (pair (@existT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_2 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) bv tt) (pair l' tt))) l. - -Definition foldW64List : unfoldedW64List -> @W64List := - @either unit (prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) (@W64List) (fun (_1 : unit) => @W64Nil) (fun (bv_l : prod (@sigT (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit)) (prod (@W64List) unit)) => @W64Cons (@projT1 (@SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) (fun (_1 : @SAWCoreVectorsAsCoqVectors.Vec 64 (@SAWCoreScaffolding.Bool)) => unit) (SAWCoreScaffolding.fst bv_l)) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd bv_l))). - Inductive IRTDesc (As : @ListSort) : Type := | IRT_varD : @SAWCoreScaffolding.Nat -> @IRTDesc As | IRT_mu : @IRTDesc As -> @IRTDesc As diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index f181fa74..d9fbad04 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -78,9 +78,6 @@ primitive String : sort 0; primitive error : (a : sort 1) -> String -> a; -primitive appendString : String -> String -> String; - - -------------------------------------------------------------------------------- -- Record types @@ -1404,6 +1401,129 @@ primitive mkDouble : Integer -> Integer -> Float; -- 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; + } + +-- A definition for the List datatype; currently needed as a workaround in Heapster +List_def : (a:sort 0) -> sort 0; +List_def 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).(1)); + +-- 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)); + + +-------------------------------------------------------------------------------- +-- 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 that use proof objects @@ -1600,129 +1720,6 @@ updSliceBVVec n len a v start' len' v_sub = (atBVVec n len a v i pf)); -------------------------------------------------------------------------------- --- 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; - } - --- A definition for the List datatype; currently needed as a workaround in Heapster -List_def : (a:sort 0) -> sort 0; -List_def 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).(1)); - --- 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)); - - --------------------------------------------------------------------------------- --- 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)); - - -------------------------------------------------------------------------------- -- Iso-recursive types