]> matita.cs.unibo.it Git - helm.git/blob - matita/components/binaries/probe/nCicScan.ml
- probe: new application to compute some data on the proof objects of
[helm.git] / matita / components / binaries / probe / nCicScan.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 module L = List
13
14 module U = NUri
15 module R = NReference
16 module C = NCic
17 module P = NCicPp
18 module E = NCicEnvironment
19
20 module O = Options
21
22 let status = new P.status
23
24 let malformed () =
25    failwith "probe: malformed term"
26
27 let rec set_list c ts cts =
28    let map cts t = (c, t) :: cts in
29    L.fold_left map cts ts
30
31 let set_funs c rfs cts =
32    let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in
33    L.fold_left map cts rfs
34
35 let set_type c cts (_, _, t, css) =
36    let map cts (_, _, t) = (c, t) :: cts in 
37    (c, t) :: L.fold_left map cts css 
38
39 let scan_lref a c i = 
40    try match List.nth c (pred i) with
41       | _, C.Decl _ -> succ a
42       | _, C.Def  _ -> a
43    with 
44       | Failure _ -> succ a 
45
46 let scan_gref a = function
47    | R.Ref (_, R.Decl) 
48    | R.Ref (_, R.Ind _)
49    | R.Ref (_, R.Con _)   -> succ a
50    | R.Ref (u, R.Def _)
51    | R.Ref (u, R.Fix _)
52    | R.Ref (u, R.CoFix _) ->
53       if L.exists (U.eq u) !O.objs then a else succ a
54
55 let rec scan_term a = function
56    | []                                 -> a
57    | (_, C.Meta _)                :: tl
58    | (_, C.Implicit _)            :: tl -> scan_term a tl
59    | (_, C.Sort _)                :: tl -> scan_term (succ a) tl
60    | (c, C.Rel i)                 :: tl -> scan_term (scan_lref a c i) tl
61    | (_, C.Const p)               :: tl -> scan_term (scan_gref a p) tl
62    | (_, C.Appl [])               :: tl -> malformed ()
63    | (c, C.Appl ts)               :: tl ->
64       scan_term (L.length ts + pred a) (set_list c ts tl)
65    | (c, C.Match (_, t0, t1, ts)) :: tl ->
66       scan_term a (set_list c (t0::t1::ts) tl)   
67    | (c, C.Prod (s, t0, t1))      :: tl
68    | (c, C.Lambda (s, t0, t1))    :: tl ->
69       scan_term (succ a) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl)
70    | (c, C.LetIn (s, t0, t1, t2)) :: tl ->
71       scan_term a ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl)
72
73 let scan_obj a u = 
74    let _, _, _, _, obj = E.get_checked_obj status u in 
75    match obj with
76       | C.Constant (_, _, None, t, _)     ->
77          scan_term (succ a) [[], t]
78       | C.Constant (_, _, Some t0, t1, _) ->
79          scan_term (succ a) (set_list [] [t0; t1] [])
80       | C.Fixpoint (_, rfs, _)            ->
81          scan_term (a + L.length rfs) (set_funs [] rfs [])
82       | C.Inductive (_, _, its, _)        ->
83          let cts = L.fold_left (set_type []) [] its in
84          scan_term (a + L.length cts) cts
85
86 let accept_obj u = 
87    let _, _, _, _, obj = E.get_checked_obj status u in 
88    let g = match obj with
89       | C.Constant (_, _, _, _, (g, _, _))
90       | C.Fixpoint (_, _, (g, _, _))
91       | C.Inductive (_, _, _, (g, _))    -> g
92    in
93    if L.mem g !O.exclude then false else true
94
95 let scan () = 
96    if !O.exclude <> [] then 
97       O.objs := L.filter accept_obj !O.objs;
98    O.net := L.fold_left scan_obj !O.net !O.objs