cakeml/pancake/pan_to_targetScript.sml at master · CakeML/cakeml · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
(*
  Compiler from Pancake to machine code
*)
Theory pan_to_target
Libs
  preamble
Ancestors
  mllist pan_to_word backend word_depth word_to_word

Definition exports_def:
  (exports(Function fi::ds) =
   if fi.export then fi.name::exports ds
   else exports ds) ∧
  exports (_::ds) = exports ds ∧
  exports [] = []
End

Definition compile_prog_def:
  compile_prog asm_conf c prog =
    (* Ensure either user-written main or new main that does nothing is first in func list *)
    let prog1:'a decl list = case SPLITP (λx. case x of
                                   Function fi => fi.name = «main»
                                 | Decl _ _ _ => F) prog of
                  ([],ys) => ys
                | (xs,[]) => Function
                                <| name := «main»
                                 ; inline := F
                                 ; export := F
                                 ; params := []
                                 ; body := Return (Const 0w)
                                 ; return := One
                                |>
                                ::xs
                | (xs,y::ys) => y::xs ++ ys in
    (* Compiler passes *)
    let prog2 = pan_to_word$compile_prog asm_conf.ISA prog1 in
    let (col,prog3) = word_to_word$compile c.word_to_word_conf asm_conf prog2 in
    let c = c with
            word_to_word_conf updated_by (λc. c with col_oracle := col) in
    (* Add user functions to name mapping *)
    let names = fromAList (ZIP (sort $< (MAP FST prog2), (* func numbers *)
                                «generated_main»::
                                MAP FST (functions prog1) (* func names *)
                          )) : mlstring$mlstring num_map in
    (* Add stubs to name mapping *)
    let names = sptree$union (sptree$fromAList $ (word_to_stack$stub_names () ++
      stack_alloc$stub_names () ++ stack_remove$stub_names ())) names in
    (* Add exported functions to  *)
    let c = c with exported := exports prog in
      from_word asm_conf c names prog3
End

(*  TODO: evaluate max_depth ... (full_call_graph dest (fromAList prog))  *)

Theorem compile_prog_eq:
  compile_prog asm_conf c prog =
    (* Ensure either user-written main or new main that does nothing is first in func list *)
    let prog1:'a decl list = case SPLITP (λx. case x of
                                   Function fi => fi.name = «main»
                                 | Decl _ _ _ => F) prog of
                  ([],ys) => ys
                | (xs,[]) => Function
                                <| name := «main»
                                 ; inline := F
                                 ; export := F
                                 ; params := []
                                 ; body := Return (Const 0w)
                                 ; return := One
                                |>
                                ::xs
                | (xs,y::ys) => y::xs ++ ys in
    (* Compiler passes *)
    let prog2 = pan_to_word$compile_prog asm_conf.ISA prog1 in
    (* Add user functions to name mapping *)
    let names = fromAList (ZIP (sort $< (MAP FST prog2), (* func numbers *)
                                «generated_main»::
                                MAP FST (functions prog1) (* func names *)
                          )) : mlstring$mlstring num_map in
    (* Add stubs to name mapping *)
    let names = sptree$union (sptree$fromAList $ (word_to_stack$stub_names () ++
                stack_alloc$stub_names () ++ stack_remove$stub_names ())) names in
    let c = c with exported := exports prog in
      from_word_0 asm_conf c names prog2
Proof
  rewrite_tac [compile_prog_def,LET_THM]
  \\ AP_THM_TAC \\ gvs [FUN_EQ_THM] \\ rw []
  \\ pairarg_tac \\ gvs[from_word_0_def]
QED