definition module StdDynamicLowLevelInterface;

import StdEnv;
import BitSet;
import memory;
import StdDynamicDefaultElem;
import StdDynamicVersion;
import StdMaybe;

// low-level interface for dynamics

// General
make_start_node_index :== (0 bitor 3);

is_external_entry_node node_index :== ((node_index bitand 3) <> 3);

// Deconstructors for a NodeIndex (external references)
get_block_i		node_index :== ((node_index bitand 0x0000ffff) >> 2);
get_en_node_i	node_index :== (node_index >> 16);

// internal references; is_internal_reference and DYNAMIC_CONTAINS_BLOCKTABLE *must* hold
get_offset_from_internal_reference	internal_reference :== internal_reference >> 2;

// dereference an internal reference to the offset realtive from block start
dereference_internal_reference offset_of_reference internal_reference
	:== offset_of_reference - (get_offset_from_internal_reference internal_reference);

// Deconstructors for a prefix_set_and_string_ptr
is_reference prefix_set_and_desc_ptr				:== (is_internal_reference	prefix_set_and_desc_ptr) || (is_external_reference	prefix_set_and_desc_ptr);
is_internal_reference	prefix_set_and_desc_ptr		:== prefix_set_and_desc_ptr bitand 3 == 1;
is_external_reference	prefix_set_and_desc_ptr		:== prefix_set_and_desc_ptr bitand 3 == 3;

get_encoded_descriptor prefix_set_and_desc_ptr	:== get_string_offset prefix_set_and_desc_ptr;

// to be applied after get_encoded_descriptor
is_boxed encoded_descP :== encoded_descP == 0;

// to be applied after get_encoded_descriptor and is_boxed must be false
convert_to_descriptor_usage_entry encoded_descP :== convert_to_descriptor_usage_entry encoded_descP
where {
	convert_to_descriptor_usage_entry encoded_descP
		| is_boxed encoded_descP
			= abort "convert_to_descriptor_usage_entry: internal error";
		= (encoded_descP - 4) >> 2;
};

// obsolete ...
get_string_offset	prefix_set_and_string_ptr	:== prefix_set_and_string_ptr bitand 0x00ffffff;
// ... obsolete
get_prefix_set		prefix_set_and_string_ptr	:== (prefix_set_and_string_ptr >> 24)  bitand 0x000000ff;

// To be used on result of (get_prefix_set prefix_set_and_string_ptr) application
get_n_prefix	prefix_set	:==	prefix_set bitand 1;
get_d_prefix	prefix_set	:== prefix_set bitand 2;
get_k_prefix	prefix_set 	:== prefix_set bitand 4;
get_c_prefix	prefix_set	:== prefix_set bitand 8;
get_t_prefix	prefix_set	:== prefix_set bitand 16;
get_r_prefix	prefix_set	:== prefix_set bitand 32;

is_record		prefix_set	:== (get_r_prefix prefix_set <> 0); // || (get_k_prefix prefix_set <> 0);

// To be used on result of (get_?_prefix prefix_set)
to_char_prefix :: !Int -> !Char;

// Order is important because in case of a labelname more than one used prefix, the offsets in
// the encoded graph are encoded in the order below. Should be tested.
GET_PREFIX_FUNC :== [get_r_prefix,get_t_prefix,get_c_prefix,get_k_prefix,get_d_prefix,get_n_prefix];

DATA_PREFIXES	:== ['r','t','k','d'];

// Header
:: DynamicHeader = {
	// required
		header_size			:: !Int			// size in bytes
	,	version_number		:: !Int			// version number representation
	,	graph_i				:: !Int			
	,	graph_s				:: !Int	
// NEW ...
	,	block_table_i		:: !Int
	,	block_table_s		:: !Int
	,	dynamic_rts_info_i	:: !Int
	,	dynamic_rts_info_s	:: !Int
// ... NEW		
	,	stringtable_i		:: !Int			
	,	stringtable_s		:: !Int
	,	descriptortable_i	:: !Int
	,	descriptortable_s	:: !Int
	,	n_nodes				:: !Int
	
	};

