aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac.ml4
-rw-r--r--contrib/subtac/subtac.mli11
-rw-r--r--contrib/subtac/subtac_coercion.ml16
-rw-r--r--contrib/subtac/subtac_command.ml216
-rw-r--r--contrib/subtac/subtac_command.mli1
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.ml3
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.mli11
-rw-r--r--contrib/subtac/subtac_utils.ml21
-rw-r--r--contrib/subtac/subtac_utils.mli11
-rw-r--r--contrib/subtac/test/euclid.v4
10 files changed, 181 insertions, 117 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 4cbfe90cf..fed61fb4c 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -43,7 +43,7 @@ open Eterm
let require_library dirpath =
let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
Library.require_library [qualid] None
-
+(*
let subtac_one_fixpoint env isevars (f, decl) =
let ((id, n, bl, typ, body), decl) =
Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl)
@@ -53,7 +53,7 @@ let subtac_one_fixpoint env isevars (f, decl) =
Ppconstr.pr_constr_expr body)
with _ -> ()
in ((id, n, bl, typ, body), decl)
-
+*)
let subtac_fixpoint isevars l =
(* TODO: Copy command.build_recursive *)
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
index a0d2fb2b9..25922782c 100644
--- a/contrib/subtac/subtac.mli
+++ b/contrib/subtac/subtac.mli
@@ -1,14 +1,3 @@
val require_library : string -> unit
-val subtac_one_fixpoint :
- 'a ->
- 'b ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c
val subtac_fixpoint : 'a -> 'b -> unit
val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index f2a1a0185..70933e99b 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -106,25 +106,25 @@ module Coercion = struct
: (Term.constr -> Term.constr) option
=
let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
- (try trace (str "Coerce called for " ++ (my_print_constr env x) ++
+ (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++
str " and "++ my_print_constr env y ++
str " with evars: " ++ spc () ++
my_print_evardefs !isevars);
with _ -> ());
let rec coerce_unify env x y =
- (try trace (str "coerce_unify from " ++ (my_print_constr env x) ++
+ (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++
str " to "++ my_print_constr env y)
with _ -> ());
try
isevars := the_conv_x_leq env x y !isevars;
- (try (trace (str "Unified " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y));
+ (try debug 1 (str "Unified " ++ (my_print_constr env x) ++
+ str " and "++ my_print_constr env y);
with _ -> ());
None
with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env isevars x y in
- (try trace (str "coerce' from " ++ (my_print_constr env x) ++
+ (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++
str " to "++ my_print_constr env y);
with _ -> ());
match (kind_of_term x, kind_of_term y) with
@@ -370,7 +370,7 @@ module Coercion = struct
let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
(try
- trace (str "inh_conv_coerce_to_fail called for " ++
+ debug 1 (str "inh_conv_coerce_to_fail called for " ++
Termops.print_constr_env env t ++ str " and "++ spc () ++
Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -436,7 +436,7 @@ module Coercion = struct
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
(try
- trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++
+ debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++
Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++
Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -461,7 +461,7 @@ module Coercion = struct
let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
(try
- trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++
+ debug 1 (str "Subtac_coercion.inh_conv_coerces_to called for " ++
Termops.print_constr_env env t ++ str " and "++ spc () ++
Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b09228c06..10c5f580b 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -173,82 +173,146 @@ let list_of_local_binders l =
| [] -> List.rev acc
in aux [] l
-let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+let lift_binders k n l =
+ let rec aux n = function
+ | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+ | [] -> []
+ in aux n l
+
+let rec gen_rels = function
+ 0 -> []
+ | n -> mkRel n :: gen_rels (pred n)
+
+let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
+ let sigma = Evd.empty in
+ let isevars = ref (Evd.create_evar_defs sigma) in
+ let env = Global.env() in
+ let n = out_some n in
+ let pr c = my_print_constr env c in
+ let prr = Printer.pr_rel_context env in
+ let pr_rel env = Printer.pr_rel_context env in
+ let _ =
+ try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
+ Ppconstr.pr_binders bl ++ str " : " ++
+ Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+ Ppconstr.pr_constr_expr body)
+ with _ -> ()
+ in
+ let env', binders_rel = interp_context isevars env bl in
+ let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
+ let before_length, after_length = List.length before, List.length after in
+ 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 = interp_constr isevars envwf r in
+ let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in
+ let argid' = id_of_string (string_of_id argid ^ "'") in
+ let full_length = before_length + 1 + after_length in
+ let wfarg len = (Name argid', None,
+ mkSubset (Name argid') argtyp
+ (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+ in
+ let top_bl = after @ (arg :: before) in
+ let intern_bl = after @ (wfarg 1 :: arg :: before) in
+ let top_env = push_rel_context top_bl env in
+ let intern_env = push_rel_context intern_bl env in
+ let top_arity = interp_type isevars top_env arityc in
+ (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ());
+ let proj = (Lazy.force sig_).Coqlib.proj1 in
+ let projection =
+ mkApp (proj, [| argtyp ;
+ (mkLambda (Name argid', argtyp,
+ (mkApp (wf_rel, [|mkRel 1; mkRel 2|])))) ;
+ mkRel 1
+ |])
+ in
+ (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
+ let intern_arity = substnl [projection] after_length top_arity in
+ (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
+ let intern_arity_prod = it_mkProd_or_LetIn intern_arity intern_bl in
+ let intern_before_env = push_rel_context before env in
+ let intern_fun_bl = after @ [wfarg 1] in
+ (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
+ let intern_fun_arity = intern_arity in
+ (try debug 2 (str "Intern fun arity: " ++
+ my_print_constr intern_env intern_fun_arity) with _ -> ());
+ let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
+ let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
+ let fun_bl = after @ (intern_fun_binder :: [arg]) in
+ (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ());
+ let fun_env = push_rel_context fun_bl intern_before_env in
+ let fun_arity = interp_type isevars fun_env arityc in
+ let intern_body = interp_casted_constr isevars fun_env body fun_arity in
+ let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
+ let _ =
+ try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+ str "Intern bl" ++ prr intern_bl ++ spc () ++
+ str "Top bl" ++ prr top_bl ++ spc () ++
+ str "Intern arity: " ++ pr intern_arity ++
+ str "Top arity: " ++ pr top_arity ++ spc () ++
+ str "Intern body " ++ pr intern_body_lam)
+ with _ -> ()
+ in
+ let impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits top_env top_arity
+ else []
+ in
+ let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
+ let fix_def =
+ mkApp (constr_of_reference (Lazy.force fix_sub_ref),
+ [| argtyp ;
+ wf_rel ;
+ make_existential dummy_loc intern_before_env isevars wf_proof ;
+ prop ;
+ intern_body_lam |])
+ in
+ let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
+ let def = it_mkLambda_or_LetIn def_appl binders_rel in
+ let typ = it_mkProd_or_LetIn top_arity binders_rel in
+ debug 2 (str "Constructed def");
+ debug 2 (my_print_constr intern_before_env def);
+ debug 2 (str "Type: " ++ my_print_constr env typ);
+ let fullcoqc = Evarutil.nf_isevar !isevars def in
+ let fullctyp = Evarutil.nf_isevar !isevars typ in
+ let _ = try trace (str "After evar normalization: " ++ spc () ++
+ str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
+ ++ str "Coq type: " ++ my_print_constr env fullctyp)
+ with _ -> ()
+ 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 tac = Eterm.etermtac (evm, fullcoqc) in
+ trace (str "Starting proof of goal: " ++ my_print_constr env fullctyp);
+ Command.start_proof recname goal_kind fullctyp (fun _ _ -> ());
+ trace (str "Started proof");
+ Pfedit.by tac
+
+let build_mutrec l boxed =
let sigma = Evd.empty
and env0 = Global.env()
- in
+ in ()
+(*
let lnameargsardef =
(*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
- lnameargsardef
+ lnameargsardef
in
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
in
- (* Build the recursive context and notations for the recursive types *)
+ (* Build the recursive context and notations for the recursive types *)
let (rec_sign,rec_impls,arityl) =
List.fold_left
- (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) ->
- let isevars = ref (Evd.create_evar_defs sigma) in
- match ro with
- CStructRec ->
- let arityc = Command.generalize_constr_expr arityc bl in
- let arity = interp_type isevars env0 arityc in
- let impl =
- if Impargs.is_implicit_args()
- then Impargs.compute_implicits env0 arity
- else [] in
- let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
- (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
- | CWfRec r ->
- let n = out_some n in
- let _ =
- try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
- Ppconstr.pr_binders bl ++ str " : " ++
- Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
- Ppconstr.pr_constr_expr body)
- with _ -> ()
- in
- let env', binders_rel = interp_context isevars env0 bl in
- let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
- let argid = match argname with Name n -> n | _ -> assert(false) in
- let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in
- let envwf = push_rel_context before env0 in
- let wf_rel = interp_constr isevars envwf r in
- let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
- let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
- let argid' = id_of_string (string_of_id argid ^ "'") in
- let before_length, after_length = List.length before, List.length after in
- let full_length = before_length + 1 + after_length in
- let wfarg len = (Name argid, None,
- mkSubset (Name argid') argtyp
- (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
- in
- let new_bl = after' @ (accarg :: arg :: before)
- and intern_bl = after @ (wfarg (before_length + 1) :: before)
- in
- let intern_env = push_rel_context intern_bl env0 in
- let env' = push_rel_context new_bl env0 in
- let arity = interp_type isevars intern_env arityc in
- let intern_arity = it_mkProd_or_LetIn arity intern_bl in
- let arity' = interp_type isevars env' arityc in
- let arity' = it_mkProd_or_LetIn arity' new_bl in
- let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
- let _ =
- let pr c = my_print_constr env c in
- let prr = Printer.pr_rel_context env in
- try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
- str "Intern bl" ++ prr intern_bl ++ spc () ++
- str "Extern bl" ++ prr new_bl ++ spc () ++
- str "Intern arity: " ++ pr intern_arity)
- with _ -> ()
- in
- let impl =
- if Impargs.is_implicit_args()
- then Impargs.compute_implicits intern_env arity'
- else [] in
- let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in
- (Environ.push_named (recname,None,arity') env, impls',
- (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl))
+ (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) ->
+ let isevars = ref (Evd.create_evar_defs sigma) in
+ let arityc = Command.generalize_constr_expr arityc bl in
+ let arity = interp_type isevars env0 arityc in
+ let impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits env0 arity
+ else [] in
+ let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+ (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
(env0,[],[]) lnameargsardef in
let arityl = List.rev arityl in
let notations =
@@ -430,6 +494,24 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
match cer with
Environ.NoBody -> trace (str "Constant has no body")
| Environ.Opaque -> trace (str "Constant is opaque")
- )
+ )*)
+
+let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+ match lnameargsardef with
+ | ((id, (n, CWfRec r), bl, typ, body), no) :: [] ->
+ (*let body = Subtac_utils.rewrite_cases env body in*)
+ build_wellfounded (id, n, bl, typ, body) r no boxed
+ | l ->
+ let lnameargsardef =
+ List.map (fun ((id, (n, ro), bl, typ, body), no) ->
+ match ro with
+ CStructRec -> (id, n, bl, typ, body), no
+ | CWfRec _ ->
+ errorlabstrm "Subtac_command.build_recursive"
+ (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
+ lnameargsardef
+ in
+ build_mutrec lnameargsardef boxed;
+ assert(false)
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index e1bbbbb5b..90ffb8925 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -38,5 +38,6 @@ val interp_constr_judgment :
constr_expr -> unsafe_judgment
val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
val recursive_message : global_reference array -> std_ppcmds
+
val build_recursive :
(fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 858fad1a8..bb35833f3 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -60,7 +60,7 @@ let pr_binder_list b =
let rec rewrite_rec_calls l c = c
-
+(*
let rewrite_fixpoint env l (f, decl) =
let (id, (n, ro), bl, typ, body) = f in
let body = rewrite_rec_calls l body in
@@ -151,3 +151,4 @@ let rewrite_fixpoint env l (f, decl) =
Ppconstr.pr_constr_expr body')
in (id, (succ n, ro), bl', typ, body'), decl
+*)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index fafbb2da5..149e75807 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -15,14 +15,3 @@ val list_of_local_binders :
val pr_binder_list :
(('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
val rewrite_rec_calls : 'a -> 'b -> 'b
-val rewrite_fixpoint :
- 'a ->
- 'b ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 59c858a6a..31fea63d5 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -22,12 +22,14 @@ let fixsub = lazy (init_constant fixsub_module "Fix_sub")
let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
-let make_ref s = Qualid (dummy_loc, (qualid_of_string s))
-let well_founded_ref = make_ref "Init.Wf.Well_founded"
-let acc_ref = make_ref "Init.Wf.Acc"
-let acc_inv_ref = make_ref "Init.Wf.Acc_inv"
-let fix_sub_ref = make_ref "Coq.subtac.FixSub.Fix_sub"
-let lt_wf_ref = make_ref "Coq.Wf_nat.lt_wf"
+let make_ref l s = lazy (init_reference l s)
+let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
+let acc_ref = make_ref ["Init";"Wf"] "Acc"
+let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv"
+let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
+let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
+
+let make_ref s = Qualid (dummy_loc, qualid_of_string s)
let sig_ref = make_ref "Init.Specif.sig"
let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
@@ -82,18 +84,19 @@ let my_print_evardefs = Evd.pr_evar_defs
let my_print_tycon_type = Evarutil.pr_tycon_type
+let debug_level = 2
let debug n s =
- if !Options.debug then
+ if !Options.debug && n >= debug_level then
msgnl s
else ()
let debug_msg n s =
- if !Options.debug then s
+ if !Options.debug && n >= debug_level then s
else mt ()
let trace s =
- if !Options.debug then msgnl s
+ if !Options.debug && debug_level > 0 then msgnl s
else ()
let wf_relations = Hashtbl.create 10
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a90f281ff..4b25ff679 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -18,12 +18,11 @@ val fixsub_module : string list
val init_constant : string list -> string -> constr
val init_reference : string list -> string -> global_reference
val fixsub : constr lazy_t
-val make_ref : string -> reference
-val well_founded_ref : reference
-val acc_ref : reference
-val acc_inv_ref : reference
-val fix_sub_ref : reference
-val lt_wf_ref : reference
+val well_founded_ref : global_reference lazy_t
+val acc_ref : global_reference lazy_t
+val acc_inv_ref : global_reference lazy_t
+val fix_sub_ref : global_reference lazy_t
+val lt_wf_ref : global_reference lazy_t
val sig_ref : reference
val proj1_sig_ref : reference
val proj2_sig_ref : reference
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 481b6708d..ba5bdf232 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -12,8 +12,8 @@ reflexivity.
Defined.
Extraction testsig.
-Extraction sigS.
-Extract Inductive sigS => "" [ "" ].
+Extraction sig.
+Extract Inductive sig => "" [ "" ].
Extraction testsig.
Require Import Coq.Arith.Compare_dec.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 12:08:16 +0000