# This file is part of NIT ( http://www.nitlanguage.org ).
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#     http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

# Module to build contract
# This module provide extension of the modele to add contracts, the building phase and the "re-driving" to call the contract.
#
# FIXME Split the module in three parts: extension of the modele, building phase and the "re-driving"
module contracts

import astbuilder
import parse_annotations
import phase
import semantize
intrude import modelize_property
intrude import scope
intrude import typing

redef class ToolContext
	# Parses contracts annotations.
	var contracts_phase: Phase = new ContractsPhase(self, [modelize_property_phase,typing_phase])
end

private class ContractsPhase
	super Phase

	# The entry point of the contract phase
	# In reality, the contract phase is executed on each module
	# FIXME: Actually all method is checked to add method if any contract is inherited
	redef fun process_nmodule(nmodule)do
		# Check if the contracts are disabled
		if toolcontext.opt_no_contract.value then return
		nmodule.do_contracts(self.toolcontext)
	end
end

redef class AModule
	# Compile all contracts
	#
	# The implementation of the contracts is done in two visits.
	#
	# - First step, the visitor analyzes and constructs the contracts
	#   for each class (invariant) and method (expects, ensures).
	#
	# - Second step the visitor analyzes each `ASendExpr` to see
	#   if the callsite calls a method with a contract. If this is
	#	the case the callsite is replaced by another callsite to the contract method.
	fun do_contracts(toolcontext: ToolContext) do
		#
		var contract_visitor = new ContractsVisitor(toolcontext, toolcontext.modelbuilder.identified_modules.first, self, new ASTBuilder(mmodule.as(not null)))
		contract_visitor.enter_visit(self)
		#
		var callsite_visitor = new CallSiteVisitor(toolcontext)
		callsite_visitor.enter_visit(self)
	end
end

# This visitor checks the `AMethPropdef` and the `AClassDef` to check if they have a contract annotation or it's a redefinition with a inheritance contract
private class ContractsVisitor
	super Visitor

	var toolcontext: ToolContext

	# The main module
	# It's strore to define if the contract need to be build depending on the selected policy `--no-contract` `--full-contract` or default
	var mainmodule: MModule

	# Actual visited module
	var visited_module: AModule

	var ast_builder: ASTBuilder

	# The `ASignature` of the actual build contract
	var n_signature: ASignature is noinit

	# The `MSignature` of the actual build contract
	var m_signature: MSignature is noinit

	# The `current_location` can corresponding of the annotation or method location.
	var current_location: Location is noinit

	# Is the contrat is an introduction or not?
	var is_intro_contract: Bool is noinit

	# Actual visited class
	var visited_class: nullable AClassdef

	# is `no_contract` annotation was found
	var find_no_contract = false

	redef fun visit(node)
	do
		node.create_contracts(self)
		node.visit_all(self)
	end

	# Method use to define the signature part of the method `ASignature` and `MSignature`
	# The given `mcontract` provided `adapt_nsignature` and `adapt_msignature` to copy and adapt the given signature (`nsignature` and `msignature`)
	fun define_signature(mcontract: MContract, nsignature: nullable ASignature, msignature: nullable MSignature)
	do
		if nsignature != null and msignature != null then nsignature.ret_type = msignature.return_mtype
		self.n_signature = mcontract.adapt_nsignature(nsignature)
		self.m_signature = mcontract.adapt_msignature(msignature)
	end

	# Define the new contract take in consideration that an old contract exist or not
	private fun build_contract(n_annotation: AAnnotation, mcontract: MContract, mclassdef: MClassDef): MMethodDef
	do
		self.current_location = n_annotation.location
		# Retrieving the expression provided in the annotation
		var n_condition = n_annotation.construct_condition(self)
		var m_contractdef: AMethPropdef
		if is_intro_contract then
			# Create new contract method
			m_contractdef = mcontract.create_intro_contract(self, n_condition, mclassdef)
		else
			# Create a redef of contract to take in consideration the new condition
			m_contractdef = mcontract.create_subcontract(self, n_condition, mclassdef)
		end
		var contract_propdef = m_contractdef.mpropdef
		# The contract has a null mpropdef, this should never happen
		assert contract_propdef != null
		return contract_propdef
	end

	# Verification if the construction of the contract is necessary.
	# Three cases are checked for `expects`:
	#
	# - Is the `--full-contract` option it's use?
	# - Is the method is in the main package
	# - Is the method is in a direct imported package.
	#
	fun check_usage_expects(actual_mmodule: MModule): Bool
	do
		var main_package = mainmodule.mpackage
		var actual_package = actual_mmodule.mpackage
		if main_package != null and actual_package != null then
			var condition_direct_arc = toolcontext.modelbuilder.model.mpackage_importation_graph.has_arc(main_package, actual_package)
			return toolcontext.opt_full_contract.value or condition_direct_arc or main_package == actual_package
		end
		return false
	end

	# Verification if the construction of the contract is necessary.
	# Two cases are checked for `ensures`:
	#
	# - Is the `--full-contract` option it's use?
	# - Is the method is in the main package
	#
	fun check_usage_ensures(actual_mmodule: MModule): Bool
	do
		return toolcontext.opt_full_contract.value or mainmodule.mpackage == actual_mmodule.mpackage
	end

end

# This visitor checks the `callsite` to see if the target `mpropdef` has a contract.
private class CallSiteVisitor
	super Visitor

	var toolcontext: ToolContext

	# Actual visited method
	var visited_method: APropdef is noinit

	redef fun visit(node)
	do
		node.check_callsite(self)
		node.visit_all(self)
	end

	# Check if the callsite calls a method with a contract.
	# If it's the case the callsite is replaced by another callsite to the contract method.
	private fun drive_method_contract(callsite: CallSite): CallSite
	do
		if callsite.mpropdef.has_contract then
			var contract_facet = callsite.mproperty.mcontract_facet
			var visited_mpropdef = visited_method.mpropdef
			assert contract_facet != null and visited_mpropdef != null

			var unsafe_mtype = callsite.recv.resolve_for(visited_mpropdef.mclassdef.bound_mtype, callsite.anchor, visited_mpropdef.mclassdef.mmodule, true)

			# This check is needed because the contract can appear after the introduction.
			if unsafe_mtype.has_mproperty(visited_method.mpropdef.mclassdef.mmodule, contract_facet) then
				var type_visitor = new TypeVisitor(toolcontext.modelbuilder, visited_mpropdef)
				var drived_callsite = type_visitor.build_callsite_by_property(visited_method, callsite.recv, contract_facet, callsite.recv_is_self)
				# This never happen this check is here for debug
				assert drived_callsite != null
				return drived_callsite
			end
		end
		return callsite
	end
end

redef class ANode
	private fun create_contracts(v: ContractsVisitor) do end
	private fun check_callsite(v: CallSiteVisitor) do end
end

redef class AAnnotation

	# Returns the conditions of annotation parameters in the form of and expr
	# exemple:
	# the contract ensures(true, i == 10, f >= 1.0)
	# return this condition (true and i == 10 and f >= 1.0)
	private fun construct_condition(v : ContractsVisitor): AExpr
	do
		var n_condition = n_args.first
		n_args.remove_at(0)
		for n_arg in n_args do n_condition = v.ast_builder.make_and(n_condition, n_arg)
		return n_condition
	end
end

