Changeset 2649 for extracted/csem.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.ml

    r2601 r2649  
    33open Extra_bool
    44
     5open Coqlib
     6
    57open Values
    68
     
    3537open Identifiers
    3638
    37 open Coqlib
    38 
    39 open Floats
    40 
    4139open Arithmetic
    4240
     
    5755open AST
    5856
     57open ErrorMessages
     58
    5959open Option
    6060
     
    6868
    6969open Positive
    70 
    71 open Char
    72 
    73 open String
    7470
    7571open PreIdentifiers
     
    710706(** val empty_env : env **)
    711707let empty_env =
    712   Identifiers.empty_map AST.symbolTag
     708  Identifiers.empty_map PreIdentifiers.SymbolTag
    713709
    714710(** val load_value_of_type :
     
    737733(** val blocks_of_env : env -> Pointers.block List.list **)
    738734let blocks_of_env e1 =
    739   List.map (fun x -> x.Types.snd) (Identifiers.elements AST.symbolTag e1)
     735  List.map (fun x -> x.Types.snd)
     736    (Identifiers.elements PreIdentifiers.SymbolTag e1)
    740737
    741738(** val select_switch :
     
    779776let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    780777| Kstop -> h_Kstop
    781 | Kseq (x_7621, x_7620) ->
    782   h_Kseq x_7621 x_7620
     778| Kseq (x_5937, x_5936) ->
     779  h_Kseq x_5937 x_5936
    783780    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    784       h_Kswitch h_Kcall x_7620)
    785 | Kwhile (x_7624, x_7623, x_7622) ->
    786   h_Kwhile x_7624 x_7623 x_7622
     781      h_Kswitch h_Kcall x_5936)
     782| Kwhile (x_5940, x_5939, x_5938) ->
     783  h_Kwhile x_5940 x_5939 x_5938
    787784    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    788       h_Kswitch h_Kcall x_7622)
    789 | Kdowhile (x_7627, x_7626, x_7625) ->
    790   h_Kdowhile x_7627 x_7626 x_7625
     785      h_Kswitch h_Kcall x_5938)
     786| Kdowhile (x_5943, x_5942, x_5941) ->
     787  h_Kdowhile x_5943 x_5942 x_5941
    791788    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    792       h_Kswitch h_Kcall x_7625)
    793 | Kfor2 (x_7631, x_7630, x_7629, x_7628) ->
    794   h_Kfor2 x_7631 x_7630 x_7629 x_7628
     789      h_Kswitch h_Kcall x_5941)
     790| Kfor2 (x_5947, x_5946, x_5945, x_5944) ->
     791  h_Kfor2 x_5947 x_5946 x_5945 x_5944
    795792    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    796       h_Kswitch h_Kcall x_7628)
    797 | Kfor3 (x_7635, x_7634, x_7633, x_7632) ->
    798   h_Kfor3 x_7635 x_7634 x_7633 x_7632
     793      h_Kswitch h_Kcall x_5944)
     794| Kfor3 (x_5951, x_5950, x_5949, x_5948) ->
     795  h_Kfor3 x_5951 x_5950 x_5949 x_5948
    799796    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    800       h_Kswitch h_Kcall x_7632)
    801 | Kswitch x_7636 ->
    802   h_Kswitch x_7636
     797      h_Kswitch h_Kcall x_5948)
     798| Kswitch x_5952 ->
     799  h_Kswitch x_5952
    803800    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    804       h_Kswitch h_Kcall x_7636)
    805 | Kcall (x_7640, x_7639, x_7638, x_7637) ->
    806   h_Kcall x_7640 x_7639 x_7638 x_7637
     801      h_Kswitch h_Kcall x_5952)
     802| Kcall (x_5956, x_5955, x_5954, x_5953) ->
     803  h_Kcall x_5956 x_5955 x_5954 x_5953
    807804    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    808       h_Kswitch h_Kcall x_7637)
     805      h_Kswitch h_Kcall x_5953)
    809806
    810807(** val cont_rect_Type3 :
     
    819816let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    820817| Kstop -> h_Kstop
    821 | Kseq (x_7681, x_7680) ->
    822   h_Kseq x_7681 x_7680
     818| Kseq (x_5997, x_5996) ->
     819  h_Kseq x_5997 x_5996
    823820    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    824       h_Kswitch h_Kcall x_7680)
    825 | Kwhile (x_7684, x_7683, x_7682) ->
    826   h_Kwhile x_7684 x_7683 x_7682
     821      h_Kswitch h_Kcall x_5996)
     822| Kwhile (x_6000, x_5999, x_5998) ->
     823  h_Kwhile x_6000 x_5999 x_5998
    827824    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    828       h_Kswitch h_Kcall x_7682)
    829 | Kdowhile (x_7687, x_7686, x_7685) ->
    830   h_Kdowhile x_7687 x_7686 x_7685
     825      h_Kswitch h_Kcall x_5998)
     826| Kdowhile (x_6003, x_6002, x_6001) ->
     827  h_Kdowhile x_6003 x_6002 x_6001
    831828    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    832       h_Kswitch h_Kcall x_7685)
    833 | Kfor2 (x_7691, x_7690, x_7689, x_7688) ->
    834   h_Kfor2 x_7691 x_7690 x_7689 x_7688
     829      h_Kswitch h_Kcall x_6001)
     830| Kfor2 (x_6007, x_6006, x_6005, x_6004) ->
     831  h_Kfor2 x_6007 x_6006 x_6005 x_6004
    835832    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    836       h_Kswitch h_Kcall x_7688)
    837 | Kfor3 (x_7695, x_7694, x_7693, x_7692) ->
    838   h_Kfor3 x_7695 x_7694 x_7693 x_7692
     833      h_Kswitch h_Kcall x_6004)
     834| Kfor3 (x_6011, x_6010, x_6009, x_6008) ->
     835  h_Kfor3 x_6011 x_6010 x_6009 x_6008
    839836    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    840       h_Kswitch h_Kcall x_7692)
    841 | Kswitch x_7696 ->
    842   h_Kswitch x_7696
     837      h_Kswitch h_Kcall x_6008)
     838| Kswitch x_6012 ->
     839  h_Kswitch x_6012
    843840    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    844       h_Kswitch h_Kcall x_7696)
    845 | Kcall (x_7700, x_7699, x_7698, x_7697) ->
    846   h_Kcall x_7700 x_7699 x_7698 x_7697
     841      h_Kswitch h_Kcall x_6012)
     842| Kcall (x_6016, x_6015, x_6014, x_6013) ->
     843  h_Kcall x_6016 x_6015 x_6014 x_6013
    847844    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    848       h_Kswitch h_Kcall x_7697)
     845      h_Kswitch h_Kcall x_6013)
    849846
    850847(** val cont_rect_Type2 :
     
    859856let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    860857| Kstop -> h_Kstop
    861 | Kseq (x_7711, x_7710) ->
    862   h_Kseq x_7711 x_7710
     858| Kseq (x_6027, x_6026) ->
     859  h_Kseq x_6027 x_6026
    863860    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    864       h_Kswitch h_Kcall x_7710)
    865 | Kwhile (x_7714, x_7713, x_7712) ->
    866   h_Kwhile x_7714 x_7713 x_7712
     861      h_Kswitch h_Kcall x_6026)
     862| Kwhile (x_6030, x_6029, x_6028) ->
     863  h_Kwhile x_6030 x_6029 x_6028
    867864    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    868       h_Kswitch h_Kcall x_7712)
    869 | Kdowhile (x_7717, x_7716, x_7715) ->
    870   h_Kdowhile x_7717 x_7716 x_7715
     865      h_Kswitch h_Kcall x_6028)
     866| Kdowhile (x_6033, x_6032, x_6031) ->
     867  h_Kdowhile x_6033 x_6032 x_6031
    871868    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    872       h_Kswitch h_Kcall x_7715)
    873 | Kfor2 (x_7721, x_7720, x_7719, x_7718) ->
    874   h_Kfor2 x_7721 x_7720 x_7719 x_7718
     869      h_Kswitch h_Kcall x_6031)
     870| Kfor2 (x_6037, x_6036, x_6035, x_6034) ->
     871  h_Kfor2 x_6037 x_6036 x_6035 x_6034
    875872    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    876       h_Kswitch h_Kcall x_7718)
    877 | Kfor3 (x_7725, x_7724, x_7723, x_7722) ->
    878   h_Kfor3 x_7725 x_7724 x_7723 x_7722
     873      h_Kswitch h_Kcall x_6034)
     874| Kfor3 (x_6041, x_6040, x_6039, x_6038) ->
     875  h_Kfor3 x_6041 x_6040 x_6039 x_6038
    879876    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    880       h_Kswitch h_Kcall x_7722)
    881 | Kswitch x_7726 ->
    882   h_Kswitch x_7726
     877      h_Kswitch h_Kcall x_6038)
     878| Kswitch x_6042 ->
     879  h_Kswitch x_6042
    883880    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    884       h_Kswitch h_Kcall x_7726)
    885 | Kcall (x_7730, x_7729, x_7728, x_7727) ->
    886   h_Kcall x_7730 x_7729 x_7728 x_7727
     881      h_Kswitch h_Kcall x_6042)
     882| Kcall (x_6046, x_6045, x_6044, x_6043) ->
     883  h_Kcall x_6046 x_6045 x_6044 x_6043
    887884    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    888       h_Kswitch h_Kcall x_7727)
     885      h_Kswitch h_Kcall x_6043)
    889886
    890887(** val cont_rect_Type1 :
     
    899896let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    900897| Kstop -> h_Kstop
    901 | Kseq (x_7741, x_7740) ->
    902   h_Kseq x_7741 x_7740
     898| Kseq (x_6057, x_6056) ->
     899  h_Kseq x_6057 x_6056
    903900    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    904       h_Kswitch h_Kcall x_7740)
    905 | Kwhile (x_7744, x_7743, x_7742) ->
    906   h_Kwhile x_7744 x_7743 x_7742
     901      h_Kswitch h_Kcall x_6056)
     902| Kwhile (x_6060, x_6059, x_6058) ->
     903  h_Kwhile x_6060 x_6059 x_6058
    907904    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    908       h_Kswitch h_Kcall x_7742)
    909 | Kdowhile (x_7747, x_7746, x_7745) ->
    910   h_Kdowhile x_7747 x_7746 x_7745
     905      h_Kswitch h_Kcall x_6058)
     906| Kdowhile (x_6063, x_6062, x_6061) ->
     907  h_Kdowhile x_6063 x_6062 x_6061
    911908    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    912       h_Kswitch h_Kcall x_7745)
    913 | Kfor2 (x_7751, x_7750, x_7749, x_7748) ->
    914   h_Kfor2 x_7751 x_7750 x_7749 x_7748
     909      h_Kswitch h_Kcall x_6061)
     910| Kfor2 (x_6067, x_6066, x_6065, x_6064) ->
     911  h_Kfor2 x_6067 x_6066 x_6065 x_6064
    915912    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    916       h_Kswitch h_Kcall x_7748)
    917 | Kfor3 (x_7755, x_7754, x_7753, x_7752) ->
    918   h_Kfor3 x_7755 x_7754 x_7753 x_7752
     913      h_Kswitch h_Kcall x_6064)
     914| Kfor3 (x_6071, x_6070, x_6069, x_6068) ->
     915  h_Kfor3 x_6071 x_6070 x_6069 x_6068
    919916    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    920       h_Kswitch h_Kcall x_7752)
    921 | Kswitch x_7756 ->
    922   h_Kswitch x_7756
     917      h_Kswitch h_Kcall x_6068)
     918| Kswitch x_6072 ->
     919  h_Kswitch x_6072
    923920    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    924       h_Kswitch h_Kcall x_7756)
    925 | Kcall (x_7760, x_7759, x_7758, x_7757) ->
    926   h_Kcall x_7760 x_7759 x_7758 x_7757
     921      h_Kswitch h_Kcall x_6072)
     922| Kcall (x_6076, x_6075, x_6074, x_6073) ->
     923  h_Kcall x_6076 x_6075 x_6074 x_6073
    927924    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    928       h_Kswitch h_Kcall x_7757)
     925      h_Kswitch h_Kcall x_6073)
    929926
    930927(** val cont_rect_Type0 :
     
    939936let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    940937| Kstop -> h_Kstop
    941 | Kseq (x_7771, x_7770) ->
    942   h_Kseq x_7771 x_7770
     938| Kseq (x_6087, x_6086) ->
     939  h_Kseq x_6087 x_6086
    943940    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    944       h_Kswitch h_Kcall x_7770)
    945 | Kwhile (x_7774, x_7773, x_7772) ->
    946   h_Kwhile x_7774 x_7773 x_7772
     941      h_Kswitch h_Kcall x_6086)
     942| Kwhile (x_6090, x_6089, x_6088) ->
     943  h_Kwhile x_6090 x_6089 x_6088
    947944    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    948       h_Kswitch h_Kcall x_7772)
    949 | Kdowhile (x_7777, x_7776, x_7775) ->
    950   h_Kdowhile x_7777 x_7776 x_7775
     945      h_Kswitch h_Kcall x_6088)
     946| Kdowhile (x_6093, x_6092, x_6091) ->
     947  h_Kdowhile x_6093 x_6092 x_6091
    951948    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    952       h_Kswitch h_Kcall x_7775)
    953 | Kfor2 (x_7781, x_7780, x_7779, x_7778) ->
    954   h_Kfor2 x_7781 x_7780 x_7779 x_7778
     949      h_Kswitch h_Kcall x_6091)
     950| Kfor2 (x_6097, x_6096, x_6095, x_6094) ->
     951  h_Kfor2 x_6097 x_6096 x_6095 x_6094
    955952    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    956       h_Kswitch h_Kcall x_7778)
    957 | Kfor3 (x_7785, x_7784, x_7783, x_7782) ->
    958   h_Kfor3 x_7785 x_7784 x_7783 x_7782
     953      h_Kswitch h_Kcall x_6094)
     954| Kfor3 (x_6101, x_6100, x_6099, x_6098) ->
     955  h_Kfor3 x_6101 x_6100 x_6099 x_6098
    959956    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    960       h_Kswitch h_Kcall x_7782)
    961 | Kswitch x_7786 ->
    962   h_Kswitch x_7786
     957      h_Kswitch h_Kcall x_6098)
     958| Kswitch x_6102 ->
     959  h_Kswitch x_6102
    963960    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    964       h_Kswitch h_Kcall x_7786)
    965 | Kcall (x_7790, x_7789, x_7788, x_7787) ->
    966   h_Kcall x_7790 x_7789 x_7788 x_7787
     961      h_Kswitch h_Kcall x_6102)
     962| Kcall (x_6106, x_6105, x_6104, x_6103) ->
     963  h_Kcall x_6106 x_6105 x_6104 x_6103
    967964    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    968       h_Kswitch h_Kcall x_7787)
     965      h_Kswitch h_Kcall x_6103)
    969966
    970967(** val cont_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.