package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file printer_model_tools.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
open Location
open Ident
open Tools
open Model

(* -------------------------------------------------------------------------- *)

exception Anomaly of string

type error_desc =
  | UnsupportedTerm of string
  | UnsupportedValue of string
  | TODO of string
[@@deriving show {with_path = false}]

let emit_error (desc : error_desc) =
  let str = Format.asprintf "%a@." pp_error_desc desc in
  raise (Anomaly str)

(* -------------------------------------------------------------------------- *)

type env = {
  f: function__ option;
  update_preds: (ident * assignment_operator * mterm) list list;
  select_preds: mterm list;
  sum_preds: mterm list;
  removeif_preds: mterm list;
  consts: (ident * mterm) list;
}
[@@deriving show {with_path = false}]

let mk_env ?f ?(update_preds=[]) ?(select_preds=[]) ?(sum_preds=[]) ?(removeif_preds=[]) ?(consts=[]) () : env =
  { f; update_preds; select_preds; sum_preds; removeif_preds; consts }

let cmp_update l1 l2 = List.for_all2 (fun (i1, op1, v1) (i2, op2, v2) -> Model.cmp_ident i1 i2 && Model.cmp_assign_op op1 op2 && Model.cmp_mterm v1 v2) l1 l2

let compute_env model =
  let update_preds =
    List.fold_right (fun x accu ->
        match x.api_loc, x.node_item with
        | (OnlyExec | ExecFormula), APIAsset (Update (_, l)) ->
          if not (List.exists (cmp_update l) accu)
          then l::accu
          else accu
        | _ -> accu
      ) model.api_items []
  in
  let select_preds =
    List.fold_right (fun x accu ->
        match x.api_loc, x.node_item with
        | (OnlyExec | ExecFormula), APIAsset (Select (_, _, _, pred)) ->
          if not (List.exists (Model.cmp_mterm pred) accu)
          then pred::accu
          else accu
        | _ -> accu
      ) model.api_items []
  in
  let sum_preds =
    List.fold_right (fun x accu ->
        match x.api_loc, x.node_item with
        | (OnlyExec | ExecFormula), APIAsset (Sum (_, _, _, pred)) ->
          if not (List.exists (Model.cmp_mterm pred) accu)
          then pred::accu
          else accu
        | _ -> accu
      ) model.api_items []
  in
  let removeif_preds =
    List.fold_right (fun x accu ->
        match x.api_loc, x.node_item with
        | (OnlyExec | ExecFormula), APIAsset (RemoveIf (_, _, _, pred)) ->
          if not (List.exists (Model.cmp_mterm pred) accu)
          then pred::accu
          else accu
        | _ -> accu
      ) model.api_items []
  in
  let consts =
    List.fold_right (fun (x : decl_node) accu ->
        match x with
        | Dvar v when v.constant -> (unloc v.name, Option.get v.default)::accu
        | _ -> accu
      ) model.decls [] in
  mk_env ~update_preds:update_preds ~select_preds:select_preds ~sum_preds:sum_preds ~removeif_preds:removeif_preds ~consts:consts ()

(* -------------------------------------------------------------------------- *)

exception Found

let is_internal l (id : lident) : bool =
  try
    List.iter (fun (x : ident * mterm) -> if (String.equal (unloc id) (fst x)) then raise Found) l ;
    false
  with
  | Found -> true

let is_const (env : env) (id : lident) : bool = is_internal env.consts id

let get_const_dv (env : env) (id : lident) : mterm =
  List.assoc (unloc id) env.consts

let get_preds_index l e : int =
  match List.index_of (fun x -> Model.cmp_mterm x e) l with
  | -1 -> assert false
  | _ as i -> i

let get_preds_index_gen cmp l e : int =
  match List.index_of (fun x -> cmp x e) l with
  | -1 -> assert false
  | _ as i -> i