src/Tools/Compute_Oracle/am_sml.ML
author wenzelm
Fri, 02 Oct 2009 22:15:08 +0200
changeset 32861 105f40051387
parent 32740 9dd0a2f83429
child 32952 aeb1e44fbc19
permissions -rw-r--r--
eliminated dead code;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 24134
diff changeset
     1
(*  Title:      Tools/Compute_Oracle/am_sml.ML
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     2
    Author:     Steven Obua
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     3
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     4
    ToDO: "parameterless rewrite cannot be used in pattern": In a lot of cases it CAN be used, and these cases should be handled properly; 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     5
          right now, all cases throw an exception.
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     6
 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     7
*)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     8
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     9
signature AM_SML = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    10
sig
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    11
  include ABSTRACT_MACHINE
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    12
  val save_result : (string * term) -> unit
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    13
  val set_compiled_rewriter : (term -> term) -> unit				       
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    14
  val list_nth : 'a list * int -> 'a
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31327
diff changeset
    15
  val dump_output : (string option) Unsynchronized.ref 
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    16
end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    17
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    18
structure AM_SML : AM_SML = struct
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    19
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    20
open AbstractMachine;
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    21
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31327
diff changeset
    22
val dump_output = Unsynchronized.ref (NONE: string option)
25520
e123c81257a5 improvements
obua
parents: 25279
diff changeset
    23
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    24
type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    25
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31327
diff changeset
    26
