From 6c42cb8273e61265a73ffbb642beeaa9295ac2b4 Mon Sep 17 00:00:00 2001 From: Evgenii Akentev Date: Sun, 16 Aug 2020 19:47:28 +0500 Subject: [PATCH] Add web version of cubicaltt --- .gitignore | 4 +- .gitmodules | 3 + CTT.hs | 21 ++- Connections.hs | 17 +- Exp/Abs.hs | 103 +++++++++++ Exp/Abs.hs.bak | 106 ++++++++++++ Exp/Doc.txt | 149 ++++++++++++++++ Exp/Doc.txt.bak | 149 ++++++++++++++++ Exp/ErrM.hs | 35 ++++ Exp/ErrM.hs.bak | 85 +++++++++ Exp/Layout.hs | 310 +++++++++++++++++++++++++++++++++ Exp/Layout.hs.bak | 311 +++++++++++++++++++++++++++++++++ Exp/Lex.x | 201 +++++++++++++++++++++ Exp/Lex.x.bak | 204 ++++++++++++++++++++++ Exp/Par.y | 215 +++++++++++++++++++++++ Exp/Par.y.bak | 237 +++++++++++++++++++++++++ Exp/Print.hs | 252 +++++++++++++++++++++++++++ Exp/Print.hs.bak | 261 ++++++++++++++++++++++++++++ Exp/Skel.hs | 105 +++++++++++ Exp/Skel.hs.bak | 106 ++++++++++++ Exp/Test.hs | 75 ++++++++ Exp/Test.hs.bak | 71 ++++++++ GNUmakefile | 2 +- Helpers.hs | 69 ++++++++ Main.hs | 431 +++++++++++++++++++++++++++------------------- Resolver.hs | 6 +- Setup.hs | 16 -- TypeChecker.hs | 177 +++++++++++-------- cabal.project | 2 + cubicaltt.cabal | 34 ++-- default.nix | 49 ++++++ reflex-platform | 1 + setup.js | 189 ++++++++++++++++++++ shell.nix | 1 + welcome.ctt | 22 +++ 35 files changed, 3726 insertions(+), 293 deletions(-) create mode 100644 .gitmodules create mode 100644 Exp/Abs.hs create mode 100644 Exp/Abs.hs.bak create mode 100644 Exp/Doc.txt create mode 100644 Exp/Doc.txt.bak create mode 100644 Exp/ErrM.hs create mode 100644 Exp/ErrM.hs.bak create mode 100644 Exp/Layout.hs create mode 100644 Exp/Layout.hs.bak create mode 100644 Exp/Lex.x create mode 100644 Exp/Lex.x.bak create mode 100644 Exp/Par.y create mode 100644 Exp/Par.y.bak create mode 100644 Exp/Print.hs create mode 100644 Exp/Print.hs.bak create mode 100644 Exp/Skel.hs create mode 100644 Exp/Skel.hs.bak create mode 100644 Exp/Test.hs create mode 100644 Exp/Test.hs.bak create mode 100644 Helpers.hs delete mode 100644 Setup.hs create mode 100644 cabal.project create mode 100644 default.nix create mode 160000 reflex-platform create mode 100644 setup.js create mode 100644 shell.nix create mode 100644 welcome.ctt diff --git a/.gitignore b/.gitignore index 097f308..de7a300 100644 --- a/.gitignore +++ b/.gitignore @@ -13,4 +13,6 @@ Main cabal.sandbox.config .stack-work .*.sw? - +dist-ghcjs +dist-newstyle +result \ No newline at end of file diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..15aca66 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "reflex-platform"] + path = reflex-platform + url = git@github.com:reflex-frp/reflex-platform.git diff --git a/CTT.hs b/CTT.hs index 7cfa412..82a2b19 100644 --- a/CTT.hs +++ b/CTT.hs @@ -1,6 +1,9 @@ {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} module CTT where +import Data.Aeson +import GHC.Generics (Generic) + import Control.Applicative import Data.List import Data.Maybe @@ -18,7 +21,7 @@ import Connections data Loc = Loc { locFile :: String , locPos :: (Int,Int) } - deriving Eq + deriving (Eq, Generic, ToJSON, FromJSON) type Ident = String type LIdent = String @@ -28,13 +31,13 @@ type Tele = [(Ident,Ter)] 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 @@ -44,7 +47,7 @@ data Decls = MutualDecls Loc [Decl] | OpaqueDecl Ident | TransparentDecl Ident | TransparentAllDecl - deriving Eq + deriving (Eq, Generic, ToJSON, FromJSON) declIdents :: [Decl] -> [Ident] declIdents decls = [ x | (x,_) <- decls ] @@ -125,7 +128,7 @@ data Ter = Pi Ter | 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]) @@ -184,7 +187,7 @@ data Val = VU | 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 @@ -237,7 +240,7 @@ data Ctxt = Empty | 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 @@ -254,7 +257,7 @@ instance Eq Ctxt where -- 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) @@ -441,7 +444,7 @@ showVal v = case v of 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] diff --git a/Connections.hs b/Connections.hs index 3a29a62..47cb2b3 100644 --- a/Connections.hs +++ b/Connections.hs @@ -1,7 +1,11 @@ {-# 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 @@ -14,7 +18,7 @@ import Data.Maybe 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 @@ -26,7 +30,7 @@ swapName k (i,j) | k == i = j -- | Directions data Dir = Zero | One - deriving (Eq,Ord) + deriving (Eq, Ord, Generic, ToJSON, FromJSON) instance Show Dir where show Zero = "0" @@ -59,6 +63,9 @@ instance Arbitrary Dir where -- 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 @@ -134,7 +141,7 @@ data Formula = Dir Dir | NegAtom Name | Formula :/\: Formula | Formula :\/: Formula - deriving Eq + deriving (Eq, Generic, ToJSON, FromJSON) instance Show Formula where show (Dir Zero) = "0" @@ -293,7 +300,7 @@ unionsMap :: Eq b => (a -> [b]) -> [a] -> [b] 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 _ = [] diff --git a/Exp/Abs.hs b/Exp/Abs.hs new file mode 100644 index 0000000..cf66a4f --- /dev/null +++ b/Exp/Abs.hs @@ -0,0 +1,103 @@ +-- 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) + diff --git a/Exp/Abs.hs.bak b/Exp/Abs.hs.bak new file mode 100644 index 0000000..c36228b --- /dev/null +++ b/Exp/Abs.hs.bak @@ -0,0 +1,106 @@ +-- 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) + diff --git a/Exp/Doc.txt b/Exp/Doc.txt new file mode 100644 index 0000000..25a3970 --- /dev/null +++ b/Exp/Doc.txt @@ -0,0 +1,149 @@ +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]// + + diff --git a/Exp/Doc.txt.bak b/Exp/Doc.txt.bak new file mode 100644 index 0000000..382fa44 --- /dev/null +++ b/Exp/Doc.txt.bak @@ -0,0 +1,149 @@ +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]// + + diff --git a/Exp/ErrM.hs b/Exp/ErrM.hs new file mode 100644 index 0000000..16507c4 --- /dev/null +++ b/Exp/ErrM.hs @@ -0,0 +1,35 @@ +-- 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 diff --git a/Exp/ErrM.hs.bak b/Exp/ErrM.hs.bak new file mode 100644 index 0000000..3e42b15 --- /dev/null +++ b/Exp/ErrM.hs.bak @@ -0,0 +1,85 @@ +{-# 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 diff --git a/Exp/Layout.hs b/Exp/Layout.hs new file mode 100644 index 0000000..8ac7e2c --- /dev/null +++ b/Exp/Layout.hs @@ -0,0 +1,310 @@ +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 + diff --git a/Exp/Layout.hs.bak b/Exp/Layout.hs.bak new file mode 100644 index 0000000..2c6b221 --- /dev/null +++ b/Exp/Layout.hs.bak @@ -0,0 +1,311 @@ +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 + diff --git a/Exp/Lex.x b/Exp/Lex.x new file mode 100644 index 0000000..90b1451 --- /dev/null +++ b/Exp/Lex.x @@ -0,0 +1,201 @@ +-- -*- 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 + ] +} diff --git a/Exp/Lex.x.bak b/Exp/Lex.x.bak new file mode 100644 index 0000000..33ba7ab --- /dev/null +++ b/Exp/Lex.x.bak @@ -0,0 +1,204 @@ +-- -*- 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 + ] +} diff --git a/Exp/Par.y b/Exp/Par.y new file mode 100644 index 0000000..edf1ab4 --- /dev/null +++ b/Exp/Par.y @@ -0,0 +1,215 @@ +-- 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 +} + diff --git a/Exp/Par.y.bak b/Exp/Par.y.bak new file mode 100644 index 0000000..1a76bd0 --- /dev/null +++ b/Exp/Par.y.bak @@ -0,0 +1,237 @@ +-- 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 +} + diff --git a/Exp/Print.hs b/Exp/Print.hs new file mode 100644 index 0000000..99b793e --- /dev/null +++ b/Exp/Print.hs @@ -0,0 +1,252 @@ +{-# 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 + diff --git a/Exp/Print.hs.bak b/Exp/Print.hs.bak new file mode 100644 index 0000000..fce18d9 --- /dev/null +++ b/Exp/Print.hs.bak @@ -0,0 +1,261 @@ +{-# 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 + diff --git a/Exp/Skel.hs b/Exp/Skel.hs new file mode 100644 index 0000000..483d3b7 --- /dev/null +++ b/Exp/Skel.hs @@ -0,0 +1,105 @@ +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 + diff --git a/Exp/Skel.hs.bak b/Exp/Skel.hs.bak new file mode 100644 index 0000000..33207c2 --- /dev/null +++ b/Exp/Skel.hs.bak @@ -0,0 +1,106 @@ +-- 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 + diff --git a/Exp/Test.hs b/Exp/Test.hs new file mode 100644 index 0000000..b61a22b --- /dev/null +++ b/Exp/Test.hs @@ -0,0 +1,75 @@ +-- 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 + + + + + diff --git a/Exp/Test.hs.bak b/Exp/Test.hs.bak new file mode 100644 index 0000000..f4bee18 --- /dev/null +++ b/Exp/Test.hs.bak @@ -0,0 +1,71 @@ +-- 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 + diff --git a/GNUmakefile b/GNUmakefile index 5a69fc5..7997b0b 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -48,7 +48,7 @@ include Makefile $(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) diff --git a/Helpers.hs b/Helpers.hs new file mode 100644 index 0000000..bb83312 --- /dev/null +++ b/Helpers.hs @@ -0,0 +1,69 @@ +{-# 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 diff --git a/Main.hs b/Main.hs index 8d62190..5152992 100644 --- a/Main.hs +++ b/Main.hs @@ -1,15 +1,28 @@ +{-# 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 @@ -18,190 +31,256 @@ import Exp.Print 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] \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" ++ - " infer type and evaluate statement\n" ++ - " :n normalize statement\n" ++ - " :q quit\n" ++ - " :l loads filename (and resets environment before)\n" ++ - " :cd 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 diff --git a/Resolver.hs b/Resolver.hs index 308e2cd..d997f80 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -3,6 +3,8 @@ -- | 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 @@ -71,12 +73,12 @@ flattenPTele (PTele exp typ : xs) = case appsToIdents exp of -- | 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 diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 index 883ae7a..0000000 --- a/Setup.hs +++ /dev/null @@ -1,16 +0,0 @@ -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 - } diff --git a/TypeChecker.hs b/TypeChecker.hs index 40050c0..7a3fcfb 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -1,22 +1,32 @@ +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE TupleSections #-} module TypeChecker where +import Data.Aeson +import GHC.Generics (Generic) + import Control.Applicative hiding (empty) import Control.Monad import Control.Monad.Except +import Control.Monad.Identity import Control.Monad.Reader import Data.Map (Map,(!),mapWithKey,assocs,filterWithKey,elems,keys ,intersection,intersectionWith,intersectionWithKey ,toList,fromList) import qualified Data.Map as Map -import qualified Data.Traversable as T +import qualified Data.Traversable as Trav +import Data.Text (Text) +import qualified Data.Text as T import Connections import CTT import Eval +import GHCJS.DOM.Types as DOM hiding (Text, Event) +import qualified Language.Javascript.JSaddle as JS +import Helpers -- Type checking monad -type Typing a = ReaderT TEnv (ExceptT String IO) a +type Typing a = ReaderT TEnv (ExceptT String JSM) a -- Environment for type checker data TEnv = @@ -24,39 +34,58 @@ data TEnv = , indent :: Int , env :: Env , verbose :: Bool -- Should it be verbose and print what it typechecks? - } deriving (Eq) + } deriving (Eq, Generic, ToJSON, FromJSON) verboseEnv, silentEnv :: TEnv verboseEnv = TEnv [] 0 emptyEnv True silentEnv = TEnv [] 0 emptyEnv False --- Trace function that depends on the verbosity flag -trace :: String -> Typing () -trace s = do - b <- asks verbose - when b $ liftIO (putStrLn s) - ------------------------------------------------------------------------------- -- | Functions for running computations in the type checker monad -runTyping :: TEnv -> Typing a -> IO (Either String a) -runTyping env t = runExceptT $ runReaderT t env +runTyping :: TEnv -> Typing a -> JSM (Either String a) +runTyping !env !t = runExceptT $ runReaderT t env -runDecls :: TEnv -> Decls -> IO (Either String TEnv) -runDecls tenv d = runTyping tenv $ do - checkDecls d +runDecls :: TEnv -> Decls -> JSM (Either String TEnv) +runDecls !tenv !d = runTyping tenv $ do + !_ <- checkDecls $! d return $ addDecls d tenv -runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv) -runDeclss tenv [] = return (Nothing, tenv) -runDeclss tenv (d:ds) = do - x <- runDecls tenv d +runDeclss :: TEnv -> [Decls] -> JSM (Maybe String, TEnv) +runDeclss !tenv [] = return (Nothing, tenv) +runDeclss !tenv !(d:ds) = do + consoleLog "runDeclss" + !x <- runDecls tenv d case x of - Right tenv' -> runDeclss tenv' ds - Left s -> return (Just s, tenv) - -runInfer :: TEnv -> Ter -> IO (Either String Val) -runInfer lenv e = runTyping lenv (infer e) + Right !tenv' -> do + runDeclss tenv' ds + Left s -> return (Just s, tenv) + +-- new, better runDeclss, with setTimeout to give browser thread time +-- to render the type checking results +runDeclss' :: TEnv -> JSM () +runDeclss' !tenv = do + mDecls <- loadDataFromLocalStorage "decls-to-process" + case mDecls :: Maybe [Decls] of + Nothing -> + writeLogAndScroll "Unexpected error: not found decls to type check.\n" + Just [] -> do + saveDataToLocalStorage "load-results-imports-repl" tenv + writeLogAndScroll "File loaded.\n" + Just (d:ds) -> do + !x <- runDecls tenv d + case x of + Right !tenv' -> do + saveDataToLocalStorage "decls-to-process" ds + f <- toJSVal $ JS.fun $ \ _ _ _ -> runDeclss' tenv' + setTimeout f 10 + Left s -> do + removeLocalStorage "load-results-names-repl" + removeLocalStorage "load-results-imports-repl" + writeLogAndScroll $ T.pack ("Type checking failed: " ++ s ++ "\n") + +runInfer :: TEnv -> Ter -> JSM (Either String Val) +runInfer !lenv !e = runTyping lenv (infer e) ------------------------------------------------------------------------------- -- | Modifiers for the environment @@ -80,7 +109,7 @@ addBranch nvs env (TEnv ns ind rho v) = TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds nvs rho) v addDecls :: Decls -> TEnv -> TEnv -addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v +addDecls !d !(TEnv ns ind rho v) = TEnv ns ind (def d rho) v addTele :: Tele -> TEnv -> TEnv addTele xas lenv = foldl (flip addType) lenv xas @@ -125,24 +154,25 @@ evalTyping t = eval <$> asks env <*> pure t -- Check that t has type a check :: Val -> Ter -> Typing () -check a t = case (a,t) of - (_,Undef{}) -> return () - (_,Hole l) -> do +check !a !t = case (a,t) of + !(_,Undef{}) -> return () + !(_,Hole l) -> do rho <- asks env let e = unlines (reverse (contextOfEnv rho)) ns <- asks names - trace $ "\nHole at " ++ show l ++ ":\n\n" ++ - e ++ replicate 80 '-' ++ "\n" ++ show (normal ns a) ++ "\n" - (_,Con c es) -> do + liftJSM $! writeLogAndScroll $ T.pack $ "\nHole at " ++ show l ++ ":\n\n" ++ + e ++ replicate 80 '-' ++ "\n" ++ show (normal ns a) ++ "\n" + pure () + !(_,Con c es) -> do (bs,nu) <- getLblType c a checks (bs,nu) es - (VU,Pi f) -> checkFam f - (VU,Sigma f) -> checkFam f - (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of + !(VU,Pi f) -> checkFam f + !(VU,Sigma f) -> checkFam f + !(VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of OLabel _ tele -> checkTele tele PLabel _ tele is ts -> throwError $ "check: no path constructor allowed in " ++ show t - (VU,HSum _ _ bs) -> forM_ bs $ \lbl -> case lbl of + !(VU,HSum _ _ bs) -> forM_ bs $ \lbl -> case lbl of OLabel _ tele -> checkTele tele PLabel _ tele is ts -> do checkTele tele @@ -158,7 +188,7 @@ check a t = case (a,t) of check (Ter t rho) talpha rho' <- asks env checkCompSystem (evalSystem rho' ts) - (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do + !(VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do check VU ty rho <- asks env unlessM (a === eval rho ty) $ throwError "check: split annotations" @@ -166,7 +196,7 @@ check a t = case (a,t) of then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va | (brc, lbl) <- zip ces cas ] else throwError "case branches does not match the data type" - (VPi va@(Ter (HSum _ _ cas) nu) f,Split _ _ ty ces) -> do + !(VPi va@(Ter (HSum _ _ cas) nu) f,Split _ _ ty ces) -> do check VU ty rho <- asks env unlessM (a === eval rho ty) $ throwError "check: split annotations" @@ -174,7 +204,7 @@ check a t = case (a,t) of then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va | (brc, lbl) <- zip ces cas ] else throwError "case branches does not match the data type" - (VPi a f,Lam x a' t) -> do + !(VPi a f,Lam x a' t) -> do check VU a' ns <- asks names rho <- asks env @@ -186,43 +216,43 @@ check a t = case (a,t) of let var = mkVarNice ns x a local (addTypeVal (x,a)) $ check (app f var) t - (VSigma a f, Pair t1 t2) -> do + !(VSigma a f, Pair t1 t2) -> do check a t1 v <- evalTyping t1 check (app f v) t2 - (_,Where e d) -> do + !(_,Where e d) -> do local (\tenv@TEnv{indent=i} -> tenv{indent=i + 2}) $ checkDecls d local (addDecls d) $ check a e - (VU,PathP a e0 e1) -> do + !(VU,PathP a e0 e1) -> do (a0,a1) <- checkPLam (constPath VU) a check a0 e0 check a1 e1 - (VPathP p a0 a1,PLam _ e) -> do + !(VPathP p a0 a1,PLam _ e) -> do (u0,u1) <- checkPLam p t ns <- asks names unless (conv ns a0 u0 && conv ns a1 u1) $ throwError $ "path endpoints don't match for " ++ show e ++ ", got " ++ show (u0,u1) ++ ", but expected " ++ show (a0,a1) - (VU,Glue a ts) -> do + !(VU,Glue a ts) -> do check VU a rho <- asks env checkGlue (eval rho a) ts - (VGlue va ts,GlueElem u us) -> do + !(VGlue va ts,GlueElem u us) -> do check va u vu <- evalTyping u checkGlueElem vu ts us - (VCompU va ves,GlueElem u us) -> do + !(VCompU va ves,GlueElem u us) -> do check va u vu <- evalTyping u checkGlueElemU vu ves us - (VU,Id a a0 a1) -> do + !(VU,Id a a0 a1) -> do check VU a - va <- evalTyping a + !va <- evalTyping a check va a0 check va a1 - (VId va va0 va1,IdPair w ts) -> do + !(VId va va0 va1,IdPair w ts) -> do check (VPathP (constPath va) va0 va1) w - vw <- evalTyping w + !vw <- evalTyping w checkSystemWith ts $ \alpha tAlpha -> local (faceEnv alpha) $ do check (va `face` alpha) tAlpha @@ -231,21 +261,22 @@ check a t = case (a,t) of throwError "malformed eqC" rho <- asks env checkCompSystem (evalSystem rho ts) -- Not needed - _ -> do - v <- infer t + !_ -> do + !v <- infer t unlessM (v === a) $ throwError $ "check conv:\n" ++ show v ++ "\n/=\n" ++ show a -- Check a list of declarations checkDecls :: Decls -> Typing () checkDecls (MutualDecls _ []) = return () -checkDecls (MutualDecls l d) = do +checkDecls !(MutualDecls l d) = do a <- asks env - let (idents,tele,ters) = (declIdents d,declTele d,declTers d) - ind <- asks indent - trace (replicate ind ' ' ++ "Checking: " ++ unwords idents) - checkTele tele - local (addDecls (MutualDecls l d)) $ do + let !(idents,tele,ters) = (declIdents d,declTele d,declTers d) + !ind <- asks indent + liftJSM $! writeLogAndScroll $! + T.pack $! replicate ind ' ' ++ "Checking: " ++ unwords idents ++ "\n" + checkTele $! tele + local (addDecls $! (MutualDecls l d)) $ do rho <- asks env checks (tele,rho) ters checkDecls (OpaqueDecl _) = return () @@ -400,7 +431,7 @@ checkPLam v (PLam i a) = do local (addSub (i,Atom i)) $ check (v @@ i) a return (eval (sub (i,Dir 0) rho) a,eval (sub (i,Dir 1) rho) a) checkPLam v t = do - vt <- infer t + !vt <- infer t case vt of VPathP a a0 a1 -> do unlessM (a === v) $ throwError ( @@ -414,7 +445,7 @@ checkPLam v t = do checkPLamSystem :: Ter -> Val -> System Ter -> Typing (System Val) checkPLamSystem t0 va ps = do rho <- asks env - v <- T.sequence $ mapWithKey (\alpha pAlpha -> + v <- Trav.sequence $ mapWithKey (\alpha pAlpha -> local (faceEnv alpha) $ do rhoAlpha <- asks env (a0,a1) <- checkPLam (va `face` alpha) pAlpha @@ -444,7 +475,7 @@ infer e = case e of U -> return VU -- U : U Var n -> lookType n <$> asks env App t u -> do - c <- infer t + !c <- infer t case c of VPi a f -> do check a u @@ -452,12 +483,12 @@ infer e = case e of return $ app f v _ -> throwError $ show c ++ " is not a product" Fst t -> do - c <- infer t + !c <- infer t case c of VSigma a f -> return a _ -> throwError $ show c ++ " is not a sigma-type" Snd t -> do - c <- infer t + !c <- infer t case c of VSigma a f -> do v <- evalTyping t @@ -467,60 +498,60 @@ infer e = case e of checkDecls d local (addDecls d) $ infer t UnGlueElem e _ -> do - t <- infer e + !t <- infer e case t of VGlue a _ -> return a _ -> throwError (show t ++ " is not a Glue") AppFormula e phi -> do checkFormula phi - t <- infer e + !t <- infer e case t of VPathP a _ _ -> return $ a @@ phi _ -> throwError (show e ++ " is not a path") Comp a t0 ps -> do (va0, va1) <- checkPLam (constPath VU) a - va <- evalTyping a + !va <- evalTyping a check va0 t0 checkPLamSystem t0 va ps return va1 HComp a u0 us -> do check VU a - va <- evalTyping a + !va <- evalTyping a check va u0 checkPLamSystem u0 (constPath va) us return va Fill a t0 ps -> do (va0, va1) <- checkPLam (constPath VU) a - va <- evalTyping a + !va <- evalTyping a check va0 t0 checkPLamSystem t0 va ps - vt <- evalTyping t0 + !vt <- evalTyping t0 rho <- asks env let vps = evalSystem rho ps return (VPathP va vt (compLine va vt vps)) PCon c a es phis -> do check VU a - va <- evalTyping a + !va <- evalTyping a (bs,nu) <- getLblType c va checks (bs,nu) es mapM_ checkFormula phis return va IdJ a u c d x p -> do check VU a - va <- evalTyping a + !va <- evalTyping a check va u - vu <- evalTyping u + !vu <- evalTyping u let refu = VIdPair (constPath vu) $ mkSystem [(eps,vu)] rho <- asks env let z = Var "z" ctype = eval rho $ Pi $ Lam "z" a $ Pi $ Lam "_" (Id a u z) U check ctype c - vc <- evalTyping c + !vc <- evalTyping c check (app (app vc vu) refu) d check va x - vx <- evalTyping x + !vx <- evalTyping x check (VId va vu vx) p - vp <- evalTyping p + !vp <- evalTyping p return (app (app vc vx) vp) _ -> throwError ("infer " ++ show e) diff --git a/cabal.project b/cabal.project new file mode 100644 index 0000000..f8b3602 --- /dev/null +++ b/cabal.project @@ -0,0 +1,2 @@ +packages: + ./ \ No newline at end of file diff --git a/cubicaltt.cabal b/cubicaltt.cabal index 2a37780..38c9e0f 100644 --- a/cubicaltt.cabal +++ b/cubicaltt.cabal @@ -12,7 +12,7 @@ author: Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg 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 @@ -24,14 +24,18 @@ executable cubical 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, @@ -41,17 +45,27 @@ executable cubical 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 diff --git a/default.nix b/default.nix new file mode 100644 index 0000000..fb7125b --- /dev/null +++ b/default.nix @@ -0,0 +1,49 @@ +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 diff --git a/reflex-platform b/reflex-platform new file mode 160000 index 0000000..df0bdcc --- /dev/null +++ b/reflex-platform @@ -0,0 +1 @@ +Subproject commit df0bdcca5eb2a3236ec0496e4430d91876b29cf5 diff --git a/setup.js b/setup.js new file mode 100644 index 0000000..9146e90 --- /dev/null +++ b/setup.js @@ -0,0 +1,189 @@ +(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: /[=> 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 diff --git a/shell.nix b/shell.nix new file mode 100644 index 0000000..ee98cc4 --- /dev/null +++ b/shell.nix @@ -0,0 +1 @@ +(import ./default.nix { }).shells.ghc diff --git a/welcome.ctt b/welcome.ctt new file mode 100644 index 0000000..f444b8f --- /dev/null +++ b/welcome.ctt @@ -0,0 +1,22 @@ +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 -- 2.34.1