CurryInfo: contract-prover-4.0.0 / ContractProver.extractPostConditionProofObligation

 
extractPostConditionProofObligation :: VerifyInfo -> [Int] -> Int -> TARule
                                    -> TransStateM Term
extractPostConditionProofObligation _ _ _ (AExternal _ s) =
  return $ tComb ("External: " ++ s) []
extractPostConditionProofObligation ti args resvar
                                    (ARule ty orgargs orgexp) = do
  let exp    = rnmAllVars renameRuleVar orgexp
      rtype  = resType (length orgargs) (stripForall ty)
  put $ makeTransState (maximum (resvar : allVars exp) + 1)
                       ((resvar, rtype) : zip args (map snd orgargs))
  binding2SMT True ti (resvar,exp)
 where
  maxArgResult = maximum (resvar : args)
  renameRuleVar r = maybe (r + maxArgResult + 1)
                          (args!!)
                          (elemIndex r (map fst orgargs))

  resType n te =
    if n==0
      then te
      else case te of
             FuncType _ rt -> resType (n-1) rt
             _             -> error $ "Internal errror: resType: " ++ show te

 argument 4

 deterministic operation

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,_,_,{AExternal}) |-> _ || (_,_,_,{ARule}) |-> _}

 extractPostConditionProofObligation

 no precedence defined

 _

 VerifierState.VerifyInfo -> [Prelude.Int] -> Prelude.Int
-> FlatCurry.Annotated.Types.ARule FlatCurry.Types.TypeExpr
-> Control.Monad.Trans.State.StateT TransState Prelude.IO ESMT.Term

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term