From f68f58e17f9be1d3760dd79064fb950d1aa885e1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Oct 2010 14:41:16 +0000 Subject: [PATCH] - bug fixed (introduced by last commit from Andrea in MatitaEngine): recursive inclusion was de-activated - some dead code removal --- .../grafite_engine/grafiteEngine.ml | 41 +-- .../grafite_engine/grafiteEngine.mli | 1 - .../grafite_parser/grafiteDisambiguate.ml | 8 +- .../grafite_parser/grafiteDisambiguate.mli | 7 - .../grafite_parser/grafiteParser.ml | 249 +----------------- .../components/grafite_parser/test_parser.ml | 5 - .../components/ng_refiner/nCicRefineUtil.ml | 2 + matita/matita/matitaEngine.ml | 4 +- 8 files changed, 17 insertions(+), 300 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 78564d421..f3c4c5a22 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -53,7 +53,6 @@ type eval_ast = ?do_heavy_checks:bool -> GrafiteTypes.status -> -(* (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) *) GrafiteAst.statement disambiguator_input -> GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } @@ -270,18 +269,6 @@ let eval_add_constraint status u1 u2 = status,`New [] ;; -(* Not used -let eval_ng_punct (_text, _prefix_len, punct) = - match punct with - | GrafiteAst.Dot _ -> NTactics.dot_tac - | GrafiteAst.Semicolon _ -> fun x -> x - | GrafiteAst.Branch _ -> NTactics.branch_tac ~force:false - | GrafiteAst.Shift _ -> NTactics.shift_tac - | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l - | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac - | GrafiteAst.Merge _ -> NTactics.merge_tac -;; *) - let eval_ng_tac tac = let rec aux f (text, prefix_len, tac) = match tac with @@ -636,23 +623,19 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status,uris = match cmd with | GrafiteAst.Include (loc, baseuri) -> - (* Old Include command is not recursive; new one is let status = - if new_or_old = `OldAndNew then - let moopath_rw, moopath_r = - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true, - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:false in - let moopath = - if Sys.file_exists moopath_r then moopath_r else - if Sys.file_exists moopath_rw then moopath_rw else - raise (IncludedFileNotCompiled (moopath_rw,baseuri)) - in - eval_from_moo.efm_go status moopath - else - status - in *) + let moopath_rw, moopath_r = + LibraryMisc.obj_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true, + LibraryMisc.obj_file_of_baseuri + ~must_exist:false ~baseuri ~writable:false in + let moopath = + if Sys.file_exists moopath_r then moopath_r else + if Sys.file_exists moopath_rw then moopath_rw else + raise (IncludedFileNotCompiled (moopath_rw,baseuri)) + in + eval_from_moo.efm_go status moopath + in let status = NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) status in diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index e8ee448c5..450fdb69b 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -37,7 +37,6 @@ val eval_ast : ?do_heavy_checks:bool -> GrafiteTypes.status -> - (* (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) *) GrafiteAst.statement disambiguator_input -> (* the new status and generated objects, if any *) GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index 5f2ac335d..8e6631929 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -27,12 +27,6 @@ exception BaseUriNotSetYet -(* -type tactic = - (NotationPt.term, NotationPt.term, - NotationPt.term GrafiteAst.reduction, string) - GrafiteAst.tactic *) - let singleton msg = function | [x], _ -> x | l, _ -> @@ -213,7 +207,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = estatus, cic ;; -let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)= +let disambiguate_command estatus (text,prefix_len,cmd)= match cmd with | GrafiteAst.Include _ | GrafiteAst.Print _ diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index 4d66251ce..2de3a1b6d 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -25,15 +25,8 @@ exception BaseUriNotSetYet -(* -type tactic = - (NotationPt.term, NotationPt.term, - NotationPt.term GrafiteAst.reduction, string) - GrafiteAst.tactic *) - val disambiguate_command: LexiconEngine.status as 'status -> - ?baseuri:string -> GrafiteAst.command Disambiguate.disambiguator_input -> 'status * GrafiteAst.command diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index fe4a8042c..23d5b5d74 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -101,16 +101,6 @@ let nmk_rec_corec ind_kind defs loc = G.NObj (loc,t) (* -let npunct_of_punct = function - | G.Branch loc -> G.NBranch loc - | G.Shift loc -> G.NShift loc - | G.Pos (loc, i) -> G.NPos (loc, i) - | G.Wildcard loc -> G.NWildcard loc - | G.Merge loc -> G.NMerge loc - | G.Semicolon loc -> G.NSemicolon loc - | G.Dot loc -> G.NDot loc -;; - let nnon_punct_of_punct = function | G.Skip loc -> G.NSkip loc | G.Unfocus loc -> G.NUnfocus loc @@ -315,200 +305,6 @@ EXTEND | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)]) ] ]; -(* - tactic: [ - [ IDENT "absurd"; t = tactic_term -> - G.Absurd (loc, t) - | IDENT "apply"; IDENT "rule"; t = tactic_term -> - G.ApplyRule (loc, t) - | IDENT "apply"; t = tactic_term -> - G.Apply (loc, t) - | IDENT "applyP"; t = tactic_term -> - G.ApplyP (loc, t) - | IDENT "applyS"; t = tactic_term ; params = auto_params -> - G.ApplyS (loc, t, params) - | IDENT "assumption" -> - G.Assumption loc - | IDENT "autobatch"; params = auto_params -> - G.AutoBatch (loc,params) - | IDENT "cases"; what = tactic_term; - pattern = OPT pattern_spec; - specs = intros_spec -> - let pattern = match pattern with - | None -> None, [], Some N.UserInput - | Some pattern -> pattern - in - G.Cases (loc, what, pattern, specs) - | IDENT "clear"; ids = LIST1 IDENT -> - G.Clear (loc, ids) - | IDENT "clearbody"; id = IDENT -> - G.ClearBody (loc,id) - | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> - G.Change (loc, what, t) - | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = - OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec -> - let times = match times with None -> 1 | Some i -> i in - G.Compose (loc, t1, t2, times, specs) - | IDENT "constructor"; n = int -> - G.Constructor (loc, n) - | IDENT "contradiction" -> - G.Contradiction loc - | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> - G.Cut (loc, ident, t) - | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] -> - let idents = match idents with None -> [] | Some idents -> idents in - G.Decompose (loc, idents) - | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p) - | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] -> - G.Destruct (loc, xts) - | IDENT "elim"; what = tactic_term; using = using; - pattern = OPT pattern_spec; - ispecs = intros_spec -> - let pattern = match pattern with - | None -> None, [], Some N.UserInput - | Some pattern -> pattern - in - G.Elim (loc, what, using, pattern, ispecs) - | IDENT "elimType"; what = tactic_term; using = using; - (num, idents) = intros_spec -> - G.ElimType (loc, what, using, (num, idents)) - | IDENT "exact"; t = tactic_term -> - G.Exact (loc, t) - | IDENT "exists" -> - G.Exists loc - | IDENT "fail" -> G.Fail loc - | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> - let (pt,_,_) = p in - if pt <> None then - raise (HExtlib.Localized (loc, CicNotationParser.Parse_error - ("the pattern cannot specify the term to replace, only its" - ^ " paths in the hypotheses and in the conclusion"))) - else - G.Fold (loc, kind, t, p) - | IDENT "fourier" -> - G.Fourier loc - | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] -> - let idents = match idents with None -> [] | Some idents -> idents in - G.FwdSimpl (loc, hyp, idents) - | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> - G.Generalize (loc,p,id) - | IDENT "id" -> G.IdTac loc - | IDENT "intro"; ident = OPT IDENT -> - let idents = match ident with None -> [] | Some id -> [Some id] in - G.Intros (loc, (Some 1, idents)) - | IDENT "intros"; specs = intros_spec -> - G.Intros (loc, specs) - | IDENT "inversion"; t = tactic_term -> - G.Inversion (loc, t) - | IDENT "lapply"; - linear = OPT [ IDENT "linear" ]; - depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; - what = tactic_term; - to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; - ident = OPT [ "as" ; ident = IDENT -> ident ] -> - let linear = match linear with None -> false | Some _ -> true in - let to_what = match to_what with None -> [] | Some to_what -> to_what in - G.LApply (loc, linear, depth, to_what, what, ident) - | IDENT "left" -> G.Left loc - | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> - G.LetIn (loc, t, where) - | kind = reduction_kind; p = pattern_spec -> - G.Reduce (loc, kind, p) - | IDENT "reflexivity" -> - G.Reflexivity loc - | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> - G.Replace (loc, p, t) - | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec; - xnames = OPT [ "as"; n = ident_list0 -> n ] -> - let (pt,_,_) = p in - if pt <> None then - raise - (HExtlib.Localized (loc, - (CicNotationParser.Parse_error - "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) - else - let n = match xnames with None -> [] | Some names -> names in - G.Rewrite (loc, d, t, p, n) - | IDENT "right" -> - G.Right loc - | IDENT "ring" -> - G.Ring loc - | IDENT "split" -> - G.Split loc - | IDENT "symmetry" -> - G.Symmetry loc - | IDENT "transitivity"; t = tactic_term -> - G.Transitivity (loc, t) - (* Produzioni Aggiunte *) - | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> - G.Assume (loc, id, t) - | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; - t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; - t' = tactic_term -> t']-> - G.Suppose (loc, t, id, t1) - | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ; - IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; - id2 = IDENT ; RPAREN -> - G.ExistsElim (loc, `Auto (None,[]), id1, t1, id2, t2) - | just = - [ IDENT "using"; t=tactic_term -> `Term t - | params = auto_params -> `Auto params] ; - cont=by_continuation -> - (match cont with - BYC_done -> G.Bydone (loc, just) - | BYC_weproved (ty,id,t1) -> - G.By_just_we_proved(loc, just, ty, id, t1) - | BYC_letsuchthat (id1,t1,id2,t2) -> - G.ExistsElim (loc, just, id1, t1, id2, t2) - | BYC_wehaveand (id1,t1,id2,t2) -> - G.AndElim (loc, just, id1, t1, id2, t2)) - | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> - G.We_need_to_prove (loc, t, id, t1) - | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> - G.We_proceed_by_cases_on (loc, t, t1) - | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> - G.We_proceed_by_induction_on (loc, t, t1) - | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN -> - G.Byinduction(loc, t, id) - | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term -> - G.Thesisbecomes(loc, t) - | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; - SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> - G.Case(loc,id,params) - (* DO NOT FACTORIZE with the two following, camlp5 sucks*) - | IDENT "conclude"; - termine = tactic_term; - SYMBOL "=" ; - t1=tactic_term ; - t2 = - [ IDENT "using"; t=tactic_term -> `Term t - | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term - | IDENT "proof" -> `Proof - | params = auto_params -> `Auto params]; - cont = rewriting_step_continuation -> - G.RewritingStep(loc, Some (None,termine), t1, t2, cont) - | IDENT "obtain" ; name = IDENT; - termine = tactic_term; - SYMBOL "=" ; - t1=tactic_term ; - t2 = - [ IDENT "using"; t=tactic_term -> `Term t - | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term - | IDENT "proof" -> `Proof - | params = auto_params -> `Auto params]; - cont = rewriting_step_continuation -> - G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont) - | SYMBOL "=" ; - t1=tactic_term ; - t2 = - [ IDENT "using"; t=tactic_term -> `Term t - | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term - | IDENT "proof" -> `Proof - | params = auto_params -> `Auto params]; - cont = rewriting_step_continuation -> - G.RewritingStep(loc, None, t1, t2, cont) - ] -]; *) auto_fixed_param: [ [ IDENT "demod" | IDENT "fast_paramod" @@ -543,22 +339,6 @@ EXTEND ] ]; -(* - inline_params:[ - [ 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 "cr" -> G.IPCR - ] -> params - ] -];*) by_continuation: [ [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1) | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; @@ -576,7 +356,7 @@ EXTEND | -> false ] ]; -(* +(* MATITA 1.0 atomic_tactical: [ "sequence" LEFTA [ t1 = SELF; SYMBOL ";"; t2 = SELF -> @@ -623,26 +403,6 @@ EXTEND | SYMBOL "." -> G.NDot loc ] ]; -(* - punctuation_tactical: - [ - [ SYMBOL "[" -> G.Branch loc - | SYMBOL "|" -> G.Shift loc - | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i) - | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc - | SYMBOL "]" -> G.Merge loc - | SYMBOL ";" -> G.Semicolon loc - | SYMBOL "." -> G.Dot loc - ] - ]; - non_punctuation_tactical: - [ "simple" NONA - [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals) - | IDENT "unfocus" -> G.Unfocus loc - | IDENT "skip" -> G.Skip loc - ] - ]; -*) nnon_punctuation_tactical: [ "simple" NONA [ IDENT "focus"; goals = LIST1 int -> G.NFocus (loc, goals) @@ -890,15 +650,8 @@ EXTEND ]]; executable: [ [ ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd) -(* | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical -> - G.Tactic (loc, Some tac, punct) *) -(* | punct = punctuation_tactical -> G.Tactic (loc, None, punct) *) | tac = ntactic; OPT [ SYMBOL "#" ; SYMBOL "#" ] ; punct = npunctuation_tactical -> cons_ntac tac punct -(* - | tac = ntactic; punct = punctuation_tactical -> - cons_ntac tac (npunct_of_punct punct) -*) | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical -> G.NTactic (loc, [punct]) | SYMBOL "#" ; SYMBOL "#" ; tac = nnon_punctuation_tactical; diff --git a/matita/components/grafite_parser/test_parser.ml b/matita/components/grafite_parser/test_parser.ml index 5cb8a3a34..7e2eb7955 100644 --- a/matita/components/grafite_parser/test_parser.ml +++ b/matita/components/grafite_parser/test_parser.ml @@ -97,11 +97,6 @@ let process_stream istream = GrafiteAstPp.pp_statement statement ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")) -(* - ~term_pp:NotationPp.pp_term - ~lazy_term_pp:(fun _ -> "_lazy_term_here_") - ~obj_pp:(fun _ -> "_obj_here_") - statement)*) with | End_of_file -> raise End_of_file | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) -> diff --git a/matita/components/ng_refiner/nCicRefineUtil.ml b/matita/components/ng_refiner/nCicRefineUtil.ml index 745f57176..7015f1b5d 100644 --- a/matita/components/ng_refiner/nCicRefineUtil.ml +++ b/matita/components/ng_refiner/nCicRefineUtil.ml @@ -128,12 +128,14 @@ let replace_lifting ~equality ~context ~what ~with_what ~where = NCic.Match (it,substaux k ctx what outt, substaux k ctx what t, List.map (substaux k ctx what) pl) in +(* prerr_endline "*** replace lifting -- what:"; List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) what; prerr_endline "\n*** replace lifting -- with what:"; List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) with_what; prerr_endline "\n*** replace lifting -- where:"; prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context where); +*) substaux 1 context what where ;; diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index ab357e5c3..ef685c595 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -31,10 +31,8 @@ let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; let disambiguate_command lexicon_status_ref grafite_status cmd = - let baseuri = grafite_status#baseuri in let lexicon_status,cmd = - GrafiteDisambiguate.disambiguate_command ~baseuri - !lexicon_status_ref cmd + GrafiteDisambiguate.disambiguate_command !lexicon_status_ref cmd in lexicon_status_ref := lexicon_status; grafite_status,cmd -- 2.39.2