git.iko.soy/Idris-dev
on master help sign in
Fix transform elaboration
commit727a3d62b855ce9a731ee90da2191a45fc31366e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 4 Jun 2015, 12:22 (11 years ago) parent84bca25
4 files changed+16−10
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Term.hs+8−7 src/Idris/Elab/Transform.hs+6−2
src/Idris/AbsSyntax.hs+1
@@ -1835,6 +1835,7 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
18351835 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
18361836 su t@(PLam fc _ _ _ _) = PHidden t
18371837 su t@(PPi _ _ _ _ _) = PHidden t
1838+ su t@(PConstant _ c) | isTypeConst c = PHidden t
18381839 su t = t
18391840
18401841 ctxt = tt_ctxt i
src/Idris/Elab/Clause.hs+1−1
@@ -376,7 +376,7 @@ elabPE info fc caller r =
376376 showTmImpls rhs)) (pe_clauses specdecl))
377377
378378 logLvl 2 $ show n ++ " transformation rule: " ++
379− show rhs ++ " ==> " ++ show lhs
379+ showTmImpls rhs ++ " ==> " ++ showTmImpls lhs
380380
381381 elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy
382382 let def = map (\(lhs, rhs) ->
src/Idris/Elab/Term.hs+8−7
@@ -35,7 +35,7 @@ import qualified Data.Text as T
3535
3636import Debug.Trace
3737
38−data ElabMode = ETyDecl | ELHS | ERHS
38+data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS
3939 deriving Eq
4040
4141
@@ -220,7 +220,7 @@ elab ist info emode opts fn tm
220220 sequence_ (get_delayed_elab est)
221221 end_unify
222222 ptm <- get_term
223− when pattern -- convert remaining holes to pattern vars
223+ when (pattern || intransform) -- convert remaining holes to pattern vars
224224 (do update_term orderPats
225225 unify_all
226226 matchProblems False -- only the ones we matched earlier
@@ -228,7 +228,8 @@ elab ist info emode opts fn tm
228228 mkPat)
229229 where
230230 pattern = emode == ELHS
231− bindfree = emode == ETyDecl || emode == ELHS
231+ intransform = emode == ETransLHS
232+ bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS
232233
233234 get_delayed_elab est =
234235 let ds = delayed_elab est in
@@ -489,7 +490,7 @@ elab ist info emode opts fn tm
489490 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
490491 | pattern && not reflection && not (e_qq ec) && e_nomatching ec
491492 = 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)
493494 = do let ina = e_inarg ec
494495 guarded = e_guarded ec
495496 inty = e_intype ec
@@ -500,7 +501,7 @@ elab ist info emode opts fn tm
500501 _ -> True
501502 -- this is to stop us resolve type classes recursively
502503 -- trace (show (n, guarded)) $
503− if (tcname n && ina)
504+ if (tcname n && ina && not intransform)
504505 then erun fc $
505506 do patvar n
506507 update_term liftPats
@@ -611,7 +612,7 @@ elab ist info emode opts fn tm
611612 ivs' <- get_instances
612613 env <- get_env
613614 elabE (ina { e_inarg = True }) (Just fc) sc
614− when (not pattern) $
615+ when (not (pattern || intransform)) $
615616 mapM_ (\n -> do focus n
616617 g <- goal
617618 hs <- get_holes
@@ -799,7 +800,7 @@ elab ist info emode opts fn tm
799800 -- to be needed.
800801 implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
801802 implicitApp elab
802− | pattern = do elab; return ()
803+ | pattern || intransform = do elab; return ()
803804 | otherwise
804805 = do s <- get
805806 imps <- elab
src/Idris/Elab/Transform.hs+6−2
@@ -53,9 +53,10 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
5353 = do ctxt <- getContext
5454 i <- getIState
5555 let lhs = addImplPat i lhs_in
56+ logLvl 5 ("Transform LHS input: " ++ showTmImpls lhs)
5657 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-
5758 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")
5960 (infTerm lhs)))
6061 setContext ctxt'
6162 processTacticDecls info newDecls
@@ -67,8 +68,11 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
6768 (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm
6869 let clhs_tm = renamepats pnames clhs_tm_in
6970 logLvl 3 ("Transform LHS " ++ show clhs_tm)
70−
71+ logLvl 3 ("Transform type " ++ show clhs_ty)
72+
7173 let rhs = addImplBound i (map fst newargs) rhs_in
74+ logLvl 5 ("Transform RHS input: " ++ showTmImpls rhs)
75+
7276 ((rhs', defer, ctxt', newDecls), _) <-
7377 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState
7478 (do pbinds i lhs_tm