be3a53a · Idris-dev · git.iko.soy

lib/builtins.idr+20−17

@@ -71,14 +71,26 @@ intToBool x = True;

7171boolOp : (a -> a -> Int) -> a -> a -> Bool;

7272boolOp op x y = intToBool (op x y);

7373

74−(+) : Int -> Int -> Int;

75−(+) = prim__addInt;

74+data Num : Set -> Set where

75+ NumInstance : (plus : a -> a -> a) ->

76+ (sub : a -> a -> a) ->

77+ (mult : a -> a -> a) ->

78+ Num a;

7679

77−(-) : Int -> Int -> Int;

78−(-) = prim__subInt;

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

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

7982

80−(*) : Int -> Int -> Int;

81−(*) = prim__mulInt;

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

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

85+

86+ (*) : Num a => a -> a -> a;

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

88+

89+instance numInt : Num Int;

90+instance numInt = NumInstance prim__addInt prim__subInt prim__mulInt;

91+

92+instance numFloat : Num Float;

93+instance numFloat = NumInstance prim__addFloat prim__subFloat prim__mulFloat;

8294

8395div : Int -> Int -> Int;

8496div = prim__divInt;

@@ -98,17 +110,8 @@ div = prim__divInt;

98110(>=) : Int -> Int -> Bool;

99111(>=) = boolOp prim__gteInt;

100112

101−(+.) : Float -> Float -> Float;

102−(+.) = prim__addFloat;

103−

104−(-.) : Float -> Float -> Float;

105−(-.) = prim__subFloat;

106−

107−(*.) : Float -> Float -> Float;

108−(*.) = prim__mulFloat;

109−

110−(/.) : Float -> Float -> Float;

111−(/.) = prim__divFloat;

113+(/) : Float -> Float -> Float;

114+(/) = prim__divFloat;

112115

113116(==.) : Float -> Float -> Bool;

114117(==.) = boolOp prim__eqFloat;

lib/nat.idr+12

@@ -27,3 +27,15 @@ plus_commutes_Sk = proof {

2727 rewrite (sym ih);

2828 refine plusn_Sm;

2929};

30+

31+sub : Nat -> Nat -> Nat;

32+sub O y = O;

33+sub (S k) (S y) = sub k y;

34+sub x O = x;

35+

36+mult : Nat -> Nat -> Nat;

37+mult O y = O;

38+mult (S k) y = plus y (mult k y);

39+

40+instance numNat : Num Nat;

41+instance numNat = NumInstance plus sub mult;

lib/vect.idr+1−1

@@ -14,7 +14,7 @@ vlookup : Fin n -> Vect a n -> a;

1414vlookup fO (x :: xs) = x;

1515vlookup (fS k) (x :: xs) = vlookup k xs;

1616

17−vapp : Vect a n -> Vect a m -> Vect a (plus n m);

17+vapp : Vect a n -> Vect a m -> Vect a (n + m);

1818vapp VNil ys = ys;

1919vapp (x :: xs) ys = x :: vapp xs ys;

2020

src/Core/CoreParser.hs+1−1

@@ -22,7 +22,7 @@ idrisDef = haskellDef {

2222 "do", "dsl", "import", "return", -- "refl",

2323 "infix", "infixl", "infixr", "prefix",

2424 "where", "with", "forall", "syntax", "proof",

25− "using", "params", "namespace",

25+ "using", "params", "namespace", "class", "instance",

2626 "Int", "Float", "Char", "String", "Ptr"]

2727 }

2828

src/Core/Elaborate.hs+8−1

@@ -110,6 +110,11 @@ get_deferred :: Elab [Name]

110110get_deferred = do ES p _ _ <- get

111111 return (deferred p)

112112

113+-- get instance argument names

114+get_instances :: Elab [Name]

115+get_instances = do ES p _ _ <- get

116+ return (instances p)

117+

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

114119unique_hole :: Name -> Elab Name

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

@@ -189,6 +194,9 @@ movelast n = processTactic' (MoveLast n)

189194defer :: Name -> Elab ()

190195defer n = processTactic' (Defer n)

191196

197+instanceArg :: Name -> Elab ()

198+instanceArg n = processTactic' (Instance n)

199+

192200proofstate :: Elab ()

193201proofstate = processTactic' ProofState

194202

@@ -200,7 +208,6 @@ qed = do processTactic' QED

200208undo :: Elab ()

201209undo = processTactic' Undo

202210

203−

204211prepare_apply :: Raw -> [Bool] -> Elab [Name]

205212prepare_apply fn imps =

