From a370bf72d9e59254327ae3801ed4201f9981c6f0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Dec 2002 18:18:02 +0000 Subject: [PATCH] First implementation of the new generalized SearchPattern on the whole type (not only the conclusion). Despite the file name, no levels have been implemented so far. --- helm/gTopLevel/.depend | 10 +- helm/gTopLevel/Makefile | 12 +- helm/gTopLevel/mQueryLevels2.ml | 193 +++++++++++++++++++++++++++++++ helm/gTopLevel/mQueryLevels2.mli | 44 +++++++ 4 files changed, 249 insertions(+), 10 deletions(-) create mode 100644 helm/gTopLevel/mQueryLevels2.ml create mode 100644 helm/gTopLevel/mQueryLevels2.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index fa76e97ae..026b4aacf 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -61,11 +61,13 @@ sequentPp.cmo: cic2Xml.cmi cic2acic.cmi proofEngine.cmi sequentPp.cmi sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx sequentPp.cmi mQueryLevels.cmo: mQueryLevels.cmi mQueryLevels.cmx: mQueryLevels.cmi +mQueryLevels2.cmo: mQueryLevels2.cmi +mQueryLevels2.cmx: mQueryLevels2.cmi mQueryGenerator.cmo: mQueryLevels.cmi mQueryGenerator.cmi mQueryGenerator.cmx: mQueryLevels.cmx mQueryGenerator.cmi gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi logicalOperations.cmi \ - mQueryGenerator.cmi mQueryLevels.cmi proofEngine.cmi sequentPp.cmi \ - xml2Gdome.cmi + mQueryGenerator.cmi mQueryLevels.cmi mQueryLevels2.cmi proofEngine.cmi \ + sequentPp.cmi xml2Gdome.cmi gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \ - mQueryGenerator.cmx mQueryLevels.cmx proofEngine.cmx sequentPp.cmx \ - xml2Gdome.cmx + mQueryGenerator.cmx mQueryLevels.cmx mQueryLevels2.cmx proofEngine.cmx \ + sequentPp.cmx xml2Gdome.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 7109f291a..9d7c8ac7d 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -24,16 +24,16 @@ DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \ logicalOperations.mli sequentPp.ml sequentPp.mli mQueryGenerator.mli \ - mQueryLevels.ml mQueryGenerator.ml gTopLevel.ml + mQueryLevels.ml mQueryLevels2.ml mQueryGenerator.ml gTopLevel.ml TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ proofEngineReduction.cmo proofEngineStructuralRules.cmo \ tacticals.cmo reductionTactics.cmo primitiveTactics.cmo \ - variousTactics.cmo \ - ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \ - doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ - logicalOperations.cmo sequentPp.cmo \ - mQueryLevels.cmo mQueryGenerator.cmo gTopLevel.cmo + variousTactics.cmo ring.cmo fourier.cmo fourierR.cmo \ + proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \ + cic2Xml.cmo logicalOperations.cmo sequentPp.cmo \ + mQueryLevels.cmo mQueryLevels2.cmo mQueryGenerator.cmo \ + gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml new file mode 100644 index 000000000..80bbdf1b6 --- /dev/null +++ b/helm/gTopLevel/mQueryLevels2.ml @@ -0,0 +1,193 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 02/12/2002 *) +(* *) +(* Missing description *) +(* *) +(******************************************************************************) + +type classification = + Backbone of int + | Branch of int + | InConclusion + | InHypothesis +;; + +let soften_classification = + function + Backbone _ -> InConclusion + | Branch _ -> InHypothesis + | k -> k +;; + +let (!!) = + function + Backbone n -> + "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion", Some n + | Branch n -> + "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis", Some n + | InConclusion -> + "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion", None + | InHypothesis -> + "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis", None +;; + +let (@@) (l1,l2,l3) (l1',l2',l3') = + let merge l1 l2 = + List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1 + in + merge l1 l1', merge l2 l2', merge l3 l3' +;; + +let get_constraints term = + let module U = UriManager in + let module C = Cic in + let rec process_type_aux kind = + function + C.Var (uri,expl_named_subst) -> + let kind',depth = !!kind in + ([UriManager.string_of_uri uri,kind',depth],[],[]) @@ + (process_type_aux_expl_named_subst kind expl_named_subst) + | C.Rel _ -> + let kind',depth = !!kind in + (match depth with + None -> [],[],[] + | Some d -> [],[kind',d],[]) + | C.Sort s -> + (match kind with + Backbone _ + | Branch _ -> + let s' = + match s with + Cic.Prop -> + "http://www.cs.unibo.it/helm/schemas/schema-helm#Prod" + | Cic.Set -> + "http://www.cs.unibo.it/helm/schemas/schema-helm#Set" + | Cic.Type -> + "http://www.cs.unibo.it/helm/schemas/schema-helm#Type" + in + let kind',depth = !!kind in + (match depth with + None -> assert false + | Some d -> [],[],[kind',d,s']) + | _ -> [],[],[]) + | C.Meta _ + | C.Implicit -> assert false + | C.Cast (te,_) -> + (* type ignored *) + process_type_aux kind te + | C.Prod (_,sou,ta) -> + let (source_kind,target_kind) = + match kind with + Backbone n -> (Branch 0, Backbone (n+1)) + | Branch n -> (InHypothesis, Branch (n+1)) + | k -> (k,k) + in + process_type_aux source_kind sou @@ + process_type_aux target_kind ta + | C.Lambda (_,sou,ta) -> + let kind' = soften_classification kind in + process_type_aux kind' sou @@ + process_type_aux kind' ta + | C.LetIn (_,te,ta)-> + let kind' = soften_classification kind in + process_type_aux kind' te @@ + process_type_aux kind ta + | C.Appl (he::tl) -> + let kind' = soften_classification kind in + process_type_aux kind he @@ + List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl + | C.Appl _ -> assert false + | C.Const (uri,_) -> + let kind',depth = !!kind in + [UriManager.string_of_uri uri,kind',depth],[],[] + | C.MutInd (uri,typeno,expl_named_subst) -> + let kind',depth = !!kind in + ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^ + ")", kind', depth],[],[]) @@ + (process_type_aux_expl_named_subst kind expl_named_subst) + | C.MutConstruct (uri,typeno,consno,expl_named_subst) -> + let kind',depth = !!kind in + ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^ + "/" ^ string_of_int consno ^ ")",kind',depth],[],[]) @@ + (process_type_aux_expl_named_subst kind expl_named_subst) + | C.MutCase (_,_,_,term,patterns) -> + (* outtype ignored *) + let kind' = soften_classification kind in + process_type_aux kind' term @@ + List.fold_left (fun i t -> i @@ process_type_aux kind' t) + ([],[],[]) patterns + | C.Fix (_,funs) -> + let kind' = soften_classification kind in + List.fold_left + (fun i (_,_,bo,ty) -> + i @@ + process_type_aux kind' bo @@ + process_type_aux kind' ty + ) ([],[],[]) funs + | C.CoFix (_,funs) -> + let kind' = soften_classification kind in + List.fold_left + (fun i (_,bo,ty) -> + i @@ + process_type_aux kind' bo @@ + process_type_aux kind' ty + ) ([],[],[]) funs + and process_type_aux_expl_named_subst kind = + List.fold_left + (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t)) + ([],[],[]) +in + process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term), + (None,None,None) +;; + +(*CSC: Debugging only *) +let get_constraints term = + let res = get_constraints term in + let ((objs,rels,sorts),can) = res in + prerr_endline "Constraints on objs:" ; + List.iter + (function (s1,s2,n) -> + prerr_endline + (s1 ^ " " ^ s2 ^ " " ^ + match n with None -> "NULL" | Some n -> string_of_int n) + ) objs ; + prerr_endline "Constraints on Rels:" ; + List.iter + (function (s,n) -> + prerr_endline (s ^ " " ^ string_of_int n)) rels ; + prerr_endline "Constraints on Sorts:" ; + List.iter + (function (s1,n,s2) -> + prerr_endline (s1 ^ " " ^ string_of_int n ^ " " ^ s2)) sorts ; + res +;; diff --git a/helm/gTopLevel/mQueryLevels2.mli b/helm/gTopLevel/mQueryLevels2.mli new file mode 100644 index 000000000..822564d3a --- /dev/null +++ b/helm/gTopLevel/mQueryLevels2.mli @@ -0,0 +1,44 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Ferruccio Guidi *) +(* 30/04/2002 *) +(* *) +(* *) +(******************************************************************************) + +val get_constraints: + Cic.term -> +(* + MQueryGenerator.must_restrictions * MQueryGenerator.can_restrictions +*) + ((string * string * int option) list * (string * int) list * + (string * int * string) list) * + ((string * string * int option) list option * (string * int) list option * + (string * int * string) list option) -- 2.39.2