07f12f9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Separate elaboration of declarations and terms

07f12f9Edwin Brady15 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -32,7 +32,7 @@ Executable idris

32 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

33 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

34 Idris.Delaborate, Idris.Primitives, Idris.Imports,

35− Idris.Compiler, Idris.Prover

35+ Idris.Compiler, Idris.Prover, Idris.ElabTerm

37 Paths_idris

src/Idris/ElabDecls.hs+24−331

@@ -6,6 +6,7 @@ import Idris.AbsSyntax

6import Idris.Error

7import Idris.Delaborate

8import Idris.Imports

9+import Idris.ElabTerm

9import Paths_idris

10import Paths_idris

11import Core.TT

12import Core.TT

@@ -19,22 +20,15 @@ import Control.Monad.State

19import Data.List

20import Data.List

20import Debug.Trace

21import Debug.Trace

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

23−-- paramaterised declarations, etc.

25−data ElabInfo = EInfo { params :: [(Name, PTerm)],

24+recheckC ctxt fc env t

26− inblock :: Ctxt [Name], -- names in the block, and their params

25+ = do (tm, ty, cs) <- tclift $ recheck ctxt env t

27− liftname :: Name -> Name }

26+ addConstraints fc cs

27+ return (tm, ty)

29−toplevel = EInfo [] emptyContext id

30−

31−recheckC ctxt env t = do (tm, ty, cs) <- tclift $ recheck ctxt env t

32− addConstraints cs

33− return (tm, ty)

34−

35−checkDef ns = do ctxt <- getContext

29+checkDef fc ns = do ctxt <- getContext

