diff options
author | 2006-10-31 12:57:26 +0000 | |
---|---|---|
committer | 2006-10-31 12:57:26 +0000 | |
commit | a9cada8872c8151c583cdac52e7e97a1b848ac45 (patch) | |
tree | b7856cbcab8f4de57ebd63e5c1a376e44d6d91b3 | |
parent | 3e317792aa9683e093465ce98f839c14f5c94867 (diff) |
Work on obligation separation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9326 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/subtac/eterm.ml | 212 | ||||
-rw-r--r-- | contrib/subtac/eterm.mli | 5 | ||||
-rw-r--r-- | contrib/subtac/g_subtac.ml4 | 5 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 14 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 81 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.mli | 9 | ||||
-rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 4 |
7 files changed, 139 insertions, 191 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 9c11569ef..b95f643a5 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -32,71 +32,33 @@ 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 evar_info id = - let rec aux i = function - (k, h, v) :: tl -> - if k = id then (i, h, v) else aux (succ i) tl - | [] -> raise Not_found - in - let (idx, hyps, v) = aux 0 evs in - n + idx + 1, hyps - 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 = - 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 - | _, _ -> acc (* failwith "subst_evars: invalid argument" *) - in aux hyps (Array.to_list args) [] - in - mkApp (ex, Array.of_list args)) - | _ -> map_constr_with_binders succ substrec depth c - in - substrec 0 t - let subst_evar_constr evs n t = + let seen = ref Intset.empty in let evar_info id = let rec aux i = function - (k, n, h, v) :: tl -> - if k = id then (n, 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 (c, hyps, v) = aux 0 evs in - c, hyps + in aux 0 evs in let rec substrec depth c = match kind_of_term c with | Evar (k, args) -> - (let ex, 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 _ -> () ); - (* 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) @@ -106,10 +68,11 @@ let subst_evar_constr evs n t = | _, _ -> 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, @@ -127,70 +90,31 @@ 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 - let copt' = option_map (subst_evars evs n) copt in + 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 - mkNamedProd_or_LetIn (id, copt', t'') (aux (id :: acc) (succ n) tl) + 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 = - (* 'Serialize' the evars, we assume that the types of the existentials - refer to previous existentials in the list only *) - let evl = to_list evm in - trace (str "Eterm, transformed to list"); - let evts = - (* Remove existential variables in types and build the corresponding products *) - fold_right - (fun (id, ev) l -> - trace (str "Eterm: " ++ str "treating evar: " ++ int id); - let hyps = Environ.named_context_of_val ev.evar_hyps in - let evtyp = etype_of_evar l ev hyps in - trace (str "Evar's type is: " ++ Termops.print_constr_env (Global.env ()) evtyp); - let y' = (id, hyps, evtyp) in - y' :: l) - evl [] - in - let t' = (* Substitute evar refs in the term by De Bruijn indices *) - subst_evars evts 0 t - in - let evar_names = - let i = ref 0 in - List.map (fun (id, _, c) -> incr i; (id_of_string ("evar_" ^ string_of_int !i)), 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 - (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(option_map - (fun typ -> - trace (str "Type :" ++ spc () ++ - Termops.print_constr_env (Global.env ()) typ)) - tycon); - with _ -> ()); - t'', tycon, evar_names - let rec take n l = if n = 0 then [] else List.hd l :: take (pred n) (List.tl l) @@ -203,34 +127,30 @@ let eterm_obligations name nclen evm t tycon = refer to previous existentials in the list only *) let evl = to_list evm in trace (str "Eterm, transformed to list"); + let evn = + let i = ref (-1) in + List.map (fun (id, ev) -> incr i; + (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int !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 hyps = trunc_named_context nclen hyps in - trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps); - let evtyp = etype_of_evar l ev hyps in - trace (str "Evar's type is: " ++ Termops.print_constr_env (Global.env ()) evtyp); - let y' = (id, hyps, evtyp) 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 evar_names = - let i = ref 0 in - List.map (fun (id, h, c) -> incr i; - (id, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int !i), h, c)) evts - in - let t' = (* Substitute evar refs in the term by De Bruijn indices *) - subst_evar_constr (List.map (fun (id, n, h, c) -> id, mkVar n, h, c) evar_names) 0 t + let t', _ = (* Substitute evar refs in the term by variables *) + subst_evar_constr evts 0 t in - let _, evars = - fold_right - (fun (_, n, h, c) (acc, l) -> - let evt = Termops.it_mkProd_wo_LetIn c acc in - ((Name n, None, c) :: acc, (n, evt) :: l)) - evar_names ([], []) + let evars = + List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts in (try trace (str "Term given to eterm" ++ spc () ++ @@ -238,26 +158,12 @@ let eterm_obligations name nclen evm t tycon = trace (str "Term constructed in eterm" ++ spc () ++ Termops.print_constr_env (Global.env ()) t'); ignore(iter - (fun (n, typ) -> - trace (str "Evar :" ++ spc () ++ str (string_of_id n) ++ + (fun (name, typ, deps) -> + trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ Termops.print_constr_env (Global.env ()) typ)) evars); with _ -> ()); - let subst_closure l = - let l' = List.map2 (fun (id, _, h, c) cst -> (id, cst, h, c)) evar_names l in - let _, l'' = - List.fold_right - (fun (id, cst, h, c) (acc, res) -> - let cst' = applist (cst, List.rev acc) in - (cst' :: acc, (id, cst', h, c) :: res)) - l' ([], []) - in - let t' = subst_evar_constr l'' 0 t in - trace (str "Term constructed in eterm" ++ spc () ++ - Termops.print_constr_env (Global.env ()) t'); - t' - in - subst_closure, evars + Array.of_list evars, t' let mkMetas n = let rec aux i acc = @@ -265,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 dec9efa8b..77d9f293d 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -12,12 +12,13 @@ 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 -> - (constr list -> constr) * (identifier * types) list + (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 ff3bcb82e..1ec77c690 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -30,6 +30,7 @@ open Topconstr module Gram = Pcoq.Gram module Vernac = Pcoq.Vernac_ +module Tactic = Pcoq.Tactic module SubtacGram = struct @@ -76,4 +77,8 @@ VERNAC COMMAND EXTEND Subtac [ "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_command.ml b/contrib/subtac/subtac_command.ml index e9e26fb88..b433af2cc 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -304,16 +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 = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in + let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in (try trace (str "Generated obligations : "); - List.iter - (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) + 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() @@ -524,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 @@ -544,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 + in assert(false) + (*build_mutrec lnameargsardef boxed*) diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 195c879c9..859180036 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -71,7 +71,7 @@ let declare_definition prg = Subtac_utils.definition_message prg.prg_name open Evd - + let add_entry n b t obls = Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let try_tactics e = @@ -103,26 +103,11 @@ let add_entry n b t obls = declare_definition prg else from_prg := ProgMap.add n prg !from_prg - -(* -let (theory_to_obj, obj_to_theory) = - let cache_th (name,th) = add_entry name th - and export_th x = Some x in - declare_object - {(default_object "program-tcc") with - open_function = (fun i o -> if i=1 then cache_th o); - cache_function = cache_th; - subst_function = (fun _ -> assert(false)); - classify_function = (fun (_,x) -> Dispose); - export_function = export_th } -*) let error s = Util.error s -let subtac_obligation (user_num, name) = - let num = pred user_num in +let get_prog name = let prg_infos = !from_prg in - let prg = match name with Some n -> ProgMap.find n prg_infos | None -> @@ -131,7 +116,20 @@ let subtac_obligation (user_num, name) = 0 -> error "No obligations remaining" | 1 -> map_first prg_infos | _ -> error "More than one program with unsolved obligations") - in + +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 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 @@ -143,14 +141,7 @@ let subtac_obligation (user_num, name) = let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in let obls = Array.copy obls in let _ = obls.(num) <- obl in - let prg' = { prg with prg_obligations = (obls, pred 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 - )); + update_obls prg obls (pred rem)); trace (str "Started obligation " ++ int user_num ++ str " proof") | Some r -> error "Obligation already solved" else error (sprintf "Unknown obligation number %i" (succ num)) @@ -166,3 +157,41 @@ let obligations_of_evars evars = obl_body = None; }) evars) in arr, Array.length arr + +let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; + evar_concl = o.obl_type ; + evar_body = Evar_empty ; + evar_extra = None } + + + +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 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 index 413272980..7d93d57bb 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,3 +1,10 @@ -val add_entry : Names.identifier -> (Term.constr list -> Term.constr) -> Term.types -> (Names.identifier * Term.types) list -> unit +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 b3f8e2210..f518f1ccf 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -158,6 +158,6 @@ 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, evars = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in + let evars, def = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in trace (str "Adding to obligations list"); - add_entry id evars_def coqt evars + add_entry id def coqt evars |