CurryInfo: verify-non-fail-2.0.0 / FlatCurry.Names

 
--------------------------------------------------------------------------
Definition of some standard names in FlatCurry programs used in this tool
together with their SMT names.

@author  Michael Hanus
@version September 2024
------------------------------------------------------------------------

 FlatCurry.Names

 anonCons binaryPrimOps isPrimOp preludePrimOps unaryPrimOps

 

module FlatCurry.Names where

import FlatCurry.Build ( pre )
import FlatCurry.Types
import qualified FlatCurry.Names2SMT

----------------------------------------------------------------------------
--- An "anonymous" constructor is used to represent case expressions
--- with a final "catch all" alternative.
anonCons :: QName
anonCons = pre "_"

----------------------------------------------------------------------------
--- Is a qualified FlatCurry name primitive?
isPrimOp :: QName -> Bool
isPrimOp (mn,fn) = mn=="Prelude" && fn `elem` map fst preludePrimOps

--- Primitive operations of the prelude and their SMT names.
preludePrimOps :: [(String,String)]
preludePrimOps = unaryPrimOps ++ binaryPrimOps ++
  [("otherwise","True")
  ,("apply","apply") -- TODO...
  ]

--- Primitive unary operations of the prelude and their SMT names.
unaryPrimOps :: [(String,String)]
unaryPrimOps = FlatCurry.Names2SMT.unaryPrimOps

--- Primitive binary operations of the prelude and their SMT names.
binaryPrimOps :: [(String,String)]
binaryPrimOps = map transEqu2 (drop 2 FlatCurry.Names2SMT.binaryPrimOps)
 where
  transEqu2 (fc,fsmt) = (fc, if fsmt == "=" then "==" else fsmt)

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

 safe