src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 62826 eb94e570c1a4
parent 62735 23de054397e5
child 63518 ae8fd6fe63a1
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4  
     1.5  fun normalize_scores _ [] = []
     1.6    | normalize_scores max_facts xs =
     1.7 -    map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
     1.8 +    map (apsnd (curry (op *) (1.0 / avg (map snd (take max_facts xs))))) xs
     1.9  
    1.10  fun mesh_facts maybe_distinct _ max_facts [(_, (sels, unks))] =
    1.11      map fst (take max_facts sels) @ take (max_facts - length sels) unks
    1.12 @@ -655,7 +655,7 @@
    1.13      (case try OS.FileSys.modTime (File.platform_path path) of
    1.14        NONE => time_state
    1.15      | SOME disk_time =>
    1.16 -      if Time.>= (memory_time, disk_time) then
    1.17 +      if memory_time >= disk_time then
    1.18          time_state
    1.19        else
    1.20          (disk_time,
    1.21 @@ -700,7 +700,7 @@
    1.22        val dirty_facts' =
    1.23          (case try OS.FileSys.modTime (File.platform_path path) of
    1.24            NONE => NONE
    1.25 -        | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE)
    1.26 +        | SOME disk_time => if disk_time <= memory_time then dirty_facts else NONE)
    1.27        val (banner, entries) =
    1.28          (case dirty_facts' of
    1.29            SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
    1.30 @@ -1278,7 +1278,7 @@
    1.31    let
    1.32      val hard_timeout = time_mult learn_timeout_slack timeout
    1.33      val birth_time = Time.now ()
    1.34 -    val death_time = Time.+ (birth_time, hard_timeout)
    1.35 +    val death_time = birth_time + hard_timeout
    1.36      val desc = ("Machine learner for Sledgehammer", "")
    1.37    in
    1.38      Async_Manager_Legacy.thread MaShN birth_time death_time desc task
    1.39 @@ -1328,7 +1328,7 @@
    1.40      learn_timeout facts =
    1.41    let
    1.42      val timer = Timer.startRealTimer ()
    1.43 -    fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
    1.44 +    fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout
    1.45  
    1.46      val {access_G, ...} = peek_state ctxt
    1.47      val is_in_access_G = is_fact_in_graph access_G o snd
    1.48 @@ -1408,11 +1408,11 @@
    1.49                val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
    1.50                val learns = (name, parents, feats, deps) :: learns
    1.51                val (learns, next_commit) =
    1.52 -                if Time.> (Timer.checkRealTimer timer, next_commit) then
    1.53 +                if Timer.checkRealTimer timer > next_commit then
    1.54                    (commit false learns [] []; ([], next_commit_time ()))
    1.55                  else
    1.56                    (learns, next_commit)
    1.57 -              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
    1.58 +              val timed_out = Timer.checkRealTimer timer > learn_timeout
    1.59              in
    1.60                (learns, (num_nontrivial, next_commit, timed_out))
    1.61              end
    1.62 @@ -1443,11 +1443,11 @@
    1.63                    SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
    1.64                  | NONE => (num_nontrivial, relearns, name :: flops))
    1.65                val (relearns, flops, next_commit) =
    1.66 -                if Time.> (Timer.checkRealTimer timer, next_commit) then
    1.67 +                if Timer.checkRealTimer timer > next_commit then
    1.68                    (commit false [] relearns flops; ([], [], next_commit_time ()))
    1.69                  else
    1.70                    (relearns, flops, next_commit)
    1.71 -              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
    1.72 +              val timed_out = Timer.checkRealTimer timer > learn_timeout
    1.73              in
    1.74                ((relearns, flops), (num_nontrivial, next_commit, timed_out))
    1.75              end