5.41. Axiom Check

Scan all exes, replace BEXE_axiom_check e with BEXE_assert (axiom e) for each axiom that matches the argument e.
Start ocaml section to src/flx_axiom.mli[1 /1 ]
     1: # 8 "./lpsrc/flx_axiom.ipk"
     2: open Flx_ast
     3: open Flx_types
     4: open Flx_mtypes1
     5: open Flx_mtypes2
     6: 
     7: val axiom_check:
     8:   sym_state_t ->
     9:   fully_bound_symbol_table_t ->
    10:   unit
    11: 
End ocaml section to src/flx_axiom.mli[1]
Start ocaml section to src/flx_axiom.ml[1 /1 ]
     1: # 20 "./lpsrc/flx_axiom.ipk"
     2: open Flx_util
     3: open Flx_ast
     4: open Flx_types
     5: open Flx_print
     6: open Flx_mtypes1
     7: open Flx_mtypes2
     8: open Flx_typing
     9: open Flx_mbind
    10: open Flx_srcref
    11: open List
    12: open Flx_unify
    13: open Flx_treg
    14: open Flx_generic
    15: open Flx_maps
    16: open Flx_exceptions
    17: open Flx_use
    18: open Flx_child
    19: 
    20: let verify syms bbdfns csr e =
    21:   let xx = ref [] in
    22:   iter
    23:   ( fun (id, axsr, bvs, bpl, x) ->
    24:     (*
    25:     print_endline ("Checking for cases of axiom " ^ id);
    26:     *)
    27:     let param = match bpl with
    28:       | [] -> `BEXPR_tuple [],`BTYP_tuple []
    29:       | [_,(i,t)] -> `BEXPR_name (i,[]),t
    30:       | ls ->
    31:         let its = map snd ls in
    32:         let xs = map (fun (i,t)->`BEXPR_name (i,[]),t) its in
    33:         let ts = map snd xs in
    34:         `BEXPR_tuple xs,`BTYP_tuple ts
    35:     in
    36:     let tvars = map (fun (_,i) -> i) bvs in
    37:     let evars = map (fun (_,(i,_)) -> i) bpl in
    38:     let result = expr_maybe_matches syms.dfns tvars evars param e in
    39:     match result with
    40:     | None -> ()
    41:     | Some (tmgu, emgu) ->
    42:       (*
    43:       print_endline (sbe syms.dfns e ^  " MATCHES AXIOM " ^ id);
    44:       *)
    45:       let xsub x = fold_left (fun x (i,e) -> expr_term_subst x i e) x emgu in
    46:       let tsub t = list_subst tmgu t in
    47:       (*
    48:       print_endline ("tmgu= " ^ catmap ", " (fun (i,t) -> si i ^ "->" ^ sbt syms.dfns t) tmgu);
    49:       *)
    50:       let cond = xsub x in
    51:       let ident x = x in
    52:       let rec aux x = map_tbexpr ident aux tsub x in
    53:       let cond = aux cond in
    54:       let ax = `BEXE_assert2 (csr,axsr,cond) in
    55:       (*
    56:       print_endline ("Assertion: " ^ tsbe syms.dfns cond);
    57:       *)
    58:       xx := ax :: !xx
    59:   )
    60:   syms.axioms
    61:   ;
    62:   !xx
    63: 
    64: let fixup_exes syms bbdfns bexes =
    65:   let rec aux inx outx = match inx with
    66:   | [] -> rev outx
    67:   | `BEXE_axiom_check (sr,e) :: t ->
    68:     (*
    69:     print_endline ("Axiom check case "  ^ sbe syms.dfns e);
    70:     *)
    71:     aux t ((verify syms bbdfns sr e) @ outx)
    72: 
    73:   | h :: t -> aux t (h::outx)
    74:   in
    75:   aux bexes []
    76: 
    77: let axiom_check syms bbdfns =
    78:   Hashtbl.iter
    79:   (fun i (id,sr,parent,entry) ->
    80:     match entry with
    81:     | `BBDCL_function (ps,bvs,bpar,bty,bexes) ->
    82:       let bexes = fixup_exes syms bbdfns bexes in
    83:       let entry = `BBDCL_function (ps,bvs,bpar,bty,bexes) in
    84:       Hashtbl.replace bbdfns i (id,sr,parent,entry)
    85: 
    86:     | `BBDCL_procedure (ps,bvs,bpar,bexes) ->
    87:       let bexes = fixup_exes syms bbdfns bexes in
    88:       let entry = `BBDCL_procedure (ps,bvs,bpar,bexes) in
    89:       Hashtbl.replace bbdfns i (id,sr,parent,entry)
    90: 
    91:     | _ -> ()
    92:   )
    93:   bbdfns
    94: 
End ocaml section to src/flx_axiom.ml[1]