enhanced and renamed emacs mode

diff --git a/Makefile b/Makefile
index e63e0bcb8f1571f4d2ffdd3d8b794be7083bef84..31db06c517f4029840c1554d49bf88044993d783 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,12 +1,14 @@
+#GHC=ghc
+GHC=cabal exec ghc -- 
 OPT=2
 
 all:
-       ghc --make -O$(OPT) -o cubical 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
+       $(GHC) --make -O$(OPT) Exp/Test.hs -o Exp/Test
 clean:
        rm -f *.log *.aux *.hi *.o cubical
        cd Exp && rm -f ParExp.y LexExp.x LexhExp.hs \

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 783d3a545070341299445b0628c0564a6260fe30..24277490b83ce276b33f07d2d8bc2bdba4d12e22 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -326,7 +326,6 @@ infer e = case e of
                          unless (conv k a0 (eval rhoAlpha t0))\r
                            (throwError ("incompatible system with " ++ show t0))\r
                      ) ts\r
-    \r
 \r
     -- check that the system is compatible\r
     k <- asks index\r
@@ -350,7 +349,7 @@ checkPath v t = do
     VIdP a a0 a1 -> do\r
       unless (conv k a v) (throwError "checkPath")\r
       return (a0,a1)\r
-    _ -> throwError "checkPath"    \r
+    _ -> throwError "checkPath"\r
 \r
 checks :: (Tele,Env) -> [Ter] -> Typing ()\r
 checks _              []     = return ()\r

diff --git a/cubical.el b/cubical.el
deleted file mode 100644 (file)
index 3230779..0000000
--- a/cubical.el
+++ /dev/null
@@ -1,64 +0,0 @@
-;; 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/cubicaltt.el b/cubicaltt.el
new file mode 100644 (file)
index 0000000..08466ec
--- /dev/null
+++ b/cubicaltt.el
@@ -0,0 +1,65 @@
+;; define several class of keywords
+(setq ctt-keywords '("data" "import" "mutual" "let" "in" "split"
+                     "module" "where" "U") )
+(setq ctt-special '("undefined" "primitive"))
+
+;; create regex strings
+(setq ctt-keywords-regexp (regexp-opt ctt-keywords 'words))
+(setq ctt-operators-regexp
+      (regexp-opt '(":" "->" "=" "|" "\\" "*" "_" "<" ">" "\\/" "/\\" "-" "@") t))
+(setq ctt-special-regexp (regexp-opt ctt-special 'words))
+(setq ctt-def-regexp "^[[:word:]']+")
+
+;; clear memory
+(setq ctt-keywords nil)
+(setq ctt-special nil)
+
+;; create the list for font-lock.
+;; each class of keyword is given a particular face
+(setq ctt-font-lock-keywords
+  `(
+    (,ctt-keywords-regexp . font-lock-type-face)
+    (,ctt-operators-regexp . font-lock-variable-name-face)
+    (,ctt-special-regexp . font-lock-warning-face)
+    (,ctt-def-regexp . font-lock-function-name-face)
+))
+
+;; command to comment/uncomment text
+(defun ctt-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 ctt-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 ctt-mode fundamental-mode
+  "ctt mode"
+  "Major mode for editing cubical type theory files."
+
+  :syntax-table ctt-syntax-table
+
+  ;; code for syntax highlighting
+  (setq font-lock-defaults '(ctt-font-lock-keywords))
+  (setq mode-name "ctt")
+
+  ;; modify the keymap
+  (define-key ctt-mode-map [remap comment-dwim] 'ctt-comment-dwim)
+
+  ;; clear memory
+  (setq ctt-keywords-regexp nil)
+  (setq ctt-operators-regexp nil)
+  (setq ctt-special-regexp nil)
+)
+
+(provide 'ctt-mode)

diff --git a/examples/nat.ctt b/examples/nat.ctt
index b673a6e1af27ca7a033d5c8d253e5986c86d5c9d..f33aa0ac0ce5492239edd47c697035ae42934ba5 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -87,4 +87,20 @@ testSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p =
      [(i = 0) -> <k> p @ (j \/ - k),
       (i = 1) -> <k> p @ (j /\ k),
       (j = 0) -> <k> p @ (i \/ - k),
-      (j = 1) -> <k> p @ (i /\ k)]
\ No newline at end of file
+      (j = 1) -> <k> p @ (i /\ k)]
+
+
+test (A : U) (a b : A) (p : Id A a b) : Id A a a =
+  <i> p @ (i /\ -i)
+
+-- testRefl (A : U) (a b : A) (p : Id A a b) : Id (Id A a a) (test A a b p) (refl A a) =
+--   <i j> fill j A a [ (i=0) -> p  @ (i /\ -i) ]
+
+
+lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
+          (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
+  <j> <k> comp A a [ (j = 0) -> <i> comp A (p @ i) [ (i = 1) -> <l> q @ k /\ l],
+                     (j = 1) -> <i> comp A (p @ i) [ (i=1) -> <l> q' @ k /\ l],
+                     (k = 0)  -> p,
+                     (k = 1)  -> s @ j ]
+