transform.ml 5.87 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
let compose f g =
37 38
  { all = (fun x -> g.all (f.all x));
    clear = (fun () -> f.clear (); g.clear ()); }
39

40
let apply f x = f.all x
Andrei Paskevich's avatar
Andrei Paskevich committed
41

42
let clear f = f.clear ()
43

44 45 46 47 48 49 50 51 52 53
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
54

55
let memo f tag h = ymemo (fun _ -> f) tag h
56

57 58 59
let d_tag d = d.d_tag
let ctxt_tag c = c.ctxt_tag

60 61 62 63 64 65 66
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)
67

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

91
let fold f acc = fold_env f (fun _ -> acc)
92

93 94 95
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
96

97 98
let map f_map =
  fold_map (fun ctxt1 ctxt2 -> (), f_map ctxt1 (snd ctxt2)) ()
99

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

104 105

let elt f_elt = 
106
  let memo_elt = Hashtbl.create 64 in
107 108 109
  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 () }
110
    
Francois Bobot's avatar
Francois Bobot committed
111 112
(* Utils *)

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

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

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
132
  
133 134
let split_goals =
  let f ctxt0 (ctxt,l) =
135
    let decl = ctxt0.ctxt_decl in
136
    match decl.d_node with
137 138
      | Dprop (Pgoal, _) -> (ctxt, add_decl ctxt decl :: l)
      | Dprop (Plemma, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
139 140
          let d1 = create_prop_decl Paxiom f in
          let d2 = create_prop_decl Pgoal f in
141
          (add_decl ctxt d1,
142 143 144 145
           add_decl ctxt d2 :: l)
      | _ -> (add_decl ctxt decl, l) 
  in
  let g = fold_env f (fun env -> init_context env, []) in
146
  conv_res g snd
147

148 149 150 151 152 153 154 155
exception NotGoalContext

let goal_of_ctxt ctxt =
  match ctxt.ctxt_decl.d_node with
    | Dprop (Pgoal,pr) -> pr
    | _ -> raise NotGoalContext

(*
156
let extract_goals () =
157
  let f ctxt0 (ctxt,l) =
158
    let decl = ctxt0.ctxt_decl in    
159
    match decl.d_node with
160 161 162
      | Dprop (Pgoal, f) -> 
	  ctxt, (f.pr_name,f.pr_fmla,ctxt) :: l
      | Dprop (Plemma, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
163
          let d = create_prop_decl Paxiom f in
164 165 166 167 168
          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
169
  conv_res g snd
170
*)
171

172 173 174 175
let identity = 
  { all = (fun x -> x);
    clear = (fun () -> ()); }

176
(*
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200
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 *)
201
*)