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
25 (* current complexity *)
31 let status = new P.status
34 let u = U.uri_of_string str in
35 if US.mem u !O.names then Printf.eprintf "probe: name clash: %S\n" str;
36 O.names := US.add u !O.names
38 let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
40 let add_ind n = O.add_xflavour n `Inductive
42 let rec set_list c ts cts =
43 let map cts t = (c, t) :: cts in
44 L.fold_left map cts ts
46 let set_funs c rfs cts =
47 let map cts (_, s, _, t0, t1) =
49 set_list c [t0; t1] cts
51 L.fold_left map cts rfs
53 let set_type c cts (_, s, t, css) =
54 let map cts (_, s, t) = add_name s; (c, t) :: cts in
55 add_name s; (c, t) :: L.fold_left map cts css
57 let inc st = {st with c = succ st.c}
59 let add st c = {st with c = st.c + c}
61 let scan_lref st c i =
62 try match List.nth c (pred i) with
63 | _, C.Decl _ -> inc st
68 let scan_gref st = function
71 | R.Ref (u, R.Con _) ->
76 | R.Ref (u, R.CoFix _) ->
78 if US.mem u !O.objs then st else inc st
80 let rec scan_term st = function
83 | (_, C.Implicit _) :: tl -> scan_term st tl
84 | (_, C.Sort _) :: tl -> scan_term (inc st) tl
85 | (c, C.Rel i) :: tl -> scan_term (scan_lref st c i) tl
86 | (_, C.Const p) :: tl -> scan_term (scan_gref st p) tl
87 | (_, C.Appl []) :: tl -> X.malformed ()
88 | (c, C.Appl ts) :: tl ->
89 scan_term (add st (pred (L.length ts))) (set_list c ts tl)
90 | (c, C.Match (_, t0, t1, ts)) :: tl ->
91 scan_term st (set_list c (t0::t1::ts) tl)
92 | (c, C.Prod (s, t0, t1)) :: tl
93 | (c, C.Lambda (s, t0, t1)) :: tl ->
94 scan_term (inc st) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl)
95 | (c, C.LetIn (s, t0, t1, t2)) :: tl ->
96 scan_term st ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl)
100 let _, _, _, _, obj = E.get_checked_obj status u in
101 let st = match obj with
102 | C.Constant (_, s, None, t, m) ->
103 add_name s; add_attr 1 m;
104 scan_term (inc st) [[], t]
105 | C.Constant (_, s, Some t0, t1, m) ->
106 add_name s; add_attr 1 m;
107 scan_term (inc st) (set_list [] [t0; t1] [])
108 | C.Fixpoint (_, rfs, m) ->
109 add_attr (L.length rfs) m;
110 scan_term (add st (L.length rfs)) (set_funs [] rfs [])
111 | C.Inductive (_, _, its, _) ->
112 add_ind (L.length its);
113 let cts = L.fold_left (set_type []) [] its in
114 scan_term (add st (L.length cts)) cts
119 let _, _, _, _, obj = E.get_checked_obj status u in
120 let g = match obj with
121 | C.Constant (_, _, _, _, (g, _, _))
122 | C.Fixpoint (_, _, (g, _, _))
123 | C.Inductive (_, _, _, (g, _)) -> g
125 if L.mem g !O.exclude then false else true
128 if !O.exclude <> [] then
129 O.objs := US.filter accept_obj !O.objs;
130 O.net := US.fold scan_obj !O.objs !O.net