Changeset 1077 for src/RTLabs


Ignore:
Timestamp:
Jul 19, 2011, 12:23:32 PM (8 years ago)
Author:
mulligan
Message:

ack, dependent types are scary

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1073 r1077  
    44include "common/FrontEndOps.ma".
    55include "common/Graphs.ma".
    6 
    7 axiom graph_add_lookup:
    8   ∀g: graph rtl_statement.
    9   ∀l: label.
    10   ∀s: rtl_statement.
    11   ∀to_insert: label.
    12     lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
    136
    147definition add_graph ≝
     
    3225      [1: @LABEL
    3326      |2: cases(HYP)
    34           generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
     27          generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
     28          normalize nodelta;
    3529          /2/
    3630      ]
     
    3933      [1: @LABEL
    4034      |2: cases(HYP)
    41           generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
     35          generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
     36          normalize nodelta;
    4237          /2/
    4338      ]
     
    12221217qed.
    12231218
    1224 axiom graph_add:
    1225   ∀g: graph rtl_statement.
    1226   ∀l: label.
    1227   ∀s: rtl_statement.
    1228     lookup ? ? (add ? ? g l s) l ≠ None ?.
    1229 
    12301219(* XXX: we use a "hack" here to circumvent the proof obligations required to
    12311220   create res, an empty internal_function record.  we insert into our graph
     
    12601249    mk_rtl_internal_function luniverse' runiverse' result' params'
    12611250                         locals' stack_size' graph' ? ? in
    1262     fold ? ? ? (translate_stmt lenv) (f_graph def) res.
     1251    foldi ? ? ? (translate_stmt lenv) (f_graph def) res.
    12631252  [1: %
    12641253      [1: @entry'
    12651254      |2: normalize nodelta;
    1266           @(graph_add ? (f_entry def) ?)
    12671255          @graph_add_lookup
     1256          @graph_add
    12681257      ]
    12691258  |2: %
    12701259      [1: @exit'
    1271       |2: /2/
     1260      |2: normalize nodelta;
     1261          @graph_add
    12721262      ]
    12731263  ]
     
    12811271  ].
    12821272
     1273(* XXX: change, we need to propagate the region information, not ignore it *)
    12831274definition init_data_to_nat ≝
    12841275  λi: init_data.
Note: See TracChangeset for help on using the changeset viewer.