diff options
author | 2006-06-20 13:52:21 +0000 | |
---|---|---|
committer | 2006-06-20 13:52:21 +0000 | |
commit | 6314b34d1eb8d8614706068020566d776f0a50fb (patch) | |
tree | fff299ea7ce4c6538e457a413202051a1ace2ee0 | |
parent | cc68954e80969fbc73b60c1ce6e4ad4ed553ccd7 (diff) |
Rewrite of the recursive defs handling in progress.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8964 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/subtac/subtac.ml | 4 | ||||
-rw-r--r-- | contrib/subtac/subtac.mli | 11 | ||||
-rw-r--r-- | contrib/subtac/subtac_coercion.ml | 16 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 216 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.mli | 1 | ||||
-rw-r--r-- | contrib/subtac/subtac_interp_fixpoint.ml | 3 | ||||
-rw-r--r-- | contrib/subtac/subtac_interp_fixpoint.mli | 11 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 21 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.mli | 11 | ||||
-rw-r--r-- | contrib/subtac/test/euclid.v | 4 |
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. |