Cubicle 1.1.2 documentation and source : Ptree.psystem_of

let psystem_of_decls ~pglobals ~pconsts ~parrays ~ptype_defs pdecls =
  let inits, pinvs, punsafe, ptrans =
    List.fold_left (fun (inits, invs, unsafes, trans) -> function
        | PInit i -> i :: inits, invs, unsafes, trans
        | PInv i -> inits, i :: invs, unsafes, trans
        | PUnsafe u -> inits, invs, u :: unsafes, trans
        | PTrans t -> inits, invs, unsafes, t :: trans
        | PFun -> inits, invs, unsafes, trans
      ) ([],[],[],[]) pdecls
  in
  let pinit = match inits with
    | [i] -> i
    | [] -> failwith "No inititial formula."
    | _::_ -> failwith "Only one initital formula alowed."
  in
  { pglobals;
    pconsts;
    parrays;
    ptype_defs;
    pinit;
    pinvs;
    punsafe;
    ptrans }