36− mapM (\(n, t) -> do (t', _) <- recheckC ctxt [] t

30+ mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t

37− return (n, t')) ns

31+ return (n, t')) ns

39elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris ()

33elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris ()

40elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

34elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

@@ -47,10 +41,10 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

47 logLvl 2 $ show n ++ " type " ++ showImp True ty

41 logLvl 2 $ show n ++ " type " ++ showImp True ty

48 ((ty', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

42 ((ty', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

49 (erun fc (build i info False ty))

43 (erun fc (build i info False ty))

50− (cty, _) <- recheckC ctxt [] ty'

44+ (cty, _) <- recheckC ctxt fc [] ty'

51 logLvl 2 $ "---> " ++ show cty

45 logLvl 2 $ "---> " ++ show cty

52 let nty = normalise ctxt [] cty

46 let nty = normalise ctxt [] cty

53− ds <- checkDef ((n, nty):defer)

47+ ds <- checkDef fc ((n, nty):defer)

54 addDeferred ds

48 addDeferred ds

56elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

50elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

@@ -63,9 +57,9 @@ elabData info syn fc (PDatadecl n t_in dcons)

63 let t = addImpl i t_in

57 let t = addImpl i t_in

64 ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

58 ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

65 (erun fc (build i info False t))

59 (erun fc (build i info False t))

66− def' <- checkDef defer

60+ def' <- checkDef fc defer

67 addDeferred def'

61 addDeferred def'

68− (cty, _) <- recheckC ctxt [] t'

62+ (cty, _) <- recheckC ctxt fc [] t'

69 logLvl 2 $ "---> " ++ show cty

63 logLvl 2 $ "---> " ++ show cty

70 updateContext (addTyDecl n cty) -- temporary, to check cons

64 updateContext (addTyDecl n cty) -- temporary, to check cons

71 cons <- mapM (elabCon info syn) dcons

65 cons <- mapM (elabCon info syn) dcons

@@ -83,10 +77,10 @@ elabCon info syn (n, t_in, fc)

83 ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

77 ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

84 (erun fc (build i info False t))

78 (erun fc (build i info False t))

85 logLvl 2 $ "Rechecking " ++ show t'

79 logLvl 2 $ "Rechecking " ++ show t'

86− def' <- checkDef defer

80+ def' <- checkDef fc defer

87 addDeferred def'

81 addDeferred def'

88 ctxt <- getContext

82 ctxt <- getContext

89− (cty, _) <- recheckC ctxt [] t'

83+ (cty, _) <- recheckC ctxt fc [] t'

90 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

84 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

91 return (n, cty)

85 return (n, cty)

@@ -122,7 +116,7 @@ elabVal info aspat tm_in

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

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

123 let vtm = getInferTerm tm'

117 let vtm = getInferTerm tm'

124 logLvl 2 (show vtm)

118 logLvl 2 (show vtm)

125− recheckC ctxt [] vtm

119+ recheckC ctxt (FC "prompt" 0) [] vtm

126

120

127elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)

121elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)

128elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

122elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

@@ -137,7 +131,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

137 let lhs_tm = orderPats (getInferTerm lhs')

131 let lhs_tm = orderPats (getInferTerm lhs')

138 let lhs_ty = getInferType lhs'

132 let lhs_ty = getInferType lhs'

139 logLvl 3 (show lhs_tm)

133 logLvl 3 (show lhs_tm)

140− (clhs, clhsty) <- recheckC ctxt [] lhs_tm

134+ (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm

141 logLvl 5 ("Checked " ++ show clhs)

135 logLvl 5 ("Checked " ++ show clhs)

142 -- Elaborate where block

136 -- Elaborate where block

143 ist <- getIState

137 ist <- getIState

@@ -164,10 +158,10 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

164 return $ runState (collectDeferred tt) [])

158 return $ runState (collectDeferred tt) [])

165 logLvl 2 $ "---> " ++ show rhs'

159 logLvl 2 $ "---> " ++ show rhs'

166 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

160 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

167− def' <- checkDef defer

161+ def' <- checkDef fc defer

168 addDeferred def'

162 addDeferred def'

169 ctxt <- getContext

163 ctxt <- getContext

170− (crhs, crhsty) <- recheckC ctxt [] rhs'

164+ (crhs, crhsty) <- recheckC ctxt fc [] rhs'

171 return (clhs, crhs)

165 return (clhs, crhs)

172 where

166 where

173 decorate x = UN (show fname ++ "#" ++ show x)

167 decorate x = UN (show fname ++ "#" ++ show x)

@@ -197,7 +191,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

197 let lhs_ty = getInferType lhs'

191 let lhs_ty = getInferType lhs'

198 let ret_ty = getRetTy lhs_ty

192 let ret_ty = getRetTy lhs_ty

199 logLvl 3 (show lhs_tm)

193 logLvl 3 (show lhs_tm)

200− (clhs, clhsty) <- recheckC ctxt [] lhs_tm

194+ (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm

201 logLvl 5 ("Checked " ++ show clhs)

195 logLvl 5 ("Checked " ++ show clhs)

202 let bargs = getPBtys lhs_tm

196 let bargs = getPBtys lhs_tm

203 let wval = addImpl i wval_in

197 let wval = addImpl i wval_in

@@ -212,9 +206,9 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

212 psolve lhs_tm

206 psolve lhs_tm

213 tt <- get_term

207 tt <- get_term

214 return (tt, d))

208 return (tt, d))

215− def' <- checkDef defer

209+ def' <- checkDef fc defer

216 addDeferred def'

210 addDeferred def'

217− (cwval, cwvalty) <- recheckC ctxt [] (getInferTerm wval')

211+ (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')

218 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

212 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

219 windex <- getName

213 windex <- getName

220 -- build a type declaration for the new function:

214 -- build a type declaration for the new function:

@@ -224,7 +218,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

224 let wname = MN windex (show fname)

218 let wname = MN windex (show fname)

225 let imps = getImps wtype -- add to implicits context

219 let imps = getImps wtype -- add to implicits context

226 put (i { idris_implicits = addDef wname imps (idris_implicits i) })

220 put (i { idris_implicits = addDef wname imps (idris_implicits i) })

227− def' <- checkDef [(wname, wtype)]

221+ def' <- checkDef fc [(wname, wtype)]

228 addDeferred def'

222 addDeferred def'

229

223

230 -- in the subdecls, lhs becomes:

224 -- in the subdecls, lhs becomes:

@@ -247,9 +241,9 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

247 psolve lhs_tm

241 psolve lhs_tm

248 tt <- get_term

242 tt <- get_term

249 return (tt, d))

243 return (tt, d))

250− def' <- checkDef defer

244+ def' <- checkDef fc defer

251 addDeferred def'

245 addDeferred def'

252− (crhs, crhsty) <- recheckC ctxt [] rhs'

246+ (crhs, crhsty) <- recheckC ctxt fc [] rhs'

253 return (clhs, crhs)

247 return (clhs, crhs)

254 where

248 where

255 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

249 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

@@ -485,304 +479,3 @@ elabDecl' info (PDirective i) = i

485-- elabDecl' info (PImport i) = loadModule i

479-- elabDecl' info (PImport i) = loadModule i

486

480

487

481

488−-- Using the elaborator, convert a term in raw syntax to a fully

489−-- elaborated, typechecked term.

490−--

491−-- If building a pattern match, we convert undeclared variables from

492−-- holes to pattern bindings.

493−

494−-- Also find deferred names in the term and their types

495−

496−build :: IState -> ElabInfo -> Bool -> PTerm -> Elab (Term, [(Name, Type)])

497−build ist info pattern tm

498− = do elab ist info pattern tm

499− tt <- get_term

500− return $ runState (collectDeferred tt) []

501−

502−elab :: IState -> ElabInfo -> Bool -> PTerm -> Elab ()

503−elab ist info pattern tm

504− = do elabE tm

505− when pattern -- convert remaining holes to pattern vars

506− mkPat

507− where

508− isph arg = case getTm arg of

509− Placeholder -> True

510− _ -> False

511−

512− toElab arg = case getTm arg of

513− Placeholder -> Nothing

514− v -> Just (priority arg, elabE v)

515−

516− mkPat = do hs <- get_holes

517− case hs of

518− (h: hs) -> do patvar h; mkPat

519− [] -> return ()

520−

521− elabE t = {- do g <- goal

522− tm <- get_term

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

524− $ -} elab' t

525−

526− local f = do e <- get_env

527− return (f `elem` map fst e)

528−

529− elab' PSet = do fill RSet; solve

530− elab' (PConstant c) = do apply (RConstant c) []; solve

531− elab' (PQuote r) = do fill r; solve

532− elab' (PTrue fc) = try (elab' (PRef fc unitCon))

533− (elab' (PRef fc unitTy))

534− elab' (PFalse fc) = elab' (PRef fc falseTy)

535− elab' (PResolveTC (FC "HACK" _))

536− = resolveTC 10 ist

537− elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

538− instanceArg c

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

540− pimp (MN 0 "x") Placeholder])

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

542− pimp (MN 0 "b") Placeholder,

543− pexp l, pexp r])

544− elab' (PPair fc l r) = try (elabE (PApp fc (PRef fc pairTy)

545− [pexp l,pexp r]))

