open MetadataTypes
let is_main_pos = function
- | `MainConclusion
- | `MainHypothesis -> true
+ | `MainConclusion _
+ | `MainHypothesis _ -> true
| _ -> false
let main_pos (pos: position): main_position =
match pos with
- | `MainConclusion -> `MainConclusion
- | `MainHypothesis -> `MainHypothesis
+ | `MainConclusion depth -> `MainConclusion depth
+ | `MainHypothesis depth -> `MainHypothesis depth
| _ -> assert false
let next_pos = function
- | `MainConclusion -> `InConclusion
- | `MainHypothesis -> `InHypothesis
+ | `MainConclusion _ -> `InConclusion
+ | `MainHypothesis _ -> `InHypothesis
| pos -> pos
let string_of_uri = UriManager.string_of_uri
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)
+ | `Sort (Cic.Type _, pos1), `Sort (Cic.Type _, pos2) ->
+ Pervasives.compare pos1 pos2
| _ -> Pervasives.compare m1 m2
end
let unopt = function Some x -> x | None -> assert false
let incr_depth = function
- | None -> assert false
- | Some x -> Some (x + 1)
+ | `MainConclusion (Some depth) -> `MainConclusion (Some (depth + 1))
+ | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1))
+ | _ -> assert false
let compute_term pos term =
- let rec aux (pos: position) pi_depth set = function
+ let rec aux (pos: position) set = function
| Cic.Rel _ ->
if is_main_pos pos then
- S.add (`Rel (main_pos pos, unopt pi_depth)) set
+ S.add (`Rel (main_pos pos)) set
else
set
| Cic.Var _ -> set
(fun set context ->
match context with
| None -> set
- | Some term -> aux pos pi_depth set term)
+ | Some term -> aux pos 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
+ S.add (`Sort (sort, main_pos pos)) set
else
set
| Cic.Implicit _ -> assert false
| Cic.Cast (term, ty) ->
(* TODO consider also ty? *)
- aux pos pi_depth set term
+ aux pos 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
+ | `MainConclusion _ ->
+ let set = aux (`MainHypothesis (Some 0)) set source in
+ aux (incr_depth pos) set target
+ | `MainHypothesis _ ->
+ let set = aux `InHypothesis set source in
+ aux (incr_depth pos) set target
| `InConclusion
| `InHypothesis
| `InBody ->
- let set = aux pos None set source in
- aux pos None set target)
+ let set = aux pos set source in
+ aux pos 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
+ let set = aux pos set source in
+ aux pos set target
| Cic.LetIn (_, term, target) ->
if is_main_pos pos then
- aux pos pi_depth set (CicSubstitution.subst term target)
+ aux pos set (CicSubstitution.subst term target)
else
- let set = aux pos None set term in
- aux pos None set target
+ let set = aux pos set term in
+ aux pos set target
| Cic.Appl [] -> assert false
| Cic.Appl (hd :: tl) ->
- let set = aux pos pi_depth set hd in
+ let set = aux pos set hd in
List.fold_left
- (fun set term -> aux (next_pos pos) None set term)
+ (fun set term -> aux (next_pos pos) set term)
set tl
| Cic.Const (uri, subst) ->
- let set = S.add (`Obj (string_of_uri uri, pos, pi_depth)) set in
+ let set = S.add (`Obj (string_of_uri uri, pos)) set in
List.fold_left
- (fun set (_, term) -> aux (next_pos pos) None set term)
+ (fun set (_, term) -> aux (next_pos pos) 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)
+ let set = S.add (`Obj (uri, pos)) set in
+ List.fold_left (fun set (_, term) -> aux (next_pos pos) 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)
+ let set = S.add (`Obj (uri, pos)) set in
+ List.fold_left (fun set (_, term) -> aux (next_pos pos) 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
+ let set = aux pos set term in
+ let set = aux pos set outtype in
+ List.fold_left (fun set term -> aux pos 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)
+ let set = aux pos set ty in
+ aux pos 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)
+ let set = aux pos set ty in
+ aux pos set body)
set funs
in
- aux pos (Some 0) S.empty term
+ aux pos 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))
+ S.elements (compute_term (`MainConclusion (Some 0)) 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)))
+ (uri, name, S.elements (compute_term (`MainConclusion (Some 0)) term)))
constructors
in
type_metadata :: constructors_metadata
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 type_metadata = compute_term (`MainConclusion (Some 0)) ty in
let body_metadata =
match body with
| None -> S.empty
S.fold
(fun metadata uris ->
match metadata with
- | `Obj (uri, _, _) -> StringSet.add uri uris
+ | `Obj (uri, _) -> StringSet.add uri uris
| _ -> uris)
type_metadata StringSet.empty
in
(S.union
(S.filter
(function
- | `Obj (uri, _, _) when StringSet.mem uri uris -> false
+ | `Obj (uri, _) when StringSet.mem uri uris -> false
| _ -> true)
body_metadata)
type_metadata)
projects / helm.git / blobdiff