X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGSearchPattern.ml;fp=helm%2Focaml%2Fmathql_generator%2FcGSearchPattern.ml;h=0000000000000000000000000000000000000000;hp=60633f897e722f988990d7157506ce178b052e34;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml deleted file mode 100644 index 60633f897..000000000 --- a/helm/ocaml/mathql_generator/cGSearchPattern.ml +++ /dev/null @@ -1,189 +0,0 @@ -(* 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 *) -(* *) -(******************************************************************************) - -module T = MQGTypes -module U = MQGUtil - -type classification = - Backbone of int - | Branch of int - | InConclusion - | InHypothesis -;; - -let soften_classification = - function - Backbone _ -> InConclusion - | Branch _ -> InHypothesis - | k -> k -;; - -let (!!) = - function - Backbone n -> `MainConclusion (Some n) - | Branch n -> `MainHypothesis (Some n) - | _ -> assert false -;; - -let (!!!) = - function - Backbone n -> `MainConclusion (Some n) - | Branch n -> `MainHypothesis (Some n) - | InConclusion -> `InConclusion - | InHypothesis -> `InHypothesis -;; - - -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) -> - ([!!!kind, UriManager.string_of_uri uri],[],[]) @@ - (process_type_aux_expl_named_subst kind expl_named_subst) - | C.Rel _ -> - (match kind with - | InConclusion - | InHypothesis -> [],[],[] - | _ -> [],[!!kind],[]) - | C.Sort s -> - (match kind with - Backbone _ - | Branch _ -> - let s' = - match s with - Cic.Prop -> T.Prop - | Cic.Set -> T.Set - | Cic.Type -> T.Type - in - [],[],[!!kind,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,_) -> - [!!!kind, UriManager.string_of_uri uri],[],[] - | C.MutInd (uri,typeno,expl_named_subst) -> - ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (typeno + 1) ^ ")"],[],[]) @@ - (process_type_aux_expl_named_subst kind expl_named_subst) - | C.MutConstruct (uri,typeno,consno,expl_named_subst) -> - ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^ - string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")"],[],[]) - @@ (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 - let obj_constraints,rel_constraints,sort_constraints = - process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term) - in - (obj_constraints,rel_constraints,sort_constraints) -;; - -(*CSC: Debugging only *) -let get_constraints term = - let res = get_constraints term in - let (objs,rels,sorts) = res in - let text_of_pos p = - U.text_of_position p ^ " " ^ U.text_of_depth p "NULL" - in - prerr_endline "Constraints on objs:" ; - List.iter - (function (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ; - prerr_endline "Constraints on Rels:" ; - List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ; - prerr_endline "Constraints on Sorts:" ; - List.iter - (function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s) - ) sorts ; - res -;;