5.44. 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: open Flx_typeclass
    20: 
    21: let string_of_bvs bvs =
    22:   catmap "," (fun (s,i)->s^"<"^si i^">") bvs
    23: 
    24: let verify syms bbdfns csr e =
    25:   let xx = ref [] in
    26:   iter
    27:   ( fun (id, axsr, parent, axiom_kind, bvs, (bpl,precond), x) ->
    28:     match x with | `BEquation _ -> () | `BPredicate x ->
    29:     (*
    30:     print_endline ("Checking for cases of axiom " ^ id);
    31:     *)
    32:     let param = match bpl with
    33:       | [] -> `BEXPR_tuple [],`BTYP_tuple []
    34:       | [{pindex=i;ptyp=t}] -> `BEXPR_name (i,[]),t
    35:       | ls ->
    36:         let xs = map (fun {pindex=i; ptyp=t}->`BEXPR_name (i,[]),t) ls in
    37:         let ts = map snd xs in
    38:         `BEXPR_tuple xs,`BTYP_tuple ts
    39:     in
    40:     let tvars = map (fun (_,i) -> i) bvs in
    41:     let evars = map (fun {pindex=i} -> i) bpl in
    42:     let result = expr_maybe_matches syms.dfns tvars evars param e in
    43:     match result with
    44:     | None -> ()
    45:     | Some (tmgu, emgu) ->
    46:       (*
    47:       print_endline (sbe syms.dfns e ^  " MATCHES AXIOM " ^ id);
    48:       print_endline ("Axiom vs =" ^ string_of_bvs bvs);
    49:       print_endline ("TMgu=" ^ string_of_varlist syms.dfns tmgu);
    50:       *)
    51:       let ok = match parent with
    52:       | None -> true
    53:       | Some i ->
    54:         try
    55:           let tcid,_,sr,entry = Hashtbl.find bbdfns i in
    56:           match entry with
    57:           | `BBDCL_typeclass (_,tcbvs) ->
    58:             begin
    59:               (*
    60:               print_endline ("Axiom "^id^" is owned by typeclass " ^ tcid);
    61:               print_endline ("Typeclass bvs=" ^ string_of_bvs tcbvs);
    62:               *)
    63:               let ts =
    64:                 try
    65:                   Some (map (fun (s,i) -> assoc i tmgu) tcbvs)
    66:                 with Not_found ->
    67:                   (*
    68:                   print_endline "Can't instantiate typeclass vars- FAIL";
    69:                   *)
    70:                   None
    71:               in
    72:               match ts with None -> false | Some ts ->
    73:               let insts =
    74:                 try
    75:                   Some (Hashtbl.find syms.instances_of_typeclass i)
    76:                 with Not_found ->
    77:                   (*
    78:                   print_endline "Typeclass has no instances";
    79:                   *)
    80:                   None
    81:               in
    82:               match insts with | None -> false | Some insts ->
    83:               try
    84:                 iter (fun (instidx,(inst_bvs, inst_traint, inst_ts)) ->
    85:                   match tcinst_chk syms true i ts sr (inst_bvs, inst_traint, inst_ts, instidx) with
    86:                   | None -> ()
    87:                   | Some _ -> raise Not_found
    88:                 )
    89:                 insts;
    90:                 (*
    91:                 print_endline "Couldn't find instance";
    92:                 *)
    93:                 false
    94:               with Not_found ->
    95:                 (*
    96:                 print_endline "FOUND INSTANCE";
    97:                 *)
    98:                 true
    99:             end
   100:           | _ -> true
   101:         with
   102:           Not_found ->
   103:           print_endline "Wha .. can't find axiom's parent";
   104:           true
   105:       in
   106:       if not ok then () else
   107:       let xsub x = fold_left (fun x (i,e) -> expr_term_subst x i e) x emgu in
   108:       let tsub t = list_subst tmgu t in
   109:       (*
   110:       print_endline ("tmgu= " ^ catmap ", " (fun (i,t) -> si i ^ "->" ^ sbt syms.dfns t) tmgu);
   111:       *)
   112:       let ident x = x in
   113:       let rec aux x = map_tbexpr ident aux tsub x in
   114:       let cond = aux (xsub x) in
   115:       let precond = match precond with
   116:       | Some x -> Some (aux (xsub x))
   117:       | None -> None
   118:       in
   119:       let comment = `BEXE_comment (csr,"Check " ^ id) in
   120:       let ax = `BEXE_assert2 (csr,axsr,precond,cond) in
   121:       (*
   122:       print_endline ("Assertion: " ^ tsbe syms.dfns cond);
   123:       *)
   124:       xx := ax :: comment :: !xx
   125:   )
   126:   syms.axioms
   127:   ;
   128:   !xx
   129: 
   130: let fixup_exes syms bbdfns bexes =
   131:   let rec aux inx outx = match inx with
   132:   | [] -> rev outx
   133:   | `BEXE_axiom_check (sr,e) :: t ->
   134:     (*
   135:     print_endline ("Axiom check case "  ^ sbe syms.dfns e);
   136:     *)
   137:     aux t ((verify syms bbdfns sr e) @ outx)
   138: 
   139:   | h :: t -> aux t (h::outx)
   140:   in
   141:   aux bexes []
   142: 
   143: let axiom_check syms bbdfns =
   144:   Hashtbl.iter
   145:   (fun i (id,sr,parent,entry) ->
   146:     match entry with
   147:     | `BBDCL_function (ps,bvs,bpar,bty,bexes) ->
   148:       let bexes = fixup_exes syms bbdfns bexes in
   149:       let entry = `BBDCL_function (ps,bvs,bpar,bty,bexes) in
   150:       Hashtbl.replace bbdfns i (id,sr,parent,entry)
   151: 
   152:     | `BBDCL_procedure (ps,bvs,bpar,bexes) ->
   153:       let bexes = fixup_exes syms bbdfns bexes in
   154:       let entry = `BBDCL_procedure (ps,bvs,bpar,bexes) in
   155:       Hashtbl.replace bbdfns i (id,sr,parent,entry)
   156: 
   157:     | _ -> ()
   158:   )
   159:   bbdfns
   160: 
End ocaml section to src/flx_axiom.ml[1]