diff options
Diffstat (limited to 'plugins/subtac/eterm.ml')
| -rw-r--r-- | plugins/subtac/eterm.ml | 94 |
1 files changed, 47 insertions, 47 deletions
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml index d65b520b6..3c947e29c 100644 --- a/plugins/subtac/eterm.ml +++ b/plugins/subtac/eterm.ml @@ -16,11 +16,11 @@ open Util open Subtac_utils open Proof_type -let trace s = +let trace s = if !Flags.debug then (msgnl s; msgerr s) else () -let succfix (depth, fixrels) = +let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) type oblinfo = @@ -32,41 +32,41 @@ type oblinfo = ev_typ: types; ev_tac: Tacexpr.raw_tactic_expr option; ev_deps: Intset.t } - -(** Substitute evar references in t using De Bruijn indices, + +(** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) -let subst_evar_constr evs n t = +let subst_evar_constr evs n t = let seen = ref Intset.empty in let transparent = ref Idset.empty in let evar_info id = List.assoc id evs in let rec substrec (depth, fixrels) c = match kind_of_term c with | Evar (k, args) -> - let { ev_name = (id, idstr) ; + let { ev_name = (id, idstr) ; ev_hyps = hyps ; ev_chop = chop } = try evar_info k - with Not_found -> + with Not_found -> anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") in seen := Intset.add id !seen; - (* Evar arguments are created in inverse order, + (* Evar arguments are created in inverse order, and we must not apply to defined ones (i.e. LetIn's) *) - let args = - let n = match chop with None -> 0 | Some c -> c in + let args = + let n = match chop with None -> 0 | Some c -> c in let (l, r) = list_chop n (List.rev (Array.to_list args)) in List.rev r in let args = let rec aux hyps args acc = match hyps, args with - ((_, None, _) :: tlh), (c :: tla) -> + ((_, None, _) :: tlh), (c :: tla) -> aux tlh tla ((substrec (depth, fixrels) c) :: acc) | ((_, Some _, _) :: tlh), (_ :: tla) -> aux tlh tla acc | [], [] -> acc | _, _ -> acc (*failwith "subst_evars: invalid argument"*) - in aux hyps args [] + in aux hyps args [] in if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then transparent := Idset.add idstr !transparent; @@ -74,25 +74,25 @@ let subst_evar_constr evs n t = | Fix _ -> map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c - in + in let t' = substrec (0, []) t in t', !seen, !transparent - -(** Substitute variable references in t using De Bruijn indices, + +(** Substitute variable references in t using De Bruijn indices, where n binders were passed through. *) -let subst_vars acc n t = +let subst_vars acc n t = let var_index id = Util.list_index id acc 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 + 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 variable references. -*) +*) let etype_of_evar evs hyps concl = let rec aux acc n = function (id, copt, t) :: tl -> @@ -102,13 +102,13 @@ let etype_of_evar evs hyps concl = let s' = Intset.union s s' in let trans' = Idset.union trans trans' in (match copt with - Some c -> + Some c -> let c', s'', trans'' = subst_evar_constr evs n c in let c' = subst_vars acc 0 c' in - mkNamedProd_or_LetIn (id, Some c', t'') rest, - Intset.union s'' s', + mkNamedProd_or_LetIn (id, Some c', t'') rest, + Intset.union s'' s', Idset.union trans'' trans' - | None -> + | None -> mkNamedProd_or_LetIn (id, None, t'') rest, s', trans') | [] -> let t', s, trans = subst_evar_constr evs n concl in @@ -117,25 +117,25 @@ let etype_of_evar evs hyps concl = open Tacticals - -let trunc_named_context n ctx = + +let trunc_named_context n ctx = let len = List.length ctx in list_firstn (len - n) ctx - -let rec chop_product n t = + +let rec chop_product n t = if n = 0 then Some t - else + else match kind_of_term t with | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None | _ -> None let evar_dependencies evm ev = - let one_step deps = - Intset.fold (fun ev s -> + let one_step deps = + Intset.fold (fun ev s -> let evi = Evd.find evm ev in Intset.union (Evarutil.evars_of_evar_info evi) s) deps deps - in + in let rec aux deps = let deps' = one_step deps in if Intset.equal deps deps' then deps @@ -143,13 +143,13 @@ let evar_dependencies evm ev = in aux (Intset.singleton ev) let sort_dependencies evl = - List.sort (fun (_, _, deps) (_, _, deps') -> + List.sort (fun (_, _, deps) (_, _, deps') -> if Intset.subset deps deps' then (* deps' depends on deps *) -1 else if Intset.subset deps' deps then 1 else Intset.compare deps deps') evl - -let eterm_obligations env name isevars evm fs ?status t ty = + +let eterm_obligations env name isevars evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in let nc_len = Sign.named_context_length nc in @@ -157,37 +157,37 @@ let eterm_obligations env name isevars evm fs ?status t ty = let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in let sevl = sort_dependencies evl in let evl = List.map (fun (id, ev, _) -> id, ev) sevl in - let evn = + let evn = let i = ref (-1) in - List.rev_map (fun (id, ev) -> incr i; + 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 = + let evts = (* Remove existential variables in types and build the corresponding products *) - fold_right + fold_right (fun (id, (n, nstr), ev) l -> let hyps = Evd.evar_filtered_context ev in let hyps = trunc_named_context nc_len hyps in let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in - let evtyp, hyps, chop = + let evtyp, hyps, chop = match chop_product fs evtyp with | Some t -> t, trunc_named_context fs hyps, fs | None -> evtyp, hyps, 0 in let loc, k = evar_source id isevars in let status = match k with QuestionMark o -> Some o | _ -> status in - let status, chop = match status with + let status, chop = match status with | Some (Define true as stat) -> - if chop <> fs then Define false, None + if chop <> fs then Define false, None else stat, Some chop | Some s -> s, None | None -> Define true, None in - let tac = match ev.evar_extra with - | Some t -> - if Dyn.tag t = "tactic" then + let tac = match ev.evar_extra with + | Some t -> + if Dyn.tag t = "tactic" then Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t)) else None | None -> None @@ -195,14 +195,14 @@ let eterm_obligations env name isevars evm fs ?status t ty = let info = { ev_name = (n, nstr); ev_hyps = hyps; ev_status = status; ev_chop = chop; ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } - in (id, info) :: l) + in (id, info) :: l) evn [] - in + in let t', _, transparent = (* Substitute evar refs in the term by variables *) - subst_evar_constr evts 0 t + subst_evar_constr evts 0 t in let ty, _, _ = subst_evar_constr evts 0 ty in - let evars = + let evars = List.map (fun (_, info) -> let { ev_name = (_, name); ev_status = status; ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info |