Ignore:
Timestamp:
Nov 16, 2012, 6:41:49 PM (7 years ago)
Author:
campbell
Message:

Tame global environments a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2468 r2471  
    444444    ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block.
    445445    find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b;
    446 
    447   find_symbol_exists:
    448     ∀F,V: Type[0]. ∀p: program F V.
    449            ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V.
    450     in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) →
    451     ∃b. find_symbol ? (globalenv ?? p) id = Some ? b;
     446*)
     447lemma find_symbol_exists:
     448    ∀F,V. ∀init. ∀p: program F V. ∀id.
     449    Exists ? (λx. x = id) (map … (λx. \fst x) (prog_funct ?? p) @ map … (λx. \fst (\fst x)) (prog_vars ?? p)) →
     450    ∃b. find_symbol ? (globalenv … init p) id = Some ? b.
     451#F #V #init * #vars #fns #main #id
     452whd in match (globalenv ????);
     453whd in match (globalenv_allocmem ????);
     454whd in match (prog_var_names ???);
     455generalize in match (F ?) in fns ⊢ %; -F #F #fns
     456#EX
     457cut (Exists ident (λx.x = id) (map … (λx.\fst (\fst x)) vars) ∨
     458     ∃b. find_symbol ? (add_functs F (empty F) fns) id = Some ? b)
     459[ cases (Exists_append … EX)
     460  [ -EX #EX %2
     461    elim fns in EX ⊢ %;
     462    [ *
     463    | * #id' #f #tl #IH *
     464      [ #E destruct
     465        change with (foldr ?????) in match (add_functs F (empty F) ?);
     466        change with (lookup ????) in match (find_symbol ???);
     467        whd in match (foldr ?????);
     468        % [2: @lookup_add_hit | skip ]
     469      | #TL
     470        change with (foldr ?????) in match (add_functs F (empty F) ?);
     471        change with (lookup ????) in match (find_symbol ???);
     472        whd in match (foldr ?????);
     473        cases (identifier_eq ? id id')
     474        [ #E destruct
     475          % [2: @lookup_add_hit | skip ]
     476        | #NE >lookup_add_miss //
     477          whd in match (drop_fn ???);
     478          >lookup_remove_miss // @IH @TL
     479        ]
     480      ]
     481    ]
     482  | #EX %1 @EX
     483  ]
     484]
     485-EX
     486generalize in match (add_functs F (empty F) fns);
     487generalize in match empty_mem;
     488elim vars
     489[ #m #ge * [ * | // ]
     490| * * #id' #r' #v' #tl #IH #m #ge *
     491  [ *
     492    [ #E destruct
     493      (* Found one, but it might be shadowed later *)
     494      whd in match (foldl ?????); normalize nodelta
     495      cases (alloc ????) #m' #b normalize nodelta
     496      cut (find_symbol F (add_symbol F id b ge) id = Some ? b)
     497      [ change with (lookup ????) in ⊢ (??%?);
     498        whd in match add_symbol; normalize nodelta
     499        @lookup_add_hit ]
     500      #F @IH %2 %{b} @F
     501    | #TL whd in match (foldl ?????); normalize nodelta
     502      cases (alloc ????) #m' #b'
     503      @IH %1 @TL
     504    ]
     505  | #H whd in match (foldl ?????); normalize nodelta
     506    cases (alloc ????) #m' #b' normalize nodelta
     507    @IH %2
     508    cases (identifier_eq ? id id')
     509    [ #E destruct %{b'}
     510      whd in match add_symbol; normalize nodelta
     511      @lookup_add_hit
     512    | #NE cases H #b #H' %{b}
     513      whd in match add_symbol; normalize nodelta
     514      change with (lookup ???? = ?) >lookup_add_miss //
     515      whd in match (drop_fn ???); >lookup_remove_miss // @H'
     516    ]
     517  ]
     518] qed.
     519
     520(*
    452521  find_funct_ptr_exists:
    453522    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F.
Note: See TracChangeset for help on using the changeset viewer.