Skip to content

GitLab

why3
why3
Commit 8e1c8b96 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

mise en place driver

parent 188d9330
Hide whitespace changes
Inline Side-by-side
Showing with 477 additions and 19 deletions
Makefile.in
View file @ 8e1c8b96
......@@ -66,7 +66,8 @@ COQLIB = "@COQLIB@"
COQVER = @COQVER@
GENERATED = src/version.ml src/parser/parser.mli src/parser/parser.ml \
src/parser/lexer.ml
src/parser/lexer.ml src/output/driver_lexer.ml \
src/output/driver_parser.mli src/output/driver_parser.ml
# main targets
##############
......@@ -117,7 +118,8 @@ TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
flatten.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
OUTPUT_CMO := print_real.cmo alt_ergo.cmo why3.cmo
OUTPUT_CMO := driver_parser.cmo driver_lexer.cmo driver.cmo \
print_real.cmo alt_ergo.cmo why3.cmo
OUTPUT_CMO := $(addprefix src/output/,$(OUTPUT_CMO))
CMO = $(UTIL_CMO) $(CORE_CMO) src/pretty.cmo $(PARSER_CMO) \
......@@ -530,7 +532,7 @@ binary: $(ALLBINARYFILES)
headers:
headache -c misc/headache_config.txt -h misc/header.txt \
Makefile.in configure.in \
*/*.ml */*.ml[ily4]
*/*.ml */*.ml[ily4] */*/*.ml */*/*.ml[ily4]
# myself
########
......
src/core/context_utils.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ident
open Theory
......
src/core/context_utils.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ident
open Theory
......
src/output/alt_ergo.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Pp
......
src/output/alt_ergo.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Ident
......
src/output/driver.ml 0 → 100644
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
type t
type translation =
| Remove
| Syntax of string
| Tag of string list
let ident dr id =
assert false (*TODO*)
src/output/driver.mli 0 → 100644
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ident
type t
type translation =
| Remove
| Syntax of string
| Tag of string list
val ident : t -> ident -> translation
src/output/driver_ast.mli 0 → 100644
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
type loc = Loc.position
type ident = { id : string; loc : loc }
type qualid =
| Qident of ident
| Qdot of qualid * ident
type star = bool
type trule =
| Rremove of star * qualid
| Rsyntax of qualid * string
| Rtag of star * qualid * string
type theory_rules = {
th_name : qualid;
th_prelude : string option;
th_rules : trule list;
}
type file = {
f_prelude : string option;
f_rules : theory_rules list;
}
src/output/driver_lexer.mll 0 → 100644
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
{
open Lexing
open Driver_parser
}
rule token = parse
| eof { EOF }
src/output/driver_parser.mly 0 → 100644
View file @ 8e1c8b96
/**************************************************************************/
/* */
/* Copyright (C) 2010- */
/* Francois Bobot */
/* Jean-Christophe Filliatre */
/* Johannes Kanig */
/* Andrei Paskevich */
/* */
/* This software is free software; you can redistribute it and/or */
/* modify it under the terms of the GNU Library General Public */
/* License version 2.1, with the special exception on linking */
/* described in file LICENSE. */
/* */
/* This software is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. */
/* */
/**************************************************************************/
%{
open Driver_ast
open Parsing
let loc () = (symbol_start_pos (), symbol_end_pos ())
%}
%token <string> IDENT
%token <string> STRING
%token THEORY END SYNTAX REMOVE TAG
%token STAR DOT EOF
%type <Driver_ast.file> file
%start file
%%
file:
| string_option list0_theory EOF
{ { f_prelude = $1; f_rules = $2 } }
;
string_option:
| /* epsilon */ { None }
| STRING { Some $1 }
;
list0_theory:
| /* epsilon */ { [] }
| theory list0_theory { $1 :: $2 }
;
theory:
| THEORY qualid string_option list0_trule END
{ { th_name = $2; th_prelude = $3; th_rules = $4 } }
;
list0_trule:
| /* epsilon */ { [] }
| trule list0_trule { $1 :: $2 }
;
trule:
| REMOVE star qualid { Rremove ($2, $3) }
;
star:
| /* epsilon */ { false }
| STAR { true }
;
qualid:
| ident { Qident $1 }
| qualid DOT ident { Qdot ($1, $3) }
;
ident:
| IDENT { { id = $1; loc = loc () } }
| STRING { { id = $1; loc = loc () } }
;
src/output/print_real.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Big_int
......
src/output/print_real.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
......
src/parser/transform_utils.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ty
open Term
open Theory
......
src/parser/transform_utils.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
val qualid_of_lstring : string list -> Ptree.qualid
val cloned_from_ts : Typing.env -> Theory.context ->
......
src/transform/flatten.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Theory
let elt a =
......
src/transform/flatten.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(* a list of decl_or_use to a list of decl *)
val t : (Theory.context,Theory.context) Transform.t
src/transform/inlining.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ident
open Term
open Theory
......
src/transform/inlining.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(* Inline the definition not recursive *)
......
src/util/hashcons.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
......
src/util/hashcons.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
......
src/util/loc.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
......
src/util/loc.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
......
src/util/pp.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
......
src/util/pp.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
......
src/util/util.ml
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
......
src/util/util.mli
View file @ 8e1c8b96
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
......
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