Skip to content

Commit

Permalink
share typed_store_universe
Browse files Browse the repository at this point in the history
  • Loading branch information
@garrigue
garrigue committed Jan 14, 2025
1 parent d97ca57 commit e45028a
Show file tree
Hide file tree
Showing 4 changed files with 119 additions and 140 deletions.
1 change: 1 addition & 0 deletions _CoqProject
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ theories/applications/example_relabeling.v
theories/applications/example_quicksort.v
theories/applications/example_iquicksort.v
theories/applications/example_monty.v
theories/applications/typed_store_universe.v
theories/applications/example_typed_store.v
theories/applications/smallstep.v
theories/applications/example_transformer.v
Expand Down
63 changes: 4 additions & 59 deletions theories/applications/example_delay_typed_store.v
View file
Original file line number Diff line number Diff line change
@@ -1,77 +1,22 @@
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later *)
Require Import ZArith Morphisms.
Require Import Morphisms.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import ssrZ.
Require Import monad_model.
From HB Require Import structures.
Require Import preamble hierarchy monad_lib typed_store_lib.
Require Import typed_store_universe.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope monae_scope.

(******************************************************************************)
(* generated by coqgen *)
(******************************************************************************)
Module MLTypes.
Inductive ml_type : Set :=
| ml_int
| ml_bool
| ml_unit
| ml_ref (_ : ml_type)
| ml_arrow (_ : ml_type) (_ : ml_type)
| ml_rlist (_ : ml_type).

Definition ml_type_eq_dec (T1 T2 : ml_type) : {T1=T2}+{T1<>T2}.
revert T2; induction T1; destruct T2;
try (right; intro; discriminate); try (now left);
try (case (IHT1_5 T2_5); [|right; injection; intros; contradiction]);
try (case (IHT1_4 T2_4); [|right; injection; intros; contradiction]);
try (case (IHT1_3 T2_3); [|right; injection; intros; contradiction]);
try (case (IHT1_2 T2_2); [|right; injection; intros; contradiction]);
(case (IHT1 T2) || case (IHT1_1 T2_1)); try (left; now subst);
right; injection; intros; contradiction.
Defined.

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

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

Inductive rlist (a : Type) (a_1 : ml_type) :=
| Nil
| Cons (_ : a) (_ : loc (ml_rlist a_1)).

Definition ml_type_eq_mixin := hasDecEq.Build _ (comparePc MLTypes.ml_type_eq_dec).
HB.instance Definition ml_type_eqType := ml_type_eq_mixin.

End MLTypes.
(******************************************************************************)

Module CoqTypeNat.
Import MLTypes.

Section with_monad.
Context [M : Type -> Type].

Fixpoint coq_type_nat (T : ml_type) : Type :=
match T with
| ml_int => nat
| ml_bool => bool
| ml_unit => unit
| ml_arrow T1 T2 => coq_type_nat T1 -> M (coq_type_nat T2)
| ml_ref T1 => loc T1
| ml_rlist T1 => rlist (coq_type_nat T1) T1
end.
End with_monad.

HB.instance Definition _ := @isML_universe.Build ml_type coq_type_nat ml_unit val_nonempty.
Import MLTypes CoqTypeNat.

Definition delayTypedStoreMonad (N : monad) :=
delaytypedStoreMonad ml_type N monad_model.locT_nat.
delaytypedStoreMonad ml_type N nat.

Section factorial.

Expand Down
85 changes: 4 additions & 81 deletions theories/applications/example_typed_store.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ From infotheo Require Import ssrZ.
Require Import monad_model.
From HB Require Import structures.
Require Import preamble hierarchy monad_lib typed_store_lib.
Require Import typed_store_universe.

(******************************************************************************)
(* Typed store examples *)
Expand All @@ -28,67 +29,8 @@ Require Import preamble hierarchy monad_lib typed_store_lib.

Local Open Scope monae_scope.

(******************************************************************************)
(* generated by coqgen *)
(******************************************************************************)
Module MLTypes.
Inductive ml_type : Set :=
| ml_int
| ml_bool
| ml_unit
| ml_ref (_ : ml_type)
| ml_arrow (_ : ml_type) (_ : ml_type)
| ml_rlist (_ : ml_type).

Definition ml_type_eq_dec (T1 T2 : ml_type) : {T1=T2}+{T1<>T2}.
revert T2; induction T1; destruct T2;
try (right; intro; discriminate); try (now left);
try (case (IHT1_5 T2_5); [|right; injection; intros; contradiction]);
try (case (IHT1_4 T2_4); [|right; injection; intros; contradiction]);
try (case (IHT1_3 T2_3); [|right; injection; intros; contradiction]);
try (case (IHT1_2 T2_2); [|right; injection; intros; contradiction]);
(case (IHT1 T2) || case (IHT1_1 T2_1)); try (left; now subst);
right; injection; intros; contradiction.
Defined.

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

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

Inductive rlist (a : Type) (a_1 : ml_type) :=
| Nil
| Cons (_ : a) (_ : loc (ml_rlist a_1)).

Definition ml_type_eq_mixin := hasDecEq.Build _ (comparePc MLTypes.ml_type_eq_dec).
HB.instance Definition ml_type_eqType := ml_type_eq_mixin.

End MLTypes.
(******************************************************************************)

Module CoqTypeNat.
Import MLTypes.

Section with_monad.
Context [M : Type -> Type].

Fixpoint coq_type_nat (T : ml_type) : Type :=
match T with
| ml_int => nat
| ml_bool => bool
| ml_unit => unit
| ml_arrow T1 T2 => coq_type_nat T1 -> M (coq_type_nat T2)
| ml_ref T1 => loc T1
| ml_rlist T1 => rlist (coq_type_nat T1) T1
end.
End with_monad.

