Skip to content

More work on memory alloc #733

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

Merged
merged 4 commits into from
May 19, 2025
Merged

More work on memory alloc #733

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
03e8580
simulate: beginning of work on simulate
clarus May 1, 2025
571c70f
simulate: using more explicit Call
clarus May 1, 2025
5b86b16
simulate: add record_cost gas example
clarus May 1, 2025
9e5e232
simulate: adding test file
clarus May 16, 2025
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
  •  
  •  
  •  
17 changes: 12 additions & 5 deletions CoqOfRust/M.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,9 @@ Module Pointer.

Module Core.
Inductive t (Value : Set) : Set :=
| Immediate (value : Value)
(** The immediate value is optional in case with have a sub-pointer of an immediate pointer for
an enum case that is not the current one. *)
| Immediate (value : option Value)
| Mutable {Address : Set} (address : Address) (path : Path.t).
Arguments Immediate {_}.
Arguments Mutable {_ _}.
Expand Down Expand Up @@ -317,6 +319,7 @@ Module LowM.
| CallClosure (ty : Ty.t) (closure : Value.t) (args : list Value.t) (k : A -> t A)
| CallLogicalOp (op : LogicalOp.t) (lhs : Value.t) (rhs : t A) (k : A -> t A)
| Let (ty : Ty.t) (e : t A) (k : A -> t A)
| LetAlloc (ty : Ty.t) (e : t A) (k : A -> t A)
| Loop (ty : Ty.t) (body : t A) (k : A -> t A)
| MatchTuple (tuple : Value.t) (k : list Value.t -> t A)
| Impossible (message : string).
Expand All @@ -325,6 +328,7 @@ Module LowM.
Arguments CallClosure {_}.
Arguments CallLogicalOp {_}.
Arguments Let {_}.
Arguments LetAlloc {_}.
Arguments Loop {_}.
Arguments MatchTuple {_}.
Arguments Impossible {_}.
Expand All @@ -342,6 +346,8 @@ Module LowM.
Let ty e (fun v => let_ (k v) e2)
| Loop ty body k =>
Loop ty body (fun v => let_ (k v) e2)
| LetAlloc ty e k =>
LetAlloc ty e (fun v => let_ (k v) e2)
| MatchTuple tuple k =>
MatchTuple tuple (fun fields => let_ (k fields) e2)
| Impossible message => Impossible message
Expand Down Expand Up @@ -384,7 +390,7 @@ Definition let_user (ty : Ty.t) (e1 : Value.t) (e2 : Value.t -> Value.t) : Value
e2 e1.

Definition let_user_monadic (ty : Ty.t) (e1 : M) (e2 : Value.t -> M) : M :=
LowM.Let ty e1 (fun v1 =>
LowM.LetAlloc ty e1 (fun v1 =>
match v1 with
| inl v1 => e2 v1
| inr error => LowM.Pure (inr error)
Expand Down Expand Up @@ -696,7 +702,7 @@ Definition get_trait_method
).

Definition catch (ty : Ty.t) (body : M) (handler : Exception.t -> M) : M :=
LowM.Let ty body (fun result =>
LowM.LetAlloc ty (let_ body read) (fun result =>
match result with
| inl v => LowM.Pure (inl v)
| inr exception => handler exception
Expand All @@ -708,7 +714,7 @@ Definition catch_return (ty : Ty.t) (body : M) : M :=
body
(fun exception =>
match exception with
| Exception.Return r => pure r
| Exception.Return r => alloc r
| _ => raise exception
end
).
Expand Down Expand Up @@ -738,7 +744,7 @@ Definition catch_break (ty : Ty.t) (body : M) : M :=
Definition loop (ty : Ty.t) (body : M) : M :=
LowM.Loop
ty
(catch_continue ty body)
(let_ (catch_continue ty body) read)
(fun result =>
catch_break ty (LowM.Pure result)).

Expand Down Expand Up @@ -795,6 +801,7 @@ Definition find_or_pattern
(body : list Value.t -> M) :
M :=
let* free_vars := find_or_pattern_aux arm_ty scrutinee arms in
let* free_vars := M.read free_vars in
LowM.MatchTuple free_vars body.

Definition never_to_any (x : Value.t) : M :=
Expand Down
Loading
Loading