diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-15 10:06:40 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-15 10:06:40 +0000 |
commit | b31c4c29e921fe581584f051ebc04228303ddfdb (patch) | |
tree | 88a478593b1685ab5a5d77a7b0c8acaca9524719 | |
parent | c33019051c716916414320b8b676202b18e2e8e4 (diff) |
Various subtac fixes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9485 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/subtac/FunctionalExtensionality.v | 3 | ||||
-rw-r--r-- | contrib/subtac/Utils.v | 2 | ||||
-rw-r--r-- | contrib/subtac/eterm.ml | 31 | ||||
-rw-r--r-- | contrib/subtac/g_subtac.ml4 | 4 | ||||
-rw-r--r-- | contrib/subtac/subtac.ml | 6 | ||||
-rw-r--r-- | contrib/subtac/subtac_cases.ml | 211 | ||||
-rw-r--r-- | contrib/subtac/subtac_coercion.ml | 143 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 118 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 136 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.mli | 2 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 29 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 8 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 6 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.mli | 1 | ||||
-rw-r--r-- | contrib/subtac/test/euclid.v | 14 |
15 files changed, 375 insertions, 339 deletions
diff --git a/contrib/subtac/FunctionalExtensionality.v b/contrib/subtac/FunctionalExtensionality.v index 24c2f0142..1a12ac824 100644 --- a/contrib/subtac/FunctionalExtensionality.v +++ b/contrib/subtac/FunctionalExtensionality.v @@ -15,8 +15,7 @@ Lemma fix_sub_eq_ext : (F_sub : forall x : A, (forall {y : A | R y x}, P (`y)) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = - let f_sub := F_sub in - F_sub x (fun {y : A | R y x}=> Fix A R Rwf P f_sub (`y)). + F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)). Proof. intros ; apply Fix_eq ; auto. intros. diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 6b613b0de..412d5ae3b 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -44,7 +44,7 @@ end. Ltac destruct_exists := repeat (destruct_one_pair) . -Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in *. +Ltac subtac_simpl := hnf ; intros ; destruct_exists ; try subst. (* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *) Ltac destruct_call f := diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 8ec173630..1844fea55 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -52,8 +52,8 @@ let subst_evar_constr evs n t = 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 _ -> () ); +(* (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) *) @@ -126,7 +126,6 @@ let eterm_obligations name nclen evm t tycon = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) let evl = List.rev (to_list evm) in - trace (str "Eterm, transformed to list"); let evn = let i = ref (-1) in List.rev_map (fun (id, ev) -> incr i; @@ -136,13 +135,9 @@ let eterm_obligations name nclen evm t tycon = (* Remove existential variables in types and build the corresponding products *) fold_right (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, 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 ++ - str " depends on evars : " ++ str (Subtac_utils.string_of_intset deps)); let y' = (id, ((n, nstr), hyps, evtyp, deps)) in y' :: l) evn [] @@ -153,17 +148,17 @@ let eterm_obligations name nclen evm t tycon = let evars = List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts 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(iter - (fun (name, typ, deps) -> - trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ - Termops.print_constr_env (Global.env ()) typ)) - evars); - with _ -> ()); +(* (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(iter *) +(* (fun (name, typ, deps) -> *) +(* trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ *) +(* Termops.print_constr_env (Global.env ()) typ)) *) +(* evars); *) +(* with _ -> ()); *) Array.of_list (List.rev evars), t' let mkMetas n = diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 129ac75df..337cc09fc 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -109,6 +109,10 @@ VERNAC COMMAND EXTEND Subtac_Solve_Obligations | [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] END +VERNAC COMMAND EXTEND Subtac_Set_Solver +| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ] +END + VERNAC COMMAND EXTEND Subtac_Show_Obligations | [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] | [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 4433239f3..a7ad70c8a 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -155,14 +155,16 @@ let start_proof_and_print env isevars idopt k t hook = print_subgoals () (*if !pcoq <> None then (out_some !pcoq).start_proof ()*) +let _ = Subtac_obligations.set_default_tactic + (Tacinterp.eval_tactic (utils_call "subtac_simpl" [])) + + let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; (* check_required_library ["Coq";"Logic";"JMeq"]; *) require_library "Coq.subtac.FixSub"; require_library "Coq.subtac.Utils"; - Subtac_obligations.set_default_tactic - (Tacinterp.eval_tactic (utils_call "subtac_simpl" [])); let env = Global.env () in let isevars = ref (create_evar_defs Evd.empty) in try diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index e6404d7f2..cea3fbf51 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1188,8 +1188,6 @@ let rec generalize_problem pb = function | [] -> pb | i::l -> let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in - trace (str "In generalize_problem"); - debug 4 (str "Generalize problem: decl " ++ my_print_context (push_rel d pb.env)); let pb' = generalize_problem pb l in let tomatch = lift_tomatch_stack 1 pb'.tomatch in let tomatch = regeneralize_index_tomatch (i+1) tomatch in @@ -1204,13 +1202,7 @@ let build_leaf pb = | None -> anomaly "Predicate not found" | Some (PrCcl typ) -> mk_tycon typ | Some _ -> anomaly "not all parameters of pred have been consumed" in - (try trace (str "In build leaf:"); - trace (str "typing: " ++ my_print_rawconstr rhs.rhs_env rhs.it); - trace (str "env is: " ++ my_print_env rhs.rhs_env) - with _ -> trace (str "error")); - let x = tag, pb.typing_function tycon rhs.rhs_env rhs.it in - trace (str "end build leaf"); - x + tag, pb.typing_function tycon rhs.rhs_env rhs.it (* Building the sub-problem when all patterns are variables *) let shift_problem (current,t) pb = @@ -1340,8 +1332,6 @@ and match_current pb tomatch = let ci = make_case_info pb.env mind RegularStyle tags in let case = mkCase (ci,nf_betaiota pred,current,brvals) in let inst = List.map mkRel deps in - debug 4 (str "Building app: " ++ my_print_constr pb.env (applist (case, inst)) ++ - str " for deps " ++ str (string_of_list "," string_of_int deps)); pattern_status tags, { uj_val = applist (case, inst); uj_type = substl inst typ } @@ -1358,7 +1348,6 @@ and compile_generalization pb d rest = tomatch = rest; pred = option_map ungeneralize_predicate pb.pred; mat = List.map (push_rels_eqn [d]) pb.mat } in - debug 4 (str "Compile generalization: " ++ my_print_env pb.env); let patstat,j = compile pb in patstat, { uj_val = mkLambda_or_LetIn d j.uj_val; @@ -1628,7 +1617,7 @@ let constr_of_pat env isevars ty pat = (* trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); *) PatVar (l, name), [name, None, ty], mkRel 1, 1 | PatCstr (l,((_, i) as cstr),args,alias) -> - let ind = inductive_of_constructor cstr in + let _ind = inductive_of_constructor cstr in let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) ty in let ind, params = dest_ind_family indf in let cstrs = get_constructors env indf in @@ -1656,9 +1645,9 @@ let constr_of_pat env isevars ty pat = else pat', sign, app, n in let pat', sign, y, z = typ env ty pat in - let prod = it_mkProd_or_LetIn y sign in - trace (str "Pattern: " ++ Printer.pr_cases_pattern pat ++ str " becomes constr : " ++ - my_print_constr env prod); +(* let prod = it_mkProd_or_LetIn y sign in *) +(* trace (str "Pattern: " ++ Printer.pr_cases_pattern pat ++ str " becomes constr : " ++ *) +(* my_print_constr env prod); *) pat', (sign, y) let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |]) @@ -1707,49 +1696,56 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = in let newpatterns, pats = List.split pats in let rhs_rels, signlen = - List.fold_left (fun (env, n) (sign,_) -> (sign @ env, List.length sign + n)) + List.fold_left (fun (renv, n) (sign,_) -> + ((lift_rel_context n sign) @ renv, List.length sign + n)) ([], 0) pats in let eqs, _, _ = List.fold_left2 (fun (eqs, n, slen) (sign, c) (tm, ty) -> - let len = n + signlen in - let cstrlen = slen - List.length sign in - let cstr = liftn (signlen - slen) signlen (lift cstrlen c) in + let len = n + signlen in (* Number of already defined equations + signature *) + let csignlen = List.length sign in + let slen' = slen - csignlen in (* Lift to get pattern variables signature *) + let c = liftn (signlen - slen) signlen c in (* Lift to jump over previous ind signatures for pattern variables outside sign + in c (e.g. type arguments of constructors instanciated by variables ) *) + let cstr = lift (slen' + n) c in +(* trace (str "lift " ++ my_print_constr (push_rels sign env) c ++ *) +(* str " by " ++ int ++ str " to get " ++ *) +(* my_print_constr (push_rels sign env) cstr); *) let app = mkApp (Lazy.force eq_ind, [| lift len (type_of_tomatch ty); cstr; lift len tm |]) - in app :: eqs, succ n, cstrlen + 1) + in app :: eqs, succ n, slen') ([], 0, signlen) pats tomatchs in let eqs_rels = List.map (fun eq -> Name (id_of_string "H"), None, eq) eqs in (* let ineqs = build_ineqs eqns newpatterns in *) let rhs_rels' = eqs_rels @ rhs_rels in let rhs_env = push_rels rhs_rels' env in - (try trace (str "branch env: " ++ print_env rhs_env) - with _ -> trace (str "error in print branch env")); +(* (try trace (str "branch env: " ++ print_env rhs_env) *) +(* with _ -> trace (str "error in print branch env")); *) let tycon = lift_tycon (List.length eqs + signlen) tycon in let j = typing_fun tycon rhs_env eqn.rhs.it in - (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ - str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); - with _ -> - trace (str "Error in typed branch pretty printing")); +(* (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *) +(* str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *) +(* with _ -> *) +(* trace (str "Error in typed branch pretty printing")); *) let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in - (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) - with _ -> trace (str "Error in branch decl pp")); +(* (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *) +(* with _ -> trace (str "Error in branch decl pp")); *) let branch = let bref = RVar (dummy_loc, branch_name) in - match vars_of_ctx rhs_rels' with + match vars_of_ctx rhs_rels with [] -> bref | l -> RApp (dummy_loc, bref, l) in - let branch = - List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels - in - (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) - with _ -> trace (str "Error in new branch pp")); +(* let branch = *) +(* List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *) +(* in *) +(* (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) *) +(* with _ -> trace (str "Error in new branch pp")); *) incr i; let rhs = { eqn.rhs with it = branch } in (branch_decl :: branches, @@ -1770,40 +1766,52 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = * A type constraint but no annotation case: it is assumed non dependent. *) -let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = +let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon = (* We extract the signature of the arity *) let arsign = extract_arity_signature env tomatchs sign in - let env0 = env in - let env = List.fold_right push_rels arsign env in +(* let env = List.fold_right push_rels arsign env in *) let allnames = List.rev (List.map (List.map pi1) arsign) in let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in let pred = out_some (valcon_of_tycon tycon) in let predcclj, pred, neqs = let _, _, eqs = - List.fold_right2 - (fun ctx (tm,_) (lift0, lift1, eqs) -> + List.fold_left2 + (fun (neqs, slift, eqs) ctx (tm,ty) -> let len = List.length ctx in - let name, _, typ = List.hd ctx in + let _name, _, _typ' = List.hd ctx in (* FixMe: Ignoring dependent inductives *) let eq = mkApp (Lazy.force eq_ind, - [| lift lift0 typ; - mkRel (lift0 - ((len - 1) + lift1)); - lift lift0 tm|]) + [| lift (neqs + nar) (type_of_tomatch ty); + mkRel (neqs + slift); + lift (neqs + nar) tm|]) in - (succ lift0, lift1 + len, (Anonymous, None, eq) :: eqs)) - arsign tomatchs (nar, 0, []) + (succ neqs, slift - len, (Anonymous, None, eq) :: eqs)) + (0, nar, []) (List.rev arsign) tomatchs in let len = List.length eqs in it_mkProd_wo_LetIn (lift (nar + len) pred) eqs, pred, len in let predccl = nf_isevar !isevars predcclj in - trace (str "Predicate: " ++ my_print_constr env predccl); build_initial_predicate true allnames predccl, pred - + +let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp = + (* We extract the signature of the arity *) + let arsign = extract_arity_signature env tomatchs sign in + let env = List.fold_right push_rels arsign env in + let allnames = List.rev (List.map (List.map pi1) arsign) in + let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in +(* let _ = *) +(* option_map (fun tycon -> *) +(* isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val *) +(* (lift_tycon_type (List.length arsign) tycon)) *) +(* tycon *) +(* in *) + let predccl = (j_nf_isevar !isevars predcclj).uj_val in + Some (build_initial_predicate true allnames predccl) + (**************************************************************************) (* Main entry of the matching compilation *) let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)= - let env0 = env in let tycon0 = tycon in (* We build the matrix of patterns and right-hand-side *) let matx = matx_of_eqns env tomatchl eqns in @@ -1811,46 +1819,69 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in - - let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in - let matx = List.rev matx in - trace (str "Old env: " ++ my_print_env env); - let env = push_rels lets env in - let len = List.length lets in - let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in - trace (str "New env: " ++ my_print_env env); - let tycon = lift_tycon len tycon in - let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in - let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in - - (* We build the elimination predicate if any and check its consistency *) - (* with the type of arguments to match *) - let tmsign = List.map snd tomatchl in - let pred, opred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon in - - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in - - let pb = - { env = env; - isevars = isevars; - pred = Some pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; - typing_function = typing_fun } in - - let _, j = compile pb in - (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; - let ty = out_some (valcon_of_tycon tycon0) in - let j = - { uj_val = it_mkLambda_or_LetIn (applistc j.uj_val args) lets; - uj_type = ty; } - in - trace (str"final judgement:" ++ Prettyp.print_judgment env0 j ++ spc ()); - inh_conv_coerce_to_tycon loc env isevars j tycon0 + match predopt with + None -> + let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in + let matx = List.rev matx in + let env = push_rels lets env in + let len = List.length lets in + let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in + let tycon = lift_tycon len tycon in + let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in + let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in + + (* We build the elimination predicate if any and check its consistency *) + (* with the type of arguments to match *) + let tmsign = List.map snd tomatchl in + let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs tmsign tycon in + + (* We push the initial terms to match and push their alias to rhs' envs *) + (* names of aliases will be recovered from patterns (hence Anonymous here) *) + let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in + + let pb = + { env = env; + isevars = isevars; + pred = Some pred; + tomatch = initial_pushed; + history = start_history (List.length initial_pushed); + mat = matx; + caseloc = loc; + typing_function = typing_fun } in + + let _, j = compile pb in + (* We check for unused patterns *) + List.iter (check_unused_pattern env) matx; + let ty = out_some (valcon_of_tycon tycon0) in + let j = + { uj_val = it_mkLambda_or_LetIn (applistc j.uj_val args) lets; + uj_type = ty; } + in + inh_conv_coerce_to_tycon loc env isevars j tycon0 + + | Some rtntyp -> + (* We build the elimination predicate if any and check its consistency *) + (* with the type of arguments to match *) + let tmsign = List.map snd tomatchl in + let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon rtntyp in + + (* We push the initial terms to match and push their alias to rhs' envs *) + (* names of aliases will be recovered from patterns (hence Anonymous here) *) + let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in + + let pb = + { env = env; + isevars = isevars; + pred = pred; + tomatch = initial_pushed; + history = start_history (List.length initial_pushed); + mat = matx; + caseloc = loc; + typing_function = typing_fun } in + + let _, j = compile pb in + (* We check for unused patterns *) + List.iter (check_unused_pattern env) matx; + inh_conv_coerce_to_tycon loc env isevars j tycon end diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index c78145357..16363ac67 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -53,8 +53,6 @@ module Coercion = struct | _ -> None and disc_exist env x = - (try trace (str "Disc_exist: " ++ my_print_constr env x) - with _ -> ()); match kind_of_term x with | App (c, l) -> (match kind_of_term c with @@ -67,8 +65,6 @@ module Coercion = struct let disc_proj_exist env x = - (try trace (str "disc_proj_exist: " ++ my_print_constr env x); - with _ -> ()); match kind_of_term x with | App (c, l) -> (if Term.eq_constr c (Lazy.force sig_).proj1 @@ -108,27 +104,27 @@ 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 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 _ -> ()); +(* (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 debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ - str " to "++ my_print_constr env y) - with _ -> ()); +(* (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 debug 1 (str "Unified " ++ (my_print_constr env x) ++ - str " and "++ my_print_constr env y); - with _ -> ()); +(* (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 debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ - str " to "++ my_print_constr env y); - with _ -> ()); +(* (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 | Sort s, Sort s' -> (match s, s' with @@ -163,7 +159,6 @@ module Coercion = struct if i = Term.destInd existS.typ then begin - trace (str "In coerce sigma types"); let (a, pb), (a', pb') = pair_of_array l, pair_of_array l' in @@ -186,7 +181,6 @@ module Coercion = struct let c2 = coerce_unify env' b b' in match c1, c2 with None, None -> - trace (str "No coercion needed"); None | _, _ -> Some @@ -201,7 +195,6 @@ module Coercion = struct end else begin - debug 1 (str "In coerce prod types"); let (a, b), (a', b') = pair_of_array l, pair_of_array l' in @@ -236,7 +229,25 @@ module Coercion = struct (* mkApp (Lazy.force eqrec, *) (* [| argtype; argx; pred; x; argy; evar |])) *) (* else *)subco () - | _ -> subco ()) + | x, y when x = y -> + let lam_type = Typing.type_of env (evars_of !isevars) c in + let rec coerce typ i co = + if i < Array.length l then + let hdx = l.(i) and hdy = l'.(i) in + let (n, eqT, restT) = destProd typ in + let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in + let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in + let evar = make_existential dummy_loc env isevars eq in + let eq_app x = mkApp (Lazy.force eq_rect, + [| eqT; hdx; pred; x; hdy; evar|]) + in + coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) + else co + in + if Array.length l = Array.length l' then + Some (coerce lam_type 0 (fun x -> x)) + else subco () + | _ -> subco ()) | _, _ -> subco () and subset_coerce env isevars x y = @@ -387,13 +398,13 @@ module Coercion = struct with Reduction.NotConvertible -> raise NoCoercion let rec inh_conv_coerce_to_fail loc env isevars v t c1 = - (try - 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 () ++ - Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ - Termops.print_env env); - with _ -> ()); +(* (try *) +(* 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 () ++ *) +(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *) +(* Termops.print_env env); *) +(* with _ -> ()); *) try (the_conv_x_leq env t c1 isevars, v, t) with Reduction.NotConvertible -> (try @@ -452,14 +463,14 @@ 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 - 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 () ++ - Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ - Termops.print_env env); - with _ -> ()); + let inh_conv_coerce_to loc env isevars cj ((n, t) as _tycon) = +(* (try *) +(* 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 () ++ *) +(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *) +(* Termops.print_env env); *) +(* with _ -> ()); *) match n with None -> let (evd', val', type') = @@ -477,40 +488,38 @@ module Coercion = struct | Some (init, cur) -> (isevars, cj) - let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) = - (try - 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 () ++ - Termops.print_env env); - with _ -> ()); + let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = +(* (try *) +(* trace (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 () ++ *) +(* Termops.print_env env); *) +(* with _ -> ()); *) let nabsinit, nabs = match abs with None -> 0, 0 | Some (init, cur) -> init, cur in - let (rels, rng) = (* a little more effort to get products is needed *) - try decompose_prod_n nabs t - with _ -> - trace (str "decompose_prod_n failed"); - raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") - in - (* The final range free variables must have been replaced by evars, we accept only that evars - in rng are applied to free vars. *) - if noccur_with_meta 0 (succ nabsinit) rng then ( - trace (str "No occur between 0 and " ++ int (succ nabsinit)); - let env', t, t' = - let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in - env', rng, lift nabs t' - in - try - pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t' - with NoCoercion -> - coerce_itf loc env' isevars None t t') - with NoSubtacCoercion -> - let sigma = evars_of isevars in - error_cannot_coerce env' sigma (t, t')) - else isevars + try let rels, rng = decompose_prod_n nabs t in + (* The final range free variables must have been replaced by evars, we accept only that evars + in rng are applied to free vars. *) + if noccur_with_meta 0 (succ nabsinit) rng then ( +(* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *) + let env', t, t' = + let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in + env', rng, lift nabs t' + in + try + pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t' + with NoCoercion -> + coerce_itf loc env' isevars None t t') + with NoSubtacCoercion -> + let sigma = evars_of isevars in + error_cannot_coerce env' sigma (t, t')) + else isevars + with _ -> isevars + (* trace (str "decompose_prod_n failed"); *) + (* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *) end diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index ef6d0bed1..68ab8c46e 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -57,7 +57,7 @@ let interp_gen kind isevars env c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in let c' = Subtac_utils.rewrite_cases env c' in - (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); +(* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' @@ -176,19 +176,19 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let sigma = Evd.empty in let isevars = ref (Evd.create_evar_defs sigma) in 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 "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) - with _ -> () - 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 _ = *) +(* 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) *) +(* with _ -> () *) + (* in *) let env', binders_rel = interp_context isevars env bl in let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in let before_length, after_length = List.length before, List.length after in @@ -228,9 +228,8 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = 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 _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 ; @@ -239,32 +238,32 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkRel 1 |]) in - (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ()); + (* (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 _ -> ()); +(* (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ()); *) 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 _ -> ()); +(* (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 _ -> ()); +(* (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 _ -> ()); +(* (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 _ = *) +(* 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 @@ -288,28 +287,23 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = 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 _ = 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 _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) 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_definition recname evars_def fullctyp evars; - trace (str "Added to obligations list") - + (* (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 _ -> ()); *) + Subtac_obligations.add_definition recname evars_def fullctyp evars + let build_mutrec l boxed = let sigma = Evd.empty and env = Global.env () in let nc = named_context env in @@ -322,9 +316,9 @@ let build_mutrec l boxed = and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef in (* Build the recursive context and notations for the recursive types *) - let (rec_sign,rec_impls,arityl) = + let (rec_sign,rec_env,rec_impls,arityl) = List.fold_left - (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) -> + (fun (sign,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 env arityc in @@ -333,8 +327,8 @@ let build_mutrec l boxed = then Impargs.compute_implicits env 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)) - (env,[],[]) lnameargsardef in + ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)) + ([],env,[],[]) lnameargsardef in let arityl = List.rev arityl in let notations = List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) @@ -353,11 +347,11 @@ let build_mutrec l boxed = match info with None -> let def = abstract_constr_expr def bl in - isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls) + isevars, info, interp_casted_constr isevars rec_env ~impls:([],rec_impls) def arity | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) -> - let rec_sign = push_rel_context fun_bl rec_sign in - let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls) + let rec_env = push_rel_context fun_bl rec_env in + let cstr = interp_casted_constr isevars rec_env ~impls:([],rec_impls) def intern_arity in isevars, info, it_mkLambda_or_LetIn cstr fun_bl) lnameargsardef arityl @@ -365,34 +359,32 @@ let build_mutrec l boxed = States.unfreeze fs; raise e in States.unfreeze fs; def in - let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec env lrecnames recdef arityl nv in let recdefs = Array.length defrec in - trace (int recdefs ++ str " recursive definitions"); (* Solve remaining evars *) let rec collect_evars i acc = if i < recdefs then let (isevars, info, def) = defrec.(i) in - let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in + (* let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *) let def = evar_nf isevars def in let isevars = Evd.undefined_evars !isevars in - let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in + (* let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *) let evm = Evd.evars_of isevars in let _, _, typ = arrec.(i) in let id = namerec.(i) in - (* Generalize by the recursive prototypes *) + (* Generalize by the recursive prototypes *) let def = - Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign) + Termops.it_mkNamedLambda_or_LetIn def rec_sign and typ = - Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) + Termops.it_mkNamedProd_or_LetIn typ rec_sign in let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in - collect_evars (succ i) ((id, nvrec.(i), def, typ, evars) :: acc) + collect_evars (succ i) ((id, def, typ, evars) :: acc) else acc in let defs = collect_evars 0 [] in - Subtac_obligations.add_mutual_definitions (List.rev defs) + Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec let out_n = function Some n -> n diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index fd0d289e3..5119145f4 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -28,7 +28,8 @@ type program_info = { prg_body: constr; prg_type: constr; prg_obligations: obligations; - prg_deps : (identifier * int) list; + prg_deps : identifier list; + prg_nvrec : int array; } let assumption_message id = @@ -126,7 +127,6 @@ open Ppconstr let declare_mutual_definition l = let len = List.length l in - let l, nvlist = List.split l in let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in let arrec = Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) @@ -137,7 +137,7 @@ let declare_mutual_definition l = let subs = (subst_body x) in snd (decompose_lam_n len subs)) l) in - let nvrec = Array.of_list nvlist in + let nvrec = (List.hd l).prg_nvrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++ @@ -183,7 +183,7 @@ let try_tactics obls = let red = Reductionops.nf_betaiota -let init_prog_info n b t deps obls = +let init_prog_info n b t deps nvrec obls = let obls' = Array.mapi (fun i (n, t, d) -> @@ -194,7 +194,7 @@ let init_prog_info n b t deps obls = obls in { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls'); - prg_deps = deps } + prg_deps = deps; prg_nvrec = nvrec; } let pperror cmd = Util.errorlabstrm "Subtac" cmd let error s = pperror (str s) @@ -227,37 +227,11 @@ let update_obls prg obls rem = declare_definition prg'; from_prg := ProgMap.remove prg.prg_name !from_prg | l -> - let progs = List.map (fun (x,y) -> ProgMap.find x !from_prg, y) prg'.prg_deps in - if List.for_all (fun x -> obligations_solved (fst x)) progs then + let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in + if List.for_all (fun x -> obligations_solved x) progs then (declare_mutual_definition progs; from_prg := List.fold_left - (fun acc x -> ProgMap.remove (fst x).prg_name acc) !from_prg progs)) - -let add_definition n b t obls = - Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); - let prg = init_prog_info n b t [] obls in - let obls,_ = prg.prg_obligations in - if Array.length obls = 0 then ( - Options.if_verbose ppnl (str "."); - declare_definition prg; - from_prg := ProgMap.remove prg.prg_name !from_prg) - else ( - let len = Array.length obls in - let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in - from_prg := ProgMap.add n prg !from_prg) - -let add_mutual_definitions l = - let deps = List.map (fun (n, nclen, b, t, obls) -> n, nclen) l in - let upd = List.fold_left - (fun acc (n, nclen, b, t, obls) -> - let prg = init_prog_info n b t deps obls in - ProgMap.add n prg acc) - !from_prg l - in - from_prg := upd; - let prg = (ProgMap.find (fst (List.hd deps)) !from_prg) in - let o, r = prg.prg_obligations in - update_obls prg o r + (fun acc x -> ProgMap.remove x.prg_name acc) !from_prg progs)) let is_defined obls x = obls.(x).obl_body <> None @@ -272,20 +246,24 @@ let solve_obligation prg num = let user_num = succ num in let obls, rem = prg.prg_obligations in let obl = obls.(num) in - match deps_remaining obls obl.obl_deps with - [] -> - let obl = subst_deps_obl obls obl in - Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type - (fun strength gr -> - debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished"); - let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - update_obls prg obls (pred rem)); - Pfedit.by !default_tactic; - trace (str "Started obligation " ++ int user_num ++ str " proof") - | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) + if obl.obl_body <> None then + pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.") + else + match deps_remaining obls obl.obl_deps with + [] -> + let obl = subst_deps_obl obls obl in + Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type + (fun strength gr -> + debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished"); + let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + update_obls prg obls (pred rem)); + Pfedit.by !default_tactic; + trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ + Subtac_utils.my_print_constr (Global.env ()) obl.obl_type) + | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " + ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) let subtac_obligation (user_num, name, typ) = let num = pred user_num in @@ -311,6 +289,20 @@ let obligations_of_evars evars = }) evars) in arr, Array.length arr +let solve_obligation_by_tac prg obls i tac = + let obl = obls.(i) in + match obl.obl_body with + Some _ -> false + | None -> + (try + if deps_remaining obls obl.obl_deps = [] then + let obl = subst_deps_obl obls obl in + let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in + obls.(i) <- { obl with obl_body = Some t }; + true + else false + with _ -> false) + let solve_obligations n tac = let prg = get_prog n in let obls, rem = prg.prg_obligations in @@ -318,22 +310,37 @@ let solve_obligations n tac = let obls' = Array.copy obls in let _ = Array.iteri (fun i x -> - match x.obl_body with - Some _ -> () - | None -> - (try - if deps_remaining obls' x.obl_deps = [] then - let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in - decr rem; - obls'.(i) <- { x with obl_body = Some t } - else () - with UserError (s, cmds) -> - debug 1 cmds - | _ -> ())) + if solve_obligation_by_tac prg obls' i tac then + decr rem) obls' in update_obls prg obls' !rem +let add_definition n b t obls = + Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); + let prg = init_prog_info n b t [] (Array.make 0 0) obls in + let obls,_ = prg.prg_obligations in + if Array.length obls = 0 then ( + Options.if_verbose ppnl (str "."); + declare_definition prg; + from_prg := ProgMap.remove prg.prg_name !from_prg) + else ( + let len = Array.length obls in + let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in + from_prg := ProgMap.add n prg !from_prg; + solve_obligations (Some n) !default_tactic) + +let add_mutual_definitions l nvrec = + let deps = List.map (fun (n, b, t, obls) -> n) l in + let upd = List.fold_left + (fun acc (n, b, t, obls) -> + let prg = init_prog_info n b t deps nvrec obls in + ProgMap.add n prg acc) + !from_prg l + in + from_prg := upd; + solve_obligations (Some (List.hd deps)) !default_tactic + let admit_obligations n = let prg = get_prog n in let obls, rem = prg.prg_obligations in @@ -356,15 +363,18 @@ let array_find f arr = raise Not_found with Found i -> i -let next_obligation n = +let rec next_obligation n = let prg = get_prog n in let obls, rem = prg.prg_obligations in let i = array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls in - solve_obligation prg i - + if solve_obligation_by_tac prg obls i !default_tactic then ( + update_obls prg obls (pred rem); + next_obligation n + ) else solve_obligation prg i + open Pp let show_obligations n = let prg = get_prog n in diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 7953fb4b0..3981d4c6c 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -8,7 +8,7 @@ val add_definition : Names.identifier -> Term.constr -> Term.types -> obligation_info -> unit val add_mutual_definitions : - (Names.identifier * int * Term.constr * Term.types * obligation_info) list -> unit + (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index d27ef4c16..7ae8f45d7 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -113,29 +113,23 @@ let env_with_binders env isevars l = in aux (env, []) l let subtac_process env isevars id l c tycon = - let evars () = evars_of !isevars in - let _ = trace (str "Creating env with binders") in let env_binders, binders_rel = env_with_binders env isevars l in - let _ = try (trace (str "New env created:" ++ my_print_context env_binders)) with _ -> () in let tycon = match tycon with None -> empty_tycon | Some t -> let t = coqintern !isevars env_binders t in - let _ = try trace (str "Internalized specification: " ++ my_print_rawconstr env_binders t) with _ -> () in let coqt, ttyp = interp env_binders isevars t empty_tycon in - let _ = try trace (str "Interpreted type: " ++ my_print_constr env_binders coqt) with _ -> () in mk_tycon coqt in let c = coqintern !isevars env_binders c in let c = Subtac_utils.rewrite_cases env c in - let _ = try trace (str "Internalized term: " ++ my_print_rawconstr env c) with _ -> () in let coqc, ctyp = interp env_binders isevars c tycon in - let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ - str "Coq type: " ++ my_print_constr env_binders ctyp) - with _ -> () - in - let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in +(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env_binders coqc ++ spc () ++ *) +(* str "Coq type: " ++ my_print_constr env_binders ctyp) *) +(* with _ -> () *) +(* in *) +(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars ())) with _ -> () in *) let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel and fullctyp = it_mkProd_or_LetIn ctyp binders_rel @@ -143,13 +137,13 @@ let subtac_process env isevars id l c tycon = let fullcoqc = Evarutil.nf_evar (evars_of !isevars) fullcoqc in let fullctyp = Evarutil.nf_evar (evars_of !isevars) fullctyp 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 _ = 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 _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) evm, fullcoqc, fullctyp open Subtac_obligations @@ -159,5 +153,4 @@ let subtac_proof env isevars id l c tycon = let nc_len = named_context_length nc in let evm, coqc, coqt = subtac_process env isevars id l c tycon in let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in - trace (str "Adding to obligations list"); add_definition id def coqt evars diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index d9c193bed..9e44c9096 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -162,10 +162,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* in environment [env], with existential variables [(evars_of isevars)] and *) (* the type constraint tycon *) let rec pretype (tycon : type_constraint) env isevars lvar c = - let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ - str " with tycon " ++ Evarutil.pr_tycon env tycon) - with _ -> () - in +(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *) +(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) +(* with _ -> () *) +(* in *) match c with | RRef (loc,ref) -> inh_conv_coerce_to_tycon loc env isevars diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index adf8dc620..973d2a150 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -47,6 +47,7 @@ let sig_ = lazy (build_sig ()) let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq") let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec") +let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect") let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal") let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq") let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal") @@ -145,8 +146,9 @@ let print_args env args = let make_existential loc env isevars c = let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in let (key, args) = destEvar evar in - (try debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++ - print_args env args) with _ -> ()); + (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ + print_args env args ++ str " for type: "++ + my_print_constr env c) with _ -> ()); evar let make_existential_expr loc env c = diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 95138c2fc..bb9b926b4 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -34,6 +34,7 @@ val sig_ : coq_sigma_data lazy_t val eq_ind : constr lazy_t val eq_rec : constr lazy_t +val eq_rect : constr lazy_t val eq_refl : constr lazy_t val eq_ind_ref : global_reference lazy_t val refl_equal_ref : global_reference lazy_t diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v index 8fedeed51..809503aa2 100644 --- a/contrib/subtac/test/euclid.v +++ b/contrib/subtac/test/euclid.v @@ -8,33 +8,31 @@ Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : (S q' & r) else (O & a). -Require Import Coq.subtac.Utils. -Require Import Coq.subtac.FixSub. Require Import Omega. Obligations. Obligation 1. intros. - destruct_exists ; simpl in * ; auto with arith. + simpl in * ; auto with arith. omega. -Qed. +Defined. Obligation 2 of euclid. intros. - destruct_exists ; simpl in * ; auto with arith. assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega. -Qed. +Defined. Obligation 4 of euclid. exact Wf_nat.lt_wf. -Qed. +Defined. Obligation 3 of euclid. intros. - destruct_exists ; simpl in *. omega. Qed. +Eval cbv delta [euclid_obligation_1 euclid_obligation_2] in (euclid 0). + Extraction Inline Fix_sub Fix_F_sub. Extract Inductive sigT => "pair" [ "" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. |