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=1d7e85937bf644f67bd94d97879f8c3c6eb8c5da;hp=0000000000000000000000000000000000000000;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953

diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml
new file mode 100644
index 000000000..1d7e85937
--- /dev/null
+++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml
@@ -0,0 +1,197 @@
+(* 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 <sacerdot@cs.unibo.it>               *)
+(*                                 02/12/2002                                 *)
+(*                                                                            *)
+(*                            Missing description                             *)
+(*                                                                            *)
+(******************************************************************************)
+
+(* $Id$ *)
+
+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) ->
+       (* andrea: this is a bug: variable are not indexedin the db 
+	  ([!!!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 (* TASSI: ?? *)
+	      | Cic.CProp -> T.CProp
+            in
+            [],[],[!!kind,s']
+         | _ -> [],[],[])
+    | C.Meta _ -> [],[],[] (* ???? To be understood *)
+    | 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
+;; *)
+
+let universe =
+   [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]