diff options
Diffstat (limited to 'contrib/subtac')
-rw-r--r-- | contrib/subtac/Utils.v | 3 | ||||
-rw-r--r-- | contrib/subtac/eterm.ml | 148 | ||||
-rw-r--r-- | contrib/subtac/eterm.mli | 8 | ||||
-rw-r--r-- | contrib/subtac/g_subtac.ml4 | 30 | ||||
-rw-r--r-- | contrib/subtac/subtac.ml | 54 | ||||
-rw-r--r-- | contrib/subtac/subtac_coercion.ml | 7 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 107 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.mli | 1 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 249 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.mli | 10 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 12 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping.mli | 3 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 45 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 72 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.mli | 10 | ||||
-rw-r--r-- | contrib/subtac/test/ListDep.v | 86 |
16 files changed, 612 insertions, 233 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index b1694d7c..219cd75b 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -4,7 +4,7 @@ Notation "'fun' { x : A | P } => Q" := (fun x:{x:A|P} => Q) (at level 200, x ident, right associativity). -Notation "( x & y )" := (@existS _ _ x y) : core_scope. +Notation "( x & ? )" := (@exist _ _ x _) : core_scope. Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. intros. @@ -44,3 +44,4 @@ end. Ltac destruct_exists := repeat (destruct_one_pair) . +Extraction Inline proj1_sig. diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 859f9013..790e61a0 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -32,47 +32,48 @@ let list_assoc_index x l = | [] -> raise Not_found in aux 0 l + (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) -let subst_evars evs n t = +let subst_evar_constr evs n t = + let seen = ref Intset.empty in let evar_info id = let rec aux i = function - (k, h, v) :: tl -> - trace (str "Searching for " ++ int id ++ str " found: " ++ int k); - if k = id then (i, h, v) else aux (succ i) tl + (k, x) :: tl -> + if k = id then x else aux (succ i) tl | [] -> raise Not_found - in - let (idx, hyps, v) = aux 0 evs in - n + idx + 1, hyps + in aux 0 evs in let rec substrec depth c = match kind_of_term c with | Evar (k, args) -> - (let index, hyps = - try evar_info k - with Not_found -> - anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") - in - (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ - int (List.length hyps) ++ str " hypotheses"); with _ -> () ); - let ex = mkRel (index + depth) in - (* Evar arguments are created in inverse order, - and we must not apply to defined ones (i.e. LetIn's) - *) - let args = - let rec aux hyps args acc = + let (id, idstr), hyps, _, _ = + try evar_info k + with Not_found -> + anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") + in + seen := Intset.add id !seen; + (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ + int (List.length hyps) ++ str " hypotheses"); with _ -> () ); + (* Evar arguments are created in inverse order, + and we must not apply to defined ones (i.e. LetIn's) + *) + let args = + let rec aux hyps args acc = match hyps, args with ((_, None, _) :: tlh), (c :: tla) -> aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc) | ((_, Some _, _) :: tlh), (_ :: tla) -> aux tlh tla acc | [], [] -> acc - | _, _ -> failwith "subst_evars: invalid argument" + | _, _ -> acc (*failwith "subst_evars: invalid argument"*) in aux hyps (Array.to_list args) [] in - mkApp (ex, Array.of_list args)) + mkApp (mkVar idstr, Array.of_list args) | _ -> map_constr_with_binders succ substrec depth c in - substrec 0 t + let t' = substrec 0 t in + t', !seen + (** Substitute variable references in t using De Bruijn indices, where n binders were passed through. *) @@ -89,73 +90,80 @@ let subst_vars acc n t = (** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) to a product : forall H1 : t1, ..., forall Hn : tn, concl. - Changes evars and hypothesis references to De Bruijn indices. + Changes evars and hypothesis references to variable references. *) let etype_of_evar evs ev hyps = let rec aux acc n = function (id, copt, t) :: tl -> - let t' = subst_evars evs n t in + let t', s = subst_evar_constr evs n t in let t'' = subst_vars acc 0 t' in - mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl) + let copt', s = + match copt with + Some c -> + let c', s' = subst_evar_constr evs n c in + Some c', Intset.union s s' + | None -> None, s + in + let copt' = option_map (subst_vars acc 0) copt' in + let rest, s' = aux (id :: acc) (succ n) tl in + mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s | [] -> - let t' = subst_evars evs n ev.evar_concl in - subst_vars acc 0 t' + let t', s = subst_evar_constr evs n ev.evar_concl in + subst_vars acc 0 t', s in aux [] 0 (rev hyps) open Tacticals -let eterm_term evm t tycon = +let rec take n l = + if n = 0 then [] else List.hd l :: take (pred n) (List.tl l) + +let trunc_named_context n ctx = + let len = List.length ctx in + take (len - n) ctx + +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"); + trace (str "Eterm, transformed to list"); + let evn = + let i = ref (-1) in + List.rev_map (fun (id, ev) -> incr i; + (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl + in let evts = (* Remove existential variables in types and build the corresponding products *) fold_right - (fun (id, ev) l -> + (fun (id, (n, nstr), ev) l -> trace (str "Eterm: " ++ str "treating evar: " ++ int id); let hyps = Environ.named_context_of_val ev.evar_hyps in - let y' = (id, hyps, etype_of_evar l ev 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); + let y' = (id, ((n, nstr), hyps, evtyp, deps)) in y' :: l) - evl [] + evn [] in - let t' = (* Substitute evar refs in the term by De Bruijn indices *) - subst_evars evts 0 t - in - let evar_names = - List.map (fun (id, _, c) -> (id_of_string ("Evar" ^ string_of_int id)), c) evts - in - let evar_bl = - List.map (fun (id, c) -> Name id, None, c) evar_names - in - let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in - (* Generalize over the existential variables *) - let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl - and tycon = option_map - (fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon - in - let _declare_evar (id, c) = - let id = id_of_string ("Evar" ^ string_of_int id) in - ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c, - Decl_kinds.IsAssumption Decl_kinds.Definitional)) + let t', _ = (* Substitute evar refs in the term by variables *) + subst_evar_constr evts 0 t in - let _declare_assert acc (id, c) = - let id = id_of_string ("Evar" ^ string_of_int id) in - tclTHEN acc (Tactics.assert_tac false (Name id) c) + 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); + Termops.print_constr_env (Global.env ()) t); trace (str "Term constructed in eterm" ++ spc () ++ - Termops.print_constr_env (Global.env ()) t''); - ignore(option_map - (fun typ -> - trace (str "Type :" ++ spc () ++ - Termops.print_constr_env (Global.env ()) typ)) - tycon); + 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 _ -> ()); - t'', tycon, evar_names + Array.of_list (List.rev evars), t' let mkMetas n = let rec aux i acc = @@ -163,12 +171,12 @@ let mkMetas n = else acc in aux n [] -let eterm evm t (tycon : types option) = - let t, tycon, evs = eterm_term evm t tycon in - match tycon with - Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] - | None -> Tactics.apply_term t (mkMetas (List.length evs)) +(* let eterm evm t (tycon : types option) = *) +(* let t, tycon, evs = eterm_term evm t tycon in *) +(* match tycon with *) +(* Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] *) +(* | None -> Tactics.apply_term t (mkMetas (List.length evs)) *) -open Tacmach +(* open Tacmach *) -let etermtac (evm, t) = eterm evm t None +let etermtac (evm, t) = assert(false) (*eterm evm t None *) diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index fbe2ac1d..3a571ee1 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -6,15 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: eterm.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) +(*i $Id: eterm.mli 9326 2006-10-31 12:57:26Z msozeau $ i*) open Tacmach open Term open Evd open Names +open Util val mkMetas : int -> constr list -val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list +(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *) + +val eterm_obligations : identifier -> int -> evar_map -> constr -> types option -> + (identifier * types * Intset.t) array * constr (* Obl. name, type as product and dependencies as indexes into the array *) val etermtac : open_constr -> tactic diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index b56ecc3d..243cb191 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -10,7 +10,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) -(* $Id: g_subtac.ml4 8917 2006-06-07 16:59:05Z herbelin $ *) +(* $Id: g_subtac.ml4 9326 2006-10-31 12:57:26Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) @@ -30,6 +30,7 @@ open Topconstr module Gram = Pcoq.Gram module Vernac = Pcoq.Vernac_ +module Tactic = Pcoq.Tactic module SubtacGram = struct @@ -40,15 +41,31 @@ end open SubtacGram open Util +open Pcoq + +let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram - GLOBAL: subtac_gallina_loc; + GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder; subtac_gallina_loc: [ [ g = Vernac.gallina -> loc, g ] ] ; + + Constr.binder_let: + [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in + LocalRawAssum ([id], typ) + ] ]; + + Constr.binder: + [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in + ([id], typ) ] ]; + END + type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype), @@ -57,6 +74,11 @@ let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_arg Genarg.create_arg "subtac_gallina_loc" VERNAC COMMAND EXTEND Subtac -[ "Program" subtac_gallina_loc(g) ] -> - [ Subtac.subtac g ] +[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ] +| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name) ] +| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None) ] +| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations (Some name) (Tacinterp.interp t) ] +| [ "Solve" "Obligations" "using" tactic(t) ] -> [ Subtac_obligations.solve_obligations None (Tacinterp.interp t) ] +| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] +| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] END diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index ffb16a19..26e8f715 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 8964 2006-06-20 13:52:21Z msozeau $ *) +(* $Id: subtac.ml 9284 2006-10-26 12:06:57Z msozeau $ *) open Global open Pp @@ -156,19 +156,19 @@ let subtac (loc, command) = match command with VernacDefinition (defkind, (locid, id), expr, hook) -> (match expr with - ProveBody (bl, c) -> - let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c None in - trace (str "Starting proof"); - Command.start_proof id goal_kind c hook; - trace (str "Started proof"); + ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None +(* let evm, c, ctyp = in *) +(* trace (str "Starting proof"); *) +(* Command.start_proof id goal_kind c hook; *) +(* trace (str "Started proof"); *) | DefineBody (bl, _, c, tycon) -> - let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c tycon in - let tac = Eterm.etermtac (evm, c) in - trace (str "Starting proof"); - Command.start_proof id goal_kind ctyp hook; - trace (str "Started proof"); - Pfedit.by tac) + Subtac_pretyping.subtac_proof env isevars id bl c tycon + (* let tac = Eterm.etermtac (evm, c) in *) + (* trace (str "Starting proof"); *) + (* Command.start_proof id goal_kind ctyp hook; *) + (* trace (str "Started proof"); *) + (* Pfedit.by tac) *)) | VernacFixpoint (l, b) -> let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l b) @@ -223,24 +223,30 @@ let subtac (loc, command) = ++ x ++ spc () ++ str "and" ++ spc () ++ y in msg_warning cmds - | Type_errors.TypeError (env, e) -> - debug 2 (Himsg.explain_type_error env e) + | Type_errors.TypeError (env, exn) as e -> + debug 2 (Himsg.explain_type_error env exn); + raise e - | Pretype_errors.PretypeError (env, e) -> - debug 2 (Himsg.explain_pretype_error env e) + | Pretype_errors.PretypeError (env, exn) as e -> + debug 2 (Himsg.explain_pretype_error env exn); + raise e - | Stdpp.Exc_located (loc, e) -> + | (Stdpp.Exc_located (loc, e')) as e -> debug 2 (str "Parsing exception: "); - (match e with - | Type_errors.TypeError (env, e) -> - debug 2 (Himsg.explain_type_error env e) + (match e' with + | Type_errors.TypeError (env, exn) -> + debug 2 (Himsg.explain_type_error env exn); + raise e - | Pretype_errors.PretypeError (env, e) -> - debug 2 (Himsg.explain_pretype_error env e) + | Pretype_errors.PretypeError (env, exn) -> + debug 2 (Himsg.explain_pretype_error env exn); + raise e - | e -> msg_warning (str "Unexplained exception: " ++ Cerrors.explain_exn e)) + | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); + raise e) | e -> - msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e) + msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); + raise e diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 78c3c70b..da5c497c 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 8964 2006-06-20 13:52:21Z msozeau $ *) +(* $Id: subtac_coercion.ml 9284 2006-10-26 12:06:57Z msozeau $ *) open Util open Names @@ -91,7 +91,9 @@ module Coercion = struct let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c let rec mu env isevars t = + let isevars = ref isevars in let rec aux v = + let v = hnf env isevars v in match disc_subset v with Some (u, p) -> let f, ct = aux u in @@ -135,8 +137,9 @@ module Coercion = struct | Type x, Type y when x = y -> None (* false *) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> - let c1 = coerce_unify env a' a in + let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in let env' = push_rel (name', None, a') env in + let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in let c2 = coerce_unify env' b b' in (match c1, c2 with None, None -> failwith "subtac.coerce': Should have detected equivalence earlier" diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index c738d7a6..b433af2c 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -43,6 +43,7 @@ open Notation module SPretyping = Subtac_pretyping.Pretyping open Subtac_utils open Pretyping +open Subtac_obligations (*********************************************************************) (* Functions to parse and interpret constructions *) @@ -149,15 +150,6 @@ let collect_non_rec env = in searchrec [] -let definition_message id = - Options.if_verbose message ((string_of_id id) ^ " is defined") - -let recursive_message v = - match Array.length v with - | 0 -> error "no recursive definition" - | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined") - | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++ - spc () ++ str "are recursively defined") let filter_map f l = let rec aux acc = function @@ -190,9 +182,12 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let env = Global.env() in let pr c = my_print_constr env c in let prr = Printer.pr_rel_context env in + let prn = Printer.pr_named_context env in let pr_rel env = Printer.pr_rel_context env in + let nc = named_context env in + let nc_len = named_context_length nc in let _ = - try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ + try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ Ppconstr.pr_binders bl ++ str " : " ++ Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ Ppconstr.pr_constr_expr body) @@ -204,25 +199,35 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let argid = match argname with Name n -> n | _ -> assert(false) in let _liftafter = lift_binders 1 after_length after in let envwf = push_rel_context before env in - let wf_rel, measure_fn = - let rconstr = interp_constr isevars envwf r in - if measure then - let lt_rel = constr_of_global (Lazy.force lt_ref) in - let name s = Name (id_of_string s) in - mkLambda (name "x", argtyp, - mkLambda (name "y", argtyp, - mkApp (lt_rel, - [| mkApp (rconstr, [| mkRel 2 |]) ; - mkApp (rconstr, [| mkRel 1 |]) |]))), - Some rconstr - else rconstr, None + let wf_rel, wf_rel_fun, measure_fn = + let rconstr_body, rconstr = + let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in + let env = push_rel_context [arg] envwf in + let capp = interp_constr isevars env app in + capp, mkLambda (argname, argtyp, capp) + in + if measure then + let lt_rel = constr_of_global (Lazy.force lt_ref) in + let name s = Name (id_of_string s) in + let wf_rel_fun = + (fun x y -> + mkApp (lt_rel, [| subst1 x rconstr_body; + subst1 y rconstr_body |])) + in + let wf_rel = + mkLambda (name "x", argtyp, + mkLambda (name "y", lift 1 argtyp, + wf_rel_fun (mkRel 2) (mkRel 1))) + in + wf_rel, wf_rel_fun , Some rconstr + else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None in let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in let argid' = id_of_string (string_of_id argid ^ "'") in let wfarg len = (Name argid', None, - mkSubset (Name argid') argtyp - (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|]))) + mkSubset (Name argid') argtyp + (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) in let top_bl = after @ (arg :: before) in let intern_bl = after @ (wfarg 1 :: arg :: before) in @@ -234,7 +239,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let projection = mkApp (proj, [| argtyp ; (mkLambda (Name argid', argtyp, - (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ; + (wf_rel_fun (mkRel 1) (mkRel 3)))) ; mkRel 1 |]) in @@ -299,40 +304,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = in let evm = non_instanciated_map env isevars in let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in - let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in - let evars_typ = out_some evars_typ in - (try trace (str "Building evars sum for : "); - List.iter - (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) - evars; - with _ -> ()); - let (sum_tac, sumg) = Subtac_utils.build_dependent_sum evars in - (try trace (str "Evars sum: " ++ my_print_constr env sumg); - trace (str "Evars type: " ++ my_print_constr env evars_typ); - with _ -> ()); - let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in - Command.start_proof proofid goal_proof_kind sumg - (fun strength gr -> - debug 2 (str "Proof finished"); - let def = constr_of_global gr in - let args = Subtac_utils.destruct_ex def sumg in - let _, newdef = decompose_lam_n (List.length args) evars_def in - let constr = Term.substl (List.rev args) newdef in - debug 2 (str "Applied existentials : " ++ my_print_constr env constr); - let ce = - { const_entry_body = constr; - const_entry_type = Some fullctyp; - const_entry_opaque = false; - const_entry_boxed = boxed} - in - let _constant = Declare.declare_constant - recname (DefinitionEntry ce,IsDefinition Definition) - in - definition_message recname); - trace (str "Started existentials proof"); - Pfedit.by sum_tac; - trace (str "Applied sum tac") - + let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in + (try trace (str "Generated obligations : "); + Array.iter + (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) + evars; + with _ -> ()); + trace (str "Adding to obligations list"); + Subtac_obligations.add_entry recname evars_def fullctyp evars; + trace (str "Added to obligations list") +(* let build_mutrec l boxed = let sigma = Evd.empty and env0 = Global.env() @@ -543,7 +524,7 @@ let build_mutrec l boxed = Environ.NoBody -> trace (str "Constant has no body") | Environ.Opaque -> trace (str "Constant is opaque") ) - +*) let out_n = function Some n -> n | None -> 0 @@ -563,8 +544,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed errorlabstrm "Subtac_command.build_recursive" (str "Well-founded fixpoints not allowed in mutually recursive blocks")) lnameargsardef - in - build_mutrec lnameargsardef boxed; - assert(false) + in assert(false) + (*build_mutrec lnameargsardef boxed*) + diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 90ffb892..846e06cf 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -37,7 +37,6 @@ val interp_constr_judgment : env -> 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_obligations.ml b/contrib/subtac/subtac_obligations.ml new file mode 100644 index 00000000..7b13b402 --- /dev/null +++ b/contrib/subtac/subtac_obligations.ml @@ -0,0 +1,249 @@ +open Printf +open Pp +open Subtac_utils + +open Term +open Names +open Libnames +open Summary +open Libobject +open Entries +open Decl_kinds +open Util +open Evd + +type obligation = + { obl_name : identifier; + obl_type : types; + obl_body : constr option; + obl_deps : Intset.t; + } + +type obligations = (obligation array * int) + +type program_info = { + prg_name: identifier; + prg_body: constr; + prg_type: types; + prg_obligations: obligations; +} + +let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; + evar_concl = o.obl_type ; + evar_body = Evar_empty ; + evar_extra = None } + +module ProgMap = Map.Make(struct type t = identifier let compare = compare end) + +let map_replace k v m = ProgMap.add k v (ProgMap.remove k m) + +let map_cardinal m = + let i = ref 0 in + ProgMap.iter (fun _ _ -> incr i) m; + !i + +exception Found of program_info + +let map_first m = + try + ProgMap.iter (fun _ v -> raise (Found v)) m; + assert(false) + with Found x -> x + +let from_prg : program_info ProgMap.t ref = ref ProgMap.empty + +let _ = + Summary.declare_summary "program-tcc-table" + { Summary.freeze_function = (fun () -> !from_prg); + Summary.unfreeze_function = + (fun v -> from_prg := v); + Summary.init_function = + (fun () -> from_prg := ProgMap.empty); + Summary.survive_module = false; + Summary.survive_section = false } + +let declare_definition prg = +(* let obls_constrs = + Array.fold_right (fun x acc -> (out_some x.obl_evar.evar_body) :: acc) (fst prg.prg_obligations) [] + in*) + let ce = + { const_entry_body = prg.prg_body; + const_entry_type = Some prg.prg_type; + const_entry_opaque = false; + const_entry_boxed = false} + in + let _constant = Declare.declare_constant + prg.prg_name (DefinitionEntry ce,IsDefinition Definition) + in + Subtac_utils.definition_message prg.prg_name + +open Evd + +let terms_of_evar ev = + match ev.evar_body with + Evar_defined b -> + let nc = Environ.named_context_of_val ev.evar_hyps in + let body = Termops.it_mkNamedLambda_or_LetIn b nc in + let typ = Termops.it_mkNamedProd_or_LetIn ev.evar_concl nc in + body, typ + | _ -> assert(false) + +let declare_obligation obl body = + let ce = + { const_entry_body = body; + const_entry_type = Some obl.obl_type; + const_entry_opaque = true; + const_entry_boxed = false} + in + let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) + in + Subtac_utils.definition_message obl.obl_name; + { obl with obl_body = Some (mkConst constant) } + +let try_tactics obls = + Array.map + (fun obl -> + match obl.obl_body with + None -> + (try + let ev = evar_of_obligation obl in + let c = Subtac_utils.solve_by_tac ev Auto.default_full_auto in + declare_obligation obl c + with _ -> obl) + | _ -> obl) + obls + +let add_entry n b t obls = + Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); + let init_obls e = + Array.map + (fun (n, t, d) -> + { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d }) + e + in + if Array.length obls = 0 then ( + Options.if_verbose ppnl (str "."); + declare_definition { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = ([||], 0) } ) + else ( + let len = Array.length obls in + let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in + let obls = init_obls obls in + let rem = Array.fold_left (fun acc obl -> if obl.obl_body = None then succ acc else acc) 0 obls in + let prg = { prg_name = n ; prg_body = b ; prg_type = t ; prg_obligations = (obls, rem) } in + if rem < len then + Options.if_verbose ppnl (int rem ++ str " obligation(s) remaining."); + if rem = 0 then + declare_definition prg + else + from_prg := ProgMap.add n prg !from_prg) + +let error s = Util.error s + +let get_prog name = + let prg_infos = !from_prg in + match name with + Some n -> ProgMap.find n prg_infos + | None -> + (let n = map_cardinal prg_infos in + match n with + 0 -> error "No obligations remaining" + | 1 -> map_first prg_infos + | _ -> error "More than one program with unsolved obligations") + +let update_obls prg obls rem = + let prg' = { prg with prg_obligations = (obls, rem) } in + if rem > 1 then ( + debug 2 (int rem ++ str " obligations remaining"); + from_prg := map_replace prg.prg_name prg' !from_prg) + else ( + declare_definition prg'; + from_prg := ProgMap.remove prg.prg_name !from_prg + ) + +let is_defined obls x = obls.(x).obl_body <> None + +let deps_remaining obls x = + let deps = obls.(x).obl_deps in + Intset.fold + (fun x acc -> + if is_defined obls x then acc + else x :: acc) + deps [] + +let subst_deps obls obl = + let t' = + Intset.fold + (fun x acc -> + let xobl = obls.(x) in + let oblb = out_some xobl.obl_body in + Term.subst1 oblb (Term.subst_var xobl.obl_name acc)) + obl.obl_deps obl.obl_type + in { obl with obl_type = t' } + +let subtac_obligation (user_num, name) = + let num = pred user_num in + let prg = get_prog name in + let obls, rem = prg.prg_obligations in + if num < Array.length obls then + let obl = obls.(num) in + match obl.obl_body with + None -> + (match deps_remaining obls num with + [] -> + let obl = subst_deps 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)); + trace (str "Started obligation " ++ int user_num ++ str " proof") + | l -> msgnl (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " + ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))) + | Some r -> error "Obligation already solved" + else error (sprintf "Unknown obligation number %i" (succ num)) + + +let obligations_of_evars evars = + let arr = + Array.of_list + (List.map + (fun (n, t) -> + { obl_name = n; + obl_type = t; + obl_body = None; + obl_deps = Intset.empty; + }) evars) + in arr, Array.length arr + +let solve_obligations n tac = + let prg = get_prog n in + let obls, rem = prg.prg_obligations in + let rem = ref rem in + let obls' = + Array.map (fun x -> + match x.obl_body with + Some _ -> x + | None -> + try + let t = Subtac_utils.solve_by_tac (evar_of_obligation x) tac in + decr rem; + { x with obl_body = Some t } + with _ -> x) + obls + in + update_obls prg obls' !rem + +open Pp +let show_obligations n = + let prg = get_prog n in + let obls, rem = prg.prg_obligations in + msgnl (int rem ++ str " obligation(s) remaining: "); + Array.iteri (fun i x -> + match x.obl_body with + None -> msgnl (int (succ i) ++ str " : " ++ spc () ++ + my_print_constr (Global.env ()) x.obl_type) + | Some _ -> ()) + obls + diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli new file mode 100644 index 00000000..7d93d57b --- /dev/null +++ b/contrib/subtac/subtac_obligations.mli @@ -0,0 +1,10 @@ +open Util + +val add_entry : Names.identifier -> Term.constr -> Term.types -> + (Names.identifier * Term.types * Intset.t) array -> unit + +val subtac_obligation : int * Names.identifier option -> unit + +val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit + +val show_obligations : Names.identifier option -> unit diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 261e0c5b..a243ba34 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 8889 2006-06-01 20:23:56Z msozeau $ *) +(* $Id: subtac_pretyping.ml 9326 2006-10-31 12:57:26Z msozeau $ *) open Global open Pp @@ -151,3 +151,13 @@ let subtac_process env isevars id l c tycon = let evm = non_instanciated_map env isevars in let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in evm, fullcoqc, fullctyp + +open Subtac_obligations + +let subtac_proof env isevars id l c tycon = + let nc = named_context env in + let nc_len = named_context_length nc in + let evm, coqc, coqt = subtac_process env isevars id l c tycon in + let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in + trace (str "Adding to obligations list"); + add_entry id def coqt evars diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli index 97e56ecb..b62a8766 100644 --- a/contrib/subtac/subtac_pretyping.mli +++ b/contrib/subtac/subtac_pretyping.mli @@ -10,3 +10,6 @@ module Pretyping : Pretyping.S val subtac_process : env -> evar_defs ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> evar_map * constr * types + +val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list -> + constr_expr -> constr_expr option -> unit diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 65952750..46af5886 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 8889 2006-06-01 20:23:56Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 9316 2006-10-29 22:49:11Z herbelin $ *) open Pp open Util @@ -315,12 +315,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in let resj = match kind_of_term resj.uj_val with - | App (f,args) when isInd f -> + | App (f,args) when isInd f or isConst f -> let sigma = evars_of !isevars in - let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in - let s = snd (splay_arity env sigma t) in - on_judgment_type (set_inductive_level env s) resj - (* Rem: no need to send sigma: no head evar, it's an arity *) + let c = mkApp (f,Array.map (whd_evar sigma) args) in + let t = Retyping.get_type_of env sigma c in + make_judge c t | _ -> resj in inh_conv_coerce_to_tycon loc env isevars resj tycon @@ -557,35 +556,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env isevars lvar c).utj_val in nf_evar (evars_of !isevars) c' - (* [check_evars] fails if some unresolved evar remains *) - (* it assumes that the defined existentials have already been substituted - (should be done in unsafe_infer and unsafe_infer_type) *) - - let check_evars env initial_sigma isevars c = - let sigma = evars_of !isevars in - let rec proc_rec c = - match kind_of_term c with - | Evar (ev,args) -> - assert (Evd.mem sigma ev); - if not (Evd.mem initial_sigma ev) then - let (loc,k) = evar_source ev !isevars in - error_unsolvable_implicit loc env sigma k - | _ -> iter_constr proc_rec c - in - proc_rec c(*; - let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in - if pbs <> [] then begin - pperrnl - (str"TYPING OF "++Termops.print_constr_env env c++fnl()++ - prlist_with_sep fnl - (fun (pb,c1,c2) -> - Termops.print_constr c1 ++ - (if pb=Reduction.CUMUL then str " <="++ spc() - else str" =="++spc()) ++ - Termops.print_constr c2) - pbs ++ fnl()) - end*) - (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage retourne aussi le nouveau sigma... @@ -595,6 +565,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let isevars = ref (create_evar_defs sigma) in let j = pretype empty_tycon env isevars ([],[]) c in let j = j_nf_evar (evars_of !isevars) j in + let isevars,_ = consider_remaining_unif_problems env !isevars in check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j @@ -611,8 +582,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let isevars = ref (Evd.create_evar_defs sigma) in let c = pretype_gen isevars env lvar kind c in + let isevars,_ = consider_remaining_unif_problems env !isevars in + let c = nf_evar (evars_of isevars) c in if fail_evar then check_evars env sigma isevars c; - !isevars, c + isevars, c (** Entry points of the high-level type synthesis algorithm *) diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index d4db7c27..7b96758a 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -80,25 +80,34 @@ open Pp let my_print_constr = Termops.print_constr_env let my_print_constr_expr = Ppconstr.pr_constr_expr let my_print_context = Termops.print_rel_context +let my_print_named_context = Termops.print_named_context let my_print_env = Termops.print_env let my_print_rawconstr = Printer.pr_rawconstr_env let my_print_evardefs = Evd.pr_evar_defs let my_print_tycon_type = Evarutil.pr_tycon_type -let debug_level = 2 +let debug_level = 1 + +let debug_on = true let debug n s = - if !Options.debug && n >= debug_level then - msgnl s + if debug_on then + if !Options.debug && n >= debug_level then + msgnl s + else () else () let debug_msg n s = - if !Options.debug && n >= debug_level then s + if debug_on then + if !Options.debug && n >= debug_level then s + else mt () else mt () let trace s = - if !Options.debug && debug_level > 0 then msgnl s + if debug_on then + if !Options.debug && debug_level > 0 then msgnl s + else () else () let wf_relations = Hashtbl.create 10 @@ -167,30 +176,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp open Tactics open Tacticals -let build_dependent_sum l = - let rec aux (tac, typ) = function - (n, t) :: tl -> - let t' = mkLambda (Name n, t, typ) in - trace (spc () ++ str ("treating evar " ^ string_of_id n)); - (try trace (str " assert: " ++ my_print_constr (Global.env ()) t) - with _ -> ()); - let tac' = - tclTHENS (assert_tac true (Name n) t) - ([intros; - (tclTHENSEQ - [constructor_tac (Some 1) 1 - (Rawterm.ImplicitBindings [mkVar n]); - tac]); - ]) - in - let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in - aux (tac', newt) tl - | [] -> tac, typ - in - match l with - (_, hd) :: tl -> aux (intros, hd) tl - | [] -> raise (Invalid_argument "build_dependent_sum") - let id x = x let build_dependent_sum l = @@ -438,3 +423,32 @@ let rewrite_cases env c = let c' = rewrite_cases c in let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in c' + +let id_of_name = function + Name n -> n + | Anonymous -> raise (Invalid_argument "id_of_name") + +let definition_message id = + Options.if_verbose message ((string_of_id id) ^ " is defined") + +let recursive_message v = + match Array.length v with + | 0 -> error "no recursive definition" + | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined") + | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++ + spc () ++ str "are recursively defined") + +(* Solve an obligation using tactics, return the corresponding proof term *) +let solve_by_tac ev t = + debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev); + let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in + let ts = Tacmach.mk_pftreestate goal in + let solved_state = Tacmach.solve_pftreestate t ts in + let c = Tacmach.extract_pftreestate solved_state in + debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c); + c + +let rec string_of_list sep f = function + [] -> "" + | x :: [] -> f x + | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index 4a7e8177..ebfc5123 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -10,6 +10,7 @@ open Rawterm open Util open Evarutil open Names +open Sign val contrib_name : string val subtac_dir : string list @@ -51,6 +52,7 @@ val my_print_constr : env -> constr -> std_ppcmds val my_print_constr_expr : constr_expr -> std_ppcmds val my_print_evardefs : evar_defs -> std_ppcmds val my_print_context : env -> std_ppcmds +val my_print_named_context : env -> std_ppcmds val my_print_env : env -> std_ppcmds val my_print_rawconstr : env -> rawconstr -> std_ppcmds val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds @@ -88,3 +90,11 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> val destruct_ex : constr -> constr -> constr list val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr +val id_of_name : name -> identifier + +val definition_message : identifier -> unit +val recursive_message : global_reference array -> std_ppcmds + +val solve_by_tac : evar_info -> Tacmach.tactic -> constr + +val string_of_list : string -> ('a -> string) -> 'a list -> string diff --git a/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v new file mode 100644 index 00000000..7ab720f6 --- /dev/null +++ b/contrib/subtac/test/ListDep.v @@ -0,0 +1,86 @@ +Require Import List. +Require Import Coq.subtac.Utils. + +Set Implicit Arguments. + +Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l. + +Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'. +Proof. + intros. + inversion H. + split. + intros. + apply H0. + auto with datatypes. + auto with arith. +Qed. + +Section Map_DependentRecursor. + Variable U V : Set. + Variable l : list U. + Variable f : { x : U | In x l } -> V. + + Program Fixpoint map_rec ( l' : list U | sub_list l' l ) + { measure l' length } : { r : list V | length r = length l' } := + match l' with + nil => nil + | cons x tl => let tl' := map_rec tl in + f x :: tl' + end. + + Obligation 1. + intros. + destruct tl' ; simpl ; simpl in e. + subst x0 tl0. + rewrite <- Heql'. + rewrite e. + auto. + Qed. + + Obligation 2. + simpl. + intros. + destruct l'. + simpl in Heql'. + destruct x0 ; simpl ; try discriminate. + inversion Heql'. + inversion s. + apply H. + auto with datatypes. + Qed. + + + Obligation 3 of map_rec. + simpl. + intros. + rewrite <- Heql'. + simpl ; auto with arith. + Qed. + + Obligation 4. + simpl. + intros. + destruct l'. + simpl in Heql'. + destruct x0 ; simpl ; try discriminate. + inversion Heql'. + subst x tl. + apply sub_list_tl with u ; auto. + Qed. + + Obligation 5. + intros. + rewrite <- Heql' ; auto. + Qed. + + Program Definition map : list V := map_rec l. + Obligation 1. + split ; auto. + Qed. + +End Map_DependentRecursor. + +Extraction map. +Extraction map_rec. + |