-
-(* *********************** *)
-(* PASSO 1 DI COMPILAZIONE *)
-(* *********************** *)
-
-(*
- PREAST_VAR_ID: aux_str_type → preast_var
- PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
- PREAST_VAR_STRUCT: ne_list preast_var → nat → preast_var.
-*)
-let rec evaluate_var_type (preast:preast_var) (e:aux_env_type) on preast : option (Prod bool ast_type) ≝
- match preast with
- [ PREAST_VAR_ID name ⇒
- opt_map ?? (get_desc_env_aux e (None ?) name)
- (λdesc.Some ? (pair ?? (get_const_desc desc) (get_type_desc desc)))
- | PREAST_VAR_ARRAY subVar expr ⇒
- opt_map ?? (evaluate_var_type subVar e)
- (λcDesc.match snd ?? cDesc with
- [ AST_TYPE_ARRAY subType dim ⇒ Some ? (pair ?? (fst ?? cDesc) subType)
- | _ ⇒ None ? ])
- | PREAST_VAR_STRUCT subVar field ⇒
- opt_map ?? (evaluate_var_type subVar e)
- (λcDesc.match snd ?? cDesc with
- [ AST_TYPE_STRUCT nelSubType ⇒
- opt_map ?? (nth_neList ? nelSubType field)
- (λsubType.Some ? (pair ?? (fst ?? cDesc) subType))
- | _ ⇒ None ? ])
- ].
-
-(*
- 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_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
-*)
-let rec evaluate_expr_type (preast:preast_expr) (e:aux_env_type) on preast : option ast_base_type ≝
- match preast with
- [ PREAST_EXPR_BYTE8 _ ⇒ Some ? AST_BASE_TYPE_BYTE8
- | PREAST_EXPR_WORD16 _ ⇒ Some ? AST_BASE_TYPE_WORD16
- | PREAST_EXPR_WORD32 _ ⇒ Some ? AST_BASE_TYPE_WORD32
- | PREAST_EXPR_NEG subExpr ⇒ evaluate_expr_type subExpr e
- | PREAST_EXPR_NOT subExpr ⇒ evaluate_expr_type subExpr e
- | PREAST_EXPR_COM subExpr ⇒ evaluate_expr_type subExpr e
- | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
- | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
- | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
- | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
- | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t2 AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
- | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t2 AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
- | PREAST_EXPR_GT subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
- | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
- | PREAST_EXPR_LT subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
- | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
- | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
- | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
- opt_map ?? (evaluate_expr_type subExpr1 e)
- (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
- (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
- | PREAST_EXPR_B8toW16 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? AST_BASE_TYPE_WORD16 | false ⇒ None ? ])
- | PREAST_EXPR_B8toW32 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? AST_BASE_TYPE_WORD32 | false ⇒ None ? ])
- | PREAST_EXPR_W16toB8 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD16 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ])
- | PREAST_EXPR_W16toW32 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD16 with [ true ⇒ Some ? AST_BASE_TYPE_WORD32 | false ⇒ None ? ])
- | PREAST_EXPR_W32toB8 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD32 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ])
- | PREAST_EXPR_W32toW16 subExpr ⇒
- opt_map ?? (evaluate_expr_type subExpr e)
- (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD32 with [ true ⇒ Some ? AST_BASE_TYPE_WORD16 | false ⇒ None ? ])
- | PREAST_EXPR_ID var ⇒
- opt_map ?? (evaluate_var_type var e)
- (λ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).
-