packages feed

uAgda (empty) → 1.0.0.0

raw patch · 17 files changed

+1732/−0 lines, 17 filesdep +BNFC-metadep +basedep +cmdargssetup-changed

Dependencies added: BNFC-meta, base, cmdargs, containers, monads-fd, parsec, pretty, transformers

Files

+ AbsSynToTerm.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE PackageImports #-}++module AbsSynToTerm where++import Terms +import qualified RawSyntax as A+import RawSyntax (Identifier(..))+import "transformers" Control.Monad.Trans.State (runStateT, StateT)+import "transformers" Control.Monad.Trans.Reader+import "transformers" Control.Monad.Trans.Error hiding (throwError)+import "monads-fd" Control.Monad.Error+import "monads-fd" Control.Monad.State+import Control.Applicative+import Data.Functor.Identity+import Data.List+import Basics++type LocalEnv = [String]+type GlobalEnv = ()++type Resolver a = ReaderT LocalEnv (StateT GlobalEnv (ErrorT String Identity)) a+++runResolver :: Resolver a -> a+runResolver x = case runIdentity $ runErrorT $ runStateT (runReaderT x []) () of+                  Left err -> error err+                  Right a -> fst a++look :: Identifier -> Resolver Term+look (ident@(Identifier (position,x))) = do+  e <- ask+  case elemIndex x e of+    Nothing -> throwError ("unknown identifier: " ++ show ident)+    Just x -> return $ Bound (Irr position) x++insertVar :: Identifier -> LocalEnv -> LocalEnv+insertVar (Identifier (_pos,x)) e = x:e++dummyVar :: Identifier+dummyVar = Identifier ((0,0),"_")+++manyDep binder a []     b = resolveTerm b+manyDep binder a (x:xs) b = binder (Irr x) <$> resolveTerm a <*> local (insertVar x) (manyDep binder a xs b)++manyLam :: [A.Bind] -> A.Exp -> Resolver Term+manyLam []            b = resolveTerm b+manyLam (A.NoBind (A.AIdent x):xs) b = Lam (Irr x) (Hole dummyPosition "") <$> local (insertVar x) (manyLam xs b)+manyLam (A.Bind (A.AIdent x) t:xs) b = Lam (Irr x) <$> resolveTerm t <*> local (insertVar x) (manyLam xs b)+++extractVars :: A.Exp -> Resolver [Identifier]+extractVars (A.EVar (A.AIdent i)) = return [i]+extractVars (A.EApp (A.EVar (A.AIdent i)) rest) = (i:) <$> extractVars rest+extractVars _ = throwError "list of variables expected"++resolveTerm :: A.Exp -> Resolver Term+resolveTerm (A.EHole (A.Hole (p,x))) = return $ Hole (Irr p) x+resolveTerm (A.EParam x) = Param <$> resolveTerm x+resolveTerm (A.EDestr x (A.Natural n)) = Destroy (Relevance $ read n) <$> resolveTerm x+resolveTerm (A.EUp x) = Shift (Sort 1 0) <$> resolveTerm x+resolveTerm (A.ELeft x) = Shift oneRel <$> resolveTerm x+resolveTerm (A.EVar (A.AIdent x)) = look x+resolveTerm (A.ESet (A.Sort (p,'*':s))) = return $ Star (Irr p) $ Sort lvl rel+    where (l,r) = break (== '@') s+          lvl = read ('0':l)+          rel = case r of+            ('@':xs) -> Relevance $ read ('0':xs)+            _ -> 0+resolveTerm (A.EProj x (A.AIdent (Identifier (_,field)))) = Proj <$> resolveTerm x <*> pure field+resolveTerm (A.EExtr x (A.AIdent (Identifier (_,field)))) = Extr <$> resolveTerm x <*> pure field+resolveTerm (A.EApp f x) = (:$:) <$> resolveTerm f <*> resolveTerm x+resolveTerm (A.ESigma a b) = case a of+   (A.EAnn vars a') -> do vs <- extractVars vars+                          manyDep Sigma a' vs b+                          +   (A.EAbs _ _ _) -> throwError "cannot use lambda for type"+   _              -> Sigma (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)            +resolveTerm (A.EPi a _arrow_ b) = case a of+   (A.EAnn vars a') -> do vs <- extractVars vars+                          manyDep Pi a' vs b+                          +   (A.EAbs _ _ _) -> throwError "cannot use lambda for type"+   _              -> Pi (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)+resolveTerm (A.EAbs ids _arrow_ b) = manyLam ids b+resolveTerm (A.EPair (A.Decl (A.AIdent i) e) rest) = Pair (Irr i) <$> resolveTerm e <*> local (insertVar i) (resolveTerm rest)+resolveTerm (A.EPair (A.PDecl (A.AIdent i) e t) rest) = +   Pair (Irr i) <$> +   (Ann <$> (OfParam (Irr i) <$> resolveTerm e) <*> resolveTerm t)+   <*> local (insertVar i) (resolveTerm rest)++resolveTerm (A.EAnn e1 e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2+
+ Basics.hs view
@@ -0,0 +1,118 @@+{-# LANGUAGE OverloadedStrings, GeneralizedNewtypeDeriving #-}+module Basics+       (module Data.Monoid, (<>),+        module Control.Applicative,+        Irr(..), +        Sort(..), prettySortNam, prettyRel,+        above, oneLev, next, oneRel, zero,+        Ident, Identifier(..), DisplayContext,+        Position, dummyPosition, identPosition, +        isDummyId, modId, synthId, dummyId, idString,+        Relevance(..), (+.),+        Lattice(..)) where++import Display+import qualified RawSyntax as A+import RawSyntax (Identifier(..))+import Control.Applicative+import Data.Monoid+import Data.Sequence (Seq)+++(<>) :: Monoid a => a -> a -> a+(<>) = mappend++-----------+-- Irr++newtype Irr a = Irr {fromIrr :: a}+    deriving Show++instance Eq (Irr a) where+    x == y = True++instance Pretty x => Pretty (Irr x) where+    pretty (Irr x) = pretty x++--------------+-- Ident+instance Pretty Identifier where+    pretty (Identifier (_,x)) = text x+++type Ident = Irr Identifier++isDummyId (Irr (Identifier (_,"_"))) = True+isDummyId _ = False ++synthId :: String -> Ident+synthId x = Irr (Identifier (fromIrr $ dummyPosition,x))++dummyId = synthId "_"++idString :: Ident -> String+idString (Irr (Identifier (_,name))) = name++type DisplayContext = Seq Ident++----------------+-- Position++type Position = (Int,Int)++identPosition (Irr (Identifier (p,_))) = Irr p++dummyPosition = Irr (0,0)++modId :: (String -> String) -> Ident -> Ident+modId f (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,f x)))++------------------+-- Sort++instance Lattice Int where+    (⊔) = max++newtype Relevance = Relevance {fromRel :: Int}+  deriving (Real,Enum,Integral,Num,Ord,Eq,Show,Lattice)++class Lattice a where+    (⊔) :: a -> a -> a+++data Sort = Sort {sortLevel :: Int, sortRelevance :: Relevance}+  deriving Eq++instance Show Sort where+    show s = render (prettySortNam s)+++instance Pretty Relevance where+    pretty (Relevance 0) = mempty+    pretty (Relevance r) = superscriptPretty r++instance Pretty Sort where+    pretty s = "∗" <> prettySortNam s  -- ⋆★*∗+    +prettySortNam s = prettyLev s <> prettyRel s++prettyRel (Sort _ r) = pretty r++prettyLev (Sort 0 _) = mempty+prettyLev (Sort l _) = subscriptPretty l++instance Num Sort where+    Sort l1 r1 + Sort l2 r2 = Sort (l1 + l2) (r1 + r2)+    negate (Sort l r) = Sort (negate l) (negate r)++above (Sort l r) = Sort (l + 1) r+oneLev = Sort 1 0++oneRel = Sort 0 1+next :: Relevance -> Relevance+next = (+ 1)++zero = Sort 0 0 ++(+.) :: Relevance -> Sort -> Relevance+r +. (Sort _ r') = r + r'
+ Display.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE PackageImports, GADTs, KindSignatures, StandaloneDeriving, EmptyDataDecls, FlexibleInstances, OverloadedStrings #-}++module Display (Pretty(..), Doc, ($$), (<+>), text, hang, vcat, parensIf, sep, comma, nest, parens,+                subscriptPretty, superscriptPretty, subscriptShow, render) where++import GHC.Exts( IsString(..) )++import Prelude hiding (length, reverse)+import Text.PrettyPrint.HughesPJ +import Numeric (showIntAtBase)+import Control.Arrow (second)+import "monads-fd" Control.Monad.Error+import Data.Monoid+import Data.Sequence hiding (empty)+import Data.Foldable++instance Monoid Doc where+    mempty = empty+    mappend = (<>)++class Pretty a where+    pretty :: a -> Doc++instance Pretty x => Pretty [x] where+    pretty x = brackets $ sep $ punctuate comma (map pretty x)++instance IsString Doc where+    fromString = text++instance Pretty Int where+  pretty = int++instance Pretty Bool where+  pretty = text . show++scriptPretty :: String -> Int -> Doc+scriptPretty s = text . scriptShow s++scriptShow (minus:digits) x = if  x < 0 then minus : sho (negate x) else sho x+  where sho x = showIntAtBase 10 (\i -> digits !! i) x []++superscriptPretty = scriptPretty "⁻⁰¹²³⁴⁵⁶⁷⁸⁹"+subscriptPretty   = scriptPretty "-₀₁₂₃₄₅₆₇₈₉"++subscriptShow :: Int -> String+subscriptShow     = scriptShow "-₀₁₂₃₄₅₆₇₈₉"++++parensIf :: Bool -> Doc -> Doc+parensIf True  = parens+parensIf False = id++
+ LICENSE view
@@ -0,0 +1,56 @@+THE WORK (AS DEFINED BELOW) IS PROVIDED UNDER THE TERMS OF THIS CREATIVE COMMONS PUBLIC LICENSE ("CCPL" OR "LICENSE"). THE WORK IS PROTECTED BY COPYRIGHT AND/OR OTHER APPLICABLE LAW. ANY USE OF THE WORK OTHER THAN AS AUTHORIZED UNDER THIS LICENSE OR COPYRIGHT LAW IS PROHIBITED.++BY EXERCISING ANY RIGHTS TO THE WORK PROVIDED HERE, YOU ACCEPT AND AGREE TO BE BOUND BY THE TERMS OF THIS LICENSE. TO THE EXTENT THIS LICENSE MAY BE CONSIDERED TO BE A CONTRACT, THE LICENSOR GRANTS YOU THE RIGHTS CONTAINED HERE IN CONSIDERATION OF YOUR ACCEPTANCE OF SUCH TERMS AND CONDITIONS.++1. Definitions++"Adaptation" means a work based upon the Work, or upon the Work and other pre-existing works, such as a translation, adaptation, derivative work, arrangement of music or other alterations of a literary or artistic work, or phonogram or performance and includes cinematographic adaptations or any other form in which the Work may be recast, transformed, or adapted including in any form recognizably derived from the original, except that a work that constitutes a Collection will not be considered an Adaptation for the purpose of this License. For the avoidance of doubt, where the Work is a musical work, performance or phonogram, the synchronization of the Work in timed-relation with a moving image ("synching") will be considered an Adaptation for the purpose of this License.+"Collection" means a collection of literary or artistic works, such as encyclopedias and anthologies, or performances, phonograms or broadcasts, or other works or subject matter other than works listed in Section 1(f) below, which, by reason of the selection and arrangement of their contents, constitute intellectual creations, in which the Work is included in its entirety in unmodified form along with one or more other contributions, each constituting separate and independent works in themselves, which together are assembled into a collective whole. A work that constitutes a Collection will not be considered an Adaptation (as defined below) for the purposes of this License.+"Creative Commons Compatible License" means a license that is listed at http://creativecommons.org/compatiblelicenses that has been approved by Creative Commons as being essentially equivalent to this License, including, at a minimum, because that license: (i) contains terms that have the same purpose, meaning and effect as the License Elements of this License; and, (ii) explicitly permits the relicensing of adaptations of works made available under that license under this License or a Creative Commons jurisdiction license with the same License Elements as this License.+"Distribute" means to make available to the public the original and copies of the Work or Adaptation, as appropriate, through sale or other transfer of ownership.+"License Elements" means the following high-level license attributes as selected by Licensor and indicated in the title of this License: Attribution, ShareAlike.+"Licensor" means the individual, individuals, entity or entities that offer(s) the Work under the terms of this License.+"Original Author" means, in the case of a literary or artistic work, the individual, individuals, entity or entities who created the Work or if no individual or entity can be identified, the publisher; and in addition (i) in the case of a performance the actors, singers, musicians, dancers, and other persons who act, sing, deliver, declaim, play in, interpret or otherwise perform literary or artistic works or expressions of folklore; (ii) in the case of a phonogram the producer being the person or legal entity who first fixes the sounds of a performance or other sounds; and, (iii) in the case of broadcasts, the organization that transmits the broadcast.+"Work" means the literary and/or artistic work offered under the terms of this License including without limitation any production in the literary, scientific and artistic domain, whatever may be the mode or form of its expression including digital form, such as a book, pamphlet and other writing; a lecture, address, sermon or other work of the same nature; a dramatic or dramatico-musical work; a choreographic work or entertainment in dumb show; a musical composition with or without words; a cinematographic work to which are assimilated works expressed by a process analogous to cinematography; a work of drawing, painting, architecture, sculpture, engraving or lithography; a photographic work to which are assimilated works expressed by a process analogous to photography; a work of applied art; an illustration, map, plan, sketch or three-dimensional work relative to geography, topography, architecture or science; a performance; a broadcast; a phonogram; a compilation of data to the extent it is protected as a copyrightable work; or a work performed by a variety or circus performer to the extent it is not otherwise considered a literary or artistic work.+"You" means an individual or entity exercising rights under this License who has not previously violated the terms of this License with respect to the Work, or who has received express permission from the Licensor to exercise rights under this License despite a previous violation.+"Publicly Perform" means to perform public recitations of the Work and to communicate to the public those public recitations, by any means or process, including by wire or wireless means or public digital performances; to make available to the public Works in such a way that members of the public may access these Works from a place and at a place individually chosen by them; to perform the Work to the public by any means or process and the communication to the public of the performances of the Work, including by public digital performance; to broadcast and rebroadcast the Work by any means including signs, sounds or images.+"Reproduce" means to make copies of the Work by any means including without limitation by sound or visual recordings and the right of fixation and reproducing fixations of the Work, including storage of a protected performance or phonogram in digital form or other electronic medium.+2. Fair Dealing Rights. Nothing in this License is intended to reduce, limit, or restrict any uses free from copyright or rights arising from limitations or exceptions that are provided for in connection with the copyright protection under copyright law or other applicable laws.++3. License Grant. Subject to the terms and conditions of this License, Licensor hereby grants You a worldwide, royalty-free, non-exclusive, perpetual (for the duration of the applicable copyright) license to exercise the rights in the Work as stated below:++to Reproduce the Work, to incorporate the Work into one or more Collections, and to Reproduce the Work as incorporated in the Collections;+to create and Reproduce Adaptations provided that any such Adaptation, including any translation in any medium, takes reasonable steps to clearly label, demarcate or otherwise identify that changes were made to the original Work. For example, a translation could be marked "The original work was translated from English to Spanish," or a modification could indicate "The original work has been modified.";+to Distribute and Publicly Perform the Work including as incorporated in Collections; and,+to Distribute and Publicly Perform Adaptations.+For the avoidance of doubt:++Non-waivable Compulsory License Schemes. In those jurisdictions in which the right to collect royalties through any statutory or compulsory licensing scheme cannot be waived, the Licensor reserves the exclusive right to collect such royalties for any exercise by You of the rights granted under this License;+Waivable Compulsory License Schemes. In those jurisdictions in which the right to collect royalties through any statutory or compulsory licensing scheme can be waived, the Licensor waives the exclusive right to collect such royalties for any exercise by You of the rights granted under this License; and,+Voluntary License Schemes. The Licensor waives the right to collect royalties, whether individually or, in the event that the Licensor is a member of a collecting society that administers voluntary licensing schemes, via that society, from any exercise by You of the rights granted under this License.+The above rights may be exercised in all media and formats whether now known or hereafter devised. The above rights include the right to make such modifications as are technically necessary to exercise the rights in other media and formats. Subject to Section 8(f), all rights not expressly granted by Licensor are hereby reserved.++4. Restrictions. The license granted in Section 3 above is expressly made subject to and limited by the following restrictions:++You may Distribute or Publicly Perform the Work only under the terms of this License. You must include a copy of, or the Uniform Resource Identifier (URI) for, this License with every copy of the Work You Distribute or Publicly Perform. You may not offer or impose any terms on the Work that restrict the terms of this License or the ability of the recipient of the Work to exercise the rights granted to that recipient under the terms of the License. You may not sublicense the Work. You must keep intact all notices that refer to this License and to the disclaimer of warranties with every copy of the Work You Distribute or Publicly Perform. When You Distribute or Publicly Perform the Work, You may not impose any effective technological measures on the Work that restrict the ability of a recipient of the Work from You to exercise the rights granted to that recipient under the terms of the License. This Section 4(a) applies to the Work as incorporated in a Collection, but this does not require the Collection apart from the Work itself to be made subject to the terms of this License. If You create a Collection, upon notice from any Licensor You must, to the extent practicable, remove from the Collection any credit as required by Section 4(c), as requested. If You create an Adaptation, upon notice from any Licensor You must, to the extent practicable, remove from the Adaptation any credit as required by Section 4(c), as requested.+You may Distribute or Publicly Perform an Adaptation only under the terms of: (i) this License; (ii) a later version of this License with the same License Elements as this License; (iii) a Creative Commons jurisdiction license (either this or a later license version) that contains the same License Elements as this License (e.g., Attribution-ShareAlike 3.0 US)); (iv) a Creative Commons Compatible License. If you license the Adaptation under one of the licenses mentioned in (iv), you must comply with the terms of that license. If you license the Adaptation under the terms of any of the licenses mentioned in (i), (ii) or (iii) (the "Applicable License"), you must comply with the terms of the Applicable License generally and the following provisions: (I) You must include a copy of, or the URI for, the Applicable License with every copy of each Adaptation You Distribute or Publicly Perform; (II) You may not offer or impose any terms on the Adaptation that restrict the terms of the Applicable License or the ability of the recipient of the Adaptation to exercise the rights granted to that recipient under the terms of the Applicable License; (III) You must keep intact all notices that refer to the Applicable License and to the disclaimer of warranties with every copy of the Work as included in the Adaptation You Distribute or Publicly Perform; (IV) when You Distribute or Publicly Perform the Adaptation, You may not impose any effective technological measures on the Adaptation that restrict the ability of a recipient of the Adaptation from You to exercise the rights granted to that recipient under the terms of the Applicable License. This Section 4(b) applies to the Adaptation as incorporated in a Collection, but this does not require the Collection apart from the Adaptation itself to be made subject to the terms of the Applicable License.+If You Distribute, or Publicly Perform the Work or any Adaptations or Collections, You must, unless a request has been made pursuant to Section 4(a), keep intact all copyright notices for the Work and provide, reasonable to the medium or means You are utilizing: (i) the name of the Original Author (or pseudonym, if applicable) if supplied, and/or if the Original Author and/or Licensor designate another party or parties (e.g., a sponsor institute, publishing entity, journal) for attribution ("Attribution Parties") in Licensor's copyright notice, terms of service or by other reasonable means, the name of such party or parties; (ii) the title of the Work if supplied; (iii) to the extent reasonably practicable, the URI, if any, that Licensor specifies to be associated with the Work, unless such URI does not refer to the copyright notice or licensing information for the Work; and (iv) , consistent with Ssection 3(b), in the case of an Adaptation, a credit identifying the use of the Work in the Adaptation (e.g., "French translation of the Work by Original Author," or "Screenplay based on original Work by Original Author"). The credit required by this Section 4(c) may be implemented in any reasonable manner; provided, however, that in the case of a Adaptation or Collection, at a minimum such credit will appear, if a credit for all contributing authors of the Adaptation or Collection appears, then as part of these credits and in a manner at least as prominent as the credits for the other contributing authors. For the avoidance of doubt, You may only use the credit required by this Section for the purpose of attribution in the manner set out above and, by exercising Your rights under this License, You may not implicitly or explicitly assert or imply any connection with, sponsorship or endorsement by the Original Author, Licensor and/or Attribution Parties, as appropriate, of You or Your use of the Work, without the separate, express prior written permission of the Original Author, Licensor and/or Attribution Parties.+Except as otherwise agreed in writing by the Licensor or as may be otherwise permitted by applicable law, if You Reproduce, Distribute or Publicly Perform the Work either by itself or as part of any Adaptations or Collections, You must not distort, mutilate, modify or take other derogatory action in relation to the Work which would be prejudicial to the Original Author's honor or reputation. Licensor agrees that in those jurisdictions (e.g. Japan), in which any exercise of the right granted in Section 3(b) of this License (the right to make Adaptations) would be deemed to be a distortion, mutilation, modification or other derogatory action prejudicial to the Original Author's honor and reputation, the Licensor will waive or not assert, as appropriate, this Section, to the fullest extent permitted by the applicable national law, to enable You to reasonably exercise Your right under Section 3(b) of this License (right to make Adaptations) but not otherwise.+5. Representations, Warranties and Disclaimer++UNLESS OTHERWISE MUTUALLY AGREED TO BY THE PARTIES IN WRITING, LICENSOR OFFERS THE WORK AS-IS AND MAKES NO REPRESENTATIONS OR WARRANTIES OF ANY KIND CONCERNING THE WORK, EXPRESS, IMPLIED, STATUTORY OR OTHERWISE, INCLUDING, WITHOUT LIMITATION, WARRANTIES OF TITLE, MERCHANTIBILITY, FITNESS FOR A PARTICULAR PURPOSE, NONINFRINGEMENT, OR THE ABSENCE OF LATENT OR OTHER DEFECTS, ACCURACY, OR THE PRESENCE OF ABSENCE OF ERRORS, WHETHER OR NOT DISCOVERABLE. SOME JURISDICTIONS DO NOT ALLOW THE EXCLUSION OF IMPLIED WARRANTIES, SO SUCH EXCLUSION MAY NOT APPLY TO YOU.++6. Limitation on Liability. EXCEPT TO THE EXTENT REQUIRED BY APPLICABLE LAW, IN NO EVENT WILL LICENSOR BE LIABLE TO YOU ON ANY LEGAL THEORY FOR ANY SPECIAL, INCIDENTAL, CONSEQUENTIAL, PUNITIVE OR EXEMPLARY DAMAGES ARISING OUT OF THIS LICENSE OR THE USE OF THE WORK, EVEN IF LICENSOR HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES.++7. Termination++This License and the rights granted hereunder will terminate automatically upon any breach by You of the terms of this License. Individuals or entities who have received Adaptations or Collections from You under this License, however, will not have their licenses terminated provided such individuals or entities remain in full compliance with those licenses. Sections 1, 2, 5, 6, 7, and 8 will survive any termination of this License.+Subject to the above terms and conditions, the license granted here is perpetual (for the duration of the applicable copyright in the Work). Notwithstanding the above, Licensor reserves the right to release the Work under different license terms or to stop distributing the Work at any time; provided, however that any such election will not serve to withdraw this License (or any other license that has been, or is required to be, granted under the terms of this License), and this License will continue in full force and effect unless terminated as stated above.+8. Miscellaneous++Each time You Distribute or Publicly Perform the Work or a Collection, the Licensor offers to the recipient a license to the Work on the same terms and conditions as the license granted to You under this License.+Each time You Distribute or Publicly Perform an Adaptation, Licensor offers to the recipient a license to the original Work on the same terms and conditions as the license granted to You under this License.+If any provision of this License is invalid or unenforceable under applicable law, it shall not affect the validity or enforceability of the remainder of the terms of this License, and without further action by the parties to this agreement, such provision shall be reformed to the minimum extent necessary to make such provision valid and enforceable.+No term or provision of this License shall be deemed waived and no breach consented to unless such waiver or consent shall be in writing and signed by the party to be charged with such waiver or consent.+This License constitutes the entire agreement between the parties with respect to the Work licensed here. There are no understandings, agreements or representations with respect to the Work not specified here. Licensor shall not be bound by any additional provisions that may appear in any communication from You. This License may not be modified without the mutual written agreement of the Licensor and You.+The rights granted under, and the subject matter referenced, in this License were drafted utilizing the terminology of the Berne Convention for the Protection of Literary and Artistic Works (as amended on September 28, 1979), the Rome Convention of 1961, the WIPO Copyright Treaty of 1996, the WIPO Performances and Phonograms Treaty of 1996 and the Universal Copyright Convention (as revised on July 24, 1971). These rights and subject matter take effect in the relevant jurisdiction in which the License terms are sought to be enforced according to the corresponding provisions of the implementation of those treaty provisions in the applicable national law. If the standard suite of rights granted under applicable copyright law includes additional rights not granted under this License, such additional rights are deemed to be included in the License; this License is not intended to restrict the license of any rights under applicable law.
+ Main.hs view
@@ -0,0 +1,91 @@+module Main where+++import System.IO ( stdin, hGetContents )+import System.Environment ( getArgs )+import Options +import qualified Normal++{-+import LexSyntax+import ParSyntax+import SkelSyntax+import PrintSyntax+-}++import RawSyntax+import AbsSynToTerm+import TypeCheckerNF+import Basics+import Terms+import Display+import Text.PrettyPrint.HughesPJ (render)+import qualified Data.Sequence as S+++import Language.LBNF(Err(..))++-- type ParseFun a = [Token] -> Err a++myLLexer = myLexer++type Verbosity = Int++putStrV :: Verbosity -> Doc -> IO ()+putStrV v s = if verb options >= v then putStrLn (render s) else return ()++runFile f = do+  putStrV 1 $ "Processing file:" <+> text f+  contents <- readFile f+  run contents f++instance Pretty Token where+    pretty = text . show++run s fname = let ts = myLLexer s in case pExp ts of+   Bad err -> do +     putStrLn "Parse Failed."+     putStrV 1 $ "Tokens:" <+> pretty ts+     putStrLn $ fname ++ ":" ++ err+   Ok tree -> do +     process fname tree++process fname modul = do+  let resolved = runResolver $ resolveTerm modul+  -- putStrV 2 $ "\n[Abstract Syntax]\n\n" ++ show tree+  -- putStrV 2 $ "\n[Linearized tree]\n\n" ++ printTree tree+  putStrV 2 $ "[Resolved into]" $$ pretty resolved+  let (checked,info) = runChecker $ iType mempty resolved+  case info of+    [] -> return ()+    _ -> putStrV 0 $ vcat info -- display constraints, etc.+  case checked of+    Right (a,b,_o) -> do +       putStrV 0 $ "nf =" <+> pretty a+       putStrV 0 $ "ty =" <+> pretty b+{-+       case b of +         (Pi i s t) -> do+           putStrV v $ "s ∈ ⟦S⟧ =" <+> prettyTerm (S.singleton i) (zerInRel s)+           putStrV v $ "T =" <+> prettyTerm (S.singleton i) t+         _ -> putStrV v "not a function!"+-}+       putStrLn "Done!"+    Left (e,err) -> let Irr (line,col) = termPosition e +                    in putStrV 0 (text fname <> ":" <> pretty line <> ":" <> pretty (col - 1) <> ":" <+> err)+      +{-+showTree tree+ = do+      putStrV 2 $ "\n[Abstract Syntax]\n\n" ++ show tree+      putStrV 2 $ "\n[Linearized tree]\n\n" ++ printTree tree+-}++main :: IO ()+main = do +  mapM_ runFile (files options)+++++
+ Normal.hs view
@@ -0,0 +1,375 @@+{-# LANGUAGE GADTs, KindSignatures, OverloadedStrings, EmptyDataDecls, StandaloneDeriving, TypeSynonymInstances, TypeFamilies, MultiParamTypeClasses #-}+module Normal where++import Prelude hiding (length,elem,foldl)+import Basics+import Display+import Data.Foldable+import Control.Arrow (first, second)+import Data.Sequence hiding (zip,replicate,reverse)+import Options++data No+data Ne+data Va++type NF = Term No+type Neutral = Term Ne+type Variable = Term Va+type NF' = (NF, NF) -- value, type.++data Term n :: * where+     Neu :: Neutral -> NF+     Var :: Variable -> Neutral+     +     Star :: Sort -> NF     +     +     -- FIXME: only "column" / relevance should be here.+     Pi  :: Relevance -> Ident -> NF -> NF -> NF+     Lam :: Relevance -> Ident -> NF -> NF -> NF +     App :: Relevance -> Neutral -> NF -> Neutral -- The sort is that of the argument.+     +     Sigma :: Relevance -> Ident -> NF -> NF -> NF+     Pair  :: Relevance -> Ident -> NF -> NF -> NF  -- Pair does not bind any variable.+     Proj  :: Relevance -> -- ^ Sort of the argument+              Neutral -> Bool -> -- ^ True for 1st projection; False for 2nd.+              Irr String -> Neutral +     +     +     OfParam :: Ident -> NF -> Neutral++     Destr :: Relevance -> Variable -> Variable -- argument: level destroyed+     Param :: Relevance -> Variable -> Variable +     V :: Sort -> Int -> Variable -- shift, deBruijn +     Hole :: String -> Variable++type Subst = [NF]++deriving instance Eq (Term n)++var :: Int -> NF+var x = Neu $ var' x++var' x = Var $ V (Sort 0 0) x+++-- | Hereditary substitution+subst0 :: NF -> NF -> NF+subst0 u = subst (u:map (var) [0..])  +++subst :: Subst -> Term n -> NF+subst f t = case t of+  Neu x -> s x+  Var x -> s x+  +  Star x -> Star x+  +  Lam o i ty bo -> Lam o i (s ty) (s' bo)+  (Pair o i x y) -> Pair o i (s x) (s y)+  Pi o i a b -> Pi o i (s a) (s' b)+  Sigma o i a b -> Sigma o i (s a) (s' b)+  (App o a b) -> app o (s a) (s b)+  (Proj o x k f) -> proj o (s x) k f++  OfParam i x -> Neu (OfParam i (s x))+  +  Hole x -> Neu $ Var $ Hole x+  V s x -> shift s (f !! x)+  Param o x -> param o (s x)+  Destr f x -> destroy f (s x)+ where s' = subst (var 0 : map wk f)+       s  = subst f++-- Double renaming substitution+-- 1st component: regular; 2nd component: param+subst' :: [(Variable,Variable)] -> Term n -> Term n+subst' f t = case t of+  Neu x -> Neu (s x)+  Var x -> Var (s x)+  +  Star x -> Star x+  +  Lam o i ty bo -> Lam o i (s ty) (s' o bo)+  (Pair o i x y) -> Pair o i (s x) (s y)+  Pi o i a b -> Pi o i (s a) (s' o b)+  Sigma o i a b -> Sigma o i (s a) (s' o  b)+  (App o a b) -> App o (s a) (s b)+  (Proj o x k f) -> Proj o (s x) k f++  OfParam i x -> OfParam i (s x)+  +  Hole x -> Hole x+  V s x -> shift s (fst $ f !! x)+  Param o (V s x) -> shift s (snd $ f !! x)+  Param o x -> Param o (s x)+  Destr f x -> Destr f (s x)+ where s' o = subst' (p o f)+       s  = subst' f+       p o xs = (V zero 0, Param o $ V zero 0) : map (both $ wkv 1) xs+       +both f (x,y) = (f x, f y)++shift' :: Int -> Sort -> Term n -> Term n+shift' n d@(Sort _ r) t = case t of+  Neu x -> Neu $ s x+  Var x -> Var (s x)+  +  Star o -> Star (o + d)+  +  Lam o i ty bo -> Lam (o +. d) i (s ty) (s' bo)+  (Pair o i x y) -> Pair (o +. d) i (s x) (s y)+  Pi o i a b -> Pi (o +. d) i (s a) (s' b)+  Sigma o i a b -> Sigma (o +. d) i (s a) (s' b)+  (App o a b) -> App (o +. d) (s a) (s b)+  (Proj o x k f) -> Proj (o +. d) (s x) k f+  +  OfParam i x -> OfParam i (s x)++  Hole x -> Hole x+  Param o x -> Param (o +. d) (s x)+  Destr f x -> Destr (f + r) (s x)+  V s x | x < n  -> V s x+        | x >= n -> V (s + d) x+ where s = shift' n d+       s' = shift' (1 + n) d++shift = shift' 0++-----------------------------+-- Hereditary operations+  +app :: Relevance -> NF -> NF -> NF +app _ (Lam _ i _ bo) u = subst0 u bo+app o (Neu n)      u = Neu (App o n u)++proj :: Relevance -> NF -> Bool -> Irr String -> NF+proj _ (Pair _ _ x y) True f = x+proj _ (Pair _ _ x y) False f = y+proj o (Neu x) k f = Neu (Proj o x k f)+++wkn :: Int -> NF -> NF+wkn n = subst (map var [n..])+wk = wkn 1+str = subst0 (Neu $ Var $ Hole "str: oops!")++wkv :: Int -> Variable -> Variable+wkv n (Destr d x) = Destr d (wkv n x)+wkv n (Param o x) = Param o (wkv n x)+wkv n (V s x) = V s (x + n)+wkv n (Hole x) = Hole x++param :: Relevance -> NF -> NF+param o t = transNF 0 t o+++-----------------------------------+-- Display++dec xs = [ x - 1 | x <- xs, x > 0]++freeVars :: Term n -> [Int]+freeVars (Var x) = freeVars x+freeVars (Neu x) = freeVars x+freeVars (Pi _ _ a b) = freeVars a <> (dec $ freeVars b)+freeVars (Sigma _ _ a b) = freeVars a <> (dec $ freeVars b)+freeVars (V _ x) = [x]+freeVars (App _ a b) = freeVars a <> freeVars b+freeVars (Lam _ _ ty b) = freeVars ty <> (dec $ freeVars b)+freeVars (Star _) = mempty+freeVars (Hole _) = mempty+freeVars (Pair _ _ x y) = freeVars x <> freeVars y+freeVars (Proj _ x _ _) = freeVars x+freeVars (Param _ x) = freeVars x+freeVars (OfParam _ x) = freeVars x+freeVars (Destr _ x) = freeVars x++iOccursIn :: Int -> Term n -> Bool+iOccursIn x t = x `elem` (freeVars t)++prettyRel' = prettySortNam++cPrint :: Int -> DisplayContext -> Term n -> Doc+cPrint p ii (Var x) = cPrint p ii x+cPrint p ii (Neu x) = cPrint p ii x+cPrint p ii (Destr i x) = cPrint p ii x <> "%" <> pretty i+cPrint p ii (Param o x) = cPrint p ii x <> sss (pretty o) <> "!"+cPrint p ii (OfParam i x) = pretty i+                             -- "⌊" <> cPrint (-1) ii x <> "⌋"+cPrint p ii (Hole x) = text x+cPrint p ii (Star i) = pretty i+cPrint p ii (V s k) +  | k < 0 || k >= length ii  = text "<deBrujn index" <+> pretty k <+> text "out of range>"+  | otherwise = pretty (ii `index` k)  <> shft+  where shft | s == Sort 0 0 = mempty+             | otherwise = "⇧" <> prettySortNam s+cPrint p ii (Proj o x k (Irr f))     = cPrint p ii x <> sss (pretty o) <> (if k then "#" else "/") <> text f+cPrint p ii t@(App _ _ _)     = let (fct,args) = nestedApp t in +                                 parensIf (p > 3) (cPrint 3 ii fct <+> sep [ sss (pretty o <> "· ") <> cPrint 4 ii a | (o,a) <- args]) +cPrint p ii t@(Pi _ _ _ _)    = parensIf (p > 1) (printBinders "→" ii mempty $ nestedPis t)+cPrint p ii t@(Sigma _ _ _ _) = parensIf (p > 1) (printBinders "×" ii mempty $ nestedSigmas t)+cPrint p ii (t@(Lam _ _ _ _))   = parensIf (p > 1) (nestedLams ii mempty t)+cPrint p ii (Pair _ name x y) = parensIf (p > (-1)) (sep [pretty name <+> text "=" <+> cPrint 0 ii x <> comma,+                                                          cPrint (-1) ii y])++nestedPis  :: NF -> ([(Ident,Bool,NF,Relevance)], NF)+nestedPis (Pi o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedPis b)+nestedPis x = ([],x)++nestedSigmas  :: NF -> ([(Ident,Bool,NF,Relevance)], NF)+nestedSigmas (Sigma o i a b) = (first ([(i,0 `iOccursIn` b,a,o)] ++)) (nestedSigmas b)+nestedSigmas x = ([],x)++printBinders :: Doc -> DisplayContext -> Seq Doc -> ([(Ident,Bool,NF,Relevance)], NF) -> Doc+printBinders sep ii xs (((i,occurs,a,o):pis),b) = printBinders sep (i <| ii) (xs |> (printBind' ii i occurs a o <+> sep)) (pis,b)+printBinders _ ii xs ([],b)                 = sep $ toList $ (xs |> cPrint 1 ii b) +++nestedLams :: DisplayContext -> Seq Doc -> Term n -> Doc+nestedLams ii xs (Lam o x ty c) = nestedLams (x <| ii) (xs |> parens (sss (pretty o) <> pretty x <+> ":" <+> cPrint 0 ii ty)) c+nestedLams ii xs t         = (text "\\ " <> (sep $ toList $ (xs |> "->")) <+> nest 3 (cPrint 0 ii t))++printBind' ii name occurs d o = case not (isDummyId name) ||  occurs of+                  True -> parens (sss (pretty o) <> pretty name <+> text ":" <+> cPrint 0 ii d)+                  False -> cPrint 2 ii d++nestedApp :: Neutral -> (Neutral,[(Relevance, NF)])+nestedApp (App o f a) = (second (++ [(o,a)])) (nestedApp f)+nestedApp t = (t,[])++sss x = if showSorts options then x else mempty++prettyTerm = cPrint (-100)+++instance Pretty (Term n) where+    pretty = prettyTerm mempty+++mv :: Int -> Int -> Int+mv d x | x < d     = (arity + 1) * x + idx+       | otherwise = (x - d) + (arity + 1) * d+                     -- x + arity * d++mv' :: Int -> Int -> (Variable, Variable)+mv' d x | x < d     = let v = (arity + 1) * x +                      in (V zero $ v + idx, V zero v)+        | otherwise = let v = V zero $ (x - d) + (arity + 1) * d +                      in (v, Hole "does not appear!")+                          -- Param evil v)++evil = Sort 0 666+++renam :: Int -> Int -> NF -> NF+renam d idx = subst [var $ mv d $ x | x <- [0..]] . shift' d oneRel++renam' d = subst' (map (mv' d) [0..])++re :: Ident -> Ident+re (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,x++"₁")))++arity, idx :: Int+arity = 1+idx = 1+++-- | Transform a term to its relational interpretation+-- NOTE: the level of the sort is incorrect! In fact only the rel. ever matters. (Destroy)+transV :: Int -> Variable -> Relevance -> Variable++transV d (V o x) o' | x < d =                V o $ (arity + 1) * x+                    | otherwise = Param o' $ V o $ (x - d) + (arity + 1) * d+transV d (Param o' x) o = Param o' $ transV d x o+transV d (Destr n x) o = destroy n (transV d x o)+transV d (Hole s) _ = Hole (s ++ "!")++transNe :: Int -> Neutral -> Relevance -> NF+transNe d (Var v) o = Neu $ Var $ transV d v o+transNe d (App o f a) o' = app o (app (next o) (transNe d f o') (renam d idx a)) (transNF d a o) +transNe d (Proj o x k f) o' = proj o (transNe d x o) k f+transNe d (OfParam i t) o = app o (renam' d t) (renam d idx (Neu $ OfParam i t))++transNF :: Int -> NF -> Relevance -> NF+transNF d (Neu v) o = transNe d v o+transNF d (Lam o i ty bo) o' = transBind d Lam o i ty (transNF (d+1) bo o')+transNF d (Pair o i x y) o' = Pair o i (transNF d x o) (transNF d y o') +transNF d ty@(Star  _) o = trans' d ty o+transNF d ty@(Pi    _ _ _ _) o = trans' d  ty o+transNF d ty@(Sigma _ _ _ _) o = trans' d ty o++trans' d ty o = Lam (next o) (synthId "z₁") (renam d idx ty) (zerInRel d ty o)++-- | Build a relation witnessing x ∈ ⟦ty⟧. (where 'x' is Bound 0 in 'ty'.)++-- In the translated context, 'z1', ... 'zn' are bound, but not+-- 'zR'. (we are going to bind it soon).  However, 'inTrans' assumes+-- it has "full" translated context.  So we weaken 'ty' (putting 'z' in scope) and apply the+-- translation as normal.  But the translation is well behaved, so it+-- does not use 'zR'. We substitute it with nothing when the job is+-- done.+zerInRel d ty o = str $ inTrans (d + 1) (wk ty) o (var 0)++-- | Build a relation z ∈ ⟦ty⟧.  z is a term that, after renaming,+-- gives the vector of terms member of the relation.  Note that+-- 'trans' is never applied to 'z', therefore 'zR' never occurs in the result.++inTrans :: Int -> NF -> Relevance -- ^ sort of the 1st argument+           -> NF -> NF+inTrans d (Star  s)       o z = (Pi (next o) dummyId (renam d idx z) (Star s))+inTrans d (Pi    o i a b) o' z = transBind d Pi o i a (inTrans (d + 1) b o' (app o (wk z) (var 0)))+inTrans d (Sigma o i a b) o' z = Sigma o i (inTrans d a o (proj o z True f)) +                             (subst (var 0:wk (renam d idx (proj o z True f)):map var [1..]) $+                              inTrans (1 + d) b o' (proj o (wk z) False f)) -- TEST: is depth ok?+ where (Irr (Identifier (_,nam))) = i+       f = Irr nam+inTrans d t o z = app (next o) (transNF d t o) (renam d idx z) +++-- | Translate a binding (x : A) into (x₁ : A₁) (⟦x⟧ : ⟦A⟧ x₁)+transBind :: Int -> (Relevance -> Ident -> NF -> NF -> NF) -> Relevance -> Ident -> NF -> NF -> NF+transBind d binder o i a rest = binder (next o) (re i) (renam d idx a) $+                                binder o            i  (zerInRel d a o) $ +                                rest+++-- Invariant: the whole term is not destroyed.+destroy :: Relevance -> Term n -> Term n+destroy d t = case t of+  Var x -> Var $ pr x+  Neu x -> Neu $ pr x++  V o x -> V o x+  Hole x -> Hole x+  Destr d' t -> destroy (min d d') t -- coalesce+  Param r x | r+1 == d -> x+            | otherwise -> Destr d $ Param r x ++  (Star o) -> Star o+  (Pi o i a b)    -> mb Pi    o i a b +  (Sigma o i a b) -> mb Sigma o i a b +  (Lam o i ty bo) -> mb Lam   o i ty bo  +  (Pair o i a b) +      | isDestroyed o -> pr b+      | otherwise -> Pair o i (pr a) (pr b) +  (App o a b)  -> case isDestroyed o of+                   True -> pr a+                   False -> App o (pr a) (pr b)+  (Proj o x k f) -> case isDestroyed o of+    True -> pr x -- result of the projection is not destroyed (by+                  -- assumpt.) but the whole pair would be -> we must+                  -- keep the 1st component.+    False -> Proj o (pr x) k f+  (OfParam n x) -> OfParam (modId (++ "%" ++ show d) n) $ pr x+  + where +   isDestroyed o = d `destroys` o+   mb :: (Relevance -> Ident -> NF -> NF -> NF) -> Relevance -> Ident -> NF -> NF -> NF+   mb binder o i a b = case isDestroyed o of+                             True -> str (pr b)+                             False -> binder o i (pr a) (pr b)+   pr x = destroy d x+++r `destroys` r' = r' >= r
+ Options.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE DeriveDataTypeable #-}++module Options (Args(..),TypeSystem(..),options) where++import System.Console.CmdArgs.Implicit+import System.IO.Unsafe++data TypeSystem = CCω+                | Predicative+  deriving (Show, Data, Typeable)++data Args = +  Args {verb :: Int,+        typeSystem :: TypeSystem,+        showSorts :: Bool,+        files :: [String]+        } +  deriving (Show, Data, Typeable)+           +sample = cmdArgsMode $ +         Args { verb = 0 &= help "verbosity" &= opt (0 :: Int),+                typeSystem = enum [Predicative &= name "P" &= help "Agda (Predicative)", +                                   CCω &= name "I" &= help "CCω (Impredicative)"]+                               , -- &= opt (0 :: Int),+                showSorts = False &= help "display sort annotations in normal forms",+                files = [] &= args &= typFile+              }+         +         +options = unsafePerformIO (cmdArgsRun sample)
+ RawSyntax.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE QuasiQuotes #-}++module RawSyntax where++import Language.LBNF++compile [$cf|+++comment "--" ;+comment "{-" "-}" ;++EHole.   Exp6 ::= Hole ;+EVar.    Exp6 ::= AIdent ;+ESet.    Exp6 ::= Sort ;+EParam.  Exp4 ::= Exp4 "!";+EUp.     Exp4 ::= Exp4 "^";+ELeft.   Exp4 ::= Exp4 "<";+EDestr.  Exp4 ::= Exp4 "%" Natural ;+EProj.   Exp4 ::= Exp4 "#" AIdent ;+EExtr.   Exp4 ::= Exp4 "/" AIdent ;+EApp.    Exp3 ::= Exp3 Exp4 ;+EPi.     Exp2  ::= Exp3 Arrow Exp2 ;+ESigma.  Exp2  ::= Exp3 ";" Exp2 ;+EAbs.    Exp2  ::= "\\" [Bind] Arrow Exp2 ;+EAnn.    Exp1 ::= Exp2 ":" Exp1 ;+EPair.   Exp  ::= Decl "," Exp ;++coercions Exp 6 ;++Decl. Decl ::= AIdent "=" Exp1 ;+PDecl. Decl ::= "param" AIdent "=" Exp1 "::" Exp2;+terminator AIdent "" ;+terminator Decl ";" ;++token Arrow  '-' '>' ;++NoBind. Bind   ::= AIdent ; +Bind.   Bind   ::= "(" AIdent ":" Exp ")" ;+AIdent. AIdent ::= Identifier ;+terminator Bind "" ;++token Natural digit+;++position token Identifier ('!'|'['|']'|letter|digit|'-'|'_'|'\'')(('*'|'['|']'|letter|digit|'-'|'_'|'\'')*) ;++position token Hole '?' ((letter|digit|'-'|'_'|'\'')*) ;++position token Sort '*' (digit*) ('@' digit+)?;++|]
+ Setup.hs view
@@ -0,0 +1,4 @@+#!/usr/bin/env runhaskell+import Distribution.Simple+main :: IO ()+main = defaultMain
+ Terms.hs view
@@ -0,0 +1,360 @@+{-# LANGUAGE PackageImports, GADTs, KindSignatures, StandaloneDeriving, EmptyDataDecls, FlexibleInstances, OverloadedStrings #-}++module Terms(Ident, Irr(..), Identifier(..), Sort(..), +             Term(..), +--                 bound, app, proj, +                      prettyTerm,+             Position, dummyPosition, identPosition, termPosition,+             isDummyId, synthId, dummyId, +--             destruction,+            -- wk, wkn, subst0, ssubst+            ) where++import Prelude hiding (length, elem,foldl)+import Basics +import Display+import Data.Sequence hiding (zip,replicate,reverse)+import Control.Arrow (second)+import Data.Foldable++data Term :: * where+     Hole :: Irr Position -> String -> Term -- placeholder+     Star :: Irr Position -> Sort -> Term -- sort+     Bound :: Irr Position -> Int -> Term -- variable+     Pi :: Ident -> Term -> Term -> Term +     Sigma :: Ident -> Term -> Term -> Term+     Lam :: Ident -> Term -> Term -> Term +     Pair :: Ident -> Term -> Term -> Term +     (:$:) :: Term -> Term -> Term+     -- 1st projection.+     Proj :: Term -> String -> Term     +     -- 2nd projection.     FIXME: remove+     Extr :: Term -> String -> Term +     +     -- term such that its relational interpretation is its argument.+     OfParam :: Ident -> Term -> Term +     +     -- Type annotation. Not present in normal forms.+     Ann :: Term -> Term -> Term +     +     -- shift the sorts of the terms. Not present in normal forms.+     Shift :: Sort -> Term -> Term ++     -- relational interpretations and world destruction.  In normal+     -- form, arguments to these are either themselves or a variable.+     Param :: Term -> Term +     Destroy :: Relevance -> Term -> Term++termPosition :: Term -> Irr Position +termPosition (Hole p _) = p+termPosition (Star p _) = p+termPosition (Bound p _) = p+termPosition (Pi i _ _) = identPosition i+termPosition (Sigma i _ _) = identPosition i+termPosition (Lam i _ _) = identPosition i+termPosition (Pair i _ _) = identPosition i+termPosition (x :$: y) = termPosition x+termPosition (Proj x _) = termPosition x+termPosition (Extr x _) = termPosition x+termPosition (Ann x _) = termPosition x+termPosition (Param x) = termPosition x+termPosition (OfParam _ x) = termPosition x+termPosition (Shift _ x) = termPosition x+termPosition (Destroy _ x) = termPosition x++{-+bound = Bound dummyPosition++-- | Hereditary application+-- invariant: preserves normal forms +app :: Term -> Term -> Term +app (Lam i _ bo) u = subst0 u bo+app neutral u = neutral :$: u++subst0 :: Term -> Term -> Term+subst0 u = subst (u:map bound [0..])  ++type Subst = [Term]++++-- | Hereditary substitution+subst :: Subst -> Term -> Term+subst f t = case t of+  Bound _ x -> f !! x+  Lam i ty bo -> Lam i (s ty) (s' bo)+  Pi i a b -> Pi i (s a) (s' b)+  Sigma i a b -> Sigma i (s a) (s' b)+  (a :$: b) -> (s a) `app` (s b)+  (Ann e t) -> Ann (s e) (s t)+  (Pair i x y) -> Pair i (s x) (s' y)+  (Proj x f) -> proj (s x) f+  (Extr x f) -> extr (s x) f+  Hole p x -> Hole p x+  Star p x -> Star p x+  Param arity x -> param0 arity (s x)+  OfParam i x -> OfParam i (s x)+  Shift f x -> ssubst f (s x)+  Destroy i x -> Destroy i (s x) -- need to move to sort annotated terms to do this correctly. +  + where s' = subst (bound 0 : map wk f)+       s  = subst f++-- | Non-hereditary substitution+subst' :: Subst -> Term -> Term+subst' f t = case t of+  Bound _ x -> f !! x+  Lam i ty bo -> Lam i (s ty) (s' bo)+  Pi i a b -> Pi i (s a) (s' b)+  Sigma i a b -> Sigma i (s a) (s' b)+  (a :$: b) -> (s a) `app` (s b)+  (Ann e t) -> Ann (s e) (s t)+  (Pair i x y) -> Pair i (s x) (s' y)+  (Proj x f) -> Proj (s x) f+  (Extr x f) -> Extr (s x) f+  Hole p x -> Hole p x+  Star p x -> Star p x+  Param arity x -> Param arity (s x)+  OfParam i x -> OfParam i (s x)+  Shift f x -> Shift f (s x)+  Destroy i x -> Destroy i (s x)+  + where s' = subst (bound 0 : map wk f)+       s  = subst f+++wkn n = subst' (map bound [n..])+wk = wkn 1+str = subst0 (Hole dummyPosition "oops!")++-- | Hereditary projection+proj (Extr x f')   f | f /= f' = proj x f+proj (Pair (Irr (Identifier (_pos,f'))) x y) f +  | f == f' = x+   | f /= f' = proj (str y) f+proj x f = Proj x f++-- | Hereditary extraction+extr (Pair (Irr (Identifier (_pos,f'))) x y) f | f == f' = str y+extr x f = Extr x f++-}++deriving instance Show (Term)+deriving instance Eq (Term)++dec xs = [ x - 1 | x <- xs, x > 0]++freeVars :: Term -> [Int]+freeVars (Ann a b) = freeVars a <> freeVars b+freeVars (Pi _ a b) = freeVars a <> (dec $ freeVars b)+freeVars (Sigma _ a b) = freeVars a <> (dec $ freeVars b)+freeVars (Bound _ x) = [x]+freeVars (a :$: b) = freeVars a <> freeVars b+freeVars (Lam _ ty b) = freeVars ty <> (dec $ freeVars b)+freeVars (Star _ _) = mempty+freeVars (Hole _ _) = mempty+freeVars (Pair _ x y) = freeVars x <> (dec $ freeVars y)+freeVars (Proj x _) = freeVars x+freeVars (Extr y _) = freeVars y+freeVars (Param x) = freeVars x+freeVars (OfParam _ x) = freeVars x+freeVars (Shift _ x) = freeVars x+freeVars (Destroy _ x) = freeVars x++iOccursIn :: Int -> Term -> Bool+iOccursIn x t = x `elem` (freeVars t)++----------------------------+-- Display++cPrint :: Int -> DisplayContext -> Term -> Doc+cPrint p ii (Destroy i x) = cPrint p ii x <> "%" <> pretty i+cPrint p ii (Shift o x) = cPrint 6 ii x <> "⇧" <> prettySortNam o+cPrint p ii (Param x) = cPrint p ii x <> "!"+cPrint p ii (OfParam i x) = pretty i+                             -- "⌊" <> cPrint (-1) ii x <> "⌋"+cPrint p ii (Hole _ x) = text x+cPrint p ii (Star _ i) = pretty i+cPrint p ii (Bound _ k) +  | k < 0 || k >= length ii  = text "<deBrujn index" <+> pretty k <+> text "out of range>"+  | otherwise = pretty (ii `index` k)+cPrint p ii (Proj x f)     = cPrint p ii x <> "#" <> text f+cPrint p ii (Extr x f)     = cPrint p ii x <> "/" <> text f+cPrint p ii t@(_ :$: _)     = let (fct,args) = nestedApp t in +                                 parensIf (p > 3) (cPrint 3 ii fct <+> sep (map (cPrint 4 ii) args))+cPrint p ii (Pi name d r)    = parensIf (p > 1) (sep [printBind ii name d r <+> text "→", cPrint 1 (name <| ii) r])+cPrint p ii (Sigma name d r) = parensIf (p > 1) (sep [printBind ii name d r <+> text "×",  cPrint 1 (name <| ii) r])+cPrint p ii (t@(Lam _ _ _))   = parensIf (p > 1) (nestedLams ii mempty t)+cPrint p ii (Ann c ty)      = parensIf (p > 0) (cPrint 1 ii c <+> text ":" <+> cPrint 0 ii ty)+cPrint p ii (Pair name (OfParam _ x) y) +                            = parensIf (p > (-1)) (sep ["⟦"<>pretty name<>"⟧" <+> text "=" <+> cPrint 0 ii x <> comma, cPrint (-1) (name <| ii) y])+cPrint p ii (Pair name x y) = parensIf (p > (-1)) (sep [pretty name <+> text "=" <+> cPrint 0 ii x <> comma, cPrint (-1) (name <| ii) y])++nestedLams :: DisplayContext -> Seq Doc -> Term -> Doc+nestedLams ii xs (Lam x (Hole _ _) c) = nestedLams (x <| ii) (xs |> pretty x) c+nestedLams ii xs (Lam x ty c) = nestedLams (x <| ii) (xs |> parens (pretty x <+> ":" <+> cPrint 0 ii ty)) c+nestedLams ii xs t         = (text "\\ " <> (sep $ toList $ xs) <+> text "->" <+> nest 3 (cPrint 0 ii t))++printBind ii name d r = case not (isDummyId name) ||  0 `iOccursIn` r of+                  True -> parens (pretty name <+> text ":" <+> cPrint 0 ii d)+                  False -> cPrint 2 ii d++nestedApp :: Term -> (Term,[Term])+nestedApp (f :$: a) = (second (++ [a])) (nestedApp f)+nestedApp t = (t,[])++prettyTerm = cPrint (-100)++instance Pretty Term where+    pretty = prettyTerm mempty++{-+---------------------------------------------------------------+-- Sort substitution++ssubst :: Sort -> Term -> Term+ssubst f t = case t of+  Bound p x -> Shift f (Bound p x)+  Lam i ty bo -> Lam i (s ty) (s bo)+  Pi i a b -> Pi i (s a) (s b)+  Sigma i a b -> Sigma i (s a) (s b)+  (a :$: b) -> (s a) :$: (s b)+  (Ann e t) -> Ann (s e) (s t)+  (Pair i x y) -> Pair i (s x) (s y)+  (Proj x f) -> Proj (s x) f+  (Extr x f) -> Extr (s x) f+  Hole p x -> Hole p x+  Star p x -> Star p (f + x)+  Param arity x -> Param arity (s x)+  OfParam i x -> OfParam (modId (++ show f) i) (s x)  +  Shift f' x -> ssubst (f + f') x+  Destroy f x -> Destroy f (s x)+ where s = ssubst f++---------------------------------------------------------------+-- Hereditary parametricity transform++type Env = [Subst]++renam :: Env -> Int -> Term -> Term+renam g idx a = ssubst nextRel $ subst (g !! idx) a++re :: Int -> Ident -> Ident+re idx = modId (++ subscriptShow idx)++param0 arity = param arity (map (Param arity . bound) [0..] : replicate arity (map bound [0..]))++-- | Transform a term to its relational interpretation+param :: Int -> Env -> Term -> Term+param arity = paramProg+  where+  extCtx gs = [bound idx:map (wkn (arity + 1)) g | (idx,g) <- zip (0:reverse [1..arity]) gs]+    +  paramProg :: Env -> Term -> Term+  paramProg g (Shift f x) = Shift f (paramProg g x) +  paramProg g (Destroy f x) = Param arity (Destroy f x)+  paramProg g (Hole p s) = Hole p ("[" ++ s ++ "]")+  paramProg g (Bound p x) = g !! 0 !! x+  paramProg g (Lam i ty bo) = paramBind g Lam  i ty $+                          paramProg (extCtx g) bo+    +  paramProg g (Pair i x y) = +     Pair i (paramProg g x) +            (paramProg (map (\d -> Hole dummyPosition "pair not in nf!":map wk d) g) y)+     -- because the input is in normal form, the variable bound by the+     -- pair can never appear in y.+  paramProg g (f :$: a) = foldl app (paramProg g f) [renam g idx a | idx <- [1..arity]] `app` paramProg g a+  paramProg g (Proj e f) = proj (paramProg g e) f+  paramProg g (Extr e f) = extr (paramProg g e) f+  paramProg g (Ann _ _) = error "Ann should not be in nf term"+  paramProg g (OfParam i x) = case arity of+      0 -> OfParam (modId (\x -> "⌈" ++ x ++ "⌉") i) (paramProg g x)                                +      1 -> x `app` ssubst nextRel (OfParam i x) +      _ -> error "mismatch in arity not yet supported"+  paramProg g x@(Param _ _) = Param arity x -- FIXME: here the renaming substitution should be applied;+                              -- but applying the current substitution has the effect of swapping the params.+  paramProg g ty = appl [Lam (synthId $ "z" ++ subscriptShow i) (wkn (i-1) $ renam g i ty) | i <- [1..arity] ] (zerInRel g ty)++  appl :: [a -> a] -> a -> a+  appl []     x = x+  appl (f:fs) x = f (appl fs x)++  -- | Build a relation witnessing x ∈ ⟦ty⟧. (where 'x' is not bound in 'ty'.)+  zerInRel :: Env -> Term -> Term+  zerInRel gs ty = inParam (map (map (wkn arity)) gs) ty (reverse $ map bound [0..arity-1])++  -- | Build a relation z ∈ ⟦ty⟧.  z is a term that, after renaming,+  -- gives the vector of terms member of the relation.  Note that+  -- 'param' is never applied to 'z', therefore 'zR' never occurs in the result.++  inParam :: Env -> Term -> [Term] -> Term+  inParam g (Star  p s)   zs = appl [Pi dummyId (wkn i z) | (i,z) <- zip [0..] zs] (Star p s)+  inParam g (Pi    i a b) zs = paramBind g Pi i a (inParam (extCtx g) b +                                                  [(wkn (arity + 1) z `app` bound i) | (i,z) <- zip (reverse [1..arity]) zs])++  inParam g@(g0:gs) (Sigma name@(Irr (Identifier (_,f))) a b) zs = +    Sigma name (inParam g a (map (`proj` f) zs))+    (inParam ((bound 0:map wk g0):[(proj (wk z) f):map wk g2 | (g2,z) <- zip gs zs]) b [(Extr (wk z) f) | z <- zs])+  -- z ∈ ⟦(x : A) × B(x)⟧ =   (x : π₁ z ∈ ⟦A⟧) × π₂ z ∈ ⟦B(x)⟧++  inParam g (Sigma _ _ _) z = error "Σ not implemented"+  inParam g t z = foldl app (paramProg g t) z++  -- | Translate a binding (x : A) into (x₁ : A₁) (⟦x⟧ : ⟦A⟧ x₁)+  paramBind :: Env -> (Ident -> Term -> Term -> Term) -> Ident -> Term -> Term -> Term+  paramBind g binder name a rest = +      appl +      [binder (re i name) (wkn (i-1) $ renam g i a) | i <- [1..arity]] $+      binder name         (zerInRel g a) $ +      rest ++nextRel = Sort 0 1+nxt = ssubst nextRel++--------------------------+-- destruction of worlds+++destruction :: Int -> Seq Bool -> Term -> Maybe Term+destruction destroyed d t = case t of+  (Hole p x)  -> Just $ Hole p ("|" ++  x ++ "|")+  (Bound p x)  +    | x >= Data.Sequence.length d -> Just (Bound p x)  +    -- FIXME: this is incorrect; instead the callers of this function+    -- must give the correct value for variables of the environment.+    | otherwise -> if d `index` x then Just (Bound p x) else Nothing+  (Star p (Sort l w))  +      | w >= destroyed -> Nothing+  (Star p (Sort l r))  -> Just $ Star p (Sort l r)+  (Pi i a b)  -> mb d Pi i a b +  (Sigma i a b)  -> mb d Sigma i a b +  (Lam i ty bo)  -> mb d Lam i ty bo  +  (Pair i a b)  -> mb d Pair i a b +  (Ann e t)  -> Ann <$> pr e <*> pr t +  (a :$: b)  -> case pr b of+                   Nothing -> pr a+                   Just b' -> (:$: b') <$> pr a +  (Proj x f) -> (\x -> Proj x f) <$> pr x  +  (Extr x f) -> (\x -> Extr x f) <$> pr x  +  +  -- FIXME: This should traverse the potential series of Param to find if the variable is removed.+  (Param arity (Bound p x)) | x < Data.Sequence.length d && not (d `index` x) -> Nothing+  -- Just a "renaming" on NFs: x should be a (renamed) variable.+  (Param arity x) -> Just (Destroy destroyed (Param arity x))+  (Shift f x)    ->  Just (Destroy destroyed (Shift f x))+   +  (OfParam n x) -> OfParam (modId (++ "%" ++ show destroyed) n) <$> pr x+  ++ where mb d binder i a b = case pr a of+                             Nothing -> str <$> destruction destroyed (False <| d) b+                             Just a' -> binder i a' <$> destruction destroyed (True <| d) b+       pr x = destruction destroyed d x++-- pr (Param x) d = Just x FIXME: there is a problem here: 1st+-- order variables have been removed, so we cannot refer to them.+++  +-}
+ TypeCheckerNF.hs view
@@ -0,0 +1,229 @@+{-# LANGUAGE PackageImports, TypeSynonymInstances, FlexibleInstances, GADTs #-}++-- Type checker loosely based on +--+-- "On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory", Abel, Coquand, Dybjer+--+-- some ideas from+--+-- "A Tutorial Implementation of a Dependently Typed Lambda Calculus", Löh, McBride, Swierstra+--+-- are also implemented.+--+-- The ideas related to parametricity and erasure are developed in+--+-- "Realizability and Parametricity in Pure Type Systems", Bernardy, Lasson+--++module TypeCheckerNF where++import Prelude hiding (length)+import Basics+import qualified Terms+import Terms (Term (Ann))+import Display+import Control.Monad.Error+import Data.Char+import Data.Maybe (isJust)+import Control.Monad.Trans.Error (ErrorT, runErrorT)+import Control.Monad.Trans.Writer+import Data.Functor.Identity+import Data.Sequence hiding (replicate)+import Data.Foldable (toList)+import Normal hiding (Term)+import Options++instance Error (Term,Doc) where+  strMsg s = (Terms.Hole dummyPosition "strMsg: panic!",text s)++type Result a = (ErrorT (Term,Doc)) -- term is used for position information+                (WriterT [Doc] Identity) a++report :: Doc -> Result ()+report x = lift $ tell [x]++runChecker :: Result a -> (Either (Term,Doc) a,[Doc])+runChecker x = runIdentity $ runWriterT $ runErrorT x++data Definition = Abstract -- ^ lambda, pi, sigma bound+                | Direct Value -- ^ pair bound++type Value    = NF+type Type     = Value+data Bind     = Bind {entryIdent :: Ident, +                      entryValue :: Definition, -- ^ Value for identifier. +                      entryType :: Type,    -- ^ Attention: context of the type does not contain the variable bound here.+                      entryRelevance :: Relevance+                     }+type Context  = Seq Bind++display :: Context -> NF -> Doc+display c = prettyTerm (fmap entryIdent c)++displayT :: Context -> Term -> Doc+displayT = Terms.prettyTerm . fmap entryIdent++dispContext :: Context -> Doc+dispContext ctx = case viewl ctx of+  EmptyL -> mempty+  Bind x val typ o :< ctx' -> let di = display ctx' in (case val of+    Abstract   ->             pretty x <+>                             ":" <+> di typ <+> ":" <+> pretty o+--    Direct (OfParam _ v) ->   "⟦"<>pretty x<>"⟧" <+> sep ["=" <+> parens (di v), "::" <+> di typ]+    Direct   v ->             pretty x <+> sep ["=" <+> parens (di v), ":" <+> di typ <+> ":" <+> pretty o]+    ) $$ dispContext ctx'++instance Lattice Sort where +  s1@(Sort l1 r1) ⊔ s2@(Sort l2 r2) +    | r1 /= r2 = s2+    | otherwise = case typeSystem options of+      CCω | l2 == 0 -> s2 -- The impredicative rule of CCω+      _ -> Sort (max l1 l2) r2++hole = Neu . Var . Hole++iType :: Context -> Term -> Result (Value,Type,Relevance)+iType g (Ann e tyt)+  =     do  (ty,o) <- iSort g tyt +            v <- cType g e ty+            return (v,ty,sortRelevance o) -- annotations are removed+iType g t@(Terms.Star p s)+   =  return (Star s,Star $ above s, sortRelevance s)  +iType g (Terms.Pi ident tyt tyt')  +   =  do  (ty ,s1) <- iSort g tyt +          let r1 = sortRelevance s1+          (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'+          let o = s1 ⊔ s2+          return (Pi r1 ident ty ty', Star o, sortRelevance o)+iType g (Terms.Sigma ident tyt tyt')  +   =  do  (ty,s1)  <- iSort g tyt +          let r1 = sortRelevance s1+          (ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'+          let o = s1 ⊔ s2+          return (Sigma r1 ident ty ty', Star o, sortRelevance o)+iType g e@(Terms.Bound _ x) = return $ (val $ entryValue e, wkn (x+1) $ entryType e,entryRelevance e)+  where val (Direct v) = wkn (x+1) v+        val _ = var x+        e = g `index` x+iType g (Terms.Hole p x) = do+  report $ hang (text ("context of " ++ x ++ " is")) 2 (dispContext g)+  return (hole x, hole ("type of " ++ x), 0)+iType g (e1 Terms.:$: e2)+  =     do  (v1,si,o') <- iType g e1+            case si of+              Pi o _ ty ty' -> do +                   v2 <- cType g e2 ty+                   return (app o v1 v2, subst0 v2 ty',o') +              _             ->  throwError (e1,"invalid application")+iType g (Terms.Proj e f) = do+  (v,t,o') <- iType g e+  search v t+ where search :: NF -> NF -> Result (Value,Type,Relevance)+       search v (Sigma o (Irr (Identifier (_,f'))) ty ty') +              | f == f' = return (π1,ty,o)+              | otherwise = search π2 (subst0 π1 ty')+           where +                 (π1,π2) = (case v of+                             Pair _ _ x y -> (x,y) -- substitution is useless if the pair is in normal form.+                             _ -> (proj o v True (Irr f'),proj o v False (Irr f'))  -- This could not happen if eta-expansion were done.+                             ) :: (NF,NF)+       search _ _ = throwError (e,"field not found")++iType g (Terms.Pair ident e1 e2) = do+  (v1,t1,o) <- iType g e1+  (v2,t2,o') <- iType (Bind ident (Direct v1) t1 o <| g) e2+  return $ (Pair o ident v1 (str v2),Sigma o ident t1 t2,o ⊔ o')+-- Note: the above does not infer a most general type: any potential dependency is discarded.++iType g t@(Terms.Lam x (Terms.Hole _ _) e) = throwError (t,"cannot infer type for" <+> displayT g t)+iType g (Terms.Lam x ty e) = do+    (vty,Sort _ o) <- iSort g ty+    (ve,t,o') <- iType (Bind x Abstract vty o <| g) e+    return $ (Lam o x vty ve, Pi o x vty t, o')++iType g (Terms.Param e) = do+  (v,t,o) <- iType g e+  return (param o v, app (next o) (param o t) (shift oneRel v), o)++iType g (Terms.Shift f e) = do+  (v,t,o) <- iType g e+  return (shift f v, shift f t, o + sortRelevance f)++iType g x@(Terms.Destroy d e) = do+  (v,t,o) <- iType g e  +  case d `destroys` o of+    True -> throwError (x,"total destruction is forbidden. destroyed term:" <+> display g v)+    False -> return (destroy d v,destroy d t, d-1) ++iSort :: Context -> Term -> Result (Type,Sort)+iSort g e = do+  (val,v,_) <- iType g e+  case v of +    Star i -> return (val,i)+    (Neu (Var (Hole h))) -> do +         report $ text h <+> "must be a type"+         return $ (hole h, Sort 1 0)+    _ -> throwError (e,displayT g e <+> "is not a type")++unify :: Context -> Term -> Type -> Type -> Result ()+unify g e q q' =+         do let ii = length g+                constraint = report $ vcat ["constraint: " <> display g q',+                                            "equal to  : " <> display g q]+            case (q,q') of+              ((Neu (Var (Hole _))), t) -> constraint+              (t, Neu (Var (Hole _))) -> constraint+              _ -> unless (q == q') +                       (throwError (e,hang "type mismatch: " 2 $ vcat +                                             ["inferred:" <+> display g q',+                                              "expected:" <+> display g q ,+                                              "for:" <+> displayT g e ,+                                              "context:" <+> dispContext g]))++-- Check the type and normalize+cType :: Context -> Term -> Type -> Result Value+cType g (Terms.Lam name (Terms.Hole _ _) e) (Pi o name' ty ty') = do+        e' <- cType (Bind name Abstract ty o <| g) e ty'+        return (Lam o name ty e') -- the type is filled in.++cType g (Terms.Lam name ty0 e) (Pi o name' ty ty')+  =     do (t,_o) <- iSort g ty0+           unify g (Terms.Hole (identPosition name) (show name)) t ty+           e' <- cType (Bind name Abstract ty o <| g) e ty'+           return (Lam o name ty e')++cType g (Terms.Pair name e1 e2) (Sigma o name' ty ty') = do+  -- note that names do not have to match.+  v1 <- cType g e1 ty           +  v2 <- cType (Bind name (Direct v1) ty o <| g) e2 (wk $ subst0 v1 ty') +        -- The above weakening is there because:+        -- * the type contains no occurence of the bound variable after substitution, but+        -- * the context is extended anyway, to bind the name to its value.+  return $ Pair o name' v1 (str v2)+  -- note that the pair must use the name of the sigma for the+  -- field. (The context will use the field name provided by the type)++--  Γ ⊢ ⌊A⌋ : B+cType g (Terms.OfParam i e) t = do+  -- Γ ⊢ A ⌊A⌋ : ⟦B⟧ ⌊A⌋+  -- Γ ⊢ A x   : ⟦B⟧ x+  -- Γ ⊢ A     : (x : ⌊B⌋) → ⟦B⟧ x+  -- FIXME: here I just assume the relevance of t is the following.+  let theRelevance = 0 +      theType = Pi (next theRelevance) i (shift oneRel $ t) +                   (zerInRel 0 t theRelevance)+  e' <- cType g e theType       +  return (Neu $ OfParam i e')++cType g (Terms.Shift f e) t = do+  shift f <$> cType g e (shift (negate f) t) +  -- there might be negative sorts in there, but that should be fine;+  -- if they occur the type checker will simply reject the term+  -- because it's impossible to create an inhabitant of a negative+  -- sort.++cType g e v +  =     do (e',v',_o) <- iType g e+           unify g e v v'+           return e'++
+ tutorial/00-Start-Here.ua view
@@ -0,0 +1,6 @@+-- A uAgda file contains exactly one term.+-- by running uAgda <file> you'll get the normal form for the term, and its type.+-- Try it on this file.++\(A : *) -> A -> A+
+ tutorial/01-Module.ua view
@@ -0,0 +1,61 @@+-- Modules, type annotations, Sigma+-------------------------------------++-- Usually you will want to break down your definitions+-- into multiple parts. That can be done by making the+-- top-level term a tuple. ++-- For example, this file starts with:+Nat = (N : *) -> (N -> N) -> N -> N,++-- which declares the 1st component of the tuple, and gives+-- it a name.+++-- Let's define some more stuff:+zer = \N s z -> z : Nat,+++-- Note that every term may be annotated by its type.  This is good+-- because no type inference is done.  (Even though the system is+-- clever enough to push down type annotations in lambdas)++-- Let's define the standard Church numeral toolbox:+++suc = \m N s z -> s (m N s z) +    : Nat -> Nat,++plus = \n m N s z -> n N s (m N s z)+     : Nat -> Nat -> Nat,++mul = \n m N s -> n N (m N s)+    : Nat -> Nat -> Nat,++exp = \n m N -> m (N -> N) (n N)+    : Nat -> Nat -> Nat,+++-- Now we're ready for some calculation! (the results can be seen in+-- the normal form)+one = suc zer,+two = suc one,+four = exp two (mul two two),++-- The syntax for pairs is "first class", we can have them anywhere:+somePair = (pi1 = two, plus two four) : (Nat ; Nat),+++-- Dependent pairs can also be declared+depPair  = (A = Nat, suc) : ((A : *1) ; A -> A),++-- fields named in the type can be extracted using #:+extract = depPair # A,++-- Finally we must give the last component of the tuple, which is NOT+-- named.  Since we have nothing special in mind, let's just give a+-- trival (meaningless) term:++*++
+ tutorial/02-Holes.ua view
@@ -0,0 +1,31 @@+-- Module parametrization, universes, holes.+-----------------------------------------------++-- If you want to parameterize your module (think ML functors), just+-- use top-level abstraction: ++\ (Z : *) (plus : Z -> Z -> Z) -> ( ++-- Note that parentheses are needed here (check operator precedence in+-- the source code: "RawSyntax.hs" contains the syntax in BNF)+++-- We define Leibniz equality for good measure:+Eq = \ A a b -> (P : A -> *) -> P a -> P b+     : (A : *) -> (a b : A) -> *1,++-- By default uAgda is predicative, hence Leibniz equality is in +-- *1.++-- Sometimes you may want to omit the definition for a particular+-- term. (For example you know a theorem to hold but you'd rather+-- write the proof later.)  In that case you can use the "hole"+-- construct as follows. ++plus-commutative = \ (x : Z) (y : Z) -> (?x : Eq Z (plus x y) (plus y x)),++-- Note that uAgda shows the context of the hole, so it's easier to+-- fill it in later.++-- End of tuple.+*)
+ tutorial/03-Parametricity.ua view
@@ -0,0 +1,41 @@+-- Parametricity, relevance and erasure+-----------------------------------------++-- In uAgda every term is assumed to be parametric.+-- hence for an arbitrary function f...+\(A : *) (B : *) (f : A -> B) -> (++-- we can use the fact that it is parametric by using the postfix '!' operator:+fparam = f! : (x : A<) -> A! x -> B! (f< x),+++-- Note that the "x" an irrelevant argument to f!. We say that it lies+-- in another relevance world. This is indicated by the postfix <+-- after its type.++-- that is ok, because we can always convert a term into a copy of it at +-- a less relevant level (using that operator).+++-- It is also possible to erase all the stuff less relevant than a+-- certain world by using the operator '%'. For example, after+-- erasing all the (level one) irrelevant stuff from the above type we+-- recover the original (check the normal form):++eraseType = ((x : A<) -> A! x -> B! (f< x)) % 1,+++-- Indeed, f!%1 = f.+fAgain = fparam %1,+++-- We can get binary parametricity by combination of unary+-- parametricity and erasure. See the following reference for+-- the explanation:++-- https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466++fparam2 = f!!%2 : (x y : A<) -> A!!%2 x y -> B!!%2 (f< x) (f< y),+++*)
+ tutorial/04-Data.ua view
@@ -0,0 +1,75 @@+-- Data+---------++-- In the Calculus of Constructions, it is possible to encode data via+-- Church-style encodings. However, it is then impossible to do+-- inductive reasoning on these. This led to the addition of inductive+-- constructions (CiC). Agda features inductive families as a native+-- construct.++-- Even though uAgda does not feature a native construction for data,+-- it is possible to encode data using parametricity, erasure and a+-- little bit of special sauce. The trick is that ++-- 1. The erasure of the induction principle for a given inductive+-- family is equal to its Church representation, and++-- 2. The relational interpretation of the representation yields back+-- the inductive principle.++-- More theoretical background can be found in Phil Wadler's "The+-- Girard-Reynolds isomorphism".+++-- In uAgda, we proceed as follows. First define the appropriate+-- induction principle and the proof that the constructors respect+-- induction. (Note that these definitions are parameterised over an+-- arbitrary module "q" containing an *abstract* version of the stuff+-- we want to define (here with fields Nat, suc and zer).++param Q = \ q -> (++Nat = \n -> (P : q#Nat -> *) -> ((n : q#Nat) -> P n -> P (q#suc n)) -> (P q#zer) -> P n,+zer = \P s z -> z,+suc = \m n P s z -> s m (n P s z),+\ _ -> *)++:: ((Nat : *1) ; (zer : Nat) ; (suc : Nat -> Nat) ; *1),++-- The keyword "param" and the double colon are special syntax to+-- construct a concrete representation (here "Q") that is+-- computationally equal to the erasure of the above, but whose+-- relational interpretation is the one given.++-- (The last component of the tuple is just noise, as usual).+++-- From there we can do simple computations:+one = Q#suc Q#zer : Q#Nat,+two = Q#suc one,++++-- And we can also do inductive reasoning (but indexed by a less+-- relevant version of the type/values):+Nat-elim = \n -> n!+         : (n : Q#Nat) -> (P : Q<#Nat -> *) -> ((n : Q<#Nat) -> P n -> P (Q<#suc n)) -> (P Q<#zer) -> P n<,+++-- In particular, we can also inductive computation.  In that case,+-- because we work in a predicative type system, we need to apply the+-- induction on a copy of the natural lifted to a higher universe.+-- That's fine, because we also have an operator for that: postfix ^.++lift = \n -> n^+     : Q#Nat -> Q#Nat^,++plus + = \m n -> n^! (\_ -> Q#Nat) (\_ r -> Q#suc r) m + : Q#Nat -> Q#Nat -> Q#Nat,+++four = plus two two,++*+
+ uAgda.cabal view
@@ -0,0 +1,57 @@+name:           uAgda+version:        1.0.0.0+category:       Dependent Types+synopsis:       A simplistic dependently-typed language with parametricity.+description:++        uAgda implements an experimental dependently-typed language+        (and proof assistant by the Curry-Howard isomorphism). The+        goal of the project is twofold:+        .+        1. Experiment with a minimalistic language that is strong enough to+        program and reason in.+        .+        2. Give a simple implementation of its type-checker (ours is ~200 lines).+        +   +license:        OtherLicense+-- Creative Commons Attribution Share-Alike+license-file:   LICENSE+author:         Jean-Philippe Bernardy+maintainer:     jeanphilippe.bernardy@gmail.com+Cabal-Version:  >= 1.8+tested-with:    GHC==6.12.3+build-type:     Simple++extra-source-files:+     tutorial/00-Start-Here.ua+     tutorial/01-Module.ua+     tutorial/02-Holes.ua+     tutorial/03-Parametricity.ua+     tutorial/04-Data.ua+++executable uAgda+  extensions: CPP, FlexibleInstances, OverloadedStrings+  main-is: Main.hs++  other-modules:+     AbsSynToTerm+     Basics+     Display+     Main+     Normal+     Options+     RawSyntax+     Terms+     TypeCheckerNF++  build-depends: base==4.*+  build-depends: cmdargs==0.6.*+  build-depends: containers==0.3.*+  build-depends: pretty==1.0.*+  build-depends: parsec==2.1.*+  build-depends: BNFC-meta==0.1.*+  build-depends: transformers == 0.2.*+  build-depends: monads-fd == 0.1.*+