summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
-rw-r--r--contrib/subtac/subtac_command.ml107
1 files changed, 44 insertions, 63 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index c738d7a6..b433af2c 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -43,6 +43,7 @@ open Notation
module SPretyping = Subtac_pretyping.Pretyping
open Subtac_utils
open Pretyping
+open Subtac_obligations
(*********************************************************************)
(* Functions to parse and interpret constructions *)
@@ -149,15 +150,6 @@ let collect_non_rec env =
in
searchrec []
-let definition_message id =
- Options.if_verbose message ((string_of_id id) ^ " is defined")
-
-let recursive_message v =
- match Array.length v with
- | 0 -> error "no recursive definition"
- | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
- | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
- spc () ++ str "are recursively defined")
let filter_map f l =
let rec aux acc = function
@@ -190,9 +182,12 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let env = Global.env() in
let pr c = my_print_constr env c in
let prr = Printer.pr_rel_context env in
+ let prn = Printer.pr_named_context env in
let pr_rel env = Printer.pr_rel_context env in
+ let nc = named_context env in
+ let nc_len = named_context_length nc in
let _ =
- try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
+ try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
Ppconstr.pr_binders bl ++ str " : " ++
Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
Ppconstr.pr_constr_expr body)
@@ -204,25 +199,35 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let argid = match argname with Name n -> n | _ -> assert(false) in
let _liftafter = lift_binders 1 after_length after in
let envwf = push_rel_context before env in
- let wf_rel, measure_fn =
- let rconstr = interp_constr isevars envwf r in
- if measure then
- let lt_rel = constr_of_global (Lazy.force lt_ref) in
- let name s = Name (id_of_string s) in
- mkLambda (name "x", argtyp,
- mkLambda (name "y", argtyp,
- mkApp (lt_rel,
- [| mkApp (rconstr, [| mkRel 2 |]) ;
- mkApp (rconstr, [| mkRel 1 |]) |]))),
- Some rconstr
- else rconstr, None
+ let wf_rel, wf_rel_fun, measure_fn =
+ let rconstr_body, rconstr =
+ let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
+ let env = push_rel_context [arg] envwf in
+ let capp = interp_constr isevars env app in
+ capp, mkLambda (argname, argtyp, capp)
+ in
+ if measure then
+ let lt_rel = constr_of_global (Lazy.force lt_ref) in
+ let name s = Name (id_of_string s) in
+ let wf_rel_fun =
+ (fun x y ->
+ mkApp (lt_rel, [| subst1 x rconstr_body;
+ subst1 y rconstr_body |]))
+ in
+ let wf_rel =
+ mkLambda (name "x", argtyp,
+ mkLambda (name "y", lift 1 argtyp,
+ wf_rel_fun (mkRel 2) (mkRel 1)))
+ in
+ wf_rel, wf_rel_fun , Some rconstr
+ else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None
in
let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
in
let argid' = id_of_string (string_of_id argid ^ "'") in
let wfarg len = (Name argid', None,
- mkSubset (Name argid') argtyp
- (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+ mkSubset (Name argid') argtyp
+ (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
in
let top_bl = after @ (arg :: before) in
let intern_bl = after @ (wfarg 1 :: arg :: before) in
@@ -234,7 +239,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let projection =
mkApp (proj, [| argtyp ;
(mkLambda (Name argid', argtyp,
- (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ;
+ (wf_rel_fun (mkRel 1) (mkRel 3)))) ;
mkRel 1
|])
in
@@ -299,40 +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_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in
- let evars_typ = out_some evars_typ in
- (try trace (str "Building evars sum for : ");
- List.iter
- (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
- evars;
- with _ -> ());
- let (sum_tac, sumg) = Subtac_utils.build_dependent_sum evars in
- (try trace (str "Evars sum: " ++ my_print_constr env sumg);
- trace (str "Evars type: " ++ my_print_constr env evars_typ);
- with _ -> ());
- let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
- Command.start_proof proofid goal_proof_kind sumg
- (fun strength gr ->
- debug 2 (str "Proof finished");
- let def = constr_of_global gr in
- let args = Subtac_utils.destruct_ex def sumg in
- let _, newdef = decompose_lam_n (List.length args) evars_def in
- let constr = Term.substl (List.rev args) newdef in
- debug 2 (str "Applied existentials : " ++ my_print_constr env constr);
- let ce =
- { const_entry_body = constr;
- const_entry_type = Some fullctyp;
- const_entry_opaque = false;
- const_entry_boxed = boxed}
- in
- let _constant = Declare.declare_constant
- recname (DefinitionEntry ce,IsDefinition Definition)
- in
- definition_message recname);
- trace (str "Started existentials proof");
- Pfedit.by sum_tac;
- trace (str "Applied sum tac")
-
+ let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
+ (try trace (str "Generated obligations : ");
+ 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()
@@ -543,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
@@ -563,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;
- assert(false)
+ in assert(false)
+ (*build_mutrec lnameargsardef boxed*)
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 01:26:23 +0000