X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=fdb1114fabdcb6e1a34639ffe21805ff9422bd7f;hb=35be38f22657bf00344e34fe75d7f3a5283832c1;hp=d06e9a4bf5197b0da61bc34efe335e984222bfc3;hpb=9cd69dd86ed337478461241d497265ccc59f819a;p=helm.git diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index d06e9a4bf..fdb1114fa 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -69,18 +69,18 @@ let incr_depth = function let compute_term pos term = let rec aux (pos: position) set = function - | Cic.Rel _ -> + | Cic.Rel _ + | Cic.Var _ -> if is_main_pos pos then 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 set term) + | Some term -> aux (next_pos pos) set term) set local_context | Cic.Sort sort -> @@ -106,9 +106,9 @@ let compute_term pos term = 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 set source in - aux pos 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 set (CicSubstitution.subst term target) @@ -158,28 +158,103 @@ let compute_term pos term = in aux pos S.empty term -let compute_type uri typeno (name, _, ty, constructors) = +module OrderedInt = +struct + type t = int + let compare = Pervasives.compare +end + +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 (Some 0)) 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 (Some 0)) 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 (Some 0)) 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 @@ -204,3 +279,44 @@ let compute ~body ~ty = 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