X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=fdb1114fabdcb6e1a34639ffe21805ff9422bd7f;hb=35be38f22657bf00344e34fe75d7f3a5283832c1;hp=9f9b721f69f60184fa47244088ee9595a4e1ea57;hpb=7403c949ea3a84624f8c05deee00de53336937ba;p=helm.git diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index 9f9b721f6..fdb1114fa 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -28,19 +28,19 @@ open Printf 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 @@ -50,8 +50,8 @@ module OrderedMetadata = 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 @@ -63,122 +63,198 @@ module S = MetadataSet 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 - | Cic.Rel _ -> + let rec aux (pos: position) set = function + | Cic.Rel _ + | Cic.Var _ -> 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 | Cic.Meta (_, local_context) -> List.fold_left (fun set context -> match context with | None -> set - | Some term -> aux pos pi_depth set term) + | Some term -> aux (next_pos 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 + (*assert (not (is_main_pos pos));*) + let set = aux (next_pos pos) set source in + aux (next_pos 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 + +module OrderedInt = +struct + type t = int + let compare = Pervasives.compare +end -let compute_type uri typeno (name, _, ty, constructors) = +module IntSet = Set.Make (OrderedInt) + +let compute_metas term = + let rec aux in_hyp ((concl_metas, hyp_metas) as acc) cic = + match cic with + | Cic.Rel _ + | Cic.Sort _ + | Cic.Var _ -> acc + | Cic.Meta (no, local_context) -> + let acc = + if in_hyp then + (concl_metas, IntSet.add no hyp_metas) + else + (IntSet.add no concl_metas, hyp_metas) + in + List.fold_left + (fun set context -> + match context with + | None -> set + | Some term -> aux in_hyp set term) + acc + local_context + | Cic.Implicit _ -> assert false + | Cic.Cast (term, ty) -> + (* TODO consider also ty? *) + aux in_hyp acc term + | Cic.Prod (_, source, target) -> + if in_hyp then + let acc = aux in_hyp acc source in + aux in_hyp acc target + else + let acc = aux true acc source in + aux in_hyp acc target + | Cic.Lambda (_, source, target) -> + let acc = aux in_hyp acc source in + aux in_hyp acc target + | Cic.LetIn (_, term, target) -> + aux in_hyp acc (CicSubstitution.subst term target) + | Cic.Appl [] -> assert false + | Cic.Appl (hd :: tl) -> + let acc = aux in_hyp acc hd in + List.fold_left (fun acc term -> aux in_hyp acc term) acc tl + | Cic.Const (_, subst) + | Cic.MutInd (_, _, subst) + | Cic.MutConstruct (_, _, _, subst) -> + List.fold_left (fun acc (_, term) -> aux in_hyp acc term) acc subst + | Cic.MutCase (uri, _, outtype, term, pats) -> + let acc = aux in_hyp acc term in + let acc = aux in_hyp acc outtype in + List.fold_left (fun acc term -> aux in_hyp acc term) acc pats + | Cic.Fix (_, funs) -> + List.fold_left + (fun acc (_, _, ty, body) -> + let acc = aux in_hyp acc ty in + aux in_hyp acc body) + acc funs + | Cic.CoFix (_, funs) -> + List.fold_left + (fun acc (_, ty, body) -> + let acc = aux in_hyp acc ty in + aux in_hyp acc body) + acc funs + in + aux false (IntSet.empty, IntSet.empty) term + + (** type of inductiveType *) +let compute_type pos 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 pos 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 pos term))) constructors in type_metadata :: constructors_metadata -let compute_ind ~uri ~types = +let compute_ind pos ~uri ~types = let idx = ref ~-1 in - List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types) + List.concat + (List.map + (fun ty -> incr idx; compute_type pos uri !idx ty) types) -let compute ~body ~ty = - let type_metadata = compute_term `MainConclusion ty in +let compute (pos:position) ~body ~ty = + let type_metadata = compute_term pos ty in let body_metadata = match body with | None -> S.empty @@ -188,7 +264,7 @@ let compute ~body ~ty = 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 @@ -196,10 +272,51 @@ let compute ~body ~ty = (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) let compute_term start_pos term = S.elements (compute_term start_pos term) +let rec compute_var pos uri = + let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + | Cic.Variable (_, body, ty, params, _) -> + let metadata_of_vars = + List.flatten + (List.map (compute_var (next_pos pos)) params) in + (match pos with + | `MainHypothesis (Some 0) -> + let pos = `MainHypothesis(Some (List.length params)) in + (compute pos ~body ~ty)@metadata_of_vars + | `InHypothesis -> + (compute pos ~body ~ty)@metadata_of_vars + | _ -> assert false) + | _ -> assert false + +let compute_obj uri = + let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + | Cic.Variable (_, body, ty, params, _) + | Cic.Constant (_, body, ty, params, _) -> + let pos = `MainConclusion(Some (List.length params)) in + let metadata = compute pos ~body ~ty + in + let metadata_of_vars = + List.flatten + (List.map (compute_var (`MainHypothesis (Some 0))) params) + in + [UriManager.string_of_uri uri, + UriManager.name_of_uri uri,metadata @ metadata_of_vars] + | Cic.InductiveDefinition (types, params, _, _) -> + let pos = `MainConclusion(Some (List.length params)) in + let metadata_of_vars = + List.flatten + (List.map (compute_var (`MainHypothesis (Some 0))) params) in + let metadata = compute_ind pos ~uri ~types in + List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata + | Cic.CurrentProof _ -> assert false + + +let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty