Rename to cubical

diff --git a/Main.hs b/Main.hs
index 21e64d88936324d4dc45de16edd9f53e54c65e1d..738237274f0cbb820173b179a61b0803f8af144b 100644 (file)
--- 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] <file.tt>\nOptions:"
+welcome = "cubical, version: " ++ version ++ "  (:h for help)\n"
+usage   = "Usage: cubical [options] <file.ctt>\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 c4afb969593ccc09640c66126d18a3b55adc71cd..e63e0bcb8f1571f4d2ffdd3d8b794be7083bef84 100644 (file)
--- 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 93c47d8dfed2035dbc773ef9119c91e2941c0be5..ae1bba4d79695c9ca9af52e42ffdbe08c8f19f9c 100644 (file)
--- a/README.md
+++ b/README.md
@@ -1 +1 @@
-# minitt
+# cubical type theory

diff --git a/cubical.el b/cubical.el
new file mode 100644 (file)
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 (file)
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)