summaryrefslogtreecommitdiff
path: root/contrib/subtac/eterm.ml
blob: 859f90136bff1785a063aecbdd3bef754a9b7747 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
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
172
173
174
(**
   - Get types of existentials ;
   - Flatten dependency tree (prefix order) ;
   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
   - Apply term prefixed by quantification on "existentials".
*)

open Term
open Names
open Evd
open List
open Pp
open Util

let reverse_array arr = 
  Array.of_list (List.rev (Array.to_list arr))
    
let trace s = 
  if !Options.debug then (msgnl s; msgerr s)
  else ()

(** Utilities to find indices in lists *)
let list_index x l =
  let rec aux i = function
      k :: tl -> if k = x then i else aux (succ i) tl
    | [] -> raise Not_found
  in aux 0 l

let list_assoc_index x l =
  let rec aux i = function
      (k, _, v) :: tl -> if k = x then i else aux (succ i) tl
    | [] -> raise Not_found
  in aux 0 l

(** Substitute evar references in t using De Bruijn indices, 
  where n binders were passed through. *)
let subst_evars evs n t = 
  let evar_info id = 
    let rec aux i = function
	(k, h, v) :: tl -> 
	  trace (str "Searching for " ++ int id ++ str " found: " ++ int k);
	  if k = id then (i, h, v) else aux (succ i) tl
      | [] -> raise Not_found
    in 
    let (idx, hyps, v) = aux 0 evs in
      n + idx + 1, hyps
  in
  let rec substrec depth c = match kind_of_term c with
    | Evar (k, args) ->
	(let index, hyps = 
	   try evar_info k
	   with Not_found -> 
	     anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
	 in
	 (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
		       int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () );
	 let ex = mkRel (index + depth) in
	   (* Evar arguments are created in inverse order, 
	      and we must not apply to defined ones (i.e. LetIn's)
	   *)
	 let args =
	   let rec aux hyps args acc =
	     match hyps, args with
		 ((_, None, _) :: tlh), (c :: tla) -> 
		   aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
		   aux tlh tla acc
	       | [], [] -> acc
	       | _, _ -> failwith "subst_evars: invalid argument"
	   in aux hyps (Array.to_list args) [] 
	 in
	   mkApp (ex, Array.of_list args))
    | _ -> map_constr_with_binders succ substrec depth c
  in 
    substrec 0 t
      
(** Substitute variable references in t using De Bruijn indices, 
  where n binders were passed through. *)
let subst_vars acc n t = 
  let var_index id = 
    let idx = list_index id acc in
      idx + 1
  in
  let rec substrec depth c = match kind_of_term c with
    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
    | _ -> map_constr_with_binders succ substrec depth c
  in 
    substrec 0 t

(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
  to a product : forall H1 : t1, ..., forall Hn : tn, concl.
  Changes evars and hypothesis references to De Bruijn indices.
*)
let etype_of_evar evs ev hyps =
  let rec aux acc n = function
      (id, copt, t) :: tl ->
	let t' = subst_evars evs n t in
	let t'' = subst_vars acc 0 t' in
 	  mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl)
    | [] ->
	let t' = subst_evars evs n ev.evar_concl in
	  subst_vars acc 0 t'	
  in aux [] 0 (rev hyps)


open Tacticals
    
let eterm_term evm t tycon = 
  (* 'Serialize' the evars, we assume that the types of the existentials
     refer to previous existentials in the list only *)
  let evl = List.rev (to_list evm) in
    trace (str "Eterm, transformed to list");
  let evts = 
    (* Remove existential variables in types and build the corresponding products *)
    fold_right 
      (fun (id, ev) l ->
	 trace (str "Eterm: " ++ str "treating evar: " ++ int id);
	 let hyps = Environ.named_context_of_val ev.evar_hyps in
	 let y' = (id, hyps, etype_of_evar l ev hyps) in
	   y' :: l) 
      evl []
  in 
  let t' = (* Substitute evar refs in the term by De Bruijn indices *)
    subst_evars evts 0 t 
  in
  let evar_names = 
    List.map (fun (id, _, c) -> (id_of_string ("Evar" ^ string_of_int id)), c) evts
  in
  let evar_bl =
    List.map (fun (id, c) -> Name id, None, c) evar_names
  in
  let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in
    (* Generalize over the existential variables *)
  let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl 
  and tycon = option_map 
		(fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
  in
  let _declare_evar (id, c) =
    let id = id_of_string ("Evar" ^ string_of_int id) in
      ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c,
					  Decl_kinds.IsAssumption Decl_kinds.Definitional))
  in
  let _declare_assert acc (id, c) =
    let id = id_of_string ("Evar" ^ string_of_int id) in
      tclTHEN acc (Tactics.assert_tac false (Name id) c)
  in
    (try 
       trace (str "Term given to eterm" ++ spc () ++
	      Termops.print_constr_env (Global.env ()) t);
       trace (str "Term constructed in eterm" ++ spc () ++
	      Termops.print_constr_env (Global.env ()) t'');
       ignore(option_map 
		(fun typ ->
		   trace (str "Type :" ++ spc () ++
			  Termops.print_constr_env (Global.env ()) typ))
		tycon);
     with _ -> ());
    t'', tycon, evar_names

let mkMetas n = 
  let rec aux i acc = 
    if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc)
    else acc
  in aux n []

let eterm evm t (tycon : types option) = 
  let t, tycon, evs = eterm_term evm t tycon in
    match tycon with
	Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) []
      | None -> Tactics.apply_term t (mkMetas (List.length evs))
     
open Tacmach

let etermtac (evm, t) = eterm evm t None