206213 do ty <- get_type fn

src/Core/ProofState.hs+18−5

@@ -24,6 +24,7 @@ data ProofState = PS { thname :: Name,

2424 ptype :: Type, -- original goal

2525 unified :: (Name, [(Name, Term)]),

2626 deferred :: [Name], -- names we'll need to define

27+ instances :: [Name], -- instance arguments (for type classes)

2728 previous :: Maybe ProofState, -- for undo

2829 context :: Context,

2930 plog :: String,

@@ -55,6 +56,7 @@ data Tactic = Attack

5556 | PatBind Name

5657 | Focus Name

5758 | Defer Name

59+ | Instance Name

5860 | MoveLast Name

5961 | ProofState

6062 | Undo

@@ -64,8 +66,8 @@ data Tactic = Attack

6466-- Some utilites on proof and tactic states

6567

6668instance Show ProofState where

67− show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"

68− show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)

69+ show (PS nm [] _ tm _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"

70+ show (PS nm (h:hs) _ tm _ _ i _ _ ctxt _ _)

6971 = let OK g = goal (Just h) tm

7072 wkenv = premises g in

7173 "Other goals: " ++ show hs ++ "\n" ++

@@ -112,7 +114,8 @@ addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

112114newProof :: Name -> Context -> Type -> ProofState

113115newProof n ctxt ty = let h = holeName 0

114116 ty' = vToP ty in

115− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []

117+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, [])

118+ [] []

116119 Nothing ctxt "" False

117120

118121type TState = ProofState -- [TacticAction])

@@ -191,6 +194,14 @@ movelast n ctxt env t = do action (\ps -> let hs = holes ps in

191194 else ps)

192195 return t

193196

197+instanceArg :: Name -> RunTactic

198+instanceArg n ctxt env (Bind x (Hole t) sc)

199+ = do action (\ps -> let hs = holes ps

200+ is = instances ps in

201+ ps { holes = (hs \\ [x]) ++ [x],

202+ instances = x:is })

203+ return (Bind x (Hole t) sc)

204+

194205defer :: Name -> RunTactic

195206defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

196207 do action (\ps -> let hs = holes ps in

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

246257

247258solve :: RunTactic

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

249− | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })

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

261+ instances = instances ps \\ [x] })

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

251263 | otherwise = fail "I see a hole in your solution."

252264solve _ _ h = fail $ "Not a guess " ++ show h

@@ -426,5 +438,6 @@ process t h = tactic (Just h) (mktac t)

426438 mktac (CheckIn r) = check_in r

427439 mktac (EvalIn r) = eval_in r

428440 mktac (Focus n) = focus n

429− mktac (MoveLast n) = movelast n

430441 mktac (Defer n) = defer n

442+ mktac (Instance n) = instanceArg n

443+ mktac (MoveLast n) = movelast n

src/Idris/AbsSyntax.hs+31−2

@@ -171,10 +171,13 @@ data Plicity = Imp { plazy :: Bool,

171171 pstatic :: Static }

172172 | Exp { plazy :: Bool,

173173 pstatic :: Static }

174+ | Constraint { plazy :: Bool,

175+ pstatic :: Static }

174176 deriving (Show, Eq)

175177

176178impl = Imp False Dynamic

177179expl = Exp False Dynamic

180+constraint = Constraint False Static

178181

179182data PDecl' t = PFix FC Fixity [String] -- fixity declaration

180183 | PTy SyntaxInfo FC Name t -- type declaration

@@ -243,6 +246,7 @@ data PTerm = PQuote Raw

243246 | PTrue FC

244247 | PFalse FC

245248 | PRefl FC

249+ | PResolveTC FC

246250 | PEq FC PTerm PTerm

247251 | PPair FC PTerm PTerm

248252 | PDPair FC PTerm PTerm

@@ -292,10 +296,12 @@ type PDo = PDo' PTerm

292296

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

294298 | PExp { lazyarg :: Bool, getTm :: t }

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

295300 deriving (Show, Eq, Functor)

296301

297302pimp = PImp False

298303pexp = PExp False

304+pconst = PConstraint False

299305

300306type PArg = PArg' PTerm

301307

@@ -372,6 +378,11 @@ getExps [] = []

372378getExps (PExp _ tm : xs) = tm : getExps xs

373379getExps (_ : xs) = getExps xs

374380

381+getConsts :: [PArg] -> [PTerm]

382+getConsts [] = []

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

384+getConsts (_ : xs) = getConsts xs

385+

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

376387getAll = map getTm

377388

@@ -400,6 +411,8 @@ showImp impl tm = se 10 tm where

400411 where st = case s of

401412 Static -> "[static] "

402413 _ -> ""

414+ se p (PPi (Constraint _ _) n ty sc)

415+ = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc

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

404417 | not impl = show f

405418 se p (PApp _ (PRef _ op@(UN [f:_])) args)

@@ -407,11 +420,13 @@ showImp impl tm = se 10 tm where

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

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

409422 se p (PApp _ f as)

410− = let (imps, args) = (getImps as, getExps as) in

411− bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")

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

412426 ++ concatMap seArg args

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

414428 se p (PRefl _) = "refl"

429+ se p (PResolveTC _) = "resolvetc"

415430 se p (PTrue _) = "()"

416431 se p (PFalse _) = "_|_"

417432 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

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

425440

426441 seArg arg = " " ++ se 0 arg

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

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

428444

429445 bracket outer inner str | inner > outer = "(" ++ str ++ ")"

430446 | otherwise = str

@@ -626,6 +642,14 @@ implicitise syn ist tm

626642 put (PExp l ty : decls,

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

628644 imps True (n:env) sc

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

646+ = do let isn = nub (namesIn ist ty ++ case sc of

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

648+ _ -> [])

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

650+ put (PConstraint l ty : decls,

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

652+ imps True (n:env) sc

629653 imps top env (PEq _ l r)

630654 = do (decls, ns) <- get

631655 let isn = namesIn ist l ++ namesIn ist r

@@ -701,6 +725,10 @@ aiFn ist fc f as

701725 insertImpl :: [PArg] -> [PArg] -> [PArg]

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

703727 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

704732 insertImpl (PImp l n ty : ps) given =

705733 case find n given [] of

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

@@ -789,6 +817,7 @@ matchClause x y = match x y where

789817 mr <- match r r'

790818 return (ml ++ mr)

791819 match (PRefl _) (PRefl _) = return []

820+ match (PResolveTC _) (PResolveTC _) = return []

792821 match (PTrue _) (PTrue _) = return []

793822 match (PFalse _) (PFalse _) = return []

794823 match (PReturn _) (PReturn _) = return []

src/Idris/Delaborate.hs+1

@@ -45,6 +45,7 @@ delab ist tm = de [] tm

4545

4646 imp (PImp l n _) arg = PImp l n arg

4747 imp (PExp l _) arg = PExp l arg

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

4849

4950pshow :: IState -> Err -> String

5051pshow i (Msg s) = s

src/Idris/ElabDecls.hs+55−34

@@ -16,6 +16,7 @@ import Core.CaseTree

1616

1717import Control.Monad

1818import Control.Monad.State

19+import Data.List

1920import Debug.Trace

2021

2122-- Data to pass to recursively called elaborators; e.g. for where blocks,

@@ -104,14 +105,14 @@ elabClauses info fc n_in cs = let n = liftname info n_in in

104105 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

105106 depat x = x

106107

107−elabVal :: ElabInfo -> PTerm -> Idris (Term, Type)

108−elabVal info tm_in

108+elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

109+elabVal info aspat tm_in

109110 = do ctxt <- getContext

110111 i <- get

111112 let tm = addImpl i tm_in

112113 logLvl 10 (showImp True tm)

113114 ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP

114− (build i info True (infTerm tm))

115+ (build i info aspat (infTerm tm))

115116 logLvl 3 ("Value: " ++ show tm')

116117 let vtm = getInferTerm tm'

117118 logLvl 2 (show vtm)

@@ -360,27 +361,6 @@ elab ist info pattern tm

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

361362 [] -> return ()

362363

363− -- Expand implict arguments here, then move on to main elaborator

364−-- elabE (PRef fc n)

365−-- | Just ps <- lookupCtxt n (inblock info)

366−-- = -- let exp = (PApp fc (PRef fc n) (map (pexp . (PRef fc)) ps))

367−-- elabE (PApp fc (PRef fc n) [])

368−-- elabE f@(PApp fc fn args) = trace ("Elaborating " ++ show f) $ elab' f

369−-- elabE (PRef fc f)

370−-- = do l <- local f

371−-- elabN f l

372−-- where elabN f False = let afn = aiFn ist fc f [] in

373−-- -- trace ("Ref expanded to " ++ showImp True afn) $

374−-- elab' afn

375−-- elabN f True = elab' (PRef fc f)

376−-- elabE (PApp fc fn@(PRef _ f) args)

377−-- = do l <- local f

378−-- elabApp f args l -- no implicits

379−-- where elabApp f args False = let afn = aiFn ist fc f args in

380−-- -- trace ("Expanded to " ++ showImp True afn) $

381−-- elab' afn

382−-- elabApp f args True = elab' (PApp fc fn args)

383−-- elabE (PApp fc f as) = elab' (mkPApp fc 1 f as)

384364 elabE t = elab' t

385365

386366 local f = do e <- get_env

@@ -392,6 +372,8 @@ elab ist info pattern tm

392372 elab' (PTrue fc) = try (elab' (PRef fc unitCon))

393373 (elab' (PRef fc unitTy))

394374 elab' (PFalse fc) = elab' (PRef fc falseTy)

375+ elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

376+ instanceArg c

395377 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

396378 pimp (MN 0 "x") Placeholder])

397379 elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

@@ -452,11 +434,25 @@ elab ist info pattern tm

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

453435 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

454436 _ ->-} args'

