ce7e45b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

EXPERIMENTAL: Syntax for applying functions by expected type

"t <== f" applies a function f to arguments in such a way that it returns something of type t. The <== is a placeholder syntax until someone comes up with something better. (Alternative: t by f, but that uses up a new keyword)

commitce7e45b9ec0fef3a533b1b25a6485c57331b3837 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 28 Jun 2013, 11:10 (13 years ago) parent127cc70

6 files changed+50−14

compare with master

unifiedsplit

src/Core/Unify.hs+18−4 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/ElabDecls.hs+3−1 src/Idris/ElabTerm.hs+5 src/Idris/Parser.hs+18−4 test/test015/test015.idr+4−4

src/Core/Unify.hs+18−4

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

3535match_unify ctxt env topx topy dont holes =

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

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

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

39− Error e -> tfail e

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) ->

45+ return (filter notTrivial v)

46+ Error e -> tfail e

4047 where

4148 un names (P _ x _) tm

4249 | holeIn env x || x `elem` holes

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

4451 un names tm (P _ y _)

4552 | holeIn env y || y `elem` holes

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

47− un names x y

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

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

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

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

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

5459 = do hf <- un names fx fy

5560 ha <- un names ax ay

5661 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

5771

5872

5973 -- 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

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

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

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

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

386385 deriving Functor

387386{-!

388387deriving instance Binary PClause'

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

494493 | PLet Name PTerm PTerm PTerm

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

496495 | PApp FC PTerm [PArg]

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

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

498498 | PTrue FC

499499 | PFalse FC

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

10471047 se p e

10481048 | Just str <- slist p e = str

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

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

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

10511052 | not impl = show f

10521053 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)

648648 let lhs_ty = getInferType lhs'

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

650650 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

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

653654 -- Elaborate where block

654655 ist <- getIState

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

765766 addP t = t

766767 propagateParams ps (PRef fc n)

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

769+ propagateParams ps x = x

768770

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

770772 = do ctxt <- getContext

src/Idris/ElabTerm.hs+5

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

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

332332 _ -> n

333333

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

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

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

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

src/Idris/Parser.hs+18−4

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

607607

608608pNoExtExpr syn =

609609 try (pApp syn)

610+ <|> try (pMatchApp syn)

610611 <|> pRecordType syn

611612 <|> try (pSimpleExpr syn)

612613 <|> pLambda syn

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

873874 return $ PHidden e

874875 <|> pSimpleExpr syn

875876

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+

876886pApp syn = do f <- pSimpleExpr syn

877887 fc <- pfc

878888 args <- many1 (do notEndApp

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

13941404 setState (ist { lastParse = Just n })

13951405 return $ PClause fc n capp wargs rhs wheres)

13961406 <|> try (do pushIndent

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

1398− reserved "of"; reserved "type"

1399− fc <- pfc

14001407 ty <- pSimpleExpr syn

1408+ symbol "<=="

1409+ fc <- pfc

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

14011411 rhs <- pRHS syn n

14021412 ist <- getState

14031413 let ctxt = tt_ctxt ist

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

14071417 return x,

14081418 do pTerminator

14091419 return ([], [])]

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

1421+ ty

1422+ (PMatchApp fc n)

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

14101424 ist <- getState

14111425 setState (ist { lastParse = Just n })

1412− return $ PTyClause fc n ty rhs wheres)

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

14131427 <|> try (do pushIndent

14141428 wargs <- many1 (pWExpr syn)

14151429 ist <- getState

test/test015/test015.idr+4−4

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

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

4949

5050addBit : 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)))

5252addBit b0 b0 b0 = bitpair b0 b0

5353addBit b0 b0 b1 = bitpair b0 b1

5454addBit b0 b1 b0 = bitpair b0 b1

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

6060

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

6262adc zero zero carry ?= zero # carry

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

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

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

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

6565 adc numx numy carry0 # lsb

6666

6767readNum : IO Nat

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

108108Main.adc_lemma_2 = proof {

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

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

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

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

112112 rewrite sym (plusZeroRightNeutral x);

113113 rewrite sym (plusZeroRightNeutral v1);

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