ce7e45b · Idris-dev · git.iko.soy

src/Core/Unify.hs+18−4

compare with master

unifiedsplit

@@ -35,8 +35,15 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

35match_unify ctxt env topx topy dont holes =

36-- trace ("Matching " ++ show (topx, topy)) $

37 case runStateT (un [] topx topy) (UI 0 []) of

38+ OK (v, UI _ []) -> return (filter notTrivial v)

39+ res ->

40+ let topxn = normalise ctxt env topx

41+ topyn = normalise ctxt env topy in

42+ case runStateT (un [] topxn topyn)

43+ (UI 0 []) of

44+ OK (v, UI _ fails) ->

38− OK (v, UI _ fails) -> return (filter notTrivial v)

45+ return (filter notTrivial v)

39− Error e -> tfail e

46+ Error e -> tfail e

40 where

47 where

41 un names (P _ x _) tm

48 un names (P _ x _) tm

42 | holeIn env x || x `elem` holes

49 | holeIn env x || x `elem` holes

@@ -44,8 +51,6 @@ match_unify ctxt env topx topy dont holes =

44 un names tm (P _ y _)

51 un names tm (P _ y _)

45 | holeIn env y || y `elem` holes

52 | holeIn env y || y `elem` holes

46 = do sc 1; checkCycle (y, tm)

53 = do sc 1; checkCycle (y, tm)

47− un names x y

48− | OK True <- convEq' ctxt x y = do sc 1; return []

49 un bnames (V i) (P _ x _)

54 un bnames (V i) (P _ x _)

50 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

55 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

51 un bnames (P _ x _) (V i)

56 un bnames (P _ x _) (V i)

@@ -54,6 +59,15 @@ match_unify ctxt env topx topy dont holes =

54 = do hf <- un names fx fy

59 = do hf <- un names fx fy

55 ha <- un names ax ay

60 ha <- un names ax ay

56 combine names hf ha

61 combine names hf ha

62+ un names x y

63+ | OK True <- convEq' ctxt x y = do sc 1; return []

64+ | otherwise = do UI s f <- get

65+ let r = recoverable x y

66+ let err = CantUnify r

67+ topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s

68+ if (not r) then lift $ tfail err

69+ else do put (UI s ((x, y, env, err) : f))

70+ lift $ tfail err

57

71

58

72

59 -- TODO: there's an annoying amount of repetition between this and the

73 -- TODO: there's an annoying amount of repetition between this and the

src/Idris/AbsSyntaxTree.hs+2−1

@@ -382,7 +382,6 @@ data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level de

