Changeset 2946 for src/LIN/LIN.ma


Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r2286 r2946  
    2727
    2828definition lin_program ≝ joint_program LIN.
     29unification hint 0 ≔ ⊢ lin_program ≡ joint_program LIN.
     30
     31definition LIN_premain : ∀p : lin_program.joint_closed_internal_function LIN (prog_var_names ?? p) ≝
     32λp.
     33let l3 : label ≝ an_identifier … (p1 one) in
     34let code ≝
     35  [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ;
     36   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 4 it) it〉 ;
     37   〈Some ? l3, GOTO ? l3〉 ] in
     38mk_joint_internal_function LIN (prog_var_names … p)
     39  (mk_universe … (p0 (p0 one)))
     40  (mk_universe … one)
     41  it it 0 0 code 0.
     42%
     43[ * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct
     44  % try @I
     45  [ %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
     46  |*: % whd in ⊢ (??%%→?); #EQ destruct
     47  ]
     48| * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
     49| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
     50| * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     51| %{it} %{(init_cost_label … p)} %
     52]
     53qed.
Note: See TracChangeset for help on using the changeset viewer.