From 82baf094141d9ef518d681b8cebcc180bca14d2c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 10 Jun 2009 20:19:42 +0000 Subject: [PATCH] - library/list/list.ma: unused code commented - proceduralClassify type argument are no longer critical: let's see how it goes - acic2Procedural: the inline parameter Debug now works - procedural2: we remove the conversions before first order relexivities (exp. to avoid conversion to []=[] in list/list.ma [does not work because []=[] in an open term since the equality type is unspecified]). so we we strengthen reflexivity (see below) - setoids: now reflexivity is retried after whd if it fails in the first place. - grafiteAst: detection of convertible rewrites is now optional and activated with the inline parameter "cr". nat/factorial2 is very slow without rewrites transcript: we now avoid the generation of dupplicated inlines (mistakely generated by the grafite parser [this can not be avoided without a better syntax for .ma scripts]) now list/list.ma is fully reconstructed :) nat/factorial2.ma takes long to be produced 22m31. Some conversion is slowing the process. nat/bertrand.ma also: we are waiting for it now :( --- .../acic_procedural/acic2Procedural.ml | 2 +- .../components/acic_procedural/procedural2.ml | 38 ++++++++++++++----- .../acic_procedural/proceduralClassify.ml | 2 +- .../components/binaries/transcript/engine.ml | 2 +- .../software/components/grafite/grafiteAst.ml | 5 ++- .../components/grafite/grafiteAstPp.ml | 5 ++- .../grafite_parser/grafiteParser.ml | 5 ++- helm/software/components/tactics/.depend | 8 ++-- helm/software/components/tactics/.depend.opt | 8 ++-- helm/software/components/tactics/setoids.ml | 9 +++++ helm/software/matita/library/list/list.ma | 11 ++---- 11 files changed, 60 insertions(+), 35 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 9152d7a43..2fec2dd1f 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -137,5 +137,5 @@ let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params let rec is_debug n = function | [] -> false - | G.IPDebug debug :: _ -> debug <= n + | G.IPDebug debug :: _ -> n <= debug | _ :: tl -> is_debug n tl diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 826cfb986..07c1da5f0 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -54,6 +54,7 @@ type status = { max_depth: int option; depth : int; defaults : bool; + cr : bool; context : C.context; case : int list } @@ -169,13 +170,20 @@ let get_sub_names head l = let get_type msg st t = H.get_type msg st.context (H.cic t) let get_uri_of_head = function - | C.AConst (_, u, _) - | C.AAppl (_, C.AConst (_, u, _) :: _) -> Some (u, 0, 0) - | C.AMutInd (_, u, i, _) - | C.AAppl (_, C.AMutInd (_, u, i, _) :: _) -> Some (u, succ i, 0) - | C.AMutConstruct (_, u, i, j, _) - | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: _) -> Some (u, succ i, j) - | _ -> None + | C.AConst (_, u, _) -> + Some (u, 0, 0, 0) + | C.AAppl (_, C.AConst (_, u, _) :: vs) -> + Some (u, 0, 0, List.length vs) + | C.AMutInd (_, u, i, _) -> + Some (u, succ i, 0, 0) + | C.AAppl (_, C.AMutInd (_, u, i, _) :: vs) -> + Some (u, succ i, 0, List.length vs) + | C.AMutConstruct (_, u, i, j, _) -> + Some (u, succ i, j, 0) + | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: vs) -> + Some (u, succ i, j, List.length vs) + | _ -> + None let get_uri_of_apply = function | T.Exact (t, _) @@ -184,8 +192,15 @@ let get_uri_of_apply = function let is_reflexivity st step = match get_uri_of_apply step with - | None -> false - | Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 + | None -> false + | Some (uri, i, j, n) -> + st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 && n = 0 + +let is_ho_reflexivity st step = + match get_uri_of_apply step with + | None -> false + | Some (uri, i, j, n) -> + st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1 && n > 0 let are_convertible st pred sx dx = let pred, sx, dx = H.cic pred, H.cic sx, H.cic dx in @@ -259,6 +274,8 @@ let get_intro = function let mk_preamble st what script = match script with | step :: script when is_reflexivity st step -> + T.Reflexivity (T.note_of_step step) :: script + | step :: script when is_ho_reflexivity st step -> convert st what @ T.Reflexivity (T.note_of_step step) :: script | T.Exact _ :: _ -> script | _ -> convert st what @ script @@ -305,7 +322,7 @@ let mk_rewrite st dtext where qs tl direction t ity = let e = Cn.mk_pattern 1 ity pred in let script = [T.Branch (qs, "")] in if Cn.does_not_occur e then script else - if are_convertible st pred sx dx then + if st.cr && are_convertible st pred sx dx then let dtext = "convertible rewrite" ^ dtext in let ity, ety, e = Cn.beta sx pred, Cn.beta dx pred, Cn.hole "" in let city, cety = H.cic ity, H.cic ety in @@ -539,6 +556,7 @@ let init ~ids_to_inner_sorts ~ids_to_inner_types params context = max_depth = List.fold_left depth_map None params; depth = 0; defaults = not (List.mem G.IPNoDefaults params); + cr = List.mem G.IPCR params; context = context; case = [] } diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml index a607bf60d..6da59eed1 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.ml +++ b/helm/software/components/acic_procedural/proceduralClassify.ml @@ -90,7 +90,7 @@ try let rc = classify_conclusion vs in let map (b, h) (c, v) = let _, argsno = PEH.split_with_whd (c, v) in - let isf = argsno > 0 || H.is_sort v in + let isf = argsno > 0 (* || H.is_sort v *) in let iu = H.is_unsafe h (List.hd vs) in (I.get_rels_from_premise h v, I.S.empty, isf && iu) :: b, succ h in diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index c55a1d19c..39086d53f 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -175,7 +175,7 @@ let is_ma st name = let set_items st name items = let i = get_index st name in let script = st.scripts.(i) in - let contents = List.rev_append items script.contents in + let contents = List.rev_append (X.list_uniq items) script.contents in st.scripts.(i) <- {script with name = name; contents = contents} let set_heading st name = diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 6b9a3eba1..e86cb082f 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -150,13 +150,14 @@ type print_kind = [ `Env | `Coer ] type inline_param = IPPrefix of string (* undocumented *) | IPAs of Cic.object_flavour (* preferred flavour *) + | IPCoercions (* show coercions *) + | IPDebug of int (* set debug level *) | IPProcedural (* procedural rendering *) | IPNoDefaults (* no default-based tactics *) | IPLevel of int (* granularity level *) | IPDepth of int (* undocumented *) | IPComments (* show statistics *) - | IPCoercions (* show coercions *) - | IPDebug of int (* set debug level *) + | IPCR (* detect convertible rewriting *) type ('term,'lazy_term) macro = (* Whelp's stuff *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index cdf90c5b9..26c73eb2f 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -282,13 +282,14 @@ let pp_macro ~term_pp ~lazy_term_pp = let pp_param = function | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\"" | IPAs flavour -> flavour_pp flavour + | IPCoercions -> "coercions" + | IPDebug debug -> "debug = " ^ string_of_int debug | IPProcedural -> "procedural" | IPNoDefaults -> "nodefaults" | IPDepth depth -> "depth = " ^ string_of_int depth | IPLevel level -> "level = " ^ string_of_int level | IPComments -> "comments" - | IPCoercions -> "coercions" - | IPDebug debug -> "debug = " ^ string_of_int debug + | IPCR -> "cr" in let s = String.concat " " (List.map pp_param l) in if s = "" then s else " " ^ s diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 93cff174c..3b8435331 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -461,13 +461,14 @@ EXTEND [ params = LIST0 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix | flavour = inline_flavour -> G.IPAs flavour + | IDENT "coercions" -> G.IPCoercions + | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug | IDENT "procedural" -> G.IPProcedural | IDENT "nodefaults" -> G.IPNoDefaults | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level | IDENT "comments" -> G.IPComments - | IDENT "coercions" -> G.IPCoercions - | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug + | IDENT "cr" -> G.IPCR ] -> params ] ]; diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index f48d55ea2..169fc76b0 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -176,10 +176,10 @@ ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \ primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \ primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi -setoids.cmo: proofEngineTypes.cmi primitiveTactics.cmi equalityTactics.cmi \ - setoids.cmi -setoids.cmx: proofEngineTypes.cmx primitiveTactics.cmx equalityTactics.cmx \ - setoids.cmi +setoids.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ + primitiveTactics.cmi equalityTactics.cmi setoids.cmi +setoids.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ + primitiveTactics.cmx equalityTactics.cmx setoids.cmi fourier.cmo: fourier.cmi fourier.cmx: fourier.cmi fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index f48d55ea2..169fc76b0 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -176,10 +176,10 @@ ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \ primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \ primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi -setoids.cmo: proofEngineTypes.cmi primitiveTactics.cmi equalityTactics.cmi \ - setoids.cmi -setoids.cmx: proofEngineTypes.cmx primitiveTactics.cmx equalityTactics.cmx \ - setoids.cmi +setoids.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ + primitiveTactics.cmi equalityTactics.cmi setoids.cmi +setoids.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ + primitiveTactics.cmx equalityTactics.cmx setoids.cmi fourier.cmo: fourier.cmi fourier.cmx: fourier.cmi fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml index 265ef99aa..1ef4e483e 100644 --- a/helm/software/components/tactics/setoids.ml +++ b/helm/software/components/tactics/setoids.ml @@ -8,6 +8,10 @@ (* $Id: setoid_replace.ml 8900 2006-06-06 14:40:27Z letouzey $ *) +module T = Tacticals +module RT = ReductionTactics +module PET = ProofEngineTypes + let default_eq () = match LibraryObjects.eq_URI () with Some uri -> uri @@ -1840,6 +1844,11 @@ let setoid_reflexivity_tac = in ProofEngineTypes.mk_tactic tac +let setoid_reflexivity_tac = + let start_tac = RT.whd_tac ~pattern:(PET.conclusion_pattern None) in + let fail_tac = T.then_ ~start:start_tac ~continuation:setoid_reflexivity_tac in + T.if_ ~start:setoid_reflexivity_tac ~continuation:T.id_tac ~fail:fail_tac + let setoid_symmetry = let tac status = try diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index c6fd212be..19866cc29 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/matita/library/list/list.ma @@ -109,8 +109,8 @@ with permut1 : list A -> list A -> Prop \def | step : \forall l1,l2:list A. \forall x,y:A. permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)). -include "nat/nat.ma". - +(* + definition x1 \def S O. definition x2 \def S x1. definition x3 \def S x2. @@ -121,15 +121,9 @@ theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []). apply (step ? (x1::[]) [] x2 x3). qed. - -(* theorem nil_append_nil_both: \forall A:Type.\forall l1,l2:list A. l1 @ l2 = [] \to l1 = [] \land l2 = []. -*) - -(* -include "nat/nat.ma". theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. reflexivity. @@ -139,6 +133,7 @@ theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O]. simplify. reflexivity. qed. + *) definition nth ≝ -- 2.39.2