fix: namespace issues with generated code

This commit is contained in:
Kiana Sheibani 2024-12-04 07:13:05 -05:00
parent bf184dd8d3
commit b3c48a5d8c
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
2 changed files with 20 additions and 9 deletions

View file

@ -73,16 +73,31 @@ allProblems (Pr day' part') = do
--- REFLECTION
public export
fetchSolution : Problem -> Elab (String -> String)
fetchSolution (Pr day part) = do
let name =
solutionName : Problem -> Name
solutionName (Pr day part) =
NS (MkNS ["Part" ++ show (partNat part),
"Day" ++ show day]) `{solution}
public export
fetchSolution : Problem -> Elab (String -> String)
fetchSolution pr = do
let name = solutionName pr
check `(\s => show (~(IVar EmptyFC name) s))
<|> fail "\{show name} does not exist as a valid solution"
public export
fetchAllSols : (latest : Problem) -> Elab (SortedMap Problem (String -> String))
fetchAllSols pr =
fromList <$> traverse (\p => (p,) <$> fetchSolution p) (allProblems pr)
let prs = allProblems pr
list = foldr (\pr,tt => `(Prelude.(::)
(Builtin.MkPair
(Data.Problem.Pr
(Prelude.fromInteger
~(IPrimVal EmptyFC $ BI $ natToInteger pr.day))
~(case pr.part of
Part1 => `(Data.Problem.Part1)
Part2 => `(Data.Problem.Part2)))
(\s => show (~(IVar EmptyFC $ solutionName pr) s)))
~(tt))) `(Prelude.Nil) prs
ttimp = `(Data.SortedMap.fromList ~(list))
in check ttimp

View file

@ -1,10 +1,6 @@
module Main
import Data.List1
import Data.Maybe
import Data.String
import Data.SortedMap
import Data.SortedMap.Dependent
import Data.Problem
import Utils