inlining.ml 4.09 KB
Newer Older
Francois Bobot's avatar
Francois Bobot committed
1 2 3
open Ident
open Term
open Theory
4
open Context
Francois Bobot's avatar
Francois Bobot committed
5 6 7 8

let ttrue _ = true
let ffalse _ = false

9 10
type env = { fs : (vsymbol list * term) Mls.t;
             ps : (vsymbol list * fmla) Mls.t}
Francois Bobot's avatar
Francois Bobot committed
11

12 13
let empty_env = { fs = Mls.empty;
                  ps = Mls.empty}
Francois Bobot's avatar
Francois Bobot committed
14 15 16 17 18 19
open Format

let print_env fmt env =
  let print_map iter pterm pfs = Pp.print_iter2 iter Pp.newline Pp.comma pfs
    (Pp.print_pair (Pp.print_list Pp.comma Pretty.print_vsymbol) pterm) in
  fprintf fmt "fs:@[<hov>%a@]@\nps:@[<hov>%a@]@\n"
20 21
    (print_map Mls.iter Pretty.print_term Pretty.print_lsymbol) env.fs
    (print_map Mls.iter Pretty.print_fmla Pretty.print_lsymbol) env.ps
Francois Bobot's avatar
Francois Bobot committed
22 23 24 25 26 27

let rec replacet env t = 
  let t = substt env t in
  match t.t_node with
    | Tapp (fs,tl) ->
        begin try 
28
          let (vs,t) = Mls.find fs env.fs in
Francois Bobot's avatar
Francois Bobot committed
29 30 31 32 33 34 35 36 37 38 39
          let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc)
            Mvs.empty vs tl in
          t_subst m t
        with Not_found -> t end
    | _ -> t

and replacep env f = 
  let f = substp env f in
  match f.f_node with
    | Fapp (ps,tl) ->
        begin try 
40
          let (vs,t) = Mls.find ps env.ps in
Francois Bobot's avatar
Francois Bobot committed
41 42 43 44 45 46 47 48 49
          let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc) 
            Mvs.empty vs tl in
          f_subst m f
        with Not_found -> f end
    | _ -> f

and substt env d = t_map (replacet env) (replacep env) d
and substp env d = f_map (replacet env) (replacep env) d

Francois Bobot's avatar
Francois Bobot committed
50
let fold isnotinlinedt isnotinlinedf _ env ctxt d = 
51
(*  Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;*)
Francois Bobot's avatar
Francois Bobot committed
52 53 54
  match d.d_node with
    | Dlogic [l] -> begin
        match l with
55
          | Lfunction (fs,None) -> env,add_decl ctxt d 
Francois Bobot's avatar
Francois Bobot committed
56 57 58
          | Lfunction (fs,Some fmla) -> 
              let _,vs,t = open_fs_defn fmla in
              let t = replacet env t in
Francois Bobot's avatar
Francois Bobot committed
59
              if t_s_any ffalse ((==) fs) t || isnotinlinedt t
60
              then  env,
Francois Bobot's avatar
Francois Bobot committed
61 62 63
              add_decl ctxt 
                (create_logic [Lfunction(fs,
                                         Some (make_fs_defn fs vs t))])
64 65
              else {env with fs = Mls.add fs (vs,t) env.fs},ctxt
          | Lpredicate (ps,None) -> env,add_decl ctxt d
Francois Bobot's avatar
Francois Bobot committed
66 67 68
          | Lpredicate (ps,Some fmla) -> 
              let _,vs,f = open_ps_defn fmla in
              let f = replacep env f in
Francois Bobot's avatar
Francois Bobot committed
69
              if f_s_any ffalse ((==) ps) f || isnotinlinedf f
70 71 72 73
              then  env,
              add_decl ctxt 
                (create_logic [Lpredicate(ps,Some (make_ps_defn ps vs f))])
              else {env with ps = Mls.add ps (vs,f) env.ps},ctxt
Francois Bobot's avatar
Francois Bobot committed
74
      end
75 76 77 78
    | Dind (ps,fmlal) ->
        let fmlal = List.map 
          (fun (id,fmla) -> id_dup id,replacep env fmla) fmlal in
        env,add_decl ctxt (create_ind ps fmlal)
Francois Bobot's avatar
Francois Bobot committed
79
    | Dlogic dl -> env,
80
        add_decl ctxt (create_logic 
Francois Bobot's avatar
Francois Bobot committed
81 82 83 84 85 86 87 88 89 90 91 92
           (List.map 
              (function
                 | Lfunction (fs,None) as a -> a 
                 | Lfunction (fs,Some fmla) -> 
                     let _,vs,t = open_fs_defn fmla in
                     let t = replacet env t in
                     Lfunction (fs,Some (make_fs_defn fs vs t))
                 | Lpredicate (ps,None) as a -> a
                 | Lpredicate (ps,Some fmla) ->
                     let _,vs,t = open_ps_defn  fmla in
                     let t = replacep env t in
                     Lpredicate (ps,Some (make_ps_defn ps vs t))
93 94
              ) dl))
    | Dtype dl -> env,add_decl ctxt d
Francois Bobot's avatar
Francois Bobot committed
95 96
    | Dprop (k,i,fmla) -> env,add_decl ctxt (create_prop k (id_dup i) 
                                               (replacep env fmla))
97
    | Duse _ | Dclone _ -> env,add_decl ctxt d
Francois Bobot's avatar
Francois Bobot committed
98
        
Francois Bobot's avatar
Francois Bobot committed
99 100 101 102 103 104 105 106 107 108 109 110 111
let t ~isnotinlinedt ~isnotinlinedf = 
  Transform.fold_map_up (fold isnotinlinedt isnotinlinedf) empty_env

let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)

let trivial = t 
  ~isnotinlinedt:(fun m -> match m.t_node with
                    | Tconst _ | Tvar _ -> false
                    | Tapp (ls,tl) when List.for_all 
                        (fun m -> match m.t_node with Tvar _ -> true | _ -> false) tl -> true
                    | _ -> true )
  ~isnotinlinedf:(fun m -> match m.f_node with Ftrue | Ffalse | Fapp _ -> false
                    | _ -> true)