tidied up repository; created core-language Haskell project from prev…

…ious core_language directory
smucclaw · Nov 9, 2020 · 594fff7 · 594fff7
commit 594fff7
Show file tree

Hide file tree

Showing 13 changed files with 1,411 additions and 0 deletions.
diff --git a/LICENSE b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Author name here (c) 2020
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Author name here nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.org b/README.org
@@ -0,0 +1,54 @@
+#+TITLE: Core Abstract Syntax
+
+* Overview
+
+Abstract syntax for core L4 concepts. 
+
+*Files:*
+
+- =AbsSyntax.hs= Declaration of data types (types, classes and instances,
+  modules, expressions, timed automata)
+- =Exec.hs= Execution / evaluation of expresssions
+- =TaToUppaal.hs= Conversion of Timed Automata to the Uppaal XTA format, see
+  https://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Introduction.shtml 
+- =TransL.hs= Translation from L4 BNFC to the core abstract syntax. Very incomplete.
+- =Typing.hs= Type checking of abstract syntax.
+
+The file =Test.hs= is for testing only and can be discarded.
+
+* Uppaal
+
+** Interactive use with the GUI
+
+Start Uppaal with =java -jar uppaal.jar &=, then =File / Open system=. Load a
+model (=*xml=) file. The view typically opens on the Editor tab (system
+definition with several automata). On the Simulator tab, one can execute the
+system by stepping through a scenario. On the Verifier tab, one finds several
+"queries" (corresponding to proof obligations). These are contained in the
+=*q= file associated with the model file. Select one of the formulas and
+verify it by clicking on the Check button. In order to obtain a
+counter-example, select "Options / Diagnostic Trace" and then one of Some /
+Shortest / Fastest. On the next Check, the counterexample will be loaded into
+the Simulator.
+
+
+** Command line interface
+
+In Haskell, running =writeFile "test_haskell_uppaal.xta" (ta_sys_to_uppaal (TmdAutSys [autA, autB]))=
+produces a textual Uppaal XTA file. The file can in principle be read in by
+the GUI. As there is no graphical layout information information associated
+with the file, the elements of the automata are first arranged in an arbitrary
+fashion. After manually rearranging and storing the model, a =.ugi= file
+stores graphic information. 
+
+The XTA file can be run (together with a query in a =.q= file) with shell
+command =verifyta= contained in the download bundle, as in =bin-Linux/verifyta -t0 
+test_haskell_uppaal.xta test_haskell_uppaal.q=, where =test_haskell_uppaal.q=
+is, for example:
+
+#+BEGIN_SRC
+E<> AutA.l3 and AutB.l2
+#+END_SRC
+
+A textual trace is then written to standard output.
+
diff --git a/Setup.hs b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/core-language.cabal b/core-language.cabal
@@ -0,0 +1,20 @@
+name:                core-language
+version:             0.1.0.0
+-- synopsis:
+-- description:
+homepage:            https://github.com/githubuser/core-language#readme
+license:             BSD3
+license-file:        LICENSE
+author:              Author name here
+maintainer:          [email protected]
+copyright:           2020 Author name here
+category:            Web
+build-type:          Simple
+cabal-version:       >=1.10
+extra-source-files:  README.md
+
+executable core-language
+  hs-source-dirs:      src
+  main-is:             Main.hs
+  default-language:    Haskell2010
+  build-depends:       base >= 4.7 && < 5
diff --git a/src/AbsSyntax.hs b/src/AbsSyntax.hs
@@ -0,0 +1,238 @@
+
+module AbsSyntax where
+
+----------------------------------------------------------------------
+-- Definition of expressions
+----------------------------------------------------------------------
+
+----- Names 
+newtype VarName = VarNm String
+  deriving (Eq, Ord, Show, Read)
+newtype ClassName = ClsNm String
+  deriving (Eq, Ord, Show, Read)
+newtype FieldName = FldNm String
+  deriving (Eq, Ord, Show, Read)
+newtype RuleName = RlNm String
+  deriving (Eq, Ord, Show, Read)
+newtype PartyName = PtNm String
+  deriving (Eq, Ord, Show, Read)
+
+
+----- Types 
+data Tp
+  = BoolT
+  | IntT
+  | FunT Tp Tp
+  | ClassT ClassName
+  | ErrT
+  deriving (Eq, Ord, Show, Read)
+
+-- Field attributes: for example cardinality restrictions
+-- data FieldAttribs = FldAtt
+data FieldDecl = FldDecl FieldName Tp -- FieldAttribs
+  deriving (Eq, Ord, Show, Read)
+
+-- superclass, list of field declarations
+data ClassDef t = ClsDef t [FieldDecl] 
+  deriving (Eq, Ord, Show, Read)
+
+data ClassDecl t = ClsDecl ClassName (ClassDef t)
+  deriving (Eq, Ord, Show, Read)
+
+name_of_class_decl :: ClassDecl t -> ClassName
+name_of_class_decl (ClsDecl cn _) = cn
+
+def_of_class_decl :: ClassDecl t -> ClassDef t
+def_of_class_decl (ClsDecl _ cd) = cd
+
+fields_of_class_def :: ClassDef t -> [FieldDecl]
+fields_of_class_def (ClsDef scn fds) = fds
+
+data Rule = TBD
+  deriving (Eq, Ord, Show, Read)
+data Module t = Mdl [ClassDecl t] [Rule]
+  deriving (Eq, Ord, Show, Read)
+
+class_decls_of_module :: Module t -> [ClassDecl t]
+class_decls_of_module (Mdl cds _) = cds
+
+rules_of_module :: Module t -> [Rule]
+rules_of_module (Mdl _ rls) = rls
+
+-- Custom Classes and Preable Module
+-- some custom classes - should eventually go into a prelude and not be hard-wired
+objectC = ClsDecl (ClsNm "Object") (ClsDef Nothing [])
+
+-- QualifiedNumeric class with val field
+-- TODO: should its type be IntT or a FloatT?
+qualifNumC = ClsDecl (ClsNm "QualifiedNumeric")
+                    (ClsDef (Just (ClsNm "Object"))
+                            [FldDecl (FldNm "val") IntT])
+
+-- Currency as QualifiedNumeric, with specific currencies (SGD, USD) as subclasses
+currencyC = ClsDecl (ClsNm "Currency")
+                    (ClsDef (Just (ClsNm "QualifiedNumeric")) [])
+currencyCs = [ClsDecl (ClsNm "SGD") (ClsDef (Just (ClsNm "Currency")) []),
+              ClsDecl (ClsNm "USD") (ClsDef (Just (ClsNm "Currency")) [])]
+
+-- Time as QualifiedNumeric, with Year, Month, Day etc. as subclasses
+-- TODO: treatment of time needs a second thought
+--       (so far no distinction between time point and duration)
+timeC = ClsDecl (ClsNm "Time")
+                    (ClsDef (Just (ClsNm "QualifiedNumeric")) [])
+timeCs = [ClsDecl (ClsNm "Year") (ClsDef (Just (ClsNm "Time")) []),
+          ClsDecl (ClsNm "Day") (ClsDef (Just (ClsNm "Time")) [])]
+
+eventC  = ClsDecl (ClsNm "Event")
+                  (ClsDef (Just (ClsNm "Object"))
+                   [FldDecl (FldNm "time") (ClassT (ClsNm "Time"))])
+customCs = [objectC, qualifNumC, currencyC] ++ currencyCs ++ [timeC] ++ timeCs ++ [eventC]
+
+preambleMdl = Mdl customCs []
+
+----- Expressions 
+data Val
+    = BoolV Bool
+    | IntV Integer
+    | RecordV ClassName [(FieldName, Val)]
+    | ErrV
+  deriving (Eq, Ord, Show, Read)
+
+-- unary arithmetic operators
+data UArithOp = UAminus
+  deriving (Eq, Ord, Show, Read)
+
+-- unary boolean operators
+data UBoolOp = UBneg
+  deriving (Eq, Ord, Show, Read)
+
+-- unary operators (union of the above)
+data UnaOp
+    = UArith UArithOp
+    | UBool UBoolOp
+  deriving (Eq, Ord, Show, Read)
+
+-- binary arithmetic operators
+data BArithOp = BAadd | BAsub | BAmul | BAdiv | BAmod
+  deriving (Eq, Ord, Show, Read)
+
+-- binary comparison operators
+data BComparOp = BCeq | BClt | BClte | BCgt | BCgte | BCne
+  deriving (Eq, Ord, Show, Read)
+
+-- binary boolean operators
+data BBoolOp = BBand | BBor
+  deriving (Eq, Ord, Show, Read)
+
+-- binary operators (union of the above)
+data BinOp
+    = BArith BArithOp
+    | BCompar BComparOp
+    | BBool BBoolOp
+  deriving (Eq, Ord, Show, Read)
+
+-- operators for combining list elements
+data ListOp = AndList | OrList | XorList | CommaList
+    deriving (Eq, Ord, Show, Read)
+
+-- Exp t is an expression of type t (to be determined during type checking / inference)
+data Exp t
+    = ValE t Val                                -- value
+    | VarE t VarName                            -- variable
+    | UnaOpE t UnaOp (Exp t)                    -- unary operator
+    | BinOpE t BinOp (Exp t) (Exp t)            -- binary operator
+    | IfThenElseE t (Exp t) (Exp t) (Exp t)     -- conditional
+    | AppE t (Exp t) (Exp t)                    -- function application
+    | FunE t VarName Tp (Exp t)                 -- function abstraction
+    | ClosE t [(VarName, Exp t)] (Exp t)        -- closure  (not externally visible)
+    | FldAccE t (Exp t) FieldName               -- field access
+    | CastE t Tp (Exp t)                        -- cast to type
+    | ListE t ListOp [Exp t]                    -- list expression
+    deriving (Eq, Ord, Show, Read)
+
+
+
+----------------------------------------------------------------------
+-- Definition of Timed Automata
+----------------------------------------------------------------------
+
+data Clock = Cl String
+  deriving (Eq, Ord, Show, Read)
+
+-- Clock constraint of the form x < c.
+-- TODO: Reconsider the Integer. Might also be a subclass of the "Time" class
+data ClConstr = ClCn Clock BComparOp Integer
+  deriving (Eq, Ord, Show, Read)
+
+data Loc = Lc String
+  deriving (Eq, Ord, Show, Read)
+
+-- Synchronization type: send or receive
+data Sync = Snd | Rec
+  deriving (Eq, Ord, Show, Read)
+
+-- Action in a transition: the string is the ClassName of a subclass of Event
+data Action
+  = Internal
+  | Act ClassName Sync
+  deriving (Eq, Ord, Show, Read)
+
+-- Transition relation from location to location via Action,
+-- provided [ClConstr] are satisfied; and resetting [Clock]
+data Transition = Trans Loc [ClConstr] Action [Clock] Loc
+  deriving (Eq, Ord, Show, Read)
+
+-- Timed Automaton having:
+-- a name
+-- a set of locations,
+-- a set of channel types (subclasses of Event),
+-- a set of clocks,
+-- a transition relation,
+-- a set of initial locations,
+-- an invariant per location and
+-- a labelling (an expression true in the location).
+-- Major extension: "Labeling function" which is typically taken to be Loc -> AP -> Bool
+-- for AP a type of atomic propositioons and which is here taken to be [(Loc, Exp t)].
+-- Note: the set of locations, actions, clocks could in principle be inferred from the remaining info.
+data TA t = TmdAut String [Loc] [ClassName] [Clock] [Transition] [Loc] [(Loc, [ClConstr])] [(Loc, Exp t)]
+  deriving (Eq, Ord, Show, Read)
+
+-- Timed Automata System: a set of TAs running in parallel
+data TASys t = TmdAutSys [TA t]
+  deriving (Eq, Ord, Show, Read)
+
+name_of_ta :: TA t -> String
+name_of_ta (TmdAut nm ta_locs ta_act_clss ta_clks trans init_locs invs lbls) = nm
+
+channels_of_ta :: TA t -> [ClassName]
+channels_of_ta (TmdAut nm ta_locs ta_act_clss ta_clks trans init_locs invs lbls) = ta_act_clss
+
+
+----------------------------------------------------------------------
+-- L4 Event Rules
+----------------------------------------------------------------------
+
+-- NB: Event rules as opposed to rules defining terminology etc.
+
+
+
+
+data Event t
+  = EventClConstr ClConstr
+  | EventCond (Exp t)
+
+-- only Must and May, assuming that Shant can be compiled away during syntax analysis
+data Modality = Must | May
+
+-- EventRule with components:
+-- rule name
+-- event list (interpreted conjunctively, all events of the list have to be satisfied)
+-- modality
+-- a non-empthy list of Parties (and not a single one). The first in the list is the one initiating the action
+-- (i.e., sender), the other ones are the receivers (if any)
+-- action
+-- clock constraints valid in the state corresponding to the name of this rule
+-- rule name corresponding to HENCE clause
+-- rule name (optional) corresponding to LEST clause
+
+data EventRule t = EvRule RuleName [Event t] Modality [PartyName] Action [ClConstr] RuleName (Maybe RuleName)