Changeset 11167

Show
Ignore:
Timestamp:
16.12.2008 17:14:49 (15 months ago)
Author:
maeder
Message:

properly quantify also operation definitions

Location:
trunk/HasCASL
Files:
2 modified

Legend:

Unmodified
Added
Removed

  • trunk/HasCASL/AsToLe.hs

    r10463 r11167  
    1414module HasCASL.AsToLe where 
    1515 
    16 import Common.AS_Annotation 
    17 import Common.GlobalAnnotations 
    18 import Common.Id 
    19 import Common.Result 
    20 import Common.ExtSign 
    21 import Common.Prec 
    22 import Common.Lib.State 
    23 import qualified Data.Map as Map 
    24 import qualified Data.Set as Set 
    25  
    2616import HasCASL.As 
    27 import HasCASL.FoldType 
    2817import HasCASL.Le 
    2918import HasCASL.TypeAna 
    … …  
    3726import HasCASL.Merge 
    3827import HasCASL.MapTerm 
    39 import HasCASL.FoldTerm 
     28 
     29import Common.AS_Annotation 
     30import Common.GlobalAnnotations 
     31import Common.Id 
     32import Common.Result 
     33import Common.ExtSign 
     34import Common.Prec 
     35import Common.Lib.State 
     36 
     37import qualified Data.Map as Map 
     38import qualified Data.Set as Set 
    4039import Data.Maybe 
    4140 
    … …  
    199198       return $ Internal ul ps 
    200199 
    201 freeVars :: Term -> Set.Set VarDecl 
    202 freeVars = foldTerm FoldRec 
    203     { foldQualVar = \ _ t -> Set.singleton t 
    204     , foldQualOp = \ _ _ _ _ _ _ _ -> Set.empty 
    205     , foldApplTerm = \ _ t1 t2 _ -> Set.union t1 t2 
    206     , foldTupleTerm = \ _ tts _ -> Set.unions tts 
    207     , foldTypedTerm = \ _ ts _ _ _ -> ts 
    208     , foldAsPattern = \ _ t ts _ -> Set.insert t ts 
    209     , foldQuantifiedTerm = \ _ _ gvs ts _ -> Set.difference ts $ 
    210          foldr ( \ gv -> case gv of 
    211            GenVarDecl t -> Set.insert t 
    212            _ -> id) Set.empty gvs 
    213     , foldLambdaTerm = \ _ pats _ ts _ -> Set.difference ts $ Set.unions pats 
    214     , foldCaseTerm = \ _ ts tts _ -> Set.difference 
    215           (Set.unions $ ts : map snd tts) $ Set.unions $ map fst tts 
    216     , foldLetTerm = \ _ _ tts ts _ -> Set.difference 
    217           (Set.unions $ ts : map snd tts) $ Set.unions $ map fst tts 
    218     , foldResolvedMixTerm = \ _ _ _ tts _ -> Set.unions tts 
    219     , foldTermToken = \ _ _ -> Set.empty 
    220     , foldMixTypeTerm = \ _ _ _ _ -> Set.empty 
    221     , foldMixfixTerm = \ _ tts -> Set.unions tts 
    222     , foldBracketTerm = \ _ _ tts _ -> Set.unions tts 
    223     , foldProgEq = \ _ ps ts _ -> (ps, ts) } 
    224  
    225 -- | quantify 
    226 mkEnvForall :: Env -> Term -> Range -> Term 
    227 mkEnvForall e t ps = 
    228   let tys = Set.fromList $ map (fst . snd) $ concatMap (leaves (>= 0)) 
    229             $ getAllTypes t 
    230       tyVs = map ( \ (i, TypeVarDefn v vk rk c) -> GenTypeVarDecl $ 
    231                    TypeArg i v vk rk c Other ps) $ Map.toList 
    232              $ Map.filterWithKey ( \ i _ -> Set.member i tys) $ localTypeVars e 
    233       vs = tyVs ++ map GenVarDecl (Set.toList $ freeVars t) 
    234   in if null vs then t else QuantifiedTerm Universal vs t ps 
    235  
    236200-- | analyse sig items 
    237201anaSigItems :: GenKind -> SigItems -> State Env SigItems 

  • trunk/HasCASL/OpDecl.hs

    r10299 r11167  
    1515  ( anaOpItem 
    1616  , anaProgEq 
     17  , mkEnvForall 
    1718  ) where 
    1819 
    … …  
    3334 
    3435import HasCASL.As 
     36import HasCASL.FoldTerm 
     37import HasCASL.FoldType 
    3538import HasCASL.HToken 
    3639import HasCASL.TypeAna 
    … …  
    124127                   monoty = monoType ty 
    125128               mt <- typeCheck Nothing $ TypedTerm rTrm AsType monoty ps 
     129               e <- get 
    126130               newSc <- generalizeS $ TypeScheme newArgs 
    127131                      (getFunType ty partial 
    … …  
    138142                           lhs = mkApplTerm ot pats 
    139143                           ef = mkEqTerm eqId monoty ps lhs lastTrm 
    140                            f = mkForall 
    141                              (map GenTypeVarDecl newArgs ++ 
    142                               (map GenVarDecl $ concatMap extractVars pats)) ef 
     144                           f = mkEnvForall e ef ps 
    143145                       addOpId i newSc Set.empty $ Definition br lamTrm 
    144146                       appendSentences 
    … …  
    155157               putLocalTypeVars tvs 
    156158               return $ replaceAnnoted Nothing oi 
     159 
     160freeVars :: Term -> Set.Set VarDecl 
     161freeVars = foldTerm FoldRec 
     162    { foldQualVar = \ _ t -> Set.singleton t 
     163    , foldQualOp = \ _ _ _ _ _ _ _ -> Set.empty 
     164    , foldApplTerm = \ _ t1 t2 _ -> Set.union t1 t2 
     165    , foldTupleTerm = \ _ tts _ -> Set.unions tts 
     166    , foldTypedTerm = \ _ ts _ _ _ -> ts 
     167    , foldAsPattern = \ _ t ts _ -> Set.insert t ts 
     168    , foldQuantifiedTerm = \ _ _ gvs ts _ -> Set.difference ts $ 
     169         foldr ( \ gv -> case gv of 
     170           GenVarDecl t -> Set.insert t 
     171           _ -> id) Set.empty gvs 
     172    , foldLambdaTerm = \ _ pats _ ts _ -> Set.difference ts $ Set.unions pats 
     173    , foldCaseTerm = \ _ ts tts _ -> Set.difference 
     174          (Set.unions $ ts : map snd tts) $ Set.unions $ map fst tts 
     175    , foldLetTerm = \ _ _ tts ts _ -> Set.difference 
     176          (Set.unions $ ts : map snd tts) $ Set.unions $ map fst tts 
     177    , foldResolvedMixTerm = \ _ _ _ tts _ -> Set.unions tts 
     178    , foldTermToken = \ _ _ -> Set.empty 
     179    , foldMixTypeTerm = \ _ _ _ _ -> Set.empty 
     180    , foldMixfixTerm = \ _ tts -> Set.unions tts 
     181    , foldBracketTerm = \ _ _ tts _ -> Set.unions tts 
     182    , foldProgEq = \ _ ps ts _ -> (ps, ts) } 
     183 
     184-- | quantify 
     185mkEnvForall :: Env -> Term -> Range -> Term 
     186mkEnvForall e t ps = 
     187  let tys = Set.fromList $ map (fst . snd) $ concatMap (leaves (>= 0)) 
     188            $ getAllTypes t 
     189      tyVs = map ( \ (i, TypeVarDefn v vk rk c) -> GenTypeVarDecl $ 
     190                   TypeArg i v vk rk c Other ps) $ Map.toList 
     191             $ Map.filterWithKey ( \ i _ -> Set.member i tys) $ localTypeVars e 
     192      vs = tyVs ++ map GenVarDecl (Set.toList $ freeVars t) 
     193  in if null vs then t else QuantifiedTerm Universal vs t ps 
    157194 
    158195-- | analyse a program equation