CurryInfo: property-prover-2.0.0 / Inference.Inference.constantResult

constantResult :: TAFuncDecl -> VarMap -> [TAExpr] -> Maybe TAExpr
constantResult decl@(AFunc qn arity vis ty (ARule rty vars exp)) vmap argExps
  = case go vmap' exp of
    [x] -> Just x
    _   -> Nothing -- todo: no results?
 where
  vmap' = foldr upd DM.empty (zip vars argExps)

  upd ((j, _), e) m = case e of
    AVar _ i -> case DM.lookup i vmap of
      Just x  -> DM.insert j x m
      Nothing -> m
    _        ->
      error $ "Inference.constantResult: normalization failure for " ++ show e

  go :: VarMap -> TAExpr -> [TAExpr]
  go vm e = case e of
    AVar _ i -> case DM.lookup i vm of
      Just x  -> case x of
        Left qn   -> case qn of
          ("Prelude", "True")  -> [boolExpr "True"]
          ("Prelude", "False") -> [boolExpr "False"]
          _                    -> error
            $ "Inference.constantResult.go: Unknown constructor " ++ show qn
        Right qns -> error
          $ "Inference.constantResult.go: Missing constructor for variable "
          ++ show i
      Nothing -> error
        $ "Inference.constantResult.go: Missing binding for variable "
        ++ show i
    ALit _ _ -> [] -- todo: literals
    AComb _ _ (("Prelude", "True"), _) [] -> [boolExpr "True"]
    AComb _ _ (("Prelude", "False"), _) [] -> [boolExpr "False"]
    AComb _ _ _ _ -> [] -- todo: function calls
    ALet _ binds expr -> go (DM.union vm (binds2VarMap binds)) expr
    AFree _ binds expr -> go vm expr -- todo: binds
    AOr _ e1 e2 -> go vm e1 ++ go vm e2
    ACase _ _ (AVar _ i) branches -> case DM.lookup i vm of
      Just x  -> case x of
        Left qn   -> selectBranchExprs qn branches
        Right qns -> removeBranchExprs qns branches
      Nothing -> concatMap (\(ABranch _ e) -> go vm e) branches
     where
      selectBranchExprs :: QName -> [TABranchExpr] -> [TAExpr]
      selectBranchExprs qname brs = concatMap (go vm) $ mapMaybe match brs
       where
        match (ABranch (APattern _ (pqn, _) _) e) | pqn == qname = Just e
                                                  | otherwise = Nothing

      removeBranchExprs :: [QName] -> [TABranchExpr] -> [TAExpr]
      removeBranchExprs qns brs = concatMap (go vm) $ mapMaybe match brs
       where
        match (ABranch (APattern _ (pqn, _) _) e) | pqn `elem` qns = Nothing
                                                  | otherwise = Just e
    ATyped _ e _ -> go vm e

argument 1

deterministic operation

--- Determines whether a function returns a constant result for a list of arguments
--- which might be bound to values contained in a map

<FAILING>

referentially transparent operation

no fixity defined

{({AFunc},_,_) |-> {Just,Nothing}}

constantResult

no precedence defined

{Just,Nothing}

FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr
-> Data.Map.Map Prelude.Int (Prelude.Either (String, String) [(String, String)])
-> [FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr]
-> Prelude.Maybe (FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr)

operation might suspend on free variables

possibly non-terminating

possibly non-reducible on same data term