--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MetadataTypes
+
+let is_main_pos = function
+ | `MainConclusion
+ | `MainHypothesis -> true
+ | _ -> false
+
+let main_pos (pos: position): main_position =
+ match pos with
+ | `MainConclusion -> `MainConclusion
+ | `MainHypothesis -> `MainHypothesis
+ | _ -> assert false
+
+let next_pos = function
+ | `MainConclusion -> `InConclusion
+ | `MainHypothesis -> `InHypothesis
+ | pos -> pos
+
+let string_of_uri = UriManager.string_of_uri
+
+module OrderedMetadata =
+ struct
+ type t = MetadataTypes.metadata
+ let compare m1 m2 = (* ignore universes in Cic.Type sort *)
+ match (m1, m2) with
+ | `Sort (Cic.Type _, p1, d1), `Sort (Cic.Type _, p2, d2) ->
+ Pervasives.compare (p1, d2) (p2, d2)
+ | _ -> Pervasives.compare m1 m2
+ end
+
+module MetadataSet = Set.Make (OrderedMetadata)
+module StringSet = Set.Make (String)
+
+module S = MetadataSet
+
+let unopt = function Some x -> x | None -> assert false
+
+let incr_depth = function
+ | None -> assert false
+ | Some x -> Some (x + 1)
+
+let compute_term pos term =
+ let rec aux (pos: position) pi_depth set = function
+ | Cic.Rel _ ->
+ if is_main_pos pos then
+ S.add (`Rel (main_pos pos, unopt pi_depth)) set
+ else
+ set
+ | Cic.Var _ -> set
+ | Cic.Meta (_, local_context) ->
+ List.fold_left
+ (fun set context ->
+ match context with
+ | None -> set
+ | Some term -> aux pos pi_depth set term)
+ set
+ local_context
+ | Cic.Sort sort ->
+ if is_main_pos pos then
+ S.add (`Sort (sort, main_pos pos, unopt pi_depth)) set
+ else
+ set
+ | Cic.Implicit _ -> assert false
+ | Cic.Cast (term, ty) ->
+ (* TODO consider also ty? *)
+ aux pos pi_depth set term
+ | Cic.Prod (_, source, target) ->
+ (match pos with
+ | `MainConclusion ->
+ let set = aux `MainHypothesis (Some 0) set source in
+ aux pos (incr_depth pi_depth) set target
+ | `MainHypothesis ->
+ let set = aux `InHypothesis None set source in
+ aux pos (incr_depth pi_depth) set target
+ | `InConclusion
+ | `InHypothesis
+ | `InBody ->
+ let set = aux pos None set source in
+ aux pos None set target)
+ | Cic.Lambda (_, source, target) ->
+ assert (not (is_main_pos pos));
+ let set = aux pos None set source in
+ aux pos None set target
+ | Cic.LetIn (_, term, target) ->
+ if is_main_pos pos then
+ aux pos pi_depth set (CicSubstitution.subst term target)
+ else
+ let set = aux pos None set term in
+ aux pos None set target
+ | Cic.Appl [] -> assert false
+ | Cic.Appl (hd :: tl) ->
+ let set = aux pos pi_depth set hd in
+ List.fold_left
+ (fun set term -> aux (next_pos pos) None set term)
+ set tl
+ | Cic.Const (uri, subst) ->
+ let set = S.add (`Obj (string_of_uri uri, pos, pi_depth)) set in
+ List.fold_left
+ (fun set (_, term) -> aux (next_pos pos) None set term)
+ set subst
+ | Cic.MutInd (uri, typeno, subst) ->
+ let uri = UriManager.string_of_uriref (uri, [typeno]) in
+ let set = S.add (`Obj (uri, pos, pi_depth)) set in
+ List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term)
+ set subst
+ | Cic.MutConstruct (uri, typeno, consno, subst) ->
+ let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
+ let set = S.add (`Obj (uri, pos, pi_depth)) set in
+ List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term)
+ set subst
+ | Cic.MutCase (uri, _, outtype, term, pats) ->
+ let pos = next_pos pos in
+ let set = aux pos None set term in
+ let set = aux pos None set outtype in
+ List.fold_left (fun set term -> aux pos None set term) set pats
+ | Cic.Fix (_, funs) ->
+ let pos = next_pos pos in
+ List.fold_left
+ (fun set (_, _, ty, body) ->
+ let set = aux pos None set ty in
+ aux pos None set body)
+ set funs
+ | Cic.CoFix (_, funs) ->
+ let pos = next_pos pos in
+ List.fold_left
+ (fun set (_, ty, body) ->
+ let set = aux pos None set ty in
+ aux pos None set body)
+ set funs
+ in
+ aux pos (Some 0) S.empty term
+
+let compute_type uri typeno (name, _, ty, constructors) =
+ let consno = ref 0 in
+ let type_metadata =
+ (UriManager.string_of_uriref (uri, [typeno]), name,
+ S.elements (compute_term `MainConclusion ty))
+ in
+ let constructors_metadata =
+ List.map
+ (fun (name, term) ->
+ incr consno;
+ let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
+ (uri, name, S.elements (compute_term `MainConclusion term)))
+ constructors
+ in
+ type_metadata :: constructors_metadata
+
+let compute_ind ~uri ~types =
+ let idx = ref ~-1 in
+ List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types)
+
+let compute ~body ~ty =
+ let type_metadata = compute_term `MainConclusion ty in
+ let body_metadata =
+ match body with
+ | None -> S.empty
+ | Some body -> compute_term `InBody body
+ in
+ let uris =
+ S.fold
+ (fun metadata uris ->
+ match metadata with
+ | `Obj (uri, _, _) -> StringSet.add uri uris
+ | _ -> uris)
+ type_metadata StringSet.empty
+ in
+ S.elements
+ (S.union
+ (S.filter
+ (function
+ | `Obj (uri, _, _) when StringSet.mem uri uris -> false
+ | _ -> true)
+ body_metadata)
+ type_metadata)
+
projects / helm.git / blobdiff