# The root of all contracts
#
# The objective of this class is to provide the set
# of services must be implemented or provided by a contract
abstract class MContract
	super MMethod

	# Define the name of the contract
	fun contract_name: String is abstract

	# Method use to diplay warning when the contract is not present at the introduction
	private fun no_intro_contract(v: ContractsVisitor, a: AAnnotation)do end

	# Creating specific inheritance block contract
	private fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr is abstract

	# Method to adapt the `n_mpropdef.n_block` to the contract
	private fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef) is abstract

	# Adapt the msignature specifically for the contract method
	private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_condition

	# Adapt the nsignature specifically for the contract method
	private fun adapt_specific_nsignature(n_signature: ASignature): ASignature do return n_signature.adapt_to_condition(null)

	# Adapt the `m_signature` to the contract
	# If it is not null call the specific adapt `m_signature` for the contract
	private fun adapt_msignature(m_signature: nullable MSignature): MSignature
	do
		if m_signature == null then return new MSignature(new Array[MParameter])
		return adapt_specific_msignature(m_signature)
	end

	# Adapt the `n_signature` to the contract
	# If it is not null call the specific adapt `n_signature` for the contract
	private fun adapt_nsignature(n_signature: nullable ASignature): ASignature
	do
		if n_signature == null then return new ASignature
		return adapt_specific_nsignature(n_signature)
	end

	# Create a new empty contract
	private fun create_empty_contract(v: ContractsVisitor, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature)
	do
		var n_contract_def = intro_mclassdef.mclass.create_empty_method(v, self, mclassdef, msignature, n_signature)
		n_contract_def.do_all(v.toolcontext)
	end

	# Create the initial contract (intro)
	# All contracts have the same implementation for the introduction.
	#
	# fun contrat([...])
	# do
	#	assert contract_condition
	# end
	#
	private fun create_intro_contract(v: ContractsVisitor, n_condition: nullable AExpr, mclassdef: MClassDef): AMethPropdef
	do
		var n_block = v.ast_builder.make_block
		if n_condition != null then
			# Create a new tid to set the name of the assert for more explicit error
			var tid = new TId.init_tk(self.location)
			tid.text = "{self.contract_name}"
			n_block.add v.ast_builder.make_assert(tid, n_condition, null)
		end
		return make_contract(v, n_block, mclassdef)
	end

	# Create a contract with old (super) and the new conditions
	private fun create_subcontract(v: ContractsVisitor, ncondition: nullable AExpr, mclassdef: MClassDef): AMethPropdef
	do
		var args = v.n_signature.make_parameter_read(v.ast_builder)
		var n_block = v.ast_builder.make_block
		if ncondition != null then n_block = self.create_nblock(v, ncondition, args)
		return make_contract(v, n_block, mclassdef)
	end

	# Build a method with a specific block `n_block` in a specified `mclassdef`
	private fun make_contract(v: ContractsVisitor, n_block: AExpr, mclassdef: MClassDef): AMethPropdef
	do
		var n_contractdef = intro_mclassdef.mclass.create_empty_method(v, self, mclassdef, v.m_signature, v.n_signature)
		n_contractdef.n_block = n_block
		# Define the location of the new method for corresponding of the annotation location
		n_contractdef.location = v.current_location
		n_contractdef.do_all(v.toolcontext)
		return n_contractdef
	end
end

# A expect (precondition) contract representation
# This method check if the requirements of the called method is true.
class MExpect
	super MContract

	# Define the name of the contract
	redef fun contract_name: String do return "expects"

	# Display warning if no contract is defined at introduction `expect`,
	# because if no contract is defined at the introduction the added
	# contracts will not cause any error even if they are not satisfied.
	#
	# exemple
	# ~~~nitish
	# class A
	# 	fun bar [...]
	# 	fun _bar_expects([...])
	# 	do
	# 		[empty contract]
	# 	end
	# end
	#
	# redef class A
	# 	redef fun bar is expects(contract_condition)
	# 	redef fun _bar_expects([...])
	# 	do
	# 		if not (contract_condition) then super
	# 	end
	# end
	# ~~~~
	#
	redef fun no_intro_contract(v: ContractsVisitor, a: AAnnotation)
	do
		v.toolcontext.warning(a.location,"","Useless contract: No contract defined at the introduction of the method")
	end

	redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr
	do
		# Creating the if expression with the new condition
		var if_block = v.ast_builder.make_if(n_condition, n_condition.mtype)
		# Creating and adding return expr to the then case
		if_block.n_then = v.ast_builder.make_return(null)
		# Creating the super call to the contract and adding this to else case
		if_block.n_else = v.ast_builder.make_super_call(args,null)
		var n_block = v.ast_builder.make_block
		n_block.add if_block
		return n_block
	end

	redef fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef)
	do
		var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true)
		var n_self = new ASelfExpr
		var args = n_mpropdef.n_signature.make_parameter_read(v.ast_builder)
		var n_callexpect = v.ast_builder.make_call(n_self,callsite,args)
		# Creation of the new instruction block with the call to expect condition
		var actual_expr = n_mpropdef.n_block
		var new_block = new ABlockExpr
		new_block.n_expr.push n_callexpect
		if actual_expr isa ABlockExpr then
			new_block.n_expr.add_all(actual_expr.n_expr)
		else if actual_expr != null then
			new_block.n_expr.push(actual_expr)
		end
		n_mpropdef.n_block = new_block
	end
