Commit 4ee074cf authored by Heiko Becker's avatar Heiko Becker
Browse files

Make top hol4 directory compile with new preambleFloVer

parent 9ee1c9d0
......@@ -3,7 +3,7 @@
**)
open realTheory realLib sptreeTheory
open MachineTypeTheory
open preamble
open preambleFloVer
val _ = new_theory "Abbrevs";
(**
......
......@@ -10,7 +10,7 @@ open AbbrevsTheory ExpressionsTheory FloverTactics ExpressionAbbrevsTheory
RealRangeArithTheory IntervalValidationTheory ErrorValidationTheory
ssaPrgsTheory FPRangeValidatorTheory TypeValidatorTheory FloverMapTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "CertificateChecker";
val _ = temp_overload_on("abs",``real$abs``);
......
open RealIntervalInferenceTheory ErrorIntervalInferenceTheory ExpressionsTheory
FloverMapTheory TypeValidatorTheory CommandsTheory AbbrevsTheory
ExpressionAbbrevsTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "CertificateGenerator";
......
(**
Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
**)
open simpLib realTheory realLib RealArith
open simpLib realTheory realLib RealArith;
open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory
ExpressionSemanticsTheory MachineTypeTheory;
open preamble
open preambleFloVer;
val _ = new_theory "Commands";
......
open simpLib realTheory realLib RealArith sptreeTheory;
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory
FloverTactics FloverMapTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "Environments";
......
......@@ -6,7 +6,7 @@ Bounds are exprlained in section 5, Deriving Computable Error Bounds
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
FloverTactics MachineTypeTheory ExpressionAbbrevsTheory EnvironmentsTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "ErrorBounds";
......
......@@ -13,7 +13,7 @@ open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
TypeValidatorTheory IntervalValidationTheory EnvironmentsTheory
RealIntervalInferenceTheory
CommandsTheory ssaPrgsTheory FloverMapTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "ErrorIntervalInference";
......
......@@ -12,7 +12,7 @@ open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
TypeValidatorTheory IntervalValidationTheory EnvironmentsTheory
CommandsTheory ssaPrgsTheory FloverMapTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "ErrorValidation";
......@@ -217,18 +217,19 @@ val validErrorboundCorrectVariable = store_thm (
\\ irule computeError_up
\\ irule contained_leq_maxAbs \\ fs[contained_def, IVlo_def, IVhi_def]);
val validErrorboundCorrectConstant_eval = store_thm (
"validErrorboundCorrectConstant_eval",
``!(E:env) (n nR:real) m Gamma.
Theorem validErrorboundCorrectConstant_eval:
!(E:env) (n nR:real) m Gamma.
validTypes (Const m n) Gamma ==>
? nF m1.
eval_Fin E Gamma (Const m n) nF m1``,
eval_Fin E Gamma (Const m n) nF m1
Proof
rpt strip_tac \\ fs[validTypes_def]
\\ qexistsl_tac [`perturb n m (mTypeToR m)`,`m`] \\ irule Const_dist'
\\ fs[]
\\ qexists_tac `mTypeToR m`
\\ fs[mTypeToR_def, realTheory.abs]
\\ Cases_on `m` \\ fs[mTypeToR_pos]);
\\ Cases_on `m` \\ fs[mTypeToR_pos]
QED
val validErrorboundCorrectConstant = store_thm (
"validErrorboundCorrectConstant",
......
......@@ -4,7 +4,7 @@
dependency
**)
open FloverMapTheory ExpressionsTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "ExpressionAbbrevs";
......
(**
Formalization of the base expression language for the flover framework
**)
open miscTheory realTheory realLib sptreeTheory
open AbbrevsTheory MachineTypeTheory FloverTactics ExpressionsTheory
open ExpressionAbbrevsTheory
open preamble
open realTheory realLib sptreeTheory;
open AbbrevsTheory MachineTypeTheory FloverTactics ExpressionsTheory;
open ExpressionAbbrevsTheory;
open preambleFloVer;
val _ = new_theory "ExpressionSemantics";
......
(**
Formalization of the base expression language for the flover framework
**)
open miscTheory realTheory realLib sptreeTheory
open realTheory realLib sptreeTheory
open AbbrevsTheory MachineTypeTheory FloverTactics
open preamble
open preambleFloVer;
val _ = new_theory "Expressions";
......
......@@ -14,7 +14,7 @@ open AbbrevsTheory MachineTypeTheory TypeValidatorTheory RealSimpsTheory
ExpressionAbbrevsTheory ExpressionSemanticsTheory FloverTactics
IntervalValidationTheory ErrorValidationTheory CommandsTheory
EnvironmentsTheory ssaPrgsTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "FPRangeValidator";
......
open MachineTypeTheory ExpressionsTheory FloverTactics
open preamble
open preambleFloVer;
val _ = new_theory "FloverMap";
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra \
$(CAKEMLDIR)/translator $(CAKEMLDIR)/basis \
$(CAKEMLDIR)/characteristic $(CAKEMLDIR)/misc
INCLUDES = Infra
OPTIONS = QUIT_ON_FAILURE
#ifdef POLY
#HOLHEAP = heap
#EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
#all: $(HOLHEAP)
#
#THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
#TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
#TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
#
#all: $(TARGETS) $(HOLHEAP)
#
#.PHONY: all
#
#BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
# alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib \
# combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs \
# listTheory llistTheory markerLib realTheory realLib RealArith\
# optionTheory pairLib pairTheory pred_setTheory \
# quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
# sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
# simpLib realTheory realLib RealArith \
# cakeml/translator/ml_translatorLib \
# cakeml/basis/basis_ffiLib
#
#DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
#
#$(HOLHEAP): $(DEPS)
# $(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
#endif
......@@ -5,7 +5,7 @@ open MachineTypeTheory ExpressionsTheory RealSimpsTheory FloverTactics
ExpressionSemanticsTheory FloverMapTheory RealRangeArithTheory
TypeValidatorTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
CommandsTheory ssaPrgsTheory EnvironmentsTheory FloverMapTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "IEEE_connection";
......
......@@ -4,7 +4,7 @@
**)
open realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics;
open preamble
open preambleFloVer;
val _ = new_theory "IntervalArith";
......
......@@ -11,7 +11,7 @@ open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics
ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
MachineTypeTheory FloverMapTheory TypeValidatorTheory RealRangeArithTheory
ExpressionSemanticsTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "IntervalValidation";
......
......@@ -11,7 +11,7 @@ open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics
ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
MachineTypeTheory FloverMapTheory TypeValidatorTheory RealRangeArithTheory
ExpressionSemanticsTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "RealIntervalInference";
......
open FloverTactics AbbrevsTheory RealSimpsTheory TypeValidatorTheory
ExpressionSemanticsTheory ssaPrgsTheory IntervalArithTheory CommandsTheory;
open preamble;
open preambleFloVer;
val _ = new_theory "RealRangeArith";
......
open miscTheory realTheory realLib sptreeTheory;
open realTheory realLib sptreeTheory;
open ExpressionsTheory MachineTypeTheory FloverTactics ExpressionAbbrevsTheory
ExpressionSemanticsTheory CommandsTheory FloverMapTheory ResultsTheory;
open ResultsLib;
open preamble;
open preambleFloVer;
val _ = new_theory "TypeValidator";
......
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