546− (elabE (PApp fc (PRef fc pairCon)

547− [pimp (MN 0 "A") Placeholder,

548− pimp (MN 0 "B") Placeholder,

549− pexp l, pexp r]))

550− elab' (PDPair fc l@(PRef _ n) t r)

551− = case t of

552− Placeholder -> try asType asValue

553− _ -> asType

554− where asType = elab' (PApp fc (PRef fc sigmaTy)

555− [pexp t,

556− pexp (PLam n Placeholder r)])

557− asValue = elab' (PApp fc (PRef fc existsCon)

558− [pimp (MN 0 "a") t,

559− pimp (MN 0 "P") Placeholder,

560− pexp l, pexp r])

561− elab' (PDPair fc l t r) = elab' (PApp fc (PRef fc existsCon)

562− [pimp (MN 0 "a") t,

563− pimp (MN 0 "P") Placeholder,

564− pexp l, pexp r])

565− elab' (PRef fc n) | pattern && not (inparamBlock n)

566− = do ctxt <- get_context

567− let sc = case lookupTy n ctxt of

568− Nothing -> True

569− _ -> False

570− if sc

571− then erun fc $

572− try (do apply (Var n) []; solve)

573− (patvar n)

574− else do apply (Var n) []; solve

575− where inparamBlock n = case lookupCtxt n (inblock info) of

576− Nothing -> False

577− _ -> True

578− elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve

579− elab' (PLam n Placeholder sc)

580− = do attack; intro (Just n); elabE sc; solve

581− elab' (PLam n ty sc)

582− = do tyn <- unique_hole (MN 0 "lamty")

583− claim tyn RSet

584− attack

585− introTy (Var tyn) (Just n)

586− -- end_unify

587− focus tyn

588− elabE ty

589− elabE sc

590− solve

591− elab' (PPi _ n Placeholder sc)

