7384683 · Idris-dev · git.iko.soy

samples/interp.idr+26−19

@@ -13,18 +13,20 @@ using (G : Vect Ty n) {

1313 Nil : Env Nil

1414 | (::) : interpTy a -> Env G -> Env (a :: G);

1515

16− lookup : (i : Fin n) -> Env G -> interpTy (lookup i G);

17− lookup fO (x :: xs) = x;

18− lookup (fS i) (x :: xs) = lookup i xs;

19−

16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

17+ stop : HasType fO (t :: G) t

18+ | pop : HasType k G t -> HasType (fS k) (u :: G) t;

19+

20+ lookup : HasType i G t -> Env G -> interpTy t;

21+ lookup stop (x :: xs) = x;

22+ lookup (pop k) (x :: xs) = lookup k xs;

23+

2024 data Expr : Vect Ty n -> Ty -> Set where

21− Var : (i : Fin n) -> Expr G (lookup i G)

25+ Var : HasType i G t -> Expr G t

2226 | Val : (x : Int) -> Expr G TyInt

2327 | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

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

25− | Op : (Int -> Int -> interpTy c) ->

26− Expr G TyInt -> Expr G TyInt -> Expr G c

27− | Op' : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

29+ | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

2830 Expr G c

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

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

@@ -35,45 +37,50 @@ using (G : Vect Ty n) {

3537 interp env (Lam sc) = \x => interp (x :: env) sc;

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

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

38− interp env (Op' op x y) = op (interp env x) (interp env y);

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

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

4142

4243 eId : Expr G (TyFun TyInt TyInt);

43− eId = Lam (Var fO);

44+ eId = Lam (Var stop);

45+

46+ eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt));

47+ eTEST = Lam (Lam (Var (pop stop)));

4448

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

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

50+ eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))));

4751

4852-- eDouble : Expr G (TyFun TyInt TyInt);

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

5054

5155 eDouble : Expr G (TyFun TyInt TyInt);

52− eDouble = Lam (App (App eAdd (Var fO)) (Var fO));

56+ eDouble = Lam (App (App eAdd (Var stop)) (Var stop));

5357

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

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

5660

5761 eFac : Expr G (TyFun TyInt TyInt);

58− eFac = Lam (If (Op (==) (Var fO) (Val 0))

59− (Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)));

62+ eFac = Lam (If (Op (==) (Var stop) (Val 0))

63+ (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)));

6064

6165 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

6266

6367 eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));

6468 eProg = Lam (Lam

65− (Bind (App eDouble (Var (fS fO)))

66− (\x => Bind (App eDouble (Var fO))

69+ (Bind (App eDouble (Var (pop stop)))

70+ (\x => Bind (App eDouble (Var stop))

6771 (\y => Bind (App eDouble (Val x))

6872 (\z => App (App eAdd (Val y)) (Val z))))));

73+

6974}

7075

7176test : Int;

72−test = interp Nil eProg 2 2;

77+test = interp [] eProg 2 2;

7378

7479testFac : Int;

75−testFac = interp Nil eFac 4;

80+testFac = interp [] eFac 4;

7681

7782main : IO ();

78−main = print testFac;

83+main = do { print testFac;

84+ print test; };

85+

7986

src/Core/Elaborate.hs+20−10

@@ -223,6 +223,9 @@ instanceArg n = processTactic' (Instance n)

223223proofstate :: Elab ()

224224proofstate = processTactic' ProofState

225225

226+reorder_claims :: Name -> Elab ()

227+reorder_claims n = processTactic' (Reorder n)

228+

226229qed :: Elab Term

227230qed = do processTactic' QED

228231 ES p _ _ <- get

@@ -231,35 +234,41 @@ qed = do processTactic' QED

231234undo :: Elab ()

232235undo = processTactic' Undo

233236

234−prepare_apply :: Raw -> [Bool] -> Elab [Name]

237+prepare_apply :: Raw -> [(Bool, Int)] -> Elab [Name]

235238prepare_apply fn imps =

236239 do ty <- get_type fn

237240 ctxt <- get_context

238241 env <- get_env

239242 -- let claims = getArgs ty imps

240− claims <- doClaims (normalise ctxt env ty) imps []

243+ claims <- mkClaims (normalise ctxt env ty) imps []

241244 ES p s prev <- get

242245 -- reverse the claims we made so that args go left to right

243− let n = length (filter not imps)

246+ let n = length (filter not (map fst imps))

244247 let (h : hs) = holes p

245248 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }) s prev)

249+-- case claims of

250+-- [] -> return ()

251+-- (h : _) -> reorder_claims h

246252 return claims

247253 where

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

