]> matita.cs.unibo.it Git - helm.git/commitdiff
CicInspect: a function for counting the nodes of a term has been activated
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 13 May 2007 12:59:43 +0000 (12:59 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 13 May 2007 12:59:43 +0000 (12:59 +0000)
Procedural: reports on node counting in proof terms are aveilable

helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralHelpers.ml
helm/software/components/acic_procedural/proceduralHelpers.mli
helm/software/components/acic_procedural/proceduralOptimizer.ml
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/acic_procedural/proceduralTypes.mli
helm/software/components/cic/cicInspect.ml
helm/software/components/cic/cicInspect.mli

index 18e1ecc5b3826b5a287bf3cd13f14c6fc443993a..4ccb78ace32522efbd43d8b9706bbe7f81deca71 100644 (file)
@@ -25,7 +25,6 @@
 
 module C    = Cic
 module I    = CicInspect
-module D    = Deannotate
 module S    = CicSubstitution
 module TC   = CicTypeChecker 
 module Un   = CicUniv
@@ -60,8 +59,6 @@ type status = {
 
 (* helpers ******************************************************************)
 
-let cic = D.deannotate_term
-
 let split2_last l1 l2 =
 try
    let n = pred (List.length l1) in
@@ -155,7 +152,7 @@ with Invalid_argument _ -> failwith "A2P.get_sort"
 *)
 let get_type msg st bo =
 try   
-   let ty, _ = TC.type_of_aux' [] st.context (cic bo) Un.empty_ugraph in
+   let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
    ty
 with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
 
@@ -199,7 +196,7 @@ let convert st ?name v =
       | None            -> []
       | Some (sty, ety) ->
         let e = Cn.hole "" in
-         let csty, cety = cic sty, cic ety in
+         let csty, cety = H.cic sty, H.cic ety in
         if Ut.alpha_equivalence csty cety then [] else 
         match name with
            | None         -> [T.Change (sty, ety, None, e, "")]
@@ -252,18 +249,18 @@ let mk_rewrite st dtext what qs tl direction =
    [T.Rewrite (direction, what, None, e, dtext); T.Branch (qs, "")]
 
 let rec proc_lambda st name v t =
-   let dno = DTI.does_not_occur 1 (cic t) in
+   let dno = DTI.does_not_occur 1 (H.cic t) in
    let dno = dno && match get_inner_types st t with
       | None          -> true
       | Some (it, et) -> 
-         DTI.does_not_occur 1 (cic it) && DTI.does_not_occur 1 (cic et)
+         DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
    in
    let name = match dno, name with
       | true, _            -> C.Anonymous
       | false, C.Anonymous -> H.mk_fresh_name st.context used_premise 
       | false, name        -> name
    in
-   let entry = Some (name, C.Decl (cic v)) in
+   let entry = Some (name, C.Decl (H.cic v)) in
    let intro = get_intro name in
    proc_proof (add st entry intro) t
 
@@ -282,9 +279,9 @@ and proc_letin st what name v t =
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
                  st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
-           st, C.Decl (cic ity), rqv
+           st, C.Decl (H.cic ity), rqv
         | None          ->
-           st, C.Def (cic v, None), [T.LetIn (intro, v, dtext)]
+           st, C.Def (H.cic v, None), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in
       let qt = proc_proof (next (add st entry intro)) t in
@@ -312,12 +309,12 @@ and proc_appl st what hd tl =
       let classes, rc = Cl.classify st.context ty in
       let goal_arity = match get_inner_types st what with
          | None          -> 0
-        | Some (ity, _) -> snd (PEH.split_with_whd (st.context, cic ity))
+        | Some (ity, _) -> snd (PEH.split_with_whd (st.context, H.cic ity))
       in
       let parsno, argsno = List.length classes, List.length tl in
       let decurry = parsno - argsno in
       let diff = goal_arity - decurry in
-      if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd)));
+      if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (H.cic hd)));
       let rec mk_synth a n =
          if n < 0 then a else mk_synth (I.S.add n a) (pred n)
       in
@@ -358,12 +355,12 @@ and proc_other st what =
 and proc_proof st t = 
    let f st =
       let xtypes, note = match get_inner_types st t with
-         | Some (it, et) -> Some (cic it, cic et), 
+         | Some (it, et) -> Some (H.cic it, H.cic et), 
          (Printf.sprintf "\nInferred: %s\nExpected: %s"
-         (Pp.ppterm (cic it)) (Pp.ppterm (cic et))) 
+         (Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et))) 
          | None          -> None, "\nNo types"
       in
-      let context, clears = Cn.get_clears st.context (cic t) xtypes in
+      let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
       let note = Pp.ppcontext st.context ^ note in
       {st with context = context; clears = clears; clears_note = note}
    in
@@ -409,8 +406,8 @@ let is_theorem pars =
 let proc_obj st = function
    | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
       let ast = proc_proof st v in
-      let count = T.count_steps 0 ast in
-      let text = Printf.sprintf "tactics: %u" count in
+      let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
+      let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
       T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
       failwith "not a theorem"
index d08dca7013501224c797916efc26ccbfdef3f1ea..0925289e250111e1921fd9d7daeadff63c6c9eb0 100644 (file)
@@ -31,6 +31,7 @@ module TC   = CicTypeChecker
 module PEH  = ProofEngineHelpers
 module E    = CicEnvironment
 module UM   = UriManager
