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 type status = {
  24 (* current complexity *)
  25   c: int;
  26 (* current uri *)
  27   u: U.uri;
  28 }
  29
  30 let status = new P.status
  31
  32 let malformed () =
  33   failwith "probe: malformed term"
  34
  35 let add_name str =
  36   let u = U.uri_of_string str in
  37   if US.mem u !O.names then Printf.eprintf "probe: name clash: %S\n" str;
  38   O.names := US.add u !O.names
  39
  40 let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour)
  41
  42 let add_ind n = O.add_xflavour n `Inductive
  43
  44 let rec set_list c ts cts =
  45   let map cts t = (c, t) :: cts in
  46   L.fold_left map cts ts
  47
  48 let set_funs c rfs cts =
  49   let map cts (_, s, _, t0, t1) =
  50     add_name s;
  51     set_list c [t0; t1] cts
  52   in
  53   L.fold_left map cts rfs
  54
  55 let set_type c cts (_, s, t, css) =
  56   let map cts (_, s, t) = add_name s; (c, t) :: cts in
  57   add_name s; (c, t) :: L.fold_left map cts css
  58
  59 let inc st = {st with c = succ st.c}
  60
  61 let add st c = {st with c = st.c + c}
  62
  63 let scan_lref st c i =
  64   try match List.nth c (pred i) with
  65     | _, C.Decl _ -> inc st
  66     | _, C.Def  _ -> st
  67   with
  68     | Failure _ -> inc st
  69
  70 let scan_gref st = function
  71   | R.Ref (u, R.Decl)
  72   | R.Ref (u, R.Ind _)
  73   | R.Ref (u, R.Con _)   ->
  74     O.add_dep st.u u;
  75     inc st
  76   | R.Ref (u, R.Def _)
  77   | R.Ref (u, R.Fix _)
  78   | R.Ref (u, R.CoFix _) ->
  79     O.add_dep st.u u;
  80     if US.mem u !O.objs then st else inc st
  81
  82 let rec scan_term st = function
  83   | []                                 -> st
  84   | (_, C.Meta _)                :: tl
  85   | (_, C.Implicit _)            :: tl -> scan_term st tl
  86   | (_, C.Sort _)                :: tl -> scan_term (inc st) tl
  87   | (c, C.Rel i)                 :: tl -> scan_term (scan_lref st c i) tl
  88   | (_, C.Const p)               :: tl -> scan_term (scan_gref st p) tl
  89   | (_, C.Appl [])               :: tl -> malformed ()
  90   | (c, C.Appl ts)               :: tl ->
  91     scan_term (add st (pred (L.length ts))) (set_list c ts tl)
  92   | (c, C.Match (_, t0, t1, ts)) :: tl ->
  93     scan_term st (set_list c (t0::t1::ts) tl)
  94   | (c, C.Prod (s, t0, t1))      :: tl
  95   | (c, C.Lambda (s, t0, t1))    :: tl ->
  96     scan_term (inc st) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl)
  97   | (c, C.LetIn (s, t0, t1, t2)) :: tl ->
  98     scan_term st ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl)
  99
 100 let scan_obj u c =
 101   let st = {c; u} in
 102   let _, _, _, _, obj = E.get_checked_obj status u in
 103   let st = match obj with
 104     | C.Constant (_, s, None, t, m)     ->
 105       add_name s; add_attr 1 m;
 106       scan_term (inc st) [[], t]
 107     | C.Constant (_, s, Some t0, t1, m) ->
 108       add_name s; add_attr 1 m;
 109       scan_term (inc st) (set_list [] [t0; t1] [])
 110     | C.Fixpoint (_, rfs, m)            ->
 111       add_attr (L.length rfs) m;
 112       scan_term (add st (L.length rfs)) (set_funs [] rfs [])
 113     | C.Inductive (_, _, its, _)        ->
 114       add_ind (L.length its);
 115       let cts = L.fold_left (set_type []) [] its in
 116       scan_term (add st (L.length cts)) cts
 117   in
 118   st.c
 119
 120 let accept_obj u =
 121   let _, _, _, _, obj = E.get_checked_obj status u in
 122   let g = match obj with
 123     | C.Constant (_, _, _, _, (g, _, _))
 124     | C.Fixpoint (_, _, (g, _, _))
 125     | C.Inductive (_, _, _, (g, _))    -> g
 126   in
 127   if L.mem g !O.exclude then false else true
 128
 129 let scan () =
 130   if !O.exclude <> [] then
 131     O.objs := US.filter accept_obj !O.objs;
 132   O.net := US.fold scan_obj !O.objs !O.net