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: