Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

reflection.ml 29.7 KB
Newer Older
1 2 3
open Term
open Ty
open Decl
4
open Ident
5
open Task
6
open Args_wrapper
7
open Generic_arg_trans_utils
8

9
exception NoReification
10
exception Exit of string
11

12 13 14 15 16 17
let debug_reification = Debug.register_info_flag
                          ~desc:"Reification"
                          "reification"
let debug_refl = Debug.register_info_flag
                     ~desc:"Reflection transformations"
                     "reflection"
18

Andrei Paskevich's avatar
Andrei Paskevich committed
19
let expl_reification_check = Ident.create_attribute "expl:reification check"
20

21
type reify_env = { kn: known_map;
22
                   store: (vsymbol * int) Mterm.t;
23 24
                   fr: int;
                   subst: term Mvs.t;
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
25
                   lv: vsymbol list;
26
                   var_maps: ty Mvs.t; (* type of values pointed by each map*)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
27
                   crc_map: Coercion.t;
28
                   ty_to_map: vsymbol Mty.t;
29
                   env: Env.env;
30
                   interps: Sls.t; (* functions that were inverted*)
31
                   task: Task.task;
32 33
                   bound_vars: Svs.t; (* bound variables, do not map them in a var map*)
                   bound_fr: int; (* separate, negative index for bound vars*)
34
                 }
35

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
36
let init_renv kn crc lv env task =
37 38 39 40 41 42
  { kn=kn;
    store = Mterm.empty;
    fr = 0;
    subst = Mvs.empty;
    lv = lv;
    var_maps = Mvs.empty;
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
43
    crc_map = crc;
44 45
    ty_to_map = Mty.empty;
    env = env;
46
    interps = Sls.empty;
47
    task = task;
48 49
    bound_vars = Svs.empty;
    bound_fr = -1;
50
  }
51 52

let rec reify_term renv t rt =
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
53
  let is_pvar p = match p.pat_node with Pvar _ -> true | _ -> false in
54 55 56 57 58 59 60 61 62 63 64 65 66
  let rec use_interp t =
    let r = match t.t_node with
      | Tconst _ -> true
      | Tvar _ -> false
      | Tapp (ls, []) ->
         begin match find_logic_definition renv.kn ls with
         | None -> false
         | Some ld ->
            let _,t = open_ls_defn ld in
            use_interp t
         end
      | Tapp (_, _) -> true
      | _ -> false in
67
    Debug.dprintf debug_reification "use_interp %a: %b@." Pretty.print_term t r;
68
    r in
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
  let add_to_maps renv vyl =
     let var_maps, ty_to_map =
       List.fold_left
         (fun (var_maps, ty_to_map) vy ->
           if Mty.mem vy.vs_ty ty_to_map
           then (Mvs.add vy vy.vs_ty var_maps, ty_to_map)
           else (Mvs.add vy vy.vs_ty var_maps,
                 Mty.add vy.vs_ty vy ty_to_map))
         (renv.var_maps, renv.ty_to_map)
         (List.map
            (fun t -> match t.t_node with Tvar vy -> vy | _ -> assert false)
            vyl)
     in
     { renv with var_maps = var_maps; ty_to_map = ty_to_map }
  in
  let open Theory in
  let th_list = Env.read_theory renv.env ["list"] "List" in
  let ty_list = ns_find_ts th_list.th_export ["list"] in
  let compat_h t rt =
    match t.t_node, rt.t_node with
    | Tapp (ls1,_), Tapp(ls2, _) -> ls_equal ls1 ls2
    | Tquant (Tforall, _), Tquant (Tforall, _)
      | Tquant (Texists, _), Tquant (Texists, _)-> true
    | _ -> false in
  let is_eq_true t = match t.t_node with
    | Tapp (eq, [_; tr])
       when ls_equal eq ps_equ && t_equal tr t_bool_true -> true
    | _ -> false in
  let lhs_eq_true t = match t.t_node with
    | Tapp (eq, [t; tr])
         when ls_equal eq ps_equ && t_equal tr t_bool_true -> t
    | _ -> assert false in
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
101
  let rec invert_nonvar_pat vl (renv:reify_env) (p,f) t =
102 103 104
    Debug.dprintf debug_reification
      "invert_nonvar_pat p %a f %a t %a@."
      Pretty.print_pat p Pretty.print_term f Pretty.print_term t;
105 106
    if is_eq_true f && not (is_eq_true t)
    then invert_nonvar_pat vl renv (p, lhs_eq_true f) t else
107
    match p.pat_node, f.t_node, t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
108
    | Pwild , _, _ | Pvar _,_,_ when t_equal_nt_na f t ->
109
       Debug.dprintf debug_reification "case equal@.";
110
       renv, t
111 112
    | Papp (cs, pl), _,_
         when compat_h f t
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
113 114
              && Svs.for_all (fun v -> t_v_occurs v f = 1) p.pat_vars
              && List.for_all is_pvar pl
115
                              (* could remove this with a bit more work in term reconstruction *)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
116
      ->
117
       Debug.dprintf debug_reification "case app@.";
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
118 119
       let rec rt_of_var svs f t v (renv, acc) =
         assert (not (Mvs.mem v acc));
120
         Debug.dprintf debug_reification "rt_of_var %a %a@."
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
                                     Pretty.print_vs v Pretty.print_term f;
         if t_v_occurs v f = 1
            && Svs.for_all (fun v' -> vs_equal v v' || t_v_occurs v' f = 0) svs
         then let renv, rt = invert_pat vl renv (pat_var v, f) t in
              renv, Mvs.add v rt acc
         else
           match f.t_node, t.t_node with
           | Tapp(ls1, la1), Tapp(ls2, la2) when ls_equal ls1 ls2 ->
              let rec aux la1 la2 =
                match la1, la2 with
                | f'::l1, t'::l2 ->
                   if t_v_occurs v f' = 1 then rt_of_var svs f' t' v (renv, acc)
                   else aux l1 l2
                | _ -> assert false in
              aux la1 la2
136 137 138 139 140 141 142
           | Tquant (Tforall, tq1), Tquant (Tforall, tq2)
             | Tquant (Texists, tq1), Tquant (Texists, tq2) ->
              let _, _, t1 = t_open_quant tq1 in
              let vl, _, t2 = t_open_quant tq2 in
              let bv = List.fold_left Svs.add_left renv.bound_vars vl in
              let renv = { renv with bound_vars = bv } in
              rt_of_var svs t1 t2 v (renv, acc)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
143 144
           | _ -> raise NoReification
       in
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
       let rec check_nonvar f t =
         match f.t_node, t.t_node with
         | Tapp (ls1, la1), Tapp (ls2, la2) ->
            if Svs.for_all (fun v -> t_v_occurs v f = 0) p.pat_vars
            then (if not (ls_equal ls1 ls2)
                  then raise NoReification);
            if ls_equal ls1 ls2 then List.iter2 check_nonvar la1 la2;
         | Tapp (ls,_), Tconst _ ->
            (* reject constants that do not match the
               definitions of logic constants*)
            if Svs.for_all (fun v -> t_v_occurs v f = 0) p.pat_vars
            then
              match find_logic_definition renv.kn ls with
              | None -> raise NoReification
              | Some ld -> let v,f = open_ls_defn ld in
                           assert (v = []);
                           check_nonvar f t
            else ()
         | Tconst (Number.ConstInt c1), Tconst (Number.ConstInt c2) ->
            let open Number in
            if not (BigInt.eq (compute_int_constant c1) (compute_int_constant c2))
            then raise NoReification
         | _ -> () (* FIXME add more failure cases if needed *)
       in
       check_nonvar f t;
       let renv, mvs = Svs.fold (rt_of_var p.pat_vars f t) p.pat_vars
                                (renv, Mvs.empty) in
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
172 173 174
       let lrt = List.map (function | {pat_node = Pvar v} -> Mvs.find v mvs
                                    | _ -> assert false) pl in
       renv, t_app cs lrt (Some p.pat_ty)
175 176
    | Pvar v, Tapp (ls1, la1), Tapp(ls2, la2)
         when ls_equal ls1 ls2 && t_v_occurs v f = 1
177
      -> Debug.dprintf debug_reification "case app_var@.";
178
         let renv, rt =
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
179 180
           List.fold_left2
             (fun (renv, acc) f t ->
181 182 183 184 185 186 187
               if acc = None
               then if t_v_occurs v f > 0
                    then let renv, rt = (invert_pat vl renv (p, f) t) in
                         renv, Some rt
                    else renv, acc
               else (assert (t_v_occurs v f = 0);
                     renv, acc))
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
188
             (renv,None) la1 la2 in
189
         renv, Opt.get rt
190 191 192
    | Pvar v, Tquant(Tforall, tq1), Tquant(Tforall, tq2)
      | Pvar v, Tquant(Texists, tq1), Tquant(Texists, tq2)
         when t_v_occurs v f = 1 ->
193
       Debug.dprintf debug_reification "case quant_var@.";
194 195 196 197 198
       let _,_,t1 = t_open_quant tq1 in
       let vl,_,t2 = t_open_quant tq2 in
       let bv = List.fold_left Svs.add_left renv.bound_vars vl in
       let renv = { renv with bound_vars = bv } in
       invert_nonvar_pat vl renv (p, t1) t2
199
    | Por (p1, p2), _, _ ->
200
       Debug.dprintf debug_reification "case or@.";
201 202
       begin try invert_pat vl renv (p1, f) t
             with NoReification -> invert_pat vl renv (p2, f) t
203
       end
204
    | Pvar _, Tvar _, Tvar _ | Pvar _, Tvar _, Tapp (_, [])
205
      | Pvar _, Tvar _, Tconst _
206
      -> Debug.dprintf debug_reification "case vars@.";
207
         (renv, t)
208
    | Pvar _, Tapp (ls, _hd::_tl), _
209
      -> Debug.dprintf debug_reification "case interp@.";
210
         invert_interp renv ls t
211 212
    | Papp (cs, [{pat_node = Pvar v}]), Tvar v', Tconst _
         when vs_equal v v'
213
      -> Debug.dprintf debug_reification "case var_const@.";
214
         renv, t_app cs [t] (Some p.pat_ty)
215 216
    | Papp (cs, [{pat_node = Pvar _}]), Tapp(ls, _hd::_tl), _
         when use_interp t (*FIXME*)
217
      -> Debug.dprintf debug_reification "case interp_var@.";
218 219
         let renv, rt = invert_interp renv ls t in
         renv, (t_app cs [rt] (Some p.pat_ty))
220
    | Papp _, Tapp (ls1, _), Tapp(ls2, _) ->
221
       Debug.dprintf debug_reification "head symbol mismatch %a %a@."
222 223
                                   Pretty.print_ls ls1 Pretty.print_ls ls2;
       raise NoReification
224
    | _ -> raise NoReification
225
  and invert_var_pat vl (renv:reify_env) (p,f) t =
226 227 228
    Debug.dprintf debug_reification
      "invert_var_pat p %a f %a t %a@."
      Pretty.print_pat p Pretty.print_term f Pretty.print_term t;
229 230 231 232
    match p.pat_node, f.t_node with
    | Papp (_, [{pat_node = Pvar v1}]),
      Tapp (ffa,[{t_node = Tvar vy}; {t_node = Tvar v2}])
      | Pvar v1, Tapp (ffa,[{t_node = Tvar vy}; {t_node = Tvar v2}])
233 234 235 236 237 238
         when ty_equal v1.vs_ty ty_int
              && Svs.mem v1 p.pat_vars
              && vs_equal v1 v2
              && ls_equal ffa fs_func_app
              && List.exists (fun vs -> vs_equal vs vy) vl (*FIXME*)
      ->
239
       Debug.dprintf debug_reification "case var@.";
240 241 242 243 244
       let rty = (Some p.pat_ty) in
       let app_pat trv = match p.pat_node with
         | Papp (cs, _) -> t_app cs [trv] rty
         | Pvar _ -> trv
         | _ -> assert false in
245 246 247 248 249 250 251 252 253 254
       let rec rm t =
         let t = match t.t_node with
           | Tapp (f,tl) -> t_app f (List.map rm tl) t.t_ty
           | Tvar _ | Tconst _ -> t
           | Tif (f,t1,t2) -> t_if (rm f) (rm t1) (rm t2)
           | Tbinop (op,f1,f2) -> t_binary op (rm f1) (rm f2)
           | Tnot f1 -> t_not (rm f1)
           | Ttrue | Tfalse -> t
           | _ -> t (* FIXME some cases missing *)
         in
Andrei Paskevich's avatar
Andrei Paskevich committed
255
         t_attr_set ?loc:t.t_loc Sattr.empty t
256
       in
257
       let t = rm t in
Andrei Paskevich's avatar
Andrei Paskevich committed
258
       (* remove attributes to identify terms modulo attributes *)
259 260 261
       if Mterm.mem t renv.store
       then
         begin
262
           Debug.dprintf debug_reification "%a exists@." Pretty.print_term t;
263
           (renv, app_pat (t_nat_const (snd (Mterm.find t renv.store))))
264 265 266
         end
       else
         begin
267
           Debug.dprintf debug_reification "%a is new@." Pretty.print_term t;
268 269 270 271 272 273 274
           let bound = match t.t_node with
             | Tvar v -> Svs.mem v renv.bound_vars
             | _ -> false in
           let renv, i=
             if bound
             then let i = renv.bound_fr in
                  { renv with bound_fr = i-1 }, i
275
             else
276 277 278 279 280 281
               let vy = Mty.find vy.vs_ty renv.ty_to_map in
               let fr = renv.fr in
               let store = Mterm.add t (vy, fr) renv.store in
               { renv with store = store; fr = fr + 1 }, fr in
           let const = Number.(ConstInt (int_const_of_int i)) in
           (renv, app_pat (t_const const Ty.ty_int))
282 283
         end
    | _ -> raise NoReification
284
  and invert_pat vl renv (p,f) t =
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
285 286 287 288 289 290 291 292 293 294 295 296 297
    if (oty_equal f.t_ty t.t_ty)
    then
      try invert_nonvar_pat vl renv (p,f) t
      with NoReification -> invert_var_pat vl renv (p,f) t
    else begin
        try
          let crc = Coercion.find renv.crc_map
                                  (Opt.get t.t_ty) (Opt.get f.t_ty) in
          let apply_crc t ls = t_app_infer ls [t] in
          let crc_t = List.fold_left apply_crc t crc in
          assert (oty_equal f.t_ty crc_t.t_ty);
          invert_pat vl renv (p,f) crc_t
        with Not_found ->
298 299 300 301
          Debug.dprintf debug_reification "type mismatch between %a and %a@."
            Pretty.print_ty (Opt.get f.t_ty)
            Pretty.print_ty (Opt.get t.t_ty);
          raise NoReification
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
302
      end
303
  and invert_interp renv ls (t:term) =
304
    let ld = try Opt.get (find_logic_definition renv.kn ls)
305
             with Invalid_argument _ ->
306 307 308 309
               Debug.dprintf debug_reification
                 "did not find def of %a@."
                 Pretty.print_ls ls;
               raise NoReification
310
    in
311
    let vl, f = open_ls_defn ld in
312
    Debug.dprintf debug_reification "invert_interp ls %a t %a@."
313
                                Pretty.print_ls ls Pretty.print_term t;
314
    invert_body { renv with interps = Sls.add ls renv.interps } ls vl f t
315 316 317 318 319 320 321
  and invert_body renv ls vl f t =
    match f.t_node with
    | Tvar v when vs_equal v (List.hd vl) -> renv, t
    | Tif (f, th, el) when t_equal th t_bool_true && t_equal el t_bool_false ->
       invert_body renv ls vl f t
    | Tcase (x, bl)
      ->
322 323
       (match x.t_node with
        | Tvar v when vs_equal v (List.hd vl) -> ()
324
        | _ -> Debug.dprintf debug_reification "not matching on first param@.";
325
               raise NoReification);
326
       Debug.dprintf debug_reification "case match@.";
327
       let rec aux invert = function
328
         | [] -> raise NoReification
329
         | tb::l ->
330
            try invert vl renv (t_open_branch tb) t
331
            with NoReification ->
332
                 Debug.dprintf debug_reification "match failed@."; aux invert l in
333
       (try aux invert_nonvar_pat bl with NoReification -> aux invert_var_pat bl)
334
    | Tapp (ls', _) ->
335
       Debug.dprintf debug_reification "case app@.";
336
       invert_interp renv ls' t
337 338
    | _ -> Debug.dprintf debug_reification "function body not handled@.";
           Debug.dprintf debug_reification "f: %a@." Pretty.print_term f;
339 340 341
           raise NoReification
  and invert_ctx_interp renv ls t l g =
    let ld = try Opt.get (find_logic_definition renv.kn ls)
342
             with Invalid_argument _ ->
343 344 345
               Debug.dprintf debug_reification "did not find def of %a@."
                 Pretty.print_ls ls;
               raise NoReification
346 347
    in
    let vl, f = open_ls_defn ld in
348
    Debug.dprintf debug_reification "invert_ctx_interp ls %a @."
349
                                Pretty.print_ls ls;
350
    let renv = { renv with interps = Sls.add ls renv.interps } in
351 352
    invert_ctx_body renv ls vl f t l g
  and invert_ctx_body renv ls vl f t l g =
353
    match f.t_node with
354
    | Tcase ({t_node = Tvar v}, [tbn; tbc] ) when vs_equal v (List.hd vl) ->
355 356 357
       let ty_g = g.vs_ty in
       let ty_list_g = ty_app ty_list [ty_g] in
       if (not (ty_equal ty_list_g l.vs_ty))
358 359
       then (Debug.dprintf debug_reification
               "bad type for context interp function@.";
360 361 362 363 364 365
             raise NoReification);
       let nil = ns_find_ls th_list.th_export ["Nil"] in
       let cons = ns_find_ls th_list.th_export ["Cons"] in
       let (pn, fn) = t_open_branch tbn in
       let (pc, fc) = t_open_branch tbc in
       begin match pn.pat_node, fn.t_node, pc.pat_node, fc.t_node with
366 367
       | Papp(n, []),
         Tapp(eq'', [{t_node=Tapp(leq,{t_node = Tvar g'}::_)};btr'']),
368
         Papp (c, [{pat_node = Pvar hdl};{pat_node = Pvar tll}]),
369 370 371 372 373 374
         Tbinop(Timplies,
                {t_node=(Tapp(eq, [({t_node = Tapp(leq', _)} as thd); btr]))},
                {t_node = (Tapp(eq',
                    [({t_node =
                         Tapp(ls', {t_node = Tvar tll'}::{t_node=Tvar g''}::_)}
                         as ttl); btr']))})
375
            when ls_equal n nil && ls_equal c cons && ls_equal ls ls'
376
                 && vs_equal tll tll'
377 378 379 380
                 && vs_equal g' g'' && ls_equal leq leq'
                 && List.mem g' vl
                 && not (Mvs.mem tll (t_vars thd))
                 && not (Mvs.mem hdl (t_vars ttl))
381 382 383
                 && ls_equal eq ps_equ && ls_equal eq' ps_equ
                 && ls_equal eq'' ps_equ && t_equal btr t_bool_true
                 && t_equal btr' t_bool_true && t_equal btr'' t_bool_true
384
         ->
385
          Debug.dprintf debug_reification "reifying goal@.";
386 387
          let (renv, rg) = invert_interp renv leq t in
          let renv = { renv with subst = Mvs.add g rg renv.subst } in
388
          Debug.dprintf debug_reification "filling context@.";
389 390 391
          let rec add_to_ctx (renv, ctx) e =
            try
              match e.t_node with
392
              | Teps _ -> (renv, ctx)
393 394 395 396 397 398 399 400
              | Tbinop (Tand,e1,e2) ->
                 add_to_ctx (add_to_ctx (renv, ctx) e1) e2
              | _ ->
                 let (renv,req) = invert_interp renv leq e in
                 (renv,(t_app cons [req; ctx] (Some ty_list_g)))
            with
            | NoReification -> renv,ctx
          in
401 402 403 404 405
          let renv, ctx =
              task_fold
                (fun (renv,ctx) td ->
                  match td.td_node with
                  | Decl {d_node = Dprop (Paxiom, _, e)}
406
                    -> add_to_ctx (renv, ctx) e
407 408 409
                  | Decl {d_node = Dlogic [ls, ld]} when ls.ls_args = []
                    ->
                     add_to_ctx (renv, ctx) (ls_defn_axiom ld)
410 411 412
                  | _-> renv,ctx)
                             (renv, (t_app nil [] (Some ty_list_g))) renv.task in
          { renv with subst = Mvs.add l ctx renv.subst }
413
       | _ -> Debug.dprintf debug_reification "unhandled interp structure@.";
414 415
              raise NoReification
       end
416 417
    | Tif (c, th, el) when t_equal th t_bool_true && t_equal el t_bool_false ->
       invert_ctx_body renv ls vl c t l g
418
    | _ -> Debug.dprintf debug_reification "not a match on list@.";
419 420
           raise NoReification
  in
421 422
  Debug.dprintf debug_reification "reify_term t %a rt %a@."
    Pretty.print_term t Pretty.print_term rt;
423
  if not (oty_equal t.t_ty rt.t_ty)
424 425 426
  then (Debug.dprintf debug_reification "reification type mismatch %a %a@."
          Pretty.print_ty (Opt.get t.t_ty)
          Pretty.print_ty (Opt.get rt.t_ty);
427 428
        raise NoReification);
  match t.t_node, rt.t_node with
429 430 431 432 433 434 435
  | _, Tapp(interp, {t_node = Tvar vx}::vyl)
       when List.mem vx renv.lv
            && List.for_all
                 (fun t -> match t.t_node with
                           | Tvar vy -> List.mem vy renv.lv
                           | _ -> false)
                 vyl  ->
436
     Debug.dprintf debug_reification "case interp@.";
437
     let renv = add_to_maps renv vyl in
438 439
     let renv, x = invert_interp renv interp t in
     { renv with subst = Mvs.add vx x renv.subst }
440
  | Tapp(eq, [t1; t2]), Tapp (eq', [rt1; rt2])
441 442 443
       when ls_equal eq ps_equ && ls_equal eq' ps_equ
            && oty_equal t1.t_ty rt1.t_ty && oty_equal t2.t_ty rt2.t_ty
    ->
444
     Debug.dprintf debug_reification "case eq@.";
445
     reify_term (reify_term renv t1 rt1) t2 rt2
446 447
  | _, Tapp(eq,[{t_node=Tapp(interp, {t_node = Tvar l}::{t_node = Tvar g}::vyl)}; tr])
       when ls_equal eq ps_equ && t_equal tr t_bool_true
448
            && ty_equal (ty_app ty_list [g.vs_ty]) l.vs_ty
449 450 451 452 453 454 455 456
            && List.mem l renv.lv
            && List.mem g renv.lv
            && List.for_all
                 (fun t -> match t.t_node with
                           | Tvar vy -> List.mem vy renv.lv
                           | _ -> false)
                 vyl
    ->
457
     Debug.dprintf debug_reification "case context@.";
458 459
     let renv = add_to_maps renv vyl in
     invert_ctx_interp renv interp t l g
460 461 462
  | Tbinop(Tiff,t,{t_node=Ttrue}), Tapp(eq,[{t_node=Tapp(interp, {t_node = Tvar f}::vyl)}; tr])
       when ls_equal eq ps_equ && t_equal tr t_bool_true
            && t.t_ty=None ->
463 464
     Debug.dprintf debug_reification "case interp_fmla@.";
     Debug.dprintf debug_reification "t %a rt %a@." Pretty.print_term t Pretty.print_term rt;
465 466 467
     let renv = add_to_maps renv vyl in
     let renv, rf = invert_interp renv interp t in
     { renv with subst = Mvs.add f rf renv.subst }
468 469
  | _ -> Debug.dprintf debug_reification "no reify_term match@.";
         Debug.dprintf debug_reification "lv = [%a]@."
470 471 472
                                     (Pp.print_list Pp.space Pretty.print_vs)
                                     renv.lv;
         raise NoReification
473 474

let build_vars_map renv prev =
475
  Debug.dprintf debug_reification "building vars map@.";
476
  let subst, prev = Mvs.fold
477
                (fun vy ty_vars (subst, prev) ->
478 479
                  Debug.dprintf debug_reification "creating var map %a@."
                    Pretty.print_vs vy;
480
                  let ly = create_fsymbol (Ident.id_fresh vy.vs_name.id_string)
481
                             [] ty_vars in
482 483 484 485 486
                  let y = t_app ly [] (Some ty_vars) in
                  let d = create_param_decl ly in
                  let prev = Task.add_decl prev d in
                  Mvs.add vy y subst, prev)
                renv.var_maps (renv.subst, prev) in
487
  let prev, mapdecls =
488 489
    Mvs.fold
      (fun vy _ (prev,prs) ->
490
        Debug.dprintf debug_reification "checking %a@." Pretty.print_vs vy;
491 492 493
        let vs = Mty.find vy.vs_ty renv.ty_to_map in
        if vs_equal vy vs then prev,prs
        else begin
494 495
            Debug.dprintf debug_reification "aliasing %a and %a@."
              Pretty.print_vs vy Pretty.print_vs vs;
496 497 498 499 500 501 502
            let y = Mvs.find vy subst in
            let z = Mvs.find vs subst in
            let et = t_equ y z in
            let pr = create_prsymbol (Ident.id_fresh "map_alias") in
            let d = create_prop_decl Paxiom pr et in
            Task.add_decl prev d, pr::prs end)
      renv.var_maps (prev, []) in
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
503
  if not (List.for_all (fun v -> Mvs.mem v subst) renv.lv)
504 505 506
  then (Debug.dprintf debug_reification "vars not matched: %a@."
          (Pp.print_list Pp.space Pretty.print_vs)
          (List.filter (fun v -> not (Mvs.mem v subst)) renv.lv);
507
        raise (Exit "vars not matched"));
508
  Debug.dprintf debug_reification "all vars matched@.";
509
  let prev, defdecls =
510 511 512 513 514 515 516
    Mterm.fold
      (fun t (vy,i) (prev,prs) ->
        let y = Mvs.find vy subst in
        let et = t_equ
                   (t_app fs_func_app [y; t_nat_const i]
                          t.t_ty)
                   t in
517
        Debug.dprintf debug_reification "%a %d = %a@."
518
                                    Pretty.print_vs vy i Pretty.print_term t;
519 520
        let s = Format.sprintf "y_val%d" i in
        let pr = create_prsymbol (Ident.id_fresh s) in
521 522
        let d = create_prop_decl Paxiom pr et in
        Task.add_decl prev d, pr::prs)
523 524
      renv.store (prev,[]) in
  subst, prev, mapdecls, defdecls
525

526
let build_goals do_trans renv prev mapdecls defdecls subst env lp g rt =
527
  Debug.dprintf debug_refl "building goals@.";
528
  let inst_rt = t_subst subst rt in
529
  Debug.dprintf debug_refl "reified goal instantiated@.";
530
  let inst_lp = List.map (t_subst subst) lp in
531
  Debug.dprintf debug_refl "premises instantiated@.";
532 533
  let hr = create_prsymbol (id_fresh "HR") in
  let d_r = create_prop_decl Paxiom hr inst_rt in
534 535
  let pr = create_prsymbol
             (id_fresh "GR"
Andrei Paskevich's avatar
Andrei Paskevich committed
536
                       ~attrs:(Sattr.singleton expl_reification_check)) in
537 538
  let d = create_prop_decl Pgoal pr g in
  let task_r = Task.add_decl (Task.add_decl prev d_r) d in
539 540
  Debug.dprintf debug_refl "building cut indication rt %a g %a@."
    Pretty.print_term rt Pretty.print_term g;
541
  let compute_hyp_few pr = Compute.normalize_hyp_few None (Some pr) env in
542
  let compute_in_goal = Compute.normalize_goal_transf_all env in
543 544 545 546 547 548
  let ltask_r =
    try let ci =
          match (rt.t_node, g.t_node) with
          | (Tapp(eq, rh::rl),
             Tapp(eq', h::l))
               when ls_equal eq eq' ->
549 550 551 552 553
             List.fold_left2
               (fun ci st rst ->
                 t_and ci (t_equ (t_subst subst rst) st))
               (t_equ (t_subst subst rh) h)
               l rl
554
          | _,_ when g.t_ty <> None -> t_equ (t_subst subst rt) g
555
          | _ -> raise Not_found in
556
        Debug.dprintf debug_refl "cut ok@.";
557
        Trans.apply (Cut.cut ci (Some "interp")) task_r
558
    with Arg_trans _ | TypeMismatch _ | Not_found ->
559
         Debug.dprintf debug_refl "no cut found@.";
560 561
         if do_trans
         then
562 563 564 565 566 567 568
           let g, prev = task_separate_goal task_r in
           let prev = Sls.fold
                     (fun ls t ->
                       Task.add_meta t Compute.meta_rewrite_def [Theory.MAls ls])
                     renv.interps prev in
           let t = Task.add_tdecl prev g in
           let t = Trans.apply (compute_hyp_few hr) t in
569 570
           match t with
           | [t] ->
571 572 573
              let rewrite = Apply.rewrite_list None false true
                              (mapdecls@defdecls) (Some hr) in
              Trans.apply rewrite t
574 575
           | [] -> []
           | _ -> assert false
576
         else [task_r] in
577 578 579
  let lt = List.map (fun ng -> Task.add_decl prev
                       (create_prop_decl Pgoal (create_prsymbol (id_fresh "G")) ng))
                    inst_lp in
580 581 582
  let lt = if do_trans
           then Lists.apply (Trans.apply compute_in_goal) lt
           else lt in
583
  Debug.dprintf debug_refl "done@.";
584 585
  ltask_r@lt

586
let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task ->
587
  let kn = task_known task in
588 589
  let g, prev = Task.task_separate_goal task in
  let g = Apply.term_decl g in
590
  Debug.dprintf debug_refl "start@.";
591 592 593 594 595 596
  let l =
    let kn' = task_known prev in (* TODO Do we want kn here ? *)
    match find_prop_decl kn' pr with
    | (_, t) -> t
    | exception Not_found -> raise (Exit "lemma not found")
  in
597 598 599 600
  let (lp, lv, rt) = Apply.intros l in
  let nt = Args_wrapper.build_naming_tables task in
  let crc = nt.Trans.coercion in
  let renv = reify_term (init_renv kn crc lv env prev) g rt in
601
  let subst, prev, mds, dds = build_vars_map renv prev in
602
  build_goals true renv prev mds dds subst env lp g rt)
603 604 605

open Expr
open Ity
Guillaume Melquiond's avatar
Guillaume Melquiond committed
606
open Wstdlib
607
open Mlinterp
608

609 610 611
exception ReductionFail of reify_env

let reflection_by_function do_trans s env = Trans.store (fun task ->
612
  Debug.dprintf debug_refl "reflection_f start@.";
613
  let kn = task_known task in
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
614 615
  let nt = Args_wrapper.build_naming_tables task in
  let crc = nt.Trans.coercion in
616 617
  let g, prev = Task.task_separate_goal task in
  let g = Apply.term_decl g in
618 619 620 621 622 623 624 625
  let ths = Task.used_theories task in
  let o =
    Mid.fold
      (fun _ th o ->
        try
          let pmod = Pmodule.restore_module th in
          let rs = Pmodule.ns_find_rs pmod.Pmodule.mod_export [s] in
          if o = None then Some (pmod, rs)
626 627
          else (let es = Format.sprintf "module or function %s found twice" s in
                raise (Exit es))
628 629
        with Not_found -> o)
      ths None in
630
  let (_pmod, rs) = if o = None
631
                   then (Debug.dprintf debug_refl "Symbol %s not found@." s;
632
                         raise Not_found)
633
                   else Opt.get o in
634 635
  let lpost = List.map open_post rs.rs_cty.cty_post in
  if List.exists (fun pv -> pv.pv_ghost) rs.rs_cty.cty_args
636
  then (Debug.dprintf debug_refl "ghost parameter@.";
637
        raise (Exit "function has ghost parameters"));
638
  Debug.dprintf debug_refl "building module map@.";
639 640 641 642 643 644 645
  let mm = Mid.fold
             (fun id th acc ->
               try
                 let pm = Pmodule.restore_module th in
                 Mstr.add id.id_string pm acc
               with Not_found -> acc)
             ths Mstr.empty in
646
  Debug.dprintf debug_refl "module map built@.";
647 648
  let args = List.map (fun pv -> pv.pv_vs) rs.rs_cty.cty_args in
  let rec reify_post = function
649
    | [] -> Debug.dprintf debug_refl "no postcondition reifies@.";
650
            raise NoReification
651 652
    | (vres, p)::t -> begin
        try
653 654 655
          Debug.dprintf debug_refl "new post@.";
          Debug.dprintf debug_refl "post: %a, %a@."
            Pretty.print_vs vres Pretty.print_term p;
656
          let (lp, lv, rt) = Apply.intros p in
657
          let lv = lv @ args in
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
658
          let renv = reify_term (init_renv kn crc lv env prev) g rt in
659
          Debug.dprintf debug_refl "computing args@.";
660 661 662 663 664
          let vars =
            List.fold_left
              (fun vars (vs, t) ->
                if List.mem vs args
                then begin
665
                    Debug.dprintf debug_refl "value of term %a for arg %a@."
666 667
                                                Pretty.print_term t
                                                Pretty.print_vs vs;
668
                    Mid.add vs.vs_name (value_of_term kn t) vars end
669 670 671
                else vars)
              Mid.empty
              (Mvs.bindings renv.subst) in
672
          Debug.dprintf debug_refl "evaluating@.";
673
          let res =
674
            try term_of_value (Mlinterp.interp env mm rs vars)
675 676 677
            with Raised (xs,_,cs) ->
              Format.eprintf "Raised %s %a@." (xs.xs_name.id_string)
                (Pp.print_list Pp.semi Expr.print_rs) cs;
678
              raise (ReductionFail renv) in
679
          Debug.dprintf debug_refl "res %a@." Pretty.print_term res;
680 681 682 683 684
          let rinfo = {renv with subst = Mvs.add vres res renv.subst} in
          rinfo, lp, lv, rt
        with NoReification -> reify_post t
      end
  in
685 686 687
  try
    let rinfo, lp, _lv, rt = reify_post lpost in
    let lp = (rs.rs_cty.cty_pre)@lp in
688
    let subst, prev, mds, dds = build_vars_map rinfo prev in
689
    build_goals do_trans rinfo prev mds dds subst env lp g rt
690 691 692
  with
    ReductionFail renv ->
    (* proof failed, show reification context for debugging *)
693
    let _, prev, _, _ = build_vars_map renv prev in
694 695 696
    let fg = create_prsymbol (id_fresh "Failure") in
    let df = create_prop_decl Pgoal fg t_false in
    [Task.add_decl prev df] )
697

698 699 700
let () = wrap_and_register
           ~desc:"reflection_l <prop> attempts to prove the goal by reflection using the lemma prop"
           "reflection_l"
701
           (Tprsymbol Tenvtrans_l) reflection_by_lemma
702

703
let () = wrap_and_register
704
           ~desc:"reflection_f <f> attempts to prove the goal by reflection using the contract of the program function f"
705
           "reflection_f"
706
           (Tstring Tenvtrans_l) (reflection_by_function true)
707

708 709 710 711
let () = wrap_and_register
           ~desc:"reflection_f <f> attempts to prove the goal by reflection using the contract of the program function f, does not automatically perform transformations afterward. Use for debugging."
           "reflection_f_nt"
           (Tstring Tenvtrans_l) (reflection_by_function false)
712 713 714 715 716
(*
Local Variables:
compile-command: "unset LANG; make -C ../.."
End:
*)