merge: Std lib updates (#1231)

cli-impl/src/test/resources/shared/.gitignore

@@ -1,2 +1,3 @@
 *.tex
-*.html
+*.html
+/.idea

cli-impl/src/test/resources/shared/src/arith/nat/base.aya

@@ -1,4 +1,5 @@
 open import relation::binary::path
+open import arith::bool
 
 open inductive Nat | zero | suc Nat
 
@@ -11,6 +12,11 @@ overlap def infixl + Nat Nat : Nat
 | a, suc b => suc (a + b)
 tighter =
 
+def subTrunc (x y : Nat) : Nat
+| n, 0 => n
+| 0, suc _ => 0
+| suc n, suc m => subTrunc n m
+
 overlap def +-comm : a + b = b + a elim a b
 | 0, _ => refl
 | suc _, _ => pmap suc +-comm
@@ -30,3 +36,10 @@ overlap def infixl * Nat Nat : Nat
 | m, 0 => 0
 | suc m, n => n + m * n
 tighter +
+
+overlap def infix =? Nat Nat : Bool
+| zero, zero => true
+| zero, suc _ => false
+| suc _, zero => false
+| suc a, suc b => a =? b
+looser + *

cli-impl/src/test/resources/shared/src/data/list/base.aya

@@ -1,5 +1,6 @@
 open import arith::nat::base
 open import relation::binary::path
+open import data::maybe using (Maybe, just, nothing)
 
 open inductive List (A : Type)
 | nil
@@ -26,3 +27,23 @@ def rev' (buf xs : List A) : List A elim xs
 | x :< xs' => rev' (x :< buf) xs'
 
 def rev (xs : List A) : List A => rev' [ ] xs
+
+@suppress(Shadowing)
+def take (n : Nat) (xs : List A) : List A
+| _, [ ] => [ ]
+| 0, _ :< _ =>  [ ]
+| suc n, x :< xs => x :< (take n xs)
+
+@suppress(Shadowing)
+def drop (n : Nat) (xs : List A) : List A
+| 0, _ => xs
+| suc n, [ ] => [ ]
+| suc n, x :< xs => drop n xs
+
+def infixl !! (List A) Nat : Maybe A
+| [ ], _ => nothing
+| x :< _, 0 => just x
+| _ :< xs, suc n => xs !! n
+tighter =
+
+def insert (n : Nat) (x : A) (xs : List A) : List A => take n xs ++ [ x ] ++ drop n xs

cli-impl/src/test/resources/shared/src/data/list/properties.aya

@@ -37,18 +37,18 @@ private def rev'-++ (buf xs : List A) : rev' buf xs = rev xs ++ buf elim xs
 | [ ] => refl
 | x :< xs =>
   let
-  | step0 /*: rev' buf (x :< xs) = rev xs ++ (x :< buf)*/ := rev'-++ (x :< buf) xs
-  | step1 /*: rev' [ x ] xs ++ buf = (rev xs ++ [ x ]) ++ buf*/ := pmap (++ buf) (rev'-++ [ x ] xs)
-  | step2 : (rev xs ++ [ x ]) ++ buf = /* rev xs ++ ([ x ] ++ buf) = */ rev xs ++ (x :< buf) := ++-assoc (rev xs) [ x ] buf
+  | step0 := rev'-++ (x :< buf) xs
+  | step1 := pmap (++ buf) (rev'-++ [ x ] xs)
+  | step2 : (rev xs ++ [ x ]) ++ buf = rev xs ++ (x :< buf) := ++-assoc (rev xs) [ x ] buf
   in step0 <=> pinv step2 <=> pinv step1
 
 @suppress(Shadowing)
 def rev-distrib-++ (xs ys : List A) : rev (xs ++ ys) = (rev ys ++ rev xs) elim xs
 | [ ] => refl
 | x :< xs =>
   let
-  | step0 : /* rev (x :< (xs ++ ys)) = */ rev' [ x ] (xs ++ ys) = rev (xs ++ ys) ++ [ x ] := rev'-++ _ _
+  | step0 : rev' [ x ] (xs ++ ys) = rev (xs ++ ys) ++ [ x ] := rev'-++ _ _
   | step1 : rev (xs ++ ys) ++ [ x ] = (rev ys ++ rev xs) ++ [ x ] := pmap (++ [ x ]) (rev-distrib-++ _ _)
   | step2 : (rev ys ++ rev xs) ++ [ x ] = rev ys ++ (rev xs ++ [ x ]) := ++-assoc _ _ _
-  | step3 : /* rev ys ++ rev (x :< xs) = */ rev ys ++ rev' [ x ] xs = rev ys ++ (rev xs ++ [ x ]) := pmap (rev ys ++) (rev'-++ _ _)
+  | step3 : rev ys ++ rev' [ x ] xs = rev ys ++ (rev xs ++ [ x ]) := pmap (rev ys ++) (rev'-++ _ _)
   in step0 <=> step1 <=> step2 <=> pinv step3

cli-impl/src/test/resources/shared/src/data/maybe.aya

@@ -0,0 +1,14 @@
+open inductive Maybe (A : Type)
+| just A | nothing
+
+variable A B : Type
+
+def map (f : A -> B) (m : Maybe A) : Maybe B elim m
+| just a => just (f a)
+| nothing => nothing
+
+def join (mm : Maybe (Maybe A)) : Maybe A
+| just (just a) => just a
+| _ => nothing
+
+def infixl >>= (f : A -> Maybe B) (m : Maybe A) : Maybe B => join (map f m)