include "primitives.alh"
include "library.alh"
include "object_operations.alh"
include "constructors.alh"
include "modelling.alh"
include "typing.alh"

Boolean function wrap_conformance(model : Element):
	String result
	result = conformance_scd(model)
	output("Success: " + result)
	if (result == "OK"):
		return True!
	else:
		return False!

Boolean function is_direct_instance(model : Element, instance : String, type : String):
	// Just check whether or not the type mapping specifies the type as the type of the instance
	return (read_type(model, instance) == type)!

Boolean function is_nominal_instance(model : Element, instance : String, type : String):
	if (read_type(model, instance) == type):
		return True!

	if (bool_not(dict_in(model["metamodel"]["model"], type))):
		// type is not even in the specified metamodel, so this will never work
		return False!

	if (bool_and(is_edge(model["metamodel"]["model"][type]), bool_not(is_edge(model["model"][instance])))):
		// type is an edge, but we aren't
		return False!

	if (element_eq(read_type(model, instance), read_root())):
		// doesn't even have a type
		return False!

	return is_nominal_subtype(model["metamodel"], read_type(model, instance), type)!

Boolean function is_nominal_subtype(metamodel : Element, subclass : String, superclass : String):
	if (element_eq(metamodel["model"][subclass], metamodel["model"][superclass])):
		return True!

	if (bool_not(dict_in(metamodel["model"], subclass))):
		return False!

	if (bool_not(dict_in(metamodel["model"], superclass))):
		return False!

	return set_in(get_superclasses(metamodel, subclass), superclass)!

Element function precompute_cardinalities(model : Element):
	Integer slc
	Integer suc
	Integer tlc
	Integer tuc
	String key
	Element tmp_dict
	Element cardinalities
	Element keys
	Element metamodel
	Boolean optional

	metamodel = model["metamodel"]
	keys = allInstances(metamodel, "Association")

	cardinalities = dict_create()
	while (0 < set_len(keys)):
		key = set_pop(keys)
		tmp_dict = dict_create()
		slc = read_attribute(metamodel, key, "source_lower_cardinality")
		suc = read_attribute(metamodel, key, "source_upper_cardinality")
		tlc = read_attribute(metamodel, key, "target_lower_cardinality")
		tuc = read_attribute(metamodel, key, "target_upper_cardinality")

		if (element_neq(slc, read_root())):
			dict_add_fast(tmp_dict, "slc", slc)
		if (element_neq(suc, read_root())):
			dict_add_fast(tmp_dict, "suc", suc)
		if (element_neq(tlc, read_root())):
			dict_add_fast(tmp_dict, "tlc", tlc)
		if (element_neq(tuc, read_root())):
			dict_add_fast(tmp_dict, "tuc", tuc)

		if (dict_len(tmp_dict) > 0):
			dict_add_fast(cardinalities, key, tmp_dict)

	keys = allInstances(metamodel, "AttributeLink")
	while (0 < set_len(keys)):
		key = set_pop(keys)
		tmp_dict = dict_create()

		// Attributes always have 1 max
		dict_add_fast(tmp_dict, "tuc", 1)

		// Depending on whether it is optional or not, the cardinality is changed
		optional = read_attribute(metamodel, key, "optional")
		if (optional):
			dict_add_fast(tmp_dict, "tlc", 0)
		else:
			dict_add_fast(tmp_dict, "tlc", 1)

		if (dict_len(tmp_dict) > 0):
			dict_add_fast(cardinalities, key, tmp_dict)

	return cardinalities!

