Commutative Monoid Solver (#30)

* [WIP] Work on commutative monoid solver

* Fix shunting

* Factor out term lens and more

* Fix a parser bug

* Commut monoid normalisation tactic mostly done

* Commut monoid solver done

* Eliminate dead code

nova-api.ipkg

@@ -3,7 +3,9 @@ package nova-api
 depends = contrib, just-a-monad
 
 modules =
-          Data.AVL
+          Control.Monad.IOEither
+
+        , Data.AVL
         , Data.AlternatingList
         , Data.AlternatingList1
         , Data.AlternatingSnocList
@@ -25,18 +27,22 @@ modules =
         , Nova.Core.Shrinking
         , Nova.Core.Substitution
         , Nova.Core.Unification
+        , Nova.Core.Util
 
         , Nova.Surface.Elaboration
         , Nova.Surface.Elaboration.Implementation
         , Nova.Surface.Elaboration.Implementation.Common
         , Nova.Surface.Elaboration.Implementation.Elem
         , Nova.Surface.Elaboration.Implementation.Solve
         , Nova.Surface.Elaboration.Implementation.Tactic
+        , Nova.Surface.Elaboration.Implementation.Tactic.NormaliseCommutativeMonoid
+        , Nova.Surface.Elaboration.Implementation.Tactic.TermLens
         , Nova.Surface.Elaboration.Implementation.Tactic.Trivial
         , Nova.Surface.Elaboration.Implementation.Tactic.Unfold
         , Nova.Surface.Elaboration.Implementation.TopLevel
         , Nova.Surface.Elaboration.Implementation.Typ
         , Nova.Surface.Elaboration.Interface
+        , Nova.Surface.Elaboration.Pretty
         , Nova.Surface.Language
         , Nova.Surface.ModuleSystem
         , Nova.Surface.Operator
@@ -46,12 +52,19 @@ modules =
         , Nova.Surface.SemanticToken
         , Nova.Surface.Shunting
 
-        , Nova.Test.Test
+        , Solver.CommutativeMonoid
+        , Solver.CommutativeMonoid.Evaluation
+        , Solver.CommutativeMonoid.Language
+        , Solver.CommutativeMonoid.Normalisation
+        , Solver.CommutativeMonoid.Parser
+        , Solver.CommutativeMonoid.Quotation
+        , Solver.CommutativeMonoid.Value
 
         , Text.Lexing.Token
         , Text.Lexing.Tokeniser
 
         , Text.Parsing.CharUtil
         , Text.Parsing.Fork
+        , Text.Parsing.TokenUtil
 
 sourcedir = "src/idris"

src/idris/Control/Monad/IOEither.idr

@@ -0,0 +1,12 @@
+module Control.Monad.IOEither
+
+public export
+(>>=) : IO (Either e a) -> (a -> IO (Either e b)) -> IO (Either e b)
+(f >>= g) = Prelude.do
+  case !f of
+    Left e => io_pure (Left e)
+    Right x => g x
+
+public export
+pure : a -> IO (Either e a)
+pure x = io_pure (Right x)

src/idris/Data/Util.idr

@@ -145,23 +145,29 @@ reflow : String -> Doc ann
 reflow = fillSep . words
 
 namespace SnocList
--- TODO PR to Idris2
--- TODO: Ordering doesn't make sense: we should order elements right-to-left in a SnocList.
--- NOTE: Or does it? I think Ohad has actually set up the Prelude's SnocList operations to
--- NOTE: act left-to-right ??
-public export
-quicksortBy : (a -> a -> Bool) -> SnocList a -> SnocList a
-quicksortBy o [<] = [<]
-quicksortBy o (xs :< x) =
- let smaller  = filter (not . o x) xs
-     bigger   = filter       (o x) xs
-     left     = quicksortBy o smaller
-     right    = quicksortBy o bigger in
-     left :< x ++ right
+  -- TODO PR to Idris2
+  -- TODO: Ordering doesn't make sense: we should order elements right-to-left in a SnocList.
+  -- NOTE: Or does it? I think Ohad has actually set up the Prelude's SnocList operations to
+  -- NOTE: act left-to-right ??
+  public export
+  quicksortBy : (a -> a -> Bool) -> SnocList a -> SnocList a
+  quicksortBy o [<] = [<]
+  quicksortBy o (xs :< x) =
+   let smaller  = filter (not . o x) xs
+       bigger   = filter       (o x) xs
+       left     = quicksortBy o smaller
+       right    = quicksortBy o bigger in
+       left :< x ++ right
 
-public export
-quicksort : Ord a => SnocList a -> SnocList a
-quicksort xs = quicksortBy (<) xs
+  public export
+  quicksort : Ord a => SnocList a -> SnocList a
+  quicksort xs = quicksortBy (<) xs
+
+  public export
+  index : (xs : SnocList a) -> Fin (length xs) -> a
+  index [<] _ impossible
+  index (xs :< x) FZ = x
+  index (xs :< x) (FS k) = index xs k
 
 namespace List
   public export
@@ -430,3 +436,8 @@ toSnocList1Acc rest (x ::: y :: zs) = toSnocList1Acc (rest :< x) (y ::: zs)
 public export
 toSnocList1 : List1 a -> (SnocList a, a)
 toSnocList1 list = toSnocList1Acc [<] list
+
+public export
+asList1 : (xxs : List a) -> (fromList xxs === Just (x ::: xs)) => List1 a
+asList1 [] @{prf} = absurd prf
+asList1 (x :: xs) = x ::: xs

src/idris/Nova/Core/Evaluation.idr

@@ -372,7 +372,7 @@ mutual
       case (lookup k omega) of
         Just (LetType _ rhs) => openEval sig omega (ContextSubstElim rhs sigma)
         Just (MetaType {}) => return (OmegaVarElim k sigma)
-        Just (LetElem {}) => throw "openEval/Type(OmegaVarElim(LetElem))"
+        Just (LetElem {}) => throw "openEval/Type(OmegaVarElim(LetElem(\{k})))"
         Just (MetaElem {}) => throw "openEval/Type(OmegaVarElim(MetaElem))"
         Just (TypeConstraint {}) => throw "openEval/Type(OmegaVarElim(TypeConstraint))"
         Just (ElemConstraint {}) => throw "openEval/Type(OmegaVarElim(ElemConstraint))"

src/idris/Nova/Core/Language.idr

@@ -62,7 +62,7 @@ mutual
       ||| ext(σ, A, t)
       Ext : SubstContext -> Elem -> SubstContextNF
 
-  namespace D
+  namespace Typ
     public export
     data Typ : Type where
       ||| 𝟘
@@ -94,7 +94,7 @@ mutual
       ||| Xᵢ(σ)
       SignatureVarElim : Nat -> SubstContext -> Typ
 
-  namespace E
+  namespace Elem
     public export
     data Elem : Type where
       ||| (x : A) → B

src/idris/Nova/Core/Monad.idr

@@ -43,12 +43,34 @@ namespace MMaybe
   nothing : M e s (Maybe a)
   nothing = M.return Nothing
 
+  public export
+  fromMaybe : Maybe a -> M e s (Maybe a)
+  fromMaybe x = M.do
+    return x
+
   public export
   liftM : M e s a -> M e s (Maybe a)
   liftM f = M.do
     x <- f
     return (Just x)
 
+  public export
+  guard : Bool -> M e s (Maybe ())
+  guard False = M.do return Nothing
+  guard True = M.do return (Just ())
+
+  public export
+  mapResult : (a -> b) -> M e s (Maybe a) -> M e s (Maybe b)
+  mapResult f t = M.mapResult (map f) t
+
+  public export
+  (<$>) : (a -> b) -> M e s (Maybe a) -> M e s (Maybe b)
+  (<$>) = MMaybe.mapResult
+
+  public export
+  (<&>) : M e s (Maybe a) -> (a -> b) -> M e s (Maybe b)
+  (<&>) = flip MMaybe.mapResult
+
 namespace MEither
   %inline
   public export

src/idris/Nova/Core/Unification.idr

@@ -41,23 +41,23 @@ UnifyM : Type -> Type
   --                  vvvvvv for critical errors only
 UnifyM = JustAMonad.M String UnifySt
 
-public export
-liftM : M a -> UnifyM a
-liftM f = M.do
-  st <- get
-  mapState (const st) (const ()) f
+namespace UnifyM
+  public export
+  liftM : M a -> UnifyM a
+  liftM f = M.do
+    st <- get
+    mapState (const st) (const ()) f
 
-public export
-liftMMaybe : String -> M (Maybe a) -> UnifyM a
-liftMMaybe err f = M.do
- case !(liftM f) of
-   Just x => return x
-   Nothing => throw err
+  namespace Maybe
+    public export
+    liftM : M a -> UnifyM (Maybe a)
+    liftM f = M.do
+      UnifyM.liftM f <&> Just
 
 public export
 liftMEither : M (Either String a) -> UnifyM a
 liftMEither f = M.do
- case !(liftM f) of
+ case !(UnifyM.liftM f) of
    Right x => return x
    Left err => throw err
 
@@ -68,6 +68,15 @@ nextOmegaName = M.do
   set (MkUnifySt (S idx))
   return ("?\{show idx}")
 
+public export
+nextOmegaIdx : UnifyM Nat
+nextOmegaIdx = M.do
+  MkUnifySt idx <- get
+  set (MkUnifySt (S idx))
+  return idx
+
+%hide UnifyM.Maybe.liftM
+
 namespace Result
   ||| Unification step result while solving a constraint.
   public export

src/idris/Nova/Core/Util.idr

@@ -0,0 +1,18 @@
+module Nova.Core.Util
+
+import Data.List1
+
+import Nova.Core.Language
+
+public export
+funTy : Typ -> Typ -> Typ
+funTy a b = PiTy "_" a (ContextSubstElim b Wk)
+
+public export
+funTyN1 : List1 Typ -> Typ
+funTyN1 (t ::: []) = t
+funTyN1 (t ::: o :: os) = funTy t (funTyN1 (o ::: os))
+
+public export
+prodTy : Typ -> Typ -> Typ
+prodTy a b = SigmaTy "_" a (ContextSubstElim b Wk)