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->FStarC #237

Merged
merged 9 commits into from
Oct 11, 2024
Merged

Moving FStar->FStarC #237

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
acd7d37
Passing in --MLish_effect FStarC.Compiler.Effect
mtzguido Oct 11, 2024
0a435df
syntax_extension: open FStarC
mtzguido Oct 11, 2024
14d9520
FStar->FStarC, result of a script
mtzguido Oct 11, 2024
93d8a0a
Rename parser file
mtzguido Oct 11, 2024
e3f7847
Update dune file
mtzguido Oct 11, 2024
273794e
snap, as usual
mtzguido Oct 11, 2024
19c24bd
Fix pulse2rust
mtzguido Oct 11, 2024
207074d
snap
mtzguido Oct 11, 2024
135175b
another snap
mtzguido Oct 11, 2024
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
3 changes: 2 additions & 1 deletion pulse2rust/src/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ include $(FSTAR_HOME)/src/Makefile.boot.common

CACHE_DIR = $(CURDIR)
OUTPUT_DIRECTORY = $(CURDIR)/ocaml/generated
FSTAR_BOOT_OPTIONS += --MLish_effect FStarC.Compiler.Effect
FSTAR_C=$(RUNLIM) $(FSTAR_EXE) $(SIL) $(FSTAR_BOOT_OPTIONS) --include $(FSTAR_HOME)/src/.cache.boot --cache_checked_modules

# Would be nice to add --already_cached 'Prims FStar'
Expand Down Expand Up @@ -40,7 +41,7 @@ include .depend
$(call msg, "EXTRACT", $(notdir $@))
$(Q)$(BENCHMARK_PRE) $(FSTAR_C) $(notdir $(subst .checked.lax,,$<)) \
--odir $(OUTPUT_DIRECTORY) \
--codegen OCaml \
--codegen OCaml --MLish \
--extract_module $(basename $(notdir $(subst .checked.lax,,$<)))

extract: $(ALL_ML_FILES)
17 changes: 9 additions & 8 deletions pulse2rust/src/Pulse2Rust.Deps.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,23 +16,24 @@

module Pulse2Rust.Deps

open FStar.Compiler
open FStar.Compiler.Util
open FStar.Compiler.List
open FStar.Compiler.Effect
open FStarC
open FStarC.Compiler
open FStarC.Compiler.Util
open FStarC.Compiler.List
open FStarC.Compiler.Effect

open Pulse2Rust.Rust.Syntax
open Pulse2Rust.Env
open Pulse2Rust.Extract

open RustBindings

open FStar.Class.Setlike
open FStarC.Class.Setlike

module S = FStar.Extraction.ML.Syntax
module EUtil = FStar.Extraction.ML.Util
module S = FStarC.Extraction.ML.Syntax
module EUtil = FStarC.Extraction.ML.Util

module UEnv = FStar.Extraction.ML.UEnv
module UEnv = FStarC.Extraction.ML.UEnv

let empty_defs : reachable_defs = RBSet.empty ()
let singleton (p:S.mlpath) : reachable_defs = singleton (S.string_of_mlpath p)
Expand Down
14 changes: 7 additions & 7 deletions pulse2rust/src/Pulse2Rust.Deps.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,21 +16,21 @@

module Pulse2Rust.Deps

open FStar.Compiler
open FStar.Compiler.Util
open FStar.Compiler.List
open FStar.Compiler.Effect
open FStarC.Compiler
open FStarC.Compiler.Util
open FStarC.Compiler.List
open FStarC.Compiler.Effect

open Pulse2Rust.Rust.Syntax
open Pulse2Rust.Env
open Pulse2Rust.Extract

open RustBindings

module S = FStar.Extraction.ML.Syntax
module EUtil = FStar.Extraction.ML.Util
module S = FStarC.Extraction.ML.Syntax
module EUtil = FStarC.Extraction.ML.Util

module UEnv = FStar.Extraction.ML.UEnv
module UEnv = FStarC.Extraction.ML.UEnv

val empty_defs : reachable_defs

