reduction of lambda expressions

smucclaw · Sep 6, 2021 · a6917e3 · a6917e3
1 parent 6525c21
commit a6917e3
Show file tree

Hide file tree

Showing 4 changed files with 94 additions and 55 deletions.
diff --git a/exe/Main.hs b/exe/Main.hs
@@ -29,6 +29,7 @@ import Error (printError)
 import Data.Either (rights)
 
 import ToDA2 (createDSyaml)
+import TimedMC (runAut)
 
 readPrelude :: IO (NewProgram SRng)
 readPrelude = do
@@ -58,6 +59,7 @@ process args input = do
 
           case format args of
             Fast                     ->  pPrint tpAst
+            Faut                     ->  runAut (fmap typeAnnot tpAst)
             (Fgf GFOpts { gflang = gfl, showast = True } ) -> GF.nlgAST gfl tpAstNoSrc
             (Fgf GFOpts { gflang = gfl, showast = False} ) -> GF.nlg    gfl tpAstNoSrc
             Fsmt -> proveProgram tpAstNoSrc
@@ -73,7 +75,7 @@ process args input = do
       print err
 
 
-data Format   = Fast | Fgf GFOpts | Fscasp | Fsmt | Fyaml
+data Format   = Fast | Faut | Fgf GFOpts | Fscasp | Fsmt | Fyaml
  deriving Show
 
 --  l4 gf en          output english only
