50c66f9 · Idris-dev · git.iko.soy

effects/Effects.idr+8−21

compare with master

unifiedsplit

@@ -146,27 +146,14 @@ effect' : {a, b: _} -> {e : Effect} ->

146 EffM m xs (updateResTy xs prf eff) t

147effect' {prf} e = effect prf e

148

149−data WrapEffM : (m : Type -> Type) ->

149+-- For making proofs implicitly for 'test' and 'test_lbl'

150− List EFFECT -> List EFFECT -> Type -> Type where

150+

151− WEffM : EffM m xs xs' t -> WrapEffM m xs xs' t

151+syntax if_valid then [e] else [t] =

152−

153−-- wrap subprograms to prevent lifting (need to guarantee same effects as

154−-- parent!)

155−

156−test_lbl' : {x : lbl} ->

157− {default tactics { applyTactic findEffElem 20; solve; }

152+ test (tactics { applyTactic findEffElem 20; solve; }) t e

158− prf : EffElem e (LRes x (Either l r)) xs} ->

153+

159− WrapEffM m (updateResTyImm xs prf (LRes x l)) xs' t ->

154+syntax if_valid [lbl] then [e] else [t] =

160− WrapEffM m (updateResTyImm xs prf (LRes x r)) xs' t ->

161− EffM m xs xs' t

162−test_lbl' {prf} (WEffM l) (WEffM r) = test_lbl prf l r

163−

164−test' : {default tactics { applyTactic findEffElem 20; solve; }

155+ test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e

165− prf : EffElem e (Either l r) xs} ->

156+

166− EffM m (updateResTyImm xs prf l) xs' t ->

167− EffM m (updateResTyImm xs prf r) xs' t ->

168− EffM m xs xs' t

169−test' {prf} l r = test prf l r

170

157

171-- for 'do' notation

158-- for 'do' notation

172

159

src/Idris/AbsSyntaxTree.hs−1

@@ -657,7 +657,6 @@ type PDo = PDo' PTerm

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

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

659-- variables, e.g. a before (interpTy a).

660−-- TODO: priority no longer serves any purpose, drop it!

661

660

662data PArg' t = PImp { priority :: Int,

661data PArg' t = PImp { priority :: Int,

663 machine_inf :: Bool, -- true if the machine inferred it

662 machine_inf :: Bool, -- true if the machine inferred it

src/Idris/ElabTerm.hs+3

@@ -393,6 +393,7 @@ elab ist info pattern tcgen fn tm

393 ns <- apply (Var f) (map isph args)

394 ptm <- get_term

395 g <- goal

396+ -- Sort so that the implicit tactics go last

396 let (ns', eargs) = unzip $

397 let (ns', eargs) = unzip $

397 sortBy (\(_,x) (_,y) ->

398 sortBy (\(_,x) (_,y) ->

398 compare (priority x) (priority y))

399 compare (priority x) (priority y))

@@ -942,6 +943,8 @@ runTac autoSolve ist tac

942 then runT tac

943 then runT tac

943 else fail "Wrong goal type"

944 else fail "Wrong goal type"

944 _ -> fail "Wrong goal type"

945 _ -> fail "Wrong goal type"

946+ runT ProofState = do g <- goal

947+ trace (show g) $ return ()

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

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

946

949

947 runReflected t = do t' <- reify ist t

950 runReflected t = do t' <- reify ist t

src/Idris/Parser.hs+1−1

@@ -797,7 +797,7 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

797 <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;

798 return [PDirective (do addHdr cgn hdr

799 addIBC (IBCHeader cgn hdr))]

800− <|> do try (lchar '%' *> reserved "hide"); n <- iName []

800+ <|> do try (lchar '%' *> reserved "hide"); n <- fnName

801 return [PDirective (do setAccessibility n Hidden

802 addIBC (IBCAccess n Hidden))]

803 <|> do try (lchar '%' *> reserved "freeze"); n <- iName []