Refactor the module structure (#66)

* Refactor module structure for easier import * Hide a meaningless warning
Beluga-lang · May 8, 2024 · 3bfedb1 · 3bfedb1
1 parent 6f029e3
commit 3bfedb1
Show file tree

Hide file tree

Showing 20 changed files with 825 additions and 787 deletions.
diff --git a/theories/Core/Base.v b/theories/Core/Base.v
@@ -1,7 +1,7 @@
-#[global] Declare Scope exp_scope.
-#[global] Delimit Scope exp_scope with exp.
-
-#[global] Bind Scope exp_scope with Sortclass.
+#[global] Declare Scope mcltt_scope.
+#[global] Delimit Scope mcltt_scope with mcltt.
+#[global] Bind Scope mcltt_scope with Sortclass.
 
 #[global] Declare Custom Entry judg.
+
 Notation "{{ x }}" := x (at level 0, x custom judg at level 99, format "'{{'  x  '}}'").
diff --git a/theories/Core/Semantic/Domain.v b/theories/Core/Semantic/Domain.v
@@ -1,4 +1,4 @@
-From Mcltt Require Import Syntax.
+From Mcltt Require Export Syntax.
 
 Reserved Notation "'env'".
 
@@ -22,34 +22,39 @@ with domain_nf : Set :=
 | d_dom : domain -> domain -> domain_nf
 where "'env'" := (nat -> domain).
 
-#[global] Declare Custom Entry domain.
-#[global] Bind Scope exp_scope with domain.
-
-Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{'  x  '}}}'") : exp_scope.
-Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : exp_scope.
-Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : exp_scope.
-Notation "x" := x (in custom domain at level 0, x global) : exp_scope.
-Notation "'λ' p M" := (d_fn p M) (in custom domain at level 0, p custom domain at level 30, M custom exp at level 30) : exp_scope.
-Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : exp_scope.
-Notation "'ℕ'" := d_nat (in custom domain) : exp_scope.
-Notation "'𝕌' @ n" := (d_univ n) (in custom domain at level 0, n constr at level 0) : exp_scope.
-Notation "'Π' a p B" := (d_pi a p B) (in custom domain at level 0, a custom domain at level 30, p custom domain at level 0, B custom exp at level 30) : exp_scope.
-Notation "'zero'" := d_zero (in custom domain at level 0) : exp_scope.
-Notation "'succ' m" := (d_succ m) (in custom domain at level 30, m custom domain at level 30) : exp_scope.
-Notation "'rec' m 'under' p 'return' P | 'zero' -> mz | 'succ' -> MS 'end'" := (d_natrec p P mz MS m) (in custom domain at level 0, P custom exp at level 60, mz custom domain at level 60, MS custom exp at level 60, p custom domain at level 60, m custom domain at level 60) : exp_scope.
-Notation "'!' n" := (d_var n) (in custom domain at level 0, n constr at level 0) : exp_scope.
-Notation "'⇑' a m" := (d_neut a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : exp_scope.
-Notation "'⇓' a m" := (d_dom a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : exp_scope.
-Notation "'⇑!' a n" := (d_neut a (d_var n)) (in custom domain at level 0, a custom domain at level 30, n constr at level 0) : exp_scope.
-
-Definition empty_env : env := fun x => d{{{ zero }}}.
+Definition empty_env : env := fun x => d_zero.
 Definition extend_env (p : env) (d : domain) : env :=
   fun n =>
     match n with
     | 0 => d
     | S n' => p n'
     end.
-Notation "p ↦ m" := (extend_env p m) (in custom domain at level 20, left associativity) : exp_scope.
 
 Definition drop_env (p : env) : env := fun n => p (S n).
-Notation "p '↯'" := (drop_env p) (in custom domain at level 10, p custom domain) : exp_scope.
+
+#[global] Declare Custom Entry domain.
+#[global] Bind Scope mcltt_scope with domain.
+
+Module Domain_Notations.
+  Export Syntax_Notations.
+
+  Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{'  x  '}}}'") : mcltt_scope.
+  Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : mcltt_scope.
+  Notation "~ x" := x (in custom domain at level 0, x constr at level 0) : mcltt_scope.
+  Notation "x" := x (in custom domain at level 0, x global) : mcltt_scope.
+  Notation "'λ' p M" := (d_fn p M) (in custom domain at level 0, p custom domain at level 30, M custom exp at level 30) : mcltt_scope.
+  Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : mcltt_scope.
+  Notation "'ℕ'" := d_nat (in custom domain) : mcltt_scope.
+  Notation "'𝕌' @ n" := (d_univ n) (in custom domain at level 0, n constr at level 0) : mcltt_scope.
+  Notation "'Π' a p B" := (d_pi a p B) (in custom domain at level 0, a custom domain at level 30, p custom domain at level 0, B custom exp at level 30) : mcltt_scope.
+  Notation "'zero'" := d_zero (in custom domain at level 0) : mcltt_scope.
+  Notation "'succ' m" := (d_succ m) (in custom domain at level 30, m custom domain at level 30) : mcltt_scope.
+  Notation "'rec' m 'under' p 'return' P | 'zero' -> mz | 'succ' -> MS 'end'" := (d_natrec p P mz MS m) (in custom domain at level 0, P custom exp at level 60, mz custom domain at level 60, MS custom exp at level 60, p custom domain at level 60, m custom domain at level 60) : mcltt_scope.
+  Notation "'!' n" := (d_var n) (in custom domain at level 0, n constr at level 0) : mcltt_scope.
+  Notation "'⇑' a m" := (d_neut a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mcltt_scope.
+  Notation "'⇓' a m" := (d_dom a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mcltt_scope.
+  Notation "'⇑!' a n" := (d_neut a (d_var n)) (in custom domain at level 0, a custom domain at level 30, n constr at level 0) : mcltt_scope.
+
+  Notation "p ↦ m" := (extend_env p m) (in custom domain at level 20, left associativity) : mcltt_scope.
+  Notation "p '↯'" := (drop_env p) (in custom domain at level 10, p custom domain) : mcltt_scope.
+End Domain_Notations.
diff --git a/theories/Core/Semantic/Evaluation.v b/theories/Core/Semantic/Evaluation.v
@@ -1,82 +1 @@
-From Mcltt Require Import Base.
-From Mcltt Require Import Domain.
-From Mcltt Require Import Syntax.
-From Mcltt Require Import System.
-
-Reserved Notation "'⟦' M '⟧' p '↘' r" (in custom judg at level 80, M custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
-Reserved Notation "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" (in custom judg at level 80, m custom domain at level 99, A custom exp at level 99, MZ custom exp at level 99, MS custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
-Reserved Notation "'$|' m '&' n '|↘' r" (in custom judg at level 80, m custom domain at level 99, n custom domain at level 99, r custom domain at level 99).
-Reserved Notation "'⟦' σ '⟧s' p '↘' p'" (in custom judg at level 80, σ custom exp at level 99, p custom domain at level 99, p' custom domain at level 99).
-
-Generalizable All Variables.
-
-Inductive eval_exp : exp -> env -> domain -> Prop :=
-| eval_exp_typ :
-  `( {{ ⟦ Type@i ⟧ p ↘ 𝕌@i }} )
-| eval_exp_nat :
-  `( {{ ⟦ ℕ ⟧ p ↘ ℕ }} )
-| eval_exp_zero :
-  `( {{ ⟦ zero ⟧ p ↘ zero }} )
-| eval_exp_succ :
-  `( {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ ⟦ succ M ⟧ p ↘ succ m }} )
-| eval_exp_natrec :
-  `( {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
-     {{ ⟦ rec M return A | zero -> MZ | succ -> MS end ⟧ p ↘ r }} )
-| eval_exp_pi :
-  `( {{ ⟦ A ⟧ p ↘ a }} ->
-     {{ ⟦ Π A B ⟧ p ↘ Π a p B }} )
-| eval_exp_fn :
-  `( {{ ⟦ λ A M ⟧ p ↘ λ p M }} )
-| eval_exp_app :
-  `( {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ ⟦ N ⟧ p ↘ n }} ->
-     {{ $| m & n |↘ r }} ->
-     {{ ⟦ M N ⟧ p ↘ r }} )
-| eval_exp_sub :
-  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
-     {{ ⟦ M ⟧ p' ↘ m }} ->
-     {{ ⟦ M[σ] ⟧ p ↘ m }} )
-where "'⟦' e '⟧' p '↘' r" := (eval_exp e p r) (in custom judg)
-with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
-| eval_natrec_zero :
-  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
-     {{ rec zero ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ mz }} )
-| eval_natrec_succ :
-  `( {{ rec b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
-     {{ ⟦ MS ⟧ p ↦ b ↦ r ↘ ms }} ->
-     {{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ms }} )
-| eval_natrec_neut :
-  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
-     {{ ⟦ A ⟧ p ↦ ⇑ ℕ m ↘ a }} ->
-     {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ⇑ a (rec m under p return A | zero -> mz | succ -> MS end) }} )
-where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" := (eval_natrec A MZ MS m p r) (in custom judg)
-with eval_app : domain -> domain -> domain -> Prop :=
-| eval_app_fn :
-  `( {{ ⟦ M ⟧ p ↦ n ↘ m }} ->
-     {{ $| λ p M & n |↘ m }} )
-| eval_app_neut :
-  `( {{ ⟦ B ⟧ p ↦ n ↘ b }} ->
-     {{ $| ⇑ (Π a p B) m & n |↘ ⇑ b (m (⇓ a n)) }} )
-where "'$|' m '&' n '|↘' r" := (eval_app m n r) (in custom judg)
-with eval_sub : sub -> env -> env -> Prop :=
-| eval_sub_id :
-  `( {{ ⟦ Id ⟧s p ↘ p }} )
-| eval_sub_weaken :
-  `( {{ ⟦ Wk ⟧s p ↘ p↯ }} )
-| eval_sub_extend :
-  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
-     {{ ⟦ M ⟧ p ↘ m }} ->
-     {{ ⟦ σ ,, M ⟧s p ↘ p' ↦ m }} )
-| eval_sub_compose :
-  `( {{ ⟦ τ ⟧s p ↘ p' }} ->
-     {{ ⟦ σ ⟧s p' ↘ p'' }} ->
-     {{ ⟦ σ ∘ τ ⟧s p ↘ p'' }} )
-where "'⟦' σ '⟧s' p '↘' p'" := (eval_sub σ p p') (in custom judg)
-.
-
-Scheme eval_exp_mut_ind := Induction for eval_exp Sort Prop
-with eval_natrec_mut_ind := Induction for eval_natrec Sort Prop
-with eval_app_mut_ind := Induction for eval_app Sort Prop
-with eval_sub_mut_ind := Induction for eval_sub Sort Prop.
+From Mcltt Require Export EvaluationDefinitions EvaluationLemmas.
diff --git a/theories/Core/Semantic/EvaluationDefinitions.v b/theories/Core/Semantic/EvaluationDefinitions.v
@@ -0,0 +1,81 @@
+From Mcltt Require Import Base.
+From Mcltt Require Export Domain.
+Import Domain_Notations.
+
+Reserved Notation "'⟦' M '⟧' p '↘' r" (in custom judg at level 80, M custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" (in custom judg at level 80, m custom domain at level 99, A custom exp at level 99, MZ custom exp at level 99, MS custom exp at level 99, p custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'$|' m '&' n '|↘' r" (in custom judg at level 80, m custom domain at level 99, n custom domain at level 99, r custom domain at level 99).
+Reserved Notation "'⟦' σ '⟧s' p '↘' p'" (in custom judg at level 80, σ custom exp at level 99, p custom domain at level 99, p' custom domain at level 99).
+
+Generalizable All Variables.
+
+Inductive eval_exp : exp -> env -> domain -> Prop :=
+| eval_exp_typ :
+  `( {{ ⟦ Type@i ⟧ p ↘ 𝕌@i }} )
+| eval_exp_nat :
+  `( {{ ⟦ ℕ ⟧ p ↘ ℕ }} )
+| eval_exp_zero :
+  `( {{ ⟦ zero ⟧ p ↘ zero }} )
+| eval_exp_succ :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ succ M ⟧ p ↘ succ m }} )
+| eval_exp_natrec :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
+     {{ ⟦ rec M return A | zero -> MZ | succ -> MS end ⟧ p ↘ r }} )
+| eval_exp_pi :
+  `( {{ ⟦ A ⟧ p ↘ a }} ->
+     {{ ⟦ Π A B ⟧ p ↘ Π a p B }} )
+| eval_exp_fn :
+  `( {{ ⟦ λ A M ⟧ p ↘ λ p M }} )
+| eval_exp_app :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ N ⟧ p ↘ n }} ->
+     {{ $| m & n |↘ r }} ->
+     {{ ⟦ M N ⟧ p ↘ r }} )
+| eval_exp_sub :
+  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
+     {{ ⟦ M ⟧ p' ↘ m }} ->
+     {{ ⟦ M[σ] ⟧ p ↘ m }} )
+where "'⟦' e '⟧' p '↘' r" := (eval_exp e p r) (in custom judg)
+with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop :=
+| eval_natrec_zero :
+  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
+     {{ rec zero ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ mz }} )
+| eval_natrec_succ :
+  `( {{ rec b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
+     {{ ⟦ MS ⟧ p ↦ b ↦ r ↘ ms }} ->
+     {{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ms }} )
+| eval_natrec_neut :
+  `( {{ ⟦ MZ ⟧ p ↘ mz }} ->
+     {{ ⟦ A ⟧ p ↦ ⇑ ℕ m ↘ a }} ->
+     {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ ⇑ a (rec m under p return A | zero -> mz | succ -> MS end) }} )
+where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' p '↘' r" := (eval_natrec A MZ MS m p r) (in custom judg)
+with eval_app : domain -> domain -> domain -> Prop :=
+| eval_app_fn :
+  `( {{ ⟦ M ⟧ p ↦ n ↘ m }} ->
+     {{ $| λ p M & n |↘ m }} )
+| eval_app_neut :
+  `( {{ ⟦ B ⟧ p ↦ n ↘ b }} ->
+     {{ $| ⇑ (Π a p B) m & n |↘ ⇑ b (m (⇓ a n)) }} )
+where "'$|' m '&' n '|↘' r" := (eval_app m n r) (in custom judg)
+with eval_sub : sub -> env -> env -> Prop :=
+| eval_sub_id :
+  `( {{ ⟦ Id ⟧s p ↘ p }} )
+| eval_sub_weaken :
+  `( {{ ⟦ Wk ⟧s p ↘ p↯ }} )
+| eval_sub_extend :
+  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
+     {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ σ ,, M ⟧s p ↘ p' ↦ m }} )
+| eval_sub_compose :
+  `( {{ ⟦ τ ⟧s p ↘ p' }} ->
+     {{ ⟦ σ ⟧s p' ↘ p'' }} ->
+     {{ ⟦ σ ∘ τ ⟧s p ↘ p'' }} )
+where "'⟦' σ '⟧s' p '↘' p'" := (eval_sub σ p p') (in custom judg)
+.
+
+Scheme eval_exp_mut_ind := Induction for eval_exp Sort Prop
+with eval_natrec_mut_ind := Induction for eval_natrec Sort Prop
+with eval_app_mut_ind := Induction for eval_app Sort Prop
+with eval_sub_mut_ind := Induction for eval_sub Sort Prop.
diff --git a/theories/Core/Semantic/EvaluationLemmas.v b/theories/Core/Semantic/EvaluationLemmas.v
@@ -1,5 +1,6 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base Domain Evaluation LibTactics Syntax System.
+From Mcltt Require Import Base LibTactics EvaluationDefinitions.
+Import Domain_Notations.
 
 Section functional_eval.
   Let functional_eval_exp_prop M p m1 (_ : {{ ⟦ M ⟧ p ↘ m1 }}) : Prop := forall m2 (Heval2: {{ ⟦ M ⟧ p ↘ m2 }}), m1 = m2.