Changeset 726 for src


Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (10 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

Location:
src
Files:
14 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/BitVector.ma

    r724 r726  
    102102        false) b c.
    103103
    104 lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
     104lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
    105105  (x = y → P true) →
    106106  (x ≠ y → P false) →

  • src/ASM/BitVectorTrie.ma

    r698 r726  
    77| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
    88| Stub: ∀n: nat. BitVectorTrie A n.
     9
     10let 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.
    918
    1019let rec lookup (A: Type[0]) (n: nat)

  • src/ASM/Vector.ma

    r700 r726  
    429429(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    430430
     431definition 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
     435definition 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
    431439let 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
     450lemma 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
    460452  [ O ⇒ λP.λv.P [[ ]] → P v
    461453  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
    462454  ] P v.
    463 @(λA,n. λP:Vector A n → Prop. λv. match v return
     455@(λA,n. λP:Vector A n → Type[0]. λv. match v return
    464456?
    465457with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P)
    … …  
    469461*)
    470462
    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)) →
     463lemma 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)) →
    474465  ∀n,x,y.
    475466  (x = y → P true) →

  • src/Clight/AST.ma

    r718 r726  
    2121include "common/Integers.ma".
    2222include "common/Floats.ma".
    23 include "utilities/binary/positive.ma".
     23include "ASM/BitVector.ma".
    2424
    2525(* * * Syntactic elements *)
    … …  
    2828  etc) are represented by the type [positive] of positive integers. *)
    2929
    30 definition ident ≝ Pos.
     30definition ident ≝ Word.
    3131
    3232definition 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 ]
     35lapply E @eq_bv_elim
     36[ 1,4: #H #_ @H | *: #_ #H destruct ]
     37qed.
     38
     39definition ident_of_nat ≝ bitvector_of_nat 16.
    3540
    3641(* Memory spaces *)

  • src/Clight/CexecComplete.ma

    r708 r726  
    328328| #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3
    329329  < H3 whd in H1:(??%?) ⊢ (??%?)
    330     destruct (H1) //
     330    destruct (H1) @refl
    331331] qed.
    332332

  • src/Clight/test/duff.ma

    r725 r726  
    22
    33definition 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  ))〉 ]
    66       (Ssequence
    7        (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     7       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    88         (Expr (Ebinop Odiv
    99           (Expr (Ebinop Oadd
    10              (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed  ))
     10             (Expr (Evar (ident_of_nat 21)) (Tint I32 Signed  ))
    1111             (Expr (Econst_int (repr 7)) (Tint I32 Signed  )))
    1212             (Tint I32 Signed  ))
    … …  
    1414           (Tint I32 Signed  )))
    1515       (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  ))
    1717                  (Expr (Econst_int (repr 8)) (Tint I32 Signed  )))
    1818                  (Tint I32 Signed  )) (
    1919         (LScase (repr 0)
    20            (Slabel (succ_pos_of_nat 22)
     20           (Slabel (ident_of_nat 22)
    2121           (Ssequence
    2222           (Ssequence
    23            (Sassign (Expr (Evar (succ_pos_of_nat 17))
     23           (Sassign (Expr (Evar (ident_of_nat 17))
    2424                      (Tpointer Any (Tint I16 Signed  )))
    25              (Expr (Evar (succ_pos_of_nat 19))
     25             (Expr (Evar (ident_of_nat 19))
    2626               (Tpointer Any (Tint I16 Signed  ))))
    27            (Sassign (Expr (Evar (succ_pos_of_nat 19))
     27           (Sassign (Expr (Evar (ident_of_nat 19))
    2828                      (Tpointer Any (Tint I16 Signed  )))
    2929             (Expr (Ebinop Oadd
    30                (Expr (Evar (succ_pos_of_nat 17))
     30               (Expr (Evar (ident_of_nat 17))
    3131                 (Tpointer Any (Tint I16 Signed  )))
    3232               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    … …  
    3434           (Ssequence
    3535           (Ssequence
    36            (Sassign (Expr (Evar (succ_pos_of_nat 18))
     36           (Sassign (Expr (Evar (ident_of_nat 18))
    3737                      (Tpointer Any (Tint I16 Signed  )))
    38              (Expr (Evar (succ_pos_of_nat 20))
     38             (Expr (Evar (ident_of_nat 20))
    3939               (Tpointer Any (Tint I16 Signed  ))))
    40            (Sassign (Expr (Evar (succ_pos_of_nat 20))
     40           (Sassign (Expr (Evar (ident_of_nat 20))
    4141                      (Tpointer Any (Tint I16 Signed  )))
    4242             (Expr (Ebinop Oadd
    43                (Expr (Evar (succ_pos_of_nat 18))
     43               (Expr (Evar (ident_of_nat 18))
    4444                 (Tpointer Any (Tint I16 Signed  )))
    4545               (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    4646               (Tpointer Any (Tint I16 Signed  )))))
    4747           (Sassign (Expr (Ederef
    48                       (Expr (Evar (succ_pos_of_nat 17))
     48                      (Expr (Evar (ident_of_nat 17))
    4949                        (Tpointer Any (Tint I16 Signed  ))))
    5050                      (Tint I16 Signed  ))
    5151             (Expr (Ederef
    52                (Expr (Evar (succ_pos_of_nat 18))
     52               (Expr (Evar (ident_of_nat 18))
    5353                 (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  ))))))
    5454           (LScase (repr 7)
    5555             (Ssequence
    56              (Sassign (Expr (Evar (succ_pos_of_nat 15))
     56             (Sassign (Expr (Evar (ident_of_nat 15))
    5757                        (Tpointer Any (Tint I16 Signed  )))
    58                (Expr (Evar (succ_pos_of_nat 19))
     58               (Expr (Evar (ident_of_nat 19))
    5959                 (Tpointer Any (Tint I16 Signed  ))))
    6060             (Ssequence
    61              (Sassign (Expr (Evar (succ_pos_of_nat 19))
     61             (Sassign (Expr (Evar (ident_of_nat 19))
    6262                        (Tpointer Any (Tint I16 Signed  )))
    6363               (Expr (Ebinop Oadd
    64                  (Expr (Evar (succ_pos_of_nat 15))
     64                 (Expr (Evar (ident_of_nat 15))
    6565                   (Tpointer Any (Tint I16 Signed  )))
    6666                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    6767                 (Tpointer Any (Tint I16 Signed  ))))
    6868             (Ssequence
    69              (Sassign (Expr (Evar (succ_pos_of_nat 16))
     69             (Sassign (Expr (Evar (ident_of_nat 16))
    7070                        (Tpointer Any (Tint I16 Signed  )))
    71                (Expr (Evar (succ_pos_of_nat 20))
     71               (Expr (Evar (ident_of_nat 20))
    7272                 (Tpointer Any (Tint I16 Signed  ))))
    7373             (Ssequence
    74              (Sassign (Expr (Evar (succ_pos_of_nat 20))
     74             (Sassign (Expr (Evar (ident_of_nat 20))
    7575                        (Tpointer Any (Tint I16 Signed  )))
    7676               (Expr (Ebinop Oadd
    77                  (Expr (Evar (succ_pos_of_nat 16))
     77                 (Expr (Evar (ident_of_nat 16))
    7878                   (Tpointer Any (Tint I16 Signed  )))
    7979                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    8080                 (Tpointer Any (Tint I16 Signed  ))))
    8181             (Sassign (Expr (Ederef
    82                         (Expr (Evar (succ_pos_of_nat 15))
     82                        (Expr (Evar (ident_of_nat 15))
    8383                          (Tpointer Any (Tint I16 Signed  ))))
    8484                        (Tint I16 Signed  ))
    8585               (Expr (Ederef
    86                  (Expr (Evar (succ_pos_of_nat 16))
     86                 (Expr (Evar (ident_of_nat 16))
    8787                   (Tpointer Any (Tint I16 Signed  )))) (Tint I16 Signed  )))))))
    8888             (LScase (repr 6)
    8989               (Ssequence
    90                (Sassign (Expr (Evar (succ_pos_of_nat 13))
     90               (Sassign (Expr (Evar (ident_of_nat 13))
    9191                          (Tpointer Any (Tint I16 Signed  )))
    92                  (Expr (Evar (succ_pos_of_nat 19))
     92                 (Expr (Evar (ident_of_nat 19))
    9393                   (Tpointer Any (Tint I16 Signed  ))))
    9494               (Ssequence
    95                (Sassign (Expr (Evar (succ_pos_of_nat 19))
     95               (Sassign (Expr (Evar (ident_of_nat 19))
    9696                          (Tpointer Any (Tint I16 Signed  )))
    9797                 (Expr (Ebinop Oadd
    98                    (Expr (Evar (succ_pos_of_nat 13))
     98                   (Expr (Evar (ident_of_nat 13))
    9999                     (Tpointer Any (Tint I16 Signed  )))
    100100                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    101101                   (Tpointer Any (Tint I16 Signed  ))))
    102102               (Ssequence
    103                (Sassign (Expr (Evar (succ_pos_of_nat 14))
     103               (Sassign (Expr (Evar (ident_of_nat 14))
    104104                          (Tpointer Any (Tint I16 Signed  )))
    105                  (Expr (Evar (succ_pos_of_nat 20))
     105                 (Expr (Evar (ident_of_nat 20))
    106106                   (Tpointer Any (Tint I16 Signed  ))))
    107107               (Ssequence
    108                (Sassign (Expr (Evar (succ_pos_of_nat 20))
     108               (Sassign (Expr (Evar (ident_of_nat 20))
    109109                          (Tpointer Any (Tint I16 Signed  )))
    110110                 (Expr (Ebinop Oadd
    111                    (Expr (Evar (succ_pos_of_nat 14))
     111                   (Expr (Evar (ident_of_nat 14))
    112112                     (Tpointer Any (Tint I16 Signed  )))
    113113                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    114114                   (Tpointer Any (Tint I16 Signed  ))))
    115115               (Sassign (Expr (Ederef
    116                           (Expr (Evar (succ_pos_of_nat 13))
     116                          (Expr (Evar (ident_of_nat 13))
    117117                            (Tpointer Any (Tint I16 Signed  ))))
    118118                          (Tint I16 Signed  ))
    119119                 (Expr (Ederef
    120                    (Expr (Evar (succ_pos_of_nat 14))
     120                   (Expr (Evar (ident_of_nat 14))
    121121                     (Tpointer Any (Tint I16 Signed  ))))
    122122                   (Tint I16 Signed  )))))))
    123123               (LScase (repr 5)
    124124                 (Ssequence
    125                  (Sassign (Expr (Evar (succ_pos_of_nat 11))
     125                 (Sassign (Expr (Evar (ident_of_nat 11))
    126126                            (Tpointer Any (Tint I16 Signed  )))
    127                    (Expr (Evar (succ_pos_of_nat 19))
     127                   (Expr (Evar (ident_of_nat 19))
    128128                     (Tpointer Any (Tint I16 Signed  ))))
    129129                 (Ssequence
    130                  (Sassign (Expr (Evar (succ_pos_of_nat 19))
     130                 (Sassign (Expr (Evar (ident_of_nat 19))
    131131                            (Tpointer Any (Tint I16 Signed  )))
    132132                   (Expr (Ebinop Oadd
    133                      (Expr (Evar (succ_pos_of_nat 11))
     133                     (Expr (Evar (ident_of_nat 11))
    134134                       (Tpointer Any (Tint I16 Signed  )))
    135135                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    136136                     (Tpointer Any (Tint I16 Signed  ))))
    137137                 (Ssequence
    138                  (Sassign (Expr (Evar (succ_pos_of_nat 12))
     138                 (Sassign (Expr (Evar (ident_of_nat 12))
    139139                            (Tpointer Any (Tint I16 Signed  )))
    140                    (Expr (Evar (succ_pos_of_nat 20))
     140                   (Expr (Evar (ident_of_nat 20))
    141141                     (Tpointer Any (Tint I16 Signed  ))))
    142142                 (Ssequence
    143                  (Sassign (Expr (Evar (succ_pos_of_nat 20))
     143                 (Sassign (Expr (Evar (ident_of_nat 20))
    144144                            (Tpointer Any (Tint I16 Signed  )))
    145145                   (Expr (Ebinop Oadd
    146                      (Expr (Evar (succ_pos_of_nat 12))
     146                     (Expr (Evar (ident_of_nat 12))
    147147                       (Tpointer Any (Tint I16 Signed  )))
    148148                     (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    149149                     (Tpointer Any (Tint I16 Signed  ))))
    150150                 (Sassign (Expr (Ederef
    151                             (Expr (Evar (succ_pos_of_nat 11))
     151                            (Expr (Evar (ident_of_nat 11))
    152152                              (Tpointer Any (Tint I16 Signed  ))))
    153153                            (Tint I16 Signed  ))
    154154                   (Expr (Ederef
    155                      (Expr (Evar (succ_pos_of_nat 12))
     155                     (Expr (Evar (ident_of_nat 12))
    156156                       (Tpointer Any (Tint I16 Signed  ))))
    157157                     (Tint I16 Signed  )))))))
    158158                 (LScase (repr 4)
    159159                   (Ssequence
    160                    (Sassign (Expr (Evar (succ_pos_of_nat 9))
     160                   (Sassign (Expr (Evar (ident_of_nat 9))
    161161                              (Tpointer Any (Tint I16 Signed  )))
    162                      (Expr (Evar (succ_pos_of_nat 19))
     162                     (Expr (Evar (ident_of_nat 19))
    163163                       (Tpointer Any (Tint I16 Signed  ))))
    164164                   (Ssequence
    165                    (Sassign (Expr (Evar (succ_pos_of_nat 19))
     165                   (Sassign (Expr (Evar (ident_of_nat 19))
    166166                              (Tpointer Any (Tint I16 Signed  )))
    167167                     (Expr (Ebinop Oadd
    168                        (Expr (Evar (succ_pos_of_nat 9))
     168                       (Expr (Evar (ident_of_nat 9))
    169169                         (Tpointer Any (Tint I16 Signed  )))
    170170                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    171171                       (Tpointer Any (Tint I16 Signed  ))))
    172172                   (Ssequence
    173                    (Sassign (Expr (Evar (succ_pos_of_nat 10))
     173                   (Sassign (Expr (Evar (ident_of_nat 10))
    174174                              (Tpointer Any (Tint I16 Signed  )))
    175                      (Expr (Evar (succ_pos_of_nat 20))
     175                     (Expr (Evar (ident_of_nat 20))
    176176                       (Tpointer Any (Tint I16 Signed  ))))
    177177                   (Ssequence
    178                    (Sassign (Expr (Evar (succ_pos_of_nat 20))
     178                   (Sassign (Expr (Evar (ident_of_nat 20))
    179179                              (Tpointer Any (Tint I16 Signed  )))
    180180                     (Expr (Ebinop Oadd
    181                        (Expr (Evar (succ_pos_of_nat 10))
     181                       (Expr (Evar (ident_of_nat 10))
    182182                         (Tpointer Any (Tint I16 Signed  )))
    183183                       (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    184184                       (Tpointer Any (Tint I16 Signed  ))))
    185185                   (Sassign (Expr (Ederef
    186                               (Expr (Evar (succ_pos_of_nat 9))
     186                              (Expr (Evar (ident_of_nat 9))
    187187                                (Tpointer Any (Tint I16 Signed  ))))
    188188                              (Tint I16 Signed  ))
    189189                     (Expr (Ederef
    190                        (Expr (Evar (succ_pos_of_nat 10))
     190                       (Expr (Evar (ident_of_nat 10))
    191191                         (Tpointer Any (Tint I16 Signed  ))))
    192192                       (Tint I16 Signed  )))))))
    193193                   (LScase (repr 3)
    194194                     (Ssequence
    195                      (Sassign (Expr (Evar (succ_pos_of_nat 7))
     195                     (Sassign (Expr (Evar (ident_of_nat 7))
    196196                                (Tpointer Any (Tint I16 Signed  )))
    197                        (Expr (Evar (succ_pos_of_nat 19))
     197                       (Expr (Evar (ident_of_nat 19))
    198198                         (Tpointer Any (Tint I16 Signed  ))))
    199199                     (Ssequence
    200                      (Sassign (Expr (Evar (succ_pos_of_nat 19))
     200                     (Sassign (Expr (Evar (ident_of_nat 19))
    201201                                (Tpointer Any (Tint I16 Signed  )))
    202202                       (Expr (Ebinop Oadd
    203                          (Expr (Evar (succ_pos_of_nat 7))
     203                         (Expr (Evar (ident_of_nat 7))
    204204                           (Tpointer Any (Tint I16 Signed  )))
    205205                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    206206                         (Tpointer Any (Tint I16 Signed  ))))
    207207                     (Ssequence
    208                      (Sassign (Expr (Evar (succ_pos_of_nat 8))
     208                     (Sassign (Expr (Evar (ident_of_nat 8))
    209209                                (Tpointer Any (Tint I16 Signed  )))
    210                        (Expr (Evar (succ_pos_of_nat 20))
     210                       (Expr (Evar (ident_of_nat 20))
    211211                         (Tpointer Any (Tint I16 Signed  ))))
    212212                     (Ssequence
    213                      (Sassign (Expr (Evar (succ_pos_of_nat 20))
     213                     (Sassign (Expr (Evar (ident_of_nat 20))
    214214                                (Tpointer Any (Tint I16 Signed  )))
    215215                       (Expr (Ebinop Oadd
    216                          (Expr (Evar (succ_pos_of_nat 8))
     216                         (Expr (Evar (ident_of_nat 8))
    217217                           (Tpointer Any (Tint I16 Signed  )))
    218218                         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    219219                         (Tpointer Any (Tint I16 Signed  ))))
    220220                     (Sassign (Expr (Ederef
    221                                 (Expr (Evar (succ_pos_of_nat 7))
     221                                (Expr (Evar (ident_of_nat 7))
    222222                                  (Tpointer Any (Tint I16 Signed  ))))
    223223                                (Tint I16 Signed  ))
    224224                       (Expr (Ederef
    225                          (Expr (Evar (succ_pos_of_nat 8))
     225                         (Expr (Evar (ident_of_nat 8))
    226226                           (Tpointer Any (Tint I16 Signed  ))))
    227227                         (Tint I16 Signed  )))))))
    228228                     (LScase (repr 2)
    229229                       (Ssequence
    230                        (Sassign (Expr (Evar (succ_pos_of_nat 5))
     230                       (Sassign (Expr (Evar (ident_of_nat 5))
    231231                                  (Tpointer Any (Tint I16 Signed  )))
    232                          (Expr (Evar (succ_pos_of_nat 19))
     232                         (Expr (Evar (ident_of_nat 19))
    233233                           (Tpointer Any (Tint I16 Signed  ))))
    234234                       (Ssequence
    235                        (Sassign (Expr (Evar (succ_pos_of_nat 19))
     235                       (Sassign (Expr (Evar (ident_of_nat 19))
    236236                                  (Tpointer Any (Tint I16 Signed  )))
    237237                         (Expr (Ebinop Oadd
    238                            (Expr (Evar (succ_pos_of_nat 5))
     238                           (Expr (Evar (ident_of_nat 5))
    239239                             (Tpointer Any (Tint I16 Signed  )))
    240240                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    241241                           (Tpointer Any (Tint I16 Signed  ))))
    242242                       (Ssequence
    243                        (Sassign (Expr (Evar (succ_pos_of_nat 6))
     243                       (Sassign (Expr (Evar (ident_of_nat 6))
    244244                                  (Tpointer Any (Tint I16 Signed  )))
    245                          (Expr (Evar (succ_pos_of_nat 20))
     245                         (Expr (Evar (ident_of_nat 20))
    246246                           (Tpointer Any (Tint I16 Signed  ))))
    247247                       (Ssequence
    248                        (Sassign (Expr (Evar (succ_pos_of_nat 20))
     248                       (Sassign (Expr (Evar (ident_of_nat 20))
    249249                                  (Tpointer Any (Tint I16 Signed  )))
    250250                         (Expr (Ebinop Oadd
    251                            (Expr (Evar (succ_pos_of_nat 6))
     251                           (Expr (Evar (ident_of_nat 6))
    252252                             (Tpointer Any (Tint I16 Signed  )))
    253253                           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    254254                           (Tpointer Any (Tint I16 Signed  ))))
    255255                       (Sassign (Expr (Ederef
    256                                   (Expr (Evar (succ_pos_of_nat 5))
     256                                  (Expr (Evar (ident_of_nat 5))
    257257                                    (Tpointer Any (Tint I16 Signed  ))))
    258258                                  (Tint I16 Signed  ))
    259259                         (Expr (Ederef
    260                            (Expr (Evar (succ_pos_of_nat 6))
     260                           (Expr (Evar (ident_of_nat 6))
    261261                             (Tpointer Any (Tint I16 Signed  ))))
    262262                           (Tint I16 Signed  )))))))
    263263                       (LScase (repr 1)
    264264                         (Ssequence
    265                          (Sassign (Expr (Evar (succ_pos_of_nat 3))
     265                         (Sassign (Expr (Evar (ident_of_nat 3))
    266266                                    (Tpointer Any (Tint I16 Signed  )))
    267                            (Expr (Evar (succ_pos_of_nat 19))
     267                           (Expr (Evar (ident_of_nat 19))
    268268                             (Tpointer Any (Tint I16 Signed  ))))
    269269                         (Ssequence
    270                          (Sassign (Expr (Evar (succ_pos_of_nat 19))
     270                         (Sassign (Expr (Evar (ident_of_nat 19))
    271271                                    (Tpointer Any (Tint I16 Signed  )))
    272272                           (Expr (Ebinop Oadd
    273                              (Expr (Evar (succ_pos_of_nat 3))
     273                             (Expr (Evar (ident_of_nat 3))
    274274                               (Tpointer Any (Tint I16 Signed  )))
    275275                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    276276                             (Tpointer Any (Tint I16 Signed  ))))
    277277                         (Ssequence
    278                          (Sassign (Expr (Evar (succ_pos_of_nat 4))
     278                         (Sassign (Expr (Evar (ident_of_nat 4))
    279279                                    (Tpointer Any (Tint I16 Signed  )))
    280                            (Expr (Evar (succ_pos_of_nat 20))
     280                           (Expr (Evar (ident_of_nat 20))
    281281                             (Tpointer Any (Tint I16 Signed  ))))
    282282                         (Ssequence
    283                          (Sassign (Expr (Evar (succ_pos_of_nat 20))
     283                         (Sassign (Expr (Evar (ident_of_nat 20))
    284284                                    (Tpointer Any (Tint I16 Signed  )))
    285285                           (Expr (Ebinop Oadd
    286                              (Expr (Evar (succ_pos_of_nat 4))
     286                             (Expr (Evar (ident_of_nat 4))
    287287                               (Tpointer Any (Tint I16 Signed  )))
    288288                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    … …  
    290290                         (Ssequence
    291291                         (Sassign (Expr (Ederef
    292                                     (Expr (Evar (succ_pos_of_nat 3))
     292                                    (Expr (Evar (ident_of_nat 3))
    293293                                      (Tpointer Any (Tint I16 Signed  ))))
    294294                                    (Tint I16 Signed  ))
    295295                           (Expr (Ederef
    296                              (Expr (Evar (succ_pos_of_nat 4))
     296                             (Expr (Evar (ident_of_nat 4))
    297297                               (Tpointer Any (Tint I16 Signed  ))))
    298298                             (Tint I16 Signed  )))
    299299                         (Ssequence
    300                          (Sassign (Expr (Evar (succ_pos_of_nat 2))
     300                         (Sassign (Expr (Evar (ident_of_nat 2))
    301301                                    (Tint I32 Signed  ))
    302302                           (Expr (Ebinop Osub
    303                              (Expr (Evar (succ_pos_of_nat 1))
     303                             (Expr (Evar (ident_of_nat 1))
    304304                               (Tint I32 Signed  ))
    305305                             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    306306                             (Tint I32 Signed  )))
    307307                         (Ssequence
    308                          (Sassign (Expr (Evar (succ_pos_of_nat 1))
     308                         (Sassign (Expr (Evar (ident_of_nat 1))
    309309                                    (Tint I32 Signed  ))
    310                            (Expr (Evar (succ_pos_of_nat 2))
     310                           (Expr (Evar (ident_of_nat 2))
    311311                             (Tint I32 Signed  )))
    312312                         (Sifthenelse (Expr (Ebinop Ogt
    313                                         (Expr (Evar (succ_pos_of_nat 2))
     313                                        (Expr (Evar (ident_of_nat 2))
    314314                                          (Tint I32 Signed  ))
    315315                                        (Expr (Econst_int (repr 0))
    316316                                          (Tint I32 Signed  )))
    317317                                        (Tint I32 Signed  ))
    318                            (Sgoto (succ_pos_of_nat 22))
     318                           (Sgoto (ident_of_nat 22))
    319319                           Sskip))))))))
    320320                         (LSdefault
    … …  
    325325     
    326326   )〉;
    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)〉 ]
    329329      (Ssequence
    330330      (Sassign (Expr (Ederef
    331331                 (Expr (Ebinop Oadd
    332                    (Expr (Evar (succ_pos_of_nat 24))
     332                   (Expr (Evar (ident_of_nat 24))
    333333                     (Tarray Any (Tint I16 Signed  ) 3))
    334334                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    … …  
    340340      (Sassign (Expr (Ederef
    341341                 (Expr (Ebinop Oadd
    342                    (Expr (Evar (succ_pos_of_nat 24))
     342                   (Expr (Evar (ident_of_nat 24))
    343343                     (Tarray Any (Tint I16 Signed  ) 3))
    344344                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    … …  
    350350      (Sassign (Expr (Ederef
    351351                 (Expr (Ebinop Oadd
    352                    (Expr (Evar (succ_pos_of_nat 24))
     352                   (Expr (Evar (ident_of_nat 24))
    353353                     (Tarray Any (Tint I16 Signed  ) 3))
    354354                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    … …  
    358358          (Tint I16 Signed  )))
    359359      (Ssequence
    360       (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0))
     360      (Scall (None expr) (Expr (Evar (ident_of_nat 0))
    361361                           (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))
    363363           (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));
    365365        (Expr (Econst_int (repr 3)) (Tint I32 Signed  ))])
    366366      (Sreturn (Some expr (Expr (Ebinop Oadd
    … …  
    369369                                (Expr (Ederef
    370370                                  (Expr (Ebinop Oadd
    371                                     (Expr (Evar (succ_pos_of_nat 25))
     371                                    (Expr (Evar (ident_of_nat 25))
    372372                                      (Tarray Any (Tint I16 Signed  ) 3))
    373373                                    (Expr (Econst_int (repr 0))
    … …  
    378378                                (Expr (Ederef
    379379                                  (Expr (Ebinop Oadd
    380                                     (Expr (Evar (succ_pos_of_nat 25))
     380                                    (Expr (Evar (ident_of_nat 25))
    381381                                      (Tarray Any (Tint I16 Signed  ) 3))
    382382                                    (Expr (Econst_int (repr 1))
    … …  
    388388                              (Expr (Ederef
    389389                                (Expr (Ebinop Oadd
    390                                   (Expr (Evar (succ_pos_of_nat 25))
     390                                  (Expr (Evar (ident_of_nat 25))
    391391                                    (Tarray Any (Tint I16 Signed  ) 3))
    392392                                  (Expr (Econst_int (repr 2))
    … …  
    399399   
    400400  )〉]
    401   (succ_pos_of_nat 23)
     401  (ident_of_nat 23)
    402402  []
    403403.

  • src/Clight/test/factorial.ma

    r725 r726  
    22
    33definition 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  )〉 ]
    77      (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))
    1010          (Tfunction Tnil (Tint I32 Signed  )))
    1111        [])
    1212      (Ssequence
    13       (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
     13      (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    1414        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    1515      (Ssequence
    1616      (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  ))
    1818              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    1919        (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  )))
    2222          (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  ))
    2424          (Expr (Ebinop Oadd
    25             (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     25            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    2626            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    2727            (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  ))
    2929          (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  )))
    3232            (Tint I32 Signed  )))
    3333      )
    3434      Sskip)
    35       (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
     35      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    3636                            (Tint I32 Signed  )))))))
    3737   
    … …  
    3939   
    4040  )〉]
    41   (succ_pos_of_nat 1)
     41  (ident_of_nat 1)
    4242  []
    4343.

  • src/Clight/test/insertsort.ma

    r725 r726  
    22
    33definition 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  )〉 ]
    66       (Ssequence
    77       (Sifthenelse (Expr (Ebinop Oeq
    88                      (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))))
    1313                        (Expr (Ecast (Tpointer Any Tvoid)
    1414                          (Expr (Econst_int (repr 0)) (Tint I32 Unsigned)))
    1515                          (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))))))
    1717                      (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  ))
    1919           (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  ))
    2121           (Expr (Ebinop One
    2222             (Expr (Ebinop Oge
    … …  
    2424                 (Expr (Efield (Expr (Ederef
    2525                                 (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))
    3030                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    3131               (Expr (Ecast (Tint I32 Signed  )
    3232                 (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))
    3636                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    3737               (Tint I32 Signed  ))
    3838             (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    3939             (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  ))
    4141         (Ssequence
    4242         (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)))))
    4747           (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))))))
    5151         (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)))))
    6262             (Expr (Eaddrof
    6363               (Expr (Efield (Expr (Ederef
    6464                               (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))))))])))
    7272     
    7373     
    7474     
    7575   )〉;
    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)))))
    8181        (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))))
    8989          (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)))))
    9595        (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))))))
    100100        (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)))))
    103103          (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)))));
    112112          (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))))))]))))
    116116      Sskip)
    117117      (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)))))))))
    123123   
    124124   
    125125   
    126126  )〉;
    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)))))
    133133        (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))
    140140        [(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)))))
    148148        (Ssequence
    149         (Scall (None expr) (Expr (Evar (succ_pos_of_nat 11))
     149        (Scall (None expr) (Expr (Evar (ident_of_nat 11))
    150150                             (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid))
    151151          [(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))
    155155             (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)))))
    158158          (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))))))))
    163163      Sskip)
    164164      (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))))))
    … …  
    167167   
    168168  )〉]
    169   (succ_pos_of_nat 12)
    170   [〈〈〈succ_pos_of_nat 15 (* l6 *),
     169  (ident_of_nat 12)
     170  [〈〈〈ident_of_nat 15 (* l6 *),
    171171     [(Init_int8 (repr 69)) ; (Init_space 3) ; (Init_null PData) ;
    172172     (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 *),
    175175    [(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 *),
    179179    [(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 *),
    183183    [(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 *),
    187187    [(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 *),
    191191    [(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 *),
    195195    [(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)))〉]
    198198.
    199199
    … …  
    201201  (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)];
    202202   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))]
    210210.
    211211normalize  (* you can examine the result here *)

  • src/Clight/test/io.ma

    r725 r726  
    22
    33definition 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  )〉 ]
    77      (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))
    1010          (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
    1111        [(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))
    1313                            (Tint I32 Signed  )))))
    1414   
    … …  
    1616   
    1717  )〉]
    18   (succ_pos_of_nat 1)
     18  (ident_of_nat 1)
    1919  []
    2020.
    … …  
    2222example exec:
    2323 (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〉.
    2525normalize  (* you can examine the result here *)
    2626@refl

  • src/Clight/test/io2.ma

    r725 r726  
    22
    33definition 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  )〉 ]
    77      (Ssequence
    8       (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  ))
     8      (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    99        (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    1010      (Ssequence
    1111      (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))
    1414          (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
    1515        [(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  ))
    1717        (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  )))
    2020          (Tint I32 Signed  ))))
    21       (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 2))
     21      (Sreturn (Some expr (Expr (Evar (ident_of_nat 2))
    2222                            (Tint I32 Signed  ))))))
    2323   
    … …  
    2525   
    2626  )〉]
    27   (succ_pos_of_nat 1)
     27  (ident_of_nat 1)
    2828  []
    2929.
    … …  
    3131example exec:
    3232 (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〉.
    3434normalize  (* you can examine the result here *)
    3535@refl

  • src/Clight/test/search.ma

    r725 r726  
    22
    33definition 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 )〉 ]
    66       (Ssequence
    7        (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned ))
     7       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    88         (Expr (Ecast (Tint I8 Unsigned )
    99           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    1010           (Tint I8 Unsigned )))
    1111       (Ssequence
    12        (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned ))
     12       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    1313         (Expr (Ecast (Tint I8 Unsigned )
    1414           (Expr (Ebinop Osub
    1515             (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 )))
    1717               (Tint I32 Signed  ))
    1818             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    … …  
    2222       (Swhile (Expr (Ebinop Oge
    2323                 (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 )))
    2525                   (Tint I32 Signed  ))
    2626                 (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 )))
    2828                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    2929         (Ssequence
    30          (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I8 Unsigned ))
     30         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    3131           (Expr (Ecast (Tint I8 Unsigned )
    3232             (Expr (Ebinop Odiv
    3333               (Expr (Ebinop Oadd
    3434                 (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 )))
    3636                   (Tint I32 Signed  ))
    3737                 (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 )))
    3939                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    4040               (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    … …  
    4545                          (Expr (Ederef
    4646                            (Expr (Ebinop Oadd
    47                               (Expr (Evar (succ_pos_of_nat 4))
     47                              (Expr (Evar (ident_of_nat 4))
    4848                                (Tpointer Any (Tint I8 Unsigned )))
    49                               (Expr (Evar (succ_pos_of_nat 3))
     49                              (Expr (Evar (ident_of_nat 3))
    5050                                (Tint I8 Unsigned )))
    5151                              (Tpointer Any (Tint I8 Unsigned ))))
    5252                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    5353                        (Expr (Ecast (Tint I32 Signed  )
    54                           (Expr (Evar (succ_pos_of_nat 6))
     54                          (Expr (Evar (ident_of_nat 6))
    5555                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    5656                        (Tint I32 Signed  ))
    57            (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
     57           (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    5858                                 (Tint I8 Unsigned ))))
    5959           Sskip)
    … …  
    6363                          (Expr (Ederef
    6464                            (Expr (Ebinop Oadd
    65                               (Expr (Evar (succ_pos_of_nat 4))
     65                              (Expr (Evar (ident_of_nat 4))
    6666                                (Tpointer Any (Tint I8 Unsigned )))
    67                               (Expr (Evar (succ_pos_of_nat 3))
     67                              (Expr (Evar (ident_of_nat 3))
    6868                                (Tint I8 Unsigned )))
    6969                              (Tpointer Any (Tint I8 Unsigned ))))
    7070                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    7171                        (Expr (Ecast (Tint I32 Signed  )
    72                           (Expr (Evar (succ_pos_of_nat 6))
     72                          (Expr (Evar (ident_of_nat 6))
    7373                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    7474                        (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 ))
    7676             (Expr (Ecast (Tint I8 Unsigned )
    7777               (Expr (Ebinop Osub
    7878                 (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 )))
    8080                   (Tint I32 Signed  ))
    8181                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    … …  
    8686                          (Expr (Ederef
    8787                            (Expr (Ebinop Oadd
    88                               (Expr (Evar (succ_pos_of_nat 4))
     88                              (Expr (Evar (ident_of_nat 4))
    8989                                (Tpointer Any (Tint I8 Unsigned )))
    90                               (Expr (Evar (succ_pos_of_nat 3))
     90                              (Expr (Evar (ident_of_nat 3))
    9191                                (Tint I8 Unsigned )))
    9292                              (Tpointer Any (Tint I8 Unsigned ))))
    9393                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    9494                        (Expr (Ecast (Tint I32 Signed  )
    95                           (Expr (Evar (succ_pos_of_nat 6))
     95                          (Expr (Evar (ident_of_nat 6))
    9696                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    9797                        (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 ))
    9999             (Expr (Ecast (Tint I8 Unsigned )
    100100               (Expr (Ebinop Oadd
    101101                 (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 )))
    103103                   (Tint I32 Signed  ))
    104104                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    … …  
    114114     
    115115   )〉;
    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 )〉 ]
    118118      (Ssequence
    119119      (Sassign (Expr (Ederef
    120120                 (Expr (Ebinop Oadd
    121                    (Expr (Evar (succ_pos_of_nat 4))
     121                   (Expr (Evar (ident_of_nat 4))
    122122                     (Tarray Any (Tint I8 Unsigned ) 5))
    123123                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    … …  
    129129      (Sassign (Expr (Ederef
    130130                 (Expr (Ebinop Oadd
    131                    (Expr (Evar (succ_pos_of_nat 4))
     131                   (Expr (Evar (ident_of_nat 4))
    132132                     (Tarray Any (Tint I8 Unsigned ) 5))
    133133                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    … …  
    139139      (Sassign (Expr (Ederef
    140140                 (Expr (Ebinop Oadd
    141                    (Expr (Evar (succ_pos_of_nat 4))
     141                   (Expr (Evar (ident_of_nat 4))
    142142                     (Tarray Any (Tint I8 Unsigned ) 5))
    143143                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    … …  
    149149      (Sassign (Expr (Ederef
    150150                 (Expr (Ebinop Oadd
    151                    (Expr (Evar (succ_pos_of_nat 4))
     151                   (Expr (Evar (ident_of_nat 4))
    152152                     (Tarray Any (Tint I8 Unsigned ) 5))
    153153                   (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
    … …  
    159159      (Sassign (Expr (Ederef
    160160                 (Expr (Ebinop Oadd
    161                    (Expr (Evar (succ_pos_of_nat 4))
     161                   (Expr (Evar (ident_of_nat 4))
    162162                     (Tarray Any (Tint I8 Unsigned ) 5))
    163163                   (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
    … …  
    167167          (Tint I8 Unsigned )))
    168168      (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))
    171171          (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));
    173173        (Expr (Ecast (Tint I8 Unsigned )
    174174          (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
    … …  
    178178          (Tint I8 Unsigned ))])
    179179      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    180                             (Expr (Evar (succ_pos_of_nat 8))
     180                            (Expr (Evar (ident_of_nat 8))
    181181                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
    182182   
    … …  
    184184   
    185185  )〉]
    186   (succ_pos_of_nat 7)
     186  (ident_of_nat 7)
    187187  []
    188188.
    … …  
    190190example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).
    191191normalize  (* you can examine the result here *)
     192%
     193qed.

  • src/RTLabs/import.ma

    r710 r726  
    22include "RTLabs/RTLabs-sem.ma".
    33
    4 definition new_reg : internal_function → register × internal_function ≝
    5 λf. let 〈r, g〉 ≝ register_new (f_reggen f) in
    6     〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f)
     4definition 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)
    77            (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    88
    9 definition new_label : internal_function → label × internal_function ≝
    10 λf. let 〈l, g〉 ≝ label_new (f_labgen f) in
    11     〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f)
     9definition 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)
    1212            (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    1313
    … …  
    1717            (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f).
    1818
    19 let rec n_labels (n:nat) (g:label_generation) : Vector label n × label_generation ≝
     19let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation) ≝
    2020match n with
    21 [ O ⇒ 〈[[ ]], g〉
    22 | S m ⇒ let 〈ls, g'〉 ≝ n_labels m g in
    23         let 〈l, g''〉 ≝ label_new g in
    24         〈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''〉
    2525].
    2626
    27 let rec n_regs (n:nat) (g:register_generation) : Vector label n × register_generation ≝
     27let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation) ≝
    2828match n with
    29 [ O ⇒ 〈[[ ]], g〉
    30 | S m ⇒ let 〈ls, g'〉 ≝ n_regs m g in
    31         let 〈l, g''〉 ≝ register_new g in
    32         〈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''〉
    3333].
    3434
    … …  
    6161                  match m r with
    6262                  [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉
    63                   | None ⇒ let 〈r',g'〉 ≝ register_new g in
     63                  | None ⇒ do 〈r',g'〉 ← register_new g;
    6464                           OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉
    6565                  ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs;
    … …  
    8888  let rmap ≝ λn. opt_to_res … (rmap3 n) in
    8989  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 in
     90  do 〈labels, gen〉 ← n_labels max_stmt label_gen_new;
    9191  let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
    9292  do graph ← foldr ?? (λp,g0. do g ← g0;

  • src/common/Graphs.ma

    r710 r726  
     1include "basics/types.ma".
    12
    2 include "basics/logic.ma".
     3include "ASM/BitVectorTrie.ma".
     4include "Clight/AST.ma".
     5include "common/Errors.ma".
    36
    4 include "utilities/binary/positive.ma".
    5 include "common/Maps.ma".
     7definition label ≝ ident.
    68
    7 definition label : Type[0] ≝ Pos.
    8 definition graph : Type[0] → Type[0] ≝ tree_t … PTree.
     9definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq.
     10
     11record label_generation : Type[0] ≝ { lab_next : label }.
     12
     13definition label_gen_new : label_generation ≝ mk_label_generation (zero ?).
     14
     15definition 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
     21definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
     22definition empty_graph : ∀T. graph T ≝ λT. Stub T 16.
    923definition 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.
    1125definition 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.
    1427
    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.
    1828
    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  
    33
    44include "basics/types.ma".
    5 include "utilities/binary/positive.ma".
    65
    7 include "common/Maps.ma".
     6include "ASM/BitVectorTrie.ma".
     7include "Clight/AST.ma".
     8include "common/Errors.ma".
    89
    9 definition register ≝ Pos.
     10definition register ≝ ident.
    1011
    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.
     12definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq.
    1413
    1514record register_generation : Type[0] ≝ { reg_next : register }.
    1615
    17 definition register_gen_new : register_generation ≝ mk_register_generation one.
     16definition register_gen_new : register_generation ≝ mk_register_generation (zero ?).
    1817
    19 definition register_new : register_generation → register × register_generation ≝
    20 λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉.
     18definition 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.
    2123
    22 definition register_env : Type[0] → Type[0] ≝ tree_t … PTree.
    23 definition register_empty : ∀T. register_env T ≝ λT. empty ? PTree T.
     24definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
     25definition register_empty : ∀T. register_env T ≝ λT. Stub T 16.
    2426definition 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.
    2628definition 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.