f98d138 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix parameter propagation

f98d138Edwin Brady13 years ago

libs/base/Control/Isomorphism.idr+5−4

compare with master

unifiedsplit

@@ -35,10 +35,10 @@ isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom

36eitherComm : Iso (Either a b) (Either b a)

37eitherComm = MkIso swap swap swapSwap swapSwap

38− where swap : Either a b -> Either b a

38+ where swap : Either a' b' -> Either b' a' -- a & b are parameters, so fixed!

39 swap (Left x) = Right x

40 swap (Right x) = Left x

41− swapSwap : (e : Either a b) -> swap (swap e) = e

41+ swapSwap : (e : Either a' b') -> swap (swap e) = e

42 swapSwap (Left x) = refl

43 swapSwap (Right x) = refl

@@ -105,9 +105,10 @@ eitherCongRight i = eitherCong isoRefl i

105-- Isomorphisms over products

106pairComm : Iso (a, b) (b, a)

107pairComm = MkIso swap swap swapSwap swapSwap

108− where swap : (a, b) -> (b, a)

108+ where swap : (a', b') -> (b', a')

109 swap (x, y) = (y, x)

110+

110− swapSwap : (x : (a, b)) -> swap (swap x) = x

111+ swapSwap : (x : (a', b')) -> swap (swap x) = x

111 swapSwap (x, y) = refl

112 swapSwap (x, y) = refl

112

113

113pairAssoc : Iso (a, (b, c)) ((a, b), c)

114pairAssoc : Iso (a, (b, c)) ((a, b), c)

libs/base/Control/Monad/State.idr+1−1

@@ -14,7 +14,7 @@ record StateT : Type -> (Type -> Type) -> Type -> Type where

15instance Functor f => Functor (StateT s f) where

16 map f (ST g) = ST (\st => map (mapFst f) (g st)) where

17− mapFst : (a -> x) -> (a, b) -> (x, b)

17+ mapFst : (a -> x) -> (a, s) -> (x, s)

18 mapFst fn (a, b) = (fn a, b)

20instance Monad f => Applicative (StateT s f) where

libs/base/Data/Vect/Quantifiers.idr+4−4

@@ -14,10 +14,10 @@ anyElim f _ (There p) = f p

15any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)

16any _ Nil = No anyNilAbsurd

17−any {P} p (x::xs) with (p x)

17+any p (x::xs) with (p x)

18 | Yes prf = Yes (Here prf)

19 | No prf =

20− case any {P} p xs of

20+ case any p xs of

21 Yes prf' => Yes (There prf')

22 No prf' => No (anyElim prf' prf)

@@ -39,9 +39,9 @@ notAllThere np (_ :: ps) = np ps

40all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)

41all _ Nil = Yes Nil

42−all {P} d (x::xs) with (d x)

42+all d (x::xs) with (d x)

43 | No prf = No (notAllHere prf)

44 | Yes prf =

45− case all {P} d xs of

45+ case all d xs of

46 Yes prf' => Yes (prf :: prf')

47 No prf' => No (notAllThere prf')

libs/effects/Effects.idr+3−3

@@ -209,8 +209,8 @@ execEff : Env m xs -> (p : EffElem e res xs) ->

209 (Env m (updateResTy xs p eff) -> a -> m t) -> m t

210execEff (val :: env) Here eff' k

211 = handle val eff' (\res, v => k (res :: env) v)

212−execEff {e} {a} {b} (val :: env) (There p) eff k

212+execEff {e} {res} {b} {a} (val :: env) (There p) eff k

213− = execEff {e} {a} {b} env p eff (\env', v => k (val :: env') v)

213+ = execEff {e} {res} {b} {a} env p eff (\env', v => k (val :: env') v)

214

215private

216testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->

@@ -224,7 +224,7 @@ testEff (val :: env) (There p) lk rk

224 (\envk => rk (val :: envk))

225

226private

227−testEffLbl : {x : lbl} ->

227+testEffLbl : {x : lblTy} ->

228 Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->

