Snapshot (not working).

diff --git a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
index b551582a3a389da4034e8b79ef955d0853a884a5..58496cb7dab15c322348a632313a12a677a865f4 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
@@ -156,6 +156,30 @@ let rec evaluate_expr_type (preast:preast_expr) (e:aux_env_type) on preast : opt
     (λcDesc.match snd ?? cDesc with [ AST_TYPE_BASE bType ⇒ Some ? bType | _ ⇒ None ? ])
   ].
 
+inductive sigma (A:Type) (P:A \to Type) : Type \def
+    sigma_intro: \forall x:A. P x \to sigma A P.
+
+notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
+  right associative with precedence 20
+for @{ 'Sigma ${default
+  @{\lambda ${ident i} : $ty. $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).
+
+
 (*
  PREAST_EXPR_BYTE8 : byte8 → preast_expr
  PREAST_EXPR_WORD16: word16 → preast_expr
@@ -183,38 +207,11 @@ let rec evaluate_expr_type (preast:preast_expr) (e:aux_env_type) on preast : opt
  PREAST_EXPR_W32toW16: preast_expr → preast_expr
  PREAST_EXPR_ID: preast_var → preast_expr
 *)
-let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) (t:ast_base_type) on preast : option (ast_expr e t) ≝
- (*match preast
-  return λpr:preast_expr.λen:aux_env_type.λtp:ast_base_type.(match pr with
-   [ PREAST_EXPR_BYTE8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_WORD16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
-   | PREAST_EXPR_WORD32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
-   | PREAST_EXPR_NEG _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_NOT _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_COM _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_ADD _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_SUB _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_MUL _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_DIV _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_SHR _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_SHL _ ⇒ option (ast_expr en tp)
-   | PREAST_EXPR_GT _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_GTE _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_LT _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_LTE _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_EQ _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_NEQ _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_B8toW16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
-   | PREAST_EXPR_B8toW32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
-   | PREAST_EXPR_W16toB8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_W16toW32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
-   | PREAST_EXPR_W32toB8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
-   | PREAST_EXPR_W32toW16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
-   | PREAST_EXPR_ID _ ⇒ option (ast_expr en tp)
-   | _ ⇒ option (ast_expr en tp)
-   ])
- with
-  [ PREAST_EXPR_BYTE8 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
+let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt:ast_base_type.ast_expr e t) ≝
+ match preast with
+  [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪AST_BASE_TYPE_BYTE8,AST_EXPR_BYTE8 e val≫
+  | _ ⇒ None ? (*
+  match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
    [ true ⇒ Some ? (AST_EXPR_BYTE8 e val) | false ⇒ None ? ]
   | PREAST_EXPR_WORD16 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
    [ true ⇒ Some ? (AST_EXPR_WORD16 e val) | false ⇒ None ? ]
@@ -316,9 +313,8 @@ let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) (t:ast_base_typ
   | PREAST_EXPR_ID var ⇒
    opt_map ?? (evaluate_var_type var e)
     (λcDesc.opt_map ?? (preast_to_ast_var var e (fst ?? cDesc) (AST_TYPE_BASE t))
-     (λres.Some ? (AST_EXPR_ID e (fst ?? cDesc) t res)))
-  ]*)
- None (ast_expr e t)
+     (λres.Some ? (AST_EXPR_ID e (fst ?? cDesc) t res)))*)
+  ]
 (*
  PREAST_VAR_ID: aux_str_type → preast_var
  PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
@@ -355,7 +351,7 @@ and preast_to_ast_var (preast:preast_var) (e:aux_env_type) (c:bool) (t:ast_type)
 *)
 and preast_to_ast_base_expr (preast:preast_expr) (e:aux_env_type) on preast : option (ast_base_expr e) ≝
  None (ast_base_expr e).
-
+ 
 (*
  PREAST_STM_ASG: preast_var → preast_expr → preast_stm
  PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm