Commit c417d728 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

remove flatten

parent f9d9f0a1
......@@ -114,7 +114,7 @@ PARSER_CMO := parser.cmo lexer.cmo typing.cmo
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo \
inlining.cmo flatten.cmo
inlining.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
OUTPUT_CMO := driver_parser.cmo driver_lexer.cmo driver.cmo \
......
......@@ -3,6 +3,7 @@
theory Test
use import prelude.Int
use BuiltIn
logic id(x: int) : int = x
logic even(x: int) = 2*(x/2) = x
goal G : (0 : BuiltIn.int) = 0
......
(**************************************************************************)
(* *)
(* 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 =
let rec aux first_level acc d = match first_level, d.d_node with
| _,Duse t -> Context.ctxt_fold (aux false) acc t.th_ctxt
| false,Dprop (Pgoal,_) -> acc
| false,Dprop (Plemma,pr) -> create_prop_decl Paxiom pr::acc
| _ -> d::acc
in
let r = (aux true [] a) in
(*Format.printf "flat %a : %a@\n" Pretty.print_decl a Pretty.print_decl_list r;*)
r
let t = Transform.elt elt
(**************************************************************************)
(* *)
(* 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 : Transform.ctxt_t
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