229 (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->

230 (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->

libs/neweffects/Effects.idr+2−2

@@ -208,8 +208,8 @@ execEff : Env m xs -> (p : EffElem e res xs) ->

208execEff (val :: env) Here eff' k

209 = handle val eff' (\v, res => k v (res :: env))

210-- FIXME: Teach the elaborator to propagate parameters here

211−execEff {a} {res} {resk} (val :: env) (There p) eff k

211+execEff {e} {a} {res} {resk} (val :: env) (There p) eff k

212− = execEff {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))

212+ = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))

213

214-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

215-- updates can be propagated even through failing computations?

src/Idris/ElabDecls.hs+86−45

@@ -76,12 +76,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

76 ctxt <- getContext

77 i <- getIState

79− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

79+ logLvl 1 $ show n ++ " pre-type " ++ showTmImpls ty'

80 ty' <- addUsingConstraints syn fc ty'

81 ty' <- implicit syn n ty'

83 let ty = addImpl i ty'

84− logLvl 2 $ show n ++ " type " ++ showTmImpls ty

84+ logLvl 1 $ show n ++ " type " ++ showTmImpls ty

85 ((tyT, defer, is), log) <-

86 tclift $ elaborate ctxt n (TType (UVal 0)) []

87 (errAt "type of " n (erun fc (build i info False [] n ty)))

@@ -662,7 +662,7 @@ elabProvider info syn fc n ty tm

662 tm <- getProvided fc rhs'

663

664 -- Finally add a top-level definition of the provided term

665− elabClauses info fc [] n [PClause fc n (PRef fc n) [] (delab i tm) []]

665+ elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

666 logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

667

668 where isTType :: TT Name -> Bool

@@ -1266,6 +1266,68 @@ checkPossible info fc tcgen fname lhs_in

1266 ((P _ x _, _), (P _ y _, _)) -> x == y

1267 _ -> False

1268

1269+getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1270+ = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1271+getFixedInType i env (_ : is) (Bind n (Pi t) sc)

1272+ = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)

1273+getFixedInType i env is tm@(App f a)

1274+ | (P _ tn _, args) <- unApply tm

1275+ = case lookupCtxt tn (idris_datatypes i) of

1276+ [t] -> nub $ paramNames args env (param_pos t) ++

1277+ getFixedInType i env is f ++

1278+ getFixedInType i env is a

1279+ [] -> nub $ getFixedInType i env is f ++

1280+ getFixedInType i env is a

1281+ | otherwise = nub $ getFixedInType i env is f ++

1282+ getFixedInType i env is a

1283+getFixedInType i _ _ _ = []

1284+

1285+getFlexInType i env (Bind n (Pi t) sc)

1286+ = nub $ getFlexInType i env t ++

1287+ getFlexInType i (n : env) (instantiate (P Bound n t) sc)

1288+getFlexInType i env tm@(App f a)

1289+ | (P _ tn _, args) <- unApply tm

1290+ = case lookupCtxt tn (idris_datatypes i) of

1291+ [t] -> nub $ paramNames args env [x | x <- [0..length args],

1292+ not (x `elem` param_pos t)]

1293+ ++ getFlexInType i env f ++

1294+ getFlexInType i env a

1295+ [] -> nub $ getFlexInType i env f ++

1296+ getFlexInType i env a

1297+ | otherwise = nub $ getFlexInType i env f ++

1298+ getFlexInType i env a

1299+getFlexInType i _ _ = []

1300+

1301+-- Treat a name as a parameter if it appears in parameter positions in

1302+-- types, and never in a non-parameter position in a type.

1303+

1304+getParamsInType i env ps t = let fix = getFixedInType i env ps t

1305+ flex = getFlexInType i env t in

1306+ [x | x <- fix, not (x `elem` flex)]

1307+

1308+paramNames args env [] = []

1309+paramNames args env (p : ps)

1310+ | length args > p = case args!!p of

1311+ P _ n _ -> if n `elem` env

1312+ then n : paramNames args env ps

1313+ else paramNames args env ps

1314+ _ -> paramNames args env ps

1315+ | otherwise = paramNames args env ps

1316+

1317+propagateParams :: [Name] -> Type -> PTerm -> PTerm

1318+propagateParams ps t tm@(PApp _ (PRef fc n) args)

1319+ = PApp fc (PRef fc n) (addP t args)

1320+ where addP (Bind n _ sc) (t : ts)

1321+ | Placeholder <- getTm t,

1322+ n `elem` ps,

