From 2e3e85acace6942eebcfac570ce6b33134d1a3dd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 24 Jan 2007 19:28:15 +0000 Subject: [PATCH] matitaGui: some missing cases during disambiguation now treated grafiteAst: rename tactic removed procedural: some improvements --- components/content_pres/acic2Procedural.ml | 102 ++++++++++++------ components/content_pres/acic2Procedural.mli | 2 +- components/content_pres/cicClassify.ml | 36 ++++--- components/content_pres/cicClassify.mli | 4 +- components/content_pres/objPp.ml | 6 +- components/content_pres/objPp.mli | 3 +- .../content_pres/proceduralConversion.ml | 29 +++++ .../content_pres/proceduralConversion.mli | 2 + components/content_pres/proceduralTypes.ml | 11 ++ components/content_pres/proceduralTypes.mli | 2 + components/grafite/grafiteAst.ml | 8 +- components/grafite/grafiteAstPp.ml | 7 +- components/grafite_engine/grafiteEngine.ml | 1 - .../grafite_parser/grafiteDisambiguate.ml | 2 - components/grafite_parser/grafiteParser.ml | 8 +- components/tactics/tactics.ml | 1 - components/tactics/tactics.mli | 3 +- matita/matitaGui.ml | 32 +++++- 18 files changed, 177 insertions(+), 82 deletions(-) diff --git a/components/content_pres/acic2Procedural.ml b/components/content_pres/acic2Procedural.ml index c92d108e5..adfe4b05c 100644 --- a/components/content_pres/acic2Procedural.ml +++ b/components/content_pres/acic2Procedural.ml @@ -45,13 +45,17 @@ type status = { prefix: string; max_depth: int option; depth: int; - entries: C.context; + context: C.context; intros: string list; ety: C.annterm option } (* helpers ******************************************************************) +let id x = x + +let comp f g x = f (g x) + let cic = D.deannotate_term let split2_last l1 l2 = @@ -80,22 +84,23 @@ let string_of_head = function | C.AMeta _ -> "meta" | C.AImplicit _ -> "implict" -let next st = {st with depth = succ st.depth; intros = []; ety = None} +let clear st = {st with intros = []; ety = None} + +let next st = {(clear st) with depth = succ st.depth} let set_ety st ety = if st.ety = None then {st with ety = ety} else st let add st entry intro ety = let st = set_ety st ety in - {st with entries = entry :: st.entries; intros = intro :: st.intros} + {st with context = entry :: st.context; intros = intro :: st.intros} let test_depth st = try let msg = Printf.sprintf "Depth %u: " st.depth in match st.max_depth with | None -> true, "" - | Some d -> - if st.depth < d then true, msg else false, "DEPTH EXCEDED" + | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: " with Invalid_argument _ -> failwith "A2P.test_depth" let is_rewrite_right = function @@ -146,6 +151,27 @@ let defined_premise = "DEFINED" let assumed_premise = "ASSUMED" +let expanded_premise = "EXPANDED" + +let eta_expand n t = + let ty = C.AImplicit ("", None) in + let name i = Printf.sprintf "%s%u" expanded_premise i in + let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in + let arg i n = T.mk_arel (n - i) (name i) in + let rec aux i f a = + if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a) + in + let absts, args = aux 0 id [] in + match Cn.lift 1 n t with + | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args)) + | t -> absts (C.AAppl ("", t :: args)) + +let appl_expand n = function + | C.AAppl (id, ts) -> + let before, after = T.list_split (List.length ts + n) ts in + C.AAppl ("", C.AAppl (id, before) :: after) + | _ -> assert false + let get_intro name t = try match name with @@ -164,17 +190,17 @@ try | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script | _ -> p1 :: script with Invalid_argument _ -> failwith "A2P.mk_intros" -(* -let rec mk_premise st dtext = function - | C.ARel (_, _, _, binder) -> [], binder - | where -> - let name = contracted_premise in - mk_fwd_proof st dtext name where, name -*) -let rec mk_fwd_rewrite st dtext name tl direction = + +let rec mk_atomic st dtext what = + if T.is_atomic what then [], what else + let name = defined_premise in + mk_fwd_proof st dtext name what, T.mk_arel 0 name + +and mk_fwd_rewrite st dtext name tl direction = let what, where = List.nth tl 5, List.nth tl 3 in let rewrite premise = - [T.Rewrite (direction, what, Some (premise, name), dtext)] + let script, what = mk_atomic st dtext what in + T.Rewrite (direction, what, Some (premise, name), dtext) :: script in match where with | C.ARel (_, _, _, binder) -> rewrite binder @@ -200,8 +226,8 @@ and mk_fwd_proof st dtext name = function let qs = [[T.Id ""]; mk_proof (next st) v] in [T.Branch (qs, ""); T.Cut (name, ity, dtext)] | None -> - let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in - let (classes, rc) as h = Cl.classify ty in + let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in + let (classes, rc) as h = Cl.classify st.context ty in let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in [T.LetIn (name, v, dtext ^ text)] end @@ -217,7 +243,7 @@ and mk_proof st = function | None -> None in mk_proof (add st entry intro ety) t - | C.ALetIn (_, name, v, t) as what -> + | C.ALetIn (_, name, v, t) as what -> let proceed, dtext = test_depth st in let script = if proceed then let entry = Some (name, C.Def (cic v, None)) in @@ -228,42 +254,51 @@ and mk_proof st = function [T.Apply (what, dtext)] in mk_intros st script - | C.ARel _ as what -> + | C.ARel _ as what -> let _, dtext = test_depth st in let text = "assumption" in let script = [T.Apply (what, dtext ^ text)] in mk_intros st script - | C.AMutConstruct _ as what -> + | C.AMutConstruct _ as what -> let _, dtext = test_depth st in let script = [T.Apply (what, dtext)] in mk_intros st script - | C.AAppl (_, hd :: tl) as t -> + | C.AAppl (_, hd :: tl) as t -> let proceed, dtext = test_depth st in let script = if proceed then - let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in - let (classes, rc) as h = Cl.classify ty in - let synth = Cl.S.singleton 0 in + let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in + let (classes, rc) as h = Cl.classify st.context ty in + let decurry = List.length classes - List.length tl in + if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else + if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else + let synth = Cl.S.singleton 0 in let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in match rc with - | Some (i, j) when i > 1 -> + | Some (i, j) when i > 1 && i <= List.length classes -> let classes, tl, _, what = split2_last classes tl in + let script, what = mk_atomic st dtext what in let synth = Cl.S.add 1 synth in let qs = mk_bkd_proofs (next st) synth classes tl in if is_rewrite_right hd then - [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")] + List.rev script @ + [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")] else if is_rewrite_left hd then - [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")] + List.rev script @ + [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")] else let using = Some hd in + List.rev script @ [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")] - | _ -> + | _ -> let qs = mk_bkd_proofs (next st) synth classes tl in - [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] + let script, hd = mk_atomic st dtext hd in + List.rev script @ + [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else [T.Apply (t, dtext)] in mk_intros st script - | t -> + | t -> let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in let script = [T.Note text] in mk_intros st script @@ -276,9 +311,6 @@ try if Cl.S.is_empty inv then Some (mk_proof st v) else Some [T.Apply (v, dtext ^ "dependent")] in - let l1, l2 = List.length classes, List.length ts in - if l1 > l2 then failwith "partial application" else - if l1 < l2 then failwith "too many arguments" else T.list_map2_filter aux classes ts with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs" @@ -299,14 +331,14 @@ let mk_obj st = function (* interface functions ******************************************************) -let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj = +let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj = let st = { sorts = ids_to_inner_sorts; types = ids_to_inner_types; prefix = prefix; - max_depth = None; + max_depth = depth; depth = 0; - entries = []; + context = []; intros = []; ety = None } in diff --git a/components/content_pres/acic2Procedural.mli b/components/content_pres/acic2Procedural.mli index 50fb60898..d1ff6a0c2 100644 --- a/components/content_pres/acic2Procedural.mli +++ b/components/content_pres/acic2Procedural.mli @@ -26,7 +26,7 @@ val acic2procedural: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> - string -> Cic.annobj -> + ?depth:int -> string -> Cic.annobj -> (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) GrafiteAst.statement list diff --git a/components/content_pres/cicClassify.ml b/components/content_pres/cicClassify.ml index 0c464c7d9..4cfd47e5a 100644 --- a/components/content_pres/cicClassify.ml +++ b/components/content_pres/cicClassify.ml @@ -24,7 +24,7 @@ *) module C = Cic -module CS = CicSubstitution +module R = CicReduction module D = Deannotate module Int = struct type t = int @@ -57,6 +57,8 @@ let out_table b = (****************************************************************************) +let id x = x + let rec list_fold_left g map = function | [] -> g | hd :: tl -> map (list_fold_left g map tl) hd @@ -98,28 +100,29 @@ let get_rels h t = let g a = a in aux 1 g t S.empty -let split t = - let rec aux a n = function - | C.Prod (_, v, t) -> aux (v :: a) (succ n) t - | C.Cast (t, v) -> aux a n t - | C.LetIn (_, v, t) -> aux a n (CS.subst v t) - | v -> v :: a, n +let split c t = + let add s v c = Some (s, C.Decl v) :: c in + let rec aux whd a n c = function + | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t + | v when whd -> v :: a, n + | v -> aux true a n c (R.whd ~delta:true c v) in - aux [] 0 t + aux false [] 0 c t let classify_conclusion = function | C.Rel i -> Some (i, 0) | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl) | _ -> None -let classify t = - let vs, h = split t in +let classify c t = +try + let vs, h = split c t in let rc = classify_conclusion (List.hd vs) in let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in let l, h = List.fold_left map ([], 0) vs in let b = Array.of_list (List.rev l) in let mk_closure b h = - let map j = S.union (fst b.(j)) in + let map j = if j < h then S.union (fst b.(j)) else id in for i = pred h downto 0 do let direct, unused = b.(i) in b.(i) <- S.fold map direct direct, unused @@ -129,16 +132,17 @@ let classify t = let rec mk_inverse i direct = if S.is_empty direct then () else let j = S.choose direct in - let unused, inverse = b.(j) in - b.(j) <- unused, S.add i inverse; - mk_inverse i (S.remove j direct) + if j < h then + let unused, inverse = b.(j) in + b.(j) <- unused, S.add i inverse + else (); + mk_inverse i (S.remove j direct) in let map i (direct, _) = mk_inverse i direct in Array.iteri map b; (* out_table b; *) List.rev_map snd (List.tl (Array.to_list b)), rc - -let aclassify t = classify (D.deannotate_term t) +with Invalid_argument _ -> failwith "Classify.classify" let overlaps s1 s2 = let predicate x = S.mem x s1 in diff --git a/components/content_pres/cicClassify.mli b/components/content_pres/cicClassify.mli index c35ba1b5c..3d92134df 100644 --- a/components/content_pres/cicClassify.mli +++ b/components/content_pres/cicClassify.mli @@ -27,9 +27,7 @@ module S : Set.S with type elt = int type conclusion = (int * int) option -val classify: Cic.term -> S.t list * conclusion - -val aclassify: Cic.annterm -> S.t list * conclusion +val classify: Cic.context -> Cic.term -> S.t list * conclusion val to_string: S.t list * conclusion -> string diff --git a/components/content_pres/objPp.ml b/components/content_pres/objPp.ml index 3cdad5528..f83b18635 100644 --- a/components/content_pres/objPp.ml +++ b/components/content_pres/objPp.ml @@ -49,17 +49,17 @@ let obj_to_string n style prefix obj = failwith msg in match style with - | GrafiteAst.Declarative -> + | GrafiteAst.Declarative -> let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in remove_closed_substs ("\n\n" ^ BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) ) - | GrafiteAst.Procedural -> + | GrafiteAst.Procedural depth -> let term_pp = term2pres (n - 8) ids_to_inner_sorts in let lazy_term_pp = term_pp in let obj_pp = CicNotationPp.pp_obj term_pp in let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in let script = Acic2Procedural.acic2procedural - ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj in + ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in "\n\n" ^ String.concat "" (List.map aux script) diff --git a/components/content_pres/objPp.mli b/components/content_pres/objPp.mli index 9367661ec..de320bf14 100644 --- a/components/content_pres/objPp.mli +++ b/components/content_pres/objPp.mli @@ -24,4 +24,5 @@ *) (* columns, rendering style, name prefix, object *) -val obj_to_string: int -> GrafiteAst.style -> string -> Cic.obj -> string +val obj_to_string: + int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string diff --git a/components/content_pres/proceduralConversion.ml b/components/content_pres/proceduralConversion.ml index e506a8f6e..abd6fd62a 100644 --- a/components/content_pres/proceduralConversion.ml +++ b/components/content_pres/proceduralConversion.ml @@ -30,3 +30,32 @@ let rec need_whd i = function | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t | _ when i > 0 -> true | _ -> false + +let lift k n = + let rec lift_xns k (uri, t) = uri, lift_term k t + and lift_ms k = function + | None -> None + | Some t -> Some (lift_term k t) + and lift_fix len k (id, name, i, ty, bo) = + id, name, i, lift_term k ty, lift_term (k + len) bo + and lift_cofix len k (id, name, ty, bo) = + id, name, lift_term k ty, lift_term (k + len) bo + and lift_term k = function + | C.ASort _ as t -> t + | C.AImplicit _ as t -> t + | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b) + | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss) + | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss) + | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss) + | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss) + | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss) + | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts) + | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty) + | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl) + | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t) + | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t) + | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t) + | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl) + | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl) + in + lift_term k diff --git a/components/content_pres/proceduralConversion.mli b/components/content_pres/proceduralConversion.mli index 448112cdb..d5ad4fd1c 100644 --- a/components/content_pres/proceduralConversion.mli +++ b/components/content_pres/proceduralConversion.mli @@ -24,3 +24,5 @@ *) val need_whd: int -> Cic.annterm -> bool + +val lift: int -> int -> Cic.annterm -> Cic.annterm diff --git a/components/content_pres/proceduralTypes.ml b/components/content_pres/proceduralTypes.ml index b7f6d3c6b..95fdc6e56 100644 --- a/components/content_pres/proceduralTypes.ml +++ b/components/content_pres/proceduralTypes.ml @@ -55,6 +55,17 @@ let list_rev_map_concat map sep a l = in aux a l +let is_atomic = function + | C.ASort _ + | C.AConst _ + | C.AMutInd _ + | C.AMutConstruct _ + | C.AVar _ + | C.ARel _ + | C.AMeta _ + | C.AImplicit _ -> true + | _ -> false + (****************************************************************************) type name = string diff --git a/components/content_pres/proceduralTypes.mli b/components/content_pres/proceduralTypes.mli index b06acd104..dfd82df12 100644 --- a/components/content_pres/proceduralTypes.mli +++ b/components/content_pres/proceduralTypes.mli @@ -31,6 +31,8 @@ val list_split: int -> 'a list -> 'a list * 'a list val mk_arel: int -> string -> Cic.annterm +val is_atomic:Cic.annterm -> bool + (****************************************************************************) type name = string diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index e75e53867..10d7b6bcc 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -77,7 +77,6 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | LetIn of loc * 'term * 'ident | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern | Reflexivity of loc - | Rename of loc * 'ident list * 'ident list | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Rewrite of loc * direction * 'term * ('term, 'lazy_term, 'ident) pattern * 'ident list @@ -109,8 +108,8 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] -type style = Declarative - | Procedural +type presentation_style = Declarative + | Procedural of int option type 'term macro = (* Whelp's stuff *) @@ -122,7 +121,8 @@ type 'term macro = (* real macros *) | Check of loc * 'term | Hint of loc - | Inline of loc * style * string * string (* URI or base-uri, name prefix *) + | Inline of loc * presentation_style * string * string + (* URI or base-uri, name prefix *) (** To be increased each time the command type below changes, used for "safe" * marshalling *) diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index ce9ea017b..183fc5ec4 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -148,8 +148,6 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Reduce (_, kind, pat) -> sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat) | Reflexivity _ -> "reflexivity" - | Rename (_, froms, tos) -> - sprintf "rename %s as %s" (pp_idents froms) (pp_idents tos) | Replace (_, pattern, t) -> sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t) | Rewrite (_, pos, t, pattern, names) -> @@ -202,8 +200,9 @@ let pp_arg ~term_pp arg = let pp_macro ~term_pp = let term_pp = pp_arg ~term_pp in let style_pp = function - | Declarative -> "" - | Procedural -> "procedural " + | Declarative -> "" + | Procedural None -> "procedural " + | Procedural (Some i) -> sprintf "procedural %u " i in let prefix_pp prefix = if prefix = "" then "" else sprintf " \"%s\"" prefix diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 09ceecebc..ab9813221 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -151,7 +151,6 @@ let tactic_of_ast status ast = | `Unfold what -> Tactics.unfold ~pattern what | `Whd -> Tactics.whd ~pattern) | GrafiteAst.Reflexivity _ -> Tactics.reflexivity - | GrafiteAst.Rename (_, froms, tos) -> Tactics.rename ~froms ~tos | GrafiteAst.Replace (_, pattern, with_what) -> Tactics.replace ~pattern ~with_what | GrafiteAst.Rewrite (_, direction, t, pattern, names) -> diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index e7f5eb1fd..7d110e2df 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -232,8 +232,6 @@ let disambiguate_tactic metasenv,GrafiteAst.Reduce(loc, red_kind, pattern) | GrafiteAst.Reflexivity loc -> metasenv,GrafiteAst.Reflexivity loc - | GrafiteAst.Rename (loc, froms, tos) -> - metasenv,GrafiteAst.Rename (loc, froms, tos) | GrafiteAst.Replace (loc, pattern, with_what) -> let pattern = disambiguate_pattern pattern in let with_what = disambiguate_lazy_term with_what in diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 586cca004..2d3789221 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -218,8 +218,6 @@ EXTEND GrafiteAst.Reduce (loc, kind, p) | IDENT "reflexivity" -> GrafiteAst.Reflexivity loc - | IDENT "rename"; froms = ident_list0; "as"; tos = ident_list0 -> - GrafiteAst.Rename (loc, froms, tos) | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> GrafiteAst.Replace (loc, p, t) | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec; @@ -428,11 +426,11 @@ EXTEND [ [ IDENT "check" ]; t = term -> GrafiteAst.Check (loc, t) | [ IDENT "inline"]; - style = OPT [ IDENT "procedural" ]; + style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; suri = QSTRING; prefix = OPT QSTRING -> let style = match style with - | None -> GrafiteAst.Declarative - | Some _ -> GrafiteAst.Procedural + | None -> GrafiteAst.Declarative + | Some depth -> GrafiteAst.Procedural depth in let prefix = match prefix with None -> "" | Some prefix -> prefix in GrafiteAst.Inline (loc,style,suri,prefix) diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml index 130ad7100..82c343085 100644 --- a/components/tactics/tactics.ml +++ b/components/tactics/tactics.ml @@ -59,7 +59,6 @@ let letin = PrimitiveTactics.letin_tac let normalize = ReductionTactics.normalize_tac let reduce = ReductionTactics.reduce_tac let reflexivity = Setoids.setoid_reflexivity_tac -let rename = ProofEngineStructuralRules.rename let replace = EqualityTactics.replace_tac let rewrite = EqualityTactics.rewrite_tac let rewrite_simpl = EqualityTactics.rewrite_simpl_tac diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 71265bc7a..eb290ff05 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Dec 29 14:56:56 CET 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Jan 14 12:32:17 CET 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -72,7 +72,6 @@ val normalize : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic -val rename : froms:string list -> tos:string list -> ProofEngineTypes.tactic val replace : pattern:ProofEngineTypes.lazy_pattern -> with_what:Cic.lazy_term -> ProofEngineTypes.tactic diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index e2a5588dc..ed39ac652 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -234,16 +234,40 @@ class interpErrorModel = let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll = + assert (List.flatten errorll <> []); let errorll' = let remove_non_significant = List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in if all_passes then errorll else let safe_list_nth l n = try List.nth l n with Failure _ -> [] in (* We remove passes 1,2 and 5,6 *) - []::[] - ::(remove_non_significant (safe_list_nth errorll 2)) - ::(remove_non_significant (safe_list_nth errorll 3)) - ::[]::[] + let res = + []::[] + ::(remove_non_significant (safe_list_nth errorll 2)) + ::(remove_non_significant (safe_list_nth errorll 3)) + ::[]::[] + in + if List.flatten res <> [] then res + else + (* all errors (if any) are not significant: we keep them *) + let res = + []::[] + ::(safe_list_nth errorll 2) + ::(safe_list_nth errorll 3) + ::[]::[] + in + if List.flatten res <> [] then + begin + HLog.warn + "All disambiguation errors are not significant. Showing them anyway." ; + res + end + else + begin + HLog.warn + "No errors in phases 2 and 3. Showing all errors in all phases" ; + errorll + end in let choices = let pass = ref 0 in -- 2.39.2