Commit a034407f authored by Heiko Becker's avatar Heiko Becker
Browse files

Start fixing parsers to get full build process working again

parent f89e7d8e
Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List Coq.Reals.Reals.
Require Import CertificateChecker.
Require Import CertificateChecker Infra.MachineType.
Import Coq.Lists.List.ListNotations.
......@@ -10,6 +10,8 @@ Inductive Token:Type :=
| DPRE
| DABS
| DCOND
| DGAMMA
| DTYPE:mType -> Token
| DVAR
| DCONST: N -> Token
| DNEG
......@@ -92,6 +94,14 @@ match fuel with
| "PRE" => DPRE :: lex input'' fuel'
| "ABS" => DABS :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| "MTYPE" => let ts := lex input'' fuel' in
(match ts with
|DCONST 32 :: ts' => DTYPE M32 :: ts'
|DCONST 64 :: ts' => DTYPE M64 :: ts'
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => []
end)
| _ => []
end
else
......@@ -120,6 +130,13 @@ Fixpoint str_of_num (n:nat) (m:nat):=
|_ => ""
end .
Fixpoint type_to_string (m:mType) :=
match m with
|M32 => "MTYPE 32"
|M64 => "MTYPE 64"
| _ => "" (* FIXME *)
end.
(*
Definition pp_token (token:Token) :=
match token with
......@@ -156,15 +173,15 @@ Fixpoint parseExp (tokList:list Token) (fuel:nat):option (exp Q * list Token) :=
match fuel with
|S fuel' =>
match tokList with
| DCONST n :: DFRAC :: DCONST m :: tokRest =>
| DTYPE t :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
match m with
|N0 => None
|Npos p => Some (Const (Z.of_N n # p), tokRest)
|Npos p => Some (Const t (Z.of_N n # p), tokRest)
end
| DVAR :: DCONST n :: tokRest => Some (Var Q (N.to_nat n), tokRest)
| DNEG :: tokRest =>
match (parseExp tokRest fuel') with
| Some (Const c, tokRest) => Some (Const (- c), tokRest)
| Some (Const m c, tokRest) => Some (Const m (- c), tokRest)
| Some (e1,tokRest') => Some (Unop Neg e1, tokRest')
| None => None
end
......@@ -220,7 +237,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
|S fuel' =>
match input with
(* We already have a valid let binding *)
| DVAR :: DCONST n :: expLetRest =>
| DVAR :: DTYPE m :: DCONST n :: expLetRest =>
(* so we parse an expression *)
match parseExp expLetRest fuel with
| Some (e, letRest) =>
......@@ -230,7 +247,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
(* Parse it *)
match (parseLet letBodyRest fuel') with
(* And construct a result from it *)
| Some (letCmd, arbRest) => Some (Let (N.to_nat n) e letCmd, arbRest)
| Some (letCmd, arbRest) => Some (Let m (N.to_nat n) e letCmd, arbRest)
| _ => None
end
(* But if we have a return *)
......@@ -238,7 +255,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
(* parse only this *)
match (parseRet retBodyRest fuel) with
(* and construct the result *)
| Some (retCmd, arbRest) => Some (Let (N.to_nat n) e retCmd, arbRest)
| Some (retCmd, arbRest) => Some (Let m (N.to_nat n) e retCmd, arbRest)
| _ => None
end
| _ => None (* fail if there is no continuation for the let *)
......@@ -312,7 +329,7 @@ Definition parsePrecond (input :list Token) fuel :=
Definition defaultAbsenv:analysisResult := fun e => (mkIntv 0 0 ,0).
Definition updAbsenv (e:exp Q) (iv:intv) (err:Q) (A:analysisResult):=
fun e' => if expEqBool e e' then (iv, err) else A e'.
fun e' => if expEq e e' then (iv, err) else A e'.
(** Abstract environment parser:
The abstract environment should be encoded in the following format:
......@@ -351,6 +368,24 @@ Definition parseAbsEnv (input:list Token) fuel :=
| _ => None
end.
Definition defaultGamma := fun n:nat => None:option mType.
Fixpoint parseGammaRec (input: list Token) : option ((nat -> option mType) * list Token) :=
match input with
| DVAR :: DCONST n :: DTYPE m :: inputRest =>
match parseGammaRec inputRest with
| Some (Gamma, rest) => Some (updDefVars (N.to_nat n) m Gamma, rest)
| None => None
end
| _ => Some (defaultGamma, input)
end.
Definition parseGamma (input:list Token) :=
match input with
| DGAMMA :: tokenRest => parseGammaRec tokenRest
| _ => None
end.
Definition dParse (input:list Token) fuel :=
let cmdParse :=
match input with
......@@ -365,20 +400,80 @@ Definition dParse (input:list Token) fuel :=
| DPRE :: preRest =>
match parsePrecond tokRest fuel with
| Some (P, absenvRest) =>
match parseAbsEnv absenvRest fuel with
| Some (A, residual) => Some ((dCmd, P, A), residual)
match absenvRest with
| DABS :: absRest =>
match parseAbsEnv absRest fuel with
| Some (A, residual) =>
match parseGamma residual with
| Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
end
| DGAMMA :: absRest =>
match parseGamma absRest with
| Some (Gamma, residual) =>
match parseAbsEnv residual fuel with
| Some (A,residual) => Some ((dCmd, P, A, Gamma), residual)
| _ => None
end
| _ => None
end
| _ => None
end
| None => None
| _ => None
end
| DABS :: absRest =>
match parseAbsEnv tokRest fuel with
| Some (A, precondRest) =>
match parsePrecond precondRest fuel with
| Some (P, residual) => Some ((dCmd, P, A),residual)
| Some (A, absenvRest) =>
match absenvRest with
| DPRE :: absRest =>
match parsePrecond absRest fuel with
| Some (P, residual) =>
match parseGamma residual with
| Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
end
| DGAMMA :: absRest =>
match parseGamma absRest with
| Some (Gamma, residual) =>
match parsePrecond residual fuel with
| Some (P,residual) => Some ((dCmd, P, A, Gamma), residual)
| _ => None
end
| _ => None
end
| _ => None
end
| _ => None
end
| DGAMMA :: absRest =>
match parseGamma tokRest with
| Some (Gamma, absenvRest) =>
match absenvRest with
| DPRE :: absRest =>
match parsePrecond absRest fuel with
| Some (P, residual) =>
match parseAbsEnv residual fuel with
| Some (A, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
end
| DABS :: absRest =>
match parseAbsEnv absRest fuel with
| Some (A, residual) =>
match parsePrecond residual fuel with
| Some (P,residual) => Some ((dCmd, P, A, Gamma), residual)
| _ => None
end
| _ => None
end
| _ => None
end
| None => None
| _ => None
end
| _ => None
end
......@@ -389,12 +484,12 @@ Fixpoint check_rec (input:list Token) (num_fun:nat) fuel:=
match num_fun with
| S n' =>
match dParse input fuel with
| Some ((dCmd, P, A), []) =>
if CertificateCheckerCmd dCmd A P
| Some ((dCmd, P, A, Gamma), []) =>
if CertificateCheckerCmd dCmd A P Gamma
then "True\n"
else "False\n"
| Some ((dCmd, P, A), residual) =>
if CertificateCheckerCmd dCmd A P
| Some ((dCmd, P, A, Gamma), residual) =>
if CertificateCheckerCmd dCmd A P Gamma
then check_rec residual n' fuel
else "False\n"
| None => "parse failure\n"
......@@ -408,9 +503,9 @@ Fixpoint str_length s :=
|"" => O
end.
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) (n:nat) :=
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma (n:nat) :=
match n with
|S n' => CertificateCheckerCmd f A P && (check f P A n')
|S n' => CertificateCheckerCmd f A P Gamma && (check f P A Gamma n')
|_ => true
end.
......@@ -418,8 +513,8 @@ Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
match num_fun with
|S nf =>
match (dParse input fuel) with
|Some ((f,P,A), residual) =>
if (check f P A iters)
|Some ((f,P,A, Gamma), residual) =>
if (check f P A Gamma iters)
then
match residual with
|a :: b => check_all nf iters residual fuel
......
......@@ -82,8 +82,8 @@ val lex_def = tDefine "lex" `
(case ts of
| DCONST 32 :: ts' => DTYPE M32 :: ts'
| DCONST 64 :: ts' => DTYPE M64 :: ts'
| DCONST 128 :: ts' => DTYPE M128 :: ts'
| DCONST 256 :: ts' => DTYPE M256 :: ts'
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => NIL)
| "Gamma" => DGAMMA :: lex input''
| _ => NIL
......@@ -113,40 +113,41 @@ val str_of_num_def = Define `
val type_to_string = Define `
(type_to_string (M32) = "MTYPE 32") /\
(type_to_string (M64) = "MTYPE 64") /\
(type_to_string (M128) = "MTYPE 128") /\
(type_to_string (M256) = "MTYPE 256")`;
val pp_token_def = Define `
pp_token (token:Token) =
case token of
| DLET => "Let"
| DRET => "Ret"
| DPRE => "PRE"
| DABS => "ABS"
| DCOND => "?"
| DGAMMA => "Gamma"
| DTYPE m => type_to_string m
| DVAR => "Var"
| DCONST num => str_of_num num
| DNEG => "~"
| DPLUS => "+"
| DSUB => "-"
| DMUL => "*"
| DDIV => "/"
| DFRAC => "#"`;
(type_of_string (_) = "FAIL"); (* FIXME *)
(* (type_to_string (M128) = "MTYPE 128") /\ *)
(* (type_to_string (M256) = "MTYPE 256")`; *)
(* val pp_token_def = Define ` *)
(* pp_token (token:Token) = *)
(* case token of *)
(* | DLET => "Let" *)
(* | DRET => "Ret" *)
(* | DPRE => "PRE" *)
(* | DABS => "ABS" *)
(* | DCOND => "?" *)
(* | DGAMMA => "Gamma" *)
(* | DTYPE m => type_to_string m *)
(* | DVAR => "Var" *)
(* | DCONST num => str_of_num num *)
(* | DNEG => "~" *)
(* | DPLUS => "+" *)
(* | DSUB => "-" *)
(* | DMUL => "*" *)
(* | DDIV => "/" *)
(* | DFRAC => "#"`; *)
(* val pp_token_correct = store_thm ("pp_token_correct", *)
(* ``!t. lex (pp_token t) = [t]``, *)
(* Induct_on `t` \\ EVAL_TAC fs[pp_token_def, lex_def] *)
(* ); *)
val str_join_def = Define `
(str_join (STRING c s1) s2 = STRING c (str_join s1 s2)) /\
(str_join "" s2 = s2)`;
(* val str_join_def = Define ` *)
(* (str_join (STRING c s1) s2 = STRING c (str_join s1 s2)) /\ *)
(* (str_join "" s2 = s2)`; *)
val str_join_empty = store_thm ("str_join_empty",
``!s. str_join s "" = s``,
Induct \\ fs[str_join_def]);
(* val str_join_empty = store_thm ("str_join_empty", *)
(* ``!s. str_join s "" = s``, *)
(* Induct \\ fs[str_join_def]); *)
(* Pretty Printer for Tokens *)
val pp_def = Define `
......
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