1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
-----------------------------------------------------------------------------
--- Definition and some operations for non-fail conditions.
---
--- @author  Michael Hanus
--- @version March 2024
---------------------------------------------------------------------------

module Verify.NonFailConditions
 where

import Data.List         ( (\\), find, isPrefixOf, isSuffixOf, nub
                         , splitOn, union )

import Contract.Names    ( encodeContractName )
import FlatCurry.Goodies
import FlatCurry.Names   ( anonCons )
import FlatCurry.Types

import FlatCurry.Build
import FlatCurry.Print
import FlatCurry.Simplify
import Verify.ProgInfo

--- Non-fail conditions are represented as a pair of typed variables
--- occurring in the conditions and a Boolean expression
--- (in FlatCurry representation).
type NonFailCond = ([(Int,TypeExpr)], Expr)

--- The always unsatisfiable non-fail condition.
nfcFalse :: NonFailCond
nfcFalse = ([],fcFalse)

--- Generate a non-fail condition from a list of variables types
--- and a list of Boolean expressions.
genNonFailCond :: [(Int,TypeExpr)] -> Expr -> NonFailCond
genNonFailCond vts cond =
  let condvars = nub (allVars cond)
  -- restrict variables to occurrences in cond:
  in (filter ((`elem` condvars) . fst) vts, cond)

--- Combine two non-fail conditions.
combineNonFailConds :: NonFailCond -> NonFailCond -> NonFailCond
combineNonFailConds (vts1,cond1) (vts2,cond2) =
  (union vts1 vts2, fcAnd cond1 cond2)

