Changeset 1644 for src/joint


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

minor changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.