@@ -99,6 +101,7 @@ optsParse = InputOpts <$>
               subparser
                 ( command "gf"   (info gfSubparser gfHelper)
                <> command "ast"  (info (pure Fast) (progDesc "Show the AST in Haskell"))
+               <> command "aut"  (info (pure Faut) (progDesc "Automata-based operations"))
                <> command "scasp" (info (pure Fscasp) (progDesc "output to sCASP for DocAssemble purposes"))
                <> command "smt"   (info (pure Fsmt) (progDesc "Check assertion with SMT solver"))
                <> command "yaml" (info (pure Fyaml) (progDesc "output to YAML for DocAssemble purposes"))

diff --git a/src/Exec.hs b/src/Exec.hs
@@ -5,66 +5,80 @@ module Exec where
 import Data.List
 import Syntax
 import Typing
+import SyntaxManipulation (mkFunTp, abstractF)
 
-lift_uarith_op :: UArithOp -> Val -> Val
-lift_uarith_op u c = case (u, c) of
+liftUarithOp :: UArithOp -> Val -> Val
+liftUarithOp u c = case (u, c) of
   (UAminus, IntV i) -> IntV (- i)
   _ -> ErrV
 
-lift_ubool_op :: UBoolOp -> Val -> Val
-lift_ubool_op u c = case (u, c) of
+liftUboolOp :: UBoolOp -> Val -> Val
+liftUboolOp u c = case (u, c) of
   (UBnot, BoolV b) -> BoolV (not b)
   _ -> ErrV
 
-lift_unaop_expr :: UnaOp -> Expr Tp -> Expr Tp
-lift_unaop_expr uop e = case (uop, e) of
-  (UArith u, ValE t c) -> ValE t (lift_uarith_op u c)
-  (UBool u, ValE t c) -> ValE t (lift_ubool_op u c)
-  _ -> ValE ErrT ErrV
+liftUnaopExpr :: Tp () -> UnaOp -> EvalResult (Tp()) -> Expr (Tp())
+liftUnaopExpr t uop (ExprResult e) = case (uop, e) of
+  (UArith u, ValE _ c) -> ValE t (liftUarithOp u c)
+  (UBool u, ValE _ c) ->  ValE t (liftUboolOp u c)
+  _ -> UnaOpE t uop e
+liftUnaopExpr t uop clos = ValE ErrT ErrV
 
-barith_fun :: BArithOp -> Integer -> Integer -> Integer
-barith_fun ba = case ba of
+barithFun :: BArithOp -> Integer -> Integer -> Integer
+barithFun ba = case ba of
   BAadd -> (+)
   BAsub -> (-)
   BAmul -> (*)
   BAdiv -> (div)
   BAmod -> (mod)
 
-lift_barith_op :: BArithOp -> Val -> Val -> Val
-lift_barith_op ba c1 c2 = case (c1, c2) of
-  (IntV i1, IntV i2) -> IntV ((barith_fun ba) i1 i2)
+liftBarithOp :: BArithOp -> Val -> Val -> Val
+liftBarithOp ba c1 c2 = case (c1, c2) of
+  (IntV i1, IntV i2) -> IntV (barithFun ba i1 i2)
   _ -> ErrV
 
 
-lift_binop_expr :: BinOp -> Expr Tp -> Expr Tp -> Expr Tp
-lift_binop_expr bop e1 e2 = case (bop, e1, e2) of
-    (BArith ba, ValE t1 c1, ValE t2 c2) -> ValE (tpBarith t1 t2 ba) (lift_barith_op ba c1 c2)
+liftBinopExpr :: Tp() -> BinOp -> EvalResult (Tp()) -> EvalResult (Tp()) -> Expr (Tp())
+liftBinopExpr t bop (ExprResult e1) (ExprResult e2) = case (bop, e1, e2) of
+    (BArith ba, ValE t1 c1, ValE t2 c2) -> ValE t (liftBarithOp ba c1 c2)
+liftBinopExpr t bop _ _ = ValE ErrT ErrV
 
-constr_clos :: Tp -> Expr Tp -> Expr Tp -> Expr Tp
-constr_clos rtp f a = case f of
-  ClosE t cbd (FunE _ v _ e) -> ClosE rtp ((v, a):cbd) e
-  _ -> error "application of non-function"
 
--- Takes an expression and returns an evaluated expression.
--- An expression is evaluated if it is of the form
--- ValE t c : explicit value
--- ClosE t1 bd (FunE ...): closure
--- All closure expressions are supposed to be closure-evaluated,
--- which means that for every closure of the form (ClosE t1 cbd e),
--- the expressions in cbd are evaluated and the closures in cbd are closure-evaluated
-eval_expr :: [(VarName, Expr Tp)] -> Expr Tp -> Expr Tp
-eval_expr bd x = case x of
-  ValE t c -> ValE t c
-  -- TODO: take into account dB indices
-  VarE t v i ->
-    case lookup v bd of
-      Nothing -> ValE ErrT ErrV
-      Just e -> e
-  UnaOpE t uop e -> lift_unaop_expr uop (eval_expr bd e)
-  BinOpE t bop e1 e2 -> lift_binop_expr bop (eval_expr bd e1) (eval_expr bd e2)
-  AppE t f a -> eval_expr bd (constr_clos t (eval_expr bd f) (eval_expr bd a))
-  fe@(FunE t v tparam e) -> ClosE t [] fe
-  ClosE t cbd e -> case eval_expr (cbd ++ bd) e of
-    ve@(ValE _ _) -> ve
-    (ClosE t2 cbd2 e2) -> ClosE t (cbd2 ++ cbd) e2
+data EvalResult t
+  = ExprResult (Expr t)
+  | ClosResult [EvalResult t] (VarDecl t) (Expr t)
+    deriving (Eq, Ord, Show, Read)
+type ReductEnv t = [EvalResult t]
 
+lookupEnv :: Int -> ReductEnv t -> Maybe (EvalResult t)
+lookupEnv i env = if i < length env then Just (env!!i) else Nothing
+
+
+evalExpr :: ReductEnv (Tp()) -> Expr (Tp()) -> EvalResult (Tp())
+evalExpr env x = case x of
+  ValE t c -> ExprResult (ValE t c)
+  VarE t v@GlobalVar {} -> ExprResult (VarE t v)
+  VarE _t (LocalVar _vn i) ->
+    case lookupEnv i env of
+      Nothing -> ExprResult (ValE ErrT ErrV)
+      Just e ->  e
+  UnaOpE t uop e -> ExprResult (liftUnaopExpr t uop (evalExpr env e))
+  BinOpE t bop e1 e2 -> ExprResult (liftBinopExpr t bop (evalExpr env e1) (evalExpr env e2))
+  IfThenElseE t ec e1 e2 -> case evalExpr env ec of 
+    ExprResult (ValE _ (BoolV True)) -> evalExpr env e1
+    ExprResult (ValE _ (BoolV False)) -> evalExpr env e2
+    _ -> ExprResult (ValE ErrT ErrV)
+  AppE t f a ->
+    case evalExpr env f of
+      ExprResult fres -> evalExpr [evalExpr env a] fres
+      ClosResult clenv v fbd -> evalExpr (evalExpr env a:clenv) fbd
+  FunE t v e -> ClosResult env v e
+  e@QuantifE {} -> ExprResult e
+  _ -> undefined
+
+{-
+reduceExpr :: Expr (Tp()) -> Expr (Tp())
+reduceExpr e = case evalExpr [] e of
+  ExprResult er -> er
+  ClosResult clenv v er -> substClos clenv (abstractF [ v] er)
+-}
diff --git a/src/TimedMC.hs b/src/TimedMC.hs
@@ -6,9 +6,12 @@ module TimedMC where
 import Syntax
 import SyntaxManipulation (conjExpr, disjExpr, abstractQ, abstractF, liftVarBy, conjsExpr, applyVars, mkVarE, mkEq, mkFloatConst, mkFunTp, index, indexListFromTo, gteExpr, eqExpr, mkIntConst, implExpr)
 
-import PrintProg (renameAndPrintExpr)
+import PrintProg (renameAndPrintExpr, printExpr)
 import Data.List (find)
 import Data.Maybe (fromMaybe)
+import Text.Pretty.Simple (pPrint)
+import Exec (evalExpr,EvalResult (ExprResult))
+import Annotation (typeAnnot)
 
 data SMTFunDef t = SMTFunDef
     { nameOfSMTFun :: Var t
@@ -213,11 +216,31 @@ myTrans = Transition (Loc "loc0")
                 (Loc "loc1")
 
 myTA :: TA (Tp ())
-myTA = TA OkT "myTA" [Loc "loc0", Loc "loc1"] [] [Clock "c1", Clock "c2"] [myTrans] [Loc "loc0"] [(Loc "loc0", [ClConstr (Clock "c1") BClt 3]), (Loc "loc1", [ClConstr (Clock "c2") BClt 2])] []
+myTA = TA OkT "myTA" [Loc "loc0", Loc "loc1"] [] [Clock "c1", Clock "c2"] [myTrans] (Loc "loc0") [(Loc "loc0", [ClConstr (Clock "c1") BClt 3]), (Loc "loc1", [ClConstr (Clock "c2") BClt 2])] []
 
 constrActionTransitionTest :: String
 constrActionTransitionTest = renameAndPrintExpr [] (constrActionTransitions myTA mystv myclvs)
 
+locToStateVar :: Loc -> Var (Tp ())
+locToStateVar (Loc n) = LocalVar (QVarName integerT  n) 0
+
+clockToStateVar :: Clock -> Var (Tp ())
+clockToStateVar (Clock n) = LocalVar (QVarName integerT  n) 0
+
+constrAutTest :: TA (Tp ()) -> String
+constrAutTest ta = renameAndPrintExpr []
+  (constrActionTransitions ta (locToStateVar (initialLocOfTA ta)) (map clockToStateVar (clocksOfTA ta)))
+
+runAut :: NewProgram (Tp ()) -> IO ()
+--runAut prg = putStrLn $ unlines (map constrAutTest (automataOfNewProgram prg))
+runAut prg =
+  let a = head (assertionsOfNewProgram prg)
+      e = argOfExprAppE (exprOfAssertion a)
+      ev = evalExpr [] e
+  in  case ev of
+   ExprResult expr -> putStrLn  (printExpr expr)
+   cl -> pPrint cl
+
 -- >>> constrActionTransitionTest
 -- "( \\ st: Integer -> ( \\ c1: Time -> ( \\ c2: Time -> ( \\ st_0: Integer -> ( \\ c1_0: Time -> ( \\ c2_0: Time -> ((st@5==loc0)&&((st_0@2==loc1)&&(((c1@4>=3)&&True)&&(((c1_0@1==c1@4)&&(c2_0@0==0.0))&&(c2_0@0<2)))))))))))"
 

diff --git a/src/ToGF/NormalizeSyntax.hs b/src/ToGF/NormalizeSyntax.hs
@@ -14,7 +14,7 @@ normalizeQuantif (Rule ann nm instr decls ifE thenE) =
   where
     -- 1) Take care of existential quantification
     (newDecls, newIfE) = go ifE -- result of the recursion
-    go (QuantifE ann Ex varnm tp expr) = (VarDecl (annotOfQVarName varnm) (nameOfQVarName varnm) tp : newDs, newE)
+    go (QuantifE ann Ex v expr) = (v : newDs, newE)
       where
         (newDs, newE) = go expr
     go e = ([], e)
@@ -25,12 +25,12 @@ normalizeQuantif (Rule ann nm instr decls ifE thenE) =
     actuallyNewIfE = fromMaybe newIfE negApp
 
     forallRule :: HasDefault t => Expr t -> ([Rule t], Maybe (Expr t))
-    forallRule (QuantifE ann All name tp ifExp) = ([Rule ann Nothing [] vardecls ifExp thenExp], Just negThenExp)
+    forallRule (QuantifE ann All v ifExp) = ([Rule ann Nothing [] vardecls ifExp thenExp], Just negThenExp)
       where
-        vardecls = [VarDecl (annotOfQVarName name) (nameOfQVarName name) tp]
+        vardecls = [v]
         predName = extractName ifExp
         newPred = VarE ann (LocalVar (QVarName defaultVal predName) 1) -- TODO: make it actually unique
-        newArg = VarE ann (LocalVar name 0) 
+        newArg = VarE ann (LocalVar (QVarName defaultVal (nameOfVarDecl v)) 0) 
         thenExp = AppE ann newPred newArg
         negThenExp = negateExpr thenExp
     forallRule _ = ([], Nothing)
@@ -43,8 +43,8 @@ normalizeQuantifGF r = r { varDeclsOfRule = [],
     ifE = precondOfRule r
     decls = varDeclsOfRule r
     wrapInExistential [] e = e
-    wrapInExistential (VarDecl ann nm tp:xs) e = 
-      wrapInExistential xs (QuantifE ann Ex (QVarName ann nm) tp e)
+    wrapInExistential (v:xs) e = 
+      wrapInExistential xs (QuantifE (annotOfVarDecl v) Ex v e)
 negateExpr :: Expr t -> Expr t
 negateExpr e = UnaOpE (annotOfExpr e) (UBool UBnot) e
 
@@ -55,13 +55,12 @@ extractName (UnaOpE t u et) = show u ++ extractName et
 extractName (BinOpE t b et et4) = extractName et ++ "_" ++ extractName et4
 extractName (IfThenElseE t et et3 et4) = extractName et ++ "_" ++ extractName et3 ++ "_" ++ extractName et4
 extractName (AppE t et et3) = extractName et ++ "_" ++ extractName et3
-extractName (FunE t p t3 et) = extractName et
-extractName (QuantifE t q l_c t4 et) = extractName et
+extractName (FunE t v et) = extractName et
+extractName (QuantifE t q v et) = extractName et
 extractName (FldAccE t et f) = extractName et
 extractName (TupleE t l_et) = intercalate "_" (map extractName l_et)
 extractName (CastE t t2 et) = extractName et
 extractName (ListE t l l_et) = intercalate "_" (map extractName l_et)
-extractName (NotDeriv _ _ et) = extractName et
 
 -- Nested binary ands into a single AndList
 normalizeAndExpr :: Expr t -> Expr t