aboutsummaryrefslogtreecommitdiff
path: root/plugins/romega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega')
-rw-r--r--plugins/romega/ROmega.v2
-rw-r--r--plugins/romega/const_omega.ml118
-rw-r--r--plugins/romega/const_omega.mli155
-rw-r--r--plugins/romega/g_romega.ml42
-rw-r--r--plugins/romega/refl_omega.ml108
5 files changed, 205 insertions, 180 deletions
diff --git a/plugins/romega/ROmega.v b/plugins/romega/ROmega.v
index 3ddb6bed12..657aae90e8 100644
--- a/plugins/romega/ROmega.v
+++ b/plugins/romega/ROmega.v
@@ -11,4 +11,4 @@ Require Export Setoid.
Require Export PreOmega.
Require Export ZArith_base.
Require Import OmegaPlugin.
-Declare ML Module "romega_plugin". \ No newline at end of file
+Declare ML Module "romega_plugin".
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 4ffbd5aa8b..0f5417e7db 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -7,14 +7,15 @@
*************************************************************************)
open Names
+open Constr
let module_refl_name = "ReflOmegaCore"
let module_refl_path = ["Coq"; "romega"; module_refl_name]
type result =
| Kvar of string
- | Kapp of string * Term.constr list
- | Kimp of Term.constr * Term.constr
+ | Kapp of string * constr list
+ | Kimp of constr * constr
| Kufo
let meaningful_submodule = [ "Z"; "N"; "Pos" ]
@@ -30,27 +31,27 @@ let string_of_global r =
prefix^(Names.Id.to_string (Nametab.basename_of_global r))
let destructurate t =
- let c, args = Term.decompose_app t in
- match Term.kind_of_term c, args with
- | Term.Const (sp,_), args ->
+ let c, args = decompose_app t in
+ match Constr.kind c, args with
+ | Const (sp,_), args ->
Kapp (string_of_global (Globnames.ConstRef sp), args)
- | Term.Construct (csp,_) , args ->
+ | Construct (csp,_) , args ->
Kapp (string_of_global (Globnames.ConstructRef csp), args)
- | Term.Ind (isp,_), args ->
+ | Ind (isp,_), args ->
Kapp (string_of_global (Globnames.IndRef isp), args)
- | Term.Var id, [] -> Kvar(Names.Id.to_string id)
- | Term.Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
+ | Var id, [] -> Kvar(Names.Id.to_string id)
+ | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
| _ -> Kufo
exception DestConstApp
let dest_const_apply t =
- let f,args = Term.decompose_app t in
+ let f,args = decompose_app t in
let ref =
- match Term.kind_of_term f with
- | Term.Const (sp,_) -> Globnames.ConstRef sp
- | Term.Construct (csp,_) -> Globnames.ConstructRef csp
- | Term.Ind (isp,_) -> Globnames.IndRef isp
+ match Constr.kind f with
+ | Const (sp,_) -> Globnames.ConstRef sp
+ | Construct (csp,_) -> Globnames.ConstructRef csp
+ | Ind (isp,_) -> Globnames.IndRef isp
| _ -> raise DestConstApp
in Nametab.basename_of_global ref, args
@@ -129,7 +130,7 @@ let coq_O = lazy(init_constant "O")
let rec mk_nat = function
| 0 -> Lazy.force coq_O
- | n -> Term.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
+ | n -> mkApp (Lazy.force coq_S, [| mk_nat (n-1) |])
(* Lists *)
@@ -141,47 +142,47 @@ let mkListConst c =
if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|]
else fun _ -> Univ.Instance.empty
in
- fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u)
+ fun u -> mkConstructU (Globnames.destConstructRef r, inst u)
-let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|])
-let coq_nil univ typ = Term.mkApp (mkListConst "nil" univ, [|typ|])
+let coq_cons univ typ = mkApp (mkListConst "cons" univ, [|typ|])
+let coq_nil univ typ = mkApp (mkListConst "nil" univ, [|typ|])
let mk_list univ typ l =
let rec loop = function
| [] -> coq_nil univ typ
| (step :: l) ->
- Term.mkApp (coq_cons univ typ, [| step; loop l |]) in
+ mkApp (coq_cons univ typ, [| step; loop l |]) in
loop l
let mk_plist =
- let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in
- fun l -> mk_list type1lev Term.mkProp l
+ let type1lev = Universes.new_univ_level () in
+ fun l -> mk_list type1lev mkProp l
let mk_list = mk_list Univ.Level.set
type parse_term =
- | Tplus of Term.constr * Term.constr
- | Tmult of Term.constr * Term.constr
- | Tminus of Term.constr * Term.constr
- | Topp of Term.constr
- | Tsucc of Term.constr
+ | Tplus of constr * constr
+ | Tmult of constr * constr
+ | Tminus of constr * constr
+ | Topp of constr
+ | Tsucc of constr
| Tnum of Bigint.bigint
| Tother
type parse_rel =
- | Req of Term.constr * Term.constr
- | Rne of Term.constr * Term.constr
- | Rlt of Term.constr * Term.constr
- | Rle of Term.constr * Term.constr
- | Rgt of Term.constr * Term.constr
- | Rge of Term.constr * Term.constr
+ | Req of constr * constr
+ | Rne of constr * constr
+ | Rlt of constr * constr
+ | Rle of constr * constr
+ | Rgt of constr * constr
+ | Rge of constr * constr
| Rtrue
| Rfalse
- | Rnot of Term.constr
- | Ror of Term.constr * Term.constr
- | Rand of Term.constr * Term.constr
- | Rimp of Term.constr * Term.constr
- | Riff of Term.constr * Term.constr
+ | Rnot of constr
+ | Ror of constr * constr
+ | Rand of constr * constr
+ | Rimp of constr * constr
+ | Riff of constr * constr
| Rother
let parse_logic_rel c = match destructurate c with
@@ -196,6 +197,7 @@ let parse_logic_rel c = match destructurate c with
(* Binary numbers *)
+let coq_Z = lazy (bin_constant "Z")
let coq_xH = lazy (bin_constant "xH")
let coq_xO = lazy (bin_constant "xO")
let coq_xI = lazy (bin_constant "xI")
@@ -209,33 +211,34 @@ let rec mk_positive n =
if Bigint.equal n Bigint.one then Lazy.force coq_xH
else
let (q,r) = Bigint.euclid n Bigint.two in
- Term.mkApp
+ mkApp
((if Bigint.equal r Bigint.zero
then Lazy.force coq_xO else Lazy.force coq_xI),
[| mk_positive q |])
let mk_N = function
| 0 -> Lazy.force coq_N0
- | n -> Term.mkApp (Lazy.force coq_Npos,
+ | n -> mkApp (Lazy.force coq_Npos,
[| mk_positive (Bigint.of_int n) |])
module type Int = sig
- val typ : Term.constr Lazy.t
- val plus : Term.constr Lazy.t
- val mult : Term.constr Lazy.t
- val opp : Term.constr Lazy.t
- val minus : Term.constr Lazy.t
-
- val mk : Bigint.bigint -> Term.constr
- val parse_term : Term.constr -> parse_term
- val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
+ val typ : constr Lazy.t
+ val is_int_typ : Proofview.Goal.t -> constr -> bool
+ val plus : constr Lazy.t
+ val mult : constr Lazy.t
+ val opp : constr Lazy.t
+ val minus : constr Lazy.t
+
+ val mk : Bigint.bigint -> constr
+ val parse_term : constr -> parse_term
+ val parse_rel : Proofview.Goal.t -> constr -> parse_rel
(* check whether t is built only with numbers and + * - *)
- val get_scalar : Term.constr -> Bigint.bigint option
+ val get_scalar : constr -> Bigint.bigint option
end
module Z : Int = struct
-let typ = lazy (bin_constant "Z")
+let typ = coq_Z
let plus = lazy (z_constant "Z.add")
let mult = lazy (z_constant "Z.mul")
let opp = lazy (z_constant "Z.opp")
@@ -265,9 +268,9 @@ let recognize_Z t =
let mk_Z n =
if Bigint.equal n Bigint.zero then Lazy.force coq_Z0
else if Bigint.is_strictly_pos n then
- Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
+ mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
else
- Term.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |])
+ mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |])
let mk = mk_Z
@@ -283,16 +286,13 @@ let parse_term t =
(match recognize_Z t with Some t -> Tnum t | None -> Tother)
| _ -> Tother
-let pf_nf gl c =
- EConstr.Unsafe.to_constr
- (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c))
+let is_int_typ gl t =
+ Tacmach.New.pf_apply Reductionops.is_conv gl
+ (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z))
let parse_rel gl t =
match destructurate t with
- | Kapp("eq",[typ;t1;t2]) ->
- (match destructurate (pf_nf gl typ) with
- | Kapp("Z",[]) -> Req (t1,t2)
- | _ -> Rother)
+ | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> Req (t1,t2)
| Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
| Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
| Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index a452b1a917..ecddc55de2 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -8,114 +8,117 @@
(** Coq objects used in romega *)
+open Constr
(* from Logic *)
-val coq_refl_equal : Term.constr lazy_t
-val coq_and : Term.constr lazy_t
-val coq_not : Term.constr lazy_t
-val coq_or : Term.constr lazy_t
-val coq_True : Term.constr lazy_t
-val coq_False : Term.constr lazy_t
-val coq_I : Term.constr lazy_t
+val coq_refl_equal : constr lazy_t
+val coq_and : constr lazy_t
+val coq_not : constr lazy_t
+val coq_or : constr lazy_t
+val coq_True : constr lazy_t
+val coq_False : constr lazy_t
+val coq_I : constr lazy_t
(* from ReflOmegaCore/ZOmega *)
-val coq_t_int : Term.constr lazy_t
-val coq_t_plus : Term.constr lazy_t
-val coq_t_mult : Term.constr lazy_t
-val coq_t_opp : Term.constr lazy_t
-val coq_t_minus : Term.constr lazy_t
-val coq_t_var : Term.constr lazy_t
-
-val coq_proposition : Term.constr lazy_t
-val coq_p_eq : Term.constr lazy_t
-val coq_p_leq : Term.constr lazy_t
-val coq_p_geq : Term.constr lazy_t
-val coq_p_lt : Term.constr lazy_t
-val coq_p_gt : Term.constr lazy_t
-val coq_p_neq : Term.constr lazy_t
-val coq_p_true : Term.constr lazy_t
-val coq_p_false : Term.constr lazy_t
-val coq_p_not : Term.constr lazy_t
-val coq_p_or : Term.constr lazy_t
-val coq_p_and : Term.constr lazy_t
-val coq_p_imp : Term.constr lazy_t
-val coq_p_prop : Term.constr lazy_t
-
-val coq_s_bad_constant : Term.constr lazy_t
-val coq_s_divide : Term.constr lazy_t
-val coq_s_not_exact_divide : Term.constr lazy_t
-val coq_s_sum : Term.constr lazy_t
-val coq_s_merge_eq : Term.constr lazy_t
-val coq_s_split_ineq : Term.constr lazy_t
-
-val coq_direction : Term.constr lazy_t
-val coq_d_left : Term.constr lazy_t
-val coq_d_right : Term.constr lazy_t
-
-val coq_e_split : Term.constr lazy_t
-val coq_e_extract : Term.constr lazy_t
-val coq_e_solve : Term.constr lazy_t
-
-val coq_interp_sequent : Term.constr lazy_t
-val coq_do_omega : Term.constr lazy_t
-
-val mk_nat : int -> Term.constr
-val mk_N : int -> Term.constr
+val coq_t_int : constr lazy_t
+val coq_t_plus : constr lazy_t
+val coq_t_mult : constr lazy_t
+val coq_t_opp : constr lazy_t
+val coq_t_minus : constr lazy_t
+val coq_t_var : constr lazy_t
+
+val coq_proposition : constr lazy_t
+val coq_p_eq : constr lazy_t
+val coq_p_leq : constr lazy_t
+val coq_p_geq : constr lazy_t
+val coq_p_lt : constr lazy_t
+val coq_p_gt : constr lazy_t
+val coq_p_neq : constr lazy_t
+val coq_p_true : constr lazy_t
+val coq_p_false : constr lazy_t
+val coq_p_not : constr lazy_t
+val coq_p_or : constr lazy_t
+val coq_p_and : constr lazy_t
+val coq_p_imp : constr lazy_t
+val coq_p_prop : constr lazy_t
+
+val coq_s_bad_constant : constr lazy_t
+val coq_s_divide : constr lazy_t
+val coq_s_not_exact_divide : constr lazy_t
+val coq_s_sum : constr lazy_t
+val coq_s_merge_eq : constr lazy_t
+val coq_s_split_ineq : constr lazy_t
+
+val coq_direction : constr lazy_t
+val coq_d_left : constr lazy_t
+val coq_d_right : constr lazy_t
+
+val coq_e_split : constr lazy_t
+val coq_e_extract : constr lazy_t
+val coq_e_solve : constr lazy_t
+
+val coq_interp_sequent : constr lazy_t
+val coq_do_omega : constr lazy_t
+
+val mk_nat : int -> constr
+val mk_N : int -> constr
(** Precondition: the type of the list is in Set *)
-val mk_list : Term.constr -> Term.constr list -> Term.constr
-val mk_plist : Term.types list -> Term.types
+val mk_list : constr -> constr list -> constr
+val mk_plist : types list -> types
(** Analyzing a coq term *)
(* The generic result shape of the analysis of a term.
One-level depth, except when a number is found *)
type parse_term =
- Tplus of Term.constr * Term.constr
- | Tmult of Term.constr * Term.constr
- | Tminus of Term.constr * Term.constr
- | Topp of Term.constr
- | Tsucc of Term.constr
+ Tplus of constr * constr
+ | Tmult of constr * constr
+ | Tminus of constr * constr
+ | Topp of constr
+ | Tsucc of constr
| Tnum of Bigint.bigint
| Tother
(* The generic result shape of the analysis of a relation.
One-level depth. *)
type parse_rel =
- Req of Term.constr * Term.constr
- | Rne of Term.constr * Term.constr
- | Rlt of Term.constr * Term.constr
- | Rle of Term.constr * Term.constr
- | Rgt of Term.constr * Term.constr
- | Rge of Term.constr * Term.constr
+ Req of constr * constr
+ | Rne of constr * constr
+ | Rlt of constr * constr
+ | Rle of constr * constr
+ | Rgt of constr * constr
+ | Rge of constr * constr
| Rtrue
| Rfalse
- | Rnot of Term.constr
- | Ror of Term.constr * Term.constr
- | Rand of Term.constr * Term.constr
- | Rimp of Term.constr * Term.constr
- | Riff of Term.constr * Term.constr
+ | Rnot of constr
+ | Ror of constr * constr
+ | Rand of constr * constr
+ | Rimp of constr * constr
+ | Riff of constr * constr
| Rother
(* A module factorizing what we should now about the number representation *)
module type Int =
sig
(* the coq type of the numbers *)
- val typ : Term.constr Lazy.t
+ val typ : constr Lazy.t
+ (* Is a constr expands to the type of these numbers *)
+ val is_int_typ : Proofview.Goal.t -> constr -> bool
(* the operations on the numbers *)
- val plus : Term.constr Lazy.t
- val mult : Term.constr Lazy.t
- val opp : Term.constr Lazy.t
- val minus : Term.constr Lazy.t
+ val plus : constr Lazy.t
+ val mult : constr Lazy.t
+ val opp : constr Lazy.t
+ val minus : constr Lazy.t
(* building a coq number *)
- val mk : Bigint.bigint -> Term.constr
+ val mk : Bigint.bigint -> constr
(* parsing a term (one level, except if a number is found) *)
- val parse_term : Term.constr -> parse_term
+ val parse_term : constr -> parse_term
(* parsing a relation expression, including = < <= >= > *)
- val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
+ val parse_rel : Proofview.Goal.t -> constr -> parse_rel
(* Is a particular term only made of numbers and + * - ? *)
- val get_scalar : Term.constr -> Bigint.bigint option
+ val get_scalar : constr -> Bigint.bigint option
end
(* Currently, we only use Z numbers *)
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 5fd9c94194..5b77d08dea 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -6,8 +6,6 @@
*************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
DECLARE PLUGIN "romega_plugin"
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 517df41d93..54ff44fbd3 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,6 +8,7 @@
open Pp
open Util
+open Constr
open Const_omega
module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
open OmegaSolver
@@ -27,8 +28,6 @@ let pp i = print_int i; print_newline (); flush stdout
(* More readable than the prefix notation *)
let (>>) = Tacticals.New.tclTHEN
-let mkApp = Term.mkApp
-
(* \section{Types}
\subsection{How to walk in a term}
To represent how to get to a proposition. Only choice points are
@@ -68,14 +67,14 @@ type comparaison = Eq | Leq | Geq | Gt | Lt | Neq
(it could contains some [Term.Var] but no [Term.Rel]). So no need to
lift when breaking or creating arrows. *)
type oproposition =
- Pequa of Term.constr * oequation (* constr = copy of the Coq formula *)
+ Pequa of constr * oequation (* constr = copy of the Coq formula *)
| Ptrue
| Pfalse
| Pnot of oproposition
| Por of int * oproposition * oproposition
| Pand of int * oproposition * oproposition
| Pimp of int * oproposition * oproposition
- | Pprop of Term.constr
+ | Pprop of constr
(* The equations *)
and oequation = {
@@ -102,9 +101,9 @@ and oequation = {
type environment = {
(* La liste des termes non reifies constituant l'environnement global *)
- mutable terms : Term.constr list;
+ mutable terms : constr list;
(* La meme chose pour les propositions *)
- mutable props : Term.constr list;
+ mutable props : constr list;
(* Traduction des indices utilisés ici en les indices finaux utilisés par
* la tactique Omega après dénombrement des variables utiles *)
real_indices : int IntHtbl.t;
@@ -184,8 +183,9 @@ let print_env_reification env =
let rec loop c i = function
[] -> str " ===============================\n\n"
| t :: l ->
+ let sigma, env = Pfedit.get_current_context () in
let s = Printf.sprintf "(%c%02d)" c i in
- spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++
+ spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
loop c (succ i) l
in
let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
@@ -219,7 +219,7 @@ let display_omega_var i = Printf.sprintf "OV%d" i
calcul des variables utiles. *)
let add_reified_atom t env =
- try List.index0 Term.eq_constr t env.terms
+ try List.index0 Constr.equal t env.terms
with Not_found ->
let i = List.length env.terms in
env.terms <- env.terms @ [t]; i
@@ -237,7 +237,7 @@ let set_reified_atom v t env =
(* \subsection{Gestion de l'environnement de proposition pour Omega} *)
(* ajout d'une proposition *)
let add_prop env t =
- try List.index0 Term.eq_constr t env.props
+ try List.index0 Constr.equal t env.props
with Not_found ->
let i = List.length env.props in env.props <- env.props @ [t]; i
@@ -547,22 +547,33 @@ let display_gl env t_concl t_lhyps =
Printf.printf "REIFED PROBLEM\n\n";
Printf.printf " CONCL: %a\n" pprint t_concl;
List.iter
- (fun (i,t) -> Printf.printf " %s: %a\n" (Id.to_string i) pprint t)
+ (fun (i,_,t) -> Printf.printf " %s: %a\n" (Id.to_string i) pprint t)
t_lhyps;
print_env_reification env
+type defined = Defined | Assumed
+
+let reify_hyp env gl i =
+ let open Context.Named.Declaration in
+ let ctxt = (false,[],i,[]) in
+ match Tacmach.New.pf_get_hyp i gl with
+ | LocalDef (_,d,t) when Z.is_int_typ gl (EConstr.Unsafe.to_constr t) ->
+ let d = EConstr.Unsafe.to_constr d in
+ let dummy = Lazy.force coq_True in
+ let p = mk_equation env ctxt dummy Eq (mkVar i) d in
+ i,Defined,p
+ | LocalDef (_,_,t) | LocalAssum (_,t) ->
+ let t = EConstr.Unsafe.to_constr t in
+ let p = oproposition_of_constr env ctxt gl t in
+ i,Assumed,p
+
let reify_gl env gl =
let concl = Tacmach.New.pf_concl gl in
let concl = EConstr.Unsafe.to_constr concl in
- let hyps = Tacmach.New.pf_hyps_types gl in
- let hyps = List.map (fun (i,t) -> (i,EConstr.Unsafe.to_constr t)) hyps in
- let t_concl =
- oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl in
- let t_lhyps =
- List.map
- (fun (i,t) -> i,oproposition_of_constr env (false,[],i,[]) gl t)
- hyps
- in
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
+ let ctxt_concl = (true,[],id_concl,[O_mono]) in
+ let t_concl = oproposition_of_constr env ctxt_concl gl concl in
+ let t_lhyps = List.map (reify_hyp env gl) hyps in
let () = if !debug then display_gl env t_concl t_lhyps in
t_concl, t_lhyps
@@ -602,7 +613,7 @@ and destruct_neg_hyp eqns = function
let rec destructurate_hyps = function
| [] -> [[]]
- | (i,t) :: l ->
+ | (i,_,t) :: l ->
let l_syst1 = destruct_pos_hyp [] t in
let l_syst2 = destructurate_hyps l in
List.cartesian (@) l_syst1 l_syst2
@@ -673,6 +684,9 @@ let rec stated_in_tree = function
| Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2)
| Leaf s -> stated_in_trace s.s_trace
+let mk_refl t =
+ EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; t|])
+
let digest_stated_equations env tree =
let do_equation st (vars,gens,eqns,ids) =
(** We turn the definition of [v]
@@ -684,9 +698,7 @@ let digest_stated_equations env tree =
(** We then update the environment *)
set_reified_atom st.st_var coq_v env;
(** The term we'll introduce *)
- let term_to_generalize =
- EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; coq_v|])
- in
+ let term_to_generalize = mk_refl coq_v in
(** Its representation as equation (but not reified yet,
we lack the proper env to do that). *)
let term_to_reify = (v_def,Oatom st.st_var) in
@@ -954,18 +966,19 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
display_solution_tree stdout solution_tree;
print_newline()
end;
- (** Collect all hypotheses used in the solution tree *)
+ (** Collect all hypotheses and variables used in the solution tree *)
let useful_equa_ids = equas_of_solution_tree solution_tree in
- let equations = List.map (get_equation env) (IntSet.elements useful_equa_ids)
+ let useful_hypnames, useful_vars =
+ IntSet.fold
+ (fun i (hyps,vars) ->
+ let e = get_equation env i in
+ Id.Set.add e.e_origin.o_hyp hyps,
+ vars_of_equations [e] @@ vars)
+ useful_equa_ids
+ (Id.Set.empty, vars_of_prop reified_concl)
in
- let hyps_of_eqns =
- List.fold_left (fun s e -> Id.Set.add e.e_origin.o_hyp s) Id.Set.empty in
- let hyps = hyps_of_eqns equations in
- let useful_hypnames = Id.Set.elements (Id.Set.remove id_concl hyps) in
- let useful_hyptypes =
- List.map (fun id -> List.assoc_f Id.equal id reified_hyps) useful_hypnames
- in
- let useful_vars = vars_of_equations equations @@ vars_of_prop reified_concl
+ let useful_hypnames =
+ Id.Set.elements (Id.Set.remove id_concl useful_hypnames)
in
(** Parts coming from equations introduced by omega: *)
@@ -996,9 +1009,17 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
let reified_concl = reified_of_proposition env reified_concl in
let l_reified_terms =
List.map
- (fun p -> reified_of_proposition env (maximize_prop useful_equa_ids p))
- useful_hyptypes
+ (fun id ->
+ match Id.Map.find id reified_hyps with
+ | Defined,p ->
+ reified_of_proposition env p, mk_refl (mkVar id)
+ | Assumed,p ->
+ reified_of_proposition env (maximize_prop useful_equa_ids p),
+ EConstr.mkVar id
+ | exception Not_found -> assert false)
+ useful_hypnames
in
+ let l_reified_terms, l_reified_hypnames = List.split l_reified_terms in
let env_props_reified = mk_plist env.props in
let reified_goal =
mk_list (Lazy.force coq_proposition)
@@ -1007,14 +1028,14 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
app coq_interp_sequent
[| reified_concl;env_props_reified;reduced_term_env;reified_goal|]
in
+ let mk_occ id = {o_hyp=id;o_path=[]} in
let initial_context =
- List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) useful_hypnames in
+ List.map (fun id -> CCHyp (mk_occ id)) useful_hypnames in
let context =
- CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
+ CCHyp (mk_occ id_concl) :: hyp_stated_vars @ initial_context in
let decompose_tactic = decompose_tree env context solution_tree in
- Tactics.generalize
- (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >>
+ Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >>
Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >>
Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >>
show_goal >>
@@ -1034,13 +1055,16 @@ let total_reflexive_omega_tactic unsafe =
rst_omega_var ();
try
let env = new_environment () in
- let (concl,hyps) as reified_goal = reify_gl env gl in
+ let (concl,hyps) = reify_gl env gl in
(* Register all atom indexes created during reification as omega vars *)
set_omega_maxvar (pred (List.length env.terms));
- let full_reified_goal = (id_concl,Pnot concl) :: hyps in
+ let full_reified_goal = (id_concl,Assumed,Pnot concl) :: hyps in
let systems_list = destructurate_hyps full_reified_goal in
+ let hyps =
+ List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps
+ in
if !debug then display_systems systems_list;
- resolution unsafe env reified_goal systems_list
+ resolution unsafe env (concl,hyps) systems_list
with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system")
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:44:23 +0000