7384683 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fiddle with elaborator; update interp sample and test

7384683Edwin Brady15 years ago

samples/interp.idr+26−19

compare with master

unifiedsplit

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

13 Nil : Env Nil

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

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

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

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

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;

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

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

19−

23+

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

24 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

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

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

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

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

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

28 | 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 ->

28 Expr G c

30 Expr G c

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

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

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

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

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

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

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

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

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

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

39 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);

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

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

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

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

42 eId : Expr G (TyFun TyInt TyInt);

43 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)));

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

49 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))));

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

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

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

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

51 eDouble : Expr G (TyFun TyInt TyInt);

55 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));

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

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

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

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

57 eFac : Expr G (TyFun TyInt TyInt);

61 eFac : Expr G (TyFun TyInt TyInt);

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

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

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

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

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

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

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

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

64 eProg = Lam (Lam

68 eProg = Lam (Lam

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

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

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

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

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

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

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

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

73+

69}

74}

71test : Int;

76test : Int;

72−test = interp Nil eProg 2 2;

77+test = interp [] eProg 2 2;

74testFac : Int;

79testFac : Int;

75−testFac = interp Nil eFac 4;

80+testFac = interp [] eFac 4;

77main : IO ();

82main : IO ();

78−main = print testFac;

83+main = do { print testFac;

84+ print test; };

85+

src/Core/Elaborate.hs+20−10

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

223proofstate :: Elab ()

224proofstate = processTactic' ProofState

225

226+reorder_claims :: Name -> Elab ()

227+reorder_claims n = processTactic' (Reorder n)

228+

226qed :: Elab Term

229qed :: Elab Term

227qed = do processTactic' QED

230qed = do processTactic' QED

228 ES p _ _ <- get

231 ES p _ _ <- get

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

231undo :: Elab ()

234undo :: Elab ()

232undo = processTactic' Undo

235undo = processTactic' Undo

233

236

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

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

235prepare_apply fn imps =

238prepare_apply fn imps =

236 do ty <- get_type fn

239 do ty <- get_type fn

237 ctxt <- get_context

240 ctxt <- get_context

238 env <- get_env

241 env <- get_env

239 -- let claims = getArgs ty imps

242 -- let claims = getArgs ty imps

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

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

241 ES p s prev <- get

244 ES p s prev <- get

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

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

244 let (h : hs) = holes p

247 let (h : hs) = holes p

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

248 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

246 return claims

252 return claims

247 where

253 where

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

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

249 do n <- unique_hole (mkMN n')

255 do n <- unique_hole (mkMN n')

250− when (null claims) (start_unify n)

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

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

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

252 claim n (forget t)

258 claim n (forget t)

253− when i (movelast n)

259+ when (fst i) (movelast n)

254− doClaims sc' is (n : claims)

260+ mkClaims sc' is (n : claims)

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

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

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

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)

257

266

258 mkMN n@(MN _ _) = n

267 mkMN n@(MN _ _) = n

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

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

260 mkMN (NS n xs) = NS (mkMN n) xs

269 mkMN (NS n xs) = NS (mkMN n) xs

261

270

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

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

263apply fn imps =

272apply fn imps =

264 do args <- prepare_apply fn imps

273 do args <- prepare_apply fn imps

265 fill (raw_apply fn (map Var args))

274 fill (raw_apply fn (map Var args))

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

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

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

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

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

269 -- so do nothing

278 -- so do nothing

279+ ptm <- get_term

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

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

271 ES p s prev <- get

281 ES p s prev <- get

272 let (n, hs) = unified p

282 let (n, hs) = unified p

src/Core/ProofState.hs+32−4

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

38data Tactic = Attack

39 | Claim Name Raw

40+ | Reorder Name

40 | Exact Raw

41 | Exact Raw

41 | Fill Raw

42 | Fill Raw

42 | PrepFill Name [Name]

43 | PrepFill Name [Name]

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

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

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

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

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

183

184

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+

184focus :: Name -> RunTactic

208focus :: Name -> RunTactic

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

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

186 if n `elem` hs

210 if n `elem` hs

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

231fill :: Raw -> RunTactic

255fill :: Raw -> RunTactic

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

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

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

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

258+ s <- get

234 ns <- lift $ unify ctxt env valty ty

259 ns <- lift $ unify ctxt env valty ty

235 ps <- get

260 ps <- get

236 let (uh, uns) = unified ps

261 let (uh, uns) = unified ps

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

259solve :: RunTactic

284solve :: RunTactic

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

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

261 | pureTerm val = do ps <- get

286 | pureTerm val = do ps <- get

287+ let (uh, uns) = unified ps

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

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

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

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

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

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

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

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

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

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

383 do ps <- get

410 do ps <- get

384 let (_, ns) = unified ps

411 let (_, ns) = unified ps

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

412 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) })

387 return (updateSolved ns tm)

414 return (updateSolved ns tm)

388

415

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

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

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

411 return (ps { pterm = tm',

438 return (ps { pterm = tm',

412 unified = (h, []),

439 unified = (h, []),

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

440 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')

415processTactic t ps

444processTactic t ps

416 = case holes ps of

445 = case holes ps of

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

446 [] -> 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

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

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

421

449

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

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

src/Core/ShellParser.hs+1−1

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

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

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

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

54− return (discard (apply tm args))

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

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

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

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

src/Idris/ElabTerm.hs+7−7

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

42 mkPat

43 where

44 isph arg = case getTm arg of

45− Placeholder -> True

45+ Placeholder -> (True, priority arg)

46− _ -> False

46+ _ -> (False, priority arg)

48 toElab arg = case getTm arg of

49 Placeholder -> Nothing

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

283 args <- apply (Var n) imps

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

285 resolveTC (depth - 1) ist)

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

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

287 solve

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

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

289− isImp _ = False

289+ isImp arg = (False, priority arg)

290

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

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

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

322 return (fn, a)

323 -- FIXME: resolve ambiguities

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

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

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

326 when autoSolve solveAll

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

328 isImp _ = False

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

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

332 (getArgTys (binderTy t))

333 _ -> 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)

335 when autoSolve solveAll

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

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

test/test001/expected+1

@@ -1 +1,2 @@

124

2+12

test/test001/test001.idr+28−20

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