- probe: new application to compute some data on the proof objects of

[helm.git] / matita / components / binaries / probe / nCicScan.ml

diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml
new file mode 100644 (file)
index 0000000..a289af8
--- /dev/null
+++ b/matita/components/binaries/probe/nCicScan.ml
@@ -0,0 +1,98 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+module L = List
+
+module U = NUri
+module R = NReference
+module C = NCic
+module P = NCicPp
+module E = NCicEnvironment
+
+module O = Options
+
+let status = new P.status
+
+let malformed () =
+   failwith "probe: malformed term"
+
+let rec set_list c ts cts =
+   let map cts t = (c, t) :: cts in
+   L.fold_left map cts ts
+
+let set_funs c rfs cts =
+   let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in
+   L.fold_left map cts rfs
+
+let set_type c cts (_, _, t, css) =
+   let map cts (_, _, t) = (c, t) :: cts in 
+   (c, t) :: L.fold_left map cts css 
+
+let scan_lref a c i = 
+   try match List.nth c (pred i) with
+      | _, C.Decl _ -> succ a
+      | _, C.Def  _ -> a
+   with 
+      | Failure _ -> succ a 
+
+let scan_gref a = function
+   | R.Ref (_, R.Decl) 
+   | R.Ref (_, R.Ind _)
+   | R.Ref (_, R.Con _)   -> succ a
+   | R.Ref (u, R.Def _)
+   | R.Ref (u, R.Fix _)
+   | R.Ref (u, R.CoFix _) ->
+      if L.exists (U.eq u) !O.objs then a else succ a
+
+let rec scan_term a = function
+   | []                                 -> a
+   | (_, C.Meta _)                :: tl
+   | (_, C.Implicit _)            :: tl -> scan_term a tl
+   | (_, C.Sort _)                :: tl -> scan_term (succ a) tl
+   | (c, C.Rel i)                 :: tl -> scan_term (scan_lref a c i) tl
+   | (_, C.Const p)               :: tl -> scan_term (scan_gref a p) tl
+   | (_, C.Appl [])               :: tl -> malformed ()
+   | (c, C.Appl ts)               :: tl ->
+      scan_term (L.length ts + pred a) (set_list c ts tl)
+   | (c, C.Match (_, t0, t1, ts)) :: tl ->
+      scan_term a (set_list c (t0::t1::ts) tl)   
+   | (c, C.Prod (s, t0, t1))      :: tl
+   | (c, C.Lambda (s, t0, t1))    :: tl ->
+      scan_term (succ a) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl)
+   | (c, C.LetIn (s, t0, t1, t2)) :: tl ->
+      scan_term a ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl)
+
+let scan_obj a u = 
+   let _, _, _, _, obj = E.get_checked_obj status u in 
+   match obj with
+      | C.Constant (_, _, None, t, _)     ->
+         scan_term (succ a) [[], t]
+      | C.Constant (_, _, Some t0, t1, _) ->
+         scan_term (succ a) (set_list [] [t0; t1] [])
+      | C.Fixpoint (_, rfs, _)            ->
+         scan_term (a + L.length rfs) (set_funs [] rfs [])
+      | C.Inductive (_, _, its, _)        ->
+        let cts = L.fold_left (set_type []) [] its in
+         scan_term (a + L.length cts) cts
+
+let accept_obj u = 
+   let _, _, _, _, obj = E.get_checked_obj status u in 
+   let g = match obj with
+      | C.Constant (_, _, _, _, (g, _, _))
+      | C.Fixpoint (_, _, (g, _, _))
+      | C.Inductive (_, _, _, (g, _))    -> g
+   in
+   if L.mem g !O.exclude then false else true
+
+let scan () = 
+   if !O.exclude <> [] then 
+      O.objs := L.filter accept_obj !O.objs;
+   O.net := L.fold_left scan_obj !O.net !O.objs