From c98166392b6c14622683d1c401e4da16db4c0546 Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Mon, 8 May 2023 15:13:46 +0200 Subject: [PATCH] Fixed desugar and made interpret --- src/Desugar/Desugar.hs | 2 +- test_program.crf | 99 ++++++++++++++++++++---------------------- 2 files changed, 47 insertions(+), 54 deletions(-) diff --git a/src/Desugar/Desugar.hs b/src/Desugar/Desugar.hs index 601f7da..7bcf417 100644 --- a/src/Desugar/Desugar.hs +++ b/src/Desugar/Desugar.hs @@ -68,7 +68,7 @@ desugarExp = \case -- EAbsS pat e -> EAbs (LIdent "$zz$") (ECase (EVar "$zz$") [Branch (desugarPattern pat) (desugarExp e)]) ELet b e -> ELet (desugarBind b) (desugarExp e) ECase e br -> ECase (desugarExp e) (map desugarBranch br) - EAnn e t -> EAnn (desugarExp e) t + EAnn e t -> EAnn (desugarExp e) (desugarType t) EVarS (VSymbol (Symbol symb)) -> EVar (LIdent $ fixName symb) EVarS (VIdent (LIdent ident)) -> EVar $ LIdent $ fixName ident EVar i -> EVar i diff --git a/test_program.crf b/test_program.crf index 3c7b31a..75ce82b 100644 --- a/test_program.crf +++ b/test_program.crf @@ -1,59 +1,52 @@ --- Peano naturals -data Nat where - Zero : Nat - Succ : Nat -> Nat +data Expr where + EInt : Int -> Expr + EBool : Bool -> Expr + EAdd : Expr -> Expr -> Expr + EAnd : Expr -> Expr -> Expr --- Returns 10_000 -main = toInt (fromInt 10000) +data Val where + VInt : Int -> Val + VBool : Bool -> Val --- Peano arithmetic -- +data Eval where + Just : Val -> Eval + Nothing : Eval --- Peano addition -add : Nat -> Nat -> Nat -add left right = case left of - Zero => right - Succ n => Succ (add n right) +interp : Expr -> Eval +interp e = case e of + EInt i => Just (VInt i) + EBool b => Just (VBool b) + EAdd e1 e2 => case interp e1 of + Just x => case x of + VInt i => case interp e2 of + Nothing => Nothing + Just y => case y of + VInt j => Just (VInt (i + j)) + _ => Nothing + _ => Nothing + Nothing => Nothing + EAnd e1 e2 => case interp e1 of + Just x => case x of + VBool i => case interp e2 of + Just y => case y of + VBool j => case i of + True => case j of + True => Just (VBool True) + _ => Just (VBool False) + _ => Just (VBool False) + Nothing => Nothing + _ => Nothing + Nothing => Nothing + --- Peano multiplication -mul : Nat -> Nat -> Nat -mul left right = case right of - Zero => Zero - Succ n => add left (mul left n) +readVal : Val -> Int +readVal v = case v of + VInt i => i + VBool a => case a of + True => 1 + False => 0 -eq : Nat -> Nat -> Nat -eq a b = case a of - Zero => case b of - Zero => Succ Zero - _ => Zero - Succ n => case b of - Zero => Zero - Succ m => eq n m +main = case interp (EAdd (EAdd (EInt 3) (EInt 5)) (EBool True)) of + Nothing => (0 - 1) + Just x => case x of -less : Nat -> Nat -> Nat -less a b = case a of - Zero => case b of - Zero => Zero - Succ n => Succ Zero - Succ n => case b of - Zero => Zero - Succ m => less n m - -greater : Nat -> Nat -> Nat -greater a b = case b of - Zero => case a of - Zero => Zero - Succ n => Succ Zero - Succ n => case a of - Zero => Zero - Succ m => less n m - --- Aux - -toInt : Nat -> Int -toInt a = case a of - Succ n => 1 + toInt n - Zero => 0 - -fromInt a = case a of - 0 => Zero - n => Succ (fromInt (a - 1))