helm/ocaml/mathql_generator/mQueryLevels2.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 type classification =
  38    Backbone of int
  39  | Branch of int
  40  | InConclusion
  41  | InHypothesis
  42 ;;
  43
  44 let soften_classification =
  45  function
  46     Backbone _ -> InConclusion
  47   | Branch _ -> InHypothesis
  48   | k -> k
  49 ;;
  50
  51 let (!!) =
  52  function
  53     Backbone n ->
  54      "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion", Some n
  55   | Branch n ->
  56      "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis", Some n
  57   | InConclusion ->
  58      "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion", None
  59   | InHypothesis ->
  60      "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis", None
  61 ;;
  62
  63 let (@@) (l1,l2,l3) (l1',l2',l3') =
  64  let merge l1 l2 =
  65   List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
  66  in
  67   merge l1 l1', merge l2 l2', merge l3 l3'
  68 ;;
  69
  70 let get_constraints term =
  71  let module U = UriManager in
  72  let module C = Cic in
  73   let rec process_type_aux kind =
  74    function
  75       C.Var (uri,expl_named_subst) ->
  76        let kind',depth = !!kind in
  77         ([UriManager.string_of_uri uri,kind',depth],[],[]) @@
  78           (process_type_aux_expl_named_subst kind expl_named_subst)
  79     | C.Rel _ ->
  80        let kind',depth = !!kind in
  81         (match depth with
  82             None -> [],[],[]
  83           | Some d -> [],[kind',Some d],[])
  84     | C.Sort s ->
  85        (match kind with
  86            Backbone _
  87          | Branch _ ->
  88             let s' =
  89              match s with
  90                 Cic.Prop ->
  91                  "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"
  92               | Cic.Set ->
  93                  "http://www.cs.unibo.it/helm/schemas/schema-helm#Set"
  94               | Cic.Type ->
  95                  "http://www.cs.unibo.it/helm/schemas/schema-helm#Type"
  96             in
  97              let kind',depth = !!kind in
  98               (match depth with
  99                   None -> assert false
 100                 | Some d -> [],[],[kind',Some d,s'])
 101          | _ -> [],[],[])
 102     | C.Meta _
 103     | C.Implicit -> assert false
 104     | C.Cast (te,_) ->
 105        (* type ignored *)
 106        process_type_aux kind te
 107     | C.Prod (_,sou,ta) ->
 108        let (source_kind,target_kind) =
 109         match kind with
 110            Backbone n -> (Branch 0, Backbone (n+1))
 111          | Branch n -> (InHypothesis, Branch (n+1))
 112          | k -> (k,k)
 113        in
 114         process_type_aux source_kind sou @@
 115         process_type_aux target_kind ta
 116     | C.Lambda (_,sou,ta) ->
 117         let kind' = soften_classification kind in
 118          process_type_aux kind' sou @@
 119          process_type_aux kind' ta
 120     | C.LetIn (_,te,ta)->
 121        let kind' = soften_classification kind in
 122         process_type_aux kind' te @@
 123         process_type_aux kind ta
 124     | C.Appl (he::tl) ->
 125        let kind' = soften_classification kind in
 126         process_type_aux kind he @@
 127         List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
 128     | C.Appl _ -> assert false
 129     | C.Const (uri,_) ->
 130        let kind',depth = !!kind in
 131         [UriManager.string_of_uri uri,kind',depth],[],[]
 132     | C.MutInd (uri,typeno,expl_named_subst) ->
 133        let kind',depth = !!kind in
 134        ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
 135           ")", kind', depth],[],[]) @@
 136          (process_type_aux_expl_named_subst kind expl_named_subst)
 137     | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
 138        let kind',depth = !!kind in
 139         ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
 140           "/" ^ string_of_int consno ^ ")",kind',depth],[],[]) @@
 141           (process_type_aux_expl_named_subst kind expl_named_subst)
 142     | C.MutCase (_,_,_,term,patterns) ->
 143        (* outtype ignored *)
 144        let kind' = soften_classification kind in
 145         process_type_aux kind' term @@
 146         List.fold_left (fun i t -> i @@ process_type_aux kind' t)
 147          ([],[],[]) patterns
 148     | C.Fix (_,funs) ->
 149        let kind' = soften_classification kind in
 150         List.fold_left
 151          (fun i (_,_,bo,ty) ->
 152            i @@
 153             process_type_aux kind' bo @@
 154             process_type_aux kind' ty
 155          ) ([],[],[]) funs
 156     | C.CoFix (_,funs) ->
 157        let kind' = soften_classification kind in
 158         List.fold_left
 159          (fun i (_,bo,ty) ->
 160            i @@
 161             process_type_aux kind' bo @@
 162             process_type_aux kind' ty
 163          ) ([],[],[]) funs
 164  and process_type_aux_expl_named_subst kind =
 165   List.fold_left
 166    (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
 167    ([],[],[])
 168 in
 169  let obj_constraints,rel_constraints,sort_constraints =
 170   process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
 171  in
 172   (obj_constraints,rel_constraints,sort_constraints)
 173 ;;
 174
 175 (*CSC: Debugging only *)
 176 let get_constraints term =
 177  let res = get_constraints term in
 178  let (objs,rels,sorts) = res in
 179   prerr_endline "Constraints on objs:" ;
 180   List.iter
 181    (function (s1,s2,n) ->
 182      prerr_endline
 183       (s1 ^ " " ^ s2 ^ " " ^
 184         match n with None -> "NULL" | Some n -> string_of_int n)
 185    ) objs ;
 186   prerr_endline "Constraints on Rels:" ;
 187   List.iter
 188    (function (s,n) ->
 189      prerr_endline
 190       (s ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
 191    ) rels ;
 192   prerr_endline "Constraints on Sorts:" ;
 193   List.iter
 194    (function (s1,n,s2) ->
 195      prerr_endline
 196       (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
 197         " " ^ s2)
 198    ) sorts ;
 199   res
 200 ;;