add parsing of hComp

diff --git a/CTT.hs b/CTT.hs
index 21f8e9f705bc8bf2b0592ae65ceb7b6e98411d4f..7cfa412caccb58837f193aca6cb2aea2d84281ac 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -116,7 +116,8 @@ data Ter = Pi Ter
            -- Kan composition and filling
          | Comp Ter Ter (System Ter)
          | Fill Ter Ter (System Ter)
-           -- Glue
+         | HComp Ter Ter (System Ter)
+         -- Glue
          | Glue Ter (System Ter)
          | GlueElem Ter (System Ter)
          | UnGlueElem Ter (System Ter)
@@ -381,6 +382,7 @@ showTer v = case v of
   PLam i e           -> char '<' <> text (show i) <> char '>' <+> showTer e
   AppFormula e phi   -> showTer1 e <+> char '@' <+> showFormula phi
   Comp e t ts        -> text "comp" <+> showTers [e,t] <+> text (showSystem ts)
+  HComp e t ts       -> text "hComp" <+> showTers [e,t] <+> text (showSystem ts) 
   Fill e t ts        -> text "fill" <+> showTers [e,t] <+> text (showSystem ts)
   Glue a ts          -> text "Glue" <+> showTer1 a <+> text (showSystem ts)
   GlueElem a ts      -> text "glue" <+> showTer1 a <+> text (showSystem ts)

diff --git a/Eval.hs b/Eval.hs
index 3581a974aca95a6cf19f1009fbcc83810aab258b..d6e364762177b9e1efbca5a2ad82f894065b4de4 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -189,6 +189,8 @@ eval rho@(Env (_,_,_,Nameless os)) v = case v of
   AppFormula e phi    -> eval rho e @@ evalFormula rho phi
   Comp a t0 ts        ->
     compLine (eval rho a) (eval rho t0) (evalSystem rho ts)
+  HComp a t0 ts       ->
+    hComp (eval rho a) (eval rho t0) (evalSystem rho ts)
   Fill a t0 ts        ->
     fillLine (eval rho a) (eval rho t0) (evalSystem rho ts)
   Glue a ts           -> glue (eval rho a) (evalSystem rho ts)

diff --git a/Exp.cf b/Exp.cf
index f93cc81c26f531b7ac829a84ff5ab27416368e6e..3f016e3576017172bd0a52bc45ef86ecbcb477cd 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -37,6 +37,7 @@ AppFormula.   Exp2 ::= Exp2 "@" Formula ;
 App.          Exp2 ::= Exp2 Exp3 ;
 PathP.        Exp3 ::= "PathP" Exp4 Exp4 Exp4 ;
 Comp.         Exp3 ::= "comp" Exp4 Exp4 System ;
+HComp.        Exp3 ::= "hComp" Exp4 Exp4 System ;
 Trans.        Exp3 ::= "transport" Exp4 Exp4 ;
 Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "Glue" Exp4 System ;

diff --git a/Resolver.hs b/Resolver.hs
index c61f65d3957b989b32b10a6ca52de20ee56998de..308e2cdfde88da2f66b23c45d2aba1c4ca81fefe 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -214,6 +214,7 @@ resolveExp e = case e of
       _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi
   PathP a u v   -> CTT.PathP <$> resolveExp a <*> resolveExp u <*> resolveExp v
   Comp u v ts   -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+  HComp u v ts  -> CTT.HComp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   Fill u v ts   -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   Trans u v     -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> pure Map.empty
   Glue u ts     -> CTT.Glue <$> resolveExp u <*> resolveSystem ts