X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fprobe%2FnCicScan.ml;h=f1c2772ec14665a40d213bfeec495423150c51ff;hp=fc6957292645700ec33c5b340e09aad9f8df98c9;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hpb=bfd440cc2a790741616cae6b375609c6bbdc3b24 diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml index fc6957292..f1c2772ec 100644 --- a/matita/components/binaries/probe/nCicScan.ml +++ b/matita/components/binaries/probe/nCicScan.ml @@ -20,88 +20,105 @@ module E = NCicEnvironment module O = Options +type status = { +(* current complexity *) + c: int; +(* current uri *) + u: U.uri; +} + let status = new P.status let malformed () = - failwith "probe: malformed term" + failwith "probe: malformed term" let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour) let add_ind n = O.add_xflavour n `Inductive let rec set_list c ts cts = - let map cts t = (c, t) :: cts in - L.fold_left map cts ts + 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 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 US.mem 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 u a = - let _, _, _, _, obj = E.get_checked_obj status u in - match obj with - | C.Constant (_, _, None, t, m) -> - add_attr 1 m; - scan_term (succ a) [[], t] - | C.Constant (_, _, Some t0, t1, m) -> - add_attr 1 m; - scan_term (succ a) (set_list [] [t0; t1] []) - | C.Fixpoint (_, rfs, m) -> - add_attr (L.length rfs) m; - scan_term (a + L.length rfs) (set_funs [] rfs []) - | C.Inductive (_, _, its, _) -> - add_ind (L.length 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 := US.filter accept_obj !O.objs; - O.net := US.fold scan_obj !O.objs !O.net + let map cts (_, _, t) = (c, t) :: cts in + (c, t) :: L.fold_left map cts css + +let inc st = {st with c = succ st.c} + +let add st c = {st with c = st.c + c} + +let scan_lref st c i = + try match List.nth c (pred i) with + | _, C.Decl _ -> inc st + | _, C.Def _ -> st + with + | Failure _ -> inc st + +let scan_gref st = function + | R.Ref (u, R.Decl) + | R.Ref (u, R.Ind _) + | R.Ref (u, R.Con _) -> + O.add_dep st.u u; + inc st + | R.Ref (u, R.Def _) + | R.Ref (u, R.Fix _) + | R.Ref (u, R.CoFix _) -> + O.add_dep st.u u; + if US.mem u !O.objs then st else inc st + +let rec scan_term st = function + | [] -> st + | (_, C.Meta _) :: tl + | (_, C.Implicit _) :: tl -> scan_term st tl + | (_, C.Sort _) :: tl -> scan_term (inc st) tl + | (c, C.Rel i) :: tl -> scan_term (scan_lref st c i) tl + | (_, C.Const p) :: tl -> scan_term (scan_gref st p) tl + | (_, C.Appl []) :: tl -> malformed () + | (c, C.Appl ts) :: tl -> + scan_term (add st (pred (L.length ts))) (set_list c ts tl) + | (c, C.Match (_, t0, t1, ts)) :: tl -> + scan_term st (set_list c (t0::t1::ts) tl) + | (c, C.Prod (s, t0, t1)) :: tl + | (c, C.Lambda (s, t0, t1)) :: tl -> + scan_term (inc st) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl) + | (c, C.LetIn (s, t0, t1, t2)) :: tl -> + scan_term st ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl) + +let scan_obj u c = + let st = {c; u} in + let _, _, _, _, obj = E.get_checked_obj status u in + let st = match obj with + | C.Constant (_, _, None, t, m) -> + add_attr 1 m; + scan_term (inc st) [[], t] + | C.Constant (_, _, Some t0, t1, m) -> + add_attr 1 m; + scan_term (inc st) (set_list [] [t0; t1] []) + | C.Fixpoint (_, rfs, m) -> + add_attr (L.length rfs) m; + scan_term (add st (L.length rfs)) (set_funs [] rfs []) + | C.Inductive (_, _, its, _) -> + add_ind (L.length its); + let cts = L.fold_left (set_type []) [] its in + scan_term (add st (L.length cts)) cts + in + st.c + +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 := US.filter accept_obj !O.objs; + O.net := US.fold scan_obj !O.objs !O.net