Skip to content

Commit

Permalink
rebase
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Dec 2, 2024
1 parent 702bde5 commit 6db6439
Show file tree
Hide file tree
Showing 7 changed files with 30 additions and 31 deletions.
10 changes: 5 additions & 5 deletions theories/lang_syntax.v
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
Require Import String.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import lra.
From mathcomp Require Import mathcomp_extra boolp classical_sets.
From mathcomp Require Import functions cardinality fsbigop.
Require Import signed reals ereal topology normedtype sequences esum exp.
Require Import measure lebesgue_measure numfun lebesgue_integral itv kernel ftc.
Require Import probability.
Require Import derive realfun charge prob_lang lang_syntax_util.
From mathcomp Require Import lra.
From mathcomp Require Import signed reals ereal topology normedtype sequences.
From mathcomp Require Import esum exp derive realfun measure lebesgue_measure.
From mathcomp Require Import numfun lebesgue_integral itv kernel ftc.
From mathcomp Require Import probability charge prob_lang lang_syntax_util.

(**md**************************************************************************)
(* # Syntax and Evaluation for a Probabilistic Programming Language *)
Expand Down
15 changes: 7 additions & 8 deletions theories/lang_syntax_examples.v
Original file line number Diff line number Diff line change
@@ -1,14 +1,13 @@
Require Import String.
From Coq Require Import String.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp.classical Require Import mathcomp_extra boolp.
From mathcomp Require Import ring.
From mathcomp Require Import classical_sets.
From mathcomp.classical Require Import functions cardinality fsbigop.
Require Import signed reals ereal topology normedtype sequences esum measure.
Require Import lebesgue_measure numfun lebesgue_integral kernel probability.
Require Import prob_lang lang_syntax_util lang_syntax.
From mathcomp Require Import lra.
From mathcomp Require Import ring lra.
From mathcomp Require Import classical_sets functions cardinality fsbigop.
From mathcomp Require Import signed reals ereal topology normedtype sequences.
From mathcomp Require Import esum measure lebesgue_measure numfun.
From mathcomp Require Import lebesgue_integral kernel probability prob_lang.
From mathcomp Require Import lang_syntax_util lang_syntax.

(**md**************************************************************************)
(* # Examples using the Probabilistic Programming Language of lang_syntax.v *)
Expand Down
12 changes: 6 additions & 6 deletions theories/lang_syntax_table_game.v
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
Require Import String.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
From mathcomp.classical Require Import functions cardinality fsbigop.
Require Import signed reals ereal topology normedtype sequences esum measure.
Require Import charge lebesgue_measure numfun lebesgue_integral kernel.
Require Import probability.
Require Import prob_lang lang_syntax_util lang_syntax lang_syntax_examples.
From mathcomp Require Import ring lra.
From mathcomp Require Import mathcomp_extra boolp classical_sets.
From mathcomp Require Import functions cardinality fsbigop.
From mathcomp Require Import signed reals ereal topology normedtype sequences.
From mathcomp Require Import esum measure charge lebesgue_measure numfun.
From mathcomp Require Import lebesgue_integral kernel probability prob_lang.
From mathcomp Require Import lang_syntax_util lang_syntax lang_syntax_examples.

(**md**************************************************************************)
(* # Eddy's table game example *)
Expand Down
6 changes: 3 additions & 3 deletions theories/lang_syntax_toy.v
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
Require Import String Classical.
From Coq Require Import String Classical.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg.
From mathcomp Require Import mathcomp_extra boolp.
Require Import signed reals topology normedtype.
Require Import lang_syntax_util.
From mathcomp Require Import signed reals topology normedtype.
From mathcomp Require Import lang_syntax_util.

(******************************************************************************)
(* Intrinsically-typed concrete syntax for a toy language *)
Expand Down
4 changes: 2 additions & 2 deletions theories/lang_syntax_util.v
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
Require Import String.
From Coq Require Import String.
From HB Require Import structures.
Require Import Classical_Prop. (* NB: to compile with Coq 8.17 *)
From mathcomp Require Import all_ssreflect.
Require Import signed.
From mathcomp Require Import signed.

(******************************************************************************)
(* Shared by lang_syntax_*.v files *)
Expand Down
8 changes: 4 additions & 4 deletions theories/prob_lang.v
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,12 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import rat archimedean.
From mathcomp Require Import lra.
From mathcomp Require Import mathcomp_extra boolp classical_sets.
From mathcomp Require Import functions cardinality fsbigop.
Require Import reals ereal signed topology normedtype sequences esum measure.
Require Import lebesgue_measure numfun lebesgue_integral exp kernel.
Require Import probability.
From mathcomp Require Import lra.
From mathcomp Require Import reals ereal signed topology normedtype sequences.
From mathcomp Require Import esum measure lebesgue_measure numfun.
From mathcomp Require Import lebesgue_integral exp kernel probability.

(**md**************************************************************************)
(* # Semantics of a probabilistic programming language using s-finite kernels *)
Expand Down
6 changes: 3 additions & 3 deletions theories/prob_lang_wip.v
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import signed reals ereal topology normedtype sequences esum measure.
Require Import lebesgue_measure numfun lebesgue_integral exp kernel trigo.
Require Import realfun charge prob_lang.
From mathcomp Require Import signed reals ereal topology normedtype sequences.
From mathcomp Require Import esum measure lebesgue_measure numfun exp trigo.
From mathcomp Require Import realfun lebesgue_integral kernel charge prob_lang.

(******************************************************************************)
(* Semantics of a probabilistic programming language using s-finite kernels *)
Expand Down

0 comments on commit 6db6439

Please sign in to comment.