end

# The root of all contracts where the call is after the execution of the original method (`invariants` and `ensures`).
abstract class BottomMContract
	super MContract

	redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr
	do
		var tid = new TId.init_tk(v.current_location)
		tid.text = "{contract_name}"
		# Creating the assert expression with the new condition
		var assert_block = v.ast_builder.make_assert(tid,n_condition,null)
		# Creating the super call to the contract
		var super_call = v.ast_builder.make_super_call(args,null)
		# Define contract block
		var n_block = v.ast_builder.make_block
		# Adding the expressions to the block
		n_block.add super_call
		n_block.add assert_block
		return n_block
	end

	# Inject the result variable in the `n_block` of the given `n_mpropdef`.
	private fun inject_result(v: ContractsVisitor, n_mpropdef: AMethPropdef, ret_type: MType): Variable
	do
		var actual_block = n_mpropdef.n_block
		# never happen. If it's the case the problem is in the contract facet building
		assert actual_block isa ABlockExpr

		var return_var: nullable Variable = null

		var return_expr = actual_block.n_expr.last.as(AReturnExpr)

		var returned_expr = return_expr.n_expr
		# The return node has no returned expression
		assert returned_expr != null

		# Check if the result variable already exit
		if returned_expr isa AVarExpr then
			if returned_expr.variable.name == "result" then
				return_var = returned_expr.variable
			end
		end

		return_var = new Variable("result")
		# Creating a new variable to keep the old return of the method
		var assign_result = v.ast_builder.make_var_assign(return_var, returned_expr)
		# Remove the actual return
		actual_block.n_expr.pop
		# Set the return type
		return_var.declared_type = ret_type
		# Adding the reading expr of result variable to the block
		actual_block.add assign_result
		# Expr to read the result variable
		var read_result = v.ast_builder.make_var_read(return_var, ret_type)
		# Definition of the new return
		return_expr = v.ast_builder.make_return(read_result)
		actual_block.add return_expr
		return return_var
	end
end

# A ensure (postcondition) representation
# This method check if the called method respects the expectations of the caller.
class MEnsure
	super BottomMContract

	# Define the name of the contract
	redef fun contract_name: String do return "ensures"

	redef fun adapt_specific_msignature(m_signature: MSignature): MSignature
	do
		return m_signature.adapt_to_ensurecondition
	end

	redef fun adapt_specific_nsignature(n_signature: ASignature): ASignature
	do
		return n_signature.adapt_to_ensurecondition
	end

	redef fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef)
	do
		var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true)
		var n_self = new ASelfExpr
		# argument to call the contract method
		var args = n_mpropdef.n_signature.make_parameter_read(v.ast_builder)
		# Inject the variable result
		# The cast is always safe because the online adapted method is the contract facet

		var actual_block = n_mpropdef.n_block
		# never happen. If it's the case the problem is in the contract facet building
		assert actual_block isa ABlockExpr

		var ret_type = n_mpropdef.mpropdef.mproperty.intro.msignature.return_mtype
		if ret_type != null then
			var result_var = inject_result(v, n_mpropdef, ret_type)
			# Expr to read the result variable
			var read_result = v.ast_builder.make_var_read(result_var, ret_type)
			var return_expr = actual_block.n_expr.pop
			# Adding the read return to argument
			args.add(read_result)
			var n_callcontract = v.ast_builder.make_call(n_self,callsite,args)
			actual_block.add_all([n_callcontract,return_expr])
		else
			# build the call to the contract method
			var n_callcontract = v.ast_builder.make_call(n_self,callsite,args)
			actual_block.add n_callcontract
		end
	end
end

