Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/frontEndMem.ml

    r2717 r2773  
    1717open Errors
    1818
    19 open Setoids
    20 
    21 open Monad
    22 
    23 open Option
    24 
    2519open Lists
    2620
     
    3630
    3731open Arithmetic
     32
     33open Setoids
     34
     35open Monad
     36
     37open Option
    3838
    3939open Extranat
     
    9090
    9191(** val loadn :
    92     GenMem.mem1 -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
     92    GenMem.mem -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
    9393    Types.option **)
    9494let rec loadn m ptr = function
     
    106106
    107107(** val load :
    108     AST.typ -> GenMem.mem1 -> Pointers.pointer -> Values.val0 Types.option **)
     108    AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 Types.option **)
    109109let load t m ptr =
    110110  match loadn m ptr (AST.typesize t) with
     
    113113
    114114(** val loadv :
    115     AST.typ -> GenMem.mem1 -> Values.val0 -> Values.val0 Types.option **)
     115    AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 Types.option **)
    116116let rec loadv t m = function
    117117| Values.Vundef -> Types.None
     
    121121
    122122(** val storen :
    123     GenMem.mem1 -> Pointers.pointer -> ByteValues.beval List.list ->
    124     GenMem.mem1 Types.option **)
     123    GenMem.mem -> Pointers.pointer -> ByteValues.beval List.list ->
     124    GenMem.mem Types.option **)
    125125let rec storen m ptr = function
    126126| List.Nil -> Types.Some m
     
    135135
    136136(** val store :
    137     AST.typ -> GenMem.mem1 -> Pointers.pointer -> Values.val0 -> GenMem.mem1
     137    AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 -> GenMem.mem
    138138    Types.option **)
    139139let store t m ptr v =
     
    141141
    142142(** val storev :
    143     AST.typ -> GenMem.mem1 -> Values.val0 -> Values.val0 -> GenMem.mem1
     143    AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 -> GenMem.mem
    144144    Types.option **)
    145145let storev t m addr v =
     
    150150  | Values.Vptr ptr -> store t m ptr v
    151151
    152 (** val valid_pointer : GenMem.mem1 -> Pointers.pointer -> Bool.bool **)
     152(** val valid_pointer : GenMem.mem -> Pointers.pointer -> Bool.bool **)
    153153let valid_pointer m ptr =
    154154  let off =
Note: See TracChangeset for help on using the changeset viewer.