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

Add handling of polymorphic constants #604

Merged
merged 5 commits into from
Aug 27, 2024
Merged

Add handling of polymorphic constants #604

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7742a4f
feat: beginning of handling of polymorphic constants
clarus Aug 26, 2024
91d4b60
feat: more for the addition of polymorphic constants
clarus Aug 27, 2024
ca32ac2
ci: add the c option to rsync to avoid recompiling files that did not…
clarus Aug 27, 2024
b573802
feat: end of add poly consts
clarus Aug 27, 2024
02aac92
feat: repeat with a Value.t as parameter
clarus Aug 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
12 changes: 6 additions & 6 deletions .github/workflows/rust.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ jobs:
cargo build
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/alloc/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/alloc/ --include='*/' --include='*.v' --exclude='*'
cd ../../../..
endGroup
startGroup "Translate the core library"
Expand All @@ -73,7 +73,7 @@ jobs:
cargo build
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --exclude='*'
cd ../../../..
endGroup
startGroup "Translate Revm"
Expand All @@ -86,28 +86,28 @@ jobs:
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/revm/translations/interpreter/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/revm/translations/interpreter/ --include='*/' --include='*.v' --exclude='*'
cd ..
# precompile
cd precompile
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/revm/translations/precompile/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/revm/translations/precompile/ --include='*/' --include='*.v' --exclude='*'
cd ..
# primitives
cd primitives
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/revm/translations/primitives/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/revm/translations/primitives/ --include='*/' --include='*.v' --exclude='*'
cd ..
# revm
cd revm
cargo coq-of-rust
touch src/lib.rs
cargo coq-of-rust
rsync -av src/ ../../../../CoqOfRust/revm/translations/revm/ --include='*/' --include='*.v' --exclude='*'
rsync -acv src/ ../../../../CoqOfRust/revm/translations/revm/ --include='*/' --include='*.v' --exclude='*'
cd ..
cd ../../..
endGroup
Expand Down
24 changes: 12 additions & 12 deletions CoqOfRust/CoqOfRust.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,12 +49,12 @@ Module FunctionTraitAutomaticImpl.
"core::ops::function::Fn"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
(* Instance *) [ ("call", InstanceField.Method (fun ε τ α =>
match ε, τ, α with
| [], [], [self; Value.Tuple args] =>
let* self := M.read self in
M.call_closure self args
| _, _ => M.impossible
| _, _, _ => M.impossible
end
)) ].

Expand All @@ -64,12 +64,12 @@ Module FunctionTraitAutomaticImpl.
"core::ops::function::FnMut"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call_mut", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
(* Instance *) [ ("call_mut", InstanceField.Method (fun ε τ α =>
match ε, τ, α with
| [], [], [self; Value.Tuple args] =>
let* self := M.read self in
M.call_closure self args
| _, _ => M.impossible
| _, _, _ => M.impossible
end
)) ].

Expand All @@ -79,11 +79,11 @@ Module FunctionTraitAutomaticImpl.
"core::ops::function::FnOnce"
(Ty.function Args Output)
(* Trait polymorphic types *) [Ty.tuple Args]
(* Instance *) [ ("call_once", InstanceField.Method (fun τ α =>
match τ, α with
| [], [self; Value.Tuple args] =>
(* Instance *) [ ("call_once", InstanceField.Method (fun ε τ α =>
match ε, τ, α with
| [], [], [self; Value.Tuple args] =>
M.call_closure self args
| _, _ => M.impossible
| _, _, _ => M.impossible
end
)) ].
End FunctionTraitAutomaticImpl.
61 changes: 34 additions & 27 deletions CoqOfRust/M.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,26 +23,6 @@ Notation "{ x @ P }" := (sigS (fun x => P)) : type_scope.
Notation "{ x : A @ P }" := (sigS (A := A) (fun x => P)) : type_scope.
Notation "{ ' pat : A @ P }" := (sigS (A := A) (fun pat => P)) : type_scope.

Module Ty.
Parameter t : Set.

Parameter path : string -> t.

Parameter apply : t -> list t -> t.

Parameter function : list t -> t -> t.

Parameter tuple : list t -> t.

(** As parameter: a list of traits, described by their absolute name and their
list of type parameters, excluding `Self`. *)
Parameter dyn : list (string * list t) -> t.

(** This primitive is for associated types; it will require additional
parameters. *)
Parameter associated : t.
End Ty.

Module List.
Fixpoint assoc {A : Set} (l : list (string * A)) (key : string) : option A :=
match l with
Expand Down Expand Up @@ -319,6 +299,26 @@ Module Value.
Qed.
End Value.

Module Ty.
Parameter t : Set.

Parameter path : string -> t.

Parameter apply : t -> list Value.t -> list t -> t.

Parameter function : list t -> t -> t.

Parameter tuple : list t -> t.

(** As parameter: a list of traits, described by their absolute name and their
list of type parameters, excluding `Self`. *)
Parameter dyn : list (string * list t) -> t.

(** This primitive is for associated types; it will require additional
parameters. *)
Parameter associated : t.
End Ty.

Module Primitive.
Inductive t : Set :=
| StateAlloc (value : Value.t)
Expand Down Expand Up @@ -402,10 +402,15 @@ Definition let_user_monadic (e1 : M) (e2 : Value.t -> M) : M :=
| inr error => LowM.Pure (inr error)
end).

Module PolymorphicFunction.
Definition t : Set :=
list Value.t -> list Ty.t -> list Value.t -> M.
End PolymorphicFunction.

Module InstanceField.
Inductive t : Set :=
| Constant (constant : Value.t)
| Method (method : list Ty.t -> list Value.t -> M)
| Method (method : PolymorphicFunction.t)
| Ty (ty : Ty.t).
End InstanceField.

Expand All @@ -424,14 +429,14 @@ Parameter IsTraitInstance :
Parameter IsFunction :
forall
(name : string)
(function : list Ty.t -> list Value.t -> M),
(function : PolymorphicFunction.t),
Prop.

Parameter IsAssociatedFunction :
forall
(Self : Ty.t)
(function_name : string)
(function : list Ty.t -> list Value.t -> M),
(function : PolymorphicFunction.t),
Prop.

Parameter IsAssociatedConstant :
Expand All @@ -445,7 +450,7 @@ Parameter IsProvidedMethod :
forall
(trait_name : string)
(method_name : string)
(method : Ty.t -> list Ty.t -> list Value.t -> M),
(method : Ty.t -> PolymorphicFunction.t),
Prop.

Module IsTraitMethod.
Expand All @@ -454,16 +459,16 @@ Module IsTraitMethod.
(self_ty : Ty.t)
(trait_tys : list Ty.t)
(method_name : string) :
(list Ty.t -> list Value.t -> M) -> Prop :=
| Explicit (instance : Instance.t) (method : list Ty.t -> list Value.t -> M) :
(PolymorphicFunction.t) -> Prop :=
| Explicit (instance : Instance.t) (method : PolymorphicFunction.t) :
M.IsTraitInstance
trait_name
self_ty
trait_tys
instance ->
List.assoc instance method_name = Some (InstanceField.Method method) ->
t trait_name self_ty trait_tys method_name method
| Implicit (instance : Instance.t) (method : Ty.t -> list Ty.t -> list Value.t -> M) :
| Implicit (instance : Instance.t) (method : Ty.t -> PolymorphicFunction.t) :
M.IsTraitInstance
trait_name
self_ty
Expand Down Expand Up @@ -829,4 +834,6 @@ Definition constructor_as_closure (constructor : string) : Value.t :=

Parameter struct_record_update : Value.t -> list (string * Value.t) -> Value.t.

Parameter unevaluated_const : Value.t -> Value.t.

Parameter yield : Value.t -> M.
Loading
Loading