default_dynamic_header :: !DynamicHeader;

//N_DUMMY_BYTES_BEFORE_DYNAMIC_HEADER		:== 8;

class BinaryDynamicIO m
where {
	bd_readi :: !*m -> (!Bool,!Int,!*m);
	bd_reads :: !*m !Int -> (!*{#Char},!*m);
	bd_seek :: !*m !Int !Int -> (!Bool,!*m);
//	bd_close :: !*m !*Files -> (!Bool,!*m);
	
	bd_delta_fp :: !*m -> (!Int,!*m);
	
	bd_freadsubstring :: !Int !Int !*{#Char} !*m -> (!Int,!*{#Char},!*m)
};


instance BinaryDynamicIO File;
//instance BinaryDynamicIO (Int,!*{#Char});
//instance BinaryDynamicIO (!Int,!*Mem);

// Offset; should correspond with graph_to_string.c
HEADER_SIZE_OFFSET		:== 8;		// header size (in bytes)
VERSION_NUMBER_OFFSET	:== 12;		// version (major,minor) 		// little or big endian format?
GRAPH_OFFSET			:== 16;		// graph offset
GRAPH_SIZE				:== 20;		// graph size
BLOCK_TABLE_OFFSET		:== 24;
BLOCK_TABLE_SIZE		:== 28;
DYNAMIC_RTS_INFO_OFFSET	:== 32;		// info from dynamic rts; filled in by StdDynamic.icl
DYNAMIC_RTS_INFO_SIZE	:== 36;
// End sharing for StdDynamic.icl

STRINGTABLE_OFFSET		:== 40;		// stringtable offset
STRINGTABLE_SIZE		:== 44;		// stringtable size
DESCADDTRESTABLE_OFFSET	:== 48;		// descriptor address table offset
DESCADDRESSTABLE_SIZE	:== 52;		// descriptor address table size
N_NODES					:== 56;

read_dynamic_header :: !*f -> *(Bool,DynamicHeader,*f) | BinaryDynamicIO f;

open_dynamic_as_binary :: !String *a -> *(Bool,DynamicHeader,*File,*a) | FileSystem a;

close_dynamic_as_binary :: !*File !*f -> (!Bool,!*f) | FileSystem f;

DYNAMIC_CONTAINS_BLOCKTABLE dynamic_header :== dynamic_header.block_table_i <> 0;

// Graph
read_graph_from_dynamic :: DynamicHeader !*f -> (!Bool,!String,!*f) | BinaryDynamicIO f;

// BlockTable
:: Block
	= {
		bk_block_n			:: !Int		// block identification
	,	bk_offset			:: !Int		// offset where block starts in encoded graph (fp)
	,	bk_size				:: !Int		// block size
	,	bk_n_node_entries	:: !Int		// # block entries - 1
	,	bk_entries			:: {#Int}	// if bk_n_node_entries > 0 then offsets in graph
	};
	
default_block_table :: BlockTable;
	
:: BlockTable
	:== {#Block};


read_block_table_from_dynamic :: DynamicHeader !*f -> (!Bool,!BlockTable,!*f) | BinaryDynamicIO f;

read_block_table_as_string_from_dynamic :: DynamicHeader !*File -> (!Bool,.{#Char},!*File);

// Descriptor Usage Table
:: DescriptorUsageEntry
	= {
		prefix_set_and_string_ptr		:: !Int
	,	dus_library_instance_nr_on_disk	:: !Int
	,	bitset							:: !BitSet
	};

	
:: DescriptorUsageTable
	:== {#.DescriptorUsageEntry};
	
default_descriptor_usage_table :: DescriptorUsageTable;

default_descriptor_usage_entry :: !Int -> !.DescriptorUsageEntry;
	

read_descriptor_usage_table_from_dynamic :: DynamicHeader !*f -> (!Bool,!.DescriptorUsageTable,!*f) | BinaryDynamicIO f;


// String Table
:: StringTable
	:== String;
	
read_string_table_from_dynamic :: DynamicHeader !*f -> (!Bool,!StringTable,!*f) | BinaryDynamicIO f;

// Interface to dynamic run-time system
LinkBlock :: !String !Bool !Int !Int -> (!Int,!Int,!String);

// 
build_code_lib_name lib_without_extension :== lib_without_extension +++ ".lib";
build_type_lib_name lib_without_extension :== lib_without_extension +++ ".typ";

/*
:: LibraryInfo
	= {
		li_code_start	:: !Int
	,	li_code_end		:: !Int
	,	li_data_start	:: !Int
	,	li_data_end		:: !Int
	,	li_name			:: !String		// location where to find the library; access path to library
	,	li_set			:: !Int			// used iff li_name1 == li_name2 and indicates the set of labels to be linked with one instance of library
										// it might be possible to collapse several sets but that is future optimization
	};
*/

// in reply from a GraphToString-request; RangeID table
:: RangeID
	= {
		rid_n_range_id_entries	:: !Int
	,	rid_n_type_tables		:: !Int
	,	rid_range_entries		:: !{#RangeIDEntry}
	};
	
:: RangeIDEntry
	= {
		ride_begin_address		:: !Int
	,	ride_end_address		:: !Int
	,	ride_type_table_i		:: !Int
	};
	
default_range_id_entry :: !RangeIDEntry;

RID_N_RANGE_ENTRIES_OFFSET		:== 0;
RID_N_TYPE_TABLES_OFFSET		:== 4;
RID_HEADER_SIZE					:== RID_N_TYPE_TABLES_OFFSET + 4;

RIDE_BEGIN_ADDRESS_OFFSET		:== 0;
RIDE_END_ADDRESS_OFFSET			:== 4;
RIDE_RUNTIME_ID_LIB_NUMBER		:== 8;
RIDE_SIZE						:== RIDE_RUNTIME_ID_LIB_NUMBER + 4;
	
instance toString RangeID;

// Type table usage table; constructed in dynamic_to_string
TTUT_UNUSED	:== 0xffffffff;

// dynamic info
:: DynamicInfo
	= {
		// Header
		di_version					:: !Version
	,	di_string_table				:: !StringTable
	,	di_descriptor_usage_table	:: !DescriptorUsageTable
	,	di_file_name				:: !String
	,	di_n_blocks					:: !Int
	

	// read_rts_info_from_dynamic reads the following fields
	// begin
	,	di_library_instance_to_library_index	:: !{#LibraryInstanceToLibraryIndexInfo}		// indexed by a RunTimeID, index in di_library_index_to_library_name
	,	di_library_index_to_library_name		:: !{#{#Char}}	// indexed by index from above array, string reference to {code,type}-library
//	,	di_external_dynamics					:: !{#{#Char}}  // references to (other) dynamics
	,	di_disk_type_equivalent_classes			:: !{DiskTypeEquivalentClass}
	,	di_lazy_dynamics_a						:: !{#{#Char}}
	,	di_lazy_type_reference_a				:: !{Maybe LazyTypeReference}
	
	// DiskTypeEquivalentClass
	// end
	
	//
	,	di_disk_id_to_library_instance_i		:: !{#Int}		// indexed by diskID
	,	di_disk_to_rt_dynamic_indices			:: !{#Int}		// ibdexed by disk_dynamic_index
	
	,	di_has_block_been_used					:: !{#Bool}
	};	
	
:: LibraryInstanceToLibraryIndexInfo
	= {
		litlii_index_in_di_library_index_to_library_name	:: !Int
	,	litlii_used_by_code									:: !Bool
	,	litlii_used_by_type									:: !Bool
	};
	
instance DefaultElem LibraryInstanceToLibraryIndexInfo;
	
instance DefaultElem DynamicInfo;
	
default_dynamic_info :: !DynamicInfo;

read_rts_info_from_dynamic :: DynamicHeader !*f -> (!Bool,!DynamicInfo,!*f) | BinaryDynamicIO f;

class DynamicInfoOps s
where {
	UpdateDynamicInfo :: !Int !DynamicInfo !*s -> !*s
};

//1.3
instance DynamicInfoOps (!*{#DynamicInfo});
//3.1
/*2.0
instance DynamicInfoOps ({#DynamicInfo});
0.2*/
class EnDecode a 
where {
	to_size	:: a -> !Int;
	to_string :: a !Int !*{#Char} -> (!Int,!*{#Char});
	from_string :: !Int !{#Char} -> (a,!Int);

	encode :: a -> !*{#Char} | EnDecode a;
	encode a :== snd (to_string a 0 (createArray (to_size a) '@'));
	
	decode :: !{#Char} -> a | EnDecode a;
	decode buffer :== fst (from_string 0 buffer)
};

instance EnDecode Int;
instance EnDecode Char;
instance EnDecode Bool;

//1.3
//instance EnDecode {#a} | EnDecode, select_u, size_u, createArray_u, DefaultElem, ArrayElem a;
instance EnDecode {#a} | EnDecode, DefaultElem, ArrayElem a;
//3.1
/*2.0
instance EnDecode {#a} | EnDecode, DefaultElem a & Array {#} a;
0.2*/
instance EnDecode DynamicInfo;

// communication between application and client
:: TypeReference
	= {
		tr_type_name	:: !String
	,	tr_module_name1	:: !String
	,	tr_module_name2	:: !String
	,	tr_library1		:: !LibraryID
	,	tr_library2		:: !LibraryID
	};
	
instance DefaultElem TypeReference;
	
:: LibraryID
	= Address !Int
	| Number !Int				// always RunTime valid (kan geen diskID zijn)
	;	

instance EnDecode LibraryID;
instance EnDecode TypeReference;

/*2.0
instance EnDecode [b] | EnDecode, DefaultElem b &  Array {#} b;
0.2*/
//1.3
instance EnDecode [b] | EnDecode b; // & DefaultElem b & ArrayElem b;
//3.1

// RunTimeID/DiskID  at run-time:
RTID_DATA_DYNAMIC				:== 0; // no code needed

// Library instances at run-time are numbered from RTID_LIBRARY_INSTANCE_ID_START
RTID_LIBRARY_INSTANCE_ID_START	:== 1; // by default, a dummy element is created

// Otherwise
RTID_DISKID_RENUMBER_START		:== 1; // change also gts_range_id; counting from 1

// Build (lazy) block labels
BUILD_BLOCK_LABEL				:== "e____SystemDynamic__nbuild__block";
BUILD_LAZY_BLOCK_LABEL			:== "e____SystemDynamic__nbuild__lazy__block";

// BUILD_BLOCK (run-time) format, from gts_build_block.c, _SystemDynamic.{dcl,icl}
BUILD_DYNAMIC_NODE__INDEX_PTR	:== 4;
BUILD_DYNAMIC_GDID__PTR			:== 8;

// BUILD_BLOCK (on disk) format, from gts_build_block.c:
BUILD_LAZY_DYNAMIC_ON_DISK__NODE_INDEX		:== 0;
BUILD_LAZY_DYNAMIC_ON_DISK__DYNAMIC_ID		:== 4;

BUILD_LAZY_DYNAMIC_ON_DISK__LAST_FIELD		:== (BUILD_LAZY_DYNAMIC_ON_DISK__DYNAMIC_ID + 4);
BUILD_LAZY_DYNAMIC_ON_DISK__BSIZE			:== BUILD_LAZY_DYNAMIC_ON_DISK__LAST_FIELD;

// A lazy dynamic reference is generated by the graph_to_string conversion routine.
:: LazyDynamicReference
	= { 
		ldr_id							:: !Int			// run-time id of lazy dynamic
	,	ldr_site						:: !String		// e.g. path to dynamic
	,	ldr_lazy_dynamic_index			:: !Int			// disk id for lazy dynamic (block)
	};

// all instance of the graph_to_string-conversion function *must* use the same LazyDynamicReference.
LazyDynamicReference_String		:== "LazyDynamicReference";

StdDynamicLowLevelInterfaceModule_String	:== "StdDynamicLowLevelInterface";

GlobalDynamicInfoDummy_String 	:== "GlobalDynamicInfoDummy";

instance DefaultElem LazyDynamicReference;
instance EnDecode LazyDynamicReference;

// Types
// Representation on disk	
:: DiskTypeEquivalentClass
	= {
	// encoded:
		dtec_type_equations			:: !{DiskTypeReference}
	,	dtec_lazy_type_equations	:: !{DiskTypeReference}
	
	//
	,	dtec_type_implementation_table_index	:: !Maybe !Int
	};

instance DefaultElem DiskTypeEquivalentClass;

:: DiskTypeReference
	= DiskTypeRef DiskTypeRef						// dtr_library_instance_i applies to the di_disk_id_to_library_instance_i of the current dynamic
	| LazyDiskTypeRef LazyDiskTypeRef				// dtr_library_instance_i applies to the di_disk_id_to_library_instance_i of lazy dynamic ldtr_lazy_dynamic_index
	;
	
:: LazyDiskTypeRef
	= { 
	// LazyDynamicReference, the path can be found for the external dynamics. The conversion-routine need not deliver the
	// string itself.
		ldtr_lazy_dynamic_index	:: !Int				// index of lazy_dynamic_a of DynamicInfo-record (build_lazy_block)
	,	ldtr_disk_type_ref		:: !DiskTypeRef	
	};

:: DiskTypeRef
	= { 
		dtr_library_instance_i	:: !Int				// index in di_disk_id_to_library_instance_i either from current dynamic or from lazy dynamic (depends on the context)
	,	dtr_tr_module_n			:: !Int
	,	dtr_tr_type_def_n		:: !Int
	};

// 
INITIAL_LAZY_DYNAMIC_INDEX	:== 100;

/*2.0
//instance EnDecode (a,b,c,d,e) | EnDecode a & EnDecode b & EnDecode c & EnDecode d & EnDecode e;
0.2*/
//1.3
//instance EnDecode (a,b,c,d,e) | EnDecode a & EnDecode b & EnDecode c & EnDecode d & EnDecode e;
//3.1

/*2.0
instance EnDecode (a,b) | EnDecode a & EnDecode b;
0.2*/
//1.3
instance EnDecode (a,b) | EnDecode b & EnDecode a;
//3.1

/*2.0
instance EnDecode (a,b,c,d) | EnDecode a & EnDecode b & EnDecode c & EnDecode d;
0.2*/
//1.3
instance EnDecode (a,b,c,d) | EnDecode a & EnDecode b & EnDecode c & EnDecode d;
//3.1

// interface to graph_to_string-routine
// update gts_code_and_type_runtime_ids.c
CODE_LIBRARY_INSTANCE	:== 0x80000000;
TYPE_LIBRARY_INSTANCE	:== 0x40000000;
LIBRARY_INSTANCE_MASK	:== 0x3fffffff;

GET_LIBRARY_INSTANCE_I x	:== x bitand LIBRARY_INSTANCE_MASK;

IS_CODE_LIBRARY_INSTANCE x 	:== (x bitand CODE_LIBRARY_INSTANCE) <> 0;
IS_TYPE_LIBRARY_INSTANCE x	:== (x bitand TYPE_LIBRARY_INSTANCE) <> 0;

instance EnDecode LibraryInstanceToLibraryIndexInfo;

//
:: LazyTypeReference
	= {
		ltr_lazy_dynamic_index	:: !Int		// within main dynamic (on disk)
	,	ltr_library_instance_i	:: !Int		// relative from the lazy dynamic (on disk)
	};
	
instance EnDecode LazyTypeReference;
//instance DefaultElem (Maybe m);
instance DefaultElem LazyTypeReference;