automate more option stuff

if the elaborator writes it then it will be kept up to date
automatically
This commit is contained in:
rhiannon morris 2023-10-24 18:25:56 +02:00
parent 3dc516e5b4
commit 53b338af02
1 changed files with 7 additions and 12 deletions

View File

@ -7,6 +7,7 @@ import System.File
import System.Term import System.Term
import Derive.Prelude import Derive.Prelude
%default total
%language ElabReflection %language ElabReflection
public export public export
@ -63,20 +64,14 @@ toOutFile "" = Ok {outFile := None}
toOutFile "-" = Ok {outFile := Stdout} toOutFile "-" = Ok {outFile := Stdout}
toOutFile f = Ok {outFile := File f} toOutFile f = Ok {outFile := File f}
private
phaseName : Phase -> String
phaseName Parse = "parse"
phaseName Check = "check"
phaseName Erase = "erase"
private private
toPhase : String -> OptAction toPhase : String -> OptAction
toPhase str = case toLower str of toPhase str =
"parse" => Ok {until := Just Parse} let lstr = toLower str in
"check" => Ok {until := Just Check} case find (\p => toLower (show p) == lstr) allPhases of
"erase" => Ok {until := Just Erase} Just p => Ok {until := Just p}
_ => Err "unknown phase name \{show str}\nphases: \{phaseNames}" Nothing => Err "unknown phase name \{show str}\nphases: \{phaseNames}"
where phaseNames = joinBy ", " $ map phaseName allPhases where phaseNames = joinBy ", " $ map (toLower . show) allPhases
private private
toWidth : String -> OptAction toWidth : String -> OptAction