Ignore:
Timestamp:
Aug 3, 2011, 1:04:49 PM (10 years ago)
Author:
campbell
Message:

Checkpoint labels work on branch again.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed

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

    r1096 r1097  
    746746definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l.
    747747
     748let rec labels_defined (s:statement) : list ident ≝
     749match s with
     750[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
     751| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
     752| Swhile _ s ⇒ labels_defined s
     753| Sdowhile _ s ⇒ labels_defined s
     754| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
     755| Sswitch _ ls ⇒ labels_defined_switch ls
     756| Slabel l s ⇒ l::(labels_defined s)
     757| Scost _ s ⇒ labels_defined s
     758| _ ⇒ [ ]
     759]
     760and labels_defined_switch (ls:labeled_statements) : list ident ≝
     761match ls with
     762[ LSdefault s ⇒ labels_defined s
     763| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
     764].
     765
     766definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
     767
     768axiom MissingLabel : String.
     769
     770definition lookup_label ≝
     771λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
     772
     773definition labels_translated : lenv → statement → stmt → Prop ≝
     774λlbls,s,s'.  ∀l.
     775  (Exists ? (λl'.l' = l) (labels_defined s)) →
     776  ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'.
     777
    748778definition stmt_inv ≝
    749779λvars. λlbls:lenv.
    … …  
    794824] qed.
    795825
    796 axiom MissingLabel : String.
    797 
    798 definition lookup_label ≝
    799 λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
    800 
    801826lemma lookup_label_hit : ∀lbls,l,l'.
    802827  lookup_label lbls l = OK ? l' →
    … …  
    806831qed.
    807832
    808 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.stmt_inv vars lbls s) ≝
    809 match s with
     833definition trans_inv : var_types → lenv → statement → stmt → Prop ≝
     834λvars,lbls,s,s'. stmt_inv vars lbls s' ∧ labels_translated lbls s s'.
     835
     836lemma trans_inv_stmt_inv : ∀vars,lbls,s,s'.
     837  trans_inv vars lbls s s' → stmt_inv vars lbls s'.
     838#var #lbls #s #s' * //
     839qed.
     840
     841lemma trans_inv_labels : ∀vars,lbls,s,s'.
     842  trans_inv vars lbls s s' → labels_translated lbls s s'.
     843#vars #lbls #s #s' @proj2
     844qed.
     845
     846lemma Exists_append : ∀A,P,l1,l2.
     847  Exists A P (l1@l2) →
     848  Exists A P l1 ∨ Exists A P l2.
     849#A #P #l1 elim l1
     850[ #l2 #H %2 @H
     851| #h #t #IH #l2 whd in ⊢ (% → ?) *
     852  [ #H %1 %1 @H
     853  | #H cases (IH l2 H) /4/
     854  ]
     855] qed.
     856
     857lemma Exists_append_l : ∀A,P,l1,l2.
     858  Exists A P l1 → Exists A P (l1@l2).
     859#A #P #l1 #l2 elim l1
     860[ *
     861| #h #t #IH *
     862  [ #H %1 @H
     863  | #H %2 @IH @H
     864  ]
     865] qed.
     866
     867lemma Exists_append_r : ∀A,P,l1,l2.
     868  Exists A P l2 → Exists A P (l1@l2).
     869#A #P #l1 #l2 elim l1
     870[ #H @H
     871| #h #t #IH #H %2 @IH @H
     872] qed.
     873
     874
     875let 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') ≝
     876match s return λs.res (Σs':stmt.trans_inv vars lbls s s') with
    810877[ Sskip ⇒ OK ? «St_skip, ?»
    811878| Sassign e1 e2 ⇒
    … …  
    897964    OK ? «St_cost l s1', ?»
    898965].
    899 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
     966try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
    900967try @I
     968try @(trans_inv_stmt_inv ???? (sig_ok ? (λs.trans_inv ??? s) …))
    901969try @(sig_ok ? (λs.stmt_inv ?? s))
    902970try @(sig_ok ? (λe.expr_vars ? e ?))
    … …  
    906974try @(sig_ok ? (local_id vars))
    907975try @(lookup_label_hit … E)
    908 [ @(sig_ok ?? s')
     976[ 1,3,5,6,7,13,14,15,16,18: whd #l *
     977| @(sig_ok ?? s')
    909978| @p
    910 ] qed.
    911 
    912 let rec labels_defined (s:statement) : list ident ≝
    913 match s with
    914 [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    915 | Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
    916 | Swhile _ s ⇒ labels_defined s
    917 | Sdowhile _ s ⇒ labels_defined s
    918 | Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
    919 | Sswitch _ ls ⇒ labels_defined_switch ls
    920 | Slabel l s ⇒ l::(labels_defined s)
    921 | Scost _ s ⇒ labels_defined s
    922 | _ ⇒ [ ]
    923 ]
    924 and labels_defined_switch (ls:labeled_statements) : list ident ≝
    925 match ls with
    926 [ LSdefault s ⇒ labels_defined s
    927 | LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
    928 ].
    929 
    930 lemma OK_sig_eq : ∀A,P,x,xp,y,yp. OK (Σx:A.P x) «x,xp» = OK (Σx:A.P x) «y,yp» → x = y.
    931 #A #P #x #xp #y #yp #E destruct @refl
    932 qed.
    933 
    934 definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
    935 
    936 lemma Exists_append : ∀A,P,l1,l2.
    937   Exists A P (l1@l2) →
    938   Exists A P l1 ∨ Exists A P l2.
    939 #A #P #l1 elim l1
    940 [ #l2 #H %2 @H
    941 | #h #t #IH #l2 whd in ⊢ (% → ?) *
    942   [ #H %1 %1 @H
    943   | #H cases (IH l2 H) /4/
    944   ]
    945 ] qed.
    946 
    947 lemma Exists_append_l : ∀A,P,l1,l2.
    948   Exists A P l1 → Exists A P (l1@l2).
    949 #A #P #l1 #l2 elim l1
    950 [ *
    951 | #h #t #IH *
    952   [ #H %1 @H
    953   | #H %2 @IH @H
    954   ]
    955 ] qed.
    956 
    957 lemma Exists_append_r : ∀A,P,l1,l2.
    958   Exists A P l2 → Exists A P (l1@l2).
    959 #A #P #l1 #l2 elim l1
    960 [ #H @H
    961 | #h #t #IH #H %2 @IH @H
    962 ] qed.
    963 
    964 lemma reflmatch : ∀A,B,e.∀P:∀v:A. e = OK ? v → res B.∀x.
    965  match e return λx.e = x → ? with [ OK v ⇒ P v | Error m ⇒ λ_.Error ? m ] (refl ? e) = OK ? x →
    966  ∃v,p. P v p = OK ? x.
    967 #A #B *
    968 [ #v #P #x normalize #H %{v} % [ @refl | @H ]
    969 | #m #P #x normalize #H destruct
    970 ] qed.
    971 
    972 lemma labels_translated : ∀vars,lbls,tmp,tmpp,s,l,s',p.
    973   (Exists ? (λl'.l' = l) (labels_defined s)) →
    974   translate_statement vars lbls tmp tmpp s = OK ? «s', p» →
    975   ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'.
    976 #vars #lbls #tmp #tmpp #s #l @(statement_ind … s) (* FIXME: once switch is done we'll need something else here *)
    977 [ #s' #p *
    978 | #e1 #e2 #s' #p *
    979 | #eo #e #args #s' #p *
    980 | #s1 #s2 #IH1 #IH2 #s' #p #H #E
    981   cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
    982   cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
    983   <(OK_sig_eq ?????? E) -E;
    984   cases (Exists_append ???? H)
    985   [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
    986   | #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @L2 ]
    987   ]
    988 | #e #s1 #s2 #IH1 #IH2 #s' #p #H #E
    989   (* Carefully get rid of the equality that will screw up the case analysis *)
    990   cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
    991   [ #sz #sg #e' #E
    992     cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
    993     cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
    994     <(OK_sig_eq ?????? E) -E;
    995     cases (Exists_append ???? H)
    996     [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
    997     | #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @L2 ]
    998     ]
    999   | *: #x #e' normalize #E destruct
    1000   ]
    1001 | #e #s #IH #s' #p #H #E
    1002   (* Carefully get rid of the equality that will screw up the case analysis *)
    1003   cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
    1004   [ #sz #sg #e' #E
    1005     cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
    1006     <(OK_sig_eq ?????? E) -E;
    1007     cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La | whd; normalize in ⊢ (???%) >append_nil @Lb ]
    1008   | *: #x #e' normalize #E destruct
    1009   ]
    1010 | #e #s #IH #s' #p #H #E
    1011   (* Carefully get rid of the equality that will screw up the case analysis *)
    1012   cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
    1013   [ #sz #sg #e' #E
    1014     cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
    1015     <(OK_sig_eq ?????? E) -E;
    1016     cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La | whd; normalize in ⊢ (???%) >append_nil @Lb ]
    1017   | *: #x #e' normalize #E destruct
    1018   ]
    1019 | #s1 #e #s1 #s2 #IH1 #IH2 #IH3 #s' #p #H #E
    1020   (* Carefully get rid of the equality that will screw up the case analysis *)
    1021   cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
    1022   [ #sz #sg #e' #E
    1023     cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
    1024     cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
    1025     cases (bind_inversion ????? E) * #s3' #I3 * #E3 -E #E
    1026     <(OK_sig_eq ?????? E) -E;
    1027     cases (Exists_append ???? H)
    1028     [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
    1029     | -H #H cases (Exists_append ???? H)
    1030       [ #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @Exists_append_l @Exists_append_r @L2 ]
    1031       | #H3 cases (IH3 s3' I3 H3 E3) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @Exists_append_l @Exists_append_l @L2 ]
    1032       ]
    1033     ]
    1034   | *: #x #e' normalize #E destruct
    1035   ]
    1036 | #s' #p *
    1037 | #s' #p *
    1038 | #eo #s' #p *
    1039 | #e #ls #IH #s' #p #H #E whd in E:(??%?); destruct (* FIXME once switch is implemented ... *)
    1040 | #l0 #s0 #IH #s' #p #H
    1041   whd in ⊢ (??%? → ?) #E cases (reflmatch ????? E) -E #l1 * #El #E
    1042   cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
    1043   <(OK_sig_eq ?????? E) -E;
    1044   cases H
    1045   [ #El' %{l1} <El' % [ @El | %1 @refl ]
    1046   | #H1 cases (IH s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | %2 @L2 ]
    1047   ]
    1048 | #l0 #s' #p *
    1049 | #l0 #s0 #IH #s' #p #H #E
    1050   cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
    1051   <(OK_sig_eq ?????? E) -E;
    1052   @(IH s1' I1 H E1)
    1053 ] qed.
     979| #l #H cases (Exists_append … H)
     980  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
     981    %{l'} % [ @E1 | @Exists_append_l @D1 ]
     982  | #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
     983    %{l'} % [ @E2 | @Exists_append_r @D2 ]
     984  ]
     985| #l #H cases (Exists_append … H)
     986  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
     987    %{l'} % [ @E1 | @Exists_append_l @D1 ]
     988  | #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
     989    %{l'} % [ @E2 | @Exists_append_r @D2 ]
     990  ]
     991| cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1
     992  %{l'} % [ @E1 | @Exists_append_l @D1 ]
     993| cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1
     994  %{l'} % [ @E1 | @Exists_append_l @D1 ]
     995| #l #H cases (Exists_append … H)
     996  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
     997    %{l'} % [ @E1 | @Exists_append_l @D1 ]
     998  | #H cases (Exists_append … H)
     999    [ #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
     1000      %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ]
     1001    | #H3 cases s3' #s3' * #S3 #L3 cases (L3 l H3) #l' * #E3 #D3
     1002      %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ]
     1003    ]
     1004  ]
     1005| cases s1' #s1' * #S1 #L1 #l0 *
     1006  [ #El <El %{l'} >E % [ @refl | %1 @refl ]
     1007  | #H cases (L1 l0 H) #l0' * #E1 #D1
     1008    %{l0'} % [ @E1 | %2 @D1 ]
     1009  ]
     1010| cases s1' #s1' * #S1 #L1 @L1
     1011] qed.
     1012
    10541013
    10551014axiom ParamGlobalMixup : String.
    10561015
    1057 definition alloc_params : ∀vars:var_types.∀ls. list (ident×type) → (Σs:stmt. stmt_inv vars ls s) → res (Σs:stmt.stmt_inv vars ls s) ≝
    1058 λvars,ls,params,s. foldl ?? (λs,it.
     1016(* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
     1017definition 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) ≝
     1018λvars,ls,s0,params,s. foldl ?? (λs,it.
    10591019  let 〈id,ty〉 ≝ it in
    10601020  do s ← s;
    … …  
    10741034try @I
    10751035[ whd >E @I
    1076 | @(sig_ok … s)
     1036| @(trans_inv_stmt_inv … s0) @(sig_ok … s)
     1037| cases s #s * #S #L @L
    10771038] qed.
    10781039
    … …  
    11211082] qed.
    11221083
     1084definition lenv_inv : lenv → lenv → statement → Prop ≝
     1085λlbls0,lbls,s. (∀l. Exists ? (λl'. l' = l) (labels_defined s) → ∃lm. lookup_label lbls l = OK ? lm) ∧
     1086  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
     1087
     1088definition lenv_inv_switch : lenv → lenv → labeled_statements → Prop ≝
     1089λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) (labels_defined_switch ls) → ∃lm. lookup_label lbls l = OK ? lm) ∧
     1090  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
     1091
     1092axiom DuplicateLabel : String.
     1093(*
    11231094(* We only record labels from Slabel, not Sgoto, so that we detect badly formed
    1124    programs. *)
    1125 let rec extend_label_env (s:statement) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝
    1126 match s with
    1127 [ Ssequence s1 s2 ⇒
    1128     let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
    1129     extend_label_env s2 lbls u
     1095   programs.  The gratutitous let-in expansion is so that Russell generated
     1096   nice hypotheses for us. *)
     1097let rec extend_label_env (s:statement) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) ≝
     1098match s return λs.res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) with
     1099[ Ssequence s1 s2 ⇒
     1100    do lu1 ← extend_label_env s1 lu0;
     1101    do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»
    11301102| Sifthenelse _ s1 s2 ⇒
    1131     let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
    1132     extend_label_env s2 lbls u
    1133 | Swhile _ s ⇒ extend_label_env s lbls u
    1134 | Sdowhile _ s ⇒ extend_label_env s lbls u
     1103    do lu1 ← extend_label_env s1 lu0;
     1104    do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»
     1105| Swhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
     1106| Sdowhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
    11351107| Sfor s1 _ s2 s3 ⇒
    1136     let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
    1137     let 〈lbls,u〉 ≝ extend_label_env s2 lbls u in
    1138     extend_label_env s3 lbls u
    1139 | Sswitch _ ls ⇒ extend_label_env' ls lbls u
     1108    do lu1 ← extend_label_env s1 lu0;
     1109    do lu2 ← extend_label_env s2 lu1;
     1110    do lu3 ← extend_label_env s3 lu2; OK ? «eject … lu3, ?»
     1111| Sswitch _ ls ⇒ do lu ← extend_label_env' ls lu0; OK ? «eject … lu, ?»
    11401112| Slabel l s ⇒
    1141     let 〈l',u〉 ≝ fresh ? u in
    1142     extend_label_env s (add … lbls l l') u
    1143 | Scost _ s ⇒ extend_label_env s lbls u
    1144 | _ ⇒ 〈lbls,u〉
     1113    let 〈lbls, u〉 ≝ lu0 in
     1114    match lookup_label lbls l with
     1115    [ OK _ ⇒ Error ? (msg DuplicateLabel)
     1116    | Error _ ⇒
     1117        let 〈l',u〉 ≝ fresh ? u in
     1118        do lu ← extend_label_env s 〈add … lbls l l', u〉; OK ? «eject … lu, ?»
     1119    ]
     1120| Scost _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
     1121| _ ⇒ OK ? «lu0, ?»
    11451122]
    1146 and extend_label_env' (ls:labeled_statements) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝
    1147 match ls with
    1148 [ LSdefault s ⇒ extend_label_env s lbls u
     1123and extend_label_env' (ls:labeled_statements) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) ≝
     1124match ls return λls.res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) with
     1125[ LSdefault s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
    11491126| LScase _ _ s ls ⇒
    1150     let 〈lbls,u〉 ≝ extend_label_env s lbls u in
    1151     extend_label_env' ls lbls u
    1152 ].
     1127    do lu1 ← extend_label_env s lu0;
     1128    do lu2 ← extend_label_env' ls lu1; OK ? «eject … lu2, ?»
     1129]. @conj
     1130[ 1,3,5,17,19,21,27: #l *
     1131| 2,4,6,18,20,22,28: #l #l' #H @H
     1132| cases lu1 in lu2 ⊢ % * #lbls1 #u1 * #I1 #E1 * * #lbls2 #u2 * #I2 #E2 whd in E2:(∀_.∀_.??(?%?)? → ?) ⊢ (∀_.? → ??(λ_.??(?%?)?))
     1133  #l #H cases (Exists_append … H)
     1134  [ #H1 cases (I1 l H1) #l' #L1 %{l'} @E2 @L1
     1135  | #H2 cases (I2 l H2) #l' #L2 %{l'} @L2
     1136  ]
    11531137
    11541138definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?).
     1139*)
     1140
     1141definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
     1142λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) ls → ∃lm. lookup_label lbls l = OK ? lm) ∧
     1143  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
     1144
     1145lemma lookup_label_add : ∀lbls,l,l'.
     1146  lookup_label (add … lbls l l') l = OK ? l'.
     1147#lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl
     1148qed.
     1149
     1150lemma lookup_label_new : ∀lbls,l,l',msg,l0,l0'.
     1151  lookup_label lbls l = Error ? msg →
     1152  lookup_label lbls l0 = OK ? l0' →
     1153  lookup_label (add … lbls l l') l0 = OK ? l0'.
     1154#lbls #l #l' #msg #l0 #l0' #E1 #E2
     1155whd in ⊢ (??%%)
     1156>lookup_add_miss
     1157[ @E2 | @(eq_identifier_elim ?? l0 l) // #E >E in E2 >E1 #X destruct ]
     1158qed. 
     1159
     1160let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝
     1161match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with
     1162[ nil ⇒ OK ? «lbls, ?»
     1163| cons l t ⇒
     1164    match lookup_label lbls l return λx.lookup_label lbls l = x → ? with
     1165    [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel)
     1166    | Error _ ⇒ λLOOK.
     1167        let 〈l',u1〉 ≝ fresh … u in
     1168        do lbls1 ← populate_lenv t (add … lbls l l') u1;
     1169        OK ? «eject … lbls1, ?»
     1170    ] (refl ? (lookup_label lbls l))
     1171]. @conj
     1172[  #l *
     1173| #l #l' #H @H
     1174| cases lbls1 #lbls' * #E1 #E2 whd in ⊢ (∀_.?→??(λ_.??(?%?)?)) #l0 *
     1175  [ #E <E %{l'} @E2 @lookup_label_add
     1176  | @E1
     1177  ]
     1178| cases lbls1 #lbls' * #E1 #E2 #l1 #l2 #L whd in ⊢ (??(?%?)?)
     1179  @E2 @(lookup_label_new … LOOK L)
     1180] qed.
     1181
     1182definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l.Exists ? (λl'.l' = l) (labels_defined body) → ∃l'.lookup_label lbls l = OK ? l') ≝
     1183λbody.
     1184  do lbls ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
     1185  OK ? «eject … lbls, ?».
     1186cases lbls #lbls * #E1 #E2 @E1
     1187qed.
     1188
     1189notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
     1190  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
    11551191
    11561192(* FIXME: the temporary handling is nonsense, I'm afraid. *)
    11571193definition translate_function : list (ident×region) → function → res internal_function ≝
    11581194λglobals, f.
    1159   let 〈lbls, label_universe〉 ≝ build_label_env (fn_body f) in
     1195  do «lbls, Ilbls» ← build_label_env (fn_body f);
    11601196  let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in
    11611197  let tmp ≝ bigid1 in (* FIXME *)
    11621198  let tmpp ≝ bigid2 in (* FIXME *)
    11631199  let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in
    1164   do s as E1 ← translate_statement vartypes lbls tmp tmpp (fn_body f);
    1165   do s as E2 ← alloc_params vartypes lbls (fn_params f) s;
     1200  do s ← translate_statement vartypes lbls tmp tmpp (fn_body f);
     1201  do «s,Is» ← alloc_params vartypes lbls ? (fn_params f) s;
    11661202  OK ? (mk_internal_function
    11671203    (opttyp_of_type (fn_return f))
    … …  
    11701206    stacksize
    11711207    s ?).
    1172 [ whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
     1208[ cases Is #S #L
     1209  @(stmt_P_mp ???? S)
     1210  #s1 * #H1 #H2 %
     1211  [ @(stmt_vars_mp … H1)
     1212    #i #H cases (identifier_eq ? tmp i)
     1213    [ #E <E @Exists_mid @refl
     1214    | #NE1 @Exists_rm cases (identifier_eq ? tmpp i)
     1215      [ #E <E @Exists_mid @refl
     1216      | #NE2 @Exists_rm
     1217        >map_append
     1218        @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
     1219                         @(local_id_add_miss ?? Local ? NE1)
     1220                         @(local_id_add_miss ?? Local ? NE2) @H
     1221                    | skip
     1222                    | * #id #ty #E1 <E1 @refl
     1223                    ]
     1224      ]
     1225    ]
     1226  | @(stmt_labels_mp … H2)
     1227    #l * #l' #LOOKUP
     1228   
     1229     generalize in ⊢ (???(?(???(????%))))
     1230    * #S #L
     1231| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
    11731232| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
    1174 | @(stmt_P_mp ???? (sig_ok ?? s))
    1175   #s1 * #H1 #H2 % [ 2: @H2 ]
    1176   @stmt_vars_mp [ 3: @sig_ok | skip ]
    1177   #i #H cases (identifier_eq ? tmp i)
    1178   [ #E <E @Exists_mid @refl
    1179   | #NE1 @Exists_rm cases (identifier_eq ? tmpp i)
    1180     [ #E <E @Exists_mid @refl
    1181     | #NE2 @Exists_rm
    1182       >map_append
    1183       @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
    1184                        @(local_id_add_miss ?? Local ? NE1)
    1185                        @(local_id_add_miss ?? Local ? NE2) @H
    1186                   | skip
    1187                   | * #id #ty #E1 <E1 @refl
    1188                   ]
    1189     ]
    1190   ]
     1233
    11911234] qed.
    11921235

  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    r1096 r1097  
    129129] qed.
    130130
     131lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
     132#P #Q #H #s elim s normalize /2/ qed.
     133
    131134(* Get labels from a Cminor statement. *)
    132135let rec labels_of (s:stmt) : list (identifier Label) ≝
Note: See TracChangeset for help on using the changeset viewer.