Changeset 12698
- Timestamp:
- 23.10.2009 10:50:12 (4 weeks ago)
- Location:
- trunk
- Files:
-
- 2 modified
-
CASL/Utils.hs (modified) (10 diffs)
-
Comorphisms/CASL2TopSort.inline.hs (modified) (9 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/CASL/Utils.hs
r12268 r12698 24 24 25 25 import CASL.AS_Basic_CASL 26 import CASL.Sign (mkVarTerm) 26 27 import CASL.Fold 27 28 … … 55 56 type FreshVARMap f = Map.Map VAR (TERM f) 56 57 57 -- | build _vMap constructs a mapping between a list of old variables and58 -- | buildVMap constructs a mapping between a list of old variables and 58 59 -- corresponding fresh variables based on two lists of VAR_DECL 59 build _vMap :: [VAR_DECL] -> [VAR_DECL] -> FreshVARMap f60 build _vMap vDecls f_vDecls =61 Map.fromList (concat (zipWith toTups vDecls f _vDecls))60 buildVMap :: [VAR_DECL] -> [VAR_DECL] -> FreshVARMap f 61 buildVMap vDecls fVDecls = 62 Map.fromList (concat (zipWith toTups vDecls fVDecls)) 62 63 where toTups (Var_decl vars1 sor1 _) (Var_decl vars2 sor2 _) = 63 64 if sor1 == sor2 then zipWith (toTup sor1) vars1 vars2 64 else error "CASL.Utils.build _vMap"65 toTup s v1 v2 = (v1, toVarTerm v2 s)65 else error "CASL.Utils.buildVMap" 66 toTup s v1 v2 = (v1, mkVarTerm (v2, s)) 66 67 67 68 -- | specialised lookup in FreshVARMap that ensures that the VAR with 68 69 -- the correct type (SORT) is replaced 69 lookup _vMap :: VAR -> SORT -> FreshVARMap f -> Maybe (TERM f)70 lookup _vMap v s =70 lookupVMap :: VAR -> SORT -> FreshVARMap f -> Maybe (TERM f) 71 lookupVMap v s = 71 72 maybe Nothing 72 73 (\ t@(Qual_var _ s' _) -> if s==s' then Just t else Nothing) … … 74 75 75 76 -- | specialized delete that deletes all shadowed variables 76 delete _vMap :: [VAR_DECL] -> FreshVARMap f -> FreshVARMap f77 delete _vMap vDecls m = foldr Map.delete m77 deleteVMap :: [VAR_DECL] -> FreshVARMap f -> FreshVARMap f 78 deleteVMap vDecls m = foldr Map.delete m 78 79 $ concatMap (\ (Var_decl vs _ _) -> vs) vDecls 79 80 … … 81 82 replaceVarsRec m mf = (mapRecord mf) 82 83 { foldQual_var = \ qv v s _ -> 83 fromMaybe qv $ lookup _vMap v s m84 fromMaybe qv $ lookupVMap v s m 84 85 , foldQuantification = \ (Quantification q vs f ps) _ _ _ _ -> 85 let nm = delete _vMap vs m86 in Quantification q vs (replace _varsF nm mf f) ps86 let nm = deleteVMap vs m 87 in Quantification q vs (replaceVarsF nm mf f) ps 87 88 } 88 89 89 -- | replace _vars replaces all Qual_var occurences that are supposed90 -- | replaceVars replaces all Qual_var occurences that are supposed 90 91 -- to be replaced according to the FreshVARMap 91 replace _varsF :: FreshVARMap f92 replaceVarsF :: FreshVARMap f 92 93 -> (f -> f) 93 94 -- ^ this function replaces Qual_var in ExtFORMULA 94 95 -> FORMULA f -> FORMULA f 95 replace _varsF m = foldFormula . replaceVarsRec m96 replaceVarsF m = foldFormula . replaceVarsRec m 96 97 97 98 codeOutUniqueRecord :: (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f) … … 103 104 if sor1 == sor2 then zipWith (eqFor sor1) vars1 vars2 104 105 else error "codeOutUniqueRecord1" 105 eqFor s v1 v2 = Strong_equation ( toSortTerm (toVarTerm v1s))106 ( toSortTerm (toVarTerm v2s))106 eqFor s v1 v2 = Strong_equation (mkVarTerm (v1, s)) 107 (mkVarTerm (v2, s)) 107 108 nullRange 108 -- fresh _vars produces new variables based on a list109 -- freshVars produces new variables based on a list 109 110 -- of defined variables 110 111 -- args: (1) set of already used variable names 111 112 -- (2) list of variables 112 fresh _vars = mapAccumL fresh_var113 fresh _var accSet (Var_decl vars sor _) =113 freshVars = mapAccumL freshVar 114 freshVar accSet (Var_decl vars sor _) = 114 115 let accSet' = Set.union (Set.fromList vars) accSet 115 116 (accSet'',vars') = mapAccumL nVar accSet' vars … … 120 121 [genVar v (i :: Int) | i<-[1..]]) 121 122 in (Set.insert v' aSet,v') 122 (vSet', vDecl') = fresh _vars Set.empty vDecl123 (_vSet'', vDecl'') = fresh _vars vSet' vDecl124 f'_rep_x = replace _varsF (build_vMap vDecl vDecl') rf f'125 f'_rep_y = replace _varsF (build_vMap vDecl vDecl'') rf f'123 (vSet', vDecl') = freshVars Set.empty vDecl 124 (_vSet'', vDecl'') = freshVars vSet' vDecl 125 f'_rep_x = replaceVarsF (buildVMap vDecl vDecl') rf f' 126 f'_rep_y = replaceVarsF (buildVMap vDecl vDecl'') rf f' 126 127 allForm = Quantification Universal (vDecl'++vDecl'') 127 128 (Implication … … 171 172 \ (Membership t s ps) _ _ _ -> 172 173 either (codeOutConditionalF fun) id 173 (mkSingleTermF (\ x y -> Membership x s y) t ps)174 (mkSingleTermF (\ x -> Membership x s) t ps) 174 175 , foldDefinedness = 175 176 \ (Definedness t ps) _ _ -> … … 184 185 codeOutCondPredication phi@(Predication _ ts _) = 185 186 maybe (Right phi) (Left . constructExpansion phi) 186 (listToMaybe (catMaybes (map findConditionalT ts)))187 $ listToMaybe $ mapMaybe findConditionalT ts 187 188 codeOutCondPredication _ = error "CASL.Utils: Predication expected" 188 189 … … 204 205 mkEquationAtom cons t1 t2 ps = 205 206 maybe (Right phi) (Left . constructExpansion phi) 206 (listToMaybe (catMaybes (map findConditionalT [t1,t2])))207 $ listToMaybe $ mapMaybe findConditionalT [t1, t2] 207 208 where phi = cons t1 t2 ps 208 209 … … 283 284 substEqPreds :: Set.Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f 284 285 substEqPreds eqPredSet = foldFormula . eqSubstRecord eqPredSet 285 286 -- | adds Sorted_term to a Qual_var term287 toSortTerm :: TERM f -> TERM f288 toSortTerm t@(Qual_var _ s ps) = Sorted_term t s ps289 toSortTerm _ = error "CASL2TopSort.toSortTerm: can only handle Qual_var"290 291 -- | generates from a variable and sort an Qual_var term292 toVarTerm :: VAR -> SORT -> TERM f293 toVarTerm vs s = Qual_var vs s nullRange -
trunk/Comorphisms/CASL2TopSort.inline.hs
r12401 r12698 31 31 import CASL.Logic_CASL 32 32 import CASL.AS_Basic_CASL 33 import CASL.Utils34 33 import CASL.Sign 35 34 import CASL.Morphism … … 241 240 where p_axs = 242 241 -- generate argument restrictions for predicates 243 Map.foldWithKey (\ pName set al->244 al++ Map.foldWithKey242 Map.foldWithKey (\ pName set -> 243 (++ Map.foldWithKey 245 244 (\ sl -> genArgRest 246 245 (genSenName "p" pName $ length sl) 247 246 (genPredication pName) 248 247 sl) 249 [] (mkProfMapPred subSortMap set)) 248 [] (mkProfMapPred subSortMap set))) 250 249 [] pMap 251 250 hi_axs = … … 324 323 genArgRest sen_name genProp sl spl fs = 325 324 let vars = genVars sl 326 mquant = genQuantification (genProp sl $ map toSortTermvars) vars spl325 mquant = genQuantification (genProp sl vars) vars spl 327 326 in maybe fs (\ quant -> mapNamed (const quant) (makeNamed "" sen_name) 328 327 : fs) mquant … … 345 344 346 345 genVars :: [SORT] -> [TERM f] 347 genVars = zipWith toVarTermvarSymbs346 genVars = map mkVarTerm . zip varSymbs 348 347 where varSymbs = map mkSimpleId 349 348 (map (: []) "xyzuwv" ++ map (\ i -> 'v' : show i) [(1::Int)..]) … … 459 458 relativize Universal vdl f1 = 460 459 if null vdl then f1 461 else Implication (mkVarPreds vdl) f1 True nullRange460 else mkImpl (mkVarPreds vdl) f1 462 461 -- existential or unique-existential? then use conjuction 463 462 relativize _ vdl f1 = 464 463 if null vdl then f1 465 else Conjunction [mkVarPreds vdl,f1] nullRange 466 mkVarPreds [v] = mkVarPred v 467 mkVarPreds vdl = Conjunction (map mkVarPred vdl) nullRange 468 mkVarPred (Var_decl [v] s _) = mkVarPred1 s v 469 mkVarPred (Var_decl vs s _) = 470 Conjunction (map (mkVarPred1 s) vs) nullRange 464 else conjunct [mkVarPreds vdl, f1] 465 mkVarPreds = conjunct . map mkVarPred 466 mkVarPred (Var_decl vs s _) = conjunct $ map (mkVarPred1 s) vs 471 467 mkVarPred1 s v = 472 468 let sTop = lkupTop subSortMap s … … 490 486 Conditional t1 f t2 pl -> 491 487 Conditional (mapTerm ssMap t1) (mapSen1 ssMap f) (mapTerm ssMap t2) pl 492 _ -> 493 error "CASL2TopSort.mapTerm" 488 _ -> error "CASL2TopSort.mapTerm" 494 489 where lTop = lkupTop ssMap 495 490 updateOP_SYMB (Op_name _) = … … 511 506 [xs@(x : _)] -> return $ genQuant x $ genImpl xs 512 507 ((x : _) : _) -> return $ genQuant x 513 $ Conjunction (map genImpl groupedInjOps) nullRange508 $ conjunct $ map genImpl groupedInjOps 514 509 _ -> error "CASL2TopSort.genEitherAxiom.groupedInjOps" 515 510 else Result [Diag Error … … 529 524 sameTarget x1 x2 = compTarget x1 x2 == EQ 530 525 lTop = lkupTop ssMap 531 varName = mkSimpleId "x" 532 mkVarTerm qon = 533 Sorted_term (Qual_var varName s nullRange) s nullRange 534 where s = lTop $ resultSort qon 535 mkVarDecl qon = 536 Var_decl [varName] (lTop (resultSort qon)) nullRange 537 genQuant qon f = Quantification Universal [mkVarDecl qon] f nullRange 538 genImpl [] = error "No OP_SYMB found" 539 genImpl xs@(x:_) = 540 assert (lTop (resultSort x) == lTop (argSort x)) 541 (if resultSort x == lTop (resultSort x) 542 then genDisj xs 543 else Implication (genProp x) (genDisj xs) True nullRange) 544 genProp qon = genPredication (lPredName (resultSort qon)) 545 [lTop (resultSort qon)] 546 [mkVarTerm qon] 526 mkXVarTerm = toQualVar . mkXVarDecl 527 -- I do not think this term needs to be a sorted term 528 mkXVarDecl = mkVarDeclStr "x" . lTop . resultSort 529 genQuant qon f = mkForall [mkXVarDecl qon] f nullRange 530 genImpl xs = case xs of 531 x : _ -> let 532 rSrt = resultSort x 533 ltSrt = lTop rSrt 534 disjs = genDisj xs 535 in if ltSrt == lTop (argSort x) then 536 if rSrt == ltSrt then disjs else mkImpl (genProp x) disjs 537 else error "CASL2TopSort.genEitherAxiom.genImpl" 538 _ -> error "CASL2TopSort.genEitherAxiom.genImpl No OP_SYMB found" 539 genProp qon = let rSrt = resultSort qon in 540 genPredication (lPredName rSrt) [lTop rSrt] [mkXVarTerm qon] 547 541 lPredName s = fromMaybe (error $ 548 542 "CASL2TopSort.genEitherAxiom: No PRED_NAME for \"" … … 550 544 genDisj qons = Disjunction (map genPred qons) nullRange 551 545 genPred qon = genPredication (lPredName $ argSort qon) 552 [lTop $ resultSort qon] [mk VarTerm qon]546 [lTop $ resultSort qon] [mkXVarTerm qon]
