CakeML
Implement `get_opt` in the basis library
Note: this is implemented in SML already in the HOL4 sources (https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/Holmake/GetOpt.sml). That would be a good starting point for the HOL/CakeML version.
@xrchz I haven't touched it for a very long time, but the draft I managed to get working was
Using this peg grammar
arg := -<letter> (* Short flag *)
| --<word>(=<word)? (* Long flag *)
| <word> (* Single option *)
word := <letter>+
letter := [^=-] (* Some reasonable alphabet *)
to parse the argument list provided by Commandline.arguments into a list of type:
val _ = Datatype`
arg =
(* Simple flags of the form -<ident> eg: -h *)
ShortFlag mlstring
(* Long flags of the form --<ident>+ eg: --help *)
| LongFlag mlstring
(* Long flags with option of the form --<ident>+=<ident>+
eg: --arch=arm6 *)
| OptionFlag mlstring mlstring
(* Standalone option of the form <ident>+ eg: cake.S*)
| Option mlstring
(* Where <ident> is equal to the regular expression [a-zA-Z0-9.-/_]
(or similar) *)
`;
From the point of view of the user, you provide 'a flag list, where 'a is whatever type you want to use to represent your options and flag is:
val _ = Datatype`
flag = <| name : mlstring; (* Long flag ("-" if disable) *)
short : char; (* Short flag (#"-" if disable) *)
desc : mlstring; (* Short description used in the help msg *)
opt : bool; (* Does it have and acompaning option/value? *)
(* Continuation modifing the underlying structure
representing the options where 'flag.cont opt x' takes
an optional value 'opt' and a value 'x' of ''a' and
uses these to update 'x' to represent the precense of
the flag 'flag.name' or 'flag.short' with potentially
some argument
*)
cont : mlstring option -> 'a -> 'a |>
`;
and then use makeArgsConf :α flag list -> α -> arg list -> mlstring + α with the configuration as α flag list, the default options of type α, and the argument list (after using the PEG parser). this should
get you either a nice set of options or a error message.
A simple example of all this is:
val test_conf_def = Define`
test_conf = mkArgsConf [<| name := implode "one" ;
short := #"1" ;
desc := implode "flag1" ;
opt := F;
cont := K (λx. case x of (_,b,c) => (T,b,c))|>;
<| name := implode "two" ;
short := #"2" ;
desc := implode "flag2" ;
opt := T;
cont := (λx y. case y of (a,_,c) => (a,x,c))|>;
<| name := implode "three" ;
short := #"3" ;
desc := implode "flag3" ;
opt := F;
cont := K (λx. case x of (a,b,_) => (a,b,T))|>
]
(F,NONE,F)
`;
and then
> EVAL ``parse_conf test_conf ["-1"]``;
val it = ⊢ parse_conf test_conf ["-1"] = INR (T,NONE,F): thm
> EVAL ``parse_conf test_conf ["-2"]``;
val it = ⊢ parse_conf test_conf ["-2"] = INL (strlit "Missing value to: -2"): thm
> EVAL ``parse_conf test_conf ["-2";"foo"]``;
val it = ⊢ parse_conf test_conf ["-2"; "foo"] = INR (F,SOME (strlit "foo"),F): thm
You can try it out loading argParseScript.sml from this repo. there is a compiled example but it seems to be broken with the newest version of CakeML
It would be very good to get some version of this merged in, since it sounds like you made a lot of progress. What still needs to be done before the draft would be finished / the issue could be closed?
The main thing missing in my opinion is some idea of correctness for the function that matches flags and configurations (mkArgsConf) aside from that maybe some helper functions to write configurations, However, it is possible to use what is already there to construct a simple argument parser. Should I move what is currently there into basis/pure/ArgParseScript.sml and basis/ArgParseProgScript.sml and start a PR?
@agomezl where is the work done so far, is it on a branch somewhere?