382 | PWith FC Name t [t] t [PDecl' t]

383 | PClauseR FC [t] t [PDecl' t]

384 | PWithR FC [t] t [PDecl' t]

385− | PTyClause FC Name t t [PDecl' t]

386 deriving Functor

385 deriving Functor

387{-!

386{-!

388deriving instance Binary PClause'

387deriving instance Binary PClause'

@@ -494,6 +493,7 @@ data PTerm = PQuote Raw

494 | PLet Name PTerm PTerm PTerm

493 | PLet Name PTerm PTerm PTerm

495 | PTyped PTerm PTerm -- ^ Term with explicit type

494 | PTyped PTerm PTerm -- ^ Term with explicit type

496 | PApp FC PTerm [PArg]

495 | PApp FC PTerm [PArg]

496+ | PMatchApp FC Name -- ^ Make an application by type matching

497 | PCase FC PTerm [(PTerm, PTerm)]

498 | PTrue FC

499 | PFalse FC

@@ -1047,6 +1047,7 @@ showImp impl tm = se 10 tm where

1047 se p e

1048 | Just str <- slist p e = str

1049 | Just num <- snat p e = show num

1050+ se p (PMatchApp _ f) = "match " ++ show f

1050 se p (PApp _ (PRef _ f) [])

1051 se p (PApp _ (PRef _ f) [])

1051 | not impl = show f

1052 | not impl = show f

1052 se p (PApp _ (PRef _ op@(UN (f:_))) args)

1053 se p (PApp _ (PRef _ op@(UN (f:_))) args)

src/Idris/ElabDecls.hs+3−1

@@ -648,7 +648,8 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

648 let lhs_ty = getInferType lhs'

649 logLvl 3 ("Elaborated: " ++ show lhs_tm)

650 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

651− (clhs, clhsty) <- recheckC fc [] lhs_tm

651+ (clhs_c, clhsty) <- recheckC fc [] lhs_tm

652+ let clhs = normalise ctxt [] clhs_c

652 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

653 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

653 -- Elaborate where block

654 -- Elaborate where block

654 ist <- getIState

655 ist <- getIState

@@ -765,6 +766,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

765 addP t = t

766 addP t = t

766 propagateParams ps (PRef fc n)

767 propagateParams ps (PRef fc n)

767 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps)

768 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps)

769+ propagateParams ps x = x

768

770

769elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

771elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

770 = do ctxt <- getContext

772 = do ctxt <- getContext

src/Idris/ElabTerm.hs+5

@@ -331,6 +331,11 @@ elab ist info pattern tcgen fn tm

331 Just xs@(_:_) -> NS n xs

332 _ -> n

333

334+ elab' (ina, g) (PMatchApp fc fn)

335+ = do let (fn', imps) = case lookupCtxtName fn (idris_implicits ist) of

336+ [(n, args)] -> (n, map (const True) args)

337+ ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

338+ solve

334 -- if f is local, just do a simple_app

339 -- if f is local, just do a simple_app

335 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

340 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

336 = do let args = {- case lookupCtxt f (inblock info) of

341 = do let args = {- case lookupCtxt f (inblock info) of

src/Idris/Parser.hs+18−4

@@ -607,6 +607,7 @@ pSimpleExtExpr syn = do i <- getState

607

608pNoExtExpr syn =

609 try (pApp syn)

610+ <|> try (pMatchApp syn)

610 <|> pRecordType syn

611 <|> pRecordType syn

611 <|> try (pSimpleExpr syn)

612 <|> try (pSimpleExpr syn)

612 <|> pLambda syn

613 <|> pLambda syn

@@ -873,6 +874,15 @@ pHSimpleExpr syn

873 return $ PHidden e

874 return $ PHidden e

874 <|> pSimpleExpr syn

875 <|> pSimpleExpr syn

875

876

877+pMatchApp syn = do ty <- pSimpleExpr syn

878+ symbol "<=="

879+ fc <- pfc

880+ f <- pfName

881+ return (PLet (MN 0 "match")

882+ ty

883+ (PMatchApp fc f)

884+ (PRef fc (MN 0 "match")))

885+

876pApp syn = do f <- pSimpleExpr syn

886pApp syn = do f <- pSimpleExpr syn

877 fc <- pfc

887 fc <- pfc

878 args <- many1 (do notEndApp

888 args <- many1 (do notEndApp

@@ -1394,10 +1404,10 @@ pClause syn

1394 setState (ist { lastParse = Just n })

1404 setState (ist { lastParse = Just n })

1395 return $ PClause fc n capp wargs rhs wheres)

1405 return $ PClause fc n capp wargs rhs wheres)

1396 <|> try (do pushIndent

1406 <|> try (do pushIndent

1397− n_in <- pfName; let n = expandNS syn n_in

1398− reserved "of"; reserved "type"

1399− fc <- pfc

1400 ty <- pSimpleExpr syn

1407 ty <- pSimpleExpr syn

1408+ symbol "<=="

1409+ fc <- pfc

1410+ n_in <- pfName; let n = expandNS syn n_in

1401 rhs <- pRHS syn n

1411 rhs <- pRHS syn n

1402 ist <- getState

1412 ist <- getState

1403 let ctxt = tt_ctxt ist

1413 let ctxt = tt_ctxt ist

@@ -1407,9 +1417,13 @@ pClause syn

1407 return x,

1417 return x,

1408 do pTerminator

1418 do pTerminator

1409 return ([], [])]

1419 return ([], [])]

1420+ let capp = PLet (MN 0 "match")

1421+ ty

1422+ (PMatchApp fc n)

1423+ (PRef fc (MN 0 "match"))

1410 ist <- getState

1424 ist <- getState

1411 setState (ist { lastParse = Just n })

1425 setState (ist { lastParse = Just n })

1412− return $ PTyClause fc n ty rhs wheres)

1426+ return $ PClause fc n capp [] rhs wheres)

1413 <|> try (do pushIndent

1427 <|> try (do pushIndent

1414 wargs <- many1 (pWExpr syn)

1428 wargs <- many1 (pWExpr syn)

1415 ist <- getState

1429 ist <- getState

test/test015/test015.idr+4−4

@@ -48,7 +48,7 @@ pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))

48term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))

49

50addBit : Bit x -> Bit y -> Bit c ->

51− (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))

51+ (bX ** (bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX)))

52addBit b0 b0 b0 = bitpair b0 b0

53addBit b0 b0 b1 = bitpair b0 b1

54addBit b0 b1 b0 = bitpair b0 b1

@@ -60,8 +60,8 @@ addBit b1 b1 b1 = bitpair b1 b1

60

61adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)

62adc zero zero carry ?= zero # carry

63−adc (numx # bx) (numy # by) carry

63+adc (numx # bX) (numy # bY) carry

64− ?= let (bitpair carry0 lsb) = addBit bx by carry in

64+ ?= let (bitpair carry0 lsb) = addBit bX bY carry in

65 adc numx numy carry0 # lsb

66

67readNum : IO Nat

@@ -108,7 +108,7 @@ Main.ntbEven = proof {

108Main.adc_lemma_2 = proof {

109 intro c,w,v,bit0,num0;

110 intro b0,v1,bit1,num1,b1;

111− intro bc,x,x1,bx,bx1;

111+ intro bc,x,x1,bX,bX1;

112 rewrite sym (plusZeroRightNeutral x);

113 rewrite sym (plusZeroRightNeutral v1);

114 rewrite sym (plusZeroRightNeutral (plus (plus x v) v1));