aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/subtac/eterm.ml212
-rw-r--r--contrib/subtac/eterm.mli5
-rw-r--r--contrib/subtac/g_subtac.ml45
-rw-r--r--contrib/subtac/subtac_command.ml14
-rw-r--r--contrib/subtac/subtac_obligations.ml81
-rw-r--r--contrib/subtac/subtac_obligations.mli9
-rw-r--r--contrib/subtac/subtac_pretyping.ml4
7 files changed, 139 insertions, 191 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 9c11569ef..b95f643a5 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -32,71 +32,33 @@ 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 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
- 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
- | _, _ -> 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
-
let subst_evar_constr evs n t =
+ let seen = ref Intset.empty in
let evar_info id =
let rec aux i = function
- (k, n, h, v) :: tl ->
- if k = id then (n, 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 (c, hyps, v) = aux 0 evs in
- c, hyps
+ in aux 0 evs
in
let rec substrec depth c = match kind_of_term c with
| Evar (k, args) ->
- (let ex, 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 _ -> () );
- (* 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)
@@ -106,10 +68,11 @@ let subst_evar_constr evs n t =
| _, _ -> 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,
@@ -127,70 +90,31 @@ 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
- let copt' = option_map (subst_evars evs n) copt in
+ 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
- mkNamedProd_or_LetIn (id, copt', t'') (aux (id :: acc) (succ n) tl)
+ 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 =
- (* 'Serialize' the evars, we assume that the types of the existentials
- refer to previous existentials in the list only *)
- let evl = 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 evtyp = etype_of_evar l ev hyps in
- trace (str "Evar's type is: " ++ Termops.print_constr_env (Global.env ()) evtyp);
- let y' = (id, hyps, evtyp) 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 =
- let i = ref 0 in
- List.map (fun (id, _, c) -> incr i; (id_of_string ("evar_" ^ string_of_int !i)), 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
- (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 rec take n l =
if n = 0 then [] else List.hd l :: take (pred n) (List.tl l)
@@ -203,34 +127,30 @@ let eterm_obligations name nclen evm t tycon =
refer to previous existentials in the list only *)
let evl = to_list evm in
trace (str "Eterm, transformed to list");
+ let evn =
+ let i = ref (-1) in
+ List.map (fun (id, ev) -> incr i;
+ (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int !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 hyps = trunc_named_context nclen hyps in
- trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps);
- let evtyp = etype_of_evar l ev hyps in
- trace (str "Evar's type is: " ++ Termops.print_constr_env (Global.env ()) evtyp);
- let y' = (id, hyps, evtyp) 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 evar_names =
- let i = ref 0 in
- List.map (fun (id, h, c) -> incr i;
- (id, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int !i), h, c)) evts
- in
- let t' = (* Substitute evar refs in the term by De Bruijn indices *)
- subst_evar_constr (List.map (fun (id, n, h, c) -> id, mkVar n, h, c) evar_names) 0 t
+ let t', _ = (* Substitute evar refs in the term by variables *)
+ subst_evar_constr evts 0 t
in
- let _, evars =
- fold_right
- (fun (_, n, h, c) (acc, l) ->
- let evt = Termops.it_mkProd_wo_LetIn c acc in
- ((Name n, None, c) :: acc, (n, evt) :: l))
- evar_names ([], [])
+ let evars =
+ List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts
in
(try
trace (str "Term given to eterm" ++ spc () ++
@@ -238,26 +158,12 @@ let eterm_obligations name nclen evm t tycon =
trace (str "Term constructed in eterm" ++ spc () ++
Termops.print_constr_env (Global.env ()) t');
ignore(iter
- (fun (n, typ) ->
- trace (str "Evar :" ++ spc () ++ str (string_of_id n) ++
+ (fun (name, typ, deps) ->
+ trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
Termops.print_constr_env (Global.env ()) typ))
evars);
with _ -> ());
- let subst_closure l =
- let l' = List.map2 (fun (id, _, h, c) cst -> (id, cst, h, c)) evar_names l in
- let _, l'' =
- List.fold_right
- (fun (id, cst, h, c) (acc, res) ->
- let cst' = applist (cst, List.rev acc) in
- (cst' :: acc, (id, cst', h, c) :: res))
- l' ([], [])
- in
- let t' = subst_evar_constr l'' 0 t in
- trace (str "Term constructed in eterm" ++ spc () ++
- Termops.print_constr_env (Global.env ()) t');
- t'
- in
- subst_closure, evars
+ Array.of_list evars, t'
let mkMetas n =
let rec aux i acc =
@@ -265,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 *)
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index dec9efa8b..77d9f293d 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -12,12 +12,13 @@ open Tacmach
open Term
open Evd
open Names
+open Util
val mkMetas : int -> constr list
-val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list
+(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
val eterm_obligations : identifier -> int -> evar_map -> constr -> types option ->
- (constr list -> constr) * (identifier * types) list
+ (identifier * types * Intset.t) array * constr (* Obl. name, type as product and dependencies as indexes into the array *)
val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index ff3bcb82e..1ec77c690 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -30,6 +30,7 @@ open Topconstr
module Gram = Pcoq.Gram
module Vernac = Pcoq.Vernac_
+module Tactic = Pcoq.Tactic
module SubtacGram =
struct
@@ -76,4 +77,8 @@ VERNAC COMMAND EXTEND Subtac
[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name) ]
| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None) ]
+| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ]
+| [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ]
+| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ]
+| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ]
END
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index e9e26fb88..b433af2cc 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -304,16 +304,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
in
let evm = non_instanciated_map env isevars in
let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
- let evars_def, evars = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
+ let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
(try trace (str "Generated obligations : ");
- List.iter
- (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+ Array.iter
+ (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
evars;
with _ -> ());
trace (str "Adding to obligations list");
Subtac_obligations.add_entry recname evars_def fullctyp evars;
trace (str "Added to obligations list")
-
+(*
let build_mutrec l boxed =
let sigma = Evd.empty
and env0 = Global.env()
@@ -524,7 +524,7 @@ let build_mutrec l boxed =
Environ.NoBody -> trace (str "Constant has no body")
| Environ.Opaque -> trace (str "Constant is opaque")
)
-
+*)
let out_n = function
Some n -> n
| None -> 0
@@ -544,8 +544,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
errorlabstrm "Subtac_command.build_recursive"
(str "Well-founded fixpoints not allowed in mutually recursive blocks"))
lnameargsardef
- in
- build_mutrec lnameargsardef boxed
+ in assert(false)
+ (*build_mutrec lnameargsardef boxed*)
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 195c879c9..859180036 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -71,7 +71,7 @@ let declare_definition prg =
Subtac_utils.definition_message prg.prg_name
open Evd
-
+
let add_entry n b t obls =
Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
let try_tactics e =
@@ -103,26 +103,11 @@ let add_entry n b t obls =
declare_definition prg
else
from_prg := ProgMap.add n prg !from_prg
-
-(*
-let (theory_to_obj, obj_to_theory) =
- let cache_th (name,th) = add_entry name th
- and export_th x = Some x in
- declare_object
- {(default_object "program-tcc") with
- open_function = (fun i o -> if i=1 then cache_th o);
- cache_function = cache_th;
- subst_function = (fun _ -> assert(false));
- classify_function = (fun (_,x) -> Dispose);
- export_function = export_th }
-*)
let error s = Util.error s
-let subtac_obligation (user_num, name) =
- let num = pred user_num in
+let get_prog name =
let prg_infos = !from_prg in
- let prg =
match name with
Some n -> ProgMap.find n prg_infos
| None ->
@@ -131,7 +116,20 @@ let subtac_obligation (user_num, name) =
0 -> error "No obligations remaining"
| 1 -> map_first prg_infos
| _ -> error "More than one program with unsolved obligations")
- in
+
+let update_obls prg obls rem =
+ let prg' = { prg with prg_obligations = (obls, rem) } in
+ if rem > 1 then (
+ debug 2 (int rem ++ str " obligations remaining");
+ from_prg := map_replace prg.prg_name prg' !from_prg)
+ else (
+ declare_definition prg';
+ from_prg := ProgMap.remove prg.prg_name !from_prg
+ )
+
+let subtac_obligation (user_num, name) =
+ let num = pred user_num in
+ let prg = get_prog name in
let obls, rem = prg.prg_obligations in
if num < Array.length obls then
let obl = obls.(num) in
@@ -143,14 +141,7 @@ let subtac_obligation (user_num, name) =
let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
- let prg' = { prg with prg_obligations = (obls, pred rem) } in
- if rem > 1 then (
- debug 2 (int rem ++ str " obligations remaining");
- from_prg := map_replace prg.prg_name prg' !from_prg)
- else (
- declare_definition prg';
- from_prg := ProgMap.remove prg.prg_name !from_prg
- ));
+ update_obls prg obls (pred rem));
trace (str "Started obligation " ++ int user_num ++ str " proof")
| Some r -> error "Obligation already solved"
else error (sprintf "Unknown obligation number %i" (succ num))
@@ -166,3 +157,41 @@ let obligations_of_evars evars =
obl_body = None;
}) evars)
in arr, Array.length arr
+
+let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ;
+ evar_concl = o.obl_type ;
+ evar_body = Evar_empty ;
+ evar_extra = None }
+
+
+
+let solve_obligations n tac =
+ let prg = get_prog n in
+ let obls, rem = prg.prg_obligations in
+ let rem = ref rem in
+ let obls' =
+ Array.map (fun x ->
+ match x.obl_body with
+ Some _ -> x
+ | None ->
+ try
+ let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in
+ decr rem;
+ { x with obl_body = Some t }
+ with _ -> x)
+ obls
+ in
+ update_obls prg obls' !rem
+
+open Pp
+let show_obligations n =
+ let prg = get_prog n in
+ let obls, rem = prg.prg_obligations in
+ msgnl (int rem ++ str " obligation(s) remaining: ");
+ Array.iteri (fun i x ->
+ match x.obl_body with
+ None -> msgnl (int i ++ str " : " ++ spc () ++
+ my_print_constr (Global.env ()) x.obl_type)
+ | Some _ -> ())
+ obls
+
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 413272980..7d93d57bb 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,3 +1,10 @@
-val add_entry : Names.identifier -> (Term.constr list -> Term.constr) -> Term.types -> (Names.identifier * Term.types) list -> unit
+open Util
+
+val add_entry : Names.identifier -> Term.constr -> Term.types ->
+ (Names.identifier * Term.types * Intset.t) array -> unit
val subtac_obligation : int * Names.identifier option -> unit
+
+val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
+
+val show_obligations : Names.identifier option -> unit
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index b3f8e2210..f518f1ccf 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -158,6 +158,6 @@ let subtac_proof env isevars id l c tycon =
let nc = named_context env in
let nc_len = named_context_length nc in
let evm, coqc, coqt = subtac_process env isevars id l c tycon in
- let evars_def, evars = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
+ let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
trace (str "Adding to obligations list");
- add_entry id evars_def coqt evars
+ add_entry id def coqt evars
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 08:55:55 +0000