transform.ml 5.76 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

Francois Bobot's avatar
Francois Bobot committed
20
open Ident
21 22
open Theory
open Context
23 24

(* the memoisation is inside the function *)
25 26 27 28
type 'a t = { 
  all : context -> 'a;
  clear : unit -> unit;
}
29

30
type ctxt_t = context t
31

32 33 34
let conv_res f c = 
  { all = (fun x -> c (f.all x));
    clear = f.clear; }
35

36 37 38
exception CompositionOfIncompatibleTranformation

let compose f g =
39 40
  { all = (fun x -> g.all (f.all x));
    clear = (fun () -> f.clear (); g.clear ()); }
41

42
let apply f x = f.all x
Andrei Paskevich's avatar
Andrei Paskevich committed
43

44
let clear f = f.clear ()
45

46 47 48 49 50 51 52 53 54 55
let ymemo f tag h =
  let rec aux x =
    let t = tag x in
    try 
      Hashtbl.find h t
    with Not_found -> 
      let r = f aux x in
      Hashtbl.add h t r;
      r in
  aux
56

57
let memo f tag h = ymemo (fun _ -> f) tag h
58

59 60 61
let d_tag d = d.d_tag
let ctxt_tag c = c.ctxt_tag

62 63 64 65 66 67 68
let t all clear_all =
  { all = all;
    clear = clear_all; }

let register f =
  let memo_t = Hashtbl.create 17 in
  t (memo f ctxt_tag memo_t) (fun () -> Hashtbl.clear memo_t)
69

70
let fold_env f_fold v_empty =
71
  let memo_t = Hashtbl.create 64 in
72
  let rewind env todo =
73
    List.fold_left
74
      (fun env ctxt ->
75
         let env = f_fold ctxt env in
76
         Hashtbl.add memo_t ctxt.ctxt_tag env;
77 78 79
         env) 
      env todo 
  in
80 81
  let rec f todo ctxt = 
    match ctxt.ctxt_prev with
82 83 84
      | None -> 
	  rewind (v_empty ctxt.ctxt_env) todo
      | Some ctxt2 ->
85
          try
86
            let env = Hashtbl.find memo_t ctxt2.ctxt_tag in
87 88 89
            rewind env (ctxt :: todo)
          with Not_found -> 
	    f (ctxt :: todo) ctxt2
90
  in
91
  t (f []) (fun () -> Hashtbl.clear memo_t)
92

93
let fold f acc = fold_env f (fun _ -> acc)
94

95 96 97
let fold_map f_fold v_empty =
  let v_empty env = v_empty, init_context env in
  conv_res (fold_env f_fold v_empty) snd
98

99 100
let map f_map =
  fold_map (fun ctxt1 ctxt2 -> (), f_map ctxt1 (snd ctxt2)) ()
101

102 103 104
let map_concat f_elt = 
  let f_elt ctxt0 ctxt = List.fold_left add_decl ctxt (f_elt ctxt0) in
  map f_elt
105

106 107

let elt f_elt = 
108
  let memo_elt = Hashtbl.create 64 in
109 110 111
  let f_elt ctxt0 = memo f_elt d_tag memo_elt ctxt0.ctxt_decl in
  let f = map_concat f_elt in
  { f with clear = fun () -> Hashtbl.clear memo_elt; f.clear () }
112
    
Francois Bobot's avatar
Francois Bobot committed
113 114
(* Utils *)

115
(*type odecl =
Francois Bobot's avatar
Francois Bobot committed
116 117 118 119 120 121
  | Otype of ty_decl
  | Ologic of logic_decl
  | Oprop of prop_decl
  | Ouse   of theory
  | Oclone of (ident * ident) list*)

122
let elt_of_oelt ~ty ~logic ~ind ~prop ~use ~clone d = 
Francois Bobot's avatar
Francois Bobot committed
123
  match d.d_node with
124 125
    | Dtype l -> [create_ty_decl (List.map ty l)]
    | Dlogic l -> [create_logic_decl (List.map logic l)]
126
    | Dind l -> ind l 
Francois Bobot's avatar
Francois Bobot committed
127 128
    | Dprop p -> prop p
    | Duse th -> use th
129
    | Dclone (th,c) -> clone th c
Francois Bobot's avatar
Francois Bobot committed
130 131 132 133

let fold_context_of_decl f ctxt env ctxt_done d =
  let env,decls = f ctxt env d in
  env,List.fold_left add_decl ctxt_done decls
134
  
135 136
let split_goals =
  let f ctxt0 (ctxt,l) =
137
    let decl = ctxt0.ctxt_decl in
138
    match decl.d_node with
139 140
      | Dprop (Pgoal, _) -> (ctxt, add_decl ctxt decl :: l)
      | Dprop (Plemma, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
141 142
          let d1 = create_prop_decl Paxiom f in
          let d2 = create_prop_decl Pgoal f in
143
          (add_decl ctxt d1,
144 145 146 147
           add_decl ctxt d2 :: l)
      | _ -> (add_decl ctxt decl, l) 
  in
  let g = fold_env f (fun env -> init_context env, []) in
148
  conv_res g snd
149

150
let extract_goals () =
151
  let f ctxt0 (ctxt,l) =
152
    let decl = ctxt0.ctxt_decl in    
153
    match decl.d_node with
154 155 156
      | Dprop (Pgoal, f) -> 
	  ctxt, (f.pr_name,f.pr_fmla,ctxt) :: l
      | Dprop (Plemma, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
157
          let d = create_prop_decl Paxiom f in
158 159 160 161 162
          add_decl ctxt d, (f.pr_name, f.pr_fmla,ctxt) :: l
      | _ -> 
	  add_decl ctxt decl, l
  in
  let g = fold_env f (fun env -> init_context env, []) in
163
  conv_res g snd
164

165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
let identity = 
  { all = (fun x -> x);
    clear = (fun () -> ()); }

let cloned_from_ts env ctxt l s ls1 =
  assert false (*TODO*)
(*   try *)
(*     let th = Typing.find_theory env l in *)
(*     let ls2 = Mnm.find s th.th_export.ns_ts in *)
(*     Context_utils.cloned_from ctxt ls1.ts_name ls2.ts_name *)
(*   with Loc.Located _ -> assert false *)
    
    
let cloned_from_ls env ctxt l s ls1 =
  assert false (*TODO*)
(*   try *)
(*     let th = Typing.find_theory env l in *)
(*     let ls2 = Mnm.find s th.th_export.ns_ls in *)
(*     Context_utils.cloned_from ctxt ls1.ls_name ls2.ls_name *)
(*   with Loc.Located _ -> assert false *)
    
let cloned_from_pr env ctxt l s pr1 =
  assert false (*TODO*)
(*   try *)
(*     let th = Typing.find_theory env l in *)
(*     let pr2 = Mnm.find s th.th_export.ns_pr in *)
(*     Context_utils.cloned_from ctxt pr1.pr_name pr2.pr_name *)
(*   with Loc.Located _ -> assert false *)
193