Commit 3637e1bb authored by Heiko Becker's avatar Heiko Becker

Update parser and lexer

parent 3d6185b5
......@@ -12,8 +12,9 @@ Inductive Token:Type :=
| DCOND
| DGAMMA
| DTYPE:mType -> Token
| DFIXED
| DVAR
| DCONST: N -> Token
| DCONST: nat -> Token
| DNEG
| DPLUS
| DSUB
......@@ -32,7 +33,7 @@ Definition getChar (input:string):=
end.
Definition getConst (c:ascii) :=
((N_of_ascii c) - 48)%N.
((nat_of_ascii c) - 48)%nat.
Definition suffix (s:string) :=
match s with
......@@ -50,7 +51,7 @@ Definition isAlpha (c:ascii) :bool :=
Definition isAlphaNum (c :ascii) :bool :=
isDigit c || isAlpha c.
Fixpoint lexConst (input:string) (akk:N) :=
Fixpoint lexConst (input:string) (akk:nat) :=
match input with
|String c input' =>
if (isDigit c)
......@@ -97,10 +98,14 @@ match fuel with
| "GAMMA" => DGAMMA :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| "Cast" => DCAST :: lex input'' fuel'
| "F" => DFIXED :: lex input'' fuel'
| "MTYPE" => let ts := lex input'' fuel' in
(match ts with
|DCONST 16 :: ts' => DTYPE M16 :: ts'
|DCONST 32 :: ts' => DTYPE M32 :: ts'
|DCONST 64 :: ts' => DTYPE M64 :: ts'
|DFIXED :: DCONST w :: DCONST f :: ts' =>
DTYPE (F (Pos.of_nat w) (Pos.of_nat f)) :: ts'
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => []
......@@ -154,9 +159,10 @@ Definition pp_token (token:Token) :=
| DABS => "ABS"
| DCOND => "?"
| DVAR => "Var"
| DCONST num => str_of_num (N.to_nat num) (N.to_nat num)
| DCONST num => str_of_num num num
| DGAMMA => "Gamma"
| DTYPE m => str_join "MTYPE " (type_to_string m)
| DFIXED => ""
| DNEG => "~"
| DPLUS => "+"
| DSUB => "-"
......@@ -181,10 +187,10 @@ Fixpoint parseExp (tokList:list Token) (fuel:nat):option (expr Q * list Token) :
match tokList with
| DCONST n :: DFRAC :: DCONST m :: DTYPE t :: tokRest =>
match m with
|N0 => None
|Npos p => Some (Const t (Z.of_N n # p), tokRest)
| 0%nat => None
|S p => Some (Const t (Z.of_nat n # (Pos.of_nat p)), tokRest)
end
| DVAR :: DCONST n :: tokRest => Some (Var Q (N.to_nat n), tokRest)
| DVAR :: DCONST n :: tokRest => Some (Var Q n, tokRest)
| DNEG :: tokRest =>
match (parseExp tokRest fuel') with
| Some (Const m c, tokRest) => Some (Const m (- c), tokRest)
......@@ -259,7 +265,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 m (N.to_nat n) e letCmd, arbRest)
| Some (letCmd, arbRest) => Some (Let m n e letCmd, arbRest)
| _ => None
end
(* But if we have a return *)
......@@ -267,7 +273,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 m (N.to_nat n) e retCmd, arbRest)
| Some (retCmd, arbRest) => Some (Let m n e retCmd, arbRest)
| _ => None
end
| _ => None (* fail if there is no continuation for the let *)
......@@ -283,13 +289,13 @@ Definition parseFrac (input:list Token) :option (Q * list Token) :=
match input with
| DNEG :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
match m with
|N0 => None
|Npos p => Some ((- Z.of_N n # p),tokRest)
|0%nat => None
|S p => Some ((- Z.of_nat n # Pos.of_nat p),tokRest)
end
| DCONST n :: DFRAC :: DCONST m :: tokRest =>
match m with
|N0 => None
|Npos p => Some ((Z.of_N n # p),tokRest)
|0%nat => None
|S p => Some ((Z.of_nat n # Pos.of_nat p),tokRest)
end
| _ => None
end.
......@@ -322,8 +328,8 @@ Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precond * list T
match parseIV fracRest with
| Some (iv, precondRest) =>
match parsePrecondRec precondRest fuel' with
| Some (P, tokRest) => Some (updPre (N.to_nat n) iv P, tokRest)
| None => Some (updPre (N.to_nat n) iv defaultPre, precondRest)
| Some (P, tokRest) => Some (updPre n iv P, tokRest)
| None => Some (updPre n iv defaultPre, precondRest)
end
| _ => None
end
......@@ -386,7 +392,7 @@ Fixpoint parseGammaRec (input: list Token) : option ((nat -> option mType) * lis
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)
| Some (Gamma, rest) => Some (updDefVars n m Gamma, rest)
| None => None
end
| _ => Some (defaultGamma, input)
......@@ -542,6 +548,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 * 100)
| DCONST n :: DCONST m :: tokRest => check_all m n tokRest (List.length tokList * 100)
| _ => "failure no num of functions"
end.
......@@ -12,6 +12,7 @@ val _ = Datatype `
| DCOND
| DGAMMA
| DTYPE mType
| DFIXED
| DVAR
| DCONST num
| DNEG
......@@ -81,10 +82,14 @@ val lex_def = tDefine "lex" `
| "GAMMA" => DGAMMA :: lex input''
| "Var" => DVAR :: lex input''
| "Cast" => DCAST :: lex input''
| "F" => DFIXED :: lex input''
| "MTYPE" => let ts = lex input'' in
(case ts of
| DCONST 16 :: ts' => DTYPE M16 :: ts'
| DCONST 32 :: ts' => DTYPE M32 :: ts'
| DCONST 64 :: ts' => DTYPE M64 :: ts'
| DFIXED :: DCONST w :: DCONST f :: ts' =>
DTYPE (F w f) :: ts'
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => NIL)
......@@ -119,7 +124,13 @@ val str_of_num_def = Define `
val type_to_string = Define `
(type_to_string (M16) = "MTYPE 16") /\
(type_to_string (M32) = "MTYPE 32") /\
(type_to_string (M64) = "MTYPE 64")`; (* FIXME *)
(type_to_string (M64) = "MTYPE 64") /\
(type_to_string (F w f) =
str_join "MTYPE "
(str_join ("F ")
(str_join (str_of_num w)
(str_join " "
(str_of_num f)))))`; (* FIXME *)
(* (type_to_string (M128) = "MTYPE 128") /\ *)
(* (type_to_string (M256) = "MTYPE 256")`; *)
......@@ -135,6 +146,7 @@ val pp_token_def = Define `
| DCONST num => str_of_num num
| DGAMMA => "Gamma"
| DTYPE m => type_to_string m
| DFIXED => ""
| DNEG => "~"
| DPLUS => "+"
| DSUB => "-"
......
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