1323+ not (n `elem` allNamesIn tm)

1324+ = t { getTm = PRef fc n } : addP sc ts

1325+ addP (Bind n _ sc) (t : ts) = t : addP sc ts

1326+ addP _ ts = ts

1327+propagateParams ps t (PRef fc n)

1328+ = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1329+propagateParams ps t x = x

1330+

1269elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

1331elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

1270 Idris (Either Term (Term, Term))

1332 Idris (Either Term (Term, Term))

1271elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

1333elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

@@ -1292,10 +1354,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1292 [t] -> t

1354 [t] -> t

1293 _ -> []

1355 _ -> []

1294 let params = getParamsInType i [] fn_is fn_ty

1356 let params = getParamsInType i [] fn_is fn_ty

1357+ let flex = getFlexInType i [] fn_ty

1295− let lhs = stripUnmatchable i $

1358+ let lhs = mkLHSapp $ stripUnmatchable i $

1296− addImplPat i (propagateParams params (stripLinear i lhs_in))

1359+ propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1297− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)

1360+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ show lhs)

1298− logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1361+ logLvl 4 ("Fixed parameters: " ++ show (flex, params) ++ " from " ++ show lhs_in ++

1362+ "\n" ++ show (fn_ty, fn_is))

1299

1363

1300 (((lhs', dlhs, []), probs, inj), _) <-

1364 (((lhs', dlhs, []), probs, inj), _) <-

1301 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1365 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

@@ -1342,7 +1406,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1342 -- Elaborate those with a type *before* RHS, those without *after*

1406 -- Elaborate those with a type *before* RHS, those without *after*

1343 let (wbefore, wafter) = sepBlocks wb

1407 let (wbefore, wafter) = sepBlocks wb

1344

1408

1345− logLvl 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1409+ logLvl 1 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1346 mapM_ (elabDecl' EAll info) wbefore

1410 mapM_ (elabDecl' EAll info) wbefore

1347 -- Now build the RHS, using the type of the LHS as the goal.

1411 -- Now build the RHS, using the type of the LHS as the goal.

1348 i <- getIState -- new implicits from where block

1412 i <- getIState -- new implicits from where block

@@ -1355,7 +1419,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1355 ((rhs', defer, is, probs), _) <-

1419 ((rhs', defer, is, probs), _) <-

1356 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

1420 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []

1357 (do pbinds ist lhs_tm

1421 (do pbinds ist lhs_tm

1358− mapM_ setinj inj

1422+ mapM_ setinj (nub (params ++ inj))

1359 setNextName

1423 setNextName

1360 (_, _, is) <- errAt "right hand side of " fname

1424 (_, _, is) <- errAt "right hand side of " fname

1361 (erun fc (build i info False opts fname rhs))

1425 (erun fc (build i info False opts fname rhs))

@@ -1415,6 +1479,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1415 addErrRev (crhs, clhs)

1479 addErrRev (crhs, clhs)

1416 return $ Right (clhs, crhs)

1480 return $ Right (clhs, crhs)

1417 where

1481 where

1482+ mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

1483+ mkLHSapp t = t

1484+

1418 decorate (NS x ns)

1485 decorate (NS x ns)

1419 = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])

1486 = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])

1420-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])

1487-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])

@@ -1447,40 +1514,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1447 -- _ -> MN i (show n)) . l

1514 -- _ -> MN i (show n)) . l

1448 }

1515 }

1449

1516

1450− getParamsInType i env (PExp _ _ _ _ : is) (Bind n (Pi t) sc)

1451− = getParamsInType i env is (instantiate (P Bound n t) sc)

1452− getParamsInType i env (_ : is) (Bind n (Pi t) sc)

1453− = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)

1454− getParamsInType i env is tm@(App f a)

1455− | (P _ tn _, args) <- unApply tm

1456− = case lookupCtxt tn (idris_datatypes i) of

1457− [t] -> nub $ paramNames args env (param_pos t) ++

1458− getParamsInType i env is f ++

1459− getParamsInType i env is a

1460− [] -> nub $ getParamsInType i env is f ++

1461− getParamsInType i env is a

1462− | otherwise = nub $ getParamsInType i env is f ++

1463− getParamsInType i env is a

1464− getParamsInType i _ _ _ = []

1465−

1466− paramNames args env [] = []

1467− paramNames args env (p : ps)

1468− | length args > p = case args!!p of

1469− P _ n _ -> if n `elem` env

1470− then n : paramNames args env ps

1471− else paramNames args env ps

1472− _ -> paramNames args env ps

1473− | otherwise = paramNames args env ps

1474−

1475− propagateParams :: [Name] -> PTerm -> PTerm

1476− propagateParams ps (PApp _ (PRef fc n) args)

1477− = PApp fc (PRef fc n) (map addP args)

1478− where addP imp@(PImp _ _ _ _ Placeholder _)

1479− | pname imp `elem` ps = imp { getTm = PRef fc (pname imp) }

1480− addP t = t

1481− propagateParams ps (PRef fc n)

1482− = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1483− propagateParams ps x = x

1484

1517

1485 -- if a hole is just an argument/result of a case block, treat it as

1518 -- if a hole is just an argument/result of a case block, treat it as

1486 -- the unit type. Hack to help elaborate case in do blocks.

1519 -- the unit type. Hack to help elaborate case in do blocks.

@@ -1508,8 +1541,16 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1508 -- Build the LHS as an "Infer", and pull out its type and

1541 -- Build the LHS as an "Infer", and pull out its type and

1509 -- pattern bindings

1542 -- pattern bindings

1510 i <- getIState

1543 i <- getIState

1544+ -- get the parameters first, to pass through to any where block

1545+ let fn_ty = case lookupTy fname (tt_ctxt i) of

1546+ [t] -> t

1547+ _ -> error "Can't happen (elabClause function type)"

1548+ let fn_is = case lookupCtxt fname (idris_implicits i) of

1549+ [t] -> t

1550+ _ -> []

1551+ let params = getParamsInType i [] fn_is fn_ty

1511− let lhs = addImplPat i (stripLinear i lhs_in)

1552+ let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1512− logLvl 5 ("LHS: " ++ showTmImpls lhs)

1553+ logLvl 1 ("LHS: " ++ show lhs)

1513 ((lhs', dlhs, []), _) <-

1554 ((lhs', dlhs, []), _) <-

1514 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1555 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1515 (errAt "left hand side of with in " fname

1556 (errAt "left hand side of with in " fname

src/Idris/ElabTerm.hs+1−1

@@ -611,7 +611,7 @@ elab ist info pattern opts fn tm

611 elab' ina (PUnifyLog t) = do unifyLog True

612 elab' ina t

613 unifyLog False

614− elab' ina x = fail $ "Unelaboratable syntactic form " ++ show x

614+ elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

615

616 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

617 isScr (PRef _ n) (n', b) = (n', (n == n', b))

test/proof002/Reflect.idr+4−3

@@ -40,9 +40,10 @@ using (xs : List a, ys : List a, G : List (List a))

40 expr_r (Var i) = (_ ** (RApp RNil i, refl))

41 expr_r (App ex ey) = let (xl ** (xr, xprf)) = expr_r ex in

42 let (yl ** (yr, yprf)) = expr_r ey in

43− appRExpr _ _ xr yr xprf yprf

43+ appRExpr _ _ xr yr xprf yprf

44 where

45− appRExpr : (xs', ys' : List a) ->

45+ appRExpr : (xs', ys' : List a) ->

46+ {G : List (List a)} -> {xs, ys : List a} ->

46 RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->

47 RExpr G xs -> RExpr G ys -> (xs' = xs) -> (ys' = ys) ->

47 (ws' ** (RExpr G ws', xs' ++ ys' = ws'))

48 (ws' ** (RExpr G ws', xs' ++ ys' = ws'))

48 appRExpr x' y' rxs (RApp e i) xprf yprf

49 appRExpr x' y' rxs (RApp e i) xprf yprf

@@ -173,7 +174,7 @@ Reflect.appRExpr1 = proof {

173 rewrite sym xprf;

174 rewrite sym xprf;

174 rewrite sym yprf;

175 rewrite sym yprf;

175 rewrite prf;

176 rewrite prf;

176− rewrite sym (appendAssociative xs xs2 ys1);

177+ rewrite sym (appendAssociative xs1 xs2 ys1);

177 trivial;

178 trivial;

178}

179}

179

180