Skip to content

GitLab

Commit 4453f63d authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Fix another parser bug

parent 1374f851
Hide whitespace changes
Inline Side-by-side
Showing with 31 additions and 31 deletions
coq/daisyParser.v
View file @ 4453f63d
......@@ -21,7 +21,7 @@ Inductive Token:Type :=
| DDIV
| DFRAC
| DCAST
| DFAIL: ascii -> Token.
| DFAIL: string -> Token.
Open Scope string_scope.
......@@ -118,7 +118,7 @@ match fuel with
| "~"%char => DNEG :: lex input' fuel'
| " "%char => lex input' fuel'
| "010"%char => lex input' fuel'
| _ => DFAIL char :: []
| _ => DFAIL (String char ("")) :: []
end
| _ => []
end
......@@ -413,8 +413,8 @@ Definition dParse (input:list Token) fuel :=
match parsePrecond tokRest fuel with
| Some (P, absenvRest) =>
match absenvRest with
| DABS :: absRest =>
match parseAbsEnv absRest fuel with
| DABS :: _ =>
match parseAbsEnv absenvRest fuel with
| Some (A, residual) =>
match parseGamma residual with
| Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
......@@ -422,8 +422,8 @@ Definition dParse (input:list Token) fuel :=
end
| _ => None
end
| DGAMMA :: absRest =>
match parseGamma absRest with
| DGAMMA :: _ =>
match parseGamma absenvRest with
| Some (Gamma, residual) =>
match parseAbsEnv residual fuel with
| Some (A,residual) => Some ((dCmd, P, A, Gamma), residual)
......@@ -435,12 +435,12 @@ Definition dParse (input:list Token) fuel :=
end
| _ => None
end
| DABS :: absRest =>
| DABS :: _ =>
match parseAbsEnv tokRest fuel with
| Some (A, absenvRest) =>
match absenvRest with
| DPRE :: absRest =>
match parsePrecond absRest fuel with
| DPRE :: _ =>
match parsePrecond absenvRest fuel with
| Some (P, residual) =>
match parseGamma residual with
| Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
......@@ -448,8 +448,8 @@ Definition dParse (input:list Token) fuel :=
end
| _ => None
end
| DGAMMA :: absRest =>
match parseGamma absRest with
| DGAMMA :: _ =>
match parseGamma absenvRest with
| Some (Gamma, residual) =>
match parsePrecond residual fuel with
| Some (P,residual) => Some ((dCmd, P, A, Gamma), residual)
......@@ -461,12 +461,12 @@ Definition dParse (input:list Token) fuel :=
end
| _ => None
end
| DGAMMA :: absRest =>
| DGAMMA :: _ =>
match parseGamma tokRest with
| Some (Gamma, absenvRest) =>
match absenvRest with
| DPRE :: absRest =>
match parsePrecond absRest fuel with
| DPRE :: _ =>
match parsePrecond absenvRest fuel with
| Some (P, residual) =>
match parseAbsEnv residual fuel with
| Some (A, residual) => Some ((dCmd,P,A,Gamma),residual)
......@@ -474,8 +474,8 @@ Definition dParse (input:list Token) fuel :=
end
| _ => None
end
| DABS :: absRest =>
match parseAbsEnv absRest fuel with
| DABS :: _ =>
match parseAbsEnv absenvRest fuel with
| Some (A, residual) =>
match parsePrecond residual fuel with
| Some (P,residual) => Some ((dCmd, P, A, Gamma), residual)
......@@ -542,6 +542,6 @@ Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
Definition runChecker (input:string) :=
let tokList := lex input (str_length input) in
match tokList with
| DCONST n :: DCONST m :: tokRest => check_all (N.to_nat m) (N.to_nat n) tokRest (List.length tokList)
| 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.
hol4/daisyParserScript.sml
View file @ 4453f63d
......@@ -450,15 +450,15 @@ val dParse_def = Define `
(case parsePrecond tokRest of
| SOME (P, absenvRest) =>
(case absenvRest of
| DABS :: absRest =>
(case parseAbsEnv absRest of
| DABS :: _ =>
(case parseAbsEnv absenvRest of
| SOME (A, residual) =>
(case parseGamma residual of
| SOME (Gamma, residual) => SOME ((dCmd,P,A,Gamma),residual)
| NONE => NONE)
| NONE => NONE)
| DGAMMA :: absRest =>
(case parseGamma absRest of
| DGAMMA :: _ =>
(case parseGamma absenvRest of
| SOME (Gamma, residual) =>
(case parseAbsEnv residual of
| SOME (A,residual) => SOME ((dCmd, P, A, Gamma), residual)
......@@ -467,19 +467,19 @@ val dParse_def = Define `
| _ => NONE)
| NONE => NONE)
| DABS :: absRest =>
| DABS :: _ =>
(case parseAbsEnv tokRest of
| SOME (A, absenvRest) =>
(case absenvRest of
| DPRE :: absRest =>
(case parsePrecond absRest 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 :: absRest =>
(case parseGamma absRest of
| DGAMMA :: _ =>
(case parseGamma absenvRest of
| SOME (Gamma, residual) =>
(case parsePrecond residual of
| SOME (P,residual) => SOME ((dCmd, P, A, Gamma), residual)
......@@ -488,19 +488,19 @@ val dParse_def = Define `
| _ => NONE)
| NONE => NONE)
| DGAMMA :: absRest =>
| DGAMMA :: _ =>
(case parseGamma tokRest of
| SOME (Gamma, absenvRest) =>
(case absenvRest of
| DPRE :: absRest =>
(case parsePrecond absRest 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 :: absRest =>
(case parseAbsEnv absRest of
| DABS :: _ =>
(case parseAbsEnv absenvRest of
| SOME (A, residual) =>
(case parsePrecond residual of
| SOME (P,residual) => SOME ((dCmd, P, A, Gamma), residual)
......
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