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: