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

inferNFExpr
  :: ProgInfo (TypeDecl, [Constructor]) -> TAExpr -> (Bool, [QName], TAExpr)
inferNFExpr info expr
  = let inf = inferNFExpr info
    in case expr of
         AVar ty i -> (False, [], AVar boolType (starVar i))
         ALit _ _ -> (False, [], boolExpr "True")
         AComb _ _ (("Prelude", "failed"), _) [] ->
           (True, [], boolExpr "False")
         AComb _ _ (("Prelude", "error"), _) _ -> (True, [], boolExpr "False")
         AComb _ ConsCall _ _ -> (False, [], boolExpr "True")
         AComb _ (ConsPartCall _) _ _ -> (False, [], boolExpr "True")
         AComb _ FuncCall ((_, '_' : 'i' : 'm' : 'p' : 'l' : _), _) _ ->
           (False, [], boolExpr "True") -- TODO: Implement whitelist?
         AComb ty FuncCall (("Prelude", "apply"), _) _ ->
           (False, [], boolExpr "True")
         AComb _ FuncCall (qn@(modname, fun), qnty) es
           | isHO qnty -> (False, [], boolExpr "True")
           | otherwise ->
             ( False
             , [qn]
             , AComb boolType FuncCall
               ((modname, fun ++ "_nonfailspec"), nonFailType qnty)
               (map starVarExp es ++ es)
             )
          where
           isHO :: TypeExpr -> Bool
           isHO t = case t of
             FuncType (FuncType _ _) _ -> True
             FuncType _ t -> isHO t
             _ -> False
         AComb _ (FuncPartCall n) (qn@(modname, fun), qnty) es ->
           (False, [], boolExpr "True")
          --  ( False
          --  , [qn]
          --  , AComb boolType (FuncPartCall n)
          --    ((modname, fun ++ "_nonfailspec"), nonFailType qnty) es -- Intertwine arguments with Boolean values?
          --  )
         ALet _ binds e ->
           let (b, qs, e')          = inf e
               (bs, qss, starBinds) = unzip3
                 (map (\((v, _), exp) ->
                       let (b2, qs2, exp') = inf exp
                       in (b2, qs2, ((starVar v, boolType), exp'))) binds)
           in ( b || or bs
              , qs ++ concat qss
              , ALet boolType (starBinds ++ binds) e'
              )
         AOr _ e1 e2 ->
           let (b1, qs1, e1') = inf e1
               (b2, qs2, e2') = inf e2
               canFail        = b1 || b2
           in if canFail
                then (True, [], boolExpr "False")
                else (b1 || b2, qs1 `union` qs2, AOr boolType e1' e2')
         ACase _ ct e brs ->
           let (mdecl, misscons, _) = missingConsInBranch info brs
               (bs, qss, brs')      = unzip3
                 (map (\(ABranch p exp) -> let (b, qs, e'') = inf exp
                                           in (b, qs, ABranch p e'')) brs)
               canFail              = or bs || not (null misscons)
               qs'                  = concat qss
               e'                   = case mdecl of
                 Just (Type tqn _ vs cs) -> ACase boolType ct e
                   (map addStarVars2Branch (brs' ++ newBrs))
                  where
                   newBrs          = map c2br misscons

                   c2br c = ABranch (patGen c) (boolExpr "False")

                   cqnts           = map (\(Cons qn _ _ ts) -> (qn, ts)) cs

                   consType        = annExpr e --TCons tqn (map (TVar . fst) vs) -- TODO: Specialize type?

                   patGen (qn, ar) = APattern consType (qn, consType)
                     (zip [1 .. ar] (fromMaybe [] (lookup qn cqnts)))
                 Nothing -> ACase boolType Rigid e brs -- TODO: Literal cases
                 _ -> error "Something went wrong" -- Should not happen
               ite                  = ACase boolType Rigid (starVarExp e)
                 [ ABranch (boolPat "True") e'
                 , ABranch (boolPat "False") (boolExpr "False")
                 ]
               boolPat str = APattern boolType (("Prelude", str), boolType) []
           in (canFail, qs', ite)
         ATyped _ e ty' -> let (b, qs, e') = inf e
                           in (b, qs, ATyped boolType e' ty')
         AFree _ vars e -> let (b, qs, e') = inf e
                           in (b, qs, AFree boolType vars e')

argument 2

deterministic operation

-- TODO: type annotations => type as result?
--- Return transformed NFC expression along with information about called functions
--- and whether the expression can fail

<FAILING>

referentially transparent operation

no fixity defined

{(_,{AVar}) |-> {(,,)} || (_,{ALit}) |-> {(,,)} || (_,{AComb}) |-> {(,,)} || (_,{ALet}) |-> {(,,)} || (_,{AOr}) |-> {(,,)} || (_,{ACase}) |-> {(,,)} || (_,{ATyped}) |-> {(,,)} || (_,{AFree}) |-> {(,,)}}

inferNFExpr

no precedence defined

{(,,)}

Analysis.ProgInfo.ProgInfo (FlatCurry.Types.TypeDecl, [((String, String), Prelude.Int)])
-> FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr
-> (Prelude.Bool, [(String, String)], FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr)

operation might suspend on free variables

possibly non-terminating

possibly non-reducible on same data term