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

Boolean function is_direct_instance(model : Element, instance : Element, type : Element):
	// Just check whether or not the type mapping specifies the type as the type of the instance
	return element_eq(dict_read_node(model["type_mapping"], instance), type)

Boolean function is_nominal_instance(model : Element, instance : Element, type : Element):
	return is_nominal_subtype(model["metamodel"], dict_read_node(model["type_mapping"], instance), type)

Boolean function is_nominal_subtype(metamodel : Element, subclass : Element, superclass : Element):
	if (element_eq(subclass, superclass)):
		return True

	Element superclasses
	Element new_superclass
	Element result

	log((("Nominal subtype? " + reverseKeyLookup(metamodel["model"], subclass)) + " --|> ") + reverseKeyLookup(metamodel["model"], superclass))
	superclasses = get_superclasses(metamodel, subclass)

	while (0 < list_len(superclasses)):
		new_superclass = set_pop(superclasses)
		result = is_nominal_subtype(metamodel, new_superclass, superclass)
		if (result):
			return True
	
	return False

Boolean function is_structural_instance(model : Element, instance : Element, type : Element):
	return is_structural_subtype(dict_read_node(model["type_mapping"], instance), type)
	
Boolean function is_structural_subtype(subtype : Element, supertype : Element):
	// Determine whether it is just the exact type or not
	if (element_eq(subtype, supertype)):
		return True

	// Find all links that are required (name and type) from the specified type
	Element required_keys
	required_keys = dict_keys(supertype)
	Integer required_keys_len
	required_keys_len = dict_len(required_keys)

	String key
	Element equivalent
	Integer i
	i = 0

	// Go over all keys that we require
	while (i < required_keys_len):
		key = set_pop(required_keys)
		// Check whether they exist in the instance
		if (dict_in(subtype, key)):
			// Normally, we should still check whether they don't violate the constraints imposed on the class (i.e., are actually present)
			// For now, we ignore this and simply require that it is always there in the metamodel (not necessarily in the instance)
			// TODO

			// Still check whether the types match
			if (bool_not(is_structural_subtype(subtype[key], supertype[key]))):
				return False

			// All clear, so pass on to the next attribute
			i = i + 1
		else:
			return False

	// No violations found, so OK
	return True

String function conformance_scd(model : Element):
	// Initialization
	Element keys
	Element metamodel
	Element typing
	String model_name
	Element src_model
	Element dst_model
	Element src_metamodel
	Element dst_metamodel
	Element element
	Element check_list
	Element check_type
	Element cardinalities

	// Load in variables
	metamodel = model["metamodel"]
	typing = model["type_mapping"]
	cardinalities = create_node()

	// Create dictionary with all associations and allowed cardinalities
	keys = dict_keys(metamodel["model"])
	Integer slc
	Integer suc
	Integer tlc
	Integer tuc
	String key
	Element tmp_dict
	while (0 < list_len(keys)):
		key = set_pop(keys)
		tmp_dict = create_node()
		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(tmp_dict, "slc", slc)
		if (element_neq(suc, read_root())):
			dict_add(tmp_dict, "suc", suc)
		if (element_neq(tlc, read_root())):
			dict_add(tmp_dict, "tlc", tlc)
		if (element_neq(tuc, read_root())):
			dict_add(tmp_dict, "tuc", tuc)

		if (list_len(tmp_dict) > 0):
			dict_add(cardinalities, key, tmp_dict)

	// 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)
		element = model["model"][model_name]

		if (bool_not(dict_in_node(typing, element))):
			return "Model has no type specified: " + model_name

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

		if (bool_not(is_nominal_instance(model, element, dict_read_node(typing, element)))):
			return "Element is not an instance of its specified type: " + model_name

		if (is_edge(element)):
			src_model = read_edge_src(element)
			dst_model = read_edge_dst(element)
			src_metamodel = read_edge_src(dict_read_node(typing, element))
			dst_metamodel = read_edge_dst(dict_read_node(typing, element))

			if (bool_not(is_nominal_instance(model, src_model, src_metamodel))):
				return "Source of model edge not typed by source of type: " + model_name

			if (bool_not(is_nominal_instance(model, dst_model, dst_metamodel))):
				return "Destination of model edge not typed by source of type: " + model_name

		// 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
		log("At element " + model_name)
		Integer lower_val
		Integer upper_val
		Integer instances
		check_list = allPossibleIncoming(model, model_name)
		while (0 < list_len(check_list)):
			check_type = set_pop(check_list)
			if (dict_in(cardinalities, reverseKeyLookup(metamodel["model"], check_type))):
				// Cardinalities defined for this association, so check them
				log("  check " + reverseKeyLookup(metamodel["model"], check_type))
				lower_val = cardinalities[check_type]["tlc"]
				upper_val = cardinalities[check_type]["tlc"]
				instances = list_len(allIncomingAssociationInstances(model, element, 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)):
						return "Lower cardinality violation for incoming edge at " + model_name
				if (dict_in(cardinalities[check_type], "tuc")):
					// An upper cardinality was defined at the target
					if (integer_gt(cardinalities[check_type]["tuc"], instances)):
						return "Upper cardinality violation for incoming edge at " + model_name

		// Identical, but for outgoing, and thus for A in the figure
		check_list = allPossibleOutgoing(model, model_name)
		while (0 < list_len(check_list)):
			check_type = set_pop(check_list)
			if (dict_in(cardinalities, reverseKeyLookup(metamodel["model"], check_type))):
				// Cardinalities defined for this association, so check them
				log("  check " + reverseKeyLookup(metamodel["model"], check_type))
				lower_val = cardinalities[check_type]["slc"]
				upper_val = cardinalities[check_type]["slc"]
				instances = list_len(allOutgoingAssociationInstances(model, element, 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)):
						return "Lower cardinality violation for outgoing edge at " + model_name
				if (dict_in(cardinalities[check_type], "suc")):
					// An upper cardinality was defined at the source
					if (integer_gt(cardinalities[check_type]["suc"], instances)):
						return "Upper cardinality violation for outgoing edge at " + model_name

	// Check multiplicities, if they are defined (optional)
	Element metamodel_keys
	String metamodel_element
	Integer attr_value

	metamodel_keys = dict_keys(metamodel["model"])
	while (0 < list_len(metamodel_keys)):
		metamodel_element = set_pop(metamodel_keys)

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

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

	// Structure seems fine, now do static semantics
	if (dict_in(metamodel, "constraints")):
		Element constraint_function
		constraint_function = metamodel["constraints"]
		return constraint_function(model)
	else:
		return "OK"

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

Element function generate_bottom_type_mapping(model : Element):
	Element mm
	mm = model["metamodel"]["model"]
	dict_delete(model, "type_mapping")
	Element tm
	tm = create_node()
	dict_add(model, "type_mapping", tm)
	
	// Iterate over every element
	Element elem_keys
	Element elem
	elem_keys = dict_keys(model["model"])
	while (0 < read_nr_out(elem_keys)):
		elem = model["model"][set_pop(elem_keys)]
		if (is_edge(elem)):
			dict_add(tm, elem, mm["Edge"])
		else:
			dict_add(tm, elem, mm["Node"])

	return model