Expand Down
14 changes: 7 additions & 7 deletions pulse2rust/src/Pulse2Rust.Env.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,20 @@

module Pulse2Rust.Env

open FStar.Compiler
open FStar.Compiler.Util
open FStar.Compiler.List
open FStar.Compiler.Effect
open FStarC.Compiler
open FStarC.Compiler.Util
open FStarC.Compiler.List
open FStarC.Compiler.Effect

open FStar.Class.Setlike
open FStarC.Class.Setlike

open Pulse2Rust.Rust.Syntax

open RustBindings

module S = FStar.Extraction.ML.Syntax
module S = FStarC.Extraction.ML.Syntax

module UEnv = FStar.Extraction.ML.UEnv
module UEnv = FStarC.Extraction.ML.UEnv

let fail (s:string) =
failwith (format1 "Pulse to Rust extraction failed: %s" s)
Expand Down
12 changes: 6 additions & 6 deletions pulse2rust/src/Pulse2Rust.Env.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,16 +16,16 @@

module Pulse2Rust.Env

open FStar.Compiler
open FStar.Compiler.Util
open FStar.Compiler.List
open FStar.Compiler.Effect
open FStarC.Compiler
open FStarC.Compiler.Util
open FStarC.Compiler.List
open FStarC.Compiler.Effect

open Pulse2Rust.Rust.Syntax

module S = FStar.Extraction.ML.Syntax
module S = FStarC.Extraction.ML.Syntax

module UEnv = FStar.Extraction.ML.UEnv
module UEnv = FStarC.Extraction.ML.UEnv

val fail (s:string) : 'a

Expand Down
32 changes: 16 additions & 16 deletions pulse2rust/src/Pulse2Rust.Extract.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,20 @@

module Pulse2Rust.Extract

open FStar.Compiler
open FStar.Compiler.Util
open FStar.Compiler.List
open FStar.Compiler.Effect
open FStarC.Compiler
open FStarC.Compiler.Util
open FStarC.Compiler.List
open FStarC.Compiler.Effect

open Pulse2Rust.Rust.Syntax
open Pulse2Rust.Env

open RustBindings

module S = FStar.Extraction.ML.Syntax
module EUtil = FStar.Extraction.ML.Util
module S = FStarC.Extraction.ML.Syntax
module EUtil = FStarC.Extraction.ML.Util

module UEnv = FStar.Extraction.ML.UEnv
module UEnv = FStarC.Extraction.ML.UEnv

//
// 'a to A
Expand Down Expand Up @@ -73,7 +73,7 @@ let lookup_datacon (g:env) (s:S.mlident) : option (list string & S.mlsymbol) =
let ropt = find_map decls (lookup_datacon_in_module1 s) in
match ropt with
| None -> None
| Some tname -> Some (FStar.Compiler.Util.split k ".", tname)
| Some tname -> Some (FStarC.Compiler.Util.split k ".", tname)
)

//
Expand Down Expand Up @@ -374,16 +374,16 @@ let extract_mlconstant_to_lit (c:S.mlconstant) : lit =
| S.MLC_Int (lit_int_val, swopt) ->
let lit_int_signed =
match swopt with
| Some (FStar.Const.Unsigned, _) -> Some false
| Some (FStar.Const.Signed, _) -> Some true
| Some (FStarC.Const.Unsigned, _) -> Some false
| Some (FStarC.Const.Signed, _) -> Some true
| None -> None in
let lit_int_width =
match swopt with
| Some (_, FStar.Const.Int8) -> Some I8
| Some (_, FStar.Const.Int16) -> Some I16
| Some (_, FStar.Const.Int32) -> Some I32
| Some (_, FStar.Const.Int64) -> Some I64
| Some (_, FStar.Const.Sizet) -> Some I64 // TODO: FIXME
| Some (_, FStarC.Const.Int8) -> Some I8
| Some (_, FStarC.Const.Int16) -> Some I16
| Some (_, FStarC.Const.Int32) -> Some I32
| Some (_, FStarC.Const.Int64) -> Some I64
| Some (_, FStarC.Const.Sizet) -> Some I64 // TODO: FIXME
| None -> None in
Lit_int {lit_int_val; lit_int_signed; lit_int_width}
| S.MLC_Bool b -> Lit_bool b
Expand Down Expand Up @@ -890,7 +890,7 @@ let extract_generic_type_param_trait_bounds (attrs:list S.mlexpr) : list (list s
match e.expr with
| MLE_Const (MLC_String s) -> s
| _ -> failwith "unexpected generic type param bounds")
|> List.map (fun bound -> FStar.Compiler.Util.split bound "::"))
|> List.map (fun bound -> FStarC.Compiler.Util.split bound "::"))
|> dflt []

