24 type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term) |
24 type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term) |
25 |
25 |
26 val saved_result = Unsynchronized.ref (NONE:(string*term)option) |
26 val saved_result = Unsynchronized.ref (NONE:(string*term)option) |
27 |
27 |
28 fun save_result r = (saved_result := SOME r) |
28 fun save_result r = (saved_result := SOME r) |
29 fun clear_result () = (saved_result := NONE) |
|
30 |
29 |
31 val list_nth = List.nth |
30 val list_nth = List.nth |
32 |
31 |
33 val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) |
32 val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) |
34 |
33 |
100 (* Remove all rules that are just parameterless rewrites. This is necessary because SML does not allow functions with no parameters. *) |
99 (* Remove all rules that are just parameterless rewrites. This is necessary because SML does not allow functions with no parameters. *) |
101 fun inline_rules rules = |
100 fun inline_rules rules = |
102 let |
101 let |
103 fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b |
102 fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b |
104 | term_contains_const c (Abs m) = term_contains_const c m |
103 | term_contains_const c (Abs m) = term_contains_const c m |
105 | term_contains_const c (Var i) = false |
104 | term_contains_const c (Var _) = false |
106 | term_contains_const c (Const c') = (c = c') |
105 | term_contains_const c (Const c') = (c = c') |
107 fun find_rewrite [] = NONE |
106 fun find_rewrite [] = NONE |
108 | find_rewrite ((prems, PConst (c, []), r) :: _) = |
107 | find_rewrite ((prems, PConst (c, []), r) :: _) = |
109 if check_freevars 0 r then |
108 if check_freevars 0 r then |
110 if term_contains_const c r then |
109 if term_contains_const c r then |
113 raise Compile "parameterless rewrite may not be guarded" |
112 raise Compile "parameterless rewrite may not be guarded" |
114 else |
113 else |
115 SOME (c, r) |
114 SOME (c, r) |
116 else raise Compile "unbound variable on right hand side or guards of rule" |
115 else raise Compile "unbound variable on right hand side or guards of rule" |
117 | find_rewrite (_ :: rules) = find_rewrite rules |
116 | find_rewrite (_ :: rules) = find_rewrite rules |
118 fun remove_rewrite (c,r) [] = [] |
117 fun remove_rewrite _ [] = [] |
119 | remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) = |
118 | remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) = |
120 (if c = c' then |
119 (if c = c' then |
121 if null args andalso r = r' andalso null (prems') then |
120 if null args andalso r = r' andalso null (prems') then |
122 remove_rewrite cr rules |
121 remove_rewrite cr rules |
123 else raise Compile "incompatible parameterless rewrites found" |
122 else raise Compile "incompatible parameterless rewrites found" |
150 Also beta reduce the adjusted right hand side of a rule. |
149 Also beta reduce the adjusted right hand side of a rule. |
151 *) |
150 *) |
152 fun adjust_rules rules = |
151 fun adjust_rules rules = |
153 let |
152 let |
154 val arity = fold (fn (prems, p, t) => fn arity => fold collect_guard_arity prems (collect_term_arity t (collect_pattern_arity p arity))) rules Inttab.empty |
153 val arity = fold (fn (prems, p, t) => fn arity => fold collect_guard_arity prems (collect_term_arity t (collect_pattern_arity p arity))) rules Inttab.empty |
155 val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty |
154 val toplevel_arity = fold (fn (_, p, _) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty |
156 fun arity_of c = the (Inttab.lookup arity c) |
155 fun arity_of c = the (Inttab.lookup arity c) |
157 fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c) |
|
158 fun test_pattern PVar = () |
156 fun test_pattern PVar = () |
159 | test_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else (map test_pattern args; ()) |
157 | test_pattern (PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else (map test_pattern args; ()) |
160 fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable") |
158 fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable") |
161 | adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters") |
159 | adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters") |
162 | adjust_rule (rule as (prems, p as PConst (c, args),t)) = |
160 | adjust_rule (rule as (prems, p as PConst (c, args),t)) = |
163 let |
161 let |
164 val patternvars_counted = count_patternvars p |
162 val patternvars_counted = count_patternvars p |
490 |
488 |
491 fun writeTextFile name s = File.write (Path.explode name) s |
489 fun writeTextFile name s = File.write (Path.explode name) s |
492 |
490 |
493 fun use_source src = use_text ML_Env.local_context (1, "") false src |
491 fun use_source src = use_text ML_Env.local_context (1, "") false src |
494 |
492 |
495 fun compile cache_patterns const_arity eqs = |
493 fun compile _ _ eqs = |
496 let |
494 let |
497 val guid = get_guid () |
495 val guid = get_guid () |
498 val code = Real.toString (random ()) |
496 val code = Real.toString (random ()) |
499 val module = "AMSML_"^guid |
497 val module = "AMSML_"^guid |
500 val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs |
498 val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs |
505 case !compiled_rewriter of |
503 case !compiled_rewriter of |
506 NONE => raise Compile "broken link to compiled function" |
504 NONE => raise Compile "broken link to compiled function" |
507 | SOME f => (module, code, arity, toplevel_arity, inlinetab, f) |
505 | SOME f => (module, code, arity, toplevel_arity, inlinetab, f) |
508 end |
506 end |
509 |
507 |
510 |
508 fun run (_, _, _, _, inlinetab, compiled_fun) t = |
511 fun run' (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = |
|
512 let |
|
513 val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") |
|
514 fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t) |
|
515 | inline (Var i) = Var i |
|
516 | inline (App (a, b)) = App (inline a, inline b) |
|
517 | inline (Abs m) = Abs (inline m) |
|
518 val t = beta (inline t) |
|
519 fun arity_of c = Inttab.lookup arity c |
|
520 fun toplevel_arity_of c = Inttab.lookup toplevel_arity c |
|
521 val term = print_term NONE arity_of toplevel_arity_of 0 0 t |
|
522 val source = "local open "^module^" in val _ = export ("^term^") end" |
|
523 val _ = writeTextFile "Gencode_call.ML" source |
|
524 val _ = clear_result () |
|
525 val _ = use_source source |
|
526 in |
|
527 case !saved_result of |
|
528 NONE => raise Run "broken link to compiled code" |
|
529 | SOME (code', t) => (clear_result (); if code' = code then t else raise Run "link to compiled code was hijacked") |
|
530 end |
|
531 |
|
532 fun run (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = |
|
533 let |
509 let |
534 val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") |
510 val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") |
535 fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t) |
511 fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t) |
536 | inline (Var i) = Var i |
512 | inline (Var i) = Var i |
537 | inline (App (a, b)) = App (inline a, inline b) |
513 | inline (App (a, b)) = App (inline a, inline b) |