Changeset 2717 for extracted/values.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/values.ml

    r2649 r2717  
    6060
    6161open Division
     62
     63open Exp
    6264
    6365open Arithmetic
     
    8890let rec val_rect_Type4 h_Vundef h_Vint h_Vnull h_Vptr = function
    8991| Vundef -> h_Vundef
    90 | Vint (sz, x_2472) -> h_Vint sz x_2472
     92| Vint (sz, x_5034) -> h_Vint sz x_5034
    9193| Vnull -> h_Vnull
    92 | Vptr x_2473 -> h_Vptr x_2473
     94| Vptr x_5035 -> h_Vptr x_5035
    9395
    9496(** val val_rect_Type5 :
     
    9799let rec val_rect_Type5 h_Vundef h_Vint h_Vnull h_Vptr = function
    98100| Vundef -> h_Vundef
    99 | Vint (sz, x_2479) -> h_Vint sz x_2479
     101| Vint (sz, x_5041) -> h_Vint sz x_5041
    100102| Vnull -> h_Vnull
    101 | Vptr x_2480 -> h_Vptr x_2480
     103| Vptr x_5042 -> h_Vptr x_5042
    102104
    103105(** val val_rect_Type3 :
     
    106108let rec val_rect_Type3 h_Vundef h_Vint h_Vnull h_Vptr = function
    107109| Vundef -> h_Vundef
    108 | Vint (sz, x_2486) -> h_Vint sz x_2486
     110| Vint (sz, x_5048) -> h_Vint sz x_5048
    109111| Vnull -> h_Vnull
    110 | Vptr x_2487 -> h_Vptr x_2487
     112| Vptr x_5049 -> h_Vptr x_5049
    111113
    112114(** val val_rect_Type2 :
     
    115117let rec val_rect_Type2 h_Vundef h_Vint h_Vnull h_Vptr = function
    116118| Vundef -> h_Vundef
    117 | Vint (sz, x_2493) -> h_Vint sz x_2493
     119| Vint (sz, x_5055) -> h_Vint sz x_5055
    118120| Vnull -> h_Vnull
    119 | Vptr x_2494 -> h_Vptr x_2494
     121| Vptr x_5056 -> h_Vptr x_5056
    120122
    121123(** val val_rect_Type1 :
     
    124126let rec val_rect_Type1 h_Vundef h_Vint h_Vnull h_Vptr = function
    125127| Vundef -> h_Vundef
    126 | Vint (sz, x_2500) -> h_Vint sz x_2500
     128| Vint (sz, x_5062) -> h_Vint sz x_5062
    127129| Vnull -> h_Vnull
    128 | Vptr x_2501 -> h_Vptr x_2501
     130| Vptr x_5063 -> h_Vptr x_5063
    129131
    130132(** val val_rect_Type0 :
     
    133135let rec val_rect_Type0 h_Vundef h_Vint h_Vnull h_Vptr = function
    134136| Vundef -> h_Vundef
    135 | Vint (sz, x_2507) -> h_Vint sz x_2507
     137| Vint (sz, x_5069) -> h_Vint sz x_5069
    136138| Vnull -> h_Vnull
    137 | Vptr x_2508 -> h_Vptr x_2508
     139| Vptr x_5070 -> h_Vptr x_5070
    138140
    139141(** val val_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.