From 7ec26dcce747c05e2f0d12940d7d92237dbe9146 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 15 Oct 2008 11:54:15 +0000 Subject: [PATCH] minor simplification + deps fixed --- .../assembly/compiler/env_to_flatenv1.ma | 22 ++++++++++++------- .../software/matita/contribs/assembly/depends | 2 ++ 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma index 8b3b2623d..f341480d7 100755 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma @@ -75,14 +75,20 @@ definition aux_map_type ≝ λd.list (map_elem d). definition empty_map ≝ nil (map_elem O). -axiom defined_nList_S_to_true : +theorem defined_nList_S_to_true : ∀d.∀l:n_list (S d).defined_nList (S d) l = True. + intros; + inversion l; + [ intros; destruct H + | intros; simplify; reflexivity + ] +qed. lemma defined_get_id : - ∀d.∀h:map_elem d.True → defined_nList (S d) (get_cur_mapElem d h). - intros 3; + ∀d.∀h:map_elem d.defined_nList (S d) (get_cur_mapElem d h). + intros 2; rewrite > (defined_nList_S_to_true ? (get_cur_mapElem d h)); - apply H. + apply I. qed. (* get_id *) @@ -90,7 +96,7 @@ let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : optio match map with [ nil ⇒ None ? | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with - [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ?? I) + [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??) | false ⇒ get_id_map_aux d t name ] ]. @@ -371,7 +377,7 @@ let rec enter_map d (map:aux_map_type d) on map ≝ (get_name_mapElem d h) (get_max_mapElem d h) (n_cons (S d) - (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ?? I)) + (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ??)) (get_cur_mapElem d h)) )::(enter_map d t) ]. @@ -422,7 +428,7 @@ let rec leave_map d (map:aux_map_type (S d)) on map ≝ (MAP_ELEM d (get_name_mapElem (S d) h) (get_max_mapElem (S d) h) - (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ?? I)) + (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ??)) )::(leave_map d t) ]. @@ -439,7 +445,7 @@ let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on match map with [ nil ⇒ [] | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with - [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ?? I))) + [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??))) | false ⇒ h ]::(new_max_map_aux d t name max) ]. diff --git a/helm/software/matita/contribs/assembly/depends b/helm/software/matita/contribs/assembly/depends index 38db65f2f..103d25a7d 100644 --- a/helm/software/matita/contribs/assembly/depends +++ b/helm/software/matita/contribs/assembly/depends @@ -9,6 +9,7 @@ freescale/extra.ma datatypes/constructors.ma list/list.ma logic/connectives.ma n freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma compiler/env_to_flatenv.ma compiler/environment.ma freescale/table_RS08.ma freescale/opcode.ma +compiler/astfe_tree1.ma compiler/ast_tree.ma compiler/ast_type.ma compiler/env_to_flatenv1.ma compiler/utility.ma freescale/word32.ma string/string.ma freescale/memory_trees.ma freescale/memory_struct.ma freescale/table_HC05_tests.ma freescale/table_HC05.ma freescale/aux_bases.ma freescale/word16.ma @@ -35,6 +36,7 @@ compiler/sigma.ma compiler/ast_to_astfe.ma compiler/astfe_tree.ma compiler/sigma.ma compiler/utility.ma freescale/extra.ma compiler/ast_type.ma compiler/utility.ma freescale/word32.ma +compiler/ast_to_astfe1.ma compiler/astfe_tree1.ma compiler/sigma.ma compiler/preast_to_ast.ma compiler/ast_tree.ma compiler/preast_tree.ma compiler/sigma.ma freescale/translation.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma freescale/byte8.ma freescale/exadecim.ma -- 2.39.2