abstracting the types of rules

core/Core.ml

@@ -18,4 +18,5 @@ type tm = gtm Proof.t
 
 let tp_of_tm = tp_of_gtm
 
+module Rule = Rule
 module Refiner = Refiner

core/Core.mli

@@ -40,6 +40,8 @@ val tp_head : tp -> tp_head
 
 (** {1 Constructing well-typed terms} *)
 
+module Rule = Rule
+
 (** The refiner is the only way to construct terms. Any term constructed by the refiner is
     guaranteed to be well-typed, in the tradition of LCF. *)
 module Refiner : sig
@@ -56,10 +58,7 @@ module Refiner : sig
       the context.
   *)
 
-  type tp_rule
-  type chk_rule
-  type syn_rule
-  type tele_rule
+  open Rule
 
   (** {1 Inference rules} *)
 

core/Refiner.ml

@@ -1,17 +1,15 @@
 open Basis
 open Syntax
 open Effect
+open Rule
 
 exception TypeError
 
 open Monad.Notation (L)
 
-type tp_rule = ltp L.m
-type chk_rule = gtp -> ltm L.m
-type syn_rule = gtm L.m
-
-let with_tp kont tp =
-  kont tp tp
+let with_tp kont =
+  ChkRule.rule @@ fun tp ->
+  ChkRule.run (kont tp) tp
 
 let inst_tp_fam : ltp -> env -> gtm -> gtp G.m =
   fun lfam env gtm ->
@@ -24,28 +22,28 @@ let inst_tm_fam : ltm -> env -> gtm -> gtm G.m =
   G.local envx @@ Eval.eval lfam
 
 
-let core =
-  L.ret
+let core x =
+  SynRule.rule @@ L.ret x
 
 let bool : tp_rule =
+  TpRule.rule @@
   L.ret LBool
 
 let tt : chk_rule =
+  ChkRule.rule @@
   function
   | GBool -> L.ret LTt
   | _ -> L.throw TypeError
 
 let ff : chk_rule =
+  ChkRule.rule @@
   function
   | GBool -> L.ret LFf
   | _ -> L.throw TypeError
 
 
-(* invariant: does not return unless the list of labels has no shadowing *)
-type tele_rule = (string list * ltele) L.m
-
 let tl_nil : tele_rule =
-  L.ret ([], LTlNil)
+  TeleRule.rule @@ L.ret ([], LTlNil)
 
 let rec freshen lbl lbls =
   if List.mem lbl lbls then
@@ -54,36 +52,41 @@ let rec freshen lbl lbls =
     lbl
 
 let tl_cons lbl tp_rule tele_rule =
-  let* lbase = tp_rule in
+  TeleRule.rule @@
+  let* lbase = TpRule.run tp_rule in
   let* gbase = Eval.eval_tp lbase in
   L.bind_tm gbase @@ fun var ->
-  let+ lbls, lfam = tele_rule var in
+  let+ lbls, lfam = TeleRule.run @@ tele_rule var in
   let lbl' = freshen lbl lbls in
   lbl' :: lbls, LTlCons (lbase, lfam)
 
 let pi (base : tp_rule) (fam : gtm -> tp_rule) : tp_rule =
-  let* lbase = base in
+  TpRule.rule @@
+  let* lbase = TpRule.run base in
   let* gbase = Eval.eval_tp lbase in
   L.bind_tm gbase @@ fun var ->
-  let+ lfam = fam var in
+  let+ lfam = TpRule.run @@ fam var in
   LPi (lbase, lfam)
 
 
 let rcd_tp (tele : tele_rule) : tp_rule =
-  let+ lbls, ltl = tele in
+  TpRule.rule @@
+  let+ lbls, ltl = TeleRule.run tele in
   LRcdTp (lbls, ltl)
 
 
 let lam (bdy : gtm -> chk_rule) : chk_rule =
+  ChkRule.rule @@
   function
   | GPi ((gbase, lfam, env) as gfam) ->
     L.bind_tm gbase @@ fun var ->
