From: Ferruccio Guidi Date: Sun, 13 May 2007 12:59:43 +0000 (+0000) Subject: CicInspect: a function for counting the nodes of a term has been activated X-Git-Tag: make_still_working~6338 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf4301b669442bdd78984d3a3a1e38660db1f2ea;p=helm.git CicInspect: a function for counting the nodes of a term has been activated Procedural: reports on node counting in proof terms are aveilable --- diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 18e1ecc5b..4ccb78ace 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -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" diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index d08dca701..0925289e2 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -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 diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 84844942a..881f7e266 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -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 diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index ab15d7087..93cb16545 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -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 diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index bc725d118..2d3c915f7 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -23,10 +23,13 @@ * 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 diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index cc5d75caf..c493873ff 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/components/acic_procedural/proceduralTypes.mli @@ -66,3 +66,6 @@ val render_steps: val count_steps: int -> step list -> int + +val count_nodes: + int -> step list -> int diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml index 3d5d65d59..a1e94e247 100644 --- a/helm/software/components/cic/cicInspect.ml +++ b/helm/software/components/cic/cicInspect.ml @@ -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 diff --git a/helm/software/components/cic/cicInspect.mli b/helm/software/components/cic/cicInspect.mli index c4bcd8aaf..e7ee2ed8d 100644 --- a/helm/software/components/cic/cicInspect.mli +++ b/helm/software/components/cic/cicInspect.mli @@ -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