592− = do attack; arg n (MN 0 "ty"); elabE sc; solve

593− elab' (PPi _ n ty sc)

594− = do attack; tyn <- unique_hole (MN 0 "ty")

595− claim tyn RSet

596− n' <- case n of

597− MN _ _ -> unique_hole n

598− _ -> return n

599− forall n' (Var tyn)

600− focus tyn

601− elabE ty

602− elabE sc

603− solve

604− elab' (PLet n ty val sc)

605− = do attack;

606− tyn <- unique_hole (MN 0 "letty")

607− claim tyn RSet

608− valn <- unique_hole (MN 0 "letval")

609− claim valn (Var tyn)

610− letbind n (Var tyn) (Var valn)

611− case ty of

612− Placeholder -> return ()

613− _ -> do focus tyn

614− elabE ty

615− focus valn

616− elabE val

617− elabE sc

618− solve

619− elab' (PApp fc (PRef _ f) args')

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

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

622− _ ->-} args'

623− ivs <- get_instances

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

625− solve

626− let (ns', eargs)

627− = unzip $

628− sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))

629− (zip ns args)

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

631− (do apply_elab f (map toElab args)

632− solve)

633− ivs' <- get_instances

634− when (not pattern) $

635− mapM_ (\n -> do focus n

636− resolveTC 10 ist) (ivs' \\ ivs)

637−-- ivs <- get_instances

638−-- when (not (null ivs)) $

639−-- do t <- get_term

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

641−-- mapM_ (\n -> do focus n

642−-- resolveTC ist) ivs

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

644− tcArg _ = False

645−

646− elab' (PApp fc f [arg])

647− = erun fc $

648− do simple_app (elabE f) (elabE (getTm arg))

649− solve

650− elab' Placeholder = do (h : hs) <- get_holes

651− movelast h

652− elab' (PMetavar n) = do attack; defer n; solve

653− elab' (PProof ts) = do mapM_ (runTac True ist) ts

654− elab' (PTactics ts) = do mapM_ (runTac False ist) ts

655− elab' (PElabError e) = fail e

656− elab' x = fail $ "Not implemented " ++ show x

657−

658− elabArgs failed retry [] _

659− | retry = let (ns, ts) = unzip (reverse failed) in

660− elabArgs [] False ns ts

661− | otherwise = return ()

662− elabArgs failed r (n:ns) ((_, Placeholder) : args)

663− = elabArgs failed r ns args

664− elabArgs failed r (n:ns) ((lazy, t) : args)

665− | lazy && not pattern

666− = do elabArg n (PApp bi (PRef bi (UN "lazy"))

667− [pimp (UN "a") Placeholder,

668− pexp t]);

669− | otherwise = elabArg n t

670− where elabArg n t = if r

671− then try (do focus n; elabE t; elabArgs failed r ns args)

672− (elabArgs ((n,(lazy, t)):failed) r ns args)

673− else do focus n; elabE t; elabArgs failed r ns args

674−

675−trivial :: IState -> Elab ()

676−trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))

677− (do env <- get_env

678− tryAll (map fst env))

679− where

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

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

682− (tryAll xs)

683−

684−resolveTC :: Int -> IState -> Elab ()

685−resolveTC depth ist

686− = do t <- goal

687− tm <- get_term

688− try (trivial ist)

689− (blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))

690− where

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

692− blunderbuss t (n:ns) | tcname n = try (resolve n depth)

693− (blunderbuss t ns)

694− | otherwise = blunderbuss t ns

695− tcname (UN ('@':_)) = True

696− tcname (NS _ n) = tcname n

697− tcname _ = False

698−

699− resolve n depth

700− | depth == 0 = fail $ "Can't resolve type class"

701− | otherwise

702− = do t <- goal

703− let imps = case lookupCtxt n (idris_implicits ist) of

704− Nothing -> []

705− Just args -> map isImp args

706− args <- apply (Var n) imps

707− mapM_ (\ (_,n) -> do focus n

708− resolveTC (depth - 1) ist)

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

710− solve

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

712− isImp _ = False

713−

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

715−collectDeferred (Bind n (GHole t) app) =

716− do ds <- get

717− put ((n, t) : ds)

718− return app

719−collectDeferred (Bind n b t) = do b' <- cdb b

