detect_polymorphism.ml 2.25 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
(********************************************************************)
(*                                                                  *)
(*  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 =
MARCHE Claude's avatar
MARCHE Claude committed
17
  register_meta_excl "encoding:monomorphic_only" []
18 19
  ~desc:"Set@ when@ no@ occurence@ of@ type@ variables@ occur."

MARCHE Claude's avatar
MARCHE Claude committed
20 21
exception Found

22 23
let find_in_decl d =
  match d.d_node with
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27 28 29 30 31 32 33 34
  | Dtype ts ->
    Format.eprintf "======@\nFound type %a@\n" Pretty.print_ts ts;
    if ts.Ty.ts_args <> [] then
      (Format.eprintf "Type is polymorphic!@\n=======@.";
       raise Found);
    Format.eprintf "=======@."
  | Ddata _dl -> () (* TODO *)
  | Dparam _ls -> () (* TODO *)
  | Dlogic _dl -> () (* TODO *)
  | Dind _ind -> () (* TODO *)
  | Dprop _p ->  () (* TODO *)
35

MARCHE Claude's avatar
MARCHE Claude committed
36
let rec find_in_theory th = List.iter find_in_tdecl th.th_decls
37

MARCHE Claude's avatar
MARCHE Claude committed
38
and find_in_tdecl td =
39 40
  match td.td_node with
  | Decl d -> find_in_decl d
MARCHE Claude's avatar
MARCHE Claude committed
41 42 43 44 45 46 47
  | Use th ->
    Format.eprintf "======@\nLook up in used theory %a@." Pretty.print_th th;
    find_in_theory th
  | Clone (th,_) ->
    Format.eprintf "======@\nLook up in cloned theory %a@." Pretty.print_th th;
    find_in_theory th
  | Meta  _ -> ()
48 49 50

let rec find_in_task task =
  match task with
MARCHE Claude's avatar
MARCHE Claude committed
51 52
  | None -> ()
  | Some t -> find_in_task t.task_prev ; find_in_tdecl t.task_decl
53 54

let detect_polymorphism task =
MARCHE Claude's avatar
MARCHE Claude committed
55 56 57 58 59 60 61 62 63 64 65 66 67
  try
    find_in_task task;
    try
      let g,t = task_separate_goal task in
      let ta = add_meta t meta_monomorphic_types_only [] in
      Task.add_tdecl ta g
    with GoalNotFound ->
      add_meta task meta_monomorphic_types_only []
  with Found -> task

let () = Trans.register_transform "detect_polymorphism"
  (Trans.store detect_polymorphism)
  ~desc:"Detect if task has polymorphic types somewhere."