include "RTLabs/RTLabs_semantics.ma".

let rec n_idents (n:nat) (tag:identifierTag) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
match n with
[ O ⇒ 〈[[ ]], g〉
| S m ⇒ let 〈ls, g'〉 ≝ n_idents m tag g in
        let 〈l, g''〉 ≝ fresh ? g' in
        〈l:::ls, g''〉
].

definition pre_register ≝ nat.

record pre_internal_function : Type[0] ≝
{ pf_result    : option (pre_register × typ)
; pf_params    : list (pre_register × typ)
; pf_locals    : list (pre_register × typ)
; pf_stacksize : nat
; pf_graph     : list (nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement))
; pf_entry     : nat
; pf_exit      : nat
}.

definition make_register : 
  (pre_register → option (register×typ)) → pre_register → typ → universe RegisterTag →
  (nat → option (register×typ)) × (universe RegisterTag) × register ≝
λm,reg,ty,g.
  match m reg with
  [ Some r' ⇒ 〈〈m,g〉,\fst r'〉
  | None ⇒ let 〈r',g'〉 ≝ fresh ? g in
             〈〈λn. if eqb reg n then Some ? 〈r',ty〉 else m n,g'〉,r'〉
  ]
.

definition make_registers_list :
  (nat → option (register×typ)) → list (pre_register × typ) → universe RegisterTag →
    (nat → option (register×typ)) × (universe RegisterTag) × (list (register×typ)) ≝
λm,lrs,g.
foldr ?? (λrst,acc. let 〈acc',l〉 ≝ acc in
                    let 〈rs,ty〉 ≝ rst in
                    let 〈m,g〉 ≝ acc' in 
                    let 〈mg,rs'〉 ≝ make_register m rs ty g in
                      〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs.

(* Doesn't check for identifier overflow, but don't really need to care here. *)
definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
λpre_f.
  let rgen0 ≝ new_universe RegisterTag in
  let 〈rmapgen1, result〉 ≝ match pf_result pre_f with
                           [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉
                           | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) (\snd rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
                           ] in
  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
  let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in
  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
  let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in
  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in
  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
  let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in
  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
  do graph ← foldr ?? (λp:nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement).λg0.
                         do g ← g0;
                         let 〈l,s〉 ≝ p in
                         do l' ← get_label l;
                         do s' ← s rmap get_label;
                         OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
  do entry ← get_label (pf_entry pre_f);
  do exit ← get_label (pf_exit pre_f);
  (* We could figure out that entry and exit are in the graph, but why bother
     for some testing code? *)
  match lookup … graph entry return λx. (x ≠ None ? → ?) → ? with
  [ None ⇒ λ_. Error ? (msg MissingLabel)
  | Some _ ⇒
      match lookup … graph exit return λx. (? → x ≠ None ? → ?) → ? with
      [ None ⇒ λ_. Error ? (msg MissingLabel)
      | Some _ ⇒ λx. x ??
      ]
  ] (λp,q. OK ? (Internal ? (mk_internal_function
         gen
         rgen3
         result
         params
         locals
         (pf_stacksize pre_f)
         graph
         ?
         ?
         (mk_Sig ?? entry p)
         (mk_Sig ?? exit q)
         )))
   .
[ 1,2: % #E destruct (E)
| 3,4: cases daemon
]
qed.

definition make_reg_list : (nat → res (register×typ)) → list pre_register → res (list register) ≝
λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do 〈r,t〉 ← m p; OK ? (r::rs)) (OK ? [ ]) ps.

(* XXX move somewhere sensible *)
let rec mmap_vec (A:Type[0]) (B:Type[0]) (f:A → res B) (n:nat) (v:Vector A n) on v : res (Vector B n) ≝
match v with
[ VEmpty ⇒ OK ? (VEmpty …)
| VCons m hd tl ⇒ do hd' ← f hd;
                  do tl' ← mmap_vec A B f m tl;
                  OK ? (hd':::tl')
].