720− t' <- collectDeferred t

721− return (Bind n b' t')

722− where

723− cdb (Let t v) = liftM2 Let (collectDeferred t) (collectDeferred v)

724− cdb (Guess t v) = liftM2 Guess (collectDeferred t) (collectDeferred v)

725− cdb b = do ty' <- collectDeferred (binderTy b)

726− return (b { binderTy = ty' })

727−collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

728−collectDeferred t = return t

729−

730−-- Running tactics directly

731−

732−runTac :: Bool -> IState -> PTactic -> Elab ()

733−runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

734− runT (Intro []) = do g <- goal

735− attack; intro (bname g)

736− where

737− bname (Bind n _ _) = Just n

738− bname _ = Nothing

739− runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

740− runT (Exact tm) = do elab ist toplevel False tm

741− when autoSolve solveAll

742− runT (Refine fn []) = do imps <- case lookupCtxt fn (idris_implicits ist) of

743− Nothing -> envArgs fn

744− Just args -> return $ map isImp args

745− ns <- apply (Var fn) imps

746− when autoSolve solveAll

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

748− isImp _ = False

749− envArgs n = do e <- get_env

750− case lookup n e of

751− Just t -> return $ map (const False)

752− (getArgTys (binderTy t))

753− _ -> return []

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

755− when autoSolve solveAll

756− runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

757− = do attack; -- (h:_) <- get_holes

758− tyn <- unique_hole (MN 0 "rty")

759− -- start_unify h

760− claim tyn RSet

761− valn <- unique_hole (MN 0 "rval")

762− claim valn (Var tyn)

763− letn <- unique_hole (MN 0 "rewrite_rule")

764− letbind letn (Var tyn) (Var valn)

765− focus valn

766− elab ist toplevel False tm

767− rewrite (Var letn)

768− when autoSolve solveAll

769− runT (LetTac n tm)

770− = do attack

771− tyn <- unique_hole (MN 0 "letty")

772− claim tyn RSet

773− valn <- unique_hole (MN 0 "letval")

774− claim valn (Var tyn)

775− letn <- unique_hole n

776− letbind letn (Var tyn) (Var valn)

777− focus valn

778− elab ist toplevel False tm

779− when autoSolve solveAll

780− runT Compute = compute

781− runT Trivial = do trivial ist; when autoSolve solveAll

782− runT (Focus n) = focus n

783− runT Solve = solve

784− runT (Try l r) = do try (runT l) (runT r)

785− runT (TSeq l r) = do runT l; runT r

786− runT x = fail $ "Not implemented " ++ show x

787−

788−solveAll = try (do solve; solveAll) (return ())

src/Idris/ElabTerm.hsnew file+322

@@ -0,0 +1,322 @@

1+module Idris.ElabTerm where

3+import Idris.AbsSyntax

5+import Core.Elaborate hiding (Tactic(..))

6+import Core.TT

7+import Core.Evaluate

9+import Control.Monad

10+import Control.Monad.State

11+import Data.List

12+

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

14+-- paramaterised declarations, etc.

15+

16+data ElabInfo = EInfo { params :: [(Name, PTerm)],

17+ inblock :: Ctxt [Name], -- names in the block, and their params

18+ liftname :: Name -> Name }

19+

20+toplevel = EInfo [] emptyContext id

21+

22+-- Using the elaborator, convert a term in raw syntax to a fully

23+-- elaborated, typechecked term.

24+--

25+-- If building a pattern match, we convert undeclared variables from

26+-- holes to pattern bindings.

27+

28+-- Also find deferred names in the term and their types

29+

30+build :: IState -> ElabInfo -> Bool -> PTerm -> Elab (Term, [(Name, Type)])

31+build ist info pattern tm

32+ = do elab ist info pattern tm

33+ tt <- get_term

34+ return $ runState (collectDeferred tt) []

35+

36+elab :: IState -> ElabInfo -> Bool -> PTerm -> Elab ()

37+elab ist info pattern tm

38+ = do elabE tm

39+ when pattern -- convert remaining holes to pattern vars

40+ mkPat

41+ where

42+ isph arg = case getTm arg of

43+ Placeholder -> True

44+ _ -> False

45+

46+ toElab arg = case getTm arg of

47+ Placeholder -> Nothing

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

49+

50+ mkPat = do hs <- get_holes

51+ case hs of

52+ (h: hs) -> do patvar h; mkPat

53+ [] -> return ()

54+

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

56+ tm <- get_term

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

58+ $ -} elab' t

59+

60+ local f = do e <- get_env

61+ return (f `elem` map fst e)

62+

63+ elab' PSet = do fill RSet; solve

64+ elab' (PConstant c) = do apply (RConstant c) []; solve

65+ elab' (PQuote r) = do fill r; solve

66+ elab' (PTrue fc) = try (elab' (PRef fc unitCon))

