implementation module linker2;

import StdInt,StdBool,StdString,StdChar,StdArray,StdFile,StdClass;
// RWS
import UtilNewlinesFile;

swap_bytes i :== i;
//swap_bytes i = ((i>>24) bitand 0xff) bitor ((i>>8) bitand 0xff00) bitor ((i<<8) bitand 0xff0000) bitor (i<<24);

::	*SymbolArray :== SSymbolArray;
::	SSymbolArray :== {!Symbol};

::	Symbol
	= Module !Int !Int !Int !Int !Int !Int !String		// section_n offset length virtual_address file_offset n_relocations relocations
	| Label !Int !Int !Int								// section_n offset module_n
	| SectionLabel !Int !Int							// section_n offset
	| ImportLabel !String								// label_name
	| ImportedLabel !Int !Int 							// file_n symbol_n
	| ImportedLabelPlusOffset !Int !Int !Int			// file_n symbol_noffset
	| ImportedFunctionDescriptor !Int !Int 				// file_n symbol_n
	| EmptySymbol;

::	SymbolIndexList = SymbolIndex !Int !SymbolIndexList | EmptySymbolIndex;

::	*NamesTable :== SNamesTable;
::	SNamesTable :== {!NamesTableElement};

::	NamesTableElement
	= NamesTableElement !String !Int !Int !NamesTableElement	// symbol_name symbol_n file_n symbol_list
	| EmptyNamesTableElement;

::	LibraryList = Library !String !LibrarySymbolsList !Int !LibraryList | EmptyLibraryList;

::	LibrarySymbolsList = LibrarySymbol !String !LibrarySymbolsList | EmptyLibrarySymbolsList;

::	*Xcoff :== *SXcoff;
:: SXcoff ={
		file_name			:: !String,
		symbol_table		:: !.SSymbolTable,
		n_symbols			:: !Int
	};

