Changeset 12715
- Timestamp:
- 24.10.2009 23:50:36 (4 weeks ago)
- Location:
- trunk/DFOL
- Files:
-
- 4 modified
-
AS_DFOL.hs (modified) (2 diffs)
-
Colimit.hs (modified) (8 diffs)
-
Logic_DFOL.hs (modified) (1 diff)
-
Morphism.hs (modified) (1 diff)
Legend:
- Unmodified
- Added
- Removed
-
trunk/DFOL/AS_DFOL.hs
r12714 r12715 38 38 Translatable, 39 39 translate, 40 getNewName 40 getNewName 41 41 ) where 42 42 … … 249 249 250 250 getNewNameH :: NAME -> Set.Set NAME -> String -> Int -> Token 251 getNewNameH var names root i = 251 getNewNameH var names root i = 252 252 if (Set.notMember var names) 253 253 then var 254 254 else let newVar = Token (root ++ (show i)) nullRange 255 in getNewNameH newVar names root $ i+1 255 in getNewNameH newVar names root $ i+1 256 256 257 257 -- equality -
trunk/DFOL/Colimit.hs
r12714 r12715 14 14 sigColimit 15 15 ) where 16 16 17 17 import DFOL.AS_DFOL 18 18 import DFOL.Sign … … 29 29 -- main functions 30 30 sigColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map.Map Int Morphism) 31 sigColimit gr = 32 let sigs = Graph.labNodes gr 31 sigColimit gr = 32 let sigs = Graph.labNodes gr 33 33 rel = computeRel gr 34 34 (sig,maps) = addSig emptySig IntMap.empty Set.empty rel sigs … … 37 37 ) 38 38 maps 39 maps2 = Map.fromList $ IntMap.toList maps1 39 maps2 = Map.fromList $ IntMap.toList maps1 40 40 in Result [] $ Just (sig,maps2) 41 41 42 42 -- preparation for computing the colimit 43 43 addSig :: Sign -> IntMap.IntMap (Map.Map NAME NAME) -> Set.Set (Int, NAME) -> 44 Rel.Rel (Int, NAME) -> [(Int, Sign)] -> 44 Rel.Rel (Int, NAME) -> [(Int, Sign)] -> 45 45 (Sign, IntMap.IntMap (Map.Map NAME NAME)) 46 46 addSig sig maps _ _ [] = (sig,maps) 47 addSig sig maps doneSyms rel ((i, Sign ds):sigs) = 47 addSig sig maps doneSyms rel ((i, Sign ds):sigs) = 48 48 processSig sig maps Map.empty i (expandDecls ds) doneSyms rel sigs 49 49 … … 59 59 (Sign, IntMap.IntMap (Map.Map NAME NAME)) -- the determined colimit 60 60 61 processSig sig maps m i [] doneSyms rel sigs = 61 processSig sig maps m i [] doneSyms rel sigs = 62 62 let maps1 = IntMap.insert i m maps 63 in addSig sig maps1 doneSyms rel sigs 63 in addSig sig maps1 doneSyms rel sigs 64 64 65 65 processSig sig maps m i (([n],t):ds) doneSyms rel sigs = … … 71 71 t1 = translate mt syms t 72 72 n2 = toName n syms 73 sig1 = addSymbolDecl ([n2],t1) sig 73 sig1 = addSymbolDecl ([n2],t1) sig 74 74 m1 = Map.insert n n2 m 75 75 doneSyms1 = Set.insert n1 doneSyms … … 78 78 c = findValue k $ IntMap.insert i m maps 79 79 m1 = Map.insert n c m 80 doneSyms1 = Set.insert n1 doneSyms 80 doneSyms1 = Set.insert n1 doneSyms 81 81 in processSig sig maps m1 i ds doneSyms1 rel sigs 82 82 … … 87 87 findValue (i,k) maps = let Just m = IntMap.lookup i maps 88 88 in Map.findWithDefault k k m 89 89 90 90 toName :: NAME -> Set.Set NAME -> NAME 91 toName n names = 91 toName n names = 92 92 if (Set.notMember n names) 93 93 then n 94 94 else let s = tokStr n 95 95 n1 = Token ("gn_" ++ s) nullRange 96 in getNewName n1 names 96 in getNewName n1 names 97 97 98 98 computeRel :: Gr Sign (Int, Morphism) -> Rel.Rel (Int, NAME) 99 computeRel gr = 99 computeRel gr = 100 100 let morphs = Graph.labEdges gr 101 rel = foldl (\ r1 (i,j,(_,m)) -> 101 rel = foldl (\ r1 (i,j,(_,m)) -> 102 102 let syms = Set.toList $ getSymbols $ source m 103 103 in foldl (\ r2 s -> let t = mapSymbol m s … … 105 105 $ Rel.insert (j,t) (i,s) r2 106 106 ) 107 r1 107 r1 108 108 syms 109 ) 109 ) 110 110 Rel.empty 111 111 morphs -
trunk/DFOL/Logic_DFOL.hs
r12714 r12715 10 10 Portability : portable 11 11 12 Ref: Florian Rabe: First-Order Logic with Dependent Types. 12 Ref: Florian Rabe: First-Order Logic with Dependent Types. 13 13 IJCAR 2006, pages 377-391. 14 14 -} -
trunk/DFOL/Morphism.hs
r12714 r12715 138 138 -- translates a term, type or formula along the given morphism 139 139 applyMorph :: Translatable a => Morphism -> a -> a 140 applyMorph m t = 140 applyMorph m t = 141 141 let syms = getSymbols (target m) 142 142 map1 = toTermMap $ symMap m
