[WIP] Work on commutative monoid solver

src/idris/Data/Util.idr

@@ -430,3 +430,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/Context.idr

@@ -5,6 +5,7 @@ import Data.Util
 import Data.AVL
 
 import Nova.Core.Language
+import Nova.Core.Monad
 import Nova.Core.Substitution
 
 ||| Σ = Σ₀ (Δ ⊦ x : A) Σ₁
@@ -93,6 +94,28 @@ lookupLetTypeSignature (sig :< (x, LetTypeEntry ctx rhs)) y = do
       (ctx, i, rhs) <- lookupLetTypeSignature sig y
       Just (subst ctx SubstSignature.Wk, S i, SignatureSubstElim rhs Wk)
 
+namespace VarName
+  public export
+  lookupSignature : Signature -> VarName -> Maybe (Nat, SignatureEntry)
+  lookupSignature [<] y = Nothing
+  lookupSignature (sig :< (x, e)) y =
+    case x == y of
+      True => Just (0, subst e Wk)
+      False => do
+        (idx, e) <- lookupSignature sig y
+        Just (S idx, subst e Wk)
+
+  public export
+  lookupSignatureE : Signature -> VarName -> M (Nat, SignatureEntry)
+  lookupSignatureE sig x =
+    case (lookupSignature sig x) of
+      Nothing => throw "Can't look up \{x} in Σ"
+      Just sig => return sig
+
+  public export
+  lookupSignatureIdxE : Signature -> VarName -> M Nat
+  lookupSignatureIdxE sig x = lookupSignatureE sig x <&> fst
+
 namespace Index
   ||| Looks up a signature entry by index. Weakens the result to be typed in the original signature.
   public export

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