254+ mkClaims (Bind n' (Pi t) sc) (i : is) claims =

249255 do n <- unique_hole (mkMN n')

250− when (null claims) (start_unify n)

256+-- when (null claims) (start_unify n)

251257 let sc' = instantiate (P Bound n t) sc

252258 claim n (forget t)

253− when i (movelast n)

254− doClaims sc' is (n : claims)

255− doClaims t [] claims = return (reverse claims)

256− doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn

259+ when (fst i) (movelast n)

260+ mkClaims sc' is (n : claims)

261+ mkClaims t [] claims = return (reverse claims)

262+ mkClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn

263+

264+ doClaim ((i, _), n, t) = do claim n t

265+ when i (movelast n)

257266

258267 mkMN n@(MN _ _) = n

259268 mkMN n@(UN x) = MN 0 x

260269 mkMN (NS n xs) = NS (mkMN n) xs

261270

262−apply :: Raw -> [Bool] -> Elab [Name]

271+apply :: Raw -> [(Bool, Int)] -> Elab [Name]

263272apply fn imps =

264273 do args <- prepare_apply fn imps

265274 fill (raw_apply fn (map Var args))

@@ -267,6 +276,7 @@ apply fn imps =

267276 -- (remove from unified list before calling end_unify)

268277 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

269278 -- so do nothing

279+ ptm <- get_term

270280 let dontunify = [] -- map fst (filter (not.snd) (zip args imps))

271281 ES p s prev <- get

272282 let (n, hs) = unified p

src/Core/ProofState.hs+32−4

@@ -37,6 +37,7 @@ data Goal = GD { premises :: Env,

3737

3838data Tactic = Attack

3939 | Claim Name Raw

40+ | Reorder Name

4041 | Exact Raw

4142 | Fill Raw

4243 | PrepFill Name [Name]

@@ -181,6 +182,29 @@ claim n ty ctxt env t =

181182 ps { holes = g : n : gs } )

182183 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)

183184

185+reorder_claims :: RunTactic

186+reorder_claims ctxt env t

187+ = -- trace (showSep "\n" (map show (scvs t))) $

188+ let (bs, sc) = scvs t []

189+ newbs = reverse (sortB (reverse bs)) in

190+ traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $

191+ return (bindAll newbs sc)

192+ where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)

193+ scvs sc acc = (reverse acc, sc)

194+

195+ sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]

196+ sortB [] = []

197+ sortB (x:xs) | all (noOcc x) xs = x : sortB xs

198+ | otherwise = sortB (insertB x xs)

199+

200+ insertB x [] = [x]

201+ insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys

202+ | otherwise = y : insertB x ys

203+

204+ noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v

205+ noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v

206+ noOcc (n, _) (_, b) = noOccurrence n (binderTy b)

207+

184208focus :: Name -> RunTactic

185209focus n ctxt env t = do action (\ps -> let hs = holes ps in

186210 if n `elem` hs

@@ -231,6 +255,7 @@ exact _ _ _ _ = fail "Can't fill here."

231255fill :: Raw -> RunTactic

232256fill guess ctxt env (Bind x (Hole ty) sc) =

233257 do (val, valty) <- lift $ check ctxt env guess

258+ s <- get

234259 ns <- lift $ unify ctxt env valty ty

235260 ps <- get

236261 let (uh, uns) = unified ps

@@ -259,7 +284,9 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

259284solve :: RunTactic

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

261286 | pureTerm val = do ps <- get

287+ let (uh, uns) = unified ps

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

289+ -- unified = (uh, uns ++ [(x, val)]),

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

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

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

@@ -383,7 +410,7 @@ solve_unified ctxt env tm =

383410 do ps <- get

384411 let (_, ns) = unified ps

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

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

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

387414 return (updateSolved ns tm)

388415

389416updateSolved xs (Bind n (Hole ty) t)

@@ -411,12 +438,13 @@ processTactic EndUnify ps = let (h, ns) = unified ps

411438 return (ps { pterm = tm',

412439 unified = (h, []),

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

414− where

441+processTactic (Reorder n) ps

442+ = do ps' <- execStateT (tactic (Just n) reorder_claims) ps

443+ return (ps' { previous = Just ps, plog = "" }, plog ps')

415444processTactic t ps

416445 = case holes ps of

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

418− (h:_) -> do let n = nextname ps

419− ps' <- execStateT (process t h) ps

447+ (h:_) -> do ps' <- execStateT (process t h) ps

420448 return (ps' { previous = Just ps, plog = "" }, plog ps')

421449

422450process :: Tactic -> Name -> StateT TState TC ()

src/Core/ShellParser.hs+1−1

@@ -51,7 +51,7 @@ pTactic = do reserved "attack"; return attack

5151 <|> do reserved "exact"; tm <- pTerm; return (exact tm)

5252 <|> do reserved "fill"; tm <- pTerm; return (fill tm)

5353 <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;

54− return (discard (apply tm args))

54+ return (discard (apply tm (map (\x -> (x,0)) args)))

5555 <|> do reserved "solve"; return solve

5656 <|> do reserved "compute"; return compute

5757 <|> do reserved "intro"; n <- iName []; return (intro (Just n))

src/Idris/ElabTerm.hs+7−7

@@ -42,8 +42,8 @@ elab ist info pattern tm

4242 mkPat

4343 where

4444 isph arg = case getTm arg of

45− Placeholder -> True

46− _ -> False

45+ Placeholder -> (True, priority arg)

46+ _ -> (False, priority arg)

4747

4848 toElab arg = case getTm arg of

4949 Placeholder -> Nothing

@@ -283,10 +283,10 @@ resolveTC depth ist

283283 args <- apply (Var n) imps

284284 mapM_ (\ (_,n) -> do focus n

285285 resolveTC (depth - 1) ist)

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

286+ (filter (\ (x, y) -> not x) (zip (map fst imps) args))

287287 solve

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

289− isImp _ = False

288+ where isImp (PImp p _ _ _) = (True, p)

289+ isImp arg = (False, priority arg)

290290

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

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

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

322322 return (fn, a)

323323 -- FIXME: resolve ambiguities

324324 [(n, args)] -> return $ (n, map isImp args)

325− ns <- apply (Var fn') imps

325+ ns <- apply (Var fn') (map (\x -> (x,0)) imps)

326326 when autoSolve solveAll

327327 where isImp (PImp _ _ _ _) = True

328328 isImp _ = False

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

331331 Just t -> return $ map (const False)

332332 (getArgTys (binderTy t))

333333 _ -> return []

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

334+ runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)

335335 when autoSolve solveAll

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

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

test/test001/expected+1

@@ -1 +1,2 @@

1124

2+12

test/test001/test001.idr+28−20

@@ -13,19 +13,21 @@ using (G : Vect Ty n) {