Ignore:
Timestamp:
Feb 18, 2013, 5:48:19 PM (7 years ago)
Author:
tranquil
Message:
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2645 r2674  
    33include "utilities/hide.ma".
    44include "ASM/BitVectorTrie.ma".
     5include "joint/TranslateUtils.ma".
    56
    67record hw_register_env : Type[0] ≝
     
    6566(******************************** GRAPHS **************************************)
    6667
    67 definition make_sem_graph_params :
    68   ∀pars : unserialized_params.
    69   ∀g_pars : ∀F.sem_unserialized_params pars F.
     68record sem_graph_params : Type[1] ≝
     69{ sgp_pars : unserialized_params
     70; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
     71}.
     72
     73definition sem_graph_params_to_graph_params :
     74  ∀pars : sem_graph_params.graph_params ≝
     75  λpars.mk_graph_params (sgp_pars pars).
     76
     77coercion graph_params_from_sem_graph_params nocomposites :
     78  ∀pars : sem_graph_params.
     79  graph_params ≝ sem_graph_params_to_graph_params
     80  on _pars : sem_graph_params to graph_params.
     81
     82definition sem_graph_params_to_sem_params :
     83  ∀pars : sem_graph_params.
    7084  sem_params ≝
    71   λpars,spars.
    72   let g_pars ≝ mk_graph_params pars in
     85  λpars.
    7386  mk_sem_params
    74     g_pars
    75     (spars ?)
     87    (pars : graph_params)
     88    (sgp_sup pars ?)
    7689    (word_of_identifier ?)
    7790    (an_identifier ?)
    7891    ? (refl …).
    7992* #p % qed.
     93
     94coercion sem_params_from_sem_graph_params :
     95  ∀pars : sem_graph_params.
     96  sem_params ≝ sem_graph_params_to_sem_params
     97  on _pars : sem_graph_params to sem_params.
     98
    8099
    81100(******************************** LINEAR **************************************)
     
    85104#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
    86105
    87 definition make_sem_lin_params :
    88   ∀pars : unserialized_params.
    89   (∀F.sem_unserialized_params pars F) →
     106record sem_lin_params : Type[1] ≝
     107{ slp_pars : unserialized_params
     108; slp_sup : ∀F.sem_unserialized_params slp_pars F
     109}.
     110
     111definition sem_lin_params_to_lin_params :
     112  ∀pars : sem_lin_params.lin_params ≝
     113  λpars.mk_lin_params (slp_pars pars).
     114
     115coercion lin_params_from_sem_lin_params nocomposites :
     116  ∀pars : sem_lin_params.
     117  lin_params ≝ sem_lin_params_to_lin_params
     118  on _pars : sem_lin_params to lin_params.
     119
     120definition sem_lin_params_to_sem_params :
     121  ∀pars : sem_lin_params.
    90122  sem_params ≝
    91   λpars,spars.
    92   let lin_pars ≝ mk_lin_params pars in
     123  λpars.
    93124  mk_sem_params
    94     lin_pars
    95     (spars ?)
     125    (pars : lin_params)
     126    (slp_sup pars ?)
    96127    succ_pos_of_nat
    97128    (λp.pred (nat_of_pos p))
     
    101132] qed.
    102133
    103 
     134coercion sem_params_from_sem_lin_params :
     135  ∀pars : sem_lin_params.
     136  sem_params ≝ sem_lin_params_to_sem_params
     137  on _pars : sem_lin_params to sem_params.
    104138
    105139
     
    130164qed.
    131165
     166(*lemma b_graph_translate_eval :
     167  ∀src : sem_graph_params.
     168  ∀dst : sem_graph_params.
     169  ∀globals: list ident.
     170  ∀init_ret,init_params,init_stack_size.
     171  ∀f_step,f_fin,def_in.
     172  let def_out ≝
     173    b_graph_translate src_g_pars dst_g_pars globals
     174      init_ret init_params init_stack_size f_step f_fin def_in in
     175  ∀st : state_pc src
     176*)
Note: See TracChangeset for help on using the changeset viewer.