67+ (elab' (PRef fc unitTy))

68+ elab' (PFalse fc) = elab' (PRef fc falseTy)

69+ elab' (PResolveTC (FC "HACK" _))

70+ = resolveTC 10 ist

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

72+ instanceArg c

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

74+ pimp (MN 0 "x") Placeholder])

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

76+ pimp (MN 0 "b") Placeholder,

77+ pexp l, pexp r])

78+ elab' (PPair fc l r) = try (elabE (PApp fc (PRef fc pairTy)

79+ [pexp l,pexp r]))

80+ (elabE (PApp fc (PRef fc pairCon)

81+ [pimp (MN 0 "A") Placeholder,

82+ pimp (MN 0 "B") Placeholder,

83+ pexp l, pexp r]))

84+ elab' (PDPair fc l@(PRef _ n) t r)

85+ = case t of

86+ Placeholder -> try asType asValue

87+ _ -> asType

88+ where asType = elab' (PApp fc (PRef fc sigmaTy)

89+ [pexp t,

90+ pexp (PLam n Placeholder r)])

91+ asValue = elab' (PApp fc (PRef fc existsCon)

92+ [pimp (MN 0 "a") t,

93+ pimp (MN 0 "P") Placeholder,

94+ pexp l, pexp r])

95+ elab' (PDPair fc l t r) = elab' (PApp fc (PRef fc existsCon)

96+ [pimp (MN 0 "a") t,

97+ pimp (MN 0 "P") Placeholder,

98+ pexp l, pexp r])

99+ elab' (PRef fc n) | pattern && not (inparamBlock n)

100+ = do ctxt <- get_context

101+ let sc = case lookupTy n ctxt of

102+ Nothing -> True

103+ _ -> False

104+ if sc

105+ then erun fc $

106+ try (do apply (Var n) []; solve)

107+ (patvar n)

108+ else do apply (Var n) []; solve

109+ where inparamBlock n = case lookupCtxt n (inblock info) of

110+ Nothing -> False

111+ _ -> True

112+ elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve

113+ elab' (PLam n Placeholder sc)

114+ = do attack; intro (Just n); elabE sc; solve

115+ elab' (PLam n ty sc)

116+ = do tyn <- unique_hole (MN 0 "lamty")

117+ claim tyn RSet

118+ attack

119+ introTy (Var tyn) (Just n)

120+ -- end_unify

121+ focus tyn

122+ elabE ty

123+ elabE sc

124+ solve

125+ elab' (PPi _ n Placeholder sc)

126+ = do attack; arg n (MN 0 "ty"); elabE sc; solve

127+ elab' (PPi _ n ty sc)

128+ = do attack; tyn <- unique_hole (MN 0 "ty")

129+ claim tyn RSet

130+ n' <- case n of

131+ MN _ _ -> unique_hole n

132+ _ -> return n

133+ forall n' (Var tyn)

134+ focus tyn

135+ elabE ty

136+ elabE sc

137+ solve

138+ elab' (PLet n ty val sc)

139+ = do attack;

140+ tyn <- unique_hole (MN 0 "letty")

141+ claim tyn RSet

142+ valn <- unique_hole (MN 0 "letval")

143+ claim valn (Var tyn)

144+ letbind n (Var tyn) (Var valn)

145+ case ty of

146+ Placeholder -> return ()

147+ _ -> do focus tyn

148+ elabE ty

149+ focus valn

150+ elabE val

151+ elabE sc

152+ solve

153+ elab' (PApp fc (PRef _ f) args')

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

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

156+ _ ->-} args'

157+ ivs <- get_instances

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

159+ solve

