--- a/src/HOL/Matrix/Compute_Oracle/am.ML Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am.ML Fri Feb 10 23:12:57 2012 +0100
@@ -13,7 +13,7 @@
(* The de-Bruijn index 0 occurring on the right hand side refers to the LAST pattern variable, when traversing the pattern from left to right,
1 to the second last, and so on. *)
-val compile : pattern list -> (int -> int option) -> (guard list * pattern * term) list -> program
+val compile : (guard list * pattern * term) list -> program
val discard : program -> unit
--- a/src/HOL/Matrix/Compute_Oracle/am_compiler.ML Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_compiler.ML Fri Feb 10 23:12:57 2012 +0100
@@ -190,7 +190,7 @@
| SOME r => (compiled_rewriter := NONE; r)
end
-fun compile _ _ eqs =
+fun compile eqs =
let
val _ = if exists (fn (a,_,_) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
val eqs = map (fn (_,b,c) => (b,c)) eqs
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Fri Feb 10 23:12:57 2012 +0100
@@ -216,7 +216,7 @@
fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
-fun compile _ _ eqs =
+fun compile eqs =
let
val _ = if exists (fn (a,_,_) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
val eqs = map (fn (_,b,c) => (b,c)) eqs
--- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML Fri Feb 10 23:12:57 2012 +0100
@@ -100,7 +100,7 @@
| check_freevars free (Abs m) = check_freevars (free+1) m
| check_freevars free (Computed t) = check_freevars free t
-fun compile _ _ eqs =
+fun compile eqs =
let
fun check p r = if check_freevars p r then () else raise Compile ("unbound variables in rule")
fun check_guard p (Guard (a,b)) = (check p a; check p b)
--- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML Fri Feb 10 23:12:57 2012 +0100
@@ -490,7 +490,7 @@
fun use_source src = use_text ML_Env.local_context (1, "") false src
-fun compile _ _ eqs =
+fun compile eqs =
let
val guid = get_guid ()
val code = Real.toString (random ())
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Feb 10 23:12:57 2012 +0100
@@ -297,24 +297,14 @@
(encoding, p::cache_patterns)
end
- val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
-
- fun arity (Type ("fun", [_, b])) = 1 + arity b
- | arity _ = 0
-
- fun make_arity (Const (s, _), i) tab =
- (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
- | make_arity _ tab = tab
-
- val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
- fun const_arity x = Inttab.lookup const_arity_tab x
+ val (encoding, _) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
val prog =
case machine of
- BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
- | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
- | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
- | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
+ BARRAS => ProgBarras (AM_Interpreter.compile rules)
+ | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile rules)
+ | HASKELL => ProgHaskell (AM_GHC.compile rules)
+ | SML => ProgSML (AM_SML.compile rules)
fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))