Changeset 12714

Timestamp:

24.10.2009 23:47:59 (4 weeks ago)

Author:

kristina

Message:

Removed too long lines
Added headers to files

Location:

trunk/DFOL

Files:

• AS_DFOL.hs (modified) (2 diffs)
• Analysis_DFOL.hs (modified) (1 diff)
• Colimit.hs (modified) (4 diffs)
• Comorphism.hs (modified) (1 diff)
• Logic_DFOL.hs (modified) (1 diff)
• Morphism.hs (modified) (1 diff)
• Parse_AS_DFOL.hs (modified) (1 diff)
• Sign.hs (modified) (1 diff)
• Symbol.hs (modified) (1 diff)
• Tests/Colimits1.het (modified) (1 diff)
• Tests/Test_Analysis_DFOL.hs (modified) (2 diffs)
• Utils.hs (modified) (1 diff)

trunk/DFOL/AS_DFOL.hs

@@ -2 +2 @@
 Module      :  $Header$
 Description :  Abstract syntax for first-order logic with dependent types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
 -}
 
@@ -240 +246 @@
    in the input set -}
 getNewName :: NAME -> Set.Set NAME -> NAME
-getNewName var names =
+getNewName var names = getNewNameH var names (tokStr var) 0
+
+getNewNameH :: NAME -> Set.Set NAME -> String -> Int -> Token
+getNewNameH var names root i = 
   if (Set.notMember var names)
      then var
-     else let newVar = Token ((tokStr var) ++ "1") nullRange
-              in getNewName newVar names
+     else let newVar = Token (root ++ (show i)) nullRange
+              in getNewNameH newVar names root $ i+1 
 
 -- equality

trunk/DFOL/Analysis_DFOL.hs

@@ -2 +2 @@
 Module      :  $Header$
 Description :  Static analysis for first-order logic with dependent types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
 -}
 

trunk/DFOL/Colimit.hs

@@ -1 @@
-module DFOL.Colimit {-(
+{- |
+Module      :  $Header$
+Description :  Signature colimits for first-order logic with dependent
+               types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
+-}
+
+module DFOL.Colimit (
     sigColimit
-  ) -} where
+  ) where
  
 import DFOL.AS_DFOL
@@ -44 +56 @@
        Set.Set (Int, NAME) ->                -- the symbols done so far
        Rel.Rel (Int, NAME) ->                -- the equality relation
-       [(Int, Sign)] ->                      -- the signatures to be processed      
+       [(Int, Sign)] ->                      -- the signatures to be processed
        (Sign, IntMap.IntMap (Map.Map NAME NAME))     -- the determined colimit
 
@@ -67 +79 @@
                      m1 = Map.insert n c m
                      doneSyms1 = Set.insert n1 doneSyms 
-                     in processSig sig maps m1 i ds doneSyms1 rel sigs     
+                     in processSig sig maps m1 i ds doneSyms1 rel sigs
 
 processSig _ _ _ _ _ _ _ _ = (emptySig, IntMap.empty)
@@ -91 +103 @@
                          in foldl (\ r2 s -> let t = mapSymbol m s
                                                  in Rel.insert (i,s) (j,t)
-                                                     $ Rel.insert (j,t) (i,s) r2 
+                                                     $ Rel.insert (j,t) (i,s) r2
                                   )
                                   r1 

trunk/DFOL/Comorphism.hs

@@ -2 +2 @@
 Module      :  $Header$
 Description :  Helper functions for the DFOL -> CASL translation
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
 -}
 

trunk/DFOL/Logic_DFOL.hs

@@ +1 @@
+{- |
+Module      :  $Header$
+Description :  Instances of classes defined in Logic.hs for first-order logic
+               with dependent types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
+
+Ref: Florian Rabe: First-Order Logic with Dependent Types. 
+     IJCAR 2006, pages 377-391.
+-}
+
 module DFOL.Logic_DFOL where
 

trunk/DFOL/Morphism.hs

@@ -3 +3 @@
 Description :  Definition of signature morphisms for
                first-order logic with dependent types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
 -}
 

trunk/DFOL/Parse_AS_DFOL.hs

@@ -1 +1 @@
 {- |
 Module      :  $Header$
-Description :  Parser for first-order logic with dependent types (DFOL)
+Description :  AParser for first-order logic with dependent types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
 -}
 

trunk/DFOL/Sign.hs

@@ -3 +3 @@
 Description :  Definition of signatures for first-order logic
                with dependent types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
 -}
 

trunk/DFOL/Symbol.hs

@@ -3 +3 @@
 Description :  Symbol definition for first-order logic
                with dependent types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
 -}
 

trunk/DFOL/Tests/Colimits1.het

@@ -17 +17 @@
 end
 
-view v1 : SP1 to SP2
-view v2 : SP1 to SP3
-view v3 : SP1 to SP4
+spec SP5 = SP1 then
+t :: Sort
+end
+

trunk/DFOL/Tests/Test_Analysis_DFOL.hs

@@ -19 +19 @@
 plusTok = mkTok "plus"
 mTok = mkTok "m"
-m1Tok = mkTok "m1"
+m1Tok = mkTok "m0"
 nTok = mkTok "n"
 
@@ -46 +46 @@
 t4 = Func [Univ nat] $ Func [Univ nat] $ Func [] Sort
 
+
+

trunk/DFOL/Utils.hs

@@ -2 +2 @@
 Module      :  $Header$
 Description :  Utilities for first-order logic with dependent types (DFOL)
+Copyright   :  (c) Kristina Sojakova, Jacobs University 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@ijacobs-university.de
+Stability   :  experimental
+Portability :  portable
 -}
+
 module DFOL.Utils where