redef class MClass

	# This method create an abstract method representation with this MMethodDef an this AMethoddef
	private fun create_abstract_method(v: ContractsVisitor, mproperty: MMethod, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature): AMethPropdef
	do
		# new methoddef definition
		var m_def = new MMethodDef(mclassdef, mproperty, v.current_location)
		# set the signature
		if msignature != null then m_def.msignature = msignature.clone
		# set the abstract flag
		m_def.is_abstract = true
		# Build the new node method
		var n_def = v.ast_builder.make_method(null,null,m_def,n_signature,null,null,null,null)
		# Define the location of the new method for corresponding of the actual method
		n_def.location = v.current_location
		# Association new npropdef to mpropdef
		v.toolcontext.modelbuilder.unsafe_add_mpropdef2npropdef(m_def,n_def)
		return n_def
	end

	# Create method with an empty block
	# the `mproperty` i.e the global property definition. The mclassdef to set where the method is declared and it's model `msignature` and ast `n_signature` signature
	private fun create_empty_method(v: ContractsVisitor, mproperty: MMethod, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature): AMethPropdef
	do
		var n_def = create_abstract_method(v, mproperty, mclassdef, msignature, n_signature)
		n_def.mpropdef.is_abstract = false
		n_def.n_block = v.ast_builder.make_block
		return n_def
	end
end

redef class MMethod

	# The contract facet of the method
	# it's representing the method with contract
	# This method call the contract and the method
	var mcontract_facet: nullable MMethod = null

	# The expected contract method
	var mexpect: nullable MExpect = null

	# The ensure contract method
	var mensure: nullable MEnsure = null

	# Check if the MMethod has no ensure contract
	# if this is the case returns false and built it
	# else return true
	private fun check_exist_ensure: Bool
	do
		if self.mensure != null then return true
		# build a new `MEnsure` contract
		self.mensure = new MEnsure(intro_mclassdef, "_ensures_{name}", intro_mclassdef.location, public_visibility)
		return false
	end

	# Check if the MMethod has no expect contract
	# if this is the case returns false and built it
	# else return true
	private fun check_exist_expect: Bool
	do
		if self.mexpect != null then return true
		# build a new `MExpect` contract
		self.mexpect = new MExpect(intro_mclassdef, "_expects_{name}", intro_mclassdef.location, public_visibility)
		return false
	end

	# Check if the MMethod has an contract facet
	# If the method has no contract facet she create it
	private fun check_exist_contract_facet(mpropdef : MMethodDef): Bool
	do
		if self.mcontract_facet != null then return true
		# build a new `MMethod` contract
		self.mcontract_facet = new MMethod(mpropdef.mclassdef, "_contract_{name}", mpropdef.mclassdef.location, public_visibility)
		return false
	end
end

