module Core.TT import public Core.FCimport public Core.Name import Data.NameMapimport Data.Vectimport public Algebra %default covering %hide Binder%hide NameType public exportdata NameType : Type where     Bound   : NameType     Func    : NameType     DataCon : (tag : Int) -> (arity : Nat) -> NameType     TyCon   : (tag : Int) -> (arity : Nat) -> NameType public exportdata Constant    = I Int    | BI Integer    | Str String    | Ch Char    | Db Double    | WorldVal     | IntType    | IntegerType    | StringType    | CharType    | DoubleType    | WorldType exportconstantEq : (x, y : Constant) -> Maybe (x = y)constantEq (I x) (I y) = case decEq x y of                              Yes Refl => Just Refl                              No contra => NothingconstantEq (BI x) (BI y) = case decEq x y of                                Yes Refl => Just Refl                                No contra => NothingconstantEq (Str x) (Str y) = case decEq x y of                                  Yes Refl => Just Refl                                  No contra => NothingconstantEq (Ch x) (Ch y) = case decEq x y of                                Yes Refl => Just Refl                                No contra => NothingconstantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!constantEq WorldVal WorldVal = Just ReflconstantEq IntType IntType = Just ReflconstantEq IntegerType IntegerType = Just ReflconstantEq StringType StringType = Just ReflconstantEq CharType CharType = Just ReflconstantEq DoubleType DoubleType = Just ReflconstantEq WorldType WorldType = Just ReflconstantEq _ _ = Nothing exportShow Constant where  show (I x) = show x  show (BI x) = show x  show (Str x) = show x  show (Ch x) = show x  show (Db x) = show x  show WorldVal = "%MkWorld"  show IntType = "Int"  show IntegerType = "Integer"  show StringType = "String"  show CharType = "Char"  show DoubleType = "Double"  show WorldType = "%World" exportEq Constant where  (I x) == (I y) = x == y  (BI x) == (BI y) = x == y  (Str x) == (Str y) = x == y  (Ch x) == (Ch y) = x == y  (Db x) == (Db y) = x == y  WorldVal == WorldVal = True  IntType == IntType = True  IntegerType == IntegerType = True  StringType == StringType = True  CharType == CharType = True  DoubleType == DoubleType = True  WorldType == WorldType = True  _ == _ = False -- for typecaseexportconstTag : Constant -> Int-- 1 = ->, 2 = TypeconstTag IntType = 3constTag IntegerType = 4constTag StringType = 5constTag CharType = 6constTag DoubleType = 7constTag WorldType = 8constTag _ = 0 -- All the internal operators, parameterised by their aritypublic exportdata PrimFn : Nat -> Type where     Add : (ty : Constant) -> PrimFn 2     Sub : (ty : Constant) -> PrimFn 2     Mul : (ty : Constant) -> PrimFn 2     Div : (ty : Constant) -> PrimFn 2     Mod : (ty : Constant) -> PrimFn 2     Neg : (ty : Constant) -> PrimFn 1     ShiftL : (ty : Constant) -> PrimFn 2     ShiftR : (ty : Constant) -> PrimFn 2      BAnd : (ty : Constant) -> PrimFn 2     BOr : (ty : Constant) -> PrimFn 2     BXOr : (ty : Constant) -> PrimFn 2      LT  : (ty : Constant) -> PrimFn 2     LTE : (ty : Constant) -> PrimFn 2     EQ  : (ty : Constant) -> PrimFn 2     GTE : (ty : Constant) -> PrimFn 2     GT  : (ty : Constant) -> PrimFn 2      StrLength : PrimFn 1     StrHead : PrimFn 1     StrTail : PrimFn 1     StrIndex : PrimFn 2     StrCons : PrimFn 2     StrAppend : PrimFn 2     StrReverse : PrimFn 1     StrSubstr : PrimFn 3      DoubleExp : PrimFn 1     DoubleLog : PrimFn 1     DoubleSin : PrimFn 1     DoubleCos : PrimFn 1     DoubleTan : PrimFn 1     DoubleASin : PrimFn 1     DoubleACos : PrimFn 1     DoubleATan : PrimFn 1     DoubleSqrt : PrimFn 1     DoubleFloor : PrimFn 1     DoubleCeiling : PrimFn 1      Cast : Constant -> Constant -> PrimFn 1     BelieveMe : PrimFn 3     Crash : PrimFn 2 exportShow (PrimFn arity) where  show (Add ty) = "+" ++ show ty  show (Sub ty) = "-" ++ show ty  show (Mul ty) = "*" ++ show ty  show (Div ty) = "/" ++ show ty  show (Mod ty) = "%" ++ show ty  show (Neg ty) = "neg " ++ show ty  show (ShiftL ty) = "shl " ++ show ty  show (ShiftR ty) = "shr " ++ show ty  show (BAnd ty) = "and " ++ show ty  show (BOr ty) = "or " ++ show ty  show (BXOr ty) = "xor " ++ show ty  show (LT ty) = "<" ++ show ty  show (LTE ty) = "<=" ++ show ty  show (EQ ty) = "==" ++ show ty  show (GTE ty) = ">=" ++ show ty  show (GT ty) = ">" ++ show ty  show StrLength = "op_strlen"  show StrHead = "op_strhead"  show StrTail = "op_strtail"  show StrIndex = "op_strindex"  show StrCons = "op_strcons"  show StrAppend = "++"  show StrReverse = "op_strrev"  show StrSubstr = "op_strsubstr"  show DoubleExp = "op_doubleExp"  show DoubleLog = "op_doubleLog"  show DoubleSin = "op_doubleSin"  show DoubleCos = "op_doubleCos"  show DoubleTan = "op_doubleTan"  show DoubleASin = "op_doubleASin"  show DoubleACos = "op_doubleACos"  show DoubleATan = "op_doubleATan"  show DoubleSqrt = "op_doubleSqrt"  show DoubleFloor = "op_doubleFloor"  show DoubleCeiling = "op_doubleCeiling"  show (Cast x y) = "cast-" ++ show x ++ "-" ++ show y  show BelieveMe = "believe_me"  show Crash = "crash" public exportdata PiInfo t = Implicit | Explicit | AutoImplicit | DefImplicit t -- There's few places where we need the default - it's just when checking if-- there's a default during elaboration - so often it's easier just to erase it-- to a normal implicitexportforgetDef : PiInfo t -> PiInfo t'forgetDef Explicit = ExplicitforgetDef Implicit = ImplicitforgetDef AutoImplicit = AutoImplicitforgetDef (DefImplicit t) = Implicit exportShow t => Show (PiInfo t) where  show Implicit = "Implicit"  show Explicit = "Explicit"  show AutoImplicit = "AutoImplicit"  show (DefImplicit t) = "DefImplicit " ++ show t exportEq t => Eq (PiInfo t) where  (==) Implicit Implicit = True  (==) Explicit Explicit = True  (==) AutoImplicit AutoImplicit = True  (==) (DefImplicit t) (DefImplicit t') = t == t'  (==) _ _ = False public exportdata Binder : Type -> Type where	   -- Lambda bound variables with their implicitness     Lam : RigCount -> PiInfo type -> (ty : type) -> Binder type		 -- Let bound variables with their value     Let : RigCount -> (val : type) -> (ty : type) -> Binder type		 -- Forall/pi bound variables with their implicitness     Pi : RigCount -> PiInfo type -> (ty : type) -> Binder type		 -- pattern bound variables. The PiInfo gives the implicitness at the     -- point it was bound (Explicit if it was explicitly named in the     -- program)     PVar : RigCount -> PiInfo type -> (ty : type) -> Binder type		 -- variable bound for an as pattern (Like a let, but no computational     -- force, and only used on the lhs. Converted to a let on the rhs because     -- we want the computational behaviour.)     PLet : RigCount -> (val : type) -> (ty : type) -> Binder type		 -- the type of pattern bound variables     PVTy : RigCount -> (ty : type) -> Binder type exportbinderType : Binder tm -> tmbinderType (Lam _ x ty) = tybinderType (Let _ val ty) = tybinderType (Pi _ x ty) = tybinderType (PVar _ _ ty) = tybinderType (PLet _ val ty) = tybinderType (PVTy _ ty) = ty exportmultiplicity : Binder tm -> RigCountmultiplicity (Lam c x ty) = cmultiplicity (Let c val ty) = cmultiplicity (Pi c x ty) = cmultiplicity (PVar c p ty) = cmultiplicity (PLet c val ty) = cmultiplicity (PVTy c ty) = c exportsetMultiplicity : Binder tm -> RigCount -> Binder tmsetMultiplicity (Lam c x ty) c' = Lam c' x tysetMultiplicity (Let c val ty) c' = Let c' val tysetMultiplicity (Pi c x ty) c' = Pi c' x tysetMultiplicity (PVar c p ty) c' = PVar c' p tysetMultiplicity (PLet c val ty) c' = PLet c' val tysetMultiplicity (PVTy c ty) c' = PVTy c' ty showCount : RigCount -> StringshowCount = elimSemi "0 " "1 " (const "") Show ty => Show (Binder ty) where	show (Lam c _ t) = "\\" ++ showCount c ++ show t	show (Pi c _ t) = "Pi " ++ showCount c ++ show t	show (Let c v t) = "let " ++ showCount c ++ show v ++ " : " ++ show t	show (PVar c _ t) = "pat " ++ showCount c ++ show t	show (PLet c v t) = "plet " ++ showCount c ++ show v ++ " : " ++ show t	show (PVTy c t) = "pty " ++ showCount c ++ show t exportsetType : Binder tm -> tm -> Binder tmsetType (Lam c x _) ty = Lam c x tysetType (Let c val _) ty = Let c val tysetType (Pi c x _) ty = Pi c x tysetType (PVar c p _) ty = PVar c p tysetType (PLet c val _) ty = PLet c val tysetType (PVTy c _) ty = PVTy c ty exportFunctor PiInfo where  map func Explicit = Explicit  map func Implicit = Implicit  map func AutoImplicit = AutoImplicit  map func (DefImplicit t) = (DefImplicit (func t)) exportFunctor Binder where  map func (Lam c x ty) = Lam c (map func x) (func ty)  map func (Let c val ty) = Let c (func val) (func ty)  map func (Pi c x ty) = Pi c (map func x) (func ty)  map func (PVar c p ty) = PVar c (map func p) (func ty)  map func (PLet c val ty) = PLet c (func val) (func ty)  map func (PVTy c ty) = PVTy c (func ty) public exportdata IsVar : Name -> Nat -> List Name -> Type where     First : IsVar n Z (n :: ns)     Later : IsVar n i ns -> IsVar n (S i) (m :: ns) public exportdropVar : (ns : List Name) -> {idx : Nat} -> .(IsVar name idx ns) -> List NamedropVar (n :: xs) First = xsdropVar (n :: xs) (Later p) = n :: dropVar xs p public exportdata Var : List Name -> Type where     MkVar : {i : Nat} -> .(IsVar n i vars) -> Var vars exportsameVar : Var xs -> Var xs -> BoolsameVar (MkVar {i=x} _) (MkVar {i=y} _) = x == y exportvarIdx : Var xs -> NatvarIdx (MkVar {i} _) = i exportdropFirst : List (Var (v :: vs)) -> List (Var vs)dropFirst [] = []dropFirst (MkVar First :: vs) = dropFirst vsdropFirst (MkVar (Later p) :: vs) = MkVar p :: dropFirst vs exportShow (Var ns) where  show (MkVar {i} _) = show i namespace CList  -- A list correspoding to another list  public export  data CList : List a -> Type -> Type where       Nil : CList [] ty       (::) : (x : ty) -> CList cs ty -> CList (c :: cs) ty -- Typechecked terms-- These are guaranteed to be well-scoped wrt local variables, because they are-- indexed by the names of local variables in scopepublic exportdata LazyReason = LInf | LLazy | LUnknown -- For as patterns matching linear arguments, select which side is-- consumedpublic exportdata UseSide = UseLeft | UseRight public exportdata Term : List Name -> Type where     Local : {name : _} ->             FC -> (isLet : Maybe Bool) ->             (idx : Nat) -> .(IsVar name idx vars) -> Term vars     Ref : FC -> NameType -> (name : Name) -> Term vars     -- Metavariables and the scope they are applied to     Meta : FC -> Name -> Int -> List (Term vars) -> Term vars     Bind : FC -> (x : Name) ->            (b : Binder (Term vars)) ->            (scope : Term (x :: vars)) -> Term vars     App : FC -> (fn : Term vars) -> (arg : Term vars) -> Term vars     -- as patterns; since we check LHS patterns as terms before turning     -- them into patterns, this helps us get it right. When normalising,     -- we just reduce the inner term and ignore the 'as' part     -- The 'as' part should really be a Name rather than a Term, but it's     -- easier this way since it gives us the ability to work with unresolved     -- names (Ref) and resolved names (Local) without having to define a     -- special purpose thing. (But it'd be nice to tidy that up, nevertheless)     As : FC -> UseSide -> (as : Term vars) -> (pat : Term vars) -> Term vars     -- Typed laziness annotations     TDelayed : FC -> LazyReason -> Term vars -> Term vars     TDelay : FC -> LazyReason -> (ty : Term vars) -> (arg : Term vars) -> Term vars     TForce : FC -> LazyReason -> Term vars -> Term vars     PrimVal : FC -> (c : Constant) -> Term vars     Erased : FC -> (imp : Bool) -> -- True == impossible term, for coverage checker              Term vars     TType : FC -> Term vars exportgetLoc : Term vars -> FCgetLoc (Local fc _ _ _) = fcgetLoc (Ref fc _ _) = fcgetLoc (Meta fc _ _ _) = fcgetLoc (Bind fc _ _ _) = fcgetLoc (App fc _ _) = fcgetLoc (As fc _ _ _) = fcgetLoc (TDelayed fc _ _) = fcgetLoc (TDelay fc _ _ _) = fcgetLoc (TForce fc _ _) = fcgetLoc (PrimVal fc _) = fcgetLoc (Erased fc i) = fcgetLoc (TType fc) = fc exportEq LazyReason where  (==) LInf LInf = True  (==) LLazy LLazy = True  (==) LUnknown LUnknown = True  (==) _ _ = False exportcompatible : LazyReason -> LazyReason -> Boolcompatible LUnknown _ = Truecompatible _ LUnknown = Truecompatible x y = x == y exportEq a => Eq (Binder a) where  (Lam c p ty) == (Lam c' p' ty') = c == c' && p == p' && ty == ty'  (Let c v ty) == (Let c' v' ty') = c == c' && v == v' && ty == ty'  (Pi c p ty) == (Pi c' p' ty') = c == c' && p == p' && ty == ty'  (PVar c p ty) == (PVar c' p' ty') = c == c' && p == p' && ty == ty'  (PLet c v ty) == (PLet c' v' ty') = c == c' && v == v' && ty == ty'  (PVTy c ty) == (PVTy c' ty') = c == c' && ty == ty'  _ == _ = False exportEq (Term vars) where  (==) (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'  (==) (Ref _ _ n) (Ref _ _ n') = n == n'  (==) (Meta _ _ i args) (Meta _ _ i' args')      = assert_total (i == i' && args == args')  (==) (Bind _ _ b sc) (Bind _ _ b' sc')      = assert_total (b == b' && sc == believe_me sc')  (==) (App _ f a) (App _ f' a') = f == f' && a == a'  (==) (As _ _ a p) (As _ _ a' p') = a == a' && p == p'  (==) (TDelayed _ _ t) (TDelayed _ _ t') = t == t'  (==) (TDelay _ _ t x) (TDelay _ _ t' x') = t == t' && x == x'  (==) (TForce _ _ t) (TForce _ _ t') = t == t'  (==) (PrimVal _ c) (PrimVal _ c') = c == c'  (==) (Erased _ i) (Erased _ i') = i == i'  (==) (TType _) (TType _) = True  (==) _ _ = False -- Check equality, ignoring variable namingexporteqTerm : Term vs -> Term vs' -> BooleqTerm (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'eqTerm (Ref _ _ n) (Ref _ _ n') = n == n'eqTerm (Meta _ _ i args) (Meta _ _ i' args')    = assert_total (i == i' && and (map Delay (zipWith eqTerm args args')))eqTerm (Bind _ _ b sc) (Bind _ _ b' sc')    = assert_total (eqBinder b b' && eqTerm sc sc')  where    eqPiInfo : PiInfo (Term vs) -> PiInfo (Term vs') -> Bool    eqPiInfo Explicit Explicit = True    eqPiInfo Implicit Implicit = True    eqPiInfo AutoImplicit AutoImplicit = True    eqPiInfo (DefImplicit t) (DefImplicit t') = eqTerm t t'    eqPiInfo _ _ = False     eqBinder : Binder (Term vs) -> Binder (Term vs') -> Bool    eqBinder (Lam c p ty) (Lam c' p' ty')        = c == c' && eqPiInfo p p' && eqTerm ty ty'    eqBinder (Let c v ty) (Let c' v' ty')        = c == c' && eqTerm v v' && eqTerm ty ty'    eqBinder (Pi c p ty) (Pi c' p' ty')        = c == c' && eqPiInfo p p' && eqTerm ty ty'    eqBinder (PVar c p ty) (PVar c' p' ty')        = c == c' && eqPiInfo p p' && eqTerm ty ty'    eqBinder (PLet c v ty) (PLet c' v' ty')        = c == c' && eqTerm v v' && eqTerm ty ty'    eqBinder (PVTy c ty) (PVTy c' ty')        = c == c' && eqTerm ty ty'    eqBinder _ _ = FalseeqTerm (App _ f a) (App _ f' a') = eqTerm f f' && eqTerm a a'eqTerm (As _ _ a p) (As _ _ a' p') = eqTerm a a' && eqTerm p p'eqTerm (TDelayed _ _ t) (TDelayed _ _ t') = eqTerm t t'eqTerm (TDelay _ _ t x) (TDelay _ _ t' x') = eqTerm t t' && eqTerm x x'eqTerm (TForce _ _ t) (TForce _ _ t') = eqTerm t t'eqTerm (PrimVal _ c) (PrimVal _ c') = c == c'eqTerm (Erased _ i) (Erased _ i') = i == i'eqTerm (TType _) (TType _) = TrueeqTerm _ _ = False public exportinterface Weaken (tm : List Name -> Type) where  weaken : tm vars -> tm (n :: vars)  weakenNs : (ns : List Name) -> tm vars -> tm (ns ++ vars)   weakenNs [] t = t  weakenNs (n :: ns) t = weaken (weakenNs ns t)   weaken = weakenNs [_] public exportdata Visibility = Private | Export | Public exportShow Visibility where  show Private = "private"  show Export = "export"  show Public = "public export" exportEq Visibility where  Private == Private = True

Lines 1–500 of 1274. Load more