437+ ivs <- get_instances

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

456439 solve

457440 elabArgs ns (map (\x -> (lazyarg x, getTm x)) args))

458441 (do apply_elab f (map toElab args)

459442 solve)

443+ ivs' <- get_instances

444+ when (not pattern) $

445+ mapM_ (\n -> do focus n

446+ resolveTC ist) (ivs' \\ ivs)

447+-- ivs <- get_instances

448+-- when (not (null ivs)) $

449+-- do t <- get_term

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

451+-- mapM_ (\n -> do focus n

452+-- resolveTC ist) ivs

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

454+ tcArg _ = False

455+

460456 elab' (PApp fc f [arg])

461457 = erun fc $

462458 do simple_app (elabE f) (elabE (getTm arg))

@@ -478,7 +474,40 @@ elab ist info pattern tm

478474 elabArgs ns args

479475 | otherwise

480476 = do focus n; elabE t; elabArgs ns args

481−

477+

478+trivial :: IState -> Elab ()

479+trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))

480+ (do env <- get_env

481+ tryAll (map fst env))

482+ where

483+ tryAll [] = fail "No trivial solution"

484+ tryAll (x:xs) = try (elab ist toplevel False (PRef (FC "prf" 0) x))

485+ (tryAll xs)

486+

487+resolveTC :: IState -> Elab ()

488+resolveTC ist = do t <- goal

489+ tm <- get_term

490+ try (trivial ist)

491+ (blunderbuss t (map fst (toAlist (tt_ctxt ist))))

492+ where

493+ blunderbuss t [] = fail $ "Can't resolve type class " ++ show t

494+ blunderbuss t (n:ns) | tcname n = try (resolve n)

495+ (blunderbuss t ns)

496+ | otherwise = blunderbuss t ns

497+ tcname (UN (('@':_) : _)) = True

498+ tcname _ = False

499+

500+ resolve n = do t <- goal

501+ let imps = case lookupCtxt n (idris_implicits ist) of

502+ Nothing -> []

503+ Just args -> map isImp args

504+ args <- apply (Var n) imps

505+ mapM_ (\ (_,n) -> do focus n

506+ resolveTC ist)

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

508+ solve

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

510+ isImp _ = False

482511

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

484513collectDeferred (Bind n (GHole t) app) =

@@ -531,15 +560,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

531560 rewrite (Var letn)

532561 when autoSolve solveAll

533562 runT Compute = compute

534− runT Trivial = try (do elab ist toplevel False (PRefl (FC "prf" 0))

535− when autoSolve solveAll)

536− (do env <- get_env

537− tryAll (map fst env))

538− where

539− tryAll [] = fail "No trivial solution"

540− tryAll (x:xs) = try (do elab ist toplevel False (PRef (FC "prf" 0) x)

541− when autoSolve solveAll)

542− (tryAll xs)

563+ runT Trivial = do trivial ist; when autoSolve solveAll

543564 runT (Focus n) = focus n

544565 runT Solve = solve

545566 runT x = fail $ "Not implemented " ++ show x

src/Idris/Parser.hs+29−6

@@ -335,7 +335,10 @@ pExt syn (Rule (s:ssym) ptm)

335335

336336pName = do i <- getState

337337 iName (syntax_keywords i)

338− where

338+ <|> do reserved "instance"

339+ i <- getState

340+ UN (n:ns) <- iName (syntax_keywords i)

341+ return (UN (('@':n) : ns))

339342

340343pfName = try pName

341344 <|> do lchar '('; o <- operator; lchar ')'; return (UN [o])

@@ -379,7 +382,8 @@ pApp syn = do f <- pSimpleExpr syn

379382 return (PApp fc f args)

