From: Anders Date: Thu, 18 Jun 2015 13:31:49 +0000 (+0200) Subject: Reintroduce glueElem X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=70b124ef3416e7a9d3ec2a80d00cfe215cf58428;p=cubicaltt.git Reintroduce glueElem --- diff --git a/Exp.cf b/Exp.cf index b0f9470..83d9a99 100644 --- a/Exp.cf +++ b/Exp.cf @@ -34,7 +34,7 @@ IdP. Exp3 ::= "IdP" Exp4 Exp4 Exp4 ; Comp. Exp3 ::= "comp" Exp4 Exp4 System ; Fill. Exp3 ::= "fill" Exp4 Exp4 System ; Glue. Exp3 ::= "glue" Exp4 System ; --- GlueElem. Exp3 ::= "glueElem" Exp4 System ; +GlueElem. Exp3 ::= "glueElem" Exp4 System ; -- CompElem. Exp3 ::= "compElem" Exp4 System Exp4 System ; -- GlueLine. Exp3 ::= "glueLine" Formula Formula Exp4 ; -- GlueLineElem. Exp3 ::= "glueLineElem" Formula Formula Exp4 ; diff --git a/Resolver.hs b/Resolver.hs index 96ddc4d..68fbb8e 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -202,11 +202,11 @@ resolveExp e = case e of CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs <*> mapM resolveFormula phis _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi - IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z - Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts - Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts - Glue u ts -> CTT.Glue <$> resolveExp u <*> resolveSystem ts - -- GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts + IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z + Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts + Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts + Glue u ts -> CTT.Glue <$> resolveExp u <*> resolveSystem ts + GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts -- GlueLine phi psi u -> -- CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi -- GlueLineElem phi psi u ->