helm/interface/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.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
  68      | C.Const (uri,_) ->
  69         (* the parameters could be not exact but only possible *)
  70         fix_params uri (Some (filename_of_uri uri)) ;
  71         (* now the parameters are surely possible *)
  72         (match CicCache.get_obj uri with
  73             C.Definition (_, _, _, params) ->
  74               List.fold_right
  75                (fun (_,l) i ->
  76                  List.fold_right
  77                   (fun x i -> S.singleton x @@ i) l i
  78                ) params S.empty
  79           | C.Axiom (_, _, params) ->
  80              List.fold_right
  81               (fun (_,l) i ->
  82                 List.fold_right
  83                  (fun x i -> S.singleton x @@ i) l i
  84               ) params S.empty
  85           | C.CurrentProof _ -> S.empty (*CSC wrong *)
  86           | _ -> raise WrongUriToConstant
  87         )
  88      | C.Abst _ -> S.empty
  89      | C.MutInd (uri,_,_) ->
  90         (match CicCache.get_obj uri with
  91             C.InductiveDefinition (_, params, _) ->
  92              List.fold_right
  93               (fun (_,l) i ->
  94                 List.fold_right
  95                  (fun x i -> S.singleton x @@ i) l i
  96               ) params S.empty
  97           | _ -> raise WrongUriToInductiveDefinition
  98         )
  99      | C.MutConstruct (uri,_,_,_) ->
 100         (match CicCache.get_obj uri with
 101             C.InductiveDefinition (_, params, _) ->
 102              List.fold_right
 103               (fun (_,l) i ->
 104                 List.fold_right
 105                  (fun x i -> S.singleton x @@ i) l i
 106               ) params S.empty
 107           | _ -> raise WrongUriToInductiveDefinition
 108         )
 109      | C.MutCase (uri,_,_,outtype,term,patterns) ->
 110         (*CSC cosa basta? Ci vuole anche uri? *)
 111         (match CicCache.get_obj uri with
 112             C.InductiveDefinition (_, params, _) ->
 113             List.fold_right
 114              (fun (_,l) i ->
 115                List.fold_right
 116                 (fun x i -> S.singleton x @@ i) l i
 117              ) params S.empty
 118           | _ -> raise WrongUriToInductiveDefinition
 119         ) @@ aux outtype @@ aux term @@
 120          List.fold_right (fun x i -> aux x @@ i) patterns S.empty
 121      | C.Fix (_,fl) ->
 122         List.fold_right
 123          (fun (_,_,ty,bo) i  -> aux ty @@ aux bo @@ i)
 124          fl S.empty
 125      | C.CoFix (_,fl) ->
 126         List.fold_right
 127          (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i)
 128          fl S.empty
 129  in
 130   let actual_params = aux te @@ aux ty in
 131    (* sort_actual_params wants in input the ordered list of possible params *)
 132    let rec sort_actual_params2 =
 133     function
 134        [] -> []
 135      | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl)
 136      | _::tl -> sort_actual_params2 tl
 137    in
 138     let rec sort_actual_params =
 139      function
 140         [] -> []
 141       | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl)
 142     in
 143      sort_actual_params pparams
 144
 145 and fix_params uri filename =
 146  let module C = Cic in
 147   let (ann, _, deann) = CicCache.get_annobj uri in
 148    match ann, deann with
 149       (C.ADefinition (xid, ann, id, te, ty, C.Possible pparams),
 150        C.Definition (id', te', ty', _)) ->
 151         (* let's freeze the object to avoid circular dependencies *)
 152         CicCache.change_obj uri None ;
 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           (* unfreeze and fix the object *)
 159           CicCache.change_obj uri
 160            (Some (C.Definition (id', te', ty', real_params)))
 161     | _ -> ()
 162 ;;