cabal.sandbox.config
.stack-work
.*.sw?
-
+dist-ghcjs
+dist-newstyle
+result
\ No newline at end of file
--- /dev/null
+[submodule "reflex-platform"]
+ path = reflex-platform
+ url = git@github.com:reflex-frp/reflex-platform.git
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module CTT where
+import Data.Aeson
+import GHC.Generics (Generic)
+
import Control.Applicative
import Data.List
import Data.Maybe
data Loc = Loc { locFile :: String
, locPos :: (Int,Int) }
- deriving Eq
+ deriving (Eq, Generic, ToJSON, FromJSON)
type Ident = String
type LIdent = String
data Label = OLabel LIdent Tele -- Object label
| PLabel LIdent Tele [Name] (System Ter) -- Path label
- deriving (Eq,Show)
+ deriving (Eq,Show, Generic, ToJSON, FromJSON)
-- OBranch of the form: c x1 .. xn -> e
-- PBranch of the form: c x1 .. xn i1 .. im -> e
data Branch = OBranch LIdent [Ident] Ter
| PBranch LIdent [Ident] [Name] Ter
- deriving (Eq,Show)
+ deriving (Eq, Show, Generic, ToJSON, FromJSON)
-- Declarations: x : A = e
-- A group of mutual declarations is identified by its location. It is used to
| OpaqueDecl Ident
| TransparentDecl Ident
| TransparentAllDecl
- deriving Eq
+ deriving (Eq, Generic, ToJSON, FromJSON)
declIdents :: [Decl] -> [Ident]
declIdents decls = [ x | (x,_) <- decls ]
| Id Ter Ter Ter
| IdPair Ter (System Ter)
| IdJ Ter Ter Ter Ter Ter Ter
- deriving Eq
+ deriving (Eq, Generic, ToJSON, FromJSON)
-- For an expression t, returns (u,ts) where u is no application and t = u ts
unApps :: Ter -> (Ter,[Ter])
| VLam Ident Val Val
| VUnGlueElemU Val Val (System Val)
| VIdJ Val Val Val Val Val Val
- deriving Eq
+ deriving (Eq, Generic, ToJSON, FromJSON)
isNeutral :: Val -> Bool
isNeutral v = case v of
| Upd Ident Ctxt
| Sub Name Ctxt
| Def Loc [Decl] Ctxt
- deriving (Show)
+ deriving (Show, Generic, ToJSON, FromJSON)
instance Eq Ctxt where
c == d = case (c, d) of
-- only need to affect the lists and not the whole context.
-- The last list is the list of opaque names
newtype Env = Env (Ctxt,[Val],[Formula],Nameless (Set Ident))
- deriving (Eq)
+ deriving (Eq, Generic, ToJSON, FromJSON)
emptyEnv :: Env
emptyEnv = Env (Empty,[],[],Nameless Set.empty)
VPLam{} -> char '<' <> showPLam v
VSplit u v -> showVal u <+> showVal1 v
VVar x _ -> text x
- VOpaque x _ -> text ('#':x)
+ VOpaque x _ -> text ("#" ++ x)
VFst u -> showVal1 u <> text ".1"
VSnd u -> showVal1 u <> text ".2"
VPathP v0 v1 v2 -> text "PathP" <+> showVals [v0,v1,v2]
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances,
- GeneralizedNewtypeDeriving, TupleSections #-}
+ GeneralizedNewtypeDeriving, TupleSections,
+ StandaloneDeriving #-}
module Connections where
+import Data.Aeson
+import GHC.Generics (Generic)
+
import Control.Applicative
import Data.List
import Data.Map (Map,(!),keys,fromList,toList,mapKeys,elems,intersectionWith
import Test.QuickCheck
newtype Name = Name String
- deriving (Arbitrary,Eq,Ord)
+ deriving (Arbitrary, Eq, Ord, Generic, ToJSON, FromJSON, ToJSONKey, FromJSONKey)
instance Show Name where
show (Name i) = i
-- | Directions
data Dir = Zero | One
- deriving (Eq,Ord)
+ deriving (Eq, Ord, Generic, ToJSON, FromJSON)
instance Show Dir where
show Zero = "0"
-- Faces of the form: [(i,0),(j,1),(k,0)]
type Face = Map Name Dir
+deriving instance ToJSONKey Face
+deriving instance FromJSONKey Face
+
instance {-# OVERLAPPING #-} Arbitrary Face where
arbitrary = fromList <$> arbitrary
| NegAtom Name
| Formula :/\: Formula
| Formula :\/: Formula
- deriving Eq
+ deriving (Eq, Generic, ToJSON, FromJSON)
instance Show Formula where
show (Dir Zero) = "0"
unionsMap f = unions . map f
newtype Nameless a = Nameless { unNameless :: a }
- deriving (Eq, Ord)
+ deriving (Eq, Ord, Generic, ToJSON, FromJSON)
instance Nominal (Nameless a) where
support _ = []
--- /dev/null
+-- Haskell data types for the abstract syntax.
+-- Generated by the BNF converter.
+
+module Exp.Abs where
+
+import Data.Aeson as JSON
+import GHC.Generics (Generic)
+
+newtype AIdent = AIdent ((Int,Int),String)
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+newtype CIdent = CIdent String
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+newtype HoleIdent = HoleIdent ((Int,Int),String)
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Module = Module AIdent [Imp] [Decl]
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Imp = Import AIdent
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Decl
+ = DeclDef AIdent [Tele] Exp ExpWhere
+ | DeclData AIdent [Tele] [Label]
+ | DeclHData AIdent [Tele] [Label]
+ | DeclSplit AIdent [Tele] Exp [Branch]
+ | DeclUndef AIdent [Tele] Exp
+ | DeclMutual [Decl]
+ | DeclOpaque AIdent
+ | DeclTransparent AIdent
+ | DeclTransparentAll
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data ExpWhere = Where Exp [Decl] | NoWhere Exp
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Exp
+ = Let [Decl] Exp
+ | Lam [PTele] Exp
+ | PLam [AIdent] Exp
+ | Split Exp [Branch]
+ | Fun Exp Exp
+ | Pi [PTele] Exp
+ | Sigma [PTele] Exp
+ | AppFormula Exp Formula
+ | App Exp Exp
+ | PathP Exp Exp Exp
+ | Comp Exp Exp System
+ | HComp Exp Exp System
+ | Trans Exp Exp
+ | Fill Exp Exp System
+ | Glue Exp System
+ | GlueElem Exp System
+ | UnGlueElem Exp System
+ | Id Exp Exp Exp
+ | IdPair Exp System
+ | IdJ Exp Exp Exp Exp Exp Exp
+ | Fst Exp
+ | Snd Exp
+ | Pair Exp [Exp]
+ | Var AIdent
+ | PCon AIdent Exp
+ | U
+ | Hole HoleIdent
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Dir = Dir0 | Dir1
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data System = System [Side]
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Face = Face AIdent Dir
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Side = Side [Face] Exp
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Formula
+ = Disj Formula Formula
+ | Conj Formula CIdent Formula
+ | Neg Formula
+ | Atom AIdent
+ | Dir Dir
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Branch
+ = OBranch AIdent [AIdent] ExpWhere
+ | PBranch AIdent [AIdent] [AIdent] ExpWhere
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Label
+ = OLabel AIdent [Tele] | PLabel AIdent [Tele] [AIdent] System
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data Tele = Tele AIdent [AIdent] Exp
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
+data PTele = PTele Exp Exp
+ deriving (Eq, Ord, Show, Read, Generic, FromJSON, ToJSON)
+
--- /dev/null
+-- Haskell data types for the abstract syntax.
+-- Generated by the BNF converter.
+
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Exp.Abs where
+
+import Prelude (Char, Double, Integer, String, Int)
+import qualified Prelude as C (Eq, Ord, Show, Read)
+import qualified Data.String
+
+newtype AIdent = AIdent ((Int,Int),String)
+ deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)
+
+newtype CIdent = CIdent String
+ deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)
+
+newtype HoleIdent = HoleIdent ((Int,Int),String)
+ deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)
+
+data Module = Module AIdent [Imp] [Decl]
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Imp = Import AIdent
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Decl
+ = DeclDef AIdent [Tele] Exp ExpWhere
+ | DeclData AIdent [Tele] [Label]
+ | DeclHData AIdent [Tele] [Label]
+ | DeclSplit AIdent [Tele] Exp [Branch]
+ | DeclUndef AIdent [Tele] Exp
+ | DeclMutual [Decl]
+ | DeclOpaque AIdent
+ | DeclTransparent AIdent
+ | DeclTransparentAll
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data ExpWhere = Where Exp [Decl] | NoWhere Exp
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Exp
+ = Let [Decl] Exp
+ | Lam [PTele] Exp
+ | PLam [AIdent] Exp
+ | Split Exp [Branch]
+ | Fun Exp Exp
+ | Pi [PTele] Exp
+ | Sigma [PTele] Exp
+ | AppFormula Exp Formula
+ | App Exp Exp
+ | PathP Exp Exp Exp
+ | Comp Exp Exp System
+ | HComp Exp Exp System
+ | Trans Exp Exp
+ | Fill Exp Exp System
+ | Glue Exp System
+ | GlueElem Exp System
+ | UnGlueElem Exp System
+ | Id Exp Exp Exp
+ | IdPair Exp System
+ | IdJ Exp Exp Exp Exp Exp Exp
+ | Fst Exp
+ | Snd Exp
+ | Pair Exp [Exp]
+ | Var AIdent
+ | PCon AIdent Exp
+ | U
+ | Hole HoleIdent
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Dir = Dir0 | Dir1
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data System = System [Side]
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Face = Face AIdent Dir
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Side = Side [Face] Exp
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Formula
+ = Disj Formula Formula
+ | Conj Formula CIdent Formula
+ | Neg Formula
+ | Atom AIdent
+ | Dir Dir
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Branch
+ = OBranch AIdent [AIdent] ExpWhere
+ | PBranch AIdent [AIdent] [AIdent] ExpWhere
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Label
+ = OLabel AIdent [Tele] | PLabel AIdent [Tele] [AIdent] System
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data Tele = Tele AIdent [AIdent] Exp
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
+data PTele = PTele Exp Exp
+ deriving (C.Eq, C.Ord, C.Show, C.Read)
+
--- /dev/null
+The Language Exp
+BNF Converter
+
+
+%This txt2tags file is machine-generated by the BNF-converter
+%Process by txt2tags to generate html or latex
+
+
+
+This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place).
+
+==The lexical structure of Exp==
+
+===Literals===
+
+
+
+
+AIdent literals are recognized by the regular expression
+`````'_' | letter (letter | digit | ''' | '_')* | '!' digit*`````
+
+CIdent literals are recognized by the regular expression
+`````'/' '\'`````
+
+HoleIdent literals are recognized by the regular expression
+`````'?'`````
+
+
+===Reserved words and symbols===
+The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions.
+
+The reserved words used in Exp are the following:
+ | ``Glue`` | ``Id`` | ``PathP`` | ``U``
+ | ``comp`` | ``data`` | ``fill`` | ``glue``
+ | ``hComp`` | ``hdata`` | ``idC`` | ``idJ``
+ | ``import`` | ``in`` | ``let`` | ``module``
+ | ``mutual`` | ``opaque`` | ``split`` | ``transparent``
+ | ``transparent_all`` | ``transport`` | ``undefined`` | ``unglue``
+ | ``where`` | ``with`` | |
+
+The symbols used in Exp are the following:
+ | { | } | ; | :
+ | = | \ | -> | <
+ | > | split@ | * | @
+ | .1 | .2 | ( | ,
+ | ) | 0 | 1 | [
+ | ] | \/ | - | |
+
+===Comments===
+Single-line comments begin with --.Multiple-line comments are enclosed with {- and -}.
+
+==The syntactic structure of Exp==
+Non-terminals are enclosed between < and >.
+The symbols -> (production), **|** (union)
+and **eps** (empty rule) belong to the BNF notation.
+All other symbols are terminals.
+
+ | //Module// | -> | ``module`` //AIdent// ``where`` ``{`` //[Imp]// //[Decl]// ``}``
+ | //Imp// | -> | ``import`` //AIdent//
+ | //[Imp]// | -> | **eps**
+ | | **|** | //Imp//
+ | | **|** | //Imp// ``;`` //[Imp]//
+ | //Decl// | -> | //AIdent// //[Tele]// ``:`` //Exp// ``=`` //ExpWhere//
+ | | **|** | ``data`` //AIdent// //[Tele]// ``=`` //[Label]//
+ | | **|** | ``hdata`` //AIdent// //[Tele]// ``=`` //[Label]//
+ | | **|** | //AIdent// //[Tele]// ``:`` //Exp// ``=`` ``split`` ``{`` //[Branch]// ``}``
+ | | **|** | //AIdent// //[Tele]// ``:`` //Exp// ``=`` ``undefined``
+ | | **|** | ``mutual`` ``{`` //[Decl]// ``}``
+ | | **|** | ``opaque`` //AIdent//
+ | | **|** | ``transparent`` //AIdent//
+ | | **|** | ``transparent_all``
+ | //[Decl]// | -> | **eps**
+ | | **|** | //Decl//
+ | | **|** | //Decl// ``;`` //[Decl]//
+ | //ExpWhere// | -> | //Exp// ``where`` ``{`` //[Decl]// ``}``
+ | | **|** | //Exp//
+ | //Exp// | -> | ``let`` ``{`` //[Decl]// ``}`` ``in`` //Exp//
+ | | **|** | ``\`` //[PTele]// ``->`` //Exp//
+ | | **|** | ``<`` //[AIdent]// ``>`` //Exp//
+ | | **|** | ``split@`` //Exp// ``with`` ``{`` //[Branch]// ``}``
+ | | **|** | //Exp1//
+ | //Exp1// | -> | //Exp2// ``->`` //Exp1//
+ | | **|** | //[PTele]// ``->`` //Exp1//
+ | | **|** | //[PTele]// ``*`` //Exp1//
+ | | **|** | //Exp2//
+ | //Exp2// | -> | //Exp2// ``@`` //Formula//
+ | | **|** | //Exp2// //Exp3//
+ | | **|** | //Exp3//
+ | //Exp3// | -> | ``PathP`` //Exp4// //Exp4// //Exp4//
+ | | **|** | ``comp`` //Exp4// //Exp4// //System//
+ | | **|** | ``hComp`` //Exp4// //Exp4// //System//
+ | | **|** | ``transport`` //Exp4// //Exp4//
+ | | **|** | ``fill`` //Exp4// //Exp4// //System//
+ | | **|** | ``Glue`` //Exp4// //System//
+ | | **|** | ``glue`` //Exp4// //System//
+ | | **|** | ``unglue`` //Exp4// //System//
+ | | **|** | ``Id`` //Exp4// //Exp4// //Exp3//
+ | | **|** | ``idC`` //Exp4// //System//
+ | | **|** | ``idJ`` //Exp4// //Exp4// //Exp4// //Exp4// //Exp4// //Exp4//
+ | | **|** | //Exp4//
+ | //Exp4// | -> | //Exp4// ``.1``
+ | | **|** | //Exp4// ``.2``
+ | | **|** | //Exp5//
+ | //Exp5// | -> | ``(`` //Exp// ``,`` //[Exp]// ``)``
+ | | **|** | //AIdent//
+ | | **|** | //AIdent// ``{`` //Exp// ``}``
+ | | **|** | ``U``
+ | | **|** | //HoleIdent//
+ | | **|** | ``(`` //Exp// ``)``
+ | //[Exp]// | -> | //Exp//
+ | | **|** | //Exp// ``,`` //[Exp]//
+ | //Dir// | -> | ``0``
+ | | **|** | ``1``
+ | //System// | -> | ``[`` //[Side]// ``]``
+ | //Face// | -> | ``(`` //AIdent// ``=`` //Dir// ``)``
+ | //[Face]// | -> | **eps**
+ | | **|** | //Face// //[Face]//
+ | //Side// | -> | //[Face]// ``->`` //Exp//
+ | //[Side]// | -> | **eps**
+ | | **|** | //Side//
+ | | **|** | //Side// ``,`` //[Side]//
+ | //Formula// | -> | //Formula// ``\/`` //Formula1//
+ | | **|** | //Formula1//
+ | //Formula1// | -> | //Formula1// //CIdent// //Formula2//
+ | | **|** | //Formula2//
+ | //Formula2// | -> | ``-`` //Formula2//
+ | | **|** | //AIdent//
+ | | **|** | //Dir//
+ | | **|** | ``(`` //Formula// ``)``
+ | //Branch// | -> | //AIdent// //[AIdent]// ``->`` //ExpWhere//
+ | | **|** | //AIdent// //[AIdent]// ``@`` //[AIdent]// ``->`` //ExpWhere//
+ | //[Branch]// | -> | **eps**
+ | | **|** | //Branch//
+ | | **|** | //Branch// ``;`` //[Branch]//
+ | //Label// | -> | //AIdent// //[Tele]//
+ | | **|** | //AIdent// //[Tele]// ``<`` //[AIdent]// ``>`` //System//
+ | //[Label]// | -> | **eps**
+ | | **|** | //Label//
+ | | **|** | //Label// ``|`` //[Label]//
+ | //Tele// | -> | ``(`` //AIdent// //[AIdent]// ``:`` //Exp// ``)``
+ | //[Tele]// | -> | **eps**
+ | | **|** | //Tele// //[Tele]//
+ | //PTele// | -> | ``(`` //Exp// ``:`` //Exp// ``)``
+ | //[PTele]// | -> | //PTele//
+ | | **|** | //PTele// //[PTele]//
+ | //[AIdent]// | -> | **eps**
+ | | **|** | //AIdent// //[AIdent]//
+
+
--- /dev/null
+The Language Exp
+BNF Converter
+
+
+%This txt2tags file is machine-generated by the BNF-converter
+%Process by txt2tags to generate html or latex
+
+
+
+This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place).
+
+==The lexical structure of Exp==
+
+===Literals===
+
+
+
+
+AIdent literals are recognized by the regular expression
+`````'_' | letter (["'_"] | digit | letter)* | '!' digit*`````
+
+CIdent literals are recognized by the regular expression
+`````{"/\"}`````
+
+HoleIdent literals are recognized by the regular expression
+`````'?'`````
+
+
+===Reserved words and symbols===
+The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions.
+
+The reserved words used in Exp are the following:
+ | ``Glue`` | ``Id`` | ``PathP`` | ``U``
+ | ``comp`` | ``data`` | ``fill`` | ``glue``
+ | ``hComp`` | ``hdata`` | ``idC`` | ``idJ``
+ | ``import`` | ``in`` | ``let`` | ``module``
+ | ``mutual`` | ``opaque`` | ``split`` | ``transparent``
+ | ``transparent_all`` | ``transport`` | ``undefined`` | ``unglue``
+ | ``where`` | ``with`` | |
+
+The symbols used in Exp are the following:
+ | { | } | ; | :
+ | = | \ | -> | <
+ | > | split@ | * | @
+ | .1 | .2 | ( | ,
+ | ) | 0 | 1 | [
+ | ] | \/ | - | |
+
+===Comments===
+Single-line comments begin with --.Multiple-line comments are enclosed with {- and -}.
+
+==The syntactic structure of Exp==
+Non-terminals are enclosed between < and >.
+The symbols -> (production), **|** (union)
+and **eps** (empty rule) belong to the BNF notation.
+All other symbols are terminals.
+
+ | //Module// | -> | ``module`` //AIdent// ``where`` ``{`` //[Imp]// //[Decl]// ``}``
+ | //Imp// | -> | ``import`` //AIdent//
+ | //[Imp]// | -> | **eps**
+ | | **|** | //Imp//
+ | | **|** | //Imp// ``;`` //[Imp]//
+ | //Decl// | -> | //AIdent// //[Tele]// ``:`` //Exp// ``=`` //ExpWhere//
+ | | **|** | ``data`` //AIdent// //[Tele]// ``=`` //[Label]//
+ | | **|** | ``hdata`` //AIdent// //[Tele]// ``=`` //[Label]//
+ | | **|** | //AIdent// //[Tele]// ``:`` //Exp// ``=`` ``split`` ``{`` //[Branch]// ``}``
+ | | **|** | //AIdent// //[Tele]// ``:`` //Exp// ``=`` ``undefined``
+ | | **|** | ``mutual`` ``{`` //[Decl]// ``}``
+ | | **|** | ``opaque`` //AIdent//
+ | | **|** | ``transparent`` //AIdent//
+ | | **|** | ``transparent_all``
+ | //[Decl]// | -> | **eps**
+ | | **|** | //Decl//
+ | | **|** | //Decl// ``;`` //[Decl]//
+ | //ExpWhere// | -> | //Exp// ``where`` ``{`` //[Decl]// ``}``
+ | | **|** | //Exp//
+ | //Exp// | -> | ``let`` ``{`` //[Decl]// ``}`` ``in`` //Exp//
+ | | **|** | ``\`` //[PTele]// ``->`` //Exp//
+ | | **|** | ``<`` //[AIdent]// ``>`` //Exp//
+ | | **|** | ``split@`` //Exp// ``with`` ``{`` //[Branch]// ``}``
+ | | **|** | //Exp1//
+ | //Exp1// | -> | //Exp2// ``->`` //Exp1//
+ | | **|** | //[PTele]// ``->`` //Exp1//
+ | | **|** | //[PTele]// ``*`` //Exp1//
+ | | **|** | //Exp2//
+ | //Exp2// | -> | //Exp2// ``@`` //Formula//
+ | | **|** | //Exp2// //Exp3//
+ | | **|** | //Exp3//
+ | //Exp3// | -> | ``PathP`` //Exp4// //Exp4// //Exp4//
+ | | **|** | ``comp`` //Exp4// //Exp4// //System//
+ | | **|** | ``hComp`` //Exp4// //Exp4// //System//
+ | | **|** | ``transport`` //Exp4// //Exp4//
+ | | **|** | ``fill`` //Exp4// //Exp4// //System//
+ | | **|** | ``Glue`` //Exp4// //System//
+ | | **|** | ``glue`` //Exp4// //System//
+ | | **|** | ``unglue`` //Exp4// //System//
+ | | **|** | ``Id`` //Exp4// //Exp4// //Exp3//
+ | | **|** | ``idC`` //Exp4// //System//
+ | | **|** | ``idJ`` //Exp4// //Exp4// //Exp4// //Exp4// //Exp4// //Exp4//
+ | | **|** | //Exp4//
+ | //Exp4// | -> | //Exp4// ``.1``
+ | | **|** | //Exp4// ``.2``
+ | | **|** | //Exp5//
+ | //Exp5// | -> | ``(`` //Exp// ``,`` //[Exp]// ``)``
+ | | **|** | //AIdent//
+ | | **|** | //AIdent// ``{`` //Exp// ``}``
+ | | **|** | ``U``
+ | | **|** | //HoleIdent//
+ | | **|** | ``(`` //Exp// ``)``
+ | //[Exp]// | -> | //Exp//
+ | | **|** | //Exp// ``,`` //[Exp]//
+ | //Dir// | -> | ``0``
+ | | **|** | ``1``
+ | //System// | -> | ``[`` //[Side]// ``]``
+ | //Face// | -> | ``(`` //AIdent// ``=`` //Dir// ``)``
+ | //[Face]// | -> | **eps**
+ | | **|** | //Face// //[Face]//
+ | //Side// | -> | //[Face]// ``->`` //Exp//
+ | //[Side]// | -> | **eps**
+ | | **|** | //Side//
+ | | **|** | //Side// ``,`` //[Side]//
+ | //Formula// | -> | //Formula// ``\/`` //Formula1//
+ | | **|** | //Formula1//
+ | //Formula1// | -> | //Formula1// //CIdent// //Formula2//
+ | | **|** | //Formula2//
+ | //Formula2// | -> | ``-`` //Formula2//
+ | | **|** | //AIdent//
+ | | **|** | //Dir//
+ | | **|** | ``(`` //Formula// ``)``
+ | //Branch// | -> | //AIdent// //[AIdent]// ``->`` //ExpWhere//
+ | | **|** | //AIdent// //[AIdent]// ``@`` //[AIdent]// ``->`` //ExpWhere//
+ | //[Branch]// | -> | **eps**
+ | | **|** | //Branch//
+ | | **|** | //Branch// ``;`` //[Branch]//
+ | //Label// | -> | //AIdent// //[Tele]//
+ | | **|** | //AIdent// //[Tele]// ``<`` //[AIdent]// ``>`` //System//
+ | //[Label]// | -> | **eps**
+ | | **|** | //Label//
+ | | **|** | //Label// ``|`` //[Label]//
+ | //Tele// | -> | ``(`` //AIdent// //[AIdent]// ``:`` //Exp// ``)``
+ | //[Tele]// | -> | **eps**
+ | | **|** | //Tele// //[Tele]//
+ | //PTele// | -> | ``(`` //Exp// ``:`` //Exp// ``)``
+ | //[PTele]// | -> | //PTele//
+ | | **|** | //PTele// //[PTele]//
+ | //[AIdent]// | -> | **eps**
+ | | **|** | //AIdent// //[AIdent]//
+
+
--- /dev/null
+-- BNF Converter: Error Monad
+-- Copyright (C) 2004 Author: Aarne Ranta
+
+-- This file comes with NO WARRANTY and may be used FOR ANY PURPOSE.
+module Exp.ErrM where
+
+-- the Error monad: like Maybe type with error msgs
+
+import Control.Monad (MonadPlus(..), liftM)
+import Control.Applicative (Applicative(..), Alternative(..))
+
+data Err a = Ok a | Bad String
+ deriving (Read, Show, Eq, Ord)
+
+instance Monad Err where
+ return = Ok
+ Ok a >>= f = f a
+ Bad s >>= _ = Bad s
+
+instance Applicative Err where
+ pure = Ok
+ (Bad s) <*> _ = Bad s
+ (Ok f) <*> o = liftM f o
+
+instance Functor Err where
+ fmap = liftM
+
+instance MonadPlus Err where
+ mzero = Bad "Err.mzero"
+ mplus (Bad _) y = y
+ mplus x _ = x
+
+instance Alternative Err where
+ empty = mzero
+ (<|>) = mplus
--- /dev/null
+{-# LANGUAGE CPP #-}
+
+#if __GLASGOW_HASKELL__ >= 708
+---------------------------------------------------------------------------
+-- Pattern synonyms exist since ghc 7.8.
+
+-- | BNF Converter: Error Monad.
+--
+-- Module for backwards compatibility.
+--
+-- The generated parser now uses @'Either' String@ as error monad.
+-- This module defines a type synonym 'Err' and pattern synonyms
+-- 'Bad' and 'Ok' for 'Left' and 'Right'.
+
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Exp.ErrM where
+
+import Control.Monad (MonadPlus(..))
+import Control.Applicative (Alternative(..))
+
+-- | Error monad with 'String' error messages.
+type Err = Either String
+
+pattern Bad msg = Left msg
+pattern Ok a = Right a
+
+#if __GLASGOW_HASKELL__ >= 808
+instance MonadFail Err where
+ fail = Bad
+#endif
+
+instance Alternative Err where
+ empty = Left "Err.empty"
+ (<|>) Left{} = id
+ (<|>) x@Right{} = const x
+
+instance MonadPlus Err where
+ mzero = empty
+ mplus = (<|>)
+
+#else
+---------------------------------------------------------------------------
+-- ghc 7.6 and before: use old definition as data type.
+
+-- | BNF Converter: Error Monad
+
+-- Copyright (C) 2004 Author: Aarne Ranta
+-- This file comes with NO WARRANTY and may be used FOR ANY PURPOSE.
+
+module Exp.ErrM where
+
+-- the Error monad: like Maybe type with error msgs
+
+import Control.Applicative (Applicative(..), Alternative(..))
+import Control.Monad (MonadPlus(..), liftM)
+
+data Err a = Ok a | Bad String
+ deriving (Read, Show, Eq, Ord)
+
+instance Monad Err where
+ return = Ok
+ Ok a >>= f = f a
+ Bad s >>= _ = Bad s
+
+instance Applicative Err where
+ pure = Ok
+ (Bad s) <*> _ = Bad s
+ (Ok f) <*> o = liftM f o
+
+instance Functor Err where
+ fmap = liftM
+
+instance MonadPlus Err where
+ mzero = Bad "Err.mzero"
+ mplus (Bad _) y = y
+ mplus x _ = x
+
+instance Alternative Err where
+ empty = mzero
+ (<|>) = mplus
+
+#endif
--- /dev/null
+module Exp.Layout where
+
+import Exp.Lex
+
+
+import Data.Maybe (isNothing, fromJust)
+
+-- Generated by the BNF Converter
+
+-- local parameters
+
+
+topLayout :: Bool
+topLayout = False
+
+layoutWords, layoutStopWords :: [String]
+layoutWords = ["where","let","split","mutual","with"]
+layoutStopWords = ["in"]
+
+-- layout separators
+
+
+layoutOpen, layoutClose, layoutSep :: String
+layoutOpen = "{"
+layoutClose = "}"
+layoutSep = ";"
+
+-- | Replace layout syntax with explicit layout tokens.
+resolveLayout :: Bool -- ^ Whether to use top-level layout.
+ -> [Token] -> [Token]
+resolveLayout tp = res Nothing [if tl then Implicit 1 else Explicit]
+ where
+ -- Do top-level layout if the function parameter and the grammar say so.
+ tl = tp && topLayout
+
+ res :: Maybe Token -- ^ The previous token, if any.
+ -> [Block] -- ^ A stack of layout blocks.
+ -> [Token] -> [Token]
+
+ -- The stack should never be empty.
+ res _ [] ts = error $ "Layout error: stack empty. Tokens: " ++ show ts
+
+ res _ st (t0:ts)
+ -- We found an open brace in the input,
+ -- put an explicit layout block on the stack.
+ -- This is done even if there was no layout word,
+ -- to keep opening and closing braces.
+ | isLayoutOpen t0 = moveAlong (Explicit:st) [t0] ts
+
+ -- We are in an implicit layout block
+ res pt st@(Implicit n:ns) (t0:ts)
+
+ -- End of implicit block by a layout stop word
+ | isStop t0 =
+ -- Exit the current block and all implicit blocks
+ -- more indented than the current token
+ let (ebs,ns') = span (`moreIndent` column t0) ns
+ moreIndent (Implicit x) y = x > y
+ moreIndent Explicit _ = False
+ -- the number of blocks exited
+ b = 1 + length ebs
+ bs = replicate b layoutClose
+ -- Insert closing braces after the previous token.
+ (ts1,ts2) = splitAt (1+b) $ addTokens (afterPrev pt) bs (t0:ts)
+ in moveAlong ns' ts1 ts2
+
+ -- End of an implicit layout block
+ | newLine pt t0 && column t0 < n =
+ -- Insert a closing brace after the previous token.
+ let b:t0':ts' = addToken (afterPrev pt) layoutClose (t0:ts)
+ -- Repeat, with the current block removed from the stack
+ in moveAlong ns [b] (t0':ts')
+
+ res pt st (t0:ts)
+ -- Start a new layout block if the first token is a layout word
+ | isLayout t0 =
+ case ts of
+ -- Explicit layout, just move on. The case above
+ -- will push an explicit layout block.
+ t1:_ | isLayoutOpen t1 -> moveAlong st [t0] ts
+ -- The column of the next token determines the starting column
+ -- of the implicit layout block.
+ -- However, the next block needs to be strictly more indented
+ -- than the previous block.
+ _ -> let col = max (indentation st + 1) $
+ -- at end of file, the start column doesn't matter
+ if null ts then column t0 else column (head ts)
+ -- insert an open brace after the layout word
+ b:ts' = addToken (nextPos t0) layoutOpen ts
+ -- save the start column
+ st' = Implicit col:st
+ in -- Do we have to insert an extra layoutSep?
+ case st of
+ Implicit n:_
+ | newLine pt t0 && column t0 == n
+ && not (isNothing pt ||
+ isTokenIn [layoutSep,layoutOpen] (fromJust pt)) ->
+ let b':t0':b'':ts'' =
+ addToken (afterPrev pt) layoutSep (t0:b:ts')
+ in moveAlong st' [b',t0',b''] ts'
+ _ -> moveAlong st' [t0,b] ts'
+
+ -- If we encounter a closing brace, exit the first explicit layout block.
+ | isLayoutClose t0 =
+ let st' = drop 1 (dropWhile isImplicit st)
+ in if null st'
+ then error $ "Layout error: Found " ++ layoutClose ++ " at ("
+ ++ show (line t0) ++ "," ++ show (column t0)
+ ++ ") without an explicit layout block."
+ else moveAlong st' [t0] ts
+
+ -- Insert separator if necessary.
+ res pt st@(Implicit n:ns) (t0:ts)
+ -- Encounted a new line in an implicit layout block.
+ | newLine pt t0 && column t0 == n =
+ -- Insert a semicolon after the previous token.
+ -- unless we are the beginning of the file,
+ -- or the previous token is a semicolon or open brace.
+ if isNothing pt || isTokenIn [layoutSep,layoutOpen] (fromJust pt)
+ then moveAlong st [t0] ts
+ else let b:t0':ts' = addToken (afterPrev pt) layoutSep (t0:ts)
+ in moveAlong st [b,t0'] ts'
+
+ -- Nothing to see here, move along.
+ res _ st (t:ts) = moveAlong st [t] ts
+
+ -- At EOF: skip explicit blocks.
+ res (Just t) (Explicit:bs) [] | null bs = []
+ | otherwise = res (Just t) bs []
+
+ -- If we are using top-level layout, insert a semicolon after
+ -- the last token, if there isn't one already
+ res (Just t) [Implicit _n] []
+ | isTokenIn [layoutSep] t = []
+ | otherwise = addToken (nextPos t) layoutSep []
+
+ -- At EOF in an implicit, non-top-level block: close the block
+ res (Just t) (Implicit _n:bs) [] =
+ let c = addToken (nextPos t) layoutClose []
+ in moveAlong bs c []
+
+ -- This should only happen if the input is empty.
+ res Nothing _st [] = []
+
+ -- | Move on to the next token.
+ moveAlong :: [Block] -- ^ The layout stack.
+ -> [Token] -- ^ Any tokens just processed.
+ -> [Token] -- ^ the rest of the tokens.
+ -> [Token]
+ moveAlong _ [] _ = error "Layout error: moveAlong got [] as old tokens"
+ moveAlong st ot ts = ot ++ res (Just $ last ot) st ts
+
+ newLine :: Maybe Token -> Token -> Bool
+ newLine pt t0 = case pt of
+ Nothing -> True
+ Just t -> line t /= line t0
+
+data Block
+ = Implicit Int -- ^ An implicit layout block with its start column.
+ | Explicit
+ deriving Show
+
+-- | Get current indentation. 0 if we are in an explicit block.
+indentation :: [Block] -> Int
+indentation (Implicit n : _) = n
+indentation _ = 0
+
+-- | Check if s block is implicit.
+isImplicit :: Block -> Bool
+isImplicit (Implicit _) = True
+isImplicit _ = False
+
+type Position = Posn
+
+-- | Insert a number of tokens at the begninning of a list of tokens.
+addTokens :: Position -- ^ Position of the first new token.
+ -> [String] -- ^ Token symbols.
+ -> [Token] -- ^ The rest of the tokens. These will have their
+ -- positions updated to make room for the new tokens .
+ -> [Token]
+addTokens p ss ts = foldr (addToken p) ts ss
+
+-- | Insert a new symbol token at the begninning of a list of tokens.
+addToken :: Position -- ^ Position of the new token.
+ -> String -- ^ Symbol in the new token.
+ -> [Token] -- ^ The rest of the tokens. These will have their
+ -- positions updated to make room for the new token.
+ -> [Token]
+addToken p s ts = sToken p s : map (incrGlobal p (length s)) ts
+
+-- | Get the position immediately to the right of the given token.
+-- If no token is given, gets the first position in the file.
+afterPrev :: Maybe Token -> Position
+afterPrev = maybe (Pn 0 1 1) nextPos
+
+-- | Get the position immediately to the right of the given token.
+nextPos :: Token -> Position
+nextPos t = Pn (g + s) l (c + s + 1)
+ where Pn g l c = position t
+ s = tokenLength t
+
+-- | Add to the global and column positions of a token.
+-- The column position is only changed if the token is on
+-- the same line as the given position.
+incrGlobal :: Position -- ^ If the token is on the same line
+ -- as this position, update the column position.
+ -> Int -- ^ Number of characters to add to the position.
+ -> Token -> Token
+incrGlobal (Pn _ l0 _) i (PT (Pn g l c) t) =
+ if l /= l0 then PT (Pn (g + i) l c) t
+ else PT (Pn (g + i) l (c + i)) t
+incrGlobal _ _ p = error $ "cannot add token at " ++ show p
+
+-- | Create a symbol token.
+sToken :: Position -> String -> Token
+sToken p s = PT p (TS s i)
+ where
+ i = case s of
+ "(" -> 1
+ ")" -> 2
+ "*" -> 3
+ "," -> 4
+ "-" -> 5
+ "->" -> 6
+ ".1" -> 7
+ ".2" -> 8
+ "0" -> 9
+ "1" -> 10
+ ":" -> 11
+ ";" -> 12
+ "<" -> 13
+ "=" -> 14
+ ">" -> 15
+ "@" -> 16
+ "Glue" -> 17
+ "Id" -> 18
+ "PathP" -> 19
+ "U" -> 20
+ "[" -> 21
+ "\\" -> 22
+ "\\/" -> 23
+ "]" -> 24
+ "comp" -> 25
+ "data" -> 26
+ "fill" -> 27
+ "glue" -> 28
+ "hComp" -> 29
+ "hdata" -> 30
+ "idC" -> 31
+ "idJ" -> 32
+ "import" -> 33
+ "in" -> 34
+ "let" -> 35
+ "module" -> 36
+ "mutual" -> 37
+ "opaque" -> 38
+ "split" -> 39
+ "split@" -> 40
+ "transparent" -> 41
+ "transparent_all" -> 42
+ "transport" -> 43
+ "undefined" -> 44
+ "unglue" -> 45
+ "where" -> 46
+ "with" -> 47
+ "{" -> 48
+ "|" -> 49
+ "}" -> 50
+ _ -> error $ "not a reserved word: " ++ show s
+
+-- | Get the position of a token.
+position :: Token -> Position
+position t = case t of
+ PT p _ -> p
+ Err p -> p
+
+-- | Get the line number of a token.
+line :: Token -> Int
+line t = case position t of Pn _ l _ -> l
+
+-- | Get the column number of a token.
+column :: Token -> Int
+column t = case position t of Pn _ _ c -> c
+
+-- | Check if a token is one of the given symbols.
+isTokenIn :: [String] -> Token -> Bool
+isTokenIn ts t = case t of
+ PT _ (TS r _) | r `elem` ts -> True
+ _ -> False
+
+-- | Check if a word is a layout start token.
+isLayout :: Token -> Bool
+isLayout = isTokenIn layoutWords
+
+-- | Check if a token is a layout stop token.
+isStop :: Token -> Bool
+isStop = isTokenIn layoutStopWords
+
+-- | Check if a token is the layout open token.
+isLayoutOpen :: Token -> Bool
+isLayoutOpen = isTokenIn [layoutOpen]
+
+-- | Check if a token is the layout close token.
+isLayoutClose :: Token -> Bool
+isLayoutClose = isTokenIn [layoutClose]
+
+-- | Get the number of characters in the token.
+tokenLength :: Token -> Int
+tokenLength t = length $ prToken t
+
--- /dev/null
+module Exp.Layout where
+
+import Exp.Lex
+
+
+
+import Data.Maybe (isNothing, fromJust)
+
+-- Generated by the BNF Converter
+
+-- local parameters
+
+
+topLayout :: Bool
+topLayout = False
+
+layoutWords, layoutStopWords :: [String]
+layoutWords = ["where","let","split","mutual","with"]
+layoutStopWords = ["in"]
+
+-- layout separators
+
+
+layoutOpen, layoutClose, layoutSep :: String
+layoutOpen = "{"
+layoutClose = "}"
+layoutSep = ";"
+
+-- | Replace layout syntax with explicit layout tokens.
+resolveLayout :: Bool -- ^ Whether to use top-level layout.
+ -> [Token] -> [Token]
+resolveLayout tp = res Nothing [if tl then Implicit 1 else Explicit]
+ where
+ -- Do top-level layout if the function parameter and the grammar say so.
+ tl = tp && topLayout
+
+ res :: Maybe Token -- ^ The previous token, if any.
+ -> [Block] -- ^ A stack of layout blocks.
+ -> [Token] -> [Token]
+
+ -- The stack should never be empty.
+ res _ [] ts = error $ "Layout error: stack empty. Tokens: " ++ show ts
+
+ res _ st (t0:ts)
+ -- We found an open brace in the input,
+ -- put an explicit layout block on the stack.
+ -- This is done even if there was no layout word,
+ -- to keep opening and closing braces.
+ | isLayoutOpen t0 = moveAlong (Explicit:st) [t0] ts
+
+ -- We are in an implicit layout block
+ res pt st@(Implicit n:ns) (t0:ts)
+
+ -- End of implicit block by a layout stop word
+ | isStop t0 =
+ -- Exit the current block and all implicit blocks
+ -- more indented than the current token
+ let (ebs,ns') = span (`moreIndent` column t0) ns
+ moreIndent (Implicit x) y = x > y
+ moreIndent Explicit _ = False
+ -- the number of blocks exited
+ b = 1 + length ebs
+ bs = replicate b layoutClose
+ -- Insert closing braces after the previous token.
+ (ts1,ts2) = splitAt (1+b) $ addTokens (afterPrev pt) bs (t0:ts)
+ in moveAlong ns' ts1 ts2
+
+ -- End of an implicit layout block
+ | newLine pt t0 && column t0 < n =
+ -- Insert a closing brace after the previous token.
+ let b:t0':ts' = addToken (afterPrev pt) layoutClose (t0:ts)
+ -- Repeat, with the current block removed from the stack
+ in moveAlong ns [b] (t0':ts')
+
+ res pt st (t0:ts)
+ -- Start a new layout block if the first token is a layout word
+ | isLayout t0 =
+ case ts of
+ -- Explicit layout, just move on. The case above
+ -- will push an explicit layout block.
+ t1:_ | isLayoutOpen t1 -> moveAlong st [t0] ts
+ -- The column of the next token determines the starting column
+ -- of the implicit layout block.
+ -- However, the next block needs to be strictly more indented
+ -- than the previous block.
+ _ -> let col = max (indentation st + 1) $
+ -- at end of file, the start column doesn't matter
+ if null ts then column t0 else column (head ts)
+ -- insert an open brace after the layout word
+ b:ts' = addToken (nextPos t0) layoutOpen ts
+ -- save the start column
+ st' = Implicit col:st
+ in -- Do we have to insert an extra layoutSep?
+ case st of
+ Implicit n:_
+ | newLine pt t0 && column t0 == n
+ && not (isNothing pt ||
+ isTokenIn [layoutSep,layoutOpen] (fromJust pt)) ->
+ let b':t0':b'':ts'' =
+ addToken (afterPrev pt) layoutSep (t0:b:ts')
+ in moveAlong st' [b',t0',b''] ts'
+ _ -> moveAlong st' [t0,b] ts'
+
+ -- If we encounter a closing brace, exit the first explicit layout block.
+ | isLayoutClose t0 =
+ let st' = drop 1 (dropWhile isImplicit st)
+ in if null st'
+ then error $ "Layout error: Found " ++ layoutClose ++ " at ("
+ ++ show (line t0) ++ "," ++ show (column t0)
+ ++ ") without an explicit layout block."
+ else moveAlong st' [t0] ts
+
+ -- Insert separator if necessary.
+ res pt st@(Implicit n:ns) (t0:ts)
+ -- Encounted a new line in an implicit layout block.
+ | newLine pt t0 && column t0 == n =
+ -- Insert a semicolon after the previous token.
+ -- unless we are the beginning of the file,
+ -- or the previous token is a semicolon or open brace.
+ if isNothing pt || isTokenIn [layoutSep,layoutOpen] (fromJust pt)
+ then moveAlong st [t0] ts
+ else let b:t0':ts' = addToken (afterPrev pt) layoutSep (t0:ts)
+ in moveAlong st [b,t0'] ts'
+
+ -- Nothing to see here, move along.
+ res _ st (t:ts) = moveAlong st [t] ts
+
+ -- At EOF: skip explicit blocks.
+ res (Just t) (Explicit:bs) [] | null bs = []
+ | otherwise = res (Just t) bs []
+
+ -- If we are using top-level layout, insert a semicolon after
+ -- the last token, if there isn't one already
+ res (Just t) [Implicit _n] []
+ | isTokenIn [layoutSep] t = []
+ | otherwise = addToken (nextPos t) layoutSep []
+
+ -- At EOF in an implicit, non-top-level block: close the block
+ res (Just t) (Implicit _n:bs) [] =
+ let c = addToken (nextPos t) layoutClose []
+ in moveAlong bs c []
+
+ -- This should only happen if the input is empty.
+ res Nothing _st [] = []
+
+ -- | Move on to the next token.
+ moveAlong :: [Block] -- ^ The layout stack.
+ -> [Token] -- ^ Any tokens just processed.
+ -> [Token] -- ^ the rest of the tokens.
+ -> [Token]
+ moveAlong _ [] _ = error "Layout error: moveAlong got [] as old tokens"
+ moveAlong st ot ts = ot ++ res (Just $ last ot) st ts
+
+ newLine :: Maybe Token -> Token -> Bool
+ newLine pt t0 = case pt of
+ Nothing -> True
+ Just t -> line t /= line t0
+
+data Block
+ = Implicit Int -- ^ An implicit layout block with its start column.
+ | Explicit
+ deriving Show
+
+-- | Get current indentation. 0 if we are in an explicit block.
+indentation :: [Block] -> Int
+indentation (Implicit n : _) = n
+indentation _ = 0
+
+-- | Check if s block is implicit.
+isImplicit :: Block -> Bool
+isImplicit (Implicit _) = True
+isImplicit _ = False
+
+type Position = Posn
+
+-- | Insert a number of tokens at the begninning of a list of tokens.
+addTokens :: Position -- ^ Position of the first new token.
+ -> [String] -- ^ Token symbols.
+ -> [Token] -- ^ The rest of the tokens. These will have their
+ -- positions updated to make room for the new tokens .
+ -> [Token]
+addTokens p ss ts = foldr (addToken p) ts ss
+
+-- | Insert a new symbol token at the begninning of a list of tokens.
+addToken :: Position -- ^ Position of the new token.
+ -> String -- ^ Symbol in the new token.
+ -> [Token] -- ^ The rest of the tokens. These will have their
+ -- positions updated to make room for the new token.
+ -> [Token]
+addToken p s ts = sToken p s : map (incrGlobal p (length s)) ts
+
+-- | Get the position immediately to the right of the given token.
+-- If no token is given, gets the first position in the file.
+afterPrev :: Maybe Token -> Position
+afterPrev = maybe (Pn 0 1 1) nextPos
+
+-- | Get the position immediately to the right of the given token.
+nextPos :: Token -> Position
+nextPos t = Pn (g + s) l (c + s + 1)
+ where Pn g l c = position t
+ s = tokenLength t
+
+-- | Add to the global and column positions of a token.
+-- The column position is only changed if the token is on
+-- the same line as the given position.
+incrGlobal :: Position -- ^ If the token is on the same line
+ -- as this position, update the column position.
+ -> Int -- ^ Number of characters to add to the position.
+ -> Token -> Token
+incrGlobal (Pn _ l0 _) i (PT (Pn g l c) t) =
+ if l /= l0 then PT (Pn (g + i) l c) t
+ else PT (Pn (g + i) l (c + i)) t
+incrGlobal _ _ p = error $ "cannot add token at " ++ show p
+
+-- | Create a symbol token.
+sToken :: Position -> String -> Token
+sToken p s = PT p (TS s i)
+ where
+ i = case s of
+ "(" -> 1
+ ")" -> 2
+ "*" -> 3
+ "," -> 4
+ "-" -> 5
+ "->" -> 6
+ ".1" -> 7
+ ".2" -> 8
+ "0" -> 9
+ "1" -> 10
+ ":" -> 11
+ ";" -> 12
+ "<" -> 13
+ "=" -> 14
+ ">" -> 15
+ "@" -> 16
+ "Glue" -> 17
+ "Id" -> 18
+ "PathP" -> 19
+ "U" -> 20
+ "[" -> 21
+ "\\" -> 22
+ "\\/" -> 23
+ "]" -> 24
+ "comp" -> 25
+ "data" -> 26
+ "fill" -> 27
+ "glue" -> 28
+ "hComp" -> 29
+ "hdata" -> 30
+ "idC" -> 31
+ "idJ" -> 32
+ "import" -> 33
+ "in" -> 34
+ "let" -> 35
+ "module" -> 36
+ "mutual" -> 37
+ "opaque" -> 38
+ "split" -> 39
+ "split@" -> 40
+ "transparent" -> 41
+ "transparent_all" -> 42
+ "transport" -> 43
+ "undefined" -> 44
+ "unglue" -> 45
+ "where" -> 46
+ "with" -> 47
+ "{" -> 48
+ "|" -> 49
+ "}" -> 50
+ _ -> error $ "not a reserved word: " ++ show s
+
+-- | Get the position of a token.
+position :: Token -> Position
+position t = case t of
+ PT p _ -> p
+ Err p -> p
+
+-- | Get the line number of a token.
+line :: Token -> Int
+line t = case position t of Pn _ l _ -> l
+
+-- | Get the column number of a token.
+column :: Token -> Int
+column t = case position t of Pn _ _ c -> c
+
+-- | Check if a token is one of the given symbols.
+isTokenIn :: [String] -> Token -> Bool
+isTokenIn ts t = case t of
+ PT _ (TS r _) | r `elem` ts -> True
+ _ -> False
+
+-- | Check if a word is a layout start token.
+isLayout :: Token -> Bool
+isLayout = isTokenIn layoutWords
+
+-- | Check if a token is a layout stop token.
+isStop :: Token -> Bool
+isStop = isTokenIn layoutStopWords
+
+-- | Check if a token is the layout open token.
+isLayoutOpen :: Token -> Bool
+isLayoutOpen = isTokenIn [layoutOpen]
+
+-- | Check if a token is the layout close token.
+isLayoutClose :: Token -> Bool
+isLayoutClose = isTokenIn [layoutClose]
+
+-- | Get the number of characters in the token.
+tokenLength :: Token -> Int
+tokenLength t = length $ prToken t
+
--- /dev/null
+-- -*- haskell -*-
+-- This Alex file was machine-generated by the BNF converter
+{
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -w #-}
+module Exp.Lex where
+
+
+
+import qualified Data.Bits
+import Data.Word (Word8)
+import Data.Char (ord)
+}
+
+
+$c = [A-Z\192-\221] # [\215] -- capital isolatin1 letter (215 = \times) FIXME
+$s = [a-z\222-\255] # [\247] -- small isolatin1 letter (247 = \div ) FIXME
+$l = [$c $s] -- letter
+$d = [0-9] -- digit
+$i = [$l $d _ '] -- identifier character
+$u = [. \n] -- universal: any character
+
+@rsyms = -- symbols and non-identifier-like reserved words
+ \{ | \} | \; | \: | \= | \\ | \- \> | \< | \> | "split" \@ | \* | \@ | \. "1" | \. "2" | \( | \, | \) | "0" | "1" | \[ | \] | \\ \/ | \- | \|
+
+:-
+"--" [.]* ; -- Toss single line comments
+"{-" ([$u # \-] | \-+ [$u # [\- \}]])* ("-")+ "}" ;
+
+$white+ ;
+@rsyms
+ { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }
+\_ | $l ($l | $d | \' | \_)* | \! $d *
+ { tok (\p s -> PT p (eitherResIdent (T_AIdent . share) s)) }
+\/ \\
+ { tok (\p s -> PT p (eitherResIdent (T_CIdent . share) s)) }
+\?
+ { tok (\p s -> PT p (eitherResIdent (T_HoleIdent . share) s)) }
+
+$l $i*
+ { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }
+
+
+
+
+
+{
+
+tok :: (Posn -> String -> Token) -> (Posn -> String -> Token)
+tok f p s = f p s
+
+share :: String -> String
+share = id
+
+data Tok =
+ TS !String !Int -- reserved words and symbols
+ | TL !String -- string literals
+ | TI !String -- integer literals
+ | TV !String -- identifiers
+ | TD !String -- double precision float literals
+ | TC !String -- character literals
+ | T_AIdent !String
+ | T_CIdent !String
+ | T_HoleIdent !String
+
+ deriving (Eq,Show,Ord)
+
+data Token =
+ PT Posn Tok
+ | Err Posn
+ deriving (Eq,Show,Ord)
+
+printPosn :: Posn -> String
+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
+
+tokenPos :: [Token] -> String
+tokenPos (t:_) = printPosn (tokenPosn t)
+tokenPos [] = "end of file"
+
+tokenPosn :: Token -> Posn
+tokenPosn (PT p _) = p
+tokenPosn (Err p) = p
+
+tokenLineCol :: Token -> (Int, Int)
+tokenLineCol = posLineCol . tokenPosn
+
+posLineCol :: Posn -> (Int, Int)
+posLineCol (Pn _ l c) = (l,c)
+
+mkPosToken :: Token -> ((Int, Int), String)
+mkPosToken t@(PT p _) = (posLineCol p, prToken t)
+
+prToken :: Token -> String
+prToken t = case t of
+ PT _ (TS s _) -> s
+ PT _ (TL s) -> show s
+ PT _ (TI s) -> s
+ PT _ (TV s) -> s
+ PT _ (TD s) -> s
+ PT _ (TC s) -> s
+ Err _ -> "#error"
+ PT _ (T_AIdent s) -> s
+ PT _ (T_CIdent s) -> s
+ PT _ (T_HoleIdent s) -> s
+
+
+data BTree = N | B String Tok BTree BTree deriving (Show)
+
+eitherResIdent :: (String -> Tok) -> String -> Tok
+eitherResIdent tv s = treeFind resWords
+ where
+ treeFind N = tv s
+ treeFind (B a t left right) | s < a = treeFind left
+ | s > a = treeFind right
+ | s == a = t
+
+resWords :: BTree
+resWords = b "data" 26 (b "<" 13 (b ".1" 7 (b "," 4 (b ")" 2 (b "(" 1 N N) (b "*" 3 N N)) (b "->" 6 (b "-" 5 N N) N)) (b "1" 10 (b "0" 9 (b ".2" 8 N N) N) (b ";" 12 (b ":" 11 N N) N))) (b "U" 20 (b "Glue" 17 (b ">" 15 (b "=" 14 N N) (b "@" 16 N N)) (b "PathP" 19 (b "Id" 18 N N) N)) (b "\\/" 23 (b "\\" 22 (b "[" 21 N N) N) (b "comp" 25 (b "]" 24 N N) N)))) (b "split" 39 (b "import" 33 (b "hdata" 30 (b "glue" 28 (b "fill" 27 N N) (b "hComp" 29 N N)) (b "idJ" 32 (b "idC" 31 N N) N)) (b "module" 36 (b "let" 35 (b "in" 34 N N) N) (b "opaque" 38 (b "mutual" 37 N N) N))) (b "unglue" 45 (b "transparent_all" 42 (b "transparent" 41 (b "split@" 40 N N) N) (b "undefined" 44 (b "transport" 43 N N) N)) (b "{" 48 (b "with" 47 (b "where" 46 N N) N) (b "}" 50 (b "|" 49 N N) N))))
+ where b s n = let bs = id s
+ in B bs (TS bs n)
+
+unescapeInitTail :: String -> String
+unescapeInitTail = id . unesc . tail . id where
+ unesc s = case s of
+ '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
+ '\\':'n':cs -> '\n' : unesc cs
+ '\\':'t':cs -> '\t' : unesc cs
+ '\\':'r':cs -> '\r' : unesc cs
+ '\\':'f':cs -> '\f' : unesc cs
+ '"':[] -> []
+ c:cs -> c : unesc cs
+ _ -> []
+
+-------------------------------------------------------------------
+-- Alex wrapper code.
+-- A modified "posn" wrapper.
+-------------------------------------------------------------------
+
+data Posn = Pn !Int !Int !Int
+ deriving (Eq, Show,Ord)
+
+alexStartPos :: Posn
+alexStartPos = Pn 0 1 1
+
+alexMove :: Posn -> Char -> Posn
+alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1)
+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1
+alexMove (Pn a l c) _ = Pn (a+1) l (c+1)
+
+type Byte = Word8
+
+type AlexInput = (Posn, -- current position,
+ Char, -- previous char
+ [Byte], -- pending bytes on the current char
+ String) -- current input string
+
+tokens :: String -> [Token]
+tokens str = go (alexStartPos, '\n', [], str)
+ where
+ go :: AlexInput -> [Token]
+ go inp@(pos, _, _, str) =
+ case alexScan inp 0 of
+ AlexEOF -> []
+ AlexError (pos, _, _, _) -> [Err pos]
+ AlexSkip inp' len -> go inp'
+ AlexToken inp' len act -> act pos (take len str) : (go inp')
+
+alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
+alexGetByte (p, _, [], s) =
+ case s of
+ [] -> Nothing
+ (c:s) ->
+ let p' = alexMove p c
+ (b:bs) = utf8Encode c
+ in p' `seq` Just (b, (p', c, bs, s))
+
+alexInputPrevChar :: AlexInput -> Char
+alexInputPrevChar (p, c, bs, s) = c
+
+-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
+utf8Encode :: Char -> [Word8]
+utf8Encode = map fromIntegral . go . ord
+ where
+ go oc
+ | oc <= 0x7f = [oc]
+
+ | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
+ , 0x80 + oc Data.Bits..&. 0x3f
+ ]
+
+ | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
+ , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+ , 0x80 + oc Data.Bits..&. 0x3f
+ ]
+ | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
+ , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
+ , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+ , 0x80 + oc Data.Bits..&. 0x3f
+ ]
+}
--- /dev/null
+-- -*- haskell -*-
+-- This Alex file was machine-generated by the BNF converter
+{
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -w #-}
+module Exp.Lex where
+
+import qualified Data.Bits
+import Data.Word (Word8)
+import Data.Char (ord)
+}
+
+
+$c = [A-Z\192-\221] # [\215] -- capital isolatin1 letter (215 = \times) FIXME
+$s = [a-z\222-\255] # [\247] -- small isolatin1 letter (247 = \div ) FIXME
+$l = [$c $s] -- letter
+$d = [0-9] -- digit
+$i = [$l $d _ '] -- identifier character
+$u = [. \n] -- universal: any character
+
+@rsyms = -- symbols and non-identifier-like reserved words
+ \{ | \} | \; | \: | \= | \\ | \- \> | \< | \> | "split" \@ | \* | \@ | \. "1" | \. "2" | \( | \, | \) | "0" | "1" | \[ | \] | \\ \/ | \- | \|
+
+:-
+
+-- Line comments
+"--" [.]* ;
+
+-- Block comments
+"{-" [$u # \-]* \- ([$u # [\- \}]] [$u # \-]* \- | \-)* \} ;
+
+$white+ ;
+@rsyms
+ { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }
+\_ | $l ([\' \_]| ($d | $l)) * | \! $d *
+ { tok (\p s -> PT p (eitherResIdent (T_AIdent . share) s)) }
+"/\\"
+ { tok (\p s -> PT p (eitherResIdent (T_CIdent . share) s)) }
+\?
+ { tok (\p s -> PT p (eitherResIdent (T_HoleIdent . share) s)) }
+
+$l $i*
+ { tok (\p s -> PT p (eitherResIdent (TV . share) s)) }
+
+
+
+
+
+{
+
+tok :: (Posn -> String -> Token) -> (Posn -> String -> Token)
+tok f p s = f p s
+
+share :: String -> String
+share = id
+
+data Tok =
+ TS !String !Int -- reserved words and symbols
+ | TL !String -- string literals
+ | TI !String -- integer literals
+ | TV !String -- identifiers
+ | TD !String -- double precision float literals
+ | TC !String -- character literals
+ | T_AIdent !String
+ | T_CIdent !String
+ | T_HoleIdent !String
+
+ deriving (Eq,Show,Ord)
+
+data Token =
+ PT Posn Tok
+ | Err Posn
+ deriving (Eq,Show,Ord)
+
+printPosn :: Posn -> String
+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
+
+tokenPos :: [Token] -> String
+tokenPos (t:_) = printPosn (tokenPosn t)
+tokenPos [] = "end of file"
+
+tokenPosn :: Token -> Posn
+tokenPosn (PT p _) = p
+tokenPosn (Err p) = p
+
+tokenLineCol :: Token -> (Int, Int)
+tokenLineCol = posLineCol . tokenPosn
+
+posLineCol :: Posn -> (Int, Int)
+posLineCol (Pn _ l c) = (l,c)
+
+mkPosToken :: Token -> ((Int, Int), String)
+mkPosToken t@(PT p _) = (posLineCol p, prToken t)
+
+prToken :: Token -> String
+prToken t = case t of
+ PT _ (TS s _) -> s
+ PT _ (TL s) -> show s
+ PT _ (TI s) -> s
+ PT _ (TV s) -> s
+ PT _ (TD s) -> s
+ PT _ (TC s) -> s
+ Err _ -> "#error"
+ PT _ (T_AIdent s) -> s
+ PT _ (T_CIdent s) -> s
+ PT _ (T_HoleIdent s) -> s
+
+
+data BTree = N | B String Tok BTree BTree deriving (Show)
+
+eitherResIdent :: (String -> Tok) -> String -> Tok
+eitherResIdent tv s = treeFind resWords
+ where
+ treeFind N = tv s
+ treeFind (B a t left right) | s < a = treeFind left
+ | s > a = treeFind right
+ | s == a = t
+
+resWords :: BTree
+resWords = b "data" 26 (b "<" 13 (b ".1" 7 (b "," 4 (b ")" 2 (b "(" 1 N N) (b "*" 3 N N)) (b "->" 6 (b "-" 5 N N) N)) (b "1" 10 (b "0" 9 (b ".2" 8 N N) N) (b ";" 12 (b ":" 11 N N) N))) (b "U" 20 (b "Glue" 17 (b ">" 15 (b "=" 14 N N) (b "@" 16 N N)) (b "PathP" 19 (b "Id" 18 N N) N)) (b "\\/" 23 (b "\\" 22 (b "[" 21 N N) N) (b "comp" 25 (b "]" 24 N N) N)))) (b "split" 39 (b "import" 33 (b "hdata" 30 (b "glue" 28 (b "fill" 27 N N) (b "hComp" 29 N N)) (b "idJ" 32 (b "idC" 31 N N) N)) (b "module" 36 (b "let" 35 (b "in" 34 N N) N) (b "opaque" 38 (b "mutual" 37 N N) N))) (b "unglue" 45 (b "transparent_all" 42 (b "transparent" 41 (b "split@" 40 N N) N) (b "undefined" 44 (b "transport" 43 N N) N)) (b "{" 48 (b "with" 47 (b "where" 46 N N) N) (b "}" 50 (b "|" 49 N N) N))))
+ where b s n = let bs = s
+ in B bs (TS bs n)
+
+unescapeInitTail :: String -> String
+unescapeInitTail = id . unesc . tail . id
+ where
+ unesc s = case s of
+ '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
+ '\\':'n':cs -> '\n' : unesc cs
+ '\\':'t':cs -> '\t' : unesc cs
+ '\\':'r':cs -> '\r' : unesc cs
+ '\\':'f':cs -> '\f' : unesc cs
+ '"':[] -> []
+ c:cs -> c : unesc cs
+ _ -> []
+
+-------------------------------------------------------------------
+-- Alex wrapper code.
+-- A modified "posn" wrapper.
+-------------------------------------------------------------------
+
+data Posn = Pn !Int !Int !Int
+ deriving (Eq, Show,Ord)
+
+alexStartPos :: Posn
+alexStartPos = Pn 0 1 1
+
+alexMove :: Posn -> Char -> Posn
+alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1)
+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1
+alexMove (Pn a l c) _ = Pn (a+1) l (c+1)
+
+type Byte = Word8
+
+type AlexInput = (Posn, -- current position,
+ Char, -- previous char
+ [Byte], -- pending bytes on the current char
+ String) -- current input string
+
+tokens :: String -> [Token]
+tokens str = go (alexStartPos, '\n', [], str)
+ where
+ go :: AlexInput -> [Token]
+ go inp@(pos, _, _, str) =
+ case alexScan inp 0 of
+ AlexEOF -> []
+ AlexError (pos, _, _, _) -> [Err pos]
+ AlexSkip inp' len -> go inp'
+ AlexToken inp' len act -> act pos (take len str) : (go inp')
+
+alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
+alexGetByte (p, _, [], s) =
+ case s of
+ [] -> Nothing
+ (c:s) ->
+ let p' = alexMove p c
+ (b:bs) = utf8Encode c
+ in p' `seq` Just (b, (p', c, bs, s))
+
+alexInputPrevChar :: AlexInput -> Char
+alexInputPrevChar (p, c, bs, s) = c
+
+-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
+utf8Encode :: Char -> [Word8]
+utf8Encode = map fromIntegral . go . ord
+ where
+ go oc
+ | oc <= 0x7f = [oc]
+
+ | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
+ , 0x80 + oc Data.Bits..&. 0x3f
+ ]
+
+ | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
+ , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+ , 0x80 + oc Data.Bits..&. 0x3f
+ ]
+ | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
+ , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
+ , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+ , 0x80 + oc Data.Bits..&. 0x3f
+ ]
+}
--- /dev/null
+-- This Happy file was machine-generated by the BNF converter
+{
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+module Exp.Par where
+import Exp.Abs
+import Exp.Lex
+import Exp.ErrM
+
+}
+
+%name pModule Module
+%name pExp Exp
+-- no lexer declaration
+%monad { Err } { thenM } { returnM }
+%tokentype {Token}
+%token
+ '(' { PT _ (TS _ 1) }
+ ')' { PT _ (TS _ 2) }
+ '*' { PT _ (TS _ 3) }
+ ',' { PT _ (TS _ 4) }
+ '-' { PT _ (TS _ 5) }
+ '->' { PT _ (TS _ 6) }
+ '.1' { PT _ (TS _ 7) }
+ '.2' { PT _ (TS _ 8) }
+ '0' { PT _ (TS _ 9) }
+ '1' { PT _ (TS _ 10) }
+ ':' { PT _ (TS _ 11) }
+ ';' { PT _ (TS _ 12) }
+ '<' { PT _ (TS _ 13) }
+ '=' { PT _ (TS _ 14) }
+ '>' { PT _ (TS _ 15) }
+ '@' { PT _ (TS _ 16) }
+ 'Glue' { PT _ (TS _ 17) }
+ 'Id' { PT _ (TS _ 18) }
+ 'PathP' { PT _ (TS _ 19) }
+ 'U' { PT _ (TS _ 20) }
+ '[' { PT _ (TS _ 21) }
+ '\\' { PT _ (TS _ 22) }
+ '\\/' { PT _ (TS _ 23) }
+ ']' { PT _ (TS _ 24) }
+ 'comp' { PT _ (TS _ 25) }
+ 'data' { PT _ (TS _ 26) }
+ 'fill' { PT _ (TS _ 27) }
+ 'glue' { PT _ (TS _ 28) }
+ 'hComp' { PT _ (TS _ 29) }
+ 'hdata' { PT _ (TS _ 30) }
+ 'idC' { PT _ (TS _ 31) }
+ 'idJ' { PT _ (TS _ 32) }
+ 'import' { PT _ (TS _ 33) }
+ 'in' { PT _ (TS _ 34) }
+ 'let' { PT _ (TS _ 35) }
+ 'module' { PT _ (TS _ 36) }
+ 'mutual' { PT _ (TS _ 37) }
+ 'opaque' { PT _ (TS _ 38) }
+ 'split' { PT _ (TS _ 39) }
+ 'split@' { PT _ (TS _ 40) }
+ 'transparent' { PT _ (TS _ 41) }
+ 'transparent_all' { PT _ (TS _ 42) }
+ 'transport' { PT _ (TS _ 43) }
+ 'undefined' { PT _ (TS _ 44) }
+ 'unglue' { PT _ (TS _ 45) }
+ 'where' { PT _ (TS _ 46) }
+ 'with' { PT _ (TS _ 47) }
+ '{' { PT _ (TS _ 48) }
+ '|' { PT _ (TS _ 49) }
+ '}' { PT _ (TS _ 50) }
+ L_AIdent { PT _ (T_AIdent _) }
+ L_CIdent { PT _ (T_CIdent $$) }
+ L_HoleIdent { PT _ (T_HoleIdent _) }
+
+%%
+
+AIdent :: { AIdent}
+AIdent : L_AIdent { AIdent (mkPosToken $1)}
+
+CIdent :: { CIdent}
+CIdent : L_CIdent { CIdent ($1)}
+
+HoleIdent :: { HoleIdent}
+HoleIdent : L_HoleIdent { HoleIdent (mkPosToken $1)}
+
+Module :: { Module }
+Module : 'module' AIdent 'where' '{' ListImp ListDecl '}' { Exp.Abs.Module $2 $5 $6 }
+Imp :: { Imp }
+Imp : 'import' AIdent { Exp.Abs.Import $2 }
+ListImp :: { [Imp] }
+ListImp : {- empty -} { [] }
+ | Imp { (:[]) $1 }
+ | Imp ';' ListImp { (:) $1 $3 }
+Decl :: { Decl }
+Decl : AIdent ListTele ':' Exp '=' ExpWhere { Exp.Abs.DeclDef $1 (reverse $2) $4 $6 }
+ | 'data' AIdent ListTele '=' ListLabel { Exp.Abs.DeclData $2 (reverse $3) $5 }
+ | 'hdata' AIdent ListTele '=' ListLabel { Exp.Abs.DeclHData $2 (reverse $3) $5 }
+ | AIdent ListTele ':' Exp '=' 'split' '{' ListBranch '}' { Exp.Abs.DeclSplit $1 (reverse $2) $4 $8 }
+ | AIdent ListTele ':' Exp '=' 'undefined' { Exp.Abs.DeclUndef $1 (reverse $2) $4 }
+ | 'mutual' '{' ListDecl '}' { Exp.Abs.DeclMutual $3 }
+ | 'opaque' AIdent { Exp.Abs.DeclOpaque $2 }
+ | 'transparent' AIdent { Exp.Abs.DeclTransparent $2 }
+ | 'transparent_all' { Exp.Abs.DeclTransparentAll }
+ListDecl :: { [Decl] }
+ListDecl : {- empty -} { [] }
+ | Decl { (:[]) $1 }
+ | Decl ';' ListDecl { (:) $1 $3 }
+ExpWhere :: { ExpWhere }
+ExpWhere : Exp 'where' '{' ListDecl '}' { Exp.Abs.Where $1 $4 }
+ | Exp { Exp.Abs.NoWhere $1 }
+Exp :: { Exp }
+Exp : 'let' '{' ListDecl '}' 'in' Exp { Exp.Abs.Let $3 $6 }
+ | '\\' ListPTele '->' Exp { Exp.Abs.Lam $2 $4 }
+ | '<' ListAIdent '>' Exp { Exp.Abs.PLam $2 $4 }
+ | 'split@' Exp 'with' '{' ListBranch '}' { Exp.Abs.Split $2 $5 }
+ | Exp1 { $1 }
+Exp1 :: { Exp }
+Exp1 : Exp2 '->' Exp1 { Exp.Abs.Fun $1 $3 }
+ | ListPTele '->' Exp1 { Exp.Abs.Pi $1 $3 }
+ | ListPTele '*' Exp1 { Exp.Abs.Sigma $1 $3 }
+ | Exp2 { $1 }
+Exp2 :: { Exp }
+Exp2 : Exp2 '@' Formula { Exp.Abs.AppFormula $1 $3 }
+ | Exp2 Exp3 { Exp.Abs.App $1 $2 }
+ | Exp3 { $1 }
+Exp3 :: { Exp }
+Exp3 : 'PathP' Exp4 Exp4 Exp4 { Exp.Abs.PathP $2 $3 $4 }
+ | 'comp' Exp4 Exp4 System { Exp.Abs.Comp $2 $3 $4 }
+ | 'hComp' Exp4 Exp4 System { Exp.Abs.HComp $2 $3 $4 }
+ | 'transport' Exp4 Exp4 { Exp.Abs.Trans $2 $3 }
+ | 'fill' Exp4 Exp4 System { Exp.Abs.Fill $2 $3 $4 }
+ | 'Glue' Exp4 System { Exp.Abs.Glue $2 $3 }
+ | 'glue' Exp4 System { Exp.Abs.GlueElem $2 $3 }
+ | 'unglue' Exp4 System { Exp.Abs.UnGlueElem $2 $3 }
+ | 'Id' Exp4 Exp4 Exp3 { Exp.Abs.Id $2 $3 $4 }
+ | 'idC' Exp4 System { Exp.Abs.IdPair $2 $3 }
+ | 'idJ' Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 { Exp.Abs.IdJ $2 $3 $4 $5 $6 $7 }
+ | Exp4 { $1 }
+Exp4 :: { Exp }
+Exp4 : Exp4 '.1' { Exp.Abs.Fst $1 }
+ | Exp4 '.2' { Exp.Abs.Snd $1 }
+ | Exp5 { $1 }
+Exp5 :: { Exp }
+Exp5 : '(' Exp ',' ListExp ')' { Exp.Abs.Pair $2 $4 }
+ | AIdent { Exp.Abs.Var $1 }
+ | AIdent '{' Exp '}' { Exp.Abs.PCon $1 $3 }
+ | 'U' { Exp.Abs.U }
+ | HoleIdent { Exp.Abs.Hole $1 }
+ | '(' Exp ')' { $2 }
+ListExp :: { [Exp] }
+ListExp : Exp { (:[]) $1 } | Exp ',' ListExp { (:) $1 $3 }
+Dir :: { Dir }
+Dir : '0' { Exp.Abs.Dir0 } | '1' { Exp.Abs.Dir1 }
+System :: { System }
+System : '[' ListSide ']' { Exp.Abs.System $2 }
+Face :: { Face }
+Face : '(' AIdent '=' Dir ')' { Exp.Abs.Face $2 $4 }
+ListFace :: { [Face] }
+ListFace : {- empty -} { [] } | ListFace Face { flip (:) $1 $2 }
+Side :: { Side }
+Side : ListFace '->' Exp { Exp.Abs.Side (reverse $1) $3 }
+ListSide :: { [Side] }
+ListSide : {- empty -} { [] }
+ | Side { (:[]) $1 }
+ | Side ',' ListSide { (:) $1 $3 }
+Formula :: { Formula }
+Formula : Formula '\\/' Formula1 { Exp.Abs.Disj $1 $3 }
+ | Formula1 { $1 }
+Formula1 :: { Formula }
+Formula1 : Formula1 CIdent Formula2 { Exp.Abs.Conj $1 $2 $3 }
+ | Formula2 { $1 }
+Formula2 :: { Formula }
+Formula2 : '-' Formula2 { Exp.Abs.Neg $2 }
+ | AIdent { Exp.Abs.Atom $1 }
+ | Dir { Exp.Abs.Dir $1 }
+ | '(' Formula ')' { $2 }
+Branch :: { Branch }
+Branch : AIdent ListAIdent '->' ExpWhere { Exp.Abs.OBranch $1 $2 $4 }
+ | AIdent ListAIdent '@' ListAIdent '->' ExpWhere { Exp.Abs.PBranch $1 $2 $4 $6 }
+ListBranch :: { [Branch] }
+ListBranch : {- empty -} { [] }
+ | Branch { (:[]) $1 }
+ | Branch ';' ListBranch { (:) $1 $3 }
+Label :: { Label }
+Label : AIdent ListTele { Exp.Abs.OLabel $1 (reverse $2) }
+ | AIdent ListTele '<' ListAIdent '>' System { Exp.Abs.PLabel $1 (reverse $2) $4 $6 }
+ListLabel :: { [Label] }
+ListLabel : {- empty -} { [] }
+ | Label { (:[]) $1 }
+ | Label '|' ListLabel { (:) $1 $3 }
+Tele :: { Tele }
+Tele : '(' AIdent ListAIdent ':' Exp ')' { Exp.Abs.Tele $2 $3 $5 }
+ListTele :: { [Tele] }
+ListTele : {- empty -} { [] } | ListTele Tele { flip (:) $1 $2 }
+PTele :: { PTele }
+PTele : '(' Exp ':' Exp ')' { Exp.Abs.PTele $2 $4 }
+ListPTele :: { [PTele] }
+ListPTele : PTele { (:[]) $1 } | PTele ListPTele { (:) $1 $2 }
+ListAIdent :: { [AIdent] }
+ListAIdent : {- empty -} { [] } | AIdent ListAIdent { (:) $1 $2 }
+{
+
+returnM :: a -> Err a
+returnM = return
+
+thenM :: Err a -> (a -> Err b) -> Err b
+thenM = (>>=)
+
+happyError :: [Token] -> Err a
+happyError ts =
+ Bad $ "syntax error at " ++ tokenPos ts ++
+ case ts of
+ [] -> []
+ [Err _] -> " due to lexer error"
+ t:_ -> " before `" ++ id(prToken t) ++ "'"
+
+myLexer = tokens
+}
+
--- /dev/null
+-- This Happy file was machine-generated by the BNF converter
+{
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+module Exp.Par where
+import qualified Exp.Abs
+import Exp.Lex
+}
+
+%name pModule Module
+%name pExp Exp
+-- no lexer declaration
+%monad { Either String } { (>>=) } { return }
+%tokentype {Token}
+%token
+ '(' { PT _ (TS _ 1) }
+ ')' { PT _ (TS _ 2) }
+ '*' { PT _ (TS _ 3) }
+ ',' { PT _ (TS _ 4) }
+ '-' { PT _ (TS _ 5) }
+ '->' { PT _ (TS _ 6) }
+ '.1' { PT _ (TS _ 7) }
+ '.2' { PT _ (TS _ 8) }
+ '0' { PT _ (TS _ 9) }
+ '1' { PT _ (TS _ 10) }
+ ':' { PT _ (TS _ 11) }
+ ';' { PT _ (TS _ 12) }
+ '<' { PT _ (TS _ 13) }
+ '=' { PT _ (TS _ 14) }
+ '>' { PT _ (TS _ 15) }
+ '@' { PT _ (TS _ 16) }
+ 'Glue' { PT _ (TS _ 17) }
+ 'Id' { PT _ (TS _ 18) }
+ 'PathP' { PT _ (TS _ 19) }
+ 'U' { PT _ (TS _ 20) }
+ '[' { PT _ (TS _ 21) }
+ '\\' { PT _ (TS _ 22) }
+ '\\/' { PT _ (TS _ 23) }
+ ']' { PT _ (TS _ 24) }
+ 'comp' { PT _ (TS _ 25) }
+ 'data' { PT _ (TS _ 26) }
+ 'fill' { PT _ (TS _ 27) }
+ 'glue' { PT _ (TS _ 28) }
+ 'hComp' { PT _ (TS _ 29) }
+ 'hdata' { PT _ (TS _ 30) }
+ 'idC' { PT _ (TS _ 31) }
+ 'idJ' { PT _ (TS _ 32) }
+ 'import' { PT _ (TS _ 33) }
+ 'in' { PT _ (TS _ 34) }
+ 'let' { PT _ (TS _ 35) }
+ 'module' { PT _ (TS _ 36) }
+ 'mutual' { PT _ (TS _ 37) }
+ 'opaque' { PT _ (TS _ 38) }
+ 'split' { PT _ (TS _ 39) }
+ 'split@' { PT _ (TS _ 40) }
+ 'transparent' { PT _ (TS _ 41) }
+ 'transparent_all' { PT _ (TS _ 42) }
+ 'transport' { PT _ (TS _ 43) }
+ 'undefined' { PT _ (TS _ 44) }
+ 'unglue' { PT _ (TS _ 45) }
+ 'where' { PT _ (TS _ 46) }
+ 'with' { PT _ (TS _ 47) }
+ '{' { PT _ (TS _ 48) }
+ '|' { PT _ (TS _ 49) }
+ '}' { PT _ (TS _ 50) }
+ L_AIdent { PT _ (T_AIdent _) }
+ L_CIdent { PT _ (T_CIdent $$) }
+ L_HoleIdent { PT _ (T_HoleIdent _) }
+
+%%
+
+AIdent :: { Exp.Abs.AIdent}
+AIdent : L_AIdent { Exp.Abs.AIdent (mkPosToken $1) }
+
+CIdent :: { Exp.Abs.CIdent}
+CIdent : L_CIdent { Exp.Abs.CIdent $1 }
+
+HoleIdent :: { Exp.Abs.HoleIdent}
+HoleIdent : L_HoleIdent { Exp.Abs.HoleIdent (mkPosToken $1) }
+
+Module :: { Exp.Abs.Module }
+Module : 'module' AIdent 'where' '{' ListImp ListDecl '}' { Exp.Abs.Module $2 $5 $6 }
+
+Imp :: { Exp.Abs.Imp }
+Imp : 'import' AIdent { Exp.Abs.Import $2 }
+
+ListImp :: { [Exp.Abs.Imp] }
+ListImp : {- empty -} { [] }
+ | Imp { (:[]) $1 }
+ | Imp ';' ListImp { (:) $1 $3 }
+
+Decl :: { Exp.Abs.Decl }
+Decl : AIdent ListTele ':' Exp '=' ExpWhere { Exp.Abs.DeclDef $1 $2 $4 $6 }
+ | 'data' AIdent ListTele '=' ListLabel { Exp.Abs.DeclData $2 $3 $5 }
+ | 'hdata' AIdent ListTele '=' ListLabel { Exp.Abs.DeclHData $2 $3 $5 }
+ | AIdent ListTele ':' Exp '=' 'split' '{' ListBranch '}' { Exp.Abs.DeclSplit $1 $2 $4 $8 }
+ | AIdent ListTele ':' Exp '=' 'undefined' { Exp.Abs.DeclUndef $1 $2 $4 }
+ | 'mutual' '{' ListDecl '}' { Exp.Abs.DeclMutual $3 }
+ | 'opaque' AIdent { Exp.Abs.DeclOpaque $2 }
+ | 'transparent' AIdent { Exp.Abs.DeclTransparent $2 }
+ | 'transparent_all' { Exp.Abs.DeclTransparentAll }
+
+ListDecl :: { [Exp.Abs.Decl] }
+ListDecl : {- empty -} { [] }
+ | Decl { (:[]) $1 }
+ | Decl ';' ListDecl { (:) $1 $3 }
+
+ExpWhere :: { Exp.Abs.ExpWhere }
+ExpWhere : Exp 'where' '{' ListDecl '}' { Exp.Abs.Where $1 $4 }
+ | Exp { Exp.Abs.NoWhere $1 }
+
+Exp :: { Exp.Abs.Exp }
+Exp : 'let' '{' ListDecl '}' 'in' Exp { Exp.Abs.Let $3 $6 }
+ | '\\' ListPTele '->' Exp { Exp.Abs.Lam $2 $4 }
+ | '<' ListAIdent '>' Exp { Exp.Abs.PLam $2 $4 }
+ | 'split@' Exp 'with' '{' ListBranch '}' { Exp.Abs.Split $2 $5 }
+ | Exp1 { $1 }
+
+Exp1 :: { Exp.Abs.Exp }
+Exp1 : Exp2 '->' Exp1 { Exp.Abs.Fun $1 $3 }
+ | ListPTele '->' Exp1 { Exp.Abs.Pi $1 $3 }
+ | ListPTele '*' Exp1 { Exp.Abs.Sigma $1 $3 }
+ | Exp2 { $1 }
+
+Exp2 :: { Exp.Abs.Exp }
+Exp2 : Exp2 '@' Formula { Exp.Abs.AppFormula $1 $3 }
+ | Exp2 Exp3 { Exp.Abs.App $1 $2 }
+ | Exp3 { $1 }
+
+Exp3 :: { Exp.Abs.Exp }
+Exp3 : 'PathP' Exp4 Exp4 Exp4 { Exp.Abs.PathP $2 $3 $4 }
+ | 'comp' Exp4 Exp4 System { Exp.Abs.Comp $2 $3 $4 }
+ | 'hComp' Exp4 Exp4 System { Exp.Abs.HComp $2 $3 $4 }
+ | 'transport' Exp4 Exp4 { Exp.Abs.Trans $2 $3 }
+ | 'fill' Exp4 Exp4 System { Exp.Abs.Fill $2 $3 $4 }
+ | 'Glue' Exp4 System { Exp.Abs.Glue $2 $3 }
+ | 'glue' Exp4 System { Exp.Abs.GlueElem $2 $3 }
+ | 'unglue' Exp4 System { Exp.Abs.UnGlueElem $2 $3 }
+ | 'Id' Exp4 Exp4 Exp3 { Exp.Abs.Id $2 $3 $4 }
+ | 'idC' Exp4 System { Exp.Abs.IdPair $2 $3 }
+ | 'idJ' Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 { Exp.Abs.IdJ $2 $3 $4 $5 $6 $7 }
+ | Exp4 { $1 }
+
+Exp4 :: { Exp.Abs.Exp }
+Exp4 : Exp4 '.1' { Exp.Abs.Fst $1 }
+ | Exp4 '.2' { Exp.Abs.Snd $1 }
+ | Exp5 { $1 }
+
+Exp5 :: { Exp.Abs.Exp }
+Exp5 : '(' Exp ',' ListExp ')' { Exp.Abs.Pair $2 $4 }
+ | AIdent { Exp.Abs.Var $1 }
+ | AIdent '{' Exp '}' { Exp.Abs.PCon $1 $3 }
+ | 'U' { Exp.Abs.U }
+ | HoleIdent { Exp.Abs.Hole $1 }
+ | '(' Exp ')' { $2 }
+
+ListExp :: { [Exp.Abs.Exp] }
+ListExp : Exp { (:[]) $1 } | Exp ',' ListExp { (:) $1 $3 }
+
+Dir :: { Exp.Abs.Dir }
+Dir : '0' { Exp.Abs.Dir0 } | '1' { Exp.Abs.Dir1 }
+
+System :: { Exp.Abs.System }
+System : '[' ListSide ']' { Exp.Abs.System $2 }
+
+Face :: { Exp.Abs.Face }
+Face : '(' AIdent '=' Dir ')' { Exp.Abs.Face $2 $4 }
+
+ListFace :: { [Exp.Abs.Face] }
+ListFace : {- empty -} { [] } | Face ListFace { (:) $1 $2 }
+
+Side :: { Exp.Abs.Side }
+Side : ListFace '->' Exp { Exp.Abs.Side $1 $3 }
+
+ListSide :: { [Exp.Abs.Side] }
+ListSide : {- empty -} { [] }
+ | Side { (:[]) $1 }
+ | Side ',' ListSide { (:) $1 $3 }
+
+Formula :: { Exp.Abs.Formula }
+Formula : Formula '\\/' Formula1 { Exp.Abs.Disj $1 $3 }
+ | Formula1 { $1 }
+
+Formula1 :: { Exp.Abs.Formula }
+Formula1 : Formula1 CIdent Formula2 { Exp.Abs.Conj $1 $2 $3 }
+ | Formula2 { $1 }
+
+Formula2 :: { Exp.Abs.Formula }
+Formula2 : '-' Formula2 { Exp.Abs.Neg $2 }
+ | AIdent { Exp.Abs.Atom $1 }
+ | Dir { Exp.Abs.Dir $1 }
+ | '(' Formula ')' { $2 }
+
+Branch :: { Exp.Abs.Branch }
+Branch : AIdent ListAIdent '->' ExpWhere { Exp.Abs.OBranch $1 $2 $4 }
+ | AIdent ListAIdent '@' ListAIdent '->' ExpWhere { Exp.Abs.PBranch $1 $2 $4 $6 }
+
+ListBranch :: { [Exp.Abs.Branch] }
+ListBranch : {- empty -} { [] }
+ | Branch { (:[]) $1 }
+ | Branch ';' ListBranch { (:) $1 $3 }
+
+Label :: { Exp.Abs.Label }
+Label : AIdent ListTele { Exp.Abs.OLabel $1 $2 }
+ | AIdent ListTele '<' ListAIdent '>' System { Exp.Abs.PLabel $1 $2 $4 $6 }
+
+ListLabel :: { [Exp.Abs.Label] }
+ListLabel : {- empty -} { [] }
+ | Label { (:[]) $1 }
+ | Label '|' ListLabel { (:) $1 $3 }
+
+Tele :: { Exp.Abs.Tele }
+Tele : '(' AIdent ListAIdent ':' Exp ')' { Exp.Abs.Tele $2 $3 $5 }
+
+ListTele :: { [Exp.Abs.Tele] }
+ListTele : {- empty -} { [] } | Tele ListTele { (:) $1 $2 }
+
+PTele :: { Exp.Abs.PTele }
+PTele : '(' Exp ':' Exp ')' { Exp.Abs.PTele $2 $4 }
+
+ListPTele :: { [Exp.Abs.PTele] }
+ListPTele : PTele { (:[]) $1 } | PTele ListPTele { (:) $1 $2 }
+
+ListAIdent :: { [Exp.Abs.AIdent] }
+ListAIdent : {- empty -} { [] } | AIdent ListAIdent { (:) $1 $2 }
+{
+
+happyError :: [Token] -> Either String a
+happyError ts = Left $
+ "syntax error at " ++ tokenPos ts ++
+ case ts of
+ [] -> []
+ [Err _] -> " due to lexer error"
+ t:_ -> " before `" ++ (prToken t) ++ "'"
+
+myLexer = tokens
+}
+
--- /dev/null
+{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+{-# LANGUAGE FlexibleInstances #-}
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
+
+-- | Pretty-printer for Exp.
+-- Generated by the BNF converter.
+
+module Exp.Print where
+
+import qualified Exp.Abs
+import Data.Char
+
+-- | The top-level printing method.
+
+printTree :: Print a => a -> String
+printTree = render . prt 0
+
+type Doc = [ShowS] -> [ShowS]
+
+doc :: ShowS -> Doc
+doc = (:)
+
+render :: Doc -> String
+render d = rend 0 (map ($ "") $ d []) "" where
+ rend i ss = case ss of
+ "[" :ts -> showChar '[' . rend i ts
+ "(" :ts -> showChar '(' . rend i ts
+ "{" :ts -> showChar '{' . new (i+1) . rend (i+1) ts
+ "}" : ";":ts -> new (i-1) . space "}" . showChar ';' . new (i-1) . rend (i-1) ts
+ "}" :ts -> new (i-1) . showChar '}' . new (i-1) . rend (i-1) ts
+ ";" :ts -> showChar ';' . new i . rend i ts
+ t : ts@(p:_) | closingOrPunctuation p -> showString t . rend i ts
+ t :ts -> space t . rend i ts
+ _ -> id
+ new i = showChar '\n' . replicateS (2*i) (showChar ' ') . dropWhile isSpace
+ space t = showString t . (\s -> if null s then "" else ' ':s)
+
+ closingOrPunctuation :: String -> Bool
+ closingOrPunctuation [c] = c `elem` closerOrPunct
+ closingOrPunctuation _ = False
+
+ closerOrPunct :: String
+ closerOrPunct = ")],;"
+
+parenth :: Doc -> Doc
+parenth ss = doc (showChar '(') . ss . doc (showChar ')')
+
+concatS :: [ShowS] -> ShowS
+concatS = foldr (.) id
+
+concatD :: [Doc] -> Doc
+concatD = foldr (.) id
+
+replicateS :: Int -> ShowS -> ShowS
+replicateS n f = concatS (replicate n f)
+
+-- | The printer class does the job.
+
+class Print a where
+ prt :: Int -> a -> Doc
+ prtList :: Int -> [a] -> Doc
+ prtList i = concatD . map (prt i)
+
+instance {-# OVERLAPPABLE #-} Print a => Print [a] where
+ prt = prtList
+
+instance Print Char where
+ prt _ s = doc (showChar '\'' . mkEsc '\'' s . showChar '\'')
+ prtList _ s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
+
+mkEsc :: Char -> Char -> ShowS
+mkEsc q s = case s of
+ _ | s == q -> showChar '\\' . showChar s
+ '\\'-> showString "\\\\"
+ '\n' -> showString "\\n"
+ '\t' -> showString "\\t"
+ _ -> showChar s
+
+prPrec :: Int -> Int -> Doc -> Doc
+prPrec i j = if j < i then parenth else id
+
+instance Print Integer where
+ prt _ x = doc (shows x)
+
+instance Print Double where
+ prt _ x = doc (shows x)
+
+instance Print Exp.Abs.AIdent where
+ prt _ (Exp.Abs.AIdent (_,i)) = doc (showString i)
+ prtList _ [] = concatD []
+ prtList _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+instance Print Exp.Abs.CIdent where
+ prt _ (Exp.Abs.CIdent i) = doc (showString i)
+
+instance Print Exp.Abs.HoleIdent where
+ prt _ (Exp.Abs.HoleIdent (_,i)) = doc (showString i)
+
+instance Print Exp.Abs.Module where
+ prt i e = case e of
+ Exp.Abs.Module aident imps decls -> prPrec i 0 (concatD [doc (showString "module"), prt 0 aident, doc (showString "where"), doc (showString "{"), prt 0 imps, prt 0 decls, doc (showString "}")])
+
+instance Print Exp.Abs.Imp where
+ prt i e = case e of
+ Exp.Abs.Import aident -> prPrec i 0 (concatD [doc (showString "import"), prt 0 aident])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+
+instance Print [Exp.Abs.Imp] where
+ prt = prtList
+
+instance Print Exp.Abs.Decl where
+ prt i e = case e of
+ Exp.Abs.DeclDef aident teles exp expwhere -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles, doc (showString ":"), prt 0 exp, doc (showString "="), prt 0 expwhere])
+ Exp.Abs.DeclData aident teles labels -> prPrec i 0 (concatD [doc (showString "data"), prt 0 aident, prt 0 teles, doc (showString "="), prt 0 labels])
+ Exp.Abs.DeclHData aident teles labels -> prPrec i 0 (concatD [doc (showString "hdata"), prt 0 aident, prt 0 teles, doc (showString "="), prt 0 labels])
+ Exp.Abs.DeclSplit aident teles exp branchs -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles, doc (showString ":"), prt 0 exp, doc (showString "="), doc (showString "split"), doc (showString "{"), prt 0 branchs, doc (showString "}")])
+ Exp.Abs.DeclUndef aident teles exp -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles, doc (showString ":"), prt 0 exp, doc (showString "="), doc (showString "undefined")])
+ Exp.Abs.DeclMutual decls -> prPrec i 0 (concatD [doc (showString "mutual"), doc (showString "{"), prt 0 decls, doc (showString "}")])
+ Exp.Abs.DeclOpaque aident -> prPrec i 0 (concatD [doc (showString "opaque"), prt 0 aident])
+ Exp.Abs.DeclTransparent aident -> prPrec i 0 (concatD [doc (showString "transparent"), prt 0 aident])
+ Exp.Abs.DeclTransparentAll -> prPrec i 0 (concatD [doc (showString "transparent_all")])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+
+instance Print [Exp.Abs.Decl] where
+ prt = prtList
+
+instance Print Exp.Abs.ExpWhere where
+ prt i e = case e of
+ Exp.Abs.Where exp decls -> prPrec i 0 (concatD [prt 0 exp, doc (showString "where"), doc (showString "{"), prt 0 decls, doc (showString "}")])
+ Exp.Abs.NoWhere exp -> prPrec i 0 (concatD [prt 0 exp])
+
+instance Print Exp.Abs.Exp where
+ prt i e = case e of
+ Exp.Abs.Let decls exp -> prPrec i 0 (concatD [doc (showString "let"), doc (showString "{"), prt 0 decls, doc (showString "}"), doc (showString "in"), prt 0 exp])
+ Exp.Abs.Lam pteles exp -> prPrec i 0 (concatD [doc (showString "\\"), prt 0 pteles, doc (showString "->"), prt 0 exp])
+ Exp.Abs.PLam aidents exp -> prPrec i 0 (concatD [doc (showString "<"), prt 0 aidents, doc (showString ">"), prt 0 exp])
+ Exp.Abs.Split exp branchs -> prPrec i 0 (concatD [doc (showString "split@"), prt 0 exp, doc (showString "with"), doc (showString "{"), prt 0 branchs, doc (showString "}")])
+ Exp.Abs.Fun exp1 exp2 -> prPrec i 1 (concatD [prt 2 exp1, doc (showString "->"), prt 1 exp2])
+ Exp.Abs.Pi pteles exp -> prPrec i 1 (concatD [prt 0 pteles, doc (showString "->"), prt 1 exp])
+ Exp.Abs.Sigma pteles exp -> prPrec i 1 (concatD [prt 0 pteles, doc (showString "*"), prt 1 exp])
+ Exp.Abs.AppFormula exp formula -> prPrec i 2 (concatD [prt 2 exp, doc (showString "@"), prt 0 formula])
+ Exp.Abs.App exp1 exp2 -> prPrec i 2 (concatD [prt 2 exp1, prt 3 exp2])
+ Exp.Abs.PathP exp1 exp2 exp3 -> prPrec i 3 (concatD [doc (showString "PathP"), prt 4 exp1, prt 4 exp2, prt 4 exp3])
+ Exp.Abs.Comp exp1 exp2 system -> prPrec i 3 (concatD [doc (showString "comp"), prt 4 exp1, prt 4 exp2, prt 0 system])
+ Exp.Abs.HComp exp1 exp2 system -> prPrec i 3 (concatD [doc (showString "hComp"), prt 4 exp1, prt 4 exp2, prt 0 system])
+ Exp.Abs.Trans exp1 exp2 -> prPrec i 3 (concatD [doc (showString "transport"), prt 4 exp1, prt 4 exp2])
+ Exp.Abs.Fill exp1 exp2 system -> prPrec i 3 (concatD [doc (showString "fill"), prt 4 exp1, prt 4 exp2, prt 0 system])
+ Exp.Abs.Glue exp system -> prPrec i 3 (concatD [doc (showString "Glue"), prt 4 exp, prt 0 system])
+ Exp.Abs.GlueElem exp system -> prPrec i 3 (concatD [doc (showString "glue"), prt 4 exp, prt 0 system])
+ Exp.Abs.UnGlueElem exp system -> prPrec i 3 (concatD [doc (showString "unglue"), prt 4 exp, prt 0 system])
+ Exp.Abs.Id exp1 exp2 exp3 -> prPrec i 3 (concatD [doc (showString "Id"), prt 4 exp1, prt 4 exp2, prt 3 exp3])
+ Exp.Abs.IdPair exp system -> prPrec i 3 (concatD [doc (showString "idC"), prt 4 exp, prt 0 system])
+ Exp.Abs.IdJ exp1 exp2 exp3 exp4 exp5 exp6 -> prPrec i 3 (concatD [doc (showString "idJ"), prt 4 exp1, prt 4 exp2, prt 4 exp3, prt 4 exp4, prt 4 exp5, prt 4 exp6])
+ Exp.Abs.Fst exp -> prPrec i 4 (concatD [prt 4 exp, doc (showString ".1")])
+ Exp.Abs.Snd exp -> prPrec i 4 (concatD [prt 4 exp, doc (showString ".2")])
+ Exp.Abs.Pair exp exps -> prPrec i 5 (concatD [doc (showString "("), prt 0 exp, doc (showString ","), prt 0 exps, doc (showString ")")])
+ Exp.Abs.Var aident -> prPrec i 5 (concatD [prt 0 aident])
+ Exp.Abs.PCon aident exp -> prPrec i 5 (concatD [prt 0 aident, doc (showString "{"), prt 0 exp, doc (showString "}")])
+ Exp.Abs.U -> prPrec i 5 (concatD [doc (showString "U")])
+ Exp.Abs.Hole holeident -> prPrec i 5 (concatD [prt 0 holeident])
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
+
+instance Print [Exp.Abs.Exp] where
+ prt = prtList
+
+instance Print Exp.Abs.Dir where
+ prt i e = case e of
+ Exp.Abs.Dir0 -> prPrec i 0 (concatD [doc (showString "0")])
+ Exp.Abs.Dir1 -> prPrec i 0 (concatD [doc (showString "1")])
+
+instance Print Exp.Abs.System where
+ prt i e = case e of
+ Exp.Abs.System sides -> prPrec i 0 (concatD [doc (showString "["), prt 0 sides, doc (showString "]")])
+
+instance Print Exp.Abs.Face where
+ prt i e = case e of
+ Exp.Abs.Face aident dir -> prPrec i 0 (concatD [doc (showString "("), prt 0 aident, doc (showString "="), prt 0 dir, doc (showString ")")])
+ prtList _ [] = concatD []
+ prtList _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+instance Print [Exp.Abs.Face] where
+ prt = prtList
+
+instance Print Exp.Abs.Side where
+ prt i e = case e of
+ Exp.Abs.Side faces exp -> prPrec i 0 (concatD [prt 0 faces, doc (showString "->"), prt 0 exp])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
+
+instance Print [Exp.Abs.Side] where
+ prt = prtList
+
+instance Print Exp.Abs.Formula where
+ prt i e = case e of
+ Exp.Abs.Disj formula1 formula2 -> prPrec i 0 (concatD [prt 0 formula1, doc (showString "\\/"), prt 1 formula2])
+ Exp.Abs.Conj formula1 cident formula2 -> prPrec i 1 (concatD [prt 1 formula1, prt 0 cident, prt 2 formula2])
+ Exp.Abs.Neg formula -> prPrec i 2 (concatD [doc (showString "-"), prt 2 formula])
+ Exp.Abs.Atom aident -> prPrec i 2 (concatD [prt 0 aident])
+ Exp.Abs.Dir dir -> prPrec i 2 (concatD [prt 0 dir])
+
+instance Print Exp.Abs.Branch where
+ prt i e = case e of
+ Exp.Abs.OBranch aident aidents expwhere -> prPrec i 0 (concatD [prt 0 aident, prt 0 aidents, doc (showString "->"), prt 0 expwhere])
+ Exp.Abs.PBranch aident aidents1 aidents2 expwhere -> prPrec i 0 (concatD [prt 0 aident, prt 0 aidents1, doc (showString "@"), prt 0 aidents2, doc (showString "->"), prt 0 expwhere])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+
+instance Print [Exp.Abs.Branch] where
+ prt = prtList
+
+instance Print Exp.Abs.Label where
+ prt i e = case e of
+ Exp.Abs.OLabel aident teles -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles])
+ Exp.Abs.PLabel aident teles aidents system -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles, doc (showString "<"), prt 0 aidents, doc (showString ">"), prt 0 system])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString "|"), prt 0 xs]
+
+instance Print [Exp.Abs.Label] where
+ prt = prtList
+
+instance Print Exp.Abs.Tele where
+ prt i e = case e of
+ Exp.Abs.Tele aident aidents exp -> prPrec i 0 (concatD [doc (showString "("), prt 0 aident, prt 0 aidents, doc (showString ":"), prt 0 exp, doc (showString ")")])
+ prtList _ [] = concatD []
+ prtList _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+instance Print [Exp.Abs.Tele] where
+ prt = prtList
+
+instance Print Exp.Abs.PTele where
+ prt i e = case e of
+ Exp.Abs.PTele exp1 exp2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 exp1, doc (showString ":"), prt 0 exp2, doc (showString ")")])
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+instance Print [Exp.Abs.PTele] where
+ prt = prtList
+
+instance Print [Exp.Abs.AIdent] where
+ prt = prtList
+
--- /dev/null
+{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ <= 708
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+{-# LANGUAGE FlexibleInstances #-}
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
+
+-- | Pretty-printer for Exp.
+-- Generated by the BNF converter.
+
+module Exp.Print where
+
+import qualified Exp.Abs
+import Data.Char
+
+-- | The top-level printing method.
+
+printTree :: Print a => a -> String
+printTree = render . prt 0
+
+type Doc = [ShowS] -> [ShowS]
+
+doc :: ShowS -> Doc
+doc = (:)
+
+render :: Doc -> String
+render d = rend 0 (map ($ "") $ d []) "" where
+ rend i ss = case ss of
+ "[" :ts -> showChar '[' . rend i ts
+ "(" :ts -> showChar '(' . rend i ts
+ "{" :ts -> showChar '{' . new (i+1) . rend (i+1) ts
+ "}" : ";":ts -> new (i-1) . space "}" . showChar ';' . new (i-1) . rend (i-1) ts
+ "}" :ts -> new (i-1) . showChar '}' . new (i-1) . rend (i-1) ts
+ [";"] -> showChar ';'
+ ";" :ts -> showChar ';' . new i . rend i ts
+ t : ts@(p:_) | closingOrPunctuation p -> showString t . rend i ts
+ t :ts -> space t . rend i ts
+ _ -> id
+ new i = showChar '\n' . replicateS (2*i) (showChar ' ') . dropWhile isSpace
+ space t s =
+ case (all isSpace t', null spc, null rest) of
+ (True , _ , True ) -> [] -- remove trailing space
+ (False, _ , True ) -> t' -- remove trailing space
+ (False, True, False) -> t' ++ ' ' : s -- add space if none
+ _ -> t' ++ s
+ where
+ t' = showString t []
+ (spc, rest) = span isSpace s
+
+ closingOrPunctuation :: String -> Bool
+ closingOrPunctuation [c] = c `elem` closerOrPunct
+ closingOrPunctuation _ = False
+
+ closerOrPunct :: String
+ closerOrPunct = ")],;"
+
+parenth :: Doc -> Doc
+parenth ss = doc (showChar '(') . ss . doc (showChar ')')
+
+concatS :: [ShowS] -> ShowS
+concatS = foldr (.) id
+
+concatD :: [Doc] -> Doc
+concatD = foldr (.) id
+
+replicateS :: Int -> ShowS -> ShowS
+replicateS n f = concatS (replicate n f)
+
+-- | The printer class does the job.
+
+class Print a where
+ prt :: Int -> a -> Doc
+ prtList :: Int -> [a] -> Doc
+ prtList i = concatD . map (prt i)
+
+instance {-# OVERLAPPABLE #-} Print a => Print [a] where
+ prt = prtList
+
+instance Print Char where
+ prt _ s = doc (showChar '\'' . mkEsc '\'' s . showChar '\'')
+ prtList _ s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
+
+mkEsc :: Char -> Char -> ShowS
+mkEsc q s = case s of
+ _ | s == q -> showChar '\\' . showChar s
+ '\\'-> showString "\\\\"
+ '\n' -> showString "\\n"
+ '\t' -> showString "\\t"
+ _ -> showChar s
+
+prPrec :: Int -> Int -> Doc -> Doc
+prPrec i j = if j < i then parenth else id
+
+instance Print Integer where
+ prt _ x = doc (shows x)
+
+instance Print Double where
+ prt _ x = doc (shows x)
+
+instance Print Exp.Abs.AIdent where
+ prt _ (Exp.Abs.AIdent (_,i)) = doc $ showString $ i
+ prtList _ [] = concatD []
+ prtList _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+instance Print Exp.Abs.CIdent where
+ prt _ (Exp.Abs.CIdent i) = doc $ showString $ i
+
+instance Print Exp.Abs.HoleIdent where
+ prt _ (Exp.Abs.HoleIdent (_,i)) = doc $ showString $ i
+
+instance Print Exp.Abs.Module where
+ prt i e = case e of
+ Exp.Abs.Module aident imps decls -> prPrec i 0 (concatD [doc (showString "module"), prt 0 aident, doc (showString "where"), doc (showString "{"), prt 0 imps, prt 0 decls, doc (showString "}")])
+
+instance Print Exp.Abs.Imp where
+ prt i e = case e of
+ Exp.Abs.Import aident -> prPrec i 0 (concatD [doc (showString "import"), prt 0 aident])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+
+instance Print [Exp.Abs.Imp] where
+ prt = prtList
+
+instance Print Exp.Abs.Decl where
+ prt i e = case e of
+ Exp.Abs.DeclDef aident teles exp expwhere -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles, doc (showString ":"), prt 0 exp, doc (showString "="), prt 0 expwhere])
+ Exp.Abs.DeclData aident teles labels -> prPrec i 0 (concatD [doc (showString "data"), prt 0 aident, prt 0 teles, doc (showString "="), prt 0 labels])
+ Exp.Abs.DeclHData aident teles labels -> prPrec i 0 (concatD [doc (showString "hdata"), prt 0 aident, prt 0 teles, doc (showString "="), prt 0 labels])
+ Exp.Abs.DeclSplit aident teles exp branchs -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles, doc (showString ":"), prt 0 exp, doc (showString "="), doc (showString "split"), doc (showString "{"), prt 0 branchs, doc (showString "}")])
+ Exp.Abs.DeclUndef aident teles exp -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles, doc (showString ":"), prt 0 exp, doc (showString "="), doc (showString "undefined")])
+ Exp.Abs.DeclMutual decls -> prPrec i 0 (concatD [doc (showString "mutual"), doc (showString "{"), prt 0 decls, doc (showString "}")])
+ Exp.Abs.DeclOpaque aident -> prPrec i 0 (concatD [doc (showString "opaque"), prt 0 aident])
+ Exp.Abs.DeclTransparent aident -> prPrec i 0 (concatD [doc (showString "transparent"), prt 0 aident])
+ Exp.Abs.DeclTransparentAll -> prPrec i 0 (concatD [doc (showString "transparent_all")])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+
+instance Print [Exp.Abs.Decl] where
+ prt = prtList
+
+instance Print Exp.Abs.ExpWhere where
+ prt i e = case e of
+ Exp.Abs.Where exp decls -> prPrec i 0 (concatD [prt 0 exp, doc (showString "where"), doc (showString "{"), prt 0 decls, doc (showString "}")])
+ Exp.Abs.NoWhere exp -> prPrec i 0 (concatD [prt 0 exp])
+
+instance Print Exp.Abs.Exp where
+ prt i e = case e of
+ Exp.Abs.Let decls exp -> prPrec i 0 (concatD [doc (showString "let"), doc (showString "{"), prt 0 decls, doc (showString "}"), doc (showString "in"), prt 0 exp])
+ Exp.Abs.Lam pteles exp -> prPrec i 0 (concatD [doc (showString "\\"), prt 0 pteles, doc (showString "->"), prt 0 exp])
+ Exp.Abs.PLam aidents exp -> prPrec i 0 (concatD [doc (showString "<"), prt 0 aidents, doc (showString ">"), prt 0 exp])
+ Exp.Abs.Split exp branchs -> prPrec i 0 (concatD [doc (showString "split@"), prt 0 exp, doc (showString "with"), doc (showString "{"), prt 0 branchs, doc (showString "}")])
+ Exp.Abs.Fun exp1 exp2 -> prPrec i 1 (concatD [prt 2 exp1, doc (showString "->"), prt 1 exp2])
+ Exp.Abs.Pi pteles exp -> prPrec i 1 (concatD [prt 0 pteles, doc (showString "->"), prt 1 exp])
+ Exp.Abs.Sigma pteles exp -> prPrec i 1 (concatD [prt 0 pteles, doc (showString "*"), prt 1 exp])
+ Exp.Abs.AppFormula exp formula -> prPrec i 2 (concatD [prt 2 exp, doc (showString "@"), prt 0 formula])
+ Exp.Abs.App exp1 exp2 -> prPrec i 2 (concatD [prt 2 exp1, prt 3 exp2])
+ Exp.Abs.PathP exp1 exp2 exp3 -> prPrec i 3 (concatD [doc (showString "PathP"), prt 4 exp1, prt 4 exp2, prt 4 exp3])
+ Exp.Abs.Comp exp1 exp2 system -> prPrec i 3 (concatD [doc (showString "comp"), prt 4 exp1, prt 4 exp2, prt 0 system])
+ Exp.Abs.HComp exp1 exp2 system -> prPrec i 3 (concatD [doc (showString "hComp"), prt 4 exp1, prt 4 exp2, prt 0 system])
+ Exp.Abs.Trans exp1 exp2 -> prPrec i 3 (concatD [doc (showString "transport"), prt 4 exp1, prt 4 exp2])
+ Exp.Abs.Fill exp1 exp2 system -> prPrec i 3 (concatD [doc (showString "fill"), prt 4 exp1, prt 4 exp2, prt 0 system])
+ Exp.Abs.Glue exp system -> prPrec i 3 (concatD [doc (showString "Glue"), prt 4 exp, prt 0 system])
+ Exp.Abs.GlueElem exp system -> prPrec i 3 (concatD [doc (showString "glue"), prt 4 exp, prt 0 system])
+ Exp.Abs.UnGlueElem exp system -> prPrec i 3 (concatD [doc (showString "unglue"), prt 4 exp, prt 0 system])
+ Exp.Abs.Id exp1 exp2 exp3 -> prPrec i 3 (concatD [doc (showString "Id"), prt 4 exp1, prt 4 exp2, prt 3 exp3])
+ Exp.Abs.IdPair exp system -> prPrec i 3 (concatD [doc (showString "idC"), prt 4 exp, prt 0 system])
+ Exp.Abs.IdJ exp1 exp2 exp3 exp4 exp5 exp6 -> prPrec i 3 (concatD [doc (showString "idJ"), prt 4 exp1, prt 4 exp2, prt 4 exp3, prt 4 exp4, prt 4 exp5, prt 4 exp6])
+ Exp.Abs.Fst exp -> prPrec i 4 (concatD [prt 4 exp, doc (showString ".1")])
+ Exp.Abs.Snd exp -> prPrec i 4 (concatD [prt 4 exp, doc (showString ".2")])
+ Exp.Abs.Pair exp exps -> prPrec i 5 (concatD [doc (showString "("), prt 0 exp, doc (showString ","), prt 0 exps, doc (showString ")")])
+ Exp.Abs.Var aident -> prPrec i 5 (concatD [prt 0 aident])
+ Exp.Abs.PCon aident exp -> prPrec i 5 (concatD [prt 0 aident, doc (showString "{"), prt 0 exp, doc (showString "}")])
+ Exp.Abs.U -> prPrec i 5 (concatD [doc (showString "U")])
+ Exp.Abs.Hole holeident -> prPrec i 5 (concatD [prt 0 holeident])
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
+
+instance Print [Exp.Abs.Exp] where
+ prt = prtList
+
+instance Print Exp.Abs.Dir where
+ prt i e = case e of
+ Exp.Abs.Dir0 -> prPrec i 0 (concatD [doc (showString "0")])
+ Exp.Abs.Dir1 -> prPrec i 0 (concatD [doc (showString "1")])
+
+instance Print Exp.Abs.System where
+ prt i e = case e of
+ Exp.Abs.System sides -> prPrec i 0 (concatD [doc (showString "["), prt 0 sides, doc (showString "]")])
+
+instance Print Exp.Abs.Face where
+ prt i e = case e of
+ Exp.Abs.Face aident dir -> prPrec i 0 (concatD [doc (showString "("), prt 0 aident, doc (showString "="), prt 0 dir, doc (showString ")")])
+ prtList _ [] = concatD []
+ prtList _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+instance Print [Exp.Abs.Face] where
+ prt = prtList
+
+instance Print Exp.Abs.Side where
+ prt i e = case e of
+ Exp.Abs.Side faces exp -> prPrec i 0 (concatD [prt 0 faces, doc (showString "->"), prt 0 exp])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
+
+instance Print [Exp.Abs.Side] where
+ prt = prtList
+
+instance Print Exp.Abs.Formula where
+ prt i e = case e of
+ Exp.Abs.Disj formula1 formula2 -> prPrec i 0 (concatD [prt 0 formula1, doc (showString "\\/"), prt 1 formula2])
+ Exp.Abs.Conj formula1 cident formula2 -> prPrec i 1 (concatD [prt 1 formula1, prt 0 cident, prt 2 formula2])
+ Exp.Abs.Neg formula -> prPrec i 2 (concatD [doc (showString "-"), prt 2 formula])
+ Exp.Abs.Atom aident -> prPrec i 2 (concatD [prt 0 aident])
+ Exp.Abs.Dir dir -> prPrec i 2 (concatD [prt 0 dir])
+
+instance Print Exp.Abs.Branch where
+ prt i e = case e of
+ Exp.Abs.OBranch aident aidents expwhere -> prPrec i 0 (concatD [prt 0 aident, prt 0 aidents, doc (showString "->"), prt 0 expwhere])
+ Exp.Abs.PBranch aident aidents1 aidents2 expwhere -> prPrec i 0 (concatD [prt 0 aident, prt 0 aidents1, doc (showString "@"), prt 0 aidents2, doc (showString "->"), prt 0 expwhere])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
+
+instance Print [Exp.Abs.Branch] where
+ prt = prtList
+
+instance Print Exp.Abs.Label where
+ prt i e = case e of
+ Exp.Abs.OLabel aident teles -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles])
+ Exp.Abs.PLabel aident teles aidents system -> prPrec i 0 (concatD [prt 0 aident, prt 0 teles, doc (showString "<"), prt 0 aidents, doc (showString ">"), prt 0 system])
+ prtList _ [] = concatD []
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, doc (showString "|"), prt 0 xs]
+
+instance Print [Exp.Abs.Label] where
+ prt = prtList
+
+instance Print Exp.Abs.Tele where
+ prt i e = case e of
+ Exp.Abs.Tele aident aidents exp -> prPrec i 0 (concatD [doc (showString "("), prt 0 aident, prt 0 aidents, doc (showString ":"), prt 0 exp, doc (showString ")")])
+ prtList _ [] = concatD []
+ prtList _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+instance Print [Exp.Abs.Tele] where
+ prt = prtList
+
+instance Print Exp.Abs.PTele where
+ prt i e = case e of
+ Exp.Abs.PTele exp1 exp2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 exp1, doc (showString ":"), prt 0 exp2, doc (showString ")")])
+ prtList _ [x] = concatD [prt 0 x]
+ prtList _ (x:xs) = concatD [prt 0 x, prt 0 xs]
+
+instance Print [Exp.Abs.PTele] where
+ prt = prtList
+
+instance Print [Exp.Abs.AIdent] where
+ prt = prtList
+
--- /dev/null
+module Exp.Skel where
+
+-- Haskell module generated by the BNF converter
+
+import Exp.Abs
+import Exp.ErrM
+type Result = Err String
+
+failure :: Show a => a -> Result
+failure x = Bad $ "Undefined case: " ++ show x
+
+transAIdent :: AIdent -> Result
+transAIdent x = case x of
+ AIdent string -> failure x
+transCIdent :: CIdent -> Result
+transCIdent x = case x of
+ CIdent string -> failure x
+transHoleIdent :: HoleIdent -> Result
+transHoleIdent x = case x of
+ HoleIdent string -> failure x
+transModule :: Module -> Result
+transModule x = case x of
+ Module aident imps decls -> failure x
+transImp :: Imp -> Result
+transImp x = case x of
+ Import aident -> failure x
+transDecl :: Decl -> Result
+transDecl x = case x of
+ DeclDef aident teles exp expwhere -> failure x
+ DeclData aident teles labels -> failure x
+ DeclHData aident teles labels -> failure x
+ DeclSplit aident teles exp branchs -> failure x
+ DeclUndef aident teles exp -> failure x
+ DeclMutual decls -> failure x
+ DeclOpaque aident -> failure x
+ DeclTransparent aident -> failure x
+ DeclTransparentAll -> failure x
+transExpWhere :: ExpWhere -> Result
+transExpWhere x = case x of
+ Where exp decls -> failure x
+ NoWhere exp -> failure x
+transExp :: Exp -> Result
+transExp x = case x of
+ Let decls exp -> failure x
+ Lam pteles exp -> failure x
+ PLam aidents exp -> failure x
+ Split exp branchs -> failure x
+ Fun exp1 exp2 -> failure x
+ Pi pteles exp -> failure x
+ Sigma pteles exp -> failure x
+ AppFormula exp formula -> failure x
+ App exp1 exp2 -> failure x
+ PathP exp1 exp2 exp3 -> failure x
+ Comp exp1 exp2 system -> failure x
+ HComp exp1 exp2 system -> failure x
+ Trans exp1 exp2 -> failure x
+ Fill exp1 exp2 system -> failure x
+ Glue exp system -> failure x
+ GlueElem exp system -> failure x
+ UnGlueElem exp system -> failure x
+ Id exp1 exp2 exp3 -> failure x
+ IdPair exp system -> failure x
+ IdJ exp1 exp2 exp3 exp4 exp5 exp6 -> failure x
+ Fst exp -> failure x
+ Snd exp -> failure x
+ Pair exp exps -> failure x
+ Var aident -> failure x
+ PCon aident exp -> failure x
+ U -> failure x
+ Hole holeident -> failure x
+transDir :: Dir -> Result
+transDir x = case x of
+ Dir0 -> failure x
+ Dir1 -> failure x
+transSystem :: System -> Result
+transSystem x = case x of
+ System sides -> failure x
+transFace :: Face -> Result
+transFace x = case x of
+ Face aident dir -> failure x
+transSide :: Side -> Result
+transSide x = case x of
+ Side faces exp -> failure x
+transFormula :: Formula -> Result
+transFormula x = case x of
+ Disj formula1 formula2 -> failure x
+ Conj formula1 cident formula2 -> failure x
+ Neg formula -> failure x
+ Atom aident -> failure x
+ Dir dir -> failure x
+transBranch :: Branch -> Result
+transBranch x = case x of
+ OBranch aident aidents expwhere -> failure x
+ PBranch aident aidents1 aidents2 expwhere -> failure x
+transLabel :: Label -> Result
+transLabel x = case x of
+ OLabel aident teles -> failure x
+ PLabel aident teles aidents system -> failure x
+transTele :: Tele -> Result
+transTele x = case x of
+ Tele aident aidents exp -> failure x
+transPTele :: PTele -> Result
+transPTele x = case x of
+ PTele exp1 exp2 -> failure x
+
--- /dev/null
+-- Haskell module generated by the BNF converter
+
+module Exp.Skel where
+
+import qualified Exp.Abs
+
+type Err = Either String
+type Result = Err String
+
+failure :: Show a => a -> Result
+failure x = Left $ "Undefined case: " ++ show x
+
+transAIdent :: Exp.Abs.AIdent -> Result
+transAIdent x = case x of
+ Exp.Abs.AIdent string -> failure x
+transCIdent :: Exp.Abs.CIdent -> Result
+transCIdent x = case x of
+ Exp.Abs.CIdent string -> failure x
+transHoleIdent :: Exp.Abs.HoleIdent -> Result
+transHoleIdent x = case x of
+ Exp.Abs.HoleIdent string -> failure x
+transModule :: Exp.Abs.Module -> Result
+transModule x = case x of
+ Exp.Abs.Module aident imps decls -> failure x
+transImp :: Exp.Abs.Imp -> Result
+transImp x = case x of
+ Exp.Abs.Import aident -> failure x
+transDecl :: Exp.Abs.Decl -> Result
+transDecl x = case x of
+ Exp.Abs.DeclDef aident teles exp expwhere -> failure x
+ Exp.Abs.DeclData aident teles labels -> failure x
+ Exp.Abs.DeclHData aident teles labels -> failure x
+ Exp.Abs.DeclSplit aident teles exp branchs -> failure x
+ Exp.Abs.DeclUndef aident teles exp -> failure x
+ Exp.Abs.DeclMutual decls -> failure x
+ Exp.Abs.DeclOpaque aident -> failure x
+ Exp.Abs.DeclTransparent aident -> failure x
+ Exp.Abs.DeclTransparentAll -> failure x
+transExpWhere :: Exp.Abs.ExpWhere -> Result
+transExpWhere x = case x of
+ Exp.Abs.Where exp decls -> failure x
+ Exp.Abs.NoWhere exp -> failure x
+transExp :: Exp.Abs.Exp -> Result
+transExp x = case x of
+ Exp.Abs.Let decls exp -> failure x
+ Exp.Abs.Lam pteles exp -> failure x
+ Exp.Abs.PLam aidents exp -> failure x
+ Exp.Abs.Split exp branchs -> failure x
+ Exp.Abs.Fun exp1 exp2 -> failure x
+ Exp.Abs.Pi pteles exp -> failure x
+ Exp.Abs.Sigma pteles exp -> failure x
+ Exp.Abs.AppFormula exp formula -> failure x
+ Exp.Abs.App exp1 exp2 -> failure x
+ Exp.Abs.PathP exp1 exp2 exp3 -> failure x
+ Exp.Abs.Comp exp1 exp2 system -> failure x
+ Exp.Abs.HComp exp1 exp2 system -> failure x
+ Exp.Abs.Trans exp1 exp2 -> failure x
+ Exp.Abs.Fill exp1 exp2 system -> failure x
+ Exp.Abs.Glue exp system -> failure x
+ Exp.Abs.GlueElem exp system -> failure x
+ Exp.Abs.UnGlueElem exp system -> failure x
+ Exp.Abs.Id exp1 exp2 exp3 -> failure x
+ Exp.Abs.IdPair exp system -> failure x
+ Exp.Abs.IdJ exp1 exp2 exp3 exp4 exp5 exp6 -> failure x
+ Exp.Abs.Fst exp -> failure x
+ Exp.Abs.Snd exp -> failure x
+ Exp.Abs.Pair exp exps -> failure x
+ Exp.Abs.Var aident -> failure x
+ Exp.Abs.PCon aident exp -> failure x
+ Exp.Abs.U -> failure x
+ Exp.Abs.Hole holeident -> failure x
+transDir :: Exp.Abs.Dir -> Result
+transDir x = case x of
+ Exp.Abs.Dir0 -> failure x
+ Exp.Abs.Dir1 -> failure x
+transSystem :: Exp.Abs.System -> Result
+transSystem x = case x of
+ Exp.Abs.System sides -> failure x
+transFace :: Exp.Abs.Face -> Result
+transFace x = case x of
+ Exp.Abs.Face aident dir -> failure x
+transSide :: Exp.Abs.Side -> Result
+transSide x = case x of
+ Exp.Abs.Side faces exp -> failure x
+transFormula :: Exp.Abs.Formula -> Result
+transFormula x = case x of
+ Exp.Abs.Disj formula1 formula2 -> failure x
+ Exp.Abs.Conj formula1 cident formula2 -> failure x
+ Exp.Abs.Neg formula -> failure x
+ Exp.Abs.Atom aident -> failure x
+ Exp.Abs.Dir dir -> failure x
+transBranch :: Exp.Abs.Branch -> Result
+transBranch x = case x of
+ Exp.Abs.OBranch aident aidents expwhere -> failure x
+ Exp.Abs.PBranch aident aidents1 aidents2 expwhere -> failure x
+transLabel :: Exp.Abs.Label -> Result
+transLabel x = case x of
+ Exp.Abs.OLabel aident teles -> failure x
+ Exp.Abs.PLabel aident teles aidents system -> failure x
+transTele :: Exp.Abs.Tele -> Result
+transTele x = case x of
+ Exp.Abs.Tele aident aidents exp -> failure x
+transPTele :: Exp.Abs.PTele -> Result
+transPTele x = case x of
+ Exp.Abs.PTele exp1 exp2 -> failure x
+
--- /dev/null
+-- automatically generated by BNF Converter
+module Main where
+
+
+import System.IO ( stdin, hGetContents )
+import System.Environment ( getArgs, getProgName )
+import System.Exit ( exitFailure, exitSuccess )
+import Control.Monad (when)
+
+import Exp.Lex
+import Exp.Par
+import Exp.Skel
+import Exp.Print
+import Exp.Abs
+import Exp.Layout
+
+
+
+import Exp.ErrM
+
+type ParseFun a = [Token] -> Err a
+
+myLLexer = resolveLayout True . myLexer
+
+type Verbosity = Int
+
+putStrV :: Verbosity -> String -> IO ()
+putStrV v s = when (v > 1) $ putStrLn s
+
+runFile :: (Print a, Show a) => Verbosity -> ParseFun a -> FilePath -> IO ()
+runFile v p f = putStrLn f >> readFile f >>= run v p
+
+run :: (Print a, Show a) => Verbosity -> ParseFun a -> String -> IO ()
+run v p s = let ts = myLLexer s in case p ts of
+ Bad s -> do putStrLn "\nParse Failed...\n"
+ putStrV v "Tokens:"
+ putStrV v $ show ts
+ putStrLn s
+ exitFailure
+ Ok tree -> do putStrLn "\nParse Successful!"
+ showTree v tree
+
+ exitSuccess
+
+
+showTree :: (Show a, Print a) => Int -> a -> IO ()
+showTree v tree
+ = do
+ putStrV v $ "\n[Abstract Syntax]\n\n" ++ show tree
+ putStrV v $ "\n[Linearized tree]\n\n" ++ printTree tree
+
+usage :: IO ()
+usage = do
+ putStrLn $ unlines
+ [ "usage: Call with one of the following argument combinations:"
+ , " --help Display this help message."
+ , " (no arguments) Parse stdin verbosely."
+ , " (files) Parse content of files verbosely."
+ , " -s (files) Silent mode. Parse content of files silently."
+ ]
+ exitFailure
+
+main :: IO ()
+main = do
+ args <- getArgs
+ case args of
+ ["--help"] -> usage
+ [] -> getContents >>= run 2 pModule
+ "-s":fs -> mapM_ (runFile 0 pModule) fs
+ fs -> mapM_ (runFile 2 pModule) fs
+
+
+
+
+
--- /dev/null
+-- Program to test parser, automatically generated by BNF Converter.
+
+module Main where
+
+import System.Environment ( getArgs, getProgName )
+import System.Exit ( exitFailure, exitSuccess )
+import Control.Monad ( when )
+
+import Exp.Lex ( Token )
+import Exp.Par ( pModule, myLexer )
+import Exp.Skel ()
+import Exp.Print ( Print, printTree )
+import Exp.Abs ()
+import Exp.Layout ( resolveLayout )
+
+type Err = Either String
+type ParseFun a = [Token] -> Err a
+
+myLLexer = resolveLayout True . myLexer
+
+type Verbosity = Int
+
+putStrV :: Verbosity -> String -> IO ()
+putStrV v s = when (v > 1) $ putStrLn s
+
+runFile :: (Print a, Show a) => Verbosity -> ParseFun a -> FilePath -> IO ()
+runFile v p f = putStrLn f >> readFile f >>= run v p
+
+run :: (Print a, Show a) => Verbosity -> ParseFun a -> String -> IO ()
+run v p s = case p ts of
+ Left s -> do
+ putStrLn "\nParse Failed...\n"
+ putStrV v "Tokens:"
+ putStrV v $ show ts
+ putStrLn s
+ exitFailure
+ Right tree -> do
+ putStrLn "\nParse Successful!"
+ showTree v tree
+
+ exitSuccess
+ where
+ ts = myLLexer s
+
+
+showTree :: (Show a, Print a) => Int -> a -> IO ()
+showTree v tree
+ = do
+ putStrV v $ "\n[Abstract Syntax]\n\n" ++ show tree
+ putStrV v $ "\n[Linearized tree]\n\n" ++ printTree tree
+
+usage :: IO ()
+usage = do
+ putStrLn $ unlines
+ [ "usage: Call with one of the following argument combinations:"
+ , " --help Display this help message."
+ , " (no arguments) Parse stdin verbosely."
+ , " (files) Parse content of files verbosely."
+ , " -s (files) Silent mode. Parse content of files silently."
+ ]
+ exitFailure
+
+main :: IO ()
+main = do
+ args <- getArgs
+ case args of
+ ["--help"] -> usage
+ [] -> getContents >>= run 2 pModule
+ "-s":fs -> mapM_ (runFile 0 pModule) fs
+ fs -> mapM_ (runFile 2 pModule) fs
+
$(ALEX) -g $<
bnfc $(GRAMMAR_FILES): Exp.cf
- $(BNFC) --haskell -d Exp.cf
+ $(BNFC) --haskell --text-token -d Exp.cf
@ touch $(GRAMMAR_FILES)
TAGS:; hasktags --etags $(INPUT) $(GRAMMAR)
--- /dev/null
+{-# LANGUAGE BangPatterns #-}
+module Helpers where
+
+import Control.Monad
+import Data.Aeson as JSON
+import Data.Text as T
+import Data.Text.Encoding as T
+import Data.ByteString.Lazy as BS
+import GHCJS.DOM.Types as DOM hiding (Text, Event)
+import qualified Language.Javascript.JSaddle as JS
+
+
+writeLogAndScroll :: Text -> JSM ()
+writeLogAndScroll !log = do
+ -- add results
+ !addResult <- JS.eval $ T.unlines
+ [ "(function(f) {"
+ , " app.log_buffer.push(f);"
+ , "})" ]
+ void $! JS.call addResult addResult [ toJSVal log ]
+
+consoleLog :: Text -> JSM ()
+consoleLog t = do
+ log <- JS.eval $ T.unlines [
+ "(function(msg) {",
+ " console.log(msg);",
+ "})"]
+ void $ JS.call log log
+ [ toJSVal t
+ ]
+
+setTimeout :: JSVal -> Int -> JSM ()
+setTimeout val t = do
+ setTimeoutJS <- JS.eval $ T.unlines [
+ "(function(f, t) {",
+ " setTimeout(f, t);",
+ "})"]
+ m <- toJSVal t
+ void $ JS.call setTimeoutJS setTimeoutJS [ val, m ]
+
+saveDataToLocalStorage :: ToJSON a => Text -> a -> JSM ()
+saveDataToLocalStorage key value = do
+ save <- JS.eval $ T.unlines [
+ "(function(key, value) {",
+ " localStorage.setItem(key, value);",
+ "})"]
+ void $ JS.call save save
+ [ toJSVal key
+ , toJSVal . T.decodeUtf8 . BS.toStrict $ encode value
+ ]
+
+removeLocalStorage :: Text -> JSM ()
+removeLocalStorage key = do
+ save <- JS.eval $ T.unlines [
+ "(function(key, value) {",
+ " localStorage.removeItem(key);",
+ "})"]
+ void $ JS.call save save
+ [ toJSVal key
+ ]
+
+loadDataFromLocalStorage :: FromJSON a => Text -> JSM (Maybe a)
+loadDataFromLocalStorage key = do
+ getItem <- JS.eval $ T.unlines [
+ "(function(key) {",
+ " return localStorage.getItem(key);",
+ "})"]
+ res <- JS.call getItem getItem [toJSVal key]
+ (JSON.decode . BS.fromStrict . T.encodeUtf8) <$> JS.valToText res
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE JavaScriptFFI #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
module Main where
+import Data.Aeson as JSON
import Control.Monad.Reader
-import qualified Control.Exception as E
-import Data.List
+import Control.Monad.Writer
+import Control.Monad.Identity
+import Control.Exception
+import Control.Lens ((^.))
+import Data.List as L
+import Data.Functor
import Data.Time
+import Data.Traversable
+import Data.Text as T
+import Data.ByteString.Lazy as BS
+import Data.Text.Encoding as T
import System.Directory
import System.FilePath
import System.Environment
import System.Console.GetOpt
-import System.Console.Haskeline
-import System.Console.Haskeline.History
import Text.Printf
import Exp.Lex
import Exp.Abs hiding (NoArg)
import Exp.Layout
import Exp.ErrM
+import Prelude as P
-import CTT
+import CTT hiding (def)
import Resolver
import qualified TypeChecker as TC
import qualified Eval as E
-type Interpreter a = InputT IO a
+import Data.Aeson
+import Data.Maybe
+import Data.FileEmbed
+import Reflex.Dom
+import GHCJS.DOM (currentDocumentUnchecked)
+import GHCJS.DOM.Element (getElementsByTagName, setAttribute)
+import GHCJS.DOM.HTMLCollection (itemUnsafe)
+import GHCJS.DOM.Types as DOM hiding (Text, Event)
+import GHCJS.DOM.NonElementParentNode (getElementById)
+import qualified Language.Javascript.JSaddle as JS
--- Flag handling
-data Flag = Debug | Batch | Help | Version | Time
- deriving (Eq,Show)
+import Helpers
-options :: [OptDescr Flag]
-options = [ Option "d" ["debug"] (NoArg Debug) "run in debugging mode"
- , Option "b" ["batch"] (NoArg Batch) "run in batch mode"
- , Option "" ["help"] (NoArg Help) "print help"
- , Option "-t" ["time"] (NoArg Time) "measure time spent computing"
- , Option "" ["version"] (NoArg Version) "print version number" ]
+main :: IO ()
+main = mainWidgetWithHead headWidget bodyWidget
--- Version number, welcome message, usage and prompt strings
-version, welcome, usage, prompt :: String
-version = "1.0"
-welcome = "cubical, version: " ++ version ++ " (:h for help)\n"
-usage = "Usage: cubical [options] <file.ctt>\nOptions:"
-prompt = "> "
+headWidget :: Widget t ()
+headWidget = do
+ elAttr "meta" ("charset" =: "utf-8") blank
+ elAttr "meta" ("http-equiv" =: "x-ua-compatible" <> "content" =: "ie-edge") blank
+ el "title" (text "CubicalTT")
+ elAttr "meta" ("name" =: "viewport"
+ <> "content" =: "width=device-width, initial-scale=1") blank
+ elAttr "link" ("rel" =: "stylesheet"
+ <> "href" =: "https://stackpath.bootstrapcdn.com/bootstrap/4.5.2/css/bootstrap.min.css"
+ <> "integrity" =: "sha384-JcKb8q3iqJ61gNV9KGb8thSsNjpSL0n8PARn9HuZOnIxN0hoP+VmmDGMN5t9UJ0Z"
+ <> "crossorigin" =: "anonymous") blank
+ elAttr "link" ("data-name" =: "vs/editor/editor.main"
+ <> "rel" =: "stylesheet"
+ <> "href" =: "https://microsoft.github.io/monaco-editor/node_modules/monaco-editor/min/vs/editor/editor.main.css") blank
+ el "style" $ text "html, body { height: 100%; }"
-lexer :: String -> [Token]
-lexer = resolveLayout True . myLexer
+bodyWidget :: Widget t ()
+bodyWidget = do
+ elAttr "div" ("class" =: "container-fluid d-flex flex-column" <> "style" =: "min-height: 100%;" ) $ do
+ elClass "div" "row" $ do
+ elClass "div" "col-7 mt-2" $ do
+ elClass "ul" "nav nav-tabs" $ do
+ elClass "li" "nav-item" $
+ elAttr "a" ("id" =: "welcome-tab"
+ <> "href" =: "#" <> "class" =: "nav-link tab-link active") $ text "welcome"
+ elClass "li" "nav-item" $
+ elAttr "a" ("id" =: "lecture1-tab"
+ <> "href" =: "#" <> "class" =: "nav-link tab-link") $ text "lecture1"
+ elClass "li" "nav-item" $
+ elAttr "a" ("id" =: "lecture2-tab"
+ <>"href" =: "#" <> "class" =: "nav-link tab-link") $ text "lecture2"
+ elClass "li" "nav-item" $
+ elAttr "a" ("id" =: "lecture3-tab"
+ <> "href" =: "#" <> "class" =: "nav-link tab-link") $ text "lecture3"
+ elClass "li" "nav-item" $
+ elAttr "a" ("id" =: "lecture4-tab"
+ <> "href" =: "#" <> "class" =: "nav-link tab-link") $ text "lecture4"
+ elClass "div" "row flex-grow-1" $ do
+ elClass "div" "col-7 flex-grow-1" $ do
+ elAttr "div" ("id" =: "editor" <> "class" =: "flex-grow-1"
+ <> "style" =: "width:auto;height:600px;border:1px solid grey") blank
+ elClass "div" "col-5 pl-0 flex-grow-1" $ do
+ elAttr "div" ("class" =: "col-md flex-grow-1" <> "id" =: "results-container"
+ <> "style" =: "width:auto;height:600px;border:1px solid grey;overflow-x:scroll;") $
+ el "pre" $ elAttr "code" ("id" =: "results") blank
+ elClass "div" "col-*-* w-100" $ do
+ elClass "div" "input-group mb-3" $ do
+ elClass "div" "input-group-prepend" $
+ elClass "span" "input-group-text" $ text ">"
+ elAttr "input" ("id" =: "eval-input"
+ <> "type" =: "text"
+ <> "class" =: "form-control"
+ <> "style" =: "box-shadow: none;") blank
+ elClass "div" "input-group-append" $
+ elAttr "button" ("id" =: "eval-button" <> "type" =: "button"
+ <> "class" =: "btn btn-outline-secondary") $ text "Eval"
+ let
+ vsPath = "https://microsoft.github.io/monaco-editor/node_modules/monaco-editor/min/vs/"
+ el "script" $ text $ "var app = {}; var require = { paths: { 'vs': '" <> vsPath <> "'} };"
+ elAttr "script" ("src" =: (vsPath <> "loader.js")) blank
+ elAttr "script" ("src" =: (vsPath <> "editor/editor.main.nls.js")) blank
+ elAttr "script" ("src" =: (vsPath <> "editor/editor.main.js")) blank
+ DOM.liftJSM $ do
+ setupEditorJS <- JS.eval editorSetupScript
+ void $ JS.call setupEditorJS setupEditorJS
+ [ toJSVal welcomeContent
+ , toJSVal lecture1Content
+ , toJSVal lecture2Content
+ , toJSVal lecture3Content
+ , toJSVal lecture4Content
+ , toJSVal (JS.fun loadHandler), toJSVal (JS.fun evalHandler)]
-showTree :: (Show a, Print a) => a -> IO ()
-showTree tree = do
- putStrLn $ "\n[Abstract Syntax]\n\n" ++ show tree
- putStrLn $ "\n[Linearized tree]\n\n" ++ printTree tree
+evalHandler :: JSVal -> JSVal -> [JSVal] -> JSM ()
+evalHandler _ _ [tabName, inputContent] = do
+ currentTabName <- JS.valToText tabName
+ mCache <- loadTabCache "repl"
+ case mCache of
+ Just (names, tenv) -> do
+ val <- JS.valToText inputContent
+ evalInput names tenv val
+ _ -> do
+ writeLogAndScroll $ "Couldn't load the cache for REPL. Please, try to load the buffer\n"
--- Used for auto completion
-searchFunc :: [String] -> String -> [Completion]
-searchFunc ns str = map simpleCompletion $ filter (str `isPrefixOf`) ns
+allTabsNames :: [Text]
+allTabsNames =
+ [ "welcome"
+ , "lecture1"
+ , "lecture2"
+ , "lecture3"
+ , "lecture4"]
-settings :: [String] -> Settings IO
-settings ns = Settings
- { historyFile = Nothing
- , complete = completeWord Nothing " \t" $ return . searchFunc ns
- , autoAddHistory = True }
+loadTabContent :: Text -> JSM TabWithContent
+loadTabContent name = do
+ loadTabContentJS <- JS.eval $ T.unlines
+ [ "(function(name) {"
+ , " return app.tabs[name + '-tab'][0].getValue();"
+ , "})"
+ ]
+ tabContentVal <- JS.call loadTabContentJS loadTabContentJS [toJSVal name]
+ val <- JS.valToText tabContentVal
+ return (name, val)
-main :: IO ()
-main = do
- args <- getArgs
- case getOpt Permute options args of
- (flags,files,[])
- | Help `elem` flags -> putStrLn $ usageInfo usage options
- | Version `elem` flags -> putStrLn version
- | otherwise -> case files of
- [] -> do
- putStrLn welcome
- runInputT (settings []) (loop flags [] [] TC.verboseEnv)
- [f] -> do
- putStrLn welcome
- putStrLn $ "Loading " ++ show f
- initLoop flags f emptyHistory
- _ -> putStrLn $ "Input error: zero or one file expected\n\n" ++
- usageInfo usage options
- (_,_,errs) -> putStrLn $ "Input error: " ++ concat errs ++ "\n" ++
- usageInfo usage options
-
-shrink :: String -> String
-shrink s = s -- if length s > 1000 then take 1000 s ++ "..." else s
-
--- Initialize the main loop
-initLoop :: [Flag] -> FilePath -> History -> IO ()
-initLoop flags f hist = do
- -- Parse and type check files
- (_,_,mods) <- E.catch (imports True ([],[],[]) f)
- (\e -> do putStrLn $ unlines $
- ("Exception: " :
- (takeWhile (/= "CallStack (from HasCallStack):")
- (lines $ show (e :: SomeException))))
- return ([],[],[]))
- -- Translate to TT
- let res = runResolver $ resolveModules mods
- case res of
- Left err -> do
- putStrLn $ "Resolver failed: " ++ err
- runInputT (settings []) (putHistory hist >> loop flags f [] TC.verboseEnv)
+loadAllTabs :: JSM [TabWithContent]
+loadAllTabs = do
+ tabsContentVals <- traverse loadTabContent allTabsNames
+ tabsContent <- traverse JS.valToText tabsContentVals
+ return $ P.zip allTabsNames tabsContent
+
+loadTabCache :: Text -> JSM (Maybe CheckedModule)
+loadTabCache tabName = do
+ mNames :: Maybe Names <-
+ loadDataFromLocalStorage ("load-results-names-" <> tabName)
+ mImports :: Maybe TC.TEnv <-
+ loadDataFromLocalStorage ("load-results-imports-" <> tabName)
+ case (mNames, mImports) of
+ (Just names, Just imports) -> pure $ Just (names, imports)
+ _ -> pure Nothing
+
+loadHandler :: JSVal -> JSVal -> [JSVal] -> JSM ()
+loadHandler _ _ [tabNameVal, contentVal] = do
+ currentTabName <- JS.valToText tabNameVal
+ currentInput <- JS.valToText contentVal
+ (_, _, loadedMods) <- processImports ([],[],[]) (currentTabName, currentInput)
+ initLoop loadedMods
+
+getModule :: TabWithContent -> JSM (Maybe Module)
+getModule (tabName, input) = do
+ -- mModule <- loadDataFromLocalStorage $ "cache-module-" <> tabName
+ -- case mModule of
+ -- Just m -> return $ Just m
+ -- Nothing -> do
+ let
+ ts = lexer $ T.unpack input
+ case pModule ts of
+ Bad s -> do
+ writeLogAndScroll $ T.pack $
+ "Parse failed in " ++ show tabName ++ "\n" ++ show s ++ "\n"
+ return Nothing
+ Ok mod -> do
+ -- saveDataToLocalStorage ("cache-module-" <> tabName) mod
+ return $ Just mod
+
+processImports
+ :: ([Text],[String],[Module])
+ -> TabWithContent
+ -> JSM ([Text],[String],[Module])
+processImports st@(notok,loaded,mods) twc@(tabName, input) = do
+ mMod <- getModule twc
+ case mMod of
+ Nothing -> return st
+ Just mod@(Module (AIdent (_,name)) imp decls) -> do
+ let
+ importModsNames = [T.pack i | Import (AIdent (_,i)) <- imp]
+ importMods <- traverse loadTabContent $
+ P.filter (\i -> i `P.elem` allTabsNames) importModsNames
+ if (name /= T.unpack tabName) then do
+ writeLogAndScroll $ T.pack $ "Module name mismatch in "
+ ++ show tabName ++ " with wrong name " ++ name
+ return st
+ else do
+ (notok1,loaded1,mods1) <- foldM processImports (tabName:notok,loaded,mods) importMods
+ return (notok,loaded1,mods1 ++ [mod])
+
+-- cubicaltt functions
+type Names = [(CTT.Ident,SymKind)]
+
+type TabWithContent = (Text, Text)
+
+type CheckedModule = (Names, TC.TEnv)
+
+initLoop
+ :: [Module]
+ -> JSM ()
+initLoop [] = pure ()
+initLoop mods = do
+ case runResolver $ resolveModules mods of
+ Left err ->
+ writeLogAndScroll $ T.pack $ "Resolver failed: " ++ err ++ "\n"
Right (adefs,names) -> do
- -- After resolivng the file check if some definitions were shadowed:
- let ns = map fst names
- uns = nub ns
- dups = ns \\ uns
+ let ns = fmap fst names
+ dups = ns \\ nub ns
unless (dups == []) $
- putStrLn $ "Warning: the following definitions were shadowed [" ++
- intercalate ", " dups ++ "]"
- (merr,tenv) <- TC.runDeclss TC.verboseEnv adefs
- case merr of
- Just err -> putStrLn $ "Type checking failed: " ++ shrink err
- Nothing -> unless (mods == []) $ putStrLn "File loaded."
- if Batch `elem` flags
- then return ()
- else -- Compute names for auto completion
- runInputT (settings [n | (n,_) <- names])
- (putHistory hist >> loop flags f names tenv)
-
--- The main loop
-loop :: [Flag] -> FilePath -> [(CTT.Ident,SymKind)] -> TC.TEnv -> Interpreter ()
-loop flags f names tenv = do
- input <- getInputLine prompt
- case input of
- Nothing -> outputStrLn help >> loop flags f names tenv
- Just ":q" -> return ()
- Just ":r" -> getHistory >>= lift . initLoop flags f
- Just (':':'l':' ':str)
- | ' ' `elem` str -> do outputStrLn "Only one file allowed after :l"
- loop flags f names tenv
- | otherwise -> getHistory >>= lift . initLoop flags str
- Just (':':'c':'d':' ':str) -> do lift (setCurrentDirectory str)
- loop flags f names tenv
- Just ":h" -> outputStrLn help >> loop flags f names tenv
- Just str' ->
- let (msg,str,mod) = case str' of
- (':':'n':' ':str) ->
- ("NORMEVAL: ",str,E.normal [])
- str -> ("EVAL: ",str,id)
- in case pExp (lexer str) of
- Bad err -> outputStrLn ("Parse error: " ++ err) >> loop flags f names tenv
- Ok exp ->
- case runResolver $ local (insertIdents names) $ resolveExp exp of
- Left err -> do outputStrLn ("Resolver failed: " ++ err)
- loop flags f names tenv
- Right body -> do
- x <- liftIO $ TC.runInfer tenv body
- case x of
- Left err -> do outputStrLn ("Could not type-check: " ++ err)
- loop flags f names tenv
- Right _ -> do
- start <- liftIO getCurrentTime
- let e = mod $ E.eval (TC.env tenv) body
- -- Let's not crash if the evaluation raises an error:
- liftIO $ catch (putStrLn (msg ++ shrink (show e)))
- -- (writeFile "examples/nunivalence3.ctt" (show e))
- (\e -> putStrLn ("Exception: " ++
- show (e :: SomeException)))
- stop <- liftIO getCurrentTime
- -- Compute time and print nicely
- let time = diffUTCTime stop start
- secs = read (takeWhile (/='.') (init (show time)))
- rest = read ('0':dropWhile (/='.') (init (show time)))
- mins = secs `quot` 60
- sec = printf "%.3f" (fromInteger (secs `rem` 60) + rest :: Float)
- when (Time `elem` flags) $
- outputStrLn $ "Time: " ++ show mins ++ "m" ++ sec ++ "s"
- -- Only print in seconds:
- -- when (Time `elem` flags) $ outputStrLn $ "Time: " ++ show time
- loop flags f names tenv
-
--- (not ok,loaded,already loaded defs) -> to load ->
--- (new not ok, new loaded, new defs)
--- the bool determines if it should be verbose or not
-imports :: Bool -> ([String],[String],[Module]) -> String ->
- IO ([String],[String],[Module])
-imports v st@(notok,loaded,mods) f
- | f `elem` notok = error ("Looping imports in " ++ f)
- | f `elem` loaded = return st
- | otherwise = do
- b <- doesFileExist f
- when (not b) $ error (f ++ " does not exist")
- let prefix = dropFileName f
- s <- readFile f
- let ts = lexer s
- case pModule ts of
- Bad s -> error ("Parse failed in " ++ show f ++ "\n" ++ show s)
- Ok mod@(Module (AIdent (_,name)) imp decls) -> do
- let imp_ctt = [prefix ++ i ++ ".ctt" | Import (AIdent (_,i)) <- imp]
- when (name /= dropExtension (takeFileName f)) $
- error ("Module name mismatch in " ++ show f ++ " with wrong name " ++ name)
- (notok1,loaded1,mods1) <-
- foldM (imports v) (f:notok,loaded,mods) imp_ctt
- when v $ putStrLn $ "Parsed " ++ show f ++ " successfully!"
- return (notok,f:loaded1,mods1 ++ [mod])
-
-help :: String
-help = "\nAvailable commands:\n" ++
- " <statement> infer type and evaluate statement\n" ++
- " :n <statement> normalize statement\n" ++
- " :q quit\n" ++
- " :l <filename> loads filename (and resets environment before)\n" ++
- " :cd <path> change directory to path\n" ++
- " :r reload\n" ++
- " :h display this message\n"
+ writeLogAndScroll $ T.pack $ "Warning: the following definitions were shadowed [" ++
+ L.intercalate ", " dups ++ "]\n"
+ saveDataToLocalStorage "load-results-names-repl" names
+ saveDataToLocalStorage "decls-to-process" adefs
+ TC.runDeclss' TC.verboseEnv
+
+evalInput :: Names -> TC.TEnv -> Text -> JSM ()
+evalInput names tenv input = do
+ writeLogAndScroll $ "> " <> input <> "\n"
+ let
+ (msg, str, mod) = if T.isInfixOf ":n" input
+ then ("NORMEVAL: ", T.drop 2 input, E.normal [])
+ else ("EVAL: ", input, id)
+ case pExp (lexer $ T.unpack str) of
+ Bad err -> writeLogAndScroll $ T.pack $ ("Parse error: " ++ err) <> "\n"
+ Ok exp -> case runResolver $ local (insertIdents names) $ resolveExp exp of
+ Left err -> writeLogAndScroll $ T.pack $ ("Resolver failed: " ++ err) <> "\n"
+ Right body -> do
+ x <- TC.runInfer tenv body
+ case x of
+ Left err -> writeLogAndScroll $ T.pack $ ("Could not type-check: " ++ err) <> "\n"
+ Right _ -> do
+ let
+ e = mod $ E.eval (TC.env tenv) body
+ writeLogAndScroll $ msg <> (T.pack $ show e) <> "\n"
+
+lexer :: String -> [Token]
+lexer = resolveLayout True . myLexer
+
+-- files
+
+welcomeContent :: Text
+welcomeContent = decodeUtf8 $ $(embedFile "welcome.ctt")
+
+lecture1Content :: Text
+lecture1Content = decodeUtf8 $ $(embedFile "lectures/lecture1.ctt")
+
+lecture2Content :: Text
+lecture2Content = decodeUtf8 $ $(embedFile "lectures/lecture2.ctt")
+
+lecture3Content :: Text
+lecture3Content = decodeUtf8 $ $(embedFile "lectures/lecture3.ctt")
+
+lecture4Content :: Text
+lecture4Content = decodeUtf8 $ $(embedFile "lectures/lecture4.ctt")
+
+editorSetupScript :: Text
+editorSetupScript = decodeUtf8 $ $(embedFile "setup.js")
\ No newline at end of file
-- | Convert the concrete syntax into the syntax of cubical TT.
module Resolver where
+import Data.Aeson
+import GHC.Generics (Generic)
import Control.Applicative
import Control.Monad
import Control.Monad.Reader
-- | Resolver and environment
data SymKind = Variable | Constructor | PConstructor | Name
- deriving (Eq,Show)
+ deriving (Eq, Show, Generic, ToJSON, FromJSON)
-- local environment for constructors
data Env = Env { envModule :: String,
variables :: [(Ident,SymKind)] }
- deriving (Eq,Show)
+ deriving (Eq, Show)
type Resolver a = ReaderT Env (ExceptT String Identity) a
+++ /dev/null
-import Distribution.Simple
-import Distribution.Simple.Program
-import System.Process (system)
-
-main :: IO ()
-main = defaultMainWithHooks $ simpleUserHooks {
- hookedPrograms = [bnfc],
- preBuild = \args buildFlags -> do
- _ <- system "bnfc --haskell -d Exp.cf"
- preBuild simpleUserHooks args buildFlags
-}
-
-bnfc :: Program
-bnfc = (simpleProgram "bnfc") {
- programFindVersion = findProgramVersion "--version" id
- }
+{-# LANGUAGE BangPatterns #-}\r
{-# LANGUAGE TupleSections #-}\r
module TypeChecker where\r
\r
+import Data.Aeson\r
+import GHC.Generics (Generic)\r
+\r
import Control.Applicative hiding (empty)\r
import Control.Monad\r
import Control.Monad.Except\r
+import Control.Monad.Identity\r
import Control.Monad.Reader\r
import Data.Map (Map,(!),mapWithKey,assocs,filterWithKey,elems,keys\r
,intersection,intersectionWith,intersectionWithKey\r
,toList,fromList)\r
import qualified Data.Map as Map\r
-import qualified Data.Traversable as T\r
+import qualified Data.Traversable as Trav\r
+import Data.Text (Text)\r
+import qualified Data.Text as T\r
\r
import Connections\r
import CTT\r
import Eval\r
+import GHCJS.DOM.Types as DOM hiding (Text, Event)\r
+import qualified Language.Javascript.JSaddle as JS\r
+import Helpers\r
\r
-- Type checking monad\r
-type Typing a = ReaderT TEnv (ExceptT String IO) a\r
+type Typing a = ReaderT TEnv (ExceptT String JSM) a\r
\r
-- Environment for type checker\r
data TEnv =\r
, indent :: Int\r
, env :: Env\r
, verbose :: Bool -- Should it be verbose and print what it typechecks?\r
- } deriving (Eq)\r
+ } deriving (Eq, Generic, ToJSON, FromJSON)\r
\r
verboseEnv, silentEnv :: TEnv\r
verboseEnv = TEnv [] 0 emptyEnv True\r
silentEnv = TEnv [] 0 emptyEnv False\r
\r
--- Trace function that depends on the verbosity flag\r
-trace :: String -> Typing ()\r
-trace s = do\r
- b <- asks verbose\r
- when b $ liftIO (putStrLn s)\r
-\r
-------------------------------------------------------------------------------\r
-- | Functions for running computations in the type checker monad\r
\r
-runTyping :: TEnv -> Typing a -> IO (Either String a)\r
-runTyping env t = runExceptT $ runReaderT t env\r
+runTyping :: TEnv -> Typing a -> JSM (Either String a)\r
+runTyping !env !t = runExceptT $ runReaderT t env\r
\r
-runDecls :: TEnv -> Decls -> IO (Either String TEnv)\r
-runDecls tenv d = runTyping tenv $ do\r
- checkDecls d\r
+runDecls :: TEnv -> Decls -> JSM (Either String TEnv)\r
+runDecls !tenv !d = runTyping tenv $ do\r
+ !_ <- checkDecls $! d\r
return $ addDecls d tenv\r
\r
-runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv)\r
-runDeclss tenv [] = return (Nothing, tenv)\r
-runDeclss tenv (d:ds) = do\r
- x <- runDecls tenv d\r
+runDeclss :: TEnv -> [Decls] -> JSM (Maybe String, TEnv)\r
+runDeclss !tenv [] = return (Nothing, tenv)\r
+runDeclss !tenv !(d:ds) = do\r
+ consoleLog "runDeclss"\r
+ !x <- runDecls tenv d\r
case x of\r
- Right tenv' -> runDeclss tenv' ds\r
- Left s -> return (Just s, tenv)\r
-\r
-runInfer :: TEnv -> Ter -> IO (Either String Val)\r
-runInfer lenv e = runTyping lenv (infer e)\r
+ Right !tenv' -> do\r
+ runDeclss tenv' ds\r
+ Left s -> return (Just s, tenv)\r
+\r
+-- new, better runDeclss, with setTimeout to give browser thread time\r
+-- to render the type checking results\r
+runDeclss' :: TEnv -> JSM ()\r
+runDeclss' !tenv = do\r
+ mDecls <- loadDataFromLocalStorage "decls-to-process"\r
+ case mDecls :: Maybe [Decls] of\r
+ Nothing ->\r
+ writeLogAndScroll "Unexpected error: not found decls to type check.\n"\r
+ Just [] -> do\r
+ saveDataToLocalStorage "load-results-imports-repl" tenv\r
+ writeLogAndScroll "File loaded.\n"\r
+ Just (d:ds) -> do\r
+ !x <- runDecls tenv d\r
+ case x of\r
+ Right !tenv' -> do\r
+ saveDataToLocalStorage "decls-to-process" ds\r
+ f <- toJSVal $ JS.fun $ \ _ _ _ -> runDeclss' tenv'\r
+ setTimeout f 10\r
+ Left s -> do\r
+ removeLocalStorage "load-results-names-repl"\r
+ removeLocalStorage "load-results-imports-repl"\r
+ writeLogAndScroll $ T.pack ("Type checking failed: " ++ s ++ "\n")\r
+\r
+runInfer :: TEnv -> Ter -> JSM (Either String Val)\r
+runInfer !lenv !e = runTyping lenv (infer e)\r
\r
-------------------------------------------------------------------------------\r
-- | Modifiers for the environment\r
TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds nvs rho) v\r
\r
addDecls :: Decls -> TEnv -> TEnv\r
-addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v\r
+addDecls !d !(TEnv ns ind rho v) = TEnv ns ind (def d rho) v\r
\r
addTele :: Tele -> TEnv -> TEnv\r
addTele xas lenv = foldl (flip addType) lenv xas\r
\r
-- Check that t has type a\r
check :: Val -> Ter -> Typing ()\r
-check a t = case (a,t) of\r
- (_,Undef{}) -> return ()\r
- (_,Hole l) -> do\r
+check !a !t = case (a,t) of\r
+ !(_,Undef{}) -> return ()\r
+ !(_,Hole l) -> do\r
rho <- asks env\r
let e = unlines (reverse (contextOfEnv rho))\r
ns <- asks names\r
- trace $ "\nHole at " ++ show l ++ ":\n\n" ++\r
- e ++ replicate 80 '-' ++ "\n" ++ show (normal ns a) ++ "\n"\r
- (_,Con c es) -> do\r
+ liftJSM $! writeLogAndScroll $ T.pack $ "\nHole at " ++ show l ++ ":\n\n" ++\r
+ e ++ replicate 80 '-' ++ "\n" ++ show (normal ns a) ++ "\n"\r
+ pure ()\r
+ !(_,Con c es) -> do\r
(bs,nu) <- getLblType c a\r
checks (bs,nu) es\r
- (VU,Pi f) -> checkFam f\r
- (VU,Sigma f) -> checkFam f\r
- (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
+ !(VU,Pi f) -> checkFam f\r
+ !(VU,Sigma f) -> checkFam f\r
+ !(VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
OLabel _ tele -> checkTele tele\r
PLabel _ tele is ts ->\r
throwError $ "check: no path constructor allowed in " ++ show t\r
- (VU,HSum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
+ !(VU,HSum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
OLabel _ tele -> checkTele tele\r
PLabel _ tele is ts -> do\r
checkTele tele\r
check (Ter t rho) talpha\r
rho' <- asks env\r
checkCompSystem (evalSystem rho' ts)\r
- (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do\r
+ !(VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do\r
check VU ty\r
rho <- asks env\r
unlessM (a === eval rho ty) $ throwError "check: split annotations"\r
then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va\r
| (brc, lbl) <- zip ces cas ]\r
else throwError "case branches does not match the data type"\r
- (VPi va@(Ter (HSum _ _ cas) nu) f,Split _ _ ty ces) -> do\r
+ !(VPi va@(Ter (HSum _ _ cas) nu) f,Split _ _ ty ces) -> do\r
check VU ty\r
rho <- asks env\r
unlessM (a === eval rho ty) $ throwError "check: split annotations"\r
then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va\r
| (brc, lbl) <- zip ces cas ]\r
else throwError "case branches does not match the data type"\r
- (VPi a f,Lam x a' t) -> do\r
+ !(VPi a f,Lam x a' t) -> do\r
check VU a'\r
ns <- asks names\r
rho <- asks env\r
let var = mkVarNice ns x a\r
\r
local (addTypeVal (x,a)) $ check (app f var) t\r
- (VSigma a f, Pair t1 t2) -> do\r
+ !(VSigma a f, Pair t1 t2) -> do\r
check a t1\r
v <- evalTyping t1\r
check (app f v) t2\r
- (_,Where e d) -> do\r
+ !(_,Where e d) -> do\r
local (\tenv@TEnv{indent=i} -> tenv{indent=i + 2}) $ checkDecls d\r
local (addDecls d) $ check a e\r
- (VU,PathP a e0 e1) -> do\r
+ !(VU,PathP a e0 e1) -> do\r
(a0,a1) <- checkPLam (constPath VU) a\r
check a0 e0\r
check a1 e1\r
- (VPathP p a0 a1,PLam _ e) -> do\r
+ !(VPathP p a0 a1,PLam _ e) -> do\r
(u0,u1) <- checkPLam p t\r
ns <- asks names\r
unless (conv ns a0 u0 && conv ns a1 u1) $\r
throwError $ "path endpoints don't match for " ++ show e ++ ", got " ++\r
show (u0,u1) ++ ", but expected " ++ show (a0,a1)\r
- (VU,Glue a ts) -> do\r
+ !(VU,Glue a ts) -> do\r
check VU a\r
rho <- asks env\r
checkGlue (eval rho a) ts\r
- (VGlue va ts,GlueElem u us) -> do\r
+ !(VGlue va ts,GlueElem u us) -> do\r
check va u\r
vu <- evalTyping u\r
checkGlueElem vu ts us\r
- (VCompU va ves,GlueElem u us) -> do\r
+ !(VCompU va ves,GlueElem u us) -> do\r
check va u\r
vu <- evalTyping u\r
checkGlueElemU vu ves us\r
- (VU,Id a a0 a1) -> do\r
+ !(VU,Id a a0 a1) -> do\r
check VU a\r
- va <- evalTyping a\r
+ !va <- evalTyping a\r
check va a0\r
check va a1\r
- (VId va va0 va1,IdPair w ts) -> do\r
+ !(VId va va0 va1,IdPair w ts) -> do\r
check (VPathP (constPath va) va0 va1) w\r
- vw <- evalTyping w\r
+ !vw <- evalTyping w\r
checkSystemWith ts $ \alpha tAlpha ->\r
local (faceEnv alpha) $ do\r
check (va `face` alpha) tAlpha\r
throwError "malformed eqC"\r
rho <- asks env\r
checkCompSystem (evalSystem rho ts) -- Not needed\r
- _ -> do\r
- v <- infer t\r
+ !_ -> do\r
+ !v <- infer t\r
unlessM (v === a) $\r
throwError $ "check conv:\n" ++ show v ++ "\n/=\n" ++ show a\r
\r
-- Check a list of declarations\r
checkDecls :: Decls -> Typing ()\r
checkDecls (MutualDecls _ []) = return ()\r
-checkDecls (MutualDecls l d) = do\r
+checkDecls !(MutualDecls l d) = do\r
a <- asks env\r
- let (idents,tele,ters) = (declIdents d,declTele d,declTers d)\r
- ind <- asks indent\r
- trace (replicate ind ' ' ++ "Checking: " ++ unwords idents)\r
- checkTele tele\r
- local (addDecls (MutualDecls l d)) $ do\r
+ let !(idents,tele,ters) = (declIdents d,declTele d,declTers d)\r
+ !ind <- asks indent\r
+ liftJSM $! writeLogAndScroll $!\r
+ T.pack $! replicate ind ' ' ++ "Checking: " ++ unwords idents ++ "\n"\r
+ checkTele $! tele\r
+ local (addDecls $! (MutualDecls l d)) $ do\r
rho <- asks env\r
checks (tele,rho) ters\r
checkDecls (OpaqueDecl _) = return ()\r
local (addSub (i,Atom i)) $ check (v @@ i) a\r
return (eval (sub (i,Dir 0) rho) a,eval (sub (i,Dir 1) rho) a)\r
checkPLam v t = do\r
- vt <- infer t\r
+ !vt <- infer t\r
case vt of\r
VPathP a a0 a1 -> do\r
unlessM (a === v) $ throwError (\r
checkPLamSystem :: Ter -> Val -> System Ter -> Typing (System Val)\r
checkPLamSystem t0 va ps = do\r
rho <- asks env\r
- v <- T.sequence $ mapWithKey (\alpha pAlpha ->\r
+ v <- Trav.sequence $ mapWithKey (\alpha pAlpha ->\r
local (faceEnv alpha) $ do\r
rhoAlpha <- asks env\r
(a0,a1) <- checkPLam (va `face` alpha) pAlpha\r
U -> return VU -- U : U\r
Var n -> lookType n <$> asks env\r
App t u -> do\r
- c <- infer t\r
+ !c <- infer t\r
case c of\r
VPi a f -> do\r
check a u\r
return $ app f v\r
_ -> throwError $ show c ++ " is not a product"\r
Fst t -> do\r
- c <- infer t\r
+ !c <- infer t\r
case c of\r
VSigma a f -> return a\r
_ -> throwError $ show c ++ " is not a sigma-type"\r
Snd t -> do\r
- c <- infer t\r
+ !c <- infer t\r
case c of\r
VSigma a f -> do\r
v <- evalTyping t\r
checkDecls d\r
local (addDecls d) $ infer t\r
UnGlueElem e _ -> do\r
- t <- infer e\r
+ !t <- infer e\r
case t of\r
VGlue a _ -> return a\r
_ -> throwError (show t ++ " is not a Glue")\r
AppFormula e phi -> do\r
checkFormula phi\r
- t <- infer e\r
+ !t <- infer e\r
case t of\r
VPathP a _ _ -> return $ a @@ phi\r
_ -> throwError (show e ++ " is not a path")\r
Comp a t0 ps -> do\r
(va0, va1) <- checkPLam (constPath VU) a\r
- va <- evalTyping a\r
+ !va <- evalTyping a\r
check va0 t0\r
checkPLamSystem t0 va ps\r
return va1\r
HComp a u0 us -> do\r
check VU a\r
- va <- evalTyping a\r
+ !va <- evalTyping a\r
check va u0\r
checkPLamSystem u0 (constPath va) us\r
return va\r
Fill a t0 ps -> do\r
(va0, va1) <- checkPLam (constPath VU) a\r
- va <- evalTyping a\r
+ !va <- evalTyping a\r
check va0 t0\r
checkPLamSystem t0 va ps\r
- vt <- evalTyping t0\r
+ !vt <- evalTyping t0\r
rho <- asks env\r
let vps = evalSystem rho ps\r
return (VPathP va vt (compLine va vt vps))\r
PCon c a es phis -> do\r
check VU a\r
- va <- evalTyping a\r
+ !va <- evalTyping a\r
(bs,nu) <- getLblType c va\r
checks (bs,nu) es\r
mapM_ checkFormula phis\r
return va\r
IdJ a u c d x p -> do\r
check VU a\r
- va <- evalTyping a\r
+ !va <- evalTyping a\r
check va u\r
- vu <- evalTyping u\r
+ !vu <- evalTyping u\r
let refu = VIdPair (constPath vu) $ mkSystem [(eps,vu)]\r
rho <- asks env\r
let z = Var "z"\r
ctype = eval rho $ Pi $ Lam "z" a $ Pi $ Lam "_" (Id a u z) U\r
check ctype c\r
- vc <- evalTyping c\r
+ !vc <- evalTyping c\r
check (app (app vc vu) refu) d\r
check va x\r
- vx <- evalTyping x\r
+ !vx <- evalTyping x\r
check (VId va vu vx) p\r
- vp <- evalTyping p\r
+ !vp <- evalTyping p\r
return (app (app vc vx) vp)\r
_ -> throwError ("infer " ++ show e)\r
\r
--- /dev/null
+packages:
+ ./
\ No newline at end of file
maintainer:
-- copyright:
category: Language
-build-type: Custom
+build-type: Simple
extra-source-files: Makefile, README.md, Exp.cf, examples/*.ctt, cubicaltt.el
cabal-version: >=1.10
Eval,
Resolver,
TypeChecker,
+ Helpers,
Exp.Abs,
Exp.ErrM,
Exp.Layout,
Exp.Lex,
Exp.Par,
Exp.Print,
- Exp.Skel,
- Exp.Test
+ Exp.Skel
+ default-extensions:
+ OverloadedStrings,
+ DeriveAnyClass,
+ DeriveGeneric
other-extensions:
TypeSynonymInstances,
FlexibleInstances,
MagicHash
build-depends:
base >=4.6 && <5,
- containers >=0.5 && <0.6,
+ containers,
pretty >=1.1 && <1.2,
- QuickCheck >=2.6 && <2.10,
+ QuickCheck,
mtl >=2.2 && <2.3,
- time >=1.4 && <1.7,
+ time,
directory >=1.2 && <1.4,
filepath >=1.4 && <1.5,
- haskeline >=0.7 && <0.8,
array >=0.4 && <0.6,
- -- Build tool
- BNFC >=2.8.1 && <3.0
+ reflex-dom,
+ ghcjs-dom,
+ text,
+ jsaddle,
+ lens,
+ file-embed,
+ aeson,
+ bytestring
-- hs-source-dirs:
- build-tools: alex, happy, bnfc
+ build-tools: alex, happy
default-language: Haskell2010
+ ghc-options: -threaded
+ if os(darwin)
+ ghc-options: -dynamic
+ if impl(ghcjs)
+ ghc-options: -dedupe
\ No newline at end of file
--- /dev/null
+reflex-platform-args:
+
+let
+ reflexPlatformSrc = builtins.fetchTarball {
+ url = "https://github.com/reflex-frp/reflex-platform/archive/df0bdcca5eb2a3236ec0496e4430d91876b29cf5.tar.gz";
+ };
+
+ ghcjsIgnoreOverrides = self: super:
+ let
+ ignore = {
+ haskeline = null;
+ };
+ in if (super.ghc.isGhcjs or false) then ignore else {};
+
+haskellOverlaysPre = (reflex-platform-args.haskellOverlaysPre or [ ])
+ ++ [ ];
+
+ haskellOverlaysPost = (reflex-platform-args.haskellOverlaysPost or [ ])
+ ++ [ ghcjsIgnoreOverrides ];
+
+ config = { allowBroken = true; };
+
+ reflex-platform = import reflexPlatformSrc (reflex-platform-args // {
+ inherit config haskellOverlaysPre haskellOverlaysPost;
+ });
+
+in reflex-platform.project ({ pkgs, ... }: {
+ useWarp = true;
+ withHoogle = false;
+
+ packages = {
+ cubicaltt = ./.;
+ };
+
+ shells = {
+ ghc = ["cubicaltt"];
+ ghcjs = ["cubicaltt"];
+ };
+
+ shellToolOverrides = ghc: super: {
+ closure-compiler = null;
+ haskell-ide-engine = null;
+ hdevtools = null;
+ hlint = null;
+ stylish-haskell = null;
+ ghcid = if pkgs.stdenv.isDarwin then null else super.ghcid;
+ cabal-install = null;
+ };
+})
\ No newline at end of file
--- /dev/null
+Subproject commit df0bdcca5eb2a3236ec0496e4430d91876b29cf5
--- /dev/null
+(function(welcomeContent, lecture1Content, lecture2Content, lecture3Content, lecture4Content, loadHandler, evalHandler) {
+ setTimeout(function(){
+ //setup editor
+ require(['vs/editor/editor.main'], function() {
+ monaco.languages.register({ id: 'cubicaltt' });
+ monaco.languages.setMonarchTokensProvider('cubicaltt', {
+ keywords: [
+ 'hdata', 'data', 'import', 'mutual', 'let', 'in'
+ , 'split', 'with', 'module', 'where', 'U', 'opaque'
+ , 'transparent', 'transparent_all', 'token'
+ ],
+ operations:
+ [ 'PathP', 'comp', 'transport', 'fill', 'Glue'
+ , 'glue', 'unglue', 'Id', 'idC', 'id' ],
+ operators:
+ [ ':', '->', '=', '|', '\/', '/\\', '\\', '*', '_', '<', '>', '@', '-' ],
+ symbols: /[=><!~?:&|+\-*\/\^%]+/,
+ tokenizer: {
+ root: [
+ [ /[A-Za-z_$][\w$]*/, { cases:
+ { '@keywords': 'keyword',
+ '@operations': 'operation',
+ '@default': 'identifier' }
+ }
+ ],
+
+ ['undefined', 'special'],
+
+ [/\\\//, 'operator'],
+ [/\\/, 'operator'],
+ [/\/\\/, 'operator'],
+
+ { include: '@whitespace' },
+
+ [/@symbols/, { cases: { '@operators': 'operator',
+ '@default' : '' } } ],
+ ],
+ comment: [
+ [/[^-}]+/, 'comment' ],
+ ['-}', 'comment', '@pop' ],
+ [/[-}]/, 'comment' ]
+ ],
+ whitespace: [
+ [/[\\t\\r\\n]+/, 'white'],
+ [/\{-/, 'comment', '@comment' ],
+ [/--.*$/, 'comment'],
+ ],
+ }
+ });
+ // create theme
+ monaco.editor.defineTheme('cubicaltt', {
+ base: 'vs',
+ inherit: false,
+ rules: [
+ { token: 'keyword', foreground: '952795' },
+ { token: 'operation', foreground: '483d8b' },
+ { token: 'operator', foreground: 'a0522d' },
+ { token: 'special', foreground: 'ff2500' },
+ { token: 'comment', foreground: 'b22222' }
+ ]});
+ // language config
+ monaco.languages.setLanguageConfiguration('cubicaltt', {
+ comments: {
+ lineComment: '//',
+ blockComment: ['{-', '-}']
+ }
+ });
+
+ // create editor
+ var editor = monaco.editor.create(document.getElementById('editor'), {
+ model: null,
+ value: "",
+ language: 'cubicaltt',
+ theme: 'cubicaltt',
+ // wordWrap: 'wordWrapColumn',
+ // wordWrapColumn: 75,
+ // wordWrapMinified: true,
+ // wrappingIndent: 'same',
+ minimap: { enabled: false }
+ });
+ // add editor action to load buffer
+ editor.addAction({
+ id: 'load-buffer',
+ label: 'load buffer',
+ keybindings: [ monaco.KeyMod.WinCtrl | monaco.KeyCode.KEY_L ],
+ run: function(ed) {
+ loadHandler(app.current_tab.slice(0, -4), ed.getModel().getValue());
+ }
+ });
+ editor.onDidChangeModelContent(function (e) {
+ localStorage.removeItem("cache-module-" + app.current_tab.slice(0, -4));
+ });
+
+ var welcome = monaco.editor.createModel(welcomeContent, 'cubicaltt');
+ editor.setModel(welcome);
+
+ var lecture1 = monaco.editor.createModel(lecture1Content, 'cubicaltt');
+ var lecture2 = monaco.editor.createModel(lecture2Content, 'cubicaltt');
+ var lecture3 = monaco.editor.createModel(lecture3Content, 'cubicaltt');
+ var lecture4 = monaco.editor.createModel(lecture4Content, 'cubicaltt');
+
+ if (app === undefined) {
+ app = {}
+ }
+
+ app.log_buffer = [];
+ app.editor = editor;
+ app.history_pre = [];
+ app.history_post = [];
+ app.current_tab = "welcome-tab";
+ app.tabs = {
+ "welcome-tab": [welcome, undefined],
+ "lecture1-tab": [lecture1, undefined],
+ "lecture2-tab": [lecture2, undefined],
+ "lecture3-tab": [lecture3, undefined],
+ "lecture4-tab": [lecture4, undefined]
+ };
+
+ var input = document.getElementById("eval-input");
+ var button = document.getElementById("eval-button");
+ button.addEventListener("click", function(event) {
+ evalHandler(app.current_tab.slice(0, -4), input.value);
+ app.history_pre.push(input.value);
+ input.value = "";
+ });
+ input.addEventListener("keyup", function(event) {
+ if (event.keyCode === 38) {
+ // arrow up
+ event.preventDefault();
+ if (app.history_pre.length > 0) {
+ var val = app.history_pre.pop()
+ app.history_post.push(val);
+ input.value = val;
+ }
+ } else if (event.keyCode === 40) {
+ // arrow down
+ event.preventDefault();
+ if (app.history_post.length > 0) {
+ var val = app.history_post.pop()
+ app.history_pre.push(val);
+ input.value = val;
+ }
+ } else if (event.keyCode === 13) {
+ event.preventDefault();
+ button.click();
+ }
+ });
+
+ function switchTab(tabName) {
+ var navLinks = document.querySelectorAll(".tab-link");
+ navLinks.forEach(navLink => {
+ navLink.classList.remove("active");
+ });
+ var link = document.getElementById(tabName);
+ link.classList.add('active');
+ var state = editor.saveViewState();
+ app.tabs[app.current_tab][1] = state;
+ editor.setModel(app.tabs[tabName][0]);
+ app.current_tab = tabName;
+ editor.restoreViewState(app.tabs[tabName][1]);
+ };
+
+ var navLinks = document.querySelectorAll(".tab-link");
+ navLinks.forEach(navLink => {
+ navLink.addEventListener("click", function(event) {
+ switchTab(navLink.id);
+ });
+ });
+
+ function flushBuffer() {
+ setTimeout(function() {
+ var msg = [];
+ app.log_buffer.forEach(item => {
+ msg.push(item);
+ });
+ app.log_buffer = [];
+ if (msg.length != 0) {
+ document.getElementById('results').textContent += msg.join('');
+ // scroll log
+ var rc = document.getElementById('results-container');
+ rc.scrollTop = rc.scrollHeight;
+ }
+ flushBuffer();
+ }, 100);
+ };
+ flushBuffer();
+ // end set timeout
+ })
+ }, 1000);})
\ No newline at end of file
--- /dev/null
+(import ./default.nix { }).shells.ghc
--- /dev/null
+module welcome where
+
+{-
+
+ Welcome to the web version of cubicaltt!
+
+ cubicaltt - is an experimental implementation of Cubical Type Theory
+ in which the user can directly manipulate n-dimensional cubes.
+
+ This page offers cubicaltt builded with GHCJS and a simple JavaScript
+ application using Monaco editor. The idea is to bring Emacs
+ experience directly to the browser.
+
+ There are five tabs: this message and four great lectures by Anders Mörtberg.
+
+ To load the editor's tab use Ctrl + L. It will type check
+ the code and load definitions. That will allow to play with them
+ in the REPL which can be noticed on the right.
+
+ Have a nice day and good luck in learning Cubical Type Theory!
+
+-}
\ No newline at end of file
projects / cubicaltt.git / commitdiff