From: Ferruccio Guidi Date: Sun, 29 Sep 2019 20:43:50 +0000 (+0200) Subject: Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita... X-Git-Tag: make_still_working~229^2~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=db020b4218272e2e35641ce3bc3b0a9b3afda899;hp=-c Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita-lablgtk3 --- db020b4218272e2e35641ce3bc3b0a9b3afda899 diff --combined matita/components/grafite/grafiteAstPp.ml index 2e088bd77,42d7df864..e16ce39bd --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@@ -1,14 -1,14 +1,14 @@@ (* Copyright (C) 2004, HELM Team. - * + * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. - * + * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. - * + * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the @@@ -18,7 -18,7 +18,7 @@@ * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. - * + * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) @@@ -32,8 -32,8 +32,8 @@@ let tactical_terminator = " let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator - let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) = - if what = None && hyp = [] && goal = None then "" else + let pp_tactic_pattern status ~map_unicode_to_tex (what, hyp, goal) = + if what = None && hyp = [] && goal = None then "" else let what_text = match what with | None -> "" @@@ -51,6 -51,22 +51,22 @@@ in Printf.sprintf "%sin %s%s" what_text hyp_text goal_text + let pp_auto_params params status = + match params with + | (None,flags) -> String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags) + | (Some l,flags) -> (String.concat "," (List.map (NotationPp.pp_term status) l)) ^ + String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flags) + ;; + + let pp_just status just = + match just with + `Term term -> "using (" ^ NotationPp.pp_term status term ^ ") " + | `Auto params -> + match params with + | (None,[]) -> "" + | params -> "by " ^ pp_auto_params params status ^ " " + ;; + let rec pp_ntactic status ~map_unicode_to_tex = let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in function @@@ -70,13 -86,13 +86,13 @@@ | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^ String.concat " " (List.map (NotationPp.pp_term status) l) | NCase1 (_,n) -> "*" ^ n ^ ":" - | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^ + | NChange (_,_what,wwhat) -> "nchange " ^ "...to be implemented..." ^ " with " ^ NotationPp.pp_term status wwhat | NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t (*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *) | NClear (_,l) -> "nclear " ^ String.concat " " l - | NDestruct (_,_dom,_skip) -> "ndestruct ..." + | NDestruct (_,_dom,_skip) -> "ndestruct ..." | NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^ "...to be implemented..." ^ " " ^ "...to be implemented..." | NId _ -> "nid" @@@ -97,16 -113,58 +113,58 @@@ | NPosbyname (_, s) -> s ^ ":" | NWildcard _ -> "*:" | NMerge _ -> "]" - | NFocus (_,l) -> - Printf.sprintf "focus %s" + | NFocus (_,l) -> + Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int l)) | NUnfocus _ -> "unfocus" | NSkip _ -> "skip" | NTry (_,tac) -> "ntry " ^ pp_ntactic status ~map_unicode_to_tex tac | NAssumption _ -> "nassumption" - | NBlock (_,l) -> + | NBlock (_,l) -> "(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")" | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t + | Assume (_, ident, term) -> "assume " ^ ident ^ ":(" ^ (NotationPp.pp_term status term) ^ ")" + | Suppose (_,term,ident) -> "suppose (" ^ (NotationPp.pp_term status term) ^ ") (" ^ ident ^ ") " + | By_just_we_proved (_, just, term1, ident) -> pp_just status just ^ " we proved (" ^ + (NotationPp.pp_term status term1) ^ ")" ^ (match ident with + None -> "" | Some ident -> "(" ^ident^ ")") + | We_need_to_prove (_,term,ident) -> "we need to prove (" ^ (NotationPp.pp_term status term) ^ ") " ^ + (match ident with None -> "" | Some id -> "(" ^ id ^ ")") + | BetaRewritingStep (_,t) -> "that is equivalent to (" ^ (NotationPp.pp_term status t) ^ ")" + | Bydone (_, just) -> pp_just status just ^ "done" + | ExistsElim (_, just, ident, term, term1, ident1) -> pp_just status just ^ "let " ^ ident ^ ": (" + ^ (NotationPp.pp_term status term) ^ ") such that (" ^ (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ")" + | AndElim (_, just, term1, ident1, term2, ident2) -> pp_just status just ^ " we have (" ^ + (NotationPp.pp_term status term1) ^ ") (" ^ ident1 ^ ") " ^ "and (" ^ (NotationPp.pp_term status + term2) + ^ ") (" ^ ident2 ^ ")" + | Thesisbecomes (_, t) -> "the thesis becomes (" ^ (NotationPp.pp_term status t) ^ ")" + | RewritingStep (_, rhs, just, cont) -> + "= (" ^ + (NotationPp.pp_term status rhs) ^ ")" ^ + (match just with + | `Auto params -> let s = pp_auto_params params status in + if s <> "" then " by " ^ s + else "" + | `Term t -> " exact (" ^ (NotationPp.pp_term status t) ^ ")" + | `Proof -> " proof" + | `SolveWith t -> " using (" ^ (NotationPp.pp_term status t) ^ ")" + ) + ^ (if cont then " done" else "") + | Obtain (_,id,t1) -> "obtain (" ^ id ^ ")" ^ " (" ^ (NotationPp.pp_term status t1) ^ ")" + | Conclude (_,t1) -> "conclude (" ^ (NotationPp.pp_term status t1) ^ ")" + | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on (" ^ NotationPp.pp_term + status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")" + | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on (" ^ + NotationPp.pp_term status term ^ ") to prove (" ^ NotationPp.pp_term status term1 ^ ")" + | Byinduction (_, term, ident) -> "by induction hypothesis we know (" ^ NotationPp.pp_term status + term ^ ") (" ^ ident ^ ")" + | Case (_, id, args) -> + "case " ^ id ^ + String.concat " " + (List.map (function (id,term) -> "(" ^ id ^ ": (" ^ NotationPp.pp_term status term ^ "))") + args) + | PrintStack _ -> "print_stack" ;; let pp_nmacro status = function @@@ -128,7 -186,7 +186,7 @@@ let pp_alias = functio desc | Number_alias (instance,desc) -> sprintf "alias num (instance %d) = \"%s\"." instance desc - + let pp_associativity = function | Gramext.LeftA -> "left associative" | Gramext.RightA -> "right associative" @@@ -144,18 -202,18 +202,18 @@@ let pp_argument_pattern = functio done; sprintf "%s%s" (Buffer.contents eta_buf) name - let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = + let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = sprintf "interpretation \"%s\" '%s %s = %s." dsc symbol (String.concat " " (List.map pp_argument_pattern arg_patterns)) (NotationPp.pp_cic_appl_pattern cic_appl_pattern) - + let pp_dir_opt = function | None -> "" | Some `LeftToRight -> "> " | Some `RightToLeft -> "< " - let pp_notation status dir_opt l1_pattern assoc prec l2_pattern = + let pp_notation status dir_opt l1_pattern assoc prec l2_pattern = sprintf "notation %s\"%s\" %s %s for %s." (pp_dir_opt dir_opt) (pp_l1_pattern status l1_pattern) @@@ -164,22 -222,22 +222,22 @@@ (pp_l2_pattern status l2_pattern) let pp_ncommand status = function - | UnificationHint (_,t, n) -> + | UnificationHint (_,t, n) -> "unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term status t | NDiscriminator (_,_) | NInverter (_,_,_,_,_) | NUnivConstraint (_) -> "not supported" | NCoercion (_) -> "not supported" - | NObj (_,obj,index) -> - (if not index then "-" else "") ^ + | NObj (_,obj,index) -> + (if not index then "-" else "") ^ NotationPp.pp_obj (NotationPp.pp_term status) obj | NQed (_,true) -> "qed" | NQed (_,false) -> "qed-" - | NCopy (_,name,uri,map) -> - "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ - String.concat " and " - (List.map - (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b) + | NCopy (_,name,uri,map) -> + "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ + String.concat " and " + (List.map + (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b) map) | Include (_,mode,path) -> (* not precise, since path is absolute *) if mode = WithPreferences then @@@ -192,14 -250,14 +250,14 @@@ | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> pp_notation status dir_opt l1_pattern assoc prec l2_pattern ;; - + let pp_executable status ~map_unicode_to_tex = function | NMacro (_, macro) -> pp_nmacro status macro ^ "." | NTactic (_,tacl) -> String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) tacl) | NCommand (_, cmd) -> pp_ncommand status cmd ^ "." - + let pp_comment status ~map_unicode_to_tex = function | Note (_,"") -> Printf.sprintf "\n" @@@ -209,5 -267,5 +267,5 @@@ let pp_statement status = function - | Executable (_, ex) -> pp_executable status ex + | Executable (_, ex) -> pp_executable status ex | Comment (_, c) -> pp_comment status c diff --combined matita/components/ng_tactics/.depend index 90de5733d,4d386aaa4..57784f373 --- a/matita/components/ng_tactics/.depend +++ b/matita/components/ng_tactics/.depend @@@ -1,30 -1,94 +1,35 @@@ -continuationals.cmo : \ - continuationals.cmi -continuationals.cmx : \ - continuationals.cmi +continuationals.cmo : continuationals.cmi +continuationals.cmx : continuationals.cmi continuationals.cmi : -declarative.cmo : \ - nnAuto.cmi \ - nTactics.cmi \ - nTacStatus.cmi \ - nCicElim.cmi \ - continuationals.cmi \ - declarative.cmi -declarative.cmx : \ - nnAuto.cmx \ - nTactics.cmx \ - nTacStatus.cmx \ - nCicElim.cmx \ - continuationals.cmx \ - declarative.cmi -declarative.cmi : \ - nnAuto.cmi \ - nTacStatus.cmi -nCicElim.cmo : \ - nCicElim.cmi -nCicElim.cmx : \ - nCicElim.cmi ++declarative.cmo : nnAuto.cmi nTactics.cmi nTacStatus.cmi nCicElim.cmi \ ++ continuationals.cmi declarative.cmi ++declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \ ++ continuationals.cmx declarative.cmi ++declarative.cmi : nnAuto.cmi nTacStatus.cmi +nCicElim.cmo : nCicElim.cmi +nCicElim.cmx : nCicElim.cmi nCicElim.cmi : -nCicTacReduction.cmo : \ - nCicTacReduction.cmi -nCicTacReduction.cmx : \ - nCicTacReduction.cmi +nCicTacReduction.cmo : nCicTacReduction.cmi +nCicTacReduction.cmx : nCicTacReduction.cmi nCicTacReduction.cmi : -nDestructTac.cmo : \ - nTactics.cmi \ - nTacStatus.cmi \ - continuationals.cmi \ +nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \ nDestructTac.cmi -nDestructTac.cmx : \ - nTactics.cmx \ - nTacStatus.cmx \ - continuationals.cmx \ +nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ nDestructTac.cmi -nDestructTac.cmi : \ - nTacStatus.cmi -nInversion.cmo : \ - nTactics.cmi \ - nTacStatus.cmi \ - nCicElim.cmi \ - continuationals.cmi \ - nInversion.cmi -nInversion.cmx : \ - nTactics.cmx \ - nTacStatus.cmx \ - nCicElim.cmx \ - continuationals.cmx \ - nInversion.cmi -nInversion.cmi : \ - nTacStatus.cmi -nTacStatus.cmo : \ - nCicTacReduction.cmi \ - continuationals.cmi \ - nTacStatus.cmi -nTacStatus.cmx : \ - nCicTacReduction.cmx \ - continuationals.cmx \ - nTacStatus.cmi -nTacStatus.cmi : \ - continuationals.cmi -nTactics.cmo : \ - nTacStatus.cmi \ - nCicElim.cmi \ - continuationals.cmi \ - nTactics.cmi -nTactics.cmx : \ - nTacStatus.cmx \ - nCicElim.cmx \ - continuationals.cmx \ - nTactics.cmi -nTactics.cmi : \ - nTacStatus.cmi -nnAuto.cmo : \ - nTactics.cmi \ - nTacStatus.cmi \ - nCicTacReduction.cmi \ - continuationals.cmi \ - nnAuto.cmi -nnAuto.cmx : \ - nTactics.cmx \ - nTacStatus.cmx \ - nCicTacReduction.cmx \ - continuationals.cmx \ - nnAuto.cmi -nnAuto.cmi : \ - nTacStatus.cmi +nDestructTac.cmi : nTacStatus.cmi +nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \ + continuationals.cmi nInversion.cmi +nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ + continuationals.cmx nInversion.cmi +nInversion.cmi : nTacStatus.cmi +nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi +nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi +nTacStatus.cmi : continuationals.cmi +nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi +nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi +nTactics.cmi : nTacStatus.cmi +nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \ + continuationals.cmi nnAuto.cmi +nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ + continuationals.cmx nnAuto.cmi +nnAuto.cmi : nTacStatus.cmi diff --combined matita/components/ng_tactics/.depend.opt index c8999df5a,ca420895d..75b2d57f8 --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@@ -1,19 -1,55 +1,22 @@@ -continuationals.cmx : \ - continuationals.cmi +continuationals.cmx : continuationals.cmi continuationals.cmi : -declarative.cmx : \ - nnAuto.cmx \ - nTactics.cmx \ - nTacStatus.cmx \ - nCicElim.cmx \ - continuationals.cmx \ - declarative.cmi -declarative.cmi : \ - nnAuto.cmi \ - nTacStatus.cmi -nCicElim.cmx : \ - nCicElim.cmi ++declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \ ++ continuationals.cmx declarative.cmi ++declarative.cmi : nnAuto.cmi nTacStatus.cmi +nCicElim.cmx : nCicElim.cmi nCicElim.cmi : -nCicTacReduction.cmx : \ - nCicTacReduction.cmi +nCicTacReduction.cmx : nCicTacReduction.cmi nCicTacReduction.cmi : -nDestructTac.cmx : \ - nTactics.cmx \ - nTacStatus.cmx \ - continuationals.cmx \ +nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ nDestructTac.cmi -nDestructTac.cmi : \ - nTacStatus.cmi -nInversion.cmx : \ - nTactics.cmx \ - nTacStatus.cmx \ - nCicElim.cmx \ - continuationals.cmx \ - nInversion.cmi -nInversion.cmi : \ - nTacStatus.cmi -nTacStatus.cmx : \ - nCicTacReduction.cmx \ - continuationals.cmx \ - nTacStatus.cmi -nTacStatus.cmi : \ - continuationals.cmi -nTactics.cmx : \ - nTacStatus.cmx \ - nCicElim.cmx \ - continuationals.cmx \ - nTactics.cmi -nTactics.cmi : \ - nTacStatus.cmi -nnAuto.cmx : \ - nTactics.cmx \ - nTacStatus.cmx \ - nCicTacReduction.cmx \ - continuationals.cmx \ - nnAuto.cmi -nnAuto.cmi : \ - nTacStatus.cmi +nDestructTac.cmi : nTacStatus.cmi +nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ + continuationals.cmx nInversion.cmi +nInversion.cmi : nTacStatus.cmi +nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi +nTacStatus.cmi : continuationals.cmi +nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi +nTactics.cmi : nTacStatus.cmi +nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ + continuationals.cmx nnAuto.cmi +nnAuto.cmi : nTacStatus.cmi diff --combined matita/components/ng_tactics/nTactics.ml index 1aba2be9d,721d9165b..11427e9a7 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@@ -31,16 -31,16 +31,16 @@@ let dot_tac status let gstatus = match status#stack with | [] -> assert false - | ([], _, [], _) :: _ as stack -> + | ([], _, [], _, _) :: _ as stack -> (* backward compatibility: do-nothing-dot *) stack - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> match filter_open g, k with | loc :: loc_tl, _ -> - (([ loc ], t, loc_tl @+ k, tag) :: s) + (([ loc ], t, loc_tl @+ k, tag, p) :: s) | [], loc :: k -> assert (is_open loc); - (([ loc ], t, k, tag) :: s) + (([ loc ], t, k, tag, p) :: s) | _ -> fail (lazy "can't use \".\" here") in status#set_stack gstatus @@@ -50,12 -50,12 +50,12 @@@ let branch_tac ?(force=false) status let gstatus = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> match init_pos g with (* TODO *) | [] -> fail (lazy "empty goals") - | [_] when (not force) -> fail (lazy "too few goals to branch") + | [_] when (not force) -> fail (lazy "too few goals to branch") | loc :: loc_tl -> - ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s + ([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag, p) :: s in status#set_stack gstatus ;; @@@ -63,12 -63,12 +63,12 @@@ let shift_tac status = let gstatus = match status#stack with - | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> + | (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s -> (match g' with | [] -> fail (lazy "no more goals to shift") | loc :: loc_tl -> - (([ loc ], t @+ filter_open g @+ k, [],`BranchTag) - :: (loc_tl, t', k', tag) :: s)) + (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p) + :: (loc_tl, t', k', tag, p') :: s)) | _ -> fail (lazy "can't shift goals here") in status#set_stack gstatus @@@ -78,11 -78,11 +78,11 @@@ let pos_tac i_s status let gstatus = match status#stack with | [] -> assert false - | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in - ((l_js, t , [],`BranchTag) - :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + ((l_js, t , [],`BranchTag, p) + :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s) | _ -> fail (lazy "can't use relative positioning here") in status#set_stack gstatus @@@ -92,7 -92,7 +92,7 @@@ let case_tac lab status let gstatus = match status#stack with | [] -> assert false - | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s + | ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> let l_js = List.filter @@@ -101,8 -101,8 +101,8 @@@ match NCicUtils.lookup_meta (goal_of_loc curloc) metasenv with attrs,_,_ when List.mem (`Name lab) attrs -> true | _ -> false) ([loc] @+ g') in - ((l_js, t , [],`BranchTag) - :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s) + ((l_js, t , [],`BranchTag, p) + :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s) | _ -> fail (lazy "can't use relative positioning here") in status#set_stack gstatus @@@ -112,9 -112,9 +112,9 @@@ let wildcard_tac status let gstatus = match status#stack with | [] -> assert false - | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s + | ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s when is_fresh loc -> - (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s) + (([loc] @+ g', t, [], `BranchTag, p) :: ([], t', k', tag, p') :: s) | _ -> fail (lazy "can't use wildcard here") in status#set_stack gstatus @@@ -124,8 -124,8 +124,8 @@@ let merge_tac status let gstatus = match status#stack with | [] -> assert false - | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> - ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) + | (g, t, k,`BranchTag, _) :: (g', t', k', tag, p) :: s -> + ((t @+ filter_open g @+ g' @+ k, t', k', tag, p) :: s) | _ -> fail (lazy "can't merge goals here") in status#set_stack gstatus @@@ -145,7 -145,7 +145,7 @@@ let focus_tac gs status if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then fail (lazy (sprintf "goal %d not found (or closed)" g))) gs; - (zero_pos gs, [], [], `FocusTag) :: deep_close gs s + (zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s in status#set_stack gstatus ;; @@@ -154,7 -154,7 +154,7 @@@ let unfocus_tac status let gstatus = match status#stack with | [] -> assert false - | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s + | (g, [], [], `FocusTag, _) :: s when filter_open g = [] -> s | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^ Continuationals.Stack.pp s)) in @@@ -165,12 -165,12 +165,12 @@@ let skip_tac status let gstatus = match status#stack with | [] -> assert false - | (gl, t, k, tag) :: s -> + | (gl, t, k, tag, p) :: s -> let gl = List.map switch_of_loc gl in if List.exists (function Open _ -> true | Closed _ -> false) gl then fail (lazy "cannot skip an open goal") else - ([],t,k,tag) :: s + ([],t,k,tag,p) :: s in status#set_stack gstatus ;; @@@ -219,7 -219,7 +219,7 @@@ let change_stack_type (status : 'a #NTa ;; let exec tac (low_status : #lowtac_status) g = - let stack = [ [0,Open g], [], [], `NoTag ] in + let stack = [ [0,Open g], [], [], `NoTag, [] ] in let status = change_stack_type low_status stack in let status = tac status in (low_status#set_pstatus status)#set_obj status#obj @@@ -228,7 -228,7 +228,7 @@@ let distribute_tac tac (status : #tac_status) = match status#stack with | [] -> assert false - | (g, t, k, tag) :: s -> + | (g, t, k, tag, p) :: s -> debug_print (lazy ("context length " ^string_of_int (List.length g))); let rec aux s go gc = function @@@ -258,7 -258,7 +258,7 @@@ debug_print (lazy ("closed: " ^ String.concat " " (List.map string_of_int gcn))); let stack = - (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s + (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s in ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn ;; @@@ -492,6 -492,7 +492,7 @@@ type indtyinfo = leftno: int; consno: int; reference: NReference.reference; + cl: NCic.constructor list; } ;; @@@ -502,11 -503,12 +503,12 @@@ let analyze_indty_tac ~what indtyref let goalty = get_goalty status goal in let status, what = disambiguate status (ctx_of goalty) what `XTInd in let status, ty_what = typeof status (ctx_of what) what in - let _status, (r,consno,lefts,rights) = analyse_indty status ty_what in + let _status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in let leftno = List.length lefts in let rightno = List.length rights in indtyref := Some { rightno = rightno; leftno = leftno; consno = consno; reference = r; + cl = cl; }; exec id_tac orig_status goal) ;; @@@ -522,6 -524,33 +524,33 @@@ let sort_of_goal_tac sortref = distribu status) ;; + let pp_ref reference = + let NReference.Ref (uri,spec) = reference in + let nstring = NUri.string_of_uri uri in + (*"Shareno: " ^ (string_of_int nuri) ^*) "Uri: " ^ nstring ^ + (match spec with + | NReference.Decl -> "Decl" + | NReference.Def n -> "Def " ^ (string_of_int n) + | NReference.Fix (n1,n2,n3) -> "Fix " ^ (string_of_int n1) ^ " " ^ (string_of_int n2) ^ " " ^ (string_of_int n3)(* fixno, recparamno, height *) + | NReference.CoFix n -> "CoFix " ^ (string_of_int n) + | NReference.Ind (b,n1,n2) -> "Ind " ^ (string_of_bool b) ^ " " ^ (string_of_int n1) ^ " " ^ (string_of_int n2)(* inductive, indtyno, leftno *) + | NReference.Con (n1,n2,n3) -> "Con " ^ (string_of_int n1) ^ " " ^ (string_of_int n2) ^ " " ^ (string_of_int n3)(* indtyno, constrno, leftno *) + ) ;; + + let pp_cl cl = + let rec pp_aux acc = + match acc with + | [] -> "" + | (_,consname,_) :: tl -> consname ^ ", " ^ pp_aux tl + in + pp_aux cl + ;; + + let pp_indtyinfo ity = "leftno: " ^ (string_of_int ity.leftno) ^ ", consno: " ^ (string_of_int + ity.consno) ^ ", rightno: " ^ + (string_of_int ity.rightno) ^ ", reference: " ^ (pp_ref ity.reference) ^ ", + cl: " ^ (pp_cl ity.cl);; + let elim_tac ~what:(txt,len,what) ~where = let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in let indtyinfo = ref None in @@@ -597,7 -626,7 +626,7 @@@ let cases ~what status goal let gty = get_goalty status goal in let status, what = disambiguate status (ctx_of gty) what `XTInd in let status, ty = typeof status (ctx_of what) what in - let status, (ref, consno, _, _) = analyse_indty status ty in + let status, (ref, consno, _, _,_) = analyse_indty status ty in let status, what = term_of_cic_term status what (ctx_of gty) in let t = NCic.Match (ref,NCic.Implicit `Term, what, @@@ -628,7 -657,7 +657,7 @@@ let case1_tac name let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal -> let gty = get_goalty status goal in - let status, (r,consno,_,_) = analyse_indty status gty in + let status, (r,consno,_,_,_) = analyse_indty status gty in if num < 1 || num > consno then fail (lazy "Non existant constructor"); let ref = NReference.mk_constructor num r in let t = @@@ -675,7 -704,7 +704,7 @@@ let assert0_tac (hyps,concl) = distribu let assert_tac seqs status = match status#stack with | [] -> assert false - | (g,_,_,_,_) :: _s -> + | (g,_,_,_) :: _s -> assert (List.length g = List.length seqs); (match seqs with [] -> id_tac