@@ -49,6 +49,23 @@ namespace MMaybe
     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,8 @@ nextOmegaName = M.do
   set (MkUnifySt (S idx))
   return ("?\{show 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)

src/idris/Nova/Surface/Elaboration/Implementation/Elem.idr

@@ -199,9 +199,9 @@ elabElemNuOtherwise sig omega ctx (App r (Hole r0 n Nothing) es) meta ty = M.do
   case (lookup n omega) of
     Just _ => return (Error "Hole already exists: \{n}")
     Nothing => M.do
-      omega <- liftUnifyM $ newElemMeta omega ctx n ty NoSolve
+      omega <- liftUnifyM $ newElemMeta omega ctx n ty (case solveNamedHoles %search of False => NoSolve; True => SolveByUnification)
       let omega = Elem.instantiateByElaboration omega meta (OmegaVarElim n Id)
-      addNamedHole (the Params %search).absFilePath r0 n
+      discard $ forMaybe (the Params %search).absFilePath (\path => addNamedHole path r0 n)
       return (Success omega [])
 elabElemNuOtherwise sig omega ctx (App r (Hole r0 n (Just vars)) es) meta ty = M.do
   case (lookup n omega) of
@@ -210,7 +210,7 @@ elabElemNuOtherwise sig omega ctx (App r (Hole r0 n (Just vars)) es) meta ty = M
       let Just regctxPrefix = pickPrefix (cast ctx) vars
         | Nothing => return (Error "Invalid context prefix")
       let ctxPrefix = cast regctxPrefix
-      omega <- liftUnifyM $ newElemMeta omega ctxPrefix n ty SolveByUnification
+      omega <- liftUnifyM $ newElemMeta omega ctxPrefix n ty (case solveNamedHoles %search of False => NoSolve; True => SolveByUnification)
       let omega = Elem.instantiateByElaboration omega meta (OmegaVarElim n (WkN (length ctx `minus` length regctxPrefix)))
       return (Success omega [])
 elabElemNuOtherwise sig omega ctx (App r (Unfold r0 x) []) meta ty = M.do

src/idris/Nova/Surface/Elaboration/Implementation/Tactic.idr

@@ -425,3 +425,5 @@ Nova.Surface.Elaboration.Interface.elabTactic sig omega (Let r x e) target =  M.
       let err = Stuck omega elabs cons
       return (Left "Stuck elaborating RHS of let;\n \{renderDocNoAnn !(liftM $ pretty sig err)}")
     Error {} => return (Left "Error elaborating RHS of let")
+Nova.Surface.Elaboration.Interface.elabTactic sig omega (NormaliseCommutativeMonoid {}) _ = M.do
+  return (Left "Not implemented yet")

src/idris/Nova/Surface/Elaboration/Implementation/Tactic/NormaliseCommutativeMonoid.idr

@@ -0,0 +1,128 @@
+module Nova.Surface.Elaboration.Implementation.Tactic.NormaliseCommutativeMonoid
+
+import Data.AVL
+import Data.Fin
+import Data.List1
+import Data.Location
+import Data.SnocList
+import Data.Util
+
+import Nova.Core.Context
+import Nova.Core.Conversion
+import Nova.Core.Evaluation
+import Nova.Core.Language
+import Nova.Core.Monad
+import Nova.Core.Substitution
+import Nova.Core.Unification
+import Nova.Core.Util
+
+import Nova.Surface.Language
+import Nova.Surface.Elaboration.Interface
+
+import Solver.CommutativeMonoid
+
+||| TODO: Think about how to preserve naming
+public export
+interpContext : Nat -> Context
+interpContext Z = [<]
+interpContext (S k) = interpContext k :< ("_", NatTy)
+
+||| For every Γ ctx
+||| We get x̄
+||| and |x̄| : Γ ⇒ ⟦x̄⟧
+public export
+Vars : Signature -> Omega -> Context -> M (Nat, SubstContext)
+Vars sig omega [<] = return (0, Terminal)
+Vars sig omega (gamma :< (_, ty)) = M.do
+  (n, subst) <- Vars sig omega gamma
+  NatTy <- openEval sig omega ty
+    | _ => M.do
+    return (n, Chain subst Wk)
+
+  return (S n, Under subst)
+
+public export
+interpTerm : Signature -> Term (Fin n) -> M Elem
+interpTerm sig (Var x) = return $ ContextVarElim (finToNat x)
+interpTerm sig Zero = return NatVal0
+interpTerm sig (Plus a b) = M.do
+  idx <- lookupSignatureIdxE sig "_+_"
+  a <- interpTerm sig a
+  b <- interpTerm sig b
+  -- ((_+_ : ℕ → ℕ → ℕ) a : ℕ → ℕ) b
+  return $
+    PiElim (PiElim (SignatureVarElim idx Terminal) "_" NatTy (funTy NatTy NatTy) a)
+      "_"
+      NatTy
+      NatTy
+      b
+
+
+||| Assumes Σ Ω Γ ⊦ t : ℕ
+||| And t is head-neutral w.r.t. evaluation
+||| Parses a term of the form:
+||| t ::= 0 | t + t | x
+-- Is it possible to generalise this to arbitrary comm monoid?
+public export
+parseNatCommutativeMonoidNu : (plusIndex : Nat) -> (Nat -> Maybe (Fin n)) -> Elem -> M (Maybe (Term (Either Nat (Fin n))))
+parseNatCommutativeMonoidNu plusIndex f NatVal0 = MMaybe.do
+  return Zero
+parseNatCommutativeMonoidNu plusIndex f (ContextVarElim k) = MMaybe.do
+  let Just k = f k
+    | Nothing => assert_total $ idris_crash "parseNatCommutativeMonoidNu"
+  return (Var (Right k))
+parseNatCommutativeMonoidNu plusIndex f (PiElim (PiElim (SignatureVarElim i _) _ _ _ a) _ _ _ b) = MMaybe.do
+  guard (i == plusIndex)
+  a <- parseNatCommutativeMonoidNu plusIndex f a
+  b <- parseNatCommutativeMonoidNu plusIndex f b
+  return (Plus a b)
+parseNatCommutativeMonoidNu plusIndex f el = MMaybe.do
+  nothing
+
+-- ||| x̄ ⊦ m ∈ FreeCommMonoid
+-- ||| σ : x̄ ⇒ Γ
+-- ||| -----------------------
+-- ||| Γ ⊦ ⟦m | σ⟧ : M
+-- ||| Γ ⊦ ⟦x | σ⟧ = σ(x) : M
+-- ||| Γ ⊦ ⟦a + b | σ⟧ = ⟦a | σ⟧ + [b | σ⟧ : M
+-- ||| Γ ⊦ ⟦0 | σ⟧ = Z : M
+--
+-- ||| For common Σ Ω:
+-- ||| Γ ⊦ E type
+-- ||| Γ ⊦ e : E
+-- ||| ε ⊦ t ∈ SurfaceTerm
+-- ||| ---------------------
+-- ||| ε ⊦ A : 𝕌
+-- ||| ε ⊦ z : A
+-- ||| ε ⊦ _+_ : A → A → A
+-- ||| ε ⊦ t' = (A, z, _+_, ?) : Comm-Monoid
+-- ||| ε ⊦ E = A type
+-- ||| x̄
+-- ||| σ : x̄ ⇒ Γ
+-- ||| x̄ ⊦ m ∈ CommMonoid
+-- ||| Γ ⊦ e = ⟦m | σ⟧ : A
+public export
+elab0 : Params => Signature -> Omega -> Context -> OpFreeTerm -> Typ -> Elem -> ElabM Elem
+elab0 sig omega gamma monoidInstTerm ty tm = M.do
+  commMonoidTy <- Elab.liftM $
+    lookupSignatureIdxE sig "Comm-Monoid" `M.(<&>)` (\idx => Typ.SignatureVarElim idx Terminal)
+  (omega, tidx) <- liftUnifyM $ newElemMeta omega [<] commMonoidTy SolveByElaboration
+  let prob = ElemElaboration [<] monoidInstTerm tidx commMonoidTy
+  case !(Elaboration.Interface.solve sig omega [prob]) of
+    Success omega => M.do
+     (omega, tyidx) <- liftUnifyM $ newElemMeta omega [<] UniverseTy SolveByUnification
+     (omega, zidx) <- liftUnifyM $ newElemMeta omega [<] (El (Elem.OmegaVarElim tyidx Terminal)) SolveByUnification
+     (omega, pidx) <- liftUnifyM $ newElemMeta omega [<]
+            (funTyN1 $
+              asList1 [ El (Elem.OmegaVarElim tyidx Terminal)
+                      , El (Elem.OmegaVarElim tyidx Terminal)
+                      , El (Elem.OmegaVarElim tyidx Terminal)
+                      ]
+            ) SolveByUnification
+     (omega, holeIdx) <- liftUnifyM $ newElemMeta omega [<] ?holeTy SolveByUnification
+     -- ε ⊦ ⟦A, z, _+_, ?⟧ ⇝ _ : Comm-Monoid
+     -- ⟦A, z, _+_, ?⟧ = π 𝕌 (A. Is-Commut-Monoid A) A ⟦z, _+_, ?⟧
+     -- = π 𝕌 (A. Is-Commut-Monoid A) A (π (El A) )
+     ?af
+    _ => throw "Couldn't check the commutative monoid instance"
+

src/idris/Nova/Surface/Elaboration/Implementation/Typ.idr

@@ -161,7 +161,7 @@ Nova.Surface.Elaboration.Interface.elabType sig omega ctx (App r (Hole r0 n Noth
     Nothing => M.do
       omega <- liftUnifyM $ newTypeMeta omega ctx n NoSolve
       let omega = Typ.instantiateByElaboration omega meta (OmegaVarElim n Id)
-      addNamedHole (the Params %search).absFilePath r0 n
+      discard $ forMaybe (the Params %search).absFilePath (\path => addNamedHole path r0 n)
       return (Success omega [])
 Nova.Surface.Elaboration.Interface.elabType sig omega ctx (App r (Hole r0 n (Just vars)) es) meta =
   case (lookup n omega) of

src/idris/Nova/Surface/Elaboration/Interface.idr

@@ -13,8 +13,8 @@ import Nova.Surface.Language
 import Nova.Surface.Operator
 import Nova.Surface.SemanticToken
 
-CoreTyp = Nova.Core.Language.D.Typ
-CoreElem = Nova.Core.Language.E.Elem
+CoreTyp = Nova.Core.Language.Typ.Typ
+CoreElem = Nova.Core.Language.Elem.Elem
 SurfaceTerm = Nova.Surface.Language.OpFreeTerm.OpFreeTerm
 
 public export
@@ -29,8 +29,11 @@ public export
 record Params where
   [noHints] -- Make sure the machine won't try to synthesise an arbitrary element of that type when we %search
   constructor MkParams
-  ||| Absolute path to a file we are currently elaborating.
-  absFilePath : String
+  ||| Just the absolute path to the file we are currently elaborating.
+  ||| Or nothing in case we are in interactive mode.
+  absFilePath : Maybe String
+  ||| Whether to solve named holes by unification (True) or not solve them at all (False).
+  solveNamedHoles : Bool
 
 public export
 initialElabSt : ElabSt

src/idris/Nova/Surface/Language.idr

@@ -1,13 +1,16 @@
 module Nova.Surface.Language
 
-import Data.Location
-import Data.List1
 import Data.AlternatingList
 import Data.AlternatingList1
+import Data.Fin
+import Data.List1
+import Data.Location
 
 import Nova.Core.Name
 import Nova.Surface.Operator
 
+import Solver.CommutativeMonoid.Language
+
 
 -- h ::= tt | Z | Refl | x | S | ℕ-elim | 𝟘-elim | J | 𝟘 | 𝟙 | ℕ | 𝕌 | !x | ?x | Π-β | Π-η | Π⁼ | Σ-β₁ | Σ-β₂ | Σ-η | Σ⁼ | 𝟙⁼ | ℕ-β-Z | ℕ-β-S | (e{≥0}) | _ | ☐
 
@@ -129,6 +132,12 @@ mutual
       Rewrite : Range -> Term -> Term -> Tactic
       ||| let x ≔ e{≥0}
       Let : Range -> VarName -> Term -> Tactic
+      ||| normalise-comm-monoid ρ ω t
+      NormaliseCommutativeMonoid : Range
+                                -> Term
+                                -> (vars : SnocList String ** Term (Fin (length vars)))
+                                -> Term
+                                -> Tactic
 
   namespace OpFreeTactic
     public export
@@ -154,6 +163,12 @@ mutual
       Rewrite : Range -> OpFreeTerm -> OpFreeTerm -> OpFreeTactic
       ||| let x ≔ t
       Let : Range -> VarName -> OpFreeTerm -> OpFreeTactic
+      ||| normalise-comm-monoid ρ ω t
+      NormaliseCommutativeMonoid : Range
+                                -> OpFreeTerm
+                                -> (vars : SnocList String ** Term (Fin (length vars)))
+                                -> OpFreeTerm
+                                -> OpFreeTactic
 
   namespace OpFreeTerm
     public export