summaryrefslogtreecommitdiff
path: root/contrib/subtac/eterm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac/eterm.ml')
-rw-r--r--contrib/subtac/eterm.ml148
1 files changed, 78 insertions, 70 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 859f9013..790e61a0 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -32,47 +32,48 @@ let list_assoc_index x l =
| [] -> 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 subst_evar_constr evs n t =
+ let seen = ref Intset.empty in
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
+ (k, x) :: tl ->
+ if k = id then x else aux (succ i) tl
| [] -> raise Not_found
- in
- let (idx, hyps, v) = aux 0 evs in
- n + idx + 1, hyps
+ in aux 0 evs
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 =
+ let (id, idstr), hyps, _, _ =
+ try evar_info k
+ with Not_found ->
+ anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
+ in
+ seen := Intset.add id !seen;
+ (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+ int (List.length hyps) ++ str " hypotheses"); with _ -> () );
+ (* 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"
+ | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
in aux hyps (Array.to_list args) []
in
- mkApp (ex, Array.of_list args))
+ mkApp (mkVar idstr, Array.of_list args)
| _ -> map_constr_with_binders succ substrec depth c
in
- substrec 0 t
+ let t' = substrec 0 t in
+ t', !seen
+
(** Substitute variable references in t using De Bruijn indices,
where n binders were passed through. *)
@@ -89,73 +90,80 @@ let subst_vars acc n 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.
+ Changes evars and hypothesis references to variable references.
*)
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', s = subst_evar_constr 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 copt', s =
+ match copt with
+ Some c ->
+ let c', s' = subst_evar_constr evs n c in
+ Some c', Intset.union s s'
+ | None -> None, s
+ in
+ let copt' = option_map (subst_vars acc 0) copt' in
+ let rest, s' = aux (id :: acc) (succ n) tl in
+ mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s
| [] ->
- let t' = subst_evars evs n ev.evar_concl in
- subst_vars acc 0 t'
+ let t', s = subst_evar_constr evs n ev.evar_concl in
+ subst_vars acc 0 t', s
in aux [] 0 (rev hyps)
open Tacticals
-let eterm_term evm t tycon =
+let rec take n l =
+ if n = 0 then [] else List.hd l :: take (pred n) (List.tl l)
+
+let trunc_named_context n ctx =
+ let len = List.length ctx in
+ take (len - n) ctx
+
+let eterm_obligations name nclen 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");
+ trace (str "Eterm, transformed to list");
+ let evn =
+ let i = ref (-1) in
+ List.rev_map (fun (id, ev) -> incr i;
+ (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl
+ in
let evts =
(* Remove existential variables in types and build the corresponding products *)
fold_right
- (fun (id, ev) l ->
+ (fun (id, (n, nstr), 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
+ let hyps = trunc_named_context nclen hyps in
+ trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps);
+ let evtyp, deps = etype_of_evar l ev hyps in
+ trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp);
+ let y' = (id, ((n, nstr), hyps, evtyp, deps)) in
y' :: l)
- evl []
+ evn []
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))
+ let t', _ = (* Substitute evar refs in the term by variables *)
+ subst_evar_constr evts 0 t
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)
+ let evars =
+ List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts
in
(try
trace (str "Term given to eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t);
+ 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);
+ Termops.print_constr_env (Global.env ()) t');
+ ignore(iter
+ (fun (name, typ, deps) ->
+ trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
+ Termops.print_constr_env (Global.env ()) typ))
+ evars);
with _ -> ());
- t'', tycon, evar_names
+ Array.of_list (List.rev evars), t'
let mkMetas n =
let rec aux i acc =
@@ -163,12 +171,12 @@ let mkMetas n =
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))
+(* 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
+(* open Tacmach *)
-let etermtac (evm, t) = eterm evm t None
+let etermtac (evm, t) = assert(false) (*eterm evm t None *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 22:23:43 +0000