Project

General

Profile

« Previous | Next » 

Revision 7ee5f69e

Added by LĂ©lio Brun 9 months ago

corrections on loggers + spec in AST

View differences:

src/machine_code_common.ml
99 99

  
100 100
let pp_machine fmt m =
101 101
  Format.fprintf fmt
102
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ const    : %a@ step     :@   @[<v 2>%a@]@ @  spec : @[%t@]@  annot : @[%a@]@]@ "
102
    "@[<v 2>machine %s@ \
103
     mem      : %a@ \
104
     instances: %a@ \
105
     init     : %a@ \
106
     const    : %a@ \
107
     step     :@   \
108
     @[<v 2>%a@]@ \
109
     spec     : @[%t@]@ \
110
     annot    : @[%a@]@]@ "
103 111
    m.mname.node_id
104 112
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
105 113
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
106 114
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
107 115
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
108 116
    (pp_step m) m.mstep
109
    (fun fmt -> match m.mspec with | None -> ()
110
                                   | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
111
                                   | Some (Contract spec) -> Printers.pp_spec fmt spec)
117
    (fun fmt -> match m.mspec.mnode_spec with
118
       | None -> ()
119
       | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
120
       | Some (Contract spec) -> Printers.pp_spec fmt spec)
112 121
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
113 122

  
114 123
let pp_machines fmt ml =
......
185 194
			[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
186 195
      step_asserts = [];
187 196
    };
188
    mspec = None;
197
    mspec = { mnode_spec = None; mtransitions = [] };
189 198
    mannot = [];
190 199
    msch = None
191 200
  }
......
226 235
      step_instrs = [];
227 236
      step_asserts = [];
228 237
    };
229
    mspec = None;
238
    mspec = { mnode_spec = None; mtransitions = [] };
230 239
    mannot = [];
231 240
    msch = None
232 241
  }

Also available in: Unified diff