Commit 4ef014e7 authored by MARCHE Claude's avatar MARCHE Claude

detect_polymorphism: in progress

parent dc4c0616
......@@ -156,7 +156,8 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
introduction abstraction close_epsilon lift_epsilon \
eliminate_epsilon \
eval_match instantiate_predicate smoke_detector \
reduction_engine compute induction_pr prop_curry
reduction_engine compute induction_pr prop_curry \
detect_polymorphism
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2014 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Decl
open Theory
open Task
let meta_monomorphic_types_only =
register_meta "encoding:monomorphic_only" []
~desc:"Set@ when@ no@ occurence@ of@ type@ variables@ occur."
let find_in_decl d =
match d.d_node with
| Dtype _ts -> true (* TODO *)
| Ddata _dl -> true (* TODO *)
| Dparam _ls -> true (* TODO *)
| Dlogic _dl -> true (* TODO *)
| Dind _ind -> true (* TODO *)
| Dprop _p -> true (* TODO *)
let find_in_tdecl td =
match td.td_node with
| Decl d -> find_in_decl d
| Use _ | Clone _ | Meta _ -> false
let rec find_in_task task =
match task with
| None -> false
| Some t -> find_in_task t.task_prev || find_in_tdecl t.task_decl
let detect_polymorphism task =
if find_in_task task then task else
add_meta task meta_monomorphic_types_only []
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