From: Anders Mörtberg <anma7372@r120.math.su.se>
Date: Tue, 16 Oct 2018 11:52:46 +0000 (+0200)
Subject: add parsing of hComp
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d48d58d583c6082ad3c38f69eed8d6e74b676185;p=cubicaltt.git

add parsing of hComp
---

diff --git a/CTT.hs b/CTT.hs
index 21f8e9f..7cfa412 100644
--- 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 3581a97..d6e3647 100644
--- 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 f93cc81..3f016e3 100644
--- 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 c61f65d..308e2cd 100644
--- 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