Move Syntax.PreorderReasoning into base (#2368)

libs/base/Syntax/PreorderReasoning.idr

@@ -4,7 +4,7 @@ module Syntax.PreorderReasoning
 
 infixl 0  ~~
 prefix 1  |~
-infix  1  ...
+infix  1  ...,..<,..>,.=.,.=<,.=>
 
 |||Slightly nicer syntax for justifying equations:
 |||```
@@ -35,3 +35,20 @@ example x =
    ~~ x+1  ...( plusZeroRightNeutral $ x + 1 )
    ~~ 1+x  ...( plusCommutative x 1          )
 -}
+
+-- Re-implement `prelude.Builtins.sym` to enable bootstrapping
+-- Remove after next release
+%inline
+public export
+symHet : (0 rule : x ~=~ y) -> y ~=~ x
+symHet Refl = Refl
+
+-- Smart constructors
+public export
+(..<) : (0 y : a) -> {0 x : b} ->
+    y ~=~ x -> Step x y
+(y ..<(prf)) {x} = (y ...(symHet prf)) -- Use `sym` from next release
+
+public export
+(..>) : (0 y : a) -> (0 step : x ~=~ y) -> Step x y
+(..>) = (...)

libs/base/Syntax/PreorderReasoning/Generic.idr

@@ -5,7 +5,7 @@ import Control.Order
 infixl 0  ~~
 infixl 0  <~
 prefix 1  |~
-infix  1  ...
+infix  1  ...,..<,..>,.=.,.=<,.=>
 
 public export
 data Step : (leq : a -> a -> Type) -> a -> a -> Type where
@@ -28,3 +28,27 @@ public export
          -> FastDerivation leq x y -> {z : dom} -> (step : Step Equal y z)
          -> FastDerivation leq x z
 (~~) der (z ... Refl) = der
+
+-- Smart constructors
+public export
+(..<) : Symmetric a leq => (y : a) -> {x : a} -> y `leq` x -> Step leq x y
+(y ..<(prf)) {x} = (y ...(symmetric prf))
+
+public export
+(..>) : (y : a) -> x `leq` y -> Step leq x y
+(..>) = (...)
+
+public export
+(.=.) : Reflexive a leq  => (y : a) -> {x : a} ->
+    x === y -> Step leq x y
+(y .=.(Refl)) {x = _} = (y ...(reflexive))
+
+public export
+(.=>) : Reflexive a leq  => (y : a) -> {x : a} ->
+    x === y -> Step leq x y
+(.=>) = (.=.)
+
+public export
+(.=<) : Reflexive a leq  => (y : a) -> {x : a} ->
+    y === x -> Step leq x y
+(y .=<(Refl)) = (y ...(reflexive))

libs/base/base.ipkg

@@ -88,6 +88,9 @@ modules = Control.App,
           Language.Reflection.TT,
           Language.Reflection.TTImp,
 
+          Syntax.PreorderReasoning,
+          Syntax.PreorderReasoning.Generic,
+
           System,
           System.Clock,
           System.Concurrency,

libs/contrib/contrib.ipkg

@@ -138,8 +138,6 @@ modules = Control.ANSI,
           Language.JSON.Tokens,
 
           Syntax.WithProof,
-          Syntax.PreorderReasoning,
-          Syntax.PreorderReasoning.Generic,
 
           System.Console.GetOpt,
           System.Directory.Tree,

libs/prelude/Builtin.idr

@@ -167,7 +167,7 @@ replace Refl prf = prf
 ||| Symmetry of propositional equality.
 %inline
 public export
-sym : (0 rule : x = y) -> y = x
+sym : (0 rule : x ~=~ y) -> y ~=~ x
 sym Refl = Refl
 
 ||| Transitivity of propositional equality.

tests/idris2/error018/expected

@@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7
 
 1/1: Building Issue1031-4 (Issue1031-4.idr)
 Error: While processing left hand side of nice. Unsolved holes:
-Main.{dotTm:816} introduced at: 
+Main.{dotTm:820} introduced at: 
 Issue1031-4:4:6--4:10
  1 | %default total
  2 | 

tests/idris2/interpreter008/expected

@@ -1,6 +1,6 @@
 1/1: Building Issue2041 (Issue2041.idr)
 Error: Unsolved holes:
-Main.{n:821} introduced at: 
+Main.{n:825} introduced at: 
 Issue2041:5:17--5:19
  1 | ex : {n : Nat} -> String
  2 | ex {n} = "hello" ++ show n
@@ -9,8 +9,8 @@ Issue2041:5:17--5:19
  5 | main = putStrLn ex
                      ^^
 
-Main> Encountered unimplemented hole Main.{n:821}
-Warning: compiling hole Main.{n:821}
+Main> Encountered unimplemented hole Main.{n:825}
+Warning: compiling hole Main.{n:825}
 Main> Encountered unimplemented hole Main.{n:4}
 Warning: compiling hole Main.{n:4}
 Main>