redef class MMethodDef

	# Verification of the contract facet
	# Check if a contract facet already exists to use it again or if it is necessary to create it.
	private fun check_contract_facet(v: ContractsVisitor, n_signature: ASignature, mcontract: MContract, exist_contract: Bool)
	do
		var exist_contract_facet = mproperty.check_exist_contract_facet(self)
		if exist_contract_facet and exist_contract then return

		var contract_facet: AMethPropdef
		if not exist_contract_facet then
			# If has no contract facet just create it
			contract_facet = create_contract_facet(v, n_signature)
		else
			# Check if the contract facet already exist in this context (in this mclassdef)
			if mclassdef.mpropdefs_by_property.has_key(mproperty.mcontract_facet) then
				# get the define
				contract_facet = v.toolcontext.modelbuilder.mpropdef2node(mclassdef.mpropdefs_by_property[mproperty.mcontract_facet]).as(AMethPropdef)
			else
				# create a new contract facet definition
				contract_facet = create_contract_facet(v, n_signature)
				var block = v.ast_builder.make_block
				# super call to the contract facet
				var n_super_call = v.ast_builder.make_super_call(n_signature.make_parameter_read(v.ast_builder), null)
				# verification for add a return or not
				if contract_facet.mpropdef.msignature.return_mtype != null then
					block.add(v.ast_builder.make_return(n_super_call))
				else
					block.add(n_super_call)
				end
				contract_facet.n_block = block
			end
		end
		contract_facet.adapt_block_to_contract(v, mcontract, contract_facet)
		contract_facet.location = v.current_location
		contract_facet.do_all(v.toolcontext)
	end

	# Method to create a contract facet of the method
	private fun create_contract_facet(v: ContractsVisitor, n_signature: ASignature): AMethPropdef
	do
		var contract_facet = mproperty.mcontract_facet
		assert contract_facet != null
		# Defines the contract phase is an init or not
		# it is necessary to use the contracts on constructor
		contract_facet.is_init = self.mproperty.is_init

		# check if the method has an `msignature` to copy it.
		var m_signature: nullable MSignature = null
		if mproperty.intro.msignature != null then m_signature = mproperty.intro.msignature.clone

		var n_contractdef = mclassdef.mclass.create_empty_method(v, contract_facet, mclassdef, m_signature, n_signature)
		# FIXME set the location because the callsite creation need the node location
		n_contractdef.location = v.current_location
		n_contractdef.validate

		var block = v.ast_builder.make_block
		var n_self = new ASelfExpr
		var args = n_contractdef.n_signature.make_parameter_read(v.ast_builder)
		var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_contractdef, mproperty, true)
		var n_call = v.ast_builder.make_call(n_self, callsite, args)

		if m_signature.return_mtype == null then
			block.add(n_call)
		else
			block.add(v.ast_builder.make_return(n_call))
		end

		n_contractdef.n_block = block
		n_contractdef.do_all(v.toolcontext)
		return n_contractdef
	end

	# Entry point to build contract (define the contract facet and define the contract method verification)
	private fun construct_contract(v: ContractsVisitor, n_signature: ASignature, n_annotation: AAnnotation, mcontract: MContract, exist_contract: Bool)
	do
		if check_same_contract(v, n_annotation, mcontract) then return
		if not exist_contract and not is_intro then no_intro_contract(v, n_signature, mcontract, n_annotation)
		v.define_signature(mcontract, n_signature, mproperty.intro.msignature)

		var conditiondef = v.build_contract(n_annotation, mcontract, mclassdef)
		check_contract_facet(v, n_signature.clone, mcontract, exist_contract)
		has_contract = true
	end

	# Create a contract on the introduction classdef of the property.
	# Display an warning message if necessary
	private fun no_intro_contract(v: ContractsVisitor, n_signature: ASignature, mcontract: MContract, n_annotation: AAnnotation)
	do
		mcontract.create_empty_contract(v, mcontract.intro_mclassdef, mcontract.adapt_msignature(self.mproperty.intro.msignature), mcontract.adapt_nsignature(n_signature))
		mcontract.no_intro_contract(v, n_annotation)
		mproperty.intro.has_contract = true
	end

	# Is the contract already defined in the context
	#
	# Exemple :
	# fun foo is expects([...]), expects([...])
	#
	# Here `check_same_contract` display an error when the second expects is processed
	private fun check_same_contract(v: ContractsVisitor, n_annotation: AAnnotation ,mcontract: MContract): Bool
	do
		if self.mclassdef.mpropdefs_by_property.has_key(mcontract) then
			v.toolcontext.error(n_annotation.location, "The method already has a defined `{mcontract.contract_name}` contract at line {self.mclassdef.mpropdefs_by_property[mcontract].location.line_start}")
			return true
		end
		return false
	end
end

redef class MPropDef
	# flag to indicate is the `MPropDef` has a contract
	var has_contract = false
end

redef class APropdef
	redef fun check_callsite(v)
	do
		v.visited_method = self
	end
end