-    let+ lbdy = bdy var @<< L.global @@ inst_tp_fam lfam env var in
+    let+ lbdy = ChkRule.run (bdy var) @<< L.global @@ inst_tp_fam lfam env var in
     LLam (gfam, lbdy)
   | _ ->
     L.throw TypeError
 
 let rcd (chk_map : chk_rule StringMap.t) : chk_rule =
+  ChkRule.rule @@
   function
   | GRcdTp (lbls, gtl) ->
     let rec loop tmap lbls gtl =
@@ -93,7 +96,7 @@ let rcd (chk_map : chk_rule StringMap.t) : chk_rule =
         begin
           match StringMap.find_opt lbl chk_map with
           | Some chk_rule ->
-            let* ltm = chk_rule gtp in
+            let* ltm = ChkRule.run chk_rule gtp in
             let* gtm = Eval.eval ltm in
             let* gtl' = L.global @@ G.local tlenv @@ L.append_tm gtm @@ Eval.eval_tele ltl in
             let tmap' = StringMap.add lbl ltm tmap in
@@ -110,27 +113,30 @@ let rcd (chk_map : chk_rule StringMap.t) : chk_rule =
     L.throw TypeError
 
 let app (fn : syn_rule) (arg : chk_rule) : syn_rule =
-  let* gtm0 = fn in
+  SynRule.rule @@
+  let* gtm0 = SynRule.run fn in
   match tp_of_gtm gtm0 with
   | GPi (gbase, _, _) ->
-    let* larg = arg gbase in
+    let* larg = ChkRule.run arg gbase in
     let* gtm1 = Eval.eval larg in
     L.global @@ Eval.gapp gtm0 gtm1
   | _ ->
     L.throw TypeError
 
 let proj lbl (syn_rule : syn_rule) : syn_rule =
-  let* gtm = syn_rule in
+  SynRule.rule @@
+  let* gtm = SynRule.run syn_rule in
   match tp_of_gtm gtm with
   | GRcdTp (lbls, _) when List.mem lbl lbls ->
     L.global @@ Eval.gproj lbl gtm
   | _ ->
     L.throw TypeError
 
 let ext_in (chk_rule : chk_rule) : chk_rule =
+  ChkRule.rule @@
   function
   | GExtTp (gtp, Prt part) ->
