equal
deleted
inserted
replaced
22 val compiled_rewriter = ref (NONE:(term -> term)Option.option) |
22 val compiled_rewriter = ref (NONE:(term -> term)Option.option) |
23 |
23 |
24 fun set_compiled_rewriter r = (compiled_rewriter := SOME r) |
24 fun set_compiled_rewriter r = (compiled_rewriter := SOME r) |
25 |
25 |
26 type program = (term -> term) |
26 type program = (term -> term) |
27 |
|
28 |
|
29 (*Returns true iff at most 0 .. (free-1) occur unbound. therefore |
|
30 check_freevars 0 t iff t is closed*) |
|
31 fun check_freevars free (Var x) = x < free |
|
32 | check_freevars free (Const c) = true |
|
33 | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v |
|
34 | check_freevars free (Abs m) = check_freevars (free+1) m |
|
35 |
27 |
36 fun count_patternvars PVar = 1 |
28 fun count_patternvars PVar = 1 |
37 | count_patternvars (PConst (_, ps)) = |
29 | count_patternvars (PConst (_, ps)) = |
38 List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps |
30 List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps |
39 |
31 |
64 fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*) |
56 fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*) |
65 "Var " ^ str x |
57 "Var " ^ str x |
66 | print_term d (Const c) = "c" ^ str c |
58 | print_term d (Const c) = "c" ^ str c |
67 | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")" |
59 | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")" |
68 | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")" |
60 | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")" |
|
61 | print_term d (Computed c) = print_term d c |
69 |
62 |
70 fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1)) |
63 fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1)) |
71 |
64 |
72 val term = print_term 0 t |
65 val term = print_term 0 t |
73 val term = |
66 val term = |
83 |
76 |
84 fun constants_of_term (Var _) = [] |
77 fun constants_of_term (Var _) = [] |
85 | constants_of_term (Abs m) = constants_of_term m |
78 | constants_of_term (Abs m) = constants_of_term m |
86 | constants_of_term (App (a,b)) = (constants_of_term a)@(constants_of_term b) |
79 | constants_of_term (App (a,b)) = (constants_of_term a)@(constants_of_term b) |
87 | constants_of_term (Const c) = [c] |
80 | constants_of_term (Const c) = [c] |
|
81 | constants_of_term (Computed c) = constants_of_term c |
88 |
82 |
89 fun load_rules sname name prog = |
83 fun load_rules sname name prog = |
90 let |
84 let |
91 val buffer = ref "" |
85 val buffer = ref "" |
92 fun write s = (buffer := (!buffer)^s) |
86 fun write s = (buffer := (!buffer)^s) |