Theory Closed_Checker

theory Closed_Checker
  imports
    SE_Graph
begin

unbundle IA_formula_notation

instantiation name :: showl
begin
fun showsl_name where
  "showsl_name (Name s) = showsl_lit (STR ''Name '') ∘ (showsl_lit s)"
| "showsl_name (UnName n) = showsl_lit (STR ''Name '') ∘ (showsl n)"
definition "showsl_list (xs :: name list) = default_showsl_list showsl xs"
instance ..
end

record ('p,'pv,'lv) abstract_state_mapping =
  pos :: 'p
  stack :: "('pv, 'lv) mapping"
  kb :: "'lv IA.formula"

definition Mapping_values where
  "Mapping_values m = (the ∘ Mapping.lookup m) ` Mapping.keys m"

fun asm_to_as where
  "asm_to_as ⦇pos = p, stack = s, kb = k⦈ = As p (Mapping.lookup s) k"

lemma asm_to_as_simps[simp]:
  "abstract_state.stack (asm_to_as x) = Mapping.lookup (abstract_state_mapping.stack x)"
  "abstract_state.kb (asm_to_as x) = abstract_state_mapping.kb x"
  "abstract_state.pos (asm_to_as x) = abstract_state_mapping.pos x"
  by (cases x, auto)+

fun update_asFun where
  "update_asFun as⇩1 as⇩2 n v⇩n φ =
   do {
    check (v⇩n ∉ Mapping_values (stack as⇩1)) (showsl STR ''update_asFun: vn not in symbolic vars'');
    check ((v⇩n, IA.IntT) ∉ vars_formula (kb as⇩1)) (showsl STR ''update_asFun: vn already in kb'');
    check (Mapping.lookup (stack as⇩2) n = Some v⇩n) (showsl STR ''update_asFun: vn not defined in as2'');
    check (∀x ∈ Mapping.keys (stack as⇩1). x ≠ n ⟶ Mapping.lookup (stack as⇩1) x =  Mapping.lookup (stack as⇩2) x)
          (showsl STR ''update_asFun: stack2 is not extensions of stack1'');
    check (Mapping.keys (stack as⇩2) = Mapping.keys (stack as⇩1) ∪ {n}) (showsl STR '''update_asFun:  stack2 is not extensions of stack1'');
    IA.check_valid_formula (kb as⇩1 ∧⇩f φ ⟶⇩f kb as⇩2);
    check (IA.formula (kb as⇩1 ∧⇩f φ ⟶⇩f kb as⇩2)) (showsl STR ''update_asFun: kbs are not proper formulas'')
}"

(* export_code update_asFun in Haskell *)

abbreviation check' where "check' x ≡ check x id"

definition checkFormula where
  "checkFormula f = do {check (IA.formula f) (showsl STR ''Non well formed formula'');
                        IA.check_valid_formula f}"

locale graph_exec =
  fixes as_map_of_node :: "'n ⇒ (LLVM_Syntax.pos, name, ('lv::{linorder,showl})) abstract_state_mapping" and
        renaming_of_edge :: "('n × 'n) ⇒ ('lv ⇒ 'lv) option" and
        edges ::  "('n × 'n) set" and
        prog :: llvm_prog
begin

definition renaming_of_edge' where
  "renaming_of_edge' x = (case renaming_of_edge x of Some f ⇒ f | None ⇒ id)"

sublocale llvm_se_graph renaming_of_edge' edges "asm_to_as ∘ as_map_of_node" prog .

definition evalFun where
  "evalFun n⇩1 n⇩2 v⇩n =
  (do { let as⇩1 = as_map_of_node n⇩1;
       let as⇩2 = as_map_of_node n⇩2;
       let fs = (case find_statement prog (pos as⇩1) of
                  Inr (Instruction (Named n (Binop binop o⇩1 o⇩2))) ⇒ Inr (n, binop, o⇩1, o⇩2)
                  | Inr _ ⇒ Inl (showsl STR ''evalFun: Not a binop'')
                  | Inl (StaticError x) ⇒ Inl (showsl x)
                  | Inl _ ⇒ Inl (showsl STR ''evalFun: unexpected error''));
       (n, binop, o⇩1, o⇩2) ← fs;
       t⇩1 ← option_to_sum (operand_value (asm_to_as as⇩1) o⇩1) (showsl STR ''evalFun 2'');
       t⇩2 ← option_to_sum (operand_value (asm_to_as as⇩1) o⇩2) (showsl STR ''evalFun 3'');
       let φ = encode_binop binop v⇩n t⇩1 t⇩2;
       update_asFun as⇩1 as⇩2 n v⇩n φ;
       check (renaming_of_edge (n⇩1, n⇩2) = None) (showsl STR ''evalFun 5'');
       check (pos as⇩2 = inc_pos (pos as⇩1)) (showsl STR ''evalFun 6'');
       check (n⇩1 ∈ nodes ∧ n⇩2 ∈ nodes  ∧ (n⇩1,n⇩2) ∈ edges) (showsl STR ''evalFun 7'')
       })"

definition evalExternalFun where
  "evalExternalFun n⇩1 n⇩2 v⇩n =
  (do { let as⇩1 = as_map_of_node n⇩1;
       let as⇩2 = as_map_of_node n⇩2;
       (n, gn, ps) ← (case find_statement prog (pos as⇩1) of
                  Inr (Instruction (Named n (Call t gn ps))) ⇒ Inr (n, gn, ps)
                  | Inr _ ⇒ Inl (showsl STR ''externalEvalFun: Not a external function call'')
                  | Inl (StaticError x) ⇒ Inl (showsl x)
                  | Inl _ ⇒ Inl (showsl STR ''externalEvalFun: unexpected error''));
       (case small_step.map_of_funs prog gn of Some (ExternalFunction _ _ _) ⇒ Inr ()
                 | _ ⇒ Inl (showsl STR ''externalEvalFun: Not a external function call''));
       update_asFun as⇩1 as⇩2 n v⇩n True⇩f;
       check (renaming_of_edge (n⇩1, n⇩2) = None) (showsl STR ''externalEvalFun: 5'');
       check (pos as⇩2 = inc_pos (pos as⇩1)) (showsl STR ''externalEvalFun: 6'');
       check (n⇩1 ∈ nodes ∧ n⇩2 ∈ nodes  ∧ (n⇩1,n⇩2) ∈ edges) (showsl STR ''externalEvalFun: 7'')
       })"

definition genFun where
  "genFun n⇩1 n⇩2 =
  (do {let as⇩1 = as_map_of_node n⇩1;
       let as⇩2 = as_map_of_node n⇩2;
       μ ←  option_to_sum (renaming_of_edge (n⇩1, n⇩2)) id;
       check (pos as⇩2 = pos as⇩1) (showsl STR ''genFun 1'');
       check (Mapping.keys (stack as⇩1) = Mapping.keys (stack as⇩2)) (showsl STR ''genFun 2'');
       check (IA.formula (kb as⇩1 ⟶⇩f rename_vars μ (kb as⇩2))) (showsl STR ''genFun 3'');
       IA.check_valid_formula (kb as⇩1 ⟶⇩f rename_vars μ (kb as⇩2));
       check (∀n ∈ Mapping.keys (stack as⇩2).
               (case Mapping.lookup (stack as⇩2) n of
                 Some lv ⇒ Mapping.lookup (stack as⇩1) n = Some (μ lv))) (showsl STR ''genFun 4'');
       check (n⇩1 ∈ nodes ∧ n⇩2 ∈ nodes  ∧ (n⇩1,n⇩2) ∈ edges) (showsl STR ''genFun 5'')
       })"



definition refineFun where
  "refineFun n n⇩t n⇩f φ =
  (do {let as = as_map_of_node n;
       let as⇩t = as_map_of_node n⇩t;
       let as⇩f = as_map_of_node n⇩f;
       check (pos as⇩t = pos as) (showsl ''refineFun 1'');
       check (pos as⇩f = pos as) (showsl ''refineFun 2'');
       check (stack as⇩t = stack as) (showsl ''refineFun 3'');
       check (stack as⇩f = stack as) (showsl ''refineFun 4'');
       check (IA.formula (kb as ∧⇩f φ ⟶⇩f kb as⇩t)) (showsl ''refineFun 5'');
       IA.check_valid_formula (kb as ∧⇩f φ ⟶⇩f kb as⇩t);
       check (IA.formula (kb as ∧⇩f (¬⇩f φ) ⟶⇩f kb as⇩f )) (showsl ''refineFun 6'');
       IA.check_valid_formula (kb as ∧⇩f (¬⇩f φ) ⟶⇩f kb as⇩f);
       check (renaming_of_edge (n, n⇩t) = None) (showsl ''refineFun 7'');
       check (renaming_of_edge (n, n⇩f) = None) (showsl ''refineFun 8'');
       check (n ∈ nodes) (showsl ''refineFun 9'');
       check (n⇩f ∈ nodes) (showsl ''refineFun 10'');
       check (n⇩t ∈ nodes) (showsl ''refineFun 11'');
       check ((n,n⇩t) ∈ edges) (showsl ''refineFun 12'');
       check ((n,n⇩f) ∈ edges) (showsl ''refineFun 13'')
       })"



definition phi_abstract'Fun where
  "phi_abstract'Fun as⇩1 as⇩2 x ps v⇩x t⇩x old_b_id = do {
       y⇩x ← option_to_sum (small_step.phi_bid old_b_id ps) id;
       check (operand_value (asm_to_as as⇩1) y⇩x = Some t⇩x) (showsl STR ''phi_abstract Fun 1'');
       check ((v⇩x ∉ Mapping_values (stack as⇩1))) (showsl STR ''phi_abstract Fun 2'');
       check (Mapping.lookup (stack as⇩2) x = Some v⇩x)  (showsl STR ''phi_abstract Fun 3'');
       check (¬ (v⇩x ∈ set (map fst (vars_formula_list (kb as⇩1))))) (showsl STR ''phi_abstract Fun 4'');
       check (IA.has_type t⇩x IA.IntT)  (showsl STR ''phi_abstract'Fun 6'')
       }"


fun phi_abstractFun where
  "phi_abstractFun as⇩1 as⇩2 ((x, ps)#xs) ((v⇩x, t⇩x)#ys) old_b_id =
    do {phi_abstract'Fun as⇩1 as⇩2 x ps v⇩x t⇩x old_b_id;
        phi_abstractFun as⇩1 as⇩2 xs ys old_b_id}"
| "phi_abstractFun as⇩1 as⇩2 [] [] old_b_id = Inr ()"
| "phi_abstractFun as⇩1 as⇩2 _ _ old_b_id = Inl (showsl STR ''phi_abstractFun'')"



definition branchFun where
  "branchFun n⇩1 n⇩2 φs =
  (do { let as⇩1 = as_map_of_node n⇩1;
       let as⇩2 = as_map_of_node n⇩2;
       let (f_id, old_b_id, p) = pos as⇩1;
       let new_b_id' = (case find_statement prog (pos as⇩1) of
                  Inr (Terminator (Named _ (Br new_b_id))) ⇒ Inr new_b_id
                | Inr (Terminator (Do (Br new_b_id))) ⇒ Inr new_b_id
                | Inr _ ⇒ Inl (showsl STR ''branchFun: Not a branch'')
                | Inl (StaticError x) ⇒ Inl (showsl x)
                | Inl _ ⇒ Inl (showsl STR ''branchFun: unexpected error''));
       new_b_id ← new_b_id';
       phis_stats ← map_sum (λ_. (showsl STR ''branchFun phis not found'')) id (find_phis prog f_id new_b_id);
       check (pos as⇩2 = (f_id, new_b_id, length phis_stats)) (showsl STR ''branchFun Wrong position'');
       phi_abstractFun as⇩1 as⇩2 phis_stats φs old_b_id;
       check (n⇩1 ∈ nodes ∧ n⇩2 ∈ nodes  ∧ (n⇩1,n⇩2) ∈ edges) ((showsl STR ''Wrong graph configuration''));
       let f = (Conjunction (map (λ(v⇩x,t⇩x). encode_eq (encode_var v⇩x) t⇩x) φs)) ∧⇩f (kb as⇩1) ⟶⇩f kb as⇩2;
       checkFormula f;
       check (inj_on (Mapping.lookup (stack as⇩2)) (fst ` set phis_stats)) ((showsl STR ''Not inj_on''));
       check ((∀x ∈ Mapping.keys (stack as⇩1).
                x ∉ (fst ` set phis_stats) ⟶ Mapping.lookup (stack as⇩2) x =
                                               Mapping.lookup (stack as⇩1) x)) ((showsl STR ''Not same vars''));
       check (Mapping.keys (stack as⇩2) = Mapping.keys (stack as⇩1) ∪ fst ` set phis_stats) ((showsl STR ''Wrong key subset''));
       check (distinct (map fst φs)) ((showsl STR ''Not distinct''));
       check (renaming_of_edge (n⇩1, n⇩2) = None) ((showsl STR ''Wrong renaming''));
       check (distinct (map fst phis_stats)) (showsl STR ''Not distinct'');
       check (∀a ∈ fst ` foldr union (map (vars_term ∘ snd) φs) {}. (a ∉ fst ` set φs)) (showsl STR ''branchFun 1'')
       })"

definition condBranchFun where
  "condBranchFun n⇩1 n⇩2 φs b =
  (do { let as⇩1 = as_map_of_node n⇩1;
       let as⇩2 = as_map_of_node n⇩2;
       let (f_id, old_b_id, p) = pos as⇩1;
       let new_b_id' = (case find_statement prog (pos as⇩1) of
                  Inr (Terminator (Named _ (CondBr c b⇩t b⇩f))) ⇒ Inr (c, b⇩t, b⇩f)
                | Inr (Terminator (Do (CondBr c b⇩t b⇩f))) ⇒  Inr (c, b⇩t, b⇩f)
                | Inr _ ⇒ Inl (showsl STR ''condbranchFun: Not a branch'')
                | Inl (StaticError x) ⇒ Inl (showsl x)
                | Inl _ ⇒ Inl (showsl STR ''condbranchFun: unexpected error''));
       (c, b_id_true, b_id_false) ← new_b_id';
       c' ← option_to_sum (operand_value (asm_to_as as⇩1) c) (showsl STR ''condBr 2'');
       let ft = kb as⇩1 ⟶⇩f encode_eq c' (Fun (IA.ConstF 1) []);
       let ff = kb as⇩1 ⟶⇩f encode_eq c' (Fun (IA.ConstF 0) []);
       let new_b_id = (if b then b_id_true else b_id_false);
       (if b then checkFormula ft else checkFormula ff);
       phis_stats ← map_sum (λ_. (showsl STR ''branchFun phis not found'')) id (find_phis prog f_id new_b_id);
       check (pos as⇩2 = (f_id, new_b_id, length phis_stats)) (showsl STR ''condBr 4'');
       phi_abstractFun as⇩1 as⇩2 phis_stats φs old_b_id;
       check (n⇩1 ∈ nodes ∧ n⇩2 ∈ nodes  ∧ (n⇩1,n⇩2) ∈ edges) (showsl STR ''condBr 5'');
       let f = (Conjunction (map (λ(v⇩x,t⇩x). encode_eq (encode_var v⇩x) t⇩x) φs)) ∧⇩f (kb as⇩1) ⟶⇩f kb as⇩2;
       checkFormula f;
       check (inj_on (Mapping.lookup (stack as⇩2)) (fst ` set phis_stats)) (showsl STR ''condBr 6'');
       check ((∀x ∈ Mapping.keys (stack as⇩1).
                x ∉ (fst ` set phis_stats) ⟶ Mapping.lookup (stack as⇩2) x =
                                               Mapping.lookup (stack as⇩1) x)) (showsl STR ''condBr 7'');
       check  (Mapping.keys (stack as⇩2) = Mapping.keys (stack as⇩1) ∪ fst ` set phis_stats) (showsl STR ''condBr 8'');
       check (distinct (map fst φs)) (showsl STR ''condBr 9'');
       check (renaming_of_edge (n⇩1, n⇩2) = None) (showsl STR ''condBr 10'');
       check (n⇩1 ∈ nodes ∧ n⇩2 ∈ nodes  ∧ (n⇩1,n⇩2) ∈ edges) (showsl STR ''condBr 11'');
       check (distinct (map fst phis_stats)) (showsl STR ''condBr 12'');
       check (∀a ∈ fst ` foldr union (map (vars_term ∘ snd) φs) {}. a ∉ fst ` set φs) (showsl STR ''condBr 13'')
       })"

definition icmpFun where
  "icmpFun n⇩1 n⇩2 v⇩n b =
  (do { let as⇩1 = as_map_of_node n⇩1;
       let as⇩2 = as_map_of_node n⇩2;
       let fs = (case find_statement prog (pos as⇩1) of
                   Inr (Instruction (Named n (Icmp p o⇩1 o⇩2))) ⇒ Inr (n, p, o⇩1, o⇩2)
                | Inr _ ⇒ Inl (showsl STR ''icmpFun: no icmp'')
                | Inl (StaticError x) ⇒ Inl (showsl x)
                | Inl _ ⇒ Inl (showsl STR ''icmpFun: unexpected error''));
       (n, p, o⇩1, o⇩2) ← fs;
       t⇩1 ←  option_to_sum (operand_value (asm_to_as as⇩1) o⇩1) id;
       t⇩2 ←  option_to_sum (operand_value (asm_to_as as⇩1) o⇩2) id;
       let φ = encode_pred p t⇩1 t⇩2;
       let χ = (if b then encode_eq (encode_var v⇩n) (Fun (IA.ConstF 1) [])
                     else encode_eq (encode_var v⇩n) (Fun (IA.ConstF 0) []));
       (if b then checkFormula (kb as⇩1 ⟶⇩f φ) else checkFormula (kb as⇩1 ⟶⇩f (¬⇩f φ)));
       update_asFun as⇩1 as⇩2 n v⇩n χ;
       check (renaming_of_edge (n⇩1, n⇩2) = None) (showsl STR ''icmpFun 2'');
       check (pos as⇩2 = inc_pos (pos as⇩1)) (showsl STR ''icmpFun 3'');
       check (n⇩1 ∈ nodes ∧ n⇩2 ∈ nodes  ∧ (n⇩1,n⇩2) ∈ edges) (showsl STR ''icmpFun 4'')
       })"

definition returnFun where
  "returnFun n⇩1 =
  (do { let as⇩1 = as_map_of_node n⇩1;
       let fs = (case find_statement prog (pos as⇩1) of
                  Inr (Terminator (Named _ (Ret (Some op)))) ⇒ Inr op
                | Inr (Terminator (Do (Ret (Some op)))) ⇒  Inr op
                | Inr _ ⇒ Inl (showsl STR ''returnFun: no return found'')
                | Inl (StaticError x) ⇒ Inl (showsl x)
                | Inl _ ⇒ Inl (showsl STR ''returnFun: unexpected error''));
       op ← fs;
       t⇩1 ←  option_to_sum (operand_value (asm_to_as as⇩1) op) (showsl STR ''returnFun 2'');
       check (n⇩1 ∈ nodes) (showsl STR ''returnFun 3'')
       })"


end

declare graph_exec.renaming_of_edge'_def [code]
declare graph_exec.evalFun_def [code]
declare graph_exec.genFun_def [code]
declare graph_exec.refineFun_def [code]
declare graph_exec.phi_abstract'Fun_def [code]
declare graph_exec.phi_abstractFun.simps [code]
declare graph_exec.branchFun_def [code]
declare graph_exec.condBranchFun_def [code]
declare graph_exec.icmpFun_def [code]
declare graph_exec.returnFun_def [code]

(*
export_code graph_exec.returnFun in Haskell
*)

datatype ('n, 'v) edge_rule =
    Eval 'n 'v
  | Gen 'n "('v × 'v) list"
  | Refine 'n 'n "(IA.sig, 'v × IA.ty) Term.term formula"
  | Br 'n "('v × (IA.sig, 'v × IA.ty) Term.term) list"
  | CondBr 'n "('v × (IA.sig, 'v × IA.ty) Term.term) list" bool
  | Icmp 'n 'v bool
  | Return

fun target_list where
  "target_list (Eval n _) = [n]"
| "target_list (Gen n _) = [n]"
| "target_list (Refine n1 n2 _) = [n1,n2]"
| "target_list (Br n _) = [n]"
| "target_list (CondBr n _ _) = [n]"
| "target_list (Icmp n _ _) = [n]"
| "target_list (Return) = []"

definition target where "target x = set (target_list x)"

type_synonym ('pos, 'pv, 'lv) as_impl = "'pos × ('pv × 'lv) list × 'lv IA.formula"

datatype ('node, 'lv) seg_impl =
  Seg_Impl
  (initial_node: "'node")
  (edges: "('node × ('node, 'lv) edge_rule) list")
  (nodes_as: "('node × ((name × name × nat), name, 'lv) as_impl) list")

(* Function to collect error messages and not just show the first one
   Useful for debugging
*)
fun collectErrorMessages :: "('e + 'a) list ⇒ 'e list + 'a list"
where
  "collectErrorMessages [] = Inr []" |
  "collectErrorMessages (m # ms) =
     (case collectErrorMessages ms of Inr ms' ⇒ map_sum (λe. [e]) (λm'. m'#ms') m
                | Inl es ⇒
     case m of Inr m' ⇒ Inl es | Inl e ⇒ Inl (e#es))
  "

lemma collectErrorMessages_sequence: "isOK (collectErrorMessages xs) ⟷ isOK (sequence xs)"
proof -
  have "isOK m"
    if "isOK (sequence xs)" "collectErrorMessages xs = Inr xs'"
      "isOK (map_sum (λe. [e]) (λm'. m' # xs') m)" for m xs xs'
    using that by (cases m) (auto)
  then show ?thesis
    by (induction xs) (auto split: sum.splits)
qed

locale graph_exec' =
  fixes seg :: "('n::{showl}, 'lv::{linorder,showl}) seg_impl"
  and prog :: llvm_prog
begin

definition edges_list where
  "edges_list =
    concat (map (λ(n,r). map (λt. (n, t)) (target_list r)) (seg_impl.edges seg))"

definition edges where "edges = set edges_list"
definition nodes_list where "nodes_list = remdups (map fst edges_list @ map snd edges_list)"
definition edge where "edge = Mapping.of_alist (seg_impl.edges seg)"

fun renaming_of_edge where
  "renaming_of_edge (n⇩1, n⇩2) =
    (case Mapping.lookup edge n⇩1
      of Some (Gen n⇩2' μ) ⇒
       if n⇩2 = n⇩2' then Some (λx. case map_of μ x of Some y ⇒ y | None ⇒ x)
                   else Some id
      | _ ⇒ None)"

definition nodes_asm_list where
  "nodes_asm_list =
    map (λ(n, (p, s, kb)). (n, ⦇pos = p, stack = Mapping.of_alist s, kb = kb⦈))
    (seg_impl.nodes_as seg)"

definition as where "as = (Mapping.of_alist nodes_asm_list)"

sublocale graph_exec "the ∘ (Mapping.lookup as)" renaming_of_edge edges prog .

definition choice_collect_error_messages where
  "choice_collect_error_messages ms =
    (try Error_Monad.choice ms catch (λf. Inl (default_showsl_list id f)))"

fun checkEdge :: "'n ⇒ ('n, 'lv) edge_rule ⇒  (String.literal ⇒ String.literal) + unit" where
  "checkEdge n1 (Eval n2 v⇩n) = choice_collect_error_messages [evalFun n1 n2 v⇩n, evalExternalFun n1 n2 v⇩n]"
| "checkEdge n1 (Gen n2 μ) = genFun n1 n2"
| "checkEdge n1 (Refine n2 n3 φ) = refineFun n1 n2 n3 φ"
| "checkEdge n1 (Br n2 φs) = branchFun n1 n2 φs"
| "checkEdge n1 (CondBr n2 φs b) = condBranchFun n1 n2 φs b"
| "checkEdge n1 (Icmp n2 v⇩n b) = icmpFun n1 n2 v⇩n b"
| "checkEdge n1 (Return) = returnFun n1"

definition checkEdge' where
  "checkEdge' n e = (let
     message_add = (λem. showsl_lit STR ''Error on node '' ∘ showsl n ∘ showsl_lit STR '':'' ∘ em)
   in
     map_sum message_add id (checkEdge n e))"

definition closedGraphFun' where
  "closedGraphFun' = (let
    check_n = (λn.
      do {
        e ← option_to_sum (Mapping.lookup edge n) (showsl STR ''No edge found for node: '' ∘ showsl n);
        checkEdge' n e
      })
  in
    map (check_n ∘ fst) (nodes_as seg))"

definition closedGraphFun where
  "closedGraphFun = do {
     check (set (map fst (nodes_as seg)) = nodes) (showsl STR ''edges and node set not in sync'');
     map_sum (default_showsl_list id) id (collectErrorMessages closedGraphFun')}"

end

declare graph_exec'.edges_def [code]
declare graph_exec'.renaming_of_edge.simps [code]
declare graph_exec'.checkEdge.simps [code]
declare graph_exec'.checkEdge'_def [code]
declare graph_exec'.closedGraphFun'_def [code]
declare graph_exec'.closedGraphFun_def [code]
declare graph_exec'.nodes_list_def [code]
declare graph_exec'.edges_list_def [code]
declare graph_exec'.edge_def [code]
declare graph_exec'.as_def [code]
declare graph_exec'.nodes_asm_list_def [code]
declare graph_exec.evalExternalFun_def [code]
declare graph_exec'.choice_collect_error_messages_def [code]


unbundle no_IA_formula_notation

end