160+ let (ns', eargs)

161+ = unzip $

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

163+ (zip ns args)

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

165+ (do apply_elab f (map toElab args)

166+ solve)

167+ ivs' <- get_instances

168+ when (not pattern) $

169+ mapM_ (\n -> do focus n

170+ resolveTC 10 ist) (ivs' \\ ivs)

171+-- ivs <- get_instances

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

173+-- do t <- get_term

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

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

176+-- resolveTC ist) ivs

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

178+ tcArg _ = False

179+

180+ elab' (PApp fc f [arg])

181+ = erun fc $

182+ do simple_app (elabE f) (elabE (getTm arg))

183+ solve

184+ elab' Placeholder = do (h : hs) <- get_holes

185+ movelast h

186+ elab' (PMetavar n) = do attack; defer n; solve

187+ elab' (PProof ts) = do mapM_ (runTac True ist) ts

188+ elab' (PTactics ts) = do mapM_ (runTac False ist) ts

189+ elab' (PElabError e) = fail e

190+ elab' x = fail $ "Not implemented " ++ show x

191+

192+ elabArgs failed retry [] _

193+ | retry = let (ns, ts) = unzip (reverse failed) in

194+ elabArgs [] False ns ts

195+ | otherwise = return ()

196+ elabArgs failed r (n:ns) ((_, Placeholder) : args)

197+ = elabArgs failed r ns args

198+ elabArgs failed r (n:ns) ((lazy, t) : args)

199+ | lazy && not pattern

200+ = do elabArg n (PApp bi (PRef bi (UN "lazy"))

201+ [pimp (UN "a") Placeholder,

202+ pexp t]);

203+ | otherwise = elabArg n t

204+ where elabArg n t = if r

205+ then try (do focus n; elabE t; elabArgs failed r ns args)

206+ (elabArgs ((n,(lazy, t)):failed) r ns args)

207+ else do focus n; elabE t; elabArgs failed r ns args

208+

209+trivial :: IState -> Elab ()

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

211+ (do env <- get_env

212+ tryAll (map fst env))

213+ where

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

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

216+ (tryAll xs)

217+

218+resolveTC :: Int -> IState -> Elab ()

219+resolveTC depth ist

220+ = do t <- goal

221+ tm <- get_term

222+ try (trivial ist)

223+ (blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))

224+ where

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

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

227+ (blunderbuss t ns)

228+ | otherwise = blunderbuss t ns

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

230+ tcname (NS _ n) = tcname n

231+ tcname _ = False

232+

233+ resolve n depth

234+ | depth == 0 = fail $ "Can't resolve type class"

235+ | otherwise

236+ = do t <- goal

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

238+ Nothing -> []

239+ Just args -> map isImp args

240+ args <- apply (Var n) imps

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

242+ resolveTC (depth - 1) ist)

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

244+ solve

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

246+ isImp _ = False

247+

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

249+collectDeferred (Bind n (GHole t) app) =

250+ do ds <- get

251+ put ((n, t) : ds)

252+ return app

253+collectDeferred (Bind n b t) = do b' <- cdb b

254+ t' <- collectDeferred t

255+ return (Bind n b' t')

256+ where

257+ cdb (Let t v) = liftM2 Let (collectDeferred t) (collectDeferred v)

258+ cdb (Guess t v) = liftM2 Guess (collectDeferred t) (collectDeferred v)

259+ cdb b = do ty' <- collectDeferred (binderTy b)

