7 (* TERM_C extends Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *) |
7 (* TERM_C extends Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *) |
8 signature TERM_C = |
8 signature TERM_C = |
9 sig |
9 sig |
10 datatype lrd = D | L | R |
10 datatype lrd = D | L | R |
11 type path |
11 type path |
12 val path2str: path -> string |
12 val string_of_path: path -> string |
13 val at_location: path -> term -> term |
13 val at_location: path -> term -> term |
14 val go_up: path -> term -> term |
14 val go_up: path -> term -> term |
15 |
15 |
16 val contains_Var: term -> bool |
16 val contains_Var: term -> bool |
17 val dest_binop_typ: typ -> typ * typ * typ |
17 val dest_binop_typ: typ -> typ * typ * typ |
107 | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*) |
107 | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*) |
108 type path = lrd list; |
108 type path = lrd list; |
109 fun ldr2str L = "L" |
109 fun ldr2str L = "L" |
110 | ldr2str R = "R" |
110 | ldr2str R = "R" |
111 | ldr2str D = "D"; |
111 | ldr2str D = "D"; |
112 fun path2str k = (strs2str' o (map ldr2str)) k; |
112 fun string_of_path k = (strs2str' o (map ldr2str)) k; |
113 (*go to a location in a term and fetch the resective sub-term*) |
113 (*go to a location in a term and fetch the resective sub-term*) |
114 fun at_location [] t = t |
114 fun at_location [] t = t |
115 | at_location (D :: p) (Abs(_, _, body)) = at_location p body |
115 | at_location (D :: p) (Abs(_, _, body)) = at_location p body |
116 | at_location (L :: p) (t1 $ _) = at_location p t1 |
116 | at_location (L :: p) (t1 $ _) = at_location p t1 |
117 | at_location (R :: p) (_ $ t2) = at_location p t2 |
117 | at_location (R :: p) (_ $ t2) = at_location p t2 |
118 | at_location l t = raise TERM ("at_location: no " ^ path2str l ^ " for ", [t]); |
118 | at_location l t = raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]); |
119 fun go_up l t = |
119 fun go_up l t = |
120 if length l > 1 then at_location (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t) |
120 if length l > 1 then at_location (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t) |
121 |
121 |
122 fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i) |
122 fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i) |
123 |
123 |