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

Jump to bottom

Fact_for63 evaluation #119

Merged
merged 2 commits into from
Jul 27, 2023
Merged

Fact_for63 evaluation #119

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3e0e81d
regularize names and add fact_for63 evaluation example
garrigue Jul 27, 2023
cd60d9d
hide dirty type parameters
garrigue Jul 27, 2023
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
46 changes: 27 additions & 19 deletions example_typed_store.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,9 +53,7 @@

Definition val_nonempty (M : UU0 -> UU0) := tt.

Definition locT := [eqType of nat].

Notation loc := (@loc _ locT).
Notation loc := (@loc _ monad_model.locT_nat).

Inductive rlist (a : Type) (a_1 : ml_type) :=
| Nil
Expand All @@ -67,7 +65,7 @@
End MLTypes.
(******************************************************************************)

Module MLTypesNat.
Module CoqTypeNat.
Import MLTypes.

Section with_monad.
Expand All @@ -84,18 +82,19 @@
end.
End with_monad.

(* use coq_type_nat (typed_store_model.v) *)
(* Standard definition using [coq_type_nat M] (typed_store_model.v) *)
HB.instance Definition _ := @isML_universe.Build ml_type
(Equality.class ml_type_eqType) coq_type_nat ml_unit val_nonempty.

(* alternative: use coq_type_nat0 (monad_model.v) *)
(*Definition coq_type_nat0 := @coq_type_nat idfun.
HB.instance Definition _ := @isML_universe.Build ml_type
(Equality.class ml_type_eqType) (fun M => @coq_type_nat0) ml_unit
(fun M => val_nonempty idfun).*)
(* Alternative: use [coq_type_nat idfun] (monad_model.v) *)
(*HB.instance Definition _ := @isML_universe.Build ml_type
(Equality.class ml_type_eqType) (fun M => @coq_type_nat idfun)
ml_unit (fun M => val_nonempty idfun).*)

Definition typedStoreMonad := typedStoreMonad ml_type monad_model.locT_nat.

Section cyclic.
Variables (M : typedStoreMonad ml_type MLTypes.locT).
Variables (M : typedStoreMonad).
Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)).
Local Open Scope do_notation.

Expand Down Expand Up @@ -130,7 +129,7 @@
End cyclic.

Section factorial.
Variable M : typedStoreMonad ml_type MLTypes.locT.
Variable M : typedStoreMonad.
Notation coq_type := (@coq_type M).

Fixpoint fact_ref (r : loc ml_int) (n : nat) : M unit :=
Expand All @@ -156,7 +155,7 @@
End factorial.

Section fact_for.
Variable M : typedStoreMonad ml_type MLTypes.locT.
Variable M : typedStoreMonad.
Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)).
Local Open Scope do_notation.

Expand Down Expand Up @@ -197,7 +196,7 @@
End fact_for.

Section fibonacci.
Variable M : typedStoreMonad ml_type MLTypes.locT.
Variable M : typedStoreMonad.
Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)).

Fixpoint fibo_rec n :=
Expand Down Expand Up @@ -252,7 +251,7 @@
Qed.
End fibonacci.

End MLTypesNat.
End CoqTypeNat.

Require Import PrimInt63.
Require Sint63.
Expand Down Expand Up @@ -403,7 +402,7 @@
Qed.
End Int63.

Module MLtypes63.
Module CoqTypeInt63.
Import MLTypes.

(******************************************************************************)
Expand All @@ -423,13 +422,17 @@
End with_monad.
(******************************************************************************)

(* Standard definition *)
HB.instance Definition _ := @isML_universe.Build ml_type
(Equality.class ml_type_eqType) coq_type63 ml_unit val_nonempty.

(*Canonical ml_type63 := @Build_ML_universe _ coq_type63 ml_unit val_nonempty.*)
(* Alternative: use [coq_type63 idfun] (monad_model.v) *)
(*HB.instance Definition _ := @isML_universe.Build ml_type
(Equality.class ml_type_eqType) (fun M => @coq_type63 idfun)
ml_unit (fun M => val_nonempty idfun).*)

Section fact_for_int63.
Variable M : typedStoreMonad ml_type MLTypes.locT.
Variable M : typedStoreMonad ml_type monad_model.locT_nat.
Local Notation coq_type := (hierarchy.coq_type (MonadTypedStore.sort M)).
Local Open Scope do_notation.

Expand Down Expand Up @@ -546,7 +549,7 @@
End fact_for_int63.

Section eval.
Require Import typed_store_model.

Check warning on line 552 in example_typed_store.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:1.16.0-coq-8.16) 

Use of “Require” inside a section is fragile. It is not recommended

Check warning on line 552 in example_typed_store.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:1.16.0-coq-8.16) 

Use of “Require” inside a module is fragile. It is not recommended

Check warning on line 552 in example_typed_store.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:1.16.0-coq-8.17) 

Use of “Require” inside a section is fragile. It is not recommended

Check warning on line 552 in example_typed_store.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:1.16.0-coq-8.17) 

Use of “Require” inside a module is fragile. It is not recommended

Check warning on line 552 in example_typed_store.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:1.17.0-coq-8.16) 

Use of “Require” inside a section is fragile. It is not recommended

Check warning on line 552 in example_typed_store.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:1.17.0-coq-8.16) 

Use of “Require” inside a module is fragile. It is not recommended

Check warning on line 552 in example_typed_store.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:1.17.0-coq-8.17) 

Use of “Require” inside a section is fragile. It is not recommended

Check warning on line 552 in example_typed_store.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:1.17.0-coq-8.17) 

Use of “Require” inside a module is fragile. It is not recommended

Definition M := [the typedStoreMonad ml_type monad_model.locT_nat of
acto ml_type].
Expand All @@ -558,6 +561,8 @@
Definition it0 : W unit := inr (tt, empty_env).

Local Open Scope do_notation.
Local Notation mkloc := (mkloc (locT:=monad_model.locT_nat)).
Local Notation coq_type := (coq_type _).

Definition incr (l : loc ml_int) : M int :=
do x <- cget l; do _ <- cput l (Uint63.succ x); Ret (Uint63.succ x).
Expand All @@ -571,6 +576,9 @@
Definition it2 := Restart it1 (do l <- FromW l; incr l).
Eval vm_compute in it2.

Definition it3 := Restart it2 (fact_for63 _ 5)%uint63.
Eval vm_compute in it3.

End eval.

End MLtypes63.
End CoqTypeInt63.
Loading