Commit 62cc26e2 authored by Heiko Becker's avatar Heiko Becker
Browse files

Minor changes to translation script

parent de713a0d
...@@ -2,7 +2,7 @@ open preamble ...@@ -2,7 +2,7 @@ open preamble
open simpLib realTheory realLib RealArith open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib realProgTheory; open ml_translatorTheory ml_translatorLib realProgTheory;
open abbrevsTheory expressionsTheory RealSimpsTheory open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
open CertificateCheckerTheory open CertificateCheckerTheory
...@@ -11,16 +11,6 @@ val _ = new_theory "trans"; ...@@ -11,16 +11,6 @@ val _ = new_theory "trans";
val _ = translation_extends "realProg"; val _ = translation_extends "realProg";
(*
TODO:
- for fast EVAL and good ML code, use sptrees to represent sets of
natural numbers (sptreeTheory in HOL) use type `:num_set` which is
an abbreviation for `:unit spt`
*)
(* for recursive translation *) (* for recursive translation *)
fun def_of_const tm = let fun def_of_const tm = let
...@@ -42,8 +32,6 @@ val _ = (find_def_for_const := def_of_const); ...@@ -42,8 +32,6 @@ val _ = (find_def_for_const := def_of_const);
(* / for recursive translation *) (* / for recursive translation *)
val _ = translate IntervalValidationTheory.freeVars_def
val divideInterval_v_thm = translate divideInterval_def; val divideInterval_v_thm = translate divideInterval_def;
val supersetInterval_v_thm = translate isSupersetInterval_def; val supersetInterval_v_thm = translate isSupersetInterval_def;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment