mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-10-26 17:33:47 +03:00
Reorganise Language.Reflection modules
This commit is contained in:
Edwin Brady
parent
1c006b647a
commit
aae3d0f718
@ -1,217 +1,10 @@
|
||||
module Language.Reflection
|
||||
|
||||
public export
|
||||
FilePos : Type
|
||||
FilePos = (Int, Int)
|
||||
import public Language.Reflection.TT
|
||||
import public Language.Reflection.TTImp
|
||||
|
||||
public export
|
||||
data FC : Type where
|
||||
MkFC : String -> FilePos -> FilePos -> FC
|
||||
EmptyFC : FC
|
||||
data TC : Type -> Type where
|
||||
Check : TTImp -> TC a
|
||||
Bind : TC a -> (a -> TC b) -> TC b
|
||||
|
||||
public export
|
||||
emptyFC : FC
|
||||
emptyFC = MkFC "(empty)" (0, 0) (0, 0)
|
||||
|
||||
public export
|
||||
data NameType : Type where
|
||||
Bound : NameType
|
||||
Func : NameType
|
||||
DataCon : (tag : Int) -> (arity : Nat) -> NameType
|
||||
TyCon : (tag : Int) -> (arity : Nat) -> NameType
|
||||
|
||||
public export
|
||||
data Constant
|
||||
= I Int
|
||||
| BI Integer
|
||||
| Str String
|
||||
| Ch Char
|
||||
| Db Double
|
||||
| WorldVal
|
||||
|
||||
| IntType
|
||||
| IntegerType
|
||||
| StringType
|
||||
| CharType
|
||||
| DoubleType
|
||||
| WorldType
|
||||
|
||||
public export
|
||||
data Name = UN String
|
||||
| MN String Int
|
||||
| NS (List String) Name
|
||||
|
||||
public export
|
||||
data Count = M0 | M1 | MW
|
||||
|
||||
public export
|
||||
data PiInfo = ImplicitArg | ExplicitArg | AutoImplicit
|
||||
|
||||
public export
|
||||
data 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 export
|
||||
data LazyReason = LInf | LLazy | LUnknown
|
||||
|
||||
-- Type checked terms in the core TT
|
||||
public export
|
||||
data TT : List Name -> Type where
|
||||
Local : FC -> (idx : Nat) -> (n : Name) ->
|
||||
(0 prf : IsVar name idx vars) -> TT vars
|
||||
Ref : FC -> NameType -> Name -> TT vars
|
||||
Pi : FC -> Count -> PiInfo ->
|
||||
(x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) ->
|
||||
TT vars
|
||||
Lam : FC -> Count -> PiInfo ->
|
||||
(x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) ->
|
||||
TT vars
|
||||
App : FC -> TT vars -> TT vars -> TT vars
|
||||
TDelayed : FC -> LazyReason -> TT vars -> TT vars
|
||||
TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars
|
||||
TForce : FC -> TT vars -> TT vars
|
||||
PrimVal : FC -> Constant -> TT vars
|
||||
Erased : FC -> TT vars
|
||||
TType : FC -> TT vars
|
||||
|
||||
public export
|
||||
data Visibility = Private | Export | Public
|
||||
|
||||
-- Unchecked terms and declarations in the intermediate language
|
||||
mutual
|
||||
public export
|
||||
data BindMode = PI Count | PATTERN | NONE
|
||||
|
||||
-- For as patterns matching linear arguments, select which side is
|
||||
-- consumed
|
||||
public export
|
||||
data UseSide = UseLeft | UseRight
|
||||
|
||||
data TTImp : Type where
|
||||
IVar : FC -> Name -> TTImp
|
||||
IPi : FC -> Count -> PiInfo -> Maybe Name ->
|
||||
(argTy : TTImp) -> (retTy : TTImp) -> TTImp
|
||||
ILam : FC -> Count -> PiInfo -> Maybe Name ->
|
||||
(argTy : TTImp) -> (lamTy : TTImp) -> TTImp
|
||||
ILet : FC -> Count -> Name ->
|
||||
(nTy : TTImp) -> (nVal : TTImp) ->
|
||||
(scope : TTImp) -> TTImp
|
||||
ICase : FC -> TTImp -> (ty : TTImp) ->
|
||||
List Clause -> TTImp
|
||||
ILocal : FC -> List Decl -> TTImp -> TTImp
|
||||
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
|
||||
|
||||
IApp : FC -> TTImp -> TTImp -> TTImp
|
||||
IImplicitApp : FC -> TTImp -> Maybe Name -> TTImp -> TTImp
|
||||
IWithApp : FC -> TTImp -> TTImp -> TTImp
|
||||
|
||||
ISearch : FC -> (depth : Nat) -> TTImp
|
||||
IAlternative : FC -> AltType -> List TTImp -> TTImp
|
||||
IRewrite : FC -> TTImp -> TTImp -> TTImp
|
||||
|
||||
-- Any implicit bindings in the scope should be bound here, using
|
||||
-- the given binder
|
||||
IBindHere : FC -> BindMode -> TTImp -> TTImp
|
||||
-- A name which should be implicitly bound
|
||||
IBindVar : FC -> String -> TTImp
|
||||
-- An 'as' pattern, valid on the LHS of a clause only
|
||||
IAs : FC -> UseSide -> Name -> TTImp -> TTImp
|
||||
-- A 'dot' pattern, i.e. one which must also have the given value
|
||||
-- by unification
|
||||
IMustUnify : FC -> (reason : String) -> TTImp -> TTImp
|
||||
|
||||
-- Laziness annotations
|
||||
IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type
|
||||
IDelay : FC -> TTImp -> TTImp -- delay constructor
|
||||
IForce : FC -> TTImp -> TTImp
|
||||
|
||||
IPrimVal : FC -> (c : Constant) -> TTImp
|
||||
IType : FC -> TTImp
|
||||
IHole : FC -> String -> TTImp
|
||||
|
||||
-- An implicit value, solved by unification, but which will also be
|
||||
-- bound (either as a pattern variable or a type variable) if unsolved
|
||||
-- at the end of elaborator
|
||||
Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
|
||||
|
||||
public export
|
||||
data IFieldUpdate : Type where
|
||||
ISetField : (path : List String) -> TTImp -> IFieldUpdate
|
||||
ISetFieldApp : (path : List String) -> TTImp -> IFieldUpdate
|
||||
|
||||
public export
|
||||
data AltType : Type where
|
||||
FirstSuccess : AltType
|
||||
Unique : AltType
|
||||
UniqueDefault : TTImp -> AltType
|
||||
|
||||
public export
|
||||
data FnOpt : Type where
|
||||
Inline : FnOpt
|
||||
-- Flag means the hint is a direct hint, not a function which might
|
||||
-- find the result (e.g. chasing parent interface dictionaries)
|
||||
Hint : Bool -> FnOpt
|
||||
-- Flag means to use as a default if all else fails
|
||||
GlobalHint : Bool -> FnOpt
|
||||
ExternFn : FnOpt
|
||||
-- Defined externally, list calling conventions
|
||||
ForeignFn : List String -> FnOpt
|
||||
-- assume safe to cancel arguments in unification
|
||||
Invertible : FnOpt
|
||||
Total : FnOpt
|
||||
Covering : FnOpt
|
||||
PartialOK : FnOpt
|
||||
|
||||
public export
|
||||
data ITy : Type where
|
||||
MkTy : FC -> (n : Name) -> (ty : TTImp) -> ITy
|
||||
|
||||
public export
|
||||
data DataOpt : Type where
|
||||
SearchBy : List Name -> DataOpt -- determining arguments
|
||||
NoHints : DataOpt -- Don't generate search hints for constructors
|
||||
|
||||
public export
|
||||
data Data : Type where
|
||||
MkData : FC -> (n : Name) -> (tycon : TTImp) ->
|
||||
(opts : List DataOpt) ->
|
||||
(datacons : List ITy) -> Data
|
||||
MkLater : FC -> (n : Name) -> (tycon : TTImp) -> Data
|
||||
|
||||
public export
|
||||
data IField : Type where
|
||||
MkIField : FC -> Count -> PiInfo -> Name -> TTImp ->
|
||||
IField
|
||||
|
||||
public export
|
||||
data Record : Type where
|
||||
MkRecord : FC -> (n : Name) ->
|
||||
(params : List (Name, TTImp)) ->
|
||||
(conName : Maybe Name) ->
|
||||
(fields : List IField) ->
|
||||
Record
|
||||
|
||||
public export
|
||||
data Clause : Type where
|
||||
PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
|
||||
WithClause : FC -> (lhs : TTImp) -> (wval : TTImp) ->
|
||||
List Clause -> Clause
|
||||
ImpossibleClause : FC -> (lhs : TTImp) -> Clause
|
||||
|
||||
public export
|
||||
data Decl : Type where
|
||||
IClaim : FC -> Count -> Visibility -> List FnOpt ->
|
||||
ITy -> Decl
|
||||
IData : FC -> Visibility -> Data -> Decl
|
||||
IDef : FC -> Name -> List Clause -> Decl
|
||||
IParameters : FC -> List (Name, TTImp) ->
|
||||
List Decl -> Decl
|
||||
IRecord : FC -> Visibility -> Record -> Decl
|
||||
INamespace : FC ->
|
||||
(nested : Bool) ->
|
||||
-- ^ if True, parent namespaces in the same file can also
|
||||
-- look inside and see private/export names in full
|
||||
List String -> List Decl -> Decl
|
||||
ITransform : FC -> TTImp -> TTImp -> Decl
|
||||
ILog : Nat -> Decl
|
||||
|
||||
80
libs/base/Language/Reflection/TT.idr
Normal file
80
libs/base/Language/Reflection/TT.idr
Normal file
@ -0,0 +1,80 @@
|
||||
module Language.Reflection.TT
|
||||
|
||||
public export
|
||||
FilePos : Type
|
||||
FilePos = (Int, Int)
|
||||
|
||||
public export
|
||||
data FC : Type where
|
||||
MkFC : String -> FilePos -> FilePos -> FC
|
||||
EmptyFC : FC
|
||||
|
||||
public export
|
||||
emptyFC : FC
|
||||
emptyFC = EmptyFC
|
||||
|
||||
public export
|
||||
data NameType : Type where
|
||||
Bound : NameType
|
||||
Func : NameType
|
||||
DataCon : (tag : Int) -> (arity : Nat) -> NameType
|
||||
TyCon : (tag : Int) -> (arity : Nat) -> NameType
|
||||
|
||||
public export
|
||||
data Constant
|
||||
= I Int
|
||||
| BI Integer
|
||||
| Str String
|
||||
| Ch Char
|
||||
| Db Double
|
||||
| WorldVal
|
||||
|
||||
| IntType
|
||||
| IntegerType
|
||||
| StringType
|
||||
| CharType
|
||||
| DoubleType
|
||||
| WorldType
|
||||
|
||||
public export
|
||||
data Name = UN String
|
||||
| MN String Int
|
||||
| NS (List String) Name
|
||||
|
||||
public export
|
||||
data Count = M0 | M1 | MW
|
||||
|
||||
public export
|
||||
data PiInfo = ImplicitArg | ExplicitArg | AutoImplicit
|
||||
|
||||
public export
|
||||
data 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 export
|
||||
data LazyReason = LInf | LLazy | LUnknown
|
||||
|
||||
-- Type checked terms in the core TT
|
||||
public export
|
||||
data TT : List Name -> Type where
|
||||
Local : FC -> (idx : Nat) -> (n : Name) ->
|
||||
(0 prf : IsVar name idx vars) -> TT vars
|
||||
Ref : FC -> NameType -> Name -> TT vars
|
||||
Pi : FC -> Count -> PiInfo ->
|
||||
(x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) ->
|
||||
TT vars
|
||||
Lam : FC -> Count -> PiInfo ->
|
||||
(x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) ->
|
||||
TT vars
|
||||
App : FC -> TT vars -> TT vars -> TT vars
|
||||
TDelayed : FC -> LazyReason -> TT vars -> TT vars
|
||||
TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars
|
||||
TForce : FC -> TT vars -> TT vars
|
||||
PrimVal : FC -> Constant -> TT vars
|
||||
Erased : FC -> TT vars
|
||||
TType : FC -> TT vars
|
||||
|
||||
public export
|
||||
data Visibility = Private | Export | Public
|
||||
|
||||
143
libs/base/Language/Reflection/TTImp.idr
Normal file
143
libs/base/Language/Reflection/TTImp.idr
Normal file
@ -0,0 +1,143 @@
|
||||
module Language.Reflection.TTImp
|
||||
|
||||
import Language.Reflection.TT
|
||||
|
||||
-- Unchecked terms and declarations in the intermediate language
|
||||
mutual
|
||||
public export
|
||||
data BindMode = PI Count | PATTERN | NONE
|
||||
|
||||
-- For as patterns matching linear arguments, select which side is
|
||||
-- consumed
|
||||
public export
|
||||
data UseSide = UseLeft | UseRight
|
||||
|
||||
public export
|
||||
data TTImp : Type where
|
||||
IVar : FC -> Name -> TTImp
|
||||
IPi : FC -> Count -> PiInfo -> Maybe Name ->
|
||||
(argTy : TTImp) -> (retTy : TTImp) -> TTImp
|
||||
ILam : FC -> Count -> PiInfo -> Maybe Name ->
|
||||
(argTy : TTImp) -> (lamTy : TTImp) -> TTImp
|
||||
ILet : FC -> Count -> Name ->
|
||||
(nTy : TTImp) -> (nVal : TTImp) ->
|
||||
(scope : TTImp) -> TTImp
|
||||
ICase : FC -> TTImp -> (ty : TTImp) ->
|
||||
List Clause -> TTImp
|
||||
ILocal : FC -> List Decl -> TTImp -> TTImp
|
||||
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
|
||||
|
||||
IApp : FC -> TTImp -> TTImp -> TTImp
|
||||
IImplicitApp : FC -> TTImp -> Maybe Name -> TTImp -> TTImp
|
||||
IWithApp : FC -> TTImp -> TTImp -> TTImp
|
||||
|
||||
ISearch : FC -> (depth : Nat) -> TTImp
|
||||
IAlternative : FC -> AltType -> List TTImp -> TTImp
|
||||
IRewrite : FC -> TTImp -> TTImp -> TTImp
|
||||
|
||||
-- Any implicit bindings in the scope should be bound here, using
|
||||
-- the given binder
|
||||
IBindHere : FC -> BindMode -> TTImp -> TTImp
|
||||
-- A name which should be implicitly bound
|
||||
IBindVar : FC -> String -> TTImp
|
||||
-- An 'as' pattern, valid on the LHS of a clause only
|
||||
IAs : FC -> UseSide -> Name -> TTImp -> TTImp
|
||||
-- A 'dot' pattern, i.e. one which must also have the given value
|
||||
-- by unification
|
||||
IMustUnify : FC -> (reason : String) -> TTImp -> TTImp
|
||||
|
||||
-- Laziness annotations
|
||||
IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type
|
||||
IDelay : FC -> TTImp -> TTImp -- delay constructor
|
||||
IForce : FC -> TTImp -> TTImp
|
||||
|
||||
IPrimVal : FC -> (c : Constant) -> TTImp
|
||||
IType : FC -> TTImp
|
||||
IHole : FC -> String -> TTImp
|
||||
|
||||
-- An implicit value, solved by unification, but which will also be
|
||||
-- bound (either as a pattern variable or a type variable) if unsolved
|
||||
-- at the end of elaborator
|
||||
Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
|
||||
|
||||
public export
|
||||
data IFieldUpdate : Type where
|
||||
ISetField : (path : List String) -> TTImp -> IFieldUpdate
|
||||
ISetFieldApp : (path : List String) -> TTImp -> IFieldUpdate
|
||||
|
||||
public export
|
||||
data AltType : Type where
|
||||
FirstSuccess : AltType
|
||||
Unique : AltType
|
||||
UniqueDefault : TTImp -> AltType
|
||||
|
||||
public export
|
||||
data FnOpt : Type where
|
||||
Inline : FnOpt
|
||||
-- Flag means the hint is a direct hint, not a function which might
|
||||
-- find the result (e.g. chasing parent interface dictionaries)
|
||||
Hint : Bool -> FnOpt
|
||||
-- Flag means to use as a default if all else fails
|
||||
GlobalHint : Bool -> FnOpt
|
||||
ExternFn : FnOpt
|
||||
-- Defined externally, list calling conventions
|
||||
ForeignFn : List String -> FnOpt
|
||||
-- assume safe to cancel arguments in unification
|
||||
Invertible : FnOpt
|
||||
Total : FnOpt
|
||||
Covering : FnOpt
|
||||
PartialOK : FnOpt
|
||||
Macro : FnOpt
|
||||
|
||||
public export
|
||||
data ITy : Type where
|
||||
MkTy : FC -> (n : Name) -> (ty : TTImp) -> ITy
|
||||
|
||||
public export
|
||||
data DataOpt : Type where
|
||||
SearchBy : List Name -> DataOpt -- determining arguments
|
||||
NoHints : DataOpt -- Don't generate search hints for constructors
|
||||
|
||||
public export
|
||||
data Data : Type where
|
||||
MkData : FC -> (n : Name) -> (tycon : TTImp) ->
|
||||
(opts : List DataOpt) ->
|
||||
(datacons : List ITy) -> Data
|
||||
MkLater : FC -> (n : Name) -> (tycon : TTImp) -> Data
|
||||
|
||||
public export
|
||||
data IField : Type where
|
||||
MkIField : FC -> Count -> PiInfo -> Name -> TTImp ->
|
||||
IField
|
||||
|
||||
public export
|
||||
data Record : Type where
|
||||
MkRecord : FC -> (n : Name) ->
|
||||
(params : List (Name, TTImp)) ->
|
||||
(conName : Maybe Name) ->
|
||||
(fields : List IField) ->
|
||||
Record
|
||||
|
||||
public export
|
||||
data Clause : Type where
|
||||
PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
|
||||
WithClause : FC -> (lhs : TTImp) -> (wval : TTImp) ->
|
||||
List Clause -> Clause
|
||||
ImpossibleClause : FC -> (lhs : TTImp) -> Clause
|
||||
|
||||
public export
|
||||
data Decl : Type where
|
||||
IClaim : FC -> Count -> Visibility -> List FnOpt ->
|
||||
ITy -> Decl
|
||||
IData : FC -> Visibility -> Data -> Decl
|
||||
IDef : FC -> Name -> List Clause -> Decl
|
||||
IParameters : FC -> List (Name, TTImp) ->
|
||||
List Decl -> Decl
|
||||
IRecord : FC -> Visibility -> Record -> Decl
|
||||
INamespace : FC ->
|
||||
(nested : Bool) ->
|
||||
-- ^ if True, parent namespaces in the same file can also
|
||||
-- look inside and see private/export names in full
|
||||
List String -> List Decl -> Decl
|
||||
ITransform : FC -> TTImp -> TTImp -> Decl
|
||||
ILog : Nat -> Decl
|
||||
@ -25,6 +25,8 @@ modules = Control.Monad.Identity,
|
||||
Decidable.Equality,
|
||||
|
||||
Language.Reflection,
|
||||
Language.Reflection.TT,
|
||||
Language.Reflection.TTImp,
|
||||
|
||||
System,
|
||||
System.Concurrency.Raw,
|
||||
|
||||
@ -118,6 +118,7 @@ data DefFlag
|
||||
-- care!
|
||||
| SetTotal TotalReq
|
||||
| BlockedHint -- a hint, but blocked for the moment (so don't use)
|
||||
| Macro
|
||||
|
||||
export
|
||||
Eq TotalReq where
|
||||
@ -134,6 +135,7 @@ Eq DefFlag where
|
||||
(==) TCInline TCInline = True
|
||||
(==) (SetTotal x) (SetTotal y) = x == y
|
||||
(==) BlockedHint BlockedHint = True
|
||||
(==) Macro Macro = True
|
||||
(==) _ _ = False
|
||||
|
||||
public export
|
||||
|
||||
@ -47,6 +47,14 @@ export
|
||||
reflection : String -> Name
|
||||
reflection n = NS ["Reflection", "Language"] (UN n)
|
||||
|
||||
export
|
||||
reflectiontt : String -> Name
|
||||
reflectiontt n = NS ["TT", "Reflection", "Language"] (UN n)
|
||||
|
||||
export
|
||||
reflectionttimp : String -> Name
|
||||
reflectionttimp n = NS ["TTImp", "Reflection", "Language"] (UN n)
|
||||
|
||||
export
|
||||
cantReify : NF vars -> String -> Core a
|
||||
cantReify val ty
|
||||
@ -206,15 +214,15 @@ export
|
||||
Reflect Name where
|
||||
reflect fc defs env (UN x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "UN") [x']
|
||||
appCon fc defs (reflectiontt "UN") [x']
|
||||
reflect fc defs env (MN x i)
|
||||
= do x' <- reflect fc defs env x
|
||||
i' <- reflect fc defs env i
|
||||
appCon fc defs (reflection "MN") [x', i']
|
||||
appCon fc defs (reflectiontt "MN") [x', i']
|
||||
reflect fc defs env (NS ns n)
|
||||
= do ns' <- reflect fc defs env ns
|
||||
n' <- reflect fc defs env n
|
||||
appCon fc defs (reflection "NS") [ns', n']
|
||||
appCon fc defs (reflectiontt "NS") [ns', n']
|
||||
reflect fc defs env val = cantReflect fc "Name"
|
||||
|
||||
export
|
||||
@ -235,16 +243,16 @@ Reify NameType where
|
||||
|
||||
export
|
||||
Reflect NameType where
|
||||
reflect fc defs env Bound = getCon fc defs (reflection "Bound")
|
||||
reflect fc defs env Func = getCon fc defs (reflection "Func")
|
||||
reflect fc defs env Bound = getCon fc defs (reflectiontt "Bound")
|
||||
reflect fc defs env Func = getCon fc defs (reflectiontt "Func")
|
||||
reflect fc defs env (DataCon t i)
|
||||
= do t' <- reflect fc defs env t
|
||||
i' <- reflect fc defs env i
|
||||
appCon fc defs (reflection "DataCon") [t', i']
|
||||
appCon fc defs (reflectiontt "DataCon") [t', i']
|
||||
reflect fc defs env (TyCon t i)
|
||||
= do t' <- reflect fc defs env t
|
||||
i' <- reflect fc defs env i
|
||||
appCon fc defs (reflection "TyCon") [t', i']
|
||||
appCon fc defs (reflectiontt "TyCon") [t', i']
|
||||
|
||||
export
|
||||
Reify Constant where
|
||||
@ -283,33 +291,33 @@ export
|
||||
Reflect Constant where
|
||||
reflect fc defs env (I x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "I") [x']
|
||||
appCon fc defs (reflectiontt "I") [x']
|
||||
reflect fc defs env (BI x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "BI") [x']
|
||||
appCon fc defs (reflectiontt "BI") [x']
|
||||
reflect fc defs env (Str x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "Str") [x']
|
||||
appCon fc defs (reflectiontt "Str") [x']
|
||||
reflect fc defs env (Ch x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "Ch") [x']
|
||||
appCon fc defs (reflectiontt "Ch") [x']
|
||||
reflect fc defs env (Db x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "Db") [x']
|
||||
appCon fc defs (reflectiontt "Db") [x']
|
||||
reflect fc defs env WorldVal
|
||||
= getCon fc defs (reflection "WorldVal")
|
||||
= getCon fc defs (reflectiontt "WorldVal")
|
||||
reflect fc defs env IntType
|
||||
= getCon fc defs (reflection "IntTyoe")
|
||||
= getCon fc defs (reflectiontt "IntTyoe")
|
||||
reflect fc defs env IntegerType
|
||||
= getCon fc defs (reflection "IntegerType")
|
||||
= getCon fc defs (reflectiontt "IntegerType")
|
||||
reflect fc defs env StringType
|
||||
= getCon fc defs (reflection "StringType")
|
||||
= getCon fc defs (reflectiontt "StringType")
|
||||
reflect fc defs env CharType
|
||||
= getCon fc defs (reflection "CharType")
|
||||
= getCon fc defs (reflectiontt "CharType")
|
||||
reflect fc defs env DoubleType
|
||||
= getCon fc defs (reflection "DoubleTyoe")
|
||||
= getCon fc defs (reflectiontt "DoubleTyoe")
|
||||
reflect fc defs env WorldType
|
||||
= getCon fc defs (reflection "WorldType")
|
||||
= getCon fc defs (reflectiontt "WorldType")
|
||||
|
||||
export
|
||||
Reify Visibility where
|
||||
@ -323,9 +331,9 @@ Reify Visibility where
|
||||
|
||||
export
|
||||
Reflect Visibility where
|
||||
reflect fc defs env Private = getCon fc defs (reflection "Private")
|
||||
reflect fc defs env Export = getCon fc defs (reflection "Export")
|
||||
reflect fc defs env Public = getCon fc defs (reflection "Public")
|
||||
reflect fc defs env Private = getCon fc defs (reflectiontt "Private")
|
||||
reflect fc defs env Export = getCon fc defs (reflectiontt "Export")
|
||||
reflect fc defs env Public = getCon fc defs (reflectiontt "Public")
|
||||
|
||||
export
|
||||
Reify RigCount where
|
||||
@ -339,9 +347,9 @@ Reify RigCount where
|
||||
|
||||
export
|
||||
Reflect RigCount where
|
||||
reflect fc defs env Rig0 = getCon fc defs (reflection "M0")
|
||||
reflect fc defs env Rig1 = getCon fc defs (reflection "M1")
|
||||
reflect fc defs env RigW = getCon fc defs (reflection "MW")
|
||||
reflect fc defs env Rig0 = getCon fc defs (reflectiontt "M0")
|
||||
reflect fc defs env Rig1 = getCon fc defs (reflectiontt "M1")
|
||||
reflect fc defs env RigW = getCon fc defs (reflectiontt "MW")
|
||||
|
||||
export
|
||||
Reify PiInfo where
|
||||
@ -355,9 +363,9 @@ Reify PiInfo where
|
||||
|
||||
export
|
||||
Reflect PiInfo where
|
||||
reflect fc defs env Implicit = getCon fc defs (reflection "ImplicitArg")
|
||||
reflect fc defs env Explicit = getCon fc defs (reflection "ExplicitArg")
|
||||
reflect fc defs env AutoImplicit = getCon fc defs (reflection "AutoImplicit")
|
||||
reflect fc defs env Implicit = getCon fc defs (reflectiontt "ImplicitArg")
|
||||
reflect fc defs env Explicit = getCon fc defs (reflectiontt "ExplicitArg")
|
||||
reflect fc defs env AutoImplicit = getCon fc defs (reflectiontt "AutoImplicit")
|
||||
|
||||
export
|
||||
Reify LazyReason where
|
||||
@ -371,9 +379,9 @@ Reify LazyReason where
|
||||
|
||||
export
|
||||
Reflect LazyReason where
|
||||
reflect fc defs env LInf = getCon fc defs (reflection "LInf")
|
||||
reflect fc defs env LLazy = getCon fc defs (reflection "LLazy")
|
||||
reflect fc defs env LUnknown = getCon fc defs (reflection "LUnknown")
|
||||
reflect fc defs env LInf = getCon fc defs (reflectiontt "LInf")
|
||||
reflect fc defs env LLazy = getCon fc defs (reflectiontt "LLazy")
|
||||
reflect fc defs env LUnknown = getCon fc defs (reflectiontt "LUnknown")
|
||||
|
||||
export
|
||||
Reify FC where
|
||||
@ -392,8 +400,8 @@ Reflect FC where
|
||||
= do fn' <- reflect fc defs env fn
|
||||
start' <- reflect fc defs env start
|
||||
end' <- reflect fc defs env end
|
||||
appCon fc defs (reflection "MkFC") [fn', start', end']
|
||||
reflect fc defs env EmptyFC = getCon fc defs (reflection "EmptyFC")
|
||||
appCon fc defs (reflectiontt "MkFC") [fn', start', end']
|
||||
reflect fc defs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC")
|
||||
|
||||
-- Reflection of well typed terms: We don't reify terms because that involves
|
||||
-- type checking, but we can reflect them
|
||||
@ -401,10 +409,10 @@ Reflect FC where
|
||||
export
|
||||
Reflect (IsVar name idx vs) where
|
||||
reflect fc defs env First
|
||||
= appCon fc defs (reflection "First") [Erased fc, Erased fc]
|
||||
= appCon fc defs (reflectiontt "First") [Erased fc, Erased fc]
|
||||
reflect fc defs env (Later p)
|
||||
= do p' <- reflect fc defs env p
|
||||
appCon fc defs (reflection "Later")
|
||||
appCon fc defs (reflectiontt "Later")
|
||||
[Erased fc, Erased fc, Erased fc, Erased fc, p']
|
||||
|
||||
-- Assume terms are normalised so there's not Let bindings in particular
|
||||
@ -415,13 +423,13 @@ Reflect (Term vs) where
|
||||
lfc' <- reflect fc defs env lfc
|
||||
idx' <- reflect fc defs env idx
|
||||
prf' <- reflect fc defs env prf
|
||||
appCon fc defs (reflection "Local")
|
||||
appCon fc defs (reflectiontt "Local")
|
||||
[Erased fc, Erased fc, lfc', idx', prf']
|
||||
reflect fc defs env (Ref rfc nt n)
|
||||
= do rfc' <- reflect fc defs env rfc
|
||||
nt' <- reflect fc defs env nt
|
||||
n' <- reflect fc defs env n
|
||||
appCon fc defs (reflection "Ref")
|
||||
appCon fc defs (reflectiontt "Ref")
|
||||
[Erased fc, rfc', nt', n']
|
||||
reflect fc defs env (Bind bfc x (Pi c p ty) sc)
|
||||
= do bfc' <- reflect fc defs env bfc
|
||||
@ -430,7 +438,7 @@ Reflect (Term vs) where
|
||||
p' <- reflect fc defs env p
|
||||
ty' <- reflect fc defs env ty
|
||||
sc' <- reflect fc defs env sc
|
||||
appCon fc defs (reflection "Pi")
|
||||
appCon fc defs (reflectiontt "Pi")
|
||||
[Erased fc, bfc', c', p', x', ty', sc']
|
||||
reflect fc defs env (Bind bfc x (Lam c p ty) sc)
|
||||
= do bfc' <- reflect fc defs env bfc
|
||||
@ -439,45 +447,45 @@ Reflect (Term vs) where
|
||||
p' <- reflect fc defs env p
|
||||
ty' <- reflect fc defs env ty
|
||||
sc' <- reflect fc defs env sc
|
||||
appCon fc defs (reflection "Lam")
|
||||
appCon fc defs (reflectiontt "Lam")
|
||||
[Erased fc, bfc', c', p', x', ty', sc']
|
||||
reflect fc defs env (App afc fn arg)
|
||||
= do afc' <- reflect fc defs env afc
|
||||
fn' <- reflect fc defs env fn
|
||||
arg' <- reflect fc defs env arg
|
||||
appCon fc defs (reflection "App")
|
||||
appCon fc defs (reflectiontt "App")
|
||||
[Erased fc, afc', fn', arg']
|
||||
reflect fc defs env (TDelayed dfc r tm)
|
||||
= do dfc' <- reflect fc defs env dfc
|
||||
r' <- reflect fc defs env r
|
||||
tm' <- reflect fc defs env tm
|
||||
appCon fc defs (reflection "TDelayed")
|
||||
appCon fc defs (reflectiontt "TDelayed")
|
||||
[Erased fc, dfc', r', tm']
|
||||
reflect fc defs env (TDelay dfc r ty tm)
|
||||
= do dfc' <- reflect fc defs env dfc
|
||||
r' <- reflect fc defs env r
|
||||
ty' <- reflect fc defs env ty
|
||||
tm' <- reflect fc defs env tm
|
||||
appCon fc defs (reflection "TDelay")
|
||||
appCon fc defs (reflectiontt "TDelay")
|
||||
[Erased fc, dfc', r', ty', tm']
|
||||
reflect fc defs env (TForce dfc r tm)
|
||||
= do dfc' <- reflect fc defs env dfc
|
||||
r' <- reflect fc defs env r
|
||||
tm' <- reflect fc defs env tm
|
||||
appCon fc defs (reflection "TForce")
|
||||
appCon fc defs (reflectiontt "TForce")
|
||||
[Erased fc, r', dfc', tm']
|
||||
reflect fc defs env (PrimVal pfc c)
|
||||
= do pfc' <- reflect fc defs env pfc
|
||||
c' <- reflect fc defs env c
|
||||
appCon fc defs (reflection "PrimVal")
|
||||
appCon fc defs (reflectiontt "PrimVal")
|
||||
[Erased fc, pfc', c']
|
||||
reflect fc defs env (Erased efc)
|
||||
= do efc' <- reflect fc defs env efc
|
||||
appCon fc defs (reflection "Erased")
|
||||
appCon fc defs (reflectiontt "Erased")
|
||||
[Erased fc, efc']
|
||||
reflect fc defs env (TType tfc)
|
||||
= do tfc' <- reflect fc defs env tfc
|
||||
appCon fc defs (reflection "TType")
|
||||
appCon fc defs (reflectiontt "TType")
|
||||
[Erased fc, tfc']
|
||||
reflect fc defs env val = cantReflect fc "Term"
|
||||
|
||||
|
||||
@ -805,6 +805,7 @@ TTC DefFlag where
|
||||
toBuf b TCInline = tag 5
|
||||
toBuf b (SetTotal x) = do tag 6; toBuf b x
|
||||
toBuf b BlockedHint = tag 7
|
||||
toBuf b Macro = tag 8
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
@ -814,6 +815,7 @@ TTC DefFlag where
|
||||
5 => pure TCInline
|
||||
6 => do x <- fromBuf b; pure (SetTotal x)
|
||||
7 => pure BlockedHint
|
||||
8 => pure Macro
|
||||
_ => corrupt "DefFlag"
|
||||
|
||||
export
|
||||
|
||||
@ -1025,6 +1025,8 @@ fnDirectOpt
|
||||
pure Inline
|
||||
<|> do exactIdent "extern"
|
||||
pure ExternFn
|
||||
<|> do exactIdent "macro"
|
||||
pure Macro
|
||||
<|> do exactIdent "foreign"
|
||||
cs <- many strLit
|
||||
pure (ForeignFn cs)
|
||||
|
||||
@ -52,6 +52,8 @@ processFnOpt fc ndef Covering
|
||||
= setFlag fc ndef (SetTotal CoveringOnly)
|
||||
processFnOpt fc ndef PartialOK
|
||||
= setFlag fc ndef (SetTotal PartialOK)
|
||||
processFnOpt fc ndef Macro
|
||||
= setFlag fc ndef Macro
|
||||
|
||||
-- If it's declared as externally defined, set the definition to
|
||||
-- ExternFn <arity>, where the arity is assumed to be fixed (i.e.
|
||||
|
||||
@ -26,11 +26,11 @@ export
|
||||
Reflect BindMode where
|
||||
reflect fc defs env (PI c)
|
||||
= do c' <- reflect fc defs env c
|
||||
appCon fc defs (reflection "PI") [c']
|
||||
appCon fc defs (reflectionttimp "PI") [c']
|
||||
reflect fc defs env PATTERN
|
||||
= getCon fc defs (reflection "PATTERN")
|
||||
= getCon fc defs (reflectionttimp "PATTERN")
|
||||
reflect fc defs env NONE
|
||||
= getCon fc defs (reflection "NONE")
|
||||
= getCon fc defs (reflectionttimp "NONE")
|
||||
|
||||
export
|
||||
Reify UseSide where
|
||||
@ -43,9 +43,9 @@ Reify UseSide where
|
||||
export
|
||||
Reflect UseSide where
|
||||
reflect fc defs env UseLeft
|
||||
= getCon fc defs (reflection "UseLeft")
|
||||
= getCon fc defs (reflectionttimp "UseLeft")
|
||||
reflect fc defs env UseRight
|
||||
= getCon fc defs (reflection "UseRight")
|
||||
= getCon fc defs (reflectionttimp "UseRight")
|
||||
|
||||
mutual
|
||||
export
|
||||
@ -220,6 +220,8 @@ mutual
|
||||
= pure Covering
|
||||
reify defs (NDCon _ (NS _ (UN "PartialOK")) _ _ _)
|
||||
= pure PartialOK
|
||||
reify defs (NDCon _ (NS _ (UN "Macro")) _ _ _)
|
||||
= pure Macro
|
||||
reify defs val = cantReify val "FnOpt"
|
||||
|
||||
export
|
||||
@ -348,7 +350,7 @@ mutual
|
||||
reflect fc defs env (IVar tfc n)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
n' <- reflect fc defs env n
|
||||
appCon fc defs (reflection "IVar") [fc', n']
|
||||
appCon fc defs (reflectionttimp "IVar") [fc', n']
|
||||
reflect fc defs env (IPi tfc c p mn aty rty)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
c' <- reflect fc defs env c
|
||||
@ -356,7 +358,7 @@ mutual
|
||||
mn' <- reflect fc defs env mn
|
||||
aty' <- reflect fc defs env aty
|
||||
rty' <- reflect fc defs env rty
|
||||
appCon fc defs (reflection "IPi") [fc', c', p', mn', aty', rty']
|
||||
appCon fc defs (reflectionttimp "IPi") [fc', c', p', mn', aty', rty']
|
||||
reflect fc defs env (ILam tfc c p mn aty rty)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
c' <- reflect fc defs env c
|
||||
@ -364,7 +366,7 @@ mutual
|
||||
mn' <- reflect fc defs env mn
|
||||
aty' <- reflect fc defs env aty
|
||||
rty' <- reflect fc defs env rty
|
||||
appCon fc defs (reflection "ILam") [fc', c', p', mn', aty', rty']
|
||||
appCon fc defs (reflectionttimp "ILam") [fc', c', p', mn', aty', rty']
|
||||
reflect fc defs env (ILet tfc c n aty aval sc)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
c' <- reflect fc defs env c
|
||||
@ -372,139 +374,140 @@ mutual
|
||||
aty' <- reflect fc defs env aty
|
||||
aval' <- reflect fc defs env aval
|
||||
sc' <- reflect fc defs env sc
|
||||
appCon fc defs (reflection "ILet") [fc', c', n', aty', aval', sc']
|
||||
appCon fc defs (reflectionttimp "ILet") [fc', c', n', aty', aval', sc']
|
||||
reflect fc defs env (ICase tfc sc ty cs)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
sc' <- reflect fc defs env sc
|
||||
ty' <- reflect fc defs env ty
|
||||
cs' <- reflect fc defs env cs
|
||||
appCon fc defs (reflection "ICase") [fc', sc', ty', cs']
|
||||
appCon fc defs (reflectionttimp "ICase") [fc', sc', ty', cs']
|
||||
reflect fc defs env (ILocal tfc ds sc)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
ds' <- reflect fc defs env ds
|
||||
sc' <- reflect fc defs env sc
|
||||
appCon fc defs (reflection "ILocal") [fc', ds', sc']
|
||||
appCon fc defs (reflectionttimp "ILocal") [fc', ds', sc']
|
||||
reflect fc defs env (IUpdate tfc ds sc)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
ds' <- reflect fc defs env ds
|
||||
sc' <- reflect fc defs env sc
|
||||
appCon fc defs (reflection "IUpdate") [fc', ds', sc']
|
||||
appCon fc defs (reflectionttimp "IUpdate") [fc', ds', sc']
|
||||
reflect fc defs env (IApp tfc f a)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
f' <- reflect fc defs env f
|
||||
a' <- reflect fc defs env a
|
||||
appCon fc defs (reflection "IApp") [fc', f', a']
|
||||
appCon fc defs (reflectionttimp "IApp") [fc', f', a']
|
||||
reflect fc defs env (IImplicitApp tfc f m a)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
f' <- reflect fc defs env f
|
||||
m' <- reflect fc defs env m
|
||||
a' <- reflect fc defs env a
|
||||
appCon fc defs (reflection "IImplicitApp") [fc', f', m', a']
|
||||
appCon fc defs (reflectionttimp "IImplicitApp") [fc', f', m', a']
|
||||
reflect fc defs env (IWithApp tfc f a)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
f' <- reflect fc defs env f
|
||||
a' <- reflect fc defs env a
|
||||
appCon fc defs (reflection "IWithApp") [fc', f', a']
|
||||
appCon fc defs (reflectionttimp "IWithApp") [fc', f', a']
|
||||
reflect fc defs env (ISearch tfc d)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
d' <- reflect fc defs env d
|
||||
appCon fc defs (reflection "ISearch") [fc', d']
|
||||
appCon fc defs (reflectionttimp "ISearch") [fc', d']
|
||||
reflect fc defs env (IAlternative tfc t as)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
t' <- reflect fc defs env t
|
||||
as' <- reflect fc defs env as
|
||||
appCon fc defs (reflection "IAlternative") [fc', t', as']
|
||||
appCon fc defs (reflectionttimp "IAlternative") [fc', t', as']
|
||||
reflect fc defs env (IRewrite tfc t sc)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
t' <- reflect fc defs env t
|
||||
sc' <- reflect fc defs env sc
|
||||
appCon fc defs (reflection "IRewrite") [fc', t', sc']
|
||||
appCon fc defs (reflectionttimp "IRewrite") [fc', t', sc']
|
||||
reflect fc defs env (ICoerced tfc d) = reflect fc defs env d
|
||||
reflect fc defs env (IBindHere tfc n sc)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
n' <- reflect fc defs env n
|
||||
sc' <- reflect fc defs env sc
|
||||
appCon fc defs (reflection "IBindHere") [fc', n', sc']
|
||||
appCon fc defs (reflectionttimp "IBindHere") [fc', n', sc']
|
||||
reflect fc defs env (IBindVar tfc n)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
n' <- reflect fc defs env n
|
||||
appCon fc defs (reflection "IBindVar") [fc', n']
|
||||
appCon fc defs (reflectionttimp "IBindVar") [fc', n']
|
||||
reflect fc defs env (IAs tfc s n t)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
s' <- reflect fc defs env s
|
||||
n' <- reflect fc defs env n
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "IAs") [fc', s', n', t']
|
||||
appCon fc defs (reflectionttimp "IAs") [fc', s', n', t']
|
||||
reflect fc defs env (IMustUnify tfc r t)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
r' <- reflect fc defs env r
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "IMustUnify") [fc', r', t']
|
||||
appCon fc defs (reflectionttimp "IMustUnify") [fc', r', t']
|
||||
reflect fc defs env (IDelayed tfc r t)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
r' <- reflect fc defs env r
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "IDelayed") [fc', r', t']
|
||||
appCon fc defs (reflectionttimp "IDelayed") [fc', r', t']
|
||||
reflect fc defs env (IDelay tfc t)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "IDelay") [fc', t']
|
||||
appCon fc defs (reflectionttimp "IDelay") [fc', t']
|
||||
reflect fc defs env (IForce tfc t)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "IForce") [fc', t']
|
||||
appCon fc defs (reflectionttimp "IForce") [fc', t']
|
||||
reflect fc defs env (IPrimVal tfc t)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "IPrimVal") [fc', t']
|
||||
appCon fc defs (reflectionttimp "IPrimVal") [fc', t']
|
||||
reflect fc defs env (IType tfc)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
appCon fc defs (reflection "IType") [fc']
|
||||
appCon fc defs (reflectionttimp "IType") [fc']
|
||||
reflect fc defs env (IHole tfc t)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "IHole") [fc', t']
|
||||
appCon fc defs (reflectionttimp "IHole") [fc', t']
|
||||
reflect fc defs env (Implicit tfc t)
|
||||
= do fc' <- reflect fc defs env tfc
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "Implicit") [fc', t']
|
||||
appCon fc defs (reflectionttimp "Implicit") [fc', t']
|
||||
|
||||
export
|
||||
Reflect IFieldUpdate where
|
||||
reflect fc defs env (ISetField p t)
|
||||
= do p' <- reflect fc defs env p
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "ISetField") [p', t']
|
||||
appCon fc defs (reflectionttimp "ISetField") [p', t']
|
||||
reflect fc defs env (ISetFieldApp p t)
|
||||
= do p' <- reflect fc defs env p
|
||||
t' <- reflect fc defs env t
|
||||
appCon fc defs (reflection "ISetFieldApp") [p', t']
|
||||
appCon fc defs (reflectionttimp "ISetFieldApp") [p', t']
|
||||
|
||||
export
|
||||
Reflect AltType where
|
||||
reflect fc defs env FirstSuccess = getCon fc defs (reflection "FirstSuccess")
|
||||
reflect fc defs env Unique = getCon fc defs (reflection "Unique")
|
||||
reflect fc defs env FirstSuccess = getCon fc defs (reflectionttimp "FirstSuccess")
|
||||
reflect fc defs env Unique = getCon fc defs (reflectionttimp "Unique")
|
||||
reflect fc defs env (UniqueDefault x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "UniqueDefault") [x']
|
||||
appCon fc defs (reflectionttimp "UniqueDefault") [x']
|
||||
|
||||
export
|
||||
Reflect FnOpt where
|
||||
reflect fc defs env Inline = getCon fc defs (reflection "FirstSuccess")
|
||||
reflect fc defs env Inline = getCon fc defs (reflectionttimp "FirstSuccess")
|
||||
reflect fc defs env (Hint x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "Hint") [x']
|
||||
appCon fc defs (reflectionttimp "Hint") [x']
|
||||
reflect fc defs env (GlobalHint x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "GlobalHint") [x']
|
||||
reflect fc defs env ExternFn = getCon fc defs (reflection "ExternFn")
|
||||
appCon fc defs (reflectionttimp "GlobalHint") [x']
|
||||
reflect fc defs env ExternFn = getCon fc defs (reflectionttimp "ExternFn")
|
||||
reflect fc defs env (ForeignFn x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "ForeignFn") [x']
|
||||
reflect fc defs env Invertible = getCon fc defs (reflection "Invertible")
|
||||
reflect fc defs env Total = getCon fc defs (reflection "Total")
|
||||
reflect fc defs env Covering = getCon fc defs (reflection "Covering")
|
||||
reflect fc defs env PartialOK = getCon fc defs (reflection "PartialOK")
|
||||
appCon fc defs (reflectionttimp "ForeignFn") [x']
|
||||
reflect fc defs env Invertible = getCon fc defs (reflectionttimp "Invertible")
|
||||
reflect fc defs env Total = getCon fc defs (reflectionttimp "Total")
|
||||
reflect fc defs env Covering = getCon fc defs (reflectionttimp "Covering")
|
||||
reflect fc defs env PartialOK = getCon fc defs (reflectionttimp "PartialOK")
|
||||
reflect fc defs env Macro = getCon fc defs (reflectionttimp "Macro")
|
||||
|
||||
export
|
||||
Reflect ImpTy where
|
||||
@ -512,14 +515,14 @@ mutual
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "MkTy") [x', y', z']
|
||||
appCon fc defs (reflectionttimp "MkTy") [x', y', z']
|
||||
|
||||
export
|
||||
Reflect DataOpt where
|
||||
reflect fc defs env (SearchBy x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "SearchBy") [x']
|
||||
reflect fc defs env NoHints = getCon fc defs (reflection "NoHints")
|
||||
appCon fc defs (reflectionttimp "SearchBy") [x']
|
||||
reflect fc defs env NoHints = getCon fc defs (reflectionttimp "NoHints")
|
||||
|
||||
export
|
||||
Reflect ImpData where
|
||||
@ -529,12 +532,12 @@ mutual
|
||||
x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "MkData") [v', w', x', y', z']
|
||||
appCon fc defs (reflectionttimp "MkData") [v', w', x', y', z']
|
||||
reflect fc defs env (MkImpLater x y z)
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "MkLater") [x', y', z']
|
||||
appCon fc defs (reflectionttimp "MkLater") [x', y', z']
|
||||
|
||||
export
|
||||
Reflect IField where
|
||||
@ -544,7 +547,7 @@ mutual
|
||||
x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "MkIField") [v', w', x', y', z']
|
||||
appCon fc defs (reflectionttimp "MkIField") [v', w', x', y', z']
|
||||
|
||||
export
|
||||
Reflect ImpRecord where
|
||||
@ -554,7 +557,7 @@ mutual
|
||||
x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "MkRecord") [v', w', x', y', z']
|
||||
appCon fc defs (reflectionttimp "MkRecord") [v', w', x', y', z']
|
||||
|
||||
export
|
||||
Reflect ImpClause where
|
||||
@ -562,17 +565,17 @@ mutual
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "PatClause") [x', y', z']
|
||||
appCon fc defs (reflectionttimp "PatClause") [x', y', z']
|
||||
reflect fc defs env (WithClause w x y z)
|
||||
= do w' <- reflect fc defs env x
|
||||
x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "WithClause") [w', x', y', z']
|
||||
appCon fc defs (reflectionttimp "WithClause") [w', x', y', z']
|
||||
reflect fc defs env (ImpossibleClause x y)
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
appCon fc defs (reflection "ImpossibleClause") [x', y']
|
||||
appCon fc defs (reflectionttimp "ImpossibleClause") [x', y']
|
||||
|
||||
export
|
||||
Reflect ImpDecl where
|
||||
@ -582,42 +585,42 @@ mutual
|
||||
x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "IClaim") [v', w', x', y', z']
|
||||
appCon fc defs (reflectionttimp "IClaim") [v', w', x', y', z']
|
||||
reflect fc defs env (IData x y z)
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "IData") [x', y', z']
|
||||
appCon fc defs (reflectionttimp "IData") [x', y', z']
|
||||
reflect fc defs env (IDef x y z)
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "IDef") [x', y', z']
|
||||
appCon fc defs (reflectionttimp "IDef") [x', y', z']
|
||||
reflect fc defs env (IParameters x y z)
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "IParameters") [x', y', z']
|
||||
appCon fc defs (reflectionttimp "IParameters") [x', y', z']
|
||||
reflect fc defs env (IRecord x y z)
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "IRecord") [x', y', z']
|
||||
appCon fc defs (reflectionttimp "IRecord") [x', y', z']
|
||||
reflect fc defs env (INamespace w x y z)
|
||||
= do w' <- reflect fc defs env w
|
||||
x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "INamespace") [w', x', y', z']
|
||||
appCon fc defs (reflectionttimp "INamespace") [w', x', y', z']
|
||||
reflect fc defs env (ITransform x y z)
|
||||
= do x' <- reflect fc defs env x
|
||||
y' <- reflect fc defs env y
|
||||
z' <- reflect fc defs env z
|
||||
appCon fc defs (reflection "ITransform") [x', y', z']
|
||||
appCon fc defs (reflectionttimp "ITransform") [x', y', z']
|
||||
reflect fc defs env (IPragma x)
|
||||
= throw (GenericMsg fc "Can't reflect a pragma")
|
||||
reflect fc defs env (ILog x)
|
||||
= do x' <- reflect fc defs env x
|
||||
appCon fc defs (reflection "ILog") [x']
|
||||
appCon fc defs (reflectionttimp "ILog") [x']
|
||||
|
||||
|
||||
|
||||
@ -170,6 +170,7 @@ mutual
|
||||
Total : FnOpt
|
||||
Covering : FnOpt
|
||||
PartialOK : FnOpt
|
||||
Macro : FnOpt
|
||||
|
||||
export
|
||||
Show FnOpt where
|
||||
@ -182,6 +183,7 @@ mutual
|
||||
show Total = "total"
|
||||
show Covering = "covering"
|
||||
show PartialOK = "partial"
|
||||
show Macro = "%macro"
|
||||
|
||||
export
|
||||
Eq FnOpt where
|
||||
@ -194,6 +196,7 @@ mutual
|
||||
Total == Total = True
|
||||
Covering == Covering = True
|
||||
PartialOK == PartialOK = True
|
||||
Macro == Macro = True
|
||||
_ == _ = False
|
||||
|
||||
public export
|
||||
@ -811,6 +814,7 @@ mutual
|
||||
toBuf b Total = tag 6
|
||||
toBuf b Covering = tag 7
|
||||
toBuf b PartialOK = tag 8
|
||||
toBuf b Macro = tag 9
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
@ -823,6 +827,7 @@ mutual
|
||||
6 => pure Total
|
||||
7 => pure Covering
|
||||
8 => pure PartialOK
|
||||
9 => pure Macro
|
||||
_ => corrupt "FnOpt"
|
||||
|
||||
export
|
||||
|
||||
Loading…
Reference in New Issue
Block a user