From 38fccc2b774e493a94eedef76342b56079c0e694 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Wed, 5 Aug 2009 18:18:06 +0000 Subject: [PATCH] freescale porting, work in progress --- .../contribs/ng_assembly/common/ascii.ma | 4 +- .../ng_assembly/common/ascii_lemmas1.ma | 4 +- .../ng_assembly/common/ascii_lemmas2.ma | 4 +- .../contribs/ng_assembly/common/list.ma | 4 +- .../ng_assembly/common/list_lemmas.ma | 4 +- .../ng_assembly/common/list_utility.ma | 4 +- .../ng_assembly/common/list_utility_lemmas.ma | 4 +- .../matita/contribs/ng_assembly/common/nat.ma | 4 +- .../contribs/ng_assembly/common/nat_lemmas.ma | 4 +- .../contribs/ng_assembly/common/nat_to_num.ma | 4 +- .../contribs/ng_assembly/common/option.ma | 4 +- .../ng_assembly/common/option_lemmas.ma | 4 +- .../contribs/ng_assembly/common/prod.ma | 4 +- .../ng_assembly/common/prod_lemmas.ma | 4 +- .../contribs/ng_assembly/common/sigma.ma | 50 ++++++++ .../contribs/ng_assembly/common/string.ma | 4 +- .../ng_assembly/common/string_lemmas.ma | 4 +- .../contribs/ng_assembly/common/theory.ma | 4 +- .../contribs/ng_assembly/compiler/ast_type.ma | 4 +- .../ng_assembly/compiler/ast_type_lemmas.ma | 4 +- .../ng_assembly/compiler/preast_tree.ma | 115 ++++++++++++++++++ .../matita/contribs/ng_assembly/depends | 2 + .../ng_assembly/freescale/load_write.ma | 4 +- .../ng_assembly/freescale/memory_abs.ma | 4 +- .../ng_assembly/freescale/memory_bits.ma | 4 +- .../ng_assembly/freescale/memory_func.ma | 4 +- .../ng_assembly/freescale/memory_struct.ma | 4 +- .../ng_assembly/freescale/memory_trees.ma | 4 +- .../contribs/ng_assembly/freescale/model.ma | 4 +- .../contribs/ng_assembly/freescale/multivm.ma | 4 +- .../ng_assembly/freescale/multivm_lemmas.ma | 4 +- .../contribs/ng_assembly/freescale/opcode.ma | 4 +- .../ng_assembly/freescale/opcode_base.ma | 4 +- .../freescale/opcode_base_lemmas.ma | 4 +- .../freescale/opcode_base_lemmas1.ma | 4 +- .../opcode_base_lemmas_instrmode1.ma | 4 +- .../opcode_base_lemmas_instrmode2.ma | 4 +- .../freescale/opcode_base_lemmas_opcode1.ma | 4 +- .../freescale/opcode_base_lemmas_opcode2.ma | 4 +- .../contribs/ng_assembly/freescale/status.ma | 4 +- .../ng_assembly/freescale/status_lemmas.ma | 4 +- .../ng_assembly/freescale/table_HC05.ma | 4 +- .../ng_assembly/freescale/table_HC05_tests.ma | 4 +- .../ng_assembly/freescale/table_HC08.ma | 4 +- .../ng_assembly/freescale/table_HC08_tests.ma | 4 +- .../ng_assembly/freescale/table_HCS08.ma | 4 +- .../freescale/table_HCS08_tests.ma | 4 +- .../ng_assembly/freescale/table_RS08.ma | 4 +- .../ng_assembly/freescale/table_RS08_tests.ma | 4 +- .../ng_assembly/freescale/translation.ma | 4 +- .../freescale_tests/medium_tests.ma | 4 +- .../freescale_tests/medium_tests_tools.ma | 4 +- .../freescale_tests/micro_tests.ma | 4 +- .../contribs/ng_assembly/num/bitrigesim.ma | 4 +- .../ng_assembly/num/bitrigesim_lemmas.ma | 4 +- .../matita/contribs/ng_assembly/num/bool.ma | 4 +- .../contribs/ng_assembly/num/bool_lemmas.ma | 4 +- .../matita/contribs/ng_assembly/num/byte8.ma | 4 +- .../contribs/ng_assembly/num/byte8_lemmas.ma | 4 +- .../contribs/ng_assembly/num/exadecim.ma | 4 +- .../ng_assembly/num/exadecim_lemmas.ma | 4 +- .../matita/contribs/ng_assembly/num/oct.ma | 4 +- .../contribs/ng_assembly/num/oct_lemmas.ma | 4 +- .../contribs/ng_assembly/num/quatern.ma | 4 +- .../ng_assembly/num/quatern_lemmas.ma | 4 +- .../matita/contribs/ng_assembly/num/word16.ma | 4 +- .../contribs/ng_assembly/num/word16_lemmas.ma | 4 +- .../matita/contribs/ng_assembly/num/word32.ma | 4 +- .../contribs/ng_assembly/num/word32_lemmas.ma | 4 +- 69 files changed, 299 insertions(+), 132 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/common/sigma.ma create mode 100755 helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii.ma b/helm/software/matita/contribs/ng_assembly/common/ascii.ma index 9cebb3317..e5e195286 100755 --- a/helm/software/matita/contribs/ng_assembly/common/ascii.ma +++ b/helm/software/matita/contribs/ng_assembly/common/ascii.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas1.ma index 9d9920dea..89cafaf0a 100755 --- a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas1.ma +++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas1.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas2.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas2.ma index b3a559e10..e7cbe0e4c 100755 --- a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas2.ma +++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas2.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/list.ma b/helm/software/matita/contribs/ng_assembly/common/list.ma index a5322a996..d4571fa92 100644 --- a/helm/software/matita/contribs/ng_assembly/common/list.ma +++ b/helm/software/matita/contribs/ng_assembly/common/list.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma index 51654011e..90461cfca 100644 --- a/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/list_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma index 3ffd1d3c5..ae40ba75d 100755 --- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma +++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma index 5ae7fce81..9cc7f317d 100755 --- a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/nat.ma b/helm/software/matita/contribs/ng_assembly/common/nat.ma index 7e9ec23e4..4db935b1e 100755 --- a/helm/software/matita/contribs/ng_assembly/common/nat.ma +++ b/helm/software/matita/contribs/ng_assembly/common/nat.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma index f4525c463..4bfc4c118 100644 --- a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma index db38d086d..6ea1507af 100755 --- a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma +++ b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/option.ma b/helm/software/matita/contribs/ng_assembly/common/option.ma index cbd1c4907..0b71c17e4 100644 --- a/helm/software/matita/contribs/ng_assembly/common/option.ma +++ b/helm/software/matita/contribs/ng_assembly/common/option.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma index 34d63c601..303d11ad3 100644 --- a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/prod.ma b/helm/software/matita/contribs/ng_assembly/common/prod.ma index 39f79e96e..5be106fcb 100644 --- a/helm/software/matita/contribs/ng_assembly/common/prod.ma +++ b/helm/software/matita/contribs/ng_assembly/common/prod.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma index 9083f2b4d..8ebed668a 100644 --- a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/sigma.ma b/helm/software/matita/contribs/ng_assembly/common/sigma.ma new file mode 100755 index 000000000..34ee411cd --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/common/sigma.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +(* coppia dipendente *) + +inductive sigma (A:Type) (P:A → Type) : Type ≝ + sigma_intro: ∀x:A.P x → sigma A P. + +notation < "hvbox(\Sigma ident i opt (: tx) break . p)" + right associative with precedence 20 +for @{ 'Sigma ${default + @{\lambda ${ident i} : $tx. $p} + @{\lambda ${ident i} . $p}}}. + +notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px" + with precedence 20 + for ${ default + @{ ${ fold right @{$Px} rec acc @{'Sigma (λ${ident x}:$T.$acc)} } } + @{ ${ fold right @{$Px} rec acc @{'Sigma (λ${ident x}.$acc)} } } + }. + +notation "\ll term 19 a, break term 19 b \gg" +with precedence 90 for @{'dependent_pair (λx:?.? x) $a $b}. +interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro ? c a b). + +interpretation "sigma" 'Sigma \eta.x = (sigma ? x). + +definition sigmaFst ≝ +λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ]. +definition sigmaSnd ≝ +λT:Type.λf:T → Type.λs:sigma T f.match s return λs.f (sigmaFst ?? s) with [ sigma_intro _ x ⇒ x ]. diff --git a/helm/software/matita/contribs/ng_assembly/common/string.ma b/helm/software/matita/contribs/ng_assembly/common/string.ma index 8763ec8fc..7cf5ab73a 100644 --- a/helm/software/matita/contribs/ng_assembly/common/string.ma +++ b/helm/software/matita/contribs/ng_assembly/common/string.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma index 67590ae1e..7429ab70b 100755 --- a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma index 2bf08ce48..bb1358926 100644 --- a/helm/software/matita/contribs/ng_assembly/common/theory.ma +++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma index f2bc4229f..7f33aada2 100755 --- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma index 7a257f335..8b4549743 100755 --- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma new file mode 100755 index 000000000..5263b84e4 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/compiler/preast_tree.ma @@ -0,0 +1,115 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) +(* *) +(* ********************************************************************** *) + +include "common/string.ma". +include "compiler/ast_type.ma". +include "num/word32.ma". + +(* ****************** *) +(* PREALBERO DI TOKEN *) +(* ****************** *) + +(* espressioni *) +ninductive preast_expr : Type ≝ + PREAST_EXPR_BYTE8 : byte8 → preast_expr +| PREAST_EXPR_WORD16: word16 → preast_expr +| PREAST_EXPR_WORD32: word32 → preast_expr + +| PREAST_EXPR_NEG: preast_expr → preast_expr +| PREAST_EXPR_NOT: preast_expr → preast_expr +| PREAST_EXPR_COM: preast_expr → preast_expr + +| PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_AND: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_OR: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_XOR: preast_expr → preast_expr → preast_expr + +| PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr +| PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr +| PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr +| PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr +| PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr + +| PREAST_EXPR_B8toW16 : preast_expr → preast_expr +| PREAST_EXPR_B8toW32 : preast_expr → preast_expr +| PREAST_EXPR_W16toB8 : preast_expr → preast_expr +| PREAST_EXPR_W16toW32: preast_expr → preast_expr +| PREAST_EXPR_W32toB8 : preast_expr → preast_expr +| PREAST_EXPR_W32toW16: preast_expr → preast_expr + +| PREAST_EXPR_ID: preast_var → preast_expr + +(* variabile: modificatori di array/struct dell'id *) +with preast_var : Type ≝ + PREAST_VAR_ID: aux_str_type → preast_var +| PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var +| PREAST_VAR_STRUCT: preast_var → nat → preast_var. + +(* -------------------------- *) + +(* inizializzatori: ... valori ... *) +inductive preast_init_val : Type ≝ + PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val +| PREAST_INIT_VAL_WORD16: word16 → preast_init_val +| PREAST_INIT_VAL_WORD32: word32 → preast_init_val +| PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val +| PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val. + +(* + inizializzatori: ammesse solo due forme, no ibridi + 1) var1 = var2 + 2) var = ... valori ... +*) +inductive preast_init : Type ≝ + PREAST_INIT_VAR: preast_var → preast_init +| PREAST_INIT_VAL: preast_init_val → preast_init. + +(* -------------------------- *) + +(* statement: assegnamento/while/if else if else *) +inductive preast_stm : Type ≝ + PREAST_STM_ASG: preast_var → preast_expr → preast_stm +| PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm +| PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm + +(* dichiarazioni *) +with preast_decl : Type ≝ + PREAST_NO_DECL: list preast_stm → preast_decl +| PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl +| PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl. + +(* -------------------------- *) + +(* programma *) +inductive preast_root : Type ≝ + PREAST_ROOT: preast_decl → preast_root. + +(* -------------------------- *) + +(* programma vuoto *) +definition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)). diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 943772164..0cc002df4 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -4,6 +4,7 @@ freescale/memory_bits.ma freescale/memory_trees.ma common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma num/bool.ma common/theory.ma freescale/table_HCS08_tests.ma freescale/opcode.ma freescale/table_HCS08.ma +compiler/preast_tree.ma common/string.ma compiler/ast_type.ma freescale/multivm.ma freescale/load_write.ma common/ascii_lemmas1.ma common/ascii.ma common/nat_to_num.ma common/nat.ma num/word32.ma @@ -58,6 +59,7 @@ common/option.ma num/bool.ma num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma common/ascii_lemmas2.ma common/ascii_lemmas1.ma num/bool_lemmas.ma common/list_lemmas.ma common/list.ma +common/sigma.ma freescale/opcode_base_lemmas_instrmode1.ma freescale/opcode_base.ma num/bitrigesim_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma num/bitrigesim.ma num/bool.ma common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma diff --git a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma index 0c14beae6..28704ff34 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma index 9c6e11cea..736f4aaea 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma index defef9be3..93dcfa53f 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma index 0da0e6e41..723ec0b84 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma index 7ce6ae07f..4fc65abeb 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma index 39a6468ae..b9d67c554 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_trees.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/model.ma b/helm/software/matita/contribs/ng_assembly/freescale/model.ma index f1e5b9488..fe01726c7 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/model.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/model.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma index 37ef8d9c6..44dacea60 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm_lemmas.ma index c1a6e2737..d0d74750d 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/multivm_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma index bfaa0e101..aeaaa8aef 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma index 20abd2f8c..f1bb166b5 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma index 1ffe02b4a..ce4e00642 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma index ba63e6013..db51eb145 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma index 8dedbf873..61cf6a5b8 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma index a80e96d21..9992a4c5e 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode2.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma index db2a96d46..72803e951 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode1.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.ma index 5e727309d..a14cd5801 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma index 7f56fe8a9..532b996ff 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma index 70161542d..9edad75cc 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_HC05.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_HC05.ma index cc26940a9..d02f4f30a 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/table_HC05.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/table_HC05.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_HC05_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_HC05_tests.ma index 67d148dee..75bb840b8 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/table_HC05_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/table_HC05_tests.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_HC08.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_HC08.ma index 578712267..bf4f48c17 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/table_HC08.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/table_HC08.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_HC08_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_HC08_tests.ma index 6ec7ad82e..8c85e3c39 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/table_HC08_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/table_HC08_tests.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08.ma index a3f3266cf..165ee1136 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma index 6cc138d66..bd4c8cd5f 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/table_HCS08_tests.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_RS08.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_RS08.ma index fc0ee75f9..8398e965e 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/table_RS08.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/table_RS08.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/table_RS08_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/table_RS08_tests.ma index 32727bcef..759d1bf0a 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/table_RS08_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/table_RS08_tests.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma index 0474e6e9b..661737793 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma index 4653cbf1a..0123dd885 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests_tools.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests_tools.ma index 6319dc6e3..da5987908 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests_tools.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests_tools.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma index 0f75a3f2f..bc9615860 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma index 943d2cb84..63eae8657 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma index 675f14fb3..08f88acfd 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/bool.ma b/helm/software/matita/contribs/ng_assembly/num/bool.ma index a4fa2eea9..a878b98af 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bool.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bool.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma index 3549148de..859082d8e 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index a8f505a9e..bc7e6f9ce 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma index 99d1b5227..1d32793cc 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma index b0c0faf19..797ac1948 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma index 7d2c418cf..ccfbdd73c 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/oct.ma b/helm/software/matita/contribs/ng_assembly/num/oct.ma index 4d6a99596..479a1ca82 100755 --- a/helm/software/matita/contribs/ng_assembly/num/oct.ma +++ b/helm/software/matita/contribs/ng_assembly/num/oct.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma index 2aca1babc..6f651b842 100755 --- a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern.ma b/helm/software/matita/contribs/ng_assembly/num/quatern.ma index 02a94e6ff..af321ea1d 100755 --- a/helm/software/matita/contribs/ng_assembly/num/quatern.ma +++ b/helm/software/matita/contribs/ng_assembly/num/quatern.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma index 49b70b81a..8d3bdf5d3 100755 --- a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma index 1d06fb2d1..e0c59bab3 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma index 3e53841ae..4570f3291 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma index 4fd80d63b..81c0af595 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) diff --git a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma index d7f6cc558..98639a642 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma @@ -15,8 +15,8 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) -- 2.39.2