Implement type checker (#164)

* Implement type checker

* Clean up type checker impl

* Remove get_subterms_of_pi_nf

theories/Extraction/NbE.v

@@ -65,7 +65,7 @@ Proof.
 Qed.
 
 #[local]
-  Hint Resolve initial_env_impl_complete' : mcltt.
+Hint Resolve initial_env_impl_complete' : mcltt.
 
 
 Lemma initial_env_impl_complete : forall G p,

theories/Extraction/PseudoMonadic.v

@@ -0,0 +1,49 @@
+From Coq Require Extraction.
+
+(* We cannot use class based generalization for
+   the following definitions as Coq does not support
+   polymorphism across [Prop] and [Set] *)
+
+Definition sumbool_failable_bind {A B} (ab : {A} + {B}) {C D : Prop} (fail : B -> D) (next : A -> {C} + {D}) :=
+  match ab with
+  | left a => next a
+  | right b => right (fail b)
+  end.
+Transparent sumbool_failable_bind.
+Arguments sumbool_failable_bind /.
+
+Notation "'let*b' a ':=' ab 'while' fail 'in' next" := (sumbool_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+Notation "'pureb' a" := (left a) (at level 0, only parsing).
+
+Definition sumor_failable_bind {A B} (ab : A + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> C + {D}) :=
+  match ab with
+  | inleft a => next a
+  | inright b => inright (fail b)
+  end.
+Transparent sumor_failable_bind.
+Arguments sumor_failable_bind /.
+
+Notation "'let*o' a ':=' ab 'while' fail 'in' next" := (sumor_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+Notation "'pureo' a" := (inleft a) (at level 0, only parsing).
+
+Definition sumbool_sumor_failable_bind {A B} (ab : {A} + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> C + {D}) :=
+  match ab with
+  | left a => next a
+  | right b => inright (fail b)
+  end.
+Transparent sumbool_sumor_failable_bind.
+Arguments sumbool_sumor_failable_bind /.
+
+Notation "'let*b->o' a ':=' ab 'while' fail 'in' next" := (sumbool_sumor_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+
+Definition sumor_sumbool_failable_bind {A B} (ab : A + {B}) {C} {D : Prop} (fail : B -> D) (next : A -> {C} + {D}) :=
+  match ab with
+  | inleft a => next a
+  | inright b => right (fail b)
+  end.
+Transparent sumor_sumbool_failable_bind.
+Arguments sumor_sumbool_failable_bind /.
+
+Notation "'let*o->b' a ':=' ab 'while' fail 'in' next" := (sumor_sumbool_failable_bind ab fail (fun a => next)) (at level 0, a pattern, next at level 10, right associativity, only parsing).
+
+Extraction Inline sumbool_failable_bind sumor_failable_bind sumbool_sumor_failable_bind sumor_sumbool_failable_bind.

theories/Extraction/Subtyping.v

@@ -1,13 +1,13 @@
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Algorithmic Require Import Subtyping.Definitions.
 From Mcltt.Core Require Import NbE.
-From Mcltt.Extraction Require Import Evaluation NbE.
+From Mcltt.Extraction Require Import Evaluation NbE PseudoMonadic.
 From Equations Require Import Equations.
 Import Domain_Notations.
 
-
 #[local]
-  Ltac subtyping_tac :=
+Ltac subtyping_tac :=
+  intros;
   lazymatch goal with
   | |- {{ ⊢anf ~_ ⊆ ~_ }} =>
       subst;
@@ -23,38 +23,33 @@ Import Domain_Notations.
 
 #[tactic="subtyping_tac"]
 Equations subtyping_nf_impl A B : { {{ ⊢anf A ⊆ B }} } + {~ {{ ⊢anf A ⊆ B }} } :=
-| n{{{ Type@i }}}, n{{{ Type@j }}} with Compare_dec.le_lt_dec i j => {
-  | left _ => left _;
-  | right _ => right _
-  }
-| n{{{ Π A B }}}, n{{{ Π A' B' }}} with nf_eq_dec A A' => {
-  | left _ with subtyping_nf_impl B B' => {
-    | left _ => left _
-    | right _ => right _
-    }
-  | right _ => right _
-  }
+| n{{{ Type@i }}}, n{{{ Type@j }}} =>
+    let*b _ := Compare_dec.le_lt_dec i j while _ in
+    pureb _
+| n{{{ Π A B }}}, n{{{ Π A' B' }}} =>
+    let*b _ := nf_eq_dec A A' while _ in
+    let*b _ := subtyping_nf_impl B B' while _ in
+    pureb _
+(* Pseudo-monadic syntax for the next catch-all branch
+   generates some unsolved obligations *)
 | A, B with nf_eq_dec A B => {
   | left _ => left _
   | right _ => right _
   }.
-
 Theorem subtyping_nf_impl_complete : forall A B,
     {{ ⊢anf A ⊆ B }} ->
     exists H, subtyping_nf_impl A B = left H.
 Proof.
   intros; dec_complete.
 Qed.
 
-
 Inductive subtyping_order G A B :=
 | subtyping_order_run :
   nbe_ty_order G A ->
   nbe_ty_order G B ->
   subtyping_order G A B.
 #[local]
-  Hint Constructors subtyping_order : mcltt.
-
+Hint Constructors subtyping_order : mcltt.
 
 Lemma subtyping_order_sound : forall G A B,
     {{ G ⊢a A ⊆ B }} ->
@@ -66,34 +61,30 @@ Proof.
 Qed.
 
 #[local]
-  Ltac subtyping_impl_tac1 :=
+Ltac subtyping_impl_tac1 :=
   match goal with
   | H : subtyping_order _ _ _ |- _ => progressive_invert H
   | H : nbe_ty_order _ _ |- _ => progressive_invert H
   end.
 
 #[local]
-  Ltac subtyping_impl_tac :=
+Ltac subtyping_impl_tac :=
   repeat subtyping_impl_tac1; try econstructor; mauto.
 
-
 #[tactic="subtyping_impl_tac"]
 Equations subtyping_impl G A B (H : subtyping_order G A B) :
   { {{G ⊢a A ⊆ B}} } + { ~ {{ G ⊢a A ⊆ B }} } :=
 | G, A, B, H =>
     let (a, Ha) := nbe_ty_impl G A _ in
     let (b, Hb) := nbe_ty_impl G B _ in
-    match subtyping_nf_impl a b with
-    | left _ => left _
-    | right _ => right _
-    end.
+    let*b _ := subtyping_nf_impl a b while _ in
+    pureb _.
 Next Obligation.
   progressive_inversion.
   functional_nbe_rewrite_clear.
   contradiction.
 Qed.
 
-
 Theorem subtyping_impl_complete' : forall G A B,
     {{G ⊢a A ⊆ B}} ->
     forall (H : subtyping_order G A B),
@@ -103,7 +94,7 @@ Proof.
 Qed.
 
 #[local]
- Hint Resolve subtyping_order_sound subtyping_impl_complete' : mcltt.
+Hint Resolve subtyping_order_sound subtyping_impl_complete' : mcltt.
 
 Theorem subtyping_impl_complete : forall G A B,
     {{G ⊢a A ⊆ B}} ->