Patch hoshino branch as a PR

cli-impl/src/test/java/org/aya/test/LibraryTest.java

@@ -66,12 +66,15 @@ public static void main(String... args) throws IOException {
   @Test public void testLiterate() throws IOException {
     FileUtil.deleteRecursively(DIR.resolve("build"));
     // Full rebuild
+    assertEquals(0, compile(makeFlagsForPretty(), DIR));
+  }
+
+  private static @NotNull CompilerFlags makeFlagsForPretty() {
     var prettyInfo = new CompilerFlags.PrettyInfo(
       true, false, false, false, CliEnums.PrettyStage.literate,
-      CliEnums.PrettyFormat.html, new AyaPrettierOptions(), new RenderOptions(), null
+      CliEnums.PrettyFormat.html, AyaPrettierOptions.pretty(), new RenderOptions(), null
     );
-    var flags = new CompilerFlags(CompilerFlags.Message.ASCII, false, false, prettyInfo, ImmutableSeq.empty(), null);
-    assertEquals(0, compile(flags, DIR));
+    return new CompilerFlags(CompilerFlags.Message.ASCII, false, false, prettyInfo, ImmutableSeq.empty(), null);
   }
 
   @Test public void testInMemoryAndPrim() throws IOException {

cli-impl/src/test/resources/negative/ParseError.txt

@@ -88,24 +88,24 @@ Parsing interrupted due to:
 Let's learn from that.
 
 ImplicitTuplePat:
-In file $FILE:2:3 ->
+In file $FILE:2:4 ->
 
   1 │   def test (Sig Type ** Type) : Type
   2 │   | ({a}, b) => a
-    │      ╰─╯
+    │       ╰╯
 
 Error: Implicit pattern is not allowed here.
 
 1 error(s), 0 warning(s).
 Let's learn from that.
 
 ImplicitListPat:
-In file $FILE:4:3 ->
+In file $FILE:4:4 ->
 
   2 │   open import arith::nat::base
   3 │   def test (List Nat) : Nat
   4 │   | [{a}] => a
-    │      ╰─╯
+    │       ╰╯
 
 Error: Implicit elements in a list pattern is disallowed
 

cli-impl/src/test/resources/negative/PatTyckError.txt

@@ -72,24 +72,24 @@ Error: Cannot split on a non-inductive type
 Let's learn from that.
 
 TupleOnNonSigma:
-In file $FILE:2:3 ->
+In file $FILE:2:4 ->
 
   1 │   def test (a' : Type) : Type
   2 │    | (a, b) => a
-    │      ╰────╯
+    │       ╰──╯
   3 │   
 
 Error: The tuple pattern
          (a, b)
        splits only on sigma types, while the actual type is not:
          Type 0
 
-In file $FILE:6:3 ->
+In file $FILE:6:4 ->
 
   4 │   def Alias => Type
   5 │   def test2 (a' : Alias) : Type
   6 │    | (a, b) => a
-    │      ╰────╯
+    │       ╰──╯
 
 Error: The tuple pattern
          (a, b)
@@ -132,12 +132,12 @@ Error: There is no pattern for the parameter
 Let's learn from that.
 
 TooManyPattern:
-In file $FILE:3:11 ->
+In file $FILE:3:12 ->
 
   1 │   open import arith::bool::base
   2 │   def ifElse {A : Type} (b : Bool) A A : A
   3 │   | true, x, {y} => x
-    │              ╰─╯
+    │               ╰╯
 
 Error: There are too many implicit patterns:
          y
@@ -289,11 +289,11 @@ Error: There is no pattern for the parameter
 Let's learn from that.
 
 ImplicitPatWithElim:
-In file $FILE:2:5 ->
+In file $FILE:2:6 ->
 
   1 │   def foo (A : Type) A : A elim A
   2 │   | _, {a} => a
-    │        ╰─╯
+    │         ╰╯
 
 Error: Pattern matching with elim is not compatible with implicit patterns.
 

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

@@ -12,9 +12,9 @@ overlap def infixl + Nat Nat : Nat
 | a, suc b => suc (a + b)
 tighter =
 
-def subTrunc (x y : Nat) : Nat
+overlap def subTrunc (x y : Nat) : Nat
+| 0, _ => 0
 | n, 0 => n
-| 0, suc _ => 0
 | suc n, suc m => subTrunc n m
 
 overlap def +-comm : a + b = b + a elim a b
@@ -36,10 +36,3 @@ 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/arith/nat/properties.aya

@@ -1,5 +1,6 @@
 open import arith::nat::base
 open import relation::nullary::empty
+open import relation::nullary::decidable using (Decidable, yes, no, map as dec_map)
 open import relation::binary::path
 
 private def diag Nat : Type
@@ -14,3 +15,9 @@ private def suc-inj Nat : Nat
 
 def s=s {m n : Nat} (p : suc m = suc n) : m = n => (\i => suc-inj (p i))
 
+overlap def infix =? (a b : Nat) : Decidable (a = b)
+| zero, zero => yes refl
+| zero, suc _ => no (fn p => z≠s p)
+| suc _, zero => no (fn p => z≠s (pinv p))
+| suc a, suc b => dec_map (pmap suc) s=s (a =? b)
+looser + *

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

@@ -29,15 +29,15 @@ def rev' (buf xs : List A) : List A elim xs
 def rev (xs : List A) : List A => rev' [ ] xs
 
 @suppress(Shadowing)
-def take (n : Nat) (xs : List A) : List A
+overlap def take (n : Nat) (xs : List A) : List A
 | _, [ ] => [ ]
-| 0, _ :< _ =>  [ ]
+| 0, _ => [ ]
 | suc n, x :< xs => x :< (take n xs)
 
 @suppress(Shadowing)
-def drop (n : Nat) (xs : List A) : List A
+overlap 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

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

@@ -1,13 +1,22 @@
 open import arith::nat::base
+open import arith::bool using (Bool, true, false)
 open import data::list::base
+open import data::maybe using (just, nothing, nothing≠just)
 open import relation::binary::path
+open import relation::binary::nat_cmp
+open import relation::nullary::empty
+open import relation::nullary::decidable hiding (map)
 
 variable A B C : Type
 
 def length-map (f : A -> B) (l : List A) : length (map f l) = length l elim l
 | [ ] => refl
 | x :< xs => pmap suc (length-map f xs)
 
+def length-++ (xs ys : List A) : length (xs ++ ys) = length xs + length ys elim xs
+| [ ] => refl
+| x :< xs' => pmap suc (length-++ _ _)
+
 def map-comp (g : B -> C) (f : A -> B) (l : List A) : map (\x => g (f x)) l = map g (map f l) elim l
 | [ ] => refl
 | x :< xs => pmap (g (f x) :<) (map-comp g f xs)
@@ -52,3 +61,65 @@ def rev-distrib-++ (xs ys : List A) : rev (xs ++ ys) = (rev ys ++ rev xs) elim x
   | step2 : (rev ys ++ rev xs) ++ [ x ] = rev ys ++ (rev xs ++ [ x ]) := ++-assoc _ _ _
   | step3 : rev ys ++ rev' [ x ] xs = rev ys ++ (rev xs ++ [ x ]) := pmap (rev ys ++) (rev'-++ _ _)
   in step0 <=> step1 <=> step2 <=> pinv step3
+
+def !!→length (i : Nat) (xs : List A) (v : A) (xs !! i = just v) : i < length xs
+| 0, [ ], _, p => exfalso (nothing≠just p)
+| 0, _ :< _, _, p => refl
+| suc i, [ ], _, p => exfalso (nothing≠just p)
+| suc i, x :< xs, _, p => !!→length i xs _ p
+
+def !!>=length (i : Nat) (xs : List A) (length xs <= i) : xs !! i = nothing
+| _, [ ], p => refl
+| 0, _ :< _, p => exfalso (sn<=z p)
+| suc i, x :< xs, p => !!>=length i xs (s<=s p)
+
+def ++-!!-l (i : Nat) (xs ys : List A) (i < length xs) : (xs ++ ys) !! i = xs !! i
+| _, [ ], _, p => exfalso (n<z→⊥ p)
+| 0, x :< xs', _, _ => refl
+| suc i', x :< xs', _, p => ++-!!-l i' xs' ys p
+
+def ++-!!-r (i : Nat) (xs ys : List A) (length xs <= i) : (ys !! (subTrunc i (length xs))) = (xs ++ ys) !! i
+| _, _, [ ], p => pinv (!!>=length i xs p)
+| 0, [ ], y :< ys', _ => refl
+| 0, _ :< _, y :< ys', p => exfalso (sn<=z p)
+| suc i', [ ], y :< ys', _ => refl
+| suc i', _ :< xs', y :< ys', p => ++-!!-r i' xs' (y :< ys') (s<=s p)
+
+def split-lemma (i : Nat) (xs : List A) (i <= length xs) : xs = take i xs ++ drop i xs
+| 0, _, _ => refl
+| suc i, [ ], p => exfalso (sn<=z p)
+| suc i, x :< xs, p => pmap (x :<) (split-lemma i xs (s<=s p))
+
+def take<=length (i : Nat) (xs : List A) (i <= length xs)
+  : length (take i xs) = i
+| 0, _, _ => refl
+| suc i, [ ], p => exfalso (n<z→⊥ p)
+| suc i, x :< xs, p => pmap suc (take<=length _ _ (s<=s p))
+
+def take-!! (i : Nat) (xs : List A) (n : Nat) (i<=xs : i <= length xs) (n<i : n < i)
+  : xs !! n = take i xs !! n => transport
+    (fn l => l !! n = take i xs !! n) (pinv (split-lemma i xs i<=xs))
+    (++-!!-l _ _ _ (transport (fn l => n < l) (pinv (take<=length i xs i<=xs)) n<i))
+
+def drop<=length (i : Nat) (xs : List A)
+  : length (drop i xs) = subTrunc (length xs) i
+| _, [ ] => refl
+| 0, x :< xs => refl
+| suc i, x :< xs => drop<=length i xs
+
+def insert<=length
+  (i : Nat) (x : A) (xs : List A) (p : i <= length xs)
+  : length (insert i x xs) = length xs + 1
+  => match i <=? length xs {
+  | _ because (reflect_true _) => let
+    | myGoal! : length (drop i xs) + length (take i xs) = length xs := transport
+        (fn a => a + length (take i xs) = length xs) (pinv (drop<=length _ _))
+        (transport
+          (fn a => (subTrunc (length xs) i + a = length xs)) (pinv (take<=length _ _ p))
+          (a-b+b=a _ _ p))
+    | BanGDream : length (take i xs) + length (drop i xs) = length xs := transport (fn lhs => lhs = length xs) +-comm myGoal!
+    | haruhikage : suc (length (take i xs) + length (drop i xs)) = suc (length xs) := pmap suc BanGDream
+    | nande : length (take i xs ++ (x :< drop i xs)) = suc (length (take i xs) + length (drop i xs)) := length-++ _ _
+    in nande <=> haruhikage
+  | _ because (reflect_false np<) => exfalso (np< p)
+  }

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

@@ -1,14 +1,2 @@
-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)
+public open import data::maybe::base
+public open import data::maybe::properties

cli-impl/src/test/resources/shared/src/data/maybe/base.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)

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

