From 4a0215119f008a31d2e1f5623a3e0a4667228fee Mon Sep 17 00:00:00 2001
From: Jonathan Sterling <jon@jonmsterling.com>
Date: Mon, 5 Apr 2021 09:39:00 -0400
Subject: [PATCH] fixing

---
 core/Core.mli          |  6 ++++++
 core/Eval.ml           |  3 +++
 core/Refiner.ml        | 27 ++++++++++++++++++++++++++-
 core/Syntax.ml         |  5 +++--
 frontend/Distiller.ml  |  3 +++
 frontend/Elaborator.ml | 18 ++++++++++++------
 6 files changed, 53 insertions(+), 9 deletions(-)

diff --git a/core/Core.mli b/core/Core.mli
index d7864ea..aa247e1 100644
--- a/core/Core.mli
+++ b/core/Core.mli
@@ -113,6 +113,12 @@ module Refiner : sig
 
   val with_tp : (tp -> chk_rule) -> chk_rule
 
+
+  (** {2 Built-in tacticals} *)
+
+  val intro_implicit_connectives : chk_rule -> chk_rule
+  val elim_implicit_connectives : syn_rule -> syn_rule
+
   (** {2 Failing rules}
       The following rules will fail with an exception.
   *)
diff --git a/core/Eval.ml b/core/Eval.ml
index 50c149b..e5e87ef 100644
--- a/core/Eval.ml
+++ b/core/Eval.ml
@@ -57,6 +57,9 @@ struct
       | LExtOut ltm ->
         let* gtm = eval ltm in
         L.global @@ gext_out gtm
+      | LExtIn (gtp, part, ltm) ->
+        let+ gtm = eval ltm in
+        GExtIn (gtp, part, gtm)
       | LAbort ->
         L.ret GAbort
 
diff --git a/core/Refiner.ml b/core/Refiner.ml
index ad19a6c..01f95ef 100644
--- a/core/Refiner.ml
+++ b/core/Refiner.ml
@@ -137,7 +137,15 @@ let ext_in (chk_rule : chk_rule) : chk_rule =
       let* gtm' = Eval.eval part.part in
       Equate.equate_gtm gtp gtm gtm'
     in
-    failwith ""
+    L.ret @@ LExtIn (gtp, Prt part, ltm)
+  | _ ->
+    L.throw TypeError
+
+let ext_out (syn_rule : syn_rule) : syn_rule =
+  let* gtm = syn_rule in
+  match tp_of_gtm gtm with
+  | GExtTp _ ->
+    L.global @@ Eval.gext_out gtm
   | _ ->
     L.throw TypeError
 
@@ -225,3 +233,20 @@ let conv : syn_rule -> chk_rule =
 let fail_tp exn = L.throw exn
 let fail_chk exn _ = L.throw exn
 let fail_syn exn = L.throw exn
+
+
+let elim_implicit_connectives : syn_rule -> syn_rule =
+  fun syn ->
+  let* tm = syn in
+  match tp_head @@ tp_of_gtm tm with
+  | `Ext ->
+    ext_out @@ L.ret tm
+  | _ ->
+    L.ret tm
+
+let intro_implicit_connectives : chk_rule -> chk_rule =
+  fun chk ->
+  with_tp @@ fun tp ->
+  match tp_head tp with
+  | `Ext -> ext_in chk
+  |_ -> chk
diff --git a/core/Syntax.ml b/core/Syntax.ml
index 2162083..886b9cb 100644
--- a/core/Syntax.ml
+++ b/core/Syntax.ml
@@ -70,6 +70,8 @@ and ltm =
   | LRcd of string list * gtele * ltm StringMap.t
   | LProj of string * ltm
   | LExtOut of ltm
+  | LExtIn of gtp * ltm part * ltm
+
   | LAbort
 
 and gtm =
@@ -77,9 +79,8 @@ and gtm =
   | GLam of gfam * ltm * env
   | GRcd of string list * gtele * gtm StringMap.t
   | Glued of (gneu, ltm) glued
-  | GAbort
-
   | GExtIn of gtp * ltm part * gtm
+  | GAbort
 
 and gneu =
   | GVar of Env.lvl
diff --git a/frontend/Distiller.ml b/frontend/Distiller.ml
index c9ab05b..eccad05 100644
--- a/frontend/Distiller.ml
+++ b/frontend/Distiller.ml
@@ -52,3 +52,6 @@ let rec distill_ltm : Syntax.ltm -> code m =
 
   | LExtOut ltm ->
     distill_ltm ltm
+
+  | LExtIn (_, _, ltm) ->
+    distill_ltm ltm
diff --git a/frontend/Elaborator.ml b/frontend/Elaborator.ml
index 2d24f1a..8eb8f90 100644
--- a/frontend/Elaborator.ml
+++ b/frontend/Elaborator.ml
@@ -21,14 +21,22 @@ let add_var x var =
   locally @@ StringMap.add x var
 
 let rec elab_chk_code : code -> R.chk_rule m =
-  function
+  fun code ->
+  M.reader @@ fun res ->
+  R.intro_implicit_connectives @@
+  M.run res @@
+  match code with
   | R rcode ->
     elab_chk_rcode rcode
   | L lcode ->
     elab_chk_lcode lcode
 
 and elab_syn_code : code -> R.syn_rule m =
-  function
+  fun code ->
+  M.reader @@ fun res ->
+  R.elim_implicit_connectives @@
+  M.run res @@
+  match code with
   | L lcode ->
     elab_syn_lcode lcode
   | R _ ->
@@ -71,12 +79,10 @@ and elab_chk_lcode (lcode : lcode) : R.chk_rule m =
     in
     let+ chk_map = loop StringMap.empty lbls in
     R.rcd chk_map
-  | `Ext ->
-    (* TODO: will this cause a loop? *)
-    reader @@ fun res ->
-    R.ext_in @@ run res @@ elab_chk_lcode lcode
   | `Abort ->
     ret @@ R.chk_abort
+  | `Ext ->
+    ret @@ R.fail_chk ElabError
 
 and elab_syn_lcode : lcode -> R.syn_rule m =
   function