git.iko.soy/Idris-dev
on master help sign in
Transform rules and constraints
908f2f2Edwin Brady
src/Idris/Elab/Clause.hs+7−4
compare with master
unifiedsplit
@@ -579,7 +579,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
579 -- If we're inferring metavariables in the type, don't recheck,
579 -- If we're inferring metavariables in the type, don't recheck,
580 -- because we're only doing this to try to work out those metavariables
580 -- because we're only doing this to try to work out those metavariables
581 (clhs_c, clhsty) <- if not inf
581 (clhs_c, clhsty) <- if not inf
582+ then recheckC_borrowing False (PEGenerated `notElem` opts)
582− then recheckC fc id [] lhs_tm
583+ [] fc id [] lhs_tm
583 else return (lhs_tm, lhs_ty)
584 else return (lhs_tm, lhs_ty)
584 let clhs = normalise ctxt [] clhs_c
585 let clhs = normalise ctxt [] clhs_c
585 let borrowed = borrowedNames [] clhs
586 let borrowed = borrowedNames [] clhs
@@ -681,14 +682,16 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
681 logLvl 6 $ " ==> " ++ show (forget rhs')
682 logLvl 6 $ " ==> " ++ show (forget rhs')
682
683
683 (crhs, crhsty) <- if not inf
684 (crhs, crhsty) <- if not inf
684− then recheckC_borrowing True borrowed fc id [] rhs'
685+ then recheckC_borrowing True (PEGenerated `notElem` opts)
686+ borrowed fc id [] rhs'
685 else return (rhs', clhsty)
687 else return (rhs', clhsty)
686 logLvl 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty
688 logLvl 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty
687 ctxt <- getContext
689 ctxt <- getContext
688 let constv = next_tvar ctxt
690 let constv = next_tvar ctxt
689 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of
691 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of
692+ OK (_, cs) -> when (PEGenerated `notElem` opts) $ do
690− OK (_, cs) -> do addConstraints fc cs
693+ addConstraints fc cs
691− logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs
694+ logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)
692 return ()
695 return ()
693 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))
696 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))
694 i <- getIState
697 i <- getIState
src/Idris/Elab/Transform.hs+2−2
@@ -65,7 +65,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
65 let lhs_ty = getInferType lhs'
65 let lhs_ty = getInferType lhs'
66 let newargs = pvars i lhs_tm
66 let newargs = pvars i lhs_tm
67
67
68− (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm
68+ (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] fc id [] lhs_tm
69 let clhs_tm = renamepats pnames clhs_tm_in
69 let clhs_tm = renamepats pnames clhs_tm_in
70 logLvl 3 ("Transform LHS " ++ show clhs_tm)
70 logLvl 3 ("Transform LHS " ++ show clhs_tm)
71 logLvl 3 ("Transform type " ++ show clhs_ty)
71 logLvl 3 ("Transform type " ++ show clhs_ty)
@@ -86,7 +86,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
86 processTacticDecls info newDecls
86 processTacticDecls info newDecls
87 sendHighlighting highlights
87 sendHighlighting highlights
88
88
89− (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'
89+ (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'
90 let crhs_tm = renamepats pnames crhs_tm_in
90 let crhs_tm = renamepats pnames crhs_tm_in
91 logLvl 3 ("Transform RHS " ++ show crhs_tm)
91 logLvl 3 ("Transform RHS " ++ show crhs_tm)
92
92
src/Idris/Elab/Utils.hs+4−4
@@ -23,9 +23,9 @@ import Debug.Trace
23
23
24import qualified Data.Map as Map
24import qualified Data.Map as Map
25
25
26−recheckC = recheckC_borrowing False []
26+recheckC = recheckC_borrowing False True []
27
27
28−recheckC_borrowing uniq_check bs fc mkerr env t
28+recheckC_borrowing uniq_check addConstrs bs fc mkerr env t
29 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
29 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
30 ctxt <- getContext
30 ctxt <- getContext
31 t' <- case safeForget t of
31 t' <- case safeForget t of
@@ -34,8 +34,8 @@ recheckC_borrowing uniq_check bs fc mkerr env t
34 (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of
34 (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of
35 Error e -> tfail (At fc (mkerr e))
35 Error e -> tfail (At fc (mkerr e))
36 OK x -> return x
36 OK x -> return x
37− logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs
37+ logLvl 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)
38− addConstraints fc cs
38+ when addConstrs $ addConstraints fc cs
39 return (tm, ty)
39 return (tm, ty)
40
40
41iderr :: Name -> Err -> Err
41iderr :: Name -> Err -> Err