From b3bfd6b249600b15552c890306a635aee30c2a74 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 24 Feb 2004 14:56:24 +0000 Subject: [PATCH] Partial porting to V8 URIs. Almost nothing has been tested yet. --- helm/ocaml/cic/helmLibraryObjects.ml | 63 +- .../ocaml/cic_disambiguation/arit_notation.ml | 37 +- .../cic_disambiguation/disambiguateChoices.ml | 9 +- .../cic_disambiguation/logic_notation.ml | 11 +- helm/ocaml/cic_omdoc/cic2content.ml | 12 +- .../cic_proof_checking/cicTypeChecker.ml | 2 +- .../content_expressions.ml | 101 +-- helm/ocaml/tactics/equalityTactics.ml | 53 +- helm/ocaml/tactics/fourierR.ml | 774 +++++++++--------- helm/ocaml/tactics/negationTactics.ml | 4 +- .../texCicTextualParser.mly | 81 +- 11 files changed, 531 insertions(+), 616 deletions(-) diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 3d32065be..83f2d3647 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -52,9 +52,32 @@ let term_of_uri ?(subst = []) uri = module Logic = struct - let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind" + let eq_SURI = "cic:/Coq/Init/Logic/eq.ind" + let eq_URI = uri eq_SURI + let eq_XURI = eq_SURI ^ "#xpointer(1/1)" + let eq_ind_URI = uri "cic:/Coq/Init/Logic/eq_ind.con" + let eq_ind_r_URI = uri "cic:/Coq/Init/Logic/eq_ind_r.con" let true_URI = uri "cic:/Coq/Init/Logic/True.ind" let false_URI = uri "cic:/Coq/Init/Logic/False.ind" + let false_ind_URI = uri "cic:/Coq/Init/Logic/False_ind.con" + let ex_SURI = "cic:/Coq/Init/Logic/ex.ind" + let ex_URI = uri ex_SURI + let ex_XURI = ex_SURI ^ "#xpointer(1/1)" + let ex_ind_URI = uri "cic:/Coq/Init/Logic/ex_ind.con" + let and_SURI = "cic:/Coq/Init/Logic/and.ind" + let and_URI = uri and_SURI + let and_XURI = and_SURI ^ "#xpointer(1/1)" + let and_ind_URI = uri "cic:/Coq/Init/Logic/and_ind.con" + let or_SURI = "cic:/Coq/Init/Logic/or.ind" + let or_URI = uri or_SURI + let or_XURI = or_SURI ^ "#xpointer(1/1)" + let not_SURI = "cic:/Coq/Init/Logic/not.con" + let not_URI = uri not_SURI + let iff_SURI = "cic:/Coq/Init/Logic/iff.con" + let iff_URI = uri "cic:/Coq/Init/Logic/iff.con" + let sym_eq_URI = uri "cic:/Coq/Init/Logic/sym_eq.con" + let trans_eq_URI = uri "cic:/Coq/Init/Logic/trans_eq.con" + let absurd_URI = uri "cic:/Coq/Init/Logic/absurd.con" end module Logic_Type = @@ -80,12 +103,27 @@ module Datatypes = module Reals = struct let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con" - let rplus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rplus.con" + let rplus_SURI = "cic:/Coq/Reals/Rdefinitions/Rplus.con" + let rplus_URI = uri rplus_SURI + let rminus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rminus.con" let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con" - let ropp_URI = uri "cic:/Coq/Reals/Rdefinitions/Ropp.con" + let rdiv_URI = uri "cic:/Coq/Reals/Rdefinitions/Rdiv.con" + let ropp_SURI = "cic:/Coq/Reals/Rdefinitions/Ropp.con" + let ropp_URI = uri ropp_SURI + let rinv_SURI = "cic:/Coq/Reals/Rdefinitions/Rinv.con" + let rinv_URI = uri rinv_SURI let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con" let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con" + let rle_SURI = "cic:/Coq/Reals/Rdefinitions/Rle.con" + let rle_URI = uri rle_SURI + let rge_SURI = "cic:/Coq/Reals/Rdefinitions/Rge.con" + let rge_URI = uri rge_SURI + let rlt_SURI = "cic:/Coq/Reals/Rdefinitions/Rlt.con" + let rlt_URI = uri rlt_SURI + let rgt_SURI = "cic:/Coq/Reals/Rdefinitions/Rgt.con" + let rgt_URI = uri rgt_SURI let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con" + let rinv_r1_URI = uri "cic:/Coq/Reals/Rbase/Rinv_R1.con" let r = const r_URI let rplus = const rplus_URI @@ -98,15 +136,32 @@ module Reals = module Peano = struct - let plus_URI = uri "cic:/Coq/Init/Peano/plus.con" + let plus_SURI = "cic:/Coq/Init/Peano/plus.con" + let plus_URI = uri plus_SURI + let minus_URI = uri "cic:/Coq/Init/Peano/minus.con" let mult_URI = uri "cic:/Coq/Init/Peano/mult.con" let pred_URI = uri "cic:/Coq/Init/Peano/pred.con" + let le_SURI = "cic:/Coq/Init/Peano/le.ind" + let le_URI = uri le_SURI + let le_XURI = le_SURI ^ "#xpointer(1/1)" + let ge_SURI = "cic:/Coq/Init/Peano/ge.con" + let ge_URI = uri ge_SURI + let lt_SURI = "cic:/Coq/Init/Peano/lt.con" + let lt_URI = uri lt_SURI + let gt_SURI = "cic:/Coq/Init/Peano/lt.con" + let gt_URI = uri gt_SURI + let lt_URI = uri "cic:/Coq/Init/Peano/lt.con" let plus = const plus_URI let mult = const mult_URI let pred = const pred_URI end +module BinInt = + struct + let zplus_SURI = "cic:/Coq/ZArith/BinInt/Zplus.con" + end + (** {2 Helpers for creating common terms} * (e.g. numbers)} *) diff --git a/helm/ocaml/cic_disambiguation/arit_notation.ml b/helm/ocaml/cic_disambiguation/arit_notation.ml index b24942775..51faaa6ac 100644 --- a/helm/ocaml/cic_disambiguation/arit_notation.ml +++ b/helm/ocaml/cic_disambiguation/arit_notation.ml @@ -65,9 +65,8 @@ EXTEND END let _ = - let uri s = UriManager.uri_of_string s in - let const s = Cic.Const (uri s, []) in - let mutind s = Cic.MutInd (uri s, 0, []) in + let const s = Cic.Const (s, []) in + let mutind s = Cic.MutInd (s, 0, []) in DisambiguateChoices.add_num_choice ("natural number", @@ -81,34 +80,34 @@ let _ = DisambiguateChoices.add_binary_op "plus" "real plus" HelmLibraryObjects.Reals.rplus; DisambiguateChoices.add_binary_op "minus" "natural minus" - (const "cic:/Coq/Arith/Minus/minus.con"); + (const HelmLibraryObjects.Peano.minus_URI); DisambiguateChoices.add_binary_op "minus" "real minus" - (const "cic:/Coq/Reals/Rdefinitions/Rminus.con"); + (const HelmLibraryObjects.Reals.rminus_URI); DisambiguateChoices.add_binary_op "times" "natural times" - (const "cic:/Coq/Init/Peano/mult.con"); + (const HelmLibraryObjects.Peano.mult_URI); DisambiguateChoices.add_binary_op "times" "real times" - (const "cic:/Coq/Reals/Rdefinitions/Rmult.con"); + (const HelmLibraryObjects.Reals.rmult_URI); DisambiguateChoices.add_binary_op "divide" "real divide" - (const "cic:/Coq/Reals/Rdefinitions/Rdiv.con"); + (const HelmLibraryObjects.Reals.rdiv_URI); DisambiguateChoices.add_unary_op "uminus" "real unary minus" - (const "cic:/Coq/Reals/Rdefinitions/Ropp.con"); + (const HelmLibraryObjects.Reals.ropp_URI); DisambiguateChoices.add_binary_op "leq" "natural 'less or equal to'" - (mutind "cic:/Coq/Init/Peano/le.ind"); + (mutind HelmLibraryObjects.Peano.le_URI); DisambiguateChoices.add_binary_op "leq" "real 'less or equal to'" - (const "cic:/Coq/Reals/Rdefinitions/Rle.con"); + (const HelmLibraryObjects.Reals.rle_URI); DisambiguateChoices.add_binary_op "geq" "natural 'greater or equal to'" - (const "cic:/Coq/Init/Peano/ge.con"); + (const HelmLibraryObjects.Peano.ge_URI); DisambiguateChoices.add_binary_op "geq" "real 'greater or equal to'" - (const "cic:/Coq/Reals/Rdefinitions/Rge.con"); + (const HelmLibraryObjects.Reals.rge_URI); DisambiguateChoices.add_binary_op "lt" "natural 'less than'" - (const "cic:/Coq/Init/Peano/lt.con"); + (const HelmLibraryObjects.Peano.lt_URI); DisambiguateChoices.add_binary_op "lt" "real 'less than'" - (const "cic:/Coq/Reals/Rdefinitions/Rlt.con"); + (const HelmLibraryObjects.Reals.rlt_URI); DisambiguateChoices.add_binary_op "gt" "natural 'greater than'" - (const "cic:/Coq/Init/Peano/gt.con"); + (const HelmLibraryObjects.Peano.gt_URI); DisambiguateChoices.add_binary_op "gt" "real 'greater than'" - (const "cic:/Coq/Reals/Rdefinitions/Rgt.con"); + (const HelmLibraryObjects.Reals.rgt_URI); DisambiguateChoices.add_symbol_choice "neq" ("not equal to (leibnitz)", (fun env _ args -> @@ -117,7 +116,7 @@ let _ = | [t1; t2] -> t1, t2 | _ -> raise DisambiguateChoices.Invalid_choice in - Cic.Appl [ const "cic:/Coq/Init/Logic/not.con"; + Cic.Appl [ const HelmLibraryObjects.Logic.not_URI; Cic.Appl [ Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); Cic.Implicit (Some `Type); t1; t2 ] ])); @@ -129,7 +128,7 @@ let _ = | [t1; t2] -> t1, t2 | _ -> raise DisambiguateChoices.Invalid_choice in - Cic.Appl [ const "cic:/Coq/Init/Logic/not.con"; + Cic.Appl [ const HelmLibraryObjects.Logic.not_URI; Cic.Appl [ Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []); Cic.Implicit (Some `Type); t1; t2 ] ])); diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml index c74566f20..9caf77aab 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml @@ -84,10 +84,5 @@ let lookup_num_by_dsc dsc = (** initial table contents *) let _ = - let uri s = UriManager.uri_of_string s in - let const s = Cic.Const (uri s, []) in - let mutind s = Cic.MutInd (uri s, 0, []) in - add_binary_op "exists" "exists" (mutind "cic:/Coq/Init/Logic/ex.ind"); - add_binary_op "exists" "exists over terms with sort Type" - (mutind "cic:/Coq/Init/Logic_Type/exT.ind"); - + add_binary_op "exists" "exists" + (Cic.MutInd (HelmLibraryObjects.Logic.ex_URI, 0, [])) diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index fdbc75bf1..885cc2140 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -51,9 +51,8 @@ END let _ = (* TODO cut-and-pasted code: here, in arit_notation.ml and * disambiguateChoices.ml *) - let uri s = UriManager.uri_of_string s in - let const s = Cic.Const (uri s, []) in - let mutind s = Cic.MutInd (uri s, 0, []) in + let const s = Cic.Const (s, []) in + let mutind s = Cic.MutInd (s, 0, []) in DisambiguateChoices.add_symbol_choice "eq" ("leibnitz's equality", (fun interp _ args -> @@ -79,9 +78,9 @@ let _ = Cic.Implicit (Some `Type); t1; t2 ])); DisambiguateChoices.add_binary_op "and" "logical and" - (mutind "cic:/Coq/Init/Logic/and.ind"); + (mutind HelmLibraryObjects.Logic.and_URI); DisambiguateChoices.add_binary_op "or" "logical or" - (mutind "cic:/Coq/Init/Logic/or.ind"); + (mutind HelmLibraryObjects.Logic.or_URI); DisambiguateChoices.add_unary_op "not" "logical not" - (const "cic:/Coq/Init/Logic/not.con"); + (const HelmLibraryObjects.Logic.not_URI); diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 61003f930..49e2e23ad 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -678,10 +678,9 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = if n<0 then raise NotApplicable else let method_name = - if (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or - uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists" - else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd" - else if uri_str = "cic:/Coq/Init/Logic/False_ind.con" then "FalseInd" + if UriManager.eq uri HelmLibraryObjects.Logic.ex_ind_URI then "Exists" + else if UriManager.eq uri HelmLibraryObjects.Logic.and_ind_URI then "AndInd" + else if UriManager.eq uri HelmLibraryObjects.Logic.false_ind_URI then "FalseInd" else "ByInduction" in let prefix = String.sub uri_str 0 n in let ind_str = (prefix ^ ".ind") in @@ -790,9 +789,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let module C = Cic in match li with C.AConst (sid,uri,exp_named_subst)::args -> - let uri_str = UriManager.string_of_uri uri in - if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or - uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then + if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI or + UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_r_URI then let subproofs,arg = (match build_subproofs_and_args diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 3f504ab79..137f786ab 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -265,7 +265,7 @@ and weakly_positive context n nn uri te = let module C = Cic in (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*) let dummy_mutind = - C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,[]) + C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[]) in (*CSC mettere in cicSubstitution *) let rec subst_inductive_type_with_dummy_mutind = diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 07373374f..4d0708ae5 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -67,78 +67,63 @@ and let symbol_table = Hashtbl.create 503;; (* eq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "eq", - None, Some "cic:/Coq/Init/Logic/eq.ind")) + None, Some HelmLibraryObjects.Logic.eq_SURI)) :: List.map acic2cexpr (List.tl args)));; -Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)" - (fun aid sid args acic2cexpr -> - Appl - (Some aid, (Symbol (Some sid, "eq", - None, Some "cic:/Coq/Init/Logic_Type/eqT.ind")) - :: List.map acic2cexpr (List.tl args)));; - (* and *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "and", - None, Some "cic:/Coq/Init/Logic/and.ind")) + None, Some HelmLibraryObjects.Logic.and_SURI)) :: List.map acic2cexpr args));; (* or *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "or", - None, Some "cic:/Coq/Init/Logic/or.ind")) + None, Some HelmLibraryObjects.Logic.or_SURI)) :: List.map acic2cexpr args));; (* iff *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "iff", - None, Some "cic:/Coq/Init/Logic/iff.con")) + None, Some HelmLibraryObjects.Logic.iff_SURI)) :: List.map acic2cexpr args));; (* not *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "not", - None, Some "cic:/Coq/Init/Logic/not.con")) + None, Some HelmLibraryObjects.Logic.not_SURI)) :: List.map acic2cexpr args));; (* Rinv *) -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "inv", - None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con")) + None, Some HelmLibraryObjects.Reals.rinv_SURI)) :: List.map acic2cexpr args));; (* Ropp *) -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "opp", - None, Some "cic:/Coq/Reals/Rdefinitions/Ropp.con")) + None, Some HelmLibraryObjects.Reals.ropp_SURI)) :: List.map acic2cexpr args));; (* exists *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" - (fun aid sid args acic2cexpr -> - match (List.tl args) with - [Cic.ALambda (_,Cic.Name n,s,t)] -> - Binder - (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t) - | _ -> raise Not_found);; - -Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI (fun aid sid args acic2cexpr -> match (List.tl args) with [Cic.ALambda (_,Cic.Name n,s,t)] -> @@ -147,101 +132,97 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" | _ -> raise Not_found);; (* leq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.le_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "leq", - None, Some "cic:/Coq/Init/Peano/le.ind")) + None, Some HelmLibraryObjects.Peano.le_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "leq", - None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con")) + None, Some HelmLibraryObjects.Reals.rle_SURI)) :: List.map acic2cexpr args));; (* lt *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "lt", - None, Some "cic:/Coq/Init/Peano/lt.con")) + None, Some HelmLibraryObjects.Peano.lt_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "lt", - None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con")) + None, Some HelmLibraryObjects.Reals.rlt_SURI)) :: List.map acic2cexpr args));; (* geq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "geq", - None, Some "cic:/Coq/Init/Peano/ge.con")) + None, Some HelmLibraryObjects.Peano.ge_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "geq", - None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con")) + None, Some HelmLibraryObjects.Reals.rge_SURI)) :: List.map acic2cexpr args));; (* gt *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "gt", - None, Some "cic:/Coq/Init/Peano/gt.con")) + None, Some HelmLibraryObjects.Peano.gt_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "gt", - None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con")) + None, Some HelmLibraryObjects.Reals.rgt_SURI)) :: List.map acic2cexpr args));; (* plus *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "plus", - None, Some "cic:/Coq/Init/Peano/plus.con")) + None, Some HelmLibraryObjects.Peano.plus_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con" +Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "plus", - None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con")) + None, Some HelmLibraryObjects.BinInt.zplus_SURI)) :: List.map acic2cexpr args));; -let rplus_uri = - UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;; -let r0_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" ;; -let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;; - -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI (fun aid sid args acic2cexpr -> let appl () = Appl (Some aid, (Symbol (Some sid, "plus", - None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con")) + None, Some HelmLibraryObjects.Reals.rplus_SURI)) :: List.map acic2cexpr args) in let rec aux acc = function | [ Cic.AConst (nid, uri, []); n] when - UriManager.eq uri r1_uri -> + UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> (match n with - | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri -> + | Cic.AConst (_, uri, []) when + UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> Num (Some aid, string_of_int (acc + 2)) | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when - UriManager.eq uri rplus_uri -> + UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI -> aux (acc + 1) args | _ -> appl ()) | _ -> appl () diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index ac28f9a28..232911450 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -32,19 +32,12 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = let eq_ind_r,ty,t1,t2 = match CicTypeChecker.type_of_aux' metasenv context equality with C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] - when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + when U.eq uri HelmLibraryObjects.Logic.eq_URI -> let eq_ind_r = C.Const - (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[]) + (HelmLibraryObjects.Logic.eq_ind_r_URI,[]) in eq_ind_r,ty,t1,t2 - | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] - when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> - let eqT_ind_r = - C.Const - (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[]) - in - eqT_ind_r,ty,t1,t2 | _ -> raise (ProofEngineTypes.Fail @@ -94,19 +87,11 @@ let rewrite_back_tac ~term:equality ~status:(proof,goal) = let eq_ind_r,ty,t1,t2 = match CicTypeChecker.type_of_aux' metasenv context equality with C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] - when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") -> + when U.eq uri HelmLibraryObjects.Logic.eq_URI -> let eq_ind_r = - C.Const - (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[]) + C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[]) in eq_ind_r,ty,t2,t1 - | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2] - when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> - let eqT_ind_r = - C.Const - (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con",[]) - in - eqT_ind_r,ty,t2,t1 | _ -> raise (ProofEngineTypes.Fail @@ -161,19 +146,11 @@ let replace_tac ~what ~with_what ~status:((proof, goal) as status) = try if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what)) then - let equality = - match CicTypeChecker.type_of_aux' metasenv context wty with - C.Sort C.Set -> "cic:/Coq/Init/Logic/eq.ind" - | C.Sort C.Type - | C.Sort C.CProp - | C.Sort C.Prop -> "cic:/Coq/Init/Logic_Type/eqT.ind" - | _ -> assert false - in T.thens ~start:( P.cut_tac (C.Appl [ - (C.MutInd ((U.uri_of_string equality), 0, [])) ; + (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ; wty ; what ; with_what])) @@ -204,13 +181,9 @@ let symmetry_tac ~status:(proof, goal) = let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> - PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", [])) - - | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri HelmLibraryObjects.Logic.eq_URI) -> PrimitiveTactics.apply_tac ~status:(proof,goal) - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", [])) + ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, [])) | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") ;; @@ -224,22 +197,14 @@ let transitivity_tac ~term ~status:((proof, goal) as status) = let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with - (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = HelmLibraryObjects.Logic.eq_URI) -> T.thens ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", []))) + ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, []))) ~continuations: [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac] ~status - | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> - T.thens - ~start:(PrimitiveTactics.apply_tac - ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", []))) - ~continuations: - [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term] - ~status - | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") ;; diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index eeda7a862..7a003dd7b 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -54,35 +54,35 @@ qui est z (** - The type for linear combinations + The type for linear combinations *) -type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational} +type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational} ;; (** - @return an empty flin + @return an empty flin *) let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0} ;; (** - @param f a flin - @param x a Cic.term - @return the rational associated with x (coefficient) + @param f a flin + @param x a Cic.term + @return the rational associated with x (coefficient) *) let flin_coef f x = - try - (Hashtbl.find f.fhom x) - with - _ -> r0 + try + (Hashtbl.find f.fhom x) + with + _ -> r0 ;; - + (** - Adds c to the coefficient of x - @param f a flin - @param x a Cic.term - @param c a rational - @return the new flin + Adds c to the coefficient of x + @param f a flin + @param x a Cic.term + @param c a rational + @return the new flin *) let flin_add f x c = match x with @@ -98,10 +98,10 @@ let flin_add f x c = f ;; (** - Adds c to f.fcste - @param f a flin - @param c a rational - @return the new flin + Adds c to f.fcste + @param f a flin + @param c a rational + @return the new flin *) let flin_add_cste f c = {fhom=f.fhom; @@ -109,12 +109,12 @@ let flin_add_cste f c = ;; (** - @return a empty flin with r1 in fcste + @return a empty flin with r1 in fcste *) let flin_one () = flin_add_cste (flin_zero()) r1;; (** - Adds two flin + Adds two flin *) let flin_plus f1 f2 = let f3 = flin_zero() in @@ -124,7 +124,7 @@ let flin_plus f1 f2 = ;; (** - Substracts two flin + Substracts two flin *) let flin_minus f1 f2 = let f3 = flin_zero() in @@ -134,7 +134,7 @@ let flin_minus f1 f2 = ;; (** - @return a times f + @return a times f *) let flin_emult a f = let f2 = flin_zero() in @@ -147,46 +147,44 @@ let flin_emult a f = (** - @param t a term - @raise Failure if conversion is impossible - @return rational proiection of t + @param t a term + @raise Failure if conversion is impossible + @return rational proiection of t *) let rec rational_of_term t = (* fun to apply f to the first and second rational-term of l *) let rat_of_binop f l = - let a = List.hd l and - b = List.hd(List.tl l) in - f (rational_of_term a) (rational_of_term b) + let a = List.hd l and + b = List.hd(List.tl l) in + f (rational_of_term a) (rational_of_term b) in (* as before, but f is unary *) let rat_of_unop f l = - f (rational_of_term (List.hd l)) + f (rational_of_term (List.hd l)) in match t with | Cic.Cast (t1,t2) -> (rational_of_term t1) | Cic.Appl (t1::next) -> (match t1 with Cic.Const (u,boh) -> - (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> - rat_of_unop rop next - |"cic:/Coq/Reals/Rdefinitions/Rinv.con" -> + if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then + rat_of_unop rop next + else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then rat_of_unop rinv next - |"cic:/Coq/Reals/Rdefinitions/Rmult.con" -> + else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then rat_of_binop rmult next - |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" -> + else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then rat_of_binop rdiv next - |"cic:/Coq/Reals/Rdefinitions/Rplus.con" -> + else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then rat_of_binop rplus next - |"cic:/Coq/Reals/Rdefinitions/Rminus.con" -> + else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then rat_of_binop rminus next - | _ -> failwith "not a rational") + else failwith "not a rational" | _ -> failwith "not a rational") | Cic.Const (u,boh) -> - (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1 - |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0 - | _ -> failwith "not a rational") + if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then r1 + else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then r0 + else failwith "not a rational" | _ -> failwith "not a rational" ;; @@ -202,110 +200,108 @@ let fails f a = ;; let rec flin_of_term t = - let fl_of_binop f l = - let a = List.hd l and - b = List.hd(List.tl l) in - f (flin_of_term a) (flin_of_term b) - in + let fl_of_binop f l = + let a = List.hd l and + b = List.hd(List.tl l) in + f (flin_of_term a) (flin_of_term b) + in try( match t with | Cic.Cast (t1,t2) -> (flin_of_term t1) | Cic.Appl (t1::next) -> - begin - match t1 with + begin + match t1 with Cic.Const (u,boh) -> begin - match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> + if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then flin_emult (rop r1) (flin_of_term (List.hd next)) - |"cic:/Coq/Reals/Rdefinitions/Rplus.con"-> + else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then fl_of_binop flin_plus next - |"cic:/Coq/Reals/Rdefinitions/Rminus.con"-> + else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then fl_of_binop flin_minus next - |"cic:/Coq/Reals/Rdefinitions/Rmult.con"-> - begin - let arg1 = (List.hd next) and - arg2 = (List.hd(List.tl next)) - in - if fails rational_of_term arg1 - then - if fails rational_of_term arg2 - then - ( (* prodotto tra 2 incognite ????? impossibile*) - failwith "Sistemi lineari!!!!\n" - ) - else - ( - match arg1 with - Cic.Rel(n) -> (*trasformo al volo*) - (flin_add (flin_zero()) arg1 (rational_of_term arg2)) - |_-> (* test this *) - let tmp = flin_of_term arg1 in - flin_emult (rational_of_term arg2) (tmp) - ) - else - if fails rational_of_term arg2 - then - ( - match arg2 with - Cic.Rel(n) -> (*trasformo al volo*) - (flin_add (flin_zero()) arg2 (rational_of_term arg1)) - |_-> (* test this *) - let tmp = flin_of_term arg2 in - flin_emult (rational_of_term arg1) (tmp) - - ) - else - ( (*prodotto tra razionali*) - (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2))) - ) - (*try - begin - (*let a = rational_of_term arg1 in - debug("ho fatto rational of term di "^CicPp.ppterm arg1^ - " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*) - let a = flin_of_term arg1 - try - begin - let b = (rational_of_term arg2) in - debug("ho fatto rational of term di "^CicPp.ppterm arg2^ - " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n"); - (flin_add_cste (flin_zero()) (rmult a b)) - end - with - _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n"); - (flin_add (flin_zero()) arg2 a) - end - with - _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n"); - (flin_add(flin_zero()) arg1 (rational_of_term arg2)) - *) - end - |"cic:/Coq/Reals/Rdefinitions/Rinv.con"-> - let a=(rational_of_term (List.hd next)) in - flin_add_cste (flin_zero()) (rinv a) - |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"-> - begin - let b=(rational_of_term (List.hd(List.tl next))) in - try - begin - let a = (rational_of_term (List.hd next)) in - (flin_add_cste (flin_zero()) (rdiv a b)) - end - with - _-> (flin_add (flin_zero()) (List.hd next) (rinv b)) - end - |_->assert false - end - |_ -> assert false - end + else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then + begin + let arg1 = (List.hd next) and + arg2 = (List.hd(List.tl next)) + in + if fails rational_of_term arg1 + then + if fails rational_of_term arg2 + then + ( (* prodotto tra 2 incognite ????? impossibile*) + failwith "Sistemi lineari!!!!\n" + ) + else + ( + match arg1 with + Cic.Rel(n) -> (*trasformo al volo*) + (flin_add (flin_zero()) arg1 (rational_of_term arg2)) + |_-> (* test this *) + let tmp = flin_of_term arg1 in + flin_emult (rational_of_term arg2) (tmp) + ) + else + if fails rational_of_term arg2 + then + ( + match arg2 with + Cic.Rel(n) -> (*trasformo al volo*) + (flin_add (flin_zero()) arg2 (rational_of_term arg1)) + |_-> (* test this *) + let tmp = flin_of_term arg2 in + flin_emult (rational_of_term arg1) (tmp) + + ) + else + ( (*prodotto tra razionali*) + (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2))) + ) + (*try + begin + (*let a = rational_of_term arg1 in + debug("ho fatto rational of term di "^CicPp.ppterm arg1^ + " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*) + let a = flin_of_term arg1 + try + begin + let b = (rational_of_term arg2) in + debug("ho fatto rational of term di "^CicPp.ppterm arg2^ + " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n"); + (flin_add_cste (flin_zero()) (rmult a b)) + end + with + _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n"); + (flin_add (flin_zero()) arg2 a) + end + with + _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n"); + (flin_add(flin_zero()) arg1 (rational_of_term arg2)) + *) + end + else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then + let a=(rational_of_term (List.hd next)) in + flin_add_cste (flin_zero()) (rinv a) + else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then + begin + let b=(rational_of_term (List.hd(List.tl next))) in + try + begin + let a = (rational_of_term (List.hd next)) in + (flin_add_cste (flin_zero()) (rdiv a b)) + end + with + _-> (flin_add (flin_zero()) (List.hd next) (rinv b)) + end + else assert false + end + |_ -> assert false + end | Cic.Const (u,boh) -> begin - match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one () - |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero () - |_-> assert false - end + if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then flin_one () + else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then flin_zero () + else assert false + end |_-> assert false) with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1 ;; @@ -315,9 +311,9 @@ let flin_of_constr = flin_of_term;; *) (** - Translates a flin to (c,x) list - @param f a flin - @return something like (c1,x1)::(c2,x2)::...::(cn,xn) + Translates a flin to (c,x) list + @param f a flin + @return something like (c1,x1)::(c2,x2)::...::(cn,xn) *) let flin_to_alist f = let res=ref [] in @@ -329,7 +325,7 @@ let flin_to_alist f = *) (** - The structure for ineq + The structure for ineq *) type hineq={hname:Cic.term; (* le nom de l'hypothèse *) htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) @@ -349,67 +345,64 @@ let ineq1_of_term (h,t) = let arg2= List.hd(List.tl next) in (match t1 with (* match t1 *) Cic.Const (u,boh) -> - (match UriManager.string_of_uri u with (* match u *) - "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> - [{hname=h; + if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then + [{hname=h; htype="Rlt"; - hleft=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) (flin_of_term arg2); - hstrict=true}] - |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> - [{hname=h; + hstrict=true}] + else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then + [{hname=h; htype="Rgt"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) (flin_of_term arg1); - hstrict=true}] - |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> + hstrict=true}] + else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then [{hname=h; htype="Rle"; - hleft=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) (flin_of_term arg2); - hstrict=false}] - |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> + hstrict=false}] + else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then [{hname=h; htype="Rge"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) (flin_of_term arg1); - hstrict=false}] - |_->assert false)(* match u *) + hstrict=false}] + else assert false | Cic.MutInd (u,i,o) -> - (match UriManager.string_of_uri u with - "cic:/Coq/Init/Logic_Type/eqT.ind" -> - let t0= arg1 in + if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then + let t0= arg1 in let arg1= arg2 in let arg2= List.hd(List.tl (List.tl next)) in - (match t0 with + (match t0 with Cic.Const (u,boh) -> - (match UriManager.string_of_uri u with - "cic:/Coq/Reals/Rdefinitions/R.con"-> + if UriManager.eq u HelmLibraryObjects.Reals.r_URI then [{hname=h; htype="eqTLR"; - hleft=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) (flin_of_term arg2); - hstrict=false}; + hstrict=false}; {hname=h; htype="eqTRL"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) (flin_of_term arg1); - hstrict=false}] - |_-> assert false) - |_-> assert false) - |_-> assert false) + hstrict=false}] + else assert false + |_-> assert false) + else assert false |_-> assert false)(* match t1 *) |_-> assert false (* match t *) ;; @@ -430,12 +423,12 @@ let rec print_sys l = match l with [] -> () | (a,b)::next -> (print_rl a; - print_string (if b=true then "strict\n"else"\n"); - print_sys next) + print_string (if b=true then "strict\n"else"\n"); + print_sys next) ;; (*let print_hash h = - Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h + Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h ;;*) let fourier_lineq lineq1 = @@ -443,12 +436,12 @@ let fourier_lineq lineq1 = let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *) List.iter (fun f -> Hashtbl.iter (fun x c -> - try (Hashtbl.find hvar x;()) - with _-> nvar:=(!nvar)+1; - Hashtbl.add hvar x (!nvar); - debug("aggiungo una var "^ - string_of_int !nvar^" per "^ - CicPp.ppterm x^"\n")) + try (Hashtbl.find hvar x;()) + with _-> nvar:=(!nvar)+1; + Hashtbl.add hvar x (!nvar); + debug("aggiungo una var "^ + string_of_int !nvar^" per "^ + CicPp.ppterm x^"\n")) f.hflin.fhom) lineq1; (*print_hash hvar;*) @@ -471,25 +464,19 @@ i.e. on obtient une contradiction. *) -let _eqT = Cic.MutInd((UriManager.uri_of_string - "cic:/Coq/Init/Logic_Type/eqT.ind"), 0, []) ;; -let _False = Cic.MutInd ((UriManager.uri_of_string - "cic:/Coq/Init/Logic/False.ind"), 0, []) ;; -let _not = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Init/Logic/not.con"), []);; -let _R0 = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/R0.con"), []) ;; -let _R1 = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/R1.con"), []) ;; -let _R = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/R.con"), []) ;; +let _eqT = Cic.MutInd(HelmLibraryObjects.Logic.eq_URI, 0, []) ;; +let _False = Cic.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []) ;; +let _not = Cic.Const (HelmLibraryObjects.Logic.not_URI,[]);; +let _R0 = Cic.Const (HelmLibraryObjects.Reals.r0_URI,[]);; +let _R1 = Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);; +let _R = Cic.Const (HelmLibraryObjects.Reals.r_URI,[]);; let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;; let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;; let _Rfourier_ge_to_le =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;; -let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string +let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;; let _Rfourier_le=Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;; @@ -511,12 +498,9 @@ let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;; let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;; -let _Rinv = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rinv.con"), []) ;; -let _Rinv_R1 = Cic.Const((UriManager.uri_of_string - "cic:/Coq/Reals/Rbase/Rinv_R1.con" ), []) ;; -let _Rle = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rle.con"), []) ;; +let _Rinv = Cic.Const (HelmLibraryObjects.Reals.rinv_URI, []);; +let _Rinv_R1 = Cic.Const(HelmLibraryObjects.Reals.rinv_r1_URI, []);; +let _Rle = Cic.Const (HelmLibraryObjects.Reals.rle_URI, []);; let _Rle_mult_inv_pos = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;; let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string @@ -525,10 +509,7 @@ let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;; let _Rle_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;; -(*let _Rle_zero_zero = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con"), []) ;;*) -let _Rlt = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rlt.con"), []) ;; +let _Rlt = Cic.Const (HelmLibraryObjects.Reals.rlt_URI, []);; let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;; let _Rlt_not_le = Cic.Const ((UriManager.uri_of_string @@ -537,20 +518,16 @@ let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;; let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;; -let _Rminus = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rminus.con"), []) ;; -let _Rmult = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rmult.con"), []) ;; +let _Rminus = Cic.Const (HelmLibraryObjects.Reals.rminus_URI, []);; +let _Rmult = Cic.Const (HelmLibraryObjects.Reals.rmult_URI, []);; let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;; let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;; let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;; -let _Ropp = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Ropp.con"), []) ;; -let _Rplus = Cic.Const ((UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rplus.con"), []) ;; +let _Ropp = Cic.Const (HelmLibraryObjects.Reals.ropp_URI, []);; +let _Rplus = Cic.Const (HelmLibraryObjects.Reals.rplus_URI, []);; (******************************************************************************) @@ -569,15 +546,15 @@ let rec int_to_real_aux n = 0 -> _R0 (* o forse R0 + R0 ????? *) | 1 -> _R1 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ] -;; - +;; + let int_to_real n = let x = int_to_real_aux (abs n) in if n < 0 then - Cic.Appl [ _Ropp ; x ] + Cic.Appl [ _Ropp ; x ] else - x + x ;; @@ -612,13 +589,13 @@ let tac_zero_inf_pos (n,d) ~status = for i=1 to n-1 do tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) ~status _Rlt_zero_pos_plus1; - PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) - ~continuation:!tacn); + PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) + ~continuation:!tacn); done; for i=1 to d-1 do tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac - ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); + ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); done; @@ -723,7 +700,7 @@ let r = ) ~continuation: (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos (-n,d))) ~status in + ~continuation:(tac_zero_inf_pos (-n,d))) ~status in debug("end tac_zero_infeq_false\n"); r (*PORTING @@ -794,7 +771,7 @@ match h.htype with |"Rle" -> exact ~term:h.hname ~status |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) - ~continuation:(exact ~term:h.hname)) ~status + ~continuation:(exact ~term:h.hname)) ~status |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) ~continuation:(exact ~term:h.hname)) ~status @@ -815,18 +792,17 @@ res let is_ineq (h,t) = match t with Cic.Appl ( Cic.Const(u,boh)::next) -> - (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true - |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true - |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true - |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true - |"cic:/Coq/Init/Logic_Type/eqT.con" -> + (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI or + UriManager.eq u HelmLibraryObjects.Reals.rgt_URI or + UriManager.eq u HelmLibraryObjects.Reals.rle_URI or + UriManager.eq u HelmLibraryObjects.Reals.rge_URI then true + else if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then (match (List.hd next) with Cic.Const (uri,_) when - UriManager.string_of_uri uri = - "cic:/Coq/Reals/Rdefinitions/R.con" -> true + UriManager.eq uri HelmLibraryObjects.Reals.r_URI + -> true | _ -> false) - |_->false) + else false) |_->false ;; @@ -844,12 +820,12 @@ let rec strip_outer_cast c = match c with (*let find_in_context id context = let rec find_in_context_aux c n = - match c with - [] -> failwith (id^" not found in context") - | a::next -> (match a with - Some (Cic.Name(name),_) when name = id -> n - (*? magari al posto di _ qualcosaltro?*) - | _ -> find_in_context_aux next (n+1)) + match c with + [] -> failwith (id^" not found in context") + | a::next -> (match a with + Some (Cic.Name(name),_) when name = id -> n + (*? magari al posto di _ qualcosaltro?*) + | _ -> find_in_context_aux next (n+1)) in find_in_context_aux context 1 ;; @@ -859,9 +835,9 @@ let rec filter_real_hyp context cont = match context with [] -> [] | Some(Cic.Name(h),Cic.Decl(t))::next -> ( - let n = find_in_context h cont in - debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n"); - [(Cic.Rel(n),t)] @ filter_real_hyp next cont) + let n = find_in_context h cont in + debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n"); + [(Cic.Rel(n),t)] @ filter_real_hyp next cont) | a::next -> debug(" no\n"); filter_real_hyp next cont ;;*) let filter_real_hyp context _ = @@ -869,18 +845,18 @@ let filter_real_hyp context _ = match context with [] -> [] | Some(Cic.Name(h),Cic.Decl(t))::next -> - ( - (*let n = find_in_context h cont in*) - debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n"); - [(Cic.Rel(num),t)] @ filter_aux next (num+1) - ) + ( + (*let n = find_in_context h cont in*) + debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n"); + [(Cic.Rel(num),t)] @ filter_aux next (num+1) + ) | a::next -> filter_aux next (num+1) in filter_aux context 1 ;; -(* lifts everithing at the conclusion level *) +(* lifts everithing at the conclusion level *) let rec superlift c n= match c with [] -> [] @@ -917,9 +893,9 @@ debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " ;; let tcl_fail a ~status:(proof,goal) = - match a with - 1 -> raise (ProofEngineTypes.Fail "fail-tactical") - |_-> (proof,[goal]) + match a with + 1 -> raise (ProofEngineTypes.Fail "fail-tactical") + |_-> (proof,[goal]) ;; (* Galla: moved in variousTactics.ml @@ -928,12 +904,12 @@ let assumption_tac ~status:(proof,goal)= let metano,context,ty = CicUtil.lookup_meta goal metasenv in let num = ref 0 in let tac_list = List.map - ( fun x -> num := !num + 1; - match x with - Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) - | _ -> ("fake",tcl_fail 1) - ) - context + ( fun x -> num := !num + 1; + match x with + Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) + | _ -> ("fake",tcl_fail 1) + ) + context in Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) ;; @@ -941,13 +917,13 @@ let assumption_tac ~status:(proof,goal)= (* Galla: moved in negationTactics.ml (* !!!!! fix !!!!!!!!!! *) let contradiction_tac ~status:(proof,goal)= - Tacticals.then_ + Tacticals.then_ (*inutile sia questo che quello prima della chiamata*) - ~start:PrimitiveTactics.intros_tac - ~continuation:(Tacticals.then_ - ~start:(VariousTactics.elim_type_tac ~term:_False) - ~continuation:(assumption_tac)) - ~status:(proof,goal) + ~start:PrimitiveTactics.intros_tac + ~continuation:(Tacticals.then_ + ~start:(VariousTactics.elim_type_tac ~term:_False) + ~continuation:(assumption_tac)) + ~status:(proof,goal) ;; *) @@ -967,16 +943,16 @@ theoreme,so let's parse our thesis *) let th_to_appl = ref _Rfourier_not_le_gt in (match s_ty with Cic.Appl ( Cic.Const(u,boh)::args) -> - (match UriManager.string_of_uri u with - "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := - _Rfourier_not_ge_lt - |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := + th_to_appl := + (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then + _Rfourier_not_ge_lt + else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then _Rfourier_not_gt_le - |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := + else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then _Rfourier_not_le_gt - |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := + else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then _Rfourier_not_lt_ge - |_-> failwith "fourier can't be applyed") + else failwith "fourier can't be applyed") |_-> failwith "fourier can't be applyed"); (* fix maybe strip_outer_cast goes here?? *) @@ -1016,18 +992,18 @@ theoreme,so let's parse our thesis *) (* transform hyps into inequations *) List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) - with _-> ()) + with _-> ()) hyps; - + debug ("applico fourier a "^ string_of_int (List.length !lineq)^ " disequazioni\n"); let res=fourier_lineq (!lineq) in let tac=ref Tacticals.id_tac in if res=[] then - (print_string "Tactic Fourier fails.\n";flush stdout; - failwith "fourier_tac fails") + (print_string "Tactic Fourier fails.\n";flush stdout; + failwith "fourier_tac fails") else ( match res with (*match res*) @@ -1042,33 +1018,33 @@ theoreme,so let's parse our thesis *) let lutil=ref [] in List.iter (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil); - (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *)) - ) + (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *)) + ) (List.combine (!lineq) lc); - + print_string (" quindi lutil e' lunga "^ - string_of_int (List.length (!lutil))^"\n"); + string_of_int (List.length (!lutil))^"\n"); (* on construit la combinaison linéaire des inéquation *) (match (!lutil) with (*match (!lutil) *) (h1,c1)::lutil -> debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n"; - + let s=ref (h1.hstrict) in - + let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in List.iter (fun (h,c) -> - s:=(!s)||(h.hstrict); - t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl - [_Rmult;rational_to_real c;h.hleft ] ]); - t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl - [_Rmult;rational_to_real c;h.hright] ])) + s:=(!s)||(h.hstrict); + t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl + [_Rmult;rational_to_real c;h.hleft ] ]); + t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl + [_Rmult;rational_to_real c;h.hright] ])) lutil; - + let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in let tc=rational_to_real cres in @@ -1077,142 +1053,142 @@ theoreme,so let's parse our thesis *) debug "inizio a costruire tac1\n"; Fourier.print_rational(c1); - + let tac1=ref ( fun ~status -> - if h1.hstrict then - (Tacticals.thens - ~start:( - fun ~status -> - debug ("inizio t1 strict\n"); - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); - debug ("ty = "^ CicPp.ppterm ty^"\n"); + if h1.hstrict then + (Tacticals.thens + ~start:( + fun ~status -> + debug ("inizio t1 strict\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] - ~status - ) + ~status + ) else - (Tacticals.thens - ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) + (Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) ~continuations:[tac_use h1;tac_zero_inf_pos - (rational_to_fraction c1)] ~status - ) - ) - + (rational_to_fraction c1)] ~status + ) + ) + in s:=h1.hstrict; List.iter (fun (h,c) -> (if (!s) then - (if h.hstrict then - (debug("tac1 1\n"); - tac1:=(Tacticals.thens - ~start:(PrimitiveTactics.apply_tac - ~term:_Rfourier_lt_lt) - ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) - ) - else - (debug("tac1 2\n"); - Fourier.print_rational(c1); - tac1:=(Tacticals.thens - ~start:( - fun ~status -> - debug("INIZIO TAC 1 2\n"); - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); - debug ("ty = "^ CicPp.ppterm ty^"\n"); + (if h.hstrict then + (debug("tac1 1\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_lt_lt) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + else + (debug("tac1 2\n"); + Fourier.print_rational(c1); + tac1:=(Tacticals.thens + ~start:( + fun ~status -> + debug("INIZIO TAC 1 2\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status) - ~continuations:[!tac1;tac_use h;tac_zero_inf_pos - (rational_to_fraction c)]) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) ) ) - else + else (if h.hstrict then - (debug("tac1 3\n"); - tac1:=(Tacticals.thens - ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) - ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (debug("tac1 3\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos (rational_to_fraction c)]) - ) - else - (debug("tac1 4\n"); - tac1:=(Tacticals.thens - ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) - ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + ) + else + (debug("tac1 4\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos (rational_to_fraction c)]) - ) + ) ) - ); - s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) - + ); + s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) + let tac2 = if sres then - tac_zero_inf_false goal (rational_to_fraction cres) + tac_zero_inf_false goal (rational_to_fraction cres) else - tac_zero_infeq_false goal (rational_to_fraction cres) + tac_zero_infeq_false goal (rational_to_fraction cres) in tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ - ~start:(fun ~status:(proof,goal as status) -> + ~start:(fun ~status:(proof,goal as status) -> let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in PrimitiveTactics.change_tac ~what:ty - ~with_what:(Cic.Appl [ _not; ineq]) ~status) - ~continuation:(Tacticals.then_ + ~with_what:(Cic.Appl [ _not; ineq]) ~status) + ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term: - (if sres then _Rnot_lt_lt else _Rnot_le_le)) - ~continuation:(Tacticals.thens - ~start:( - fun ~status -> - debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); - let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc - ~status - in - (match r with (p,gl) -> - debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); + (if sres then _Rnot_lt_lt else _Rnot_le_le)) + ~continuation:(Tacticals.thens + ~start:( + fun ~status -> + debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); + let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc + ~status + in + (match r with (p,gl) -> + debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); r) - ~continuations:[(Tacticals.thens - ~start:( - fun ~status -> - let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in - (match r with (p,gl) -> - debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); - r) - ~continuations: + ~continuations:[(Tacticals.thens + ~start:( + fun ~status -> + let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in + (match r with (p,gl) -> + debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations: [PrimitiveTactics.apply_tac ~term:_Rinv_R1 - ;Tacticals.try_tactics - ~tactics:[ "ring", (fun ~status -> - debug("begin RING\n"); - let r = Ring.ring_tac ~status in - debug ("end RING\n"); - r) - ; "id", Tacticals.id_tac] - ]) - ;(*Tacticals.id_tac*) - Tacticals.then_ - ~start: - ( - fun ~status:(proof,goal as status) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - (* check if ty is of type *) - let w1 = - debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); - (match ty with - Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) - |_ -> assert false) - in - let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in - debug("fine MY_CHNGE\n"); - r - - ) - ~continuation:(*PORTINGTacticals.id_tac*)tac2])) - ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) + ;Tacticals.try_tactics + ~tactics:[ "ring", (fun ~status -> + debug("begin RING\n"); + let r = Ring.ring_tac ~status in + debug ("end RING\n"); + r) + ; "id", Tacticals.id_tac] + ]) + ;(*Tacticals.id_tac*) + Tacticals.then_ + ~start: + ( + fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + (* check if ty is of type *) + let w1 = + debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); + (match ty with + Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) + |_ -> assert false) + in + let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in + debug("fine MY_CHNGE\n"); + r + + ) + ~continuation:(*PORTINGTacticals.id_tac*)tac2])) + ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*) diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index 12848ad26..fc21ec405 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -32,7 +32,7 @@ let absurd_tac ~term ~status:((proof,goal) as status) = let _,context,ty = CicUtil.lookup_meta goal metasenv in if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *) then P.apply_tac - ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status + ~term:(C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; term ; ty]) ~status else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition") ;; @@ -50,7 +50,7 @@ let contradiction_tac ~status = ~start: (EliminationTactics.elim_type_tac ~term: - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"), 0, []))) + (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []))) ~continuation: VariousTactics.assumption_tac) ~status with diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly index f6f557947..3ca69d5c6 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly @@ -184,20 +184,13 @@ expr2: { [], function interp -> let rec cic_real_of_real = function - 0 -> - Cic.Const - (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/R0.con",[]) - | 1 -> - Cic.Const - (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con",[]) + 0 -> Cic.Const (HelmLibraryObjects.Reals.r0_URI, []) + | 1 -> Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]) | n -> Cic.Appl [ Cic.Const - (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ; - Cic.Const (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/R1.con",[]); + (HelmLibraryObjects.Reals.rplus_URI,[]) ; + Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]); cic_real_of_real (n - 1) ] in @@ -208,14 +201,10 @@ expr2: let rec cic_int_of_int = function 0 -> - Cic.MutConstruct - (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", - 0,1,[]) + Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,1,[]) | n -> Cic.Appl - [ Cic.MutConstruct - (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", - 0,2,[]) ; + [ Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,2,[]) ; cic_int_of_int (n - 1) ] in @@ -227,9 +216,7 @@ expr2: let dom = union dom1 dom2 in dom, function interp -> Cic.Appl - [Cic.Const - (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ; + [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ; (mk_expr1 interp) ; (mk_expr2 interp) ] @@ -240,9 +227,7 @@ expr2: let dom = union dom1 dom2 in dom, function interp -> Cic.Appl - [Cic.Const - (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rminus.con",[]) ; + [Cic.Const (HelmLibraryObjects.Reals.rminus_URI,[]); (mk_expr1 interp) ; (mk_expr2 interp) ] @@ -253,9 +238,7 @@ expr2: let dom = union dom1 dom2 in dom, function interp -> Cic.Appl - [Cic.Const - (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rmult.con",[]) ; + [Cic.Const (HelmLibraryObjects.Reals.rmult_URI,[]) ; (mk_expr1 interp) ; (mk_expr2 interp) ] @@ -266,9 +249,7 @@ expr2: let dom = union dom1 dom2 in dom, function interp -> Cic.Appl - [Cic.Const - (UriManager.uri_of_string - "cic:/Coq/Reals/Rdefinitions/Rdiv.con",[]) ; + [Cic.Const (HelmLibraryObjects.Reals.rdiv_URI,[]) ; (mk_expr1 interp) ; (mk_expr2 interp) ] @@ -279,8 +260,7 @@ expr2: let dom = union dom1 dom2 in dom, function interp -> Cic.Appl - [Cic.Const - (UriManager.uri_of_string "cic:/Coq/Init/Peano/plus.con",[]) ; + [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ; (mk_expr1 interp) ; (mk_expr2 interp) ] @@ -291,8 +271,7 @@ expr2: let dom = union dom1 dom2 in dom, function interp -> Cic.Appl - [Cic.Const - (UriManager.uri_of_string "cic:/Coq/Arith/Minus/minus.con",[]) ; + [Cic.Const (HelmLibraryObjects.Peano.minus_URI,[]) ; (mk_expr1 interp) ; (mk_expr2 interp) ] @@ -303,42 +282,11 @@ expr2: let dom = union dom1 dom2 in dom, function interp -> Cic.Appl - [Cic.Const - (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ] - } - | expr2 EQT expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom3,mk_expr3 = mk_implicit () in - let dom = union dom1 (union dom2 dom3) in - dom, function interp -> - Cic.Appl - [Cic.MutInd - (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ; - (mk_expr3 interp) ; + [Cic.Const (HelmLibraryObjects.Peano.mult_URI,[]) ; (mk_expr1 interp) ; (mk_expr2 interp) ] } - | expr2 NEQT expr2 - { let dom1,mk_expr1 = $1 in - let dom2,mk_expr2 = $3 in - let dom3,mk_expr3 = mk_implicit () in - let dom = union dom1 (union dom2 dom3) in - dom, function interp -> - Cic.Appl [ - Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con",[]); - Cic.Appl - [Cic.MutInd - (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ; - (mk_expr3 interp) ; - (mk_expr1 interp) ; - (mk_expr2 interp) - ]] - } | expr2 EQ expr2 { let dom1,mk_expr1 = $1 in let dom2,mk_expr2 = $3 in @@ -346,8 +294,7 @@ expr2: let dom = union dom1 (union dom2 dom3) in dom, function interp -> Cic.Appl - [Cic.MutInd - (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind",0,[]) ; + [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI,0,[]) ; (mk_expr3 interp) ; (mk_expr1 interp) ; (mk_expr2 interp) -- 2.39.2