String function conformance_scd(model : Element):
	// Initialization
	Element keys
	Element metamodel
	Element typing
	String model_name
	String src_model
	String dst_model
	String src_metamodel
	String dst_metamodel
	Element element
	Element check_list
	String check_type
	Element cardinalities
	Element scd
	Integer instances
	String type_name
	Element spo_cache
	Element spi_cache
	Element constraint_function

	Element reverse_m
	Element reverse_mm
	reverse_m = make_reverse_dictionary(model["model"])
	reverse_mm = make_reverse_dictionary(model["metamodel"]["model"])

	spo_cache = dict_create()
	spi_cache = dict_create()

	// Load in variables
	scd = import_node("models/SimpleClassDiagrams")
	metamodel = model["metamodel"]
	typing = get_type_mapping_as_dict(model)

	// Create dictionary with all associations and allowed cardinalities
	if (dict_len(model["model"]) > 0):
		cardinalities = precompute_cardinalities(model)

		// Iterate over each element of the model, finding out whether everything is fine
		keys = dict_keys(model["model"])
		while (0 < list_len(keys)):
			model_name = set_pop(keys)
			type_name = read_type(model, model_name)
			element = model["model"][model_name]

			//log("Check " + model_name)
			//log("   : " + type_name)

			if (bool_not(dict_in(typing, model_name))):
				return "Model has no type specified: " + model_info(model, model_name)!

			if (bool_not(dict_in(metamodel["model"], typing[model_name]))):
				return "Type of element not in specified metamodel: " + model_info(model, model_name)!

			if (is_edge(element)):
				src_model = reverse_m[cast_id(read_edge_src(element))]
				dst_model = reverse_m[cast_id(read_edge_dst(element))]
				src_metamodel = reverse_mm[cast_id(read_edge_src(metamodel["model"][typing[model_name]]))]
				dst_metamodel = reverse_mm[cast_id(read_edge_dst(metamodel["model"][typing[model_name]]))]

				if (bool_not(is_nominal_instance(model, src_model, src_metamodel))):
					log("got: " + src_model)
					log("expected: " + src_metamodel)
					return "Source of model edge not typed by source of type: " + model_info(model, model_name) + " Expected: " + src_metamodel + " Got: " + src_model!

				if (bool_not(is_nominal_instance(model, dst_model, dst_metamodel))):
					log("got: " + dst_model)
					log("expected: " + dst_metamodel)
					return "Destination of model edge not typed by source of type: " + model_info(model, model_name) + " Expected: " + dst_metamodel + " Got: " + dst_model!

			// Check cardinality for all of our edges
			//
			//      SLC..SUC     TLC..TUC
			//   A  ---------------------> B
			//
			// First the incoming, so we are at B in the above figure
			if (bool_not(dict_in(spo_cache, type_name))):
				dict_add_fast(spo_cache, type_name, selectPossibleOutgoing(metamodel, type_name, dict_keys(cardinalities)))

			check_list = set_copy(spo_cache[type_name])
			while (0 < list_len(check_list)):
				check_type = set_pop(check_list)
				if (dict_in(cardinalities, check_type)):
					// Cardinalities defined for this association, so check them
					if (bool_or(dict_in(cardinalities[check_type], "tlc"), dict_in(cardinalities[check_type], "tuc"))):
						instances = list_len(allOutgoingAssociationInstances(model, model_name, check_type))
						if (dict_in(cardinalities[check_type], "tlc")):
							// A lower cardinality was defined at the target
							if (integer_gt(cardinalities[check_type]["tlc"], instances)):
								String error
								error = "Lower cardinality violation for outgoing edge of type " + check_type + " at " + model_info(model, model_name)
								return error!
						if (dict_in(cardinalities[check_type], "tuc")):
							// An upper cardinality was defined at the target
							if (integer_lt(cardinalities[check_type]["tuc"], instances)):
								String error
								error = "Upper cardinality violation for outgoing edge of type " + check_type + " at " + model_info(model, model_name)
								return error!

			// Identical, but for outgoing, and thus for A in the figure
			if (bool_not(dict_in(spi_cache, type_name))):
				dict_add_fast(spi_cache, type_name, selectPossibleIncoming(metamodel, type_name, dict_keys(cardinalities)))

			check_list = set_copy(spi_cache[type_name])
			while (0 < list_len(check_list)):
				check_type = set_pop(check_list)
				if (dict_in(cardinalities, check_type)):
					// Cardinalities defined for this association, so check them
					if (bool_or(dict_in(cardinalities[check_type], "slc"), dict_in(cardinalities[check_type], "suc"))):
						instances = list_len(allIncomingAssociationInstances(model, model_name, check_type))
						if (dict_in(cardinalities[check_type], "slc")):
							// A lower cardinality was defined at the source
							if (integer_gt(cardinalities[check_type]["slc"], instances)):
								String error
								error = "Lower cardinality violation for incoming edge of type " + check_type + " at " + model_info(model, model_name)
								return error!
						if (dict_in(cardinalities[check_type], "suc")):
							// An upper cardinality was defined at the source
							if (integer_lt(cardinalities[check_type]["suc"], instances)):
								String error
								error = "Upper cardinality violation for incoming edge of type " + check_type + " at " + model_info(model, model_name)
								return error!

			constraint_function = read_attribute(metamodel, typing[model_name], "constraint")
			if (element_neq(constraint_function, read_root())):
				String result
				Element func

				log("Fetching local constraint at location " + cast_string(constraint_function))
				func = get_func_AL_model(import_node(constraint_function))
				result = func(model, model_name)

				if (result != "OK"):
					return result!

	// Check multiplicities, if they are defined (optional)
	Element metamodel_keys
	String metamodel_element
	Element mm_model
	Integer attr_value
	mm_model = metamodel["model"]

	metamodel_keys = dict_keys(mm_model)
	while (set_len(metamodel_keys) > 0):
		metamodel_element = set_pop(metamodel_keys)

		// Lower multiplicities
		attr_value = read_attribute(metamodel, metamodel_element, "lower_cardinality")
		if (element_neq(attr_value, read_root())):
			// We have defined a lower cardinality, so check number of instances!
			if (attr_value > list_len(allInstances(model, metamodel_element))):
				return "Lower cardinality violated for class: " + metamodel_element!

		// Upper multiplicities
		attr_value = read_attribute(metamodel, metamodel_element, "upper_cardinality")
		if (element_neq(attr_value, read_root())):
			// We have defined a lower cardinality, so check number of instances!
			if (attr_value < list_len(allInstances(model, metamodel_element))):
				return "Upper cardinality violated for class: " + metamodel_element!

	// Check all ActionLanguage recursively
	Element all_complex_types
	Element complex_instances
	String complex_instance
	String complex_type
	String result
	all_complex_types = allInstances(model["metamodel"], "ActionLanguage")
	while (set_len(all_complex_types) > 0):
		complex_type = set_pop(all_complex_types)
		complex_instances = allInstances(model, complex_type)

		while (set_len(complex_instances) > 0):
			complex_instance = set_pop(complex_instances)
			result = conformance_scd(import_node(model["model"][complex_instance]))
			if (result != "OK"):
				return "ActionLanguage attribute doesn't match for: " + complex_instance + "\n Message: " + result!

	// Structure seems fine, now do global constraints
	Element global_constraints
	String constraint
	Element func

	global_constraints = allInstances(model["metamodel"], "GlobalConstraint")
	while (set_len(global_constraints) > 0):
		constraint = set_pop(global_constraints)
		func = get_func_AL_model(import_node(read_attribute(model["metamodel"], constraint, "global_constraint")))
		result = func(model)
		if (result != "OK"):
			return result!

	return "OK"!

String function check_location_conformance(instance_location : String, type_location : String):
	// Check whether the instance is typed by the type
	Element instance
	Element type

	instance = import_node(instance_location)
	type = import_node(type_location)

	if (element_neq(instance["metamodel"], type)):
		return "Instance not statically typed by specified metamodel"!
	
	return conformance_scd(instance)!

Element function set_model_constraints(model : Element, func : Element):
	if (dict_in(model, "constraints")):
		dict_delete(model, "constraints")
	dict_add_fast(model, "constraints", func)
	return model!

String function model_info(model : Element, name : String):
	if (is_edge(model["model"][name])):
		return "EDGE " + name + " (ID: " + cast_id(model["model"][name]) + ")" + "  src: " + readAssociationSource(model, name) + "  dst: " + readAssociationDestination(model, name)!
	else:
		return "NODE " + name + " (ID: " + cast_id(model["model"][name]) + ")"!
	return name!