@@ -0,0 +1,18 @@
+open import data::unit
+open import data::maybe::base
+open import relation::nullary::empty
+open import relation::binary::path
+
+variable A : Type
+
+private def maybe-diag (m : Maybe A) : Type
+| just a => Unit
+| nothing => Empty
+
+def nothing≠just {A : Type} {a : A} (p : nothing = just a) : ⊥ => coe 0 1 (fn i => maybe-diag ((pinv p) i)) tt
+
+private def just-wrap {A : Type} (v : A) (m : Maybe A) : A elim m
+| nothing => v
+| just a => a
+
+def just-inj {A : Type} {a b : A} (p : just a = just b) : a = b => fn i => just-wrap a (p i)

cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya

@@ -0,0 +1,78 @@
+open import arith::nat using (Nat, zero, suc, z≠s, subTrunc, =?, +)
+open import arith::bool using (Bool, true, false)
+open import relation::unary::negation using (neg)
+open import relation::nullary::empty using (⊥, exfalso)
+open import relation::binary::path
+open import relation::nullary::decidable using (Decidable, yes, no, because, reflect_true, reflect_false, map as dec_map)
+open import data::sum using (Sum, inl, inr)
+
+def infix <= (a b : Nat) : Type => subTrunc a b = 0
+
+def infix < (a b : Nat) : Type => (suc a) <= b
+
+def infix >= (a b : Nat) : Type => subTrunc b a = 0
+
+def infix > (a b : Nat) : Type => a >= (suc b)
+
+def n<z→⊥ {n : Nat} (eq : n < 0) : ⊥ => exfalso (z≠s (pinv eq))
+
+def s<s {a b : Nat} (p : suc a < suc b) : a < b => p
+def s<=s {a b : Nat} (p : suc a <= suc b) : a <= b => p
+
+def n<=n (n : Nat) : n <= n
+| 0 => refl
+| suc n => n<=n n
+
+def n<=s {a b : Nat} (p : a <= b) : a <= suc b elim a b
+| zero, _ => refl
+| suc a, zero => exfalso (sn<=z p)
+| suc a, suc b => n<=s p
+
+def infix <=? (a b : Nat) : Decidable (a <= b) => subTrunc a b =? 0
+
+def infix <? (a b : Nat) : Decidable (a < b) => (suc a) <=? b
+
+def n<=z {n : Nat} (p : n <= 0) : n = 0 => p
+def sn<=z {n : Nat} (p : suc n <= 0) : ⊥ => z≠s (pinv (n<=z p))
+
+def <=-trans {a b c : Nat} (p : a <= b) (q : b <= c) : a <= c elim a b c
+| zero, _, _ => refl
+| suc a, zero, _ => exfalso (sn<=z p)
+| suc a, suc b, zero => exfalso (sn<=z q)
+| suc a, suc b, suc c => <=-trans (s<=s p) (s<=s q)
+
+private def some-lemma (a b : Nat) (p : subTrunc a b = 0) (np : neg (subTrunc (suc a) b = 0)) : a = b
+| 0, 0, _, _ => refl
+| 0, suc b, _, _ => exfalso (np p)
+| suc a, 0, p, _ => exfalso (z≠s (pinv p))
+| suc a, suc b, _, _ => pmap suc (some-lemma a b p np)
+
+def <=-case {a b : Nat} (p : a <= b) : Sum (a < b) (a = b) =>
+  match a <? b {
+  | _ because reflect_true p => inl p
+  | _ because reflect_false np => inr (some-lemma _ _ p np)
+  }
+
+def ¬<→>= {a b : Nat} (np : neg (a < b)) : a >= b
+| {_}, {0}, np => refl
+| {0}, {suc b}, np => exfalso (np refl)
+| {suc a}, {suc b}, np => s<=s (¬<→>= {a} {b} (fn p => np p))
+
+def <=-with-≠ {a b : Nat} (p : a <= b) (q : neg (a = b)) : a < b => match <=-case p {
+| inl proof => proof
+| inr eq => exfalso (q eq)
+}
+
+def <→s {a b : Nat} (p : a < b) : Sig (n : Nat) ** b = suc n elim a b
+| _, 0 => exfalso (n<z→⊥ p)
+| _, suc b => (b, refl)
+
+def a-b+b=a (a b : Nat) (p : b <= a) : subTrunc a b + b = a
+| 0, _, _ => n<=z p
+| suc a', 0, _ => refl
+| suc a', suc b', _ => pmap suc (a-b+b=a a' b' (s<=s p))
+
+def suc-sub {a b : Nat} (p : b < (suc a)) : subTrunc (suc a) b = suc (subTrunc a b) elim a b
+| _, zero => refl
+| zero, suc b => exfalso (n<z→⊥ (s<s {b} {0} p))
+| suc a, suc b => suc-sub p