Changeset 3042


Ignore:
Timestamp:
Mar 29, 2013, 6:27:21 PM (4 years ago)
Author:
sacerdot
Message:

Repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_printer.ma

    r2996 r3042  
    4747 ; print_Op1: Op1 → string
    4848 ; print_Op2: Op2 → string
    49  ; print_nat: nat → string }.
     49 ; print_nat: nat → string
     50 ; print_bitvector: ∀n. BitVector n → string }.
    5051
    5152record printing_params (string: Type[0]) (P: unserialized_params) : Type[0] ≝
     
    119120  | PUSH arg ⇒
    120121     print_list … pp [print_keyword … pp kwPUSH; print_acc_a_arg … pp arg]
    121   | ADDRESS i Hi arg1 arg2 ⇒
     122  | ADDRESS i Hi offset arg1 arg2 ⇒
    122123     print_list … pp
    123124      [print_keyword … pp kwADDRESS;
    124125       print_ident … pp i;
     126       print_bitvector … pp … offset;
    125127       print_dpl_reg … pp arg1;
    126128       print_dph_reg … pp arg2]
     
    289291
    290292definition print_joint_function:
    291  ∀p:params. ∀lines. ∀globals. ∀string. code_iteration_params string p lines globals → printing_params string p →
    292   joint_function p globals → list string ≝
    293  λp,lines,globals,string,cip,pp,f.
     293 ∀p:params. ∀lines. ∀globals. ∀functions. ∀string.
     294  code_iteration_params string p lines (globals@functions) → printing_params string p →
     295   joint_function p functions globals → list string ≝
     296 λp,lines,globals,functions,string,cip,pp,f.
    294297  match f with
    295298  [ Internal f ⇒ print_joint_internal_function … cip … pp f
     
    300303  printing_params string p →
    301304  ∀prog:joint_program p.
    302    code_iteration_params string p lines (map … (λx. \fst (\fst x)) (prog_vars ?? prog)) →
     305   code_iteration_params string p lines (prog_names … prog) →
    303306   list (ident × (list string)) ≝
    304307 λp,lines,string,pp,prog,cip.
Note: See TracChangeset for help on using the changeset viewer.