update to new dependent lcf (#181)

* update to new (still broken) dependent lcf

* fix

* fix bug in goal printer

* update dependent lcf

* update libs

* strange temporary fix (why does this work?)

* print out generic judgments

* cleanup

* actually, just print out the parametric judgments

src/redprl/judgment.fun

@@ -1,21 +1,25 @@
 functor SequentJudgment
   (structure S : SEQUENT where type 'a CJ.Tm.O.Ar.Vl.Sp.t = 'a list
-   structure TermPrinter : SHOW where type t = S.CJ.Tm.abt) : LCF_JUDGMENT =
+   structure TermPrinter : SHOW where type t = S.CJ.Tm.abt) : LCF_BINDING_JUDGMENT =
 struct
   structure CJ = S.CJ
   structure Tm = CJ.Tm
   type sort = Tm.valence
   type env = Tm.metaenv
   type jdg = Tm.abt S.jdg
+  type symenv = Tm.symenv
+  type varenv = Tm.varenv
 
   val subst = S.map o Tm.substMetaenv
   val eq = S.eq
   val toString = S.toString TermPrinter.toString
 
+  val substSymenv = S.map o Tm.substSymenv
+  val substVarenv = S.map o Tm.substVarenv
 
   local
     open S
-    infix >> |>
+    infix >>
   in
     val rec sort =
       fn H >> catjdg => (([],[]), CJ.synthesis catjdg)
@@ -25,12 +29,6 @@ struct
            in
              List.nth (vls, k)
            end
