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.ml221
1 files changed, 0 insertions, 221 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
deleted file mode 100644
index 00a69bba..00000000
--- a/contrib/subtac/eterm.ml
+++ /dev/null
@@ -1,221 +0,0 @@
-(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
-(**
- - 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 Sign
-open Names
-open Evd
-open List
-open Pp
-open Util
-open Subtac_utils
-open Proof_type
-
-let trace s =
- if !Flags.debug then (msgnl s; msgerr s)
- else ()
-
-let succfix (depth, fixrels) =
- (succ depth, List.map succ fixrels)
-
-type oblinfo =
- { ev_name: int * identifier;
- ev_hyps: named_context;
- ev_status: obligation_definition_status;
- ev_chop: int option;
- ev_loc: Util.loc;
- ev_typ: types;
- ev_tac: Tacexpr.raw_tactic_expr option;
- ev_deps: Intset.t }
-
-(** Substitute evar references in t using De Bruijn indices,
- where n binders were passed through. *)
-
-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) ;
- ev_hyps = hyps ; ev_chop = chop } =
- try evar_info k
- 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,
- 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 (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) ->
- 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
- 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;
- mkApp (mkVar idstr, Array.of_list args)
- | Fix _ ->
- map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
- | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
- in
- let t' = substrec (0, []) t in
- t', !seen, !transparent
-
-
-(** 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 = 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
- 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.
- A little optimization: don't include unnecessary let-ins and their dependencies.
-*)
-let etype_of_evar evs hyps concl =
- let rec aux acc n = function
- (id, copt, t) :: tl ->
- let t', s, trans = subst_evar_constr evs n t in
- let t'' = subst_vars acc 0 t' in
- let rest, s', trans' = aux (id :: acc) (succ n) tl in
- let s' = Intset.union s s' in
- let trans' = Idset.union trans trans' in
- (match copt with
- Some c ->
-(* if noccurn 1 rest then lift (-1) rest, s', trans' *)
-(* else *)
- 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',
- Idset.union trans'' trans'
- | None ->
- mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
- | [] ->
- let t', s, trans = subst_evar_constr evs n concl in
- subst_vars acc 0 t', s, trans
- in aux [] 0 (rev hyps)
-
-
-open Tacticals
-
-let trunc_named_context n ctx =
- let len = List.length ctx in
- list_firstn (len - n) ctx
-
-let rec chop_product n t =
- if n = 0 then Some t
- 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 evi = Evd.find evm ev in
- Intset.union (Evarutil.evars_of_evar_info evi) s)
- deps deps
- in
- let rec aux deps =
- let deps' = one_step deps in
- if Intset.equal deps deps' then deps
- else aux deps'
- in aux (Intset.singleton ev)
-
-let sort_dependencies evl =
- 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 =
- (* 'Serialize' the evars *)
- let nc = Environ.named_context env in
- let nc_len = Sign.named_context_length nc in
- let evl = List.rev (to_list evm) in
- 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 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, (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 =
- 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
- | Some (Define true as stat) ->
- 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
- Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t))
- else None
- | None -> None
- in
- 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)
- evn []
- in
- let t', _, transparent = (* Substitute evar refs in the term by variables *)
- subst_evar_constr evts 0 t
- in
- let ty, _, _ = subst_evar_constr evts 0 ty in
- 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
- in
- let status = match status with
- | Define true when Idset.mem name transparent -> Define false
- | _ -> status
- in name, typ, loc, status, deps, tac) evts
- in Array.of_list (List.rev evars), t', ty
-
-let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
-
-let etermtac (evm, t) = assert(false) (*eterm evm t None *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 03:26:58 +0000