Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
13 edited
9 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/Clight/Cexec.ma

    r1153 r1311  
    499499axiom MainMissing : String.
    500500
    501 let rec make_initial_state (p:clight_program) : res (genv × state) ≝
    502   do ge ← globalenv Genv ?? (fst ??) p;
     501definition make_global : clight_program → genv ≝
     502λp. globalenv Genv ?? (fst ??) p.
     503
     504let rec make_initial_state (p:clight_program) : res state ≝
     505  let ge ≝ make_global p in
    503506  do m0 ← init_mem Genv ?? (fst ??) p;
    504507  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    505508  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    506   OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
     509  OK ? (Callstate f (nil ?) Kstop m0).
    507510
    508511let rec is_final (s:state) : option int ≝
     
    558561λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    559562
    560 definition clight_exec : execstep io_out io_in ≝
    561   mk_execstep … is_final mem_of_state exec_step.
     563definition clight_exec : trans_system io_out io_in ≝
     564  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
    562565
    563566definition clight_fullexec : fullexec io_out io_in ≝
    564   mk_fullexec ?? clight_exec ? make_initial_state.
     567  mk_fullexec ??? clight_exec make_global make_initial_state.
  • Deliverables/D3.3/id-lookup-branch/Clight/CexecComplete.ma

    r1058 r1311  
    8181
    8282theorem the_initial_state:
    83   ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉.
    84 #p #s cases p; #fns #main #globs #H
     83  ∀p,s. initial_state p s → yields ? (make_initial_state p) s.
     84#p #s cases p; #globs #fns #main #H
    8585inversion H;
    86 #b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge}
    87 whd in ⊢ (??%?);
    88 >e1
     86#b #f #ge #m #e1 #e2 #e3 #e4 #e5
    8987whd in ⊢ (??%?);
    9088>e2
    9189whd in ⊢ (??%?);
     90change in e1:(??%?) with (make_global (mk_program ?? globs fns main))
     91>e1
    9292>e3
    9393whd in ⊢ (??%?);
  • Deliverables/D3.3/id-lookup-branch/Clight/CexecEquiv.ma

    r961 r1311  
    1313
    1414coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
    15 | seo_stop : ∀tr,r,m. single_exec_of (e_stop ??? tr r m) (se_stop tr r m)
     15| seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r (mem_of_state s))
    1616| seo_step : ∀tr,s,e,se.
    1717    single_exec_of e se →
     
    5959] qed.
    6060
    61 lemma is_final_elim': ∀s.∀P:option int → Type[0].
     61lemma is_final_elim': ∀ge,s.∀P:option int → Type[0].
    6262 (∀r. final_state s r → P (Some ? r)) →
    6363 ((¬∃r.final_state s r) → P (None ?)) →
    64 P (is_final io_out io_in clight_fullexec s).
    65 @is_final_elim qed.
     64P (is_final io_out io_in clight_fullexec ge s).
     65#ge @is_final_elim qed.
    6666
    6767lemma exec_e_step: ∀ge,x,tr,s,e.
     
    300300
    301301
    302 lemma e_stop_inv: ∀ge,x,tr,r,m.
    303   exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r m
    304   x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop m〉.
    305 #ge #x #tr #r #m
     302lemma e_stop_inv: ∀ge,x,tr,r,s.
     303  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r s
     304  x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop (mem_of_state s)〉.
     305#ge #x #tr #r #s
    306306>(exec_inf_aux_unfold …) cases x;
    307307[ #o #k #EXEC whd in EXEC:(??%?); destruct;
     
    684684  single_exec_of e1 e2 →
    685685  match e1 with
    686   [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
     686  [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ mem_of_state s = m' | _ ⇒ False ]
    687687  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
    688688  | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ]
     
    691691#e01 #e02 #H
    692692cases H;
    693 [ #tr #r #m whd; % [ % ] //
     693[ #tr #r #s whd; % [ % ] //
    694694| #tr #s #e1' #e2' #H' whd; % [ % ] //
    695695| #msg whd; //
     
    10211021whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?)
    10221022cases (make_initial_state p)
    1023 [ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    1024     cases INITIAL; #Ege #INITIAL''
     1023[ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    10251024    >exec_inf_aux_unfold
    10261025    whd in ⊢ (?%? → ?)
    10271026    @is_final_elim'
    10281027    [ #r #F @False_ind
    1029         @(absurd ?? (initial_state_not_final … INITIAL''))
     1028        @(absurd ?? (initial_state_not_final … INITIAL))
    10301029        %{r} @F
    10311030    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
     
    10331032        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
    10341033    lapply (behavior_of_execution ??
    1035               (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
     1034              (execution_characterisation_complete classic constructive_indefinite_description ? s ? EXEC'));
    10361035        *; #b #MATCHES %{b} % [ @MATCHES ]
    1037         #ge' >Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ]
     1036        #ge #Ege
    10381037        inversion MATCHES;
    10391038        [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM
     
    10421041            >E1 in TERM #TERM
    10431042            @(program_terminates (mk_transrel … step) ?? ge s)
    1044             [ 2: @INITIAL''
    1045             | 3: @(terminates_sound … TERM EXEC')
     1043            [ 2: @INITIAL
     1044            | 3: <Ege @(terminates_sound … TERM EXEC')
    10461045            | skip
    10471046            | //;
     
    10551054            #E7 <E7 in INITSTEPS #INITSTEPS
    10561055            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV
    1057             @(program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR)
    1058             @(silent_sound … DIVERGING EXECDIV)
     1056            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL)
     1057            [ 2: <Ege @INITSTAR
     1058            | 3: <Ege @(silent_sound … DIVERGING EXECDIV)
     1059            ]
    10591060        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS
    10601061            lapply (exec_state_reacts … REACTS);
     
    10641065            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
    10651066            #E7 <E7 in REACTING #REACTING
    1066             @(program_reacts (mk_transrel … step) ?? ge s … INITIAL'')
    1067             @(reacts_sound … REACTING EXEC')
     1067            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL)
     1068            <Ege @(reacts_sound … REACTING EXEC')
    10681069        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG
    10691070            lapply (exec_state_wrong … WRONG);
     
    10741075            #E8 <E8 in GOESWRONG #GOESWRONG
    10751076            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
    1076             @(program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP)
     1077            <Ege
     1078            @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP)
    10771079            #r % #F @(absurd ?? FINAL) %{r} @F
    10781080        | #msg #E destruct (E);
  • Deliverables/D3.3/id-lookup-branch/Clight/CexecSound.ma

    r1153 r1311  
    533533qed.
    534534
    535 lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? (fst ??) p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
     535lemma make_initial_state_sound : ∀p. P_res ? (initial_state p) (make_initial_state p).
    536536#p cases p; #fns #main #vars
    537537whd in ⊢ (???%);
    538 @bind_OK #ge #Ege
    539538@bind_OK #m #Em
    540539@opt_bind_OK #x cases x; #sp #b #esb
    541540@opt_bind_OK #f #ef
    542 whd; % [ whd in ⊢ (???(??%)) // | @(initial_state_intro … Ege Em esb ef) ]
     541@(initial_state_intro … Em esb ef) @refl
    543542qed.
    544543
  • Deliverables/D3.3/id-lookup-branch/Clight/Csem.ma

    r1153 r1311  
    12111211inductive initial_state (p: clight_program): state -> Prop :=
    12121212  | initial_state_intro: ∀b,f,ge,m0.
    1213       globalenv Genv ?? (fst ??) p = OK ? ge →
     1213      globalenv Genv ?? (fst ??) p = ge →
    12141214      init_mem Genv ?? (fst ??) p = OK ? m0 →
    12151215      find_symbol ?? ge (prog_main ?? p) = Some ? b →
     
    12291229
    12301230definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1231   ∀ge. globalenv ??? (fst ??) p = OK ? ge →
     1231  ∀ge. globalenv ??? (fst ??) p = ge →
    12321232  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    12331233 
  • Deliverables/D3.3/id-lookup-branch/Clight/Csyntax.ma

    r1153 r1311  
    318318  data.  See module [AST] for more details. *)
    319319
    320 definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type).
     320definition clight_program : Type[0] ≝ program (λ_.clight_fundef) (list init_data × type).
    321321
    322322(* * * Operations over types *)
  • Deliverables/D3.3/id-lookup-branch/Clight/TypeComparison.ma

    r891 r1311  
    9191definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
    9292λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? (msg TypeMismatch)].
     93
     94definition type_eq : type → type → bool ≝
     95λt1,t2. match type_eq_dec t1 t2 with [ inl _ ⇒ true | inr _ ⇒ false ].
     96
  • Deliverables/D3.3/id-lookup-branch/Clight/clightPrintMatita.ml

    r1197 r1311  
    466466  collect_program prog;
    467467  fprintf p "include \"Clight/Cexec.ma\".@\ninclude \"common/Animation.ma\".@\n@\n";
    468   fprintf p "@[<v 2>definition myprog := mk_program clight_fundef ((list init_data) × type)@ ";
     468  fprintf p "@[<v 2>definition myprog := mk_program (\\lambda _. clight_fundef) ((list init_data) × type)@ ";
    469469(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
    470470  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
     471  print_list print_globvar p prog.prog_vars;
    471472  print_list print_fundef p prog.prog_funct;
    472473  fprintf p "@\n(ident_of_nat %i)@\n" (id_i "main");
    473   print_list print_globvar p prog.prog_vars;
    474   fprintf p "@;<0 -2>.@]@\n@\n";
     474  fprintf p "@;<0 -2>.@]@\n@\n(*@\n";
    475475  fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).@\n";
    476   fprintf p "normalize  (* you can examine the result here *)@."
     476  fprintf p "normalize  (* you can examine the result here *)@\n";
     477  fprintf p "*)@."
    477478
    478479let print_program prog =
  • Deliverables/D3.3/id-lookup-branch/Clight/label.ma

    r1056 r1311  
    187187
    188188definition clight_label : clight_program → res clight_program ≝
    189   transform_partial_program ??? label_fundef.
     189 λp. transform_partial_program … p label_fundef.
  • Deliverables/D3.3/id-lookup-branch/Clight/test/search.c.ma

    r1153 r1311  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef ((list init_data) × type)
     4definition myprog := mk_program (λ_.clight_fundef) ((list init_data) × type)
     5  []
    56  [〈ident_of_nat 0 (* search *), CL_Internal (
    67     mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
     
    181182  )〉]
    182183  (ident_of_nat 7)
    183   []
    184184.
    185185
     
    192192include "Cminor/semantics.ma".
    193193
     194example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
     195(*
    194196example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     197*)
    195198normalize
    196199@refl
     
    202205example e2: finishes_with (repr 3) ? (
    203206do p1 ← clight_to_cminor myprog;
     207bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2.
     208 exec_up_to RTLabs_fullexec p2 1000 [ ])).
     209(*
     210example e2: finishes_with (repr 3) ? (
     211do p1 ← clight_to_cminor myprog;
    204212do p2 ← cminor_to_rtlabs p1;
    205  exec_up_to RTLabs_fullexec p2 1000 [ ]).
     213 exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
    206214normalize
    207215@refl
  • Deliverables/D3.3/id-lookup-branch/Clight/test/sum.c.ma

    r1153 r1311  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef (list init_data × type)
    5   [〈ident_of_nat 0 (* main *), CL_Internal (
    6      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [〈〈ident_of_nat 0 (* src *), Any〉,
     6     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
     7        (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
     8        (Init_int8 (repr I8 4)) ], (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     9  [〈ident_of_nat 1 (* main *), CL_Internal (
     10     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    711       (Ssequence
    8        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     12       (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    913         (Expr (Ecast (Tint I8 Unsigned )
    1014           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1115           (Tint I8 Unsigned )))
    1216       (Ssequence
    13        (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     17       (Sfor (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    1418               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1519         (Expr (Ebinop Olt
    1620           (Expr (Ecast (Tint I32 Unsigned)
    17              (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
     21             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    1822             (Tint I32 Unsigned))
    1923           (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
    2024             (Tint I32 Unsigned))) (Tint I32 Signed  ))
    21          (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     25         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    2226           (Expr (Ebinop Oadd
    23              (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     27             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    2428             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2529             (Tint I32 Signed  )))
    26          (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     30         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    2731           (Expr (Ecast (Tint I8 Unsigned )
    2832             (Expr (Ebinop Oadd
    2933               (Expr (Ecast (Tint I32 Signed  )
    30                  (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     34                 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    3135                 (Tint I32 Signed  ))
    3236               (Expr (Ecast (Tint I32 Signed  )
    3337                 (Expr (Ederef
    3438                   (Expr (Ebinop Oadd
    35                      (Expr (Evar (ident_of_nat 3))
     39                     (Expr (Evar (ident_of_nat 0))
    3640                       (Tarray Any (Tint I8 Unsigned ) 5))
    37                      (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
     41                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    3842                     (Tpointer Any (Tint I8 Unsigned ))))
    3943                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     
    4145       )
    4246       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    43                              (Expr (Evar (ident_of_nat 2))
     47                             (Expr (Evar (ident_of_nat 3))
    4448                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
    4549     
     
    4751     
    4852   )〉]
    49   (ident_of_nat 0)
    50   [〈〈ident_of_nat 3 (* src *), Any〉,
    51      〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
    52      (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
    53      (Init_int8 (repr I8 4)) ],
    54      (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     53  (ident_of_nat 1)
     54 
    5555.
    5656
    57 example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     57(*
     58example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    5859normalize  (* you can examine the result here *)
    59 @refl
    60 qed.
    61 
    62 include "Clight/toCminor.ma".
    63 include "Cminor/semantics.ma".
    64 
    65 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
    66 normalize
    67 @refl
    68 qed.
    69 
    70 include "Cminor/toRTLabs.ma".
    71 include "RTLabs/semantics.ma".
    72 
    73 example e2: finishes_with (repr I32 74) ? (
    74 do p1 ← clight_to_cminor myprog;
    75 do p2 ← cminor_to_rtlabs p1;
    76  exec_up_to RTLabs_fullexec p2 1000 [ ]).
    77 normalize
    78 @refl
    79 qed.
     60*)
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    r1197 r1311  
    694694axiom FIXME : String.
    695695
     696record tmpgen : Type[0] ≝ {
     697  tmp_universe : universe SymbolTag;
     698  tmp_env : list (ident × typ)
     699}.
     700
     701definition alloc_tmp : memory_chunk → tmpgen → ident × tmpgen ≝
     702λc,g.
     703  let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in
     704  〈tmp, mk_tmpgen u (〈tmp, typ_of_memory_chunk c〉::(tmp_env g))〉.
     705
    696706lemma lookup_label_hit : ∀lbls,l,l'.
    697707  lookup_label lbls l = OK ? l' →
     
    700710qed.
    701711
    702 definition trans_inv : var_types → lenv → statement → stmt → Prop ≝
    703 λvars,lbls,s,s'. stmt_inv vars lbls s' ∧ labels_translated lbls s s'.
    704 
    705 lemma trans_inv_stmt_inv : ∀vars,lbls,s,s'.
    706   trans_inv vars lbls s s' → stmt_inv vars lbls s'.
    707 #var #lbls #s #s' * //
     712definition add_tmps : var_types → tmpgen → var_types ≝
     713λvs,g.
     714  foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g).
     715
     716definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝
     717λvars,u1,u2.
     718  ∀id. local_id (add_tmps vars u1) id → local_id (add_tmps vars u2) id.
     719
     720lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q.
     721  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
     722#tmp #g #g' #vars #q
     723whd in ⊢ (???% → ?)
     724generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
     725* #tmp' #u whd in ⊢ (???% → ?) #E
     726>(pair_eq2 ?????? E)
     727#id #H
     728whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
     729cases (identifier_eq ? id tmp')
     730[ #E1 >E1 >lookup_add_hit @I
     731| * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E1 cases (NE E1)
     732] qed.
     733
     734definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝
     735λvars,lbls,s,u,su'.
     736  let 〈s',u'〉 ≝ su' in
     737  stmt_inv (add_tmps vars u') lbls s' ∧
     738  labels_translated lbls s s' ∧
     739  tmps_preserved vars u u'.
     740
     741lemma trans_inv_stmt_inv : ∀vars,lbls,s,u,su.
     742  trans_inv vars lbls s u su → stmt_inv (add_tmps vars (\snd su)) lbls (\fst su).
     743#var #lbls #s #u * #s' #u' * * #H1 #H2 #H3 @H1
    708744qed.
    709745
    710 lemma trans_inv_labels : ∀vars,lbls,s,s'.
    711   trans_inv vars lbls s s' → labels_translated lbls s s'.
    712 #vars #lbls #s #s' @proj2
     746lemma trans_inv_labels : ∀vars,lbls,s,u,su.
     747  trans_inv vars lbls s u su → labels_translated lbls s (\fst su).
     748#vars #lbls #s #u * #s' #u' * * #_ #H #_ @H
    713749qed.
    714750
    715 
    716 let rec translate_statement (vars:var_types) (lbls:lenv) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs':stmt.trans_inv vars lbls s s') ≝
    717 match s return λs.res (Σs':stmt.trans_inv vars lbls s s') with
    718 [ Sskip ⇒ OK ? «St_skip, ?»
     751lemma local_id_add_local_oblivious : ∀vars,id,id'.
     752  local_id vars id → local_id (add ?? vars id' Local) id.
     753#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     754cases (identifier_eq ? id id')
     755[ #E >E >lookup_add_hit @I
     756| * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E cases (NE E)
     757] qed.
     758
     759lemma local_id_add_tmps_oblivious : ∀vars,id,u.
     760  local_id vars id → local_id (add_tmps vars u) id.
     761#vars #id * #u #l #H elim l
     762[ //
     763| * #id' #ty #tl @local_id_add_local_oblivious
     764] qed.
     765
     766lemma add_tmps_oblivious : ∀vars,lbls,s,u.
     767  stmt_inv vars lbls s → stmt_inv (add_tmps vars u) lbls s.
     768#vars #lbls #s #u #H
     769@(stmt_P_mp … H)
     770#s' * #H1 #H2 %
     771[ @(stmt_vars_mp … H1)
     772  #id @local_id_add_tmps_oblivious
     773| @H2
     774] qed.
     775
     776lemma local_id_fresh_tmp : ∀tmp,u,q,u0,vars.
     777  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
     778#tmp #u #q #u0 #vars
     779whd in ⊢ (???% → ?)
     780generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
     781* #tmp' #u' whd in ⊢ (???% → ?) #E
     782>(pair_eq1 ?????? E) >(pair_eq2 ?????? E)
     783whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
     784@I
     785qed.
     786
     787lemma use_sig' : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' x.
     788#A #P #P' #H1 * #x #H2 @H1 @H2
     789qed.
     790
     791definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝
     792λA,B,C,P,e,f.
     793  match e with
     794  [ OK v ⇒ match v with [ dp v' p ⇒ match v' return λv'. P v' → res C with [ pair a b ⇒ f a b ] p ]
     795  | Error msg ⇒ Error ? msg
     796  ].
     797
     798notation > "vbox('do' 〈ident v1, ident v2〉 'with' ident H ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
     799(*
     800notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
     801notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     802notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
     803*)
     804interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).
     805
     806let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝
     807match s return λs.res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) with
     808[ Sskip ⇒ OK ? «〈St_skip, u〉, ?»
    719809| Sassign e1 e2 ⇒
    720810    do s' ← translate_assign vars e1 e2;
    721     OK ? «eject ?? s', ?»
     811    OK ? «〈eject ?? s', u〉, ?»
    722812| Scall ret ef args ⇒
    723813    do ef' ← translate_expr vars ef;
     
    725815    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
    726816    match ret with
    727     [ None ⇒ OK ? «St_call (None ?) ef' args', ?»
     817    [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?»
    728818    | Some e1 ⇒
    729819        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
    730820        match dest with
    731         [ IdDest id p ⇒ OK ? «St_call (Some ? id) ef' args', ?»
     821        [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?»
    732822        | MemDest r q e1' ⇒
    733             let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
    734             OK ? «St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), ?»
     823            let 〈tmp, u〉 as Etmp ≝ alloc_tmp q u in
     824            OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?»
    735825        ]
    736826    ]
    737827| Ssequence s1 s2 ⇒
    738     do s1' ← translate_statement vars lbls tmp tmpp s1;
    739     do s2' ← translate_statement vars lbls tmp tmpp s2;
    740     OK ? «St_seq s1' s2', ?»
     828    do 〈s1', u1〉 with H1 ← translate_statement vars lbls u s1;
     829    do 〈s2', u2〉 with H2 ← translate_statement vars lbls u1 s2;
     830    OK ? «〈St_seq s1' s2', u2〉, ?»
    741831| Sifthenelse e1 s1 s2 ⇒
    742832    do e1' ← translate_expr vars e1;
    743833    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    744834    [ ASTint _ _ ⇒ λe1'.
    745         do s1' ← translate_statement vars lbls tmp tmpp s1;
    746         do s2' ← translate_statement vars lbls tmp tmpp s2;
    747         OK ? «St_ifthenelse ?? e1' s1' s2', ?»
     835        do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     836        do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2;
     837        OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?»
    748838    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    749839    ] e1'
     
    752842    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    753843    [ ASTint _ _ ⇒ λe1'.
    754         do s1' ← translate_statement vars lbls tmp tmpp s1;
     844        do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
    755845        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    756         OK ? «St_block
     846        OK ? «St_block
    757847               (St_loop
    758                  (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))),
     848                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉,
    759849    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    760850    ] e1'
     
    763853    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    764854    [ ASTint _ _ ⇒ λe1'.
    765         do s1' ← translate_statement vars lbls tmp tmpp s1;
     855        do 〈s1',u〉 with H1 ← translate_statement vars lbls u s1;
    766856        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    767         OK ? «St_block
     857        OK ? «St_block
    768858               (St_loop
    769                  (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))),
     859                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉,
    770860    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    771861    ] e1'
     
    774864    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    775865    [ ASTint _ _ ⇒ λe1'.
    776         do s1' ← translate_statement vars lbls tmp tmpp s1;
    777         do s2' ← translate_statement vars lbls tmp tmpp s2;
    778         do s3' ← translate_statement vars lbls tmp tmpp s3;
     866        do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     867        do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2;
     868        do 〈s3', u〉 with H3 ← translate_statement vars lbls u s3;
    779869        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    780         OK ? «St_seq s1'
     870        OK ? «St_seq s1'
    781871             (St_block
    782872               (St_loop
    783                  (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))),
     873                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉,
    784874    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    785875    ] e1'
    786 | Sbreak ⇒ OK ? «St_exit 1, ?»
    787 | Scontinue ⇒ OK ? «St_exit 0, ?»
     876| Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?»
     877| Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?»
    788878| Sreturn ret ⇒
    789879    match ret with
    790     [ None ⇒ OK ? «St_return (None ?), ?»
     880    [ None ⇒ OK ? «〈St_return (None ?), u〉, ?»
    791881    | Some e1 ⇒
    792882        do e1' ← translate_expr vars e1;
    793         OK ? «St_return (Some ? (dp … e1')), ?»
     883        OK ? «〈St_return (Some ? (dp … e1')), u〉, ?»
    794884    ]
    795885| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    796886| Slabel l s1 ⇒
    797887    do l' as E ← lookup_label lbls l;
    798     do s1' ← translate_statement vars lbls tmp tmpp s1;
    799     OK ? «St_label l' s1', ?»
     888    do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     889    OK ? «〈St_label l' s1', u〉, ?»
    800890| Sgoto l ⇒
    801891    do l' as E ← lookup_label lbls l;
    802     OK ? «St_goto l', ?»
     892    OK ? «〈St_goto l', u〉, ?»
    803893| Scost l s1 ⇒
    804     do s1' ← translate_statement vars lbls tmp tmpp s1;
    805     OK ? «St_cost l s1', ?»
    806 ].
    807 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
     894    do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     895    OK ? «〈St_cost l s1', u〉, ?»
     896].
     897try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
    808898try @I
    809 try @(trans_inv_stmt_inv ???? (use_sig ? (λs.trans_inv ??? s) …))
    810 try @(use_sig ? (λs.stmt_inv ?? s))
    811 try @(use_sig ? (λe.expr_vars ? e ?))
    812 try @(use_sig ? (λs.stmt_vars ?? s))
    813 try @(use_sig ? (λs.stmt_labels ?? s))
    814 try @(use_sig ? (All ??))
    815 try @(use_sig ? (local_id vars))
    816 try @(lookup_label_hit … E)
    817 [ 1,3,5,6,7,13,14,15,16,18: whd #l *
    818 | @(use_sig ?? s')
    819 | @p
     899try (#l #H @(match H in False with [ ]))
     900try (#id #H @H)
     901[ @add_tmps_oblivious @(use_sig ?? s')
     902| @local_id_add_tmps_oblivious @p
     903]
     904try (@use_sig' #x @expr_vars_mp #i @local_id_add_tmps_oblivious)
     905[ 1,3,6: @use_sig' #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious
     906| 2,4: @(local_id_fresh_tmp … Etmp)
     907| @(alloc_tmp_preserves … Etmp)
     908| 7,11: @(stmt_P_mp … (π1 (π1 H1))) #s * #H3 #H4 % [ 1,3: @(stmt_vars_mp … H3) cases H2 #_ #H @H | *: @H4 ]
     909| 8,12: @(trans_inv_stmt_inv … H2)
     910| 9,13: #l #H cases (Exists_append … H)
     911  [ 1,3: #H3 cases H1 * #S1 #L1 #T1 cases (L1 l H3) #l' * #E1 #D1
     912    %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
     913  | *: #H3 cases H2 * #S2 #L2 #T2 cases (L2 l H3) #l' * #E2 #D2
     914    %{l'} % [ 1,3: @E2 | *: @Exists_append_r @D2 ]
     915  ]
     916| 10,14: cases H2 #_ #TP2 #id #L @TP2 cases H1 #_ #TP1 @TP1 @L
     917| 15,18: @(π1 (π1 H1))
     918| 16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1
     919  %{l'} % [ 1,3: @E1 | *: @Exists_append_l @D1 ]
     920| 17,20: @(π2 H1)
     921(* Sfor *)
     922| @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @(π2 H2) @H | @H5 ]
     923| @(π1 (π1 H3))
     924| @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #H @(π2 H3) @H | @H5 ]
    820925| #l #H cases (Exists_append … H)
    821   [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
     926  [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1
    822927    %{l'} % [ @E1 | @Exists_append_l @D1 ]
    823   | #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
    824     %{l'} % [ @E2 | @Exists_append_r @D2 ]
    825   ]
    826 | #l #H cases (Exists_append … H)
    827   [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
    828     %{l'} % [ @E1 | @Exists_append_l @D1 ]
    829   | #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
    830     %{l'} % [ @E2 | @Exists_append_r @D2 ]
    831   ]
    832 | cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1
    833   %{l'} % [ @E1 | @Exists_append_l @D1 ]
    834 | cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1
    835   %{l'} % [ @E1 | @Exists_append_l @D1 ]
    836 | #l #H cases (Exists_append … H)
    837   [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
    838     %{l'} % [ @E1 | @Exists_append_l @D1 ]
    839   | #H cases (Exists_append … H)
    840     [ #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
     928  | #EX cases (Exists_append … EX)
     929    [ #EX2 cases H2 * #S2 #L2 #_ cases (L2 l EX2) #l' * #E2 #D2
    841930      %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ]
    842     | #H3 cases s3' #s3' * #S3 #L3 cases (L3 l H3) #l' * #E3 #D3
     931    | #EX3 cases H3 * #S3 #L3 #_ cases (L3 l EX3) #l' * #E3 #D3
    843932      %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ]
    844933    ]
    845934  ]
    846 | cases s1' #s1' * #S1 #L1 #l0 *
    847   [ #El <El %{l'} >E % [ @refl | %1 @refl ]
    848   | #H cases (L1 l0 H) #l0' * #E1 #D1
    849     %{l0'} % [ @E1 | %2 @D1 ]
    850   ]
    851 | cases s1' #s1' * #S1 #L1 @L1
     935| #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H
     936(* Slabel *)
     937| %{l} @E
     938| @(π1 (π1 H1))
     939| #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
     940| @(π2 H1)
     941(* Sgoto *)
     942| %{l} @E
     943| @(π1 (π1 H1))
     944(* Scost *)
     945| @(π2 (π1 H1))
     946| @(π2 H1)
    852947] qed.
    853948
     
    856951
    857952(* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
    858 definition alloc_params : ∀vars:var_types.∀ls,s0. list (ident×type) → (Σs:stmt. trans_inv vars ls s0 s) → res (Σs:stmt.trans_inv vars ls s0 s) ≝
    859 λvars,ls,s0,params,s. foldl ?? (λs,it.
     953definition alloc_params : ∀vars:var_types.∀ls,s0,u. list (ident×type) → (Σsu:stmt×tmpgen. trans_inv vars ls s0 u su) → res (Σsu:stmt×tmpgen.trans_inv vars ls s0 u su) ≝
     954λvars,ls,s0,u,params,s. foldl ?? (λsu,it.
    860955  let 〈id,ty〉 ≝ it in
    861   do s ← s;
     956  do 〈s,u〉 with Is ← su;
    862957  do t as E ← lookup' vars id;
    863958  match t return λx.? → ? with
    864   [ Local ⇒ λE. OK (Σs:stmt.?) s
     959  [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is»
    865960  | Stack n ⇒ λE.
    866961      do q ← match access_mode ty with
     
    869964      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    870965      ];
    871       OK ? «St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, ?»
     966      OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, u〉, ?»
    872967  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    873968  ] E) (OK ? s) params.
    874 try @conj try @conj try @conj try @conj try @conj
     969try @conj try @conj try @conj try @conj try @conj try @conj
    875970try @I
    876 [ whd >E @I
    877 | @(trans_inv_stmt_inv … s0) @(use_sig … s)
    878 | cases s #s * #S #L @L
    879 ] qed.
    880 
    881 definition bigid1 ≝ an_identifier SymbolTag [[
    882 false;true;false;false;
    883 false;false;false;false;
    884 false;false;false;false;
    885 false;false;false;false]].
    886 definition bigid2 ≝ an_identifier SymbolTag [[
    887 false;true;false;false;
    888 false;false;false;false;
    889 false;false;false;false;
    890 false;false;false;true]].
    891 
     971[ @(expr_vars_mp … (λid. local_id_add_tmps_oblivious vars id u)) whd >E @I
     972| @(π1 (π1 Is))
     973| @(π2 (π1 Is))
     974| @(π2 Is)
     975] qed.
     976
     977(*
    892978lemma local_id_add_local : ∀vars,id,id'.
    893979  local_id vars id →
     
    898984| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
    899985] qed.
    900 
     986*)
    901987axiom DuplicateLabel : String.
    902988
     
    9551041qed.
    9561042
    957 (* FIXME: the temporary handling is nonsense, I'm afraid. *)
    958 definition translate_function : list (ident×region) → function → res internal_function ≝
    959 λglobals, f.
     1043lemma local_id_split : ∀vars,tmpgen,i.
     1044  local_id (add_tmps vars tmpgen) i →
     1045  local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
     1046#vars #tmpgen #i
     1047whd in ⊢ (?%? → ?)
     1048elim (tmp_env tmpgen)
     1049[ #H %1 @H
     1050| * #id #ty #tl #IH
     1051  cases (identifier_eq ? i id)
     1052  [ #E >E #H %2 whd %1 @refl
     1053  | * #NE #H cases (IH ?)
     1054    [ #H' %1 @H'
     1055    | #H' %2 %2 @H'
     1056    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
     1057      >lookup_add_miss in H; [ #H @H | @eq_identifier_elim // #E cases (NE E) ]
     1058    ]
     1059  ]
     1060] qed.
     1061
     1062lemma Exists_squeeze : ∀A,P,l1,l2,l3.
     1063  Exists A P (l1@l3) → Exists A P (l1@l2@l3).
     1064#A #P #l1 #l2 #l3 #EX
     1065cases (Exists_append … EX)
     1066[ #EX1 @Exists_append_l @EX1
     1067| #EX3 @Exists_append_r @Exists_append_r @EX3
     1068] qed.
     1069
     1070definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝
     1071λtmpuniverse, globals, f.
    9601072  do «lbls, Ilbls» ← build_label_env (fn_body f);
    961   let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in
    962   let tmp ≝ bigid1 in (* FIXME *)
    963   let tmpp ≝ bigid2 in (* FIXME *)
    964   let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in
    965   do s ← translate_statement vartypes lbls tmp tmpp (fn_body f);
    966   do «s,Is» ← alloc_params vartypes lbls ? (fn_params f) s;
     1073  let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
     1074  let tmp ≝ mk_tmpgen tmpuniverse [ ] in
     1075  do s ← translate_statement vartypes lbls tmp (fn_body f);
     1076  do 〈s,tmp〉 with Is ← alloc_params vartypes lbls ?? (fn_params f) s;
    9671077  OK ? (mk_internal_function
    9681078    (opttyp_of_type (fn_return f))
    9691079    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
    970     (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
     1080    ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    9711081    stacksize
    9721082    s ?).
    973 [ cases Is #S #L
    974   @(stmt_P_mp ???? S)
    975   #s1 * #H1 #H2 %
    976   [ @(stmt_vars_mp … H1)
    977     #i #H cases (identifier_eq ? tmp i)
    978     [ #E <E @Exists_mid @refl
    979     | #NE1 @Exists_add cases (identifier_eq ? tmpp i)
    980       [ #E <E @Exists_mid @refl
    981       | #NE2 @Exists_add
    982         >map_append
    983         @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
    984                          @(local_id_add_miss ?? Local ? NE1)
    985                          @(local_id_add_miss ?? Local ? NE2) @H
    986                     | skip
    987                     | * #id #ty #E1 <E1 @refl
    988                     ]
    989       ]
    990     ]
    991   | @(stmt_labels_mp … H2)
    992     #l * #l' #LOOKUP
    993     lapply (Ilbls l' l LOOKUP) #DEFINED
    994     cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
    995     #H @H
    996   ]
    997 | whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
    998 | whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
    999 ] qed.
    1000 
    1001 definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
    1002 λglobals,f.
     1083cases Is * #S #L #TP
     1084@(stmt_P_mp ???? S)
     1085#s1 * #H1 #H2 %
     1086[ @(stmt_vars_mp … H1)
     1087  #i #H
     1088  cases (local_id_split … H)
     1089  [ #H' @Exists_squeeze >map_append
     1090    @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i) @H'
     1091                | skip
     1092                | * #id #ty #E1 <E1 @refl
     1093                ]
     1094  | #EX @Exists_append_r @Exists_append_l @EX
     1095  ]
     1096| @(stmt_labels_mp … H2)
     1097  #l * #l' #LOOKUP
     1098  lapply (Ilbls l' l LOOKUP) #DEFINED
     1099  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
     1100  #H @H
     1101] qed.
     1102
     1103definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝
     1104λtmpuniverse,globals,f.
    10031105match f with
    1004 [ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
     1106[ CL_Internal fn ⇒ do fn' ← translate_function tmpuniverse globals fn; OK ? (Internal ? fn')
    10051107| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
    10061108].
     1109
     1110(* TODO: move universe generation to higher level once we do runtime function
     1111   generation.  Cheating a bit - we only need the new identifiers to be fresh
     1112   for individual functions. *)
     1113include "Clight/fresh.ma".
    10071114
    10081115definition clight_to_cminor : clight_program → res Cminor_program ≝
    10091116λp.
     1117  let tmpuniverse ≝ universe_for_program p in
    10101118  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
    10111119  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
    10121120  let globals ≝ fun_globals @ var_globals in
    1013   transform_partial_program2 ???? (translate_fundef globals) (λi. OK ? (\fst i)) p.
     1121  transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
Note: See TracChangeset for help on using the changeset viewer.