+module D    = Deannotate
 
 (* fresh name generator *****************************************************)
 
@@ -149,3 +150,5 @@ let get_ind_parameters c t =
       | _             -> assert false
    in
    ps, disp
+
+let cic = D.deannotate_term
index 84844942ae36807410ec7cf594da05e960cd570b..881f7e26635c192968d862c64f721ac0b3890e26 100644 (file)
@@ -49,3 +49,4 @@ val get_default_eliminator:
   Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term
 val get_ind_parameters:
    Cic.context -> Cic.term -> Cic.term list * int
+val cic: Cic.annterm -> Cic.term
index ab15d70872aeccf94f99493eabc8511a577dbfb1..93cb165452d1996d5d375c9d274f1679e4b6e956 100644 (file)
@@ -261,7 +261,8 @@ and opt2_term g c t =
 let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
       let g bo = 
-         Printf.eprintf "Optimized: %s\n" (Pp.ppterm bo);
+         Printf.eprintf "Optimized: %s\nNodes    : %u" 
+           (Pp.ppterm bo) (I.count_nodes 0 bo);
         let _ = H.get_type [] (C.Cast (bo, ty)) in
         C.Constant (name, Some bo, ty, pars, attrs)
       in
index bc725d118f1124d3d2d3adf22492677a20a797cc..2d3c915f7234e7ed8b7437086277ec4d77740d85 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-module H = HExtlib
-module C = Cic
-module G = GrafiteAst
-module N = CicNotationPt
+module HEL = HExtlib
+module C   = Cic
+module I   = CicInspect
+module G   = GrafiteAst
+module N   = CicNotationPt
+
+module H   = ProceduralHelpers
 
 (* functions to be moved ****************************************************)
 
@@ -83,7 +86,7 @@ let mk_arel i b = Cic.ARel ("", "", i, b)
 
 (* grafite ast constructors *************************************************)
 
-let floc = H.dummy_floc
+let floc = HEL.dummy_floc
 
 let mk_note str = G.Comment (floc, G.Note (floc, str))
 
@@ -219,3 +222,23 @@ let rec count_step a = function
    | _               -> succ a   
 
 and count_steps a = List.fold_left count_step a
+
+let rec count_node a = function
+   | Note _
+   | Theorem _   
+   | Qed _
+   | Id _
+   | Intros _
+   | Clear _
+   | ClearBody _             -> a
+   | Cut (_, t, _)
+   | LetIn (_, t, _)
+   | Apply (t, _)            -> I.count_nodes a (H.cic t)
+   | Rewrite (_, t, _, p, _)
+   | Elim (t, _, p, _)
+   | Change (t, _, _, p, _)  -> 
+      let a = I.count_nodes a (H.cic t) in
+      I.count_nodes a (H.cic p) 
+   | Branch (ss, _)          -> List.fold_left count_nodes a ss
+
+and count_nodes a = List.fold_left count_node a
index cc5d75caf2918cec3f10beffe680905441b135eb..c493873ff2b0fd736c56d5fc26082f9acb811b48 100644 (file)
@@ -66,3 +66,6 @@ val render_steps:
 
 val count_steps:
    int -> step list -> int
+
+val count_nodes:
+   int -> step list -> int
index 3d5d65d59a48e0cbae302ee6d715cd3b653d1f50..a1e94e247649f4fd6e5cd3237d3f15a4fd918fa3 100644 (file)
@@ -109,3 +109,35 @@ let get_mutinds_of_uri u t =
    in
    let g a = a in
    aux g t S.empty
+
+let rec aux n = function
+   | C.Sort _
+   | C.Implicit _
+   | C.Rel _                      -> succ n
+   | C.Appl ts                    -> List.fold_left aux (succ n) ts
+   | C.Const (_, ss)
+   | C.MutConstruct (_, _, _, ss)
+   | C.MutInd (_, _, ss)
+   | C.Var (_, ss)                -> 
+      let map n (_, t) = aux n t in 
+      List.fold_left map (succ n) ss
+   | C.Meta (_, ss)               ->
+      let map n = function 
+        | None   -> n
+        | Some t -> aux n t
+      in
+      List.fold_left map (succ n) ss
+   | C.Cast (t1, t2)
+   | C.LetIn (_, t1, t2)
+   | C.Lambda (_, t1, t2)
+   | C.Prod (_, t1, t2)           -> aux (aux (succ n) t2) t1
+   | C.MutCase (_, _, t1, t2, ss) ->
+      aux (aux (List.fold_left aux (succ n) ss) t2) t1
+   | C.Fix (_, ss)                ->
+      let map n (_, _, t1, t2) = aux (aux n t2) t1 in
+      List.fold_left map (succ n) ss
+   | C.CoFix (_, ss)              ->
+      let map n (_, t1, t2) = aux (aux n t2) t1 in
+      List.fold_left map (succ n) ss
+
+let count_nodes = aux
index c4bcd8aaf060a8e54216e9faf68455f3aa2a6d79..e7ee2ed8dd72adcef986ecf401336a57cf981907 100644 (file)
@@ -30,3 +30,6 @@ val overlaps: S.t -> S.t -> bool
 val get_rels_from_premise: int -> Cic.term -> S.t
 
 val get_mutinds_of_uri: UriManager.uri -> Cic.term -> S.t
+
+(* count_nodes n t returns n + the number of nodes in t *)
+val count_nodes: int -> Cic.term -> int