source: LTS/asm.ma

Last change on this file was 3574, checked in by piccolo, 4 years ago

assembly pass in place

File size: 2.7 KB
RevLine 
[3574]1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "Vm.ma".
16include "stack.ma".
17include "mono_stack.ma".
18
19(*status flag for conditionals*)
20definition asm_store_t ≝ mono_stack_store_t × bool.
21
22inductive asm_seq_i : Type[0] ≝
23| asm_seq : stack_seq → asm_seq_i
24| pop_cond : asm_seq_i
25| asm_pop_frame : asm_seq_i
26| asm_push_frame : asm_seq_i
27| asm_alloc_frame : ℕ → asm_seq_i.
28
29definition asm_eval_seq : asm_seq_i → asm_store_t → option asm_store_t ≝
30λi,s.match i with
31[ asm_seq x ⇒ ! y ← mono_stack_eval_seq x (\fst s);
32                return 〈y,(\snd s)〉
33| pop_cond ⇒ !〈val,y〉 ← mono_pop (\fst s);
34             return 〈y,eqb val 1〉
35| asm_pop_frame ⇒ ! y ← mono_stack_return_call (\fst s);
36                  return 〈y,(\snd s)〉
37| asm_push_frame ⇒  !〈exp_val,st1〉 ← mono_pop (\fst s);
38                    let new_fp ≝ (|(\fst st1)|) in
39                    let st2 ≝ mono_push st1 (\fst (\snd (\fst s))) in
40                    let st3 ≝ mono_push st2 O in
41                    let st4 ≝ mono_push st3 exp_val in
42                    return 〈 〈(\fst st4),〈new_fp,(\snd(\snd st4))〉〉,(\snd s)〉
43| asm_alloc_frame n ⇒ let new_frame ≝ list_n … O (pred (to_shift + n)) in
44                      return 〈〈new_frame @ (\fst (\fst s)),(\snd (\fst s))〉,(\snd s)〉
45].
46
47definition asm_eval_cond : asm_store_t → option bool ≝
48λs.return (\snd s).
49
50definition asm_assembler_params ≝ mk_assembler_params
51asm_seq_i unit False.
52
53definition asm_sem_params ≝ mk_sem_params asm_assembler_params asm_store_t asm_eval_seq
54(λ_.asm_eval_cond) ?.
55* qed.
56
57definition asm_instructions ≝ AssemblerInstr asm_assembler_params flat_labels.
58
59definition asm_program ≝ AssemblerProgram asm_assembler_params flat_labels.
60
61definition asm_state ≝ vm_state asm_assembler_params asm_sem_params.
Note: See TracBrowser for help on using the repository browser.