redef class AMethPropdef

	# Execute all method verification scope flow and typing.
	# It also execute an ast validation to define all parents and all locations
	private fun do_all(toolcontext: ToolContext)
	do
		self.validate
		# FIXME: The `do_` usage it is maybe to much (verification...). Solution: Cut the `do_` methods into simpler parts
		self.do_scope(toolcontext)
		self.do_flow(toolcontext)
		self.do_typing(toolcontext.modelbuilder)
	end

	# Entry point to create a contract (verification of inheritance, or new contract).
	redef fun create_contracts(v)
	do
		v.ast_builder.check_mmodule(mpropdef.mclassdef.mmodule)

		v.current_location = self.location
		v.is_intro_contract = mpropdef.is_intro

		if n_annotations != null then
			for n_annotation in n_annotations.n_items do
				check_annotation(v,n_annotation)
			end
		end

		if not mpropdef.is_intro and not v.find_no_contract then
			self.check_redef(v)
		end

		# reset the flag
		v.find_no_contract = false
	end

	# Verification of the annotation to know if it is a contract annotation.
	# If this is the case, we built the appropriate contract.
	private fun check_annotation(v: ContractsVisitor, n_annotation: AAnnotation)
	do
		if n_annotation.name == "expects" then
			if not v.check_usage_expects(mpropdef.mclassdef.mmodule) then return
			var exist_contract = mpropdef.mproperty.check_exist_expect
			mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.mexpect.as(not null), exist_contract)
		else if n_annotation.name == "ensures" then
			if not v.check_usage_ensures(mpropdef.mclassdef.mmodule) then return
			var exist_contract = mpropdef.mproperty.check_exist_ensure
			mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.mensure.as(not null), exist_contract)
		else if n_annotation.name == "no_contract" then
			# no_contract found set the flag to true
			v.find_no_contract = true
		end
	end

	# Verification if the method have an inherited contract to apply it.
	private fun check_redef(v: ContractsVisitor)
	do
		# Check if the method has an attached contract
		if not mpropdef.has_contract then
			if mpropdef.mproperty.intro.has_contract then
				mpropdef.has_contract = true
			end
		end
	end

	# Adapt the block to use the contracts
	private fun adapt_block_to_contract(v: ContractsVisitor, contract: MContract, n_mpropdef: AMethPropdef)
	do
		contract.adapt_block_to_contract(v, n_mpropdef)
		mpropdef.has_contract = true
		n_mpropdef.do_all(v.toolcontext)
	end
end

redef class MSignature

	# Adapt signature for a expect condition
	# Removed the return type is it not necessary
	private fun adapt_to_condition: MSignature do return new MSignature(mparameters.to_a, null)

	# Adapt signature for a ensure condition
	#
	# Create new parameter with the return type
	private fun adapt_to_ensurecondition: MSignature
	do
		var rtype = return_mtype
		var msignature = adapt_to_condition
		if rtype != null then
			msignature.mparameters.add(new MParameter("result", rtype, false))
		end
		return msignature
	end

	# Adapt signature for a expect condition
	# Removed the return type is it not necessary
	private fun clone: MSignature do return new MSignature(mparameters.to_a, return_mtype)
end

redef class ASignature

	# Create an array of AVarExpr representing the read of every parameters
	private fun make_parameter_read(ast_builder: ASTBuilder): Array[AVarExpr]
	do
		var args = new Array[AVarExpr]
		for n_param in self.n_params do
			var mtype = n_param.variable.declared_type
			var variable = n_param.variable
			if variable != null and mtype != null then
				args.push ast_builder.make_var_read(variable, mtype)
			end
		end
		return args
	end

	# Return a copy of self adapted for the expect condition
	# npropdef it is use to define the parent of the parameters
	private fun adapt_to_condition(return_type: nullable AType): ASignature
	do
		var adapt_nsignature = self.clone
		adapt_nsignature.n_type = return_type
		return adapt_nsignature
	end

	# Return a copy of self adapted for postcondition on npropdef
	private fun adapt_to_ensurecondition: ASignature do
		var nsignature = adapt_to_condition(null)
		if ret_type != null then
			var n_id = new TId
			n_id.text = "result"
			var new_param = new AParam
			new_param.n_id = n_id
			new_param.variable = new Variable(n_id.text)
			new_param.variable.declared_type = ret_type
			nsignature.n_params.add new_param
		end
		return nsignature
	end
end

redef class ASendExpr
	redef fun check_callsite(v)
	do
		var actual_callsite = callsite
		if actual_callsite != null then
			callsite = v.drive_method_contract(actual_callsite)
		end
	end
end

redef class ANewExpr
	redef fun check_callsite(v)
	do
		var actual_callsite = callsite
		if actual_callsite != null then
			callsite = v.drive_method_contract(actual_callsite)
		end
	end
end