From d48d58d583c6082ad3c38f69eed8d6e74b676185 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 16 Oct 2018 13:52:46 +0200 Subject: [PATCH] add parsing of hComp --- CTT.hs | 4 +++- Eval.hs | 2 ++ Exp.cf | 1 + Resolver.hs | 1 + 4 files changed, 7 insertions(+), 1 deletion(-) 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 -- 2.34.1