X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Ftests.ma;fp=matitaB%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Ftests.ma;h=344ac7c337fb48902a48fdf8f6ef1c7e92f17500;hb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;hp=0000000000000000000000000000000000000000;hpb=f04a064bb34aabaf91dc0c48e3b08b37ecd7b0a2;p=helm.git

diff --git a/matitaB/matita/contribs/assembly/compiler/tests.ma b/matitaB/matita/contribs/assembly/compiler/tests.ma
new file mode 100755
index 000000000..344ac7c33
--- /dev/null
+++ b/matitaB/matita/contribs/assembly/compiler/tests.ma
@@ -0,0 +1,229 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                                                                        *)
+(* Sviluppato da:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "compiler/ast_to_astfe.ma".
+include "compiler/preast_to_ast.ma".
+
+definition parsingResult \def
+ (PREAST_ROOT
+  (PREAST_CONST_DECL
+   ([ch_n;ch_1])
+   (AST_TYPE_ARRAY
+    (AST_TYPE_STRUCT
+     (\laquo
+      (AST_TYPE_ARRAY
+       (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+       1
+      )
+      ;
+      (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+      £
+      (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+     \raquo)
+    )
+    1
+   )
+   (PREAST_INIT_VAL
+    (PREAST_INIT_VAL_ARRAY
+     (\laquo
+      (PREAST_INIT_VAL_STRUCT
+       (\laquo
+        (PREAST_INIT_VAL_ARRAY
+         (\laquo
+          (PREAST_INIT_VAL_BYTE8 (\langle x0,x0 \rangle))
+          £
+          (PREAST_INIT_VAL_BYTE8 (\langle x0,x1 \rangle))
+         \raquo)
+        )
+        ;
+        (PREAST_INIT_VAL_WORD16 (\langle \langle x0,x0 \rangle : \langle x0,x0 \rangle \rangle))
+        £
+        (PREAST_INIT_VAL_WORD32 (\langle \langle \langle x0,x0 \rangle : \langle x0,x0 \rangle \rangle . \langle \langle x0,x0 \rangle : \langle x0,x0 \rangle \rangle \rangle))
+       \raquo)
+      )
+      £
+      (PREAST_INIT_VAL_STRUCT
+       (\laquo
+        (PREAST_INIT_VAL_ARRAY
+         (\laquo
+          (PREAST_INIT_VAL_BYTE8 (\langle x0,x2 \rangle))
+          £
+          (PREAST_INIT_VAL_BYTE8 (\langle x0,x3 \rangle))
+         \raquo)
+        )
+        ;
+        (PREAST_INIT_VAL_WORD16 (\langle \langle x0,x0 \rangle : \langle x0,x1 \rangle \rangle))
+        £
+        (PREAST_INIT_VAL_WORD32 (\langle \langle \langle x0,x0 \rangle : \langle x0,x0 \rangle \rangle . \langle \langle x0,x0 \rangle : \langle x0,x1 \rangle \rangle \rangle))
+       \raquo)
+      )
+     \raquo)
+    )
+   )
+   (PREAST_VAR_DECL
+    ([ch_n;ch_2])
+    (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+    (Some ?
+     (PREAST_INIT_VAR
+      (PREAST_VAR_STRUCT
+       (PREAST_VAR_ARRAY
+        (PREAST_VAR_ID ([ch_n;ch_1]))
+        (PREAST_EXPR_BYTE8 (\langle x0,x0 \rangle))
+       )
+       1
+      )
+     )
+    )
+    (PREAST_VAR_DECL
+     ([ch_n;ch_3])
+     (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+     (None ?)
+     (PREAST_NO_DECL
+      [
+       (PREAST_STM_WHILE
+        (PREAST_EXPR_ID
+         (PREAST_VAR_ID ([ch_n;ch_2]))
+        )
+        (PREAST_VAR_DECL
+         ([ch_n;ch_1])
+         (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+         (Some ?
+          (PREAST_INIT_VAR
+           (PREAST_VAR_STRUCT
+            (PREAST_VAR_ARRAY
+             (PREAST_VAR_ID ([ch_n;ch_1]))
+             (PREAST_EXPR_ID
+              (PREAST_VAR_ID ([ch_n;ch_2]))
+             )
+            )
+            2
+           )
+          )
+         )
+         (PREAST_NO_DECL
+          [
+           (PREAST_STM_IF
+            (\laquo
+             £
+             (pair ??
+              (PREAST_EXPR_GT
+               (PREAST_EXPR_ID
+                (PREAST_VAR_ID ([ch_n;ch_1]))
+               )
+               (PREAST_EXPR_WORD32 (\langle \langle \langle x1,x2 \rangle : \langle x3,x4 \rangle \rangle . \langle \langle xA,xB \rangle : \langle xC,xD \rangle \rangle \rangle))
+              )
+              (PREAST_NO_DECL
+               [
+                (PREAST_STM_ASG
+                 (PREAST_VAR_ID ([ch_n;ch_3]))
+                 (PREAST_EXPR_NEG
+                  (PREAST_EXPR_NOT
+                   (PREAST_EXPR_COM
+                    (PREAST_EXPR_OR
+                     (PREAST_EXPR_AND
+                      (PREAST_EXPR_SHR
+                       (PREAST_EXPR_SUB
+                        (PREAST_EXPR_ADD
+                         (PREAST_EXPR_W32toB8
+                          (PREAST_EXPR_W16toW32
+                           (PREAST_EXPR_B8toW16
+                            (PREAST_EXPR_ID
+                             (PREAST_VAR_ID ([ch_n;ch_3]))
+                            )
+                           )
+                          )
+                         )
+                         (PREAST_EXPR_BYTE8 (\langle x0,x1 \rangle))
+                        )
+                        (PREAST_EXPR_DIV
+                         (PREAST_EXPR_MUL
+                          (PREAST_EXPR_BYTE8 (\langle x0,x2 \rangle))
+                          (PREAST_EXPR_BYTE8 (\langle x0,x3 \rangle))
+                         )
+                         (PREAST_EXPR_BYTE8 (\langle x0,x4 \rangle))
+                        )
+                       )
+                       (PREAST_EXPR_SHL
+                        (PREAST_EXPR_BYTE8 (\langle x0,x5 \rangle))
+                        (PREAST_EXPR_BYTE8 (\langle x0,x6 \rangle))
+                       )
+                      )
+                      (PREAST_EXPR_BYTE8 (\langle x0,x7 \rangle))
+                     )
+                     (PREAST_EXPR_XOR
+                      (PREAST_EXPR_BYTE8 (\langle x0,x8 \rangle))
+                      (PREAST_EXPR_BYTE8 (\langle x0,x9 \rangle))
+                     )
+                    )
+                   )
+                  )
+                 )
+                )
+               ]
+              )
+             )
+            \raquo)
+            (None ?)
+           )
+           ;
+           (PREAST_STM_ASG
+            (PREAST_VAR_ID ([ch_n;ch_2]))
+            (PREAST_EXPR_ADD
+             (PREAST_EXPR_ID
+              (PREAST_VAR_ID ([ch_n;ch_2]))
+             )
+             (PREAST_EXPR_WORD16 (\langle \langle x0,x0 \rangle : \langle x0,x1 \rangle \rangle))
+            )
+           )
+          ]
+         )
+        )
+       )
+       ;
+       (PREAST_STM_ASG
+        (PREAST_VAR_ID ([ch_n;ch_3]))
+        (PREAST_EXPR_ID
+         (PREAST_VAR_ARRAY
+          (PREAST_VAR_STRUCT
+           (PREAST_VAR_ARRAY
+            (PREAST_VAR_ID ([ch_n;ch_1]))
+            (PREAST_EXPR_BYTE8 (\langle x0,x1 \rangle))
+           )
+           O
+          )
+          (PREAST_EXPR_BYTE8 (\langle x0,x0 \rangle))
+         )
+        )
+       )
+      ]
+     )
+    )
+   )
+  )
+ ).
+
+lemma pippo : ∃b.preast_to_ast parsingResult = Some ? b.
+ normalize;
+ exists;
+ [ apply (match preast_to_ast parsingResult with [ None ⇒ AST_ROOT (AST_NO_DECL O empty_env []) | Some x ⇒ x]);
+ | reflexivity
+ ]
+qed.