definition make_opt_reg : (pre_register → res (register×typ)) → option pre_register → res (option register) ≝
λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do 〈r',t'〉 ← m r; OK ? (Some ? r') ].

inductive pre_op1 : Type[0] ≝
  | POcastint: intsize → signedness → intsize → pre_op1
  | POnegint:  pre_op1
  | POnotbool: pre_op1
  | POnotint:  pre_op1
  | POid: pre_op1
  | POptrofint: pre_op1
  | POintofptr: pre_op1
.

(* duplicated from Clight/toCminor.ma. *)
definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
qed.

definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
* [ #sz1 #sg1 | #r1 | #sz1 ]
* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
| *; #P #p @(region_should_eq r1 ?? p)
| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
] qed.

definition is_bool_src : ∀ty. res (boolsrc ty) ≝
λty. match ty return λt.res (boolsrc t) with [ ASTint _ _ ⇒ OK ? I | ASTptr _ ⇒ OK ? I | _ ⇒ Error ? (msg TypeMismatch) ].

definition make_op1 : ∀t,t'. pre_op1 → res (unary_operation t' t) ≝
λt,t',op.
  match op with
  [ POcastint sz sg sz' ⇒
      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Ocastint sz sg sz' sg2);
               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
      | _ ⇒ Error ? (msg TypeMismatch) ]
  | POnegint ⇒
      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onegint sz2 sg2);
               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
      | _ ⇒ Error ? (msg TypeMismatch) ]
  | POnotbool ⇒
      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
        do p ← is_bool_src t';
               OK ? (Onotbool t' sz2 sg2 p)
      | _ ⇒ Error ? (msg TypeMismatch) ]
  | POnotint ⇒
      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onotint sz2 sg2);
               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
      | _ ⇒ Error ? (msg TypeMismatch) ]
  | POid ⇒ typ_should_eq t t' (λt'. unary_operation t' t) (Oid t)
  | POptrofint ⇒
      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
      match t return λt. res (unary_operation ? t) with [ ASTptr r1 ⇒
        OK ? (Optrofint …)
      | _ ⇒ Error ? (msg TypeMismatch) ]
      | _ ⇒ Error ? (msg TypeMismatch) ]
  | POintofptr ⇒
      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
      match t' return λt'. res (unary_operation t' ?) with [ ASTptr r1 ⇒
        OK ? (Ointofptr …)
      | _ ⇒ Error ? (msg TypeMismatch) ]
      | _ ⇒ Error ? (msg TypeMismatch) ]
  ].

let rec make_St_skip l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_skip l').
let rec make_St_cost cl l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
let rec make_St_const rs cst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈rs',ty'〉 ← r rs; do l' ← f l; OK ? (St_const rs' cst l').
let rec make_St_op1 op dst src l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈dst',dty〉 ← r dst; do 〈src',sty〉 ← r src; do l' ← f l; do op ← make_op1 dty sty op; OK ? (St_op1 dty sty op dst' src' l').
let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈dst',dty〉 ← r dst; do 〈src1',sty1〉 ← r src1; do 〈src2',sty2〉 ← r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
let rec make_St_load chunk addr dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈addr',aty〉 ← r addr; do 〈dst',dty〉 ← r dst; do l' ← f l; OK ? (St_load chunk addr' dst' l').
let rec make_St_store chunk addr src l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈addr',aty〉 ← r addr; do 〈src',sty〉 ← r src; do l' ← f l; OK ? (St_store chunk addr' src' l').
let rec make_St_call_id id args dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l').
let rec make_St_call_ptr frs args dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈frs',fty〉 ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l').
let rec make_St_tailcall_id id args ≝ λr:nat → res (register×typ).λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args').
let rec make_St_tailcall_ptr frs args ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈frs',fty〉 ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args').
let rec make_St_cond src ltrue lfalse ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈src',sty〉 ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond src' ltrue' lfalse').
let rec make_St_jumptable rs ls ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈rs',rty〉 ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
definition make_St_return ≝ λr:nat → res (register×typ).λf:nat → res label. OK statement St_return.