- Timestamp:
- Mar 30, 2011, 6:47:35 PM (10 years ago)
- Location:
- src
- Files:
-
- 14 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/BitVector.ma
r724 r726 102 102 false) b c. 103 103 104 lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.104 lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y. 105 105 (x = y → P true) → 106 106 (x ≠ y → P false) → -
src/ASM/BitVectorTrie.ma
r698 r726 7 7 | Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) 8 8 | Stub: ∀n: nat. BitVectorTrie A n. 9 10 let rec lookup_opt (A: Type[0]) (n: nat) 11 (b: BitVector n) (t: BitVectorTrie A n) on t 12 : option A ≝ 13 (match t return λx.λ_. BitVector x → option A with 14 [ Leaf l ⇒ λ_.Some ? l 15 | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l) 16 | Stub _ ⇒ λ_.None ? 17 ]) b. 9 18 10 19 let rec lookup (A: Type[0]) (n: nat) -
src/ASM/Vector.ma
r700 r726 429 429 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 430 430 431 definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝ 432 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with 433 [ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ]. 434 435 definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝ 436 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with 437 [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ]. 438 431 439 let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝ 432 (match b return λx.λ_. n = x → bool with 433 [ VEmpty ⇒ 434 match c return λx.λ_. x = O → bool with 435 [ VEmpty ⇒ λ_. true 436 | VCons p hd tl ⇒ λabsd.⊥ 437 ] 438 | VCons o hd tl ⇒ 439 match c return λx.λ_. x = S o → bool with 440 [ VEmpty ⇒ λabsd.⊥ 441 | VCons p hd' tl' ⇒ 442 λprf. 443 if (f hd hd') then 444 (eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉)) 445 else 446 false 447 ] 448 ]) (refl ? n). 449 [1,2: 450 destruct 451 | lapply (injective_S … prf); 452 # X 453 < X 454 % 455 ] 456 qed. 457 458 lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n. 459 match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with 440 (match b return λx.λ_. Vector A x → bool with 441 [ VEmpty ⇒ λc. 442 match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool | _ ⇒ True ] with 443 [ VEmpty ⇒ true 444 | VCons p hd tl ⇒ I 445 ] 446 | VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c)) 447 ] 448 ) c. 449 450 lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n. 451 match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with 460 452 [ O ⇒ λP.λv.P [[ ]] → P v 461 453 | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v 462 454 ] P v. 463 @(λA,n. λP:Vector A n → Prop. λv. match v return455 @(λA,n. λP:Vector A n → Type[0]. λv. match v return 464 456 ? 465 457 with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P) … … 469 461 *) 470 462 471 (* dpm: commented out to get out stuff to typecheck *) 472 lemma eq_v_elim: ∀P:bool → Prop. ∀A,f. 473 (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → 463 lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f. 464 (∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → 474 465 ∀n,x,y. 475 466 (x = y → P true) → -
src/Clight/AST.ma
r718 r726 21 21 include "common/Integers.ma". 22 22 include "common/Floats.ma". 23 include " utilities/binary/positive.ma".23 include "ASM/BitVector.ma". 24 24 25 25 (* * * Syntactic elements *) … … 28 28 etc) are represented by the type [positive] of positive integers. *) 29 29 30 definition ident ≝ Pos.30 definition ident ≝ Word. 31 31 32 32 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y). 33 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y); 34 [ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed. 33 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %) #E 34 [ % | %2 ] 35 lapply E @eq_bv_elim 36 [ 1,4: #H #_ @H | *: #_ #H destruct ] 37 qed. 38 39 definition ident_of_nat ≝ bitvector_of_nat 16. 35 40 36 41 (* Memory spaces *) -
src/Clight/CexecComplete.ma
r708 r726 328 328 | #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3 329 329 < H3 whd in H1:(??%?) ⊢ (??%?) 330 destruct (H1) //330 destruct (H1) @refl 331 331 ] qed. 332 332 -
src/Clight/test/duff.ma
r725 r726 2 2 3 3 definition myprog := mk_program clight_fundef type 4 [〈 succ_pos_of_nat 0 (* copy *), CL_Internal (5 mk_function Tvoid [〈 succ_pos_of_nat 19, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 20, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 21, (Tint I32 Signed )〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 2, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 3, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 4, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 5, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 7, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 8, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 9, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 10, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 11, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 12, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 13, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 14, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 15, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 16, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 17, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 18, (Tpointer Any (Tint I16 Signed ))〉 ]4 [〈ident_of_nat 0 (* copy *), CL_Internal ( 5 mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed )〉 ] [〈ident_of_nat 1, (Tint I32 Signed )〉 ; 〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed ))〉 ] 6 6 (Ssequence 7 (Sassign (Expr (Evar ( succ_pos_of_nat 1)) (Tint I32 Signed ))7 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) 8 8 (Expr (Ebinop Odiv 9 9 (Expr (Ebinop Oadd 10 (Expr (Evar ( succ_pos_of_nat 21)) (Tint I32 Signed ))10 (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed )) 11 11 (Expr (Econst_int (repr 7)) (Tint I32 Signed ))) 12 12 (Tint I32 Signed )) … … 14 14 (Tint I32 Signed ))) 15 15 (Sswitch (Expr (Ebinop Omod 16 (Expr (Evar ( succ_pos_of_nat 21)) (Tint I32 Signed ))16 (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed )) 17 17 (Expr (Econst_int (repr 8)) (Tint I32 Signed ))) 18 18 (Tint I32 Signed )) ( 19 19 (LScase (repr 0) 20 (Slabel ( succ_pos_of_nat 22)20 (Slabel (ident_of_nat 22) 21 21 (Ssequence 22 22 (Ssequence 23 (Sassign (Expr (Evar ( succ_pos_of_nat 17))23 (Sassign (Expr (Evar (ident_of_nat 17)) 24 24 (Tpointer Any (Tint I16 Signed ))) 25 (Expr (Evar ( succ_pos_of_nat 19))25 (Expr (Evar (ident_of_nat 19)) 26 26 (Tpointer Any (Tint I16 Signed )))) 27 (Sassign (Expr (Evar ( succ_pos_of_nat 19))27 (Sassign (Expr (Evar (ident_of_nat 19)) 28 28 (Tpointer Any (Tint I16 Signed ))) 29 29 (Expr (Ebinop Oadd 30 (Expr (Evar ( succ_pos_of_nat 17))30 (Expr (Evar (ident_of_nat 17)) 31 31 (Tpointer Any (Tint I16 Signed ))) 32 32 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) … … 34 34 (Ssequence 35 35 (Ssequence 36 (Sassign (Expr (Evar ( succ_pos_of_nat 18))36 (Sassign (Expr (Evar (ident_of_nat 18)) 37 37 (Tpointer Any (Tint I16 Signed ))) 38 (Expr (Evar ( succ_pos_of_nat 20))38 (Expr (Evar (ident_of_nat 20)) 39 39 (Tpointer Any (Tint I16 Signed )))) 40 (Sassign (Expr (Evar ( succ_pos_of_nat 20))40 (Sassign (Expr (Evar (ident_of_nat 20)) 41 41 (Tpointer Any (Tint I16 Signed ))) 42 42 (Expr (Ebinop Oadd 43 (Expr (Evar ( succ_pos_of_nat 18))43 (Expr (Evar (ident_of_nat 18)) 44 44 (Tpointer Any (Tint I16 Signed ))) 45 45 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 46 46 (Tpointer Any (Tint I16 Signed ))))) 47 47 (Sassign (Expr (Ederef 48 (Expr (Evar ( succ_pos_of_nat 17))48 (Expr (Evar (ident_of_nat 17)) 49 49 (Tpointer Any (Tint I16 Signed )))) 50 50 (Tint I16 Signed )) 51 51 (Expr (Ederef 52 (Expr (Evar ( succ_pos_of_nat 18))52 (Expr (Evar (ident_of_nat 18)) 53 53 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )))))) 54 54 (LScase (repr 7) 55 55 (Ssequence 56 (Sassign (Expr (Evar ( succ_pos_of_nat 15))56 (Sassign (Expr (Evar (ident_of_nat 15)) 57 57 (Tpointer Any (Tint I16 Signed ))) 58 (Expr (Evar ( succ_pos_of_nat 19))58 (Expr (Evar (ident_of_nat 19)) 59 59 (Tpointer Any (Tint I16 Signed )))) 60 60 (Ssequence 61 (Sassign (Expr (Evar ( succ_pos_of_nat 19))61 (Sassign (Expr (Evar (ident_of_nat 19)) 62 62 (Tpointer Any (Tint I16 Signed ))) 63 63 (Expr (Ebinop Oadd 64 (Expr (Evar ( succ_pos_of_nat 15))64 (Expr (Evar (ident_of_nat 15)) 65 65 (Tpointer Any (Tint I16 Signed ))) 66 66 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 67 67 (Tpointer Any (Tint I16 Signed )))) 68 68 (Ssequence 69 (Sassign (Expr (Evar ( succ_pos_of_nat 16))69 (Sassign (Expr (Evar (ident_of_nat 16)) 70 70 (Tpointer Any (Tint I16 Signed ))) 71 (Expr (Evar ( succ_pos_of_nat 20))71 (Expr (Evar (ident_of_nat 20)) 72 72 (Tpointer Any (Tint I16 Signed )))) 73 73 (Ssequence 74 (Sassign (Expr (Evar ( succ_pos_of_nat 20))74 (Sassign (Expr (Evar (ident_of_nat 20)) 75 75 (Tpointer Any (Tint I16 Signed ))) 76 76 (Expr (Ebinop Oadd 77 (Expr (Evar ( succ_pos_of_nat 16))77 (Expr (Evar (ident_of_nat 16)) 78 78 (Tpointer Any (Tint I16 Signed ))) 79 79 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 80 80 (Tpointer Any (Tint I16 Signed )))) 81 81 (Sassign (Expr (Ederef 82 (Expr (Evar ( succ_pos_of_nat 15))82 (Expr (Evar (ident_of_nat 15)) 83 83 (Tpointer Any (Tint I16 Signed )))) 84 84 (Tint I16 Signed )) 85 85 (Expr (Ederef 86 (Expr (Evar ( succ_pos_of_nat 16))86 (Expr (Evar (ident_of_nat 16)) 87 87 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed ))))))) 88 88 (LScase (repr 6) 89 89 (Ssequence 90 (Sassign (Expr (Evar ( succ_pos_of_nat 13))90 (Sassign (Expr (Evar (ident_of_nat 13)) 91 91 (Tpointer Any (Tint I16 Signed ))) 92 (Expr (Evar ( succ_pos_of_nat 19))92 (Expr (Evar (ident_of_nat 19)) 93 93 (Tpointer Any (Tint I16 Signed )))) 94 94 (Ssequence 95 (Sassign (Expr (Evar ( succ_pos_of_nat 19))95 (Sassign (Expr (Evar (ident_of_nat 19)) 96 96 (Tpointer Any (Tint I16 Signed ))) 97 97 (Expr (Ebinop Oadd 98 (Expr (Evar ( succ_pos_of_nat 13))98 (Expr (Evar (ident_of_nat 13)) 99 99 (Tpointer Any (Tint I16 Signed ))) 100 100 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 101 101 (Tpointer Any (Tint I16 Signed )))) 102 102 (Ssequence 103 (Sassign (Expr (Evar ( succ_pos_of_nat 14))103 (Sassign (Expr (Evar (ident_of_nat 14)) 104 104 (Tpointer Any (Tint I16 Signed ))) 105 (Expr (Evar ( succ_pos_of_nat 20))105 (Expr (Evar (ident_of_nat 20)) 106 106 (Tpointer Any (Tint I16 Signed )))) 107 107 (Ssequence 108 (Sassign (Expr (Evar ( succ_pos_of_nat 20))108 (Sassign (Expr (Evar (ident_of_nat 20)) 109 109 (Tpointer Any (Tint I16 Signed ))) 110 110 (Expr (Ebinop Oadd 111 (Expr (Evar ( succ_pos_of_nat 14))111 (Expr (Evar (ident_of_nat 14)) 112 112 (Tpointer Any (Tint I16 Signed ))) 113 113 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 114 114 (Tpointer Any (Tint I16 Signed )))) 115 115 (Sassign (Expr (Ederef 116 (Expr (Evar ( succ_pos_of_nat 13))116 (Expr (Evar (ident_of_nat 13)) 117 117 (Tpointer Any (Tint I16 Signed )))) 118 118 (Tint I16 Signed )) 119 119 (Expr (Ederef 120 (Expr (Evar ( succ_pos_of_nat 14))120 (Expr (Evar (ident_of_nat 14)) 121 121 (Tpointer Any (Tint I16 Signed )))) 122 122 (Tint I16 Signed ))))))) 123 123 (LScase (repr 5) 124 124 (Ssequence 125 (Sassign (Expr (Evar ( succ_pos_of_nat 11))125 (Sassign (Expr (Evar (ident_of_nat 11)) 126 126 (Tpointer Any (Tint I16 Signed ))) 127 (Expr (Evar ( succ_pos_of_nat 19))127 (Expr (Evar (ident_of_nat 19)) 128 128 (Tpointer Any (Tint I16 Signed )))) 129 129 (Ssequence 130 (Sassign (Expr (Evar ( succ_pos_of_nat 19))130 (Sassign (Expr (Evar (ident_of_nat 19)) 131 131 (Tpointer Any (Tint I16 Signed ))) 132 132 (Expr (Ebinop Oadd 133 (Expr (Evar ( succ_pos_of_nat 11))133 (Expr (Evar (ident_of_nat 11)) 134 134 (Tpointer Any (Tint I16 Signed ))) 135 135 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 136 136 (Tpointer Any (Tint I16 Signed )))) 137 137 (Ssequence 138 (Sassign (Expr (Evar ( succ_pos_of_nat 12))138 (Sassign (Expr (Evar (ident_of_nat 12)) 139 139 (Tpointer Any (Tint I16 Signed ))) 140 (Expr (Evar ( succ_pos_of_nat 20))140 (Expr (Evar (ident_of_nat 20)) 141 141 (Tpointer Any (Tint I16 Signed )))) 142 142 (Ssequence 143 (Sassign (Expr (Evar ( succ_pos_of_nat 20))143 (Sassign (Expr (Evar (ident_of_nat 20)) 144 144 (Tpointer Any (Tint I16 Signed ))) 145 145 (Expr (Ebinop Oadd 146 (Expr (Evar ( succ_pos_of_nat 12))146 (Expr (Evar (ident_of_nat 12)) 147 147 (Tpointer Any (Tint I16 Signed ))) 148 148 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 149 149 (Tpointer Any (Tint I16 Signed )))) 150 150 (Sassign (Expr (Ederef 151 (Expr (Evar ( succ_pos_of_nat 11))151 (Expr (Evar (ident_of_nat 11)) 152 152 (Tpointer Any (Tint I16 Signed )))) 153 153 (Tint I16 Signed )) 154 154 (Expr (Ederef 155 (Expr (Evar ( succ_pos_of_nat 12))155 (Expr (Evar (ident_of_nat 12)) 156 156 (Tpointer Any (Tint I16 Signed )))) 157 157 (Tint I16 Signed ))))))) 158 158 (LScase (repr 4) 159 159 (Ssequence 160 (Sassign (Expr (Evar ( succ_pos_of_nat 9))160 (Sassign (Expr (Evar (ident_of_nat 9)) 161 161 (Tpointer Any (Tint I16 Signed ))) 162 (Expr (Evar ( succ_pos_of_nat 19))162 (Expr (Evar (ident_of_nat 19)) 163 163 (Tpointer Any (Tint I16 Signed )))) 164 164 (Ssequence 165 (Sassign (Expr (Evar ( succ_pos_of_nat 19))165 (Sassign (Expr (Evar (ident_of_nat 19)) 166 166 (Tpointer Any (Tint I16 Signed ))) 167 167 (Expr (Ebinop Oadd 168 (Expr (Evar ( succ_pos_of_nat 9))168 (Expr (Evar (ident_of_nat 9)) 169 169 (Tpointer Any (Tint I16 Signed ))) 170 170 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 171 171 (Tpointer Any (Tint I16 Signed )))) 172 172 (Ssequence 173 (Sassign (Expr (Evar ( succ_pos_of_nat 10))173 (Sassign (Expr (Evar (ident_of_nat 10)) 174 174 (Tpointer Any (Tint I16 Signed ))) 175 (Expr (Evar ( succ_pos_of_nat 20))175 (Expr (Evar (ident_of_nat 20)) 176 176 (Tpointer Any (Tint I16 Signed )))) 177 177 (Ssequence 178 (Sassign (Expr (Evar ( succ_pos_of_nat 20))178 (Sassign (Expr (Evar (ident_of_nat 20)) 179 179 (Tpointer Any (Tint I16 Signed ))) 180 180 (Expr (Ebinop Oadd 181 (Expr (Evar ( succ_pos_of_nat 10))181 (Expr (Evar (ident_of_nat 10)) 182 182 (Tpointer Any (Tint I16 Signed ))) 183 183 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 184 184 (Tpointer Any (Tint I16 Signed )))) 185 185 (Sassign (Expr (Ederef 186 (Expr (Evar ( succ_pos_of_nat 9))186 (Expr (Evar (ident_of_nat 9)) 187 187 (Tpointer Any (Tint I16 Signed )))) 188 188 (Tint I16 Signed )) 189 189 (Expr (Ederef 190 (Expr (Evar ( succ_pos_of_nat 10))190 (Expr (Evar (ident_of_nat 10)) 191 191 (Tpointer Any (Tint I16 Signed )))) 192 192 (Tint I16 Signed ))))))) 193 193 (LScase (repr 3) 194 194 (Ssequence 195 (Sassign (Expr (Evar ( succ_pos_of_nat 7))195 (Sassign (Expr (Evar (ident_of_nat 7)) 196 196 (Tpointer Any (Tint I16 Signed ))) 197 (Expr (Evar ( succ_pos_of_nat 19))197 (Expr (Evar (ident_of_nat 19)) 198 198 (Tpointer Any (Tint I16 Signed )))) 199 199 (Ssequence 200 (Sassign (Expr (Evar ( succ_pos_of_nat 19))200 (Sassign (Expr (Evar (ident_of_nat 19)) 201 201 (Tpointer Any (Tint I16 Signed ))) 202 202 (Expr (Ebinop Oadd 203 (Expr (Evar ( succ_pos_of_nat 7))203 (Expr (Evar (ident_of_nat 7)) 204 204 (Tpointer Any (Tint I16 Signed ))) 205 205 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 206 206 (Tpointer Any (Tint I16 Signed )))) 207 207 (Ssequence 208 (Sassign (Expr (Evar ( succ_pos_of_nat 8))208 (Sassign (Expr (Evar (ident_of_nat 8)) 209 209 (Tpointer Any (Tint I16 Signed ))) 210 (Expr (Evar ( succ_pos_of_nat 20))210 (Expr (Evar (ident_of_nat 20)) 211 211 (Tpointer Any (Tint I16 Signed )))) 212 212 (Ssequence 213 (Sassign (Expr (Evar ( succ_pos_of_nat 20))213 (Sassign (Expr (Evar (ident_of_nat 20)) 214 214 (Tpointer Any (Tint I16 Signed ))) 215 215 (Expr (Ebinop Oadd 216 (Expr (Evar ( succ_pos_of_nat 8))216 (Expr (Evar (ident_of_nat 8)) 217 217 (Tpointer Any (Tint I16 Signed ))) 218 218 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 219 219 (Tpointer Any (Tint I16 Signed )))) 220 220 (Sassign (Expr (Ederef 221 (Expr (Evar ( succ_pos_of_nat 7))221 (Expr (Evar (ident_of_nat 7)) 222 222 (Tpointer Any (Tint I16 Signed )))) 223 223 (Tint I16 Signed )) 224 224 (Expr (Ederef 225 (Expr (Evar ( succ_pos_of_nat 8))225 (Expr (Evar (ident_of_nat 8)) 226 226 (Tpointer Any (Tint I16 Signed )))) 227 227 (Tint I16 Signed ))))))) 228 228 (LScase (repr 2) 229 229 (Ssequence 230 (Sassign (Expr (Evar ( succ_pos_of_nat 5))230 (Sassign (Expr (Evar (ident_of_nat 5)) 231 231 (Tpointer Any (Tint I16 Signed ))) 232 (Expr (Evar ( succ_pos_of_nat 19))232 (Expr (Evar (ident_of_nat 19)) 233 233 (Tpointer Any (Tint I16 Signed )))) 234 234 (Ssequence 235 (Sassign (Expr (Evar ( succ_pos_of_nat 19))235 (Sassign (Expr (Evar (ident_of_nat 19)) 236 236 (Tpointer Any (Tint I16 Signed ))) 237 237 (Expr (Ebinop Oadd 238 (Expr (Evar ( succ_pos_of_nat 5))238 (Expr (Evar (ident_of_nat 5)) 239 239 (Tpointer Any (Tint I16 Signed ))) 240 240 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 241 241 (Tpointer Any (Tint I16 Signed )))) 242 242 (Ssequence 243 (Sassign (Expr (Evar ( succ_pos_of_nat 6))243 (Sassign (Expr (Evar (ident_of_nat 6)) 244 244 (Tpointer Any (Tint I16 Signed ))) 245 (Expr (Evar ( succ_pos_of_nat 20))245 (Expr (Evar (ident_of_nat 20)) 246 246 (Tpointer Any (Tint I16 Signed )))) 247 247 (Ssequence 248 (Sassign (Expr (Evar ( succ_pos_of_nat 20))248 (Sassign (Expr (Evar (ident_of_nat 20)) 249 249 (Tpointer Any (Tint I16 Signed ))) 250 250 (Expr (Ebinop Oadd 251 (Expr (Evar ( succ_pos_of_nat 6))251 (Expr (Evar (ident_of_nat 6)) 252 252 (Tpointer Any (Tint I16 Signed ))) 253 253 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 254 254 (Tpointer Any (Tint I16 Signed )))) 255 255 (Sassign (Expr (Ederef 256 (Expr (Evar ( succ_pos_of_nat 5))256 (Expr (Evar (ident_of_nat 5)) 257 257 (Tpointer Any (Tint I16 Signed )))) 258 258 (Tint I16 Signed )) 259 259 (Expr (Ederef 260 (Expr (Evar ( succ_pos_of_nat 6))260 (Expr (Evar (ident_of_nat 6)) 261 261 (Tpointer Any (Tint I16 Signed )))) 262 262 (Tint I16 Signed ))))))) 263 263 (LScase (repr 1) 264 264 (Ssequence 265 (Sassign (Expr (Evar ( succ_pos_of_nat 3))265 (Sassign (Expr (Evar (ident_of_nat 3)) 266 266 (Tpointer Any (Tint I16 Signed ))) 267 (Expr (Evar ( succ_pos_of_nat 19))267 (Expr (Evar (ident_of_nat 19)) 268 268 (Tpointer Any (Tint I16 Signed )))) 269 269 (Ssequence 270 (Sassign (Expr (Evar ( succ_pos_of_nat 19))270 (Sassign (Expr (Evar (ident_of_nat 19)) 271 271 (Tpointer Any (Tint I16 Signed ))) 272 272 (Expr (Ebinop Oadd 273 (Expr (Evar ( succ_pos_of_nat 3))273 (Expr (Evar (ident_of_nat 3)) 274 274 (Tpointer Any (Tint I16 Signed ))) 275 275 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 276 276 (Tpointer Any (Tint I16 Signed )))) 277 277 (Ssequence 278 (Sassign (Expr (Evar ( succ_pos_of_nat 4))278 (Sassign (Expr (Evar (ident_of_nat 4)) 279 279 (Tpointer Any (Tint I16 Signed ))) 280 (Expr (Evar ( succ_pos_of_nat 20))280 (Expr (Evar (ident_of_nat 20)) 281 281 (Tpointer Any (Tint I16 Signed )))) 282 282 (Ssequence 283 (Sassign (Expr (Evar ( succ_pos_of_nat 20))283 (Sassign (Expr (Evar (ident_of_nat 20)) 284 284 (Tpointer Any (Tint I16 Signed ))) 285 285 (Expr (Ebinop Oadd 286 (Expr (Evar ( succ_pos_of_nat 4))286 (Expr (Evar (ident_of_nat 4)) 287 287 (Tpointer Any (Tint I16 Signed ))) 288 288 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) … … 290 290 (Ssequence 291 291 (Sassign (Expr (Ederef 292 (Expr (Evar ( succ_pos_of_nat 3))292 (Expr (Evar (ident_of_nat 3)) 293 293 (Tpointer Any (Tint I16 Signed )))) 294 294 (Tint I16 Signed )) 295 295 (Expr (Ederef 296 (Expr (Evar ( succ_pos_of_nat 4))296 (Expr (Evar (ident_of_nat 4)) 297 297 (Tpointer Any (Tint I16 Signed )))) 298 298 (Tint I16 Signed ))) 299 299 (Ssequence 300 (Sassign (Expr (Evar ( succ_pos_of_nat 2))300 (Sassign (Expr (Evar (ident_of_nat 2)) 301 301 (Tint I32 Signed )) 302 302 (Expr (Ebinop Osub 303 (Expr (Evar ( succ_pos_of_nat 1))303 (Expr (Evar (ident_of_nat 1)) 304 304 (Tint I32 Signed )) 305 305 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 306 306 (Tint I32 Signed ))) 307 307 (Ssequence 308 (Sassign (Expr (Evar ( succ_pos_of_nat 1))308 (Sassign (Expr (Evar (ident_of_nat 1)) 309 309 (Tint I32 Signed )) 310 (Expr (Evar ( succ_pos_of_nat 2))310 (Expr (Evar (ident_of_nat 2)) 311 311 (Tint I32 Signed ))) 312 312 (Sifthenelse (Expr (Ebinop Ogt 313 (Expr (Evar ( succ_pos_of_nat 2))313 (Expr (Evar (ident_of_nat 2)) 314 314 (Tint I32 Signed )) 315 315 (Expr (Econst_int (repr 0)) 316 316 (Tint I32 Signed ))) 317 317 (Tint I32 Signed )) 318 (Sgoto ( succ_pos_of_nat 22))318 (Sgoto (ident_of_nat 22)) 319 319 Sskip)))))))) 320 320 (LSdefault … … 325 325 326 326 )〉; 327 〈 succ_pos_of_nat 23 (* main *), CL_Internal (328 mk_function (Tint I32 Signed ) [] [〈 succ_pos_of_nat 24, (Tarray Any (Tint I16 Signed ) 3)〉 ; 〈succ_pos_of_nat 25, (Tarray Any (Tint I16 Signed ) 3)〉 ]327 〈ident_of_nat 23 (* main *), CL_Internal ( 328 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 24, (Tarray Any (Tint I16 Signed ) 3)〉 ; 〈ident_of_nat 25, (Tarray Any (Tint I16 Signed ) 3)〉 ] 329 329 (Ssequence 330 330 (Sassign (Expr (Ederef 331 331 (Expr (Ebinop Oadd 332 (Expr (Evar ( succ_pos_of_nat 24))332 (Expr (Evar (ident_of_nat 24)) 333 333 (Tarray Any (Tint I16 Signed ) 3)) 334 334 (Expr (Econst_int (repr 0)) (Tint I32 Signed ))) … … 340 340 (Sassign (Expr (Ederef 341 341 (Expr (Ebinop Oadd 342 (Expr (Evar ( succ_pos_of_nat 24))342 (Expr (Evar (ident_of_nat 24)) 343 343 (Tarray Any (Tint I16 Signed ) 3)) 344 344 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) … … 350 350 (Sassign (Expr (Ederef 351 351 (Expr (Ebinop Oadd 352 (Expr (Evar ( succ_pos_of_nat 24))352 (Expr (Evar (ident_of_nat 24)) 353 353 (Tarray Any (Tint I16 Signed ) 3)) 354 354 (Expr (Econst_int (repr 2)) (Tint I32 Signed ))) … … 358 358 (Tint I16 Signed ))) 359 359 (Ssequence 360 (Scall (None expr) (Expr (Evar ( succ_pos_of_nat 0))360 (Scall (None expr) (Expr (Evar (ident_of_nat 0)) 361 361 (Tfunction (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tint I32 Signed ) Tnil))) Tvoid)) 362 [(Expr (Evar ( succ_pos_of_nat 25))362 [(Expr (Evar (ident_of_nat 25)) 363 363 (Tarray Any (Tint I16 Signed ) 3)); 364 (Expr (Evar ( succ_pos_of_nat 24)) (Tarray Any (Tint I16 Signed ) 3));364 (Expr (Evar (ident_of_nat 24)) (Tarray Any (Tint I16 Signed ) 3)); 365 365 (Expr (Econst_int (repr 3)) (Tint I32 Signed ))]) 366 366 (Sreturn (Some expr (Expr (Ebinop Oadd … … 369 369 (Expr (Ederef 370 370 (Expr (Ebinop Oadd 371 (Expr (Evar ( succ_pos_of_nat 25))371 (Expr (Evar (ident_of_nat 25)) 372 372 (Tarray Any (Tint I16 Signed ) 3)) 373 373 (Expr (Econst_int (repr 0)) … … 378 378 (Expr (Ederef 379 379 (Expr (Ebinop Oadd 380 (Expr (Evar ( succ_pos_of_nat 25))380 (Expr (Evar (ident_of_nat 25)) 381 381 (Tarray Any (Tint I16 Signed ) 3)) 382 382 (Expr (Econst_int (repr 1)) … … 388 388 (Expr (Ederef 389 389 (Expr (Ebinop Oadd 390 (Expr (Evar ( succ_pos_of_nat 25))390 (Expr (Evar (ident_of_nat 25)) 391 391 (Tarray Any (Tint I16 Signed ) 3)) 392 392 (Expr (Econst_int (repr 2)) … … 399 399 400 400 )〉] 401 ( succ_pos_of_nat 23)401 (ident_of_nat 23) 402 402 [] 403 403 . -
src/Clight/test/factorial.ma
r725 r726 2 2 3 3 definition myprog := mk_program clight_fundef type 4 [〈 succ_pos_of_nat 0 (* get_input *), CL_External (succ_pos_of_nat 0) Tnil (Tint I32 Signed )〉;5 〈 succ_pos_of_nat 1 (* main *), CL_Internal (6 mk_function (Tint I32 Signed ) [] [〈 succ_pos_of_nat 2, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 4, (Tint I32 Signed )〉 ]4 [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed )〉; 5 〈ident_of_nat 1 (* main *), CL_Internal ( 6 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tint I32 Signed )〉 ; 〈ident_of_nat 4, (Tint I32 Signed )〉 ] 7 7 (Ssequence 8 (Scall (Some expr (Expr (Evar ( succ_pos_of_nat 2)) (Tint I32 Signed )))9 (Expr (Evar ( succ_pos_of_nat 0))8 (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 9 (Expr (Evar (ident_of_nat 0)) 10 10 (Tfunction Tnil (Tint I32 Signed ))) 11 11 []) 12 12 (Ssequence 13 (Sassign (Expr (Evar ( succ_pos_of_nat 3)) (Tint I32 Signed ))13 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 14 14 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 15 15 (Ssequence 16 16 (Ssequence 17 (Sfor (Sassign (Expr (Evar ( succ_pos_of_nat 4)) (Tint I32 Signed ))17 (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 18 18 (Expr (Econst_int (repr 2)) (Tint I32 Signed ))) 19 19 (Expr (Ebinop Ole 20 (Expr (Evar ( succ_pos_of_nat 4)) (Tint I32 Signed ))21 (Expr (Evar ( succ_pos_of_nat 2)) (Tint I32 Signed )))20 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 21 (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 22 22 (Tint I32 Signed )) 23 (Sassign (Expr (Evar ( succ_pos_of_nat 4)) (Tint I32 Signed ))23 (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 24 24 (Expr (Ebinop Oadd 25 (Expr (Evar ( succ_pos_of_nat 4)) (Tint I32 Signed ))25 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 26 26 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 27 27 (Tint I32 Signed ))) 28 (Sassign (Expr (Evar ( succ_pos_of_nat 3)) (Tint I32 Signed ))28 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 29 29 (Expr (Ebinop Omul 30 (Expr (Evar ( succ_pos_of_nat 3)) (Tint I32 Signed ))31 (Expr (Evar ( succ_pos_of_nat 4)) (Tint I32 Signed )))30 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 31 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed ))) 32 32 (Tint I32 Signed ))) 33 33 ) 34 34 Sskip) 35 (Sreturn (Some expr (Expr (Evar ( succ_pos_of_nat 3))35 (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) 36 36 (Tint I32 Signed ))))))) 37 37 … … 39 39 40 40 )〉] 41 ( succ_pos_of_nat 1)41 (ident_of_nat 1) 42 42 [] 43 43 . -
src/Clight/test/insertsort.ma
r725 r726 2 2 3 3 definition myprog := mk_program clight_fundef type 4 [〈 succ_pos_of_nat 0 (* insert *), CL_Internal (5 mk_function Tvoid [〈 succ_pos_of_nat 2, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed )〉 ]4 [〈ident_of_nat 0 (* insert *), CL_Internal ( 5 mk_function Tvoid [〈ident_of_nat 2, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed )〉 ] 6 6 (Ssequence 7 7 (Sifthenelse (Expr (Ebinop Oeq 8 8 (Expr (Ederef 9 (Expr (Evar ( succ_pos_of_nat 6))10 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))11 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))12 (Expr (Ecast (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))9 (Expr (Evar (ident_of_nat 6)) 10 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 11 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 12 (Expr (Ecast (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) 13 13 (Expr (Ecast (Tpointer Any Tvoid) 14 14 (Expr (Econst_int (repr 0)) (Tint I32 Unsigned))) 15 15 (Tpointer Any Tvoid))) 16 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))16 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 17 17 (Tint I32 Signed )) 18 (Sassign (Expr (Evar ( succ_pos_of_nat 1)) (Tint I32 Signed ))18 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) 19 19 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 20 (Sassign (Expr (Evar ( succ_pos_of_nat 1)) (Tint I32 Signed ))20 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) 21 21 (Expr (Ebinop One 22 22 (Expr (Ebinop Oge … … 24 24 (Expr (Efield (Expr (Ederef 25 25 (Expr (Ederef 26 (Expr (Evar ( succ_pos_of_nat 6))27 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))28 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))29 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))26 (Expr (Evar (ident_of_nat 6)) 27 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 28 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 29 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4)) 30 30 (Tint I8 Unsigned ))) (Tint I32 Signed )) 31 31 (Expr (Ecast (Tint I32 Signed ) 32 32 (Expr (Efield (Expr (Ederef 33 (Expr (Evar ( succ_pos_of_nat 2))34 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))35 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))33 (Expr (Evar (ident_of_nat 2)) 34 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 35 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4)) 36 36 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 37 37 (Tint I32 Signed )) 38 38 (Expr (Econst_int (repr 0)) (Tint I32 Signed ))) 39 39 (Tint I32 Signed )))) 40 (Sifthenelse (Expr (Evar ( succ_pos_of_nat 1)) (Tint I32 Signed ))40 (Sifthenelse (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed )) 41 41 (Ssequence 42 42 (Sassign (Expr (Efield (Expr (Ederef 43 (Expr (Evar ( succ_pos_of_nat 2))44 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))45 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))46 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))43 (Expr (Evar (ident_of_nat 2)) 44 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 45 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5)) 46 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 47 47 (Expr (Ederef 48 (Expr (Evar ( succ_pos_of_nat 6))49 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))50 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))48 (Expr (Evar (ident_of_nat 6)) 49 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 50 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 51 51 (Sassign (Expr (Ederef 52 (Expr (Evar ( succ_pos_of_nat 6))53 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))54 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))55 (Expr (Evar ( succ_pos_of_nat 2))56 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))57 (Scall (None expr) (Expr (Evar ( succ_pos_of_nat 0))58 (Tfunction (Tcons (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil)) Tvoid))59 [(Expr (Evar ( succ_pos_of_nat 2))60 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))));61 (Expr (Ecast (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))52 (Expr (Evar (ident_of_nat 6)) 53 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 54 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 55 (Expr (Evar (ident_of_nat 2)) 56 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 57 (Scall (None expr) (Expr (Evar (ident_of_nat 0)) 58 (Tfunction (Tcons (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid)) 59 [(Expr (Evar (ident_of_nat 2)) 60 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))); 61 (Expr (Ecast (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 62 62 (Expr (Eaddrof 63 63 (Expr (Efield (Expr (Ederef 64 64 (Expr (Ederef 65 (Expr (Evar ( succ_pos_of_nat 6))66 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))67 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))68 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))69 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))70 (Tpointer PData (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))71 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))])))65 (Expr (Evar (ident_of_nat 6)) 66 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 67 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 68 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5)) 69 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 70 (Tpointer PData (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 71 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))]))) 72 72 73 73 74 74 75 75 )〉; 76 〈 succ_pos_of_nat 7 (* sort *), CL_Internal (77 mk_function Tvoid [〈 succ_pos_of_nat 10, (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))〉 ] [〈succ_pos_of_nat 8, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 5, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 9, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ]78 (Ssequence 79 (Sassign (Expr (Evar ( succ_pos_of_nat 5))80 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))76 〈ident_of_nat 7 (* sort *), CL_Internal ( 77 mk_function Tvoid [〈ident_of_nat 10, (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 8, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 5, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 9, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ] 78 (Ssequence 79 (Sassign (Expr (Evar (ident_of_nat 5)) 80 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 81 81 (Expr (Ederef 82 (Expr (Evar ( succ_pos_of_nat 10))83 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))84 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))85 (Ssequence 86 (Sassign (Expr (Evar ( succ_pos_of_nat 9))87 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))88 (Expr (Ecast (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))82 (Expr (Evar (ident_of_nat 10)) 83 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 84 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 85 (Ssequence 86 (Sassign (Expr (Evar (ident_of_nat 9)) 87 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 88 (Expr (Ecast (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) 89 89 (Expr (Econst_int (repr 0)) (Tint I32 Signed ))) 90 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))91 (Ssequence 92 (Ssequence 93 (Swhile (Expr (Evar ( succ_pos_of_nat 5))94 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))90 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 91 (Ssequence 92 (Ssequence 93 (Swhile (Expr (Evar (ident_of_nat 5)) 94 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 95 95 (Ssequence 96 (Sassign (Expr (Evar ( succ_pos_of_nat 8))97 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))98 (Expr (Evar ( succ_pos_of_nat 5))99 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))96 (Sassign (Expr (Evar (ident_of_nat 8)) 97 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 98 (Expr (Evar (ident_of_nat 5)) 99 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 100 100 (Ssequence 101 (Sassign (Expr (Evar ( succ_pos_of_nat 5))102 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))101 (Sassign (Expr (Evar (ident_of_nat 5)) 102 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 103 103 (Expr (Efield (Expr (Ederef 104 (Expr (Evar ( succ_pos_of_nat 5))105 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))106 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))107 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))108 (Scall (None expr) (Expr (Evar ( succ_pos_of_nat 0))109 (Tfunction (Tcons (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil)) Tvoid))110 [(Expr (Evar ( succ_pos_of_nat 8))111 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))));104 (Expr (Evar (ident_of_nat 5)) 105 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 106 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5)) 107 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 108 (Scall (None expr) (Expr (Evar (ident_of_nat 0)) 109 (Tfunction (Tcons (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid)) 110 [(Expr (Evar (ident_of_nat 8)) 111 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))); 112 112 (Expr (Eaddrof 113 (Expr (Evar ( succ_pos_of_nat 9))114 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))115 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))]))))113 (Expr (Evar (ident_of_nat 9)) 114 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 115 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))])))) 116 116 Sskip) 117 117 (Sassign (Expr (Ederef 118 (Expr (Evar ( succ_pos_of_nat 10))119 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))120 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))121 (Expr (Evar ( succ_pos_of_nat 9))122 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))))118 (Expr (Evar (ident_of_nat 10)) 119 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))) 120 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 121 (Expr (Evar (ident_of_nat 9)) 122 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))))) 123 123 124 124 125 125 126 126 )〉; 127 〈 succ_pos_of_nat 11 (* out *), CL_External (succ_pos_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;128 〈 succ_pos_of_nat 12 (* main *), CL_Internal (129 mk_function (Tint I32 Signed ) [] [〈 succ_pos_of_nat 13, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ]130 (Ssequence 131 (Sassign (Expr (Evar ( succ_pos_of_nat 13))132 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))127 〈ident_of_nat 11 (* out *), CL_External (ident_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉; 128 〈ident_of_nat 12 (* main *), CL_Internal ( 129 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 13, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ] 130 (Ssequence 131 (Sassign (Expr (Evar (ident_of_nat 13)) 132 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 133 133 (Expr (Eaddrof 134 (Expr (Evar ( succ_pos_of_nat 14))135 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))136 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))137 (Ssequence 138 (Scall (None expr) (Expr (Evar ( succ_pos_of_nat 7))139 (Tfunction (Tcons (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil) Tvoid))134 (Expr (Evar (ident_of_nat 14)) 135 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 136 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 137 (Ssequence 138 (Scall (None expr) (Expr (Evar (ident_of_nat 7)) 139 (Tfunction (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil) Tvoid)) 140 140 [(Expr (Eaddrof 141 (Expr (Evar ( succ_pos_of_nat 13))142 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))143 (Tpointer Any (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))])144 (Ssequence 145 (Ssequence 146 (Swhile (Expr (Evar ( succ_pos_of_nat 13))147 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))141 (Expr (Evar (ident_of_nat 13)) 142 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 143 (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))]) 144 (Ssequence 145 (Ssequence 146 (Swhile (Expr (Evar (ident_of_nat 13)) 147 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 148 148 (Ssequence 149 (Scall (None expr) (Expr (Evar ( succ_pos_of_nat 11))149 (Scall (None expr) (Expr (Evar (ident_of_nat 11)) 150 150 (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid)) 151 151 [(Expr (Efield (Expr (Ederef 152 (Expr (Evar ( succ_pos_of_nat 13))153 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))154 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))152 (Expr (Evar (ident_of_nat 13)) 153 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 154 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4)) 155 155 (Tint I8 Unsigned ))]) 156 (Sassign (Expr (Evar ( succ_pos_of_nat 13))157 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))156 (Sassign (Expr (Evar (ident_of_nat 13)) 157 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) 158 158 (Expr (Efield (Expr (Ederef 159 (Expr (Evar ( succ_pos_of_nat 13))160 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))161 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))162 (Tpointer PData (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))))159 (Expr (Evar (ident_of_nat 13)) 160 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))) 161 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5)) 162 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))) 163 163 Sskip) 164 164 (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed ))))))) … … 167 167 168 168 )〉] 169 ( succ_pos_of_nat 12)170 [〈〈〈 succ_pos_of_nat 15 (* l6 *),169 (ident_of_nat 12) 170 [〈〈〈ident_of_nat 15 (* l6 *), 171 171 [(Init_int8 (repr 69)) ; (Init_space 3) ; (Init_null PData) ; 172 172 (Init_space 3) ]〉, PData〉, 173 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;174 〈〈〈 succ_pos_of_nat 16 (* l5 *),173 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉; 174 〈〈〈ident_of_nat 16 (* l5 *), 175 175 [(Init_int8 (repr 36)) ; (Init_space 3) ; 176 (Init_addrof PData ( succ_pos_of_nat 15) (repr 0))]〉, PData〉,177 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;178 〈〈〈 succ_pos_of_nat 17 (* l4 *),176 (Init_addrof PData (ident_of_nat 15) (repr 0))]〉, PData〉, 177 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉; 178 〈〈〈ident_of_nat 17 (* l4 *), 179 179 [(Init_int8 (repr 136)) ; (Init_space 3) ; 180 (Init_addrof PData ( succ_pos_of_nat 16) (repr 0))]〉, PData〉,181 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;182 〈〈〈 succ_pos_of_nat 18 (* l3 *),180 (Init_addrof PData (ident_of_nat 16) (repr 0))]〉, PData〉, 181 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉; 182 〈〈〈ident_of_nat 18 (* l3 *), 183 183 [(Init_int8 (repr 105)) ; (Init_space 3) ; 184 (Init_addrof PData ( succ_pos_of_nat 17) (repr 0))]〉, PData〉,185 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;186 〈〈〈 succ_pos_of_nat 19 (* l2 *),184 (Init_addrof PData (ident_of_nat 17) (repr 0))]〉, PData〉, 185 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉; 186 〈〈〈ident_of_nat 19 (* l2 *), 187 187 [(Init_int8 (repr 234)) ; (Init_space 3) ; 188 (Init_addrof PData ( succ_pos_of_nat 18) (repr 0))]〉, PData〉,189 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;190 〈〈〈 succ_pos_of_nat 20 (* l1 *),188 (Init_addrof PData (ident_of_nat 18) (repr 0))]〉, PData〉, 189 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉; 190 〈〈〈ident_of_nat 20 (* l1 *), 191 191 [(Init_int8 (repr 240)) ; (Init_space 3) ; 192 (Init_addrof PData ( succ_pos_of_nat 19) (repr 0))]〉, PData〉,193 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;194 〈〈〈 succ_pos_of_nat 14 (* l0 *),192 (Init_addrof PData (ident_of_nat 19) (repr 0))]〉, PData〉, 193 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉; 194 〈〈〈ident_of_nat 14 (* l0 *), 195 195 [(Init_int8 (repr 102)) ; (Init_space 3) ; 196 (Init_addrof PData ( succ_pos_of_nat 20) (repr 0))]〉, PData〉,197 (Tstruct ( succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉]196 (Init_addrof PData (ident_of_nat 20) (repr 0))]〉, PData〉, 197 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉] 198 198 . 199 199 … … 201 201 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)]; 202 202 OK ? t) = OK ? 203 [EVextcall ( succ_pos_of_nat 11) [EVint (repr 36)] (EVint (repr 0));204 EVextcall ( succ_pos_of_nat 11) [EVint (repr 69)] (EVint (repr 0));205 EVextcall ( succ_pos_of_nat 11) [EVint (repr 102)] (EVint (repr 0));206 EVextcall ( succ_pos_of_nat 11) [EVint (repr 105)] (EVint (repr 0));207 EVextcall ( succ_pos_of_nat 11) [EVint (repr 136)] (EVint (repr 0));208 EVextcall ( succ_pos_of_nat 11) [EVint (repr 234)] (EVint (repr 0));209 EVextcall ( succ_pos_of_nat 11) [EVint (repr 240)] (EVint (repr 0))]203 [EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0)); 204 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0)); 205 EVextcall (ident_of_nat 11) [EVint (repr 102)] (EVint (repr 0)); 206 EVextcall (ident_of_nat 11) [EVint (repr 105)] (EVint (repr 0)); 207 EVextcall (ident_of_nat 11) [EVint (repr 136)] (EVint (repr 0)); 208 EVextcall (ident_of_nat 11) [EVint (repr 234)] (EVint (repr 0)); 209 EVextcall (ident_of_nat 11) [EVint (repr 240)] (EVint (repr 0))] 210 210 . 211 211 normalize (* you can examine the result here *) -
src/Clight/test/io.ma
r725 r726 2 2 3 3 definition myprog := mk_program clight_fundef type 4 [〈 succ_pos_of_nat 0 (* dosomething *), CL_External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed )〉;5 〈 succ_pos_of_nat 1 (* main *), CL_Internal (6 mk_function (Tint I32 Signed ) [] [〈 succ_pos_of_nat 2, (Tint I32 Signed )〉 ]4 [〈ident_of_nat 0 (* dosomething *), CL_External (ident_of_nat 0) (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed )〉; 5 〈ident_of_nat 1 (* main *), CL_Internal ( 6 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 2, (Tint I32 Signed )〉 ] 7 7 (Ssequence 8 (Scall (Some expr (Expr (Evar ( succ_pos_of_nat 2)) (Tint I32 Signed )))9 (Expr (Evar ( succ_pos_of_nat 0))8 (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 9 (Expr (Evar (ident_of_nat 0)) 10 10 (Tfunction (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed ))) 11 11 [(Expr (Econst_int (repr 10)) (Tint I32 Signed ))]) 12 (Sreturn (Some expr (Expr (Evar ( succ_pos_of_nat 2))12 (Sreturn (Some expr (Expr (Evar (ident_of_nat 2)) 13 13 (Tint I32 Signed ))))) 14 14 … … 16 16 17 17 )〉] 18 ( succ_pos_of_nat 1)18 (ident_of_nat 1) 19 19 [] 20 20 . … … 22 22 example exec: 23 23 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) = 24 OK ? 〈[EVextcall ( succ_pos_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.24 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉. 25 25 normalize (* you can examine the result here *) 26 26 @refl -
src/Clight/test/io2.ma
r725 r726 2 2 3 3 definition myprog := mk_program clight_fundef type 4 [〈 succ_pos_of_nat 0 (* dosomething *), CL_External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed )〉;5 〈 succ_pos_of_nat 1 (* main *), CL_Internal (6 mk_function (Tint I32 Signed ) [] [〈 succ_pos_of_nat 2, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed )〉 ]4 [〈ident_of_nat 0 (* dosomething *), CL_External (ident_of_nat 0) (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed )〉; 5 〈ident_of_nat 1 (* main *), CL_Internal ( 6 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 2, (Tint I32 Signed )〉 ; 〈ident_of_nat 3, (Tint I32 Signed )〉 ] 7 7 (Ssequence 8 (Sassign (Expr (Evar ( succ_pos_of_nat 2)) (Tint I32 Signed ))8 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed )) 9 9 (Expr (Econst_int (repr 2)) (Tint I32 Signed ))) 10 10 (Ssequence 11 11 (Ssequence 12 (Scall (Some expr (Expr (Evar ( succ_pos_of_nat 3)) (Tint I32 Signed )))13 (Expr (Evar ( succ_pos_of_nat 0))12 (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed ))) 13 (Expr (Evar (ident_of_nat 0)) 14 14 (Tfunction (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed ))) 15 15 [(Expr (Econst_int (repr 10)) (Tint I32 Signed ))]) 16 (Sassign (Expr (Evar ( succ_pos_of_nat 2)) (Tint I32 Signed ))16 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed )) 17 17 (Expr (Ebinop Oadd 18 (Expr (Evar ( succ_pos_of_nat 2)) (Tint I32 Signed ))19 (Expr (Evar ( succ_pos_of_nat 3)) (Tint I32 Signed )))18 (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed )) 19 (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed ))) 20 20 (Tint I32 Signed )))) 21 (Sreturn (Some expr (Expr (Evar ( succ_pos_of_nat 2))21 (Sreturn (Some expr (Expr (Evar (ident_of_nat 2)) 22 22 (Tint I32 Signed )))))) 23 23 … … 25 25 26 26 )〉] 27 ( succ_pos_of_nat 1)27 (ident_of_nat 1) 28 28 [] 29 29 . … … 31 31 example exec: 32 32 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) = 33 OK ? 〈[EVextcall ( succ_pos_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉.33 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉. 34 34 normalize (* you can examine the result here *) 35 35 @refl -
src/Clight/test/search.ma
r725 r726 2 2 3 3 definition myprog := mk_program clight_fundef type 4 [〈 succ_pos_of_nat 0 (* search *), CL_Internal (5 mk_function (Tint I8 Unsigned ) [〈 succ_pos_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈succ_pos_of_nat 5, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 6, (Tint I8 Unsigned )〉 ] [〈succ_pos_of_nat 1, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 2, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 3, (Tint I8 Unsigned )〉 ]4 [〈ident_of_nat 0 (* search *), CL_Internal ( 5 mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ] 6 6 (Ssequence 7 (Sassign (Expr (Evar ( succ_pos_of_nat 1)) (Tint I8 Unsigned ))7 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) 8 8 (Expr (Ecast (Tint I8 Unsigned ) 9 9 (Expr (Econst_int (repr 0)) (Tint I32 Signed ))) 10 10 (Tint I8 Unsigned ))) 11 11 (Ssequence 12 (Sassign (Expr (Evar ( succ_pos_of_nat 2)) (Tint I8 Unsigned ))12 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 13 13 (Expr (Ecast (Tint I8 Unsigned ) 14 14 (Expr (Ebinop Osub 15 15 (Expr (Ecast (Tint I32 Signed ) 16 (Expr (Evar ( succ_pos_of_nat 5)) (Tint I8 Unsigned )))16 (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned ))) 17 17 (Tint I32 Signed )) 18 18 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) … … 22 22 (Swhile (Expr (Ebinop Oge 23 23 (Expr (Ecast (Tint I32 Signed ) 24 (Expr (Evar ( succ_pos_of_nat 2)) (Tint I8 Unsigned )))24 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 25 25 (Tint I32 Signed )) 26 26 (Expr (Ecast (Tint I32 Signed ) 27 (Expr (Evar ( succ_pos_of_nat 1)) (Tint I8 Unsigned )))27 (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) 28 28 (Tint I32 Signed ))) (Tint I32 Signed )) 29 29 (Ssequence 30 (Sassign (Expr (Evar ( succ_pos_of_nat 3)) (Tint I8 Unsigned ))30 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )) 31 31 (Expr (Ecast (Tint I8 Unsigned ) 32 32 (Expr (Ebinop Odiv 33 33 (Expr (Ebinop Oadd 34 34 (Expr (Ecast (Tint I32 Signed ) 35 (Expr (Evar ( succ_pos_of_nat 2)) (Tint I8 Unsigned )))35 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 36 36 (Tint I32 Signed )) 37 37 (Expr (Ecast (Tint I32 Signed ) 38 (Expr (Evar ( succ_pos_of_nat 1)) (Tint I8 Unsigned )))38 (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))) 39 39 (Tint I32 Signed ))) (Tint I32 Signed )) 40 40 (Expr (Econst_int (repr 2)) (Tint I32 Signed ))) … … 45 45 (Expr (Ederef 46 46 (Expr (Ebinop Oadd 47 (Expr (Evar ( succ_pos_of_nat 4))47 (Expr (Evar (ident_of_nat 4)) 48 48 (Tpointer Any (Tint I8 Unsigned ))) 49 (Expr (Evar ( succ_pos_of_nat 3))49 (Expr (Evar (ident_of_nat 3)) 50 50 (Tint I8 Unsigned ))) 51 51 (Tpointer Any (Tint I8 Unsigned )))) 52 52 (Tint I8 Unsigned ))) (Tint I32 Signed )) 53 53 (Expr (Ecast (Tint I32 Signed ) 54 (Expr (Evar ( succ_pos_of_nat 6))54 (Expr (Evar (ident_of_nat 6)) 55 55 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 56 56 (Tint I32 Signed )) 57 (Sreturn (Some expr (Expr (Evar ( succ_pos_of_nat 3))57 (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) 58 58 (Tint I8 Unsigned )))) 59 59 Sskip) … … 63 63 (Expr (Ederef 64 64 (Expr (Ebinop Oadd 65 (Expr (Evar ( succ_pos_of_nat 4))65 (Expr (Evar (ident_of_nat 4)) 66 66 (Tpointer Any (Tint I8 Unsigned ))) 67 (Expr (Evar ( succ_pos_of_nat 3))67 (Expr (Evar (ident_of_nat 3)) 68 68 (Tint I8 Unsigned ))) 69 69 (Tpointer Any (Tint I8 Unsigned )))) 70 70 (Tint I8 Unsigned ))) (Tint I32 Signed )) 71 71 (Expr (Ecast (Tint I32 Signed ) 72 (Expr (Evar ( succ_pos_of_nat 6))72 (Expr (Evar (ident_of_nat 6)) 73 73 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 74 74 (Tint I32 Signed )) 75 (Sassign (Expr (Evar ( succ_pos_of_nat 2)) (Tint I8 Unsigned ))75 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 76 76 (Expr (Ecast (Tint I8 Unsigned ) 77 77 (Expr (Ebinop Osub 78 78 (Expr (Ecast (Tint I32 Signed ) 79 (Expr (Evar ( succ_pos_of_nat 3)) (Tint I8 Unsigned )))79 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) 80 80 (Tint I32 Signed )) 81 81 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) … … 86 86 (Expr (Ederef 87 87 (Expr (Ebinop Oadd 88 (Expr (Evar ( succ_pos_of_nat 4))88 (Expr (Evar (ident_of_nat 4)) 89 89 (Tpointer Any (Tint I8 Unsigned ))) 90 (Expr (Evar ( succ_pos_of_nat 3))90 (Expr (Evar (ident_of_nat 3)) 91 91 (Tint I8 Unsigned ))) 92 92 (Tpointer Any (Tint I8 Unsigned )))) 93 93 (Tint I8 Unsigned ))) (Tint I32 Signed )) 94 94 (Expr (Ecast (Tint I32 Signed ) 95 (Expr (Evar ( succ_pos_of_nat 6))95 (Expr (Evar (ident_of_nat 6)) 96 96 (Tint I8 Unsigned ))) (Tint I32 Signed ))) 97 97 (Tint I32 Signed )) 98 (Sassign (Expr (Evar ( succ_pos_of_nat 1)) (Tint I8 Unsigned ))98 (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )) 99 99 (Expr (Ecast (Tint I8 Unsigned ) 100 100 (Expr (Ebinop Oadd 101 101 (Expr (Ecast (Tint I32 Signed ) 102 (Expr (Evar ( succ_pos_of_nat 3)) (Tint I8 Unsigned )))102 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))) 103 103 (Tint I32 Signed )) 104 104 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) … … 114 114 115 115 )〉; 116 〈 succ_pos_of_nat 7 (* main *), CL_Internal (117 mk_function (Tint I32 Signed ) [] [〈 succ_pos_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈succ_pos_of_nat 8, (Tint I8 Unsigned )〉 ]116 〈ident_of_nat 7 (* main *), CL_Internal ( 117 mk_function (Tint I32 Signed ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ] 118 118 (Ssequence 119 119 (Sassign (Expr (Ederef 120 120 (Expr (Ebinop Oadd 121 (Expr (Evar ( succ_pos_of_nat 4))121 (Expr (Evar (ident_of_nat 4)) 122 122 (Tarray Any (Tint I8 Unsigned ) 5)) 123 123 (Expr (Econst_int (repr 0)) (Tint I32 Signed ))) … … 129 129 (Sassign (Expr (Ederef 130 130 (Expr (Ebinop Oadd 131 (Expr (Evar ( succ_pos_of_nat 4))131 (Expr (Evar (ident_of_nat 4)) 132 132 (Tarray Any (Tint I8 Unsigned ) 5)) 133 133 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) … … 139 139 (Sassign (Expr (Ederef 140 140 (Expr (Ebinop Oadd 141 (Expr (Evar ( succ_pos_of_nat 4))141 (Expr (Evar (ident_of_nat 4)) 142 142 (Tarray Any (Tint I8 Unsigned ) 5)) 143 143 (Expr (Econst_int (repr 2)) (Tint I32 Signed ))) … … 149 149 (Sassign (Expr (Ederef 150 150 (Expr (Ebinop Oadd 151 (Expr (Evar ( succ_pos_of_nat 4))151 (Expr (Evar (ident_of_nat 4)) 152 152 (Tarray Any (Tint I8 Unsigned ) 5)) 153 153 (Expr (Econst_int (repr 3)) (Tint I32 Signed ))) … … 159 159 (Sassign (Expr (Ederef 160 160 (Expr (Ebinop Oadd 161 (Expr (Evar ( succ_pos_of_nat 4))161 (Expr (Evar (ident_of_nat 4)) 162 162 (Tarray Any (Tint I8 Unsigned ) 5)) 163 163 (Expr (Econst_int (repr 4)) (Tint I32 Signed ))) … … 167 167 (Tint I8 Unsigned ))) 168 168 (Ssequence 169 (Scall (Some expr (Expr (Evar ( succ_pos_of_nat 8)) (Tint I8 Unsigned )))170 (Expr (Evar ( succ_pos_of_nat 0))169 (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned ))) 170 (Expr (Evar (ident_of_nat 0)) 171 171 (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned ))) 172 [(Expr (Evar ( succ_pos_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));172 [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5)); 173 173 (Expr (Ecast (Tint I8 Unsigned ) 174 174 (Expr (Econst_int (repr 5)) (Tint I32 Signed ))) … … 178 178 (Tint I8 Unsigned ))]) 179 179 (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed ) 180 (Expr (Evar ( succ_pos_of_nat 8))180 (Expr (Evar (ident_of_nat 8)) 181 181 (Tint I8 Unsigned ))) (Tint I32 Signed )))))))))) 182 182 … … 184 184 185 185 )〉] 186 ( succ_pos_of_nat 7)186 (ident_of_nat 7) 187 187 [] 188 188 . … … 190 190 example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]). 191 191 normalize (* you can examine the result here *) 192 % 193 qed. -
src/RTLabs/import.ma
r710 r726 2 2 include "RTLabs/RTLabs-sem.ma". 3 3 4 definition new_reg : internal_function → re gister × internal_function≝5 λf. let 〈r, g〉 ≝ register_new (f_reggen f) in6 〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f)4 definition new_reg : internal_function → res (register × internal_function) ≝ 5 λf. do 〈r, g〉 ← register_new (f_reggen f); 6 OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f) 7 7 (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 8 8 9 definition new_label : internal_function → label × internal_function≝10 λf. let 〈l, g〉 ≝ label_new (f_labgen f) in11 〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f)9 definition new_label : internal_function → res (label × internal_function) ≝ 10 λf. do 〈l, g〉 ← label_new (f_labgen f); 11 OK ? 〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f) 12 12 (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. 13 13 … … 17 17 (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f). 18 18 19 let rec n_labels (n:nat) (g:label_generation) : Vector label n × label_generation≝19 let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation) ≝ 20 20 match n with 21 [ O ⇒ 〈[[ ]], g〉22 | S m ⇒ let 〈ls, g'〉 ≝ n_labels m g in23 let 〈l, g''〉 ≝ label_new g in24 〈l:::ls, g''〉21 [ O ⇒ OK ? 〈[[ ]], g〉 22 | S m ⇒ do 〈ls, g'〉 ← n_labels m g; 23 do 〈l, g''〉 ← label_new g; 24 OK ? 〈l:::ls, g''〉 25 25 ]. 26 26 27 let rec n_regs (n:nat) (g:register_generation) : Vector label n × register_generation≝27 let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation) ≝ 28 28 match n with 29 [ O ⇒ 〈[[ ]], g〉30 | S m ⇒ let 〈ls, g'〉 ≝ n_regs m g in31 let 〈l, g''〉 ≝ register_new g in32 〈l:::ls, g''〉29 [ O ⇒ OK ? 〈[[ ]], g〉 30 | S m ⇒ do 〈ls, g'〉 ← n_regs m g; 31 do 〈l, g''〉 ← register_new g; 32 OK ? 〈l:::ls, g''〉 33 33 ]. 34 34 … … 61 61 match m r with 62 62 [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉 63 | None ⇒ let 〈r',g'〉 ≝ register_new g in63 | None ⇒ do 〈r',g'〉 ← register_new g; 64 64 OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉 65 65 ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs; … … 88 88 let rmap ≝ λn. opt_to_res … (rmap3 n) in 89 89 let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in 90 let 〈labels, gen〉 ≝ n_labels max_stmt label_gen_new in90 do 〈labels, gen〉 ← n_labels max_stmt label_gen_new; 91 91 let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in 92 92 do graph ← foldr ?? (λp,g0. do g ← g0; -
src/common/Graphs.ma
r710 r726 1 include "basics/types.ma". 1 2 2 include "basics/logic.ma". 3 include "ASM/BitVectorTrie.ma". 4 include "Clight/AST.ma". 5 include "common/Errors.ma". 3 6 4 include "utilities/binary/positive.ma". 5 include "common/Maps.ma". 7 definition label ≝ ident. 6 8 7 definition label : Type[0] ≝ Pos. 8 definition graph : Type[0] → Type[0] ≝ tree_t … PTree. 9 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq. 10 11 record label_generation : Type[0] ≝ { lab_next : label }. 12 13 definition label_gen_new : label_generation ≝ mk_label_generation (zero ?). 14 15 definition label_new : label_generation → res (label × label_generation) ≝ 16 λg. let 〈gen, carries〉 ≝ add_with_carries ? (lab_next g) (zero ?) true in 17 if get_index_v ?? carries 0 ? then Error ? else 18 OK ? 〈lab_next g, mk_label_generation gen〉. 19 // qed. 20 21 definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16. 22 definition empty_graph : ∀T. graph T ≝ λT. Stub T 16. 9 23 definition graph_lookup : ∀T. graph T → label → option T ≝ 10 λT,g,l. get …l g.24 λT,g,l. lookup_opt T 16 l g. 11 25 definition graph_add : ∀T. graph T → label → T → graph T ≝ 12 λT,g,l,t. set … l t g. 13 definition empty_graph : ∀T. graph T ≝ λT. empty ? PTree T. 26 λT,g,l,v. insert T 16 l v g. 14 27 15 definition label_eq : ∀x,y:label. (x=y) + (x≠y).16 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);17 [ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.18 28 19 record label_generation : Type[0] ≝ { label_next : label }.20 21 definition label_new : label_generation → label × label_generation ≝22 λg. 〈label_next g, mk_label_generation (succ (label_next g))〉.23 24 definition label_gen_new : label_generation ≝ mk_label_generation one. -
src/common/Registers.ma
r710 r726 3 3 4 4 include "basics/types.ma". 5 include "utilities/binary/positive.ma".6 5 7 include "common/Maps.ma". 6 include "ASM/BitVectorTrie.ma". 7 include "Clight/AST.ma". 8 include "common/Errors.ma". 8 9 9 definition register ≝ Pos.10 definition register ≝ ident. 10 11 11 definition register_eq : ∀x,y:register. (x=y) + (x≠y). 12 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y); 13 [ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed. 12 definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq. 14 13 15 14 record register_generation : Type[0] ≝ { reg_next : register }. 16 15 17 definition register_gen_new : register_generation ≝ mk_register_generation one.16 definition register_gen_new : register_generation ≝ mk_register_generation (zero ?). 18 17 19 definition register_new : register_generation → register × register_generation ≝ 20 λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉. 18 definition register_new : register_generation → res (register × register_generation) ≝ 19 λg. let 〈gen, carries〉 ≝ add_with_carries ? (reg_next g) (zero ?) true in 20 if get_index_v ?? carries 0 ? then Error ? else 21 OK ? 〈reg_next g, mk_register_generation gen〉. 22 // qed. 21 23 22 definition register_env : Type[0] → Type[0] ≝ tree_t … PTree.23 definition register_empty : ∀T. register_env T ≝ λT. empty ? PTree T.24 definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16. 25 definition register_empty : ∀T. register_env T ≝ λT. Stub T 16. 24 26 definition register_lookup : ∀T. register_env T → register → option T ≝ 25 λT,g,l. get …l g.27 λT,g,l. lookup_opt T 16 l g. 26 28 definition register_update : ∀T. register → T → register_env T → register_env T ≝ 27 λT,l,v,g. set …l v g.29 λT,l,v,g. insert T 16 l v g.
Note: See TracChangeset
for help on using the changeset viewer.