From 7288b45eacf9f7dcd118b3b89b81ff19ae9d6ce5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 7 Oct 2009 09:43:18 +0000 Subject: [PATCH] - oCic2NCic and nCic2OCic moved to ng_library - spurious dependencies of ng_library on modules that need to convert old tables added; to be removed in the future --- .../components/METAS/meta.helm-ng_library.src | 2 +- helm/software/components/Makefile | 16 +++++++--------- .../components/binaries/transcript/.depend | 5 +++++ .../components/ng_cic_content/ncic2astMatcher.ml | 5 ++++- .../ng_cic_content/ncic2astMatcher.mli | 2 ++ .../ng_disambiguation/nCicDisambiguate.ml | 5 ++++- .../ng_disambiguation/nCicDisambiguate.mli | 2 ++ helm/software/components/ng_kernel/.depend | 9 +-------- helm/software/components/ng_kernel/.depend.opt | 8 -------- helm/software/components/ng_kernel/Makefile | 2 -- helm/software/components/ng_library/.depend | 11 +++++++++-- helm/software/components/ng_library/.depend.opt | 10 ++++++++-- helm/software/components/ng_library/Makefile | 2 ++ .../{ng_kernel => ng_library}/nCic2OCic.ml | 0 .../{ng_kernel => ng_library}/nCic2OCic.mli | 0 .../{ng_kernel => ng_library}/oCic2NCic.ml | 6 ++++++ .../{ng_kernel => ng_library}/oCic2NCic.mli | 0 .../components/ng_paramodulation/nCicBlob.ml | 5 ++++- .../components/ng_paramodulation/nCicBlob.mli | 2 ++ .../components/ng_paramodulation/nCicProof.ml | 12 ++++++++---- .../components/ng_paramodulation/nCicProof.mli | 5 ++--- .../components/ng_refiner/nCicCoercion.ml | 5 ++++- .../components/ng_refiner/nCicCoercion.mli | 3 +++ .../components/ng_refiner/nCicUnifHint.ml | 2 ++ .../components/syntax_extensions/.depend | 3 +++ 25 files changed, 79 insertions(+), 43 deletions(-) rename helm/software/components/{ng_kernel => ng_library}/nCic2OCic.ml (100%) rename helm/software/components/{ng_kernel => ng_library}/nCic2OCic.mli (100%) rename helm/software/components/{ng_kernel => ng_library}/oCic2NCic.ml (99%) rename helm/software/components/{ng_kernel => ng_library}/oCic2NCic.mli (100%) diff --git a/helm/software/components/METAS/meta.helm-ng_library.src b/helm/software/components/METAS/meta.helm-ng_library.src index 94402278d..ebe2e340e 100644 --- a/helm/software/components/METAS/meta.helm-ng_library.src +++ b/helm/software/components/METAS/meta.helm-ng_library.src @@ -1,4 +1,4 @@ -requires="helm-ng_refiner" +requires="helm-ng_refiner helm-ng_cic_content helm-ng_disambiguation helm-ng_paramodulation" version="0.0.1" archive(byte)="ng_library.cma" archive(native)="ng_library.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index e12688b64..02125883f 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -26,23 +26,21 @@ MODULES = \ ng_kernel \ acic_content \ grafite \ - ng_refiner \ - ng_library \ - ng_cic_content \ - content_pres \ cic_unification \ whelp \ tactics \ acic_procedural \ - disambiguation \ + disambiguation \ cic_disambiguation \ - lexicon \ - ng_disambiguation \ - ng_paramodulation \ - tptp_grafite \ ng_kernel \ ng_refiner \ + ng_disambiguation \ + ng_cic_content \ + ng_paramodulation \ ng_library \ + content_pres \ + lexicon \ + tptp_grafite \ grafite_parser \ ng_tactics \ grafite_engine \ diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index bb6f22a64..87d1ed25c 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/ng_cic_content/ncic2astMatcher.ml b/helm/software/components/ng_cic_content/ncic2astMatcher.ml index 41d9aa08c..2245e3429 100644 --- a/helm/software/components/ng_cic_content/ncic2astMatcher.ml +++ b/helm/software/components/ng_cic_content/ncic2astMatcher.ml @@ -28,6 +28,9 @@ module Ast = CicNotationPt module Util = CicNotationUtil +let reference_of_oxuri = ref (fun _ -> assert false);; +let set_reference_of_oxuri f = reference_of_oxuri := f;; + module Matcher32 = struct module Pattern32 = @@ -49,7 +52,7 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Ast.UriPattern uri -> NRef (OCic2NCic.reference_of_oxuri uri), [] + | Ast.UriPattern uri -> NRef (!reference_of_oxuri uri), [] | Ast.NRefPattern nref -> NRef nref, [] | Ast.ImplicitPattern | Ast.VarPattern _ -> Blob, [] diff --git a/helm/software/components/ng_cic_content/ncic2astMatcher.mli b/helm/software/components/ng_cic_content/ncic2astMatcher.mli index 14e59e002..6205f8522 100644 --- a/helm/software/components/ng_cic_content/ncic2astMatcher.mli +++ b/helm/software/components/ng_cic_content/ncic2astMatcher.mli @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit + module Matcher32: sig (** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 1e88c3714..d50eec796 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -22,6 +22,9 @@ module NRef = NReference let debug_print s = prerr_endline (Lazy.force s);; let debug_print _ = ();; +let reference_of_oxuri = ref (fun _ -> assert false);; +let set_reference_of_oxuri f = reference_of_oxuri := f;; + let cic_name_of_name = function | Ast.Ident (n, None) -> n | _ -> assert false @@ -325,7 +328,7 @@ let interpretate_term_and_interpretate_term_option | CicNotationPt.Uri (uri, subst) -> assert (subst = None); (try - NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri)) + NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri)) with NRef.IllFormedReference _ -> CicNotationPt.fail loc "Ill formed reference") | CicNotationPt.NRef nref -> NCic.Const nref diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index b86849f35..a9f15244c 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -11,6 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit + val disambiguate_term : context:NCic.context -> metasenv:NCic.metasenv -> diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index fa6e42064..9a4ae3fc1 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,8 +1,7 @@ +nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo -oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmo -nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo nCicPp.cmi: nUri.cmi nReference.cmi nCic.cmo nCicReduction.cmi: nCic.cmo @@ -20,12 +19,6 @@ nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmo \ nCicSubstitution.cmi nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \ nCicSubstitution.cmi -oCic2NCic.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCic.cmo \ - oCic2NCic.cmi -oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ - oCic2NCic.cmi -nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi -nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicEnvironment.cmi \ diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index f50abe93c..d7c542af5 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -2,8 +2,6 @@ nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx -oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmx -nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx nCicPp.cmi: nUri.cmi nReference.cmi nCic.cmx nCicReduction.cmi: nCic.cmx @@ -21,12 +19,6 @@ nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmx \ nCicSubstitution.cmi nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \ nCicSubstitution.cmi -oCic2NCic.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCic.cmx \ - oCic2NCic.cmi -oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ - oCic2NCic.cmi -nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi -nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicEnvironment.cmi \ diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 5b5a48593..3cacb50d1 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -6,8 +6,6 @@ INTERFACE_FILES = \ nReference.mli \ nCicUtils.mli \ nCicSubstitution.mli \ - oCic2NCic.mli \ - nCic2OCic.mli \ nCicEnvironment.mli \ nCicPp.mli \ nCicReduction.mli \ diff --git a/helm/software/components/ng_library/.depend b/helm/software/components/ng_library/.depend index c76001c01..e379b9fc6 100644 --- a/helm/software/components/ng_library/.depend +++ b/helm/software/components/ng_library/.depend @@ -1,2 +1,9 @@ -nCicLibrary.cmo: nCicLibrary.cmi -nCicLibrary.cmx: nCicLibrary.cmi +nCic2OCic.cmi: +oCic2NCic.cmi: +nCicLibrary.cmi: +nCic2OCic.cmo: nCic2OCic.cmi +nCic2OCic.cmx: nCic2OCic.cmi +oCic2NCic.cmo: oCic2NCic.cmi +oCic2NCic.cmx: oCic2NCic.cmi +nCicLibrary.cmo: oCic2NCic.cmi nCic2OCic.cmi nCicLibrary.cmi +nCicLibrary.cmx: oCic2NCic.cmx nCic2OCic.cmx nCicLibrary.cmi diff --git a/helm/software/components/ng_library/.depend.opt b/helm/software/components/ng_library/.depend.opt index 48127a325..e379b9fc6 100644 --- a/helm/software/components/ng_library/.depend.opt +++ b/helm/software/components/ng_library/.depend.opt @@ -1,3 +1,9 @@ +nCic2OCic.cmi: +oCic2NCic.cmi: nCicLibrary.cmi: -nCicLibrary.cmo: nCicLibrary.cmi -nCicLibrary.cmx: nCicLibrary.cmi +nCic2OCic.cmo: nCic2OCic.cmi +nCic2OCic.cmx: nCic2OCic.cmi +oCic2NCic.cmo: oCic2NCic.cmi +oCic2NCic.cmx: oCic2NCic.cmi +nCicLibrary.cmo: oCic2NCic.cmi nCic2OCic.cmi nCicLibrary.cmi +nCicLibrary.cmx: oCic2NCic.cmx nCic2OCic.cmx nCicLibrary.cmi diff --git a/helm/software/components/ng_library/Makefile b/helm/software/components/ng_library/Makefile index ee8fbad13..e5cd7fb1f 100644 --- a/helm/software/components/ng_library/Makefile +++ b/helm/software/components/ng_library/Makefile @@ -2,6 +2,8 @@ PACKAGE = ng_library PREDICATES = INTERFACE_FILES = \ + nCic2OCic.mli \ + oCic2NCic.mli \ nCicLibrary.mli IMPLEMENTATION_FILES = \ diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_library/nCic2OCic.ml similarity index 100% rename from helm/software/components/ng_kernel/nCic2OCic.ml rename to helm/software/components/ng_library/nCic2OCic.ml diff --git a/helm/software/components/ng_kernel/nCic2OCic.mli b/helm/software/components/ng_library/nCic2OCic.mli similarity index 100% rename from helm/software/components/ng_kernel/nCic2OCic.mli rename to helm/software/components/ng_library/nCic2OCic.mli diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_library/oCic2NCic.ml similarity index 99% rename from helm/software/components/ng_kernel/oCic2NCic.ml rename to helm/software/components/ng_library/oCic2NCic.ml index 1487881c1..1cf194a4c 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_library/oCic2NCic.ml @@ -876,3 +876,9 @@ let reference_of_oxuri u = NCic.Const nref, [] -> nref | _,_ -> assert false ;; + +NCicCoercion.set_convert_term convert_term;; +Ncic2astMatcher.set_reference_of_oxuri reference_of_oxuri;; +NCicDisambiguate.set_reference_of_oxuri reference_of_oxuri;; +NCicBlob.set_reference_of_oxuri reference_of_oxuri;; +NCicProof.set_reference_of_oxuri reference_of_oxuri;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_library/oCic2NCic.mli similarity index 100% rename from helm/software/components/ng_kernel/oCic2NCic.mli rename to helm/software/components/ng_library/oCic2NCic.mli diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 91746f210..05867b00e 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -11,6 +11,9 @@ (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *) +let reference_of_oxuri = ref (fun _ -> assert false);; +let set_reference_of_oxuri f = reference_of_oxuri := f;; + module type NCicContext = sig val metasenv : NCic.metasenv @@ -80,7 +83,7 @@ with type t = NCic.term and type input = NCic.term = struct let eqP = let r = - OCic2NCic.reference_of_oxuri + !reference_of_oxuri (UriManager.uri_of_string "cic:/matita/logic/equality/eq.ind#xpointer(1/1)") in diff --git a/helm/software/components/ng_paramodulation/nCicBlob.mli b/helm/software/components/ng_paramodulation/nCicBlob.mli index 16a8c33a2..58f97a3f2 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.mli +++ b/helm/software/components/ng_paramodulation/nCicBlob.mli @@ -11,6 +11,8 @@ (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *) +val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit + module type NCicContext = sig val metasenv : NCic.metasenv diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 9223d1bcb..9a7285062 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -11,9 +11,13 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) +let reference_of_oxuri = ref (fun _ -> assert false);; +let set_reference_of_oxuri f = reference_of_oxuri := f;; + + let eqP () = let r = - OCic2NCic.reference_of_oxuri + !reference_of_oxuri (UriManager.uri_of_string "cic:/matita/logic/equality/eq.ind#xpointer(1/1)") in @@ -22,7 +26,7 @@ let eq_ind () = let r = - OCic2NCic.reference_of_oxuri + !reference_of_oxuri (UriManager.uri_of_string "cic:/matita/logic/equality/eq_ind.con") in @@ -31,7 +35,7 @@ let eq_ind_r () = let r = - OCic2NCic.reference_of_oxuri + !reference_of_oxuri (UriManager.uri_of_string "cic:/matita/logic/equality/eq_elim_r.con") in @@ -40,7 +44,7 @@ let eq_refl () = let r = - OCic2NCic.reference_of_oxuri + !reference_of_oxuri (UriManager.uri_of_string "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)") in diff --git a/helm/software/components/ng_paramodulation/nCicProof.mli b/helm/software/components/ng_paramodulation/nCicProof.mli index 7a1032482..337752edc 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.mli +++ b/helm/software/components/ng_paramodulation/nCicProof.mli @@ -11,7 +11,6 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val mk_proof: - NCic.term Terms.bag -> Terms.M.key -> Terms.M.key list -> NCic.term - +val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit +val mk_proof:NCic.term Terms.bag -> Terms.M.key -> Terms.M.key list -> NCic.term diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index fd697265a..04fddee83 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -14,6 +14,9 @@ let debug s = prerr_endline (Lazy.force s);; let debug _ = ();; +let convert_term = ref (fun _ _ -> assert false);; +let set_convert_term f = convert_term := f;; + module COT : Set.OrderedType with type t = string * NCic.term * int * int * NCic.term * NCic.term = @@ -67,7 +70,7 @@ let index_old_db odb (status : #status) = List.fold_left (fun status (uri,_,arg) -> try - let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in + let c=fst (!convert_term uri (CicUtil.term_of_uri uri)) in let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in let src, tgt = let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli index 0f514eef6..ff6b43997 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.mli +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -13,6 +13,9 @@ type db +val set_convert_term: + (UriManager.uri -> Cic.term -> NCic.term * NCic.obj list) -> unit + class type g_status = object inherit NCicUnifHint.g_status diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index 1ea21dbcc..313fbbd0d 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -144,6 +144,7 @@ let add_user_provided_hint db t precedence = index_hint db c a b precedence ;; +(* let db () = let combine f l = List.flatten @@ -203,6 +204,7 @@ let db () = !user_db (List.flatten hints) *) ;; +*) let saturate ?(delta=0) metasenv subst context ty goal_arity = assert (goal_arity >= 0); diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi -- 2.39.2