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
24 (* current complexity *)
30 let status = new P.status
33 failwith "probe: malformed term"
35 let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
37 let add_ind n = O.add_xflavour n `Inductive
39 let rec set_list c ts cts =
40 let map cts t = (c, t) :: cts in
41 L.fold_left map cts ts
43 let set_funs c rfs cts =
44 let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in
45 L.fold_left map cts rfs
47 let set_type c cts (_, _, t, css) =
48 let map cts (_, _, t) = (c, t) :: cts in
49 (c, t) :: L.fold_left map cts css
51 let inc st = {st with c = succ st.c}
53 let add st c = {st with c = st.c + c}
55 let scan_lref st c i =
56 try match List.nth c (pred i) with
57 | _, C.Decl _ -> inc st
62 let scan_gref st = function
65 | R.Ref (u, R.Con _) ->
70 | R.Ref (u, R.CoFix _) ->
72 if US.mem u !O.objs then st else inc st
74 let rec scan_term st = function
77 | (_, C.Implicit _) :: tl -> scan_term st tl
78 | (_, C.Sort _) :: tl -> scan_term (inc st) tl
79 | (c, C.Rel i) :: tl -> scan_term (scan_lref st c i) tl
80 | (_, C.Const p) :: tl -> scan_term (scan_gref st p) tl
81 | (_, C.Appl []) :: tl -> malformed ()
82 | (c, C.Appl ts) :: tl ->
83 scan_term (add st (pred (L.length ts))) (set_list c ts tl)
84 | (c, C.Match (_, t0, t1, ts)) :: tl ->
85 scan_term st (set_list c (t0::t1::ts) tl)
86 | (c, C.Prod (s, t0, t1)) :: tl
87 | (c, C.Lambda (s, t0, t1)) :: tl ->
88 scan_term (inc st) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl)
89 | (c, C.LetIn (s, t0, t1, t2)) :: tl ->
90 scan_term st ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl)
94 let _, _, _, _, obj = E.get_checked_obj status u in
95 let st = match obj with
96 | C.Constant (_, _, None, t, m) ->
98 scan_term (inc st) [[], t]
99 | C.Constant (_, _, Some t0, t1, m) ->
101 scan_term (inc st) (set_list [] [t0; t1] [])
102 | C.Fixpoint (_, rfs, m) ->
103 add_attr (L.length rfs) m;
104 scan_term (add st (L.length rfs)) (set_funs [] rfs [])
105 | C.Inductive (_, _, its, _) ->
106 add_ind (L.length its);
107 let cts = L.fold_left (set_type []) [] its in
108 scan_term (add st (L.length cts)) cts
113 let _, _, _, _, obj = E.get_checked_obj status u in
114 let g = match obj with
115 | C.Constant (_, _, _, _, (g, _, _))
116 | C.Fixpoint (_, _, (g, _, _))
117 | C.Inductive (_, _, _, (g, _)) -> g
119 if L.mem g !O.exclude then false else true
122 if !O.exclude <> [] then
123 O.objs := US.filter accept_obj !O.objs;
124 O.net := US.fold scan_obj !O.objs !O.net