val saved_result = Unsynchronized.ref (NONE:(string*term)option)
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    27
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    28
fun save_result r = (saved_result := SOME r)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    29
fun clear_result () = (saved_result := NONE)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    30
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    31
val list_nth = List.nth
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    32
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    33
(*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    34
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31327
diff changeset
    35
val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    36
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    37
fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    38
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    39
fun count_patternvars PVar = 1
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    40
  | count_patternvars (PConst (_, ps)) =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    41
      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    42
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    43
fun update_arity arity code a = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    44
    (case Inttab.lookup arity code of
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    45
	 NONE => Inttab.update_new (code, a) arity
24134
6e69e0031f34 added int type constraints to accomodate hacked SML/NJ;
wenzelm
parents: 23663
diff changeset
    46
       | SOME (a': int) => if a > a' then Inttab.update (code, a) arity else arity)
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    47
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    48
(* We have to find out the maximal arity of each constant *)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    49
fun collect_pattern_arity PVar arity = arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    50
  | collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    51
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    52
(* We also need to find out the maximal toplevel arity of each function constant *)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    53
fun collect_pattern_toplevel_arity PVar arity = raise Compile "internal error: collect_pattern_toplevel_arity"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    54
  | collect_pattern_toplevel_arity (PConst (c, args)) arity = update_arity arity c (length args)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    55
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    56
local
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    57
fun collect applevel (Var _) arity = arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    58
  | collect applevel (Const c) arity = update_arity arity c applevel
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    59
  | collect applevel (Abs m) arity = collect 0 m arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    60
  | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    61
in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    62
fun collect_term_arity t arity = collect 0 t arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    63
end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    64
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    65
fun collect_guard_arity (Guard (a,b)) arity  = collect_term_arity b (collect_term_arity a arity)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    66
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    67
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    68
fun rep n x = if n < 0 then raise Compile "internal error: rep" else if n = 0 then [] else x::(rep (n-1) x)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    69
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    70
fun beta (Const c) = Const c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    71
  | beta (Var i) = Var i
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    72
  | beta (App (Abs m, b)) = beta (unlift 0 (subst 0 m (lift 0 b)))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    73
  | beta (App (a, b)) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    74
    (case beta a of
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    75
	 Abs m => beta (App (Abs m, b))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    76
       | a => App (a, beta b))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    77
  | beta (Abs m) = Abs (beta m)
25217
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
    78
  | beta (Computed t) = Computed t
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    79
and subst x (Const c) t = Const c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    80
  | subst x (Var i) t = if i = x then t else Var i
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    81
  | subst x (App (a,b)) t = App (subst x a t, subst x b t)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    82
  | subst x (Abs m) t = Abs (subst (x+1) m (lift 0 t))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    83
and lift level (Const c) = Const c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    84
  | lift level (App (a,b)) = App (lift level a, lift level b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    85
  | lift level (Var i) = if i < level then Var i else Var (i+1)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    86
  | lift level (Abs m) = Abs (lift (level + 1) m)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    87
and unlift level (Const c) = Const c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    88
  | unlift level (App (a, b)) = App (unlift level a, unlift level b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    89
  | unlift level (Abs m) = Abs (unlift (level+1) m)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    90
  | unlift level (Var i) = if i < level then Var i else Var (i-1)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    91
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    92
fun nlift level n (Var m) = if m < level then Var m else Var (m+n) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    93
  | nlift level n (Const c) = Const c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    94
  | nlift level n (App (a,b)) = App (nlift level n a, nlift level n b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    95
  | nlift level n (Abs b) = Abs (nlift (level+1) n b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    96
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    97
fun subst_const (c, t) (Const c') = if c = c' then t else Const c'
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    98
  | subst_const _ (Var i) = Var i
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    99
  | subst_const ct (App (a, b)) = App (subst_const ct a, subst_const ct b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   100
  | subst_const ct (Abs m) = Abs (subst_const ct m)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   101
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   102
(* Remove all rules that are just parameterless rewrites. This is necessary because SML does not allow functions with no parameters. *)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   103
fun inline_rules rules =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   104
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   105
	fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   106
	  | term_contains_const c (Abs m) = term_contains_const c m
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   107
	  | term_contains_const c (Var i) = false
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   108
	  | term_contains_const c (Const c') = (c = c')
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   109
	fun find_rewrite [] = NONE
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   110
	  | find_rewrite ((prems, PConst (c, []), r) :: _) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   111
	    if check_freevars 0 r then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   112
		if term_contains_const c r then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   113
		    raise Compile "parameterless rewrite is caught in cycle"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   114
		else if not (null prems) then
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   115
		    raise Compile "parameterless rewrite may not be guarded"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   116
		else
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   117
		    SOME (c, r) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   118
	    else raise Compile "unbound variable on right hand side or guards of rule"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   119
	  | find_rewrite (_ :: rules) = find_rewrite rules
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   120
	fun remove_rewrite (c,r) [] = []
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   121
	  | remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   122
	    (if c = c' then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   123
		 if null args andalso r = r' andalso null (prems') then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   124
		     remove_rewrite cr rules 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   125
		 else raise Compile "incompatible parameterless rewrites found"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   126
	     else
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   127
		 rule :: (remove_rewrite cr rules))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   128
	  | remove_rewrite cr (r::rs) = r::(remove_rewrite cr rs)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   129
	fun pattern_contains_const c (PConst (c', args)) = (c = c' orelse exists (pattern_contains_const c) args)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   130
	  | pattern_contains_const c (PVar) = false
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   131
	fun inline_rewrite (ct as (c, _)) (prems, p, r) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   132
	    if pattern_contains_const c p then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   133
		raise Compile "parameterless rewrite cannot be used in pattern"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   134
	    else (map (fn (Guard (a,b)) => Guard (subst_const ct a, subst_const ct b)) prems, p, subst_const ct r)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   135
	fun inline inlined rules =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   136
	    (case find_rewrite rules of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   137
		 NONE => (Inttab.make inlined, rules)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   138
	       | SOME ct => 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   139
		 let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   140
		     val rules = map (inline_rewrite ct) (remove_rewrite ct rules)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   141
		     val inlined =  ct :: (map (fn (c', r) => (c', subst_const ct r)) inlined)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   142
		 in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   143
		     inline inlined rules
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   144
		 end)		
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   145
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   146
	inline [] rules		
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   147
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   148
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   149
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   150
(*
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   151
   Calculate the arity, the toplevel_arity, and adjust rules so that all toplevel pattern constants have maximal arity.
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   152
   Also beta reduce the adjusted right hand side of a rule.   
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   153
*)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   154
fun adjust_rules rules = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   155
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   156
	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
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   157
	val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   158
	fun arity_of c = the (Inttab.lookup arity c)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   159
	fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c)
25520
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   160
	fun test_pattern PVar = ()
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   161
	  | 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; ())
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   162
	fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   163
	  | adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   164
	  | adjust_rule (rule as (prems, p as PConst (c, args),t)) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   165
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   166
		val patternvars_counted = count_patternvars p
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   167
		fun check_fv t = check_freevars patternvars_counted t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   168
		val _ = if not (check_fv t) then raise Compile ("unbound variables on right hand side of rule") else () 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   169
		val _ = if not (forall (fn (Guard (a,b)) => check_fv a andalso check_fv b) prems) then raise Compile ("unbound variables in guards") else () 
25520
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   170
		val _ = map test_pattern args	        
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   171
		val len = length args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   172
		val arity = arity_of c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   173
		val lift = nlift 0
25520
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   174
		fun addapps_tm n t = if n=0 then t else addapps_tm (n-1) (App (t, Var (n-1)))
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   175
		fun adjust_term n t = addapps_tm n (lift n t)
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   176
		fun adjust_guard n (Guard (a,b)) = Guard (lift n a, lift n b)
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   177
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   178
		if len = arity then
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   179
		    rule
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   180
		else if arity >= len then  
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   181
		    (map (adjust_guard (arity-len)) prems, PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) t)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   182
		else (raise Compile "internal error in adjust_rule")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   183
	    end
25520
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   184
	fun beta_rule (prems, p, t) = ((prems, p, beta t) handle Match => raise Compile "beta_rule")
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   185
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   186
	(arity, toplevel_arity, map (beta_rule o adjust_rule) rules)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   187
    end		    
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   188
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   189
fun print_term module arity_of toplevel_arity_of pattern_var_count pattern_lazy_var_count =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   190
let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   191
    fun str x = string_of_int x
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   192
    fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   193
    val module_prefix = (case module of NONE => "" | SOME s => s^".")											  
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   194
    fun print_apps d f [] = f
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   195
      | print_apps d f (a::args) = print_apps d (module_prefix^"app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   196
    and print_call d (App (a, b)) args = print_call d a (b::args) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   197
      | print_call d (Const c) args = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   198
	(case arity_of c of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   199
	     NONE => print_apps d (module_prefix^"Const "^(str c)) args 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   200
	   | SOME 0 => module_prefix^"C"^(str c)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   201
	   | SOME a =>
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   202
	     let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   203
		 val len = length args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   204
	     in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   205
		 if a <= len then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   206
		     let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   207
			 val strict_a = (case toplevel_arity_of c of SOME sa => sa | NONE => a)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   208
			 val _ = if strict_a > a then raise Compile "strict" else ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   209
			 val s = module_prefix^"c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   210
			 val s = s^(concat (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   211
		     in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   212
			 print_apps d s (List.drop (args, a))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   213
		     end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   214
		 else 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   215
		     let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   216
			 fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n - 1)))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   217
			 fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   218
			 fun append_args [] t = t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   219
			   | append_args (c::cs) t = append_args cs (App (t, c))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   220
		     in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   221
			 print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c)))))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   222
		     end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   223
	     end)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   224
      | print_call d t args = print_apps d (print_term d t) args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   225
    and print_term d (Var x) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   226
	if x < d then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   227
	    "b"^(str (d-x-1)) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   228
	else 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   229
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   230
		val n = pattern_var_count - (x-d) - 1
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   231
		val x = "x"^(str n)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   232
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   233
		if n < pattern_var_count - pattern_lazy_var_count then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   234
		    x
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   235
		else 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   236
		    "("^x^" ())"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   237
	    end								
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   238
      | print_term d (Abs c) = module_prefix^"Abs (fn b"^(str d)^" => "^(print_term (d + 1) c)^")"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   239
      | print_term d t = print_call d t []
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   240
in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   241
    print_term 0 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   242
end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   243
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   244
fun section n = if n = 0 then [] else (section (n-1))@[n-1]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   245
			 			
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   246
fun print_rule gnum arity_of toplevel_arity_of (guards, p, t) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   247
    let	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   248
	fun str x = Int.toString x		    
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   249
	fun print_pattern top n PVar = (n+1, "x"^(str n))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   250
	  | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else ""))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   251
	  | print_pattern top n (PConst (c, args)) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   252
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   253
		val f = (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else "")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   254
		val (n, s) = print_pattern_list 0 top (n, f) args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   255
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   256
		(n, s)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   257
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   258
	and print_pattern_list' counter top (n,p) [] = if top then (n,p) else (n,p^")")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   259
	  | print_pattern_list' counter top (n, p) (t::ts) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   260
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   261
		val (n, t) = print_pattern false n t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   262
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   263
		print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^", "^t) ts
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   264
	    end	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   265
	and print_pattern_list counter top (n, p) (t::ts) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   266
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   267
		val (n, t) = print_pattern false n t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   268
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   269
		print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^" ("^t) ts
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   270
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   271
	val c = (case p of PConst (c, _) => c | _ => raise Match)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   272
	val (n, pattern) = print_pattern true 0 p
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   273
	val lazy_vars = the (arity_of c) - the (toplevel_arity_of c)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   274
	fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   275
        fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   276
	val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(concat (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   277
	fun print_guards t [] = print_tm t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   278
	  | print_guards t (g::gs) = "if ("^(print_guard g)^")"^(concat (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   279
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   280
	(if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   281
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   282
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   283
fun group_rules rules =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   284
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   285
	fun add_rule (r as (_, PConst (c,_), _)) groups =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   286
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   287
		val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   288
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   289
		Inttab.update (c, r::rs) groups
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   290
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   291
	  | add_rule _ _ = raise Compile "internal error group_rules"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   292
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   293
	fold_rev add_rule rules Inttab.empty
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   294
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   295
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   296
fun sml_prog name code rules = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   297
    let
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31327
diff changeset
   298
	val buffer = Unsynchronized.ref ""
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   299
	fun write s = (buffer := (!buffer)^s)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   300
	fun writeln s = (write s; write "\n")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   301
	fun writelist [] = ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   302
	  | writelist (s::ss) = (writeln s; writelist ss)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   303
	fun str i = Int.toString i
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   304
	val (inlinetab, rules) = inline_rules rules
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   305
	val (arity, toplevel_arity, rules) = adjust_rules rules
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   306
	val rules = group_rules rules
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   307
	val constants = Inttab.keys arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   308
	fun arity_of c = Inttab.lookup arity c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   309
	fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   310
	fun rep_str s n = concat (rep n s)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   311
	fun indexed s n = s^(str n)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   312
        fun string_of_tuple [] = ""
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   313
	  | string_of_tuple (x::xs) = "("^x^(concat (map (fn s => ", "^s) xs))^")"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   314
        fun string_of_args [] = ""
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   315
	  | string_of_args (x::xs) = x^(concat (map (fn s => " "^s) xs))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   316
	fun default_case gnum c = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   317
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   318
		val leftargs = concat (map (indexed " x") (section (the (arity_of c))))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   319
		val rightargs = section (the (arity_of c))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   320
		val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   321
		val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   322
		val right = (indexed "C" c)^" "^(string_of_tuple xs)
31322
526e149999cc attempt to eliminate adhoc makestring at runtime (which is not well-defined);
wenzelm
parents: 30678
diff changeset
   323
		val message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")"
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   324
		val right = if strict_args < the (arity_of c) then "raise AM_SML.Run "^message else right		
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   325
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   326
		(indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   327
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   328
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   329
	fun eval_rules c = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   330
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   331
		val arity = the (arity_of c)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   332
		val strict_arity = (case toplevel_arity_of c of NONE => arity | SOME sa => sa)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   333
		fun eval_rule n = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   334
		    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   335
			val sc = string_of_int c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   336
			val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section n) ("AbstractMachine.Const "^sc)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   337
                        fun arg i = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   338
			    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   339
				val x = indexed "x" i
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   340
				val x = if i < n then "(eval bounds "^x^")" else x
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   341
				val x = if i < strict_arity then x else "(fn () => "^x^")"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   342
			    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   343
				x
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   344
			    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   345
			val right = "c"^sc^" "^(string_of_args (map arg (section arity)))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   346
			val right = fold_rev (fn i => fn s => "Abs (fn "^(indexed "x" i)^" => "^s^")") (List.drop (section arity, n)) right		
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   347
			val right = if arity > 0 then right else "C"^sc
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   348
		    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   349
			"  | eval bounds ("^left^") = "^right
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   350
		    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   351
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   352
		map eval_rule (rev (section (arity + 1)))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   353
	    end
25217
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   354
25220
f22c1fcbc501 made SML/NJ happy;
wenzelm
parents: 25217
diff changeset
   355
	fun convert_computed_rules (c: int) : string list = 
25217
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   356
	    let
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   357
		val arity = the (arity_of c)
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   358
		fun eval_rule () = 
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   359
		    let
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   360
			val sc = string_of_int c
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   361
			val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section arity) ("AbstractMachine.Const "^sc)
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   362
                        fun arg i = "(convert_computed "^(indexed "x" i)^")" 
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   363
			val right = "C"^sc^" "^(string_of_tuple (map arg (section arity)))		
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   364
			val right = if arity > 0 then right else "C"^sc
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   365
		    in
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   366
			"  | convert_computed ("^left^") = "^right
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   367
		    end
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   368
	    in
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   369
		[eval_rule ()]
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   370
	    end
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   371
        
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   372
	fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n-1)) else ""
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   373
	val _ = writelist [                   
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   374
		"structure "^name^" = struct",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   375
		"",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   376
		"datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   377
		"         "^(concat (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   378
		""]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   379
	fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   380
	fun make_term_eq c = "  | term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   381
                             (case the (arity_of c) of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   382
				  0 => "true"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   383
				| n => 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   384
				  let 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   385
				      val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   386
				      val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   387
				  in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   388
				      eq^(concat eqs)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   389
				  end)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   390
	val _ = writelist [
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   391
		"fun term_eq (Const c1) (Const c2) = (c1 = c2)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   392
		"  | term_eq (App (a1,a2)) (App (b1,b2)) = term_eq a1 b1 andalso term_eq a2 b2"]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   393
	val _ = writelist (map make_term_eq constants)		
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   394
	val _ = writelist [
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   395
		"  | term_eq _ _ = false",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   396
                "" 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   397
		] 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   398
	val _ = writelist [
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   399
		"fun app (Abs a) b = a b",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   400
		"  | app a b = App (a, b)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   401
		""]	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   402
	fun defcase gnum c = (case arity_of c of NONE => [] | SOME a => if a > 0 then [default_case gnum c] else [])
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   403
	fun writefundecl [] = () 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   404
	  | writefundecl (x::xs) = writelist ((("and "^x)::(map (fn s => "  | "^s) xs)))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   405
	fun list_group c = (case Inttab.lookup rules c of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   406
				NONE => [defcase 0 c]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   407
			      | SOME rs => 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   408
				let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   409
				    val rs = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   410
					fold
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   411
					    (fn r => 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   412
					     fn rs =>
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   413
						let 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   414
						    val (gnum, l, rs) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   415
							(case rs of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   416
							     [] => (0, [], []) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   417
							   | (gnum, l)::rs => (gnum, l, rs))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   418
						    val (gnum', r) = print_rule gnum arity_of toplevel_arity_of r 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   419
						in 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   420
						    if gnum' = gnum then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   421
							(gnum, r::l)::rs
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   422
						    else
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   423
							let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   424
							    val args = concat (map (fn i => " a"^(str i)) (section (the (arity_of c))))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   425
							    fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   426
							    val s = gnumc (gnum) ^ " = " ^ gnumc (gnum') 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   427
							in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   428
							    (gnum', [])::(gnum, s::r::l)::rs
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   429
							end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   430
						end)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   431
					rs []
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   432
				    val rs = (case rs of [] => [(0,defcase 0 c)] | (gnum,l)::rs => (gnum, (defcase gnum c)@l)::rs)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   433
				in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   434
				    rev (map (fn z => rev (snd z)) rs)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   435
				end)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   436
	val _ = map (fn z => (map writefundecl z; writeln "")) (map list_group constants)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   437
	val _ = writelist [
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   438
		"fun convert (Const i) = AM_SML.Const i",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   439
		"  | convert (App (a, b)) = AM_SML.App (convert a, convert b)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   440
                "  | convert (Abs _) = raise AM_SML.Run \"no abstraction in result allowed\""]	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   441
	fun make_convert c = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   442
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   443
		val args = map (indexed "a") (section (the (arity_of c)))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   444
		val leftargs = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   445
		    case args of
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   446
			[] => ""
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   447
		      | (x::xs) => "("^x^(concat (map (fn s => ", "^s) xs))^")"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   448
		val args = map (indexed "convert a") (section (the (arity_of c)))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   449
		val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   450
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   451
		"  | convert (C"^(str c)^" "^leftargs^") = "^right
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   452
	    end 		
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   453
	val _ = writelist (map make_convert constants)
25217
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   454
        val _ = writelist [
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   455
                "",
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   456
                "fun convert_computed (AbstractMachine.Abs b) = raise AM_SML.Run \"no abstraction in convert_computed allowed\"",
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   457
                "  | convert_computed (AbstractMachine.Var i) = raise AM_SML.Run \"no bound variables in convert_computed allowed\""]
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   458
        val _ = map (writelist o convert_computed_rules) constants
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   459
        val _ = writelist [
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   460
                "  | convert_computed (AbstractMachine.Const c) = Const c",
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   461
                "  | convert_computed (AbstractMachine.App (a, b)) = App (convert_computed a, convert_computed b)",
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   462
                "  | convert_computed (AbstractMachine.Computed a) = raise AM_SML.Run \"no nesting in convert_computed allowed\""] 
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   463
	val _ = writelist [
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   464
		"",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   465
		"fun eval bounds (AbstractMachine.Abs m) = Abs (fn b => eval (b::bounds) m)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   466
		"  | eval bounds (AbstractMachine.Var i) = AM_SML.list_nth (bounds, i)"]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   467
	val _ = map (writelist o eval_rules) constants
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   468
	val _ = writelist [
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   469
                "  | eval bounds (AbstractMachine.App (a, b)) = app (eval bounds a) (eval bounds b)",
25217
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   470
                "  | eval bounds (AbstractMachine.Const c) = Const c",
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   471
                "  | eval bounds (AbstractMachine.Computed t) = convert_computed t"]                
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   472
	val _ = writelist [		
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   473
		"",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   474
		"fun export term = AM_SML.save_result (\""^code^"\", convert term)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   475
		"",
24654
329f1b4d9d16 improved computing
obua
parents: 24584
diff changeset
   476
                "val _ = AM_SML.set_compiled_rewriter (fn t => (convert (eval [] t)))",
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   477
                "",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   478
		"end"]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   479
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   480
	(arity, toplevel_arity, inlinetab, !buffer)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   481
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   482
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31327
diff changeset
   483
val guid_counter = Unsynchronized.ref 0
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   484
fun get_guid () = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   485
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   486
	val c = !guid_counter
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   487
	val _ = guid_counter := !guid_counter + 1
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   488
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   489
	(LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   490
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   491
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   492
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   493
fun writeTextFile name s = File.write (Path.explode name) s
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   494
31327
ffa5356cc343 ML_Env;
wenzelm
parents: 31322
diff changeset
   495
fun use_source src = use_text ML_Env.local_context (1, "") false src
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   496
    
25520
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   497
fun compile cache_patterns const_arity eqs = 
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   498
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   499
	val guid = get_guid ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   500
	val code = Real.toString (random ())
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   501
	val module = "AMSML_"^guid
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   502
	val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs
25520
e123c81257a5 improvements
obua
parents: 25279
diff changeset
   503
	val _ = case !dump_output of NONE => () | SOME p => writeTextFile p source
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   504
	val _ = compiled_rewriter := NONE
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   505
	val _ = use_source source
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   506
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   507
	case !compiled_rewriter of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   508
	    NONE => raise Compile "broken link to compiled function"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   509
	  | SOME f => (module, code, arity, toplevel_arity, inlinetab, f)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   510
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   511
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   512
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   513
fun run' (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   514
    let	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   515
	val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   516
	fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   517
	  | inline (Var i) = Var i
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   518
	  | inline (App (a, b)) = App (inline a, inline b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   519
	  | inline (Abs m) = Abs (inline m)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   520
	val t = beta (inline t)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   521
	fun arity_of c = Inttab.lookup arity c		 	 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   522
	fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   523
	val term = print_term NONE arity_of toplevel_arity_of 0 0 t 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   524
        val source = "local open "^module^" in val _ = export ("^term^") end"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   525
	val _ = writeTextFile "Gencode_call.ML" source
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   526
	val _ = clear_result ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   527
	val _ = use_source source
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   528
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   529
	case !saved_result of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   530
	    NONE => raise Run "broken link to compiled code"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   531
	  | SOME (code', t) => (clear_result (); if code' = code then t else raise Run "link to compiled code was hijacked")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   532
    end		
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   533
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   534
fun run (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   535
    let	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   536
	val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   537
	fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   538
	  | inline (Var i) = Var i
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   539
	  | inline (App (a, b)) = App (inline a, inline b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   540
	  | inline (Abs m) = Abs (inline m)
25217
3224db6415ae better compute oracle
obua
parents: 24654
diff changeset
   541
	  | inline (Computed t) = Computed t
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   542
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   543
	compiled_fun (beta (inline t))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   544
    end	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   545
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   546
fun discard p = ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   547
			 	  
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   548
end