Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
module Core.SExpr where
import Prelude
import Data.List (List(..))
import Data.Maybe (Maybe(..))
import Data.Tuple (Tuple(..))
data SExpr
= Array (Array SExpr)
| Atom String
data Term
= Variable Int
| Universe
| FunctionType -- TODO
| FunctionTerm -- TODO
| FunctionElim { head :: Term, arguments :: Array { name :: String, term :: Term } }
| RecordType -- TODO
| RecordTerm -- TODO
| RecordElim { head :: Term, fieldName :: String }
| EqualType -- TODO
| EqualTerm -- TODO
| EqualElim { head :: Term } -- TODO
derive instance eqTerm :: Eq Term
data Value
= VNeutral Head Spine
| VUniverse
| VFunctionType -- TODO
| VFunctionTerm -- TODO
| VRecordType -- TODO
| VRecordTerm -- TODO
| VEqualType -- TODO
| VEqualTerm -- TODO
data Head
= HVariable Int
data Elim
= Function { name :: String, value :: Value }
| Record { fieldName :: String }
| Equal { head :: Term } -- TODO
type Spine =
Array Elim
type Context =
{ tys :: List Value
, values :: List Value
-- , literals :: String -> Type -> Maybe Term
}
check :: Context -> SExpr -> Value -> Maybe Term
check context term ty =
case term, ty of
Array [Atom "record.term", Array fields], RecordType -> ?todo
Array [Atom "function.term", Array parameters, body], FunctionType -> ?todo
Array [Atom "equal.term", _], EqualType -> ?todo
term, ty -> do
{ term, ty: ty' } <- synth context term
if equal ty ty' then
Just term
else
Nothing
synth :: Context -> SExpr -> Maybe { term :: Term, ty :: Value }
synth context term =
case term of
Array [Atom "variable", Atom name] -> ?todo
Array [Atom "the", ty, term] -> do
ty <- check context ty VUniverse
term <- check context term ty
Just { term, ty }
Array [Atom "let", Array items, body] -> ?todo
Array [Atom "record.type", Array fields] -> ?todo
Array [Atom "record.elim", head, Atom field] -> do
{ term: head, ty: headTy } <- synth context head
case headTy of
RecordType -> ?todo
_ -> Nothing
Array [Atom "function.type", Array parameters, body] -> ?todo
Array [Atom "function.elim", head, Array arguments] -> do
{ term: head, ty: headTy } <- synth context head
case headTy of
FunctionType -> ?todo
_ -> Nothing
Array [Atom "equal.type", lhs, rhs] -> ?todo
Array [Atom "equal.elim", head, lhs, rhs] -> do
{ term: head, ty: headTy } <- synth context head
case headTy of
EqualElim -> ?todo
_ -> Nothing
Array _ -> ?todo
Atom _ -> ?todo
eval :: List Value -> Term -> Value
eval env term =
case term of
Variable index -> ?todo
Universe -> VUniverse
FunctionType -> VFunctionType
FunctionTerm -> VFunctionTerm
FunctionElim { head, arguments } ->
case eval env head of
_ -> ?todo
RecordType -> VRecordType
RecordTerm -> VRecordTerm
RecordElim { head, fieldName } ->
case eval env head of
_ -> ?todo
EqualType -> VEqualType
EqualTerm -> VEqualTerm
EqualElim { head } -> ?todo
readbackNeutral :: Head -> Spine -> Term
readbackNeutral head spine =
?todo
equal :: Value -> Value -> Boolean
equal term0 term1 =
case term0, term1 of
VNeutral head0 spine0, VNeutral head1 spine1 ->
readbackNeutral head0 spine0 == readbackNeutral head1 spine1
VUniverse, VUniverse -> true
VFunctionType, VFunctionType -> true
VFunctionTerm, VFunctionTerm -> true
VRecordType, VRecordType -> true
VRecordTerm, VRecordTerm -> true
VEqualType, VEqualType -> true
VEqualTerm, VEqualTerm -> true
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.