Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ArgParse for CakeML #511

Closed
wants to merge 15 commits into from

Conversation

Projects
None yet
4 participants
@agomezl
Copy link
Contributor

agomezl commented Aug 15, 2018

This is a relatively simple library for parsing arguments using a declarative interface for specifying which kind of argument/options to take. the following example shows a simple use case.

Assume a program foo with the following arguments

Usage foo
  -f  --input     Input file to use
  -o  --output    Output file
  -h  --help      This message

We use a datatype to represent the configuration of foo

val _ = Datatype`
  foo_opt = <| input  : mlstring option;
               output : mlstring option;
               help   : bool|>
`;

and write a configuration using the flag datatype

val foo_conf_def = Define`
  foo_conf = mkArgsConf [(* -i --input *)
                         <| name  := implode "input";
                            short := #"i";
                            desc  := implode "Input file to use";
                            has_option := T; (* It spects an option *)
                            cont := (λarg conf. conf with <|input := arg|>) |>;
                         (* -o --output  *)
                         <| name  := implode "output";
                            short := #"o";
                            desc  := implode "Output file";
                            has_option := T;
                            cont := (λarg conf. conf with <|input := arg|>) |>;
                         (* -h --help *)
                         <| name  := implode "help";
                            short := #"h";
                            desc  := implode "This message";
                            has_option := F;
                            cont := K (λconf. conf with <|help := T|>)|>
                        ]
                  (* Default configuration *)
                  <|input  := NONE;
                    output := NONE;
                    help   := F
                   |>
`;

and then

> EVAL ``parse_conf foo_conf (MAP implode ["--input"])``;
val it =
   ⊢ parse_conf foo_conf (MAP implode ["--input"]) =
       INL (strlit "Missing value to: --input"): thm

> EVAL ``parse_conf foo_conf (MAP implode ["--input";"text.txt"])``;
val it =
   ⊢ parse_conf foo_conf (MAP implode ["--input"; "text.txt"]) =
       INR <|input := SOME (strlit "text.txt"); output := NONE; help := F|>:
   thm

> EVAL ``parse_conf foo_conf (MAP implode ["--input=in.txt";"--output";"out.txt"])``;
val it =
   ⊢ parse_conf foo_conf (MAP implode ["--input=text.txt"; "--output"; "out.txt"]) =
       INR <|input := SOME (strlit "out.txt"); output := NONE; help := F|>:
   thm

This is just the core functionality since there are still some quality of life components missing (help message generation, helper functions, etc).

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Aug 16, 2018

Somehow this breaks compilerTheory - can you fix?

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Aug 18, 2018

I think this breaks grepProg somehow

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Aug 19, 2018

Reopen when fixed

@xrchz xrchz closed this Aug 19, 2018

@xrchz xrchz added the test failing label Aug 20, 2018

@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Aug 24, 2018

Fixed the issues with grepProg and some other down the line with parseProg

@agomezl agomezl reopened this Aug 24, 2018

@xrchz xrchz added test failing and removed test failing labels Aug 25, 2018

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Aug 25, 2018

Now breaks with something to do with the article reader

@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Aug 25, 2018

Ok, rebasing and fixing!

@agomezl agomezl force-pushed the agomezl:argparse branch from a9772ba to 553e522 Aug 27, 2018

@xrchz xrchz closed this Aug 27, 2018

@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Aug 30, 2018

@oskarabrahamsson fixed the problem with the article reader!

@agomezl agomezl reopened this Aug 30, 2018

@xrchz xrchz removed the test failing label Aug 30, 2018

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Sep 11, 2018

This may be timing out in translator/other-examples -- either that or Holmake has died silently...

@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Sep 11, 2018

It did't actually failed, but I some how I messed up the job. How can I trigger a rebuild?

@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Sep 18, 2018

This is getting stuck in compiler/inference/test I'm currently looking at what is happening

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Oct 7, 2018

Did you find anything out about that?

@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Oct 10, 2018

This bit is the one looping:

val test = inf_eval ``infertype_prog init_config basis``

I honestly don't know what is happening there, I will ask around tomorrow (today I was rebasing and building the whole thing)

@agomezl agomezl force-pushed the agomezl:argparse branch from 747a323 to 95b9799 Oct 10, 2018

@agomezl agomezl force-pushed the agomezl:argparse branch from 95b9799 to d83742f Oct 10, 2018

@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Oct 10, 2018

Rebased to fix conflict

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Oct 10, 2018

Maybe there's something in what you added that needs to go in one of the compsets for evaluation.

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Oct 24, 2018

To make progress on this, I think someone needs to do binary search on prefixes of the basis to see where the inferencer goes into a loop.

@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Oct 24, 2018

Running val test = inf_eval "infertype_prog init_config (TAKE 73 basis)" works just fine, but anything more than that hangs, EVAL "EL 73" gives:

val it =
  ⊢ EL 73 basis =
    Dmod "Map"
      [Dlet
         (Locs <|row := 0; col := 0; offset := 0|>
            <|row := 0; col := 0; offset := 0|>) (Pvar "size")
         (Fun "v6"
            (Mat (Var (Short "v6"))
               [(Pcon (SOME (Short "Tip")) [],Lit (IntLit 0));
                (Pcon (SOME (Short "Bin"))
                   [Pvar "v5"; Pvar "v4"; Pvar "v3"; Pvar "v2"; Pvar "v1"],
                 Var (Short "v5"))]));
       Dlet
         (Locs <|row := 0; col := 0; offset := 0|>
            <|row := 0; col := 0; offset := 0|>) (Pvar "singleton")
         (Fun "v1"
...(etc)...
@agomezl

This comment has been minimized.

Copy link
Contributor Author

agomezl commented Oct 24, 2018

Doing some more digging, TAKE 74 basis looks the same both in master and argparse (after merging) so the ast hasn't change, but doing a diff on the compsets being used (computeLib.listItems cmp) gives me:

$ colordiff cake_argparse/computeLib.log cake_master/computeLib.log
687,688c687,688
<     (("Asub", "ast"), []), (("Atapp", "ast"), []), (("Atfun", "ast"), []),
<     (("Attup", "ast"), []), (("Atvar", "ast"), []), (("Aupdate", "ast"), []),
---
>     (("Asub", "ast"), []), (("Atapp", "ast"), []), (("Attup", "ast"), []),
>     (("Atvar", "ast"), []), (("Aupdate", "ast"), []),
880,881c880,884
<     (("EVEN", "arithmetic"), [RRules [? ?n. EVEN (BIT1 n) ? F, ...]]),
<     (("EVERY", "list"), [...]), ...]:
---
>     (("EVEN", "arithmetic"),
>      [RRules [? ?n. EVEN (BIT1 n) ? F, ? ?n. EVEN (BIT2 n) ? T, ...]]),
>     (("EVERY", "list"),
>      [RRules [? ?t h P. EVERY P (h::t) ? P h ? EVERY P t, ...]]),
>     (("EXISTS", "list"), [...]), ...]:

so EXISTS got removed from the compset somehow in the argparse branch which might be an indication that something went wrong at some point.

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Oct 29, 2018

I'm closing this for now -- please reopen when fixed.

@myreen myreen removed the test failing label Nov 26, 2018

@myreen myreen added the test failing label Nov 28, 2018

@myreen

This comment has been minimized.

Copy link
Contributor

myreen commented Nov 28, 2018

I'm temporarily closing this since its current state causes the regression test to get stuck.

@myreen myreen closed this Nov 28, 2018

@xrchz

This comment has been minimized.

Copy link
Member

xrchz commented Dec 25, 2018

Do we know what's wrong?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.