260+ return (b { binderTy = ty' })

261+collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

262+collectDeferred t = return t

263+

264+-- Running tactics directly

265+

266+runTac :: Bool -> IState -> PTactic -> Elab ()

267+runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

268+ runT (Intro []) = do g <- goal

269+ attack; intro (bname g)

270+ where

271+ bname (Bind n _ _) = Just n

272+ bname _ = Nothing

273+ runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

274+ runT (Exact tm) = do elab ist toplevel False tm

275+ when autoSolve solveAll

276+ runT (Refine fn []) = do imps <- case lookupCtxt fn (idris_implicits ist) of

277+ Nothing -> envArgs fn

278+ Just args -> return $ map isImp args

279+ ns <- apply (Var fn) imps

280+ when autoSolve solveAll

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

282+ isImp _ = False

283+ envArgs n = do e <- get_env

284+ case lookup n e of

285+ Just t -> return $ map (const False)

286+ (getArgTys (binderTy t))

287+ _ -> return []

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

289+ when autoSolve solveAll

290+ runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

291+ = do attack; -- (h:_) <- get_holes

292+ tyn <- unique_hole (MN 0 "rty")

293+ -- start_unify h

294+ claim tyn RSet

295+ valn <- unique_hole (MN 0 "rval")

296+ claim valn (Var tyn)

297+ letn <- unique_hole (MN 0 "rewrite_rule")

298+ letbind letn (Var tyn) (Var valn)

299+ focus valn

300+ elab ist toplevel False tm

301+ rewrite (Var letn)

302+ when autoSolve solveAll

303+ runT (LetTac n tm)

304+ = do attack

305+ tyn <- unique_hole (MN 0 "letty")

306+ claim tyn RSet

307+ valn <- unique_hole (MN 0 "letval")

308+ claim valn (Var tyn)

309+ letn <- unique_hole n

310+ letbind letn (Var tyn) (Var valn)

311+ focus valn

312+ elab ist toplevel False tm

313+ when autoSolve solveAll

314+ runT Compute = compute

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

316+ runT (Focus n) = focus n

317+ runT Solve = solve

318+ runT (Try l r) = do try (runT l) (runT r)

319+ runT (TSeq l r) = do runT l; runT r

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

321+

322+solveAll = try (do solve; solveAll) (return ())

src/Idris/Parser.hs+1

@@ -4,6 +4,7 @@ import Idris.AbsSyntax

4import Idris.Imports

5import Idris.Error

6import Idris.ElabDecls

7+import Idris.ElabTerm

7import Paths_idris

8import Paths_idris

9import Core.CoreParser

10import Core.CoreParser

src/Idris/Primitives.hs+1

@@ -3,6 +3,7 @@

3module Idris.Primitives(elabPrims) where

5import Idris.ElabDecls

6+import Idris.ElabTerm

6import Idris.AbsSyntax

7import Idris.AbsSyntax

8import Core.TT

9import Core.TT

src/Idris/Prover.hs+2−1

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

9import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.ElabDecls

12+import Idris.ElabTerm

12import Idris.Parser

13import Idris.Parser

13import Idris.Error

14import Idris.Error

@@ -37,7 +38,7 @@ prove ctxt n ty

37 lift $ dumpProof n prf

38 lift $ dumpProof n prf

38 let tree = simpleCase False [(P Ref n ty, tm)]

39 let tree = simpleCase False [(P Ref n ty, tm)]

39 logLvl 3 (show tree)

40 logLvl 3 (show tree)

40− (ptm, pty) <- recheckC ctxt [] tm

41+ (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm

41 updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)

42 updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)

42 solveDeferred n

43 solveDeferred n

src/Idris/REPL.hs+5−3

@@ -6,6 +6,7 @@ module Idris.REPL where

6import Idris.AbsSyntax

7import Idris.REPLParser

8import Idris.ElabDecls

9+import Idris.ElabTerm

9import Idris.Error

10import Idris.Error

10import Idris.Delaborate

11import Idris.Delaborate

11import Idris.Compiler

12import Idris.Compiler

@@ -110,9 +111,10 @@ process (Check t) = do (tm, ty) <- elabVal toplevel False t

110 let ty' = normaliseC ctxt [] ty

111 let ty' = normaliseC ctxt [] ty

111 iputStrLn (showImp imp (delab ist tm) ++ " : " ++

112 iputStrLn (showImp imp (delab ist tm) ++ " : " ++

112 showImp imp (delab ist ty))

113 showImp imp (delab ist ty))

113−process Universes = do ctxt <- getContext

114+process Universes = do i <- get

114− let cs = nub $ uconstraints ctxt

115+ let cs = nub $ idris_constraints i

116+-- iputStrLn $ showSep "\n" (map show cs)

115− lift $ print cs

117+ lift $ print (map fst cs)

116 iputStrLn $ "(" ++ show (length cs) ++ " constraints)"

118 iputStrLn $ "(" ++ show (length cs) ++ " constraints)"

117process (Defn n) = do ctxt <- getContext

119process (Defn n) = do ctxt <- getContext

118 lift $ print (lookupDef n ctxt)

120 lift $ print (lookupDef n ctxt)