Unfold tactic as a better reduce

nova.ipkg

@@ -35,8 +35,8 @@ modules =
         , Nova.Surface.SemanticToken
         , Nova.Surface.Shunting
 
-        , Nova.Surface.Tactic.Reduce
         , Nova.Surface.Tactic.Trivial
+        , Nova.Surface.Tactic.Unfold
 
         , Nova.Test.Test
 

src/idris/Nova/Surface/Elaboration.idr

@@ -28,7 +28,7 @@ import Nova.Surface.Shunting
 import Nova.Surface.Operator
 import Nova.Surface.SemanticToken
 
-import Nova.Surface.Tactic.Reduce
+import Nova.Surface.Tactic.Unfold
 import Nova.Surface.Tactic.Trivial
 
 CoreTyp = Nova.Core.Language.D.Typ
@@ -1296,13 +1296,13 @@ mutual
     Right (omega, source, restInterp) <- elabTactic sig omega (Composition r (beta ::: gammas)) alphaSource
       | Left err => return (Left err)
     return (Right (omega, source, restInterp . alphaInterp))
-  -- ⟦reduce ρ⟧ : ε (Γ ⊦ B) ⇒ ε (Γ ⊦ A)
-  elabTactic sig omega (Reduce r path) [< (x, ElemEntry ctx ty)] = M.do
-   Right ty' <- Elab.liftM $ applyReduce sig omega ty path
+  -- ⟦unfold ρ⟧ : ε (Γ ⊦ B) ⇒ ε (Γ ⊦ A)
+  elabTactic sig omega (Unfold r path) [< (x, ElemEntry ctx ty)] = M.do
+   Right ty' <- Elab.liftM $ applyUnfold sig omega (map fst ctx) ty path
      | Left r => --FIX: use the range
-                 return (Left "Can't apply 'reduce', range: \{show r}, ρ: \{show path}")
+                 return (Left "Can't apply 'unfold', range: \{show r}, ρ: \{show path}")
    return (Right (omega, [< (x, ElemEntry ctx ty')], id))
-  elabTactic sig omega (Reduce r path) _ = return (Left "Target context is empty or its last entry is a let")
+  elabTactic sig omega (Unfold r path) _ = return (Left "Target context is empty or its last entry is a let")
   elabTactic sig omega (RewriteInv r path prf) [< (x, ElemEntry ctx ty)] = M.do
     case !(applyRewrite sig omega ctx ty path prf False) of
       Left r0 => M.do

src/idris/Nova/Surface/Language.idr

@@ -113,8 +113,8 @@ mutual
       ||| α
       ||| β
       Composition : Range -> List1 Tactic -> Tactic
-      ||| reduce ρ
-      Reduce : Range -> Term -> Tactic
+      ||| unfold ρ
+      Unfold : Range -> Term -> Tactic
       ||| exact t
       Exact : Range -> Term -> Tactic
       ||| * α
@@ -138,8 +138,8 @@ mutual
       ||| α
       ||| β
       Composition : Range -> List1 OpFreeTactic -> OpFreeTactic
-      ||| reduce ρ
-      Reduce : Range -> OpFreeTerm -> OpFreeTactic
+      ||| unfold ρ
+      Unfold : Range -> OpFreeTerm -> OpFreeTactic
       ||| exact t
       Exact : Range -> OpFreeTerm -> OpFreeTactic
       ||| * α

src/idris/Nova/Surface/Parser.idr

@@ -619,11 +619,11 @@ mutual
     sepBy1 spaceDelimDef topLevel
 
 mutual
-  tactic = composition <|> split <|> exact <|> reduce <|> id <|> trivial <|> rewriteInv <|> let' <|> rewrite'
+  tactic = composition <|> split <|> exact <|> unfold <|> id <|> trivial <|> rewriteInv <|> let' <|> rewrite'
 
   public export
   compositionArg : Rule Tactic
-  compositionArg = split <|> exact <|> reduce <|> id <|> trivial <|> rewriteInv <|> let' <|> rewrite'
+  compositionArg = split <|> exact <|> unfold <|> id <|> trivial <|> rewriteInv <|> let' <|> rewrite'
 
   ensureColumn : (col : Int) -> Rule a -> Rule a
   ensureColumn col f = do
@@ -660,12 +660,12 @@ mutual
     pure (Exact (l + r) tm)
 
   public export
-  reduce : Rule Tactic
-  reduce = do
-    l <- delim "reduce"
+  unfold : Rule Tactic
+  unfold = do
+    l <- delim "unfold"
     spaceDelim
     (r, tm) <- located (term 0)
-    pure (Reduce (l + r) tm)
+    pure (Unfold (l + r) tm)
 
   continueSplit : (col : Int) -> Rule (List Tactic)
   continueSplit col = do

src/idris/Nova/Surface/Shunting.idr

@@ -181,9 +181,9 @@ mutual
   shuntTactic ops (Composition r alphas) = MEither.do
     alphas <- forList1 alphas (shuntTactic ops)
     return (Composition r alphas)
-  shuntTactic ops (Reduce r tm) = MEither.do
+  shuntTactic ops (Unfold r tm) = MEither.do
     tm <- shunt ops tm 0
-    return (Reduce r tm)
+    return (Unfold r tm)
   shuntTactic ops (Exact r tm) = MEither.do
     tm <- shunt ops tm 0
     return (Exact r tm)