CristalCaveGem » LustreC

        (opt_machine_spec, guarantees, 4)

    | _ -> None, [], 0

          List.map (build_pp_var_decl_local (Some (true, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),

  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees, past_size), machine)) =

  let pp_invariant_name fmt = fprintf fmt "invariant"

  let pp_name_generic fmt = fprintf fmt "name"

  let pp_type_generic fmt = fprintf fmt "string"

  (** Printing function for basic assignement [var := value].

      @param fmt the formater to print on

      @param var_name the name of the variable

      @param value the value to be assigned

   **)

  let pp_local_eq env fmt var value =

    fprintf fmt "%t = %a"

      (pp_var_name var)

      (pp_value env) value

  (** Printing function for basic assignement [var := value].

      @param fmt the formater to print on

      @param var_name the name of the variable

      @param value the value to be assigned

   **)

  let pp_state_eq env fmt var value =

    fprintf fmt "%t = %a"

      (pp_access (pp_state_name_predicate suffixNew) (pp_var_name var))

      (pp_value env) value

  (** Printing function for instruction. See

      {!type:Machine_code_types.instr_t} for more details on

      machine types.

      @param typed_submachines list of all typed machine instances of this machine

      @param machine the current machine

      @param fmt the formater to print on

      @param instr the instruction to print

   **)

  let pp_machine_instr typed_submachines env (pps, assigned) instr =

    let pp_state suffix i fmt = fprintf fmt "%t.%s" (pp_state_name_predicate suffix) i in

    let fresh x l = not (List.exists (fun y -> String.equal x.var_id y.var_id) l) in

    let pp, newvals =

      match get_instr_desc instr with

        (* no reset *)

        | MNoReset _ -> ((fun fmt -> ()), [])

        (* reset  *)

        | MReset i when List.mem_assoc i typed_submachines ->

            let (substitution, submachine) = get_instance i typed_submachines in

            let pp_package = pp_package_name_with_polymorphic substitution submachine in

            let args = if is_machine_statefull submachine then [[pp_state suffixNew i]] else [] in

            ((fun fmt -> pp_call fmt (pp_package_access (pp_package, pp_init_name), args)),

            [])

        | MLocalAssign (ident, value) ->

            assert(fresh ident assigned);

            ((fun fmt -> pp_local_eq env fmt ident value),

            [ident])

        | MStateAssign (ident, value) ->

            assert(fresh ident assigned);

            ((fun fmt -> pp_state_eq env fmt ident value),

            [ident])

        | MStep ([i0], i, vl) when is_builtin_fun i ->

            assert(fresh i0 assigned);

            let value = mk_val (Fun (i, vl)) i0.var_type in

            ((fun fmt -> (if List.mem_assoc i0.var_id env then

              pp_state_eq env fmt i0 value

            else

              pp_local_eq env fmt i0 value)),

            [i0])

        | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->

            assert(List.for_all (fun x -> fresh x assigned) il);

            let (substitution, submachine) = get_instance i typed_submachines in

            let pp_package = pp_package_name_with_polymorphic substitution submachine in

            let input = List.map (fun x fmt -> pp_value env fmt x) vl in

            let output = List.map pp_var_name il in

            let args =

              (if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [])

                @(if input!=[] then [input] else [])

                @(if output!=[] then [output] else [])

            in

            ((fun fmt -> fprintf fmt "(%a)" pp_call (pp_package_access (pp_package, pp_transition_name), args)),

            il)

        | MComment s -> ((fun fmt -> ()), [])

        | _ -> assert false

      in

      (pp::pps, newvals@assigned)

