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.

Sign up for GitHub

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

Moving FStar.Getopt -> FStarC.Getopt #148

Merged
merged 1 commit into from
Oct 11, 2024
Merged

Moving FStar.Getopt -> FStarC.Getopt #148

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/3d/FStar.Getopt.fsti → src/3d/FStarC.Getopt.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
See the License for the specific language governing permissions and
limitations under the License.
*)
module FStar.Getopt
module FStarC.Getopt
open FStar.ST
open FStar.All
open FStar.Char
Expand Down
2 changes: 1 addition & 1 deletion src/3d/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ export KRML_HOME?=$(realpath ../../../karamel)

INCLUDE_PATHS=
OTHERFLAGS?=
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS) $(addprefix --include , $(INCLUDE_PATHS) $(EVERPARSE_HOME)/src/3d/prelude) --already_cached 'Prims FStar -FStar.Getopt'
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS) $(addprefix --include , $(INCLUDE_PATHS) $(EVERPARSE_HOME)/src/3d/prelude) --already_cached 'Prims FStar -FStarC'

all: 3d prelude

Expand Down
30 changes: 15 additions & 15 deletions src/3d/Options.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ type cmd_option_kind =
(v: ref (list (valid_string valid))) ->
cmd_option_kind

let fstar_opt = FStar.Getopt.opt & string
let fstar_opt = FStarC.Getopt.opt & string

noeq
type cmd_option
Expand Down Expand Up @@ -167,7 +167,7 @@ let cmd_option_arg_desc (a: cmd_option) : Tot string =
match a with
| CmdFStarOption ((_, _, arg), _) ->
begin match arg with
| FStar.Getopt.OneArg (_, argdesc) -> argdesc
| FStarC.Getopt.OneArg (_, argdesc) -> argdesc
| _ -> ""
end
| CmdOption _ kind _ _ ->
Expand Down Expand Up @@ -206,15 +206,15 @@ let fstar_options_of_cmd_option
begin match kind with
| OptBool v ->
[
((FStar.Getopt.noshort, name, FStar.Getopt.ZeroArgs (fun _ -> set_implies options implies; v := true)), desc);
((FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := false)), negate_description desc);
((FStarC.Getopt.noshort, name, FStarC.Getopt.ZeroArgs (fun _ -> set_implies options implies; v := true)), desc);
((FStarC.Getopt.noshort, negate_name name, FStarC.Getopt.ZeroArgs (fun _ -> v := false)), negate_description desc);
]
| OptStringOption arg_desc valid v ->
[
(
(
FStar.Getopt.noshort, name,
FStar.Getopt.OneArg (
FStarC.Getopt.noshort, name,
FStarC.Getopt.OneArg (
(fun (x: string) ->
if valid x
then begin
Expand All @@ -228,14 +228,14 @@ let fstar_options_of_cmd_option
),
desc
);
((FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := None)), negate_description desc)
((FStarC.Getopt.noshort, negate_name name, FStarC.Getopt.ZeroArgs (fun _ -> v := None)), negate_description desc)
]
| OptList arg_desc valid v ->
[
(
(
FStar.Getopt.noshort, name,
FStar.Getopt.OneArg (
FStarC.Getopt.noshort, name,
FStarC.Getopt.OneArg (
(fun (x: string) ->
if valid x
then begin
Expand All @@ -251,8 +251,8 @@ let fstar_options_of_cmd_option
);
(
(
FStar.Getopt.noshort, negate_name name,
FStar.Getopt.ZeroArgs (fun _ -> v := [])
FStarC.Getopt.noshort, negate_name name,
FStarC.Getopt.ZeroArgs (fun _ -> v := [])
),
desc
);
Expand Down Expand Up @@ -342,7 +342,7 @@ let (display_usage_2, compute_options_2, fstar_options) =
CmdOption "input_stream_include" (OptStringOption ".h file" always_valid input_stream_include) "Include file defining the EverParseInputStreamBase type (only for --input_stream extern or static)" [];
CmdOption "no_copy_everparse_h" (OptBool no_copy_everparse_h) "Do not Copy EverParse.h (--batch only)" [];
CmdOption "debug" (OptBool debug) "Emit a lot of debugging output" [];
CmdFStarOption (('h', "help", FStar.Getopt.ZeroArgs (fun _ -> display_usage (); exit 0)), "Show this help message");
CmdFStarOption (('h', "help", FStarC.Getopt.ZeroArgs (fun _ -> display_usage (); exit 0)), "Show this help message");
CmdOption "json" (OptBool json) "Dump the AST in JSON format" [];
CmdOption "makefile" (OptStringOption "gmake|nmake" valid_makefile makefile) "Do not produce anything, other than a Makefile to produce everything" [];
CmdOption "makefile_name" (OptStringOption "some file name" always_valid makefile_name) "Name of the Makefile to produce (with --makefile, default <output directory>/EverParse.Makefile" [];
Expand All @@ -352,7 +352,7 @@ let (display_usage_2, compute_options_2, fstar_options) =
CmdOption "skip_c_makefiles" (OptBool skip_c_makefiles) "Do not Generate Makefile.basic, Makefile.include" [];
CmdOption "skip_o_rules" (OptBool skip_o_rules) "With --makefile, do not generate rules for .o files" [];
CmdOption "test_checker" (OptStringOption "parser name" always_valid test_checker) "produce a test checker executable" [];
CmdFStarOption ((let open FStar.Getopt in noshort, "version", ZeroArgs (fun _ -> FStar.IO.print_string (Printf.sprintf "EverParse/3d %s\nCopyright 2018, 2019, 2020 Microsoft Corporation\n" Version.everparse_version); exit 0)), "Show this version of EverParse");
CmdFStarOption ((let open FStarC.Getopt in noshort, "version", ZeroArgs (fun _ -> FStar.IO.print_string (Printf.sprintf "EverParse/3d %s\nCopyright 2018, 2019, 2020 Microsoft Corporation\n" Version.everparse_version); exit 0)), "Show this version of EverParse");
CmdOption "equate_types" (OptList "an argument of the form A,B, to generate asserts of the form (A.t == B.t)" valid_equate_types equate_types_list) "Takes an argument of the form A,B and then for each entrypoint definition in B, it generates an assert (A.t == B.t) in the B.Types file, useful when refactoring specs, you can provide multiple equate_types on the command line" [];
CmdOption "z3_branch_depth" (OptStringOption "nb" always_valid z3_branch_depth) "enumerate branch choices up to depth nb (default 0)" [];
CmdOption "z3_diff_test" (OptStringOption "parser1,parser2" valid_equate_types z3_diff_test) "produce differential tests for two parsers" [];
Expand All @@ -376,8 +376,8 @@ let display_usage = display_usage_2
let compute_options = compute_options_2

let parse_cmd_line () : ML (list string) =
let open FStar.Getopt in
let res = FStar.Getopt.parse_cmdline (List.Tot.map fst fstar_options) (fun file -> input_file := file :: !input_file; Success) in
let open FStarC.Getopt in
let res = FStarC.Getopt.parse_cmdline (List.Tot.map fst fstar_options) (fun file -> input_file := file :: !input_file; Success) in
match res with
| Success -> !input_file
| Help -> display_usage(); exit 0
Expand Down
Loading