From bb7856dbce4f4b27cb603a6a3e2463857b81e91c Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Tue, 24 Mar 2015 10:59:55 +0100 Subject: [PATCH] enhanced and renamed emacs mode --- Makefile | 6 +++-- TypeChecker.hs | 3 +-- cubical.el | 64 ----------------------------------------------- cubicaltt.el | 65 ++++++++++++++++++++++++++++++++++++++++++++++++ examples/nat.ctt | 18 +++++++++++++- 5 files changed, 87 insertions(+), 69 deletions(-) delete mode 100644 cubical.el create mode 100644 cubicaltt.el diff --git a/Makefile b/Makefile index e63e0bc..31db06c 100644 --- 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 783d3a5..2427749 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -326,7 +326,6 @@ infer e = case e of unless (conv k a0 (eval rhoAlpha t0)) (throwError ("incompatible system with " ++ show t0)) ) ts - -- check that the system is compatible k <- asks index @@ -350,7 +349,7 @@ checkPath v t = do VIdP a a0 a1 -> do unless (conv k a v) (throwError "checkPath") return (a0,a1) - _ -> throwError "checkPath" + _ -> throwError "checkPath" checks :: (Tele,Env) -> [Ter] -> Typing () checks _ [] = return () diff --git a/cubical.el b/cubical.el deleted file mode 100644 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 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 b673a6e..f33aa0a 100644 --- 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) -> p @ (j \/ - k), (i = 1) -> p @ (j /\ k), (j = 0) -> p @ (i \/ - k), - (j = 1) -> p @ (i /\ k)] \ No newline at end of file + (j = 1) -> p @ (i /\ k)] + + +test (A : U) (a b : A) (p : Id A a b) : Id A a a = + 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) = +-- 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' = + comp A a [ (j = 0) -> comp A (p @ i) [ (i = 1) -> q @ k /\ l], + (j = 1) -> comp A (p @ i) [ (i=1) -> q' @ k /\ l], + (k = 0) -> p, + (k = 1) -> s @ j ] + -- 2.34.1