677799c · Idris-dev · git.iko.soy

62 (errAt "type of " n (erun fc (build i info False n ty)))

63 ds <- checkDef fc defer

64 addDeferred ds

65− mapM_ (elabCaseBlock info) is

65+ mapM_ (elabCaseBlock info opts) is

66 ctxt <- getContext

67 logLvl 5 $ "Rechecking"

68 logLvl 6 $ show tyT

128 (erun fc (build i info False n t))

129 def' <- checkDef fc defer

130 addDeferredTyCon def'

131− mapM_ (elabCaseBlock info) is

131+ mapM_ (elabCaseBlock info []) is

132 (cty, _) <- recheckC fc [] t'

133 logLvl 2 $ "---> " ++ show cty

134 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

145 (errAt "data declaration " n (erun fc (build i info False n t)))

146 def' <- checkDef fc defer

147 addDeferredTyCon def'

148− mapM_ (elabCaseBlock info) is

148+ mapM_ (elabCaseBlock info []) is

149 (cty, _) <- recheckC fc [] t'

150 logLvl 2 $ "---> " ++ show cty

151 -- temporary, to check cons

492 logLvl 2 $ "Rechecking " ++ show t'

493 def' <- checkDef fc defer

494 addDeferred def'

495− mapM_ (elabCaseBlock info) is

495+ mapM_ (elabCaseBlock info []) is

496 ctxt <- getContext

497 (cty, _) <- recheckC fc [] t'

498 let cty' = normaliseC ctxt [] cty

528 -- question: CAFs in where blocks?

529 tclift $ tfail $ At fc (NoTypeDecl n)

530 [ty] -> return ty

531− pats_in <- mapM (elabClause info (Dictionary `elem` opts))

531+ pats_in <- mapM (elabClause info opts)

532 (zip [0..] cs)

533 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

534

748 (build i info aspat (MN 0 "val") (infTerm tm)))

749 def' <- checkDef (FC "(input)" 0) defer

750 addDeferred def'

751− mapM_ (elabCaseBlock info) is

751+ mapM_ (elabCaseBlock info []) is

752

753 logLvl 3 ("Value: " ++ show tm')

754 recheckC (FC "(input)" 0) [] tm'

778-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

779 err@(Error _) -> return False

780

781−elabClause :: ElabInfo -> Bool -> (Int, PClause) ->

781+elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

782 Idris (Either Term (Term, Term))

783−elabClause info tcgen (_, PClause fc fname lhs_in [] PImpossible [])

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

784+ = do let tcgen = Dictionary `elem` opts

784− = do b <- checkPossible info fc tcgen fname lhs_in

785+ b <- checkPossible info fc tcgen fname lhs_in

785 case b of

786 case b of

786 True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

787 True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

787 False -> do ptm <- mkPatTm lhs_in

788 False -> do ptm <- mkPatTm lhs_in

788 return (Left ptm)

789 return (Left ptm)

789−elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

790+elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

791+ = do let tcgen = Dictionary `elem` opts

790− = do ctxt <- getContext

792+ ctxt <- getContext

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

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

792 -- pattern bindings

794 -- pattern bindings

793 i <- getIState

795 i <- getIState

857 -- from the where block

859 -- from the where block

858

860

859 mapM_ (elabDecl' EAll info) wafter

861 mapM_ (elabDecl' EAll info) wafter

860− mapM_ (elabCaseBlock info) is

862+ mapM_ (elabCaseBlock info opts) is

861

863

862 ctxt <- getContext

864 ctxt <- getContext

863 logLvl 5 $ "Rechecking"

865 logLvl 5 $ "Rechecking"

937 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps)

939 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps)

938 propagateParams ps x = x

940 propagateParams ps x = x

939

941

940−elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

942+elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

943+ = do let tcgen = Dictionary `elem` opts

941− = do ctxt <- getContext

944+ ctxt <- getContext

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

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

943 -- pattern bindings

946 -- pattern bindings

944 i <- getIState

947 i <- getIState

970 return (tt, d, is))

973 return (tt, d, is))

971 def' <- checkDef fc defer

974 def' <- checkDef fc defer

972 addDeferred def'

975 addDeferred def'

973− mapM_ (elabCaseBlock info) is

976+ mapM_ (elabCaseBlock info opts) is

974 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

977 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

975 let cwvaltyN = explicitNames cwvalty

978 let cwvaltyN = explicitNames cwvalty

976 let cwvalN = explicitNames cwval

979 let cwvalN = explicitNames cwval

1026 return (tt, d, is))

1029 return (tt, d, is))

1027 def' <- checkDef fc defer

1030 def' <- checkDef fc defer

1028 addDeferred def'

1031 addDeferred def'

1029− mapM_ (elabCaseBlock info) is

1032+ mapM_ (elabCaseBlock info opts) is

1030 logLvl 5 ("Checked RHS " ++ show rhs')

1033 logLvl 5 ("Checked RHS " ++ show rhs')

1031 (crhs, crhsty) <- recheckC fc [] rhs'

1034 (crhs, crhsty) <- recheckC fc [] rhs'

1032 return $ Right (clhs, crhs)

1035 return $ Right (clhs, crhs)

1549 = elabTransform info fc safety old new

1552 = elabTransform info fc safety old new

1550elabDecl' _ _ _ = return () -- skipped this time

1553elabDecl' _ _ _ = return () -- skipped this time

1551

1554

1552−elabCaseBlock info d@(PClauses f o n ps)

1555+elabCaseBlock info opts d@(PClauses f o n ps)

1553 = do addIBC (IBCDef n)

1556 = do addIBC (IBCDef n)

1554 logLvl 6 $ "CASE BLOCK: " ++ show (n, d)

1557 logLvl 6 $ "CASE BLOCK: " ++ show (n, d)

1555− elabDecl' EAll info d

1558+ elabDecl' EAll info (PClauses f (nub (o ++ opts)) n ps )

1556

1559

1557-- elabDecl' info (PImport i) = loadModule i

1560-- elabDecl' info (PImport i) = loadModule i

1558

1561