------------------------------------------------------------------------------
-- Replace all variables in a FlatCurry expression by their bindings
-- passed as a mapping from variables to expressions.
expandExpr :: [(Int,TypeExpr,Expr)] -> Expr -> Expr
expandExpr bs = updVars updvar
 where
  updvar v = maybe (Var v)
                   (\(_,_,e) -> if e == Var v then e else expandExpr bs e)
                   (find (\(v',_,_) -> v' == v) bs)

-- Replace all variables (even bound variables) in a FlatCurry expression
-- by new variables. Thus, the result is a renamed variant of the input.
renameAllVars :: [(Int,Int)] -> Expr -> Expr
renameAllVars rnm = rnmE
 where
  rnmE exp = case exp of
    Var v         -> Var (rnmV v)
    Lit _         -> exp
    Comb ct qf es -> Comb ct qf (map rnmE es)
    Or e1 e2      -> Or (rnmE e1) (rnmE e2)
    Free vs e     -> Free (map rnmV vs) (rnmE e)
    Let vbs e     -> Let (map (\(v,ve) -> (rnmV v, rnmE ve)) vbs) (rnmE e)
    Case ct e brs -> Case ct (rnmE e)
                          (map (\(Branch p pe) -> Branch (rnmP p) (rnmE pe)) brs)
    Typed e t     -> Typed (rnmE e) t

  rnmV v = maybe v id (lookup v rnm)

  rnmP pat@(LPattern _) = pat
  rnmP (Pattern qc vs)  = Pattern qc (map rnmV vs)

------------------------------------------------------------------------------

--- The suffix of functions specifying non-fail conditions.
nonfailSuffix :: String
nonfailSuffix = "'nonfail"

--- Extracts explicit non-fail conditions specified in a module as
--- operations with suffix `'nonfail`.
nonFailCondsOfModule :: Prog -> [(QName,NonFailCond)]
nonFailCondsOfModule prog = map toNFCond nfconds
 where
  toNFCond fdecl = (stripNF (funcName fdecl),
                    (ruleTVars,
                     trRule (\_ exp -> exp) (const fcTrue) (funcRule fdecl)))
   where
    ruleTVars = zip (trRule (\args _ -> args) (const []) (funcRule fdecl))
                    (argTypes (funcType fdecl))

  stripNF (mn,fn) = (mn, take (length fn - length nonfailSuffix) fn)

  nfconds = filter ((nonfailSuffix `isSuffixOf`) . snd . funcName)
                   (progFuncs prog)

------------------------------------------------------------------------------
--- Returns the non-fail condition for particular predefined operations
--- with non-trivial non-fail conditions.
lookupPredefinedNonFailCond :: QName -> Maybe NonFailCond
lookupPredefinedNonFailCond qf = lookup qf predefinedNonFailConds

predefinedNonFailConds :: [(QName,NonFailCond)]
predefinedNonFailConds =
  map (\divop -> (divop, (divargs fcInt, divcond int0))) intDivOps ++
  map (\divop -> (divop, (divargs fcFloat, divcond float0))) floatDivOps ++
  map (\sqop -> (pre sqop, sqrtcond)) sqrtops
 where
  divargs te = map (\i -> (i,te)) [1,2]
  divcond lit0 = fcNot (Comb FuncCall (pre "==") [Var 2, Lit lit0])
  int0 = Intc 0
  float0 = Floatc 0

  sqrtcond = ([(1,fcFloat)], Comb FuncCall (pre ">=") [Var 1, Lit float0])
  sqrtops = [ "_impl#sqrt#Prelude.Floating#Prelude.Float#", "sqrt" ]

--- Integer division operators defined in the prelude.
intDivOps :: [QName]
intDivOps = map pre
  [ "_impl#div#Prelude.Integral#Prelude.Int#"
  , "_impl#mod#Prelude.Integral#Prelude.Int#"
  , "_impl#quot#Prelude.Integral#Prelude.Int#"
  , "_impl#rem#Prelude.Integral#Prelude.Int#"
  , "div", "mod", "quot", "rem" ]

--- Float division operators defined in the prelude.
floatDivOps :: [QName]
floatDivOps = map pre
  [ "_impl#/#Prelude.Fractional#Prelude.Float#", "/" ]

------------------------------------------------------------------------------
--- Prints a list of conditions for operations (if not empty).
--- The first argument contains all function declarations of the current module.
showConditions :: [FuncDecl] -> [(QName, NonFailCond)] -> String
showConditions fdecls = unlines . map (showCondFunc . genNonFailFunction fdecls)
 where
  showCondFunc (fn,cf) =
    "\n-- Non-fail condition of operation `" ++ fn ++ "`:\n" ++
    showFuncDecl cf

--- Generates the function representing the non-fail condition for a given
--- function and non-fail condition.
--- The first argument is the list of all functions of the module.
genNonFailFunction :: [FuncDecl] -> (QName, NonFailCond) -> (String,FuncDecl)
genNonFailFunction fdecls (qfc,(_,cnd)) =
  maybe (error $ "genNonFailFunction: function '" ++ snd qfc ++ "'' not found!")
        (\fdecl -> genNonFailFunc fdecl)
        (find (\fd -> funcName fd == qfc) fdecls)
 where
  genNonFailFunc (Func (mn,fn) ar vis texp _) =
    (fn,
     Func (mn, encodeContractName $ fn ++ nonfailSuffix) ar vis
          (nftype [1..ar] texp)
          (Rule [1..ar] (if all (`elem` [1..ar]) nfcondvars
                           then nfcondexp
                           else Free (nfcondvars \\ [1..ar]) nfcondexp)))
   where
    nftype []     _     = TCons (pre "Bool") []
    nftype (v:vs) ftype = case ftype of
      FuncType t1 t2 -> FuncType t1 (nftype vs t2)
      ForallType _ t -> nftype (v:vs) t
      _              -> error "Illegal function type in genNonFailFunction"

  nfcondexp = updCombs transClassImplOp (simpExpr cnd)
  nfcondvars = nub (allFreeVars nfcondexp)

  -- transform possible implementation of a class operation, e.g.,
  -- `_impl#minBound#Prelude.Bounded#Prelude.Char#` -> `minBound :: Char`
  transClassImplOp ct qf@(mnf,fnf) args = case splitOn "#" fnf of
    [impl,fname,_,types,_] | impl == "_impl"
       -> maybe (Comb ct (mnf,fname) args)
                (Typed (Comb ct (mnf,fname) args))
                (typeString2TExp types)
    _  -> Comb ct qf args
   where
    typeString2TExp s | s == "Prelude.Bool"      = Just fcBool
                      | s == "Prelude.Char"      = Just fcChar
                      | s == "Prelude.Int"       = Just fcInt
                      | s == "Prelude.Float"     = Just fcFloat
                      | s == "Prelude.Ordering"  = Just fcOrdering
                      | otherwise                = Nothing

-- Generate a test predicate for a given data constructor and an expression.
-- generated by `Main.aCallType2Bool`.
transTester :: [(QName,ConsInfo)] -> QName -> Expr -> Expr
transTester consinfos qc exp
  | qc == pre "True"  = exp
  | qc == pre "False" = fcNot exp
  | qc == pre "[]"    = Comb FuncCall (pre "null") [exp]
  | qc == pre ":"     = fcNot (Comb FuncCall (pre "null") [exp])
  | otherwise
  = Case Rigid exp
      ([Branch (Pattern qc (take arity [100..])) fcTrue] ++
       if null siblings then [] else [Branch (Pattern anonCons []) fcFalse])
 where
  (arity,_,siblings) = infoOfCons consinfos qc

--- Gets all free variables (i.e., without let/free/pattern bound variables)
--- occurring in an expression.
allFreeVars :: Expr -> [Int]
allFreeVars e = trExpr (:) (const id) comb lt fr (.) cas branch const e []
 where
  comb _ _ = foldr (.) id
  lt bs exp = (filter (`notElem` (map fst bs))) . exp . foldr (.) id (map snd bs)
  fr vs exp = (filter (`notElem` vs)) . exp
  cas _ exp bs = exp . foldr (.) id bs
  branch pat exp = (filter (`notElem` (args pat))) . exp
  args pat | isConsPattern pat = patArgs pat
           | otherwise = []

------------------------------------------------------------------------------