727a3d6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix transform elaboration

727a3d6Edwin Brady11 years ago

src/Idris/AbsSyntax.hs+1

compare with master

unifiedsplit

@@ -1835,6 +1835,7 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1835 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

1836 su t@(PLam fc _ _ _ _) = PHidden t

1837 su t@(PPi _ _ _ _ _) = PHidden t

1838+ su t@(PConstant _ c) | isTypeConst c = PHidden t

1838 su t = t

1839 su t = t

1839

1840

1840 ctxt = tt_ctxt i

1841 ctxt = tt_ctxt i

src/Idris/Elab/Clause.hs+1−1

@@ -376,7 +376,7 @@ elabPE info fc caller r =

376 showTmImpls rhs)) (pe_clauses specdecl))

377

378 logLvl 2 $ show n ++ " transformation rule: " ++

379− show rhs ++ " ==> " ++ show lhs

379+ showTmImpls rhs ++ " ==> " ++ showTmImpls lhs

380

381 elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy

382 let def = map (\(lhs, rhs) ->

src/Idris/Elab/Term.hs+8−7

@@ -35,7 +35,7 @@ import qualified Data.Text as T

36import Debug.Trace

38−data ElabMode = ETyDecl | ELHS | ERHS

38+data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS

39 deriving Eq

@@ -220,7 +220,7 @@ elab ist info emode opts fn tm

220 sequence_ (get_delayed_elab est)

221 end_unify

222 ptm <- get_term

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

223+ when (pattern || intransform) -- convert remaining holes to pattern vars

224 (do update_term orderPats

225 unify_all

226 matchProblems False -- only the ones we matched earlier

@@ -228,7 +228,8 @@ elab ist info emode opts fn tm

228 mkPat)

229 where

230 pattern = emode == ELHS

231+ intransform = emode == ETransLHS

231− bindfree = emode == ETyDecl || emode == ELHS

232+ bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS

232

233

233 get_delayed_elab est =

234 get_delayed_elab est =

234 let ds = delayed_elab est in

235 let ds = delayed_elab est in

@@ -489,7 +490,7 @@ elab ist info emode opts fn tm

489 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

490 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

490 | pattern && not reflection && not (e_qq ec) && e_nomatching ec

491 | pattern && not reflection && not (e_qq ec) && e_nomatching ec

491 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

492 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

492− | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

493+ | (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)

493 = do let ina = e_inarg ec

494 = do let ina = e_inarg ec

494 guarded = e_guarded ec

495 guarded = e_guarded ec

495 inty = e_intype ec

496 inty = e_intype ec

@@ -500,7 +501,7 @@ elab ist info emode opts fn tm

500 _ -> True

501 _ -> True

501 -- this is to stop us resolve type classes recursively

502 -- this is to stop us resolve type classes recursively

502 -- trace (show (n, guarded)) $

503 -- trace (show (n, guarded)) $

503− if (tcname n && ina)

504+ if (tcname n && ina && not intransform)

504 then erun fc $

505 then erun fc $

505 do patvar n

506 do patvar n

506 update_term liftPats

507 update_term liftPats

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

611 ivs' <- get_instances

612 ivs' <- get_instances

612 env <- get_env

613 env <- get_env

613 elabE (ina { e_inarg = True }) (Just fc) sc

614 elabE (ina { e_inarg = True }) (Just fc) sc

614− when (not pattern) $

615+ when (not (pattern || intransform)) $

615 mapM_ (\n -> do focus n

616 mapM_ (\n -> do focus n

616 g <- goal

617 g <- goal

617 hs <- get_holes

618 hs <- get_holes

@@ -799,7 +800,7 @@ elab ist info emode opts fn tm

799 -- to be needed.

800 -- to be needed.

800 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

801 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

801 implicitApp elab

802 implicitApp elab

802− | pattern = do elab; return ()

803+ | pattern || intransform = do elab; return ()

803 | otherwise

804 | otherwise

804 = do s <- get

805 = do s <- get

805 imps <- elab

806 imps <- elab

src/Idris/Elab/Transform.hs+6−2

@@ -53,9 +53,10 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

53 = do ctxt <- getContext

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56+ logLvl 5 ("Transform LHS input: " ++ showTmImpls lhs)

56 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

57 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

57 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

58 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

58− (erun fc (buildTC i info ELHS [] (sUN "transform")

59+ (erun fc (buildTC i info ETransLHS [] (sUN "transform")

59 (infTerm lhs)))

60 (infTerm lhs)))

60 setContext ctxt'

61 setContext ctxt'

61 processTacticDecls info newDecls

62 processTacticDecls info newDecls

@@ -67,8 +68,11 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

67 (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm

68 (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm

68 let clhs_tm = renamepats pnames clhs_tm_in

69 let clhs_tm = renamepats pnames clhs_tm_in

69 logLvl 3 ("Transform LHS " ++ show clhs_tm)

70 logLvl 3 ("Transform LHS " ++ show clhs_tm)

70−

71+ logLvl 3 ("Transform type " ++ show clhs_ty)

72+

71 let rhs = addImplBound i (map fst newargs) rhs_in

73 let rhs = addImplBound i (map fst newargs) rhs_in

74+ logLvl 5 ("Transform RHS input: " ++ showTmImpls rhs)

75+

72 ((rhs', defer, ctxt', newDecls), _) <-

76 ((rhs', defer, ctxt', newDecls), _) <-

73 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState

77 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState

74 (do pbinds i lhs_tm

78 (do pbinds i lhs_tm