HB.instance Definition _ := @isML_universe.Build ml_type coq_type_nat ml_unit val_nonempty.

Definition typedStoreMonad (N : monad) :=
typedStoreMonad ml_type N monad_model.locT_nat.

Definition typedStoreRunMonad (N : monad) :=
typedStoreRunMonad ml_type N monad_model.locT_nat.
Import MLTypes CoqTypeNat.

Section cyclic.
Variables (N : monad) (M : typedStoreMonad N).
Expand Down Expand Up @@ -119,7 +61,7 @@ Arguments Nil {a a_1}.
Arguments Cons {a a_1}.
Arguments rtl {T}.
Notation "x ':::' y" := (Cons x y) (at level 60).
b

Lemma rtl_tl_self T (a b : coq_type N T) :
do l <- cycle T a b; do l1 <- rtl l; rtl l1 = cycle T a b.
Proof.
Expand Down Expand Up @@ -740,26 +682,7 @@ Qed.
End Int63.

Module CoqTypeInt63.
Import MLTypes.

(******************************************************************************)
(* generated by coqgen *)
(******************************************************************************)
Section with_monad.
Context [M : Type -> Type].
Fixpoint coq_type63 (T : ml_type) : Type :=
match T with
| ml_int => int
| ml_bool => bool
| ml_unit => unit
| ml_arrow T1 T2 => coq_type63 T1 -> M (coq_type63 T2)
| ml_ref T1 => loc T1
| ml_rlist T1 => rlist (coq_type63 T1) T1
end.
End with_monad.
(******************************************************************************)

HB.instance Definition _ := @isML_universe.Build ml_type coq_type63 ml_unit val_nonempty.
Import MLTypes CoqTypeInt63.

Section fact_for_int63.
Variable N : monad.
Expand Down
110 changes: 110 additions & 0 deletions theories/applications/typed_store_universe.v
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,110 @@
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later *)
Require Import ZArith.
From mathcomp Require Import all_ssreflect.
Require Import monad_model.
From HB Require Import structures.
Require Import preamble hierarchy monad_lib typed_store_lib.

(******************************************************************************)
(* Typed store universes *)
(* *)
(* Inductive ml_type == generated by coqgen *)
(* *)
(* Module CoqTypeNat *)
(* coq_type_nat == adapted from code generated by coqgen *)
(* *)
(* Module CoqTypeInt63 *)
(* Fixpoint coq_type63 == generated type translation function *)
(******************************************************************************)

Local Open Scope monae_scope.

(******************************************************************************)
(* generated by coqgen *)
(******************************************************************************)
Module MLTypes.
Inductive ml_type : Set :=
| ml_int
| ml_bool
| ml_unit
| ml_ref (_ : ml_type)
| ml_arrow (_ : ml_type) (_ : ml_type)
| ml_rlist (_ : ml_type).

Definition ml_type_eq_dec (T1 T2 : ml_type) : {T1=T2}+{T1<>T2}.
revert T2; induction T1; destruct T2;
try (right; intro; discriminate); try (now left);
try (case (IHT1_5 T2_5); [|right; injection; intros; contradiction]);
try (case (IHT1_4 T2_4); [|right; injection; intros; contradiction]);
try (case (IHT1_3 T2_3); [|right; injection; intros; contradiction]);
try (case (IHT1_2 T2_2); [|right; injection; intros; contradiction]);
(case (IHT1 T2) || case (IHT1_1 T2_1)); try (left; now subst);
right; injection; intros; contradiction.
Defined.

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

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

Inductive rlist (a : Type) (a_1 : ml_type) :=
| Nil
| Cons (_ : a) (_ : loc (ml_rlist a_1)).

Definition ml_type_eq_mixin := hasDecEq.Build _ (comparePc MLTypes.ml_type_eq_dec).
HB.instance Definition ml_type_eqType := ml_type_eq_mixin.

End MLTypes.
(******************************************************************************)

Module CoqTypeNat.
Import MLTypes.

Section with_monad.
Context [M : Type -> Type].

Fixpoint coq_type_nat (T : ml_type) : Type :=
match T with
| ml_int => nat
| ml_bool => bool
| ml_unit => unit
| ml_arrow T1 T2 => coq_type_nat T1 -> M (coq_type_nat T2)
| ml_ref T1 => loc T1
| ml_rlist T1 => rlist (coq_type_nat T1) T1
end.
End with_monad.

HB.instance Definition _ := @isML_universe.Build ml_type coq_type_nat ml_unit val_nonempty.

Definition typedStoreMonad (N : monad) :=
typedStoreMonad ml_type N monad_model.locT_nat.

Definition typedStoreRunMonad (N : monad) :=
typedStoreRunMonad ml_type N monad_model.locT_nat.
End CoqTypeNat.

Require Import PrimInt63.
Require Sint63.

Module CoqTypeInt63.
Import MLTypes.

(******************************************************************************)
(* generated by coqgen *)
(******************************************************************************)
Section with_monad.
Context [M : Type -> Type].
Fixpoint coq_type63 (T : ml_type) : Type :=
match T with
| ml_int => int
| ml_bool => bool
| ml_unit => unit
| ml_arrow T1 T2 => coq_type63 T1 -> M (coq_type63 T2)
| ml_ref T1 => loc T1
| ml_rlist T1 => rlist (coq_type63 T1) T1
end.
End with_monad.
(******************************************************************************)

HB.instance Definition _ := @isML_universe.Build ml_type coq_type63 ml_unit val_nonempty.
End CoqTypeInt63.

0 comments on commit e45028a

Please sign in to comment.