Changeset 2946 for src/LTL/LTL.ma


Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (8 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/LTL/LTL.ma

    r2286 r2946  
    2727
    2828definition ltl_program ≝ joint_program LTL.
     29unification hint 0 ≔ ⊢ ltl_program ≡ joint_program LTL.
    2930
    3031coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝
     
    3233coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝
    3334  hdw_argument_from_reg on _r : Register to snd_arg LTL.
     35
     36definition LTL_premain : ∀p : ltl_program.joint_closed_internal_function LTL (prog_var_names ?? p) ≝
     37λp.
     38let l1 : label ≝ an_identifier … one in
     39let l2 : label ≝ an_identifier … (p0 one) in
     40let l3 : label ≝ an_identifier … (p1 one) in
     41let res ≝
     42  mk_joint_internal_function LTL (prog_var_names … p)
     43  (mk_universe … (p0 (p0 one)))
     44  (mk_universe … one)
     45  it it 0 0 (empty_map …) l1 in
     46(* todo: args for main? *)
     47let res ≝ add_graph … l1
     48  (sequential … (COST_LABEL … (init_cost_label … p)) l2)
     49  res in
     50let res ≝ add_graph … l2
     51  (sequential … (CALL LTL ? (inl … (prog_main … p)) 4 it) l3)
     52  res in
     53let res ≝ add_graph … l3
     54  (GOTO ? l3)
     55  res in
     56res.
     57%
     58[ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct
     59  %
     60  [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
     61  |2: %
     62  |4,6: % whd in ⊢ (??%%→?); #EQ destruct
     63  ]
     64| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
     65| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
     66| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
     67| %{l2} %{(init_cost_label … p)} %
     68]
     69qed.
Note: See TracChangeset for help on using the changeset viewer.