source: src/RTLabs/RTLabs_syntax.ma @ 2689

Last change on this file since 2689 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 3.8 KB
RevLine 
[639]1include "basics/logic.ma".
2
[747]3include "common/AST.ma".
[720]4include "common/CostLabel.ma".
[702]5include "common/FrontEndOps.ma".
6include "common/Registers.ma".
[639]7
[702]8include "ASM/Vector.ma".
9include "common/Graphs.ma".
[639]10
11inductive statement : Type[0] ≝
12| St_skip : label → statement
13| St_cost : costlabel → label → statement
[1878]14| St_const : ∀t. register → constant t → label → statement
15| St_op1 : ∀t',t. unary_operation t t' → register → register → label → statement (* destination source *)
16| St_op2 : ∀t',t1,t2. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *)
[1872]17| St_load : typ → register → register → label → statement
18| St_store : typ → register → register → label → statement
[816]19| St_call_id : ident → list register → option register → label → statement
20| St_call_ptr : register → list register → option register → label → statement
[1680]21(* We're not using these just now, and they'd make the Traces.ma proofs more difficult.
[816]22| St_tailcall_id : ident → list register → statement
23| St_tailcall_ptr : register → list register → statement
[1680]24*)
[888]25| St_cond : register → label → label → statement
[765]26| St_return : statement
[639]27.
28
[1626]29definition env_has : list (register × typ) → register → typ → Prop ≝
30λl,r,t. Exists ? (λx. 〈r,t〉 = x) l.
31
32definition statement_typed : list (register × typ) → statement → Prop ≝
33λe,s. match s with
[1878]34[ St_const t r _ _ ⇒ env_has e r t
35| St_op1 t' t _ r' r _ ⇒ env_has e r' t' ∧ env_has e r t
36| St_op2 t' t1 t2 _ r' r1 r2 _ ⇒ env_has e r1 t1 ∧ env_has e r2 t2 ∧ env_has e r' t'
[2287]37| St_load t' addr dst _ ⇒ env_has e dst t' ∧ env_has e addr ASTptr
38| St_store t' addr src _ ⇒ env_has e src t' ∧ env_has e addr ASTptr
[2292]39| St_call_id id args dst _ ⇒ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True])
40| St_call_ptr fnptr args dst _ ⇒ env_has e fnptr ASTptr ∧ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True])
41| St_cond r _ _ ⇒ ∃t. env_has e r t
[1626]42| _ ⇒ True
43].
44
[1316]45definition labels_P : (label → Prop) → statement → Prop ≝
46λP,s. match s with
47[ St_skip l ⇒ P l
48| St_cost _ l ⇒ P l
[1878]49| St_const _ _ _ l ⇒ P l
[1369]50| St_op1 _ _ _ _ _ l ⇒ P l
[1872]51| St_op2 _ _ _ _ _ _ _ l ⇒ P l
[1316]52| St_load _ _ _ l ⇒ P l
53| St_store _ _ _ l ⇒ P l
54| St_call_id _ _ _ l ⇒ P l
55| St_call_ptr _ _ _ l ⇒ P l
[1680]56(*
[1316]57| St_tailcall_id _ _ ⇒ True
58| St_tailcall_ptr _ _ ⇒ True
[1680]59*)
[1316]60| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
61| St_return ⇒ True
62].
63
64lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
65#P #Q #H * /3/
66#r #l #l' * /3/
67qed.
68
69definition labels_present : graph statement → statement → Prop ≝
70λg,s. labels_P (present ?? g) s.
71
[1626]72definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝
73λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n.
74
[1316]75definition graph_closed : graph statement → Prop ≝
[1626]76  λg. forall_nodes ? (labels_present g) g.
77definition graph_typed : list (register × typ) → graph statement → Prop ≝
78  λe. forall_nodes ? (statement_typed e).
[1316]79
[639]80record internal_function : Type[0] ≝
[738]81{ f_labgen    : universe LabelTag
82; f_reggen    : universe RegisterTag
[887]83; f_result    : option (register × typ)
84; f_params    : list (register × typ)
85; f_locals    : list (register × typ)
[639]86; f_stacksize : nat
87; f_graph     : graph statement
[1316]88; f_closed    : graph_closed f_graph
[1626]89; f_typed     : graph_typed (f_locals @ f_params) f_graph
[1316]90; f_entry     : Σl:label. present ?? f_graph l
91; f_exit      : Σl:label. present ?? f_graph l
[639]92}.
93
[764]94(* Note that the global variables will be initialised by the code in main
[1139]95   by this stage, so the only initialisation data is the amount of space to
96   allocate. *)
[639]97
[1675]98definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
99
100
101
102
Note: See TracBrowser for help on using the repository browser.