::	*SymbolTable :== *SSymbolTable;
:: SSymbolTable ={
		text_symbols	:: !SymbolIndexList,
		data_symbols	:: !SymbolIndexList,
		bss_symbols		:: !SymbolIndexList,
		imported_symbols:: !SymbolIndexList,
		section_symbol_ns::!.{#Int},
		symbols			:: !.SSymbolArray
	};

:: XcoffArray :== {#SXcoff};

n_symbols_of_xcoff_list :: !Int ![Xcoff] -> (!Int,![Xcoff]);
n_symbols_of_xcoff_list n_symbols0 []
	= (n_symbols0,[]);
n_symbols_of_xcoff_list n_symbols0 [xcoff=:{n_symbols}:xcoff_list0]
	= (n_symbols1,[xcoff:xcoff_list1]);
	{
		(n_symbols1,xcoff_list1)=n_symbols_of_xcoff_list (n_symbols0+n_symbols) xcoff_list0;
	}

imported_library_symbols :: !.LibrarySymbolsList !Int !{#.Bool} -> .[String];
imported_library_symbols EmptyLibrarySymbolsList offset marked_bool_a
	= [];
imported_library_symbols (LibrarySymbol symbol_name library_symbols) offset marked_bool_a
	| marked_bool_a.[offset]
		= [symbol_name : imported_library_symbols library_symbols (inc offset) marked_bool_a];
		= imported_library_symbols library_symbols (inc offset) marked_bool_a;

(FWI) infixl;
(FWI) f i = fwritei (swap_bytes i) f;

(FWS) infixl;
(FWS) f s :== fwrites s f;

(FWC) infixl;
(FWC) f c :== fwritec c f;

(FWB) infixl;
(FWB) f i :== fwritec (toChar i) f;

(FWW) infixl;
(FWW) f i :== fwritec (toChar (i>>8)) (fwritec (toChar i) f);

create_coff_file :: !String !Int !Int !Int !Int !Int !Int !Bool !*Files -> (!Bool,!*File,!*Files);
create_coff_file xcoff_file_name text_section_size data_section_size bss_section_size idata_section_size main_offset stack_size open_console_window files0
	| not ok
		= (False,file0,files1);
		= (True,file6,files1);
	{}{
		(ok,file0,files1) = fopen xcoff_file_name FWriteData files0;
		
		executable_size = 1024+text_section_size_512+data_section_size_512+idata_section_size_512;

		file01 = file0
//			FWI 0x00005A4D FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 64;
			FWS "MZ"
			FWW 0 // (executable_size mod 512)
			FWW (executable_size >> 9)
			FWW 0
			FWW 2									// MZ-header / 16
			FWW 0
			FWI 0
			FWI 0
			FWI 0
			FWW 0x40								// PE-header offset
			FWW 0
			FWI 0
			FWB 0x0e								// push cs
			FWB 0x1f								// pop ds
			FWB 0xba FWB 0x0d FWB 0x00				// mov dx,offset msg$
			FWB 0xb4 FWB 0x09						// mov ah,9
			FWB 0xcd FWB 0x21						// int 21h				; write string
			FWB 0xb4 FWB 0x4c						// mov ah,4ch
			FWB 0xcd FWB 0x21						// int 21h				; exit
			FWS "Win32 required$"
			FWI 0x40								// PE-header offset
			;

		text_section_size_512=(text_section_size+511) bitand (-512);
		data_section_size_512=(data_section_size+511) bitand (-512);
		bss_section_size_512=(bss_section_size+511) bitand (-512);
		idata_section_size_512=(idata_section_size+511) bitand (-512);

		text_section_size_4096=(text_section_size+4095) bitand (-4096);
		data_section_size_4096=(data_section_size+4095) bitand (-4096);
		bss_section_size_4096=(bss_section_size+4095) bitand (-4096);
		idata_section_size_4096=(idata_section_size+4096) bitand (-4096);
		
		stack_size_4096=if (stack_size>0) ((stack_size+4095) bitand (-4096)) 4096;
		
		image_size = 0x1000+text_section_size_4096 + data_section_size_4096 + bss_section_size_4096+idata_section_size_4096;
		
		file1 = file01
			FWI 0x00004550
			FWI 0x0004014c FWI 0 FWI 0 FWI 0 FWI 0x010f00e0
			FWI 0x0000010b FWI text_section_size_512 FWI data_section_size_512 FWI bss_section_size_512 FWI (0x1000+main_offset) FWI 0x1000 FWI data_vaddr FWI 0x400000
			FWI 4096 FWI 512
			/* FWI 0x00000001 */ FWI 0x00000004
			FWI 00000001 
			/* FWI 0x000a0003 */ FWI 0x00000004
			FWI 0 FWI image_size FWI 1024 FWI 0 FWI (if open_console_window 0x00000003 0x00000002) 
//			FWI 0x100000
			FWI stack_size_4096
			FWI 0x1000 FWI 0x100000 FWI 0x1000 FWI 0 FWI 16
			FWI 0 FWI 0 FWI idata_vaddr FWI idata_section_size FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0
			FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0 FWI 0;

		file2 = file1
			FWS ".text\000\000\000" FWI text_section_size FWI 0x1000 FWI text_section_size_512 FWI 1024
			FWI 0 FWI 0 FWI 0 FWI 0x60000020;
		file3 = file2
			FWS ".data\000\000\000" FWI data_section_size FWI data_vaddr FWI data_section_size_512 FWI (1024+text_section_size_512)
			FWI 0  FWI 0 FWI 0 FWI 0xc0000040;
		file4 = file3
			FWS ".bss\000\000\000\000" FWI bss_section_size FWI bss_vaddr FWI 0 FWI 0
			FWI 0 FWI 0 FWI 0 FWI 0xc0000080;
		file5 = file4
			FWS ".idata\000\000" FWI idata_section_size FWI idata_vaddr FWI idata_section_size_512 FWI (1024+text_section_size_512+data_section_size_512)
			FWI 0 FWI 0 FWI 0 FWI 0xc0000040;
		file6 = write_zero_bytes_to_file 552 file5;
		
		data_vaddr=0x1000+text_section_size_4096;
		bss_vaddr=data_vaddr+data_section_size_4096;
		idata_vaddr=bss_vaddr+bss_section_size_4096;
	}

write_zero_bytes_to_file n pe_file0
	| n==0
		= pe_file0;
		= write_zero_bytes_to_file (dec n) (fwritec '\0' pe_file0);

SIZE_OF_HEADER:==20;
SIZE_OF_SECTION_HEADER:==40;
SIZE_OF_SYMBOL:==18;
SIZE_OF_RELOCATION:==10;

C_EXT:==2;
C_STAT:==3;
C_LABEL:==6;
C_FUNCTION:==101;
C_FILE:==103;

N_ABS:==0xffff;
N_UNDEF:==0;
TEXT_SECTION:==1;
DATA_SECTION:==2;
BSS_SECTION:==3;

REL_DIR32:==6;
REL_REL32:==024;
REL_DUMMY:==0;

(CHAR) string i :== string.[i];

(BYTE) string i :== toInt (string.[i]);

(WORD) string i = (string BYTE i<<8) bitor (string BYTE (i+1));

(IWORD) string i = (string BYTE (i+1)<<8) bitor (string BYTE i);

(ILONG) string i
	= (string BYTE (i+3)<<24) bitor (string BYTE (i+2)<<16) bitor (string BYTE (i+1)<<8) bitor (string BYTE i);

SYMBOL_TABLE_SIZE:==4096;
SYMBOL_TABLE_SIZE_MASK:==4095;

create_names_table :: NamesTable;
create_names_table = createArray SYMBOL_TABLE_SIZE EmptyNamesTableElement;

insert_symbol_in_symbol_table :: !String Int Int !NamesTable -> NamesTable;
insert_symbol_in_symbol_table symbol_name symbol_n file_n names_table=:{[symbol_hash]=symbol_list}
	| symbol_in_symbol_table_list symbol_list
		= names_table;
		= { names_table & [symbol_hash] = NamesTableElement symbol_name symbol_n file_n symbol_list};
	{}{
		symbol_hash=symbol_name_hash symbol_name;
		
		symbol_in_symbol_table_list EmptyNamesTableElement
			= False;
		symbol_in_symbol_table_list (NamesTableElement string  _ _ symbol_table_list)
			| string==symbol_name
				= True;
				= symbol_in_symbol_table_list symbol_table_list;
	}

find_symbol_in_symbol_table :: !String !NamesTable -> (!NamesTableElement,!NamesTable);
find_symbol_in_symbol_table symbol_name names_table=:{[symbol_hash]=symbol_list}
	=	(symbol_in_symbol_table_list symbol_list,names_table);
	{
		symbol_hash=symbol_name_hash symbol_name;
		
		symbol_in_symbol_table_list EmptyNamesTableElement
			= EmptyNamesTableElement;
		symbol_in_symbol_table_list names_table_element=:(NamesTableElement string _ _ symbol_table_list)
			| string==symbol_name
				= names_table_element;
				= symbol_in_symbol_table_list symbol_table_list;
	}

	symbol_name_hash symbol_name = (simple_hash symbol_name 0 0) bitand SYMBOL_TABLE_SIZE_MASK;
	{
		simple_hash string index value
			| index== size string
				= value;
				= simple_hash string (inc index) (((value<<2) bitxor (value>>10)) bitxor (string BYTE index));
	}

::	SortArray :== {#SortElement};
::	SortElement = { index::!Int, offset::!Int };

sort_symbols :: !SymbolIndexList !SymbolArray -> (!SymbolIndexList,!SymbolArray);
sort_symbols symbols symbol_array0
	=	(array_to_list sorted_array 0,symbol_array1);
	{
		sorted_array=heap_sort array;
		(array,symbol_array1)=fill_array new_array 0 symbols symbol_array0;
		new_array=createArray n_elements {index=0,offset=0};
		n_elements=length_of_symbol_index_list symbols 0;
		
		fill_array :: *SortArray Int SymbolIndexList SymbolArray -> (!*SortArray,!SymbolArray);
		fill_array a i EmptySymbolIndex symbol_array
			= (a,symbol_array);
		fill_array a i (SymbolIndex index l) symbol_array=:{[index]=m}
			= c a i m symbol_array;
			{
				c :: *SortArray Int Symbol SymbolArray -> (!*SortArray,!SymbolArray);
				c a i (Module _ offset _ _ _ _ _) symbol_array
					= fill_array {a & [i]={index=index,offset=offset}} (inc i) l symbol_array;
			};
		
		array_to_list :: SortArray Int -> SymbolIndexList;
		array_to_list a i
			| i<n_elements
				= SymbolIndex a.[i].index (array_to_list a (inc i));
				= EmptySymbolIndex;
			
		heap_sort :: *SortArray -> *SortArray;
		heap_sort a
			| n_elements<2
				=	a
				=	sort_heap max_index (init_heap (n_elements>>1) a);
				{
					sort_heap :: Int *SortArray -> *SortArray;
					sort_heap i a=:{[i]=a_i,[0]=a_0}
						| i==1
							= { a & [0]=a_i,[i]=a_0}; 
							= sort_heap deci (add_element_to_heap {a & [i]=a_0} a_i 0 deci);{
								deci=dec i;
							}
				
					init_heap :: Int *SortArray -> *SortArray;
					init_heap i a0
						| i>=0
							= init_heap (dec i) (add_element_to_heap1 a0 i max_index); {
								add_element_to_heap1 :: *SortArray Int Int -> *SortArray;
								add_element_to_heap1 a=:{[i]=ir} i max_index
									= add_element_to_heap a ir i max_index;
							}
							= a0;
					
					max_index=dec n_elements;
				}
		
		add_element_to_heap :: *SortArray SortElement Int Int -> *SortArray;
		add_element_to_heap a ir i max_index
			= heap_sort_lp a i (inc (i+i)) max_index ir;
		{
			heap_sort_lp :: *SortArray Int Int Int SortElement-> *SortArray;
			heap_sort_lp a i j max_index ir
				| j<max_index
					= heap_sort1 a i j max_index ir;
				{
					heap_sort1 :: !*SortArray !Int !Int !Int !SortElement -> *SortArray;
					heap_sort1 a=:{[j]=a_j,[j1]=a_j_1} i j max_index ir
						= heap_sort1 a_j a_j_1 a i j max_index ir;
					{
						heap_sort1 :: !SortElement !SortElement !*SortArray !Int !Int !Int !SortElement -> *SortArray;
						heap_sort1 a_j a_j_1 a i j max_index ir
						| a_j.offset < a_j_1.offset
							= heap_sort2 a i (inc j) max_index ir;
							= heap_sort2 a i j max_index ir;

						j1=inc j;
					}
				}
				| j>max_index
					= {a & [i] = ir};
				// j==max_index
					= heap_sort2 a i j max_index ir;
				{}{
					heap_sort2 a=:{[j]=a_j} i j max_index ir
						= heap_sort2 a_j a i j max_index ir;
					{
						heap_sort2 :: SortElement *SortArray !Int !Int !Int SortElement-> *SortArray;
						heap_sort2 a_j a i j max_index ir
						| ir.offset<a_j.offset
							= heap_sort_lp {a & [i] = a_j} j (inc (j+j)) max_index ir;
			   				= {a & [i] = ir};
			   		}
				}
		}
	}

length_of_symbol_index_list EmptySymbolIndex length
	= length;
length_of_symbol_index_list (SymbolIndex _ l) length
	= length_of_symbol_index_list l (inc length);

symbols_are_sorted :: SymbolIndexList {!Symbol} -> Bool;
symbols_are_sorted EmptySymbolIndex symbol_array
	= True;
symbols_are_sorted (SymbolIndex i1 l) symbol_array
	=	sorted_symbols2 i1 l symbol_array;
	{
		sorted_symbols2 :: Int SymbolIndexList {!Symbol} -> Bool;
		sorted_symbols2 i1 EmptySymbolIndex symbol_array
			= True;
		sorted_symbols2 i1 (SymbolIndex i2 l) symbol_array
			= symbol_index_less_or_equal i1 i2 symbol_array && sorted_symbols2 i2 l symbol_array;
	}

reverse_and_sort_symbols :: !SymbolIndexList !SymbolArray -> (!SymbolIndexList,!SymbolArray);
reverse_and_sort_symbols symbols symbol_array
	| symbols_are_sorted reversed_symbols symbol_array
		= (reversed_symbols,symbol_array);
		= sort_symbols reversed_symbols symbol_array;
//	| symbols_are_sorted sorted_symbols symbol_array1
//		= (sorted_symbols,symbol_array1);
	{}{
//		(sorted_symbols,symbol_array1) = sort_symbols reversed_symbols symbol_array;
		reversed_symbols=reverse_symbols symbols;
	}

reverse_symbols l = reverse_symbols l EmptySymbolIndex;
{
	reverse_symbols EmptySymbolIndex t = t;
	reverse_symbols (SymbolIndex i l) t = reverse_symbols l (SymbolIndex i t);
}

	symbol_index_less_or_equal :: Int Int {!Symbol} -> Bool;
	symbol_index_less_or_equal i1 i2 {[i1]=m1,[i2]=m2}
		= case (m1,m2) of {
			(Module _ offset1 _ _ _ _ _,Module _ offset2 _ _ _ _ _)
				-> offset1<=offset2; 
		}

sort_modules :: !*SXcoff -> .SXcoff;
sort_modules xcoff
	= { xcoff & symbol_table = 
		{ symbol_table &
			text_symbols=text_symbols1,
			data_symbols=data_symbols1,
			bss_symbols=bss_symbols1,
			symbols=symbols3
		}
	  };
	{
		(text_symbols1,symbols1)=reverse_and_sort_symbols text_symbols symbols0;
		(data_symbols1,symbols2)=reverse_and_sort_symbols data_symbols symbols1;
		(bss_symbols1,symbols3)=reverse_and_sort_symbols bss_symbols symbols2;
		
		{symbol_table} = xcoff;
		{text_symbols,data_symbols,bss_symbols,symbols=symbols0} = symbol_table;
	}

read_library_files :: ![String] Int Int !*Files NamesTable -> (![String],!LibraryList,!Int,!*Files,!NamesTable);
read_library_files [] library_n n_library_symbols0 files0 names_table0
	= ([],EmptyLibraryList,n_library_symbols0,files0,names_table0);
read_library_files [file_name:file_names] library_n n_library_symbols0 files0 names_table0
	| ok1
		= (errors,Library library_name library_symbols n_library_symbols libraries,n_library_symbols1,files2,names_table2);
		= (["Cannot read library '" +++ file_name +++ "'"],EmptyLibraryList,0,files1,names_table1);
	{}{
		(errors,libraries,n_library_symbols1,files2,names_table2)
			= read_library_files file_names (inc library_n) (n_library_symbols0+n_library_symbols) files1 names_table1;
		(ok1,library_name,library_symbols,n_library_symbols,files1,names_table1)
			= read_library_file file_name library_n files0 names_table0;
	}
 
read_library_file :: String Int *Files NamesTable -> (!Bool,!String,!LibrarySymbolsList,!Int,!*Files,!NamesTable);
read_library_file library_file_name library_n files0 names_table0
	| not ok1
		= (False,"",EmptyLibrarySymbolsList,0,files1,names_table0);
	| size library_name1<>0 && ok2
		= (True,library_name1,library_symbols,n_library_symbols,files2,names_table1);
		= (False,"",EmptyLibrarySymbolsList,0,files2,names_table1);
	{}{
		(ok2,files2) = fclose library_file2 files1;
		(library_symbols,n_library_symbols,library_file2,names_table1) = read_library_symbols library_file1 0 names_table0;
		(library_name0,library_file1) = readLine library_file0;
		(ok1,library_file0,files1) = fopen library_file_name FReadData files0;

		library_name1 :: {#Char}; // to help the typechecker
		library_name1
			| size library_name0==0 || library_name0 .[size library_name0-1]<>'\n'
				= library_name0;
				= library_name0 % (0,size library_name0-2);

		read_library_symbols :: *File Int NamesTable -> (!LibrarySymbolsList,!Int,!*File,!NamesTable);
		read_library_symbols file0 symbol_n names_table0
			| size symbol_name==0
				= (EmptyLibrarySymbolsList,symbol_n,file1,names_table0);
			| symbol_name.[size symbol_name-1]<>'\n'
				= (LibrarySymbol symbol_name library_symbols,symbol_n1,file2,names_table2);
				{
					(library_symbols,symbol_n1,file2,names_table2) = read_library_symbols file1 (symbol_n+2) names_table1;
					names_table1 = insert_symbol_in_symbol_table ("_"+++symbol_name) symbol_n library_n names_table0;
				}
			| size symbol_name==1
				= read_library_symbols file1 symbol_n names_table0;
				= (LibrarySymbol symbol_name1 library_symbols,symbol_n1,file2,names_table2);
				{
					(library_symbols,symbol_n1,file2,names_table2) = read_library_symbols file1 (symbol_n+2) names_table1;
					names_table1 = insert_symbol_in_symbol_table ("_"+++symbol_name1) symbol_n library_n names_table0;
					symbol_name1 = symbol_name % (0,size symbol_name-2);
				}
			{
				(symbol_name,file1)=readLine file0;
			}
	}

	read_string_table :: *File -> (!Bool,!String,!*File);
	read_string_table file0
		| not ok
			= error file1;
		| string_table_size==0
			= (True,"",file1);
		| string_table_size<4
			= error file1;
		| not (size string_table_string==string_table_size2)
			= error file2;
			= (True,string_table_string,file2);
		{}{
			error file=(False,"",file);
			(string_table_string,file2)=freads file1 string_table_size2;
			string_table_size2=string_table_size-4;

			string_table_size=swap_bytes string_table_size0;

			(ok,string_table_size0,file1)=freadi file0;
		}

	read_symbols :: Int *File -> (!Bool,!String,!String,!*File);
	read_symbols n_symbols file0
		| not (size symbol_table_string==symbol_table_size)
			= (False,"","",file1);
			= (ok,symbol_table_string,string_table,file2);
			{
				(ok,string_table,file2)=read_string_table file1;
			}
		{
			(symbol_table_string,file1)=freads file0 symbol_table_size;
			symbol_table_size=n_symbols*SIZE_OF_SYMBOL;
		}

read_symbol_table :: !Int !Int !*File -> (!Bool,!String,!String,!*File);
read_symbol_table symbol_table_offset n_symbols file0
	| not fseek_ok
		= error file1;
		= read_symbols n_symbols file1;
	{}{
		(fseek_ok,file1)=fseek file0 symbol_table_offset FSeekSet;
		error file=(False,"","",file);
	}

/*
PRINT_INT s i
	| not error
		= i;
	{}{
		(error,_)=ferror (fwritec ' ' (fwritei i (fwrites s stderr)));
	}
*/

define_symbols :: Int Int String String {!Section} NamesTable Int -> (!NamesTable,!SymbolTable);
define_symbols n_sections n_symbols symbol_table_string string_table sections names_table file_n
	= define_symbols_lp 0 names_table empty_symbol_table;
	{
		empty_symbol_table = {	text_symbols=EmptySymbolIndex,
								data_symbols=EmptySymbolIndex,
								bss_symbols=EmptySymbolIndex,
								imported_symbols=EmptySymbolIndex,
								section_symbol_ns=createArray (n_sections+1) (-1),
								symbols=createArray n_symbols EmptySymbol
							 };

		define_symbols_lp :: Int NamesTable SymbolTable -> (!NamesTable,!SymbolTable);
		define_symbols_lp symbol_n names_table0 symbol_table0
			| offset==size symbol_table_string
				= (names_table0,symbol_table0);
				= case (symbol_table_string BYTE (offset+16)) of {
					C_EXT
						| n_scnum==N_UNDEF
							| n_value==0
								->	define_symbols_lp (symbol_n+1+n_numaux) names_table0 symbol_table1;
								{
									symbol_table1
										= {symbol_table0 & 
												symbols={symbol_table0.symbols & [symbol_n]= ImportLabel name_of_symbol},
												imported_symbols= SymbolIndex symbol_n symbol_table0.imported_symbols												
										  };
								}
								->	define_symbols_lp (symbol_n+1+n_numaux) names_table1 symbol_table2;
								{
									symbol_table2=
										 {symbol_table0 & 
											symbols = {symbol_table0.symbols & [symbol_n]= Module BSS_SECTION 0 n_value 0 0 0 ""},
											bss_symbols = SymbolIndex symbol_n symbol_table0.bss_symbols
									  };
									names_table1=insert_symbol_in_symbol_table name_of_symbol symbol_n file_n names_table0;
								}
							-> if (n_numaux==0 || n_type==0x20)
								(define_symbols_lp (symbol_n+1+n_numaux) names_table1 (new_symbol_table n_value))
								(define_symbols_lp (symbol_n+1+n_numaux) names_table1 (new_symbol_table_with_aux n_value))
								;
							{
								names_table1=insert_symbol_in_symbol_table name_of_symbol symbol_n file_n names_table0;
							}
					C_LABEL
						| n_numaux==0
							-> define_symbols_lp (symbol_n+1+n_numaux) names_table0 (new_symbol_table n_value);
					C_STAT
						| n_scnum==N_ABS
							-> define_symbols_lp (symbol_n+1+n_numaux) names_table0 symbol_table0;
							-> if (n_numaux==0 || n_type==0x20)
								(define_symbols_lp (symbol_n+1+n_numaux) names_table0 (new_symbol_table n_value))
								(define_symbols_lp (symbol_n+1+n_numaux) names_table0 (new_symbol_table_with_aux n_value));
					C_FUNCTION
						-> define_symbols_lp (symbol_n+1+n_numaux) names_table0 symbol_table0;
					C_FILE
						-> define_symbols_lp (symbol_n+1+n_numaux) names_table0 symbol_table0;
				}
			{
				new_symbol_table n_value
				#	segment_n=sections.[n_scnum].section_segment_n;
					| segment_n>0
						= {symbol_table0 & symbols = {symbol_table0.symbols & [symbol_n]=SectionLabel n_scnum n_value} };
						= symbol_table0;

				new_symbol_table_with_aux :: Int -> SymbolTable;
				new_symbol_table_with_aux n_value
				#	section_section_n=sections.[n_scnum];
					{section_segment_n,section_n_relocations,section_relocations,section_size,section_virtual_address,section_data_offset}=section_section_n;
					| section_segment_n==TEXT_SECTION && x_scnlen==section_size
						= {symbol_table0 & 
							symbols     = {symbol_table0.symbols & [symbol_n]=Module TEXT_SECTION n_value x_scnlen section_virtual_address section_data_offset section_n_relocations section_relocations},
							text_symbols= SymbolIndex symbol_n symbol_table0.text_symbols,
							section_symbol_ns = {symbol_table0.section_symbol_ns & [n_scnum]=symbol_n}
						  };
					| section_segment_n==DATA_SECTION && x_scnlen==section_size
						= {symbol_table0 &
							symbols     ={symbol_table0.symbols & [symbol_n]=Module DATA_SECTION n_value x_scnlen section_virtual_address section_data_offset section_n_relocations section_relocations},
							data_symbols= SymbolIndex symbol_n symbol_table0.data_symbols,
							section_symbol_ns = {symbol_table0.section_symbol_ns & [n_scnum]=symbol_n}
					 	  };
					| section_segment_n==BSS_SECTION
						= {symbol_table0 & 
							symbols     = {symbol_table0.symbols & [symbol_n]= Module BSS_SECTION n_value x_scnlen 0 0 section_n_relocations section_relocations},
							bss_symbols= SymbolIndex symbol_n symbol_table0.bss_symbols,
							section_symbol_ns = {symbol_table0.section_symbol_ns & [n_scnum]=symbol_n}
						  };
						= symbol_table0;
//						= symbol_table_with_label;
				

				name_of_symbol :: {#Char}; // to help the typechecker
				name_of_symbol
					| first_chars==0
						= string_table % (string_table_offset,dec (first_zero_char_offset_or_max string_table string_table_offset (size string_table)));
						{
							string_table_offset = (symbol_table_string ILONG (offset+4))-4;
						}
						= symbol_table_string % (offset,dec (first_zero_char_offset_or_max symbol_table_string offset (offset+8)));
					{}{
						first_chars = symbol_table_string ILONG offset;
						
						first_zero_char_offset_or_max string offset max
							| offset>=max || string CHAR offset=='\0'
								= offset;
								= first_zero_char_offset_or_max string (offset+1) max;
					}

				
				x_scnlen=symbol_table_string ILONG last_aux_offset;

				last_aux_offset=offset+SIZE_OF_SYMBOL*n_numaux;
				
				n_value=symbol_table_string ILONG (offset+8);
				n_scnum=symbol_table_string IWORD (offset+12);
				n_type=symbol_table_string IWORD (offset+14);
				n_numaux=symbol_table_string BYTE (offset+17);
			}
		{
			offset=SIZE_OF_SYMBOL*symbol_n;
		}
	}

read_coff_header :: *File -> (!Bool,!Int,!Int,!Int,!*File);
read_coff_header file
#	(header_string,file) = freads file SIZE_OF_HEADER;
	f_nscns =header_string IWORD 2;
	| not (size header_string==SIZE_OF_HEADER && header_string IWORD 0==0x014c && f_nscns>=2)
		= error file;
#
	f_opthdr=header_string IWORD 16;
	f_symptr=header_string ILONG 8;
	f_nsyms=header_string ILONG 12;
	| f_opthdr==0
		= (True,f_nscns,f_symptr,f_nsyms,file);
#
	(fseek_ok,file2)=fseek file f_opthdr FSeekCur;
	| fseek_ok
		= (True,f_nscns,f_symptr,f_nsyms,file2);
	= (error file2);
	{}{
		error file = (False,0,0,0,file);
	}

:: Section = {
		section_segment_n			::!Int,
		section_virtual_address		::!Int,
		section_size				::!Int,
		section_data_offset			::!Int,
		section_relocations_offset	::!Int,
		section_n_relocations		::!Int,
		section_relocations			::!String
	};

read_section_headers :: Int Int *{!Section} *File -> (!Bool,*{!Section},!*File);
read_section_headers section_n n_sections sections file
	| section_n>n_sections
		= (True,sections,file);
#
	(header_string,file) = freads file SIZE_OF_SECTION_HEADER;
	| size header_string<>SIZE_OF_SECTION_HEADER
		= (False,sections,file);
#
	section_segment_n =	if (header_string % (0,5)==".text\0") TEXT_SECTION
						(if (header_string % (0,5)==".data\0") DATA_SECTION
						(if (header_string % (0,6)==".rdata\0") DATA_SECTION
						(if (header_string % (0,4)==".bss\0") BSS_SECTION
						0)));
	| section_segment_n <> 0
#		sections = {sections & [section_n] = {
						section_segment_n			=section_segment_n,
						section_virtual_address		=header_string ILONG 12,
						section_size				=header_string ILONG 16,
						section_data_offset			=header_string ILONG 20,
						section_relocations_offset	=header_string ILONG 24,
						section_n_relocations		=header_string IWORD 32,
						section_relocations			=""
					}};
		= read_section_headers (inc section_n) n_sections sections file;

		= read_section_headers (inc section_n) n_sections sections file;

read_relocations section_n n_sections sections file
	| section_n>n_sections
		= (True,sections,file);

	| sections.[section_n].section_n_relocations<=0
		= read_relocations (section_n+1) n_sections sections file;
#	
	(sections_section_n,sections) = uselect sections section_n;
	(fseek_ok,file)=fseek file sections_section_n.section_relocations_offset FSeekSet;
	| not fseek_ok
		= (False,sections,file);
#
	relocation_size=sections_section_n.section_n_relocations * SIZE_OF_RELOCATION;
	(relocation_string,file) = freads file relocation_size;
	| size relocation_string<>relocation_size
		= (False,sections,file);

	= read_relocations (section_n+1) n_sections {sections & [section_n]={sections_section_n & section_relocations=relocation_string} } file;

read_xcoff_file :: !String NamesTable Bool !Files Int -> (![String],!*String,!*String,!Xcoff,!NamesTable,!Files);
read_xcoff_file file_name names_table0 one_pass_link files file_n
#	(ok,file,files) = fopen file_name FReadData files;
	| not ok
		= error ("Cannot open file \""+++file_name+++"\"") file files;
#
	(ok,n_sections,symbol_table_offset,n_symbols,file) = read_coff_header file;
	| not ok
		= error ("Not an xcoff file: \""+++file_name+++"\"") file files;
#
	sections = createArray (n_sections+1) {	section_segment_n= -1,section_virtual_address=0,section_size= -1,
											section_data_offset=0,section_relocations_offset=0,section_n_relocations= -1,
											section_relocations=""
										  };
	(ok,sections,file) = read_section_headers 1 n_sections sections file;
	| not ok
		= error "Error in section header" file files;
#
	(ok,sections,file) = read_relocations 1 n_sections sections file;
	| not ok
		= error "Error in text relocations" file files;
#
	text_section = {};
	data_section = {};
	(ok,symbol_table_string,string_table,file) = read_symbol_table symbol_table_offset n_symbols file;
	| not ok
		= error ("Error in symbol table "+++file_name) file files;
		
		= ([],text_section,data_section,xcoff_file,names_table1,close_file file files);
		{
			xcoff_file={file_name=file_name,symbol_table=symbol_table0,n_symbols=n_symbols };
			(names_table1,symbol_table0)
				=define_symbols n_sections n_symbols symbol_table_string string_table sections names_table0 file_n;
		}
	{		
		close_file file files = files2;
		{
			(_,files2)=fclose file files;
		}

		error :: String !*File !*Files -> (![String],!*String,!*String,!Xcoff,!NamesTable,!Files);
		error error_string file files
			= ([error_string],empty_section_string,empty_section_string,empty_xcoff,names_table0,close_file file files);
	}

empty_section_string :: .String;
empty_section_string = createArray 0 ' ';

empty_xcoff ::.SXcoff;
empty_xcoff
	= { file_name="",symbol_table=empty_symbol_table,n_symbols=0 };
	{
		empty_symbol_table = {	
			text_symbols=EmptySymbolIndex,data_symbols=EmptySymbolIndex,bss_symbols=EmptySymbolIndex,
			imported_symbols=EmptySymbolIndex,symbols={},section_symbol_ns={}
		};
	}
