From: Stefano Zacchiroli Date: Mon, 18 Jul 2005 12:29:45 +0000 (+0000) Subject: merged cic_notation with matita: good luck! X-Git-Tag: V_0_7_2~200 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6b5e1d495c61f459738187e8d71efadb162abdbe;p=helm.git merged cic_notation with matita: good luck! --- diff --git a/helm/matita/.depend b/helm/matita/.depend index 1232842f0..c2c023dfc 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,11 +1,23 @@ -matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx +matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ + matitacleanLib.cmi +matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ + matitacleanLib.cmi +matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ + buildTimeConf.cmo +matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ + buildTimeConf.cmx +matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ + matitaLog.cmi matitaExcPp.cmi matitaEngine.cmi matitaDb.cmi \ + buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ + matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx matitaDb.cmx \ + buildTimeConf.cmx matitacLib.cmi +matitac.cmo: matitacLib.cmi +matitac.cmx: matitacLib.cmx matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi +matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi buildTimeConf.cmo +matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaEngine.cmo: matitaTypes.cmi matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ @@ -18,14 +30,22 @@ matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi -matitaGui.cmo: matitacleanLib.cmi matitacLib.cmi matitaTypes.cmi \ - matitaScript.cmi matitaMisc.cmi matitaLog.cmi matitaGtkMisc.cmi \ - matitaGeneratedGui.cmi matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi -matitaGui.cmx: matitacleanLib.cmx matitacLib.cmx matitaTypes.cmx \ - matitaScript.cmx matitaMisc.cmx matitaLog.cmx matitaGtkMisc.cmx \ - matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi +matitaGui.cmo: matitamakeLib.cmi matitacleanLib.cmi matitacLib.cmi \ + matitaTypes.cmi matitaScript.cmi matitaMisc.cmi matitaLog.cmi \ + matitaGtkMisc.cmi matitaGeneratedGui.cmi matitaExcPp.cmi \ + buildTimeConf.cmo matitaGui.cmi +matitaGui.cmx: matitamakeLib.cmx matitacleanLib.cmx matitacLib.cmx \ + matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaLog.cmx \ + matitaGtkMisc.cmx matitaGeneratedGui.cmx matitaExcPp.cmx \ + buildTimeConf.cmx matitaGui.cmi matitaLog.cmo: matitaLog.cmi matitaLog.cmx: matitaLog.cmi +matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \ + matitamakeLib.cmi +matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \ + matitamakeLib.cmi +matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo +matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaGui.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \ matitaMathView.cmi @@ -34,40 +54,24 @@ matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmi matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi -matitaScript.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \ - matitaMisc.cmi matitaLog.cmi matitaEngine.cmi matitaDisambiguator.cmi \ - matitaDb.cmi buildTimeConf.cmo matitaScript.cmi -matitaScript.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \ - matitaMisc.cmx matitaLog.cmx matitaEngine.cmx matitaDisambiguator.cmx \ - matitaDb.cmx buildTimeConf.cmx matitaScript.cmi +matita.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo +matita.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx +matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \ + matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \ + matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi +matitaScript.cmx: matitamakeLib.cmx matitacleanLib.cmx matitaTypes.cmx \ + matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaEngine.cmx \ + matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaScript.cmi matitaSync.cmo: matitaTypes.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ matitaSync.cmi matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ matitaSync.cmi matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi -matitac.cmo: matitacLib.cmi -matitac.cmx: matitacLib.cmx -matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaLog.cmi matitaExcPp.cmi matitaEngine.cmi matitaDb.cmi \ - buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx matitaDb.cmx \ - buildTimeConf.cmx matitacLib.cmi -matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaDb.cmi \ - buildTimeConf.cmo -matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaDb.cmx \ - buildTimeConf.cmx -matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \ - matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \ - matitacleanLib.cmi -matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi -matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx -matitamake.cmo: buildTimeConf.cmo -matitamake.cmx: buildTimeConf.cmx -matitamakeLib.cmo: matitaMisc.cmi buildTimeConf.cmo matitamakeLib.cmi -matitamakeLib.cmx: matitaMisc.cmx buildTimeConf.cmx matitamakeLib.cmi matitaDisambiguator.cmi: matitaTypes.cmi matitaEngine.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi @@ -76,4 +80,3 @@ matitaMathView.cmi: matitaTypes.cmi matitaMisc.cmi: matitaTypes.cmi matitaScript.cmi: matitaTypes.cmi matitaSync.cmi: matitaTypes.cmi -matitamakeLib.cmi: matitaLog.cmi diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 94847494d..b38eb2ce4 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -40,6 +40,7 @@ let images_dir = runtime_base_dir ^ "/icons" let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc" let lang_file = runtime_base_dir ^ "/matita.lang" let script_template = runtime_base_dir ^ "/matita.ma.templ" +let core_notation_script = runtime_base_dir ^ "/core_notation.ma" let matita_conf = runtime_base_dir ^ "/matita.conf.xml" let matitamake_makefile_template = runtime_base_dir ^ "/template_makefile.in" diff --git a/helm/matita/core_notation.ma b/helm/matita/core_notation.ma new file mode 100644 index 000000000..88cd759b8 --- /dev/null +++ b/helm/matita/core_notation.ma @@ -0,0 +1,126 @@ +notation "hvbox(a break \to b)" + right associative with precedence 20 +for @{ \forall $_:$a.$b }. + +notation "hvbox(a break = b)" + non associative with precedence 45 +for @{ 'eq $a $b }. + +notation "hvbox(a break \leq b)" + non associative with precedence 45 +for @{ 'leq $a $b }. + +notation "hvbox(a break \geq b)" + non associative with precedence 45 +for @{ 'geq $a $b }. + +notation "hvbox(a break \lt b)" + non associative with precedence 45 +for @{ 'lt $a $b }. + +notation "hvbox(a break \gt b)" + non associative with precedence 45 +for @{ 'gt $a $b }. + +notation "hvbox(a break \neq b)" + non associative with precedence 45 +for @{ 'neq $a $b }. + +notation "hvbox(a break + b)" + left associative with precedence 50 +for @{ 'plus $a $b }. + +notation "hvbox(a break - b)" + left associative with precedence 50 +for @{ 'minus $a $b }. + +notation "hvbox(a break * b)" + left associative with precedence 55 +for @{ 'times $a $b }. + +notation "hvbox(a break / b)" + left associative with precedence 55 +for @{ 'divide $a $b }. + +notation "\frac a b" + non associative with precedence 90 +for @{ 'divide $a $b }. + +notation "a \over b" + left associative with precedence 55 +for @{ 'divide $a $b }. + +notation "- a" + non associative with precedence 60 +for @{ 'uminus $a }. + +notation "\sqrt a" + non associative with precedence 60 +for @{ 'sqrt $a }. + +notation "hvbox(a break \lor b)" + left associative with precedence 30 +for @{ 'or $a $b }. + +notation "hvbox(a break \land b)" + left associative with precedence 35 +for @{ 'and $a $b }. + +notation "hvbox(\lnot a)" + left associative with precedence 40 +for @{ 'not $a }. + +(* aritmetic operators *) + +interpretation "natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y). +interpretation "real plus" 'plus x y = (cic:/Coq/Reals/Rdefinitions/Rplus.con x y). +interpretation "binary integer plus" 'plus x y = (cic:/Coq/ZArith/BinInt/Zplus.con x y). +interpretation "binary positive plus" 'plus x y = (cic:/Coq/NArith/BinPos/Pplus.con x y). +interpretation "natural minus" 'minus x y = (cic:/Coq/Init/Peano/minus.con x y). +interpretation "real minus" 'minus x y = (cic:/Coq/Reals/Rdefinitions/Rminus.con x y). +interpretation "binary integer minus" 'minus x y = (cic:/Coq/ZArith/BinInt/Zminus.con x y). +interpretation "binary positive minus" 'minus x y = (cic:/Coq/NArith/BinPos/Pminus.con x y). +interpretation "natural times" 'times x y = (cic:/Coq/Init/Peano/mult.con x y). +interpretation "real times" 'times x y = (cic:/Coq/Reals/Rdefinitions/Rmult.con x y). +interpretation "binary positive times" 'times x y = (cic:/Coq/NArith/BinPos/Pmult.con x y). +interpretation "binary integer times" 'times x y = (cic:/Coq/ZArith/BinInt/Zmult.con x y). +interpretation "real power" 'power x y = (cic:/Coq/Reals/Rfunctions/pow.con x y). +interpretation "integer power" 'power x y = (cic:/Coq/ZArith/Zpower/Zpower.con x y). +interpretation "real divide" 'divide x y = (cic:/Coq/Reals/Rdefinitions/Rdiv.con x y). +interpretation "real unary minus" 'uminus x = (cic:/Coq/Reals/Rdefinitions/Ropp.con x). +interpretation "binary integer negative sign" 'uminus x = (cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/3) x). +interpretation "binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/BinInt/Zopp.con x). + +(* relational operators *) + +interpretation "natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind x y). +interpretation "real 'less or equal to'" 'leq x y = (cic:/Coq/Reals/Rdefinitions/Rle.con x y). +interpretation "natural 'greater or equal to'" 'geq x y = (cic:/Coq/Init/Peano/ge.con x y). +interpretation "real 'greater or equal to'" 'geq x y = (cic:/Coq/Reals/Rdefinitions/Rge.con x y). +interpretation "natural 'less than'" 'lt x y = (cic:/Coq/Init/Peano/lt.con x y). +interpretation "real 'less than'" 'lt x y = (cic:/Coq/Reals/Rdefinitions/Rlt.con x y). +interpretation "natural 'greater than'" 'gt x y = (cic:/Coq/Init/Peano/gt.con x y). +interpretation "real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinitions/Rgt.con x y). + +interpretation "leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y). +interpretation "not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)). + +(* logical operators *) + +interpretation "logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y). +interpretation "logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y). +interpretation "logical not" 'not x = (cic:/Coq/Init/Logic/not.con x). +interpretation "exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y). + +(* + add_symbol_choice "cast" + ("type cast", + (fun env _ args -> + let t1, t2 = + match args with + | [t1; t2] -> t1, t2 + | _ -> raise Invalid_choice + in + Cic.Cast (t1, t2))); +*) + diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index d01280c90..17a8f4661 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -1,6 +1,6 @@ - + \ @@ -168,4 +168,3 @@ - diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 4e225e03b..6319921eb 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -33,15 +33,14 @@ open MatitaMisc let _ = Helm_registry.load_from BuildTimeConf.matita_conf; + CicNotation.load_notation BuildTimeConf.core_notation_script; Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); MatitaDb.create_owner_environment (); MatitamakeLib.initialize (); GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) ignore (GMain.Main.init ()); - - (* environment trust *) - CicEnvironment.set_trust + CicEnvironment.set_trust (* environment trust *) (let trust = Helm_registry.get_bool "matita.environment_trust" in fun _ -> trust) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index cf83195dc..b456bb6eb 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -1,3 +1,27 @@ +(* Copyright (C) 2005, 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 + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * 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/ + *) open Printf open MatitaTypes @@ -10,6 +34,9 @@ let debug_print = if debug then prerr_endline else ignore ;; type options = { do_heavy_checks: bool ; include_paths: string list } +type statement = + (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement + (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation * using FreshNamesGenerator module *) @@ -25,32 +52,32 @@ let namer_of names = FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ let tactic_of_ast = function - | TacticAst.Absurd (_, term) -> Tactics.absurd term - | TacticAst.Apply (_, term) -> Tactics.apply term - | TacticAst.Assumption _ -> Tactics.assumption - | TacticAst.Auto (_,depth,width) -> + | GrafiteAst.Absurd (_, term) -> Tactics.absurd term + | GrafiteAst.Apply (_, term) -> Tactics.apply term + | GrafiteAst.Assumption _ -> Tactics.assumption + | GrafiteAst.Auto (_,depth,width) -> AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) () - | TacticAst.Change (_, pattern, with_what) -> + | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what - | TacticAst.Clear (_,id) -> Tactics.clear id - | TacticAst.ClearBody (_,id) -> Tactics.clearbody id - | TacticAst.Contradiction _ -> Tactics.contradiction - | TacticAst.Compare (_, term) -> Tactics.compare term - | TacticAst.Constructor (_, n) -> Tactics.constructor n - | TacticAst.Cut (_, ident, term) -> + | GrafiteAst.Clear (_,id) -> Tactics.clear id + | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id + | GrafiteAst.Contradiction _ -> Tactics.contradiction + | GrafiteAst.Compare (_, term) -> Tactics.compare term + | GrafiteAst.Constructor (_, n) -> Tactics.constructor n + | GrafiteAst.Cut (_, ident, term) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.cut ~mk_fresh_name_callback:(namer_of names) term - | TacticAst.DecideEquality _ -> Tactics.decide_equality - | TacticAst.Decompose (_,term) -> Tactics.decompose term - | TacticAst.Discriminate (_,term) -> Tactics.discriminate term - | TacticAst.Elim (_, what, using, depth, names) -> + | GrafiteAst.DecideEquality _ -> Tactics.decide_equality + | GrafiteAst.Decompose (_,term) -> Tactics.decompose term + | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term + | GrafiteAst.Elim (_, what, using, depth, names) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what - | TacticAst.ElimType (_, what, using, depth, names) -> + | GrafiteAst.ElimType (_, what, using, depth, names) -> Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what - | TacticAst.Exact (_, term) -> Tactics.exact term - | TacticAst.Exists _ -> Tactics.exists - | TacticAst.Fail _ -> Tactics.fail - | TacticAst.Fold (_, reduction_kind, term, pattern) -> + | GrafiteAst.Exact (_, term) -> Tactics.exact term + | GrafiteAst.Exists _ -> Tactics.exists + | GrafiteAst.Fail _ -> Tactics.fail + | GrafiteAst.Fold (_, reduction_kind, term, pattern) -> let reduction = match reduction_kind with | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] @@ -59,42 +86,42 @@ let tactic_of_ast = function | `Whd -> CicReduction.whd ~delta:false ~subst:[] in Tactics.fold ~reduction ~term ~pattern - | TacticAst.Fourier _ -> Tactics.fourier - | TacticAst.FwdSimpl (_, hyp, names) -> + | GrafiteAst.Fourier _ -> Tactics.fourier + | GrafiteAst.FwdSimpl (_, hyp, names) -> Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp - | TacticAst.Generalize (_,pattern,ident) -> + | GrafiteAst.Generalize (_,pattern,ident) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern - | TacticAst.Goal (_, n) -> Tactics.set_goal n - | TacticAst.IdTac _ -> Tactics.id - | TacticAst.Injection (_,term) -> Tactics.injection term - | TacticAst.Intros (_, None, names) -> + | GrafiteAst.Goal (_, n) -> Tactics.set_goal n + | GrafiteAst.IdTac _ -> Tactics.id + | GrafiteAst.Injection (_,term) -> Tactics.injection term + | GrafiteAst.Intros (_, None, names) -> PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () - | TacticAst.Intros (_, Some num, names) -> + | GrafiteAst.Intros (_, Some num, names) -> PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) () - | TacticAst.LApply (_, how_many, to_what, what, ident) -> + | GrafiteAst.LApply (_, how_many, to_what, what, ident) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what - | TacticAst.Left _ -> Tactics.left - | TacticAst.LetIn (loc,term,name) -> + | GrafiteAst.Left _ -> Tactics.left + | GrafiteAst.LetIn (loc,term,name) -> Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) - | TacticAst.Reduce (_, reduction_kind, pattern) -> + | GrafiteAst.Reduce (_, reduction_kind, pattern) -> (match reduction_kind with | `Normalize -> Tactics.normalize ~pattern | `Reduce -> Tactics.reduce ~pattern | `Simpl -> Tactics.simpl ~pattern | `Whd -> Tactics.whd ~pattern) - | TacticAst.Reflexivity _ -> Tactics.reflexivity - | TacticAst.Replace (_, pattern, with_what) -> + | GrafiteAst.Reflexivity _ -> Tactics.reflexivity + | GrafiteAst.Replace (_, pattern, with_what) -> Tactics.replace ~pattern ~with_what - | TacticAst.Rewrite (_, direction, t, pattern) -> + | GrafiteAst.Rewrite (_, direction, t, pattern) -> EqualityTactics.rewrite_tac ~direction ~pattern t - | TacticAst.Right _ -> Tactics.right - | TacticAst.Ring _ -> Tactics.ring - | TacticAst.Split _ -> Tactics.split - | TacticAst.Symmetry _ -> Tactics.symmetry - | TacticAst.Transitivity (_, term) -> Tactics.transitivity term + | GrafiteAst.Right _ -> Tactics.right + | GrafiteAst.Ring _ -> Tactics.ring + | GrafiteAst.Split _ -> Tactics.split + | GrafiteAst.Symmetry _ -> Tactics.symmetry + | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term let disambiguate_term status term = let (aliases, metasenv, cic, _) = @@ -132,105 +159,105 @@ let disambiguate_pattern status (wanted, hyp_paths, goal_path) = status, (wanted, hyp_paths ,goal_path) let disambiguate_tactic status = function - | TacticAst.Apply (loc, term) -> + | GrafiteAst.Apply (loc, term) -> let status, cic = disambiguate_term status term in - status, TacticAst.Apply (loc, cic) - | TacticAst.Absurd (loc, term) -> + status, GrafiteAst.Apply (loc, cic) + | GrafiteAst.Absurd (loc, term) -> let status, cic = disambiguate_term status term in - status, TacticAst.Absurd (loc, cic) - | TacticAst.Assumption loc -> status, TacticAst.Assumption loc - | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width) - | TacticAst.Change (loc, pattern, with_what) -> + status, GrafiteAst.Absurd (loc, cic) + | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc + | GrafiteAst.Auto (loc,depth,width) -> status, GrafiteAst.Auto (loc,depth,width) + | GrafiteAst.Change (loc, pattern, with_what) -> let status, with_what = disambiguate_term status with_what in let status, pattern = disambiguate_pattern status pattern in - status, TacticAst.Change (loc, pattern, with_what) - | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id) - | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id) - | TacticAst.Compare (loc,term) -> + status, GrafiteAst.Change (loc, pattern, with_what) + | GrafiteAst.Clear (loc,id) -> status,GrafiteAst.Clear (loc,id) + | GrafiteAst.ClearBody (loc,id) -> status,GrafiteAst.ClearBody (loc,id) + | GrafiteAst.Compare (loc,term) -> let status, term = disambiguate_term status term in - status, TacticAst.Compare (loc,term) - | TacticAst.Constructor (loc,n) -> - status, TacticAst.Constructor (loc,n) - | TacticAst.Contradiction loc -> - status, TacticAst.Contradiction loc - | TacticAst.Cut (loc, ident, term) -> + status, GrafiteAst.Compare (loc,term) + | GrafiteAst.Constructor (loc,n) -> + status, GrafiteAst.Constructor (loc,n) + | GrafiteAst.Contradiction loc -> + status, GrafiteAst.Contradiction loc + | GrafiteAst.Cut (loc, ident, term) -> let status, cic = disambiguate_term status term in - status, TacticAst.Cut (loc, ident, cic) - | TacticAst.DecideEquality loc -> - status, TacticAst.DecideEquality loc - | TacticAst.Decompose (loc,term) -> + status, GrafiteAst.Cut (loc, ident, cic) + | GrafiteAst.DecideEquality loc -> + status, GrafiteAst.DecideEquality loc + | GrafiteAst.Decompose (loc,term) -> let status,term = disambiguate_term status term in - status, TacticAst.Decompose(loc,term) - | TacticAst.Discriminate (loc,term) -> + status, GrafiteAst.Decompose(loc,term) + | GrafiteAst.Discriminate (loc,term) -> let status,term = disambiguate_term status term in - status, TacticAst.Discriminate(loc,term) - | TacticAst.Exact (loc, term) -> + status, GrafiteAst.Discriminate(loc,term) + | GrafiteAst.Exact (loc, term) -> let status, cic = disambiguate_term status term in - status, TacticAst.Exact (loc, cic) - | TacticAst.Elim (loc, what, Some using, depth, idents) -> + status, GrafiteAst.Exact (loc, cic) + | GrafiteAst.Elim (loc, what, Some using, depth, idents) -> let status, what = disambiguate_term status what in let status, using = disambiguate_term status using in - status, TacticAst.Elim (loc, what, Some using, depth, idents) - | TacticAst.Elim (loc, what, None, depth, idents) -> + status, GrafiteAst.Elim (loc, what, Some using, depth, idents) + | GrafiteAst.Elim (loc, what, None, depth, idents) -> let status, what = disambiguate_term status what in - status, TacticAst.Elim (loc, what, None, depth, idents) - | TacticAst.ElimType (loc, what, Some using, depth, idents) -> + status, GrafiteAst.Elim (loc, what, None, depth, idents) + | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> let status, what = disambiguate_term status what in let status, using = disambiguate_term status using in - status, TacticAst.ElimType (loc, what, Some using, depth, idents) - | TacticAst.ElimType (loc, what, None, depth, idents) -> + status, GrafiteAst.ElimType (loc, what, Some using, depth, idents) + | GrafiteAst.ElimType (loc, what, None, depth, idents) -> let status, what = disambiguate_term status what in - status, TacticAst.ElimType (loc, what, None, depth, idents) - | TacticAst.Exists loc -> status, TacticAst.Exists loc - | TacticAst.Fail loc -> status,TacticAst.Fail loc - | TacticAst.Fold (loc,reduction_kind, term, pattern) -> + status, GrafiteAst.ElimType (loc, what, None, depth, idents) + | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc + | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc + | GrafiteAst.Fold (loc,reduction_kind, term, pattern) -> let status, pattern = disambiguate_pattern status pattern in let status, term = disambiguate_term status term in - status, TacticAst.Fold (loc,reduction_kind, term, pattern) - | TacticAst.FwdSimpl (loc, hyp, names) -> - status, TacticAst.FwdSimpl (loc, hyp, names) - | TacticAst.Fourier loc -> status, TacticAst.Fourier loc - | TacticAst.Generalize (loc,pattern,ident) -> + status, GrafiteAst.Fold (loc,reduction_kind, term, pattern) + | GrafiteAst.FwdSimpl (loc, hyp, names) -> + status, GrafiteAst.FwdSimpl (loc, hyp, names) + | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc + | GrafiteAst.Generalize (loc,pattern,ident) -> let status, pattern = disambiguate_pattern status pattern in - status, TacticAst.Generalize(loc,pattern,ident) - | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) - | TacticAst.IdTac loc -> status,TacticAst.IdTac loc - | TacticAst.Injection (loc,term) -> + status, GrafiteAst.Generalize(loc,pattern,ident) + | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g) + | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc + | GrafiteAst.Injection (loc,term) -> let status, term = disambiguate_term status term in - status, TacticAst.Injection (loc,term) - | TacticAst.Intros (loc, num, names) -> - status, TacticAst.Intros (loc, num, names) - | TacticAst.LApply (loc, depth, to_what, what, ident) -> + status, GrafiteAst.Injection (loc,term) + | GrafiteAst.Intros (loc, num, names) -> + status, GrafiteAst.Intros (loc, num, names) + | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> let f term (status, to_what) = let status, term = disambiguate_term status term in status, term :: to_what in let status, to_what = List.fold_right f to_what (status, []) in let status, what = disambiguate_term status what in - status, TacticAst.LApply (loc, depth, to_what, what, ident) - | TacticAst.Left loc -> status, TacticAst.Left loc - | TacticAst.LetIn (loc, term, name) -> + status, GrafiteAst.LApply (loc, depth, to_what, what, ident) + | GrafiteAst.Left loc -> status, GrafiteAst.Left loc + | GrafiteAst.LetIn (loc, term, name) -> let status, term = disambiguate_term status term in - status, TacticAst.LetIn (loc,term,name) - | TacticAst.Reduce (loc, reduction_kind, pattern) -> + status, GrafiteAst.LetIn (loc,term,name) + | GrafiteAst.Reduce (loc, reduction_kind, pattern) -> let status, pattern = disambiguate_pattern status pattern in - status, TacticAst.Reduce(loc, reduction_kind, pattern) - | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc - | TacticAst.Replace (loc, pattern, with_what) -> + status, GrafiteAst.Reduce(loc, reduction_kind, pattern) + | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc + | GrafiteAst.Replace (loc, pattern, with_what) -> let status, pattern = disambiguate_pattern status pattern in let status, with_what = disambiguate_term status with_what in - status, TacticAst.Replace (loc, pattern, with_what) - | TacticAst.Rewrite (loc, dir, t, pattern) -> + status, GrafiteAst.Replace (loc, pattern, with_what) + | GrafiteAst.Rewrite (loc, dir, t, pattern) -> let status, term = disambiguate_term status t in let status, pattern = disambiguate_pattern status pattern in - status, TacticAst.Rewrite (loc, dir, term, pattern) - | TacticAst.Right loc -> status, TacticAst.Right loc - | TacticAst.Ring loc -> status, TacticAst.Ring loc - | TacticAst.Split loc -> status, TacticAst.Split loc - | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc - | TacticAst.Transitivity (loc, term) -> + status, GrafiteAst.Rewrite (loc, dir, term, pattern) + | GrafiteAst.Right loc -> status, GrafiteAst.Right loc + | GrafiteAst.Ring loc -> status, GrafiteAst.Ring loc + | GrafiteAst.Split loc -> status, GrafiteAst.Split loc + | GrafiteAst.Symmetry loc -> status, GrafiteAst.Symmetry loc + | GrafiteAst.Transitivity (loc, term) -> let status, cic = disambiguate_term status term in - status, TacticAst.Transitivity (loc, cic) + status, GrafiteAst.Transitivity (loc, cic) let apply_tactic tactic status = let status,tactic = disambiguate_tactic status tactic in @@ -255,7 +282,8 @@ module MatitaStatus = let set_goals (status,_) goals = status,goals - let id_tac status = apply_tactic (TacticAst.IdTac CicAst.dummy_floc) status + let id_tac status = + apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status let mk_tactic tac = tac @@ -268,22 +296,22 @@ module MatitaTacticals = Tacticals.Make(MatitaStatus) let eval_tactical status tac = let rec tactical_of_ast tac = match tac with - | TacticAst.Tactic (loc, tactic) -> apply_tactic tactic - | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) + | GrafiteAst.Tactic (loc, tactic) -> apply_tactic tactic + | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) MatitaTacticals.seq ~tactics:(List.map tactical_of_ast tacticals) - | TacticAst.Do (loc, num, tactical) -> + | GrafiteAst.Do (loc, num, tactical) -> MatitaTacticals.do_tactic ~n:num ~tactic:(tactical_of_ast tactical) - | TacticAst.Repeat (loc, tactical) -> + | GrafiteAst.Repeat (loc, tactical) -> MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast tactical) - | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) + | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) MatitaTacticals.thens ~start:(tactical_of_ast tactical) ~continuations:(List.map tactical_of_ast tacticals) - | TacticAst.First (loc, tacticals) -> + | GrafiteAst.First (loc, tacticals) -> MatitaTacticals.first ~tactics:(List.map (fun t -> "", tactical_of_ast t) tacticals) - | TacticAst.Try (loc, tactical) -> + | GrafiteAst.Try (loc, tactical) -> MatitaTacticals.try_tactic ~tactic:(tactical_of_ast tactical) - | TacticAst.Solve (loc, tacticals) -> + | GrafiteAst.Solve (loc, tacticals) -> MatitaTacticals.solve_tactics ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals) in @@ -353,11 +381,11 @@ let eval_coercion status coercion = List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status) status new_coercions in let statement_of name = - TacticAstPp.pp_statement - (TacticAst.Executable (CicAst.dummy_floc, - (TacticAst.Command (CicAst.dummy_floc, - (TacticAst.Coercion (CicAst.dummy_floc, - (CicAst.Ident (name, None)))))))) ^ "\n" + GrafiteAstPp.pp_statement + (GrafiteAst.Executable (Disambiguate.dummy_floc, + (GrafiteAst.Command (Disambiguate.dummy_floc, + (GrafiteAst.Coercion (Disambiguate.dummy_floc, + (CicNotationPt.Ident (name, None)))))))) ^ "\n" in let moo_content_rev = [statement_of (UriManager.name_of_uri coer_uri)] @ @@ -409,11 +437,11 @@ let eval_from_stream_ref = ref (fun _ _ _ -> assert false);; let disambiguate_obj status obj = let uri = match obj with - TacticAst.Inductive (_,(name,_,_,_)::_) - | TacticAst.Record (_,name,_,_) -> + GrafiteAst.Inductive (_,(name,_,_,_)::_) + | GrafiteAst.Record (_,name,_,_) -> Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind")) - | TacticAst.Inductive _ -> assert false - | TacticAst.Theorem _ -> None in + | GrafiteAst.Inductive _ -> assert false + | GrafiteAst.Theorem _ -> None in let (aliases, metasenv, cic, _) = match MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) @@ -434,17 +462,23 @@ let disambiguate_obj status obj = status, cic let disambiguate_command status = function - | TacticAst.Default _ - | TacticAst.Alias _ - | TacticAst.Include _ as cmd -> status,cmd - | TacticAst.Coercion (loc, term) -> + | GrafiteAst.Alias _ + | GrafiteAst.Default _ + | GrafiteAst.Drop _ + | GrafiteAst.Dump _ + | GrafiteAst.Include _ + | GrafiteAst.Interpretation _ + | GrafiteAst.Notation _ + | GrafiteAst.Qed _ + | GrafiteAst.Render _ + | GrafiteAst.Set _ as cmd -> + status,cmd + | GrafiteAst.Coercion (loc, term) -> let status, term = disambiguate_term status term in - status, TacticAst.Coercion (loc,term) - | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd -> - status, cmd - | TacticAst.Obj (loc,obj) -> + status, GrafiteAst.Coercion (loc,term) + | GrafiteAst.Obj (loc,obj) -> let status,obj = disambiguate_obj status obj in - status, TacticAst.Obj (loc,obj) + status, GrafiteAst.Obj (loc,obj) let try_open_in paths path = let rec aux = function @@ -464,13 +498,17 @@ let try_open_in paths path = ;; let eval_command opts status cmd = - let status,cmd = disambiguate_command status cmd in + let status,cmd = disambiguate_command status cmd in + let cmd,notation_ids' = CicNotation.process_notation cmd in + let status = + { status with notation_ids = notation_ids' @ status.notation_ids } + in match cmd with - | TacticAst.Default (loc, what, uris) as cmd -> + | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; {status with moo_content_rev = - (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev} - | TacticAst.Include (loc, path) -> + (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev} + | GrafiteAst.Include (loc, path) -> let path = MatitaMisc.obj_file_of_script path in let stream = try @@ -480,7 +518,7 @@ let eval_command opts status cmd = let status = ref status in !eval_from_stream_ref status stream (fun _ _ -> ()); !status - | TacticAst.Set (loc, name, value) -> + | GrafiteAst.Set (loc, name, value) -> let value = if name = "baseuri" then let v = MatitaMisc.strip_trailing_slash value in @@ -492,8 +530,8 @@ let eval_command opts status cmd = value in set_option status name value - | TacticAst.Drop loc -> raise Drop - | TacticAst.Qed loc -> + | GrafiteAst.Drop loc -> raise Drop + | GrafiteAst.Qed loc -> let uri, metasenv, bo, ty = match status.proof_status with | Proof (Some uri, metasenv, body, ty) -> @@ -510,28 +548,32 @@ let eval_command opts status cmd = let name = UriManager.name_of_uri uri in let obj = Cic.Constant (name,Some bo,ty,[],[]) in MatitaSync.add_obj uri obj status - | TacticAst.Coercion (loc, coercion) -> + | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion - | TacticAst.Alias (loc, spec) -> + | GrafiteAst.Alias (loc, spec) -> let aliases = match spec with - | TacticAst.Ident_alias (id,uri) -> + | GrafiteAst.Ident_alias (id,uri) -> DisambiguateTypes.Environment.add (DisambiguateTypes.Id id) (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) status.aliases - | TacticAst.Symbol_alias (symb, instance, desc) -> - DisambiguateTypes.Environment.add + | GrafiteAst.Symbol_alias (symb, instance, desc) -> + DisambiguateTypes.Environment.add (DisambiguateTypes.Symbol (symb,instance)) - (DisambiguateChoices.lookup_symbol_by_dsc symb desc) + (DisambiguateChoices.lookup_symbol_by_dsc symb desc) status.aliases - | TacticAst.Number_alias (instance,desc) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Num instance) + | GrafiteAst.Number_alias (instance,desc) -> + DisambiguateTypes.Environment.add + (DisambiguateTypes.Num instance) (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases in MatitaSync.set_proof_aliases status aliases - | TacticAst.Obj (loc,obj) -> + | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *) + | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *) + | GrafiteAst.Interpretation _ + | GrafiteAst.Notation _ -> status + | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with Cic.Constant (name,_,_,_,_) @@ -601,11 +643,11 @@ let eval_command opts status cmd = let eval_executable opts status ex = match ex with - | TacticAst.Tactical (_, tac) -> eval_tactical status tac - | TacticAst.Command (_, cmd) -> eval_command opts status cmd - | TacticAst.Macro (_, mac) -> + | GrafiteAst.Tactical (_, tac) -> eval_tactical status tac + | GrafiteAst.Command (_, cmd) -> eval_command opts status cmd + | GrafiteAst.Macro (_, mac) -> command_error (sprintf "The macro %s can't be in a script" - (TacticAstPp.pp_macro_ast mac)) + (GrafiteAstPp.pp_macro_ast mac)) let eval_comment status c = status @@ -615,26 +657,26 @@ let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st = {do_heavy_checks = do_heavy_checks ; include_paths = include_paths} in match st with - | TacticAst.Executable (_,ex) -> eval_executable opts status ex - | TacticAst.Comment (_,c) -> eval_comment status c + | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex + | GrafiteAst.Comment (_,c) -> eval_comment status c let eval_from_stream ?do_heavy_checks ?include_paths status str cb = - let stl = CicTextualParser2.parse_statements str in - List.iter - (fun ast -> - cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths !status ast) - stl -;; + try + while true do + let ast = GrafiteParser.parse_statement str in + cb !status ast; + status := eval_ast ?do_heavy_checks ?include_paths !status ast + done + with End_of_file -> () (* to avoid a long list of recursive functions *) -eval_from_stream_ref := eval_from_stream;; +let _ = eval_from_stream_ref := eval_from_stream let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb = while true do print_string "matita> "; flush stdout; - let ast = CicTextualParser2.parse_statement str in + let ast = GrafiteParser.parse_statement str in cb !status ast; status := eval_ast ?do_heavy_checks ?include_paths !status ast done @@ -667,6 +709,6 @@ let initial_status = proof_status = No_proof; options = default_options (); objects = []; + notation_ids = []; } - diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 7ceb965e9..6b9f235cd 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -26,6 +26,9 @@ exception Drop exception UnableToInclude of string +type statement = + (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement + (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) val eval_string: @@ -37,23 +40,21 @@ val eval_from_stream: ?do_heavy_checks:bool -> ?include_paths:string list -> MatitaTypes.status ref -> char Stream.t -> - (MatitaTypes.status -> - (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> + (MatitaTypes.status -> statement -> unit) -> unit val eval_from_stream_greedy: ?do_heavy_checks:bool -> ?include_paths:string list -> MatitaTypes.status ref-> char Stream.t -> - (MatitaTypes.status -> - (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> + (MatitaTypes.status -> statement -> unit) -> unit val eval_ast: ?do_heavy_checks:bool -> ?include_paths:string list -> MatitaTypes.status -> - (CicAst.term,TacticAst.obj,string) TacticAst.statement -> + statement -> MatitaTypes.status val initial_status: MatitaTypes.status lazy_t diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index 74f2c9f41..2c46da4f5 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -31,8 +31,8 @@ let to_string = "Baseuri not set for this script. " ^ "Use 'set \"baseuri\" \"\".' to set it." | MatitaTypes.Command_error msg -> "Error: " ^ msg - | CicTextualParser2.Parse_error (floc,err) -> - let (x, y) = CicAst.loc_of_floc floc in + | CicNotationParser.Parse_error (floc,err) -> + let (x, y) = CicNotationPt.loc_of_floc floc in sprintf "Parse error at %d-%d: %s" x y err | UriManager.IllFormedUri uri -> sprintf "invalid uri: %s" uri | CicEnvironment.Object_not_found uri -> diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 51b17451e..efe629ac1 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -322,19 +322,20 @@ class gui () = (fun _ -> adj#set_value (adj#upper -. adj#page_size))); console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version); (* toolbar *) - let module A = TacticAst in - let hole = CicAst.UserInput in - let loc = CicAst.dummy_floc in + let module A = GrafiteAst in + let hole = CicNotationPt.UserInput in + let loc = Disambiguate.dummy_floc in let tac ast _ = if (MatitaScript.instance ())#onGoingProof () then (MatitaScript.instance ())#advance - ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) () + ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast))) + () in let tac_w_term ast _ = if (MatitaScript.instance ())#onGoingProof () then let buf = source_buffer in buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) - ("\n" ^ TacticAstPp.pp_tactic ast) + ("\n" ^ GrafiteAstPp.pp_tactic ast) in let tbar = self#main in connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 4a6115813..f1a0e6429 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -61,8 +61,8 @@ let prepend_text header base = (** creates a statement AST for the Goal tactic, e.g. "goal 7" *) let goal_ast n = - let module A = TacticAst in - let loc = CicAst.dummy_floc in + let module A = GrafiteAst in + let loc = Disambiguate.dummy_floc in A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))) type guistuff = { @@ -74,8 +74,8 @@ type guistuff = { } let eval_with_engine guistuff status user_goal parsed_text st = - let module TA = TacticAst in - let module TAPp = TacticAstPp in + let module TA = GrafiteAst in + let module TAPp = GrafiteAstPp in let include_ = match guistuff.filenamedata with | None,None -> [] @@ -130,7 +130,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = if DisambiguateTypes.Environment.is_empty new_aliases then parsed_text else - prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases) + prepend_text (DisambiguatePp.pp_environment new_aliases) parsed_text in let new_text = @@ -208,8 +208,8 @@ let disambiguate term status = let eval_macro guistuff status parsed_text script mac = - let module TA = TacticAst in - let module TAPp = TacticAstPp in + let module TA = GrafiteAst in + let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in let module MDB = MatitaDb in let module CTC = CicTypeChecker in @@ -267,7 +267,7 @@ let eval_macro guistuff status parsed_text script mac TA.Executable (loc, (TA.Tactical (loc, TA.Tactic (loc, - TA.Apply (loc, CicAst.Uri (UriManager.string_of_uri uri,None)))))) + TA.Apply (loc, CicNotationPt.Uri (UriManager.string_of_uri uri,None)))))) in let new_status = MatitaEngine.eval_ast status ast in let extra_text = @@ -323,8 +323,8 @@ let eval_macro guistuff status parsed_text script mac let eval_executable guistuff status user_goal parsed_text script ex = - let module TA = TacticAst in - let module TAPp = TacticAstPp in + let module TA = GrafiteAst in + let module TAPp = GrafiteAstPp in let module MD = MatitaDisambiguator in let module ML = MatitacleanLib in let parsed_text_length = String.length parsed_text in @@ -354,14 +354,14 @@ let eval_executable guistuff status user_goal parsed_text script ex = let rec eval_statement guistuff status user_goal script s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - let st = CicTextualParser2.parse_statement (Stream.of_string s) in + let st = GrafiteParser.parse_statement (Stream.of_string s) in let text_of_loc loc = - let parsed_text_length = snd (CicAst.loc_of_floc loc) in + let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in let parsed_text = safe_substring s 0 parsed_text_length in parsed_text, parsed_text_length in match st with - | TacticAst.Comment (loc,_)-> + | GrafiteAst.Comment (loc,_)-> let parsed_text, parsed_text_length = text_of_loc loc in let remain_len = String.length s - parsed_text_length in let s = String.sub s parsed_text_length remain_len in @@ -372,7 +372,7 @@ let rec eval_statement guistuff status user_goal script s = | (status, text) :: tl -> ((status, parsed_text ^ text)::tl), (parsed_text_length + len) | [] -> [], 0) - | TacticAst.Executable (loc, ex) -> + | GrafiteAst.Executable (loc, ex) -> let parsed_text, parsed_text_length = text_of_loc loc in eval_executable guistuff status user_goal parsed_text script ex @@ -638,19 +638,19 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; let s = self#getFuture in let rec is_there_and_executable s = if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - let st = CicTextualParser2.parse_statement (Stream.of_string s) in + let st = GrafiteParser.parse_statement (Stream.of_string s) in match st with - | TacticAst.Comment (loc,_)-> - let parsed_text_length = snd (CicAst.loc_of_floc loc) in + | GrafiteAst.Comment (loc,_)-> + let parsed_text_length = snd (CicNotationPt.loc_of_floc loc) in let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in is_there_and_executable next - | TacticAst.Executable (loc, ex) -> false + | GrafiteAst.Executable (loc, ex) -> false in try is_there_and_executable s with - | CicTextualParser2.Parse_error _ -> false + | CicNotationParser.Parse_error _ -> false | Margin -> true diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index b54c67790..4df2ab7fb 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -50,7 +50,7 @@ let set_proof_aliases status aliases = let new_status = {status with aliases = aliases } in let diff = alias_diff ~from:status new_status in let moo_content_rev = - CicTextualParser2.EnvironmentP3.to_string diff :: + DisambiguatePp.pp_environment diff :: status.moo_content_rev in {new_status with moo_content_rev = moo_content_rev} @@ -167,44 +167,55 @@ struct let compare (u1, _) (u2, _) = UriManager.compare u1 u2 end +module OrderedId = +struct + type t = CicNotation.notation_id + let compare = Pervasives.compare +end + module UriSet = Set.Make (OrderedUri) +module IdSet = Set.Make (OrderedId) -(* returns the uri of objects that were added in the meanwhile... - * status1 ----> status2 - * assumption: objects defined in status2 are a superset of those defined in - * status1 - *) -let delta_status status1 status2 = + (** @return l2 \ l1 *) +let uri_list_diff l2 l1 = let module S = UriSet in - let diff l1 l2 = - let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in - let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in - let diff = S.diff s2 s1 in - S.fold (fun uri uris -> uri :: uris) diff [] - in - diff status1.objects status2.objects + let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in + let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in + let diff = S.diff s2 s1 in + S.fold (fun uri uris -> uri :: uris) diff [] + + (** @return l2 \ l1 *) +let id_list_diff l2 l1 = + let module S = IdSet in + let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in + let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in + let diff = S.diff s2 s1 in + S.fold (fun uri uris -> uri :: uris) diff [] let remove_coercion uri = CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) let time_travel ~present ~past = - let list_of_objs_to_remove = List.rev (delta_status past present) in - (* List.rev is just for the debugging code, which otherwise may list both - * something.ind and something.ind#xpointer ... (ask Enrico :-) *) + let objs_to_remove = uri_list_diff present.objects past.objects in + let notation_to_remove = + id_list_diff present.notation_ids past.notation_ids + in let debug_list = ref [] in - List.iter (fun (uri,p) -> - MatitaMisc.safe_remove p; - remove_coercion uri; - (try - CicEnvironment.remove_obj uri - with CicEnvironment.Object_not_found _ -> - MatitaLog.debug - (sprintf "time_travel removes from cache %s that is not in" - (UriManager.string_of_uri uri))); - let l = MatitaDb.remove_uri uri in - debug_list := UriManager.string_of_uri uri :: !debug_list @ l) - list_of_objs_to_remove; - + List.iter + (fun (uri,p) -> + MatitaMisc.safe_remove p; + remove_coercion uri; + (try + CicEnvironment.remove_obj uri + with CicEnvironment.Object_not_found _ -> + MatitaLog.debug + (sprintf "time_travel removes from cache %s that is not in" + (UriManager.string_of_uri uri))); + let l = MatitaDb.remove_uri uri in + debug_list := UriManager.string_of_uri uri :: !debug_list @ l) + objs_to_remove; + List.iter CicNotation.remove_notation notation_to_remove + (* (* this is debug code * idea: debug_list is the list of objects to be removed as computed from the * db, while list_of_objs_to_remove is the same list but computer from the @@ -230,6 +241,7 @@ let time_travel ~present ~past = List.iter MatitaLog.debug l1; MatitaLog.debug "l2:"; List.iter MatitaLog.debug l2 + *) let remove ~verbose uri = let derived_uris_of_uri uri = diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index e349a6e4d..1e5957ae8 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -58,18 +58,18 @@ type options = option_value StringMap.t let no_options = StringMap.empty type status = { - aliases: DisambiguateTypes.environment; (** disambiguation aliases *) - moo_content_rev: string list; (*CSC: a TacticAst.command list would be better *) - proof_status: proof_status; - options: options; - objects: (UriManager.uri * string) list; - (** in-scope objects, with their paths *) + aliases : DisambiguateTypes.environment; + moo_content_rev : string list; + proof_status : proof_status; + options : options; + objects : (UriManager.uri * string) list; + notation_ids: CicNotation.notation_id list; } let dump_status status = MatitaLog.message "status.aliases:\n"; MatitaLog.message - (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n"); + (DisambiguatePp.pp_environment status.aliases ^ "\n"); MatitaLog.message "status.proof_status:"; MatitaLog.message (match status.proof_status with diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index 662dad6ab..c36afca24 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -48,11 +48,12 @@ type options = option_value StringMap.t val no_options : 'a StringMap.t type status = { - aliases : DisambiguateTypes.environment; - moo_content_rev : string list; - proof_status : proof_status; - options : options; - objects : (UriManager.uri * string) list; + aliases: DisambiguateTypes.environment; (** disambiguation aliases *) + moo_content_rev: string list;(*CSC: GrafiteAst.command list would be better *) + proof_status: proof_status; + options: options; + objects: (UriManager.uri * string) list; (** in-scope objects, with paths *) + notation_ids: CicNotation.notation_id list; (** in-scope notation ids *) } val dump_status : status -> unit diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 37bb571ef..076be5416 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -59,7 +59,7 @@ let run_script is eval_function = else fun status stm -> (* dump_status status; *) - let stm = TacticAstPp.pp_statement stm in + let stm = GrafiteAstPp.pp_statement stm in let stm = Pcre.replace ~rex:slash_n_RE stm in let stm = if String.length stm > 50 then @@ -73,7 +73,7 @@ let run_script is eval_function = eval_function status is cb with | MatitaEngine.Drop - | CicTextualParser2.Parse_error _ as exn -> raise exn + | CicNotationParser.Parse_error _ as exn -> raise exn | exn -> MatitaLog.error (MatitaExcPp.to_string exn); raise exn @@ -119,7 +119,7 @@ let rec interactive_loop () = | MatitaEngine.Drop -> pp_ocaml_mode () | Sys.Break -> MatitaLog.error "user break!"; interactive_loop () | MatitaTypes.Command_error _ -> interactive_loop () - | CicTextualParser2.Parse_error (floc,err) -> + | CicNotationParser.Parse_error (floc,err) -> (* check for EOI *) if Stream.peek str = None then begin @@ -127,7 +127,7 @@ let rec interactive_loop () = clean_exit (Some 0) end else - let (x, y) = CicAst.loc_of_floc floc in + let (x, y) = CicNotationPt.loc_of_floc floc in MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); interactive_loop () | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop () @@ -149,6 +149,7 @@ let dump_moo_to_file file moo = let main ~mode = Helm_registry.load_from BuildTimeConf.matita_conf; + CicNotation.load_notation BuildTimeConf.core_notation_script; Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); MatitaDb.create_owner_environment (); @@ -218,8 +219,8 @@ let main ~mode = clean_exit (Some 1) else pp_ocaml_mode () - | CicTextualParser2.Parse_error (floc,err) -> - let (x, y) = CicAst.loc_of_floc floc in + | CicNotationParser.Parse_error (floc,err) -> + let (x, y) = CicNotationPt.loc_of_floc floc in MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); if mode = `COMPILER then clean_exit (Some 1) diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index df6fdfecb..d37f0bfdd 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -1,8 +1,34 @@ +(* Copyright (C) 2005, 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 + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * 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/ + *) + module UM = UriManager;; -module TA = TacticAst;; +module TA = GrafiteAst;; let _ = Helm_registry.load_from BuildTimeConf.matita_conf; + CicNotation.load_notation BuildTimeConf.core_notation_script; Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); MatitaDb.create_owner_environment () @@ -19,7 +45,7 @@ let usage () = prerr_endline ""; exit 1 -let _ = +let _ = if Array.length Sys.argv < 2 then usage (); if Sys.argv.(1) = "all" then begin diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 06c6835ca..c34084d34 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -30,10 +30,9 @@ module HGT = Http_getter_types;; module HG = Http_getter;; module HGM = Http_getter_misc;; module UM = UriManager;; -module TA = TacticAst;; +module TA = GrafiteAst;; let baseuri_of_baseuri_decl st = - let module TA = TacticAst in match st with | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> Some buri @@ -130,12 +129,12 @@ let close_uri_list uri_to_remove = uri_to_remove, depend let baseuri_of_file file = + let uri = ref None in let ic = open_in file in - let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in - close_in ic; - let uri = ref "" in - List.iter - (fun stm -> + let istream = Stream.of_channel ic in + (try + while true do + let stm = GrafiteParser.parse_statement istream in match baseuri_of_baseuri_decl stm with | Some buri -> let u = MatitaMisc.strip_trailing_slash buri in @@ -147,10 +146,14 @@ let baseuri_of_file file = | HGT.Unresolvable_URI _ -> MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) | HGT.Key_not_found _ -> ()); - uri := u - | None -> ()) - stms; - !uri + uri := Some u; + raise End_of_file + | None -> () + done + with End_of_file -> close_in ic); + match !uri with + | Some uri -> uri + | None -> failwith ("No baseuri defined in " ^ file) let rec fix uris next = match next with diff --git a/helm/matita/matitacleanLib.mli b/helm/matita/matitacleanLib.mli index 7077ed41e..a63a8edb0 100644 --- a/helm/matita/matitacleanLib.mli +++ b/helm/matita/matitacleanLib.mli @@ -26,7 +26,7 @@ val clean_baseuris : ?verbose:bool -> string list -> unit val baseuri_of_file : string -> string -val baseuri_of_baseuri_decl : ('a, 'b, 'c) TacticAst.statement -> string option +val baseuri_of_baseuri_decl : ('a, 'b, 'c) GrafiteAst.statement -> string option (** check whether no objects are defined below a given baseuri *) val is_empty: string -> bool diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index bd05558f3..56c60aff8 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -35,7 +35,7 @@ let usage = Printf.sprintf "MatitaDep v%s\nUsage: matitadep [options] file...\nOptions:" BuildTimeConf.version -module TA = TacticAst +module TA = GrafiteAst module U = UriManager let deps = Hashtbl.create (Array.length Sys.argv) @@ -78,39 +78,39 @@ let find path = ;; let main () = + Helm_registry.load_from BuildTimeConf.matita_conf; + CicNotation.load_notation BuildTimeConf.core_notation_script; let files = ref [] in Arg.parse arg_spec (add_l files) usage; List.iter (fun file -> let ic = open_in file in - let stms = - try - CicTextualParser2.parse_statements (Stream.of_channel ic) - with - (CicTextualParser2.Parse_error _) as exc -> - prerr_endline ("Unable to parse: " ^ file); - prerr_endline (MatitaExcPp.to_string exc); - exit 1 - in - close_in ic; - List.iter - (function - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> - let uri = MatitaMisc.strip_trailing_slash uri in - baseuri := (uri, file) :: !baseuri - | TA.Executable (_, TA.Command - (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> - Hashtbl.add aliases file uri - | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> - Hashtbl.add deps file (find path) - | _ -> ()) - stms; + let istream = Stream.of_channel ic in + (try + while true do + match GrafiteParser.parse_statement istream with + | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> + let uri = MatitaMisc.strip_trailing_slash uri in + baseuri := (uri, file) :: !baseuri + | TA.Executable (_, TA.Command + (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> + Hashtbl.add aliases file uri + | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> + Hashtbl.add deps file (find path) + | _ -> () + done + with + | CicNotationParser.Parse_error _ as exn -> + prerr_endline ("Unable to parse: " ^ file); + prerr_endline (MatitaExcPp.to_string exn); + exit 1 + | End_of_file -> close_in ic); Hashtbl.iter (fun file alias -> let dep = resolve alias in match dep with | None -> () | Some d -> Hashtbl.add deps file d) - aliases;) + aliases) !files; List.iter (fun file -> let deps = Hashtbl.find_all deps file in @@ -125,5 +125,6 @@ let main () = !files ;; +let _ = + main () -let _ = main () diff --git a/helm/matita/tests/absurd.ma b/helm/matita/tests/absurd.ma index ce110718a..f5f27f622 100644 --- a/helm/matita/tests/absurd.ma +++ b/helm/matita/tests/absurd.ma @@ -24,4 +24,4 @@ intros. absurd a. assumption. assumption. -qed. \ No newline at end of file +qed. diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index 565a5c49a..8958b250d 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -95,4 +95,5 @@ theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z). intros 1. elim x. clear x. auto. clear H. fwd H1 [H]. decompose H. -*) \ No newline at end of file +*) + diff --git a/helm/matita/tests/first.ma b/helm/matita/tests/first.ma index d75f372ce..69b4adf26 100644 --- a/helm/matita/tests/first.ma +++ b/helm/matita/tests/first.ma @@ -10,7 +10,6 @@ inductive eq (A:Set): A \to A \to Prop \def inductive list (A:Set) : Set \def | nil : list A | cons : A \to list A \to list A. -alias symbol "cast" (instance 0) = "type cast". let rec list_len (A:Set) (l:list A) on l \def [\lambda x.nat]