helm/fix_params/cicFindParameters.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 exception WrongUriToConstant;;
  27 exception WrongUriToInductiveDefinition;;
  28 exception CircularDependency of string;;
  29
  30 module OrderedUris =
  31  struct
  32   type t = UriManager.uri
  33   let compare (s1 : t) (s2 : t) =
  34    (* library function for = *)
  35    compare s1 s2
  36    (*if s1 = s2 then 0 else if s1 < s2 then (-1) else 1*)
  37  end
  38 ;;
  39
  40 let filename_of_uri uri =
  41  let uri' = UriManager.string_of_uri uri in
  42   let fn = Str.replace_first (Str.regexp "cic:") Configuration.helm_dir uri' in
  43    fn ^ ".xml"
  44 ;;
  45
  46 (* quite inefficient coding of a set of strings: the only operations  *)
  47 (* performed are mem O(log n), and union O(n * log n?)                *)
  48 (* Perhaps a better implementation would be an array of bits or a map *)
  49 (* from uri to booleans                                               *)
  50 module SetOfUris = Set.Make(OrderedUris);;
  51
  52 let (@@) = SetOfUris.union;;
  53
  54 let rec parameters_of te ty pparams=
  55  let module S = SetOfUris in
  56  let module C = Cic in
  57    let rec aux =
  58     function
  59        C.Rel _ -> S.empty
  60      | C.Var uri -> S.singleton uri
  61      | C.Meta _ -> S.empty
  62      | C.Sort _ -> S.empty
  63      | C.Implicit -> S.empty
  64      | C.Cast (te, ty) -> aux te @@ aux ty
  65      | C.Prod (_, s, t) -> aux s @@ aux t
  66      | C.Lambda (_, s, t) -> aux s @@ aux t
  67      | C.LetIn (_, s, t) -> aux s @@ aux t
  68      | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
  69      | C.Const (uri,_) ->
  70         (* the parameters could be not exact but only possible *)
  71         fix_params uri (Some (filename_of_uri uri)) ;
  72         (* now the parameters are surely possible *)
  73         (match CicCache.get_obj uri with
  74             C.Definition (_, _, _, params) ->
  75               List.fold_right
  76                (fun (_,l) i ->
  77                  List.fold_right
  78                   (fun x i -> S.singleton x @@ i) l i
  79                ) params S.empty
  80           | C.Axiom (_, _, params) ->
  81              List.fold_right
  82               (fun (_,l) i ->
  83                 List.fold_right
  84                  (fun x i -> S.singleton x @@ i) l i
  85               ) params S.empty
  86           | C.CurrentProof _ -> S.empty (*CSC wrong *)
  87           | _ -> raise WrongUriToConstant
  88         )
  89      | C.Abst _ -> S.empty
  90      | C.MutInd (uri,_,_) ->
  91         (match CicCache.get_obj uri with
  92             C.InductiveDefinition (_, params, _) ->
  93              List.fold_right
  94               (fun (_,l) i ->
  95                 List.fold_right
  96                  (fun x i -> S.singleton x @@ i) l i
  97               ) params S.empty
  98           | _ -> raise WrongUriToInductiveDefinition
  99         )
 100      | C.MutConstruct (uri,_,_,_) ->
 101         (match CicCache.get_obj uri with
 102             C.InductiveDefinition (_, params, _) ->
 103              List.fold_right
 104               (fun (_,l) i ->
 105                 List.fold_right
 106                  (fun x i -> S.singleton x @@ i) l i
 107               ) params S.empty
 108           | _ -> raise WrongUriToInductiveDefinition
 109         )
 110      | C.MutCase (uri,_,_,outtype,term,patterns) ->
 111         (*CSC cosa basta? Ci vuole anche uri? *)
 112         (match CicCache.get_obj uri with
 113             C.InductiveDefinition (_, params, _) ->
 114             List.fold_right
 115              (fun (_,l) i ->
 116                List.fold_right
 117                 (fun x i -> S.singleton x @@ i) l i
 118              ) params S.empty
 119           | _ -> raise WrongUriToInductiveDefinition
 120         ) @@ aux outtype @@ aux term @@
 121          List.fold_right (fun x i -> aux x @@ i) patterns S.empty
 122      | C.Fix (_,fl) ->
 123         List.fold_right
 124          (fun (_,_,ty,bo) i  -> aux ty @@ aux bo @@ i)
 125          fl S.empty
 126      | C.CoFix (_,fl) ->
 127         List.fold_right
 128          (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i)
 129          fl S.empty
 130  in
 131   let actual_params = aux te @@ aux ty in
 132    (* sort_actual_params wants in input the ordered list of possible params *)
 133    let rec sort_actual_params2 =
 134     function
 135        [] -> []
 136      | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl)
 137      | _::tl -> sort_actual_params2 tl
 138    in
 139     let rec sort_actual_params =
 140      function
 141         [] -> []
 142       | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl)
 143     in
 144      sort_actual_params pparams
 145
 146 and fix_params uri filename =
 147  let module C = Cic in
 148   let ann = CicCache.get_annobj uri in
 149    match ann with
 150       C.ADefinition (xid, ann, id, te, ty, C.Possible pparams) ->
 151        let te' = Deannotate.deannotate_term te in
 152        let ty' = Deannotate.deannotate_term ty in
 153         let real_params = parameters_of te' ty' pparams in
 154          let fixed =
 155           C.ADefinition (xid,ann,id,te,ty,C.Actual real_params)
 156          in
 157           Xml.pp (Cic2Xml.pp fixed uri) filename ;
 158     | _ -> ()
 159 ;;