Skip to content

GitLab

F
FloVer
Commit 121a578e authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Update parsers to properly parse fBits environment

parent 65819a08
Hide whitespace changes
Inline Side-by-side
Showing with 83 additions and 189 deletions
coq/floverParser.v
View file @ 121a578e
......@@ -12,6 +12,7 @@ Inductive Token:Type :=
| DABS
| DCOND
| DGAMMA
| DFBITS
| DTYPE:mType -> Token
| DFIXED
| DVAR
......@@ -22,8 +23,7 @@ Inductive Token:Type :=
| DMUL
| DDIV
| DFRAC
| DCAST
| DFAIL: string -> Token.
| DCAST.
Open Scope string_scope.
......@@ -96,6 +96,7 @@ match fuel with
| "Let" => DLET :: lex input'' fuel'
| "PRE" => DPRE :: lex input'' fuel'
| "ABS" => DABS :: lex input'' fuel'
| "FBITS" => DFBITS :: lex input'' fuel'
| "GAMMA" => DGAMMA :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| "Cast" => DCAST :: lex input'' fuel'
......@@ -124,7 +125,7 @@ match fuel with
| "~"%char => DNEG :: lex input' fuel'
| " "%char => lex input' fuel'
| "010"%char => lex input' fuel'
| _ => DFAIL (String char ("")) :: []
| _ => []
end
| _ => []
end
......@@ -160,6 +161,7 @@ Definition pp_token (token:Token) :=
| DABS => "ABS"
| DCOND => "?"
| DVAR => "Var"
| DFBITS => "FBITS"
| DCONST num => str_of_num num (N.to_nat num)
| DGAMMA => "Gamma"
| DTYPE m => str_join "MTYPE " (type_to_string m)
......@@ -171,7 +173,6 @@ Definition pp_token (token:Token) :=
| DDIV => "/"
| DFRAC => "#"
| DCAST => "Cast"
| DFAIL s => ""
end .
(* Pretty Printer for Tokens *)
......@@ -405,6 +406,33 @@ Definition parseGamma (input:list Token) :=
| _ => None
end.
Definition defaultFBits := FloverMap.empty N.
Fixpoint parseFBitsRec (input: list Token) akk (fuel:nat)
: option (FloverMap.t N * list Token) :=
match fuel with
| 0%nat => None
| S fuel' =>
match input with
|[] => Some (akk, [])
| _ =>
match parseExp input fuel with
| None => Some (akk, input)
| Some (e, res1) =>
match res1 with
|DCONST n :: res2 => parseFBitsRec res2 (FloverMap.add e n akk) fuel'
| _ => Some (akk, input)
end
end
end
end.
Definition parseFBits input fuel :=
match input with
|DFBITS :: tokRest => parseFBitsRec tokRest defaultFBits fuel
|_ => None
end.
Definition dParse (input:list Token) fuel :=
let cmdParse :=
match input with
......@@ -414,106 +442,24 @@ Definition dParse (input:list Token) fuel :=
end
in
match cmdParse with
| None => None
| Some (dCmd, tokRest) =>
match tokRest with
| DPRE :: preRest =>
match parsePrecond tokRest fuel with
match parseGamma tokRest with
| None => None
| Some (Gamma, residual) =>
match parsePrecond residual fuel with
| None => None
| Some (P, absenvRest) =>
match absenvRest with
| DABS :: _ =>
match parseAbsEnv absenvRest fuel with
| Some (A, residual) =>
match parseGamma residual with
| Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
end
| DGAMMA :: _ =>
match parseGamma absenvRest 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
end
| DABS :: _ =>
match parseAbsEnv tokRest fuel with
| Some (A, absenvRest) =>
match absenvRest with
| DPRE :: _ =>
match parsePrecond absenvRest fuel with
| Some (P, residual) =>
match parseGamma residual with
| Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
match parseAbsEnv absenvRest fuel with
| None => None
| Some (A, residual) =>
match parseFBits residual fuel with
|None => None
|Some (fBits, residual) => Some ((dCmd, P, A, Gamma, fBits), residual)
end
| DGAMMA :: _ =>
match parseGamma absenvRest 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 :: _ =>
match parseGamma tokRest with
| Some (Gamma, absenvRest) =>
match absenvRest with
| DPRE :: _ =>
match parsePrecond absenvRest fuel with
| Some (P, residual) =>
match parseAbsEnv residual fuel with
| Some (A, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
end
| DABS :: _ =>
match parseAbsEnv absenvRest 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
end
| _ => None
end
| _ => None
end.
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, Gamma), []) =>
if CertificateCheckerCmd dCmd A P Gamma (FloverMap.empty N)
then "True\n"
else "False\n"
| Some ((dCmd, P, A, Gamma), residual) =>
if CertificateCheckerCmd dCmd A P Gamma (FloverMap.empty N)
then check_rec residual n' fuel
else "False\n"
| None => "parse failure\n"
end
| _ => "failure num of functions given"
end.
Fixpoint str_length s :=
......@@ -522,9 +468,9 @@ Fixpoint str_length s :=
|"" => O
end.
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma (n:nat) :=
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma fBits (n:nat) :=
match n with
|S n' => CertificateCheckerCmd f A P Gamma (FloverMap.empty N) && (check f P A Gamma n')
|S n' => CertificateCheckerCmd f A P Gamma fBits && (check f P A Gamma fBits n')
|_ => true
end.
......@@ -532,8 +478,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, Gamma), residual) =>
if (check f P A Gamma iters)
|Some ((f,P,A, Gamma, fBits), residual) =>
if (check f P A Gamma fBits iters)
then
match residual with
|a :: b => check_all nf iters residual fuel
......@@ -551,4 +497,4 @@ Definition runChecker (input:string) :=
match tokList with
| DCONST n :: DCONST m :: tokRest => check_all (N.to_nat m) (N.to_nat n) tokRest (List.length tokList * 100)
| _ => "failure no num of functions"
end.
end.
\ No newline at end of file
hol4/floverParserScript.sml
View file @ 121a578e
......@@ -455,100 +455,48 @@ val defaultFBits = Define `
val parseFBitsRec_def = tDefine "parseFBitsRec" `
parseFBitsRec (input: Token list) akk =
(case parseExp input of
|NONE => (akk, input)
|SOME (e, res1) =>
(case res1 of
|DCONST n :: res2 => parseFBitsRec res2 (FloverMapTree_insert e n akk)
| _ => (akk, input)))`
(case input of
| [] => SOME (akk, [])
| _ =>
(case parseExp input of
|NONE => SOME (akk, input)
|SOME (e, res1) =>
(case res1 of
|DCONST n :: res2 => parseFBitsRec res2 (FloverMapTree_insert e n akk)
| _ => SOME (akk, input))))`
(WF_REL_TAC `measure (LENGTH o FST)` \\ fs[]
\\ rpt strip_tac
\\ IMP_RES_TAC parseExp_LESS_EQ \\ fs[]);
val parseFBits_def = Define `
parseFBits input = parseFBitsRec input defaultFBits `;
parseFBits input =
(case input of
|DFBITS:: tokRest => parseFBitsRec tokRest defaultFBits
|_ => NONE)`;
(* Global parsing function*)
val dParse_def = Define `
dParse (input:Token list) =
let cmdParse = (case input of
| DLET :: tokRest => parseLet tokRest
| DRET :: tokRest => parseRet tokRest
| _ => NONE) in
case cmdParse of
| SOME (dCmd, tokRest) =>
(case parsePrecond tokRest of
| SOME (P, absenvRest) =>
(case parseGamma absenvRest of
| SOME (Gamma, residual) =>
(case parseAbsEnv residual of
| SOME (A,residual) =>
let (fBits,remainder) = parseFBits residual in
SOME ((dCmd, P, A, Gamma, fBits), residual)
| NONE => NONE)
| NONE => NONE)
| _ => NONE)
| NONE => NONE`;
(* case cmdParse of *)
(* | SOME (dCmd, tokRest) => *)
(* (case tokRest of *)
(* | DPRE :: preRest => *)
(* (case parsePrecond tokRest of *)
(* | SOME (P, absenvRest) => *)
(* (case absenvRest of *)
(* | DGAMMA :: _ => *)
(* (case parseGamma absenvRest of *)
(* | SOME (Gamma, residual) => *)
(* (case parseAbsEnv residual of *)
(* | SOME (A,residual) => SOME ((dCmd, P, A, Gamma), residual) *)
(* | NONE => NONE) *)
(* | NONE => NONE) *)
(* | _ => NONE) *)
(* | NONE => NONE) *)
(* | DABS :: _ => *)
(* (case parseAbsEnv tokRest of *)
(* | SOME (A, absenvRest) => *)
(* (case absenvRest of *)
(* | DPRE :: _ => *)
(* (case parsePrecond absenvRest of *)
(* | SOME (P, residual) => *)
(* (case parseGamma residual of *)
(* | SOME (Gamma, residual) => SOME ((dCmd,P,A,Gamma),residual) *)
(* | NONE => NONE) *)
(* | NONE => NONE) *)
(* | DGAMMA :: _ => *)
(* (case parseGamma absenvRest of *)
(* | SOME (Gamma, residual) => *)
(* (case parsePrecond residual of *)
(* | SOME (P,residual) => SOME ((dCmd, P, A, Gamma), residual) *)
(* | NONE => NONE) *)
(* | NONE => NONE) *)
(* | _ => NONE) *)
(* | NONE => NONE) *)
(* | DGAMMA :: _ => *)
(* (case parseGamma tokRest of *)
(* | SOME (Gamma, absenvRest) => *)
(* (case absenvRest of *)
(* | DPRE :: _ => *)
(* (case parsePrecond absenvRest of *)
(* | SOME (P, residual) => *)
(* (case parseAbsEnv residual of *)
(* | SOME (A, residual) => SOME ((dCmd,P,A,Gamma),residual) *)
(* | NONE => NONE) *)
(* | NONE => NONE) *)
(* | DABS :: _ => *)
(* (case parseAbsEnv absenvRest of *)
(* | SOME (A, residual) => *)
(* (case parsePrecond residual of *)
(* | SOME (P,residual) => SOME ((dCmd, P, A, Gamma), residual) *)
(* | NONE => NONE) *)
(* | NONE => NONE) *)
(* | _ => NONE) *)
(* | _ => NONE) *)
(* | _ => NONE) *)
(* | _ => NONE`; *)
let cmdParse =
(case input of
| DLET :: tokRest => parseLet tokRest
| DRET :: tokRest => parseRet tokRest
| _ => NONE) in
case cmdParse of
|NONE => NONE
| SOME (dCmd, tokRest) =>
(case parseGamma tokRest of
|NONE => NONE
|SOME (Gamma, residual) =>
(case parsePrecond residual of
|NONE => NONE
|SOME (P, residual) =>
(case parseAbsEnv residual of
|NONE => NONE
|SOME (A, residual) =>
(case parseFBits residual of
|NONE => NONE
|SOME (fBits, residual) =>
SOME ((dCmd, P, A, Gamma, fBits), residual)))))`;
val _ = export_theory();
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