Skip to content

Commit 52ab8f3

Browse files
g-nakovg-nakov
committedSep 9, 2024
[ new ] support for subtraction
1 parent 24cb6c6 commit 52ab8f3

File tree

6 files changed

+134
-42
lines changed

6 files changed

+134
-42
lines changed
 

‎examples/imeko.m

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
%%> times :: [ 1 x 12 ] double
2+
3+
%%> voltages :: [ 1 x 12 ] double
4+
5+
6+
%> z3 :: [ 3 x 1 ] double
7+
z3 = [ 0; 0; 0 ]
8+
%> i3 :: [ 3 x 1 ] double
9+
i3 = [ 1; 1; 1 ]
10+
11+
% %> ddnc :: [ 12 x 4 ] double
12+
ddnc = [ i3 z3 i3 z3
13+
-i3 z3 i3 z3
14+
z3 i3 z3 i3
15+
z3 -i3 z3 i3 ]
16+
%> typeof ddnc
17+
18+
%M = [ ddnc times' ]
19+
%%> typeof M
20+
21+
%x = M \ voltages
22+
%%> typeof x

‎src/CoreTT.hs

+4-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ import Term
1313

1414
import Debug.Trace
1515

16-
track = const id --trace
16+
track = const id -- track
1717

1818
data Status = Crying | Waiting | Hoping | Abstract | ProgramVar
1919
deriving (Ord, Eq, Show)
@@ -534,6 +534,9 @@ evalSynth tm = withScope $ case tm of
534534
, Atom Stranspose <- dstr -> do
535535
let sg = subSnoc (subSnoc (idSubst natty :^ No (No (io natty))) (var 0)) (var 1)
536536
pure (E $^ D $^ ((R $^ (tgt <&> tgtTy)) <&> dstr), mk SMatrix colGenTy rowGenTy (lam c $ lam r $ cellTy //^ sg) cs rs)
537+
Just (SMatrix, [rowGenTy, colGenTy, cellTy, rs, cs])
538+
| Atom Suminus <- dstr ->
539+
pure (E $^ D $^ ((R $^ (tgt <&> tgtTy)) <&> dstr), tgtTy)
537540
_ -> fail "evalSynth: eliminator for an unknown type"
538541
tm | Just tm <- MX $? tm, (lmx, rmx) <- split tm -> do
539542
(lmx, lmxTy) <- evalSynth lmx

‎src/Machine.hs

+99-41
Original file line numberDiff line numberDiff line change
@@ -865,7 +865,7 @@ data FlexEh (gamma :: Nat) where
865865
-> Subst n ^ delta -- how to map the permitted variables into the
866866
-- flex variable's context
867867
-> FlexEh gamma
868-
868+
869869
data FlexEhWork (gamma' :: Nat)(delta' :: Nat) where
870870
FlexEhWork
871871
:: n <= gamma' -- the thinning for the candidate solution's
@@ -2338,8 +2338,7 @@ runElabTask sol meta@Meta{..} etask = nattily (vlen mctxt) $ do
23382338
run
23392339
TypeExprTask whereAmI synthMode (TyBinaryOp Plus x y) -> do
23402340
-- TODO:
2341-
-- 1. make sure `mtype` admits plus
2342-
-- 2. find the correct way of doing plus in `mtype`
2341+
-- 1. find the correct way of doing plus in `mtype`
23432342
(xTy, yTy, stats) <- case synthMode of
23442343
EnsureCompatibility -> pure (mtype, mtype, [])
23452344
FindSimplest -> do
@@ -2357,6 +2356,12 @@ runElabTask sol meta@Meta{..} etask = nattily (vlen mctxt) $ do
23572356
pushProblems [xProb, yProb]
23582357
newProb . Elab sol $ Await (conjunction stats) (mk Splus xSol ySol) -- FIXME: do proper addition, eg if mtype is a matrix type
23592358
move winning
2359+
TypeExprTask whereAmI synthMode (TyUnaryOp UMinus x) -> do
2360+
(_, _, _, _, _, stat) <- ensureMatrix mctxt mtype
2361+
(xSol, xProb) <- elab "minusXTy" mctxt mtype (TypeExprTask whereAmI synthMode <$> x)
2362+
pushProblems [xProb]
2363+
newProb . Elab sol $ Await stat (E $^ matrixUminus (R $^ xSol <&> mtype))
2364+
move winning
23602365
TypeExprTask whereAmI synthMode (TyBinaryOp (Mul False{- x*y -} Times) x y) -> do
23612366
-- Two main issues:
23622367
-- redundancy in representation of matrices:
@@ -2444,48 +2449,101 @@ runElabTask sol meta@Meta{..} etask = nattily (vlen mctxt) $ do
24442449
}
24452450
newProb . Elab sol $ Await cs (ixKI mtype (lit s))
24462451
run
2447-
{-
2448-
TypeExprTask whereAmI _ (TyStringLiteral s) -> case tagEh mtype of
2449-
Just (SList, [genTy]) -> do
2450-
(_, cs) <- constrain "IsChar" $ Constraint
2451-
{ constraintCtx = fmap Hom <$> mctxt
2452-
, constraintType = Hom (atom SType)
2453-
, lhs = genTy
2454-
, rhs = atom SChar
2455-
}
2456-
newProb . Elab sol $ Await cs (ixKI mtype (lit s))
2457-
run
2458-
_ -> move worried
2459-
-}
2460-
TypeExprTask MatLab EnsureCompatibility (TyJux dir x (TyNil _ :<=: _)) -> do
2452+
TypeExprTask MatLab synthMode (TyJux dir x (TyNil _ :<=: _)) -> do
24612453
(rowGenTy, colGenTy, cellTy, rs, cs, tystat) <- ensureMatrix mctxt mtype
2462-
(xSol, xProb) <- elab "vjuxTop" mctxt (mk SMatrix rowGenTy colGenTy cellTy rs cs) (TypeExprTask MatLab EnsureCompatibility <$> x)
2454+
(xSol, xProb) <- elab "nextToNil" mctxt (mk SMatrix rowGenTy colGenTy cellTy rs cs) (TypeExprTask MatLab synthMode <$> x)
24632455
pushProblems [xProb]
24642456
newProb . Elab sol $ Await tystat $ xSol
24652457
run
2466-
{-
2467-
let nill = nil in do
2468-
(rowTy, colTy, cellTy, rs, cs, tystat) <- ensureMatrixType mctxt mtype
2469-
case dir of
2470-
Vertical -> do
2471-
(_, rstat) <- constrain "noRs" $ Constraint
2472-
{ constraintCtx = fmap Hom <$> mctxt
2473-
, constraintType = Hom (mk SList rowTy)
2474-
, lhs = nill
2475-
, rhs = rs
2476-
}
2477-
newProb . Elab sol $ Await rstat $ nill
2478-
run
2479-
Horizontal -> do
2480-
(_, cstat) <- constrain "noCs" $ Constraint
2481-
{ constraintCtx = fmap Hom <$> mctxt
2482-
, constraintType = Hom (mk SList colTy)
2483-
, lhs = nill
2484-
, rhs = cs
2485-
}
2486-
newProb . Elab sol $ Await cstat $ nill
2487-
run
2488-
-}
2458+
TypeExprTask MatLab FindSimplest (TyJux dir x y) -> let n = vlen mctxt in nattily n $ do
2459+
(rowGenTy, colGenTy, cellTy', rs, cs, tystat) <- ensureMatrix mctxt mtype
2460+
xTy <- invent "xType" mctxt (atom SType)
2461+
yTy <- invent "yType" mctxt (atom SType)
2462+
(xRowGenTy, xColGenTy, xCellTy', xrs, xcs, xTystat) <- ensureMatrix mctxt xTy
2463+
(yRowGenTy, yColGenTy, yCellTy', yrs, ycs, yTystat) <- ensureMatrix mctxt yTy
2464+
let ((i, j), cellTy) = unpackCellType cellTy'
2465+
let (_, xCellTy) = unpackCellType xCellTy'
2466+
let (_, yCellTy) = unpackCellType yCellTy'
2467+
(xSol, xProb) <- elab "juxX" mctxt xTy (TypeExprTask MatLab FindSimplest <$> x)
2468+
(ySol, yProb) <- elab "juxY" mctxt yTy (TypeExprTask MatLab FindSimplest <$> y)
2469+
(_ , rj) <- constrain "rowJoin" $ JoinConstraint
2470+
{ constraintCtx = fmap Hom <$> mctxt
2471+
, leftGenType = xRowGenTy
2472+
, rightGenType = yRowGenTy
2473+
, joinGenType = rowGenTy
2474+
}
2475+
(_ , cj) <- constrain "colJoin" $ JoinConstraint
2476+
{ constraintCtx = fmap Hom <$> mctxt
2477+
, leftGenType = xColGenTy
2478+
, rightGenType = yColGenTy
2479+
, joinGenType = colGenTy
2480+
}
2481+
(jux, stats) <- case dir of
2482+
Vertical -> do
2483+
(_, rstat) <- constrain "catRows" $ Constraint
2484+
{ constraintCtx = fmap Hom <$> mctxt
2485+
, constraintType = Het (mk SList (tag SAbel [rowGenTy])) rj (mk SList (tag SAbel [rowGenTy]))
2486+
, lhs = rs
2487+
, rhs = mk Splus xrs yrs
2488+
}
2489+
(_, sameStat) <- constrain "sameCol" $ Constraint
2490+
{ constraintCtx = fmap Hom <$> mctxt
2491+
, constraintType = Het (mk SList (tag SAbel [colGenTy])) cj (mk SList (tag SAbel [colGenTy]))
2492+
, lhs = cs
2493+
, rhs = xcs
2494+
}
2495+
joinElt <- invent "joinElement" mctxt colGenTy
2496+
(_, cstat) <- constrain "colCompat" $ HeadersCompatibility
2497+
{ constraintCtx = fmap Hom <$> mctxt
2498+
, leftGenType = xColGenTy
2499+
, rightGenType = yColGenTy
2500+
, joinGenType = colGenTy
2501+
, joinStatus = cj
2502+
, leftList = xcs
2503+
, rightList = ycs
2504+
, joinElement = joinElt
2505+
}
2506+
(_, cellStat) <- constrain "cellJoin" $ JoinConstraint
2507+
{ constraintCtx = fmap Hom <$> (mctxt \\\ (i, mk SAbel rowGenTy) \\\ (j, wk $ mk SAbel colGenTy))
2508+
, leftGenType = xCellTy
2509+
, rightGenType = yCellTy //^ subSnoc (subSnoc (idSubst n :^ No (No (io n))) (var 1)) (R $^ (mk Splus (var 0) (wk (wk joinElt))) <&> wk (wk $ mk SAbel colGenTy))
2510+
, joinGenType = cellTy
2511+
}
2512+
pure (Svjux, [rstat, sameStat, cstat, cellStat])
2513+
Horizontal -> do
2514+
(_, cstat) <- constrain "catCols" $ Constraint
2515+
{ constraintCtx = fmap Hom <$> mctxt
2516+
, constraintType = Het (mk SList (tag SAbel [colGenTy])) cj (mk SList (tag SAbel [colGenTy]))
2517+
, lhs = cs
2518+
, rhs = mk Splus xcs ycs
2519+
}
2520+
(_, sameStat) <- constrain "sameRows" $ Constraint
2521+
{ constraintCtx = fmap Hom <$> mctxt
2522+
, constraintType = Het (mk SList (tag SAbel [rowGenTy])) rj (mk SList (tag SAbel [rowGenTy]))
2523+
, lhs = rs
2524+
, rhs = xrs
2525+
}
2526+
joinElt <- invent "joinElement" mctxt rowGenTy
2527+
(_, rstat) <- constrain "rowCompat" $ HeadersCompatibility
2528+
{ constraintCtx = fmap Hom <$> mctxt
2529+
, leftGenType = xRowGenTy
2530+
, rightGenType = yRowGenTy
2531+
, joinGenType = rowGenTy
2532+
, joinStatus = rj
2533+
, leftList = xrs
2534+
, rightList = yrs
2535+
, joinElement = joinElt
2536+
}
2537+
(_, cellStat) <- constrain "cellJoin" $ JoinConstraint
2538+
{ constraintCtx = fmap Hom <$> (mctxt \\\ (i, mk SAbel rowGenTy) \\\ (j, wk $ mk SAbel colGenTy))
2539+
, leftGenType = xCellTy
2540+
, rightGenType = yCellTy //^ subSnoc (subSnoc (idSubst n :^ No (No (io n))) (R $^ (mk Splus (var 1) (wk (wk joinElt))) <&> wk (wk $ mk SAbel rowGenTy))) (var 0)
2541+
, joinGenType = cellTy
2542+
}
2543+
pure (Shjux, [cstat, sameStat, rstat, cellStat])
2544+
pushProblems [xProb, yProb]
2545+
newProb . Elab sol $ Await (conjunction $ [tystat, xTystat, yTystat, rj, cj] ++ stats) (mk jux xSol ySol)
2546+
run
24892547
TypeExprTask MatLab EnsureCompatibility (TyJux dir x y) -> do
24902548
(rowGenTy, colGenTy, cellTy, rs, cs, tystat) <- ensureMatrix mctxt mtype
24912549
case dir of

‎src/MagicStrings.hs

+1
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ pattern Sfst = "fst"
1919
pattern Ssnd = "snd"
2020
pattern Sinverse = "inverse"
2121
pattern Stranspose = "transpose"
22+
pattern Suminus = "uminus"
2223

2324
-- constructors
2425
pattern Splus = "plus"

‎src/Syntax.hs

+5
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,11 @@ toTypeExpr' (BinaryOp (Mul d LDiv) x y) = do
136136
x <- toTypeExpr x
137137
y <- toTypeExpr y
138138
pure (TyBinaryOp (Mul d Times) (TyUnaryOp UInvert x :<=: xsrc) y)
139+
toTypeExpr' (BinaryOp Minus x y) = do
140+
let ysrc = source y
141+
x <- toTypeExpr x
142+
y <- toTypeExpr y
143+
pure (TyBinaryOp Plus x (TyUnaryOp UMinus y :<=: ysrc))
139144
toTypeExpr' (BinaryOp op x y) = TyBinaryOp op <$> toTypeExpr x <*> toTypeExpr y
140145
toTypeExpr' (Mat exps) = do
141146
exps <- traverse (traverse toTypeExpr) exps

‎src/Term.hs

+3
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,9 @@ matrixInverse t = withScopeOf t $ (D $^ t <&> atom Sinverse)
6363
matrixTranspose :: Term Syn ^ n -> Term Syn ^ n
6464
matrixTranspose t = withScopeOf t $ (D $^ t <&> atom Stranspose)
6565

66+
matrixUminus :: Term Syn ^ n -> Term Syn ^ n
67+
matrixUminus t = withScopeOf t $ (D $^ t <&> atom Suminus)
68+
6669
type Root = Bwd (String, Int)
6770
type NameSupply = (Root, Int)
6871
newtype Name = Name { longname :: [(String, Int)] }

0 commit comments

Comments
 (0)
Please sign in to comment.