380383

381384pArg :: SyntaxInfo -> IParser PArg

382−pArg syn = pImplicitArg syn

385+pArg syn = try (pImplicitArg syn)

386+ <|> try (pConstraintArg syn)

383387 <|> do e <- pSimpleExpr syn

384388 return (pexp e)

385389

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

389393 lchar '}'

390394 return (pimp n v)

391395

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

397+ return (pconst e)

398+

392399pTSig syn = do lchar ':'

393− pExpr syn

400+ cs <- pConstList syn

401+ sc <- pExpr syn

402+ return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

394403

395404pLambda syn = do lchar '\\';

396405 xt <- tyOptDeclList syn

@@ -422,6 +431,16 @@ pPi syn =

422431 sc <- pExpr syn

423432 return (PPi (Exp False Static) (MN 0 "X") t sc)

424433

434+pConstList :: SyntaxInfo -> IParser [PTerm]

435+pConstList syn = try (do lchar '('

436+ tys <- sepBy1 (pExpr' syn) (lchar ',')

437+ lchar ')'

438+ reservedOp "=>"

439+ return tys)

440+ <|> try (do t <- pExpr syn

441+ reservedOp "=>"

442+ return [t])

443+ <|> return []

425444

426445tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))

427446 (lchar ',')

@@ -548,6 +567,7 @@ whereSyn n syn args = let ns = concatMap allNamesIn args

548567pClause :: SyntaxInfo -> IParser PClause

549568pClause syn

550569 = try (do n <- pfName

570+ cargs <- many (pConstraintArg syn)

551571 iargs <- many (pImplicitArg syn)

552572 fc <- pfc

553573 args <- many (pHSimpleExpr syn)

@@ -556,12 +576,15 @@ pClause syn

556576 rhs <- pExpr syn

557577 ist <- getState

558578 let ctxt = tt_ctxt ist

559− let wsyn = whereSyn n syn (map getTm iargs ++ args ++ wargs)

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

580+ map getTm iargs ++

581+ args ++ wargs)

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

561583 return ([], [])]

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

563− (iargs ++ map pexp args)) wargs rhs wheres)

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

564586 <|> try (do n <- pfName

587+ cargs <- many (pConstraintArg syn)

565588 iargs <- many (pImplicitArg syn)

566589 fc <- pfc

567590 args <- many (pHSimpleExpr syn)

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

573596 let withs = concat ds

574597 lchar '}'

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

576− (iargs ++ map pexp args)) wargs wval withs)

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

577600

578601 <|> do l <- pSimpleExpr syn

579602 op <- operator

src/Idris/Prover.hs+2−2

@@ -48,8 +48,8 @@ elabStep st e = do case runStateT e st of

4848 fail (pshow i a)

4949

5050dumpState :: IState -> ProofState -> IO ()

51−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

52−dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ cyxy _ _)

51+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

52+dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ _ ctxy _ _)

5353 = do let OK ty = goalAtFocus ps

5454 let OK env = envAtFocus ps

5555 putStrLn $ "Other goals: " ++ show hs ++ "\n"

src/Idris/REPL.hs+3−3

@@ -77,7 +77,7 @@ process f Edit

7777 where getEditor env | Just ed <- lookup "EDITOR" env = ed

7878 | Just ed <- lookup "VISUAL" env = ed

7979 | otherwise = "vi"

80−process _ (Eval t) = do (tm, ty) <- elabVal toplevel t

80+process _ (Eval t) = do (tm, ty) <- elabVal toplevel False t

8181 ctxt <- getContext

8282 ist <- get

8383 let tm' = normaliseC ctxt [] tm

@@ -85,13 +85,13 @@ process _ (Eval t) = do (tm, ty) <- elabVal toplevel t

8585 logLvl 3 $ "Raw: " ++ show (tm', ty')

8686 iputStrLn (show (delab ist tm') ++ " : " ++

8787 show (delab ist ty'))

88−process _ (Spec t) = do (tm, ty) <- elabVal toplevel t

88+process _ (Spec t) = do (tm, ty) <- elabVal toplevel False t

8989 ctxt <- getContext

9090 ist <- get

9191 let tm' = specialise ctxt (idris_statics ist) tm

9292 iputStrLn (show (delab ist tm'))

9393process _ (Prove n) = prover n

94−process _ (HNF t) = do (tm, ty) <- elabVal toplevel t

94+process _ (HNF t) = do (tm, ty) <- elabVal toplevel False t

9595 ctxt <- getContext

9696 ist <- get

9797 let tm' = hnf ctxt [] tm