Changeset 1644


Ignore:
Timestamp:
Jan 13, 2012, 3:08:55 PM (8 years ago)
Author:
tranquil
Message:

minor changes

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1643 r1644  
    9696
    9797
    98 definition rtl_instruction ≝ joint_instruction rtl_uns_params.
     98definition rtl_instruction ≝ joint_instruction rtl_params.
     99unification hint 0 ≔
     100(*---------------*) ⊢
     101ext_instruction (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_instruction_extension.
     102unification hint 0 ≔ globals
     103(*---------------*) ⊢
     104joint_instruction (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_instruction globals.
    99105
    100106definition rtl_statement ≝ joint_statement rtl_params.
     107unification hint 0 ≔
     108(*---------------*) ⊢
     109ext_fin_instruction (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
     110unification hint 0 ≔ globals
     111(*---------------*) ⊢
     112joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    101113
    102114definition rtl_internal_function ≝
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1643 r1644  
    196196  | _ ⇒ True
    197197  ].
    198 
    199198definition translate_cst :
    200199  ∀globals: list ident.
     
    219218    | Oaddrstack offset ⇒ λeqcst.
    220219      let 〈r1, r2〉 ≝ make_addr … destrs ? in
    221       [extension rtl_params globals (rtl_st_ext_stack_address r1 r2)]
     220      [(rtl_st_ext_stack_address r1 r2 : rtl_instruction globals)]
    222221    ] (refl …)
    223222  ] (refl …).
     
    822821  | _ ⇒ True ].
    823822
    824 (* XXX: following conversation with CSC about the mix up in extension statements
    825         and extension instructions in RTL, use fake_label in calls to
    826         tailcall_* instructions. *)
    827823definition translate_inst : ∀globals.?→?→?→
    828824  (bind_list register unit (rtl_instruction globals)) × label ≝
     
    869865    (* Paolo: no notation to avoid ambiguity *)
    870866    〈bcons … (
    871       match retr with
     867      match retr return λ_.rtl_instruction globals with
    872868      [ Some retr ⇒
    873         extension rtl_params globals (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))
     869        rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv)
    874870      | None ⇒
    875         extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])
     871        rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ]
    876872      ]) [ ], lbl'〉
    877873  | St_cond r lbl_true lbl_false ⇒ λ_.
     
    894890  | St_tailcall_id f args ⇒ λ_.
    895891    add_graph rtl_params globals lbl
    896       (extension_fin rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
     892      (extension_fin (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
    897893  | St_tailcall_ptr f args ⇒ λ_.
    898894    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    899895    add_graph rtl_params globals lbl
    900       (extension_fin rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
     896      (extension_fin (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
    901897  | _ ⇒ λstmt_eq.
    902898    let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in
     
    935931  let entry' ≝ f_entry def in
    936932  let exit' ≝ f_exit def in
    937   let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry'
    938     (GOTO (rtl_params : params) globals entry') in
     933  let graph' ≝ empty_map LabelTag ? in
     934  let graph' ≝ add LabelTag ? graph' entry'
     935    (GOTO … exit') in
    939936  let graph' ≝ add LabelTag ? graph' exit'
    940     (RETURN (rtl_params : params) globals) in
     937    (RETURN ) in
    941938  let res ≝
    942939    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
    943940     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
    944941    foldi … (translate_stmt globals … lenv) (f_graph def) res.
    945 [ @graph_add_lookup @graph_add
    946 | @graph_add ]
     942[ @graph_add_lookup ] @graph_add
    947943qed.
    948944
  • src/joint/Joint_paolo.ma

    r1643 r1644  
    7272  | extension: ext_instruction p → joint_instruction p globals.
    7373
    74 (* Paolo: to be moved elsewhere *)
     74coercion extension_to_instruction :
     75  ∀p,globals.∀c : ext_instruction p.joint_instruction p globals ≝
     76  extension
     77  on _c : ext_instruction ? to joint_instruction ??.
    7578
    7679notation "r ← a1 .op. a2" with precedence 50 for
     
    123126  | extension_fin : ext_fin_instruction p → joint_statement p globals.
    124127
     128coercion extension_fin_to_statement :
     129  ∀p : stmt_params.∀globals.∀c : ext_fin_instruction p.joint_statement p globals ≝
     130  extension_fin
     131  on _c : ext_fin_instruction ? to joint_statement ??.
     132
    125133record params : Type[1] ≝
    126134 { stmt_pars :> stmt_params
     
    147155
    148156definition lin_params_to_params ≝
    149   λlp : lin_params.let stmt_pars ≝ (mk_stmt_params lp unit (λ_.λ_.True)) in
     157  λlp : lin_params.
    150158     mk_params
    151       stmt_pars
    152     (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement stmt_pars globals)))
     159      (mk_stmt_params lp unit (λ_.λ_.True))
     160    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    153161    (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
    154162        (λl_stmt. \fst l_stmt = Some ? lbl) code)
     
    165173   (all languages but LIN) *)
    166174definition graph_params_to_params ≝
    167   λgp : graph_params.let stmt_pars ≝ mk_stmt_params gp label (λP.P) in
     175  λgp : graph_params.
    168176     mk_params
    169       stmt_pars
    170     (* codeT ≝ *)(λglobals.graph (joint_statement stmt_pars globals))
     177      (mk_stmt_params gp label (λP.P))
     178    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    171179    (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
    172180    (* forall_statements ≝ *)(λglobals,P,code.
Note: See TracChangeset for help on using the changeset viewer.