2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
19 module E = NCicEnvironment
23 let status = new P.status
26 failwith "probe: malformed term"
28 let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
30 let add_ind n = O.add_xflavour n `Inductive
32 let rec set_list c ts cts =
33 let map cts t = (c, t) :: cts in
34 L.fold_left map cts ts
36 let set_funs c rfs cts =
37 let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in
38 L.fold_left map cts rfs
40 let set_type c cts (_, _, t, css) =
41 let map cts (_, _, t) = (c, t) :: cts in
42 (c, t) :: L.fold_left map cts css
45 try match List.nth c (pred i) with
46 | _, C.Decl _ -> succ a
51 let scan_gref a = function
54 | R.Ref (_, R.Con _) -> succ a
57 | R.Ref (u, R.CoFix _) ->
58 if US.mem u !O.objs then a else succ a
60 let rec scan_term a = function
63 | (_, C.Implicit _) :: tl -> scan_term a tl
64 | (_, C.Sort _) :: tl -> scan_term (succ a) tl
65 | (c, C.Rel i) :: tl -> scan_term (scan_lref a c i) tl
66 | (_, C.Const p) :: tl -> scan_term (scan_gref a p) tl
67 | (_, C.Appl []) :: tl -> malformed ()
68 | (c, C.Appl ts) :: tl ->
69 scan_term (L.length ts + pred a) (set_list c ts tl)
70 | (c, C.Match (_, t0, t1, ts)) :: tl ->
71 scan_term a (set_list c (t0::t1::ts) tl)
72 | (c, C.Prod (s, t0, t1)) :: tl
73 | (c, C.Lambda (s, t0, t1)) :: tl ->
74 scan_term (succ a) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl)
75 | (c, C.LetIn (s, t0, t1, t2)) :: tl ->
76 scan_term a ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl)
79 let _, _, _, _, obj = E.get_checked_obj status u in
81 | C.Constant (_, _, None, t, m) ->
83 scan_term (succ a) [[], t]
84 | C.Constant (_, _, Some t0, t1, m) ->
86 scan_term (succ a) (set_list [] [t0; t1] [])
87 | C.Fixpoint (_, rfs, m) ->
88 add_attr (L.length rfs) m;
89 scan_term (a + L.length rfs) (set_funs [] rfs [])
90 | C.Inductive (_, _, its, _) ->
91 add_ind (L.length its);
92 let cts = L.fold_left (set_type []) [] its in
93 scan_term (a + L.length cts) cts
96 let _, _, _, _, obj = E.get_checked_obj status u in
97 let g = match obj with
98 | C.Constant (_, _, _, _, (g, _, _))
99 | C.Fixpoint (_, _, (g, _, _))
100 | C.Inductive (_, _, _, (g, _)) -> g
102 if L.mem g !O.exclude then false else true
105 if !O.exclude <> [] then
106 O.objs := US.filter accept_obj !O.objs;
107 O.net := US.fold scan_obj !O.objs !O.net