Skip to content
Snippets Groups Projects
Commit 54109a31 authored by WASQUEL Valentin's avatar WASQUEL Valentin
Browse files

change naming convention to prevent conflics

parent 53082e83
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 1
− 1
View file @ 54109a31
......@@ -63,6 +63,6 @@ src/verification/FPSProp.v
src/parser/FlightPlanParsed.v
src/parser/FPPUtils.v
src/parser/Parser.v
src/parser/Lexer.v
src/parser/CoqLexer.v
src/parser/Importer.v
src/extraction.v
\ No newline at end of file
src/parser/Lexer.v → src/parser/CoqLexer.v
+ 2
− 2
View file @ 54109a31
......@@ -109,8 +109,8 @@ Definition Dictionary (s : string) : option token :=
| "pre_call"%string => Some (PRE_CALL tt)
| "post_call"%string => Some (POST_CALL tt)
| "pitch"%string => Some (PITCH tt)
| "p1"%string => Some (P1 tt)
| "p2"%string => Some (P2 tt)
| "p1"%string => Some (WP tt)
| "p2"%string => Some (WP2 tt)
| "on_exit"%string => Some (ON_EXIT tt)
| "in_enter"%string => Some (ON_ENTER tt)
| "nav_type"%string => Some (NAV_TYPE tt)
......
src/parser/FPPUtils.v
+ 16
− 140
View file @ 54109a31
......@@ -931,6 +931,22 @@ Definition app_block_stage (x : fpp_stage) (b : block) :=
(get_block_exceptions b)
(get_block_fbd b)
((get_block_stages b) ++ (x :: nil)).
Definition set_block_stage (x : list fpp_stage) (b : block) :=
mk_block
(get_block_name b)
(get_block_pre_call b)
(get_block_post_call b)
(get_block_on_enter b)
(get_block_on_exit b)
(get_block_strip_button b)
(get_block_strip_icon b)
(get_block_group b)
(get_block_key b)
(get_block_description b)
(get_block_exceptions b)
(get_block_fbd b)
x.
(** stage parameters *)
......@@ -966,8 +982,6 @@ Definition empty_stage :=
None
None
None
None
None
None.
Definition set_stage_roll (x : option string)
......@@ -987,8 +1001,6 @@ Definition set_stage_roll (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1024,8 +1036,6 @@ Definition set_stage_pitch (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1061,8 +1071,6 @@ Definition set_stage_yaw (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1098,8 +1106,6 @@ Definition set_stage_climb (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1135,8 +1141,6 @@ Definition set_stage_wp (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1172,8 +1176,6 @@ Definition set_stage_wp2 (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1209,8 +1211,6 @@ Definition set_stage_wpts (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1246,8 +1246,6 @@ Definition set_stage_wp_qdr (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1283,8 +1281,6 @@ Definition set_stage_wp_dist (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1320,8 +1316,6 @@ Definition set_stage_from (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1357,8 +1351,6 @@ Definition set_stage_from_qdr (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1394,8 +1386,6 @@ Definition set_stage_from_dist (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1431,8 +1421,6 @@ Definition set_stage_course (x : option string)
x
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1468,8 +1456,6 @@ Definition set_stage_radius (x : option string)
(get_stage_course ob)
x
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1505,82 +1491,6 @@ Definition set_stage_center (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
x
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
(get_stage_ac_id ob)
(get_stage_distance ob)
(get_stage_vmode ob)
(get_stage_hmode ob)
(get_stage_alt ob)
(get_stage_height ob)
(get_stage_throttle ob)
(get_stage_pre_call ob)
(get_stage_post_call ob)
(get_stage_nav_type ob)
(get_stage_nav_params ob)
(get_stage_until ob)
(get_stage_approaching_time ob)
(get_stage_exceeding_time ob).
Definition set_stage_p1 (x : option string)
(ob : nav_stage_param) :=
mk_stage_param (get_stage_roll ob)
(get_stage_pitch ob)
(get_stage_yaw ob)
(get_stage_climb ob)
(get_stage_wp ob)
(get_stage_wp2 ob)
(get_stage_wpts ob)
(get_stage_wp_qdr ob)
(get_stage_wp_dist ob)
(get_stage_from ob)
(get_stage_from_qdr ob)
(get_stage_from_dist ob)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
x
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
(get_stage_ac_id ob)
(get_stage_distance ob)
(get_stage_vmode ob)
(get_stage_hmode ob)
(get_stage_alt ob)
(get_stage_height ob)
(get_stage_throttle ob)
(get_stage_pre_call ob)
(get_stage_post_call ob)
(get_stage_nav_type ob)
(get_stage_nav_params ob)
(get_stage_until ob)
(get_stage_approaching_time ob)
(get_stage_exceeding_time ob).
Definition set_stage_p2 (x : option string)
(ob : nav_stage_param) :=
mk_stage_param (get_stage_roll ob)
(get_stage_pitch ob)
(get_stage_yaw ob)
(get_stage_climb ob)
(get_stage_wp ob)
(get_stage_wp2 ob)
(get_stage_wpts ob)
(get_stage_wp_qdr ob)
(get_stage_wp_dist ob)
(get_stage_from ob)
(get_stage_from_qdr ob)
(get_stage_from_dist ob)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
x
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1616,8 +1526,6 @@ Definition set_stage_turn_around (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
x
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1653,8 +1561,6 @@ Definition set_stage_commands (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
x
(get_stage_flags ob)
......@@ -1690,8 +1596,6 @@ Definition set_stage_flags (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
x
......@@ -1727,8 +1631,6 @@ Definition set_stage_ac_id (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1764,8 +1666,6 @@ Definition set_stage_distance (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1801,8 +1701,6 @@ Definition set_stage_vmode (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1838,8 +1736,6 @@ Definition set_stage_hmode (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1875,8 +1771,6 @@ Definition set_stage_alt (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1912,8 +1806,6 @@ Definition set_stage_height (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1949,8 +1841,6 @@ Definition set_stage_throttle (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -1986,8 +1876,6 @@ Definition set_stage_pre_call (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -2023,8 +1911,6 @@ Definition set_stage_post_call (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -2060,8 +1946,6 @@ Definition set_stage_nav_type (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -2097,8 +1981,6 @@ Definition set_stage_nav_params (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -2134,8 +2016,6 @@ Definition set_stage_until (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -2171,8 +2051,6 @@ Definition set_stage_approaching_time (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......@@ -2208,8 +2086,6 @@ Definition set_stage_exceeding_time (x : option string)
(get_stage_course ob)
(get_stage_radius ob)
(get_stage_center ob)
(get_stage_p1 ob)
(get_stage_p2 ob)
(get_stage_turn_around ob)
(get_stage_commands ob)
(get_stage_flags ob)
......
src/parser/FlightPlanParsed.v
+ 0
− 2
View file @ 54109a31
......@@ -192,8 +192,6 @@ Record nav_stage_param := create_nav_stage_param {
get_stage_radius : option string;
get_stage_center : option string;
get_stage_p1 : option string;
get_stage_p2 : option string;
get_stage_turn_around : option string;
get_stage_commands : option string;
......
src/parser/Importer.v
+ 3
− 3
View file @ 54109a31
Require Import Ascii List String PeanoNat.
From VFP Require Import Parser Lexer FlightPlanParsed.
From VFP Require Import Parser CoqLexer FlightPlanParsed.
Import MenhirLibParser.Inter.
Open Scope string_scope.
(** Lexer + Parser function *)
Definition string2fp s :=
match option_map (Parser.parse_fp 50) (Lexer.lex_string s) with
match option_map (Parser.parse_fp 50) (lex_string s) with
| Some (Parsed_pr f _) => Some f
| _ => None
end.
Definition string2proc s :=
match option_map (Parser.parse_proc 50) (Lexer.lex_string s) with
match option_map (Parser.parse_proc 50) (lex_string s) with
| Some (Parsed_pr f _) => Some f
| _ => None
end.
src/parser/Parser.vy
+ 1
− 5
View file @ 54109a31
......@@ -83,7 +83,7 @@ From VFP Require Import BasicTypes FlightPlan FlightPlanGeneric
%type<list fpp_stage> Fp_stage_list
%token COURSE VMODE HMODE THROTTLE CLIMB PITCH YAW ROLL
%token UNTIL NAV_TYPE APPRTIME EXCEEDTIME WP WP2 WP_QDR
%token WP_DIST FROM_QDR FROM_DIST WPTS RADIUS CENTER P1 P2
%token WP_DIST FROM_QDR FROM_DIST WPTS RADIUS CENTER
%token TURN_AROUND COMMANDS FLAGS AC_ID DISTANCE NAV_PARAMS
%token BHOME
......@@ -607,10 +607,6 @@ Nav_stage_param:
{ set_stage_radius (Some data) param }
| CENTER "=" data = Data param = Nav_stage_param
{ set_stage_center (Some data) param }
| P1 "=" data = Data param = Nav_stage_param
{ set_stage_p1 (Some data) param }
| P2 "=" data = Data param = Nav_stage_param
{ set_stage_p2 (Some data) param }
| TURN_AROUND "=" data = Data param = Nav_stage_param
{ set_stage_turn_around (Some data) param }
| COMMANDS "=" data = Data param = Nav_stage_param
......
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