-    let* ltm = chk_rule gtp in
+    let* ltm = ChkRule.run chk_rule gtp in
     let* () =
       L.scope_thy (`Ext part.supp) @@
       let* gtm = Eval.eval ltm in
@@ -142,7 +148,8 @@ let ext_in (chk_rule : chk_rule) : chk_rule =
     L.throw TypeError
 
 let ext_out (syn_rule : syn_rule) : syn_rule =
-  let* gtm = syn_rule in
+  SynRule.rule @@
+  let* gtm = SynRule.run syn_rule in
   match tp_of_gtm gtm with
   | GExtTp _ ->
     L.global @@ Eval.gext_out gtm
@@ -168,6 +175,7 @@ let pair (chk_rule0 : chk_rule) (chk_rule1 : chk_rule) : chk_rule =
   |> rcd
 
 let chk_abort : chk_rule =
+  ChkRule.rule @@
   fun _ ->
   let* thy = L.theory in
   match Logic.consistency thy with
@@ -180,9 +188,10 @@ let rec conv_ : gtm -> chk_rule =
   | GTt -> tt
   | GFf -> ff
   | GLam (_, ltm, env) ->
-    lam @@ fun var gfib ->
+    lam @@ fun var ->
+    ChkRule.rule @@ fun gfib ->
     let* gtm = L.global @@ inst_tm_fam ltm env var in
-    conv_ gtm gfib
+    ChkRule.run (conv_ gtm) gfib
   | GExtIn (_, _, gtm) ->
     ext_in (conv_ gtm)
   | GRcd (_, _, gmap) ->
@@ -194,12 +203,13 @@ let rec conv_ : gtm -> chk_rule =
 
 
 and conv_glued_ : (gneu, ltm) glued -> chk_rule =
-  fun (Gl glued) gtp ->
+  fun (Gl glued) ->
+  ChkRule.rule @@ fun gtp ->
   let* gtm = L.global @@ G.local glued.env @@ Eval.eval glued.part in
   let* () = Equate.equate_gtp gtp glued.gtp in
   let* thy = L.theory in
   if Logic.test thy [] glued.supp then
-    conv_ gtm gtp
+    ChkRule.run (conv_ gtm) gtp
   else
     conv_neu_ glued.base
 
@@ -218,29 +228,31 @@ and conv_neu_ : gneu -> ltm L.m =
     | GApp arg ->
       let* ltm = conv_neu_ gneu in
       let tp_arg = tp_of_gtm arg in
-      let+ larg = conv_ arg tp_arg in
+      let+ larg = ChkRule.run (conv_ arg) tp_arg in
       LApp (ltm, larg)
     | GExtOut ->
       let+ ltm = conv_neu_ gneu in
       LExtOut ltm
 
 let conv : syn_rule -> chk_rule =
-  fun syn gtp ->
-  let* gtm = syn in
-  conv_ gtm gtp
+  fun syn ->
+  ChkRule.rule @@ fun gtp ->
+  let* gtm = SynRule.run syn in
+  ChkRule.run (conv_ gtm) gtp
 
 
-let fail_tp exn = L.throw exn
-let fail_chk exn _ = L.throw exn
-let fail_syn exn = L.throw exn
+let fail_tp exn = TpRule.rule @@ L.throw exn
+let fail_chk exn = ChkRule.rule @@ fun _ -> L.throw exn
+let fail_syn exn = SynRule.rule @@ L.throw exn
 
 
 let elim_implicit_connectives : syn_rule -> syn_rule =
   fun syn ->
-  let* tm = syn in
+  SynRule.rule @@
+  let* tm = SynRule.run syn in
   match tp_head @@ tp_of_gtm tm with
   | `Ext ->
-    ext_out @@ L.ret tm
+    SynRule.run @@ ext_out @@ SynRule.rule @@ L.ret tm
   | _ ->
     L.ret tm
 

core/Rule.ml

@@ -0,0 +1,36 @@
+open Syntax
+open Effect
+
+type tp_rule = ltp L.m
+type chk_rule = gtp -> ltm L.m
+type syn_rule = gtm L.m
+
+type tele_rule = (string list * ltele) L.m
+
+module TpRule =
+struct
+  type t = tp_rule
+  let rule x = x
+  let run x = x
+end
+
+module ChkRule =
+struct
+  type t = chk_rule
+  let rule x = x
+  let run x = x
+end
+
+module SynRule =
+struct
+  type t = syn_rule
+  let rule x = x
+  let run x = x
+end
+
+module TeleRule =
+struct
+  type t = tele_rule
+  let rule x = x
+  let run x = x
+end

core/Rule.mli

@@ -0,0 +1,32 @@
+open Syntax
+open Effect
+
+type tp_rule
+type chk_rule
+type syn_rule
+type tele_rule
+
+module TpRule : sig
+  type t = tp_rule
+  val rule : ltp L.m -> t
+  val run : t -> ltp L.m
+end
+
+module ChkRule : sig
+  type t = chk_rule
+  val rule : (gtp -> ltm L.m) -> t
+  val run : t -> (gtp -> ltm L.m)
+end
+
+module SynRule : sig
+  type t = syn_rule
+  val rule : gtm L.m -> t
+  val run : t -> gtm L.m
+end
+
+(** Invariant: does not return unless the list of labels has no shadowing *)
+module TeleRule : sig
+  type t = tele_rule
+  val rule : (string list * ltele) L.m -> t
+  val run : t -> (string list * ltele) L.m
+end

core/dune

@@ -2,6 +2,6 @@
  (name Core)
  (libraries dreamtt.basis)
  (flags
-  (:standard -w -32-26-27-37))
+  (:standard -w -32-34-26-27-37))
  (public_name dreamtt.core))