229a99c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better elaboration order; also changed instance argument syntax slightly

commit229a99c8f6781d044f497634e3032641d06e0aba authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 6 Nov 2011, 17:54 (15 years ago) parent2d6c12e

9 files changed+147−100

compare with master

unifiedsplit

interp.idr+9−12 lib/builtins.idr+6−6 lib/prelude.idr+18−13 src/Core/Elaborate.hs+19−5 src/Core/ProofState.hs+11−24 src/Idris/AbsSyntax.hs+63−26 src/Idris/Delaborate.hs+3−3 src/Idris/ElabDecls.hs+13−6 src/Idris/Parser.hs+5−5

interp.idr+9−12

@@ -22,8 +22,8 @@ using (G : Vect Ty n) {

2222 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

2323 | Op : (Int -> Int -> interpTy c) ->

2424 Expr G TyInt -> Expr G TyInt -> Expr G c

25− -- | Op' : (interpTy a -> interpTy b -> interpTy c) ->

26− -- Expr G a -> Expr G b -> Expr G c

25+ | Op' : (interpTy a -> interpTy b -> interpTy c) ->

26+ Expr G a -> Expr G b -> Expr G c

2727 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

2828 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

2929

@@ -34,6 +34,7 @@ using (G : Vect Ty n) {

3434 interp env (Lam sc) = \x => interp (Extend x env) sc;

3535 interp env (App f s) = (interp env f) (interp env s);

3636 interp env (Op op x y) = op (interp env x) (interp env y);

37+ interp env (Op' op x y) = op (interp env x) (interp env y);

3738 interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);

3839 interp env (Bind v f) = interp env (f (interp env v));

3940

@@ -41,13 +42,13 @@ using (G : Vect Ty n) {

4142 eId = Lam (Var fO);

4243

4344 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

44− eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));

45+ eAdd = Lam (Lam (Op' (Var fO) (Var (fS fO)) prim__addInt));

4546

46− eDouble : Expr G (TyFun TyInt TyInt);

47− eDouble = Lam (App (App (Lam (Lam (Op (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

47+-- eDouble : Expr G (TyFun TyInt TyInt);

48+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

4849

49− eDouble' : Expr G (TyFun TyInt TyInt);

50− eDouble' = Lam (App (App eAdd (Var fO)) (Var fO));

50+ eDouble : Expr G (TyFun TyInt TyInt);

51+ eDouble = Lam (App (App eAdd (Var fO)) (Var fO));

5152

5253 app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;

5354 app = \f, a => App f a;

@@ -72,10 +73,6 @@ test = interp Empty eProg 2 2;

7273testFac : Int;

7374testFac = interp Empty eFac 4;

7475

75−intToStr : Int -> String;

76−intToStr 0 = "O";

77−intToStr n = "s" ++ intToStr (n - 1);

78−

7976main : IO ();

80−main = putStrLn (intToStr testFac);

77+main = print testFac;

8178

lib/builtins.idr+6−6

@@ -82,13 +82,13 @@ data Num : Set -> Set where

8282 Num a;

8383

8484 (+) : Num a => a -> a -> a;

85− (+) {{NumInstance p s m}} x y = p x y;

85+ (+) @{ NumInstance p s m } x y = p x y;

8686

8787 (-) : Num a => a -> a -> a;

88− (-) {{NumInstance p s m}} x y = s x y;

88+ (-) @{ NumInstance p s m } x y = s x y;

8989

9090 (*) : Num a => a -> a -> a;

91− (*) {{NumInstance p s m}} x y = m x y;

91+ (*) @{ NumInstance p s m } x y = m x y;

9292

9393instance numInt : Num Int;

9494instance numInt = NumInstance prim__addInt prim__subInt prim__mulInt;

@@ -102,10 +102,10 @@ data Eq : Set -> Set where

102102 Eq a;

103103

104104 (==) : Eq a => a -> a -> Bool;

105− (==) {{EqInstance eq neq}} x y = eq x y;

105+ (==) @{ EqInstance eq neq } x y = eq x y;

106106

107107 (/=) : Eq a => a -> a -> Bool;

108− (/=) {{EqInstance eq neq}} x y = neq x y;

108+ (/=) @{ EqInstance eq neq } x y = neq x y;

109109

110110instance EqInt : Eq Int;

111111instance EqInt = EqInstance (boolOp prim__eqInt) (\x, y => not (x == y));

@@ -121,7 +121,7 @@ data Ord : Set -> Set where

121121 Ord a;

122122

123123 compare : Ord a => a -> a -> Ordering;

124− compare {{OrdInstance c}} = c;

124+ compare @{ OrdInstance c } = c;

125125

126126instance OrdInt : Ord Int;

127127instance OrdInt = OrdInstance cmpInt where {

lib/prelude.idr+18−13

@@ -5,24 +5,13 @@ import maybe;

55import vect;

66import io;

8−---- some basic io

9−

10−putStr : String -> IO ();

11−putStr x = mkForeign (FFun "putStr" (Cons FString Nil) FUnit) x;

12−

13−putStrLn : String -> IO ();

14−putStrLn x = putStr (x ++ "\n");

15−

16−readLine : IO String;

17−readLine = mkForeign (FFun "readStr" Nil FString);

18−

198-- Show and instances

209

2110data Show : Set -> Set where

2211 ShowInstance : (show : a -> String) -> Show a;

2312

2413show : Show a => a -> String;

25−show {{ShowInstance s}} v = s v;

14+show @{ShowInstance s} v = s v;

2615

2716instance showNat : Show Nat;

2817instance showNat = ShowInstance show where {

@@ -50,6 +39,22 @@ instance showList = ShowInstance lshow where {

5039 show' : Show a => List a -> String;

5140 show' Nil = "";

5241 show' (Cons x Nil) = show x;

53− show' (Cons x xs) = show x ++ ", " ++ show' xs;

42+ show' (Cons x xs') = show x ++ ", " ++ show' xs';

5443 }

5544}

45+

46+

47+---- some basic io

48+

49+putStr : String -> IO ();

50+putStr x = mkForeign (FFun "putStr" (Cons FString Nil) FUnit) x;

51+

52+putStrLn : String -> IO ();

53+putStrLn x = putStr (x ++ "\n");

54+

55+print : Show a => a -> IO ();

56+print = putStrLn . show;

57+

58+readLine : IO String;

59+readLine = mkForeign (FFun "readStr" Nil FString);

60+

src/Core/Elaborate.hs+19−5

@@ -18,6 +18,7 @@ import Core.Typecheck

1818

1919import Control.Monad.State

2020import Data.Char

21+import Data.List

2122import Debug.Trace

2223

2324-- I don't really want this here, but it's useful for the test shell

@@ -118,9 +119,16 @@ get_instances = do ES p _ _ <- get

118119-- given a desired hole name, return a unique hole name

119120unique_hole :: Name -> Elab Name

120121unique_hole n = do ES p _ _ <- get

121− env <- get_env

122− return (uniqueName n (holes p ++ map fst env))

122+ let bs = bound_in (pterm p)

123+ return (uniqueName n (holes p ++ bs))

123124 where

125+ bound_in (Bind n b sc) = n : bi b ++ bound_in sc

126+ where

127+ bi (Let t v) = bound_in t ++ bound_in v

128+ bi (Guess t v) = bound_in t ++ bound_in v

129+ bi b = bound_in (binderTy b)

130+ bound_in (App f a) = bound_in f ++ bound_in a

131+ bound_in _ = []

124132

125133elog :: String -> Elab ()

126134elog str = do ES p logs prev <- get

@@ -251,17 +259,23 @@ apply fn imps =

251259 end_unify

252260 return args

253261

254−apply_elab :: Name -> [Maybe (Elab ())] -> Elab ()

262+apply_elab :: Name -> [Maybe (Int, Elab ())] -> Elab ()

255263apply_elab n args =

256264 do ty <- get_type (Var n)

257265 ctxt <- get_context

258266 env <- get_env

259267 claims <- doClaims (normalise ctxt env ty) args []

260268 prep_fill n (map fst claims)

261− elabClaims [] True claims

269+ let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

270+ elabClaims [] False claims

262271 complete_fill

263272 end_unify

264273 where

274+ priOrder Nothing Nothing = EQ

275+ priOrder Nothing _ = LT

276+ priOrder _ Nothing = GT

277+ priOrder (Just (x, _)) (Just (y, _)) = compare x y

278+

265279 doClaims (Bind n' (Pi t) sc) (i : is) claims =

266280 do n <- unique_hole (mkMN n')

267281 when (null claims) (start_unify n)

@@ -276,7 +290,7 @@ apply_elab n args =

276290 | otherwise = if r then elabClaims [] False failed

277291 else return ()

278292 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs

279− elabClaims failed r (e@(n, Just elaboration) : xs)

293+ elabClaims failed r (e@(n, Just (_, elaboration)) : xs)

280294 | r = try (do ES p _ _ <- get

281295 focus n; elaboration; elabClaims failed r xs)

282296 (elabClaims (e : failed) r xs)

src/Core/ProofState.hs+11−24

@@ -257,7 +257,8 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

257257

258258solve :: RunTactic

259259solve ctxt env (Bind x (Guess ty val) sc)

260− | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x],

260+ | pureTerm val = do ps <- get

261+ action (\ps -> ps { holes = holes ps \\ [x],

261262 instances = instances ps \\ [x] })

262263 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

263264 | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val

@@ -365,21 +366,15 @@ solve_unified ctxt env tm =

365366 action (\ps -> ps { holes = holes ps \\ map fst ns })

366367-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })

367368 return (updateSolved ns tm)

368− where

369− updateSolved xs (Bind n (Hole ty) t)

370− | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

371− updateSolved xs (Bind n b t)

372− | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

373− updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

374− updateSolved xs (P _ n _)

375− | Just v <- lookup n xs = v

376− updateSolved xs t = t

377−

378−-- shuffleHoles :: Term -> Term

379−-- shuffleHoles tm = shuffle [] tm

380−-- where

381−-- shuffle ns (Bind n b sc)

382−-- |

369+

370+updateSolved xs (Bind n (Hole ty) t)

371+ | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

372+updateSolved xs (Bind n b t)

373+ | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

374+updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

375+updateSolved xs (P _ n _)

376+ | Just v <- lookup n xs = v

377+updateSolved xs t = t

383378

384379processTactic :: Tactic -> ProofState -> TC (ProofState, String)

385380processTactic QED ps = case holes ps of

@@ -398,14 +393,6 @@ processTactic EndUnify ps = let (h, ns) = unified ps

398393 unified = (h, []),

399394 holes = holes ps \\ map fst ns }, "")

400395 where

401− updateSolved xs (Bind n (Hole ty) t)

402− | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))

403− updateSolved xs (Bind n b t)

404− | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)

405− updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)

406− updateSolved xs (P _ n _)

407− | Just v <- lookup n xs = v

408− updateSolved xs t = t

409396processTactic t ps

410397 = case holes ps of

411398 [] -> fail "Nothing to fill in."

src/Idris/AbsSyntax.hs+63−26

@@ -294,14 +294,21 @@ data PDo' t = DoExp FC t

294294

295295type PDo = PDo' PTerm

296296

297−data PArg' t = PImp { lazyarg :: Bool, pname :: Name, getTm :: t }

298− | PExp { lazyarg :: Bool, getTm :: t }

299− | PConstraint { lazyarg :: Bool, getTm :: t }

297+-- The priority gives a hint as to elaboration order. Best to elaborate

298+-- things early which will help give a more concrete type to other

299+-- variables, e.g. a before (interpTy a).

300+

301+data PArg' t = PImp { priority :: Int,

302+ lazyarg :: Bool, pname :: Name, getTm :: t }

303+ | PExp { priority :: Int,

304+ lazyarg :: Bool, getTm :: t }

305+ | PConstraint { priority :: Int,

306+ lazyarg :: Bool, getTm :: t }

300307 deriving (Show, Eq, Functor)

301308

302−pimp = PImp False

303−pexp = PExp False

304−pconst = PConstraint False

309+pimp = PImp 0 False

310+pexp = PExp 0 False

311+pconst = PConstraint 0 False

305312

306313type PArg = PArg' PTerm

307314

@@ -370,17 +377,17 @@ showDImp impl (PDatadecl n ty cons)

370377

371378getImps :: [PArg] -> [(Name, PTerm)]

372379getImps [] = []

373−getImps (PImp _ n tm : xs) = (n, tm) : getImps xs

380+getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs

374381getImps (_ : xs) = getImps xs

375382

376383getExps :: [PArg] -> [PTerm]

377384getExps [] = []

378−getExps (PExp _ tm : xs) = tm : getExps xs

385+getExps (PExp _ _ tm : xs) = tm : getExps xs

379386getExps (_ : xs) = getExps xs

380387

381388getConsts :: [PArg] -> [PTerm]

382389getConsts [] = []

383−getConsts (PConstraint _ tm : xs) = tm : getConsts xs

390+getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs

384391getConsts (_ : xs) = getConsts xs

385392

386393getAll :: [PArg] -> [PTerm]

@@ -420,10 +427,9 @@ showImp impl tm = se 10 tm where

420427 = let [l, r] = getExps args in

421428 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

422429 se p (PApp _ f as)

423− = let (imps, cs, args) = (getImps as, getConsts as, getExps as) in

424− bracket p 1 $ se 1 f ++ concatMap scArg cs

425− ++ (if impl then concatMap siArg imps else "")

426− ++ concatMap seArg args

430+ = let args = getExps as in

431+ bracket p 1 $ se 1 f ++ if impl then concatMap sArg as

432+ else concatMap seArg args

427433 se p (PHidden tm) = "." ++ se 0 tm

428434 se p (PRefl _) = "refl"

429435 se p (PResolveTC _) = "resolvetc"

@@ -438,6 +444,10 @@ showImp impl tm = se 10 tm where

438444 se p (PMetavar n) = "?" ++ show n

439445 se p Placeholder = "_"

440446

447+ sArg (PImp _ _ n tm) = siArg (n, tm)

448+ sArg (PExp _ _ tm) = seArg tm

449+ sArg (PConstraint _ _ tm) = scArg tm

450+

441451 seArg arg = " " ++ se 0 arg

442452 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"

443453 scArg val = " {{" ++ se 10 val ++ "}}"

@@ -592,6 +602,33 @@ expandParamsD dec ps ns (PClauses fc n cs)

592602 (map (expandParamsD dec ps ns) ds)

593603expandParamsD dec ps ns d = d

594604

605+-- Calculate a priority for a type, for deciding elaboration order

606+-- * if it's just a type variable or concrete type, do it early (0)

607+-- * if there's only type variables and injective constructors, do it next (1)

608+-- * if there's a function type, next (2)

609+-- * finally, everything else (3)

610+

611+getPriority :: IState -> PTerm -> Int

612+getPriority i tm = pri tm

613+ where

614+ pri (PRef _ n) =

615+ case lookupP n (tt_ctxt i) of

616+ Just (P (DCon _ _) _ _) -> 1

617+ Just (P (TCon _ _) _ _) -> 1

618+ Just (P Ref _ _) -> 3

619+ Nothing -> 0 -- must be locally bound, if it's not an error...

620+ pri (PPi _ _ x y) = max 4 (max (pri x) (pri y))

621+ pri (PTrue _) = 0

622+ pri (PFalse _) = 0

623+ pri (PRefl _) = 1

624+ pri (PEq _ l r) = max 1 (max (pri l) (pri r))

625+ pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

626+ pri (PPair _ l r) = max 1 (max (pri l) (pri r))

627+ pri (PDPair _ l r) = max 1 (max (pri l) (pri r))

628+ pri (PConstant _) = 0

629+ pri Placeholder = 1

630+ pri _ = 3

631+

595632-- Dealing with implicit arguments

596633

597634-- Add implicit Pi bindings for any names in the term which appear in an

@@ -631,7 +668,7 @@ implicitise syn ist tm

631668 imps top env (PPi (Imp l _) n ty sc)

632669 = do let isn = nub (namesIn ist ty) `dropAll` [n]

633670 (decls , ns) <- get

634− put (PImp l n ty : decls,

671+ put (PImp (getPriority ist ty) l n ty : decls,

635672 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

636673 imps True (n:env) sc

637674 imps top env (PPi (Exp l _) n ty sc)

@@ -639,7 +676,7 @@ implicitise syn ist tm

639676 (PRef _ x) -> namesIn ist sc `dropAll` [n]

640677 _ -> [])

641678 (decls, ns) <- get -- ignore decls in HO types

642− put (PExp l ty : decls,

679+ put (PExp (getPriority ist ty) l ty : decls,

643680 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

644681 imps True (n:env) sc

645682 imps top env (PPi (Constraint l _) n ty sc)

@@ -647,7 +684,7 @@ implicitise syn ist tm

647684 (PRef _ x) -> namesIn ist sc `dropAll` [n]

648685 _ -> [])

649686 (decls, ns) <- get -- ignore decls in HO types

650− put (PConstraint l ty : decls,

687+ put (PConstraint 10 l ty : decls,

651688 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

652689 imps True (n:env) sc

653690 imps top env (PEq _ l r)

@@ -723,21 +760,21 @@ aiFn ist fc f as

723760 Nothing -> mkPApp fc 1 (PRef fc f) as

724761 where

725762 insertImpl :: [PArg] -> [PArg] -> [PArg]

726− insertImpl (PExp l ty : ps) (PExp _ tm : given) =

727− PExp l tm : insertImpl ps given

728− insertImpl (PConstraint l ty : ps) (PConstraint _ tm : given) =

729− PConstraint l tm : insertImpl ps given

730− insertImpl (PConstraint l ty : ps) given =

731− PConstraint l (PResolveTC fc) : insertImpl ps given

732− insertImpl (PImp l n ty : ps) given =

763+ insertImpl (PExp p l ty : ps) (PExp _ _ tm : given) =

764+ PExp p l tm : insertImpl ps given

765+ insertImpl (PConstraint p l ty : ps) (PConstraint _ _ tm : given) =

766+ PConstraint p l tm : insertImpl ps given

767+ insertImpl (PConstraint p l ty : ps) given =

768+ PConstraint p l (PResolveTC fc) : insertImpl ps given

769+ insertImpl (PImp p l n ty : ps) given =

733770 case find n given [] of

734− Just (tm, given') -> PImp l n tm : insertImpl ps given'

735− Nothing -> PImp l n Placeholder : insertImpl ps given

771+ Just (tm, given') -> PImp p l n tm : insertImpl ps given'

772+ Nothing -> PImp p l n Placeholder : insertImpl ps given

736773 insertImpl expected [] = []

737774 insertImpl [] given = given

738775

739776 find n [] acc = Nothing

740− find n (PImp _ n' t : gs) acc

777+ find n (PImp _ _ n' t : gs) acc

741778 | n == n' = Just (t, reverse acc ++ gs)

742779 find n (g : gs) acc = find n gs (g : acc)

743780

src/Idris/Delaborate.hs+3−3

@@ -43,9 +43,9 @@ delab ist tm = de [] tm

4343 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

4444 | otherwise = PApp un (PRef un n) (map pexp args)

4545

46− imp (PImp l n _) arg = PImp l n arg

47− imp (PExp l _) arg = PExp l arg

48− imp (PConstraint l _) arg = PConstraint l arg

46+ imp (PImp p l n _) arg = PImp p l n arg

47+ imp (PExp p l _) arg = PExp p l arg

48+ imp (PConstraint p l _) arg = PConstraint p l arg

4949

5050pshow :: IState -> Err -> String

5151pshow i (Msg s) = s

src/Idris/ElabDecls.hs+13−6

@@ -354,14 +354,17 @@ elab ist info pattern tm

354354

355355 toElab arg = case getTm arg of

356356 Placeholder -> Nothing

357− v -> Just (elabE v)

357+ v -> Just (priority arg, elabE v)

358358

359359 mkPat = do hs <- get_holes

360360 case hs of

361361 (h: hs) -> do patvar h; mkPat

362362 [] -> return ()

363363

364− elabE t = elab' t

364+ elabE t = {- do g <- goal

365+ tm <- get_term

366+ trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

367+ $ -} elab' t

365368

366369 local f = do e <- get_env

367370 return (f `elem` map fst e)

@@ -437,7 +440,11 @@ elab ist info pattern tm

437440 ivs <- get_instances

438441 try (do ns <- apply (Var f) (map isph args)

439442 solve

440− elabArgs [] True ns (map (\x -> (lazyarg x, getTm x)) args))

443+ let (ns', eargs)

444+ = unzip $

445+ sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

446+ (zip ns args)

447+ elabArgs [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))

441448 (do apply_elab f (map toElab args)

442449 solve)

443450 ivs' <- get_instances

@@ -450,7 +457,7 @@ elab ist info pattern tm

450457-- trace (show ivs ++ "\n" ++ show t) $

451458-- mapM_ (\n -> do focus n

452459-- resolveTC ist) ivs

453− where tcArg (n, PConstraint _ Placeholder) = True

460+ where tcArg (n, PConstraint _ _ Placeholder) = True

454461 tcArg _ = False

455462

456463 elab' (PApp fc f [arg])

@@ -516,7 +523,7 @@ resolveTC depth ist

516523 resolveTC (depth - 1) ist)

517524 (filter (\ (x, y) -> not x) (zip imps args))

518525 solve

519− where isImp (PImp _ _ _) = True

526+ where isImp (PImp _ _ _ _) = True

520527 isImp _ = False

521528

522529collectDeferred :: Term -> State [(Name, Type)] Term

@@ -552,7 +559,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

552559 Just args -> map isImp args

553560 ns <- apply (Var fn) imps

554561 when autoSolve solveAll

555− where isImp (PImp _ _ _) = True

562+ where isImp (PImp _ _ _ _) = True

556563 isImp _ = False

557564 runT (Refine fn imps) = do ns <- apply (Var fn) imps

558565 when autoSolve solveAll

src/Idris/Parser.hs+5−5

@@ -393,7 +393,7 @@ pImplicitArg syn = do lchar '{'; n <- pName

393393 lchar '}'

394394 return (pimp n v)

395395

396−pConstraintArg syn = do symbol "{{"; e <- pExpr syn; symbol "}}"

396+pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"

397397 return (pconst e)

398398

399399pTSig syn = do lchar ':'

@@ -576,13 +576,13 @@ pClause syn

576576 rhs <- pExpr syn

577577 ist <- getState

578578 let ctxt = tt_ctxt ist

579− let wsyn = whereSyn n syn (map getTm cargs ++

580− map getTm iargs ++

579+ let wsyn = whereSyn n syn (map getTm iargs ++

580+ map getTm cargs ++

581581 args ++ wargs)

582582 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'

583583 return ([], [])]

584584 return $ PClause n (PApp fc (PRef fc n)

585− (cargs ++ iargs ++ map pexp args)) wargs rhs wheres)

585+ (iargs ++ cargs ++ map pexp args)) wargs rhs wheres)

586586 <|> try (do n <- pfName

587587 cargs <- many (pConstraintArg syn)

588588 iargs <- many (pImplicitArg syn)

@@ -596,7 +596,7 @@ pClause syn

596596 let withs = concat ds

597597 lchar '}'

598598 return $ PWith n (PApp fc (PRef fc n)

599− (cargs ++ iargs ++ map pexp args)) wargs wval withs)

599+ (iargs ++ cargs ++ map pexp args)) wargs wval withs)

600600

601601 <|> do l <- pSimpleExpr syn

602602 op <- operator