Ignore:
Timestamp:
Nov 6, 2012, 4:12:21 PM (7 years ago)
Author:
tranquil
Message:

new back end operations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndVal.ma

    r2286 r2435  
    66   resolve the sizes; they are not strictly checked. *)
    77
    8 let rec make_parts_aux (*r:region*) (n:nat) (H:lt n (size_pointer (*r*))) (tl:list (part (*r*))) on n : list (part (*r*)) ≝
    9 match n return λn.lt n ? → ? with
    10 [ O ⇒ λH'. (mk_part (*r*) O H')::tl
    11 | S m ⇒ λH'. make_parts_aux (*r*) m ? ((mk_part (*r*) n H)::tl)
    12 ] H.
    13 /2/
    14 qed.
    15 
    16 definition make_parts : (*∀r:region.*) list (part (*r*)) ≝
    17 (*λr.*) make_parts_aux (*r*) (pred (size_pointer (*r*))) ? [ ].
    18 //
    19 qed.
     8definition make_parts : list part ≝
     9  map ?? part_from_sig (range_strong size_pointer).
    2010
    2111definition make_be_null : (*region →*) list beval ≝
     
    8676| cons h t ⇒
    8777    match h with
    88     [ BVundef ⇒ Vundef
    89     | BVnonzero ⇒ Vundef
    90     | BVByte b ⇒ build_integer_val ty l
    91     | BVptr _ _ _ ⇒
     78    [ BVByte b ⇒ build_integer_val ty l
     79    | BVptr _ _ ⇒
    9280      match pointer_of_bevals l with
    9381      [ OK ptr ⇒ Vptr ptr
     
    9583      ]
    9684    | BVnull  pt ⇒ if eqb (part_no  pt) O ∧ check_be_null  (S O) t then Vnull  else Vundef
     85    | _ ⇒ Vundef
    9786    ]
    9887].
Note: See TracChangeset for help on using the changeset viewer.