Changeset 1280 for src/joint


Ignore:
Timestamp:
Sep 28, 2011, 2:43:37 AM (8 years ago)
Author:
sacerdot
Message:

Some progress in the porting of RTLAbstoRTL to the joint syntax:

1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are

probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.

Location:
src/joint
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1275 r1280  
    1717 
    1818 ; extend_statements: Type[0]
    19  
    20  ; resultT: Type[0]
    21  ; localsT: Type[0]
    22  ; paramsT: Type[0]
    2319 }.
    2420
     
    2723 ; succ: Type[0]
    2824 }.
     25
     26(* One common instantiation of params via Graphs of joint_statements
     27   (all languages but LIN) *)
     28definition graph_params_ : params__ → params_ ≝
     29 λpars__. mk_params_ pars__ label.
    2930
    3031inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
     
    5253  | joint_st_return: joint_statement p globals.
    5354
     55record params0: Type[1] ≝
     56 { pars__' :> params__
     57 ; resultT: Type[0]
     58 ; paramsT: Type[0]
     59 }.
     60
     61record params1 : Type[1] ≝
     62 { pars0 :> params0
     63 ; localsT: Type[0]
     64 }.
    5465
    5566record params (globals: list ident): Type[1] ≝
    56  { pars_:> params_
     67 { succ_ : Type[0]
     68 ; pars1 :> params1
    5769 ; codeT: Type[0]
    58  ; lookup: codeT → label → option (joint_statement pars_ globals)
     70 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
    5971 }.
     72 
     73definition params__of_params: ∀globals. params globals → params_ ≝
     74 λglobals,pars. mk_params_ pars (succ_ … pars).
     75coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
     76 on _p: params ? to params_.
    6077
    6178include alias "common/Graphs.ma". (* To pick the right lookup *)
    6279
    63 (* One common instantiation of params via Graphs of joint_statements *)
    64 definition graph_params: params_ → ∀globals: list ident. params globals ≝
    65  λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …).
     80(* One common instantiation of params via Graphs of joint_statements
     81   (all languages but LIN) *)
     82definition graph_params: params1 → ∀globals: list ident. params globals ≝
     83 λpars1,globals.
     84  mk_params globals label pars1
     85   (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).
     86
     87
     88(* CSC: special case where localsT is a list of register (RTL and ERTL) *)
     89definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
     90definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).
    6691
    6792record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
     
    123148(* Specialized for graph_params *)
    124149definition add_graph ≝
    125   λpars_,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars_ globals).
     150  λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
    126151   let code ≝ add … (joint_if_code ?? p) l stmt in
    127     mk_joint_internal_function … (graph_params pars_ globals)
     152    mk_joint_internal_function … (graph_params globals)
    128153     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    129154     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
Note: See TracChangeset for help on using the changeset viewer.