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 US = U.UriSet
  16 module R  = NReference
  17 module C  = NCic
  18 module P  = NCicPp
  19 module E  = NCicEnvironment
  20
  21 module O  = Options
  22
  23 let status = new P.status
  24
  25 let malformed () =
  26    failwith "probe: malformed term"
  27
  28 let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
  29
  30 let add_ind n = O.add_xflavour n `Inductive
  31
  32 let rec set_list c ts cts =
  33    let map cts t = (c, t) :: cts in
  34    L.fold_left map cts ts
  35
  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
  39
  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
  43
  44 let scan_lref a c i =
  45    try match List.nth c (pred i) with
  46       | _, C.Decl _ -> succ a
  47       | _, C.Def  _ -> a
  48    with
  49       | Failure _ -> succ a
  50
  51 let scan_gref a = function
  52    | R.Ref (_, R.Decl)
  53    | R.Ref (_, R.Ind _)
  54    | R.Ref (_, R.Con _)   -> succ a
  55    | R.Ref (u, R.Def _)
  56    | R.Ref (u, R.Fix _)
  57    | R.Ref (u, R.CoFix _) ->
  58       if US.mem u !O.objs then a else succ a
  59
  60 let rec scan_term a = function
  61    | []                                 -> a
  62    | (_, C.Meta _)                :: tl
  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)
  77
  78 let scan_obj u a =
  79    let _, _, _, _, obj = E.get_checked_obj status u in
  80    match obj with
  81       | C.Constant (_, _, None, t, m)     ->
  82          add_attr 1 m;
  83          scan_term (succ a) [[], t]
  84       | C.Constant (_, _, Some t0, t1, m) ->
  85          add_attr 1 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
  94
  95 let accept_obj u =
  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
 101    in
 102    if L.mem g !O.exclude then false else true
 103
 104 let scan () =
 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