helm/interface/cicFindParameters.ml

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