pisigma 0.1.0.2 → 0.1.0.3
raw patch · 37 files changed
+4293/−1537 lines, 37 filesdep +bytestringdep +haskeline-classdep +mpppcdep −ansi-wl-pprintdep ~basedep ~parsec
Dependencies added: bytestring, haskeline-class, mpppc, text, utf8-string
Dependencies removed: ansi-wl-pprint
Dependency ranges changed: base, parsec
Files
- emacs-mode/eri.el +186/−0
- emacs-mode/pisigma-input.el +740/−0
- emacs-mode/pisigma-mode.el +140/−0
- examples/Broken.pi +9/−0
- examples/Curry.pi +13/−0
- examples/Data.pi +0/−107
- examples/EqProb.pi +0/−39
- examples/Equal.pi +60/−0
- examples/Foo.pi +1/−0
- examples/Hurkens.pi +42/−0
- examples/Parser.pi +89/−0
- examples/Parser2.pi +331/−0
- examples/Parser3.pi +331/−0
- examples/SubjectReduction.pi +58/−0
- examples/Universe.pi +0/−47
- examples/stl.pi +14/−0
- pisigma.cabal +52/−17
- src/Language/PiSigma/Check.hs +261/−0
- src/Language/PiSigma/Equality.hs +129/−0
- src/Language/PiSigma/Evaluate.hs +190/−0
- src/Language/PiSigma/Lexer.hs +278/−0
- src/Language/PiSigma/Normalise.hs +123/−0
- src/Language/PiSigma/Parser.hs +160/−0
- src/Language/PiSigma/Pretty.hs +193/−0
- src/Language/PiSigma/Syntax.hs +356/−0
- src/Language/PiSigma/Util/String/Internal.hs +48/−0
- src/Language/PiSigma/Util/String/Parser.hs +118/−0
- src/PiSigma.hs +0/−265
- src/PiSigma/Check.hs +0/−189
- src/PiSigma/Equality.hs +0/−128
- src/PiSigma/Evaluation.hs +0/−151
- src/PiSigma/Nf.hs +0/−111
- src/PiSigma/Parser.hs +0/−141
- src/PiSigma/Print.hs +0/−108
- src/PiSigma/Syntax.hs +0/−234
- src/Tools/Interpreter/Main.hs +15/−0
- src/Tools/Interpreter/REPL.hs +356/−0
+ emacs-mode/eri.el view
@@ -0,0 +1,186 @@+;;; eri.el --- Enhanced relative indentation (eri)++;;; Commentary:++;;; Code:++(require 'cl)++(defun eri-current-line-length nil+ "Calculates length of current line."+ (- (line-end-position) (line-beginning-position)))++(defun eri-current-line-empty nil+ "Return non-nil if the current line is empty (not counting white space)."+ (equal (current-indentation)+ (eri-current-line-length)))++(defun eri-maximum (xs)+ "Calculate maximum element in XS. Return nil if the list is empty."+ (if xs (apply 'max xs)))++(defun eri-take (n xs)+ "Return the first N elements of XS."+ (butlast xs (- (length xs) n)))++(defun eri-split (x xs)+ "Return a pair of lists (XS1 . XS2).+If XS is sorted, then XS = (append XS1 XS2), and all elements in XS1 are <= X,+whereas all elements in XS2 are > X."+ (let* ((pos (or (position-if (lambda (y) (> y x)) xs) (length xs)))+ (xs1 (eri-take pos xs))+ (xs2 (nthcdr pos xs)))+ `(,xs1 . ,xs2)))++(defun eri-calculate-indentation-points-on-line (max)+ "Calculate indentation points on current line.+Only points left of column number MAX are included.+If MAX is nil, then all points are included. Return points in ascending order.++Example (positions marked with ^ are returned):++ f x y = g 3 (Just y) 5 4+ ^ ^ ^ ^ ^ ^ ^ ^ |+ |+ MAX"+ (let ((result))+ (save-restriction+ (beginning-of-line)+ ; To make \\` work in the regexp below:+ (narrow-to-region (line-beginning-position) (line-end-position))+ (while+ (progn+ (let ((pos (and (search-forward-regexp+ "\\(?:\\s-\\|\\`\\)\\(\\S-\\)" nil t)+ (match-beginning 1))))+ (when (not (null pos))+ (let ((pos1 (- pos (line-beginning-position))))+ (when (or (null max) (< pos1 max))+ (add-to-list 'result pos1))))+ (and pos+ (< (point) (line-end-position))+ (or (null max) (< (current-column) max))))))+ (nreverse result) ; Destructive operation.+ )))++(defun eri-new-indentation-point ()+ "Calculate a new indentation point, two steps in from the+indentation of the first non-empty line above the current line.+If there is no such line 2 is returned."+ (save-excursion+ (while+ (progn+ (forward-line -1)+ (not (or (bobp)+ (not (eri-current-line-empty))))))+ (+ 2 (current-indentation))))++(defun eri-calculate-indentation-points (reverse)+ "Calculate some indentation points. Gives them in reverse order if+REVERSE is non-nil. See `eri-indent' for a description of how+the indentation points are calculated."+ ;; First find a bunch of indentations used above the current line.+ (let ((points)+ (max))+ (save-excursion+ (while+ (progn+ (forward-line -1)+ ; Skip lines with only white space.+ (unless (eri-current-line-empty)+ (setq points+ (append+ (eri-calculate-indentation-points-on-line max)+ points))+ (setq max (car points)))+ ;; Stop after hitting the beginning of the buffer or a+ ;; non-empty, non-indented line.+ (not (or (bobp)+ (and (equal (current-indentation) 0)+ (> (eri-current-line-length) 0)))))))+ ;; Add a new indentation point. Sort the indentations.+ ;; Rearrange the points so that the next point is the one after the+ ;; current one.+ (let* ((ps (add-to-list 'points (eri-new-indentation-point)))+ (ps1 (sort ps '<)) ; Note: sort is destructive.+ (ps2 (eri-split (current-indentation)+ (remove (current-indentation) ps1))))+ (if reverse+ (append (nreverse (car ps2)) (nreverse (cdr ps2)))+ (append (cdr ps2) (car ps2))))))++(defun eri-indent (&optional reverse)+ "Cycle between some possible indentation points.+With prefix argument REVERSE, cycle in reverse order.++Assume that a file contains the following lines of code, with point on+the line with three dots:++frob = loooooooooooooooooooooooooong identifier+foo = f a b+ where+ f (Foo x) y = let bar = x+ baz = 3 + 5++...++^ ^ ^ ^ ^ ^ ^ ^ ^ * ^ ^ ^ ^++Then the ^'s and the * mark the indentation points that this function+cycles through. The indentation points are selected as follows:++ * All lines before the current one, up to and including the first+ non-indented line (or the beginning of the buffer) are considered.++ foo = f a b+ where+ f (Foo x) y = let bar = x+ baz = 3 + 5++ * On these lines, erase all characters that stand to the right of+ some non-white space character on a lower line.++ foo+ whe+ f (Foo x) y = let b+ baz = 3 + 5++ * Also erase all characters not immediately preceded by white+ space.++ f+ w+ f ( x y = l b+ b = 3 + 5++ * The columns of all remaining characters are indentation points.++ f w f ( x y = l b = 3 + 5+ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^++ * A new indentation point is also added, two steps in from the+ indentation of the first non-empty line above the current line+ (or in the second column, if there is no such line).++ f w f ( x y = l b = 3 + 5+ ^ ^ ^ ^ ^ ^ ^ ^ ^ * ^ ^ ^ ^"+ (interactive "P")+ (let* ((points (eri-calculate-indentation-points reverse))+ (remaining-points (cdr (member (current-indentation) points)))+ (indentation (if remaining-points+ (car remaining-points)+ (car points))))+ (when indentation+ (save-excursion (indent-line-to indentation))+ (if (< (current-column) indentation)+ (indent-line-to indentation)))))++(defun eri-indent-reverse nil+ "Cycle between some possible indentation points (in reverse order).+See `eri-indent' for a description of how the indentation points are+calculated."+ (interactive)+ (eri-indent t))++(provide 'eri)+;;; eri.el ends here
+ emacs-mode/pisigma-input.el view
@@ -0,0 +1,740 @@+;;; pisigma-input.el --- The PiSigma input method++;;; Commentary:++;; A highly customisable input method which can inherit from other+;; Quail input methods. By default the input method is geared towards+;; the input of mathematical and other symbols in PiSigma programs.+;;+;; Use M-x customize-group pisigma-input to customise this input+;; method. Note that the functions defined under "Functions used to+;; tweak translation pairs" below can be used to tweak both the key+;; translations inherited from other input methods as well as the ones+;; added specifically for this one.+;;+;; Use pisigma-input-show-translations to see all the characters which+;; can be typed using this input method (except for those+;; corresponding to ASCII characters).++;;; Code:++(require 'quail)+(require 'cl)++;; Quail is quite stateful, so be careful when editing this code.+;; Note that with-temp-buffer is used below whenever buffer-local+;; state is modified.++;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;+;; Utility functions++(defun pisigma-input-concat-map (f xs)+ "Concat (map F XS)."+ (apply 'append (mapcar f xs)))++(defun pisigma-input-to-string-list (s)+ "Convert a string S to a list of one-character strings, after+removing all space and newline characters."+ (pisigma-input-concat-map+ (lambda (c) (if (member c (string-to-list " \n"))+ nil+ (list (string c))))+ (string-to-list s)))++;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;+;; Functions used to tweak translation pairs++;; lexical-let is used since Elisp lacks lexical scoping.++(defun pisigma-input-compose (f g)+ "\x -> concatMap F (G x)"+ (lexical-let ((f1 f) (g1 g))+ (lambda (x) (pisigma-input-concat-map f1 (funcall g1 x)))))++(defun pisigma-input-or (f g)+ "\x -> F x ++ G x"+ (lexical-let ((f1 f) (g1 g))+ (lambda (x) (append (funcall f1 x) (funcall g1 x)))))++(defun pisigma-input-nonempty ()+ "Only keep pairs with a non-empty first component."+ (lambda (x) (if (> (length (car x)) 0) (list x))))++(defun pisigma-input-prepend (prefix)+ "Prepend PREFIX to all key sequences."+ (lexical-let ((prefix1 prefix))+ (lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x))))))++(defun pisigma-input-prefix (prefix)+ "Only keep pairs whose key sequence starts with PREFIX."+ (lexical-let ((prefix1 prefix))+ (lambda (x)+ (if (equal (substring (car x) 0 (length prefix1)) prefix1)+ (list x)))))++(defun pisigma-input-suffix (suffix)+ "Only keep pairs whose key sequence ends with SUFFIX."+ (lexical-let ((suffix1 suffix))+ (lambda (x)+ (if (equal (substring (car x)+ (- (length (car x)) (length suffix1)))+ suffix1)+ (list x)))))++(defun pisigma-input-drop (ss)+ "Drop pairs matching one of the given key sequences.+SS should be a list of strings."+ (lexical-let ((ss1 ss))+ (lambda (x) (unless (member (car x) ss1) (list x)))))++(defun pisigma-input-drop-beginning (n)+ "Drop N characters from the beginning of each key sequence."+ (lexical-let ((n1 n))+ (lambda (x) `((,(substring (car x) n1) . ,(cdr x))))))++(defun pisigma-input-drop-end (n)+ "Drop N characters from the end of each key sequence."+ (lexical-let ((n1 n))+ (lambda (x)+ `((,(substring (car x) 0 (- (length (car x)) n1)) .+ ,(cdr x))))))++(defun pisigma-input-drop-prefix (prefix)+ "Only keep pairs whose key sequence starts with PREFIX.+This prefix is dropped."+ (pisigma-input-compose+ (pisigma-input-drop-beginning (length prefix))+ (pisigma-input-prefix prefix)))++(defun pisigma-input-drop-suffix (suffix)+ "Only keep pairs whose key sequence ends with SUFFIX.+This suffix is dropped."+ (lexical-let ((suffix1 suffix))+ (pisigma-input-compose+ (pisigma-input-drop-end (length suffix1))+ (pisigma-input-suffix suffix1))))++;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;+;; Customization++;; The :set keyword is set to+;; 'pisigma-input-incorporate-changed-setting so that the input method+;; gets updated immediately when users customize it. However, the+;; setup functions cannot be run before all variables have been+;; defined. Hence the :initialize keyword is set to+;; 'custom-initialize-default to ensure that the setup is not+;; performed until pisigma-input-setup is called at the end of this+;; file.++(defgroup pisigma-input nil+ "The PiSigma input method.+After tweaking these settings you may want to inspect the+resulting translations using `pisigma-input-show-translations'."+ :group 'pisigma+ :group 'leim)++(defcustom pisigma-input-tweak-all+ '(pisigma-input-compose+ (pisigma-input-prepend "\\")+ (pisigma-input-nonempty))+ "An expression yielding a function which can be used to tweak+all translations before they are included in the input method.+The resulting function (if non-nil) is applied to every+\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of+such pairs. (Note that the translations can be anything accepted+by `quail-defrule'.)++If you change this setting manually (without using the+customization buffer) you need to call `pisigma-input-setup' in+order for the change to take effect."+ :group 'pisigma-input+ :set 'pisigma-input-incorporate-changed-setting+ :initialize 'custom-initialize-default+ :type 'sexp)++(defcustom pisigma-input-inherit+ `(("TeX" . (pisigma-input-compose+ (pisigma-input-drop '("geq" "leq" "bullet" "qed"))+ (pisigma-input-or+ (pisigma-input-drop-prefix "\\")+ (pisigma-input-or+ (pisigma-input-compose+ (pisigma-input-drop '("^o"))+ (pisigma-input-prefix "^"))+ (pisigma-input-prefix "_")))))+ )+ "A list of Quail input methods whose translations should be+inherited by the PiSigma input method (with the exception of+translations corresponding to ASCII characters).++The list consists of pairs (qp . tweak), where qp is the name of+a Quail package, and tweak is an expression of the same kind as+`pisigma-input-tweak-all' which is used to tweak the translation+pairs of the input method.++The inherited translation pairs are added last, after+`pisigma-input-user-translations' and+`pisigma-input-translations'.++If you change this setting manually (without using the+customization buffer) you need to call `pisigma-input-setup' in+order for the change to take effect."+ :group 'pisigma-input+ :set 'pisigma-input-incorporate-changed-setting+ :initialize 'custom-initialize-default+ :type '(repeat (cons (string :tag "Quail package")+ (sexp :tag "Tweaking function"))))++(defcustom pisigma-input-translations+ (let ((max-lisp-eval-depth 2800)) `(++ ;; Equality and similar symbols.++ ("eq" . ,(pisigma-input-to-string-list "=∼∽≈≋∻∾∿≀≃⋍≂≅ ≌≊≡≣≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≍≎≏≬⋕"))+ ("eqn" . ,(pisigma-input-to-string-list "≠≁ ≉ ≄ ≇≆ ≢ ≭ "))++ ("=n" . ("≠"))+ ("~" . ("∼")) ("~n" . ("≁"))+ ("~~" . ("≈")) ("~~n" . ("≉"))+ ("~~~" . ("≋"))+ (":~" . ("∻"))+ ("~-" . ("≃")) ("~-n" . ("≄"))+ ("-~" . ("≂"))+ ("~=" . ("≅")) ("~=n" . ("≇"))+ ("~~-" . ("≊"))+ ("==" . ("≡")) ("==n" . ("≢"))+ ("===" . ("≣"))+ (".=" . ("≐")) (".=." . ("≑"))+ (":=" . ("≔")) ("=:" . ("≕"))+ ("=o" . ("≗"))+ ("(=" . ("≘"))+ ("and=" . ("≙")) ("or=" . ("≚"))+ ("*=" . ("≛"))+ ("t=" . ("≜"))+ ("def=" . ("≝"))+ ("m=" . ("≞"))+ ("?=" . ("≟"))++ ;; Inequality and similar symbols.++ ("leq" . ,(pisigma-input-to-string-list "<≪⋘≤≦≲ ≶≺≼≾⊂⊆ ⋐⊏⊑ ⊰⊲⊴⋖⋚⋜⋞"))+ ("leqn" . ,(pisigma-input-to-string-list "≮ ≰≨≴⋦≸⊀ ⋨⊄⊈⊊ ⋢⋤ ⋪⋬ ⋠"))+ ("geq" . ,(pisigma-input-to-string-list ">≫⋙≥≧≳ ≷≻≽≿⊃⊇ ⋑⊐⊒ ⊱⊳⊵⋗⋛⋝⋟"))+ ("geqn" . ,(pisigma-input-to-string-list "≯ ≱≩≵⋧≹⊁ ⋩⊅⊉⊋ ⋣⋥ ⋫⋭ ⋡"))++ ("<=" . ("≤")) (">=" . ("≥"))+ ("<=n" . ("≰")) (">=n" . ("≱"))+ ("len" . ("≰")) ("gen" . ("≱"))+ ("<n" . ("≮")) (">n" . ("≯"))+ ("<~" . ("≲")) (">~" . ("≳"))+ ("<~n" . ("⋦")) (">~n" . ("⋧"))+ ("<~nn" . ("≴")) (">~nn" . ("≵"))++ ("sub" . ("⊂")) ("sup" . ("⊃"))+ ("subn" . ("⊄")) ("supn" . ("⊅"))+ ("sub=" . ("⊆")) ("sup=" . ("⊇"))+ ("sub=n" . ("⊈")) ("sup=n" . ("⊉"))++ ("squb" . ("⊏")) ("squp" . ("⊐"))+ ("squb=" . ("⊑")) ("squp=" . ("⊒"))+ ("squb=n" . ("⋢")) ("squp=n" . ("⋣"))++ ;; Set membership etc.++ ("member" . ,(pisigma-input-to-string-list "∈∉∊∋∌∍⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿"))++ ("inn" . ("∉"))+ ("nin" . ("∌"))++ ;; Intersections, unions etc.++ ("intersection" . ,(pisigma-input-to-string-list "∩⋂∧⋀⋏⨇⊓⨅⋒∏ ⊼ ⨉"))+ ("union" . ,(pisigma-input-to-string-list "∪⋃∨⋁⋎⨈⊔⨆⋓∐⨿⊽⊻⊍⨃⊎⨄⊌∑⅀"))++ ("and" . ("∧")) ("or" . ("∨"))+ ("And" . ("⋀")) ("Or" . ("⋁"))+ ("i" . ("∩")) ("un" . ("∪")) ("u+" . ("⊎")) ("u." . ("⊍"))+ ("I" . ("⋂")) ("Un" . ("⋃")) ("U+" . ("⨄")) ("U." . ("⨃"))+ ("glb" . ("⊓")) ("lub" . ("⊔"))+ ("Glb" . ("⨅")) ("Lub" . ("⨆"))++ ;; Entailment etc.++ ("entails" . ,(pisigma-input-to-string-list "⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯"))++ ("|-" . ("⊢")) ("|-n" . ("⊬"))+ ("-|" . ("⊣"))+ ("|=" . ("⊨")) ("|=n" . ("⊭"))+ ("||-" . ("⊩")) ("||-n" . ("⊮"))+ ("||=" . ("⊫")) ("||=n" . ("⊯"))+ ("|||-" . ("⊪"))++ ;; Divisibility, parallelity.++ ("|" . ("∣")) ("|n" . ("∤"))+ ("||" . ("∥")) ("||n" . ("∦"))++ ;; Some symbols from logic and set theory.++ ("all" . ("∀"))+ ("ex" . ("∃"))+ ("exn" . ("∄"))+ ("0" . ("∅"))+ ("C" . ("∁"))++ ;; Corners, ceilings and floors.++ ("c" . ,(pisigma-input-to-string-list "⌜⌝⌞⌟⌈⌉⌊⌋"))+ ("cu" . ,(pisigma-input-to-string-list "⌜⌝ ⌈⌉ "))+ ("cl" . ,(pisigma-input-to-string-list " ⌞⌟ ⌊⌋"))++ ("cul" . ("⌜")) ("cuL" . ("⌈"))+ ("cur" . ("⌝")) ("cuR" . ("⌉"))+ ("cll" . ("⌞")) ("clL" . ("⌊"))+ ("clr" . ("⌟")) ("clR" . ("⌋"))++ ;; Various operators/symbols.++ ("qed" . ("∎"))+ ("x" . ("×"))+ ("o" . ("∘"))+ ("comp" . ("∘"))+ ("." . ("∙"))+ ("*" . ("⋆"))+ (".+" . ("∔"))+ (".-" . ("∸"))+ (":" . ("∶"))+ ("::" . ("∷"))+ ("::-" . ("∺"))+ ("-:" . ("∹"))+ ("+ " . ("⊹"))+ ("surd3" . ("∛"))+ ("surd4" . ("∜"))+ ("increment" . ("∆"))+ ("inf" . ("∞"))++ ;; Circled operators.++ ("o+" . ("⊕"))+ ("o--" . ("⊖"))+ ("ox" . ("⊗"))+ ("o/" . ("⊘"))+ ("o." . ("⊙"))+ ("oo" . ("⊚"))+ ("o*" . ("⊛"))+ ("o=" . ("⊜"))+ ("o-" . ("⊝"))++ ("O+" . ("⨁"))+ ("Ox" . ("⨂"))+ ("O." . ("⨀"))+ ("O*" . ("⍟"))++ ;; Boxed operators.++ ("b+" . ("⊞"))+ ("b-" . ("⊟"))+ ("bx" . ("⊠"))+ ("b." . ("⊡"))++ ;; Various symbols.++ ("integral" . ,(pisigma-input-to-string-list "∫∬∭∮∯∰∱∲∳"))+ ("angle" . ,(pisigma-input-to-string-list "∟∡∢⊾⊿"))+ ("join" . ,(pisigma-input-to-string-list "⋈⋉⋊⋋⋌⨝⟕⟖⟗"))++ ;; Arrows.++ ("l" . ,(pisigma-input-to-string-list "←⇐⇚⇇⇆↤⇦↞↼↽⇠⇺↜⇽⟵⟸↚⇍⇷ ↹ ↢↩↫⇋⇜⇤⟻⟽⤆↶↺⟲ "))+ ("r" . ,(pisigma-input-to-string-list "→⇒⇛⇉⇄↦⇨↠⇀⇁⇢⇻↝⇾⟶⟹↛⇏⇸⇶ ↴ ↣↪↬⇌⇝⇥⟼⟾⤇↷↻⟳⇰⇴⟴⟿ ➵➸➙➔➛➜➝➞➟➠➡➢➣➤➧➨➩➪➫➬➭➮➯➱➲➳➺➻➼➽➾"))+ ("u" . ,(pisigma-input-to-string-list "↑⇑⟰⇈⇅↥⇧↟↿↾⇡⇞ ↰↱➦ ⇪⇫⇬⇭⇮⇯ "))+ ("d" . ,(pisigma-input-to-string-list "↓⇓⟱⇊⇵↧⇩↡⇃⇂⇣⇟ ↵↲↳➥ ↯ "))+ ("ud" . ,(pisigma-input-to-string-list "↕⇕ ↨⇳ "))+ ("lr" . ,(pisigma-input-to-string-list "↔⇔ ⇼↭⇿⟷⟺↮⇎⇹ "))+ ("ul" . ,(pisigma-input-to-string-list "↖⇖ ⇱↸ "))+ ("ur" . ,(pisigma-input-to-string-list "↗⇗ ➶➹➚ "))+ ("dr" . ,(pisigma-input-to-string-list "↘⇘ ⇲ ➴➷➘ "))+ ("dl" . ,(pisigma-input-to-string-list "↙⇙ "))++ ("l-" . ("←")) ("<-" . ("←")) ("l=" . ("⇐"))+ ("r-" . ("→")) ("->" . ("→")) ("r=" . ("⇒")) ("=>" . ("⇒"))+ ("u-" . ("↑")) ("u=" . ("⇑"))+ ("d-" . ("↓")) ("d=" . ("⇓"))+ ("ud-" . ("↕")) ("ud=" . ("⇕"))+ ("lr-" . ("↔")) ("<->" . ("↔")) ("lr=" . ("⇔")) ("<=>" . ("⇔"))+ ("ul-" . ("↖")) ("ul=" . ("⇖"))+ ("ur-" . ("↗")) ("ur=" . ("⇗"))+ ("dr-" . ("↘")) ("dr=" . ("⇘"))+ ("dl-" . ("↙")) ("dl=" . ("⇙"))++ ("l==" . ("⇚")) ("l-2" . ("⇇")) ("l-r-" . ("⇆"))+ ("r==" . ("⇛")) ("r-2" . ("⇉")) ("r-3" . ("⇶")) ("r-l-" . ("⇄"))+ ("u==" . ("⟰")) ("u-2" . ("⇈")) ("u-d-" . ("⇅"))+ ("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵"))++ ("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜"))+ ("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿"))+ ("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭"))++ ("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍"))+ ("r-n" . ("↛")) ("->n" . ("↛")) ("r=n" . ("⇏")) ("=>n" . ("⇏"))+ ("lr-n" . ("↮")) ("<->n" . ("↮")) ("lr=n" . ("⇎")) ("<=>n" . ("⇎"))++ ("l-|" . ("↤")) ("ll-" . ("↞"))+ ("r-|" . ("↦")) ("rr-" . ("↠"))+ ("u-|" . ("↥")) ("uu-" . ("↟"))+ ("d-|" . ("↧")) ("dd-" . ("↡"))+ ("ud-|" . ("↨"))++ ("dz" . ("↯"))++ ;; Ellipsis.++ ("..." . ,(pisigma-input-to-string-list "⋯⋮⋰⋱"))++ ;; Box-drawing characters.++ ("---" . ,(pisigma-input-to-string-list "─│┌┐└┘├┤┬┼┴╴╵╶╷╭╮╯╰╱╲╳"))+ ("--=" . ,(pisigma-input-to-string-list "═║╔╗╚╝╠╣╦╬╩ ╒╕╘╛╞╡╤╪╧ ╓╖╙╜╟╢╥╫╨"))+ ("--_" . ,(pisigma-input-to-string-list "━┃┏┓┗┛┣┫┳╋┻╸╹╺╻+ ┍┯┑┕┷┙┝┿┥┎┰┒┖┸┚┠╂┨┞╀┦┟╁┧┢╈┪┡╇┩+ ┮┭┶┵┾┽┲┱┺┹╊╉╆╅╄╃ ╿╽╼╾"))+ ("--." . ,(pisigma-input-to-string-list "╌╎┄┆┈┊+ ╍╏┅┇┉┋"))++ ;; Triangles.++ ;; Big/small, black/white.++ ("t" . ,(pisigma-input-to-string-list "◂◃◄◅▸▹►▻▴▵▾▿◢◿◣◺◤◸◥◹"))+ ("T" . ,(pisigma-input-to-string-list "◀◁▶▷▲△▼▽◬◭◮"))++ ("tb" . ,(pisigma-input-to-string-list "◂▸▴▾◄►◢◣◤◥"))+ ("tw" . ,(pisigma-input-to-string-list "◃▹▵▿◅▻◿◺◸◹"))++ ("Tb" . ,(pisigma-input-to-string-list "◀▶▲▼"))+ ("Tw" . ,(pisigma-input-to-string-list "◁▷△▽"))++ ;; Squares.++ ("sq" . ,(pisigma-input-to-string-list "■□◼◻◾◽▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳"))+ ("sqb" . ,(pisigma-input-to-string-list "■◼◾"))+ ("sqw" . ,(pisigma-input-to-string-list "□◻◽"))+ ("sq." . ("▣"))+ ("sqo" . ("▢"))++ ;; Rectangles.++ ("re" . ,(pisigma-input-to-string-list "▬▭▮▯"))+ ("reb" . ,(pisigma-input-to-string-list "▬▮"))+ ("rew" . ,(pisigma-input-to-string-list "▭▯"))++ ;; Parallelograms.++ ("pa" . ,(pisigma-input-to-string-list "▰▱"))+ ("pab" . ("▰"))+ ("paw" . ("▱"))++ ;; Diamonds.++ ("di" . ,(pisigma-input-to-string-list "◆◇◈"))+ ("dib" . ("◆"))+ ("diw" . ("◇"))+ ("di." . ("◈"))++ ;; Circles.++ ("ci" . ,(pisigma-input-to-string-list "●○◎◌◯◍◐◑◒◓◔◕◖◗◠◡◴◵◶◷⚆⚇⚈⚉"))+ ("cib" . ("●"))+ ("ciw" . ("○"))+ ("ci." . ("◎"))+ ("ci.." . ("◌"))+ ("ciO" . ("◯"))++ ;; Stars.++ ("st" . ,(pisigma-input-to-string-list "⋆✦✧✶✴✹ ★☆✪✫✯✰✵✷✸"))+ ("st4" . ,(pisigma-input-to-string-list "✦✧"))+ ("st6" . ("✶"))+ ("st8" . ("✴"))+ ("st12" . ("✹"))++ ;; Blackboard bold letters.++ ("bn" . ("ℕ"))+ ("bz" . ("ℤ"))+ ("bq" . ("ℚ"))+ ("br" . ("ℝ"))+ ("bc" . ("ℂ"))+ ("bp" . ("ℙ"))+ ("bsum" . ("⅀"))++ ;; Parentheses.++ ("(" . ,(pisigma-input-to-string-list "([{⁅⁽₍〈⎴⟦⟨⟪〈《「『【〔〖〚︵︷︹︻︽︿﹁﹃﹙﹛﹝（［｛｢"))+ (")" . ,(pisigma-input-to-string-list ")]}⁆⁾₎〉⎵⟧⟩⟫〉》」』】〕〗〛︶︸︺︼︾﹀﹂﹄﹚﹜﹞）］｝｣"))++ ("[[" . ("⟦"))+ ("]]" . ("⟧"))+ ("<" . ("⟨"))+ (">" . ("⟩"))+ ("<<" . ("⟪"))+ (">>" . ("⟫"))++ ;; Primes.++ ("'" . ,(pisigma-input-to-string-list "′″‴⁗"))+ ("`" . ,(pisigma-input-to-string-list "‵‶‷"))++ ;; Fractions.++ ("frac" . ,(pisigma-input-to-string-list "¼½¾⅓⅔⅕⅖⅗⅘⅙⅚⅛⅜⅝⅞⅟"))++ ;; Bullets.++ ("bu" . ,(pisigma-input-to-string-list "•◦‣⁌⁍"))+ ("bub" . ("•"))+ ("buw" . ("◦"))+ ("but" . ("‣"))++ ;; Musical symbols.++ ("note" . ,(pisigma-input-to-string-list "♩♪♫♬"))+ ("b" . ("♭"))+ ("#" . ("♯"))++ ;; Other punctuation and symbols.++ ("\\" . ("\\"))+ ("en" . ("–"))+ ("em" . ("—"))+ ("^i" . ("ⁱ"))+ ("!!" . ("‼"))+ ("??" . ("⁇"))+ ("?!" . ("‽" "⁈"))+ ("!?" . ("⁉"))+ ("die" . ,(pisigma-input-to-string-list "⚀⚁⚂⚃⚄⚅"))+ ("asterisk" . ,(pisigma-input-to-string-list "⁎⁑⁂✢✣✤✥✱✲✳✺✻✼✽❃❉❊❋"))+ ("8<" . ("✂" "✄"))+ ("tie" . ("⁀"))+ ("undertie" . ("‿"))+ ("apl" . ,(pisigma-input-to-string-list "⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈+ ⍉⍊⍋⍌⍍⍎⍏⍐⍑⍒⍓⍔⍕⍖⍗⍘⍙⍚⍛+ ⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮+ ⍯⍰⍱⍲⍳⍴⍵⍶⍷⍸⍹⍺⎕"))++ ;; Shorter forms of many greek letters plus ƛ.++ ("Ga" . ("α")) ("GA" . ("Α"))+ ("Gb" . ("β")) ("GB" . ("Β"))+ ("Gg" . ("γ")) ("GG" . ("Γ"))+ ("Gd" . ("δ")) ("GD" . ("Δ"))+ ("Ge" . ("ε")) ("GE" . ("Ε"))+ ("Gz" . ("ζ")) ("GZ" . ("Ζ"))+ ;; \eta \Eta+ ("Gth" . ("θ")) ("GTH" . ("θ"))+ ("Gi" . ("ι")) ("GI" . ("Ι"))+ ("Gk" . ("κ")) ("GK" . ("Κ"))+ ("Gl" . ("λ")) ("GL" . ("Λ")) ("Gl-" . ("ƛ"))+ ("Gm" . ("μ")) ("GM" . ("Μ"))+ ("Gn" . ("ν")) ("GN" . ("Ν"))+ ("Gx" . ("ξ")) ("GX" . ("Ξ"))+ ;; \omicron \Omicron+ ;; \pi \Pi+ ("Gr" . ("ρ")) ("GR" . ("Ρ"))+ ("Gs" . ("σ")) ("GS" . ("Σ"))+ ("Gt" . ("τ")) ("GT" . ("Τ"))+ ("Gu" . ("υ")) ("GU" . ("Υ"))+ ("Gf" . ("φ")) ("GF" . ("Φ"))+ ("Gc" . ("χ")) ("GC" . ("Χ"))+ ("Gp" . ("ψ")) ("GP" . ("Ψ"))+ ("Go" . ("ω")) ("GO" . ("Ω"))++ ;; Some ISO8859-1 characters.++ (" " . (" "))+ ("!" . ("¡"))+ ("cent" . ("¢"))+ ("brokenbar" . ("¦"))+ ("degree" . ("°"))+ ("?" . ("¿"))+ ("^a_" . ("ª"))+ ("^o_" . ("º"))++ ;; Circled, parenthesised etc. numbers and letters.++ ( "(0)" . ,(pisigma-input-to-string-list " ⓪"))+ ( "(1)" . ,(pisigma-input-to-string-list "⑴①⒈❶➀➊"))+ ( "(2)" . ,(pisigma-input-to-string-list "⑵②⒉❷➁➋"))+ ( "(3)" . ,(pisigma-input-to-string-list "⑶③⒊❸➂➌"))+ ( "(4)" . ,(pisigma-input-to-string-list "⑷④⒋❹➃➍"))+ ( "(5)" . ,(pisigma-input-to-string-list "⑸⑤⒌❺➄➎"))+ ( "(6)" . ,(pisigma-input-to-string-list "⑹⑥⒍❻➅➏"))+ ( "(7)" . ,(pisigma-input-to-string-list "⑺⑦⒎❼➆➐"))+ ( "(8)" . ,(pisigma-input-to-string-list "⑻⑧⒏❽➇➑"))+ ( "(9)" . ,(pisigma-input-to-string-list "⑼⑨⒐❾➈➒"))+ ("(10)" . ,(pisigma-input-to-string-list "⑽⑩⒑❿➉➓"))+ ("(11)" . ,(pisigma-input-to-string-list "⑾⑪⒒"))+ ("(12)" . ,(pisigma-input-to-string-list "⑿⑫⒓"))+ ("(13)" . ,(pisigma-input-to-string-list "⒀⑬⒔"))+ ("(14)" . ,(pisigma-input-to-string-list "⒁⑭⒕"))+ ("(15)" . ,(pisigma-input-to-string-list "⒂⑮⒖"))+ ("(16)" . ,(pisigma-input-to-string-list "⒃⑯⒗"))+ ("(17)" . ,(pisigma-input-to-string-list "⒄⑰⒘"))+ ("(18)" . ,(pisigma-input-to-string-list "⒅⑱⒙"))+ ("(19)" . ,(pisigma-input-to-string-list "⒆⑲⒚"))+ ("(20)" . ,(pisigma-input-to-string-list "⒇⑳⒛"))++ ("(a)" . ,(pisigma-input-to-string-list "⒜Ⓐⓐ"))+ ("(b)" . ,(pisigma-input-to-string-list "⒝Ⓑⓑ"))+ ("(c)" . ,(pisigma-input-to-string-list "⒞Ⓒⓒ"))+ ("(d)" . ,(pisigma-input-to-string-list "⒟Ⓓⓓ"))+ ("(e)" . ,(pisigma-input-to-string-list "⒠Ⓔⓔ"))+ ("(f)" . ,(pisigma-input-to-string-list "⒡Ⓕⓕ"))+ ("(g)" . ,(pisigma-input-to-string-list "⒢Ⓖⓖ"))+ ("(h)" . ,(pisigma-input-to-string-list "⒣Ⓗⓗ"))+ ("(i)" . ,(pisigma-input-to-string-list "⒤Ⓘⓘ"))+ ("(j)" . ,(pisigma-input-to-string-list "⒥Ⓙⓙ"))+ ("(k)" . ,(pisigma-input-to-string-list "⒦Ⓚⓚ"))+ ("(l)" . ,(pisigma-input-to-string-list "⒧Ⓛⓛ"))+ ("(m)" . ,(pisigma-input-to-string-list "⒨Ⓜⓜ"))+ ("(n)" . ,(pisigma-input-to-string-list "⒩Ⓝⓝ"))+ ("(o)" . ,(pisigma-input-to-string-list "⒪Ⓞⓞ"))+ ("(p)" . ,(pisigma-input-to-string-list "⒫Ⓟⓟ"))+ ("(q)" . ,(pisigma-input-to-string-list "⒬Ⓠⓠ"))+ ("(r)" . ,(pisigma-input-to-string-list "⒭Ⓡⓡ"))+ ("(s)" . ,(pisigma-input-to-string-list "⒮Ⓢⓢ"))+ ("(t)" . ,(pisigma-input-to-string-list "⒯Ⓣⓣ"))+ ("(u)" . ,(pisigma-input-to-string-list "⒰Ⓤⓤ"))+ ("(v)" . ,(pisigma-input-to-string-list "⒱Ⓥⓥ"))+ ("(w)" . ,(pisigma-input-to-string-list "⒲Ⓦⓦ"))+ ("(x)" . ,(pisigma-input-to-string-list "⒳Ⓧⓧ"))+ ("(y)" . ,(pisigma-input-to-string-list "⒴Ⓨⓨ"))+ ("(z)" . ,(pisigma-input-to-string-list "⒵Ⓩⓩ"))++ ))+ "A list of translations specific to the PiSigma input method.+Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS).+All the translation strings are possible translations+of the given key sequence; if there is more than one you can choose+between them using the arrow keys.++Note that if you customize this setting you will not+automatically benefit (or suffer) from modifications to its+default value when the library is updated. If you just want to+add some bindings it is probably a better idea to customize+`pisigma-input-user-translations'.++These translation pairs are included after those in+`pisigma-input-user-translations', but before the ones inherited+from other input methods (see `pisigma-input-inherit').++If you change this setting manually (without using the+customization buffer) you need to call `pisigma-input-setup' in+order for the change to take effect."+ :group 'pisigma-input+ :set 'pisigma-input-incorporate-changed-setting+ :initialize 'custom-initialize-default+ :type '(repeat (cons (string :tag "Key sequence")+ (repeat :tag "Translations" string))))++(defcustom pisigma-input-user-translations nil+ "Like `pisigma-input-translations', but more suitable for user+customizations since by default it is empty.++These translation pairs are included first, before those in+`pisigma-input-translations' and the ones inherited from other input+methods."+ :group 'pisigma-input+ :set 'pisigma-input-incorporate-changed-setting+ :initialize 'custom-initialize-default+ :type '(repeat (cons (string :tag "Key sequence")+ (repeat :tag "Translations" string))))++;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;+;; Inspecting and modifying translation maps++(defun pisigma-input-get-translations (qp)+ "Return a list containing all translations from the Quail+package QP (except for those corresponding to ASCII).+Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)."+ (with-temp-buffer+ (activate-input-method qp) ; To make sure that the package is loaded.+ (unless (quail-package qp)+ (error "%s is not a Quail package." qp))+ (let ((decode-map (list 'decode-map)))+ (quail-build-decode-map (list (quail-map)) "" decode-map 0)+ (cdr decode-map))))++(defun pisigma-input-show-translations (qp)+ "Display all translations used by the Quail package QP (a string).+\(Except for those corresponding to ASCII)."+ (interactive (list (read-input-method-name+ "Quail input method (default %s): " "PiSigma")))+ (let ((buf (concat "*" qp " input method translations*")))+ (with-output-to-temp-buffer buf+ (with-current-buffer buf+ (quail-insert-decode-map+ (cons 'decode-map (pisigma-input-get-translations qp)))))))++(defun pisigma-input-add-translations (trans)+ "Add the given translations TRANS to the PiSigma input method.+TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The+translations are appended to the current translations."+ (with-temp-buffer+ (dolist (tr (pisigma-input-concat-map (eval pisigma-input-tweak-all) trans))+ (quail-defrule (car tr) (cdr tr) "PiSigma" t))))++(defun pisigma-input-inherit-package (qp &optional fun)+ "Let the PiSigma input method inherit the translations from the+Quail package QP (except for those corresponding to ASCII).++The optional function FUN can be used to modify the translations.+It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return+a list of such pairs."+ (let ((trans (pisigma-input-get-translations qp)))+ (pisigma-input-add-translations+ (if fun (pisigma-input-concat-map fun trans)+ trans))))++;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;+;; Setting up the input method++(defun pisigma-input-setup ()+ "Set up the PiSigma input method based on the customisable+variables and underlying input methods."++ ;; Create (or reset) the input method.+ (with-temp-buffer+ (quail-define-package "PiSigma" "UTF-8" "∏Σ" t ; guidance+ "PiSigma input method.+The purpose of this input method is to edit PiSigma programs, but+since it is highly customisable it can be made useful for other+tasks as well."+ nil nil nil nil nil nil t ; maximum-shortest+ ))++ (pisigma-input-add-translations+ (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr))))+ (append pisigma-input-user-translations+ pisigma-input-translations)))+ (dolist (def pisigma-input-inherit)+ (pisigma-input-inherit-package (car def)+ (eval (cdr def)))))++(defun pisigma-input-incorporate-changed-setting (sym val)+ "Update the PiSigma input method based on the customisable+variables and underlying input methods. Suitable for use in+the :set field of `defcustom'."+ (set-default sym val)+ (pisigma-input-setup))++;; Set up the input method.++(pisigma-input-setup)++;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;+;; Administrative details++(provide 'pisigma-input)+;;; pisigma-input.el ends here
+ emacs-mode/pisigma-mode.el view
@@ -0,0 +1,140 @@+;;; pisigma-mode.el --- PiSigma major mode++;; Author: DarinMorrison+;; Keywords: extensions++;; Copyright (c) 2009, Darin Morrison+;; All rights reserved.++;; Redistribution and use in source and binary forms, with or without+;; modification, are permitted provided that the following conditions+;; are met:++;; 1. Redistributions of source code must retain the above copyright+;; notice, this list of conditions and the following disclaimer.++;; 2. Redistributions in binary form must reproduce the above+;; copyright notice, this list of conditions and the following+;; disclaimer in the documentation and/or other materials provided+;; with the distribution.++;; 3. Neither the name of the author nor the names of his contributors+;; may be used to endorse or promote products derived from this+;; software without specific prior written permission.++;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+;; "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+;; LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS+;; FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE+;; COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT,+;; INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+;; (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+;; SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+;; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+;; STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)+;; ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED+;; OF THE POSSIBILITY OF SUCH DAMAGE.++;;; Commentary:+;; ++;;; History:+;; ++;;; Code:++(require 'eri)+(require 'pisigma-input)++;; Associate .pi files with pisigma-mode+(add-to-list 'auto-mode-alist '("\\.pi\\'" . pisigma-mode))+(modify-coding-system-alist 'file "\\.pi$" 'utf-8)++(defgroup pisigma nil+ "Major mode for editing PiSigma programs."+ :group 'languages)++(defcustom pisigma-mode-hook nil+ "Hook run after entering PiSigma mode."+ :type 'hook+ :group 'pisigma)++(defvar pisigma-mode-map+ (let ((keymap (make-sparse-keymap)))+ keymap)+ "Keymap for `pisigma-mode'.")++(defvar pisigma-mode-syntax-table+ (let ((syntax-table (make-syntax-table)))+ (modify-syntax-entry ?\ " " syntax-table)+ (modify-syntax-entry ?\t " " syntax-table)+ (modify-syntax-entry ?\' "\'" syntax-table)+ (modify-syntax-entry ?_ "w" syntax-table)+ (modify-syntax-entry ?\( "()" syntax-table)+ (modify-syntax-entry ?\) ")(" syntax-table)+ (modify-syntax-entry ?\[ "(]" syntax-table)+ (modify-syntax-entry ?\] ")[" syntax-table)+ (modify-syntax-entry ?{ "(}1n" syntax-table)+ (modify-syntax-entry ?} "){4n" syntax-table)+ (modify-syntax-entry ?- "w 123b" syntax-table)+ (modify-syntax-entry ?\n "> b" syntax-table)+ syntax-table)+ "Syntax table for `pisigma-mode'.")++;; TODO: 1. matcher functions for type signatures and variables.+;; 2. multiline font-lock for case?+(defvar pisigma-font-lock-keywords+ '(("^\\(:l\\)\\s-*\\([^ \t\n]+\\)"+ (1 font-lock-preprocessor-face)+ (2 font-lock-constant-face))+ ("^\\([[:alpha:]][[:alnum:]_']*\\)[[:space:]]*:"+ (1 font-lock-function-name-face))+ ("^\\([[:alpha:]][[:alnum:]_']*\\)[[:space:]]*="+ (1 font-lock-function-name-face))+ ("\\<Type\\>" . font-lock-type-face)+ ("\\<\\(case\\|in\\|let\\|of\\|split\\|with\\)\\>" . font-lock-keyword-face)+ ("\\[\\|\\]\\|♯\\|!\\|♭\\|\\^\\|∞" . font-lock-warning-face)+ ("\\('\\)\\([[:alpha:]][[:alnum:]_']*\\)"+ (1 font-lock-warning-face)+ (2 font-lock-constant-face)))+ "Keyword highlighting specification for `pisigma-mode'.")++(defvar pisigma-imenu-generic-expression+ nil)++(defvar pisigma-outline-regexp+ nil)++;;; Indentation++(defun pisigma-indent-line ()+ "This is what happens when TAB is pressed."+ (interactive)+ (eri-indent))++(defun agda2-indent-line-reverse ()+ "This is what happens when S-TAB is pressed."+ (interactive)+ (eri-indent-reverse))++;;;###autoload+(define-derived-mode pisigma-mode fundamental-mode "PiSigma"+ "A major mode for editing PiSigma files."+ :syntax-table pisigma-mode-syntax-table+ (set (make-local-variable 'comment-start) "-- ")+ (set (make-local-variable 'comment-start-skip) "[-{]-[ \t]*")+ (set (make-local-variable 'comment-end) "")+ (set (make-local-variable 'comment-end-skip) "[ \t]*\\(-}\\|\\s>\\)")+ (set (make-local-variable 'font-lock-defaults) '(pisigma-font-lock-keywords))+ (set (make-local-variable 'indent-line-function) 'pisigma-indent-line)+ (set (make-local-variable 'imenu-generic-expression) pisigma-imenu-generic-expression)+ (set (make-local-variable 'outline-regexp) pisigma-outline-regexp)+ (set (make-local-variable 'parse-sexp-ignore-comments) t)+ ;; Protect global value of default-input-method from set-input-method.+ (make-local-variable 'default-input-method)+ (set (make-local-variable 'ident-tabs-mode) nil)+ (set (make-local-variable 'tab-width) 8)+ (set-input-method "PiSigma"))++(provide 'pisigma-mode)+;;; pisigma-mode.el ends here
+ examples/Broken.pi view
@@ -0,0 +1,9 @@+Bool : Type;+Bool = { true false };++broken : Bool -> Bool;+broken = \ b -> case b of {+ true -> 'true+ | true -> 'true+ | false -> 'true };+
+ examples/Curry.pi view
@@ -0,0 +1,13 @@+⊥ : Type;+⊥ = {};++-- Curry's paradox (usually ruled out by positivity check).++A : Type;+A = [A] → ⊥;++¬A : A → ⊥;+¬A = λ x → x x;++contradiction : ⊥;+contradiction = ¬A (λ x → ¬A x);
− examples/Data.pi
@@ -1,107 +0,0 @@-:l Maybe.pi-:l Bool.pi--data : Type;-El : data -> Type;--data = ( l : {empty maybe sigma box} ) * - case l of {- empty -> Unit- | maybe -> [data]- | sigma -> [(a : data) * (El a -> data)]- | box -> [^ data] }; --El = \ a -> split a with (la,a') ->- case la of {- empty -> {}- | maybe -> [Maybe (El a')]- | sigma -> split a' with (b,c) ->- [(x:El b)*(El (c x))]- | box -> [El (! a')] };--unit : data;-unit = ('maybe,('empty,'unit));--un : El unit;-un = ('nothing,'unit);--bool : data;-bool = ('maybe, unit);--tt : El bool;-tt = ('nothing,'unit);--ff : El bool;-ff = ('just,('nothing,'unit));--nat : data;-nat = ('sigma,(bool,\ b -> split b with (lb,b') ->- case lb of {- nothing -> unit- | just -> ('box, [nat]) }));- -zero : El nat;-zero = (tt,un);--succ : El nat -> El nat;-succ = \ n -> (ff,n);--Eq : Type -> Type;-Eq = \ A -> A -> A -> Bool;--eqMaybe : (A:Type) -> Eq A -> Eq (Maybe A);-eqMaybe = \ A eqA a b ->- split a with (la,a') ->- split b with (lb,b') ->- case la of {- nothing -> case lb of {- nothing -> 'true - | just -> 'false }- | just -> case lb of {- nothing -> 'false- | just -> eqA a' b'}};---eq : (a : data) -> Eq (El a);--subst : (a : data) - -> (x:El a) -> (y : El a) -> T (eq a x y)- -> (P : El a -> Type) -> P x -> P y;--sigmab : (b : Bool) -> (T b -> Bool) -> Bool;-sigmab = \ b c -> case b of {- true -> c 'unit- | false -> 'false };--eq = \ a x y -> split a with (la,a') ->- ! case la of {- empty -> case x of {} - | maybe -> [eqMaybe (El a') (eq a') x y]- | sigma -> split a' with (b,c) ->- split x with (x0,x1) ->- split y with (y0,y1) ->- [sigmab (eq b x0 y0)- (\ p -> eq (c y0) - (subst b x0 y0 p (\ x -> El (c x))- x1) y1)]- | box -> [eq (! a') x y]}; --{--subst = \ a x y p P px ->- split a with (la,a') ->- ! case la of {- empty -> case x of {} - | maybe -> split x with (lx,x') ->- split y with (ly,y') -> - case lx of {- nothing -> (case ly of {- nothing -> (case x' of {- unit -> case y' of {- unit -> [px] } })- | just -> case p of {}})- | just -> case ly of {- nothing -> (case p of {})- | just -> [subst a' x' y' p (\ z -> P ('just,z)) px]}}- | sigma -> [subst a x y p P px]- | box -> [subst (! a') x y p P px]}; --}
− examples/EqProb.pi
@@ -1,39 +0,0 @@-Eq : (a:Type) -> a -> a -> Type;-Eq = \ a x y -> (P : a -> Type) -> P x -> P y;--refl : (a:Type) -> (x:a) -> Eq a x x;-refl = \ a x P px -> px;--Stream : Type;-Stream = (tag : {Cons}) * case tag of {Cons -> [^Stream] };--ticks : Stream;-ticks = ('Cons, [ticks]);--l1 : Eq Stream ticks ('Cons, [ticks]);-l1 = refl Stream ticks;--l2 : (s : Stream) -> (t : Stream) -> (Eq Stream s t)- -> Eq Stream ('Cons, [s]) ('Cons, [t]);-l2 = \ s t q P p -> q (\ x -> P ('Cons,[x])) p;--{- bad error message! -}--{- unbox x with [y] -> t -- |- C : Type- |- x : ^A- y:A, x==[y] |- t : C- ------------------------------ |- unbox x with [y] -> t : C-- unbox [a] with [y] -> t ==> let y=a in t--- ![a] = a---}--{--l3 : (A:Type) -> (a:A) -> (b:A) -> Eq A a b -> Eq (^A) [a] [b];--}
examples/Equal.pi view
@@ -52,3 +52,63 @@ t6 : Eq A (id a) a; t6 = refl A a; +c:A;++t7 : Eq (A*(^A)) (let x:A=a in (a,[x])) (a,let x:A=a in [x])+ = refl (A*(^A)) (let x:A=a in (a,[x]));+++t8 : Eq (A*(^A)) (let x:A=a in (a,[x])) (a,let x:A=a in [x])+ = refl (A*(^A)) (let x:A=a in (a,[x]));++{-+t8a : Eq (^A) (let x:A=a in [x]) (let x:A=c in [x])+ = refl (^A) (let x:A=c in [x]);+-}++t9 : Eq (^(A * A)) (let x:A=a; y:A=c in [(x,y)]) (let y:A=c; x:A=a in [(x,y)])+ = refl (^(A * A)) (let x:A=a; y:A=c in [(x,y)]);++t9a : Eq (^(A * A)) (let x:A=a; y:A=c in [(x,y)]) (let y:A=c; x:A=a in [(x,y)])+ = refl (^(A * A)) (let x:A=a; y:A=c in [(x,y)]);++t10 : Eq (^A) (let x:A=a in [x]) (let x:A=a;y:A=x in [y])+ = refl (^A) (let x:A=a in [x]);+{- according due to the draft rules (Friday 30/10/09) should not work. -}++t11 : Eq (^(^A)) [let x:A=a in [x]] [let x:A=a;y:A=x in [y]]+ = refl (^(^A)) [let x:A=a in [x]];+{- works, uses bet equality in contexts. -}++t11a : Eq (^(^A)) [let x:A=a in [x]] [let y:A=a in [y]]+ = refl (^(^A)) [let x:A=a in [x]]; +{- works now -}++t12 : Eq (^A) (let y:A=y in [y]) (let z:A=z in [z])+ = refl (^A) (let y:A=y in [y]);++{-+t13 : Eq (^A) [let x:A=a in x] [a]+ = refl (^A) [a];+{- doesn't work and shouldn't. -}+-}++Stream : Type;+Stream = A * [∞ Stream];++as : Stream;+as = (a, [as]);++repeat : (x : A) → Stream;+repeat = λ x → (x, [repeat x]);++-- as is equal to its unfolding.++unfolds : Eq Stream as (a, [as]);+unfolds = refl Stream as;++-- repeat a is not equal to its unfolding.+{-+doesNotUnfold : Eq Stream (repeat a) (a, [repeat a]);+doesNotUnfold = refl Stream (repeat a);+-}
+ examples/Foo.pi view
@@ -0,0 +1,1 @@+Nat
+ examples/Hurkens.pi view
@@ -0,0 +1,42 @@+-- Hurkens' Paradox, a simplification of Girard's Paradox++-- (translated from Agda examples)++⊥ : Type;+⊥ = (α : Type) → α;++¬ : Type → Type;+¬ = λ α → α → ⊥;++P : Type → Type;+P = λ α → α → Type;++U : Type;+U = (χ : Type) → (P (P χ) → χ) → P (P χ);++τ : P (P U) → U;+τ = λ t χ f p → t (λ x → p (f (x χ f)));++σ : U → P (P U);+σ = λ s → s U (λ t → τ t);++Δ : P U;+Δ = λ y → ¬ ((p : P U) → σ y p → p (τ (σ y)));++Ω : U;+Ω = τ (λ p → (x : U) → σ x p → p x);++D : Type;+D = (p : P U) → σ Ω p → p (τ (σ Ω));++lem1 : (p : P U) → ((x : U) → σ x p → p x) → p Ω;+lem1 = λ p H1 → H1 Ω (λ x → H1 (τ (σ x)));++lem2 : ¬ D;+lem2 = lem1 Δ (λ x H2 H3 → H3 Δ H2 (λ p → H3 (λ y → p (τ (σ y)))));++lem3 : D;+lem3 = λ p → lem1 (λ y → p (τ (σ y)));++loop : ⊥;+loop = lem2 lem3;
+ examples/Parser.pi view
@@ -0,0 +1,89 @@+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;+Nat : type;
+ examples/Parser2.pi view
@@ -0,0 +1,331 @@+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;+Nat;
+ examples/Parser3.pi view
@@ -0,0 +1,331 @@+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat+Nat
+ examples/SubjectReduction.pi view
@@ -0,0 +1,58 @@+-- Context:+-- Recursion with boxes+-- Thorsten Altenkirch+-- http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=104++Stream : Type;+Stream = [∞ Stream];++ticks : Stream;+ticks = [ticks];++Eq : (A : Type) → A → A → Type;+Eq = λ A x y → (P : A → Type) → P x → P y;++refl : (A : Type) → (x : A) → Eq A x x;+refl = λ A x P px → px;++unfold : Eq Stream ticks [ticks];+unfold = refl Stream ticks;++-- We can prove this variant of congruence for boxes:++cong : (xs ys : Stream) → Eq Stream xs ys →+ Eq Stream [let zs : Stream = xs in zs]+ [let zs : Stream = ys in zs];+cong = λ xs ys eq P p → eq (λ zs → P [let us : Stream = zs in us]) p;++-- This does not (obviously) break subject reduction, because the+-- following property can be proved using refl:++unfoldInContext : Eq Stream [let xs : Stream = ticks in xs]+ [let xs : Stream = [ticks] in xs];+unfoldInContext = cong ticks [ticks] unfold;+unfoldInContext = refl Stream [let xs : Stream = ticks in xs];++-- Note also that unlimited unfolding is not possible (using refl):++-- unfoldTwiceInContext : Eq Stream [let xs : Stream = ticks in xs]+-- [let xs : Stream = [[ticks]] in xs];+-- unfoldTwiceInContext = refl Stream [let xs : Stream = ticks in xs];++-- However, we can move lets through boxes, so the idea from+-- Thorsten's blog post needs to be qualified.++letThroughBox : (xs : Stream) →+ Eq Stream [let ys : Stream = xs in ys]+ (let ys : Stream = xs in [ys]);+letThroughBox = λ xs → refl Stream [let ys : Stream = xs in ys];++letThrough2Boxes : (xs : Stream) →+ Eq Stream [[let ys : Stream = xs in ys]]+ (let ys : Stream = xs in [[ys]]);+letThrough2Boxes = λ xs → refl Stream [[let ys : Stream = xs in ys]];++anotherExample : (A : Type) → (x : A) →+ Eq (∞ (∞ A)) [let y : A = x in [y]]+ (let y : A = x in [[let z : A = y in z]]);+anotherExample = λ A x → refl (∞ (∞ A)) (let y : A = x in [[y]]);
− examples/Universe.pi
@@ -1,47 +0,0 @@-:l Maybe.pi--data : Type;-El : data -> Type;--data = ( l : {empty maybe sigma box} ) * - case l of {- empty -> Unit- | maybe -> [data]- | sigma -> [(a : data) * (El a -> data)]- | box -> [^ data] }; --El = \ a -> split a with (la,a') ->- case la of {- empty -> {}- | maybe -> Maybe [El a']- | sigma -> split a' with (b,c) ->- [(x:El b)*(El (c x))]- | box -> [El (! a')] };--unit : data;-unit = ('maybe,('empty,'unit));--un : El unit;-un = ('nothing,'unit);--bool : data;-bool = ('maybe, unit);--tt : El bool;-tt = ('nothing,'unit);--ff : El bool;-ff = ('just,('nothing,'unit));--nat : data;-nat = ('sigma,(bool,\ b -> split b with (lb,b') ->- case lb of {- nothing -> unit- | just -> ('box, [nat]) }));- -zero : El nat;-zero = (tt,un);--succ : El nat -> El nat;-succ = \ n -> (ff,n);-
examples/stl.pi view
@@ -129,3 +129,17 @@ lam : (g:Con) -> (a:Ty) -> (b:Ty) -> Lam (ext g a) b -> Lam g (arr a b); lam = \ g a b t -> ('lam,t);++{- ++Ren : Con -> Con -> Type+Subst : Con -> Con -> Type++Subst Γ Δ = {A : Ty} → Var Γ A → Tm Δ A++subst : (Γ Δ : Con) → ({A : Ty} → Var Γ A → Tm Δ A) → {A : Ty} → Tm Δ A → Tm Γ A+ren: (Γ Δ : Con) → Subst Γ Δ → {A : Ty} → Tm Δ A → Tm Γ A++monad laws...++-}
pisigma.cabal view
@@ -1,11 +1,15 @@ cabal-version: >= 1.6 name: pisigma-version: 0.1.0.2+version: 0.1.0.3 license: BSD3 license-file: LICENSE data-files: examples/*.pi+ emacs-mode/*.el author: Thorsten Altenkirch <txa@cs.nott.ac.uk>,- Andres Loeh <kspisigma@andres-loeh.de>+ Andres Loeh <kspisigma@andres-loeh.de>,+ Nils Anders Danielsson <nad@cs.nott.ac.uk>,+ Nicolas Oury <Nicolas.Oury@ed.ac.uk>,+ Darin Morrison <dwm@cs.nott.ac.uk> maintainer: Thorsten Altenkirch <txa@cs.nott.ac.uk>, Andres Loeh <kspisigma@andres-loeh.de> description: dependently typed core language@@ -13,19 +17,50 @@ category: Development, Language, Dependent Types build-type: Simple +library+ build-depends: array >= 0.2 && < 0.3,+ base >= 4.0 && < 5.0,+ bytestring >= 0.9 && < 1.0,+ haskeline >= 0.6 && < 0.7,+ haskeline-class >= 0.6.1 && < 0.7,+ mpppc >= 0.1.0 && < 0.2,+ mtl >= 1.1 && < 1.2,+ parsec >= 3.0 && < 4.0,+ text >= 0.5 && < 0.6,+ utf8-string >= 0.3.5 && < 0.4++ exposed-modules: Language.PiSigma.Check+ Language.PiSigma.Equality+ Language.PiSigma.Evaluate+ Language.PiSigma.Normalise+ Language.PiSigma.Lexer+ Language.PiSigma.Parser+ Language.PiSigma.Pretty+ Language.PiSigma.Syntax+ Language.PiSigma.Util.String.Internal+ Language.PiSigma.Util.String.Parser++ ghc-options: -funbox-strict-fields++ hs-source-dirs: src+++ executable pisigma- main-is: PiSigma.hs- other-modules: PiSigma.Check- PiSigma.Equality- PiSigma.Evaluation- PiSigma.Nf- PiSigma.Parser- PiSigma.Print- PiSigma.Syntax- hs-source-dirs:src- build-depends: base >= 4 && < 5,- array >= 0.2 && < 0.3,- mtl >= 1.1 && < 1.2,- haskeline >= 0.6 && < 0.7,- parsec >= 3 && < 4,- ansi-wl-pprint >= 0.5 && <1+ ghc-options: -funbox-strict-fields++ hs-source-dirs: src++ main-is: Tools/Interpreter/Main.hs++ other-modules: Language.PiSigma.Check+ Language.PiSigma.Equality+ Language.PiSigma.Evaluate+ Language.PiSigma.Normalise+ Language.PiSigma.Lexer+ Language.PiSigma.Parser+ Language.PiSigma.Pretty+ Language.PiSigma.Syntax+ Language.PiSigma.Util.String.Internal+ Language.PiSigma.Util.String.Parser+ Tools.Interpreter.REPL
+ src/Language/PiSigma/Check.hs view
@@ -0,0 +1,261 @@+{-# LANGUAGE OverloadedStrings #-}++module Language.PiSigma.Check+ ( checkProg+ , infer )+ where++import Control.Arrow+ ( first )+import Control.Monad.Error+import qualified Data.List+ as List++import Language.PiSigma.Equality+import Language.PiSigma.Evaluate+import Language.PiSigma.Pretty+import Language.PiSigma.Syntax+import qualified Language.PiSigma.Util.String.Internal+ as Internal++--import Debug.Trace+--trace "check\n" $++-- closures are the other way around+-- should be fixed by changing closures.++{-+fog :: CTerm -> Closure+fog (g,t) = (con2scope g,t)+-}++throwErrorc :: (Print b, GetLoc b, Env e) => b -> Pretty -> Eval e a+throwErrorc t m =+ do+ pt <- evalPrint t+ throwError $ fromPretty $+ text (Seq $ Internal.fromString $ locMessage $ getLoc t)+ <$> "Expression: " <+> align pt+ <$> m++expected :: (Env e) => Clos Term -> Val -> Pretty -> Eval e ()+expected t expected' inferred = do+ pExpected <- evalPrint expected'+ throwErrorc t $ "Expected type:" <+> align pExpected <$> parens inferred++expectedButFound :: (GetLoc a, Print a, Print b, Print c, Env e)+ => a+ -> b+ -> c+ -> Internal.String+ -> Eval e d+expectedButFound t expected' found inferred =+ do+ pExpected <- evalPrint expected'+ pFound <- evalPrint found+ throwErrorc t $+ "Inferred type:" <+> align pFound+ <$> "Expected type:" <+> align pExpected+ <$> parens (text . Seq $ inferred)++duplicateLabels :: (GetLoc a, Print a, Env e) => a -> Eval e d+duplicateLabels t =+ throwErrorc t $ "Duplicate labels in enum type"++nonLinearSplit :: (GetLoc a, Print a, Env e) => a -> Eval e d+nonLinearSplit t =+ throwErrorc t $ "Repeated variables in a split"++-- | Takes a term and an (unevaluated) type. We first+-- handle the cases that may potentially change the+-- environment. If none of those cases match, we can+-- safely evaluate the type and call check'.+check :: Env e => Clos Term -> Clos Type -> Eval e ()+--check (g,t) c | trace ("check\ng ="++(show g)++"\n t="++(show t)++"\nc="++(show c)++"\n") False = undefined++check (Let _ p t,g) c = + do g' <- checkProg (p,g)+ check (t,g') c++check (Split _ t (x,(y,u)),g) c | x==y = nonLinearSplit t+check (Split _ t (x,(y,u)),g) c | otherwise =+ do sigab <- infer' (t,g)+ case sigab of+ (VQ Sigma ((a,(z,b)),s)) -> + do t' <- eval (t,g)+ (_,g') <- tdecl x g (a,s) + b' <- subst (z,(b,s)) (Var Unknown x, g')+ (_,g'') <- tdecl y g' b'+ case t' of+ (Ne (NVar i)) ->+ letn' i (Pair Unknown (Var Unknown x) (Var Unknown y), g'')+ (check (u,g'') c)+ -- this is a bit silly since we know the ids.+ _ -> check (u,g'') c+ -- instead of failing, we just omit the assignment.+ _ -> expectedButFound (t,g) msg1 sigab msg2+ where+ msg1 = "sigma type" :: Internal.String+ msg2 = "split" :: Internal.String++check gt @ (Case _ t lus,g) c = + do enum <- infer' (t,g)+ case enum of+ VEnum ls -> + let ls' = map fst lus+ in if ls /= ls'+ then -- pt' <- evalPrint t'+ throwErrorc gt $ text $ Seq $+ Internal.concat [ "Labels don't match."+ , "\nProvided labels: ", Internal.fromString $ show ls+ , "\nExpected labels: ", Internal.fromString $ show ls'+ , "\n(Case)\n"+ ]+ -- set equivalence would be sufficent+ else do t' <- eval (t,g)+ case t' of+ -- if the scrutinee is a variable, we add a constraint+ -- while checking each of the branches+ (Ne (NVar i)) ->+ mapM_ (\ (l,u) -> + letn' i (label l)+ (check (u,g) c)) lus+ -- if the scrutinee is not a variable, we do not add+ -- a constraint, but continue+ _ -> mapM_ (\ (_,u) -> check (u,g) c) lus+ _ -> expectedButFound (t,g) msg1 enum msg2+ where+ msg1 = "enum type" :: Internal.String+ msg2 = "case" :: Internal.String+ ++ {- Problem: here and other places: we try to print the term t which isn't yet + typechecked and may contain undefined variables which may crash the printer...+ see undef-bug.pi+ -}+check (Force _ t,g) (a , s) =+ check (t,g) (Lift Unknown a , s)++check t a = check' t =<< feval a++check' :: Env e => Clos Term -> Val -> Eval e ()+-- we ignore boxes in types, this is the other part of the lifting story.+check' gt (VBox (Boxed a)) = check gt a +check' (Lam _ (x,t),g) (VQ Pi ((a,(y,b)),s)) =+ do (i,g') <- tdecl x g (a,s)+ let s' = extendScope s y (i,Nothing)+ check (t,g') (b,s')+check' gt @ (Lam _ _,_) a =+ expected gt a "Lam"+check' (Pair _ t u,g) (VQ Sigma ((a,(y,b)),s)) =+ do check (t,g) (a,s)+ b' <- subst (y,(b,s)) (t,g)+ check (u,g) b'+check' gt @ (Pair _ _ _, _) a =+ expected gt a "Pair"+-- Labels cannot be inferred because there is no way to know+-- what the other labels are.+check' (Label _ l,_) (VEnum ls) | l `elem` ls = return ()+check' gt @ (Label _ _,_) a =+ expected gt a "Label"+-- To check that [sigma] is a type, it's sufficient to know+-- that sigma is a type. The alternative would seem to be to+-- assume that ^Type == Type, but that does not work.+check' (Box _ a,g) VType = + check (a,g) ty+check' (Box _ t,g) (VLift a) =+ check (t,g) a+check' gt @ (Box _ _,_) a =+ expected gt a "Box"+check' t a =+ do b <- infer' t+ catchE (eq a b) $ const $ expectedButFound t a b "check"++inferVar :: Env e => Loc -> Clos Name -> Eval e (Clos Type)+inferVar l (x,g) =+ case lookupCon g x of+ Just a -> return a+ Nothing -> throwError msg+ where+ msg = Internal.concat [ Internal.fromString $ locMessage l+ , "\nUndefined variable: "+ , x+ , "\n(inferVar)\n"+ ]++infer :: Env e => Clos Term -> Eval e (Clos Type)+--infer (g,t) | trace ("infer\ng ="++(show g)++"\n t="++(show t)++"\n") False = undefined++infer (Var l x,g) = inferVar l (x,g)++infer (Let _ tel t,g) = + do g' <- checkProg (tel,g)+ infer (t,g') ++infer (Type _,_) = return ty++infer (Q _ _ (a,(x,b)),g) = + do check (a,g) ty+ (_,g') <- tdecl x g (a,g)+ check (b,g') ty+ return ty++infer (App t u,g) = + do piab <- infer' (t,g)+ case piab of + (VQ Pi ((a,(x,b)),s)) -> do check (u,g) (a,s)+ subst (x,(b,s)) (u,g)+ _ -> expectedButFound (t,g) msg1 piab msg2+ where+ msg1 = "pi type" :: Internal.String+ msg2 = "App" :: Internal.String++infer (t@(Enum _ ls),_) =+ if List.length (List.nub ls) < List.length ls+ then duplicateLabels t+ else return ty++infer (Box _ t,g) = liftM (first $ Lift Unknown) (infer (t,g))++-- TODO: either use infer', or explain why forced eval+-- cannot be used here.+infer (Force _ t,g) =+ do a <- infer (t,g)+ a' <- eval a+ case a' of+ VLift b -> return b+ _ -> expectedButFound (t,g) msg1 a' msg2+ where+ msg1 = "lifted type" :: Internal.String+ msg2 = "Force" :: Internal.String++infer (Lift _ a,g) =+ do check (a,g) ty+ return ty++-- infer (LType _ a,g) =+-- do check (a,g) lty+-- return ty+++infer gt = throwErrorc gt $ "Not inferable" <$> "(infer)"+++-- | Infers a type and evaluates it.+infer' :: Env e => Clos Term -> Eval e Val+infer' gt = feval =<< infer gt++checkProg :: Env e => Clos Prog -> Eval e Scope+checkProg ([],g) = return g+checkProg ((Decl _ x a):tel,g) = + do check (a,g) ty + (_,g') <- decl x PrtInfo{ name = x, expand = False } g (Just (a,g))+ checkProg (tel,g')+checkProg ((Defn l x t):tel,g) =+ do a <- inferVar l (x,g)+ check (t,g) a+ i <- getId l x g+ defn' i (t,g)+ checkProg (tel,g)+ +
+ src/Language/PiSigma/Equality.hs view
@@ -0,0 +1,129 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Language.PiSigma.Equality+ ( eq )+ where++import Control.Monad++import Language.PiSigma.Evaluate+import Language.PiSigma.Syntax++class Equal a where+ eq :: Env e => a -> a -> Eval e ()++instance Equal (Clos Term) where+ eq t u = do t' <- eval t+ u' <- eval u+ eq t' u'++-- unused?+-- eq' :: Env e => Clos (Term,Term) -> Eval e ()+-- eq' ((t,u),s) = eq (t,s) (u,s)++eqBind :: (Env e,Closure a) =>+ (a -> a -> Eval e ()) ->+ Bind a -> Bind a -> Eval e ()+eqBind eqArg (x0,c0) (x1,c1) =+ do let s0 = getScope c0+ s1 = getScope c1+ (i,s0') <- decl' x0 s0+ let s1' = extendScope s1 x1 (i,Nothing)+ let c0' = putScope c0 s0'+ c1' = putScope c1 s1'+ eqArg c0' c1'++instance (Equal a,Closure a) => Equal (Bind a) where+ eq = eqBind eq++instance Equal Val where+ eq (Ne t0) (Ne t1) = eq t0 t1+ eq (VQ ps0 ((a0,(x0,b0)),s0)) (VQ ps1 ((a1,(x1,b1)),s1))+ | ps0 == ps1 = + do eq (a0,s0) (a1,s1)+ eq (x0,(b0,s0)) (x1,(b1,s1))+ eq (VLam xt0) (VLam xt1) = eq xt0 xt1+ eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = + do eq (t0,s0) (t1,s1)+ eq (u0,s0) (u1,s1)+ eq (VBox b) (VBox b') = eq b b' + eq (VLift a) (VLift a') = eq a a'+-- eq (VLType a) (VLType a') = eq a a'+ eq v0 v1 | v0 == v1 = return () -- Type, Label, Enum+ | otherwise = fail "Different values"++{- eqBox implements alpha equality -}+eqBox :: Env e => Clos Term -> Clos Term -> Eval e ()+--eqBox c c' | c == c' = return ()+eqBox (Var l x,s) (Var l' y,s') = + do x' <- getId l x s+ y' <- getId l' y s'+ eq x' y'+eqBox (Let _ p t,s) c = + do s' <- evalProg (p,s)+ eqBox (t,s') c+eqBox c c'@(Let _ _ _,_) = eqBox c' c +eqBox (Q _ ps (a,(x,b)),s) (Q _ ps' (a',(x',b')),s')+ | ps == ps' = + do eqBox (a,s) (a',s')+ eq (x,Boxed (b,s)) (x',Boxed (b',s'))+eqBox (Lam _ (x,t),s) (Lam _ (x',t'),s') =+ eq (x,Boxed (t,s)) (x',Boxed (t',s'))+eqBox (App t u,s) (App t' u',s') =+ do eqBox (t,s) (t',s')+ eqBox (u,s) (u',s')+eqBox (Pair _ t u,s) (Pair _ t' u',s') =+ do eqBox (t,s) (t',s')+ eqBox (u,s) (u',s')+eqBox (Split _ t (x,(y,u)),s) (Split _ t' (x',(y',u')),s') =+ do eqBox (t,s) (t',s')+ eq (x,(y,Boxed (u,s))) (x',(y',Boxed (u',s')))+eqBox (Case _ t bs,s) (Case _ t' bs',s') =+ do eqBox (t,s) (t',s')+ zipWithM_ (\ (l,t'') (l',t''') -> + if l==l' then eqBox (t'',s) (t''',s')+ else fail "eqBox case") bs bs'+eqBox (Lift _ t,s) (Lift _ t',s') = eqBox (t,s) (t',s')+-- eqBox (LType _ t,s) (LType _ t',s') = eqBox (t,s) (t',s')+eqBox (Box _ t,s) (Box _ t',s') = eqBox (t,s) (t',s')+eqBox (Force _ t,s) (Force _ t',s') = eqBox (t,s) (t',s') +eqBox (t,_) (t',_) | t == t' = return () -- Type, Label, Enum+ | otherwise = fail "Different terms"+ +instance Equal Boxed where+ eq (Boxed c) (Boxed c') = eqBox c c'++instance Equal Id where+ eq i0 i1 + | i0 == i1 = return ()+ | otherwise = do ei0 <- lookupId i0+ ei1 <- lookupId i1+ case (ei0,ei1) of+ (Id j0, Id j1) -> unless (j0 == j1)+ (fail "Different variables")+ (Closure t0, Closure t1) ->+ letn i0 (Id i0)+ (letn i1 (Id i0)+ (eq t0 t1))+ _ -> fail "Variable vs neutral"++instance Equal Ne where+ eq (NVar i0) (NVar i1) = eq i0 i1+ eq (t0 :.. u0) (t1 :.. u1) = + do eq t0 t1+ eq u0 u1+ eq (NSplit t0 xyu0) (NSplit t1 xyu1) =+ do eq t0 t1+ eq xyu0 xyu1+ eq (NCase t0 (lus0,s0)) (NCase t1 (lus1,s1)) =+ do eq t0 t1+ let eqBranches [] [] = return ()+ eqBranches ((l0,u0):lus0') ((l1,u1):lus1')+ | l0 == l1 = do+ eq (u0,s0) (u1,s1)+ eqBranches lus0' lus1'+ eqBranches _ _ = fail "Case: branches differ"+ eqBranches lus0 lus1+ eq (NForce t) (NForce t') = eq t t'+ eq t u = fail ("Different neutrals:\n"++ show t ++"\n/=\n"++ show u ++"\n")
+ src/Language/PiSigma/Evaluate.hs view
@@ -0,0 +1,190 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Language.PiSigma.Evaluate+ ( Eval (..)+ , catchE+ , decl+ , decl'+ , defn'+ , eval+ , evalProg+ , feval+ , getEnv+ , getId+ , letn+ , letn'+ , lookupId+ , run+ , subst+ , tdecl )+ where++import Control.Monad.Error+import Control.Monad.State+import Control.Monad.Identity++import Language.PiSigma.Syntax+import qualified Language.PiSigma.Util.String.Internal+ as Internal++-- * Monad used for evaluation++type EvalErr = Internal.String++instance Error EvalErr where+++newtype Eval e a = Eval { unEval :: StateT e (ErrorT EvalErr Identity) a }+ deriving ( Monad+ , MonadError EvalErr+ , MonadState e )++run :: e -> Eval e a -> Either EvalErr (a, e)+run e (Eval p) = runIdentity $ runErrorT $ runStateT p e ++catchE :: Eval e a -> (EvalErr -> Eval e a) -> Eval e a+catchE = catchError++getEnv :: Eval e e+getEnv = get++setEnv :: e -> Eval e ()+setEnv = put++getId :: Loc -> Name -> Scope -> Eval e Id+getId l x s = case lookupScope s x of + Just i -> return i+ Nothing -> throwError msg+ where+ msg = Internal.concat [ Internal.fromString $ locMessage l+ , "\nUndefined variable: "+ , x+ , "\n"+ ]++-- | Takes a name, a scope, and potentially a type.+-- It extends the environment and the scope with that name.+decl :: Env e+ => Name+ -> PrtInfo+ -> Scope+ -> Maybe (Clos Type)+ -> Eval e (Id, Scope)+decl x x' s a =+ do e <- getEnv+ let (i,e') = extE e x'+ setEnv e'+ return (i,extendScope s x (i,a))++decl' :: Env e => Name -> Scope -> Eval e (Id, Scope)+decl' x s = decl x PrtInfo{ name = x, expand = True } s Nothing++tdecl :: Env e => Name -> Scope -> (Clos Type) -> Eval e (Id, Scope)+tdecl x g = decl x PrtInfo{ name = x, expand = True } g . Just++-- | Updates the environment.+defn :: Env e => Id -> EnvEntry -> Eval e ()+defn i ei =+ do e <- getEnv+ setEnv (setE e i ei)++defn' :: Env e => Id -> Clos Type -> Eval e ()+defn' i = defn i . Closure++-- | Locally updates the environment.+letn :: Env e => Id -> EnvEntry -> Eval e a -> Eval e a+letn i ei p =+ do eo <- lookupId i+ defn i ei+ a <- p+ defn i eo+ return a++letn' :: Env e => Id -> Clos Type -> Eval e a -> Eval e a+letn' i = letn i . Closure++subst :: Env e => Bind (Clos Term) -> (Clos Term) -> Eval e (Clos Term)+subst (x,(t,s)) u =+ do (i,s') <- decl' x s+ defn' i u + return (t,s')++evalApp :: Env e => Val -> (Clos Term) -> Eval e Val+evalApp (VLam xt) u = eval =<< subst xt u+evalApp (Ne t) u = return (Ne (t :.. u))+evalApp _ _ = throwError "function expected"++lookupId :: Env e => Id -> Eval e EnvEntry+lookupId i = liftM (flip getE i) getEnv++evalId :: Env e => Id -> Eval e Val+evalId i =+ do ei <- lookupId i+ case ei of+ Closure t -> eval t+ Id j -> return (Ne (NVar j))++-- use subst!+evalSplit :: Env e+ => Val+ -> Bind (Bind (Clos Term))+ -> Eval e Val+evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) = + do (x',s2) <- decl' x s'+ (y',s3) <- decl' y s2+ defn' x' (l,s)+ defn' y' (r,s)+ eval (t,s3)++evalSplit (Ne n) (xy,t) = return (Ne (NSplit n (xy,t)))+evalSplit _ _ = throwError "Pair expected"++evalCase :: Env e => Val -> Clos [(Label,Term)] -> Eval e Val+evalCase (VLabel l) (lts,s) = + case lookup l lts of+ Nothing -> throwError "case not matched"+ Just t -> eval (t,s)+evalCase (Ne n) lts = return (Ne (NCase n lts))+evalCase _ _ = throwError "Label expected"++force :: Env e => Val -> Eval e Val+force (VBox (Boxed c)) = eval c+force (Ne n) = return (Ne (NForce n))+force _ = throwError "Box expected"++eval :: Env e => (Clos Term) -> Eval e Val+eval (Var l x, s) = evalId =<< getId l x s+eval (Let _ g t, s) = curry eval t =<< evalProg (g,s)+eval (Type _, _) = return VType+eval (Q _ ps axb, s) = return (VQ ps (axb,s))+eval (Lift _ t, s) = return (VLift (t,s))+--eval (LType _ t, s) = return (VLType (t,s))+eval (Lam _ (x,t), s) = return (VLam (x,(t,s)))+eval (App t u, s) = flip evalApp (u,s) =<< eval (t,s)+eval (Pair _ t u, s) = return (VPair ((t,u),s))+eval (Split _ t (x, (y, u)), s) = flip evalSplit (x,(y,(u,s))) =<< eval (t,s)+eval (Enum _ ls, _) = return (VEnum ls)+eval (Label _ l, _) = return (VLabel l)+eval (Case _ t lts, s) = flip evalCase (lts,s) =<< eval (t,s)+eval (Box _ t, s) = return (VBox (Boxed (t,s)))+eval (Force _ t, s) = force =<< eval (t,s)+++-- forced eval (should be integrated into eval?)+feval :: Env e => (Clos Term) -> Eval e Val+feval t = do t' <- eval t+ case t' of + VBox (Boxed u) -> feval u+ v -> return v++ ++evalProg :: Env e => Clos Prog -> Eval e Scope+evalProg ([],s) = return s+evalProg ((Decl _ x _):tel, s) = do (_,s') <- decl x (PrtInfo x False) s Nothing+ evalProg (tel,s')+evalProg ((Defn l x t):tel, s) = do i <- getId l x s+ defn' i (t,s)+ evalProg (tel,s)
+ src/Language/PiSigma/Lexer.hs view
@@ -0,0 +1,278 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Language.PiSigma.Lexer+ ( Parser+ , angles+ , braces+ , brackets+ , charLiteral+ , colon+ , comma+ , commaSep+ , commaSep1+ , decimal+ , dot+ , float+ , hexadecimal+ , identifier+ , integer+ , locate+ , location+ , locReserved+ , locReservedOp+ , locSymbol+ , lexeme+ , natural+ , naturalOrFloat+ , octal+ , operator+ , parens+ , reserved+ , reservedOp+ , semi+ , semiSep+ , semiSep1+ , squares+ , stringLiteral+ , symbol+ , tokArr+ , tokForce+ , tokLam+ , tokLift+ , whiteSpace )+ where++import Control.Applicative+import Control.Monad.Identity+import Data.Char+import Text.Parsec.Prim+ ( Parsec+ , Stream (..)+ , (<?>)+ , getPosition+ )+import qualified Text.Parsec.Token+ as Token+import Text.ParserCombinators.Parsec+ ( SourcePos+ , choice+ , sourceColumn+ , sourceLine+ , sourceName )+import Text.ParserCombinators.Parsec.Char++import Language.PiSigma.Syntax+ ( Loc (..) )+import qualified Language.PiSigma.Util.String.Parser+ as Parser++instance (Monad m) => Stream Parser.String m Char where+ uncons = return . Parser.uncons++type Parser = Parsec Parser.String ()++nonIdentStr :: String+nonIdentStr = [ '('+ , ')'+ , '['+ , ']'+ , '{'+ , '}' ]++opLetterStr :: String+opLetterStr = [ '!'+ , '*'+ , ','+ , '-'+ , ':'+ , ';'+ , '='+ , '>'+ , '\\'+ , '^'+ , '|'+ , '♭'+ , '♯'+ , 'λ'+ , '→'+ , '∞' ]++-- * The lexical definition of PiSigma. Used to make token parsers.+pisigmaDef :: (Monad m) => Token.GenLanguageDef Parser.String u m+pisigmaDef = Token.LanguageDef+ { Token.commentStart = "{-"+ , Token.commentEnd = "-}"+ , Token.commentLine = "--"+ , Token.nestedComments = True+ , Token.identStart = satisfy $ \ c -> not (isSpace c)+ && not (c `elem` nonIdentStr)+ && not (c `elem` opLetterStr)+ && not (isControl c)+ && not (isDigit c)+ , Token.identLetter = satisfy $ \ c -> not (isSpace c)+ && not (c `elem` nonIdentStr)+ && not (c `elem` opLetterStr)+ && not (isControl c)+ , Token.opStart = oneOf ""+ , Token.opLetter = oneOf opLetterStr+ , Token.reservedNames = [ "Type"+ , "case"+ , "in"+ , "let"+ , "of"+ , "split"+ , "with" ]+ , Token.reservedOpNames = [ "!"+ , "*"+ , ","+ , "->"+ , ":"+ , ";"+ , "=" + , "\\"+ , "^"+ , "|"+ , "♭"+ , "♯"+ , "λ"+ , "→"+ , "∞" ]+ , Token.caseSensitive = True+ }++-- * The PiSigma token parser, generated from the lexical definition.++tokenParser :: Token.GenTokenParser Parser.String () Identity+tokenParser = Token.makeTokenParser pisigmaDef++-- * PiSigma parser combinators.++angles :: Parser a -> Parser a+angles = Token.angles tokenParser++braces :: Parser a -> Parser a+braces = Token.braces tokenParser++brackets :: Parser a -> Parser a+brackets = Token.brackets tokenParser++charLiteral :: Parser Char+charLiteral = Token.charLiteral tokenParser++colon :: Parser String+colon = Token.colon tokenParser++comma :: Parser String+comma = Token.comma tokenParser++commaSep :: Parser a -> Parser [a]+commaSep = Token.commaSep tokenParser++commaSep1 :: Parser a -> Parser [a]+commaSep1 = Token.commaSep1 tokenParser++decimal :: Parser Integer+decimal = Token.decimal tokenParser++dot :: Parser String+dot = Token.dot tokenParser++float :: Parser Double+float = Token.float tokenParser++hexadecimal :: Parser Integer+hexadecimal = Token.hexadecimal tokenParser++identifier :: Parser String+identifier = Token.identifier tokenParser++integer :: Parser Integer+integer = Token.integer tokenParser++lexeme :: Parser a -> Parser a+lexeme = Token.lexeme tokenParser++natural :: Parser Integer+natural = Token.natural tokenParser++naturalOrFloat :: Parser (Either Integer Double)+naturalOrFloat = Token.naturalOrFloat tokenParser++octal :: Parser Integer+octal = Token.octal tokenParser++operator :: Parser String+operator = Token.operator tokenParser++parens :: Parser a -> Parser a+parens = Token.parens tokenParser++reserved :: String -> Parser ()+reserved = Token.reserved tokenParser++reservedOp :: String -> Parser ()+reservedOp = Token.reservedOp tokenParser++semi :: Parser String+semi = Token.semi tokenParser++semiSep :: Parser a -> Parser [a]+semiSep = Token.semiSep tokenParser++semiSep1 :: Parser a -> Parser [a]+semiSep1 = Token.semiSep1 tokenParser++squares :: Parser a -> Parser a+squares = Token.squares tokenParser++stringLiteral :: Parser String+stringLiteral = Token.stringLiteral tokenParser++symbol :: String -> Parser String+symbol = Token.symbol tokenParser++whiteSpace :: Parser ()+whiteSpace = Token.whiteSpace tokenParser++-- * Derived parser combinators++location :: Parser Loc+location = sourcePosToLoc <$> getPosition++locate :: Parser a -> Parser Loc+locate = (location <*)++sourcePosToLoc :: SourcePos -> Loc+sourcePosToLoc p = Loc (sourceName p) (sourceLine p) (sourceColumn p)++locReserved :: String -> Parser Loc+locReserved = locate . reserved++locReservedOp :: String -> Parser Loc+locReservedOp = locate . reservedOp++locSymbol :: String -> Parser Loc+locSymbol xs = locate (symbol xs) <?> show xs++tokArr :: Parser Loc+tokArr = locate (choice [ reservedOp "->"+ , reservedOp "→"+ ] <?> "->")++tokForce :: Parser Loc+tokForce = locate (choice [ reservedOp "!"+ , reservedOp "♭"+ ] <?> "!")++tokLam :: Parser Loc+tokLam = locate (choice [ reservedOp "\\"+ , reservedOp "λ"+ ] <?> "\\")++tokLift :: Parser Loc+tokLift = locate (choice [ reservedOp "^"+ , reservedOp "∞"+ ] <?> "^")
+ src/Language/PiSigma/Normalise.hs view
@@ -0,0 +1,123 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}++module Language.PiSigma.Normalise+ ( quote+ , nf )+ where++import Control.Monad++import Language.PiSigma.Evaluate+import Language.PiSigma.Syntax+import qualified Language.PiSigma.Util.String.Internal+ as Internal++{- Implementation of a normalisation function.+ Useful for testing.+-}++type Vars = [Name]++fresh :: Name -> Vars -> Name+fresh x xs+ | x /= "" && x `elem` xs = (x `Internal.append` "'") `fresh` xs+ | otherwise = x++class Nf a b | a -> b where+ nf :: Env e => Vars -> a -> Eval e b+ nf = nf' True+ quote :: Env e => Vars -> a -> Eval e b+ quote = nf' False+ nf' :: Env e => Bool -> Vars -> a -> Eval e b+++instance Nf (Clos Term) Term where+ nf' True xs t = nf' True xs =<< eval t+ nf' False xs t = qq xs t++instance Nf Id Term where+ nf' b xs i = do e <- getEnv+ let (PrtInfo x shouldExpand) = prtE e i+ case getE e i of+ (Id _) -> return (Var Unknown x) + (Closure t) -> if shouldExpand then nf' b xs t+ -- this is bad, we should not+ -- expand inside a box!+ else return (Var Unknown x) ++qq :: Env e => Vars -> Clos Term -> Eval e Term+qq xs (Var l x , s) = quote xs =<< getId l x s+qq _ (Let _ _ _, _) = return (Label Unknown "*quote-let-not-implemented*")+--qq xs (Let l g t, s) = fail "quote let: not implemented!"+{-do s' <- evalProg (g,s)+ qq xs (t,s') + -- this seems wrong! we should return a Let+ -- and we should extend xs!+-}+qq xs (Q l ps (a,(x,b)),s) = + do a' <- qq xs (a,s)+ xb' <- quote xs (x,(b,s))+ return (Q l ps (a',xb'))+qq xs (Lift l t,s) = liftM (Lift l) (qq xs (t,s))+-- qq xs (LType l t,s) = liftM (LType l) (qq xs (t,s))+qq xs (Lam l (x,t), s) = liftM (Lam l) (quote xs (x,(t,s)))+qq xs (App t u ,s) = do t' <- qq xs (t,s)+ u' <- qq xs (u,s)+ return (App t' u')+qq xs (Pair l t u,s) = do t' <- qq xs (t,s)+ u' <- qq xs (u,s)+ return (Pair l t' u')+qq xs (Split l t (x,(y,u)),s) = do t' <- qq xs (t,s)+ xyu' <- quote xs (x,(y,(u,s)))+ return (Split l t' xyu')+qq xs (Case l t lts,s) = do t' <- qq xs (t,s)+ lts' <- mapM (\ (l',t'') -> + do t''' <- qq xs (t'',s)+ return (l',t''')) lts+ return (Case l t' lts') +qq xs (Box l t,s) = liftM (Box l) (qq xs (t,s))+qq xs (Force l t,s) = liftM (Force l) (qq xs (t,s))+qq _ (t,_) = return t -- Type, Enum, Label++instance (Closure a,Nf a b) => Nf (Bind a) (Bind b) where+ nf' b xs (x,t) = do let x' = fresh x xs+ (_,s') <- decl x (PrtInfo x' True) (getScope t) Nothing+ t' <- nf' b (x':xs) (putScope t s')+ return (x',t')++instance Nf Val Term where+ nf' b xs (Ne n) = nf' b xs n+ nf' _ _ VType = return (Type Unknown)+ nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) + xc' <- nf' b xs (x,(c,s))+ return (Q Unknown ps (a',xc'))+ nf' b xs (VLift c) = liftM (Lift Unknown) (nf' b xs c)+-- nf' b xs (VLType c) = liftM (LType Unknown) (nf' b xs c)+ nf' b xs (VLam xt) = liftM (Lam Unknown) (nf' b xs xt)+ nf' b xs (VPair ((t,u),s)) = do t' <- nf' b xs (t,s)+ u' <- nf' b xs (u,s)+ return (Pair Unknown t' u')+ nf' _ xs (VBox (Boxed c)) = liftM (Box Unknown) (nf' False xs c)+ nf' _ _ (VEnum ls) = return (Enum Unknown ls)+ nf' _ _ (VLabel l) = return (Label Unknown l)+++instance Nf Ne Term where+ nf' b xs (NVar i) = nf' b xs i+ nf' b xs (t :.. u) = do t' <- nf' b xs t+ u' <- nf' b xs u+ return (App t' u')+ nf' b xs (NSplit t xyu) = do t' <- nf' b xs t+ xyu' <- nf' b xs xyu+ return (Split Unknown t' xyu')+ nf' b xs (NCase t (lus,s)) = do t' <- nf xs t+ lus' <- mapM (\ (l,u) -> + do u' <- nf' b xs (u,s)+ return (l,u')) lus+ return (Case Unknown t' lus')+ nf' _ xs (NForce t) = liftM (Force Unknown) (nf xs t)
+ src/Language/PiSigma/Parser.hs view
@@ -0,0 +1,160 @@+module Language.PiSigma.Parser+ ( parse+ , sPhrase+ , sProg+ , s2Terms+ , sTerm )+ where++import Prelude hiding (pi)+import Control.Monad+import Control.Applicative hiding ((<|>), many)+import Data.List+import Text.Parsec.Combinator+import Text.Parsec.Error+ ( ParseError )+import Text.Parsec.Pos+ ( SourceName )+import Text.Parsec.Prim+ hiding+ ( label+ , parse+ , token )+import qualified Text.ParserCombinators.Parsec+ as Parsec+ ( parse )+import Text.ParserCombinators.Parsec.Char+ ( string )++import Language.PiSigma.Lexer+import Language.PiSigma.Syntax hiding (label)+import qualified Language.PiSigma.Util.String.Internal+ as Internal+import qualified Language.PiSigma.Util.String.Parser+ as Parser++sLabel :: Parser Name+sLabel = Internal.fromString <$> (string "'" *> identifier)++sName :: Parser Name+sName = Internal.fromString <$> identifier++-- * Terms++sTerm5 :: Parser Term+sTerm5 = choice+ [ Type <$> locReserved "Type"++ , Enum <$> location+ <*> braces (many sName)+ <?> "enumeration"++ , Case <$> locReserved "case"+ <*> sTerm+ <* reserved "of"+ <*> braces (sBranch `sepBy` locReservedOp "|")++ , Label <$> location+ <*> sLabel+ <?> "label"++ , Box <$> location+ <*> boxed sTerm+ <?> "box"++ , Lift <$> tokLift+ <*> sTerm5+ <?> "'^'"++ , Var <$> location <*> sName+ , parens sTerm+ ]+ where+ boxed p = choice [ brackets p+ , reservedOp "♯" *> p+ ]++sTerm4 :: Parser Term+sTerm4 = choice+ [ try $ (uncurry . Pair) <$> location+ <*> parens ((,) <$> sTerm <* comma <*> sTerm)+ , sTerm5+ ]++sTerm3 :: Parser Term+sTerm3 = choice+ [ try (parens (sigmas <$> many1 ((,) <$> location <*> sName) <* reservedOp ":" <*> sTerm) <* reservedOp "*") <*> sTerm2+ , Force <$> tokForce <*> sTerm4+ , foldl1 App <$> many1 sTerm4+ ]++sTerm2 :: Parser Term+sTerm2 = foldr1 (-*-) <$> sTerm3 `sepBy1` reservedOp "*"++-- TODO: make more beautiful or renumber+sTerm1b :: Parser Term+sTerm1b = choice+ [ try (parens (pis <$> many1 ((,) <$> location <*> sName) <* reservedOp ":" <*> sTerm) <* tokArr) <*> sTerm+ , sTerm2+ ]+ +sTerm1 :: Parser Term+sTerm1 = foldr1 (->-) <$> sTerm1b `sepBy1` tokArr++sTerm :: Parser Term+sTerm = choice+ [ lam <$ tokLam+ <*> many ((,) <$> location <*> sName)+ <* tokArr+ <*> sTerm++ , split <$> locReserved "split"+ <*> sTerm+ <* reserved "with"+ <*> parens ((,) <$> sName+ <* comma+ <*> sName)+ <* tokArr+ <*> sTerm++ , Let <$> locReserved "let"+ <*> sProg+ <* reserved "in"+ <*> sTerm+ , sTerm1+ ]++sProg :: Parser Prog+sProg = concat <$> (sEntry `sepEndBy` semi)++sEntry :: Parser [Entry]+sEntry =+ do+ l <- location+ n <- sName+ b <- choice [ True <$ reservedOp ":"+ , False <$ reservedOp "="+ ]+ t <- sTerm+ if b+ then do+ d <- option Nothing (Just <$ reservedOp "=" <*> sTerm)+ case d of+ Nothing -> return [Decl l n t]+ Just t' -> return [Decl l n t, Defn l n t']+ else return [Defn l n t]++sBranch :: Parser (Label,Term)+sBranch = (,) <$> sName <* tokArr <*> sTerm++sPhrase :: Parser Phrase+sPhrase = choice+ [ try $ Prog <$> sProg <* eof+ , Term <$> sTerm <* eof+ ]++s2Terms :: Parser (Term, Term)+s2Terms = (,) <$> sTerm5 <*> sTerm5++parse :: Parser a -> SourceName -> Parser.String -> Either ParseError a+parse p = Parsec.parse (whiteSpace *> p <* eof)
+ src/Language/PiSigma/Pretty.hs view
@@ -0,0 +1,193 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Language.PiSigma.Pretty+ ( module Text.PrettyPrint.MPPPC.OneDim+ , Pretty+ , Print+ , evalPrint+ , fromPretty )+ where++import Control.Monad.Error+import Text.PrettyPrint.MPPPC.OneDim+ hiding+ ( Pretty )+import qualified Text.PrettyPrint.MPPPC.OneDim+ as OneDim++import Language.PiSigma.Evaluate+import Language.PiSigma.Normalise+import Language.PiSigma.Syntax+import qualified Language.PiSigma.Util.String.Internal+ as Internal++type Pretty = OneDim.Pretty (Seq Internal.String Char) (Tok Internal.String Char)++-- * Print class for various types++class Print a where+ evalPrint :: Env e => a -> Eval e Pretty++instance Print Internal.String where+ evalPrint = return . text . Seq++instance Print Pretty where+ evalPrint = return++instance Print Val where+ evalPrint a = evalPrint =<< quote [] a++instance Print (Clos Term) where+ evalPrint a = evalPrint =<< quote [] a++instance Print Ne where+ evalPrint a = evalPrint =<< quote [] a++instance Print Term where+ evalPrint = return . prettyTerm 0++fromPretty :: Pretty -> Internal.String+fromPretty = unSeq . renderSeq++data Msg+ = MsgV Val+ | MsgC (Clos Term)+ | MsgT Term+ | MsgS Internal.String+ | MsgD Pretty++instance Print Msg where+ evalPrint (MsgV v) = evalPrint v+ evalPrint (MsgC c) = evalPrint c+ evalPrint (MsgT t) = evalPrint t+ evalPrint (MsgS s) = evalPrint s+ evalPrint (MsgD d) = evalPrint d++-- * Pretty printer for terms++-- | Context for printing. Determines whether parentheses are+-- required.+type PrintContext = Int+++prettyTerm :: PrintContext -> Term -> Pretty++prettyTerm _ (Var _ x) =+ text $ Seq x++prettyTerm _ (Let _ p t) =+ list (map prettyEntry p)+ <> prettyTerm 0 t++prettyTerm _ (Type _) =+ text "Type"++prettyTerm c (Q _ Pi (t1, (n, t2))) =+ contextParens c 1+ $ group+ $ binding 2 n t1+ <$> text "->"+ <+> prettyTerm 1 t2++prettyTerm c (Q _ Sigma (t1, (n, t2))) =+ contextParens c 2+ $ binding 3 n t1+ <+> text "*"+ <+> prettyTerm 2 t2++prettyTerm c (Lam _ (n, t)) =+ contextParens c 0+ $ text "\\"+ <+> text (Seq n)+ <+> text "->"+ <+> prettyTerm 0 t++prettyTerm c (App t1 t2) =+ group+ $ hang 2+ $ contextParens c 3+ $ prettyTerm 3 t1+ <$> prettyTerm 4 t2++prettyTerm _ (Pair _ t1 t2) =+ tupled $ map (prettyTerm 0) [t1, t2]++prettyTerm c (Split _ t1 (n1, (n2, t2))) =+ contextParens c 0+ $ hang 2+ $ text "split"+ <+> prettyTerm 0 t1+ <+> text "with"+ <+> (parens $ text (Seq n1)+ <> comma+ <> text (Seq n2))+ <+> text "->"+ <$> prettyTerm 0 t2++prettyTerm _ (Enum _ ls) =+ braces+ $ sep+ $ map (text . Seq) ls++prettyTerm _ (Label _ l) =+ text $ Tok '\'' `cons` Seq l++prettyTerm _ (Case _ t bs) =+ hang 1+ $ text "case"+ <+> prettyTerm 0 t+ <+> text "of"+ <$> branches bs++prettyTerm c (Lift _ t) =+ contextParens c 5+ $ text "^"+ <> prettyTerm 5 t++prettyTerm _ (Box _ t) =+ brackets $ prettyTerm 0 t++prettyTerm c (Force _ t) =+ contextParens c 3+ $ text "!"+ <> prettyTerm 4 t+++prettyEntry :: Entry -> Pretty++prettyEntry (Defn _ n t) =+ hang 2+ $ text (Seq n)+ <+> text "="+ <$> prettyTerm 0 t+ <> text ";"++prettyEntry (Decl _ n t) =+ hang 2+ $ text (Seq n)+ <+> text ":"+ <$> prettyTerm 0 t+ <> text ";"+++binding :: PrintContext -> Name -> Term -> Pretty+binding c n t | Internal.null n = prettyTerm c t+ | otherwise = parens+ $ text (Seq n)+ <+> colon+ <+> prettyTerm 0 t++branches :: [(Label,Term)] -> Pretty+branches = encloseSep (text " { ") (text " } ") (text " | ") . map branch+ where+ branch (n, t) = text (Seq n)+ <+> text "->"+ <+> prettyTerm 0 t++-- | Prints parens if the current context is higher+-- than a certain limit.+contextParens :: PrintContext -> PrintContext -> Pretty -> Pretty+contextParens c d p | c > d = parens p+ | otherwise = p
+ src/Language/PiSigma/Syntax.hs view
@@ -0,0 +1,356 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Language.PiSigma.Syntax+ ( Bind+ , Boxed (..)+ , Clos+ , Closure (..)+ , Entry (..)+ , Enum+ , Env+ , EnvEntry (..)+ , EnvEntries+ , GetLoc (..)+ , Id+ , Label+ , Loc (..)+ , Name+ , Ne (..)+ , Phrase (..)+ , PiSigma (..)+ , Prog+ , PrtInfo (..)+ , Scope (..)+ , Term (..)+ , Type+ , Val (..)+ , (-*-)+ , (->-)+ , emptyE+ , emptyScope+ , extE+ , extendScope+ , getE+ , label+ , lam+ , locMessage+ , lookupCon+ , lookupScope+ , pis+ , prtE+ , setE+ , sigmas+ , split+ , ty )+ where++import Prelude+ hiding+ ( pi )+import Data.Maybe+ ( fromJust )++import qualified Language.PiSigma.Util.String.Internal+ as Internal++-- * Locations++data Loc+ = Unknown+ | Loc { filename :: !String+ , line :: !Int+ , column :: !Int }+ deriving Show++locMessage :: Loc -> String+locMessage Unknown = "<unknown>:"+locMessage (Loc f l c) = concat+ [ f+ , ":"+ , show l+ , ":"+ , show c+ , ":"+ ]++-- | Locations are always equal. This allows us to+-- derive equality for the abstract syntax that ignores+-- the locations.+instance Eq Loc where+ _ == _ = True++class GetLoc a where+ getLoc :: a -> Loc++-- * Abstract syntax++data Phrase+ = Prog Prog+ | Term Term+ deriving (Show, Eq)++type Name = Internal.String++type Label = Internal.String++data Entry+ = Decl Loc Name Type+ | Defn Loc Name Term+ deriving (Show, Eq)++instance GetLoc Entry where+ getLoc (Decl l _ _) = l+ getLoc (Defn l _ _) = l++type Prog = [Entry]++{-+Maybe better+data Prog = Decl Type (Bind Prog) | Defn Name Term Prog+-}++type Type = Term++-- | The use of Bind indicates the scope of the+-- bound identifier.+type Bind a = (Name, a)++-- | For treating quantifiers in a uniform way.+data PiSigma+ = Pi+ | Sigma+ deriving (Show, Eq)++data Term+ = Var Loc Name+ | Let Loc Prog Term+ | Type Loc+ | Q Loc PiSigma (Type, Bind Type)+ | Lam Loc (Bind Term)+ | App Term Term+ | Pair Loc Term Term+ | Split Loc Term (Bind (Bind Term)) -- split t with (x,y) -> u+ | Enum Loc [Name]+ | Label Loc Label+ | Case Loc Term [(Label, Term)] -- case t of { L -> u }+ | Lift Loc Term+ | Box Loc Term+ | Force Loc Term+-- | LType Loc Term -- lazy type ($ sigma)+ deriving (Show,Eq)++instance GetLoc Term where+ getLoc (Var l _ ) = l+ getLoc (Let l _ _) = l+ getLoc (Type l ) = l+ getLoc (Q l _ _) = l+ getLoc (Lam l _ ) = l+ getLoc (App t _ ) = getLoc t+ getLoc (Pair l _ _) = l+ getLoc (Split l _ _) = l+ getLoc (Enum l _ ) = l+ getLoc (Label l _ ) = l+ getLoc (Case l _ _) = l+ getLoc (Lift l _ ) = l+ getLoc (Box l _ ) = l+ getLoc (Force l _ ) = l+-- getLoc (LType l _) = l++-- * Smart constructors++-- | Smart constructor for lambda abstractions.+lam :: [(Loc, Name)] -> Term -> Term+lam [] t = t+lam ((l, x) : xs) t = Lam l (x, lam xs t)++-- | Smart constructor for split.+split :: Loc -> Term -> (Name, Name) -> Term -> Term+split l t1 (x, y) t2 = Split l t1 (x, (y, t2))++-- | Smart constructor for quantifiers.+q :: PiSigma -> [(Loc, Name, Type)] -> Type -> Type+q _ [] b = b+q ps ((l, x, a) : xas) b = Q l ps (a, (x, q ps xas b))++-- | Smart constructor for multiple Pi applications.+pis' :: [(Loc, Name, Type)] -> Type -> Type+pis' = q Pi++-- | Smart constructor for multiple Pi applications.+pis :: [(Loc, Name)] -> Type -> Type -> Type+pis ns t = pis' (map (\ (l, n) -> (l, n, t)) ns)++-- | Smart constructor for Pi.+pi :: Loc -> Name -> Type -> Type -> Type+pi l n t = pis' [(l, n, t)]++-- | Smart constructor for multiple Sigma applications.+sigmas' :: [(Loc,Name,Type)] -> Type -> Type+sigmas' = q Sigma++-- | Smart constructor for multiple Sigma applications.+sigmas :: [(Loc,Name)] -> Type -> Type -> Type+sigmas ns t = sigmas' (map (\ (l, n) -> (l, n, t)) ns)++-- | Smart constructor for Sigma.+sigma :: Loc -> Name -> Type -> Type -> Type+sigma l n t = sigmas' [(l, n, t)]++-- | Smart constructor for function space.+(->-) :: Type -> Type -> Type+(->-) t = pi (getLoc t) "" t++-- | Smart constructor for product.+(-*-) :: Type -> Type -> Type+(-*-) t = sigma (getLoc t) "" t++-- * Values (well-scoped WHNFs) and environments++-- ** Identifiers++type Id = Int -- index in (potentially multiple) environments++-- ** Scopes++newtype Scope = Scope [(Name, (Id, Maybe (Clos Type)))]+ deriving (Show, Eq)++{-++TODO:++Perhaps return to the following types for scopes:++data Sc a = Scope [(Name,(Id, a))]++type Scope = Sc ()+type Ctx = Sc (Clos Type)++We then need a forgetful mapping:++fog :: Ctx -> Scope+fog c = map (\ (x,(i,a)) -> (x,(i,()))) c ++Alternatively, we can try to make Scopes+existential, essentially:++type Scope = exists a. Sc a++-}++emptyScope :: Scope+emptyScope = Scope []++extendScope :: Scope -> Name -> (Id, Maybe (Clos Type)) -> Scope+extendScope (Scope s) x (i, a) = Scope $ (x, (i, a)) : s++lookupScope :: Scope -> Name -> Maybe Id+lookupScope (Scope s) x = do idCon <- lookup x s+ return $! fst idCon++lookupCon :: Scope -> Name -> Maybe (Clos Type)+lookupCon (Scope s) x = do idCon <- lookup x s+ return $! fromJust $! snd idCon++-- ** Closures++type Clos a = (a, Scope)++instance GetLoc a => GetLoc (Clos a) where+ getLoc (x, _) = getLoc x++--type C a = (Con,a)++--c2clos :: C a -> Clos a+--c2clos (g,a) = (a,fog g)++-- fix order, name of C...++class Closure a where + getScope :: a -> Scope+ putScope :: a -> Scope -> a++instance Closure (Clos a) where+ getScope (_, s) = s+ putScope (a, _) s = (a, s)++instance Closure a => Closure (Bind a) where+ getScope (_, a) = getScope a+ putScope (x, a) s = (x, putScope a s)++instance Closure Boxed where+ getScope (Boxed c) = getScope c+ putScope (Boxed c) = Boxed . putScope c++{- could be used to refactor the code using bindings. -}++ty :: Clos Type+ty = (Type Unknown, emptyScope)++--lty :: Clos Type+--lty = (Lift Unknown (Type Unknown), emptyScope)++label :: Label -> Clos Term+label s = (Label Unknown s, emptyScope)++-- type VType = Val -- unused?++newtype Boxed = Boxed (Clos Term)+ deriving (Show, Eq)++-- ** Values++data Val+ = Ne Ne+ | VType + | VQ PiSigma (Clos (Type, Bind Type))+ | VLift (Clos Type)+ | VLam (Bind (Clos Term))+ | VPair (Clos (Term, Term))+ | VEnum [Label]+ | VLabel Label + | VBox Boxed+-- | VLType (Clos Type)+ deriving (Show, Eq)++-- | Neutral terms.+data Ne+ = NVar Id+ | Ne :.. (Clos Term)+ | NSplit Ne (Bind (Bind (Clos Term)))+ | NCase Ne (Clos [(Label, Term)])+ | NForce Ne+ deriving (Show, Eq)++-- ** Environments++data EnvEntry+ = Id Id+ | Closure (Clos Term)+ deriving Show++data PrtInfo+ = PrtInfo { name :: Name+ , expand :: Bool }++class Env e where + emptyE :: e+ extE :: e -> PrtInfo -> (Id,e)+ setE :: e -> Id -> EnvEntry -> e+ getE :: e -> Id -> EnvEntry+ prtE :: e -> Id -> PrtInfo++set :: [a] -> Int -> a -> [a]+set [] _ _ = error "list is empty"+set (_ : as) 0 b = b : as+set (a : as) i b = a : set as (i - 1) b++type EnvEntries = [(EnvEntry, PrtInfo)]++instance Env EnvEntries where+ emptyE = []+ extE e x = case length e of i -> (i, e ++ [(Id i, x)])+ setE e i v = case e !! i of (_, x) -> set e i (v, x)+ getE e i = case e !! i of (v, _) -> v+ prtE e i = case e !! i of (_, x) -> x
+ src/Language/PiSigma/Util/String/Internal.hs view
@@ -0,0 +1,48 @@+module Language.PiSigma.Util.String.Internal+ ( String+ , append+ , concat+ , fromString+ , isPrefixOf+ , null+ , putStrLn+ , toString )+ where++import Prelude+ hiding+ ( String+ , concat+ , null+ , putStrLn )+import qualified Prelude+ as Prelude+import qualified Data.ByteString+ as Word8+import qualified Data.Text+ as Text+import qualified Data.Text.Encoding+ as Text++type String = Text.Text++append :: String -> String -> String+append = Text.append++concat :: [String] -> String+concat = Text.concat++fromString :: Prelude.String -> String+fromString = Text.pack++isPrefixOf :: String -> String -> Bool+isPrefixOf = Text.isPrefixOf++null :: String -> Bool+null = Text.null++putStrLn :: String -> IO ()+putStrLn = Word8.putStrLn . Text.encodeUtf8++toString :: String -> Prelude.String+toString = Text.unpack
+ src/Language/PiSigma/Util/String/Parser.hs view
@@ -0,0 +1,118 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Language.PiSigma.Util.String.Parser+ ( String+ , append+ , fromString+ , isPrefixOf+ , lines+ , null+ , readFile+ , span+ , toString+ , uncons+ , unlines )+ where++import Prelude+ hiding+ ( String+ , lines+ , null+ , readFile+ , replicate+ , span+ , unlines )+import qualified Prelude+ as Prelude+import qualified Data.ByteString.Lazy+ as Lazy+import qualified Data.ByteString.Lazy.UTF8+ as LazyUTF8+import qualified Data.String as String++-- * The parser input type++type String = LazyUTF8.ByteString++instance String.IsString String where+ fromString = fromString++append :: String -> String -> String+append = Lazy.append++fromString :: Prelude.String -> String+fromString = LazyUTF8.fromString++isPrefixOf :: String -> String -> Bool+isPrefixOf = Lazy.isPrefixOf++lines :: String -> [String]+lines = LazyUTF8.lines++null :: String -> Bool+null = Lazy.null++readFile :: FilePath -> IO String+readFile = Lazy.readFile++span :: (Char -> Bool) -> String -> (String, String)+span = LazyUTF8.span++toString :: String -> Prelude.String+toString = LazyUTF8.toString++uncons :: String -> Maybe (Char, String)+uncons = LazyUTF8.uncons++unlines :: [String] -> String+unlines = Lazy.intercalate "\n"++++-- NOTE: Commenting out the code above and uncommenting the code below+-- results in an incredible slowdown during parsing. I'm not sure why+-- this is since Data.Text should be pretty fast. Using strict versus+-- lazy Data.Text is even worse.++-- import Control.Monad+-- ( liftM )+-- import qualified Data.ByteString.Lazy+-- as Word8+-- import qualified Data.Text.Lazy+-- as Text+-- import qualified Data.Text.Lazy.Encoding+-- as Text++-- type String = Text.Text++-- append :: String -> String -> String+-- append = Text.append++-- fromString :: Prelude.String -> String+-- fromString = Text.pack++-- isPrefixOf :: String -> String -> Bool+-- isPrefixOf = Text.isPrefixOf++-- lines :: String -> [String]+-- lines = Text.lines++-- null :: String -> Bool+-- null = Text.null++-- readFile :: FilePath -> IO String+-- readFile = liftM Text.decodeUtf8 . Word8.readFile++-- span :: (Char -> Bool) -> String -> (String, String)+-- span = Text.spanBy++-- toString :: String -> Prelude.String+-- toString = Text.unpack++-- uncons :: String -> Maybe (Char, String)+-- uncons = Text.uncons++-- unlines :: [String] -> String+-- unlines = Text.unlines
− src/PiSigma.hs
@@ -1,265 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}--module Main where--import Prelude hiding (catch)-import System.IO-import System.Environment-import System.Console.Haskeline hiding (catch)-import Control.Monad-import Control.Monad.Trans-import Control.Monad.State-import Control.Exception-import Data.List-import Data.Char- -import PiSigma.Syntax-import PiSigma.Evaluation-import PiSigma.Check-import PiSigma.Print-import PiSigma.Nf-import PiSigma.Equality-import PiSigma.Parser--main :: IO ()-main = - do- args <- getArgs- let ini = mapM_ (handleCommand . Load) args- liftM fst $ runStateT (runInputT - (setComplete pisigmaCompletion defaultSettings)- (ini >> repl))- initialReplState---- | Completion in PiSigma. For the moment, we use file name completion--- while in a load command, and identifier completion everywhere else.-pisigmaCompletion :: CompletionFunc (StateT ReplState IO)-pisigmaCompletion (x1,x2)- | ":l" `isPrefixOf` reverse x1 = completeFilename (x1,x2)- | otherwise = completeWord Nothing " " identifier (x1,x2)- where- identifier x = do- (Scope sc,env) <- gets replState- let names = map fst sc- xr = reverse x- cands = filter (x `isPrefixOf`) names- return $ map simpleCompletion (sort cands)--type Repl = InputT (StateT ReplState IO)-type Continue = Bool--data ReplState =- ReplState- { replState :: (Scope, EnvEntries)- , replFiles :: [FilePath]- }--data ReplCommand =- Load String- | Reload- | Quit- | EvalPhrase Phrase- | Noop- | Clear- | Equal (Term,Term)- | TypeOf Term- | Help---- TODO:--- browse current identifiers---- | Preliminary interpreter help message.-help :: String-help =- unlines $- [ "PiSigma currently supports the following commands:",- "",- " :l load a source file",- " :r reload current source file",- " :c clear the environment",- " :t ask for the type of a term",- " :e test two terms for beta equality",- " :q quit",- "",- "Type a declaration or an expression to evaluate it." ]--initialReplState :: ReplState-initialReplState = - ReplState (emptyScope, emptyE) []--replStep :: Repl Continue-replStep =- do- f <- lift $ gets replFiles- x <- getInputLine (unwords (reverse f) ++ "> ")- c <- interpretInput x- handleCommand c---- | Preliminary input interpretation, based on the--- current parser and no particular intelligence in--- parsing commands correctly.-interpretInput :: Maybe String -> Repl ReplCommand-interpretInput Nothing = return Quit-interpretInput (Just x)- | ":l" `isPrefixOf` x = case break (== ' ') x of- (x1,x2) -> return (Load (norm (trim x2)))- | ":r" `isPrefixOf` x = return Reload- | ":q" `isPrefixOf` x = return Quit- | ":c" `isPrefixOf` x = return Clear- | ":e" `isPrefixOf` x = case break (== ' ') x of- (x1,x2) -> parseInputInteractive s2Terms Equal x2- | ":t" `isPrefixOf` x = case break (== ' ') x of- (x1,x2) -> parseInputInteractive sTerm TypeOf x2- | ":h" `isPrefixOf` x || ":?" `isPrefixOf` x- = return Help- | ":" `isPrefixOf` x = replMessage "unknown command" >> return Noop- | otherwise = parseInputInteractive sPhrase EvalPhrase x---- | Turn a string into a Repl command.-parseInput :: String -> SParser t -> (t -> ReplCommand) ->- String -> Repl ReplCommand-parseInput f p cmd s =- case parse p f s of- Left s -> do- liftIO $ putStrLn ("Parse error: " ++ show s ++ "\n")- return Noop- Right p -> return (cmd p)--parseInputInteractive = parseInput "<interactive>"---- | Placeholder for a message function that can depend--- on verbosity settings.-replMessage :: String -> Repl ()-replMessage = liftIO . putStrLn---- | Command handler. Returns a flag indicating whether--- the interpreter should continue.-handleCommand :: ReplCommand -> Repl Continue-handleCommand c =- case c of- Help ->- do- replMessage $ help- return True- Load f ->- do- fs <- lift $ gets replFiles- if f `elem` fs then do- replMessage $ "Skipping " ++ f ++ "."- return True- else do- mx <- liftIO $ catch (liftM Just (readFile f))- (\ (_ :: IOException) -> return Nothing)- case mx of- Nothing -> do- replMessage $ "Could not find " ++ f ++ "."- return True- Just x -> do- -- Allow source files to have interpreter commands at the top;- -- we currently use this as a replacement for a module system- let (cmds,rest) = span (":" `isPrefixOf`) (lines x)- mapM_ (\ c -> interpretInput (Just c) >>= handleCommand) cmds- -- We print the "Loaded" message after executing initial- -- interpreter commands in order to reflect the dependency- -- order of different source files.- replMessage $ "Loaded " ++ f ++ "."- p <- parseInput f sProg (EvalPhrase . Prog)- (unlines (replicate (length cmds) "" ++ rest))- lift $ modify (\ s -> s { replFiles =- case replFiles s of- (g : fs) | g == f -> g : fs- xs -> f : xs })- handleCommand p- Reload ->- do- f <- lift $ gets replFiles- handleCommand Clear- mapM_ (handleCommand . Load) (reverse f)- return True- Quit ->- return False- EvalPhrase (Prog p) ->- do- execProg p- return True- EvalPhrase (Term t) ->- do- execTerm t- return True- Equal (t1,t2) ->- do- eqTerms t1 t2- return True- TypeOf t ->- do- inferTerm t- return True- Clear ->- do- lift $ put initialReplState- return True- Noop ->- return True--execProg :: Prog -> Repl ()-execProg p =- do- s <- lift get- let (con,env) = replState s- case run env (checkProg (p,con)) of- Right s' -> lift $ put (s { replState = s' })- Left e -> liftIO $ putStrLn e--execTerm :: Term -> Repl ()-execTerm t =- do- s <- lift get- let (con,env) = replState s- p = do- a <- infer (t,con)- pa <- prt a- t' <- nf [] (t,con)- pt <- prt t'- return (pt++"\n: "++pa)- case run env p of- Right (m,_) -> liftIO $ putStrLn m- Left e -> liftIO $ putStrLn e--eqTerms :: Term -> Term -> Repl ()-eqTerms t1 t2 =- do- s <- lift get- let (con,env) = replState s- p = eq (t1,con) (t2,con)- case run env p of- Right _ -> liftIO $ putStrLn "yes"- Left e -> liftIO $ putStrLn e- --inferTerm :: Term -> Repl ()-inferTerm t =- do- s <- lift get- let (con,env) = replState s- p = infer (t,con) >>= prt- case run env p of- Right (m,_) -> liftIO $ putStrLn m- Left e -> liftIO $ putStrLn e---- | Run the interpreter as long as desired.-repl :: Repl ()-repl =- do- continue <- replStep- when continue repl---- * Helper functions--trim :: String -> String-trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace--norm :: String -> String-norm [] = []-norm ('\\':c:xs) = c : norm xs-norm (x:xs) = x : norm xs-
− src/PiSigma/Check.hs
@@ -1,189 +0,0 @@-module PiSigma.Check where--import Control.Monad--import PiSigma.Syntax-import PiSigma.Evaluation-import PiSigma.Print-import PiSigma.Equality----import Debug.Trace---trace "check\n" $---- closures are the other way around--- should be fixed by changing closures.--{--fog :: CTerm -> Closure-fog (g,t) = (con2scope g,t)--}--failc :: Env e => Clos Term -> [Msg] -> Eval e a-failc t m = failp ([S "Checking:\t",C t,S "\n"]++m)---- | Takes a term and an (unevaluated) type. We first--- handle the cases that may potentially change the--- environment. If none of those cases match, we can--- safely evaluate the type and call check'.-check :: Env e => Clos Term -> Clos Type -> Eval e ()---check (g,t) c | trace ("check\ng ="++(show g)++"\n t="++(show t)++"\nc="++(show c)++"\n") False = undefined--check (Let p t,g) c = - do g' <- checkProg (p,g)- check (t,g') c--check (gt @ (Split t (x,(y,u)),g)) c = - do sigab <- infer' (t,g)- case sigab of- (VQ Sigma ((a,(z,b)),s)) -> - do t' <- eval (t,g)- (_,g') <- tdecl x g (a,s)- b <- subst (z,(b,s)) (Var x, g')- (_,g'') <- tdecl y g' b- case t' of- (Ne (NVar i)) ->- letn' i (Pair (Var x,Var y), g'')- (check (u,g'') c)- -- this is a bit silly since we know the ids.- _ -> check (u,g'') c- -- instead of failing, we just omit the assignment.- _ -> failc gt [S "split : Sigma type expected\nFound:\t",V sigab,S "\n(split)\n"]--check gt @ (t'@(Case t lus),g) c = - do enum <- infer' (t,g)- case enum of- VEnum ls -> - let ls' = map fst lus- in if ls /= ls'- then do -- pt' <- prt t'- failc gt [S ("case: labels don't match"- ++ "\n expected : " ++ show ls- ++ "\n inferred : " ++ show ls'- ++ "\n(match)\n")]- -- set equivalence would be sufficent- else do t' <- eval (t,g)- case t' of- -- if the scrutinee is a variable, we add a constraint- -- while checking each of the branches- (Ne (NVar i)) ->- mapM_ (\ (l,u) -> - letn' i (label l)- (check (u,g) c)) lus- -- if the scrutinee is not a variable, we do not add- -- a constraint, but continue- _ -> mapM_ (\ (l,u) -> check (u,g) c) lus- _ -> failc gt [S "case : enum type expected\nFound:\t",V enum,S "\n(case)\n"]- {- Problem: here and other places: we try to print the term t which isn't yet - typechecked and may contain undefined variables which may crash the printer...- see undef-bug.pi- -}-check (Force t,g) (a , s) =- check (t,g) (Lift a , s)--check t a = do a' <- feval a- check' t a'--check' :: Env e => Clos Term -> Val -> Eval e ()-check' gt (VBox (Boxed a)) = check gt a -- do we still need this line?-check' (Lam (x,t),g) (VQ Pi ((a,(y,b)),s)) =- do (i,g') <- tdecl x g (a,s)- let s' = extendScope s y (i,Nothing)- check (t,g') (b,s')-check' gt @ (Lam _,g) a = failc gt [S "Expected:\t",V a,S "\n(Lam)\n"]-check' (Pair (t,u),g) (VQ Sigma ((a,(y,b)),s)) =- do check (t,g) (a,s)- b <- subst (y,(b,s)) (t,g)- check (u,g) b-check' gt @ (t @ (Pair _),g) a = failc gt [S "Expected\t",V a,S "\n(Pair)\n"]--- Labels cannot be inferred because there is no way to know--- what the other labels are.-check' gt @ (Label l,g) a @ (VEnum ls) | l `elem` ls = return ()-check' gt @ (Label l,g) a = failc gt [S "Expected\t",V a,S "\n(Label)\n"]--- To check that [sigma] is a type, it's sufficient to know--- that sigma is a type. The alternative would seem to be to--- assume that ^Type == Type, but that does not work.-check' (Box a,g) VType =- check (a,g) ty-check' (Box t,g) (VLift a) =- check (t,g) a-check' gt @ (Box _,g) a = failc gt [S "Expected\t",V a,S "\n(Box)\n"]-check' t a =- do b <- infer' t- catchE (eq a b)- (\ s -> failc t [S "Expected:\t",V a,- S "\nFound:\t",V b,S $ "\n(check)\n"])--- ++s++"\n"++(show a)++"\n"++(show b)])--- useful for debugging.--inferVar :: Env e => Clos Name -> Eval e (Clos Type)-inferVar (x,g) =- case lookupCon g x of- Just a -> return a- Nothing -> fail ("Undefined variable: "++x++"\n(inferVar)\n")--infer :: Env e => Clos Term -> Eval e (Clos Type)---infer (g,t) | trace ("infer\ng ="++(show g)++"\n t="++(show t)++"\n") False = undefined--infer (Var x,g) = inferVar (x,g)--infer (Let tel t,g) = - do g' <- checkProg (tel,g)- infer (t,g') --infer (Type,g) = return ty--infer (Q _ (a,(x,b)),g) = - do check (a,g) ty- (_,g') <- tdecl x g (a,g)- check (b,g') ty- return ty--infer gt@(t :. u,g) = - do piab <- infer' (t,g)- case piab of - (VQ Pi ((a,(x,b)),s)) -> do check (u,g) (a,s)- subst (x,(b,s)) (u,g)- _ -> failc gt [S "Pi type expected, but found:\t",- V piab,- S "\n(app)\n"]--infer (Enum _,_) = return ty--infer (Box t,g) =- liftM (\ (a,s) -> (Lift a,s)) (infer (t,g))---- TODO: either use infer', or explain why forced eval--- cannot be used here.-infer gt@(Force t,g) =- do a <- infer (t,g)- a' <- eval a- case a' of- VLift b -> return b- _ -> failc gt [S "Lifted type expected\n(Force)\n"]-infer (Lift a,g) =- do check (a,g) ty- return ty--infer gt = failc gt [S "Not inferable\n(infer)\n"]----- | Infers a type and evaluates it.-infer' :: Env e => Clos Term -> Eval e Val-infer' gt =- do a <- infer gt- feval a--checkProg :: Env e => Clos Prog -> Eval e Scope-checkProg ([],g) = return g-checkProg ((Decl x a):tel,g) = - do check (a,g) ty - (_,g') <- decl x (PrtInfo {name=x, expand=False}) g (Just (a,g))- checkProg (tel,g')-checkProg ((Defn x t):tel,g) =- do a <- inferVar (x,g)- check (t,g) a- i <- getId x g- defn' i (t,g)- checkProg (tel,g)- -
− src/PiSigma/Equality.hs
@@ -1,128 +0,0 @@-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}-module PiSigma.Equality where--import Control.Monad--import PiSigma.Syntax-import PiSigma.Evaluation--class Equal a where- eq :: Env e => a -> a -> Eval e ()--instance Equal (Clos Term) where- eq t u = do t' <- eval t- u' <- eval u- eq t' u'--eq' :: Env e => Clos (Term,Term) -> Eval e ()-eq' ((t,u),s) = eq (t,s) (u,s)--eqBind :: (Env e,Closure a) =>- (a -> a -> Eval e ()) ->- Bind a -> Bind a -> Eval e ()-eqBind eq (x0,c0) (x1,c1) =- do let s0 = getScope c0- s1 = getScope c1- (i,s0') <- decl' x0 s0- let s1' = extendScope s1 x1 (i,Nothing)- let c0' = putScope c0 s0'- c1' = putScope c1 s1'- eq c0' c1'--instance (Equal a,Closure a) => Equal (Bind a) where- eq = eqBind eq--instance Equal Val where- eq (Ne t0) (Ne t1) = eq t0 t1- eq (VQ ps0 ((a0,(x0,b0)),s0)) (VQ ps1 ((a1,(x1,b1)),s1))- | ps0 == ps1 = - do eq (a0,s0) (a1,s1)- eq (x0,(b0,s0)) (x1,(b1,s1))- eq (VLam xt0) (VLam xt1) = eq xt0 xt1- eq (VPair ((t0,u0),s0)) (VPair ((t1,u1),s1)) = - do eq (t0,s0) (t1,s1)- eq (u0,s0) (u1,s1)- eq (VBox b) (VBox b') = eq b b' - eq (VLift a) (VLift a') = eq a a'- eq v0 v1 | v0 == v1 = return () -- Type, Label, Enum- | otherwise = fail "Different values"--eqBox :: Env e => Clos Term -> Clos Term -> Eval e ()-eqBox (Var x,s) (Var y,s') = - do x' <- getId x s- y' <- getId y s'- eq x' y'-{--eqBox (Var x,s) u =- do x' <- getId x s- ei <- lookupId x'- case ei of- Closure t -> eqBox t u- Id j -> fail "eqBox: var vs term"- -- wrong level - this should use functions in Evaluation- -- have to avoid races: don't unfold the same id twice!-eqBox t u @ (Var _,_) = eqBox u t --}-eqBox (Let p t,s) c = fail "eqBox: let not implemented"-{-- do s' <- evalProg (p,s)- eqBox (t,s') c--}-eqBox c c'@(Let p t,s) = eqBox c' c -eqBox (Q ps (a,(x,b)),s) (Q ps' (a',(x',b')),s')- | ps == ps' = - do eqBox (a,s) (a',s')- eq (x,Boxed (b,s)) (x',Boxed (b',s'))-eqBox (t :. u,s) (t' :. u',s') =- do eqBox (t,s) (t',s')- eqBox (u,s) (u',s')-eqBox (Split t (x,(y,u)),s) (Split t' (x',(y',u')),s') =- do eqBox (t,s) (t',s')- eq (x,(y,Boxed (u,s))) (x',(y',Boxed (u',s')))-eqBox (Case t bs,s) (Case t' bs',s') =- do eqBox (t,s) (t',s')- zipWithM_ (\ (l,t) (l',t') -> - if l==l' then eqBox (t,s) (t',s')- else fail "eqBox case") bs bs'-eqBox (Lift t,s) (Lift t',s') = eqBox (t,s) (t',s')-eqBox (Box t,s) (Box t',s') = eqBox (t,s) (t',s')-eqBox (Force t,s) (Force t',s') = eqBox (t,s) (t',s') -eqBox (t,s) (t',s') | t == t' = return () -- Type, Label, Enum- | otherwise = fail "Different terms"--- TODO: check that it cannot happen that t and t' are syntacically equal but not alpha equivalent!- -instance Equal Boxed where- eq (Boxed c) (Boxed c') = eqBox c c'--instance Equal Id where- eq i0 i1 - | i0 == i1 = return ()- | otherwise = do ei0 <- lookupId i0- ei1 <- lookupId i1- case (ei0,ei1) of- (Id j0, Id j1) -> unless (j0 == j1)- (fail "Different variables")- (Closure t0, Closure t1) ->- letn i0 (Id i0)- (letn i1 (Id i0)- (eq t0 t1))- _ -> fail "Variable vs neutral"--instance Equal Ne where- eq (NVar i0) (NVar i1) = eq i0 i1- eq (t0 :.. u0) (t1 :.. u1) = - do eq t0 t1- eq u0 u1- eq (NSplit t0 xyu0) (NSplit t1 xyu1) =- do eq t0 t1- eq xyu0 xyu1- eq (NCase t0 (lus0,s0)) (NCase t1 (lus1,s1)) =- do eq t0 t1- let eqBranches [] [] = return ()- eqBranches ((l0,u0):lus0) ((l1,u1):lus1) | l0 == l1 =- do eq (u0,s0) (u1,s1)- eqBranches lus0 lus1- eqBranches _ _ = fail "Case: branches differ"- eqBranches lus0 lus1- eq (NForce t) (NForce t') = eq t t'- eq t u = fail ("Different neutrals:\n"++ show t ++"\n/=\n"++ show u ++"\n")
− src/PiSigma/Evaluation.hs
@@ -1,151 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-module PiSigma.Evaluation where--import Control.Monad.Error-import Control.Monad.State-import Control.Monad.Identity--import PiSigma.Syntax---- * Monad used for evaluation--newtype Eval e a =- Eval {unEval :: StateT e (ErrorT String Identity) a}- deriving (Monad,MonadError String,MonadState e)--run :: e -> Eval e a -> Either String (a,e)-run e (Eval p) = runIdentity $ runErrorT $ runStateT p e --catchE :: Eval e a -> (String -> Eval e a) -> Eval e a-catchE = catchError--getEnv :: Eval e e-getEnv = get--setEnv :: e -> Eval e ()-setEnv = put--getId :: Name -> Scope -> Eval e Id-getId x s = case lookupScope s x of - Just i -> return i- Nothing -> fail ("Undefined Variable: "++x++"\n")---- | Takes a name, a scope, and potentially a type.--- It extends the environment and the scope with that name.-decl :: Env e =>- Name -> PrtInfo -> Scope -> Maybe (Clos Type) ->- Eval e (Id,Scope)-decl x x' s a =- do e <- getEnv- let (i,e') = extE e x'- setEnv e'- return (i,extendScope s x (i,a))--decl' :: Env e => Name -> Scope -> Eval e (Id,Scope)-decl' x s = decl x (PrtInfo {name = x, expand = True}) s Nothing--tdecl :: Env e => Name -> Scope -> (Clos Type) -> Eval e (Id,Scope)-tdecl x g a = decl x (PrtInfo {name = x, expand = True}) g (Just a)---- | Updates the environment.-defn :: Env e => Id -> EnvEntry -> Eval e ()-defn i ei =- do e <- getEnv- setEnv (setE e i ei)--defn' :: Env e => Id -> Clos Type -> Eval e ()-defn' i t = defn i (Closure t)---- | Locally updates the environment.-letn :: Env e => Id -> EnvEntry -> Eval e a -> Eval e a-letn i ei p =- do eo <- lookupId i- defn i ei- a <- p- defn i eo- return a--letn' :: Env e => Id -> Clos Type -> Eval e a -> Eval e a-letn' i t p = letn i (Closure t) p--subst :: Env e => Bind (Clos Term) -> (Clos Term) -> Eval e (Clos Term)-subst (x,(t,s)) u =- do (i,s') <- decl' x s- defn' i u - return (t,s')--evalApp :: Env e => Val -> (Clos Term) -> Eval e Val-evalApp (VLam xt) u = subst xt u >>= eval-evalApp (Ne t) u = return (Ne (t :.. u))-evalApp _ _ = fail "function expected"--lookupId :: Env e => Id -> Eval e EnvEntry-lookupId i = liftM (flip getE i) getEnv--evalId :: Env e => Id -> Eval e Val-evalId i =- do ei <- lookupId i- case ei of- Closure t -> eval t- Id j -> return (Ne (NVar j))---- use subst!-evalSplit :: Env e => Val -> (Bind (Bind (Clos Term))) ->- Eval e Val-evalSplit (VPair ((l,r),s)) (x,(y,(t,s'))) = - do (x',s2) <- decl' x s'- (y',s3) <- decl' y s2- defn' x' (l,s)- defn' y' (r,s)- eval (t,s3)--evalSplit (Ne n) (xy,t) = return (Ne (NSplit n (xy,t)))-evalSplit _ _ = fail "Pair expected"--evalCase :: Env e => Val -> Clos [(Label,Term)] -> Eval e Val-evalCase (VLabel l) (lts,s) = - case lookup l lts of- Nothing -> fail "case not matched"- Just t -> eval (t,s)-evalCase (Ne n) lts = return (Ne (NCase n lts))-evalCase _ _ = fail "Label expected"--force :: Env e => Val -> Eval e Val-force (VBox (Boxed c)) = eval c-force (Ne n) = return (Ne (NForce n))-force _ = fail "Box expected"--eval :: Env e => (Clos Term) -> Eval e Val-eval (Var x, s) = getId x s >>= evalId-eval (Let g t, s) = evalProg (g,s) >>= curry eval t-eval (Type,s) = return VType-eval (Q ps axb,s) = return (VQ ps (axb,s))-eval (Lift t,s) = return (VLift (t,s))-eval (Lam (x,t), s) = return (VLam (x,(t,s)))-eval (t :. u ,s) = eval (t,s) >>= flip evalApp (u,s)-eval (Pair tu,s) = return (VPair (tu,s))-eval (Split t (x,(y,u)),s)- = eval (t,s) >>= flip evalSplit (x,(y,(u,s)))-eval (Enum ls,s) = return (VEnum ls)-eval (Label l,s) = return (VLabel l)-eval (Case t lts,s) = eval (t,s) >>= flip evalCase (lts,s)-eval (Box t,s) = return (VBox (Boxed (t,s)))-eval (Force t,s) = eval (t,s) >>= force----- forced eval (should be integrated into eval?)-feval :: Env e => (Clos Term) -> Eval e Val-feval t = do t' <- eval t- case t' of - VBox (Boxed u) -> feval u- v -> return v-- --evalProg :: Env e => Clos Prog -> Eval e Scope-evalProg ([],s) = return s-evalProg ((Decl x _):tel, s) = do (_,s') <- decl x (PrtInfo x False) s Nothing- evalProg (tel,s')-evalProg ((Defn x t):tel, s) = do i <- getId x s- defn' i (t,s)- evalProg (tel,s)
− src/PiSigma/Nf.hs
@@ -1,111 +0,0 @@-{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, FunctionalDependencies,- TypeSynonymInstances, FlexibleInstances #-}-module PiSigma.Nf where--{- Implementation of a normalisation function.- Useful for testing.--}--import Control.Monad--import PiSigma.Syntax-import PiSigma.Evaluation--type Vars = [String]--fresh :: Name -> Vars -> Name-fresh x xs = if x/="" && elem x xs then fresh (x++"'") xs- else x--class Nf a b | a -> b where- nf :: Env e => Vars -> a -> Eval e b- nf = nf' True- quote :: Env e => Vars -> a -> Eval e b- quote = nf' False- nf' :: Env e => Bool -> Vars -> a -> Eval e b---instance Nf (Clos Term) Term where- nf' True xs t = do t' <- eval t- nf' True xs t'- nf' False xs t = qq xs t--instance Nf Id Term where- nf' b xs i = do e <- getEnv- let (PrtInfo x exp) = prtE e i- case getE e i of- (Id _) -> return (Var x) - (Closure t) -> if exp then nf' b xs t- -- this is bad, we should not- -- expand inside a box!- else return (Var x) --qq :: Env e => Vars -> Clos Term -> Eval e Term-qq xs (Var x,s) = do i <- getId x s- quote xs i-qq xs (Let g t, s) = fail "quote let: not implemented!"-{-do s' <- evalProg (g,s)- qq xs (t,s') - -- this seems wrong! we should return a Let- -- and we should extend xs!--}-qq xs (Q ps (a,(x,b)),s) = - do a' <- qq xs (a,s)- xb' <- quote xs (x,(b,s))- return (Q ps (a',xb'))-qq xs (Lift t,s) = liftM Lift (qq xs (t,s))-qq xs (Lam (x,t), s) = liftM Lam (quote xs (x,(t,s)))-qq xs (t :. u ,s) = do t' <- qq xs (t,s)- u' <- qq xs (u,s)- return (t' :. u')-qq xs (Pair (t,u),s) = do t' <- qq xs (t,s)- u' <- qq xs (u,s)- return (Pair (t',u'))-qq xs (Split t (x,(y,u)),s) = do t' <- qq xs (t,s)- xyu' <- quote xs (x,(y,(u,s)))- return (Split t' xyu')-qq xs (Case t lts,s) = do t' <- qq xs (t,s)- lts' <- mapM (\ (l,t) -> - do t' <- qq xs (t,s)- return (l,t')) lts- return (Case t' lts') -qq xs (Box t,s) = liftM Box (qq xs (t,s))-qq xs (Force t,s) = liftM Force (qq xs (t,s))-qq xs (t,s) = return t -- Type, Enum, Label--instance (Closure a,Nf a b) => Nf (Bind a) (Bind b) where- nf' b xs (x,t) = do let x' = fresh x xs- (i,s') <- decl x (PrtInfo x' True) (getScope t) Nothing- t' <- nf' b (x':xs) (putScope t s')- return (x',t')--instance Nf Val Term where- nf' b xs (Ne n) = nf' b xs n- nf' b xs VType = return Type- nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) - xc' <- nf' b xs (x,(c,s))- return (Q ps (a',xc'))- nf' b xs (VLift c) = liftM Lift (nf' b xs c)- nf' b xs (VLam xt) = liftM Lam (nf' b xs xt)- nf' b xs (VPair ((t,u),s)) = do t' <- nf' b xs (t,s)- u' <- nf' b xs (u,s)- return (Pair (t',u'))- nf' b xs (VBox (Boxed c)) = liftM Box (nf' False xs c)- nf' b xs (VEnum ls) = return (Enum ls)- nf' b xs (VLabel l) = return (Label l)---instance Nf Ne Term where- nf' b xs (NVar i) = nf' b xs i- nf' b xs (t' :.. u) = do t <- nf' b xs t'- u' <- nf' b xs u- return (t :. u')- nf' b xs (NSplit t xyu) = do t' <- nf' b xs t- xyu' <- nf' b xs xyu- return (Split t' xyu')- nf' b xs (NCase t (lus,s)) = do t' <- nf xs t- lus' <- mapM (\ (l,u) -> - do u' <- nf' b xs (u,s)- return (l,u')) lus- return (Case t' lus')- nf' b xs (NForce t) = liftM Force (nf xs t)
− src/PiSigma/Parser.hs
@@ -1,141 +0,0 @@-module PiSigma.Parser (module PiSigma.Parser, Parser) where--import Prelude hiding (pi)-import Data.Char-import Data.List--import Control.Monad-import Control.Applicative hiding ((<|>), many)--import Text.ParserCombinators.Parsec as P hiding (token, label)--import PiSigma.Syntax hiding (label)--type SParser = CharParser ()---- * Comments and whitespace--blockComment :: SParser ()-blockComment = () <$ try (string "{-") <* inComment <* string "-}"--inComment :: SParser ()-inComment =- () <$ many (choice [ () <$ noneOf "{-"- , try $ () <$ char '-' <* notFollowedBy (char '}')- , try $ () <$ char '{' <* notFollowedBy (char '-')- , blockComment ])--lineComment :: SParser ()-lineComment = () <$ try (string "--") <* many (noneOf "\n")--whiteSpace :: SParser ()-whiteSpace = () <$ spaces <* many ((lineComment <|> blockComment) <* spaces)- <?> ""---- * Identifiers--identChar :: SParser Char-identChar = alphaNum <|> oneOf "_'"--ident :: SParser String-ident = - (try $ do- xs <- (:) <$> letter <*> many identChar <* whiteSpace- guard (xs `notElem` keywords)- return xs) <?> "identifier"--keywords :: [String]-keywords = [ "case", "of", "let", "in", "split", "Type", "with" ]--label :: SParser Name-label = char '\'' *> ident---- * Tokens--token :: String -> SParser String-token xs = (try $ (string xs <* whiteSpace)) <?> show xs---- * Brackets--parensed = between (token "(") (token ")")-braced = between (token "{") (token "}")-bracketed = between (token "[") (token "]")---- * Terms--sTerm5 :: SParser Term-sTerm5 =- Type <$ token "Type"- <|> (Enum <$> braced (many ident) <?> "enumeration")- <|> Case <$ token "case" <*> sTerm <* token "of"- <*> braced (sBranch `sepBy` token "|")- <|> (Label <$> label <?> "label")- <|> (Box <$> bracketed sTerm <?> "box")- <|> (Lift <$ token "^" <*> sTerm5 <?> "'^'")- <|> Var <$> ident- <|> parensed sTerm--sTerm4 :: SParser Term-sTerm4 =- try (parensed (curry Pair <$> sTerm <* token "," <*> sTerm))- <|> sTerm5--sTerm3 :: SParser Term-sTerm3 =- try (parensed (sigmas <$> many1 ident <* token ":" <*> sTerm) <* token "*")- <*> sTerm3- <|> Force <$ token "!" <*> sTerm4- <|> foldl1 (:.) <$> many1 sTerm4--sTerm2 :: SParser Term-sTerm2 =- foldl1 (-*-) <$> sTerm3 `sepBy1` token "*"---- TODO: make more beautiful or renumber-sTerm1b :: SParser Term-sTerm1b =- try (parensed (pis <$> many1 ident <* token ":" <*> sTerm) <* token "->")- <*> sTerm- <|> sTerm2- -sTerm1 :: SParser Term-sTerm1 =- flip ($) <$> sTerm1b <*> option id (flip (->-) <$ token "->" <*> sTerm)--sTerm :: SParser Term-sTerm =- lam <$ token "\\" <*> many ident <* token "->" <*> sTerm- <|> split <$ token "split" <*> sTerm <* token "with"- <* token "(" <*> ident <* token "," <*> ident <* token ")"- <* token "->" <*> sTerm- <|> Let <$ token "let" <*> sProg <* token "in" <*> sTerm- <|> sTerm1--sProg :: SParser Prog-sProg = concat <$> (sEntry `sepEndBy` token ";")--sEntry :: SParser [Entry]-sEntry = - do- n <- ident- b <- (True <$ token ":" <|> False <$ token "=")- t <- sTerm- if b- then do- d <- option Nothing (Just <$ token "=" <*> sTerm)- case d of- Nothing -> return [Decl n t]- Just t' -> return [Decl n t, Defn n t']- else return [Defn n t]--sBranch :: SParser (Label,Term)-sBranch = (,) <$> ident <* token "->" <*> sTerm--sPhrase :: SParser Phrase-sPhrase =- (try $ Prog <$> sProg <* eof) <|> Term <$> sTerm <* eof--s2Terms :: SParser (Term, Term)-s2Terms = (,) <$> sTerm5 <*> sTerm5--parse p = P.parse (whiteSpace *> p <* eof)
− src/PiSigma/Print.hs
@@ -1,108 +0,0 @@-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleInstances #-}-module PiSigma.Print where--import Control.Monad--import Text.PrettyPrint.ANSI.Leijen--import PiSigma.Syntax-import PiSigma.Evaluation-import PiSigma.Nf---- * Print class for various types--class Print a where- prt :: Env e => a -> Eval e String--instance Print Val where- prt a = quote [] a >>= prt--instance Print (Clos Term) where- prt a = quote [] a >>= prt--instance Print Ne where- prt a = quote [] a >>= prt--instance Print Term where- prt a = return (displayS (renderPretty 0.8 75 (pretty a)) "")---data Msg = V Val | C (Clos Term) | T Term | S String--instance Print Msg where- prt (V v) = prt v- prt (C c) = prt c- prt (T t) = prt t- prt (S s) = return s--failp :: (Print a, Env e) => [a] -> Eval e b-failp ps = do msg <- foldM (\ msg p -> do s <- prt p- return (msg++s)) "" ps- fail msg---- * Pretty printer for terms---- | Context for printing. Determines whether parentheses are--- required.-type PrintContext = Int--prettyTerm :: PrintContext -> Term -> Doc-prettyTerm _ (Var x) = text x-prettyTerm _ (Let p t) = pretty p <> pretty t-prettyTerm _ Type = text "Type"-prettyTerm c (Q Pi (t1,(n,t2))) =- contextParens c 1 $- group (binding 2 n t1 <$> text "->" <+> prettyTerm 1 t2)-prettyTerm c (Q Sigma (t1,(n,t2))) =- contextParens c 2 $- binding 2 n t1 <+> text "*" <+> prettyTerm 3 t2-prettyTerm _ (Lam (n,t)) =- text "\\" <+> text n <+> text "->" <+> prettyTerm 0 t-prettyTerm c (t1 :. t2) =- group (hang 2 (contextParens c 3 (prettyTerm 3 t1 <$> prettyTerm 4 t2)))-prettyTerm c (Pair (t1,t2)) =- tupled (map (prettyTerm 0) [t1,t2])-prettyTerm _ (Split t1 (n1,(n2,t2))) =- hang 2 (text "split" <+> prettyTerm 0 t1 <+> text "with"- <+> parens (text n1 <> comma <> text n2)- <+> text "->" <$> prettyTerm 0 t2)-prettyTerm _ (Enum ls) = braces (sep (map text ls))-prettyTerm _ (Label l) = text ('\'' : l)-prettyTerm _ (Case t bs) =- hang 2 (text "case" <+> prettyTerm 0 t <+> text "of" <$> branches bs)-prettyTerm c (Lift t) =- contextParens c 5 $- text "^" <> prettyTerm 5 t-prettyTerm _ (Box t) =- brackets (prettyTerm 0 t)-prettyTerm c (Force t) =- contextParens c 3 $- text "!" <> prettyTerm 4 t--prettyEntry :: Entry -> Doc-prettyEntry (Defn n t) =- hang 2 (text n <+> text "=" <$> prettyTerm 0 t <> text ";")-prettyEntry (Decl n t) =- hang 2 (text n <+> text ":" <$> prettyTerm 0 t <> text ";")--binding :: PrintContext -> String -> Term -> Doc-binding c "" t = prettyTerm c t-binding _ n t = parens (text n <+> colon <+> prettyTerm 0 t)--branches :: [(Label,Term)] -> Doc-branches bs = encloseSep lbrace rbrace (text "|") (map branch bs)- where branch (n,t) = text n <+> text "->" <+> prettyTerm 0 t---- | Prints parens if the current context is higher--- than a certain limit.-contextParens :: PrintContext -> PrintContext -> Doc -> Doc-contextParens c d p | c > d = parens p- | otherwise = p--instance Pretty Term where- pretty = prettyTerm 0--instance Pretty Entry where- pretty = prettyEntry-
− src/PiSigma/Syntax.hs
@@ -1,234 +0,0 @@-{-# LANGUAGE TypeSynonymInstances #-}-module PiSigma.Syntax where--import Prelude hiding (pi)---- * Abstract syntax--data Phrase = Prog Prog | Term Term- deriving (Show,Eq)--type Name = String--type Label = String--data Entry = Decl Name Type | Defn Name Term- deriving (Show,Eq)--type Prog = [Entry]--{--Maybe better-data Prog = Decl Type (Bind Prog) | Defn Name Term Prog--}--type Type = Term---- | The use of Bind indicates the scope of the--- bound identifier.-type Bind a = (Name,a)---- | For treating quantifiers in a uniform way.-data PiSigma = Pi | Sigma- deriving (Show,Eq)--data Term =- Var String- | Let Prog Term- | Type- | Q PiSigma (Type,Bind Type)- | Lam (Bind Term)- | Term :. Term- | Pair (Term,Term)- | Split Term (Bind (Bind Term)) -- split t with (x,y) -> u- | Enum [Label]- | Label Label- | Case Term [(Label,Term)] -- case t of { L -> u }- | Lift Term- | Box Term- | Force Term- deriving (Show,Eq)---- * Smart constructors---- | Smart constructor for lambda abstractions.-lam :: [Name] -> Term -> Term-lam [] t = t-lam (x:xs) t = Lam (x,lam xs t)---- | Smart constructor for split.-split :: Term -> Name -> Name -> Term -> Term-split t1 x y t2 = Split t1 (x,(y,t2))---- | Smart constructor for quantifiers.-q :: PiSigma -> [(Name,Type)] -> Type -> Type-q ps [] b = b-q ps ((x,a):xas) b = Q ps (a,(x,q ps xas b))---- | Smart constructor for multiple Pi applications.-pis' :: [(Name,Type)] -> Type -> Type-pis' = q Pi---- | Smart constructor for multiple Pi applications.-pis :: [Name] -> Type -> Type -> Type-pis ns t = pis' (map (\ n -> (n,t)) ns)---- | Smart constructor for Pi.-pi :: Name -> Type -> Type -> Type-pi n t = pis' [(n,t)]---- | Smart constructor for multiple Sigma applications.-sigmas' :: [(Name,Type)] -> Type -> Type-sigmas' = q Sigma---- | Smart constructor for multiple Sigma applications.-sigmas :: [Name] -> Type -> Type -> Type-sigmas ns t = sigmas' (map (\ n -> (n,t)) ns)---- | Smart constructor for Sigma.-sigma :: Name -> Type -> Type -> Type-sigma n t = sigmas' [(n,t)]---- | Smart constructor for function space.-(->-) :: Type -> Type -> Type-(->-) = pi ""---- | Smart constructor for product.-(-*-) :: Type -> Type -> Type-(-*-) = sigma ""---- * Values (well-scoped WHNFs) and environments---- ** Identifiers--type Id = Int -- index in (potentially multiple) environments---- ** Scopes--data Scope = Scope [(Name,(Id,Maybe (Clos Type)))]- deriving (Show,Eq)--{---TODO:--Perhaps return to the following types for scopes:--data Sc a = Scope [(Name,(Id, a))]--type Scope = Sc ()-type Ctx = Sc (Clos Type)--We then need a forgetful mapping:--fog :: Ctx -> Scope-fog c = map (\ (x,(i,a)) -> (x,(i,()))) c --Alternatively, we can try to make Scopes-existential, essentially:--type Scope = exists a. Sc a---}--emptyScope :: Scope-emptyScope = Scope []--extendScope :: Scope -> Name -> (Id,Maybe (Clos Type)) -> Scope-extendScope (Scope s) x (i,a) = Scope ((x,(i,a)) : s)--lookupScope :: Scope -> Name -> Maybe Id-lookupScope (Scope s) x = do (i,_) <- lookup x s- return i--lookupCon :: Scope -> Name -> Maybe (Clos Type)-lookupCon (Scope s) x = do (_,Just a) <- lookup x s- return a---- ** Closures--type Clos a = (a,Scope)----type C a = (Con,a)----c2clos :: C a -> Clos a---c2clos (g,a) = (a,fog g)---- fix order, name of C...--class Closure a where - getScope :: a -> Scope- putScope :: a -> Scope -> a--instance Closure (Clos a) where- getScope (_,s) = s- putScope (a,_) s = (a,s)--instance Closure a => Closure (Bind a) where- getScope (_,a) = getScope a- putScope (x,a) s = (x,putScope a s)--instance Closure Boxed where- getScope (Boxed c) = getScope c- putScope (Boxed c) s = Boxed (putScope c s)--{- could be used to refactor the code using bindings. -}--ty :: Clos Type-ty = (Type,emptyScope)--label :: String -> Clos Term-label s = (Label s,emptyScope)--type VType = Val--newtype Boxed = Boxed (Clos Term) deriving (Show,Eq)---- ** Values--data Val =- Ne Ne- | VType - | VQ PiSigma (Clos (Type,Bind Type))- | VLift (Clos Type)- | VLam (Bind (Clos Term))- | VPair (Clos (Term, Term))- | VEnum [Label]- | VLabel Label - | VBox Boxed- deriving (Show,Eq)---- | Neutral terms.-data Ne =- NVar Id- | Ne :.. (Clos Term)- | NSplit Ne (Bind (Bind (Clos Term)))- | NCase Ne (Clos [(Label,Term)])- | NForce Ne- deriving (Show,Eq)---- ** Environments--data EnvEntry = Id Id | Closure (Clos Term) deriving Show--data PrtInfo = PrtInfo {name :: Name, expand :: Bool}--class Env e where - emptyE :: e- extE :: e -> PrtInfo -> (Id,e)- setE :: e -> Id -> EnvEntry -> e- getE :: e -> Id -> EnvEntry- prtE :: e -> Id -> PrtInfo--set :: [a] -> Int -> a -> [a]-set (a:as) 0 b = b:as-set (a:as) i b = a:set as (i-1) b- -type EnvEntries = [(EnvEntry,PrtInfo)]--instance Env EnvEntries where- emptyE = []- extE e x = let i = length e in (i,e++[(Id i,x)])- setE e i v = let (_,x) = e!!i in set e i (v,x)- getE e i = let (v,_) = e!!i in v- prtE e i = let (_,x) = e!!i in x
+ src/Tools/Interpreter/Main.hs view
@@ -0,0 +1,15 @@+module Main where++import System.Environment++import Tools.Interpreter.REPL++main :: IO ()+main = + do+ args <- getArgs+ let ini = mapM_ (handleCommand . Load) args+ runREPL (handleCommand Startup >> ini >> repl)++-- TODO: better command line arg handling; allow non-interactive mode+
+ src/Tools/Interpreter/REPL.hs view
@@ -0,0 +1,356 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Tools.Interpreter.REPL+ ( REPL (..)+ , REPLCommand (..)+ , handleCommand+ , repl+ , runREPL )+ where++import Prelude hiding (catch)+import Control.Monad.Error+import Control.Monad.State+import Control.Monad.Trans+import Data.Char+import qualified Data.List as List+import System.Console.Haskeline.Class+import System.IO+import Data.Version (showVersion)++import Language.PiSigma.Check+import Language.PiSigma.Equality+import Language.PiSigma.Evaluate+import Language.PiSigma.Lexer+ as Lexer+ ( Parser )+import Language.PiSigma.Normalise+import Language.PiSigma.Parser+import Language.PiSigma.Pretty+import Language.PiSigma.Syntax+import qualified Language.PiSigma.Util.String.Internal+ as Internal+import qualified Language.PiSigma.Util.String.Parser+ as Parser++import Paths_pisigma++-- * Instances needed for newtype deriving++instance (Error e, MonadException m) => MonadException (ErrorT e m) where+ catch m = ErrorT . catch (runErrorT m) . (runErrorT .)+ block = mapErrorT block+ unblock = mapErrorT unblock++instance (Error e, MonadHaskeline m) => MonadHaskeline (ErrorT e m) where+ getInputLine = lift . getInputLine+ getInputChar = lift . getInputChar+ outputStr = lift . outputStr+ outputStrLn = lift . outputStrLn++-- * Types++-- | The REPL monad has exceptions, a line editor with history using+-- Haskeline, and state.+newtype REPL a = REPL { unREPL :: ErrorT REPLError (HaskelineT (StateT REPLState IO)) a }+ deriving ( Monad+ , MonadException+ , MonadError REPLError+ , MonadHaskeline+ , MonadIO+ , MonadState REPLState )++-- | The state currently keeps track of identifiers defined and their+-- types, as well as a list of files currently loaded.+data REPLState =+ REPLState+ { replState :: (Scope, EnvEntries)+ , replFiles :: [FilePath]+ }++-- TODO: Add a search path and verbosity options.++-- ** Commands++-- | Commands that can be entered at the REPL prompt.+data REPLCommand =+ Load String+ | Reload+ | Quit+ | EvalPhrase Phrase+ | Noop+ | Clear+ | Equal (Term,Term)+ | TypeOf Term+ | Help+ | Browse+ | Startup+ | Version++-- ** Errors++-- | Normal Errors abort the current command but do not quit the REPL.+-- If we actually wish to quit, we can throw a Terminate error.+data REPLError =+ Error+ | Terminate++instance Error REPLError where+ noMsg = Error+ strMsg _ = Error++-- * REPL monad++initialREPLState :: REPLState+initialREPLState = + REPLState (emptyScope, emptyE) []++runREPL :: REPL () -> IO ()+runREPL r =+ do+ runStateT (runHaskelineT (setComplete pisigmaCompletion defaultSettings)+ (runErrorT (unREPL r)))+ initialREPLState+ return ()++-- * Haskeline++-- | Completion in PiSigma. For the moment, we use file name completion+-- while in a load command, and identifier completion everywhere else.+pisigmaCompletion :: CompletionFunc (StateT REPLState IO)+pisigmaCompletion (x1, x2)+ | ":l" `List.isPrefixOf` List.reverse x1 = completeFilename (x1, x2)+ | otherwise = completeWord Nothing " " identifier (x1, x2)+ where+ identifier :: String -> StateT REPLState IO [Completion]+ identifier x = do+ (Scope sc, _) <- gets replState+ let names = map fst sc+ cands = filter (Internal.fromString x `Internal.isPrefixOf`) names+ return $ map (simpleCompletion . Internal.toString) (List.sort cands)++-- * Help++-- | Preliminary interpreter help message.+help :: String+help = List.unlines+ [ "PiSigma currently supports the following commands:"+ , ""+ , " :l load a source file"+ , " :r reload current source file"+ , " :b browse current identifiers"+ , " :c clear the environment"+ , " :t ask for the type of a term"+ , " :e test two terms for beta equality"+ , " :v version"+ , " :q quit"+ , ""+ , "Type a declaration or an expression to evaluate it."+ ]++-- * REPL core++-- | Performs a single REPL step. Print prompt, read input,+-- dispatch.+replStep :: REPL ()+replStep =+ do+ f <- gets replFiles+ x <- getInputLine (List.unwords (List.reverse f) ++ "> ")+ c <- interpretInput (fmap id x)+ handleCommand c++-- | Run the interpreter as long as desired.+repl :: REPL ()+repl =+ do+ catchError replStep+ (\ e -> case e of+ Error -> return ()+ Terminate -> throwError Terminate)+ repl++-- * Command handling++-- | Preliminary input interpretation, based on the+-- current parser and no particular intelligence in+-- parsing commands correctly.+interpretInput :: Maybe String -> REPL REPLCommand+interpretInput Nothing = return Quit+interpretInput (Just x)+ | ":l" `List.isPrefixOf` x = return $ Load $ norm $ strip xArg+ | ":r" `List.isPrefixOf` x = return Reload+ | ":b" `List.isPrefixOf` x = return Browse+ | ":q" `List.isPrefixOf` x = return Quit+ | ":c" `List.isPrefixOf` x = return Clear+ | ":e" `List.isPrefixOf` x = parseInputInteractive s2Terms Equal xArg+ | ":t" `List.isPrefixOf` x = parseInputInteractive sTerm TypeOf xArg+ | ":h" `List.isPrefixOf` x+ || ":?" `List.isPrefixOf` x = return Help+ | ":v" `List.isPrefixOf` x = return Version+ | ":" `List.isPrefixOf` x = replMessage "unknown command" >> return Noop+ | otherwise = parseInputInteractive sPhrase EvalPhrase x+ where+ norm :: String -> String+ norm [] = []+ norm ('\\' : c : xs) = c : norm xs+ norm ( c : xs) = c : norm xs++ strip :: String -> String+ strip = List.reverse+ . List.dropWhile isSpace+ . List.reverse+ . List.dropWhile isSpace++ xArg :: String+ xArg = snd $ break (== ' ') x++-- | Turn a string into a REPL command.+parseInput :: FilePath+ -> Parser t+ -> (t -> REPLCommand)+ -> Parser.String+ -> REPL REPLCommand+parseInput f p cmd s =+ case parse p f s of+ Left err -> do+ replMessage $ "Parse error: " ++ (show) err ++ "\n"+ return Noop+ Right p' -> return (cmd p')++parseInputInteractive :: Parser t+ -> (t -> REPLCommand)+ -> String+ -> REPL REPLCommand+parseInputInteractive p cmd = parseInput "<interactive>" p cmd . Parser.fromString++-- | Command handler. Returns a flag indicating whether+-- the interpreter should continue.+handleCommand :: REPLCommand -> REPL ()+handleCommand c =+ case c of+ Version-> replMessage $ "PiSigma version " ++ showVersion version+ Startup-> handleCommand Version >> replMessage "Type :? for help."+ Help -> replMessage help+ Load f ->+ do+ fs <- gets replFiles+ if f `elem` fs then+ replMessage $ "Skipping " ++ f ++ "."+ else do+ mx <- liftIO $ liftM (Just) (Parser.readFile f)+ `catch` (\ (_ :: IOException) -> return Nothing)+ case mx of+ Nothing -> do+ replMessage $ "Could not find " ++ f ++ "."+ throwError Error+ Just x -> do+ -- Allow source files to have interpreter commands at the top;+ -- we currently use this as a replacement for a module system+ let spanP s = case Parser.uncons s of+ Just (':', _) -> True+ _ -> False+ (cmds, rest) = List.span spanP $ Parser.lines x+ mapM_ (\ c' -> handleCommand =<< (interpretInput . Just . Parser.toString) c') cmds+ p <- parseInput f sProg (EvalPhrase . Prog)+ (Parser.unlines (List.replicate (List.length cmds) "" ++ rest))+ handleCommand p+ modify (\ s -> s { replFiles =+ case replFiles s of+ (g : fs') | g == f -> g : fs'+ xs -> f : xs })+ -- We print the "Loaded" message after executing initial+ -- interpreter commands in order to reflect the dependency+ -- order of different source files.+ replMessage $ "Loaded " ++ f ++ "."+ Reload ->+ do+ f <- gets replFiles+ handleCommand Clear+ mapM_ (handleCommand . Load) (List.reverse f)+ Browse ->+ do+ (Scope sc, _) <- gets replState+ let names :: [Pretty]+ names = map (text . Seq . fst) sc+ liftIO $ putPretty $ vcat names+ liftIO $ putStrLn ""+ Quit ->+ throwError Terminate+ EvalPhrase (Prog p) ->+ execProg p+ EvalPhrase (Term t) ->+ execTerm t+ Equal (t1,t2) ->+ eqTerms t1 t2+ TypeOf t ->+ inferTerm t+ Clear ->+ put initialREPLState+ Noop ->+ return ()++-- ** Command handler helpers++execProg :: Prog -> REPL ()+execProg p =+ do+ s <- get+ let (con,env) = replState s+ case run env (checkProg (p,con)) of+ Right s' -> put (s { replState = s' })+ Left e -> do+ liftIO $ Internal.putStrLn e+ throwError Error++execTerm :: Term -> REPL ()+execTerm t =+ do+ s <- get+ let (con,env) = replState s+ p = do+ a <- infer (t,con)+ t' <- nf [] (t,con)+ pa <- evalPrint a+ pt <- evalPrint t'+ return $ fromPretty $ pt <$> colon <+> align pa+ case run env p of+ Right (m,_) -> liftIO $ Internal.putStrLn m+ Left e -> do+ liftIO $ Internal.putStrLn e+ throwError Error++eqTerms :: Term -> Term -> REPL ()+eqTerms t1 t2 =+ do+ s <- get+ let (con,env) = replState s+ p = eq (t1,con) (t2,con)+ case run env p of+ Right _ -> liftIO $ putStrLn "yes"+ Left e -> do+ liftIO $ Internal.putStrLn e+ throwError Error+ ++inferTerm :: Term -> REPL ()+inferTerm t =+ do+ s <- get+ let (con,env) = replState s+ p = evalPrint =<< infer (t,con)+ case run env p of+ Right (m,_) -> do+ liftIO $ putPretty m+ liftIO $ putStrLn ""+ Left e -> do+ liftIO $ Internal.putStrLn e+ throwError Error++-- | Placeholder for a message function that can depend+-- on verbosity settings.+replMessage :: String -> REPL ()+replMessage = liftIO . putStrLn