added final types to web app

one-sided-defs/Environment.hs

@@ -9,6 +9,7 @@ module Environment (
   lookupMRec,
   getTypeNames,
   getXtorNames,
+  getTypes,
   emptyEnv,
   addDeclEnv,
   addVarEnv,
@@ -17,6 +18,7 @@ module Environment (
 
 import Syntax.Typed.Program 
 import Syntax.Typed.Terms
+import Syntax.Typed.Types
 import Errors 
 import Common
 import Loc
@@ -39,6 +41,16 @@ xtorErr loc xtn = toError loc ("Xtor " <> show xtn <> " not found in environment
 emptyEnv :: Environment
 emptyEnv = MkEnv M.empty 
 
+getTypes :: Modulename -> Environment -> [(Variable,Ty)]
+getTypes mn (MkEnv defs) = case M.lookup mn defs of 
+  Nothing -> [] 
+  Just prog -> do
+    let varDecls = snd <$> M.toList (progVars prog)
+    let vars = (\decl -> (varName decl,varTy decl)) <$> varDecls
+    let recDecls = snd <$> M.toList (progRecs prog)
+    let recs = (\decl -> (recName decl,recTy decl)) <$> recDecls 
+    vars ++ recs
+
 addDeclEnv :: Modulename -> DataDecl -> Environment -> Environment 
 addDeclEnv nm decl (MkEnv defs) = 
   case M.lookup nm defs of 

one-sided-sequent.cabal

@@ -183,4 +183,5 @@ executable web-app
                    eval,
   hs-source-dirs:  web-app
   other-modules:   Callback,
-                   JSBits
+                   JSBits,
+                   StringFormat

web-app/JSBits.hs

@@ -13,17 +13,22 @@ foreign import javascript "((arr,offset) => document.getElementById('resultStr')
 -- id traceStr
 foreign import javascript "((arr,offset) => document.getElementById('traceStr').innerHTML = h$decodeUtf8z(arr,offset))"
   setTraceString :: CString -> IO () 
+-- id typesStr
+foreign import javascript "((arr,offset) => document.getElementById('typesStr').innerHTML = h$decodeUtf8z(arr,offset))"
+  setTypesString :: CString -> IO ()
 
-setSuccess :: String -> String -> IO () 
-setSuccess res tr = do 
+setSuccess :: String -> String -> String -> IO () 
+setSuccess res tr tys = do 
   setWithString setResClass "evalSucc"
   setWithString setResString res
   setWithString setTraceString tr
+  setWithString setTypesString tys
 
 
 setError :: String -> IO () 
 setError str = do 
   setWithString setResClass "evalError"
   setWithString setResString str
   setWithString setTraceString ""
+  setWithString setTypesString ""
 

web-app/Main.hs

@@ -5,7 +5,8 @@ import Driver.Driver
 import Environment
 import Eval.Definition
 import Errors
-import Syntax.Typed.Terms
+import StringFormat
+
 import Callback
 import JSBits
 import GHC.JS.Prim
@@ -24,22 +25,10 @@ runProg val = do
   case res of 
     Left err  -> let msg = getMessage err in setError msg
     --(Either T.Command EvalTrace)
-    Right (Left c,_) -> setSuccess (show c) ""
-    Right (Right (MkTrace c tr),_) -> setSuccess (show c) (traceToStr tr) 
+    Right (Left c,st) -> setSuccess (replStr $ show c) "" (envToStr $ drvEnv st)
+    Right (Right (MkTrace c tr),st) -> setSuccess (replStr $ show c) (traceToStr tr) (envToStr $ drvEnv st)
   return ()
 
-traceToStr :: [Command] -> String
-traceToStr [] = ""
-traceToStr (c:cs) = replStr (show c) <> "<br/>" <> traceToStr cs
-
-repl :: Char -> String
-repl '<' = "&lt;"
-repl '+' = "&plus;"
-repl '|' = "&vert;"
-repl c =  [c]
-
-replStr :: String -> String 
-replStr = concatMap repl
 
 main :: IO () 
 main = do 

web-app/StringFormat.hs

@@ -0,0 +1,26 @@
+module StringFormat where 
+
+import Environment 
+import Common
+import Syntax.Typed.Terms
+import Pretty.Typed () 
+
+import Data.List (intercalate)
+
+envToStr :: Environment -> String 
+envToStr env = do 
+  let tys = getTypes (MkModule "") env
+  let tyStrs = (\(nm,ty) -> replStr (show nm) <> "::" <> replStr (show ty)) <$> tys
+  intercalate "<br/>" tyStrs
+
+traceToStr :: [Command] -> String
+traceToStr cmds = intercalate "<br />" (replStr . show  <$> cmds)
+
+repl :: Char -> String
+repl '<' = "&lt;"
+repl '+' = "&plus;"
+repl '|' = "&vert;"
+repl c =  [c]
+
+replStr :: String -> String 
+replStr = concatMap repl

web-app/index.html

@@ -40,6 +40,8 @@ <h1>One Sided Sequent Calculus</h1>
     <div class="results">
       <h2>Results</h2>
       <div id="resultStr"></div>
+      Types: <br/>
+      <div id="typesStr"></div>
       Trace: <br/>
       <div id="traceStr"></div>
     </div>