From 85a3c08be20176ba5fc6062f962069a434cba8d1 Mon Sep 17 00:00:00 2001 From: Anders Date: Wed, 18 Mar 2015 11:53:37 +0100 Subject: [PATCH] Rename to cubical --- Main.hs | 11 +++---- Makefile | 4 +-- README.md | 2 +- cubical.el | 64 ++++++++++++++++++++++++++++++++++++ examples/{nat.tt => nat.ctt} | 0 minitt.el | 64 ------------------------------------ 6 files changed, 72 insertions(+), 73 deletions(-) create mode 100644 cubical.el rename examples/{nat.tt => nat.ctt} (100%) delete mode 100644 minitt.el diff --git a/Main.hs b/Main.hs index 21e64d8..7382372 100644 --- a/Main.hs +++ b/Main.hs @@ -35,8 +35,8 @@ options = [ Option "d" ["debug"] (NoArg Debug) "run in debugging mode" -- Version number, welcome message, usage and prompt strings version, welcome, usage, prompt :: String version = "1.0" -welcome = "minitt, version: " ++ version ++ " (:h for help)\n" -usage = "Usage: minitt [options] \nOptions:" +welcome = "cubical, version: " ++ version ++ " (:h for help)\n" +usage = "Usage: cubical [options] \nOptions:" prompt = "> " lexer :: String -> [Token] @@ -149,14 +149,13 @@ imports v st@(notok,loaded,mods) f Bad s -> do putStrLn $ "Parse failed in " ++ show f ++ "\n" ++ show s return ([],[],[]) - Ok mod@(Module id imp decls) -> - let name = unAIdent id - imp_tt = [prefix ++ unAIdent i ++ ".tt" | Import i <- imp] + Ok mod@(Module (AIdent (_,name)) imp decls) -> + let imp_ctt = [prefix ++ i ++ ".ctt" | Import (AIdent (_,i)) <- imp] in do when (name /= dropExtension (takeFileName f)) $ error $ "Module name mismatch " ++ show (f,name) (notok1,loaded1,mods1) <- - foldM (imports v) (f:notok,loaded,mods) imp_tt + foldM (imports v) (f:notok,loaded,mods) imp_ctt when v $ putStrLn $ "Parsed " ++ show f ++ " successfully!" return (notok,f:loaded1,mods1 ++ [mod]) diff --git a/Makefile b/Makefile index c4afb96..e63e0bc 100644 --- a/Makefile +++ b/Makefile @@ -1,13 +1,13 @@ OPT=2 all: - ghc --make -O$(OPT) -o minitt Main.hs + ghc --make -O$(OPT) -o cubical Main.hs bnfc: bnfc --haskell -d Exp.cf happy -gca Exp/Par.y alex -g Exp/Lex.x ghc --make -O$(OPT) Exp/Test.hs -o Exp/Test clean: - rm -f *.log *.aux *.hi *.o minitt + rm -f *.log *.aux *.hi *.o cubical cd Exp && rm -f ParExp.y LexExp.x LexhExp.hs \ ParExp.hs PrintExp.hs AbsExp.hs *.o *.hi diff --git a/README.md b/README.md index 93c47d8..ae1bba4 100644 --- a/README.md +++ b/README.md @@ -1 +1 @@ -# minitt +# cubical type theory diff --git a/cubical.el b/cubical.el new file mode 100644 index 0000000..a5a0ce1 --- /dev/null +++ b/cubical.el @@ -0,0 +1,64 @@ +;; define several class of keywords +(setq cubical-keywords '("data" "import" "mutual" "let" "in" "split" + "module" "where" "U") ) +(setq cubical-special '("undefined" "primitive")) + +;; create regex strings +(setq cubical-keywords-regexp (regexp-opt cubical-keywords 'words)) +(setq cubical-operators-regexp (regexp-opt '(":" "->" "=" "\\" "|" "\\" "*" "_") t)) +(setq cubical-special-regexp (regexp-opt cubical-special 'words)) +(setq cubical-def-regexp "^[[:word:]]+") + +;; clear memory +(setq cubical-keywords nil) +(setq cubical-special nil) + +;; create the list for font-lock. +;; each class of keyword is given a particular face +(setq cubical-font-lock-keywords + `( + (,cubical-keywords-regexp . font-lock-type-face) + (,cubical-operators-regexp . font-lock-variable-name-face) + (,cubical-special-regexp . font-lock-warning-face) + (,cubical-def-regexp . font-lock-function-name-face) +)) + +;; command to comment/uncomment text +(defun cubical-comment-dwim (arg) + "Comment or uncomment current line or region in a smart way. For detail, see `comment-dwim'." + (interactive "*P") + (require 'newcomment) + (let ((comment-start "--") (comment-end "")) + (comment-dwim arg))) + + +;; syntax table for comments, same as for haskell-mode +(defvar cubical-syntax-table + (let ((st (make-syntax-table))) + (modify-syntax-entry ?\{ "(}1nb" st) + (modify-syntax-entry ?\} "){4nb" st) + (modify-syntax-entry ?- "_ 123" st) + (modify-syntax-entry ?\n ">" st) + st)) + +;; define the mode +(define-derived-mode cubical-mode fundamental-mode + "cubical mode" + "Major mode for editing cubical files…" + + :syntax-table cubical-syntax-table + + ;; code for syntax highlighting + (setq font-lock-defaults '(cubical-font-lock-keywords)) + (setq mode-name "cubical") + + ;; modify the keymap + (define-key cubical-mode-map [remap comment-dwim] 'cubical-comment-dwim) + + ;; clear memory + (setq cubical-keywords-regexp nil) + (setq cubical-operators-regexp nil) + (setq cubical-special-regexp nil) +) + +(provide 'cubical-mode) diff --git a/examples/nat.tt b/examples/nat.ctt similarity index 100% rename from examples/nat.tt rename to examples/nat.ctt diff --git a/minitt.el b/minitt.el deleted file mode 100644 index 42dee62..0000000 --- a/minitt.el +++ /dev/null @@ -1,64 +0,0 @@ -;; define several class of keywords -(setq minitt-keywords '("data" "import" "mutual" "let" "in" "split" - "module" "where" "U") ) -(setq minitt-special '("undefined" "primitive")) - -;; create regex strings -(setq minitt-keywords-regexp (regexp-opt minitt-keywords 'words)) -(setq minitt-operators-regexp (regexp-opt '(":" "->" "=" "\\" "|" "\\" "*" "_") t)) -(setq minitt-special-regexp (regexp-opt minitt-special 'words)) -(setq minitt-def-regexp "^[[:word:]]+") - -;; clear memory -(setq minitt-keywords nil) -(setq minitt-special nil) - -;; create the list for font-lock. -;; each class of keyword is given a particular face -(setq minitt-font-lock-keywords - `( - (,minitt-keywords-regexp . font-lock-type-face) - (,minitt-operators-regexp . font-lock-variable-name-face) - (,minitt-special-regexp . font-lock-warning-face) - (,minitt-def-regexp . font-lock-function-name-face) -)) - -;; command to comment/uncomment text -(defun minitt-comment-dwim (arg) - "Comment or uncomment current line or region in a smart way. For detail, see `comment-dwim'." - (interactive "*P") - (require 'newcomment) - (let ((comment-start "--") (comment-end "")) - (comment-dwim arg))) - - -;; syntax table for comments, same as for haskell-mode -(defvar minitt-syntax-table - (let ((st (make-syntax-table))) - (modify-syntax-entry ?\{ "(}1nb" st) - (modify-syntax-entry ?\} "){4nb" st) - (modify-syntax-entry ?- "_ 123" st) - (modify-syntax-entry ?\n ">" st) - st)) - -;; define the mode -(define-derived-mode minitt-mode fundamental-mode - "minitt mode" - "Major mode for editing minitt files…" - - :syntax-table minitt-syntax-table - - ;; code for syntax highlighting - (setq font-lock-defaults '(minitt-font-lock-keywords)) - (setq mode-name "minitt") - - ;; modify the keymap - (define-key minitt-mode-map [remap comment-dwim] 'minitt-comment-dwim) - - ;; clear memory - (setq minitt-keywords-regexp nil) - (setq minitt-operators-regexp nil) - (setq minitt-special-regexp nil) -) - -(provide 'minitt-mode) -- 2.34.1