Changeset 12771
- Timestamp:
- 02.11.2009 17:36:36 (3 weeks ago)
- Files:
-
- 1 modified
-
trunk/Logic/Comorphism.hs (modified) (11 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/Logic/Comorphism.hs
r12643 r12771 44 44 import Logic.Coerce 45 45 import Logic.ExtSign 46 import Common.ExtSign 47 import Common.Result 48 import Common.ProofUtils 46 49 47 import Common.AS_Annotation 50 48 import Common.Doc 51 49 import Common.DocUtils 50 import Common.ExtSign 51 import Common.Id 52 import Common.ProofUtils 53 import Common.Result 54 55 import Data.Maybe 52 56 import qualified Data.Set as Set 53 57 import Data.Typeable … … 120 124 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 121 125 => cid -> sublogics2 122 targetSublogic cid = maybe (top_sublogic $ targetLogic cid)123 id$ mapSublogic cid $ sourceSublogic cid126 targetSublogic cid = fromMaybe (top_sublogic $ targetLogic cid) 127 $ mapSublogic cid $ sourceSublogic cid 124 128 125 129 -- | this function is base on 'map_theory' using no sentences as input … … 187 191 if isSubElem senLog sub 188 192 then res 189 else fail $ "for '" ++ language_name cid ++ 193 else Result 194 [ Diag Hint 195 (show (vcat $ pretty sign : map 196 (print_named $ sourceLogic cid) sens)) 197 nullRange 198 , Diag Error 199 ("for '" ++ language_name cid ++ 190 200 "' expected sublogic '" ++ 191 201 sublogicName sub ++ … … 193 203 sublogicName senLog ++ 194 204 "' with signature sublogic '" ++ 195 sublogicName sigLog ++ "'\n" ++ 196 show (vcat $ pretty sign : map 197 (print_named $ sourceLogic cid) sens) 205 sublogicName sigLog ++ "'") nullRange] Nothing 198 206 199 207 simpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2) … … 237 245 mkInclComorphism lid srcSub trgSub = 238 246 if isSubElem srcSub trgSub 239 then return $InclComorphism247 then return InclComorphism 240 248 { inclusion_logic = lid 241 249 , inclusion_source_sublogic = srcSub … … 251 259 in if sub_src == sub_trg 252 260 then "id_" ++ lname ++ 253 if null sblName 254 then "" else "." ++ sblName 255 else "incl_" ++ lname ++ ":" ++ 256 sblName ++ "->" ++ sublogicName sub_trg 261 if null sblName then "" else '.' : sblName 262 else "incl_" ++ lname ++ ':' 263 : sblName ++ "->" ++ sublogicName sub_trg 257 264 258 265 instance Logic lid sublogics … … 276 283 map_theory _ = return 277 284 map_morphism _ = return 278 map_sentence _ = \_ ->return285 map_sentence _ _ = return 279 286 map_symbol _ _ = Set.singleton 280 287 constituents cid = … … 318 325 mapSublogic (CompComorphism cid1 cid2) sl = 319 326 mapSublogic cid1 sl >>= 320 (\ y -> mapSublogic cid2 $ 321 forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2) y) 322 map_sentence (CompComorphism cid1 cid2) = 323 \si1 se1 -> 327 mapSublogic cid2 . 328 forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2) 329 map_sentence (CompComorphism cid1 cid2) si1 se1 = 324 330 do (si2,_) <- map_sign cid1 si1 325 331 se2 <- map_sentence cid1 si1 se1 … … 331 337 _ -> error "CompComorphism.map_sentence" 332 338 333 map_theory (CompComorphism cid1 cid2) = 334 \ti1 -> 339 map_theory (CompComorphism cid1 cid2) ti1 = 335 340 do ti2 <- map_theory cid1 ti1 336 341 ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2) … … 338 343 wrapMapTheory cid2 ti2' 339 344 340 map_morphism (CompComorphism cid1 cid2) = \ m1 ->345 map_morphism (CompComorphism cid1 cid2) m1 = 341 346 do m2 <- map_morphism cid1 m1 342 347 m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2) … … 459 464 _ -> -} return $ Comorphism (CompComorphism cid1 cid2) 460 465 else fail $ "Subl" ++ msg 461 else fail $ "L" ++msg466 else fail $ 'L' : msg