-       | (U, G) |> jdg =>
-           let
-             val ((sigmas, taus), tau) = sort jdg
-           in
-             ((List.map #2 U @ sigmas, List.map #2 G @ taus), tau)
-           end
   end
 end
 

src/redprl/lcf_model.fun

@@ -19,16 +19,16 @@ struct
   fun interpret (sign, env) rule =
     case out rule of
        O.MONO O.RULE_ID $ _ => (fn _ => Lcf.idn)
-     | O.MONO O.RULE_EVAL_GOAL $ _ => Rules.Lift (Rules.CEquiv.EvalGoal sign)
-     | O.MONO O.RULE_CEQUIV_REFL $ _ => Rules.Lift (Rules.CEquiv.Refl)
-     | O.MONO O.RULE_AUTO_STEP $ _ => Rules.Lift (Rules.AutoStep sign)
-     | O.POLY (O.RULE_HYP z) $ _ => Rules.Lift (Rules.Hyp.Project z)
-     | O.POLY (O.RULE_ELIM z) $ _ => Rules.Lift (Rules.Elim sign z)
-     | O.MONO O.RULE_WITNESS $ [_ \ tm] => Rules.Lift (Rules.Truth.Witness tm)
-     | O.MONO O.RULE_HEAD_EXP $ _ => Rules.Lift (Rules.Computation.EqHeadExpansion sign)
-     | O.MONO O.RULE_SYMMETRY $ _ => Rules.Lift Rules.Equality.Symmetry
-     | O.MONO O.RULE_CUT $ [_ \ catjdg] => Rules.Lift (Rules.Cut (RedPrlCategoricalJudgment.fromAbt catjdg))
-     | O.MONO (O.RULE_LEMMA _) $ [_ \ thm] => Rules.Lift (Rules.Lemma thm)
+     | O.MONO O.RULE_EVAL_GOAL $ _ => Rules.CEquiv.EvalGoal sign
+     | O.MONO O.RULE_CEQUIV_REFL $ _ => Rules.CEquiv.Refl
+     | O.MONO O.RULE_AUTO_STEP $ _ => Rules.AutoStep sign
+     | O.POLY (O.RULE_HYP z) $ _ => Rules.Hyp.Project z
+     | O.POLY (O.RULE_ELIM z) $ _ => Rules.Elim sign z
+     | O.MONO O.RULE_WITNESS $ [_ \ tm] => Rules.Truth.Witness tm
+     | O.MONO O.RULE_HEAD_EXP $ _ => Rules.Computation.EqHeadExpansion sign
+     | O.MONO O.RULE_SYMMETRY $ _ => Rules.Equality.Symmetry
+     | O.MONO O.RULE_CUT $ [_ \ catjdg] => Rules.Cut (RedPrlCategoricalJudgment.fromAbt catjdg)
+     | O.MONO (O.RULE_LEMMA _) $ [_ \ thm] => Rules.Lemma thm
      | _ => raise E.error [E.% "Invalid rule", E.! rule]
 
   fun rule (sign, env) rule alpha goal =

src/redprl/machine.sml

@@ -115,10 +115,7 @@ struct
       O.MONO O.MTAC_PROGRESS $$ [([],[]) \ mt]
 
     fun multirepeat mt =
-      let
-      in
         O.MONO O.MTAC_REPEAT $$ [([],[]) \ mt]
-      end
 
     fun cut jdg =
       O.MONO O.RULE_CUT $$ [([],[]) \ jdg]

src/redprl/refiner.sig

@@ -6,7 +6,6 @@ sig
   type rule
   type hyp
 
-  val Lift : rule -> rule
   val Lemma : abt -> 'n -> Lcf.jdg Lcf.tactic
   val Cut : catjdg -> rule
   val Elim : sign -> hyp -> rule

src/redprl/refiner_kit.fun

@@ -1,36 +1,64 @@
 structure LcfLanguage = LcfAbtLanguage (RedPrlAbt)
 
+signature LCF_GENERIC_UTIL = 
+sig
+  structure Abt : ABT
+  datatype 'a generic = || of ((Abt.symbol * Abt.psort) list * (Abt.variable * Abt.sort) list) * 'a
+  include LCF_UTIL where type 'a Eff.t = 'a generic
+end
+
 structure Lcf :
 sig
-  include LCF_UTIL
+  include LCF_GENERIC_UTIL
   val prettyState : jdg state -> PP.doc
   val stateToString : jdg state -> string
 end =
 struct
-  structure Def = LcfUtil (structure Lcf = Lcf (LcfLanguage) and J = RedPrlJudgment)
-  open Def
-  infix |>
-
-  fun prettyGoal (x, jdg) =
-    PP.concat
-      [PP.text "Goal ",
-       PP.text (RedPrlAbt.Metavar.toString x),
-       PP.text ".",
-       PP.nest 2 (PP.concat [PP.line, RedPrlSequent.pretty TermPrinter.toString jdg]),
-       PP.line]
-
-  val prettyGoals : jdg Tl.telescope -> {doc : PP.doc, env : J.env, idx : int} =
+  structure LcfGeneric = LcfGeneric (LcfLanguage)
+  structure Def = LcfGenericUtil (structure Lcf = LcfGeneric and J = RedPrlJudgment)
+  open Def LcfGeneric
+  infix |> ||
+
+
+  val prettySyms =
+    PP.text o ListSpine.pretty (fn (u, sigma) => Sym.toString u ^ " : " ^ Abt.O.Ar.Vl.PS.toString sigma) ", "
+
+  val prettyVars = 
+    PP.text o ListSpine.pretty (fn (x, tau) => Var.toString x ^ " : " ^ Abt.O.Ar.Vl.S.toString tau) ", "
+
+  fun prettyGoal (syms, vars) (x, jdg) =
+    let
+      val parametric = 
+        if List.length syms > 0 then
+          PP.concat [PP.line, PP.text "nabla {", prettySyms syms, PP.text "}. "]
+        else
+          PP.empty
+    in
+      PP.concat
+        [PP.text "Goal ",
+         PP.text (RedPrlAbt.Metavar.toString x),
+         PP.text ".",
+         parametric,
+         PP.nest 2 (PP.concat [PP.line, RedPrlSequent.pretty TermPrinter.toString jdg]),
+         PP.line]
+    end
+
+
+  val prettyGoals : jdg eff Tl.telescope -> {doc : PP.doc, env : J.env, idx : int} =
     let
       open RedPrlAbt
     in
       Tl.foldl
-        (fn (x, jdg, {doc, env, idx}) =>
+        (fn (x, (syms, vars) || jdg, {doc, env, idx}) =>
           let
             val x' = Metavar.named (Int.toString idx)
             val jdg' = J.subst env jdg
-            val env' = Metavar.Ctx.insert env x (LcfLanguage.var x' (J.sort jdg'))
+            val ((ssorts, vsorts), tau) = J.sort jdg'
+            val vl' = ((ssorts @ List.map #2 syms, vsorts @ List.map #2 vars), tau)
+            val env' = Metavar.Ctx.insert env x (LcfLanguage.var x' vl')
+
           in
-            {doc = PP.concat [doc, prettyGoal (x', jdg'), PP.line],
+            {doc = PP.concat [doc, prettyGoal (syms, vars) (x', jdg'), PP.line],
              env = env',
              idx = idx + 1}
           end)
@@ -97,14 +125,14 @@ struct
       end
   end
 
-  fun makeGoal jdg =
+  fun makeGoal (Lcf.|| (bs, jdg)) =
     let
       open Abt infix 1 $#
       val x = newMeta ""
       val vl as (_, tau) = J.sort jdg
-      fun hole ps ms = check (x $# (ps, ms), tau)
+      fun hole ps ms = check (x $# (ps, ms), tau) handle _ => raise Fail "makeGoal"
     in
-      ((x, jdg), hole)
+      ((x, Lcf.|| (bs, jdg)), hole)
     end
 
 

src/redprl/sequent.sig

@@ -15,7 +15,6 @@ sig
 
   datatype 'a jdg =
      >> of 'a CJ.jdg ctx * 'a CJ.jdg                            (* sequents / formal hypothetical judgment *)
-   | |> of ((sym * psort) list * (var * sort) list) * 'a jdg    (* generic+parametric judgment *)
    | MATCH of operator * int * 'a                               (* unify a term w/ a head operator and extract the kth subterm *)
 
   val map : ('a -> 'b) -> 'a jdg -> 'b jdg

src/redprl/sequent.sml

@@ -15,14 +15,12 @@ struct
 
   datatype 'a jdg =
      >> of 'a CJ.jdg ctx * 'a CJ.jdg
-   | |> of ((sym * psort) list * (var * sort) list) * 'a jdg
    | MATCH of operator * int * 'a
 
-  infix >> |>
+  infix >>
 
   fun map f =
     fn H >> catjdg => Hyps.map (CJ.map f) H >> CJ.map f catjdg
-     | (U,G) |> jdg => (U,G) |> map f jdg
      | MATCH (th, k, a) => MATCH (th, k, f a)
 
   local
@@ -43,10 +41,6 @@ struct
     fn (H1 >> catjdg1, H2 >> catjdg2) =>
           telescopeEq (H1, H2)
             andalso CJ.eq (catjdg1, catjdg2)
-     | ((U1,G1) |> jdg1, (U2,G2) |> jdg2) =>
-          ListPair.allEq (fn ((u1, sort1), (u2, sort2)) => CJ.Tm.Sym.eq (u1, u2) andalso CJ.Tm.O.Ar.Vl.PS.eq (sort1, sort2)) (U1, U2)
-            andalso ListPair.allEq (fn ((x1, sort1), (x2, sort2)) => CJ.Tm.Var.eq (x1, x2) andalso CJ.Tm.O.Ar.Vl.S.eq (sort1, sort2)) (G1, G2)
-            andalso eq (jdg1, jdg2)
      | (MATCH (th1, k1, a1), MATCH (th2, k2, a2)) =>
           CJ.Tm.O.eq CJ.Tm.Sym.eq (th1, th2)
             andalso k1 = k2
@@ -64,7 +58,6 @@ struct
     fun pretty f : 'a jdg -> doc =
       fn H >> catjdg => concat [prettyHyps (CJ.pretty f) H, text "\226\138\162 ", CJ.pretty f catjdg]
        | MATCH (th, k, a) => concat [text (f a), text " match ", text (Tm.O.toString Tm.Sym.toString th), text " @ ", int k]
-       | (U, G) |> jdg => pretty f jdg
   end
 
   fun toString f = PP.toString 80 true o pretty f

test/success/bool-hcom.prl

@@ -8,7 +8,8 @@ Thm BasicHcom : [
   { lam a. lam b. lam c. lam d.
     lam pab. lam pac. lam pbd.
     <i> 'hcom{i; 0 ~> 1}(bool; ,pab @ i; {j}. ,pac @ j; {j}. ,pbd @ j)
-  }; auto
+  };
+  <|auto|>;
 ].
 
 Thm Cap{i : dim} : [ hcom{i; 0 ~> 0}(bool; tt; {_}. tt; {_}. tt) = tt : bool ] by [