diff options
Diffstat (limited to 'contrib/subtac/eterm.ml')
| -rw-r--r-- | contrib/subtac/eterm.ml | 51 |
1 files changed, 35 insertions, 16 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 66a2b3601..ced1756f1 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -24,27 +24,43 @@ let list_index x 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 + (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_index id = - let idx = list_assoc_index id evs in - idx + 1 + let evar_info id = + let rec aux i = function + (k, h, v) :: tl -> if k = id then (i, h, v) else aux (succ i) tl + | [] -> raise Not_found + in + let (idx, hyps, v) = aux 0 evs in + idx + 1, hyps in let rec substrec depth c = match kind_of_term c with | Evar (k, args) -> (try - msgnl (str "Evar " ++ int k ++ str " found"); - let ex = -(* mkVar (id_of_string ("Evar" ^ string_of_int k));*) - mkRel (evar_index k + depth) + let index, hyps = evar_info k in + msgnl (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ + int (List.length hyps) ++ str " hypotheses"); + + 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 - (* Evar arguments are created in inverse order *) - let args = List.rev_map (map_constr_with_binders succ substrec depth) (Array.to_list args) in mkApp (ex, Array.of_list args) with Not_found -> msgnl (str "Evar " ++ int k ++ str " not found!!!"); @@ -70,7 +86,7 @@ let subst_vars acc n t = 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 = +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 @@ -79,7 +95,7 @@ let etype_of_evar evs ev = | [] -> let t' = subst_evars evs n ev.evar_concl in subst_vars acc 0 t' - in aux [] 0 (rev (Environ.named_context_of_val ev.evar_hyps)) + in aux [] 0 (rev hyps) open Tacticals @@ -91,8 +107,9 @@ let eterm evm t = let evts = (* Remove existential variables in types and build the corresponding products *) fold_left - (fun l (id, y) -> - let y' = (id, etype_of_evar l y) in + (fun l (id, ev) -> + 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 @@ -102,7 +119,7 @@ let eterm evm t = let t'' = (* Make the lambdas 'generalizing' the existential variables *) fold_left - (fun acc (id, c) -> + (fun acc (id, _, c) -> mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)), c, acc)) t' evts @@ -116,7 +133,9 @@ let eterm evm t = let id = id_of_string ("Evar" ^ string_of_int id) in tclTHEN acc (Tactics.assert_tac false (Name id) c) in - msgnl (str "Term constructed in Eterm" ++ + msgnl (str "Term given to eterm" ++ spc () ++ + Termops.print_constr_env (Global.env ()) t); + msgnl (str "Term constructed in eterm" ++ spc () ++ Termops.print_constr_env (Global.env ()) t''); Tactics.apply_term t'' (List.map (fun _ -> Evarutil.mk_new_meta ()) evts) |