clean version of records parser w/o records

ast.mli

@@ -50,11 +50,11 @@ type transition_info = {
   tr_name : Hstring.t; (** name of the transition *)
   tr_args : Variable.t list;
   (** existentially quantified parameters of the transision *)
-  tr_reqs : SAtom.t; (** guard *)
-  tr_ureq : (Variable.t * dnf) list;
+  tr_reqs : SAtom.t * loc; (** guard *)
+  tr_ureq : (Variable.t * dnf * loc) list;
   (** global condition of the guard, i.e. universally quantified DNF *)
   tr_lets : (Hstring.t * Term.t) list;
-  tr_assigns : (Hstring.t * glob_update) list; (** updates of global variables *)
+  tr_assigns : (Hstring.t * glob_update * loc) list; (** updates of global variables *)
   tr_upds : update list; (** updates of arrays *)
   tr_nondets : Hstring.t list;
   (** non deterministic updates (only for global variables) *)
@@ -72,11 +72,14 @@ type transition = {
   tr_reset : unit -> unit;
 }
 
+type type_defs =
+  | Constructors of (loc * type_constructors)
+
 type system = {
   globals : (loc * Hstring.t * Smt.Type.t) list;
   consts : (loc * Hstring.t * Smt.Type.t) list;
-  arrays : (loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list;
-  type_defs : (loc * type_constructors) list;
+  arrays : (loc * Hstring.t * (Hstring.t list * Hstring.t)) list;
+  type_defs : type_defs list;
   init : loc * Variable.t list * dnf;
   invs : (loc * Variable.t list * SAtom.t) list;
   unsafe : (loc * Variable.t list * SAtom.t) list;  

common/hstring.ml

@@ -40,6 +40,11 @@ module HS = struct
     | [] -> raise Not_found
     | (y, v) :: l -> if equal x y then v else list_assoc x l
 
+  let rec list_assoc_triplet x = function
+    | [] -> raise Not_found
+    | (y, v, k) :: l -> if equal x y then v,k else list_assoc_triplet x l
+
+
   let rec list_assoc_inv x = function
     | [] -> raise Not_found
     | (y, v) :: l -> if equal x v then y else list_assoc_inv x l

common/hstring.mli

@@ -53,6 +53,11 @@ val list_assoc : t -> (t * 'a) list -> 'a
     pairs [l].
     @raise Not_found if there is no value associated with [x] in the list [l].*)
 
+val list_assoc_triplet: t -> (t * 'a * 'b) list -> 'a * 'b
+(** [list_assoc_triplet x l] returns the element associated with [x] in the list of
+    triplets [l].
+    @raise Not_found if there is no value associated with [x] in the list [l].*)
+
 val list_assoc_inv : t -> ('a * t) list -> 'a
 (** [list_assoc_inv x l] returns the first element which is associated to [x]
     in the list of pairs [l].

enumerative.ml

@@ -752,7 +752,7 @@ let swts_to_stites env at sigma swts =
 
 let assigns_to_actions env sigma acc tr_assigns =
   List.fold_left 
-    (fun acc (h, gu) ->
+    (fun acc (h, gu, _) ->
       let nt = Elem (h, Glob) in
       match gu with
       | UTerm t ->
@@ -935,7 +935,7 @@ let ordered_fst_subst = function
 
 let transitions_to_func_aux procs env reduce acc 
                             { tr_info = { tr_args = tr_args; 
-		                          tr_reqs = reqs; 
+		                          tr_reqs = (reqs,_); 
 		                          tr_name = name;
 		                          tr_ureq = ureqs;
 		                          tr_assigns = assigns; 

forward.ml

@@ -469,7 +469,7 @@ let swts_to_ites at swts sigma =
 
 let apply_assigns assigns sigma =
   List.fold_left 
-    (fun (nsa, terms) (h, gu) ->
+    (fun (nsa, terms) (h, gu, _) ->
       let nt = Elem (h, Glob) in
       let sa = 
         match gu with
@@ -510,7 +510,7 @@ let preserve_terms upd_terms sa =
 
 let uguard_dnf sigma args tr_args = function
   | [] -> []
-  | [j, dnf] ->
+  | [j, dnf, _] ->
       let uargs = List.filter (fun a -> not (H.list_mem a tr_args)) args in
       List.map (fun i ->
 	List.map (fun sa -> SAtom.subst ((j, i)::sigma) sa) dnf) uargs
@@ -523,7 +523,7 @@ let possible_init args init reqs =
     (* try Prover.check_guard args init reqs; true *)
     (* with Smt.Unsat _ -> false *)
 
-let possible_guard args all_args tr_args sigma init reqs ureqs =
+let possible_guard args all_args tr_args sigma init (reqs,_) ureqs =
   let reqs = SAtom.subst sigma reqs in
   possible_init args init reqs &&
     let t_args_ef = 
@@ -793,7 +793,7 @@ let mkinits procs ({t_init = ia, l_init}) =
 
 
 let instance_of_transition { tr_args = tr_args; 
-		             tr_reqs = reqs; 
+		             tr_reqs = (reqs,_); 
 		             tr_name = name;
 		             tr_ureq = ureqs;
 		             tr_assigns = assigns; 

forward.mli

@@ -78,4 +78,4 @@ val conflicting_from_trace : t_system -> trace -> SAtom.t list
 val uguard_dnf : 
   Variable.subst ->
   Variable.t list -> Variable.t list ->
-  (Variable.t * SAtom.t list) list -> SAtom.t list list
+  (Variable.t * SAtom.t list * 'a) list -> SAtom.t list list

murphi.ml

@@ -466,7 +466,7 @@ let print_swts ot fmt swts =
   end
 
 
-let print_assign fmt (v, up) =
+let print_assign fmt (v, up, _) =
   let tv = Elem (v, Glob) in
   match up with
   | UTerm t ->
@@ -523,7 +523,7 @@ let rec print_is_other fmt (v, args) = match args with
       print_is_other (v, ra)
 
 
-let print_forall_other args fmt (v, dnf) =
+let print_forall_other args fmt (v, dnf,_) =
   let close_forall = print_forall fmt v in
   print_is_other fmt (v, args);
   fprintf fmt "(%a)" print_dnf dnf;
@@ -537,10 +537,10 @@ let rec print_ureqs args fmt = function
     fprintf fmt "%a@ &@ %a" (print_forall_other args) u (print_ureqs args) ru
 
 
-let print_guard fmt { tr_args; tr_reqs; tr_ureq } =
+let print_guard fmt { tr_args; tr_reqs = (reqs,_); tr_ureq } =
   (* fprintf fmt "  @[<v>"; *)
-  print_satom fmt tr_reqs;
-  if tr_ureq <> [] && not(SAtom.is_empty tr_reqs) then fprintf fmt " &@ ";
+  print_satom fmt reqs;
+  if tr_ureq <> [] && not(SAtom.is_empty reqs) then fprintf fmt " &@ ";
   print_ureqs tr_args fmt tr_ureq
   (* fprintf fmt "@]\n" *)
 
@@ -765,9 +765,9 @@ let ordered_procs_globu = function
 let ordered_procs_up u = ordered_procs_swts u.up_swts
 
 let ordered_procs_trans { tr_info = t } =
-  ordered_procs_satom t.tr_reqs
-  || List.exists (fun (_, dnf) -> ordered_procs_dnf dnf) t.tr_ureq
-  || List.exists (fun (_, gu) -> ordered_procs_globu gu) t.tr_assigns
+  ordered_procs_satom (fst t.tr_reqs)
+  || List.exists (fun (_, dnf, _) -> ordered_procs_dnf dnf) t.tr_ureq
+  || List.exists (fun (_, gu, _) -> ordered_procs_globu gu) t.tr_assigns
   || List.exists ordered_procs_up t.tr_upds
 
 let ordered_procs_sys s =