From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 Jan 2009 10:50:29 +0000 (+0000)
Subject: - Added new output in standard C.
X-Git-Tag: make_still_working~4263
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b7aefa8f362d07bf9042f6879252345e69da07c8;p=helm.git

- Added new output in standard C.
---

diff --git a/helm/software/matita/contribs/assembly/parser/parser.y b/helm/software/matita/contribs/assembly/parser/parser.y
index 40d901ac7..373f3b2fd 100755
--- a/helm/software/matita/contribs/assembly/parser/parser.y
+++ b/helm/software/matita/contribs/assembly/parser/parser.y
@@ -158,6 +158,7 @@ typedef struct _valueLeaf_
 /* ************************************************************************* */
 
 valueLeaf	root;				/* radice dell'AST */
+valueLeaf	*typeRoot=NULL;		/* radice degli user type */
 
 int			numErr=0;
 
@@ -187,6 +188,10 @@ valueLeaf	*treeId1Alloc(vEnum id,valueLeaf *param1,const YYLTYPE *locp);
 valueLeaf	*treeId2Alloc(vEnum id,valueLeaf *param1,valueLeaf *param2,const YYLTYPE *locp);
 valueLeaf	*treeId3Alloc(vEnum id,valueLeaf *param1,valueLeaf *param2,valueLeaf *param3,const YYLTYPE *locp);
 
+int			eqUserType(valueLeaf *type1,valueLeaf *type2);
+int			getUserType(valueLeaf *type,valueLeaf **res);
+void		createUserType(valueLeaf *type);
+
 void prettyPrint(valueLeaf *cur,int indent);
 
 /* ************************************************************************* */
@@ -289,7 +294,7 @@ _decl_lst_		:	Keyword_CONST _type_ Value_STRING DualOperator_ASG _init_choice_ S
 					_type_ Value_STRING _init_ Separator_COLUMN _decl_lst_
 						{
 						$$=treeId3Alloc(E_DECL_VAR,$1,$2,$3,&@1);
-						$$->next=$5;
+						$$->next=$5;						
 						}|
 					_stm_lst_
 						{ $$=$1; };
@@ -308,6 +313,8 @@ _type_			:	Keyword_ARRAY OpenBracket_SQUARE Value_INUM CloseBracket_SQUARE Keywo
 						{
 						$$=treeId1Alloc(E_TYPE_STRUCT,$3,&@1);
 						$3->next=$5;
+
+						createUserType($$);
 						}|
 					Type_DWORD
 						{ $$=treeId0Alloc(E_TYPE_DWORD,&@1); }|
@@ -863,6 +870,107 @@ void usage(char *name)
 	return;
 }
 
