Commit 1636dcb5 authored by Heiko Becker's avatar Heiko Becker

Start working on lexer and parser, fix Holmakefile which has been broken by merge

parent c6dc52d4
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......@@ -19,6 +19,7 @@ BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith \
cakeml/translator/ml_translatorLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
......
open preamble
open simpLib realTheory realLib RealArith
open ml_translatorTheory ml_translatorLib realProgTheory;
open stringTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory DaisyTactics
......@@ -11,7 +12,194 @@ val _ = new_theory "trans";
val _ = translation_extends "realProg";
val _ = translate lookup_def
val _ = translate lookup_def;
val _ = Datatype `
Token =
| DLET
| DRET
| DPRE
| DABS
| DCOND
| DVAR
| DCONST num
| DNEG
| DPLUS
| DSUB
| DMUL
| DDIV
| DFRAC`;
val getChar_def = Define `
getChar input =
case input of
| "" => CHR 0
| STRING c input' => c`;
val getConst_def = Define `
getConst (c:char) = ORD c - 48`;
val suffix_def = Define `
suffix s = case s of
| STRING c s' => s'
| "" => ""`;
val lexConst_def = Define`
lexConst (input:tvarN) (akk:num) =
case input of
| STRING char input' =>
if (isDigit char)
then lexConst input' (akk * 10 + (getConst char))
else (akk, input')
|"" => (akk, input)`;
val lexName_def = Define `
lexName (input:tvarN) =
case input of
| STRING char input' =>
if (isAlphaNum char)
then
let (name, input') = lexName input' in
(STRING char name, input')
else ("", input)
| "" => ("","")`;
val strSize_def = Define `strSize str =
case str of
| STRING _ str' => 1 + strSize str'
| "" => 0`;
val lex_def = Define `
lex input fuel =
case fuel of
| SUC fuel' =>
(case input of
| STRING char input' =>
if isDigit char
then
let (num, input'') = lexConst input 0 in
DCONST num :: lex input'' fuel'
else
if isAlpha char
then
let (name, input'') = lexName input in
case name of
| "Ret" => DRET :: lex input'' fuel'
| "Let" => DLET :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| _ => NIL
else
(case char of
| #"+" => DPLUS :: lex input' fuel'
| #"-" => DSUB :: lex input' fuel'
| #"*" => DMUL :: lex input' fuel'
| #"/" => DDIV :: lex input' fuel'
| #"#" => DFRAC :: lex input' fuel'
| #"?" => DCOND :: lex input' fuel'
| #"~" => DNEG :: lex input' fuel'
| #" " => lex input' fuel'
| _ => NIL)
| _ => NIL)
| _ => NIL`;
(* Prefix form parser for expressions *)
val parseExp_def = Define `
parseExp (tokList:Token list) fuel :(real exp # Token list) option =
case fuel of
| SUC fuel' =>
(case tokList of
| DCONST n :: DFRAC :: DCONST m :: tokRest => SOME (Const ((&n):real / &m), tokRest)
| DCONST n :: tokRest => SOME (Const &n, tokRest)
| DVAR :: DCONST n :: tokRest => SOME (Var n, tokRest)
| DNEG :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') => SOME (Unop Neg e1, tokRest')
| NONE => NONE)
| DPLUS :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Plus e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DSUB :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Sub e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DMUL :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Mult e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DDIV :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Div e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE))
| _ => NONE`;
val parseRet_def = Define `
parseRet input fuel :(real cmd # Token list) option =
case parseExp input fuel of
| SOME (e, tokRest) => SOME (Ret e, tokRest)
| NONE => NONE`;
val parseLet_def = Define `
parseLet input fuel:(real cmd # Token list) option =
case fuel of
| SUC fuel' =>
(case input of
(* We have a valid let binding *)
| DVAR :: DCONST n :: expLetRest =>
(* so we parse an expression *)
(case parseExp expLetRest (fuel-1) of
| SOME (e, letRest) =>
(case letRest of
(* If we continue with a let *)
| DLET :: letBodyRest =>
(* Parse it *)
(case (parseLet letRest (fuel - 1)) of
(* And construct a result from it *)
| SOME (letCmd, arbRest) => SOME (Let n e letCmd, arbRest)
| _ => NONE)
(* But if we have a return *)
| DRET :: retBodyRest =>
(* parse only this *)
(case (parseRet letRest (fuel - 1)) of
(* and construct the result *)
| SOME (retCmd, arbRest) => SOME (Let n e retCmd, arbRest)
| _ => NONE)
| _ => NONE) (* fail if there is no continuation for the let *)
| NONE => NONE) (* fail if we do not have an expression to bind *)
| _ => NONE) (* fail if we cannot find a variable *)
| _ => NONE`; (* fail if there is no fuel left *)
(* Global parsing function FIXME: should parse all three definitions (cmd, absenv and precond) or fail otherwise*)
val parse_def = Define `
parse input fuel =
case fuel of
| SUC fuel' =>
(case input of
| DLET :: tokRest => SOME (parseLet tokRest fuel)
| DRET :: tokRest => SOME (parseRet tokRest fuel)
| DPRE :: tokRest => NONE (*SOME (parsePrecond input fuel) *)
| DABS :: tokRest => NONE (*SOME (parseAbsEnv input fuel) *)
| _ => NONE )
| _ => NONE`;
(* TESTING STATEMENTS
EVAL ``case (EXPLODE "abc") of
| STRING c s => SOME c
| "" => ``
EVAL ``CHR 0``
EVAL ``ORD #"0"`` *)
(* for recursive translation *)
......@@ -131,53 +319,57 @@ val precond_validErrorbound_true = prove (``
\\ rpt gen_tac \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ disch_then ASSUME_TAC
\\ rpt gen_tac
\\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ conj_tac
>- (conj_tac \\ first_x_assum match_mp_tac
>- (rpt strip_tac
\\ first_x_assum match_mp_tac
\\ fs [Once validIntervalbounds_def])
>- (disch_then ASSUME_TAC
\\ rpt gen_tac
\\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ rpt gen_tac
\\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ rpt (disch_then ASSUME_TAC)
\\ rveq
\\ rename1 `absenv (Binop Div e1 e2) = (ivDiv, errDiv)`
\\ rename1 `absenv e1 = (ive1,err1)`
\\ Cases_on `ive1` \\ rename1 `absenv e1 = ((e1lo,e1hi), err1)`
\\ rename1 `absenv e2 = (ive2,err2)`
\\ Cases_on `ive2` \\ rename1 `absenv e2 = ((e2lo,e2hi), err2)`
\\ rewrite_tac [divideinterval_side_def, widenInterval_def, minAbsFun_def, invertinterval_side_def, IVlo_def, IVhi_def]
\\ `valid (FST(absenv e1)) /\ valid (FST(absenv e2))`
by (conj_tac \\ drule validIntervalbounds_validates_iv
>- (disch_then match_mp_tac
\\ qexists_tac `P`
\\ fs [Once validIntervalbounds_def])
>- (disch_then match_mp_tac
\\ qexists_tac `P`
\\ fs [Once validIntervalbounds_def]))
\\ rw_asm `absenv e1 = _`
\\ rw_asm `absenv e2 = _`
\\ qpat_x_assum `!v. _` kall_tac
\\ `0 <= err2`
by (drule err_always_positive
\\ disch_then (fn thm => qspecl_then [`e2lo,e2hi`, `err2`] match_mp_tac thm)
\\ fs [])
\\ `e2lo - err2 0 /\ e2hi + err2 0`
by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
\\ conj_tac \\ REAL_ASM_ARITH_TAC)
\\ `noDivzero (SND (FST (absenv e2))) (FST (FST (absenv e2)))`
by (drule validIntervalbounds_noDivzero_real
\\ fs [])
\\ `abs (e2lo - err2) 0 /\ abs (e2hi + err2) 0`
by (REAL_ASM_ARITH_TAC)
\\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) 0`
by (fs [min_def]
\\ Cases_on `abs (e2lo - err2) <= abs (e2hi + err2)`
\\ fs [] \\ REAL_ASM_ARITH_TAC)
\\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
\\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
\\ REAL_ASM_ARITH_TAC));
>- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ conj_tac
>- (conj_tac \\ first_x_assum match_mp_tac
\\ fs [Once validIntervalbounds_def])
>- (disch_then ASSUME_TAC
\\ rpt gen_tac
\\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ rpt gen_tac
\\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ rpt (disch_then ASSUME_TAC)
\\ rveq
\\ rename1 `absenv (Binop Div e1 e2) = (ivDiv, errDiv)`
\\ rename1 `absenv e1 = (ive1,err1)`
\\ Cases_on `ive1` \\ rename1 `absenv e1 = ((e1lo,e1hi), err1)`
\\ rename1 `absenv e2 = (ive2,err2)`
\\ Cases_on `ive2` \\ rename1 `absenv e2 = ((e2lo,e2hi), err2)`
\\ rewrite_tac [divideinterval_side_def, widenInterval_def, minAbsFun_def, invertinterval_side_def, IVlo_def, IVhi_def]
\\ `valid (FST(absenv e1)) /\ valid (FST(absenv e2))`
by (conj_tac \\ drule validIntervalbounds_validates_iv
>- (disch_then match_mp_tac
\\ qexists_tac `P`
\\ fs [Once validIntervalbounds_def])
>- (disch_then match_mp_tac
\\ qexists_tac `P`
\\ fs [Once validIntervalbounds_def]))
\\ rw_asm `absenv e1 = _`
\\ rw_asm `absenv e2 = _`
\\ qpat_x_assum `!v. _` kall_tac
\\ `0 <= err2`
by (drule err_always_positive
\\ disch_then (fn thm => qspecl_then [`e2lo,e2hi`, `err2`] match_mp_tac thm)
\\ fs [])
\\ `e2lo - err2 0 /\ e2hi + err2 0`
by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
\\ conj_tac \\ REAL_ASM_ARITH_TAC)
\\ `noDivzero (SND (FST (absenv e2))) (FST (FST (absenv e2)))`
by (drule validIntervalbounds_noDivzero_real
\\ fs [])
\\ `abs (e2lo - err2) 0 /\ abs (e2hi + err2) 0`
by (REAL_ASM_ARITH_TAC)
\\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) 0`
by (fs [min_def]
\\ Cases_on `abs (e2lo - err2) <= abs (e2hi + err2)`
\\ fs [] \\ REAL_ASM_ARITH_TAC)
\\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
\\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
\\ REAL_ASM_ARITH_TAC)));
val precond_errorbounds_true = prove (``
!P f absenv dVars.
......
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