src/Tools/Compute_Oracle/am_ghc.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_ghc.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
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     5
structure AM_GHC : ABSTRACT_MACHINE = struct
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     6
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     7
open AbstractMachine;
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     8
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
     9
type program = string * string * (int Inttab.table)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    10
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    11
fun count_patternvars PVar = 1
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    12
  | count_patternvars (PConst (_, ps)) =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    13
      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    14
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    15
fun update_arity arity code a = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    16
    (case Inttab.lookup arity code of
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    17
	 NONE => Inttab.update_new (code, a) arity
24134
6e69e0031f34 added int type constraints to accomodate hacked SML/NJ;
wenzelm
parents: 23663
diff changeset
    18
       | 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
    19
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    20
(* We have to find out the maximal arity of each constant *)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    21
fun collect_pattern_arity PVar arity = arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    22
  | 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
    23
 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    24
local
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    25
fun collect applevel (Var _) arity = arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    26
  | collect applevel (Const c) arity = update_arity arity c applevel
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    27
  | collect applevel (Abs m) arity = collect 0 m arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    28
  | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    29
in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    30
fun collect_term_arity t arity = collect 0 t arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    31
end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    32
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    33
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
    34
  | nlift level n (Const c) = Const c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    35
  | 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
    36
  | nlift level n (Abs b) = Abs (nlift (level+1) n b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    37
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    38
fun rep n x = if n = 0 then [] else x::(rep (n-1) x)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    39
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    40
fun adjust_rules rules =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    41
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    42
	val arity = fold (fn (p, t) => fn arity => collect_term_arity t (collect_pattern_arity p arity)) rules Inttab.empty
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    43
	fun arity_of c = the (Inttab.lookup arity c)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    44
	fun adjust_pattern PVar = PVar
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    45
	  | adjust_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else C
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    46
	fun adjust_rule (PVar, t) = raise Compile ("pattern may not be a variable")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    47
	  | adjust_rule (rule as (p as PConst (c, args),t)) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    48
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    49
		val _ = if not (check_freevars (count_patternvars p) t) then raise Compile ("unbound variables on right hand side") else () 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    50
		val args = map adjust_pattern args	        
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    51
		val len = length args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    52
		val arity = arity_of c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    53
		fun lift level n (Var m) = if m < level then Var m else Var (m+n) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    54
		  | lift level n (Const c) = Const c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    55
		  | lift level n (App (a,b)) = App (lift level n a, lift level n b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    56
		  | lift level n (Abs b) = Abs (lift (level+1) n b)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    57
		val lift = lift 0
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    58
		fun adjust_term n t = if n=0 then t else adjust_term (n-1) (App (t, Var (n-1))) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    59
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    60
		if len = arity then
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    61
		    rule
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    62
		else if arity >= len then  
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    63
		    (PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) (lift (arity-len) t))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    64
		else (raise Compile "internal error in adjust_rule")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    65
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    66
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    67
	(arity, map adjust_rule rules)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    68
    end		    
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    69
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    70
fun print_term arity_of n =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    71
let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    72
    fun str x = string_of_int x
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    73
    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
    74
											  
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    75
    fun print_apps d f [] = f
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    76
      | print_apps d f (a::args) = print_apps d ("app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    77
    and print_call d (App (a, b)) args = print_call d a (b::args) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    78
      | print_call d (Const c) args = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    79
	(case arity_of c of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    80
	     NONE => print_apps d ("Const "^(str c)) args 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    81
	   | SOME a =>
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    82
	     let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    83
		 val len = length args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    84
	     in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    85
		 if a <= len then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    86
		     let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    87
			 val s = "c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a))))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    88
		     in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    89
			 print_apps d s (List.drop (args, a))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    90
		     end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    91
		 else 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    92
		     let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    93
			 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
    94
			 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
    95
			 fun append_args [] t = t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    96
			   | append_args (c::cs) t = append_args cs (App (t, c))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    97
		     in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
    98
			 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
    99
		     end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   100
	     end)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   101
      | print_call d t args = print_apps d (print_term d t) args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   102
    and print_term d (Var x) = if x < d then "b"^(str (d-x-1)) else "x"^(str (n-(x-d)-1))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   103
      | print_term d (Abs c) = "Abs (\\b"^(str d)^" -> "^(print_term (d + 1) c)^")"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   104
      | print_term d t = print_call d t []
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   105
in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   106
    print_term 0 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   107
end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   108
			 			
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   109
fun print_rule arity_of (p, t) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   110
    let	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   111
	fun str x = Int.toString x		    
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   112
	fun print_pattern top n PVar = (n+1, "x"^(str n))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   113
	  | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   114
	  | print_pattern top n (PConst (c, args)) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   115
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   116
		val (n,s) = print_pattern_list (n, (if top then "c" else "C")^(str c)) args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   117
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   118
		(n, if top then s else "("^s^")")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   119
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   120
	and print_pattern_list r [] = r
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   121
	  | print_pattern_list (n, p) (t::ts) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   122
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   123
		val (n, t) = print_pattern false n t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   124
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   125
		print_pattern_list (n, p^" "^t) ts
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   126
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   127
	val (n, pattern) = print_pattern true 0 p
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   128
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   129
	pattern^" = "^(print_term arity_of n t)	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   130
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   131
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   132
fun group_rules rules =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   133
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   134
	fun add_rule (r as (PConst (c,_), _)) groups =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   135
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   136
		val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   137
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   138
		Inttab.update (c, r::rs) groups
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   139
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   140
	  | add_rule _ _ = raise Compile "internal error group_rules"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   141
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   142
	fold_rev add_rule rules Inttab.empty
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   143
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   144
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   145
fun haskell_prog name rules = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   146
    let
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
   147
	val buffer = Unsynchronized.ref ""
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   148
	fun write s = (buffer := (!buffer)^s)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   149
	fun writeln s = (write s; write "\n")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   150
	fun writelist [] = ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   151
	  | writelist (s::ss) = (writeln s; writelist ss)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   152
	fun str i = Int.toString i
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   153
	val (arity, rules) = adjust_rules rules
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   154
	val rules = group_rules rules
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   155
	val constants = Inttab.keys arity
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   156
	fun arity_of c = Inttab.lookup arity c
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   157
	fun rep_str s n = concat (rep n s)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   158
	fun indexed s n = s^(str n)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   159
	fun section n = if n = 0 then [] else (section (n-1))@[n-1]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   160
	fun make_show c = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   161
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   162
		val args = section (the (arity_of c))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   163
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   164
		"  show ("^(indexed "C" c)^(concat (map (indexed " a") args))^") = "
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   165
		^"\""^(indexed "C" c)^"\""^(concat (map (fn a => "++(show "^(indexed "a" a)^")") args))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   166
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   167
	fun default_case c = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   168
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   169
		val args = concat (map (indexed " x") (section (the (arity_of c))))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   170
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   171
		(indexed "c" c)^args^" = "^(indexed "C" c)^args
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   172
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   173
	val _ = writelist [        
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   174
		"module "^name^" where",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   175
		"",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   176
		"data Term = Const Integer | App Term Term | Abs (Term -> Term)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   177
		"         "^(concat (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)),
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   178
		"",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   179
		"instance Show Term where"]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   180
	val _ = writelist (map make_show constants)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   181
	val _ = writelist [
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   182
		"  show (Const c) = \"c\"++(show c)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   183
		"  show (App a b) = \"A\"++(show a)++(show b)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   184
		"  show (Abs _) = \"L\"",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   185
		""]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   186
	val _ = writelist [
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   187
		"app (Abs a) b = a b",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   188
		"app a b = App a b",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   189
		"",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   190
		"calc s c = writeFile s (show c)",
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   191
		""]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   192
	fun list_group c = (writelist (case Inttab.lookup rules c of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   193
					   NONE => [default_case c, ""] 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   194
					 | SOME (rs as ((PConst (_, []), _)::rs')) => 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   195
					   if not (null rs') then raise Compile "multiple declaration of constant"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   196
					   else (map (print_rule arity_of) rs) @ [""]
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   197
					 | SOME rs => (map (print_rule arity_of) rs) @ [default_case c, ""]))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   198
	val _ = map list_group constants
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   199
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   200
	(arity, !buffer)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   201
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   202
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
   203
val guid_counter = Unsynchronized.ref 0
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   204
fun get_guid () = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   205
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   206
	val c = !guid_counter
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   207
	val _ = guid_counter := !guid_counter + 1
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   208
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   209
	(LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   210
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   211
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   212
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   213
fun wrap s = "\""^s^"\""
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   214
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   215
fun writeTextFile name s = File.write (Path.explode name) s
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   216
    
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30161
diff changeset
   217
val ghc = Unsynchronized.ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   218
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   219
fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   220
25520
e123c81257a5 improvements
obua
parents: 25217
diff changeset
   221
fun compile cache_patterns const_arity eqs = 
23663
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   222
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   223
	val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   224
	val eqs = map (fn (a,b,c) => (b,c)) eqs
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   225
	val guid = get_guid ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   226
	val module = "AMGHC_Prog_"^guid
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   227
	val (arity, source) = haskell_prog module eqs
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   228
	val module_file = tmp_file (module^".hs")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   229
	val object_file = tmp_file (module^".o")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   230
	val _ = writeTextFile module_file source
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   231
	val _ = system ((!ghc)^" -c "^module_file)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   232
	val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   233
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   234
	(guid, module_file, arity)	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   235
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   236
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   237
fun readResultFile name = File.read (Path.explode name) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   238
			  			  			      			    
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   239
fun parse_result arity_of result =
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   240
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   241
	val result = String.explode result
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   242
	fun shift NONE x = SOME x
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   243
	  | shift (SOME y) x = SOME (y*10 + x)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   244
	fun parse_int' x (#"0"::rest) = parse_int' (shift x 0) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   245
	  | parse_int' x (#"1"::rest) = parse_int' (shift x 1) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   246
	  | parse_int' x (#"2"::rest) = parse_int' (shift x 2) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   247
	  | parse_int' x (#"3"::rest) = parse_int' (shift x 3) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   248
	  | parse_int' x (#"4"::rest) = parse_int' (shift x 4) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   249
	  | parse_int' x (#"5"::rest) = parse_int' (shift x 5) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   250
	  | parse_int' x (#"6"::rest) = parse_int' (shift x 6) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   251
	  | parse_int' x (#"7"::rest) = parse_int' (shift x 7) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   252
	  | parse_int' x (#"8"::rest) = parse_int' (shift x 8) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   253
	  | parse_int' x (#"9"::rest) = parse_int' (shift x 9) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   254
	  | parse_int' x rest = (x, rest)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   255
	fun parse_int rest = parse_int' NONE rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   256
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   257
	fun parse (#"C"::rest) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   258
	    (case parse_int rest of 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   259
		 (SOME c, rest) => 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   260
		 let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   261
		     val (args, rest) = parse_list (the (arity_of c)) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   262
		     fun app_args [] t = t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   263
		       | app_args (x::xs) t = app_args xs (App (t, x))
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   264
		 in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   265
		     (app_args args (Const c), rest)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   266
		 end		     
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   267
	       | (NONE, rest) => raise Run "parse C")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   268
	  | parse (#"c"::rest) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   269
	    (case parse_int rest of
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   270
		 (SOME c, rest) => (Const c, rest)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   271
	       | _ => raise Run "parse c")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   272
	  | parse (#"A"::rest) = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   273
	    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   274
		val (a, rest) = parse rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   275
		val (b, rest) = parse rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   276
	    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   277
		(App (a,b), rest)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   278
	    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   279
	  | parse (#"L"::rest) = raise Run "there may be no abstraction in the result"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   280
	  | parse _ = raise Run "invalid result"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   281
	and parse_list n rest = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   282
	    if n = 0 then 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   283
		([], rest) 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   284
	    else 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   285
		let 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   286
		    val (x, rest) = parse rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   287
		    val (xs, rest) = parse_list (n-1) rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   288
		in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   289
		    (x::xs, rest)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   290
		end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   291
	val (parsed, rest) = parse result
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   292
	fun is_blank (#" "::rest) = is_blank rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   293
	  | is_blank (#"\n"::rest) = is_blank rest
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   294
	  | is_blank [] = true
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   295
	  | is_blank _ = false
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   296
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   297
	if is_blank rest then parsed else raise Run "non-blank suffix in result file"	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   298
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   299
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   300
fun run (guid, module_file, arity) t = 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   301
    let
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   302
	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
   303
	fun arity_of c = Inttab.lookup arity c			 
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   304
	val callguid = get_guid()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   305
	val module = "AMGHC_Prog_"^guid
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   306
	val call = module^"_Call_"^callguid
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   307
	val result_file = tmp_file (module^"_Result_"^callguid^".txt")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   308
	val call_file = tmp_file (call^".hs")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   309
	val term = print_term arity_of 0 t
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   310
	val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   311
	val _ = writeTextFile call_file call_source
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   312
	val _ = system ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   313
	val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   314
	val t' = parse_result arity_of result
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   315
	val _ = OS.FileSys.remove call_file
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   316
	val _ = OS.FileSys.remove result_file
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   317
    in
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   318
	t'
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   319
    end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   320
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   321
	
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   322
fun discard _ = ()
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   323
		 	  
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   324
end
84b5c89b8b49 new version of computing oracle
obua
parents:
diff changeset
   325