let extract_generic_type_params (tyvars:list S.ty_param)
Expand Down
10 changes: 5 additions & 5 deletions pulse2rust/src/Pulse2Rust.Extract.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,15 @@

module Pulse2Rust.Extract

open FStar.Compiler
open FStar.Compiler.Util
open FStar.Compiler.List
open FStar.Compiler.Effect
open FStarC.Compiler
open FStarC.Compiler.Util
open FStarC.Compiler.List
open FStarC.Compiler.Effect

open Pulse2Rust.Rust.Syntax
open Pulse2Rust.Env

module S = FStar.Extraction.ML.Syntax
module S = FStarC.Extraction.ML.Syntax

val extract_mlty (g:env) (t:S.mlty) : typ

Expand Down
4 changes: 2 additions & 2 deletions pulse2rust/src/Pulse2Rust.Rust.Syntax.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@

module Pulse2Rust.Rust.Syntax

open FStar.Compiler.Effect
open FStarC.Compiler.Effect

module L = FStar.Compiler.List
module L = FStarC.Compiler.List

let vec_new_fn = "vec_new"
let panic_fn = "panic"
Expand Down
2 changes: 1 addition & 1 deletion pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@

module Pulse2Rust.Rust.Syntax

open FStar.Compiler.Effect
open FStarC.Compiler.Effect

type lit_int_width =
| I8
Expand Down
18 changes: 9 additions & 9 deletions pulse2rust/src/Pulse2Rust.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,10 @@

module Pulse2Rust

open FStar.Compiler
open FStar.Compiler.Util
open FStar.Compiler.List
open FStar.Compiler.Effect
open FStarC.Compiler
open FStarC.Compiler.Util
open FStarC.Compiler.List
open FStarC.Compiler.Effect

open Pulse2Rust.Deps
open Pulse2Rust.Rust.Syntax
Expand All @@ -28,12 +28,12 @@ open Pulse2Rust.Extract

open RustBindings

open FStar.Class.Setlike
open FStarC.Class.Setlike

module S = FStar.Extraction.ML.Syntax
module EUtil = FStar.Extraction.ML.Util
module S = FStarC.Extraction.ML.Syntax
module EUtil = FStarC.Extraction.ML.Util

module UEnv = FStar.Extraction.ML.UEnv
module UEnv = FStarC.Extraction.ML.UEnv

let mlmodule1_name (m:S.mlmodule1) : list S.mlsymbol =
let open S in
Expand Down Expand Up @@ -182,7 +182,7 @@ let extract (files:list string) (odir:string) (libs:string) : unit =
let root_module = file_to_module_name (let root_file::_ = files in root_file) in
// print1 "root_module: %s\n" root_module;
let reachable_defs = collect_reachable_defs d root_module in
let external_libs = FStar.Compiler.Util.split libs "," |> List.map trim_string in
let external_libs = FStarC.Compiler.Util.split libs "," |> List.map trim_string in
let g = empty_env external_libs d all_modules reachable_defs in
let _, all_rust_files = List.fold_left (fun (g, all_rust_files) f ->
// print1 "Extracting file: %s\n" f;
Expand Down
2 changes: 1 addition & 1 deletion pulse2rust/src/RustBindings.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@

module RustBindings

open FStar.Compiler.Effect
open FStarC.Compiler.Effect

open Pulse2Rust.Rust.Syntax

Expand Down
Loading
Loading