helm/mathql/mathql_generator/cGSearchPattern.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 02/12/2002                                 *)
  32 (*                                                                            *)
  33 (*                            Missing description                             *)
  34 (*                                                                            *)
  35 (******************************************************************************)
  36
  37 (* $Id$ *)
  38
  39 module T = MQGTypes
  40 module U = MQGUtil
  41
  42 type classification =
  43    Backbone of int
  44  | Branch of int
  45  | InConclusion
  46  | InHypothesis
  47 ;;
  48
  49 let soften_classification =
  50  function
  51     Backbone _ -> InConclusion
  52   | Branch _ -> InHypothesis
  53   | k -> k
  54 ;;
  55
  56 let (!!) =
  57  function
  58     Backbone n -> `MainConclusion (Some n)
  59   | Branch n -> `MainHypothesis (Some n)
  60   | _        -> assert false
  61 ;;
  62
  63 let (!!!) =
  64  function
  65     Backbone n -> `MainConclusion (Some n)
  66   | Branch n -> `MainHypothesis (Some n)
  67   | InConclusion -> `InConclusion
  68   | InHypothesis -> `InHypothesis
  69 ;;
  70
  71
  72 let (@@) (l1,l2,l3) (l1',l2',l3') =
  73  let merge l1 l2 =
  74   List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
  75  in
  76   merge l1 l1', merge l2 l2', merge l3 l3'
  77 ;;
  78
  79 let get_constraints term =
  80  let module U = UriManager in
  81  let module C = Cic in
  82   let rec process_type_aux kind =
  83    function
  84       C.Var (uri,expl_named_subst) ->
  85        (* andrea: this is a bug: variable are not indexedin the db
  86           ([!!!kind, UriManager.string_of_uri uri],[],[]) @@ *)
  87          (process_type_aux_expl_named_subst kind expl_named_subst)
  88     | C.Rel _ ->
  89        (match kind with
  90          | InConclusion
  91          | InHypothesis -> [],[],[]
  92          | _            -> [],[!!kind],[])
  93     | C.Sort s ->
  94        (match kind with
  95            Backbone _
  96          | Branch _ ->
  97             let s' =
  98              match s with
  99                 Cic.Prop -> T.Prop
 100               | Cic.Set -> T.Set
 101               | Cic.Type _ -> T.Type (* TASSI: ?? *)
 102               | Cic.CProp -> T.CProp
 103             in
 104             [],[],[!!kind,s']
 105          | _ -> [],[],[])
 106     | C.Meta _ -> [],[],[] (* ???? To be understood *)
 107     | C.Implicit _ -> assert false
 108     | C.Cast (te,_) ->
 109        (* type ignored *)
 110        process_type_aux kind te
 111     | C.Prod (_,sou,ta) ->
 112        let (source_kind,target_kind) =
 113         match kind with
 114            Backbone n -> (Branch 0, Backbone (n+1))
 115          | Branch n -> (InHypothesis, Branch (n+1))
 116          | k -> (k,k)
 117        in
 118         process_type_aux source_kind sou @@
 119         process_type_aux target_kind ta
 120     | C.Lambda (_,sou,ta) ->
 121         let kind' = soften_classification kind in
 122          process_type_aux kind' sou @@
 123          process_type_aux kind' ta
 124     | C.LetIn (_,te,ta)->
 125        let kind' = soften_classification kind in
 126         process_type_aux kind' te @@
 127         process_type_aux kind ta
 128     | C.Appl (he::tl) ->
 129        let kind' = soften_classification kind in
 130         process_type_aux kind he @@
 131         List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
 132     | C.Appl _ -> assert false
 133     | C.Const (uri,_) ->
 134        [!!!kind, UriManager.string_of_uri uri],[],[]
 135     | C.MutInd (uri,typeno,expl_named_subst) ->
 136        ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^
 137         string_of_int (typeno + 1) ^ ")"],[],[]) @@
 138          (process_type_aux_expl_named_subst kind expl_named_subst)
 139     | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
 140         ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^
 141          string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")"],[],[])
 142           @@ (process_type_aux_expl_named_subst kind expl_named_subst)
 143     | C.MutCase (_,_,_,term,patterns) ->
 144        (* outtype ignored *)
 145        let kind' = soften_classification kind in
 146         process_type_aux kind' term @@
 147         List.fold_left (fun i t -> i @@ process_type_aux kind' t)
 148          ([],[],[]) patterns
 149     | C.Fix (_,funs) ->
 150        let kind' = soften_classification kind in
 151         List.fold_left
 152          (fun i (_,_,bo,ty) ->
 153            i @@
 154             process_type_aux kind' bo @@
 155             process_type_aux kind' ty
 156          ) ([],[],[]) funs
 157     | C.CoFix (_,funs) ->
 158        let kind' = soften_classification kind in
 159         List.fold_left
 160          (fun i (_,bo,ty) ->
 161            i @@
 162             process_type_aux kind' bo @@
 163             process_type_aux kind' ty
 164          ) ([],[],[]) funs
 165  and process_type_aux_expl_named_subst kind =
 166   List.fold_left
 167    (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
 168    ([],[],[])
 169 in
 170  let obj_constraints,rel_constraints,sort_constraints =
 171   process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
 172  in
 173   (obj_constraints,rel_constraints,sort_constraints)
 174 ;;
 175
 176 (*CSC: Debugging only *)
 177 (*
 178 let get_constraints term =
 179  let res = get_constraints term in
 180  let (objs,rels,sorts) = res in
 181   let text_of_pos p =
 182     U.text_of_position p ^ " " ^ U.text_of_depth p "NULL"
 183   in
 184   prerr_endline "Constraints on objs:" ;
 185   List.iter
 186    (function (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ;
 187   prerr_endline "Constraints on Rels:" ;
 188   List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ;
 189   prerr_endline "Constraints on Sorts:" ;
 190   List.iter
 191    (function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s)
 192    ) sorts ;
 193   res
 194 ;; *)
 195
 196 let universe =
 197    [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]