Changeset 12749

Timestamp:

29.10.2009 16:26:02 (3 weeks ago)

Author:

kristina

Message:

Added headers and algorithm descriptions

Location:

trunk

Files:

• Comorphisms/DFOL2CASL.hs (modified) (1 diff)
• DFOL/AS_DFOL.hs (modified) (1 diff)
• DFOL/Colimit.hs (modified) (1 diff)
• DFOL/Morphism.hs (modified) (3 diffs)

trunk/Comorphisms/DFOL2CASL.hs

@@ +1 @@
+{- |
+Module      :  $Header$
+Description :  Translation of first-order logic with dependent types (DFOL) to
+               CASL
+Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
+License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
+
+Maintainer  :  k.sojakova@jacobs-university.de
+Stability   :  experimental
+Portability :  portable
+
+Ref: K. Sojakova and F. Rabe. Translating a Dependently-Typed Logic to
+     First-Order Logic. LNCS 2009, pages 326-341.
+-}
+
 module Comorphisms.DFOL2CASL where
 

trunk/DFOL/AS_DFOL.hs

@@ -39 +39 @@
       translate,
       getNewName,
-      getFreeVars  
+      getFreeVars
    )  where
 

trunk/DFOL/Colimit.hs

@@ -9 +9 @@
 Stability   :  experimental
 Portability :  portable
+
+Algorithm description:
+
+Input : graph where nodes are signatures and edges are morphisms
+Output : a signature "sig" and for each input signature "sig1" a morphism
+         m : sig1 -> sig
+
+1 : Compute the transitive and symmetric closure of the relation R induced
+    by the morphisms in the graph
+
+2 : Initialize the output signature "sig" and collection of morphisms "M" to
+    empty
+    Initialize the set of analyzed symbols to empty
+
+3 : For each input signature sig1 :
+    3.1 : Initialize the output map "m" to empty
+    3.2 : For each symbol "s" in sig1 (keeping the order in which they are
+              defined) :
+          3.1.1 Check if s R s' for any already analyzed symbol "s'"
+          3.1.2 If yes:
+                3.1.2.1 Recover from M the value "c" that s' maps to
+                                3.1.2.2 Update m by adding the pair (s,c)
+                  3.1.3 If no:
+                3.1.3.1 Get the type "t" of s in sig1
+                3.1.3.2 Translate t along m; call this new type "t1"
+                3.1.3.3 Update sig by adding the declaration s : t1
+                        (in case the name s is already contained in sig,
+                                                we generate a fresh name "s1" and add the declaration
+                        s1 : t and pair (s,s1) to sig and m respectively.
+    3.3 : Add m to M
 -}
 

trunk/DFOL/Morphism.hs

@@ -97 +97 @@
 
 -- generated and cogenerated signatures
+{- Algorithm description:
+
+FOR GENERATED SIGNATURES
+
+Input : a signature "sig" and a set of symbols "syms"
+Output : an inclusion morphism
+
+1 : Check if all symbols in syms occur in sig; if not, output Nothing
+
+2 : Initialize the set of symbols "incl" which necessarily must be included
+    in the generated signature to syms
+    Initialize the set "done" of analyzed symbols to empty
+    Initialize the set "todo" of symbols to be analyzed to syms
+
+3 : Check if todo is empty
+    3.1 : If yes, go to 5
+        3.2 : If not, go to 4
+
+4 : Pick a symbol "s" from todo
+    4.1 : Get the type "t" of s in sig
+        4.2 : Get the set "vars" of free variables in t, i.e. the symbols of sig
+          that t depends on
+    4.3 : For each "v" in vars :
+          4.3.1 : Add v to incl
+          4.3.2 : If v does not occur in done, add it to todo
+    4.4 : Remove v from todo and add it to done
+    4.5 : Go to 3
+
+5 : Let "sig1" be the subsignature of sig containing only the symbols in incl
+    and output the inclusion morphism m : sig1 -> sig
+
+FOR COGENERATED SIGNATURES
+
+Input : a signature "sig" and a set of symbols "syms"
+Output : an inclusion morphism
+
+1 : Check if all symbols in syms occur in sig; if not, output Nothing
+
+2 : Initialize the set of symbols "excl" which necessarily must be excluded
+    from the cogenerated signature to syms
+
+3 : For each symbol "s" in sig (keeping the order in which they are defined) :
+    3.1 : If s does not occur in excl :
+          4.1 : Get the type "t" of s in sig
+              4.2 : Get the set "vars" of free variables in t, i.e. the symbols of
+                        sig that t depends on
+          4.3 : If any of the symbols in vars occurs in excl, add s to excl
+
+4 : Let "sig1" be the subsignature of sig containing all the symbols not
+    occurring in excl and output the inclusion morphism m : sig1 -> sig
+-}
 coGenSig :: Bool -> Set.Set Symbol -> Sign -> Result Morphism
 coGenSig flag syms sig@(Sign ds) =
@@ -107 +158 @@
                      ds2 = filter (\ ([n],_) -> Set.member n incl) ds1
                      in inclusionMorph (Sign ds2) sig
-            else Result.Result [symsNotInSigError names sig] Nothing   
+            else Result.Result [symsNotInSigError names sig] Nothing
 
 genSig :: Set.Set NAME -> Set.Set NAME -> Set.Set NAME -> Sign -> Set.Set NAME
 genSig incl done todo sig =
   if (Set.null todo)
-     then incl   
+     then incl
      else let n = Set.findMin todo
               Just t = getSymbolType n sig
@@ -123 +174 @@
 
 cogSig :: Set.Set NAME -> [DECL] -> Sign -> Set.Set NAME
-cogSig incl [] sig = Set.difference (getSymbols sig) incl 
-cogSig incl (([n],t):ds) sig =
-  if (Set.member n incl)
-     then cogSig incl ds sig  
+cogSig excl [] sig = Set.difference (getSymbols sig) excl
+cogSig excl (([n],t):ds) sig =
+  if (Set.member n excl)
+     then cogSig excl ds sig
      else let ns = Set.toList $ getFreeVars t
-              depen = or $ map (\ n1 -> Set.member n1 incl) ns 
+              depen = or $ map (\ n1 -> Set.member n1 excl) ns
               in if depen
-                    then let incl1 = Set.insert n incl
-                             in cogSig incl1 ds sig
-                    else cogSig incl ds sig       
+                    then let incl1 = Set.insert n excl
+                             in cogSig excl1 ds sig
+                    else cogSig excl ds sig
 cogSig _ _ _ = Set.empty