diff --git a/src/Data/Problem.idr b/src/Data/Problem.idr index f1a70d0..3f5300d 100644 --- a/src/Data/Problem.idr +++ b/src/Data/Problem.idr @@ -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 diff --git a/src/Main.idr b/src/Main.idr index 85e6388..0ccb97d 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -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