+/* *************************** gestione degli user type *********** */
+
+int eqUserType(valueLeaf *type1,valueLeaf *type2)
+{
+	valueLeaf	*tmp1,*tmp2;
+
+	if(type1->id!=type2->id)
+		{ return(0); }
+
+	switch(type1->id)
+		{
+		case E_TYPE_DWORD:
+		case E_TYPE_WORD:
+		case E_TYPE_BYTE:
+			return(1);
+
+		case E_TYPE_ARRAY:
+			if(type1->param1->inumValue!=type2->param1->inumValue)
+				{ return(0); }
+
+			return(eqUserType(type1->param2,type2->param2));
+
+		case E_TYPE_STRUCT:
+			tmp1=type1->param1;
+			tmp2=type2->param1;
+
+			while(tmp1&&tmp2)
+				{
+				if(!eqUserType(tmp1,tmp2))
+					{ return(0); }
+
+				tmp1=tmp1->next;
+				tmp2=tmp2->next;
+				}
+
+			return(!(tmp1||tmp2));
+
+		/* dummy */
+		default:
+			return(0);
+		}
+}
+
+int getUserType(valueLeaf *type,valueLeaf **res)
+{
+	valueLeaf	*tmpRes=typeRoot;
+	valueLeaf	*lastRes;
+	int			index=1;
+
+	while(tmpRes)
+		{
+		if(eqUserType(type,tmpRes))
+			{
+			if(res)
+				{ *res=tmpRes; }
+			return(index);
+			}
+
+		lastRes=tmpRes;
+		tmpRes=tmpRes->next;
+		index++;
+		}
+
+	if(res)
+		{ *res=lastRes; }
+	return(0);
+}
+
+void createUserType(valueLeaf *type)
+{
+	if(!typeRoot)
+		{
+		if(!(typeRoot=(valueLeaf *) myMalloc(sizeof(valueLeaf))))
+			{
+			printf("[%s:%d] ParsError:OutOfMemory%c",__FILE__,__LINE__,SEP);
+			exit(ERR_EXIT);
+			}
+
+		memcpy(typeRoot,type,sizeof(valueLeaf));
+		typeRoot->next=NULL;
+		}
+	else
+		{
+		valueLeaf	*res;
+
+		if(!getUserType(type,&res))
+			{
+			if(!(res->next=(valueLeaf *) myMalloc(sizeof(valueLeaf))))
+				{
+				printf("[%s:%d] ParsError:OutOfMemory%c",__FILE__,__LINE__,SEP);
+				exit(ERR_EXIT);
+				}
+
+			memcpy(res->next,type,sizeof(valueLeaf));
+			res->next->next=NULL;
+			}
+		}
+}
+
+/* *************************** prettyPrint ************************ */
+
 void prettyPrintString(char *str)
 {
 	printf("([");
@@ -1421,6 +1529,255 @@ void prettyPrint(valueLeaf *cur,int indent)
 		}
 }
 
