@@ -365,12 +365,13 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
366type EliminatorState = StateT (Map.Map String Int) Idris
366type EliminatorState = StateT (Map.Map String Int) Idris
368−-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
368+-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
369elabEliminator :: [Int] -> Name -> PTerm ->
369elabEliminator :: [Int] -> Name -> PTerm ->
370 [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
370 [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
371 ElabInfo -> EliminatorState ()
371 ElabInfo -> EliminatorState ()
372elabEliminator paramPos n ty cons info = do
372elabEliminator paramPos n ty cons info = do
373 elimLog $ "Elaborating eliminator"
373 elimLog $ "Elaborating eliminator"
374+ put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
374 let (cnstrs, _) = splitPi ty
375 let (cnstrs, _) = splitPi ty
375 let (splittedTy@(pms, idxs)) = splitPms cnstrs
376 let (splittedTy@(pms, idxs)) = splitPms cnstrs
376 generalParams <- namePis False pms
377 generalParams <- namePis False pms
@@ -389,13 +390,14 @@ elabEliminator paramPos n ty cons info = do
389 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
390 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
390 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
391 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
391 let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
392 let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
392 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
394 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
393 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
394 elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
396 elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
395 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
397 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
396 -- Do not elaborate clauses if there aren't any
398 -- Do not elaborate clauses if there aren't any
397 case eliminatorClauses of
399 case eliminatorClauses of
398− [] -> return ()
400+ [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
399 _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
401 _ -> State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
400 where elimLog :: String -> EliminatorState ()
402 where elimLog :: String -> EliminatorState ()
401 elimLog s = State.lift (logLvl 2 s)
403 elimLog s = State.lift (logLvl 2 s)
@@ -458,9 +460,9 @@ elabEliminator paramPos n ty cons info = do
458 freshName key = do
460 freshName key = do
459 nameMap <- get
461 nameMap <- get
460 let i = fromMaybe 0 (Map.lookup key nameMap)
462 let i = fromMaybe 0 (Map.lookup key nameMap)
461− let name = key ++ show i
463+ let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)
462 put $ Map.insert key (i+1) nameMap
464 put $ Map.insert key (i+1) nameMap
463− return (sUN name)
465+ return name
465 scrutineeName :: Name
467 scrutineeName :: Name
466 scrutineeName = sUN "scrutinee"
468 scrutineeName = sUN "scrutinee"
@@ -553,7 +555,7 @@ elabEliminator paramPos n ty cons info = do
553 let cons' = replaceParams paramPos generalParameters ty
555 let cons' = replaceParams paramPos generalParameters ty
554 let (args, resTy) = splitPi cons'
556 let (args, resTy) = splitPi cons'
555 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
557 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
556− consArgs <- namePis True args
558+ consArgs <- namePis False args
557 let recArgs = findRecArgs consArgs
559 let recArgs = findRecArgs consArgs
558 let recMotives = map applyRecMotive recArgs
560 let recMotives = map applyRecMotive recArgs
559 let (_, consIdxs) = splitArgPms resTy
561 let (_, consIdxs) = splitArgPms resTy
@@ -592,7 +594,7 @@ elabEliminator paramPos n ty cons info = do
592 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
594 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
593 let (_, generalIdxs') = splitArgPms resTy
595 let (_, generalIdxs') = splitArgPms resTy
594 let generalIdxs = map pexp generalIdxs'
596 let generalIdxs = map pexp generalIdxs'
595− consArgs <- namePis True args
597+ consArgs <- namePis False args
596 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
598 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
597 let recArgs = findRecArgs consArgs
599 let recArgs = findRecArgs consArgs
598 let recElims = map applyRecElim recArgs
600 let recElims = map applyRecElim recArgs