X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmquery_generator%2FmQueryLevels2.ml;fp=helm%2Focaml%2Fmquery_generator%2FmQueryLevels2.ml;h=0000000000000000000000000000000000000000;hb=4c9da07604c4f8b66e4e92861ee38129422d23fb;hp=968d2a35e8d6439c65c0549bc35d7f58c372f383;hpb=11b9b274291baa8c5462b2ce3e2a5f93a39c9d57;p=helm.git

diff --git a/helm/ocaml/mquery_generator/mQueryLevels2.ml b/helm/ocaml/mquery_generator/mQueryLevels2.ml
deleted file mode 100644
index 968d2a35e..000000000
--- a/helm/ocaml/mquery_generator/mQueryLevels2.ml
+++ /dev/null
@@ -1,200 +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 <sacerdot@cs.unibo.it>               *)
-(*                                 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',Some 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#Prop"
-              | 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',Some 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
- 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
-  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 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
-   ) rels ;
-  prerr_endline "Constraints on Sorts:" ;
-  List.iter
-   (function (s1,n,s2) ->
-     prerr_endline
-      (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
-        " " ^ s2)
-   ) sorts ;
-  res
-;;