fixing

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.
   *)

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
 

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

core/Syntax.ml

@@ -70,16 +70,17 @@ 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 =
   | GTt | GFf
   | 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

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

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