Changeset 1882


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

Location:
src
Files:
3 added
25 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r1522 r1882  
    22include "common/Identifiers.ma".
    33include "common/CostLabel.ma".
     4include "common/LabelledObjects.ma".
    45
    56axiom ASMTag : String.
     
    203204  | Mov: [[dptr]] → Identifier → pseudo_instruction.
    204205
    205 definition labelled_instruction ≝ option Identifier × pseudo_instruction.
     206definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
    206207definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
    207208definition assembly_program ≝ list instruction.
  • src/ASM/Status.ma

    r1666 r1882  
    510510  λac: option Bit.
    511511  λov: Bit.
    512     let old_cy ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) O ? in
    513     let old_ac ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 1 ? in
    514     let old_fo ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 2 ? in
    515     let old_rs1 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 3 ? in
    516     let old_rs0 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 4 ? in
    517     let old_ov ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 5 ? in
    518     let old_ud ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 6 ? in
    519     let old_p ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 7 ? in
     512    let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in
     513    let old_cy ≝ get_index_v ?? sfr_psw O ? in
     514    let old_ac ≝ get_index_v ?? sfr_psw 1 ? in
     515    let old_fo ≝ get_index_v ?? sfr_psw 2 ? in
     516    let old_rs1 ≝ get_index_v ?? sfr_psw 3 ? in
     517    let old_rs0 ≝ get_index_v ?? sfr_psw 4 ? in
     518    let old_ov ≝ get_index_v ?? sfr_psw 5 ? in
     519    let old_ud ≝ get_index_v ?? sfr_psw 6 ? in
     520    let old_p ≝ get_index_v ?? sfr_psw 7 ? in
    520521    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
    521522      set_8051_sfr ?? s SFR_PSW
     
    11281129qed.
    11291130
    1130 definition instruction_matches_identifier ≝
    1131   λy: Identifier.
    1132   λx: labelled_instruction.
    1133     match \fst x with
    1134     [ None ⇒ false
    1135     | Some x ⇒ eq_identifier ? x y
    1136     ].
    1137 
    1138 let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
    1139  match l with
    1140   [ nil ⇒ true
    1141   | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
    1142 
    1143 lemma does_not_occur_None:
    1144  ∀id,i,list_instr.
    1145   does_not_occur id (list_instr@[〈None …,i〉]) =
    1146   does_not_occur id list_instr.
    1147  #id #i #list_instr elim list_instr
    1148   [ % | #hd #tl #IH whd in ⊢ (??%%); >IH %]
    1149 qed.
    1150 
    1151 lemma does_not_occur_Some:
    1152  ∀id,id',i,list_instr.
    1153   eq_identifier ? id' id = false →
    1154    does_not_occur id (list_instr@[〈Some ? id',i〉]) =
    1155     does_not_occur id list_instr.
    1156  #id #id' #i #list_instr elim list_instr
    1157   [ #H normalize in H ⊢ %; >H %
    1158   | * #x #i' #tl #IH #H whd in ⊢ (??%%); >(IH H) %]
    1159 qed.
    1160 
    1161 lemma does_not_occur_absurd:
    1162  ∀id,i,list_instr.
    1163   does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
    1164  #id #i #list_instr elim list_instr
    1165   [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
    1166     >eq_identifier_refl %
    1167   | * #x #i' #tl #IH whd in ⊢ (??%%); >IH cases (notb ?) %]
    1168 qed.
    1169 
    1170 
    1171 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
    1172  match l with
    1173   [ nil ⇒ false
    1174   | cons hd tl ⇒
    1175      if instruction_matches_identifier id hd then
    1176       does_not_occur id tl
    1177      else
    1178       occurs_exactly_once id tl ].
    1179 
    1180 lemma occurs_exactly_once_None:
    1181  ∀id,i,list_instr.
    1182   occurs_exactly_once id (list_instr@[〈None …,i〉]) =
    1183   occurs_exactly_once id list_instr.
    1184  #id #i #list_instr elim list_instr
    1185   [ % | #hd #tl #IH whd in ⊢ (??%%); >IH >does_not_occur_None %]
    1186 qed.
    1187 
    1188 lemma occurs_exactly_once_Some:
    1189  ∀id,id',i,prefix.
    1190   occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
    1191  #id #id' #i #prefix elim prefix
    1192   [ whd in ⊢ (?% → ?);
    1193     change with (eq_identifier ? id' id) in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    1194     @eq_identifier_elim normalize nodelta; /2/
    1195   | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    1196     cases he; normalize nodelta
    1197      [ #H @ (IH H)
    1198      | #x whd in ⊢ (? → ?(??%)); change with (eq_identifier ? x id) in match (instruction_matches_identifier ??);
    1199        @eq_identifier_elim #E normalize nodelta
    1200        [ destruct @eq_identifier_elim normalize nodelta;
    1201         /2/ #H >does_not_occur_Some /2/
    1202        | #H @IH @H]]]
    1203 qed.
    1204 
    1205 lemma occurs_exactly_once_Some_stronger:
    1206   ∀id,id',i,prefix.
    1207     occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
    1208     (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨
    1209     (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
    1210  #id #id' #i #prefix elim prefix
    1211  [ whd in ⊢ (?% → ?); change with (eq_identifier ???) in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?);
    1212    @eq_identifier_elim #E
    1213   [ normalize //
    1214   | normalize #H @⊥ @H 
    1215   ]
    1216  | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    1217    cases he; normalize nodelta
    1218    [ #H @ (IH H)
    1219    | #x @eq_identifier_elim #Heq
    1220      [ @eq_identifier_elim normalize nodelta
    1221        [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
    1222        | #H >(does_not_occur_Some)
    1223          [ #H2 whd in match (does_not_occur ??);
    1224            change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    1225            >Heq >eq_identifier_refl normalize nodelta
    1226            @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);
    1227            change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    1228            >eq_identifier_refl
    1229            normalize nodelta @H2 
    1230          | /2/
    1231          ]
    1232        ]
    1233      | normalize nodelta #H lapply (IH H) -IH -H;
    1234        @eq_identifier_elim #Heq2
    1235        #Hor @orb_elim
    1236        [ <Heq2 in Hor; #Hor normalize in Hor;
    1237          whd in match (does_not_occur ??); change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    1238          >eq_identifier_false // normalize nodelta
    1239          cases (does_not_occur id' tl) in Hor; normalize nodelta //
    1240        | normalize nodelta whd in match (occurs_exactly_once ??);
    1241          change with (eq_identifier ???) in match (instruction_matches_identifier ??);
    1242          >eq_identifier_false //
    1243        ]
    1244      ] 
    1245    ]
    1246  ]
    1247 qed.   
    1248 
    1249 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
    1250   match l with
    1251   [ nil ⇒ ?
    1252   | cons hd tl ⇒
    1253     if pred hd then
    1254       acc
    1255     else
    1256       index_of_internal A pred tl (S acc)
    1257   ].
    1258   cases not_implemented.
    1259 qed.
    1260 
    1261 
    1262 definition index_of ≝
    1263   λA.
    1264   λeq.
    1265   λl.
    1266     index_of_internal A eq l 0.
    1267 
    1268 lemma index_of_internal_None: ∀i,id,instr_list,n.
    1269  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    1270   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    1271    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
    1272  #i #id #instr_list elim instr_list
    1273   [ #n #abs whd in abs; cases abs
    1274   | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
    1275     cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%);
    1276     [ #H %
    1277     | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %;
    1278       [ #_ % | #abs cases abs ]]]
    1279 qed.
    1280 
    1281 lemma index_of_internal_Some_miss: ∀i,id,id'.
    1282  eq_identifier ? id' id = false →
    1283  ∀instr_list,n.
    1284  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    1285   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    1286    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
    1287  #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
    1288  change with (occurs_exactly_once ?? → ?) generalize in match n; -n -H; elim instr_list
    1289   [ #n #abs cases abs
    1290   | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
    1291     [ // | #K @IH //]]
    1292 qed.
    1293 
    1294 lemma index_of_internal_Some_hit: ∀i,id.
    1295  ∀instr_list,n.
    1296   occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
    1297    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
    1298   = |instr_list| + n.
    1299  #i #id #instr_list elim instr_list
    1300   [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
    1301   | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
    1302     [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
    1303 qed.
    1304 
    13051131definition address_of_word_labels_code_mem ≝
    1306   λcode_mem.
     1132  λcode_mem : list labelled_instruction.
    13071133  λid: Identifier.
    1308     bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
     1134    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
    13091135
    13101136lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
    1311  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     1137 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
    13121138  address_of_word_labels_code_mem instr_list id =
    13131139  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    13141140 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    1315  >(index_of_internal_None H) %
     1141 >(index_of_internal_None ?????? H) %
    13161142qed.
    13171143
    13181144lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    13191145 eq_identifier ? id' id = false →
    1320   occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
     1146  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
    13211147   address_of_word_labels_code_mem instr_list id =
    13221148   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    13231149 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    1324  >(index_of_internal_Some_miss H) [ @refl | // ]
     1150 >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
    13251151qed.
    13261152
    13271153lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
    1328   occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
     1154  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
    13291155   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    13301156   = bitvector_of_nat … (|instr_list|).
    13311157 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
    1332  >(index_of_internal_Some_hit H) <plus_n_O @refl
     1158 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
    13331159qed.
    13341160
  • src/ASM/Util.ma

    r1811 r1882  
    1212notation "⊥" with precedence 90
    1313  for @{ match ? in False with [ ] }.
     14notation "Ⓧ" with precedence 90
     15  for @{ λabs.match abs in False with [ ] }.
     16
    1417
    1518definition ltb ≝
     
    561564    foldr ? ? (append ?) [ ] l.
    562565
    563 let rec rev (A: Type[0]) (l: list A) on l ≝
    564   match l with
    565   [ nil ⇒ nil A
    566   | cons hd tl ⇒ (rev A tl) @ [ hd ]
    567   ].
     566(* redirecting to library reverse *)
     567definition rev ≝ reverse.
    568568
    569569lemma append_length:
     
    594594  elim L
    595595  [ normalize >append_nil %
    596   | #HD #TL #IH
    597     normalize >IH
     596  | #HD #TL normalize #IH
     597    >rev_append_def
     598    >rev_append_def
     599    >rev_append_def
     600    >append_nil
     601    normalize
     602    >IH
    598603    @associative_append
    599604  ]
     
    607612  elim L
    608613  [ %
    609   | #HD #TL #IH
    610     normalize
     614  | #HD #TL normalize #IH
     615    >rev_append_def
    611616    >(append_length A (rev A TL) [HD])
    612     normalize /2/
     617    normalize /2 by /
    613618  ]
    614619qed.
     
    834839coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    835840
     841lemma bool_as_Prop_to_eq : ∀b : bool. b → b = true.
     842**%
     843qed.
     844
     845(* with this you can use prf : b with b : bool with rewriting
     846   >prf rewrites b as true *)
     847coercion bool_to_Prop_to_eq : ∀b : bool.∀prf : b.b = true
     848 ≝ bool_as_Prop_to_eq on _prf : bool_to_Prop ? to (? = true).
     849
     850lemma andb_Prop : ∀b,d : bool.b → d → b∧d.
     851#b #d #btrue #dtrue >btrue >dtrue %
     852qed.
     853
     854lemma andb_Prop_true : ∀b,d : bool. (b∧d) → And (bool_to_Prop b) (bool_to_Prop d).
     855#b #d #bdtrue elim (andb_true … bdtrue) #btrue #dtrue >btrue >dtrue % %
     856qed.
     857
     858lemma orb_Prop_l : ∀b,d : bool.b → b∨d.
     859#b #d #btrue >btrue %
     860qed.
     861
     862lemma orb_Prop_r : ∀b,d : bool.d → b∨d.
     863#b #d #dtrue >dtrue elim b %
     864qed.
     865
     866lemma orb_Prop_true : ∀b,d : bool. (b∨d) → Or (bool_to_Prop b) (bool_to_Prop d).
     867#b #d #bdtrue elim (orb_true_l … bdtrue) #xtrue >xtrue [%1 | %2] %
     868qed.
     869
     870lemma notb_Prop : ∀b : bool. Not (bool_to_Prop b) → notb b.
     871* * #H [@H % | %]
     872qed.
     873
    836874lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    837  *; /2/
    838 qed.
     875 *; /2 by eq_true_false, I/
     876qed.
     877
     878lemma not_b_to_eq_false : ∀b : bool. Not (bool_to_Prop b) → b = false.
     879** #H [elim (H ?) % | %]
     880qed.
     881
     882(* with this you can use prf : ¬b with b : bool with rewriting
     883   >prf rewrites b as false *)
     884coercion not_bool_to_Prop_to_eq : ∀b : bool.∀prf : Not (bool_to_Prop b).b = false
     885 ≝ not_b_to_eq_false on _prf : Not (bool_to_Prop ?) to (? = false).
     886
     887
     888lemma true_or_false_Prop : ∀b : bool.Or (bool_to_Prop b) (¬(bool_to_Prop b)).
     889* [%1 % | %2 % *]
     890qed.
     891
     892lemma eq_true_to_b : ∀b. b = true → b.
     893#b #btrue >btrue %
     894qed.
     895
     896definition if_then_else_safe : ∀A : Type[0].∀b : bool.(b → A) → (¬(bool_to_Prop b) → A) → A ≝
     897  λA,b,f,g.
     898  match b return λx.match x with [true ⇒ bool_to_Prop b | false ⇒ ¬bool_to_Prop b] → A with
     899  [ true ⇒ f
     900  | false ⇒ g
     901  ] ?. elim b % *
     902qed.
     903
     904notation > "'If' b 'then' 'with' ident prf1 'do' f 'else' 'with' ident prf2 'do' g" with precedence 46 for
     905  @{'if_then_else_safe $b (λ${ident prf1}.$f) (λ${ident prf2}.$g)}.
     906notation > "'If' b 'then' 'with' ident prf1 : ty1 'do' f 'else' 'with' ident prf2 : ty2 'do' g" with precedence 46 for
     907  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     908notation > "'If' b 'then' f 'else' 'with' ident prf2 'do' g" with precedence 46 for
     909  @{'if_then_else_safe $b (λ_.$f) (λ${ident prf2}.$g)}.
     910notation > "'If' b 'then' f 'else' 'with' ident prf2 : ty2 'do' g" with precedence 46 for
     911  @{'if_then_else_safe $b (λ_.$f) (λ${ident prf2}:$ty2.$g)}.
     912notation > "'If' b 'then' 'with' ident prf1 'do' f 'else' g" with precedence 46 for
     913  @{'if_then_else_safe $b (λ${ident prf1}.$f) (λ_.$g)}.
     914notation > "'If' b 'then' 'with' ident prf1 : ty1 'do' f 'else' g" with precedence 46 for
     915  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ_.$g)}.
     916
     917notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break 'with' \nbsp ident prf1 : ty1 \nbsp 'do' \nbsp break f \nbsp break 'else' \nbsp break 'with' \nbsp ident prf2 : ty2 \nbsp 'do' \nbsp break g)" with precedence 46 for
     918  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     919notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break f \nbsp break 'else' \nbsp break 'with' \nbsp ident prf2 : ty2 \nbsp 'do' \nbsp break g)" with precedence 46 for
     920  @{'if_then_else_safe $b (λ_:$ty1.$f) (λ${ident prf2}:$ty2.$g)}.
     921notation < "hvbox('If' \nbsp b \nbsp 'then' \nbsp break 'with' \nbsp ident prf1 : ty1 \nbsp 'do' \nbsp break f \nbsp break 'else' \nbsp break g)" with precedence 46 for
     922  @{'if_then_else_safe $b (λ${ident prf1}:$ty1.$f) (λ_:$ty2.$g)}.
     923 
     924interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g).
    839925
    840926lemma length_append:
  • src/RTL/RTL_paolo.ma

    r1644 r1882  
    1616  on _n : nat to rtl_argument.
    1717
    18 (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
    19   are not sequential. Thus there is a dummy label at the moment in the code.
    20   To be fixed once we understand exactly what to do with tail calls. *)
    21 inductive rtl_instruction_extension: Type[0] ≝
    22   | rtl_st_ext_stack_address: register → register → rtl_instruction_extension
    23   | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_instruction_extension.
     18inductive rtl_step_extension: Type[0] ≝
     19  | rtl_st_ext_stack_address: register → register → rtl_step_extension
     20  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_step_extension.
    2421
    2522inductive rtl_statement_extension : Type[0] ≝
     
    2825
    2926definition rtl_uns_params ≝ mk_unserialized_params
    30   (mk_inst_params
     27  (mk_step_params
    3128    (* acc_a_reg ≝ *) register
    3229    (* acc_b_reg ≝ *) register
     
    4138    (* call_args ≝ *) (list rtl_argument)
    4239    (* call_dest ≝ *) (list register)
    43     (* ext_instruction ≝ *) rtl_instruction_extension
    44     (* ext_forall_labels ≝ *) (λP.λes.True)
    45     (* ext_fin_instruction ≝ *) rtl_statement_extension
    46     (* ext_fin_forall_labels ≝ *) (λP.λes.True))
     40    (* ext_step ≝ *) rtl_step_extension
     41    (* ext_step_labels ≝ *) (λes.[ ])
     42    (* ext_fin_stmt ≝ *) rtl_statement_extension
     43    (* ext_fin_stmt_labels ≝ *) (λes.[ ]))
    4744  (mk_local_params
    4845    (mk_funct_params
     
    5350definition rtl_params ≝ mk_graph_params rtl_uns_params.
    5451definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
     52definition rtl_internal_function ≝
     53  λglobals. joint_internal_function globals rtl_params.
     54definition rtl_program ≝ joint_program rtl_params.
     55definition rtl_step ≝ joint_step rtl_params.
     56definition rtl_statement ≝ joint_statement rtl_params.
    5557
    56 interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
     58
     59interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
    5760
    5861(* aid unification *)
     
    9598call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
    9699
    97 
    98 definition rtl_instruction ≝ joint_instruction rtl_params.
    99100unification hint 0 ≔
    100101(*---------------*) ⊢
    101 ext_instruction (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_instruction_extension.
     102ext_step (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_step_extension.
    102103unification hint 0 ≔ globals
    103104(*---------------*) ⊢
    104 joint_instruction (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_instruction globals.
     105joint_step (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_step globals.
    105106
    106 definition rtl_statement ≝ joint_statement rtl_params.
    107107unification hint 0 ≔
    108108(*---------------*) ⊢
    109 ext_fin_instruction (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
     109ext_fin_stmt (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
    110110unification hint 0 ≔ globals
    111111(*---------------*) ⊢
    112112joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    113 
    114 definition rtl_internal_function ≝
    115   λglobals. joint_internal_function globals rtl_params.
    116 
    117 definition rtl_program ≝ joint_program rtl_params.
    118113
    119114(************ Same without tail calls ****************)
     
    124119
    125120definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
    126   (mk_inst_params
     121  (mk_step_params
    127122    (* acc_a_reg ≝ *) register
    128123    (* acc_b_reg ≝ *) register
     
    138133    (* call_dest ≝ *) (list register)
    139134    (* extend_statements ≝ *) rtlntc_statement_extension
    140     (* ext_forall_labels ≝ *) (λP.λes.True)
    141     void (λP,es.True))
     135    (* ext_forall_labels ≝ *) (λes.[ ])
     136    void (λes.[ ]))
    142137  (mk_local_params
    143138    (mk_funct_params
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1644 r1882  
    2828definition local_env ≝ identifier_map RegisterTag (list register).
    2929
    30 definition mem_local_env : register → local_env → bool ≝
    31   λr,e. member … e r.
    32 
    33 definition add_local_env : register → list register → local_env → local_env ≝
    34   λr,v,e. add … e r v.
    35 
    36 definition find_local_env : register → local_env → list register ≝
    37   λr: register.λenv. lookup_def … env r [].
     30definition local_env_typed :
     31  list (register × typ) → local_env → Prop ≝
     32  λl,env.All ?
     33    (λp.let 〈r, ty〉 ≝ p in ∃regs.lookup … env r = Some ? regs ∧
     34                                 |regs| = size_of_sig_type ty) l.
     35
     36definition find_local_env ≝ λr.λlenv : local_env.
     37  λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?.
     38lapply (in_map_domain … lenv r)
     39>prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS)
     40qed.
     41
     42lemma find_local_env_elim : ∀P : list register → Prop.∀r. ∀lenv: local_env.∀prf.
     43  (∀x.lookup … lenv r = Some ? x → P x) → P (find_local_env r lenv prf).
     44#P#r#lenv#prf #H
     45change with (P (opt_safe ???))
     46@opt_safe_elim assumption
     47qed.
    3848
    3949definition find_local_env_arg ≝
    40   λr,lenv. map … Reg (find_local_env r lenv).
     50  λr,lenv,prf. map … Reg (find_local_env r lenv prf).
    4151
    4252let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
     
    4959
    5060definition initialize_local_env_internal ≝
    51   λlenv_runiverse.
     61  λlenv_runiverse : local_env × ?.
    5262  λr_sig.
    5363  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
     
    5565  let size ≝ size_of_sig_type sig in
    5666  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
    57     〈add_local_env r rs lenv,runiverse〉.
     67    〈add … lenv r rs,runiverse〉.
    5868
    5969definition initialize_local_env ≝
     
    7080
    7181definition map_list_local_env_internal ≝
    72   λlenv,res,r. res @ (find_local_env r lenv).
     82  λlenv,res,r_sig. res @ (find_local_env (pi1 … r_sig) lenv (pi2 … r_sig)).
    7383   
    7484definition map_list_local_env ≝
     
    8090  λprf: 2 = length A lst.
    8191  match lst return λx. 2 = |x| → A × A with
    82   [ nil ⇒ λlst_nil_prf. ?
     92  [ nil ⇒ λlst_nil_prf.
    8393  | cons hd tl ⇒ λprf.
    8494    match tl return λx. 1 = |x| → A × A with
    85     [ nil ⇒ λtl_nil_prf. ?
     95    [ nil ⇒ λtl_nil_prf.
    8696    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
    8797    ] ?
     
    98108
    99109definition find_and_addr ≝
    100   λr,lenv. make_addr ? (find_local_env r lenv).
     110  λr,lenv,prf. make_addr ? (find_local_env r lenv prf).
    101111
    102112definition rtl_args ≝
    103   λregs_list,lenv. flatten … (map … (λr.find_local_env_arg r lenv) regs_list).
     113  λlenv,regs_list. flatten … (map … (λr.find_local_env_arg (pi1 … r) lenv (pi2 … r)) regs_list).
    104114
    105115definition split_into_bytes:
     
    119129qed.
    120130
    121 
    122 lemma eqb_implies_eq:
    123   ∀m, n: nat.
    124     eqb m n = true → m = n.
    125     #m#n@eqb_elim // #_ #F destruct(F) qed.
    126 
    127131definition translate_op:
    128132  ∀globals. Op2 →
     
    131135  ∀srcrs2 : list rtl_argument.
    132136  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    133   list (rtl_instruction globals)
     137  list (rtl_step globals)
    134138   ≝
    135139  λglobals: list ident.
     
    140144  λprf1,prf2.
    141145  let f_add ≝ OP2 rtl_params globals in
    142   let res : list (rtl_instruction globals) ≝
     146  let res : list (rtl_step globals) ≝
    143147    map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in
    144148  (* first, clear carry if op relies on it *)
     
    151155  (* if adding, we use a first Add op, that clear the carry, and then Addc's *)
    152156  [ Add ⇒
    153     match destrs return λx.|destrs| = |x| → list (rtl_instruction globals) with
     157    match destrs return λx.|destrs| = |x| → list (rtl_step globals) with
    154158    [ nil ⇒ λeq_destrs.[ ]
    155159    | cons destr destrs' ⇒ λeq_destrs.
    156       match srcrs1 return λy.|srcrs1| = |y| → list (rtl_instruction globals) with
     160      match srcrs1 return λy.|srcrs1| = |y| → list (rtl_step globals) with
    157161      [ nil ⇒ λeq_srcrs1.⊥
    158162      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
    159         match srcrs2 return λz.|srcrs2| = |z| → list (rtl_instruction globals) with
     163        match srcrs2 return λz.|srcrs2| = |z| → list (rtl_step globals) with
    160164        [ nil ⇒ λeq_srcrs2.⊥
    161165        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
     
    196200  | _ ⇒ True
    197201  ].
     202
    198203definition translate_cst :
    199204  ∀globals: list ident.
    200205  ∀cst_sig: Σcst : constant.cst_well_defd globals cst.
    201206  ∀destrs: list register.
    202   |destrs| = size_of_cst cst_sig → list (rtl_instruction globals)
     207  |destrs| = size_of_cst cst_sig → list (rtl_step globals)
    203208 ≝
    204209  λglobals,cst_sig,destrs,prf.
    205   match cst_sig return λy.cst_sig = y → list (rtl_instruction globals) with
     210  match cst_sig return λy.cst_sig = y → list (rtl_step globals) with
    206211  [ mk_Sig cst cst_good ⇒ λeqcst_sig.
    207     match cst return λx.cst = x → list (rtl_instruction globals)
     212    match cst return λx.cst = x → list (rtl_step globals)
    208213    with
    209214    [ Ointconst size const ⇒ λeqcst.
     
    218223    | Oaddrstack offset ⇒ λeqcst.
    219224      let 〈r1, r2〉 ≝ make_addr … destrs ? in
    220       [(rtl_st_ext_stack_address r1 r2 : rtl_instruction globals)]
     225      [(rtl_st_ext_stack_address r1 r2 : rtl_step globals)]
    221226    ] (refl …)
    222227  ] (refl …).
     
    235240  ∀destrs: list register.
    236241  ∀srcrs: list rtl_argument.
    237   |destrs| = |srcrs| → list (rtl_instruction globals) ≝
     242  |destrs| = |srcrs| → list (rtl_step globals) ≝
    238243  λglobals,destrs,srcrs,length_eq.
    239244  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
     
    259264qed.
    260265
    261 definition sign_mask : ∀globals.register → register → list (rtl_instruction globals) ≝
     266definition sign_mask : ∀globals.register → register → list (rtl_step globals) ≝
    262267    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
    263268       byte in destr if srcr is: neg   |  pos
     
    275280definition translate_cast_signed :
    276281  ∀globals : list ident.
    277   list register → register → bind_list register unit (rtl_instruction globals) ≝
     282  list register → register → bind_list register (rtl_step globals) ≝
    278283  λglobals,destrs,srcr.
    279284  ν tmp in
     
    283288definition translate_cast_unsigned :
    284289  ∀globals : list ident.
    285   list register → list (rtl_instruction globals) ≝
     290  list register → list (rtl_step globals) ≝
    286291  λglobals,destrs.
    287292  match nat_to_args (|destrs|) 0 with
     
    296301  ∀globals: list ident.
    297302  signedness → list register → list register →
    298     bind_list register unit (rtl_instruction globals) ≝
     303    bind_list register (rtl_step globals) ≝
    299304  λglobals,src_sign,destrs,srcrs.
    300305  match srcrs
    301   return λy. y = srcrs → bind_list register unit (rtl_instruction globals)
     306  return λy. y = srcrs → bind_list register (rtl_step globals)
    302307  with
    303308  [ nil ⇒ λ_.translate_cast_unsigned ? destrs (* srcrs = [ ] ⇒ we fill with 0 *)
     
    306311    [ mk_Sig crl len_proof ⇒
    307312      (* move prefix of srcrs in destrs *)
    308       translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @
    309       match \snd (\snd crl) with
     313      translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @@
     314      match \snd (\snd crl) return λ_.bind_list ?? with
    310315      [ nil ⇒
    311         match src_sign return λ_.bind_list register unit (rtl_instruction globals) with
     316        match src_sign return λ_.bind_list register (rtl_step globals) with
    312317        [ Unsigned ⇒ translate_cast_unsigned ? (\snd (\fst crl))
    313318        | Signed ⇒
     
    326331  ∀destrs : list register.
    327332  ∀srcrs_arg : list register.
    328   |destrs| = |srcrs_arg| → list (rtl_instruction globals) ≝
     333  |destrs| = |srcrs_arg| → list (rtl_step globals) ≝
    329334  λglobals, destrs, srcrs, prf.
    330335  map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf.
    331336
    332 
    333 definition translate_negint : ∀globals.? → ? → ? → bind_list register unit (rtl_instruction globals) ≝
     337definition translate_negint : ∀globals.? → ? → ? → bind_list register (rtl_step globals) ≝
    334338  λglobals: list ident.
    335339  λdestrs: list register.
     
    346350  ∀globals : list ident.
    347351  list register → list register →
    348     bind_list register unit (rtl_instruction globals) ≝
     352    bind_list register (rtl_step globals) ≝
    349353  λglobals,destrs,srcrs.
    350354  match destrs with
    351355  [ nil ⇒ [ ]
    352356  | cons destr destrs' ⇒
    353     translate_cast_unsigned ? destrs' @ (* fill destrs' with 0 *)
     357    translate_cast_unsigned ? destrs' @@ (* fill destrs' with 0 *)
    354358    match srcrs with
    355359    [ nil ⇒ [destr ← 0]
    356360    | cons srcr srcrs' ⇒
    357       let f : register → rtl_instruction globals ≝
     361      let f : register → rtl_step globals ≝
    358362        λr. destr ← destr .Or. r in
    359       MOVE rtl_params globals 〈destr,srcr〉 ::
    360       map … f srcrs' @
     363      (destr ← srcr) ::: ? ]].
     364      map ?? f srcrs' @@
    361365      (* now destr is non-null iff srcrs was non-null *)
    362366      CLEAR_CARRY ? ? ::
     
    371375
    372376definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
    373   bind_list register unit (rtl_instruction globals) ≝
     377  bind_list register unit (rtl_step globals) ≝
    374378  λglobals.
    375379  λty, ty'.
     
    381385  match op1
    382386  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
    383     bind_list register unit (rtl_instruction globals) with
     387    bind_list register unit (rtl_step globals) with
    384388  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
    385389    translate_cast globals src_sign destrs srcrs
     
    440444  (Σi.i<S k) →
    441445  (* the accumulator *)
    442   list (rtl_instruction globals) →
    443     list (rtl_instruction globals) ≝
     446  list (rtl_step globals) →
     447    list (rtl_step globals) ≝
    444448  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
    445449    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
     
    488492] qed.
    489493
    490 definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     494definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    491495λglobals : list ident.
    492496λdestrs : list register.
     
    504508(* the step calculating all products with least significant byte going in the
    505509   k-th position of the result *)
    506 let translate_mul_k : (Σk.k<|destrs|) → list (rtl_instruction globals) →
    507   list (rtl_instruction globals) ≝
     510let translate_mul_k : (Σk.k<|destrs|) → list (rtl_step globals) →
     511  list (rtl_step globals) ≝
    508512  λk_sig,acc.match k_sig with
    509513  [ mk_Sig k k_prf ⇒
     
    528532
    529533definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
    530     bind_list register unit (rtl_instruction globals) ≝
     534    bind_list register unit (rtl_step globals) ≝
    531535  λglobals: list ident.
    532536  λdiv_not_mod: bool.
     
    536540  λsrcrs1_prf : |destrs| = |srcrs1|.
    537541  λsrcrs2_prf : |srcrs1| = |srcrs2|.
    538   let return_type ≝ bind_list register unit (rtl_instruction globals) in
     542  let return_type ≝ bind_list register unit (rtl_step globals) in
    539543  match destrs return λx.x = destrs → return_type with
    540544  [ nil ⇒ λ_.[ ]
     
    575579qed.
    576580
    577 definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     581definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    578582  λglobals: list ident.
    579583  λdestrs: list register.
     
    582586  λsrcrs1_prf : |destrs| = |srcrs1|.
    583587  λsrcrs2_prf : |srcrs1| = |srcrs2|.
    584   let return_type ≝ bind_list register unit (rtl_instruction globals) in
     588  let return_type ≝ bind_list register unit (rtl_step globals) in
    585589  match destrs return λx.x = destrs → return_type with
    586590  [ nil ⇒ λ_.[ ]
     
    593597      | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
    594598        νtmpr in
    595         let f : rtl_argument → rtl_argument → list (rtl_instruction globals) → list (rtl_instruction globals) ≝
     599        let f : rtl_argument → rtl_argument → list (rtl_step globals) → list (rtl_step globals) ≝
    596600          λs1,s2,acc.
    597601          tmpr  ← s1 .Xor. s2 ::
    598602          destr ← destr .Or. tmpr ::
    599603          acc in
    600         let epilogue : list (rtl_instruction globals) ≝
     604        let epilogue : list (rtl_step globals) ≝
    601605          [ CLEAR_CARRY … ;
    602606            tmpr ← 0 .Sub. destr ;
     
    613617(* if destrs is 0 or 1, it inverses it. To be used after operations that
    614618   ensure this. *)
    615 definition translate_toggle_bool : ∀globals.?→list (rtl_instruction globals) ≝
     619definition translate_toggle_bool : ∀globals.?→list (rtl_step globals) ≝
    616620  λglobals: list ident.
    617621  λdestrs: list register.
     
    628632  |destrs| = |srcrs1| →
    629633  |srcrs1| = |srcrs2| →
    630   list (rtl_instruction globals) ≝
     634  list (rtl_step globals) ≝
    631635  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
    632636  match destrs with
     
    645649  (tmp : register)
    646650  (srcrs : list rtl_argument) on srcrs :
    647   (list rtl_argument) × (list (rtl_instruction globals)) ≝
     651  (list rtl_argument) × (list (rtl_step globals)) ≝
    648652  match srcrs with
    649653  [ nil ⇒ 〈[ ],[ ]〉
     
    674678  |destrs| = |srcrs1| →
    675679  |srcrs1| = |srcrs2| →
    676   bind_list register unit (rtl_instruction globals) ≝
     680  bind_list register unit (rtl_step globals) ≝
    677681  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
    678682  νtmp_last_s1 in
     
    688692>shift_signed_length [2: >shift_signed_length] assumption qed.
    689693
    690 definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     694definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    691695  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
    692696  if is_unsigned then
     
    717721 
    718722definition translate_op2 :
    719   ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     723  ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    720724  λglobals: list ident.
    721725  λop2.
     
    758762  cases not_implemented (* XXX: yes, really *) qed.
    759763
    760 definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_instruction globals) ≝
     764definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_step globals) ≝
    761765  λglobals: list ident.
    762766  λsrcrs: list register.
     
    766770  | cons srcr srcrs' ⇒
    767771    ν tmpr in
    768     let f : register → rtl_instruction globals ≝
     772    let f : register → rtl_step globals ≝
    769773      λr. tmpr ← tmpr .Or. r in
    770774    MOVE rtl_params globals 〈tmpr,srcr〉 ::
     
    781785  ν tmp_addr_l in
    782786  ν tmp_addr_h in
    783   let f ≝ λdestr : register.λacc : list (rtl_instruction globals).
     787  let f ≝ λdestr : register.λacc : list (rtl_step globals).
    784788    LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) ::
    785789    translate_op … Add
     
    798802  ν tmp_addr_l in
    799803  ν tmp_addr_h in
    800   let f ≝ λsrcr : rtl_argument.λacc : list (rtl_instruction globals).
     804  let f ≝ λsrcr : rtl_argument.λacc : list (rtl_step globals).
    801805    STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr ::
    802806    translate_op … Add
     
    822826
    823827definition translate_inst : ∀globals.?→?→?→
    824   (bind_list register unit (rtl_instruction globals)) × label ≝
     828  (bind_list register unit (rtl_step globals)) × label ≝
    825829  λglobals: list ident.
    826830  λlenv: local_env.
    827831  λstmt.
     832  λstmt_typed :
    828833  λstmt_prf : stmt_not_final stmt.
    829834  match stmt return λx.stmt = x →
    830     (bind_list register unit (rtl_instruction globals)) × label with
     835    (bind_list register unit (rtl_step globals)) × label with
    831836  [ St_skip lbl' ⇒ λ_.
    832837    〈[ ], lbl'〉
     
    865870    (* Paolo: no notation to avoid ambiguity *)
    866871    〈bcons … (
    867       match retr return λ_.rtl_instruction globals with
     872      match retr return λ_.rtl_step globals with
    868873      [ Some retr ⇒
    869874        rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv)
  • src/RTLabs/semantics.ma

    r1880 r1882  
    124124      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    125125      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    126       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     126      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    127127      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    128128  | St_call_ptr frs args dst l ⇒ λH.
    129129      ! fv ← reg_retrieve (locals f) frs;
    130130      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    131       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     131      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    132132      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    133133(*
     
    135135      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    136136      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    137       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     137      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    138138      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    139139  | St_tailcall_ptr frs args ⇒ λH.
    140140      ! fv ← reg_retrieve (locals f) frs;
    141141      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    142       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     142      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    143143      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    144144*)
  • src/common/AST.ma

    r1873 r1882  
    353353definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
    354354                         list (A × B) → res (list (A × C)) ≝
    355 λA,B,C,f. m_mmap ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
     355λA,B,C,f. m_list_map ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
    356356
    357357lemma map_partial_preserves_first:
  • src/common/Errors.ma

    r1647 r1882  
    1 (* *********************************************************************)
    2 (*                                                                     *)
    3 (*              The Compcert verified compiler                         *)
    4 (*                                                                     *)
    5 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
    6 (*                                                                     *)
    7 (*  Copyright Institut National de Recherche en Informatique et en     *)
    8 (*  Automatique.  All rights reserved.  This file is distributed       *)
    9 (*  under the terms of the GNU General Public License as published by  *)
    10 (*  the Free Software Foundation, either version 2 of the License, or  *)
    11 (*  (at your option) any later version.  This file is also distributed *)
    12 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
    13 (*                                                                     *)
    14 (* *********************************************************************)
    15 
    161include "basics/types.ma".
    172include "basics/logic.ma".
     
    205include "basics/russell.ma".
    216include "utilities/monad.ma".
     7include "utilities/option.ma".
     8
     9(* first, generic exception monad *)
     10
     11inductive except (E : Type[0]) (X : Type[0]) : Type[0] ≝
     12  | raise : E → except E X
     13  | success : X → except E X.
     14
     15definition Except ≝ λE.MakeMonadProps
     16  (except E)
     17  (success E)
     18  (λX,Y,m,f.match m with [raise e ⇒ raise … e | success x ⇒ f x])
     19  ????.
     20//
     21[ #X * #x %
     22| #X#Y#Z * #x#f#g %
     23| #X#Y normalize * #x #f #g #H // normalize @H
     24]
     25qed.
     26
     27unification hint 0 ≔ E,X;
     28O ≟ Except E, N ≟ max_def O
     29(*--------------------------------------*) ⊢
     30except E X ≡ monad N X.
     31
     32definition try_catch : ∀E,X.except E X → (E → X) → X ≝
     33  λE,X,m,f.match m with
     34  [ success x ⇒ x
     35  | raise e ⇒ f e
     36  ].
     37
     38interpretation "exception try catch" 'trycatch e f = (try_catch ?? e f).
     39
     40definition except_elim : ∀E,X.∀m : except E X.∀P : ? → Prop.
     41  (∀x.m = success ?? x → P (success ?? x)) →
     42  (∀e.m = raise ?? e → P (raise ?? e)) →
     43  P m.
     44#E #X * /2/
     45qed.
     46
     47definition except_success ≝ λE,X.λm : except E X.
     48  match m with [success _ ⇒ True | _ ⇒ False].
     49
     50definition except_safe ≝
     51  λE,X.λm : except E X.
     52    match m return λx.except_success ?? x → X with
     53    [ success y ⇒ λ_.y
     54    | _ ⇒ λprf.match prf in False with []
     55    ].
     56
     57definition Except_P ≝ λE.λP_e : E → Prop.mk_MonadPred (Except E)
     58  (λX,P,m. Try ! x ← m ; return P x catch e ⇒ P_e e) ???.
     59[ //
     60| #X#Y #P1 #P2 * #x normalize /2/
     61| #X #P #Q #H * #y normalize /2/
     62]
     63qed.
     64
     65definition except_P ≝ λE,P_e.m_pred … (Except_P E P_e).
     66
     67definition except_All : ∀E,X.(X → Prop) → except E X → Prop ≝
     68  λE : Type[0].except_P E (λe.True).
     69
     70definition except_Exists : ∀E,X.(X → Prop) → except E X → Prop ≝
     71  λE : Type[0].except_P E (λe.False).
     72
     73definition except_rel ≝ λE,F.λrel_e : E → F → Prop.mk_MonadRel (Except E) (Except F)
     74  (λX,Y,rel,m,n.
     75    match m with
     76    [ success x ⇒ match n with [success y ⇒ rel x y | _ ⇒ False]
     77    | raise e ⇒ match n with [raise f ⇒ rel_e e f | _ ⇒ False]
     78    ]) ???.
     79[ //
     80|*: #X#Y[#Z#W] #rel1 #rel2 [2: #H] * #x * #y normalize /2/ *
     81]
     82qed.
    2283
    2384(* * Error reporting and the error monad. *)
     
    42103  The return value is either [OK res] to indicate success,
    43104  or [Error msg] to indicate failure. *)
     105
     106(* Paolo: not using except for backward compatbility
     107  (would break Error ? msg) *)
    44108
    45109inductive res (A: Type[0]) : Type[0] ≝
     
    56120  (* bind *)
    57121  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
    58   ???.
     122  ????.
    59123//
    60124[(* bind_ret *)
     
    62126|(* bind_bind *)
    63127 #X#Y#Z*normalize //
     128| normalize #X #Y * normalize /2/
    64129]
    65130qed.
     
    67132include "hints_declaration.ma".
    68133unification hint 0 ≔ X;
    69 N ≟ max_def Res, M ≟ m_def N
     134N ≟ max_def Res
    70135(*---------------*) ⊢
    71 res X ≡ monad M X
     136res X ≡ monad N X
    72137.
    73138
     
    267332definition bind2 ≝ m_bind2 Res.
    268333definition bind3 ≝ m_bind3 Res.
    269 definition mmap ≝ m_mmap Res.
    270 definition mmap_sigma ≝ m_mmap_sigma Res.
     334definition mmap ≝ m_list_map Res.
     335definition mmap_sigma ≝ m_list_map_sigma Res.
  • src/common/Graphs.ma

    r1635 r1882  
    5959  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
    6060
    61 axiom graph_num_nodes:
    62   ∀A: Type[0].
    63   ∀g: graph A.
    64     nat.
     61definition graph_num_nodes:
     62  ∀A: Type[0].graph A → ℕ ≝ λA,g.|g|.
     63 
     64lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop.
     65  (∀g.(∀g'.|g'|<|g| → P g') → P g) → ∀g.P g.
     66#A#P#H#g
     67lapply (refl ? (|g|))
     68generalize in ⊢(???%→?);
     69#n lapply g -g
     70@(nat_elim1 … n)
     71#m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …))
     72qed.
  • src/common/IOMonad.ma

    r1647 r1882  
    3131  (* bind *)
    3232  (bindIO O I)
    33   ???. / by /
     33  ????. / by /
    3434[(* bind_ret *)
    3535 #X#m elim m normalize // #o#f#Hi @interact_proper //
     
    3838 (* Interact *)
    3939  #o#f #Hi @interact_proper //
     40|#X #Y #m #f #g #H elim m normalize
     41  [ #o #x @interact_proper ] //
    4042]
    4143qed.
     
    4648
    4749unification hint 0 ≔ O, I, T;
    48   N ≟ IOMonad O I, M ≟ max_def N, M' ≟ m_def M
     50  N ≟ IOMonad O I, M ≟ max_def N
    4951(*******************************************) ⊢
    50   IO O I T ≡ monad M' T
     52  IO O I T ≡ monad M T
    5153.
    5254
  • src/common/Identifiers.ma

    r1635 r1882  
    33include "utilities/binary/positive.ma".
    44include "utilities/lists.ma".
     5include "utilities/extralib.ma".
    56include "common/Errors.ma".
    67
     
    370371(* Sets *)
    371372
    372 inductive identifier_set (tag:String) : Type[0] ≝
    373   an_id_set : positive_map unit → identifier_set tag.
    374 
    375 definition empty_set : ∀tag:String. identifier_set tag ≝
    376 λtag. an_id_set tag (pm_leaf unit).
    377 
    378 let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
    379   an_id_set tag (insert unit (match i with [ an_identifier i' ⇒ i' ])
    380                           it (match s with [ an_id_set s' ⇒ s' ])).
     373definition identifier_set ≝ λtag.identifier_map tag unit.
     374
     375definition empty_set : ∀tag.identifier_set tag ≝ λtag.empty_map ….
     376
     377
     378definition add_set : ∀tag.identifier_set tag → identifier tag → identifier_set tag ≝
     379  λtag,s,i.add … s i it.
    381380
    382381definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
    383382λtag,i. add_set tag (empty_set tag) i.
    384383
    385 let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
    386   match lookup_opt ? (match i with [ an_identifier i' ⇒ i' ])
    387                      (match s with [ an_id_set s' ⇒ s' ]) with
     384(* mem set is generalised to all maps *)
     385let rec mem_set (tag:String) A (s:identifier_map tag A) (i:identifier tag) on s : bool ≝
     386  match lookup … s i with
    388387  [ None ⇒ false
    389388  | Some _ ⇒ true
    390389  ].
    391 
    392 let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
    393   an_id_set tag (merge unit (match s with [ an_id_set s0 ⇒ s0 ])
    394                             (match s' with [ an_id_set s1 ⇒ s1 ])).
    395 
    396 interpretation "identifier set union" 'union a b = (union_set ? a b).
     390 
     391let rec union_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝
     392  an_id_map tag unit (merge … (λo,o'.match o with [Some _ ⇒ Some ? it | None ⇒ !_ o'; return it])
     393    (match s with [ an_id_map s0 ⇒ s0 ])
     394    (match s' with [ an_id_map s1 ⇒ s1 ])).
     395
     396
     397(* set minus is generalised to maps *)
     398let rec minus_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_map tag A ≝
     399  an_id_map tag A (merge A B A (λo,o'.match o' with [None ⇒ o | Some _ ⇒ None ?])
     400    (match s with [ an_id_map s0 ⇒ s0 ])
     401    (match s' with [ an_id_map s1 ⇒ s1 ])).
     402
     403notation "a ∖ b" left associative with precedence 50 for @{'setminus $a $b}.
     404
     405interpretation "identifier set union" 'union a b = (union_set ??? a b).
    397406notation "∅" non associative with precedence 90 for @{ 'empty }.
    398407interpretation "empty identifier set" 'empty = (empty_set ?).
    399408interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
    400 interpretation "identifier set membership" 'mem a b = (mem_set ? b a).
     409interpretation "identifier set membership" 'mem a b = (mem_set ?? b a).
     410interpretation "identifier map difference" 'setminus a b = (minus_set ??? a b).
     411
     412definition IdentifierSet : String → Setoid ≝ λtag.
     413  mk_Setoid (identifier_set tag) (λs,s'.∀i.i ∈ s = (i ∈ s')) ???.
     414  // qed.
     415
     416unification hint 0 ≔ tag;
     417S ≟ IdentifierSet tag
     418(*-----------------------------*)⊢
     419identifier_set tag ≡ std_supp S.
     420unification hint 0 ≔ tag;
     421S ≟ IdentifierSet tag
     422(*-----------------------------*)⊢
     423identifier_map tag unit ≡ std_supp S.
     424
     425lemma mem_set_add : ∀tag,A.∀i,j : identifier tag.∀s,x.
     426  i ∈ add ? A s j x = (eq_identifier ? i j ∨ i ∈ s).
     427#tag #A *#i *#j *#s #x normalize
     428@(eqb_elim i j)
     429[#EQ destruct
     430  >(lookup_opt_insert_hit A x j)
     431|#NEQ >(lookup_opt_insert_miss … s NEQ)
     432] elim (lookup_opt  A j s) normalize // qed.
     433
     434lemma mem_set_add_id : ∀tag,A,i,s,x.bool_to_Prop (i ∈ add tag A s i x).
     435#tag #A #i #s #x >mem_set_add
     436@eq_identifier_elim [#_ %| #ABS elim (absurd … (refl ? i) ABS)] qed.
     437
     438lemma in_map_domain : ∀tag,A.∀m : identifier_map tag A.∀i.
     439  if i ∈ m then (∃s.lookup … m i = Some ? s) else (lookup … m i = None ?).
     440#tag #A * #m * #i normalize
     441elim (lookup_opt A i m) normalize
     442[ % | #x %{x} % ]
     443qed.
    401444
    402445lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
    403 #tag * //
     446#tag * normalize #m >map_opt_id_eq_ext // * %
    404447qed.
    405448
    406449lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
    407 #tag * * // qed.
    408 
     450#tag * * [//] *[2: *] #l#r normalize
     451>map_opt_id_eq_ext [1,3: >map_opt_id_eq_ext [2,4: *] |*: *] //
     452qed.
     453
     454lemma minus_empty_l : ∀tag,A.∀s:identifier_map tag A. ∅ ∖ s ≅ ∅.
     455#tag #A * * [//] *[2:#x]#l#r * * normalize [1,4://]
     456#p >lookup_opt_map elim (lookup_opt ???) normalize //
     457qed.
     458
     459lemma minus_empty_r : ∀tag,A.∀s:identifier_map tag A. s ∖ ∅ = s.
     460#tag #A * * [//] *[2:#x]#l#r normalize
     461>map_opt_id >map_opt_id //
     462qed.
     463
     464lemma mem_set_union : ∀tag.∀i : identifier tag.∀s,s' : identifier_set tag.
     465  i ∈ (s ∪ s') = (i ∈ s ∨ i ∈ s').
     466#tag * #i * #s * #s' normalize
     467>lookup_opt_merge [2: @refl]
     468elim (lookup_opt ???)
     469elim (lookup_opt ???)
     470normalize // qed.
     471
     472lemma mem_set_minus : ∀tag,A,B.∀i : identifier tag.∀s : identifier_map tag A.
     473  ∀s' : identifier_map tag B.
     474  i ∈ (s ∖ s') = (i ∈ s ∧ ¬ i ∈ s').
     475#tag #A #B * #i * #s * #s' normalize
     476>lookup_opt_merge [2: @refl]
     477elim (lookup_opt ???)
     478elim (lookup_opt ???)
     479normalize // qed.
     480
     481lemma set_eq_ext_node : ∀tag.∀o,o',l,l',r,r'.
     482  an_id_map tag ? (pm_node ? o l r) ≅ an_id_map … (pm_node ? o' l' r') →
     483    o = o' ∧ an_id_map tag ? l ≅ an_id_map … l' ∧ an_id_map tag ? r ≅ an_id_map … r'.
     484#tag#o#o'#l#l'#r#r'#H
     485%[
     486%[ lapply (H (an_identifier ? one))
     487   elim o [2: *] elim o' [2,4: *] normalize // #EQ destruct
     488 | *#p lapply (H (an_identifier ? (p0 p))) normalize //
     489]| *#p lapply (H (an_identifier ? (p1 p))) normalize //
     490]
     491qed.
     492
     493lemma set_eq_ext_leaf : ∀tag,A.∀o,l,r.
     494  (∀i.i∈an_id_map tag A (pm_node ? o l r) = false) →
     495    o = None ? ∧ (∀i.i∈an_id_map tag ? l = false) ∧ (∀i.i∈an_id_map tag ? r = false).
     496#tag#A#o#l#r#H
     497%[
     498%[ lapply (H (an_identifier ? one))
     499   elim o [2: #a] normalize // #EQ destruct
     500 | *#p lapply (H (an_identifier ? (p0 p))) normalize //
     501]| *#p lapply (H (an_identifier ? (p1 p))) normalize //
     502]
     503qed.
     504
     505
     506definition id_map_size : ∀tag : String.∀A. identifier_map tag A → ℕ ≝
     507  λtag,A,s.match s with [an_id_map p ⇒ |p|].
     508
     509interpretation "identifier map domain size" 'norm s = (id_map_size ?? s).
     510
     511lemma set_eq_ext_empty_to_card : ∀tag,A.∀s : identifier_map tag A. (∀i.i∈s = false) → |s| = 0.
     512#tag#A * #s elim s [//]
     513#o#l#r normalize in ⊢((?→%)→(?→%)→?); #Hil #Hir #H
     514elim (set_eq_ext_leaf … H) * #EQ destruct #Hl #Hr normalize
     515>(Hil Hl) >(Hir Hr) // qed.
     516
     517lemma set_eq_ext_to_card : ∀tag.∀s,s' : identifier_set tag. s ≅ s' → |s| = |s'|.
     518#tag *#s elim s
     519[** [//] #o#l#r #H
     520  >(set_eq_ext_empty_to_card … (std_symm … H)) //
     521| #o#l#r normalize in ⊢((?→?→??%?)→(?→?→??%?)→?);
     522  #Hil #Hir **
     523  [#H @(set_eq_ext_empty_to_card … H)]
     524  #o'#l'#r' #H elim (set_eq_ext_node … H) * #EQ destruct(EQ) #Hl #Hr
     525  normalize >(Hil ? Hl) >(Hir ? Hr) //
     526] qed.
     527
     528lemma add_size: ∀tag,A,s,i,x.
     529  |add tag A s i x| = (if i ∈ s then 0 else 1) + |s|.
     530#tag #A *#s *#i #x
     531lapply (insert_size ? i x s)
     532lapply (refl ? (lookup_opt ? i s))
     533generalize in ⊢ (???%→?); * [2: #x']
     534normalize #EQ >EQ normalize //
     535qed.
     536
     537lemma mem_set_O_lt_card : ∀tag,A.∀i.∀s : identifier_map tag A. i ∈ s → |s| > 0.
     538#tag #A * #i * #s normalize #H
     539@(lookup_opt_O_lt_size … i)
     540% #EQ >EQ in H; normalize *
     541qed.
     542
     543(* NB: no control on values if applied to maps *)
     544definition set_subset ≝ λtag,A,B.λs : identifier_map tag A.
     545  λs' : identifier_map tag B. ∀i.i ∈ s → (bool_to_Prop (i ∈ s')).
     546
     547interpretation "identifier set subset" 'subseteq s s' = (set_subset ??? s s').
     548
     549lemma add_subset :
     550  ∀tag,A,B.∀i : identifier tag.∀x.∀s : identifier_map ? A.∀s' : identifier_map ? B.
     551    i ∈ s' → s ⊆ s' → add … s i x ⊆ s'.
     552#tag#A#B#i#x#s#s' #H #G #j
     553>mem_set_add
     554@eq_identifier_elim #H' [* >H' @H | #js @(G ? js)]
     555qed.
     556
     557definition set_forall : ∀tag,A.(identifier tag → Prop) →
     558  identifier_map tag A → Prop ≝ λtag,A,P,m.∀i. i ∈ m → P i.
     559 
     560lemma set_forall_add : ∀tag,P,m,i.set_forall tag ? P m → P i →
     561  set_forall tag ? P (add_set ? m i).
     562#tag#P#m#i#Pm#Pi#j
     563>mem_set_add
     564@eq_identifier_elim
     565[#EQ destruct(EQ) #_ @Pi
     566|#_ @Pm
     567]
     568qed.
     569
     570include "utilities/proper.ma".
     571
     572lemma minus_subset : ∀tag,A,B.minus_set tag A B ⊨ set_subset … ++> set_subset … -+> set_subset ….
     573#tag#A#B#s#s' #H #s'' #s''' #G #i
     574>mem_set_minus >mem_set_minus
     575#H' elim (andb_Prop_true … H') -H' #is #nis''
     576>(H … is)
     577elim (true_or_false_Prop (i∈s'''))
     578[ #is''' >(G … is''') in nis''; *
     579| #nis''' >nis''' %
     580]
     581qed.
     582
     583lemma subset_node : ∀tag,A,B.∀o,o',l,l',r,r'.
     584  an_id_map tag A (pm_node ? o l r) ⊆ an_id_map tag B (pm_node ? o' l' r') →
     585    opt_All ? (λ_.o' ≠ None ?) o ∧ an_id_map tag ? l ⊆ an_id_map tag  ? l' ∧
     586      an_id_map tag ? r ⊆ an_id_map tag ? r'.
     587#tag#A#B#o#o'#l#l'#r#r'#H
     588%[%
     589  [ lapply (H (an_identifier ? (one))) elim o [2: #a] elim o' [2:#b]
     590    normalize // [#_ % #ABS destruct(ABS) | #G lapply (G I) *]
     591  | *#p lapply (H (an_identifier ? (p0 p)))
     592  ]
     593 | *#p lapply (H (an_identifier ? (p1 p)))
     594] #H @H
     595qed.
     596
     597lemma subset_leaf : ∀tag,A.∀o,l,r.
     598  an_id_map tag A (pm_node ? o l r) ⊆ ∅ →
     599    o = None ? ∧ (∀i.i∈an_id_map tag ? l = false) ∧ (∀i.i∈an_id_map tag ? r = false).
     600#tag#A#o#l#r#H
     601%[
     602%[ lapply (H (an_identifier ? one))
     603   elim o [2: #a] normalize // #EQ lapply(EQ I) *
     604 | *#p lapply (H (an_identifier ? (p0 p)))
     605 ]
     606|  *#p lapply (H (an_identifier ? (p1 p)))
     607] normalize elim (lookup_opt ? p ?) normalize
     608// #a #H lapply (H I) *
     609qed.
     610
     611lemma subset_card : ∀tag,A,B.∀s : identifier_map tag A.∀s' : identifier_map tag B.
     612  s ⊆ s' → |s| ≤ |s'|.
     613#tag #A #B *#s elim s
     614[ //
     615| #o#l#r #Hil #Hir **
     616  [ #H elim (subset_leaf … H) * #EQ >EQ #Hl #Hr
     617    lapply (set_eq_ext_empty_to_card … Hl)
     618    lapply (set_eq_ext_empty_to_card … Hr)
     619    normalize //
     620  | #o' #l' #r' #H elim (subset_node … H) *
     621    elim o [2: #a] elim o' [2,4: #a']
     622    [3: #G normalize in G; elim(absurd ? (refl ??) G)
     623    |*: #_ #Hl #Hr lapply (Hil ? Hl) lapply (Hir ? Hr)
     624      normalize #H1 #H2
     625      [@le_S_S | @(transitive_le … (|l'|+|r'|)) [2: / by /]]
     626      @le_plus assumption
     627    ]
     628  ]
     629]
     630qed.
     631
     632lemma mem_set_empty : ∀tag.∀i: identifier tag. i∈∅ = false.
     633#tag * #i normalize %
     634qed.
     635
     636lemma mem_set_singl_to_eq : ∀tag.∀i,j : identifier tag.i∈{(j)} → i = j.
     637#tag
     638#i #j >mem_set_add >mem_set_empty
     639#H elim (orb_true_l … H) -H
     640[@eq_identifier_elim [//] #_] #EQ destruct
     641qed.
     642
     643lemma subset_add_set : ∀tag,i,s.s ⊆ add_set tag s i.
     644#tag#i#s#j #H >mem_set_add >H
     645>commutative_orb %
     646qed.
     647
     648lemma add_set_monotonic : ∀tag,i,s,s'.s ⊆ s' → add_set tag s i ⊆ add_set tag s' i.
     649#tag#i#s#s' #H #j >mem_set_add >mem_set_add
     650@orb_elim elim (eq_identifier ???)
     651whd lapply (H j) /2 by /
     652qed.
     653
     654lemma transitive_subset : ∀tag,A.transitive ? (set_subset tag A A).
     655#tag#A#s#s'#s''#H#G#i #is
     656@(G … (H … is))
     657qed.
     658
     659definition set_from_list : ∀tag.list (identifier tag) → identifier_map tag unit ≝
     660  λtag.foldl … (add_set ?) ∅.
     661
     662coercion id_set_from_list : ∀tag.∀l : list (identifier tag).identifier_map tag unit ≝
     663  set_from_list on _l : list (identifier ?) to identifier_map ? unit.
     664
     665lemma mem_map_domain : ∀tag,A.∀m : identifier_map tag A.∀i.
     666i∈m → lookup … m i ≠ None ?.
     667#tag#A * #m #i
     668whd in match (i∈?);
     669elim (lookup ????) normalize [2: #x]
     670* % #EQ destruct(EQ)
     671qed.
     672
     673
     674
     675lemma mem_list_as_set : ∀tag.∀l : list (identifier tag).
     676  ∀i.i ∈ l → In ? l i.
     677#tag #l @(list_elim_left … l)
     678[ #i *
     679| #t #h #Hi  #i
     680  whd in ⊢ (?(???%?)→?);
     681  >foldl_append
     682  whd in ⊢ (?(???%?)→?);
     683  >mem_set_add
     684  @eq_identifier_elim
     685  [ #EQi destruct(EQi)
     686    #_ @Exists_append_r % %
     687  | #_ #H @Exists_append_l @Hi assumption
     688  ]
     689]
     690qed.
     691
     692lemma list_as_set_mem : ∀tag.∀l : list (identifier tag).
     693  ∀i.In ? l i → i ∈ l.
     694#tag #l @(list_elim_left … l)
     695[ #i *
     696| #t #h #Hi #i #H
     697  whd in ⊢ (?(???%?));
     698  >foldl_append
     699  whd in ⊢ (?(???%?));
     700  elim (Exists_append … H) -H
     701  [ #H >mem_set_add
     702    @eq_identifier_elim [//] #_ normalize
     703    @Hi @H
     704  | * [2: *] #EQi destruct(EQi) >mem_set_add_id %
     705  ]
     706]
     707qed.
     708
     709lemma list_as_set_All : ∀tag,P.∀ l : list (identifier tag).
     710  (∀i.i ∈ l → P i) → All ? P l.
     711#tag #P #l @(list_elim_left … l)
     712[ #_ %
     713| #x #l' #Hi
     714  whd in match (l'@[x] : identifier_map tag unit);
     715  >foldl_append
     716  #H @All_append
     717  [ @Hi #i #G @H
     718    whd in ⊢ (?(???%?));
     719    >mem_set_add @orb_Prop_r @G
     720  | % [2: %]
     721    @H
     722    whd in ⊢ (?(???%?));
     723    @mem_set_add_id
     724  ]
     725]
     726qed.
     727
     728lemma All_list_as_set : ∀tag,P.∀ l : list (identifier tag).
     729  All ? P l → ∀i.i ∈ l → P i.
     730#tag #P #l @(list_elim_left … l)
     731[ * #i *
     732| #x #l' #Hi #H
     733  lapply (All_append_l … H)
     734  lapply (All_append_r … H)
     735  * #Px * #Pl' #i
     736  whd in match (l'@[x] : identifier_map ??);
     737  >foldl_append
     738  >mem_set_add
     739  @eq_identifier_elim
     740  [ #EQx >EQx #_ @Px
     741  | #_ whd in match (?∨?); @Hi @Pl'
     742  ]
     743]
     744qed. 
     745
     746
     747
  • src/common/Pointers.ma

    r1545 r1882  
    118118 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
    119119qed.
     120
     121lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
     122  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
     123#P * #r0 #b0 #H0 * #o0 * #r1 #b1 #H1 * #o1
     124#Ptrue #Pfalse
     125whd in match (eq_pointer ??);
     126@eq_region_elim #reg_eq
     127[ @eq_block_elim #block_eq
     128  [ change with (eqZb ??) in match (eq_offset ??);
     129    @eqZb_elim #offset_eq
     130    [ destruct @Ptrue %
     131    ]
     132  ]
     133]
     134@Pfalse % #EQ destruct /2 by absurd/
     135qed.
  • src/common/PositiveMap.ma

    r1601 r1882  
    191191] qed.
    192192
    193 let rec merge (A: Type[0]) (b: positive_map A) (c:positive_map A) on b: positive_map A ≝
    194 match b with
    195 [ pm_leaf ⇒ c
     193include "utilities/option.ma".
     194
     195let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
     196match b with
     197[ pm_leaf ⇒ pm_leaf ?
     198| pm_node a l r ⇒ pm_node ? (a »= f)
     199    (map_opt ?? f l)
     200    (map_opt ?? f r)
     201].
     202
     203definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
     204
     205lemma lookup_opt_map : ∀A,B,f,b,p.
     206  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
     207#A#B#f#b elim b [//]
     208#a #l #r #Hil #Hir * [//]
     209#p
     210whd in ⊢ (??(???%)(????%?));
     211whd in ⊢ (??%?); //
     212qed.
     213
     214lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
     215#A #m #f #Hf elim m [//]
     216* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
     217qed.
     218
     219lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
     220#A #m @map_opt_id_eq_ext //
     221qed.
     222
     223let rec merge A B C (choice : option A → option B → option C)
     224  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
     225match a with
     226[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
     227| pm_node o l r ⇒
     228  match b with
     229  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
     230  | pm_node o' l' r' ⇒
     231    pm_node ? (choice o o')
     232      (merge … choice l l')
     233      (merge … choice r r')
     234  ]
     235].
     236
     237lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
     238  choice (None ?) (None ?) = None ? →
     239  lookup_opt … p (merge A B C choice a b) =
     240    choice (lookup_opt … p a) (lookup_opt … p b).
     241 #A#B#C#choice#a elim a
     242[ normalize #b
     243| #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
     244]
     245#p#choice_good >lookup_opt_map
     246elim (lookup_opt ???)
     247normalize //
     248qed.
     249
     250let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
     251match b with
     252[ pm_leaf ⇒ 0
    196253| pm_node a l r ⇒
    197   match c with
    198   [ pm_leaf ⇒ pm_node A a l r
    199   | pm_node a' l' r' ⇒ pm_node A a' (merge A l l') (merge A r r')
    200   ]
    201 ].
    202 
     254  (match a with
     255   [ Some _ ⇒ 1
     256   | None ⇒ 0
     257   ]) + domain_size A l + domain_size A r
     258].
     259
     260(* just to load notation for 'norm (list.ma's notation overrides core's 'card)*)
     261include "basics/lists/list.ma".
     262interpretation "positive map size" 'norm p = (domain_size ? p).
     263
     264lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
     265#A#B#f#b elim b [//]
     266*[2:#x]#l#r#Hil#Hir normalize
     267[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
     268@le_plus assumption
     269qed.
     270
     271lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
     272#A#B#f#b elim b [//]
     273*[2:#x]#l#r#Hil#Hir normalize
     274>Hil >Hir @refl
     275qed.
     276
     277lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
     278#A#m elim m
     279[#p normalize #F elim (absurd ? (refl ??) F)
     280|* [2: #x]  #l #r #Hil #Hir * normalize
     281  [1,2,3: //
     282  |4:  #F elim (absurd ? (refl ??) F)]
     283  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
     284qed.
     285
     286lemma insert_size : ∀A,p,a,m. |insert A p a m| =
     287  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
     288#A#p elim p
     289[ #a * [2: * [2: #x] #l #r] normalize //
     290|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
     291] qed.
  • src/joint/BEMem.ma

    r1419 r1882  
    4444     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
    4545
     46definition is_addressable : region → bool ≝ λr.match r with
     47  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
     48
     49
     50definition is_address : (beval × beval) → Prop ≝ λa.
     51  ∃p : Σp.bool_to_Prop (is_addressable (ptype p)).∃p0,p1.
     52    \fst a = BVptr p p0 ∧ part_no ? p0 = 0 ∧
     53    \snd a = BVptr p p1 ∧ part_no ? p1 = 1.
     54
     55definition is_addressb : (beval × beval) → bool ≝ λa.
     56  match a with
     57  [ mk_Prod a0 a1 ⇒
     58    match a0 with
     59    [ BVptr p0 part0 ⇒
     60      is_addressable (ptype p0) ∧ eqb part0 0 ∧
     61        match a1 with
     62        [ BVptr p1 part1 ⇒
     63          eq_pointer p0 p1 ∧ eqb part1 1
     64        | _ ⇒ false
     65        ]
     66    | _ ⇒ false
     67    ]
     68  ].
     69
     70lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
     71  (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
     72#P * *
     73[4:|*: [|#b0|#r0#part0] #a1 #_ #Pfalse @Pfalse % * #x * #p0 * #p1 *** #EQ destruct(EQ)]
     74#p0 #part0 #a1
     75whd in match is_addressb; normalize nodelta
     76elim (true_or_false_Prop (is_addressable (ptype p0)))
     77#H >H
     78[ @(eqb_elim part0 0) #Heq
     79  [ cases a1 [|#b0|#r0#part0|#p1#part1] whd in match (?∧?);
     80    [4: @eq_pointer_elim #Heq'
     81      [ @(eqb_elim part1 1) #Heq''
     82        [ #Ptrue #_ @Ptrue destruct
     83          %{p1} [assumption] %{part0} %{part1}
     84          % [ % [ % ]] try % assumption
     85        ]
     86      ]
     87    ]
     88  ]
     89]
     90#_ #Pfalse @Pfalse % ** #p0' #H' * #part0' * #part1' ***
     91#H0 #H1 #H2 #H3 destruct /2 by absurd/
     92qed.
     93
    4694(* CSC: only pointers to XRAM or code memory ATM *)
    4795definition address ≝ beval × beval.
     96definition safe_address ≝ Sig address is_address.
     97unification hint 0 ≔ ;
     98P ≟ Prod beval beval
     99(*------------------*)⊢
     100safe_address ≡ Sig P is_address.
    48101
    49102definition eq_address: address → address → bool ≝
     
    53106definition pointer_of_address: address → res pointer ≝
    54107 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
    55 definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
    56 
    57 definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
     108 
     109definition pointer_of_address_safe : safe_address → pointer ≝
     110  λp.match \fst p return λx.\fst p = x → ? with
     111    [ BVptr ptr _ ⇒ λ_.ptr
     112    | _ ⇒ λabs.⊥
     113    ] (refl …).
     114lapply abs -abs cases p
     115* #a0 #a1 * #x * #p0 * #p1 *** #H0 #H1 #H2 #H3 #H4
     116destruct(H0 H4)
     117qed.
     118
     119definition pointer_compat' ≝ λb,r.
     120  match b with
     121  [ mk_block r' z ⇒
     122    if eq_region r' r then True
     123    else
     124      match r with
     125      [ Any ⇒ True
     126      | XData ⇒ match r' with
     127        [ PData ⇒ True
     128        | _ ⇒ False
     129        ]
     130      | _ ⇒ False
     131      ]
     132   ].
     133
     134lemma pointer_compat_to_ind : ∀b,r.pointer_compat' b r → pointer_compat b r.
     135** #z ** //
     136qed.
     137
     138lemma pointer_compat_from_ind : ∀b,r.pointer_compat b r → pointer_compat' b r.
     139#b #r #H inversion H
     140[ #s #id #EQ1 #EQ2 #EQ3 whd >reflexive_eq_region %
     141| #id #EQ1 #EQ2 #EQ3 %
     142| #r #id #EQ1 #EQ2 #EQ3 whd @eq_region_elim #EQ4 destruct(EQ4) %
     143]
     144qed.
     145
     146lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
     147** #a0 #a1 ***** #r #z #Hr #o * lapply (pointer_compat_from_ind ?? Hr)
     148cases r in Hr ⊢ %; #Hr *
     149** #part0 #H0 ** #part1 #H1 *** #EQa0 #EQpart0 #EQa1 #EQpart1
     150destruct normalize
     151@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     152@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     153#_ #_ normalize %
     154qed.
     155   
     156definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
     157
     158example address_of_pointer_OK_to_safe :
     159  ∀p,a.address_of_pointer p = OK … a → is_address a.
     160#p
     161lapply (refl … p)
     162generalize in match p in ⊢ (???%→%); **
     163whd in match (address_of_pointer ?);
     164#b #H #o #EQp * #a0 #a1
     165normalize #EQ destruct(EQ)
     166%{p} >EQp [1,3: %]
     167% [2,4: % [2,4: % [1,3: % [1,3: %]]]] %
     168qed.
     169
     170definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
     171  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
     172
     173lemma address_of_pointer_is_safe :
     174  ∀p.address_of_pointer p = ! a ← safe_address_of_pointer p ; return (a : address).
     175****#z #H
     176lapply (pointer_compat_from_ind ?? H) * #o
     177normalize %
     178qed.
     179
     180definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝
     181code_pointer_of_beval_pair.
     182
    58183definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
    59184
     185definition safe_address_of_code_pointer: (Σp:pointer. ptype p = Code) → safe_address ≝ address_of_code_pointer.
     186cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
     187lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
     188%{«mk_pointer ? (mk_block Code z) H o,I»}
     189% [2: % [2: % [ % [ % ]] % |]|]
     190qed.
     191
     192(* Paolo: why only code pointers and not XRAM too? *)
    60193definition addr_add: address → nat → res address ≝
    61194 λaddr,n.
     
    65198qed.
    66199
     200definition safe_addr_add: safe_address → nat → res safe_address ≝
     201 λaddr,n.
     202  do ptr ← code_pointer_of_address addr ;
     203  OK … (safe_address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
     204normalize cases ptr #p #E @E
     205qed.
     206
    67207definition addr_sub: address → nat → res address ≝
    68208 λaddr,n.
     
    71211normalize cases ptr #p #E @E
    72212qed.
     213
     214definition safe_addr_sub: safe_address → nat → res safe_address ≝
     215 λaddr,n.
     216  do ptr ← code_pointer_of_address addr ;
     217  OK … (safe_address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
     218normalize cases ptr #p #E @E
     219qed.
  • src/joint/Joint_paolo.ma

    r1644 r1882  
    44include "common/Registers.ma".
    55include "common/Graphs.ma".
     6include "utilities/lists.ma".
     7include "common/LabelledObjects.ma".
     8include "ASM/Util.ma".
    69
    710(* Here is the structure of parameter records (downward edges are coercions,
     
    1215
    1316        lin_params      graph_params
    14           |       \_____ /____   |
    15           |             /     \  |
    16           \_______     /      ↓  ↓
    17                   \   _\____ params
    18                    \_/  \      |
    19                     / \  \     ↓
    20               _____/   unserialized_params
    21              /      _______/   |
    22             /      /           |
    23      stmt_params  /   local_params
    24         |      __/             |
    25     inst_params       funct_params
    26 
    27 inst_params : types needed to define instructions
     17              |   \_____ /____   |
     18              |         /     \  |
     19              |        /      ↓  ↓
     20              |       |      params
     21              |       |        |
     22              |       |   stmt_params
     23              |       |    /   
     24          unserialized_params             
     25            |            \       
     26            |             \     
     27            |         local_params
     28            |              |   
     29    step_params       funct_params
     30
     31step_params : types needed to define steps (stmts with a default fallthrough)
    2832stmt_params : adds successor type needed to define statements
    2933funct_params : types of result register and parameters of function
    3034local_params : adds types of local registers
    31 params : adds type of code and lookup function
    32 graph_params : is made just of inst_params and local_params, and the coercion
    33   to params adds structure common to graph languages *)
    34 
    35 record inst_params : Type[1] ≝
     35params : adds type of code and related properties *)
     36
     37record step_params : Type[1] ≝
    3638 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
    3739 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
     
    4648 ; call_args: Type[0] (* arguments of function calls *)
    4749 ; call_dest: Type[0] (* possible destination of function computation *)
    48  ; ext_instruction: Type[0] (* other instructions not fitting in the general framework *)
    49  ; ext_forall_labels : (label → Prop) → ext_instruction → Prop
    50  ; ext_fin_instruction: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
    51  ; ext_fin_forall_labels : (label → Prop) → ext_fin_instruction → Prop
     50 ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
     51 ; ext_step_labels : ext_step → list label
     52 ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
     53 ; ext_fin_stmt_labels : ext_fin_stmt → list label
    5254 }.
    5355 
    54 inductive joint_instruction (p:inst_params) (globals: list ident): Type[0] ≝
    55   | COMMENT: String → joint_instruction p globals
    56   | COST_LABEL: costlabel → joint_instruction p globals
    57   | MOVE: pair_move p → joint_instruction p globals
    58   | POP: acc_a_reg p → joint_instruction p globals
    59   | PUSH: acc_a_arg p → joint_instruction p globals
    60   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    61   | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals
    62   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    63   | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
     56inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
     57  | COMMENT: String → joint_step p globals
     58  | COST_LABEL: costlabel → joint_step p globals
     59  | MOVE: pair_move p → joint_step p globals
     60  | POP: acc_a_reg p → joint_step p globals
     61  | PUSH: acc_a_arg p → joint_step p globals
     62  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
     63  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
     64  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
     65  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
    6466  (* int done with generic move *)
    65 (*| INT: generic_reg p → Byte → joint_instruction p globals *)
    66   | CLEAR_CARRY: joint_instruction p globals
    67   | SET_CARRY: joint_instruction p globals
    68   | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
    69   | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals
    70   | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
    71   | COND: acc_a_reg p → label → joint_instruction p globals
    72   | extension: ext_instruction p → joint_instruction p globals.
    73 
    74 coercion extension_to_instruction :
    75   ∀p,globals.∀c : ext_instruction p.joint_instruction p globals ≝
    76   extension
    77   on _c : ext_instruction ? to joint_instruction ??.
    78 
    79 notation "r ← a1 .op. a2" with precedence 50 for
     67(*| INT: generic_reg p → Byte → joint_step p globals *)
     68  | CLEAR_CARRY: joint_step p globals
     69  | SET_CARRY: joint_step p globals
     70  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
     71  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
     72  | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
     73  | COND: acc_a_reg p → label → joint_step p globals
     74  | extension: ext_step p → joint_step p globals.
     75
     76notation "r ← a1 .op. a2" with precedence 55 for
    8077  @{'op2 $op $r $a1 $a2}.
    81 notation "r ← . op . a" with precedence 50 for
     78notation "r ← . op . a" with precedence 55 for
    8279  @{'op1 $op $r $a}.
    83 notation "r ← a" with precedence 50 for
     80notation "r ← a" with precedence 55 for
    8481  @{'mov $r $a}. (* to be set in individual languages *)
    8582notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
     
    9087interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    9188
    92 
    93 definition inst_forall_labels : ∀p : inst_params.∀globals.
    94     (label → Prop) → joint_instruction p globals → Prop ≝
    95 λp,g,P,inst. match inst with
    96   [ COND _ l ⇒ P l
    97   | extension ext_s ⇒ ext_forall_labels p P ext_s
    98   | _ ⇒ True
    99  ].
    100 
     89coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
     90  extension on _s : ext_step ? to joint_step ??.
     91
     92definition step_labels ≝
     93  λp, globals.λs : joint_step p globals.
     94    match s with
     95    [ COND _ l ⇒ [l]
     96    | extension ext_s ⇒ ext_step_labels ? ext_s
     97    | _ ⇒ [ ]
     98    ].
     99
     100definition step_forall_labels : ∀p : step_params.∀globals.
     101    (label → Prop) → joint_step p globals → Prop ≝
     102λp,g,P,inst. All … P (step_labels … inst).
     103 
    101104record funct_params : Type[1] ≝
    102105  { resultT : Type[0]
     
    109112 }.
    110113
     114
    111115record unserialized_params : Type[1] ≝
    112  { u_inst_pars :> inst_params
     116 { u_inst_pars :> step_params
    113117 ; u_local_pars :> local_params
    114118 }.
    115119
    116120record stmt_params : Type[1] ≝
    117   { unserialized_pars :> unserialized_params
     121  { uns_pars :> unserialized_params
    118122  ; succ : Type[0]
    119   ; succ_forall_labels : (label → Prop) → succ → Prop
     123  ; succ_label : succ → option label
    120124  }.
    121125
    122126inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    123   | sequential: joint_instruction p globals → succ p → joint_statement p globals
     127  | sequential: joint_step p globals → succ p → joint_statement p globals
    124128  | GOTO: label → joint_statement p globals
    125129  | RETURN: joint_statement p globals
    126   | extension_fin : ext_fin_instruction p → joint_statement p globals.
    127 
    128 coercion extension_fin_to_statement :
    129   ∀p : stmt_params.∀globals.∀c : ext_fin_instruction p.joint_statement p globals ≝
    130   extension_fin
    131   on _c : ext_fin_instruction ? to joint_statement ??.
     130  | extension_fin : ext_fin_stmt p → joint_statement p globals.
     131
     132coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
     133  extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
     134
     135definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
     136  match s with
     137  [ sequential _ _ ⇒ False
     138  | _ ⇒ True
     139  ].
    132140
    133141record params : Type[1] ≝
    134142 { stmt_pars :> stmt_params
    135143 ; codeT: list ident → Type[0]
    136  ; code_has_label: ∀globals.codeT globals → label → Prop
    137  ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) →
    138     codeT globals → Prop
     144 ; code_point : Type[0]
     145 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
     146 ; point_of_label : ∀globals.codeT globals → label → option code_point
     147 ; point_of_succ : code_point → succ stmt_pars → code_point
    139148 }.
    140149
    141 
    142 definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    143     (label → Prop) → joint_statement p globals → Prop ≝
    144   λp,g,P,stmt. match stmt with
    145   [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next
    146   | GOTO l ⇒ P l
    147   | RETURN ⇒ True
    148   | extension_fin c ⇒ ext_fin_forall_labels … P c
     150definition code_has_point ≝
     151  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
     152
     153interpretation "code membership" 'mem p c = (code_has_point ?? c p).
     154
     155definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
     156unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
     157
     158definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
     159  match pt with
     160  [ mk_Sig pt' pt_prf ⇒
     161    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
     162    [ Some x ⇒ λ_.x
     163    | None ⇒ λabs.⊥
     164    ] (refl …)
     165  ]. normalize in pt_prf;
     166    >abs in pt_prf; // qed.
     167
     168definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
     169  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
     170
     171definition forall_statements_i :
     172  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
     173    codeT p globals → Prop  ≝
     174  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
     175
     176lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
     177#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     178
     179lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
     180  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
     181#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     182
     183definition code_has_label ≝ λp,globals,c,l.
     184  match point_of_label p globals c l with
     185  [ Some pt ⇒ code_has_point … c pt
     186  | None ⇒ false
    149187  ].
     188
     189definition stmt_explicit_labels :
     190  ∀p,globals.
     191  joint_statement p globals → list label ≝
     192  λp,globals,stmt. match stmt with
     193  [ sequential c _ ⇒ step_labels … c
     194  | GOTO l ⇒ [ l ]
     195  | RETURN ⇒ [ ]
     196  | extension_fin c ⇒ ext_fin_stmt_labels … c
     197  ].
     198
     199definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
     200  option label ≝
     201 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
     202 
     203definition stmt_labels : ∀p : stmt_params.∀globals.
     204    joint_statement p globals → list label ≝
     205  λp,g,stmt.
     206  (match stmt_implicit_label … stmt with
     207     [ Some l ⇒ [l]
     208     | None ⇒ [ ]
     209     ]) @ stmt_explicit_labels … stmt.
     210
     211definition stmt_forall_labels ≝
     212  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
     213  All … P (stmt_labels … s).
     214
     215lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
     216  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
     217#p#globals#P #s
     218whd in ⊢ (% → ?);
     219whd in ⊢ (???% → ?);
     220elim (stmt_implicit_label ???) [2: #next * #_] //
     221qed.
     222
     223lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
     224  stmt_forall_labels … P s →
     225    opt_All … P (stmt_implicit_label … s).
     226#p#globals#P#s
     227whd in ⊢ (% → ?);
     228whd in ⊢ (???% → ?);
     229elim (stmt_implicit_label ???)
     230[ //
     231| #next * #Pnext #_ @Pnext
     232]
     233qed.
     234
     235definition code_forall_labels ≝
     236  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
     237
     238lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
     239  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
     240  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
    150241
    151242record lin_params : Type[1] ≝
    152243  { l_u_pars :> unserialized_params }.
    153 
    154 include "utilities/option.ma".
     244 
     245lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     246#tag #A #lbl #l elim l [*]
     247** [2: #id] #a #tl #IH
     248[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
     249  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
     250  @eq_identifier_elim #Heq normalize nodelta
     251  [ #_ normalize / by /]
     252| whd in ⊢ (?%→?%?);
     253]
     254#H >(index_of_label_from_internal … H)
     255@le_S_S @(IH H)
     256qed.
     257
     258(* mv *)
     259lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
     260#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
     261#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
     262qed.
     263
     264lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
     265#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
     266#n' #H @le_S_S @(IH … H)
     267qed.
     268
     269lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
     270#A #l elim l
     271[ #n #ABS @⊥ /2 by absurd/
     272| #hd #tl #IH * normalize //
     273]
     274qed.
    155275
    156276definition lin_params_to_params ≝
    157277  λlp : lin_params.
    158278     mk_params
    159       (mk_stmt_params lp unit (λ_.λ_.True))
     279      (mk_stmt_params lp unit (λ_.None ?))
    160280    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    161     (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
    162         (λl_stmt. \fst l_stmt = Some ? lbl) code)
    163     (* forall_statements ≝ *)(λglobals,P,code.All ?
    164         (λl_stmt. P (\snd l_stmt)) code).
     281    (* code_point ≝ *)ℕ
     282    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
     283    (* point_of_label ≝ *)(λglobals,c,lbl.
     284      If occurs_exactly_once ?? lbl c then with prf do
     285        return index_of_label ?? lbl c
     286      else
     287        None ?)
     288    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
    165289
    166290coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
    167291  on _lp : lin_params to params.
     292 
     293lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     294  ∀pt.pt ∈ code = leb (S pt) (|code|).
     295#lp #globals #code elim code
     296[ #pt %
     297| #hd #tl #IH * [%]
     298  #n @IH
     299]qed.
     300
     301lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     302  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
     303#lp #globals #code #lbl
     304whd in match (code_has_label ????);
     305whd in match (point_of_label ????);
     306elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
     307#Heq >Heq normalize nodelta
     308[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
     309  #ABS elim(absurd ?? ABS) -ABS
     310  @index_of_label_length assumption ]] %
     311qed.
    168312
    169313record graph_params : Type[1] ≝
    170314  { g_u_pars :> unserialized_params }.
     315
     316(* move *)
     317definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
     318  λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
     319  [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
     320    [ an_identifier i' ⇒
     321      match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
     322      [ Some y ⇒ λ_.y
     323      | None ⇒ Ⓧ
     324      ]
     325    ]
     326  ].
     327 
     328lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
     329  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
     330#tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
     331[ * ]
     332#s * #H @H %
     333qed.
    171334
    172335(* One common instantiation of params via Graphs of joint_statements
     
    175338  λgp : graph_params.
    176339     mk_params
    177       (mk_stmt_params gp label (λP.P))
     340      (mk_stmt_params gp label (Some ?))
    178341    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    179     (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
    180     (* forall_statements ≝ *)(λglobals,P,code.
    181       ∀l,s.lookup … code l = Some ? s → P s).
    182    
     342    (* code_point ≝ *)label
     343    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
     344    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
     345    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
     346
    183347coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
    184348on _gp : graph_params to params.
    185    
    186 
    187 definition labels_present : ∀globals.∀p : params.
    188   codeT p globals → (joint_statement p globals) → Prop ≝
    189 λglobals,p,code,s. stmt_forall_labels p globals
    190   (λl.code_has_label ?? code l) s.
     349
     350lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     351  ∀pt.code_has_point … code pt = mem_set … code pt.
     352#gp#globals*#m*#i % qed.
     353
     354lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     355  ∀lbl.code_has_label … code lbl = mem_set … code lbl.
     356#gp #globals * #m * #i % qed.
     357
     358definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
     359  λs : joint_statement p globals.
     360  match s with
     361  [ sequential _ n ⇒ P n
     362  | _ ⇒ True
     363  ].
     364
     365definition statement_closed : ∀globals.∀p : params.
     366  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
     367λglobals,p,code,pt,s.
     368  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
     369  stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
    191370
    192371definition code_closed : ∀p : params.∀globals.
    193372  codeT p globals → Prop ≝ λp,globals,code.
    194     forall_statements … (labels_present … code) code.
     373    forall_statements_i … (statement_closed … code) code.
    195374
    196375(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
    197376definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
    198   (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).
     377  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
    199378
    200379record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
     
    206385  joint_if_result   : resultT p;
    207386  joint_if_params   : paramsT p;
    208   joint_if_locals   : localsT p;
     387  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
    209388(*CSC: XXXXX stacksize unused for LTL-...*)
    210389  joint_if_stacksize: nat;
    211390  joint_if_code     : codeT p globals ;
    212 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    213   joint_if_entry    : Σl: label. code_has_label … joint_if_code l;
    214 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    215   joint_if_exit     : Σl: label. code_has_label …  … joint_if_code l
     391  joint_if_entry : point_in_code … joint_if_code ;
     392  joint_if_exit : point_in_code … joint_if_code
    216393}.
    217394
     
    219396  λglobals,p.
    220397    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
    221 
    222 (* Currified form *)
    223 definition set_joint_if_exit ≝
    224   λglobals,pars.
    225   λexit: label.
    226   λp:joint_internal_function globals pars.
    227   λprf: code_has_label … (joint_if_code … p) exit.
    228    mk_joint_internal_function globals pars
    229     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    230     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    231     (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
    232398
    233399definition set_joint_code ≝
     
    244410
    245411definition set_joint_if_graph ≝
    246   λglobals,pars.
     412  λglobals.λpars : graph_params.
    247413  λgraph.
    248414  λp:joint_internal_function globals pars.
    249   λentry_prf: code_has_label … graph (joint_if_entry … p).
    250   λexit_prf: code_has_label … graph (joint_if_exit … p).
     415  λentry_prf.
     416  λexit_prf.
    251417    set_joint_code globals pars p
    252418      graph
    253       (mk_Sig … (joint_if_entry … p) entry_prf)
    254       (mk_Sig … (joint_if_exit p) exit_prf).
     419      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
     420      (mk_Sig … (joint_if_exit ?? p) exit_prf).
    255421
    256422definition set_luniverse ≝
     
    272438    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    273439   
    274 (* Paolo: probably should move these elsewhere *)
    275 definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?.
    276 definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X.
    277   graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l.
    278   mk_Sig … (pi1 ?? sig_l) ?.
    279 @graph_add_lookup
    280 @(pi2 … sig_l)
    281 qed.
    282 
    283440(* Specialized for graph_params *)
    284441definition add_graph ≝
     
    290447     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    291448     code
    292      (graph_dom_add_incl … (joint_if_entry … p))
    293      (graph_dom_add_incl … (joint_if_exit … p)).
     449     (pi1 … (joint_if_entry … p))
     450     (pi1 … (joint_if_exit … p)).
     451>graph_code_has_point whd in match code; >mem_set_add
     452@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
     453#x #H <graph_code_has_point @H
     454qed.
    294455
    295456definition set_locals ≝
  • src/joint/TranslateUtils_paolo.ma

    r1643 r1882  
    55(* type T is the syntactic type of the generated things *)
    66(* (sig for RTLabs registers, unit in others ) *)
    7 definition freshT ≝ λg.λpars : params.λX,T : Type[0].
    8    T → state_monad (joint_internal_function … g pars) X.
     7definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).
    98
    109definition rtl_ertl_fresh_reg:
    1110 ∀inst_pars,funct_pars,globals.
    12   freshT globals (rtl_ertl_params inst_pars funct_pars) register unit
    13   λinst_pars,var_pars,globals,it,def.
     11  freshT globals (rtl_ertl_params inst_pars funct_pars) register
     12  λinst_pars,var_pars,globals,def.
    1413    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    1514    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
    1615
     16include alias "basics/lists/list.ma".
    1717let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
    18   freshT globals (rtl_ertl_params inst_pars funct_pars) (list register) unit ≝
    19   match n with
    20   [ O ⇒ λ_. return [ ]
    21   | S n' ⇒ λ_.
    22     ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n' it;
    23     ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals it;
    24     return (reg :: regs')
    25   ].
    26 
    27 lemma rtl_ertl_fresh_regs_length:
    28  ∀i_pars,f_pars,globals.∀def: joint_internal_function … globals
    29   (rtl_ertl_params i_pars f_pars). ∀n: nat.
    30   |(\snd (rtl_ertl_fresh_regs … n it def))| = n.
    31  #ipars#fpars #globals #def #n elim n
    32   [ %
    33   | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
    34     #def' #regs #EQ>EQ
    35     whd in ⊢ (? → ??(??(???%))?); @pair_elim #def'' #reg #_ normalize // ]
    36 qed.
    37 
    38 definition rtl_ertl_fresh_regs_strong:
    39  ∀i_pars,f_pars,globals. joint_internal_function … globals (rtl_ertl_params i_pars f_pars) →
    40   ∀n: nat. Σregs: (joint_internal_function … globals (rtl_ertl_params i_pars f_pars)) × (list register). |\snd regs| = n ≝
    41  λi_pars,f_pars,globals,def,n.rtl_ertl_fresh_regs i_pars f_pars globals n it def. //
    42 qed.
     18  freshT globals (rtl_ertl_params inst_pars funct_pars)
     19    (Σl : list register. |l| = n) ≝
     20  let ret_type ≝ (Σl : list register. |l| = n) in
     21  match n  return λx.x = n → freshT … ret_type with
     22  [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
     23  | S n' ⇒ λeq'.
     24    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
     25    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
     26    return (mk_Sig … (reg :: regs') ?)
     27  ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
     28  qed.
    4329
    4430definition fresh_label:
    45  ∀g_pars,globals.freshT globals g_pars label unit
    46   λg_pars,globals,it,def.
     31 ∀g_pars,globals.freshT globals g_pars label
     32  λg_pars,globals,def.
    4733    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
    4834     〈set_luniverse … def luniverse, r〉.
     
    5238  (g_pars: graph_params)
    5339  (globals: list ident)
    54   (insts: list (joint_instruction g_pars globals))
     40  (insts: list (joint_step g_pars globals))
    5541  (src : label)
    5642  (dest : label)
     
    6349      add_graph … src (sequential … instr dest) def
    6450    | _ ⇒ (* need to generate label *)
    65       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     51      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    6652      adds_graph g_pars globals others tmp_lbl dest
    6753        (add_graph … src (sequential … instr tmp_lbl) def)
     
    7258  ∀g_pars: graph_params.
    7359  ∀globals: list ident.
    74   (* type of allocatable registers and of their types (unit if not in RTLabs) *)
    75   ∀R,T : Type[0].
    7660  (* fresh register creation *)
    77   freshT globals g_pars R T
    78   ∀insts: bind_list R T (joint_instruction g_pars globals).
     61  freshT globals g_pars (localsT … g_pars)
     62  ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals).
    7963  ∀src : label.
    8064  ∀dest : label.
    8165  joint_internal_function globals g_pars →
    8266  joint_internal_function globals g_pars ≝
    83   λg_pars,globals,T,R,fresh_r,insts,src,dest,def.
     67  λg_pars,globals,fresh_r,insts,src,dest,def.
    8468  let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in
    8569  adds_graph … stmts src dest def'.
     
    8973  ∀src_g_pars,dst_g_pars : graph_params.
    9074  ∀globals: list ident.
    91   (* type of allocatable registers (unit if not in RTLabs) *)
    92   ∀T : Type[0].
    9375  (* fresh register creation *)
    94   freshT globals dst_g_pars (localsT dst_g_pars) T
     76  freshT globals dst_g_pars (localsT dst_g_pars)
    9577  (* function dictating the translation *)
    96   (label → joint_instruction src_g_pars globals →
    97     bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
     78  (label → joint_step src_g_pars globals →
     79    bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals)
    9880    (* this can be added to allow redirections: × label *)) →
    99   (label → ext_fin_instruction src_g_pars →
    100     (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals))
    101     ×
    102     (joint_statement dst_g_pars globals)) →
     81  (label → ext_fin_stmt src_g_pars →
     82     bind_new (localsT dst_g_pars)
     83      ((list (joint_step dst_g_pars globals))
     84      ×
     85      (joint_statement dst_g_pars globals))) →
    10386  (* initialized function definition with empty graph *)
    10487  joint_internal_function globals dst_g_pars →
     
    10790  (* destination function *)
    10891  joint_internal_function globals dst_g_pars ≝
    109   λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,trans',empty,def.
     92  λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def.
    11093  let f : label → joint_statement (src_g_pars : params) globals →
    11194    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     
    11598    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    11699    | RETURN ⇒ add_graph … lbl (RETURN …) def
    117     | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
    118       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
    119       b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def)
     100    | extension_fin c ⇒
     101      let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in
     102      let 〈insts, fin〉 ≝ p in
     103      let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in
     104      adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def)
    120105    ] in
    121106  foldi … f (joint_if_code … def) empty.
    122 
    123 definition b_graph_translate_no_fin :
    124   ∀src_g_pars : graph_params.
    125   ext_fin_instruction src_g_pars = void →
    126   ∀dst_g_pars : graph_params.
    127   ∀globals: list ident.
    128   (* type of allocatable registers (unit if not in RTLabs) *)
    129   ∀T : Type[0].
    130   (* fresh register creation *)
    131   freshT globals dst_g_pars (localsT dst_g_pars) T →
    132   (* function dictating the translation *)
    133   (label → joint_instruction src_g_pars globals →
    134     bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
    135     (* this can be added to allow redirections: × label *)) →
    136   (* initialized function definition with empty graph *)
    137   joint_internal_function globals dst_g_pars →
    138   (* source function *)
    139   joint_internal_function globals src_g_pars →
    140   (* destination function *)
    141   joint_internal_function globals dst_g_pars ≝
    142   λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans.
    143     b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg
    144       trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
    145107 
    146108(* translation without register allocation *)
     
    149111  ∀globals: list ident.
    150112  (* function dictating the translation *)
    151   (label → joint_instruction src_g_pars globals →
    152     list (joint_instruction dst_g_pars globals)) →
    153   (label → ext_fin_instruction src_g_pars →
    154     (list (joint_instruction dst_g_pars globals))
     113  (label → joint_step src_g_pars globals →
     114    list (joint_step dst_g_pars globals)) →
     115  (label → ext_fin_stmt src_g_pars →
     116    (list (joint_step dst_g_pars globals))
    155117    ×
    156118    (joint_statement dst_g_pars globals)) →
     
    171133    | RETURN ⇒ add_graph … lbl (RETURN …) def
    172134    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
    173       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     135      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    174136      adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    175137    ] in
    176138  foldi ??? f (joint_if_code ?? def) empty.
     139
     140definition graph_to_lin_statement :
     141  ∀p : unserialized_params.∀globals.
     142  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
     143  λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globals with
     144  [ sequential c _ ⇒ sequential … c it
     145  | GOTO l ⇒ GOTO … l
     146  | RETURN ⇒ RETURN …
     147  | extension_fin c ⇒ extension_fin … c
     148  ].
     149
     150lemma graph_to_lin_labels :
     151  ∀p : unserialized_params.∀globals,s.
     152  stmt_labels … (graph_to_lin_statement p globals s) =
     153  stmt_explicit_labels … s.
     154#p#globals * //
     155qed.
     156
     157(* in order to make the coercion from lists to sets to work, one needs these hints *)
     158unification hint 0 ≔ ;
     159X ≟ identifier LabelTag
     160
     161list label ≡ list X.
     162
     163unification hint 0 ≔ ;
     164X ≟ identifier RegisterTag
     165
     166list register ≡ list X.
     167
     168   
     169definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
     170definition hide_Prop : Prop → Prop ≝ λP.P.
     171
     172interpretation "hide proof" 'hide p = (hide_prf ? p).
     173interpretation "hide Prop" 'hide p = (hide_Prop p).
     174
     175(* discard all elements failing test, return first element succeeding it *)
     176(* and the rest of the list, if any. *)
     177let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
     178  match l with
     179  [ nil ⇒ None ?
     180  | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l'
     181  ].
     182
     183lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr →
     184  let x ≝ \fst pr in
     185  let post ≝ \snd pr in
     186  ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x).
     187#A#f#l elim l
     188[ normalize * #x #post #EQ destruct
     189| #y #l' #Hi * #x #post
     190  normalize elim (true_or_false_Prop (f y)) #fy >fy normalize
     191  #EQ
     192  [ destruct >fy %{[ ]} /3 by refl, conj, I/
     193  | elim (Hi … EQ) #pre ** #prefalse #chopd #fx
     194    %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx]
     195  ]
     196]
     197qed.
     198
     199lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l.
     200#A#f#l elim l
     201[ normalize #_ %
     202| #y #l' #Hi normalize
     203  elim (true_or_false_Prop (f y)) #fy >fy normalize
     204  #EQ
     205  [ destruct
     206  | /3 by conj, nmk/
     207  ]
     208]
     209qed.
     210
     211unification hint 0 ≔ p, globals;
     212lp ≟ lin_params_to_params p,
     213sp ≟ stmt_pars lp,
     214js ≟ joint_statement sp globals,
     215lo ≟ labelled_obj LabelTag js
     216(*----------------------------*)⊢
     217list lo ≡ codeT lp globals.
     218
     219definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
     220  λentry : label.
     221  (Σ〈visited'   : identifier_map LabelTag ℕ,
     222   required'  : identifier_set LabelTag,
     223   generated' : codeT (mk_lin_params p) globals〉.'hide (
     224      And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited'))
     225        (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated'))
     226        (∀l,n.lookup ?? visited' l = Some ? n →
     227          And (code_has_label … (rev ? generated') l)
     228            (∃s.And (And
     229              (lookup … g l = Some ? s)
     230              (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
     231              (opt_All ?
     232                (λnext.Or (lookup … visited' next = Some ? (S n))
     233                  (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
     234                (stmt_implicit_label … s)))))).
     235               
     236unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.
     237
     238let rec graph_visit
     239  (p : unserialized_params)
     240  (globals: list ident)
     241  (g : codeT (mk_graph_params p) globals)
     242  (* = graph (joint_statement (mk_graph_params p) globals *)
     243  (required: identifier_set LabelTag)
     244  (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
     245  (generated: codeT (mk_lin_params p) globals)
     246  (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
     247  (visiting: list label)
     248  (gen_length : ℕ)
     249  (n: nat)
     250  (entry : label)
     251  (g_prf : code_closed … g)
     252  (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited)))
     253  (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated)
     254  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
     255    And (code_has_label … (rev ? generated) l)
     256    (∃s.And (And
     257      (lookup … g l = Some ? s)
     258      (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
     259      (opt_All ? (λnext.match lookup … visited next with
     260                     [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
     261                     | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
     262  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
     263  (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting)
     264  (gen_length_prf : gen_length = length ? generated)
     265  (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
     266                  (lookup … visited entry = Some ? 0))
     267  (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
     268  on n
     269  : graph_visit_ret_type … g entry ≝
     270  match chop ? (λx.¬x∈visited) visiting
     271  return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with
     272  [ None ⇒ λeq_chop.
     273    let H ≝ chop_miss … eq_chop in
     274    mk_Sig … 〈visited, required, generated〉 ?
     275  | Some pr ⇒ λeq_chop.
     276    let vis_hd ≝ \fst pr in
     277    let vis_tl ≝ \snd pr in
     278    let H ≝ chop_hit ???? eq_chop in
     279    match n return λx.x = n → graph_visit_ret_type … g entry with
     280    [ O ⇒ λeq_n.⊥
     281    | S n' ⇒ λeq_n.
     282      (* add the label to the visited ones *)
     283      let visited' ≝ add … visited vis_hd gen_length in
     284      (* take l's statement *)
     285      let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in 
     286      (* translate it to its linear version *)
     287      let translated_statement ≝ graph_to_lin_statement p globals statement in
     288      (* add the translated statement to the code (which will be reversed later) *)
     289      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
     290      let required' ≝ stmt_explicit_labels … statement ∪ required in
     291      (* put successors in the visiting worklist *)
     292      let visiting' ≝ stmt_labels … statement @ vis_tl in
     293      (* finally, check the implicit successor *)
     294      (* if it has been already visited, we need to add a GOTO *)
     295      let add_req_gen ≝ match stmt_implicit_label … statement with
     296        [ Some next ⇒
     297          if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉
     298        | None ⇒ 〈0, ∅, [ ]〉
     299        ] in
     300      graph_visit ???
     301        (\snd (\fst add_req_gen) ∪ required')
     302        visited'
     303        (\snd add_req_gen @ generated')
     304        visiting'
     305        (\fst (\fst add_req_gen) + S(gen_length))
     306        n' entry g_prf ????????
     307    ] (refl …)
     308  ] (refl …).
     309whd
     310[ (* base case, visiting is all visited *)
     311  %[
     312    %[
     313      %[
     314        elim entry_prf
     315        [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis
     316          * #ABS elim (ABS I)
     317        | //
     318        ]
     319      | #l #l_req
     320        elim (required_prf1 … l_req) #G
     321        [ lapply (All_In … H G) #H >(notb_false ? H) %
     322        | assumption
     323        ]
     324      ]
     325    | assumption
     326    ]
     327   | #l #n #H elim (generated_prf1 … H)
     328      #H1 * #s ** #H2 #H3 #H4
     329      % [assumption] %{s} %
     330      [% assumption
     331      | @(opt_All_mp … H4) -l #l
     332        lapply (in_map_domain … visited l)
     333        elim (true_or_false (l∈visited)) #l_vis >l_vis
     334        normalize nodelta [ * #n' ] #EQlookup >EQlookup
     335        normalize nodelta *
     336        [ #EQn' % >EQn' %
     337        | #H %2{H}
     338        | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I)
     339        ]
     340      ]
     341    ]
     342|*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ]
     343(* first, close goals where add_gen_req plays no role *)
     344[10: (* vis_hd is in g *) @(All_split … visiting_prf … H2)
     345|1: (* n = 0 absrud *)
     346  @(absurd … n_prf)
     347  @lt_to_not_le
     348  <eq_n
     349  lapply (add_size … visited vis_hd 0 (* dummy value *))
     350  >(notb_true … H3)
     351  whd in match (if ? then ? else ?);
     352  whd in match (? + ?);
     353  whd in match (lt ? ?);
     354  #EQ <EQ @subset_card @add_subset
     355  [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
     356    #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) %
     357  | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H)
     358    generalize in match (opt_safe ???); #n #l_is_n
     359    elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g
     360    elim g #mg  whd in ⊢ (?→?%); #H >H whd %
     361  ]
     362|6:
     363  @All_append
     364  [ @(g_prf … vis_hd) <opt_to_opt_safe %
     365  | >H2 in visiting_prf;
     366    #H' lapply (All_append_r … H') -H' * #_ //
     367  ]
     368|8:
     369  %2 elim entry_prf
     370  [ ** >H2 cases pre
     371    [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
     372      cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
     373    |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_
     374      >lookup_add_hit >eq_gen_length %
     375    ]
     376  | #lookup_entry cut (entry ≠ vis_hd)
     377    [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis
     378      lapply (in_map_domain … visited entry) >(notb_true … entry_vis)
     379      normalize nodelta >lookup_entry #ABS destruct(ABS)]
     380    #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
     381  ]
     382|9:
     383  >commutative_plus
     384  >add_size >(notb_true … H3) normalize nodelta
     385  whd in match (? + ?);
     386  >commutative_plus
     387  change with (? ≤ S(?) + ?)
     388  >eq_n assumption
     389|*: (* where add_gen_req does matter, expand the three possible cases *)
     390  lapply (refl … add_req_gen)
     391  whd in ⊢ (???%→?);
     392  lapply (refl … (stmt_implicit_label … statement))
     393  (* BUG *)
     394  [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     395  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     396  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     397  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     398  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     399  ]
     400  *[2,4,6,8,10: #next]
     401  #EQimpl
     402  whd in ⊢ (???%→?);
     403  [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis
     404    whd in ⊢ (???%→?);]
     405  #EQ_req_gen >EQ_req_gen
     406  (* these are the cases, reordering them *)
     407  [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ]
     408  [1,2,3: #i >mem_set_union
     409    [ #H elim (orb_Prop_true … H) -H
     410      [ #H >(mem_set_singl_to_eq … H) %2{next_vis}]
     411    |*: >mem_set_empty whd in match (false ∨ ?);
     412    ]
     413    >mem_set_union
     414    #H elim(orb_Prop_true … H) -H
     415    [1,3,5: (* i is an explicit successor *)
     416      #i_succ
     417      (* if it's visited it's ok *)
     418      elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis
     419      [1,3,5: %2 %
     420      |*: %
     421        @Exists_append_l
     422        whd in match (stmt_labels ???);
     423        @Exists_append_r
     424        @mem_list_as_set
     425        @i_succ
     426      ]
     427    |2,4,6: (* i was already required *)
     428      #i_req
     429      elim (required_prf1 … i_req)
     430      [1,3,5: >H2 #H elim (Exists_append … H) -H
     431        [1,3,5: (* i in preamble → i∈visited *)
     432          #i_pre %2 >mem_set_add @orb_Prop_r
     433          lapply (All_In … H1 i_pre)
     434          #H >(notb_false … H) %
     435        |*: *
     436          [1,3,5: (* i is vis_hd *)
     437            #eq_i >eq_i %2 @mem_set_add_id
     438          |*: (* i in vis_tl → i∈visiting' *)
     439            #i_post % @Exists_append_r assumption
     440          ]
     441        ]
     442      |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption
     443      ]
     444    ]
     445  |4,5,6:
     446    [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]]
     447    whd in match (? @ ?); %
     448    [1,3,5:
     449      whd
     450      >graph_to_lin_labels
     451      change with (All ?? (stmt_explicit_labels ?? statement))
     452      whd in match required';
     453      generalize in match (stmt_explicit_labels … statement);
     454      #l @list_as_set_All
     455      #i >mem_set_union >mem_set_union
     456      #i_l @orb_Prop_r @orb_Prop_l @i_l
     457    |*: @(All_mp … required_prf2)
     458      * #l_opt #s @All_mp
     459      #l #l_req >mem_set_union @orb_Prop_r
     460      >mem_set_union @orb_Prop_r @l_req
     461    ]
     462  |7,8,9:
     463    #i whd in match visited';
     464    @(eq_identifier_elim … i vis_hd)
     465    [1,3,5: #EQi >EQi #pos
     466      >lookup_add_hit #EQpos cut (gen_length = pos)
     467        [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
     468        -EQpos #EQpos <EQpos -pos
     469      %
     470      [1,3,5: whd in match (rev ? ?);
     471        >rev_append_def
     472        whd
     473        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     474          <associative_append >occurs_exactly_once_None]
     475        >occurs_exactly_once_Some_eq >eq_identifier_refl
     476        normalize nodelta
     477        @generated_prf2
     478        lapply (in_map_domain … visited vis_hd)
     479        >(notb_true … H3) normalize nodelta //
     480      |*: %{statement}
     481        %
     482        [1,3,5: %
     483          [1,3,5:
     484           change with (? = Some ? (opt_safe ???))
     485           @opt_safe_elim #s //
     486          |*: whd in match (rev ? ?);
     487            >rev_append_def
     488            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     489              <associative_append @nth_opt_append_hit_l ]
     490            >nth_opt_append_r
     491            >rev_length
     492            <gen_length_prf
     493            [1,3,5: <minus_n_n] %
     494          ]
     495        |*: >EQimpl whd [3: %]
     496          >mem_set_add in next_vis;
     497          @eq_identifier_elim
     498          [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)]
     499            >lookup_add_hit
     500          |*: #NEQ >(lookup_add_miss … visited … NEQ)
     501            whd in match (false ∨ ?);
     502            #next_vis lapply(in_map_domain … visited next) >next_vis
     503            whd in ⊢ (% → ?); [ * #s ]
     504            #EQlookup >EQlookup
     505          ] whd
     506          [1,2: %2
     507            >rev_append >nth_opt_append_r
     508            >rev_length whd in match generated';
     509            whd in match (|? :: ?|); <gen_length_prf
     510            [1,3: <minus_n_n ] %
     511          |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
     512            >EQimpl %
     513          ]
     514        ]
     515      ]
     516    |*:
     517      #NEQ #n_i >(lookup_add_miss … visited … NEQ)
     518      #Hlookup elim (generated_prf1 … Hlookup)
     519      #G1 * #s ** #G2 #G3 #G4
     520      %
     521      [1,3,5: whd in match (rev ??);
     522        >rev_append_def whd
     523        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     524          <associative_append >occurs_exactly_once_None]
     525        >occurs_exactly_once_Some_eq
     526        >eq_identifier_false
     527        [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %]
     528        normalize nodelta
     529        assumption
     530      |*: %{s}
     531        %
     532        [1,3,5: %
     533          [1,3,5: assumption
     534          |*: whd in match (rev ??); >rev_append_def
     535            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     536              <associative_append @nth_opt_append_hit_l ]
     537            @nth_opt_append_hit_l assumption
     538          ]
     539        |*: @(opt_All_mp … G4)
     540          #x
     541          @(eq_identifier_elim … x vis_hd) #Heq
     542          [1,3,5: >Heq
     543            lapply (in_map_domain … visited vis_hd)
     544            >(notb_true … H3)
     545           normalize nodelta #EQlookup >EQlookup normalize nodelta
     546           * #nth_opt_visiting #gen_length_eq
     547           >lookup_add_hit normalize nodelta %
     548           >gen_length_eq %
     549          |*: >(lookup_add_miss ?????? Heq)
     550            lapply (in_map_domain … visited x)
     551            elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta
     552            [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta *
     553            [1,3,5: #G %{G}
     554            |2,4,6: #G %2 whd in match (rev ??); >rev_append_def
     555              [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     556              <associative_append @nth_opt_append_hit_l ]
     557              @nth_opt_append_hit_l assumption
     558            |*: #G elim(absurd ?? Heq)
     559              (* BUG (but useless): -required -g -generated *)
     560               >H2 in G; #G
     561              lapply (refl … (nth_opt ? 0 pre))
     562              (* BUG *)
     563              [generalize in ⊢ (???%→?);
     564              |generalize in ⊢ (???%→?);
     565              |generalize in ⊢ (???%→?);
     566              ] *
     567              [1,3,5: #G' >(nth_opt_append_miss_l … G') in G;
     568                change with (Some ? vis_hd = ? → ?)
     569                #EQvis_hd' destruct(EQvis_hd') %
     570              |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G;
     571                #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G')
     572                >x_vis * #ABS elim (ABS I)
     573              ]
     574            ]
     575          ]
     576        ]
     577      ]
     578    ]
     579  |10,11,12:
     580    #i whd in match visited';
     581    lapply (in_map_domain … visited' i)
     582    >mem_set_add
     583    elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd
     584    >eq_identifier_sym >i_vis_hd
     585    [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis]
     586    [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)]
     587    #_ #EQlookup >lookup_add_miss in EQlookup;
     588    [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *]
     589    #EQlookup
     590    [1,2,3: @EQlookup %]
     591    whd in match (rev ??); >rev_append_def
     592    [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     593              <associative_append >does_not_occur_None]
     594    >(does_not_occur_Some ?????? (i_vis_hd))
     595    @generated_prf2 assumption
     596  |13,14,15:
     597    whd in match generated'; normalize <gen_length_prf %
     598  ]
     599]
     600qed.
     601
     602(* CSC: The branch compression (aka tunneling) optimization is not implemented
     603   in Matita *)
     604definition branch_compress
     605  ≝ λp: graph_params.λglobals.λg:codeT p globals.
     606    λentry : Σl.code_has_label … g l.g.
    177607 
    178 definition graph_translate_no_fin :
    179   ∀src_g_pars : graph_params.
    180   ext_fin_instruction src_g_pars = void →
    181   ∀dst_g_pars : graph_params.
    182   ∀globals: list ident.
    183   (* type of allocatable registers (unit if not in RTLabs) *)
    184   (* function dictating the translation *)
    185   (label → joint_instruction src_g_pars globals →
    186     list (joint_instruction dst_g_pars globals)
    187     (* this can be added to allow redirections: × label *)) →
    188   (* initialized function definition with empty graph *)
    189   joint_internal_function globals dst_g_pars →
    190   (* source function *)
    191   joint_internal_function globals src_g_pars →
    192   (* destination function *)
    193   joint_internal_function globals dst_g_pars ≝
    194   λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans.
    195     graph_translate src_g_pars dst_g_pars globals
    196       trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
     608lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
     609  code_closed … (branch_compress p globals g l).
     610#p#globals#g#l#H @H qed.
     611
     612lemma branch_compress_has_entry : ∀p,globals,g,l.
     613  code_has_label … (branch_compress p globals g l) l.
     614#p#globals#g*#l#l_prf @l_prf qed.
     615
     616definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
     617  map ??
     618    (λs. let 〈l_opt,x〉 ≝ s in
     619      〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
     620     
     621lemma does_not_occur_filter_labels :
     622  ∀tag,A,test,id,c.
     623    does_not_occur ?? id (filter_labels tag A test c) =
     624      (does_not_occur ?? id c ∨ ¬ test id).
     625#tag #A #test #id #c elim c
     626[ //
     627| ** [2: #lbl] #s #tl #IH
     628  whd in match (filter_labels ????); normalize nodelta
     629  whd in match (does_not_occur ????) in ⊢ (??%%);
     630  [2: @IH]
     631  normalize in match (! l ← ? ; ?); >IH
     632  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
     633  elim (test lbl) normalize nodelta
     634  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
     635  [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
     636  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
     637  ]
     638]
     639qed.
     640
     641lemma occurs_exactly_once_filter_labels :
     642  ∀tag,A,test,id,c.
     643    occurs_exactly_once ?? id (filter_labels tag A test c) =
     644      (occurs_exactly_once ?? id c ∧ test id).
     645#tag #A #test #id #c elim c
     646[ //
     647| ** [2: #lbl] #s #tl #IH
     648  whd in match (filter_labels ????); normalize nodelta
     649  whd in match (occurs_exactly_once ????) in ⊢ (??%%);
     650  [2: @IH]
     651  normalize in match (! l ← ? ; ?); >IH
     652  >does_not_occur_filter_labels
     653  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
     654  elim (test lbl) normalize nodelta
     655  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
     656  [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
     657  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
     658  ]
     659]
     660qed.
     661
     662lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
     663  nth_opt ? n (filter_labels tag A test instrs) =
     664  ! 〈lopt, s〉 ← nth_opt ? n instrs ;
     665  return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
     666#tag #A #test #instrs elim instrs
     667[ * [2: #n'] %
     668| * #lopt #s #tl #IH * [2: #n']
     669  whd in match (filter_labels ????); normalize nodelta
     670  whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
     671]
     672qed.
     673
     674definition linearize_code:
     675 ∀p : unserialized_params.∀globals.
     676  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
     677  ∀entry : (Σl. code_has_label … g l).
     678    (Σc : codeT (mk_lin_params p) globals.
     679      code_closed … c ∧
     680      ∃ sigma : identifier_map LabelTag ℕ.
     681      lookup … sigma entry = Some ? 0 ∧
     682      ∀l,n.lookup … sigma l = Some ? n →
     683        ∃s. lookup … g l = Some ? s ∧
     684          opt_Exists ?
     685            (λls.let 〈lopt, ts〉 ≝ ls in
     686              opt_All ? (eq ? l) lopt ∧
     687              ts = graph_to_lin_statement … s ∧
     688              opt_All ?
     689                (λnext.Or (lookup … sigma next = Some ? (S n))
     690                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
     691                (stmt_implicit_label … s)) (nth_opt … n c))
     692
     693 λp,globals,g,g_prf,entry_sig.
     694    let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
     695    let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
     696    let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in
     697    match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
     698      (entry_sig) g_prf ????????
     699    with
     700    [ mk_Sig triple H ⇒
     701      let sigma ≝ \fst (\fst triple) in
     702      let required ≝ \snd (\fst triple) in
     703      let crev ≝ \snd triple in
     704      let lbld_code ≝ rev ? crev in
     705      mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
     706[ (* done later *)
     707| #i >mem_set_empty *
     708| %
     709|#l #n normalize in ⊢ (%→?); #ABS destruct(ABS)
     710| #l #_ %
     711| % [2: %] @(pi2 … entry_sig')
     712| %
     713| % % [% %] cases (pi1 … entry_sig) normalize #_ % //
     714| >commutative_plus change with (? ≤ |g|) %
     715]
     716lapply (refl … triple)
     717generalize in match triple in ⊢ (???%→%); **
     718#visited #required #generated #EQtriple
     719>EQtriple in H ⊢ %; normalize nodelta ***
     720#entry_O #req_vis #labels_in_req #sigma_prop
     721% >EQtriple
     722[ (* code closed *)
     723  @All_map
     724  [2: @All_rev
     725    @(All_mp … labels_in_req) #ls #H @H
     726  |1: (* side-effect close *)
     727  |3: * #lopt #s @All_mp
     728    #lbl #lbl_req whd in match (code_has_label ????);
     729    >occurs_exactly_once_filter_labels
     730    @andb_Prop [2: assumption]
     731    lapply (in_map_domain … visited lbl)
     732    >(req_vis … lbl_req) * #n #eq_lookup
     733    elim (sigma_prop ?? eq_lookup) #H #_ @H
     734  ]
     735]
     736%{visited} % [assumption]
     737#lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
     738#lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
     739% [2: % [ assumption ] |]
     740>nth_opt_filter_labels in ⊢ (???%);
     741>nth_opt_is_stmt
     742whd in match (! 〈lopt, s〉 ← Some ??; ?);
     743whd
     744whd in match (! lbl0 ← Some ??; ?);
     745% [ % [ elim (lbl ∈ required) ] % ]
     746whd
     747lapply (refl … (stmt_implicit_label … stmt))
     748generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next]
     749#eq_impl_lbl normalize nodelta [2: %]
     750>eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H
     751[ %{H}
     752| %2 >nth_opt_filter_labels >H
     753  whd in match (! 〈lopt, s〉 ← ?; ?);
     754  whd in match (! lbl0 ← ?; ?);
     755  %
     756]
     757qed.
     758
     759definition graph_linearize :
     760  ∀p : unserialized_params.
     761  ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p).
     762    Σfout : joint_closed_internal_function globals (mk_lin_params p).
     763      ∃sigma : identifier_map LabelTag ℕ.
     764        let g ≝ joint_if_code ?? (pi1 … fin) in
     765        let c ≝ joint_if_code ?? (pi1 … fout) in
     766        let entry ≝ joint_if_entry ?? (pi1 … fin) in
     767         lookup … sigma entry = Some ? 0 ∧
     768          ∀l,n.lookup … sigma l = Some ? n →
     769            ∃s. lookup … g l = Some ? s ∧
     770              opt_Exists ?
     771                (λls.let 〈lopt, ts〉 ≝ ls in
     772                  opt_All ? (eq ? l) lopt ∧
     773                  ts = graph_to_lin_statement … s ∧
     774                  opt_All ?
     775                    (λnext.Or (lookup … sigma next = Some ? (S n))
     776                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
     777                    (stmt_implicit_label … s)) (nth_opt … n c) ≝
     778  λp,globals,f_sig.
     779  mk_Sig ?? (match f_sig with
     780  [ mk_Sig f f_prf ⇒ 
     781  mk_joint_internal_function globals (mk_lin_params p)
     782   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f)
     783   (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f)
     784   (joint_if_stacksize ?? f)
     785   (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f))
     786   (mk_Sig ?? it I) (mk_Sig ?? it I)
     787  ]) ?.
     788elim f_sig
     789normalize nodelta #f_in #f_in_prf
     790elim (linearize_code ?????)
     791#f_out * #f_out_closed #H assumption
     792qed.
     793
    197794 
    198795
  • src/joint/semanticsUtils_paolo.ma

    r1641 r1882  
    2121(******************************** GRAPHS **************************************)
    2222
    23 definition graph_pointer_of_label0:
    24  pointer → label → Σp:pointer. ptype p = Code ≝
    25  λoldpc,l.
    26   mk_pointer Code
    27    (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
    28 // qed.
    29 
    30 definition graph_pointer_of_label :
    31   ∀pars : graph_params.∀globals. genv globals pars → pointer → label →
    32     res (Σp:pointer. ptype p = Code) ≝
    33  λ_.λ_.λ_.λoldpc,l.
    34   OK ? (graph_pointer_of_label0 oldpc l).
     23definition graph_pointer_of_label : cpointer → label → res cpointer ≝
     24  λoldpc,l.
     25  return (mk_pointer Code
     26   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer).
     27% qed.
    3528
    3629definition graph_label_of_pointer: pointer → res label ≝
    3730 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
    38 
    39 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    40  But I can't use it directly because this one uses a concrete definition of
    41  pointer_of_label and it is used to istantiate the more_sem_params record
    42  where the abstract version is declared as a field. Is there a better way
    43  to organize the code? *)
    44 definition graph_succ_p: label → address → res address ≝
    45  λl,old.
    46   do ptr ← pointer_of_address old ;
    47   let newptr ≝ graph_pointer_of_label0 ptr l in
    48   address_of_pointer newptr.
    4931
    5032definition graph_fetch_statement:
     
    5335 ∀globals.
    5436  genv globals pars →
    55   state sem_pars
     37  cpointer
    5638  res (joint_statement pars globals) ≝
    57  λpars,sem_pars,globals,ge,st.
    58   do p ← code_pointer_of_address (pc … st) ;
     39 λpars,sem_pars,globals,ge,p.
    5940  do f ← fetch_function … ge p ;
    6041  do l ← graph_label_of_pointer p;
     
    7152      pars
    7253      g_pars
    73       graph_succ_p
    74       (graph_pointer_of_label ?)
    75       (graph_fetch_statement ? ?)
     54      graph_pointer_of_label
     55      (λ_.λ_.graph_pointer_of_label)
     56      (graph_fetch_statement ? g_pars)
    7657    ).
    7758   
    7859(******************************** LINEAR **************************************)
    79 
    80 definition lin_succ_p: unit → address → res address :=
    81  λ_.λaddr. addr_add addr 1.
    82 
     60check mk_pointer
     61definition lin_succ_p: cpointer → unit → res cpointer :=
     62 λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?».
     63[%| cases ptr //] qed.
    8364
    8465axiom BadLabel: String.
     
    8667definition lin_pointer_of_label:
    8768 ∀pars : lin_params.
    88  ∀globals. genv globals pars → pointer → label →
    89   res (Σp:pointer. ptype p = Code) ≝
     69 ∀globals. genv globals pars → cpointer → label → res cpointer ≝
    9070 λpars,globals,ge,old,l.
    9171  do fn ← fetch_function … ge old ;
     
    9777     (joint_if_code … pars fn)) ;
    9878  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
    99 // qed.
     79% qed.
    10080
    10181definition lin_fetch_statement:
     
    10383 ∀sem_pars : sem_state_params.
    10484 ∀globals.
    105  genv globals pars → state sem_pars → res (joint_statement pars globals) ≝
    106  λpars,sem_pars,globals,ge,st.
    107   do ppc ← pointer_of_address (pc … st) ;
     85 genv globals pars → cpointer → res (joint_statement pars globals) ≝
     86 λpars,sem_pars,globals,ge,ppc.
    10887  do fn ← fetch_function … ge ppc ;
    10988  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
     
    123102      lin_succ_p
    124103      (lin_pointer_of_label ?)
    125       (lin_fetch_statement ? ?)
     104      (lin_fetch_statement ? g_pars)
    126105    ).
    127106   
    128 
     107definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝
     108  λp,globals,stp.match stp with
     109  [ COND _ _ ⇒ false
     110  | CALL_ID _ _ _ ⇒ false
     111  | extension c' ⇒ (* FIXME: does not care about calling extensions!! *)
     112    match ext_step_labels … c' with
     113    [ nil ⇒ true
     114    | _ ⇒ false
     115    ]
     116  | _ ⇒ true
     117  ].
     118
     119definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝
     120  λp,globals,stp.match stp with
     121  [ sequential _ _ ⇒ false
     122  | _ ⇒ true
     123  ].
     124
     125inductive s_block (p : params) (globals : list ident) : Type[0] ≝
     126  | Skip : s_block p globals
     127  | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals
     128  | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals
     129  | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals.
     130
     131include "utilities/bind_new.ma".
     132
     133definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals).
     134
     135definition Bcons ≝ λp : params.λglobals.
     136    λs : Σs.bool_to_Prop (step_unbranching p globals s).
     137    λB : Block p globals.
     138    ! b ← B ; return Cons ?? s b.
     139
     140interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl).
     141
     142let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝
     143  match b1 with
     144  [ Skip ⇒ true
     145  | FinStep _ ⇒ false
     146  | FinStmt _ ⇒ false
     147  | Cons _ tl ⇒ is_unbranching ?? tl
     148  ].
     149
     150let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝
     151  match b1 with
     152  [ bret b ⇒ bool_to_Prop (is_unbranching … b)
     153  | bnew f ⇒ ∀x.Is_unbranching … (f x)
     154  ].
     155
     156let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝
     157  match b1 return λx.is_unbranching ?? x → ? with
     158  [ Skip ⇒ λ_.b2
     159  | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf)
     160  | _ ⇒ Ⓧ
     161  ].
     162
     163definition s_block_append ≝
     164  λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2.
     165  match b1 with
     166  [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ].
     167
     168definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) →
     169  bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝
     170  λp,globals. ?.
     171* #b elim b -b
     172[ #b #H @bret @b @H
     173| #f #IH #H @bnew #x @(IH x) @H
     174]
     175qed.
     176
     177lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B.
     178#p #globals * #b elim b
     179[ //
     180| #f #IH #H @bnew_proper
     181  #x @IH
     182]
     183qed.
     184 
     185definition Block_append ≝
     186  λp,globals.λB : Σb.Is_unbranching … b.λB'.
     187  ! b1 ← Is_to_is_unbr … B;
     188  ! b2 ← B';
     189  return s_block_append p globals b1 b2.
     190
     191definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)).
     192
     193let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l :
     194    s_block p globals ≝
     195  match l  with
     196  [ nil ⇒ Skip ??
     197  | cons hd tl ⇒
     198    If step_unbranching … hd then with prf do
     199      Cons ?? hd (step_list_to_s_block ?? tl)
     200    else with prf do
     201      FinStep ?? hd
     202  ]. [assumption | >prf % ] qed.
     203 
     204definition step_list_to_block : ∀R,p,g.? → Block R p g ≝
     205  λR,p,globals,l.bret R ? (step_list_to_s_block p globals l).
     206
     207record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝
     208  { function_rel : joint_function globals p1 → joint_function globals p2 → Prop
     209  ; genv_rel : genv globals p1 → genv globals p2 → Prop
     210  ; pc_rel : cpointer → cpointer → Prop
     211  ; st_rel : state p1 → state p2 → Prop
     212  ; stmt_rel : joint_statement p1 globals → Block
     213  (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *)
     214  ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2)
     215  }.
     216 
     217(* move *)
     218definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝
     219 λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒
     220  match pty return λpty. ? → pty = XData → ? with
     221   [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ?
     222   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
     223[@(pi2 … p) |6: // |7: %] destruct (abs)
     224qed.
     225
     226definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer.
     227cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
     228lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
     229%{«mk_pointer ? (mk_block ? z) H o,I»}
     230% [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:]
     231qed.
     232
     233definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝
     234  λp1,p2,R,st1,st2.
     235    frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧
     236    pc_rel p1 p2 R (pc … st1) (pc … st2) ∧
     237    sp_rel p1 p2 R
     238      (safe_address_of_xdata_pointer (sp … st1))
     239      (safe_address_of_xdata_pointer (sp … st2)) ∧
     240    isp_rel p1 p2 R
     241      (safe_address_of_xdata_pointer (isp … st1))
     242      (safe_address_of_xdata_pointer (isp … st2)) ∧
     243    sp_rel p1 p2 R
     244      (safe_address_of_xdata_pointer (sp … st1))
     245      (safe_address_of_xdata_pointer (sp … st2)) ∧
     246    carry … st1 = carry … st2 ∧
     247    regs_rel p1 p2 R (regs … st1) (regs … st2) ∧
     248    mem_rel p1 p2 R (m … st1) (m … st2).
     249elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1
     250elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2
     251assumption
     252qed.
     253 elim st2
     254-st1 -st2 #st2 ** #good_pc2 # ∧
     255    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     256    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     257    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     258
     259
     260
  • src/joint/semantics_paolo.ma

    r1709 r1882  
    1212
    1313definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p).
     14definition cpointer ≝ Σp.ptype p = Code.
     15definition xpointer ≝ Σp.ptype p = XData.
     16unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
     17unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).
    1418
    1519record sem_state_params : Type[1] ≝
     
    1721 ; empty_framesT: framesT
    1822 ; regsT : Type[0]
    19  ; empty_regsT: address → regsT (* Stack pointer *)
     23 ; empty_regsT: xpointer → regsT (* Stack pointer *)
    2024 }.
    2125 
    2226record state (semp: sem_state_params): Type[0] ≝
    2327 { st_frms: framesT semp
    24  ; pc: address
    25  ; sp: pointer
    26  ; isp: pointer
     28 ; sp: xpointer
     29 ; isp: xpointer
    2730 ; carry: beval
    2831 ; regs: regsT semp
    2932 ; m: bemem
    3033 }.
    31  
     34
     35record state_pc (semp : sem_state_params) : Type[0] ≝
     36  { st_no_pc :> state semp
     37  ; pc : cpointer
     38  }.
     39
    3240definition set_m: ∀p. bemem → state p → state p ≝
    33  λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     41 λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
    3442
    3543definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    36  λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
    37 
    38 definition set_sp: ∀p. pointer → state p → state p ≝
    39  λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
    40 
    41 definition set_isp: ∀p. pointer → state p → state p ≝
    42  λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
     44 λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
     45
     46definition set_sp: ∀p. ? → state p → state p ≝
     47 λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
     48
     49definition set_isp: ∀p. ? → state p → state p ≝
     50 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
    4351
    4452definition set_carry: ∀p. beval → state p → state p ≝
    45  λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
    46 
    47 definition set_pc: ∀p. address → state p → state p ≝
    48  λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     53 λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
     54
     55definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     56 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
     57
     58definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
     59 λp,s,st. mk_state_pc … s (pc … st).
    4960
    5061definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    51  λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     62 λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    5263
    5364axiom BadProgramCounter : String.
     
    5768 ∀globals.
    5869  genv globals pars →
    59   pointer →
     70  cpointer →
    6071  res (joint_internal_function … pars) ≝
    6172 λpars,globals,ge,p.
     
    6576  [ Internal def' ⇒ OK … def'
    6677  | External _ ⇒ Error … [MSG BadProgramCounter]].
    67  
     78
     79inductive step_flow (p : params) (globals : list ident) : Type[0] ≝
     80  | Redirect : label → step_flow p globals (* used for goto-like flow alteration *)
     81  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals (* call a function with given id, then proceed *)
     82  | Proceed  : step_flow p globals. (* go to implicit successor *)
     83
     84inductive stmt_flow (p : params) (globals : list ident) : Type[0] ≝
     85  | SRedirect : label → stmt_flow p globals
     86  | SProceed : succ p → stmt_flow p globals
     87  | SInit     : Z → joint_internal_function globals p → call_args p → call_dest p → succ p → stmt_flow p globals
     88  | STailInit : Z → joint_internal_function globals p → call_args p → stmt_flow p globals
     89  | SEnd  : stmt_flow p globals. (* end flow *)
     90
     91
    6892record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
    6993  { st_pars :> sem_state_params
     
    82106  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    83107  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    84   ; fetch_ra: state st_pars →
    85       res ((state st_pars) × address)
    86 
    87   ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
     108  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
     109
     110  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
    88111  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    89   ; save_frame: address → call_dest uns_pars → state st_pars → state st_pars
     112  ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
    90113   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    91114     type of arguments. To be fixed using a dependent type *)
     
    94117  ; fetch_external_args: external_function → state st_pars →
    95118      res (list val)
    96   ; set_result: list val → state st_pars →
    97       res (state st_pars)
     119  ; set_result: list val → state st_pars → res (state st_pars)
    98120  ; call_args_for_main: call_args uns_pars
    99121  ; call_dest_for_main: call_dest uns_pars
     
    111133  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
    112134  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
    113   λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st).
     135  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
    114136
    115137definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
     
    126148definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
    127149definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
    128 definition pair_reg_move : ?→?→?→?→res ?
     150definition pair_reg_move : ?→?→?→?→?
    129151  λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
    130152    ! r ← pair_reg_move_ ? p (regs ? st) pm;
    131     return (set_regs ? r st).
    132 
     153    return set_regs ? r st.
     154
     155 
    133156axiom BadPointer : String.
    134 
     157 
    135158(* this is preamble to all calls (including tail ones). The optional argument in
    136159   input tells the function whether it has to save the frame for internal
    137160   calls.
    138    the first element of the triple is the label at the start of the function
    139    in case of an internal call, or None in case of an external one.
     161   the first element of the triple is the entry point of the function if
     162   it is an internal one, or false in case of an external one.
    140163   The actual update of the pc is left to later, as it depends on
    141164   serialization and on whether the call is a tail one. *)
    142 definition eval_call_block_preamble:
     165definition eval_call_block:
    143166 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
    144   genv globals p → state p' → block → call_args p → option ((call_dest p) × address)
    145     IO io_out io_in ((option label)×trace×(state p')) ≝
    146  λglobals,p,p',ge,st,b,args,dest_ra.
     167  genv globals p → state p' → block → call_args p → call_dest p
     168    IO io_out io_in ((step_flow p globals)×trace×(state p')) ≝
     169 λglobals,p,p',ge,st,b,args,dest.
    147170  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
    148171    match fd with
    149172    [ Internal fn ⇒
    150       let st ≝ match dest_ra with
    151         [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st
    152         | None ⇒ st
    153         ] in
    154       ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    155               args st ;
    156       let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    157       let l' ≝ joint_if_entry … fn in
    158       let st ≝ set_regs p' regs st in
    159       return 〈Some label l', E0, st〉
     173      return 〈Init … (block_id b) fn args dest, E0, st〉
    160174    | External fn ⇒
    161175      ! params ← fetch_external_args … p' fn st : IO ???;
     
    167181      let vs ≝ [mk_val ? evres] in
    168182      ! st ← set_result … p' vs st : IO ???;
    169       return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     183      return 〈Proceed ??, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    170184      ].
    171185
    172186axiom FailedStore: String.
    173187
    174 definition push: ∀p. state p → beval → res (state p) ≝
     188definition push: ∀p.state p → beval → res (state p) ≝
    175189 λp,st,v.
    176   let isp ≝ isp … st in
    177   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    178   let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    179   OK … (set_m … m (set_isp … isp st)).
    180 
    181 definition pop: ∀p. state p → res (state p × beval) ≝
     190  let isp' ≝ isp ? st in
     191  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
     192  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
     193  return set_m … m (set_isp … isp'' st).
     194  normalize elim (isp p st) //
     195qed.
     196
     197definition pop: ∀p. state p → res ((state p ) × beval) ≝
    182198 λp,st.
    183   let isp ≝ isp ? st in
    184   let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    185   let ist ≝ set_isp … isp st in
    186   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    187   OK ? 〈st,v〉.
    188 
    189 definition save_ra : ∀p. state p → address → res (state p) ≝
     199  let isp' ≝ isp ? st in
     200  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
     201  let ist ≝ set_isp … isp'' st in
     202  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
     203  OK ? 〈ist,v〉.
     204  normalize elim (isp p st) //
     205qed.
     206 
     207definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    190208 λp,st,l.
    191   let 〈addrl,addrh〉 ≝ l in
    192   do st ← push … st addrl;
    193   push … st addrh.
    194 
    195 definition load_ra : ∀p.state p → res (state p × address) ≝
     209  let 〈addrl,addrh〉 ≝ address_of_code_pointer l in
     210  ! st' ← push … st addrl;
     211  push … st' addrh.
     212
     213definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
    196214 λp,st.
    197   do 〈st,addrh〉 ← pop … st;
    198   do 〈st,addrl〉 ← pop … st;
    199   OK ? 〈st, 〈addrl,addrh〉〉.
    200 
     215  do 〈st',addrh〉 ← pop … st;
     216  do 〈st'',addrl〉 ← pop … st';
     217  do pr ← code_pointer_of_address 〈addrh, addrl〉;
     218  return 〈st'', pr〉.
     219
     220definition flow_no_seq : ∀p,g.stmt_flow p g → Prop ≝ λp,g,flow.
     221  match flow with
     222  [ SProceed _ ⇒ False
     223  | SInit _ _ _ _ _ ⇒ False
     224  | _ ⇒ True
     225  ].
    201226
    202227(* parameters that need full params to have type of functions,
    203    but are still independent of serialization
    204    Paolo: the first element returned by exec extended is None if flow is
    205    left to regular sequential one, otherwise a label.
    206    The address input is the address of the next statement, to be provided to
    207    accomodate extensions that make calls. *)
     228   but are still independent of serialization *)
    208229record more_sem_genv_params (pp : params) : Type[1] ≝
    209230  { msu_pars :> more_sem_unserialized_params pp
    210231  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    211   ; exec_extended: ∀globals.genv globals pp → ext_instruction pp →
    212       state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars))
    213   ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp →
    214       state msu_pars → IO io_out io_in (trace × (state msu_pars))
     232  (* change of pc must be left to *_flow execution *)
     233  ; exec_extended: ∀globals.genv globals pp → ext_step pp →
     234      state msu_pars →
     235      IO io_out io_in ((step_flow pp globals)× trace × (state msu_pars))
     236  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_stmt pp →
     237      state msu_pars →
     238      IO io_out io_in ((Σs.flow_no_seq pp globals s)× trace × (state msu_pars))
    215239  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    216240  }.
    217  
    218241
    219242(* parameters that are defined by serialization *)
    220243record more_sem_params (pp : params) : Type[1] ≝
    221244  { msg_pars :> more_sem_genv_params pp
    222   ; succ_pc: succ pp → address → res address
    223   ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code)
    224   ; fetch_statement: ∀globals.genv globals pp → state msg_pars → res (joint_statement pp globals)
     245  ; offset_of_point : code_point pp → offset
     246  ; point_of_offset : offset → option (code_point pp)
     247  ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
     248  ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
    225249  }.
     250
     251definition pointer_of_point : ∀p.more_sem_params p →
     252  cpointer→ code_point p → cpointer ≝
     253  λp,msp,ptr,pt.
     254    mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt).
     255[ elim ptr #ptr' #EQ <EQ @pok
     256| %] qed.
     257
     258axiom BadOffsetForCodePoint : String.
     259
     260definition point_of_pointer :
     261  ∀p.more_sem_params p → cpointer → res (code_point p) ≝
     262  λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
     263    (point_of_offset p msp (poff ptr)).
     264
     265lemma point_of_pointer_of_point :
     266  ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
     267#p #msp #ptr #pt normalize
     268>point_of_offset_of_point %
     269qed.
     270
     271lemma pointer_of_point_block :
     272  ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
     273/ by refl/
     274qed.
     275
     276lemma pointer_of_point_uses_block :
     277  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
     278#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
     279        ** #ty2 #bl2 #H2 #o2 #EQ2
     280#pt #EQ3 destruct normalize //
     281qed.
     282
     283lemma pointer_of_point_of_pointer :
     284  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
     285    pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
     286    pointer_of_point p msp ptr2 pt = ptr1.
     287#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
     288        ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ
     289destruct
     290lapply (offset_of_point_of_offset p msp o1)
     291normalize
     292elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
     293#pt' #EQ #EQ' destruct %
     294qed.
     295
     296
     297axiom ProgramCounterOutOfCode : String.
     298axiom PointNotFound : String.
     299axiom LabelNotFound : String.
     300
     301definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
     302  genv globals p → cpointer → res (joint_statement p globals) ≝
     303  λp,msp,globals,ge,ptr.
     304  ! pt ← point_of_pointer ? msp ptr ;
     305  ! fn ← fetch_function … ge ptr ;
     306  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
     307
     308definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
     309  genv globals p → cpointer → label → res cpointer ≝
     310  λp,msp,globals,ge,ptr,lbl.
     311  ! fn ← fetch_function … ge ptr ;
     312  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
     313            (point_of_label … (joint_if_code … fn) lbl) ;
     314  return pointer_of_point ? msp ptr pt.
     315
     316definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
     317  cpointer → succ p → res cpointer ≝
     318  λp,msp,ptr,nxt.
     319  ! curr ← point_of_pointer p msp ptr ;
     320  return pointer_of_point p msp ptr (point_of_succ p curr nxt). 
    226321
    227322record sem_params : Type[1] ≝
     
    230325  }.
    231326
    232 definition address_of_label: ∀globals. ∀p:sem_params.
     327(* definition address_of_label: ∀globals. ∀p:sem_params.
    233328  genv globals p → pointer → label → res address ≝
    234329 λglobals,p,ge,ptr,l.
    235330  do newptr ← pointer_of_label … p ? ge … ptr l ;
    236   OK … (address_of_code_pointer newptr).
     331  OK … (address_of_code_pointer newptr). *)
    237332
    238333definition goto: ∀globals. ∀p:sem_params.
    239   genv globals p → label → state p → res (state p) ≝
     334  genv globals p → label → state_pc p → res (state_pc p) ≝
    240335 λglobals,p,ge,l,st.
    241   ! oldpc ← pointer_of_address (pc … st);
    242   ! newpc ← address_of_label … ge oldpc l ;
    243   OK (state p) (set_pc … newpc st).
     336  ! newpc ← pointer_of_label ? p … ge (pc … st) l ;
     337  return set_pc … newpc st.
    244338
    245339(*
     
    248342*)
    249343
    250 definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
     344definition next : ∀p : sem_params.succ p → state_pc p → res (state_pc p) ≝
    251345 λp,l,st.
    252   ! l' ← succ_pc … p l (pc … st) ;
    253   OK … (set_pc … l' st).
     346 ! nw ← succ_pc ? p … (pc ? st) l ;
     347 return set_pc … nw st.
    254348
    255349axiom MissingSymbol : String.
    256350axiom FailedLoad : String.
    257351axiom BadFunction : String.
    258 
    259 definition eval_call_block:
     352axiom SuccessorNotProvided : String.
     353
     354(* the optional point must be given only for calls *)
     355definition eval_step :
    260356 ∀globals.∀p:sem_params. genv globals p → state p →
    261   block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    262  λglobals,p,ge,st,b,args,dest,ra.
    263  ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ;
    264  ! new_pc ← match next with
    265   [ Some lbl ⇒
    266     let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
    267     address_of_label globals p ge pointer_in_fn lbl
    268   | None ⇒ return ra
    269   ] ;
    270  let st ≝ set_pc … new_pc st in
    271  return 〈tr, st〉.
    272 % qed.
    273 
    274 definition eval_call_id:
    275  ∀globals.∀p:sem_params. genv globals p → state p →
    276   ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    277  λglobals,p,ge,st,id,args,dest,ra.
    278   ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
    279   eval_call_block … ge st b args dest ra.
    280 
    281 
    282 (* defining because otherwise typechecker stalls *)
    283 definition eval_address : ∀globals.∀p : sem_params. genv globals p → state p →
    284   ∀i : ident.member i (eq_identifier SymbolTag) globals
    285      →dpl_reg p→dph_reg p→ succ p → res (trace × (state p)) ≝
    286      λglobals,p,ge,st,ident,prf,ldest,hdest,l.
    287      let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
    288      ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
    289      ! st ← dpl_store … ldest laddr st;
    290      ! st ← dph_store … hdest haddr st;
    291      ! st ← next … p l st ;
    292      return 〈E0, st〉.
    293   [ cases addr //
    294   | (* TODO: to prove *)
    295     elim daemon
    296   ] qed.
    297 
    298 (* defining because otherwise typechecker stalls *)
    299 definition eval_pop : ∀globals.∀p : sem_params. genv globals p → state p →
    300   acc_a_reg p → succ p → res (trace × (state p)) ≝
    301   λglobals,p,ge,st,dst,l.
    302         ! 〈st,v〉 ← pop p st;
    303         ! st ← acca_store p p dst v st;
    304         ! st ← next p l st ;
    305         return 〈E0, st〉.
    306 
    307 (* defining because otherwise typechecker stalls *)
    308 definition eval_sequential :
    309  ∀globals.∀p:sem_params. genv globals p → state p →
    310   joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝
    311  λglobals,p,ge,st,seq,l.
     357  joint_step p globals →
     358  IO io_out io_in ((step_flow p globals)×trace×(state p)) ≝
     359 λglobals,p,ge,st,seq.
    312360  match seq with
    313361  [ extension c ⇒
    314     ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ;
    315     ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr;
    316     ! st ← match next_pc with
    317       [ None ⇒ next … p l st
    318       | Some lbl ⇒ goto … ge lbl st
    319       ] ;
    320     return 〈tr, st〉
     362    exec_extended … ge c st
    321363  | COST_LABEL cl ⇒
    322     ! st ← next … p l st ;
    323     return 〈Echarge cl, st〉
     364    return 〈Proceed ??, Echarge cl, st〉
    324365  | COMMENT c ⇒
    325     ! st ← next … p l st ;
    326     return 〈E0, st〉
     366    return 〈Proceed ??, E0, st〉
    327367  | LOAD dst addrl addrh ⇒
    328368    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    331371    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    332372    ! st ← acca_store p … dst v st ;
    333     ! st ← next … p l st ;
    334     return 〈E0, st〉
     373    return 〈Proceed ??, E0, st〉
    335374  | STORE addrl addrh src ⇒
    336375    ! vaddrh ← dph_arg_retrieve … st addrh;
     
    339378    ! v ← acca_arg_retrieve … st src;
    340379    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    341     let st ≝ set_m … m' st in
    342     ! st ← next … p l st ;
    343     return 〈E0, st〉
     380    return 〈Proceed ??, E0, set_m … m' st〉
    344381  | COND src ltrue ⇒
    345382    ! v ← acca_retrieve … st src;
    346383    ! b ← bool_of_beval v;
    347384    if b then
    348      ! st ← goto … p ge ltrue st ;
    349      return 〈E0, st〉
     385      return 〈Redirect ?? ltrue, E0, st〉
    350386    else
    351      ! st ← next … p l st ;
    352      return 〈E0, st〉
     387      return 〈Proceed ??, E0, st〉
    353388  | ADDRESS ident prf ldest hdest ⇒
    354     eval_address … ge st ident prf ldest hdest l
     389    let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
     390    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
     391    ! st' ← dpl_store … ldest laddr st;
     392    ! st'' ← dph_store … hdest haddr st';
     393    return 〈Proceed ??, E0, st''〉
    355394  | OP1 op dacc_a sacc_a ⇒
    356395    ! v ← acca_retrieve … st sacc_a;
     
    358397    let v' ≝ BVByte (op1 eval op v) in
    359398    ! st ← acca_store … dacc_a v' st;
    360     ! st ← next … l st ;
    361     return 〈E0, st〉
     399    return 〈Proceed ??, E0, st〉
    362400  | OP2 op dacc_a sacc_a src ⇒
    363401    ! v1 ← acca_arg_retrieve … st sacc_a;
     
    369407      let v' ≝ BVByte v' in
    370408      let carry ≝ beval_of_bool carry in
    371     ! st ← acca_store … dacc_a v' st;
    372       let st ≝ set_carry … carry st in
    373     ! st ← next … l st ;
    374     return 〈E0, st〉
     409    ! st' ← acca_store … dacc_a v' st;
     410      let st'' ≝ set_carry … carry st' in
     411    return 〈Proceed ??, E0, st''〉
    375412  | CLEAR_CARRY ⇒
    376     ! st ← next … l (set_carry … BVfalse st) ;
    377     return 〈E0, st
     413    let st' ≝ set_carry … BVfalse st in
     414    return 〈Proceed ??, E0, st'
    378415  | SET_CARRY ⇒
    379     ! st ← next … l (set_carry … BVtrue st) ;
    380     return 〈E0, st
     416    let st' ≝ set_carry … BVtrue st in
     417    return 〈Proceed ??, E0, st'
    381418  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    382419    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     
    387424    let v1' ≝ BVByte v1' in
    388425    let v2' ≝ BVByte v2' in
    389     ! st ← acca_store … dacc_a_reg v1' st;
    390     ! st ← accb_store … dacc_b_reg v2' st;
    391     ! st ← next … l st ;
    392     return 〈E0, st〉
     426    ! st' ← acca_store … dacc_a_reg v1' st;
     427    ! st'' ← accb_store … dacc_b_reg v2' st';
     428    return 〈Proceed ??, E0, st''〉
    393429  | POP dst ⇒
    394     eval_pop … ge st dst l
     430    ! 〈st',v〉 ← pop p st;
     431    ! st'' ← acca_store p p dst v st';
     432    return 〈Proceed ??, E0, st''〉
    395433  | PUSH src ⇒
    396434    ! v ← acca_arg_retrieve … st src;
    397435    ! st ← push … st v;
    398     ! st ← next … l st ;
    399     return 〈E0, st〉
     436    return 〈Proceed ??, E0, st〉
    400437  | MOVE dst_src ⇒
    401438    ! st ← pair_reg_move … st dst_src ;
    402     ! st ← next … l st ;
    403     return 〈E0, st〉
     439    return 〈Proceed ??, E0, st〉
    404440  | CALL_ID id args dest ⇒
    405     ! ra ← succ_pc … p l (pc … st) : IO ??? ;
    406     eval_call_id … ge st id args dest ra
     441    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
     442    eval_call_block … ge st b args dest
    407443  ].
     444  [ cases addr //
     445  | (* TODO: to prove *)
     446    elim daemon
     447  ] qed.
     448
     449definition eval_step_flow :
     450 ∀globals.∀p:sem_params.step_flow p globals →
     451  succ p → stmt_flow p globals ≝
     452 λglobals,p,cmd,nxt.
     453 match cmd with
     454 [ Redirect l ⇒ SRedirect … l
     455 | Init id fn args dest ⇒ SInit … id fn args dest nxt
     456 | Proceed ⇒ SProceed … nxt
     457 ].
    408458
    409459definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
    410   state p → IO io_out io_in (trace × (state p)) ≝
    411  λglobals,p,ge,st.
    412   ! s ← fetch_statement … ge st : IO ???;
    413   match s return λ_.IO io_out io_in (trace × (state p)) with
    414     [ GOTO l ⇒
    415        ! st ← goto … ge l st ;
    416        return 〈E0, st〉
    417     | RETURN ⇒
     460  state p → joint_statement … p globals →
     461  IO io_out io_in ((stmt_flow p globals) × trace × (state p)) ≝
     462 λglobals,p,ge,st,s.
     463  match s with
     464    [ GOTO l ⇒ return 〈SRedirect … l, E0, (st : state ?)〉
     465    | RETURN ⇒ return 〈SEnd ??, E0, (st : state ?) 〉
     466    | sequential seq l ⇒
     467      ! 〈flow, tr, st〉 ← eval_step … ge st seq ;
     468      return 〈eval_step_flow … flow l, tr, st〉
     469    | extension_fin c ⇒
     470      ! 〈flow, tr, st〉 ← exec_fin_extended … ge c st ;
     471      return 〈pi1 … flow, tr, st〉
     472    ].
     473
     474definition eval_statement_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
     475  state p → (Σs : joint_statement … p globals.no_seq … s) →
     476  IO io_out io_in ((Σf.flow_no_seq p globals f) × trace × (state p)) ≝
     477 λglobals,p,ge,st,s_sig.
     478  match s_sig with
     479  [ mk_Sig s s_prf ⇒
     480    match s return λx.no_seq p globals x → ? with
     481    [ GOTO l ⇒ λ_.return 〈«SRedirect … l,?», E0, (st : state ?)〉
     482    | RETURN ⇒ λ_.return 〈«SEnd ??,?», E0, (st : state ?) 〉
     483    | sequential seq l ⇒ Ⓧ
     484    | extension_fin c ⇒ λ_.exec_fin_extended … ge c st
     485    ] s_prf
     486  ]. % qed.
     487
     488let rec rel_io O I A B (P : A → B → Prop) (v1 : IO O I A)
     489  (v2 : IO O I B) on v1 : Prop ≝
     490  match v1 with
     491  [ Value x ⇒
     492    match v2 with
     493    [ Value y ⇒
     494      P x y
     495    | _ ⇒ False
     496    ]
     497  | Wrong _ ⇒
     498    match v2 with
     499    [ Wrong _ ⇒ True
     500    | _ ⇒ False
     501    ]
     502  | Interact o1 f1 ⇒
     503    match v2 with
     504    [ Interact o2 f2 ⇒
     505      ∃prf:o1 = o2.∀i.rel_io … P (f1 i) (f2 ?)
     506    | _ ⇒ False
     507    ]
     508  ]. <prf @i qed.
     509
     510definition IORel ≝ λO,I.
     511  mk_MonadRel (IOMonad O I) (IOMonad O I)
     512    (rel_io O I) ???.
     513[//
     514|#X #Y #Z #W #relin #relout #m elim m
     515  [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G
     516    #f1 #f2 #G' whd %{(refl …)} #i
     517    @(IH … (G i) f1 f2 G')
     518  | #v * [#o #f * | #v' | #e *]
     519    #Pvv' #f #g #H normalize @H @Pvv'
     520  | #e1 * [#o #f * | #v' *| #e2] * #f #g #_ %
     521  ]
     522| #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] *
     523  [1,4,7: #o' #f' [2,3: *]
     524    normalize * #prf destruct(prf) normalize #G
     525    % [%] normalize #i @IH @G
     526  |2,5,8: #v' [1,3: *]
     527    @H
     528  |*: #e' [1,2: *] //
     529  ]
     530]
     531qed.
     532
     533lemma IORel_refl : ∀O,I,X,rel.reflexive X rel →
     534  reflexive ? (m_rel ?? (IORel O I) ?? rel).
     535#O #I #X #rel #H #m elim m
     536[ #o #f #IH whd %[%] #i normalize @IH
     537| #v @H
     538| #e %
     539]
     540qed.
     541
     542lemma IORel_transitive : ∀O,I,X,Y,Z,rel1,rel2,rel3.
     543  (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) →
     544  ∀m,n,o.
     545  m_rel ?? (IORel O I) … rel1 m n →
     546  m_rel ?? (IORel O I) … rel2 n o →
     547  m_rel ?? (IORel O I) … rel3 m o.
     548#O #I #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m
     549[ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ]
     550  normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) //
     551| #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *]
     552  @H
     553| #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] //
     554]
     555qed.
     556
     557lemma mr_bind' : ∀M1,M2.∀Rel : MonadRel M1 M2.
     558  ∀X,Y,Z,W,relin,relout,m,n.m_rel ?? Rel X Y relin m n →
     559  ∀f,g.(∀x,y.relin x y → m_rel ?? Rel Z W relout (f x) (g y)) →
     560                  m_rel ?? Rel ?? relout (! x ← m ; f x) (! y ← n ; g y).
     561#M1 #M2 #Rel #X #Y #Z #W #relin #relout #m #n #H #f #g #G
     562@(mr_bind … H) @G qed.
     563
     564lemma m_bind_ext_eq' : ∀M : MonadProps.∀X,Y.∀m1,m2 : monad M X.∀f1,f2 : X → monad M Y.
     565  m1 = m2 → (∀x.f1 x = f2 x) → ! x ← m1 ; f1 x = ! x ← m2 ; f2 x.
     566#M #X #Y #m1 #m2 #f1 #f2 #EQ >EQ @m_bind_ext_eq
     567qed.
     568
     569lemma eval_statement_no_seq_to_normal : ∀globals,p,ge,st,s1,s2.
     570  pi1 ?? s1 = s2 →
     571  m_rel ?? (IORel ??) ??
     572    (λx,y.pi1 ?? (\fst (\fst x)) = \fst (\fst y) ∧
     573      \snd (\fst x) = \snd (\fst y) ∧ \snd x = \snd y)
     574    (eval_statement_no_seq globals p ge st s1)
     575    (eval_statement globals p ge st s2).
     576#globals #p #ge #st * * [#s #n | #lbl || #c ]*
     577#s2 #EQ destruct(EQ)
     578whd in match eval_statement;
     579whd in match eval_statement_no_seq;
     580normalize nodelta
     581[1,2: @(mr_return … (IORel ??)) /3 by pair_destruct, conj/]
     582<(m_bind_return … (exec_fin_extended ??????)) in ⊢ (???????%?);
     583@(mr_bind … (IORel ??)) [@eq | @IORel_refl // |
     584#x #y #EQ destruct(EQ) cases y ** #a #prf #b #c whd /3 by pair_destruct, conj/
     585qed.
     586
     587definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
     588  state p → Z → joint_internal_function globals p → call_args p →
     589  res (state_pc p) ≝
     590  λglobals,p,ge,st,id,fn,args.
     591    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
     592              args st ;
     593    let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
     594    let l' ≝ joint_if_entry … fn in
     595    let st' ≝ set_regs p regs st in
     596    let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in
     597    let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
     598    return mk_state_pc ? st' pc. % qed.
     599
     600definition eval_stmt_flow : ∀globals: list ident.∀p:sem_params. genv globals p →
     601  state_pc p → stmt_flow p globals → IO io_out io_in (state_pc p) ≝
     602  λglobals,p,ge,st,flow.
     603  match flow with
     604  [ SRedirect l ⇒ goto … ge l st
     605  | SProceed nxt ⇒ next ? nxt st
     606  | SInit id fn args dest nxt ⇒
     607    ! ra ← succ_pc ? p … (pc … st) nxt ;
     608    let st' ≝ set_no_pc … (set_frms … (save_frame … ra dest st) st) st in
     609    do_call ?? ge st' id fn args
     610  | STailInit id fn args ⇒
     611    do_call … ge st id fn args
     612  | SEnd ⇒
     613    ! 〈st,ra〉 ← fetch_ra … st ;
     614    ! st' ← pop_frame … ge st;
     615    return mk_state_pc ? st' ra
     616  ].
     617
     618definition eval_stmt_flow_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
     619  state p → Z → (Σf:stmt_flow p globals.flow_no_seq … f) →
     620    IO io_out io_in (state_pc p) ≝
     621  λglobals,p,ge,st,id,flow_sig.
     622  match flow_sig with
     623  [ mk_Sig flow prf ⇒
     624    match flow return λx.flow_no_seq p globals x → ? with
     625    [ SRedirect l ⇒ λ_.
     626      ! newpc ← pointer_of_label ? p … ge
     627        (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) l ;
     628      return mk_state_pc … st newpc
     629    | STailInit id fn args ⇒ λ_.
     630      do_call … ge st id fn args
     631    | SEnd ⇒ λ_.
    418632      ! 〈st,ra〉 ← fetch_ra … st ;
    419       ! st ← pop_frame … ge st;
    420       return 〈E0,set_pc … ra st〉
    421    | sequential seq l ⇒ eval_sequential … ge st seq l
    422    | extension_fin c ⇒ exec_fin_extended … ge c st
    423    ].
     633      ! st' ← pop_frame … ge st;
     634      return mk_state_pc ? st' ra
     635    | _ ⇒ Ⓧ
     636    ] prf
     637  ]. % qed.
     638
     639lemma pointer_of_label_eq_with_id :
     640∀g.∀p : sem_params.∀ge : genv g p.∀ptr1,ptr2 : cpointer.∀lbl.
     641  block_id (pblock ptr1) = block_id (pblock ptr2) →
     642  pointer_of_label ? p ? ge ptr1 lbl = pointer_of_label ? p ? ge ptr2 lbl.
     643#g #p #ge
     644** #ty1 * #r1 #id1 #H1 inversion H1 [#s || #s] #id #EQ1 #EQ2 #EQ3 #o #EQ4 destruct
     645** #ty2 * #r2 #id2 #H2 inversion H2
     646[1,3: #s] #id2' #EQ5 #EQ6 #EQ7 #o2 #EQ8 #lbl #EQ9 destruct %
     647qed.
     648
     649
     650lemma eval_stmt_flow_no_seq_to_normal : ∀g.∀p : sem_params.∀ge.∀st : state_pc p.
     651  ∀id.∀s1 : Σs.flow_no_seq p g s.∀s2.
     652  pi1 … s1 = s2 → block_id (pblock (pc … st)) = id →
     653    (eval_stmt_flow_no_seq g p ge st id s1) =
     654    (eval_stmt_flow g p ge st s2).
     655#g#p#ge#st#id'
     656**[#lbl|#nxt*|#id#fn#args#dest#n*|#id#fn#args]*
     657#s2 #EQ #EQ' destruct(EQ)
     658whd in match eval_stmt_flow_no_seq; normalize nodelta
     659whd in match eval_stmt_flow; normalize nodelta
     660[2,3: %]
     661whd in match goto; normalize nodelta
     662whd in match set_pc; normalize nodelta
     663>pointer_of_label_eq_with_id [% | >EQ' % |]
     664qed.
     665
     666definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
     667  state_pc p → IO io_out io_in (trace × (state_pc p)) ≝
     668  λglobals,p,ge,st.
     669  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
     670  ! 〈flow, tr, st_npc〉 ← eval_statement … ge st s;
     671  let st ≝ set_no_pc … st_npc st in
     672  ! st ← eval_stmt_flow … ge st flow;
     673  return 〈tr, st〉.
    424674
    425675definition is_final: ∀globals:list ident. ∀p: sem_params.
    426   genv globals p → address → state p → option int ≝
     676  genv globals p → cpointer → state_pc p → option int ≝
    427677 λglobals,p,ge,exit,st.res_to_opt ? (
    428   do s ← fetch_statement … ge st;
     678  do s ← fetch_statement ? p … ge (pc … st);
    429679  match s with
    430680   [ RETURN ⇒
    431681      do 〈st,ra〉 ← fetch_ra … st;
    432       if eq_address ra exit then
     682      if eq_pointer ra exit then
    433683       do vals ← read_result … ge st ;
    434684       Word_of_list_beval vals
     
    436686       Error ? [ ]
    437687   | _ ⇒ Error ? [ ]]).
    438 
     688 
    439689record evaluation_parameters : Type[1] ≝
    440690 { globals: list ident
    441691 ; sparams:> sem_params
    442  ; exit: address
     692 ; exit: cpointer
    443693 ; genv2: genv globals sparams
    444694 }.
    445695
    446696definition joint_exec: trans_system io_out io_in ≝
    447   mk_trans_system … evaluation_parameters (λG. state G)
     697  mk_trans_system … evaluation_parameters (λG. state_pc G)
    448698   (λG.is_final (globals G) G (genv2 G) (exit G))
    449    (λG.eval_statement (globals G) G (genv2 G)).
     699   (λG.eval_state (globals G) G (genv2 G)).
    450700
    451701definition make_global :
     
    457707 let b ≝ mk_block Code (-1) in
    458708 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
    459  let addr ≝ address_of_code_pointer ptr in
    460709  (λp. mk_evaluation_parameters
    461710    (prog_var_names … p)
    462711    (mk_sem_params … pars)
    463     addr
     712    ptr
    464713    (globalenv Genv … p)
    465714  ).
     
    470719definition make_initial_state :
    471720 ∀pars: sem_params.
    472  ∀p: joint_program … pars. res (state pars) ≝
     721 ∀p: joint_program … pars. res (state_pc pars) ≝
    473722λpars,p.
    474723  let sem_globals ≝ make_global pars p in
     
    480729  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
    481730  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
    482   do sp ← address_of_pointer spp ;
    483731  let main ≝ prog_main … p in
    484   let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
    485   let trace_state ≝
    486    eval_call_id … pars ge st0 main (call_args_for_main … pars)
    487     (call_dest_for_main … pars) (exit sem_globals) in
    488   match trace_state with
    489   [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
    490   | Wrong msg ⇒ Error … msg
    491   | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    492   ].
    493 [3: % | cases ispb | cases spb] * #r #off #E >E %
     732  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
     733  (* use exit sem_globals as ra and call_dest_for_main as dest *)
     734  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
     735  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     736  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ?? ge main) ;
     737  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge main_block) ;
     738  match main_fd with
     739  [ Internal fn ⇒
     740    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
     741  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
     742  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
    494743qed.
    495744
  • src/utilities/bindLists.ma

    r1647 r1882  
    1 include "utilities/monad.ma".
    2 include "basics/lists/list.ma".
     1include "utilities/bind_new.ma".
    32
    4 inductive bind_list
    5   (B : Type[0])
    6   (T : Type[0])
    7   (E : Type[0])
    8   : Type[0] ≝
    9   | bnil : bind_list B T E
    10   | bcons : E → bind_list B T E → bind_list B T E
    11   | bnew : T → (B → bind_list B T E) → bind_list B T E.
    12  
    13 interpretation "new blist" 'new t f = (bnew ??? t f).
    14 interpretation "cons blist" 'cons hd tl = (bcons ??? hd tl).
    15 interpretation "nil blist" 'nil = (bnil ???).
     3definition bind_list ≝ λB,E.bind_new B (list E).
    164
    17 notation > "ν list1 ident x sep , opt('of' t) 'in' f"
    18   with precedence 48 for
    19   ${ default
    20     @{ ${ fold right @{$f} rec acc @{'new $t (λ${ident x}.$acc)} } }
    21     @{ ${ fold right @{$f} rec acc @{'new 'it (λ${ident x}.$acc)} } }
    22   }.
     5coercion blist_from_list :
     6  ∀B,E. ∀l:list E. bind_list B E ≝ λB,E,l.bret … l on _l : list ? to bind_list ??.
    237
    24 notation < "hvbox(ν ident i \nbsp 'of' \nbsp t \nbsp 'in' \nbsp break p)"
    25  with precedence 48 for
    26   @{'new $t (λ${ident i} : $ty. $p) }.
     8unification hint 0 ≔ B,E;
     9Es ≟ list E
     10(*--------------------------*)⊢
     11bind_list B E ≡ bind_new B Es.
    2712
    28 interpretation "unit it" 'it = it.
     13definition bappend : ∀B,E.bind_list B E → bind_list B E →
     14  bind_list B E ≝ λB,E. m_bin_op … (append ?).
    2915
    30 notation < "hvbox(ν ident i \nbsp 'in' \nbsp break p)"
    31  with precedence 48 for
    32     @{'new 'it (λ${ident i} : $ty. $p) }.
    33    
    34 let rec bnews B T E (tys : list T) (f : list B → bind_list B T E) on tys : bind_list B T E ≝
    35   match tys with
    36   [ nil ⇒ f [ ]
    37   | cons ty tys ⇒ νx of ty in bnews … tys (λl. f (x :: l))
    38   ].
    39  
    40 let rec bnews_strong B T E (tys : list T) (f : ∀l : list B.|l| = |tys| → bind_list B T E) on tys : bind_list B T E ≝
    41   match tys return λx.x = tys → bind_list B T E with
    42   [ nil ⇒ λprf.f [ ] ?
    43   | cons ty tys' ⇒ λprf.νx of ty in bnews_strong … tys' (λl',prf'. f (x :: l') ?)
    44   ] (refl …). destruct normalize // qed.
    45  
    46 let rec bnews_n B E n (f : list B → bind_list B unit E) on n : bind_list B unit E ≝
    47   match n with
    48   [ O ⇒ f [ ]
    49   | S n ⇒ νx in bnews_n … n (λl. f (x :: l))
    50   ].
    51  
    52 let rec bnews_n_strong B E n (f : ∀l:list B.|l| = n → bind_list B unit E) on n : bind_list B unit E ≝
    53   match n return λx.x = n → bind_list B unit E with
    54   [ O ⇒ λprf.f [ ] ?
    55   | S n' ⇒ λprf.νx in bnews_n_strong … n' (λl',prf'. f (x :: l') ?)
    56   ] (refl …). normalize // qed.
    57  
    58 interpretation "iterated typed new" 'tnews ts f = (bnews ??? ts f).
    59 interpretation "iterated untyped new" 'unews n f = (bnews_n ?? n f).
    60 interpretation "iterated typed new strong" 'stnews ts f = (bnews_strong ??? ts f).
    61 interpretation "iterated untyped new strong" 'sunews n f = (bnews_n_strong ?? n f).
     16include "ASM/Vector.ma".
     17interpretation "append blist" 'vappend l1 l2 = (bappend ?? l1 l2).
    6218
    63 notation > "νν ident l 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
    64  ${default
    65    @{ 'stnews $ts (λ${ident l}.λ${ident EQ}.$f) }
    66    @{ 'tnews $ts (λ${ident l}.$f)}
    67  }.
    68  
    69 notation > "νν ident l : ty 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
    70  ${default
    71    @{ 'stnews $ts (λ${ident l}:$ty.λ${ident EQ}.$f) }
    72    @{ 'tnews $ts (λ${ident l}:$ty.$f)}
    73  }.
    74  
    75 notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    76    @{ 'stnews $ts (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    77 notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
    78    @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
     19definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝
     20  λB,E,e,l.[e] @@ l.
    7921
    80 notation > "νν ident l ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
    81  ${default
    82    @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
    83    @{ 'unews $n (λ${ident l}.$f)}
    84  }.
    85  
    86 notation > "νν ident l : ty ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
    87  ${default
    88    @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
    89    @{ 'unews $n (λ${ident l}:$ty.$f)}
    90  }.
    91  
    92 notation < "hvbox(νν \nbsp ident l : ty ^ n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    93    @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    94 notation < "hvbox(νν_ n \nbsp ident l : ty ^ n \nbsp 'in' \nbsp break f)" with precedence 47 for
    95    @{ 'unews $n (λ${ident l} : $ty.$f) }.
     22interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2).
    9623
    97 
    98 axiom bnew_proper : ∀B,T,E. bnew B T E ⊨ eq ? ++> (eq ? ++> eq ?) ++> eq ?.
    99 (* the following is equivalent to the above *)
    100 theorem bnew_proper' : ∀X,Y,Z.Y (* non-empty *) →
    101   ∀f,g : X → bind_list X Y Z.  (∀x. f x = g x) → f = g.
    102 #X#Y#Z#y#f#g#eqf
    103 cut ('new y f = 'new y g) /2 by bnew_proper/
    104 #eq destruct //
    105 qed.
    106 
    107 definition blist_of_list : ∀B,T,E. list E →
    108   bind_list B T E ≝
    109   λB,T,E,l.
    110   let f ≝ λe.λbl. e :: bl in
    111   foldr … f [] l.
    112  
    113  
    114 coercion blist_from_list :
    115   ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???.
    116 
    117 let rec bappend A B C (l1 : bind_list A B C) l2 on l1 : bind_list A B C ≝
    118 match l1 with
    119 [ bnil ⇒ l2
    120 | bcons x l1' ⇒ x :: (bappend … l1' l2)
    121 | bnew t l1' ⇒ νx of t in bappend … (l1' x) l2
    122 ].
    123 
    124 interpretation "append blist" 'append l1 l2 = (bappend ??? l1 l2).
    125 
    126 let rec bbind A B C D (l : bind_list A B C) (f : C → bind_list A B D) on l
    127   : bind_list A B D ≝
    128   match l with
    129   [ bnil ⇒ bnil …
    130   | bcons x l1' ⇒ bappend … (f x) (bbind … l1' f)
    131   | bnew t l1' ⇒ bnew … t (λx. bbind … (l1' x) f)
    132   ].
    133  
    134 interpretation "bind_list bind" 'm_bind m f = (bbind ? ? ? ? m f).
    135 
    136 include "utilities/proper.ma".
    137 
    138 lemma bappend_assoc : ∀A,B,C.∀l1,l2,l3:bind_list A B C.
    139   ((l1@l2)@l3) = (l1 @ l2 @ l3).
    140 #A#B#C#l1 elim l1 normalize
    141 [
    142 (* case bnil *)
    143   #l2#l3 //
    144 | #x#l'#Hi#l2#l3 >Hi //
    145 | #t#l'#Hi#l2#l3 @bnew_proper //
    146 qed.
    147 
    148 lemma bbind_bappend : ∀A,B,C,D.∀l1,l2:bind_list A B C.∀f:C→bind_list A B D.
    149   ((l1 @ l2) »= f) = ((l1 »= f) @ (l2 »= f)).
    150 #A#B#C#D#l1 elim l1 normalize /2 by bnew_proper/ qed.
    151 
    152 lemma bappend_bnil : ∀A,B,C.∀l : bind_list A B C.( l@[ ]) = l.
    153 #A#B#C#l elim l normalize /2 by bnew_proper/ qed.
    154  
    155 definition BindList ≝
    156   λB,T.MakeMonadProps
    157   (* the monad *)
    158   (λX.bind_list B T X)
    159   (* return *)
    160   (λE,x.[x])
    161   (* bind *)
    162   (bbind B T)
    163   ???.
    164 [(* ret_bind *)
    165   #X#Y#x#f normalize @bappend_bnil
    166 |(* bind_ret *)
    167  #X#m elim m normalize /2 by /
    168  #t #l' #Hi @bnew_proper // normalize #s#t#eq destruct @Hi
    169 |(* bind_bind *)
    170  #X#Y#Z#m#f#g elim m normalize
    171  [//
    172  |(* case bcons *)
    173   #x #l1' #Hi <Hi @bbind_bappend
    174  |(* case bnew *)
    175   #t #l #Hi @bnew_proper //
    176   #x#y #x_eq_y destruct(x_eq_y) @Hi
    177  ]
    178 ]
    179 qed.
    180 
    181 unification hint 0 ≔ B, T, X;
    182   N ≟ BindList B T, M ≟ max_def N, O ≟ m_def M
    183 (*--------------------------------------------*) ⊢
    184   bind_list B T X ≡ monad O X.
    185 
    186 include "utilities/state.ma".
    187 
    188 let rec bcompile R T E U
    189   (fresh : T → state_monad U R)
    190   (blist : bind_list R T E) on blist : state_monad U (list E) ≝
    191   match blist with
    192   [ bnil ⇒ return [ ]
    193   | bcons x l ⇒
    194     ! res ← bcompile … fresh l ;
    195     return (x :: res)
    196   | bnew t f ⇒
    197     ! r ← fresh t ;
    198     bcompile … fresh (f r)
    199   ].
     24include "utilities/lists.ma".
    20025 
    20126theorem bcompile_append :
    202   ∀E, R, T, U, fresh, bl1, bl2.
    203   (bcompile E R T U fresh (bl1 @ bl2)) ≅
     27  ∀U, R, E, fresh, bl1, bl2.
     28  (bcompile U R (list E) fresh (bl1 @@ bl2)) ≅
    20429  (
    20530  ! l1 ← bcompile … fresh bl1 ;
     
    20732  return (l1 @ l2)
    20833  ).
    209   #E#R#T#U#fresh#bl1#bl2
    210   elim bl1 normalize
    211    [
    212      #u @pair_elim //
    213    |
    214     #x#bl1' #Hi #u0 >Hi -Hi
    215     elim (bcompile E R T U fresh bl1' u0) #u1 #l1
    216     normalize
    217     elim (bcompile E R T U fresh bl2 u1) #u2 #l2
    218     normalize //
    219    |
    220     #t #blf #Hi #u0
    221     @pair_elim normalize #u #r
    222     >(Hi r) -Hi //
     34  #U#R#E#fresh#bl1#bl2
     35  #u >bcompile_bbind normalize @pair_elim
     36  #u' #l' normalize @pair_elim
     37  #u'' #l'' normalize >bcompile_bbind #EQ #EQ'
     38  normalize >EQ normalize //
    22339qed.
     40
     41theorem bcompile_cons :
     42  ∀U, R, E, fresh, e, bl2.
     43  (bcompile U R (list E) fresh (e ::: bl2)) ≅
     44    ! l ← bcompile … fresh bl2 ; return (e :: l).
     45      #U#R#E#fresh#e#bl2 #u
     46      >bcompile_append normalize //
     47qed.
  • src/utilities/extralib.ma

    r1599 r1882  
    5353
    5454(* should be proved in nat.ma, but it's not! *)
     55(* Paolo: there is eqb_elim which does something very similar *)
    5556lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
    5657#n elim n;
     
    135136 ]
    136137qed.
     138
     139lemma associative_orb : associative ? orb.
     140*** // qed.
     141
     142lemma commutative_orb : commutative ? orb.
     143** // qed.
     144
     145lemma associative_andb : associative ? andb.
     146*** // qed.
     147
     148lemma commutative_andb : commutative ? andb.
     149** // qed.
     150
     151
     152lemma notb_false : ∀b.(¬b) = false → b = true.
     153* [#_ % | normalize #EQ destruct]
     154qed.
     155
     156lemma notb_true : ∀b.(¬b) = true → b = false.
     157* [normalize #EQ destruct | #_ %]
     158qed.
     159
     160
     161
     162notation > "Σ 〈 ident x : tyx, ident y : tyy 〉 . P" with precedence 20 for
     163  @{'sigma (λ${fresh p}.
     164    match ${fresh p} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P])}.
     165notation > "Σ 〈 ident x, ident y 〉 . P" with precedence 20 for
     166  @{'sigma (λ${fresh p}.
     167    match ${fresh p} with [mk_Prod ${ident x} ${ident y} ⇒ $P])}.
     168notation > "Σ 〈 ident x : tyx, ident y : tyy, ident z : tyz 〉 . P" with precedence 20 for
     169  @{'sigma (λ${fresh p1}.
     170    match ${fresh p1} with [mk_Prod ${fresh p2} (${ident z} : $tyz) ⇒
     171      match ${fresh p2} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P]])}.
     172notation > "Σ 〈 ident x , ident y , ident z 〉 . P" with precedence 20 for
     173  @{'sigma (λ${fresh p1}.
     174    match ${fresh p1} with [mk_Prod ${fresh p2} ${ident z} ⇒
     175      match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}.
     176
  • src/utilities/lists.ma

    r1647 r1882  
    11include "basics/lists/list.ma".
     2include "ASM/Util.ma". (* coercion from bool to Prop *)
     3
     4lemma All_map : ∀A,B,P,Q,f,l.
     5All A P l →
     6(∀a.P a → Q (f a)) →
     7All B Q (map A B f l).
     8#A #B #P #Q #f #l elim l //
     9#h #t #IH * #Ph #Pt #F % [@(F ? Ph) | @(IH Pt F)] qed.
     10
     11lemma Exists_map : ∀A,B,P,Q,f,l.
     12Exists A P l →
     13(∀a.P a → Q (f a)) →
     14Exists B Q (map A B f l).
     15#A #B #P #Q #f #l elim l //
     16#h #t #IH * #H #F
     17[ %1 @(F ? H) | %2 @(IH H F) ]
     18qed.
    219
    320lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r).
     
    3249] qed.
    3350
     51lemma All_split : ∀A,P,l. All A P l → ∀pre,x,post.l = pre @ x :: post → P x.
     52#A #P #l elim l
     53[ * * normalize [2: #y #pre'] #x #post #ABS destruct(ABS)
     54| #hd #tl #IH * #Phd #Ptl * normalize [2: #y #pre'] #x #post #EQ destruct(EQ)
     55  [ @(IH Ptl … (refl …))
     56  | @Phd
     57  ]
     58]
     59qed.
     60
    3461let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
    3562match la with
     
    5784] H.
    5885
     86lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l).
     87#A#P#l elim l //
     88#h #t #Hi * #Ph #Pt normalize
     89>rev_append_def
     90@All_append
     91[ @(Hi Pt)
     92| %{Ph I}
     93]
     94qed.
     95
     96lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l).
     97#A#P#l elim l //
     98#h #t #Hi normalize >rev_append_def
     99* [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)]
     100qed.
     101
     102include "utilities/option.ma".
     103
     104lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) →
     105  ∀l. All ? P l → opt_All ? Q (find … f l).
     106#A#B#P#Q#f#H#l elim l [#_%]
     107#x #l' #Hi
     108* #Px #AllPl'
     109whd in ⊢ (???%);
     110lapply (H x Px)
     111lapply (refl ? (f x))
     112generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//]
     113#_ whd in ⊢ (???%); @(Hi AllPl')
     114qed.
     115
    59116include "utilities/monad.ma".
    60117
     
    65122  list
    66123  (λX,x.[x])
    67   (λX,Y,l,f.\fold [append ?, [ ]]_{x ∈ l} (f x))
    68   ???. normalize
     124  (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l)
     125  ????. normalize
    69126[ / by /
    70127| #X#m elim m normalize //
    71128| #X#Y#Z #m #f#g
    72129  elim m normalize [//]
    73   #x#l' #Hi
    74   <(fold_sum ?? (f x) ? [ ] (Append ?))
    75   >Hi //
     130  #x#l' #Hi elim (f x)
     131  [@Hi] normalize #hd #tl #IH >associative_append >IH %
     132|#X#Y#m #f #g #H elim m normalize [//]
     133  #hd #tl #IH >H >IH %
    76134] qed.
    77135
    78136unification hint 0 ≔ X ;
    79 N ≟ max_def List, M ≟ m_def N
     137N ≟ max_def List
    80138(*---------------------------*)⊢
    81 list X ≡ monad M X.
     139list X ≡ monad N X.
     140
     141definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l.
     142
     143lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x.
     144#A#P#l#x #Pl #xl elim (Exists_All … xl Pl)
     145#x' * #EQx' >EQx' //
     146qed.
     147
     148lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l.
     149#A#P#l elim l
     150[#_ %
     151|#x #l' #IH #H %
     152  [ @H % %
     153  | @IH #y #G @H %2 @G
     154  ]
     155]
     156qed.
     157
     158
     159lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1.
     160#A#l1 elim l1 normalize
     161[ #l2 #n #ABS elim (absurd ? ABS ?) //
     162| #x #l' #IH #l2 #n cases n normalize
     163  [//
     164  | #n #H @IH @le_S_S_to_le assumption
     165  ]
     166]
     167qed.
     168
     169lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
     170#A#l1 elim l1
     171[#l2 #n #_ <minus_n_O %
     172|#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???);
     173  cases n -n
     174  [  #ABS elim (absurd ? ABS ?) //
     175  | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption
     176  ]
     177]
     178qed.
     179
     180lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x →
     181  nth_opt A n (l1 @ l2) = Some ? x.
     182#A #l1 elim l1 normalize
     183[ #l2 #n #x #ABS destruct
     184| #hd #tl #IH #l2 * [2: #n] #x normalize /2 by /
     185]
     186qed.
     187
     188lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? →
     189  nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
     190#A #l1 elim l1 normalize
     191[ #l2 #n #_ <minus_n_O %
     192| #hd #tl #IH #l2 * [2: #n] normalize
     193  [ @IH
     194  | #ABS destruct(ABS)
     195  ]
     196]
     197qed.
     198
     199 
     200(* count occurrences satisfying a test *)
     201let rec count A (f : A → bool) (l : list A) on l : ℕ ≝
     202  match l with
     203  [ nil ⇒ 0
     204  | cons x l' ⇒ (if f x then 1 else 0) + count A f l'
     205  ].
     206 
     207theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2.
     208#A #f #l1 elim l1
     209[ #l2 %
     210| #hd #tl #IH #l2 normalize elim (f hd) normalize >IH %
     211]
     212qed.
     213
     214
     215include "utilities/option.ma".
     216
     217lemma position_of_from_aux : ∀A,test,l,n.
     218  position_of_aux A test l n = !n' ← position_of A test l; return n + n'.
     219#A #test #l elim l
     220[ normalize #_ %
     221| #hd #tl #IH #n
     222  normalize in ⊢ (??%?); >IH
     223  normalize elim (test hd) normalize
     224  [ <plus_n_O %
     225  | >(IH 1) whd in match (position_of ???);
     226    elim (position_of_aux ??? 0) normalize
     227    [ % | #x <plus_n_Sm % ]
     228  ]
     229]
     230qed.
     231
     232definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1.
     233  opt_safe ? (position_of A test l) ?.
     234  lapply prf -prf elim l normalize
     235  [ #ABS elim (absurd ? ABS (not_le_Sn_O 0))
     236  |#hd #tl #IH elim (test hd) normalize
     237    [2: >position_of_from_aux #H
     238      change with (position_of_aux ????) in match (position_of ???);
     239      >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x]
     240    #_ % #ABS destruct(ABS)
     241qed.
     242
     243definition index_of ≝
     244  λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?.
     245  lapply prf -prf @eqb_elim #EQ * >EQ %
     246qed.
     247
     248lemma position_of_append_hit : ∀A,test,l1,l2,x.
     249  position_of A test (l1@l2) = Some ? x →
     250    position_of A test l1 = Some ? x ∨
     251      (position_of A test l1 = None ? ∧
     252        ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x).
     253#A#test#l1 elim l1
     254[ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2
     255  % %
     256| #hd #tl #IH #l2 #x
     257  normalize elim (test hd) normalize
     258  [#H %{H}
     259  | >position_of_from_aux
     260    lapply (refl … (position_of A test (tl@l2)))
     261    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
     262    normalize #EQ destruct(EQ)
     263    elim (IH … Heq) -IH
     264    [ #G %
     265    | * #G #H
     266     lapply (refl … (position_of A test l2))
     267     generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize
     268     #EQ destruct (EQ) %2 %]
     269    >position_of_from_aux
     270    [1,2: >G % | >H' %]
     271  ]
     272]
     273qed.
     274
     275lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x →
     276  count A test l ≥ 1.
     277#A#test#l elim l normalize
     278[#x #ABS destruct(ABS)
     279|#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //]
     280  >position_of_from_aux
     281  lapply (refl … (position_of ? test tl))
     282  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
     283  #EQ destruct(EQ) @(IH … Heq)
     284]
     285qed.
     286
     287lemma position_of_miss : ∀A,test,l.position_of A test l = None ? →
     288  count A test l = 0.
     289#A#test#l elim l normalize
     290[ #_ %
     291|#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)]
     292  >position_of_from_aux
     293  lapply (refl … (position_of ? test tl))
     294  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
     295  #EQ destruct(EQ) @(IH … Heq)
     296]
     297qed.
     298
     299
     300lemma position_of_append_miss : ∀A,test,l1,l2.
     301  position_of A test (l1@l2) = None ? →
     302    position_of A test l1 = None ? ∧ position_of A test l2 = None ?.
     303#A#test#l1 elim l1
     304[ #l2 change with l2 in match (? @ l2); #EQ >EQ % %
     305| #hd #tl #IH #l2
     306  normalize elim (test hd) normalize
     307  [#H destruct(H)
     308  | >position_of_from_aux
     309    lapply (refl … (position_of A test (tl@l2)))
     310    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
     311    normalize #EQ destruct(EQ)
     312    elim (IH … Heq) #H1 #H2
     313    >position_of_from_aux
     314    >position_of_from_aux
     315    >H1 >H2 normalize % %
     316  ]
     317]
     318qed.
     319
     320
  • src/utilities/monad.ma

    r1648 r1882  
    22include "basics/relations.ma".
    33include "utilities/setoids.ma".
    4 include "utilities/proper.ma".
     4
     5definition pred_transformer ≝ λA,B : Type[0].(A → Prop) → B → Prop.
     6
     7definition modus_ponens ≝ λA,B.λPT : pred_transformer A B.
     8  ∀P,Q.(∀x.P x → Q x) → ∀y.PT P y → PT Q y.
     9 
     10lemma mp_transitive :
     11  ∀A,B,C,PT1,PT2.modus_ponens A B PT1 → modus_ponens B C PT2 →
     12    modus_ponens A C (PT2 ∘ PT1). /4/ qed.
     13
     14definition rel_transformer ≝ λA,B,C,D : Type[0].
     15  (A → B → Prop) → C → D → Prop.
     16 
     17definition rel_modus_ponens ≝ λA,B,C,D.λRT : rel_transformer A B C D.
     18  ∀P,Q.(∀x,y.P x y → Q x y) → ∀z,w.RT P z w → RT Q z w.
     19 
     20lemma rel_mp_transitive :
     21  ∀A,B,C,D,E,F,RT1,RT2.rel_modus_ponens A B C D RT1 → rel_modus_ponens C D E F RT2 →
     22    rel_modus_ponens … (RT2 ∘ RT1). /4/ qed.
    523 
    6 record MonadDefinition : Type[1] ≝ {
     24record Monad : Type[1] ≝ {
    725  monad : Type[0] → Type[0] ;
    826  m_return : ∀X. X → monad X ;
     
    1129
    1230notation "m »= f" with precedence 49
    13   for @{'m_bind $m $f) }.
     31  for @{'m_bind $m $f }.
    1432
    1533notation > "!_ e; e'"
     
    104122
    105123
    106 include "basics/lists/list.ma".
    107 
    108 
    109 (* add structure and properties as needed *)
    110 record Monad : Type[1] ≝ {
    111   m_def :> MonadDefinition ;
    112   m_map : ∀X, Y. (X → Y) → monad m_def X → monad m_def Y ;
    113   m_map2 : ∀X, Y, Z. (X → Y → Z) →
    114     monad m_def X → monad m_def Y → monad m_def Z;
    115   m_bind2 : ∀X,Y,Z.monad m_def (X×Y) → (X → Y → monad m_def Z) → monad m_def Z;
    116   m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W;
    117   m_join : ∀X.monad m_def (monad m_def X) → monad m_def X;
    118   m_sigbind2 : ∀A,B,C.∀P:A×B → Prop. monad m_def (Σx:A×B.P x) →
    119       (∀a,b. P 〈a,b〉 → monad m_def C) → monad m_def C;
    120   m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y);
    121   m_mmap_sigma : ∀X,Y,P.(X → monad m_def (Σy : Y.P y)) → list X → monad m_def (Σl : list Y.All ? P l)
    122 }.
    123 
    124 interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
    125 interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
    126 interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
    127 
    128 (*
    129 check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H)
    130 *)
    131 
    132124record MonadProps : Type[1] ≝
    133125  { max_def :> Monad
     
    136128  ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y.
    137129      ∀g : Y → monad max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y
     130  ; m_bind_ext_eq : ∀X,Y.∀m : monad max_def X.∀f,g : X → monad max_def Y.
     131      (∀x.f x = g x) → ! x ← m ; f x = ! x ← m ; g x
    138132  }.
    139133
     
    144138  ; sm_eq_trans : ∀X.transitive ? (sm_eq X)
    145139  ; sm_eq_sym : ∀X.symmetric ? (sm_eq X)
    146   ; sm_return_proper : ∀X .m_return smax_def X ⊨ eq ? ++> sm_eq ?
    147   ; sm_bind_proper : ∀X, Y.m_bind smax_def X Y ⊨ sm_eq ? ++> (eq ? ++> sm_eq ?) ++> sm_eq ?
     140  ; sm_return_proper : ∀X,x.sm_eq X (return x) (return x)
     141  ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y (x »= f) (y »= g)
    148142  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y.
    149143      sm_eq Y (! y ← return x ; f y) (f x)
     
    153147  }.
    154148
    155 interpretation "monad setoid equality" 'std_eq x y = (sm_eq ?? x y).
    156 
    157 
    158 definition MakeMonad : ?→?→?→Monad ≝ λmonad,m_return,m_bind.
    159   mk_Monad (mk_MonadDefinition monad m_return m_bind)
    160   (* map *)
    161   (λX,Y,f,m.
    162     ! x ← m ;
    163     return f x)
    164   (* map2 *)
    165   (λX,Y,Z,f,m,n.
    166     ! x ← m ;
    167     ! y ← n ;
    168     return (f x y))
    169   (* bind2 *)
    170   (λX,Y,Z,m,f.
    171     ! p ← m ;
    172     let 〈x, y〉 ≝ p in
    173     f x y)
    174   (λX,Y,Z,W,m,f.
    175     ! p ← m ;
    176     let 〈x, y, z〉 ≝ p in
    177     f x y z)
    178   (* join *)
    179   (λX,m.! x ← m ; x)
    180   (* m_sigbind2 *)
    181   (λA,B,C,P,e,f.
     149definition setoid_of_monad : ∀M : SetoidMonadProps.∀X : Type[0].
     150  Setoid ≝
     151  λM,X.mk_Setoid (monad M X) (sm_eq M X) (sm_eq_refl M X) (sm_eq_trans M X) (sm_eq_sym M X).
     152
     153include "hints_declaration.ma".
     154
     155unification hint 0 ≔ M, X;
     156M' ≟ smax_def M, S ≟ setoid_of_monad M X
     157(*-----------------------------*)⊢
     158monad M' X ≡ std_supp S.
     159
     160include "basics/lists/list.ma".
     161
     162definition m_map ≝ λM,X,Y.λf : X → Y.λm : monad M X.
     163  ! x ← m ; return f x.
     164
     165definition m_map2 ≝ λM,X,Y,Z.λf : X → Y → Z.λm : monad M X.λn : monad M Y.
     166  ! x ← m ; ! y ← n ; return f x y.
     167 
     168definition m_bind2 ≝ λM,X,Y,Z.λm : monad M (X × Y).λf : X → Y → monad M Z.
     169  ! p ← m ; f (\fst p) (\snd p).
     170
     171interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
     172
     173definition m_bind3 :
     174  ∀M,X,Y,Z,W.monad M (X×Y×Z) → (X → Y → Z → monad M W) → monad M W ≝
     175  λM,X,Y,Z,W,m,f.
     176  ! p ← m ; f (\fst (\fst p)) (\snd (\fst p)) (\snd p).
     177
     178interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
     179
     180definition m_join : ∀M,X.monad M (monad M X) → monad M X ≝
     181  λM,X,m.! x ← m ; x.
     182
     183definition m_sigbind2 :
     184  ∀M,A,B,C.∀P:A×B → Prop. monad M (Σx:A×B.P x) →
     185      (∀a,b. P 〈a,b〉 → monad M C) → monad M C ≝
     186λM,A,B,C,P,e,f.
    182187    ! e_sig ← e ;
    183188    match e_sig with
     
    187192      λeq_p.  f a b (eq_ind_r ?? (λx.λ_.P x) p_prf ? eq_p)
    188193      ](refl …)
    189     ])
    190   (λX,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l)
    191   (λX,Y,P,f,l.foldr … (λel,macc.
     194    ].
     195
     196interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
     197
     198definition m_list_map :
     199  ∀M,X,Y.(X → monad M Y) → list X → monad M (list Y) ≝
     200  λM,X,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l.
     201
     202definition m_list_map_sigma :
     203  ∀M,X,Y,P.(X → monad M (Σy : Y.P y)) → list X → monad M (Σl : list Y.All ? P l) ≝
     204  λM,X,Y,P,f,l.foldr … (λel,macc.
    192205    ! «r, r_prf» ← f el ;
    193206    ! «acc, acc_prf» ← macc ;
    194207    return (mk_Sig ?? (r :: acc) ?))
    195     (return (mk_Sig … [ ] ?)) l).
    196   % assumption qed.
    197 
    198 definition MakeMonadProps : ?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind,p1,p2,p3.
    199 mk_MonadProps (MakeMonad monad m_return m_bind) p1 p2 p3.
     208    (return (mk_Sig … [ ] ?)) l. % assumption qed.
     209
     210definition m_bin_op :
     211  ∀M,X,Y,Z.(X → Y → Z) → monad M X → monad M Y → monad M Z ≝
     212  λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y.
     213
     214unification hint 0 ≔ M, X, Y, Z, m, f ⊢
     215m_bind M (X×Y) Z m (λp.f (\fst p) (\snd p)) ≡ m_bind2 M X Y Z m f.
     216
     217unification hint 0 ≔ M, X, Y, Z, W, m, f ⊢
     218m_bind M (X×Y×Z) W m (λp.f (\fst (\fst p)) (\snd (\fst p)) (\snd p)) ≡
     219m_bind3 M X Y Z W m f.
     220
     221definition MakeMonadProps : ?→?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind.
     222mk_MonadProps (mk_Monad monad m_return m_bind).
    200223
    201224definition MakeSetoidMonadProps : ?→?→?→?→?→?→?→?→?→?→?→?→SetoidMonadProps ≝
    202   λmonad,m_return,m_bind,sm_eq,p1,p2,p3,p4,p5,p6,p7,p8.
    203   mk_SetoidMonadProps (MakeMonad monad m_return m_bind) sm_eq p1 p2 p3 p4 p5 p6 p7 p8.
     225  λmonad,m_return,m_bind.
     226  mk_SetoidMonadProps (mk_Monad monad m_return m_bind).
     227 
     228record MonadPred (M : Monad) : Type[1] ≝
     229  { m_pred :> ∀X.pred_transformer X (monad M X)
     230  ; mp_return : ∀X,P,x.P x → m_pred X P (return x)
     231  ; mp_bind : ∀X,Y,Pin,Pout,m.m_pred X Pin m →
     232      ∀f.(∀x.Pin x → m_pred Y Pout (f x)) →
     233                  m_pred ? Pout (m_bind … m f)
     234  ; m_pred_mp : ∀X.modus_ponens ?? (m_pred X)
     235  }.
     236
     237record MonadRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
     238  { m_rel :> ∀X,Y.rel_transformer X Y (monad M1 X) (monad M2 Y)
     239  ; mr_return : ∀X,Y,rel,x,y.rel x y → m_rel X Y rel (return x) (return y)
     240  ; mr_bind : ∀X,Y,Z,W,relin,relout,m,n.m_rel X Y relin m n → ∀f,g.(∀x,y.relin x y → m_rel Z W relout (f x) (g y)) →
     241                  m_rel ?? relout (m_bind … m f) (m_bind … n g)
     242  ; m_rel_mp : ∀X,Y.rel_modus_ponens ???? (m_rel X Y)
     243  }.
  • src/utilities/option.ma

    r1647 r1882  
    99  (* bind *)
    1010  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
    11   ???.
    12 // #X[2:#Y#Z]*normalize//qed.
     11  ????.
     12// #X[|*:#Y[#Z]]*normalize//qed.
    1313
    1414include "hints_declaration.ma".
    1515unification hint 0 ≔ X;
    16 N ≟ max_def Option, M ≟ m_def N
     16N ≟ max_def Option
    1717(*---------------*) ⊢
    18 option X ≡ monad M X
     18option X ≡ monad N X
    1919.
    2020
     
    2424  | None ⇒ λeq_m.?
    2525  ] (refl …). elim (absurd … eq_m prf) qed.
     26
     27lemma opt_to_opt_safe : ∀A,m,prf. m = Some ? (opt_safe A m prf).
     28#A *
     29[ #ABS elim (absurd ? (refl ??) ABS)
     30| //
     31] qed.
     32
     33lemma opt_safe_elim : ∀A.∀P : A → Prop.∀m,prf.
     34  (∀x.m = Some ? x → P x) → P (opt_safe ? m prf).
     35#A#P*
     36[#prf elim(absurd … (refl ??) prf)
     37|#x normalize #_ #H @H @refl
     38] qed.
     39
     40definition opt_try_catch : ∀X.option X → (unit → X) → X ≝
     41  λX,m,f.match m with [Some x ⇒ x | None ⇒ f it].
     42
     43notation > "'Try' m 'catch' opt (ident e opt( : ty)) ⇒ f" with precedence 46 for
     44  ${ default
     45    @{ ${ default
     46      @{'trycatch $m (λ${ident e}:$ty.$f)}
     47      @{'trycatch $m (λ${ident e}.$f)}
     48    }}
     49    @{'trycatch $m (λ_.$f)}
     50  }.
     51
     52notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ident e : ty \nbsp ⇒ \nbsp break f)" with precedence 46 for
     53  @{'trycatch $m (λ${ident e}:$ty.$f)}.
     54notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ⇒ \nbsp break f)" with precedence 46 for
     55  @{'trycatch $m (λ_:$ty.$f)}.
     56
     57interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
     58
     59definition OptPred ≝ λPdef : Prop.mk_MonadPred Option (λX,P,m.Try ! x ← m ; return P x catch ⇒ Pdef) ???.
     60#X[2:#Y]#P1[1,3:#P2[2:#H]*] normalize /2/
     61qed.
     62
     63definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True).
     64 
     65lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o
     66  ≝ m_pred_mp ….
     67
     68definition opt_Exists : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred False).
     69 
     70lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
     71  ≝ m_pred_mp ….
     72
  • src/utilities/state.ma

    r1647 r1882  
    1212  (λX,c1,c2.∀s.c1 s = c2 s)
    1313  ????????.
    14 //
     14// normalize
    1515#X
    1616[ (* bind_proper *)
    17   #Y #m#n #m_eq_n
    18   #f #g #f_eq_g
    19   #s
    20   generalize in match (m_eq_n s); -m_eq_n
    21   normalize
    22   #m_eq_n >m_eq_n -m_eq_n
    23   elim (n s) #s' #y
    24   normalize @f_eq_g //
    25 | #m#s normalize
    26   elim (m s) normalize /2 by /
    27 | #Y #Z #m #f #g #s normalize
    28   elim (m s) normalize
    29   #s' #x
    30   elim (f x s') normalize
    31   #s'' #y //
     17  #Y #m #n #f #g #H #G #s >H elim (n s) #s' #x normalize @G
     18| #m#s @pair_elim //
     19| #Y#Z #m #f #g #s elim (m s) //
    3220]
    3321qed.
     
    4129include "hints_declaration.ma".
    4230unification hint 0 ≔ S,X;
    43 N ≟ State S, M ≟ smax_def N, O ≟ m_def M
     31N ≟ State S, M ≟ smax_def N
    4432(*---------------*) ⊢
    45 state_monad S X ≡ monad O X
     33state_monad S X ≡ monad M X
    4634.
    4735
     36definition StatePred ≝ λS.λPs : S → Prop.mk_MonadPred (State S)
     37  (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???.
     38[ normalize /2/
     39| normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps)
     40  elim (m s) #s' #x normalize * /2/
     41| #X #P #Q #H #m normalize #G #s #Ps elim (G … Ps) /3/
     42]
     43qed.
     44
     45definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (State S) (State T)
     46  (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in
     47    Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
     48[ normalize /2/
     49| normalize #X#Y#Z#W#P1#P2 #m #n #H #f #g #G #s #t #Ps lapply (H … Ps)
     50  * elim (m s) elim (n t) /2/
     51| #X #Y #P #Q #H #m #n normalize #G #s #t #Ps elim (G … Ps) /3/
     52]
     53qed.
     54
  • src/utilities/trace.ma

    r1635 r1882  
    2626M ≟ Trace T
    2727(*---------------*) ⊢
    28 X × (list T) ≡ monad (m_def M) X
     28X × (list T) ≡ monad M X
    2929.
    3030
Note: See TracChangeset for help on using the changeset viewer.