+/* *************************** cPrint ***************************** */
+
+void cPrintIndent(int indent)
+{
+	int	index;
+
+	for(index=0;index<indent;index++)
+		{ printf("\t"); }
+}
+
+void cPrintTypesAux(valueLeaf *type,int field)
+{
+	if(type->id==E_TYPE_STRUCT)
+		{ printf("\tuser%d_t\tfield%d;\n\n",getUserType(type,NULL),field); }
+	else if(type->id==E_TYPE_ARRAY)
+		{
+		char		bufferDim[256];
+		valueLeaf	*tmp=type;
+
+		memset(bufferDim,0,256);
+
+		while(tmp->id==E_TYPE_ARRAY)
+			{
+			sprintf(&bufferDim[strlen(bufferDim)],"[%d]",tmp->param1->inumValue+1);
+			tmp=tmp->param2;
+			}
+
+		if(tmp->id==E_TYPE_STRUCT)
+			{ printf("\tuser%d_t\tfield%d%s;\n\n",getUserType(tmp,NULL),field,bufferDim); }
+		else if(tmp->id==E_TYPE_DWORD)
+			{ printf("\t_DWORD_\tfield%d%s;\n\n",field,bufferDim); }
+		else if(tmp->id==E_TYPE_WORD)
+			{ printf("\t_WORD_\tfield%d%s;\n\n",field,bufferDim); }
+		else
+			{ printf("\t_BYTE_\tfield%d%s;\n\n",field,bufferDim); }
+		}
+	else if(type->id==E_TYPE_DWORD)
+		{ printf("\t_DWORD_\tfield%d;\n\n",field); }
+	else if(type->id==E_TYPE_WORD)
+		{ printf("\t_WORD_\tfield%d;\n\n",field); }
+	else
+		{ printf("\t_BYTE_\tfield%d;\n\n",field); }
+
+	if(type->next)
+		{ cPrintTypesAux(type->next,field+1); }
+}
+
+void cPrintTypes(void)
+{
+	int			index=1;
+	valueLeaf	*cur=typeRoot;
+
+	while(cur)
+		{
+		printf("typedef struct\n");
+		printf("{\n");
+		cPrintTypesAux(cur->param1,0);
+		printf("} user%d_t;\n\n",index);
+
+		cur=cur->next;
+		index++;
+		}
+}
+
+void cPrint(valueLeaf *cur,int indent)
+{
+	/* ** valori ** */
+	if(cur->id==E_VALUE_INUM)
+		{ printf("%lu",cur->inumValue); }
+	else if(cur->id==E_VALUE_BYTE)
+		{ printf("0x%02lX",(_DWORD_) cur->byteValue); }
+	else if(cur->id==E_VALUE_WORD)
+		{ printf("0x%04lX",(_DWORD_) cur->wordValue); }
+	else if(cur->id==E_VALUE_DWORD)
+		{ printf("0x%08lX",cur->dwordValue); }
+	else if((cur->id==E_VALUE_ARRAY)||(cur->id==E_VALUE_STRUCT))
+		{
+		valueLeaf	*tmp=cur->param1;
+
+		printf("{ ");
+		while(tmp)
+			{
+			cPrint(tmp,indent);
+			tmp=tmp->next;
+			if(tmp)
+				{ printf(", "); }
+			}
+		printf(" }");
+		}
+
+	/* ** variabili ** */
+	else if((cur->id==E_VAR_ROOT)||(cur->id==E_VAR_STRUCT)||(cur->id==E_VAR_ARRAY))
+		{
+		valueLeaf	*tmp=cur;
+
+		while(tmp->id!=E_VAR_ROOT)
+			{
+			tmp->next->last=tmp;
+			tmp=tmp->next;
+			}
+
+		while(1)
+			{
+			if(tmp->id==E_VAR_ROOT)
+				{ printf("%s",tmp->param1->stringValue); }
+			else if(tmp->id==E_VAR_STRUCT)
+				{ printf(".field%lu",tmp->param1->inumValue); }
+			else if(tmp->id==E_VAR_ARRAY)
+				{ printf("["); cPrint(tmp->param1,indent); printf("]"); }
+
+			if(tmp==cur)
+				{ break; }
+			else
+				{ tmp=tmp->last; }
+			}
+		}
+
+	/* ** espressioni ** */
+	else if(cur->id==E_EXPR_VAR)
+		{ cPrint(cur->param1,indent); }
+	else if(cur->id==E_EXPR_NOT)
+		{ printf("!("); cPrint(cur->param1,indent); printf(")"); }
+	else if(cur->id==E_EXPR_COM)
+		{ printf("~("); cPrint(cur->param1,indent); printf(")"); }
+	else if(cur->id==E_EXPR_NEG)
+		{ printf("-("); cPrint(cur->param1,indent); printf(")"); }
+	else if((cur->id==E_EXPR_W2B)||(cur->id==E_EXPR_DW2B))
+		{ printf("((_BYTE_) ("); cPrint(cur->param1,indent); printf("))"); }
+	else if((cur->id==E_EXPR_B2W)||(cur->id==E_EXPR_DW2W))
+		{ printf("((_WORD_) ("); cPrint(cur->param1,indent); printf("))"); }
+	else if((cur->id==E_EXPR_B2DW)||(cur->id==E_EXPR_W2DW))
+		{ printf("((_DWORD_) ("); cPrint(cur->param1,indent); printf("))"); }
+	else if(cur->id==E_EXPR_ADD)
+		{ printf("("); cPrint(cur->param1,indent); printf(") + ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_SUB)
+		{ printf("("); cPrint(cur->param1,indent); printf(") - ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_MUL)
+		{ printf("("); cPrint(cur->param1,indent); printf(") * ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_DIV)
+		{ printf("("); cPrint(cur->param1,indent); printf(") / ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_SHL)
+		{ printf("("); cPrint(cur->param1,indent); printf(") << ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_SHR)
+		{ printf("("); cPrint(cur->param1,indent); printf(") >> ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_AND)
+		{ printf("("); cPrint(cur->param1,indent); printf(") & ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_OR)
+		{ printf("("); cPrint(cur->param1,indent); printf(") | ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_XOR)
+		{ printf("("); cPrint(cur->param1,indent); printf(") ^ ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_LT)
+		{ printf("("); cPrint(cur->param1,indent); printf(") < ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_LTE)
+		{ printf("("); cPrint(cur->param1,indent); printf(") <= ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_GT)
+		{ printf("("); cPrint(cur->param1,indent); printf(") > ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_GTE)
+		{ printf("("); cPrint(cur->param1,indent); printf(") >= ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_EQ)
+		{ printf("("); cPrint(cur->param1,indent); printf(") == ("); cPrint(cur->param2,indent); printf(")"); }
+	else if(cur->id==E_EXPR_NEQ)
+		{ printf("("); cPrint(cur->param1,indent); printf(") != ("); cPrint(cur->param2,indent); printf(")"); }
+
+	/* ** statement ** */
+	else if(cur->id==E_STM_ASG)
+		{
+		cPrintIndent(indent); cPrint(cur->param1,indent); printf(" = "); cPrint(cur->param2,indent); printf(";\n\n");
+
+		if(cur->next)
+			{ cPrint(cur->next,indent); }
+		}
+	else if(cur->id==E_STM_WHILE)
+		{
+		cPrintIndent(indent); printf("while("); cPrint(cur->param1,indent); printf(")\n");
+		cPrintIndent(indent+1); printf("{\n");
+		cPrint(cur->param2,indent+1);
+		cPrintIndent(indent+1); printf("}\n\n");
+
+		if(cur->next)
+			{ cPrint(cur->next,indent); }
+		}
+	else if(cur->id==E_STM_IF)
+		{
+		valueLeaf	*tmp=cur->param1;
+
+		while(tmp)
+			{
+			cPrintIndent(indent); printf("%s(",(tmp==cur->param1) ? "if" : "else if"); cPrint(tmp->param1,indent); printf(")\n");
+			cPrintIndent(indent+1); printf("{\n");
+			cPrint(tmp->param2,indent+1);
+			cPrintIndent(indent+1); printf("}\n");
+
+			tmp=tmp->next;
+			}
+
+		if(cur->param2)
+			{
+			cPrintIndent(indent); printf("else\n");
+			cPrintIndent(indent+1); printf("{\n");
+			cPrint(cur->param2,indent+1);
+			cPrintIndent(indent+1); printf("}\n");
+			}
+
+		printf("\n");
+
+		if(cur->next)
+			{ cPrint(cur->next,indent); }
+		}
+
+	/* ** dichiarazioni ** */
+	else if((cur->id==E_DECL_CONST)||(cur->id==E_DECL_VAR))
+		{
+		valueLeaf	*tmp=cur->param1;
+		char		bufferDim[256];
+
+		memset(bufferDim,0,256);
+
+		while(tmp->id==E_TYPE_ARRAY)
+			{
+			sprintf(&bufferDim[strlen(bufferDim)],"[%d]",tmp->param1->inumValue+1);
+			tmp=tmp->param2;
+			}
+
+		cPrintIndent(indent);
+		if(cur->id==E_DECL_CONST)
+			{ printf("const "); }
+
+		if(tmp->id==E_TYPE_STRUCT)
+			{ printf("user%d_t\t",getUserType(tmp,NULL)); }
+		else if(tmp->id==E_TYPE_DWORD)
+			{ printf("_DWORD_\t"); }
+		else if(tmp->id==E_TYPE_WORD)
+			{ printf("_WORD_\t"); }
+		else
+			{ printf("_BYTE_\t"); }
+
+		printf("%s%s",cur->param2->stringValue,bufferDim);
+
+		if(cur->param3)
+			{ printf(" = "); cPrint(cur->param3,indent); }
+		printf(";\n\n");
+
+		if(cur->next)
+			{ cPrint(cur->next,indent); }
+		}
+}
+
+/* *************************** main ******************************* */
+
 int main(int argc,char **argv)
 {
 	int		ret;
@@ -1433,10 +1790,29 @@ int main(int argc,char **argv)
 
 	if((!ret)&&(!numErr))
 		{
+		printf("(* matita language *)\n\n");
 		printf("definition parsingResult \\def\n");
 		printf(" (PREAST_ROOT\n");
 		prettyPrint(&root,2);
-		printf(" ).");
+		printf(" ).\n\n");
+
+		printf("(* C language\n\n");
+		printf("#ifndef\t__STDC__\n");
+		printf("typedef\tunsigned __int32\t_DWORD_;\n");
+		printf("typedef\tunsigned __int16\t_WORD_;\n");
+		printf("typedef\tunsigned __int8\t_BYTE_;\n");
+		printf("#else\n");
+		printf("typedef\t__uint32_t\t_DWORD_;\n");
+		printf("typedef\t__uint16_t\t_WORD_;\n");
+		printf("typedef\t__uint8_t\t_BYTE_;\n");
+		printf("#endif\n\n");
+		cPrintTypes();
+		printf("void main(void)\n");
+		printf("{\n");
+		cPrint(&root,1);
+		printf("\treturn;\n\n");
+		printf("}\n\n");
+		printf("*)");
 		}
 
 	return(ret);
diff --git a/helm/software/matita/contribs/assembly/parser/test0.cm b/helm/software/matita/contribs/assembly/parser/test0.cm
new file mode 100644
index 000000000..cd8183bf2
--- /dev/null
+++ b/helm/software/matita/contribs/assembly/parser/test0.cm
@@ -0,0 +1,19 @@
+{
+	const array[2] of struct { array[2] of byte; word; dword; } n1=[{[0x00,0x01],0x0000,0x00000000},{[0x02,0x03],0x0001,0x00000001}];
+
+	word n2=n1[0x00].1;
+
+	byte n3;
+
+	while(n2)
+		{
+		dword n1=n1[n2].2;
+
+		if(n1>0x1234ABCD)
+			{ n3=-!~(dw2b(w2dw(b2w(n3)))+0x01-0x02*0x03/0x04>>0x05<<0x06&0x07|0x08^0x09); }
+
+		n2=n2+0x0001;
+		}
+
+	n3=n1[0x01].0[0x00];
+}
\ No newline at end of file
diff --git a/helm/software/matita/contribs/assembly/parser/test1.cm b/helm/software/matita/contribs/assembly/parser/test1.cm
new file mode 100644
index 000000000..a53a87950
--- /dev/null
+++ b/helm/software/matita/contribs/assembly/parser/test1.cm
@@ -0,0 +1,42 @@
+#define u1 struct { byte; word; }
+#define u2 struct { word; byte; }
+#define u3 struct { array[2] of u1; array[3] of u2; }
+#define u4 struct { array[3] of u1; array[2] of u2; }
+#define u5 struct { dword; u3; u4; array[5] of word; }
+
+{
+	u5 var5;
+	byte index=0x00;
+
+	while(index<0x02)
+		{
+		const array[4] of u1 const1=[{0x00,0x0000},{0x01,0x0001},{0x02,0x0002},{0x03,0x0003}];
+		const array[4] of u2 const2=[{0x0000,0x00},{0x0001,0x01},{0x0002,0x02},{0x0003,0x03}];
+
+		var5.1.0[index].0=const1[index].0+(index*0x03);
+		var5.1.0[index].1=const1[index].1*(b2w(index)-0x1234);
+		var5.2.1[index].0=const1[index].1&(b2w(index)/0xABCD);
+		var5.2.1[index].1=const1[index].0^(!index);
+
+		if(index!=0x00)
+			{
+			dword tmp=0x1234FEDC;
+
+			var5.0=tmp;
+			}
+		elsif(index==0x01)
+			{
+			array[7] of array[8] of array [9] of byte tmp;
+
+			tmp[0x02][0x01][0x00]=index;
+			}
+		else
+			{
+			array[10] of u5 tmp;
+
+			tmp[0x00].0=var5.0;
+			}
+
+		index=index+0x01;
+		}
+}