- let rec aux (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e'))))
- (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on nel ≝
- match nel with
- [ ne_nil h ⇒
- opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
- (λtripleRes.match tripleRes with
- [ tripleT resDecl m' flatE' ⇒
- Some ? (tripleT ??? « pair ?? resExpr (ASTFE_BODY resDecl) £» (rollback_map m' (build_snapshot m)) flatE')
- ]))
- | ne_cons h tl ⇒
- opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
- (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
- (λtripleRes.match tripleRes with
- [ tripleT resDecl m' flatE' ⇒
- opt_map ?? (aux tl (rollback_map m' (build_snapshot m)) flatE')
- (λtripleRes'.match tripleRes' with
- [ tripleT tl' m'' flatE'' ⇒
- Some ? (tripleT ??? (« pair ?? resExpr (ASTFE_BODY resDecl) £»&tl') m'' flatE'')
- ])]))] in
- opt_map ?? (aux nelExprDecl map fe)
- (λtRes.match tRes with
- [ tripleT resNel resMap resFe ⇒
- match optDecl with
- [ None ⇒ Some ? (tripleT ??? (ASTFE_STM_IF resNel (None ?)) resMap resFe)
- | Some decl ⇒
- opt_map ?? (ast_to_astfe_decl (enter_env e') decl resMap resFe)
- (λtRes'.match tRes' with
- [ tripleT rDecl resMap' resFe' ⇒
- Some ? (tripleT ??? (ASTFE_STM_IF resNel (Some ? (ASTFE_BODY rDecl))) (rollback_map resMap' (build_snapshot resMap)) resFe')
- ])
- ]])
+ λmap:aux_trasfMap_type e' fe.
+ let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
+ (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
+ match nel with
+ [ ne_nil h ⇒
+ opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
+ (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
+ (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
+ [ pair m' resDecl ⇒
+ Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
+ « pair ?? (retype_base_expr fenv fenv' resExpr) (ASTFE_BODY fenv' resDecl) £»≫)
+ ]]]))
+
+ | ne_cons h tl ⇒
+ opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
+ (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
+ (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type (f (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
+ [ pair m' resDecl ⇒
+ opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
+ (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
+ [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
+ [ pair m'' tl' ⇒
+ Some ? (≪fenv'',pair ?? m''
+ (« pair ?? (retype_base_expr fenv fenv'' resExpr)
+ (ASTFE_BODY fenv'' (retype_list_decl fenv' fenv'' resDecl)) £»&tl')≫)
+ ]])]]]))
+ ] in
+ opt_map ?? (aux fe map nelExprDecl)
+ (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
+ [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
+ [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
+ [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
+ | Some decl ⇒
+ opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
+ (λsigmaRes':(Σf'.(Σfe'.Prod (aux_trasfMap_type (f' (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
+ [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+ [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type (f (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
+ [ pair (m'':aux_trasfMap_type (f (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
+ Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+ (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
+ (ASTFE_STM_IF fe'' (retype_neList_body fe' fe'' resNel) (Some ? (ASTFE_BODY fe'' resDecl)))≫)
+ ]]])]]])