let pp_predicate_special pp_name args fmt content_opt =

  let rec quantify pp_content = function

    | [] -> pp_content

    | (pp_var, pp_type)::q -> fun fmt ->

      fprintf fmt "for some %t in %t => (@,  @[<v>%t@])" pp_var pp_type (quantify pp_content q)

  in

  let content = match content_opt with

    | Some (locals, booleans) -> Some (quantify (fun fmt -> Utils.fprintf_list ~sep:"@,and " (fun fmt pp->pp fmt) fmt booleans) locals)

    | None -> None

  in

  pp_predicate pp_name args fmt content

  let pp_init_predicate prototype typed_submachines fmt (opt_spec_machine, m) =

    let env = [] in

    let instrs = push_if_in_expr m.minit in

    let content = fst (List.fold_left (pp_machine_instr typed_submachines env) ([], []) instrs) in

    pp_predicate_special pp_init_name ([[new_state]]) fmt (if prototype then None else Some ([], content))

  let pp_transition_predicate prototype typed_submachines fmt (opt_spec_machine, m) =

    let env = List.map (fun x -> x.var_id, pp_state_name_predicate suffixOld) m.mmemory in

    let instrs = push_if_in_expr m.mstep.step_instrs in

    let content = fst (List.fold_left (pp_machine_instr typed_submachines env) ([], []) instrs) in

    let locals = List.map (fun x-> (pp_var_name x, fun fmt -> pp_var_type fmt x)) m.mstep.step_locals in

    pp_predicate_special pp_transition_name ([[old_state; new_state]]@inputs@outputs) fmt (if prototype then None else Some (locals, content))

  let build_pp_past mode with_st i = (mode, pp_past_name (i+1), pp_state_type , with_st)

  let pp_invariant_predicate prototype typed_submachines fmt (past_size, opt_spec_machine, m) =

    let pp_state nbr = if nbr = 0 then pp_state_name else pp_past_name nbr in

    if past_size < 1 then fprintf fmt "" else

    begin

      let pp_var x fmt =

          pp_clean_ada_identifier fmt x

      in

      let input = List.map pp_var_name m.mstep.step_inputs in

      let output = List.map pp_var_name m.mstep.step_outputs in

      let args =

        [[pp_old pp_state_name;pp_state_name]]

          @(if input!=[] then [input] else [])

          @(if output!=[] then [output] else [])

      in

      let transition fmt = pp_call fmt (pp_transition_name, args) in

      let pp_append_nbr pp nbr fmt = fprintf fmt "%t_%i" pp nbr in

      let pp_transition nbr fmt =

        assert(is_machine_statefull m);

        let args =

          [[pp_past_name (nbr+1);pp_state nbr]]

            @(if input!=[] then [input] else [])

            @(if output!=[] then [output] else [])

        in

        pp_call fmt (pp_transition_name, args)

      in

      let build_chain nbr =

        assert (nbr > 0);

        pp_and (init pp_transition nbr)

      in

      let pp_init nbr fmt = pp_call fmt (pp_init_name, [[pp_state nbr]]) in

      let rec build_initial nbr = pp_and (match nbr with

        | 0 -> [pp_init 0]

        | i when i > 0 -> [pp_init i;build_chain i]

        | _ -> assert false)

      in

      let content = pp_or ((build_chain (past_size-1))::(init build_initial (past_size-1))) in

      fprintf fmt ";@,@,%a" (pp_predicate pp_invariant_name [init (build_pp_past AdaIn None) (past_size-1);[build_pp_state_decl AdaIn None]]) (if prototype then None else Some content)

    end

    let instanciations = ((pp_name_generic, pp_adastring pp_name))::(List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions) in

  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees, past_size), m)) =

      (*List.filter (fun (l, _) -> l != [])*) typed_machines_set in

      | Some m -> List.map (fun x-> pp_var_decl (build_pp_var_decl AdaNoMode (Some (true, [], [])) x)) m.mmemory

      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode (Some (true, [], []))) (m_spec.mmemory)

      let init fmt = pp_call fmt (pp_init_name, [[pp_state_name]]) in

      let contract = Some (false, [], [init]) in

      fprintf fmt "@,private@,@,%a%t%a;@,@,%a;@,@,%a%a%t%a"

      (*Declare the init predicate*)

      (pp_init_predicate false typed_submachines) (m_spec_opt, m)

      (*Declare the transition predicate*)

      (pp_transition_predicate false typed_submachines) (m_spec_opt, m)

      (*Declare the transition predicate*)

      (pp_invariant_predicate false typed_submachines) (past_size, m_spec_opt, m)

            let transition fmt = pp_call fmt (pp_transition_name, args) in

            let invariant fmt = pp_call fmt (pp_invariant_name, [init (fun i->pp_past_name (i+1)) (past_size-1);[pp_state_name]]) in

            if past_size > 0 then

              [invariant], [transition;invariant]

            else

              [], [transition]

          Some (false, pre_conditions, post_conditions)

      let pp_guarantee name = pp_var_decl (AdaNoMode, (fun fmt -> pp_clean_ada_identifier fmt name), pp_boolean_type , (Some (true, [], []))) in

      let pasts = List.map pp_var_decl (init (build_pp_past AdaNoMode (Some (true, [], []))) (past_size-1)) in

      let ghost_public = pasts@(List.map pp_guarantee guarantees) in

      fprintf fmt "@,%a%t%a%a%a@,@,%a;@,@,%a%a;%t"

        (*Declare the init predicate*)

        (pp_init_predicate true typed_submachines) (m_spec_opt, m)

        (*Declare the transition predicate*)

        (pp_transition_predicate true typed_submachines) (m_spec_opt, m)

        (*Declare the transition predicate*)

        (pp_invariant_predicate true typed_submachines) (past_size, m_spec_opt, m)

    let pp_generics = (pp_var_decl (AdaNoMode, pp_name_generic, pp_type_generic , None))::(List.map pp_poly_type polymorphic_types) in

  fprintf fmt "%t_inst%t%a"

type ada_with = (bool * (printer list) * (printer list)) option

  | Some (ghost, pres, posts) ->

      assert(ghost || (pres != []) || (posts != []));

        fprintf fmt " Ghost%t" (Utils.pp_final_char_if_non_empty ",@," contract)

      fprintf fmt " with%t%t"

let pp_predicate pp_name args fmt content_opt =

    | None -> AdaNoContent, Some (true, [], [])

type ada_with = (bool * (printer list) * (printer list)) option

val pp_predicate : printer -> (ada_var_decl list list) -> formatter -> (printer option) -> unit