From 560db5569f54fba5bded568699a33947f88df3ba Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 13 Oct 2010 11:04:46 +0000 Subject: [PATCH] Propagation of changes to grafiteAst. --- .../components/binaries/transcript/engine.ml | 26 +- .../binaries/transcript/gallina8Parser.mly | 16 +- .../components/binaries/transcript/grafite.ml | 6 +- .../binaries/transcript/grafiteParser.mly | 2 +- .../components/binaries/transcript/types.ml | 4 +- matita/components/grafite/grafiteAst.ml | 152 +--------- matita/components/grafite/grafiteAstPp.ml | 282 +----------------- matita/components/grafite/grafiteAstPp.mli | 50 +--- .../grafite_engine/grafiteEngine.ml | 22 +- .../grafite_engine/grafiteEngine.mli | 4 +- .../grafite_parser/grafiteDisambiguate.ml | 5 +- .../grafite_parser/grafiteDisambiguate.mli | 3 +- .../grafite_parser/grafiteParser.ml | 78 +++-- .../grafite_parser/grafiteParser.mli | 6 +- .../components/grafite_parser/test_parser.ml | 7 +- matita/matita/matitaEngine.mli | 9 +- matita/matita/matitaScript.ml | 4 +- matita/matita/matitacLib.ml | 11 +- 18 files changed, 111 insertions(+), 576 deletions(-) diff --git a/matita/components/binaries/transcript/engine.ml b/matita/components/binaries/transcript/engine.ml index da07dd235..39d4d8ddd 100644 --- a/matita/components/binaries/transcript/engine.ml +++ b/matita/components/binaries/transcript/engine.ml @@ -198,22 +198,6 @@ let make_script_name st script name = let ext = if script.is_ma then ".ma" else ".mma" in Filename.concat st.output_path (name ^ ext) -let get_iparams st name = - let debug debug = GA.IPDebug debug in - let map = function - | "comments" -> GA.IPComments - | "nodefaults" -> GA.IPNoDefaults - | "coercions" -> GA.IPCoercions - | "cr" -> GA.IPCR - | s -> - try Scanf.sscanf s "debug-%u" debug with - | Scanf.Scan_failure _ - | Failure _ - | End_of_file -> - failwith ("unknown inline parameter: " ^ s) - in - List.map map (X.list_assoc_all name st.iparams) - let commit st name = let i = get_index st name in let script = st.scripts.(i) in @@ -241,20 +225,14 @@ let produce st = let in_base_uri = Filename.concat st.input_base_uri name in let out_base_uri = Filename.concat st.output_base_uri name in let filter path = function - | T.Inline (b, k, obj, p, f, params) -> + | T.Inline (b, k, obj, p, f) -> let obj, p = if b then Filename.concat (make_path path) obj, make_prefix path else obj, p in let ext = G.string_of_inline_kind k in let s = Filename.concat in_base_uri (obj ^ ext) in - let params = - params @ - get_iparams st "*" @ - get_iparams st ("*" ^ ext) @ - get_iparams st (Filename.concat name obj) - in - path, Some (T.Inline (b, k, s, p, f, params)) + path, Some (T.Inline (b, k, s, p, f)) | T.Include (moo, s) -> begin try path, Some (T.Include (moo, List.assoc s st.requires)) diff --git a/matita/components/binaries/transcript/gallina8Parser.mly b/matita/components/binaries/transcript/gallina8Parser.mly index e72dbbf30..baacd3f40 100644 --- a/matita/components/binaries/transcript/gallina8Parser.mly +++ b/matita/components/binaries/transcript/gallina8Parser.mly @@ -37,7 +37,7 @@ let mk_vars local idents = let kind = if local then T.Var else T.Con in - let map ident = T.Inline (local, kind, trim ident, "", None, []) in + let map ident = T.Inline (local, kind, trim ident, "", None) in List.map map idents let strip2 s = @@ -65,7 +65,7 @@ | _ -> assert false let mk_morphism ext = - let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem, []) in + let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem) in List.rev_map generate ["2"; "1"] %} @@ -297,25 +297,25 @@ macro_step: | th ident opt_lskips def xskips FS { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])] + [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] } | th ident lskips fs just FS { out "TH" $2; - $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])] + $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] } | gen ident def xskips FS { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])] + [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] } | mor ident cn ident fs just FS { out "MOR" $4; $6 @ mk_morphism (trim $4) } | xlet ident opt_lskips def xskips FS { out "TH" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1, [])] + [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] } | xlet ident lskips fs just FS { out "TH" $2; - $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1, [])] + $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] } | var idents cn xskips FS { out "VAR" (cat $2); mk_vars true $2 } @@ -323,7 +323,7 @@ { out "AX" (cat $2); mk_vars false $2 } | ind ident skips FS { out "IND" $2; - T.Inline (false, T.Ind, trim $2, "", None, []) :: snd $3 + T.Inline (false, T.Ind, trim $2, "", None) :: snd $3 } | sec ident FS { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] } diff --git a/matita/components/binaries/transcript/grafite.ml b/matita/components/binaries/transcript/grafite.ml index 176c7f55e..8d4e71174 100644 --- a/matita/components/binaries/transcript/grafite.ml +++ b/matita/components/binaries/transcript/grafite.ml @@ -65,14 +65,14 @@ let out_command och cmd = let term_pp = NP.pp_term in let lazy_term_pp = NP.pp_term in let obj_pp = NP.pp_obj NP.pp_term in - let s = GP.pp_statement ~map_unicode_to_tex:false ~term_pp ~lazy_term_pp ~obj_pp cmd in + let s = GP.pp_statement cmd ~map_unicode_to_tex:false in Printf.fprintf och "%s\n\n" s let command_of_obj obj = G.Executable (floc, G.Command (floc, obj)) let require moo value = - command_of_obj (G.Include (floc, moo, `OldAndNew, value ^ ".ma")) + command_of_obj (G.Include (floc, value ^ ".ma")) let out_alias och name uri = Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri @@ -94,7 +94,7 @@ let commit kind och items = if !O.comments then out_unexported och "COERCION" (snd specs) | T.Notation specs -> if !O.comments then out_unexported och "NOTATION" (snd specs) (**) - | T.Inline (_, T.Var, src, _, _, _) -> + | T.Inline (_, T.Var, src, _, _) -> if !O.comments then out_unexported och "UNEXPORTED" src | T.Section specs -> if !O.comments then out_unexported och "UNEXPORTED" (trd specs) diff --git a/matita/components/binaries/transcript/grafiteParser.mly b/matita/components/binaries/transcript/grafiteParser.mly index 82295c69b..2f4d1e264 100644 --- a/matita/components/binaries/transcript/grafiteParser.mly +++ b/matita/components/binaries/transcript/grafiteParser.mly @@ -127,7 +127,7 @@ { out "OK" $1; [T.Verbatim $1] } | TH SPC id line drops { out "TH" $3; - let a, b = mk_flavour $1 in [T.Inline (false, a, $3, "", b, [])] + let a, b = mk_flavour $1 in [T.Inline (false, a, $3, "", b)] } | UNX line drops { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] } | PS steps { out "PS" $2; [] } diff --git a/matita/components/binaries/transcript/types.ml b/matita/components/binaries/transcript/types.ml index 1fa7971b7..ba1619641 100644 --- a/matita/components/binaries/transcript/types.ml +++ b/matita/components/binaries/transcript/types.ml @@ -37,7 +37,7 @@ type prefix = string type flavour = Cic.object_flavour option -type params = GrafiteAst.inline_param list +(* type params = GrafiteAst.inline_param list *) type item = Heading of (string * int) | Line of string @@ -47,7 +47,7 @@ type item = Heading of (string * int) | Coercion of (local * string) | Notation of (local * string) | Section of (local * string * string) - | Inline of (local * inline_kind * source * prefix * flavour * params) + | Inline of (local * inline_kind * source * prefix * flavour) | Verbatim of string | Discard of string diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 833f98d7c..e32131a06 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -29,25 +29,10 @@ type direction = [ `LeftToRight | `RightToLeft ] type loc = Stdpp.location -type ('term, 'lazy_term, 'ident) pattern = - 'lazy_term option * ('ident * 'term) list * 'term option - type npattern = NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option -type 'lazy_term reduction = - [ `Normalize - | `Simpl - | `Unfold of 'lazy_term option - | `Whd ] - -type 'ident intros_spec = int option * 'ident option list - -type 'term auto_params = 'term list option * (string*string) list - -type 'term just = - [ `Term of 'term - | `Auto of 'term auto_params ] +type auto_params = NotationPt.term list option * (string*string) list type ntactic = | NApply of loc * NotationPt.term @@ -71,7 +56,7 @@ type ntactic = | NLetIn of loc * npattern * NotationPt.term * string | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern | NRewrite of loc * direction * NotationPt.term * npattern - | NAuto of loc * NotationPt.term auto_params + | NAuto of loc * auto_params | NDot of loc | NSemicolon of loc | NBranch of loc @@ -88,117 +73,20 @@ type ntactic = | NRepeat of loc * ntactic | NBlock of loc * ntactic list -type ('term, 'lazy_term, 'reduction, 'ident) tactic = - (* Higher order tactics (i.e. tacticals) *) - | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic - | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic - | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list - (* sequential composition *) - | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic * - ('term, 'lazy_term, 'reduction, 'ident) tactic list - | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list - (* try a sequence of loc * tactic until one succeeds, fail otherwise *) - | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic - (* try a tactic and mask failures *) - | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list - | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic - (* Real tactics *) - | Absurd of loc * 'term - | Apply of loc * 'term - | ApplyRule of loc * 'term - | ApplyP of loc * 'term (* apply for procedural reconstruction *) - | ApplyS of loc * 'term * 'term auto_params - | Assumption of loc - | AutoBatch of loc * 'term auto_params - | Cases of loc * 'term * ('term, 'lazy_term, 'ident) pattern * - 'ident intros_spec - | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term - | Clear of loc * 'ident list - | ClearBody of loc * 'ident - | Compose of loc * 'term * 'term option * int * 'ident intros_spec - | Constructor of loc * int - | Contradiction of loc - | Cut of loc * 'ident option * 'term - | Decompose of loc * 'ident option list - | Demodulate of loc * 'term auto_params - | Destruct of loc * 'term list option - | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern * - 'ident intros_spec - | ElimType of loc * 'term * 'term option * 'ident intros_spec - | Exact of loc * 'term - | Exists of loc - | Fail of loc - | Fold of loc * 'reduction * 'lazy_term * ('term, 'lazy_term, 'ident) pattern - | Fourier of loc - | FwdSimpl of loc * string * 'ident option list - | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option - | IdTac of loc - | Intros of loc * 'ident intros_spec - | Inversion of loc * 'term - | LApply of loc * bool * int option * 'term list * 'term * 'ident option - | Left of loc - | LetIn of loc * 'term * 'ident - | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern - | Reflexivity of loc - | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term - | Rewrite of loc * direction * 'term * - ('term, 'lazy_term, 'ident) pattern * 'ident option list - | Right of loc - | Ring of loc - | Split of loc - | Symmetry of loc - | Transitivity of loc * 'term - (* Declarative language *) - | Assume of loc * 'ident * 'term - | Suppose of loc * 'term *'ident * 'term option - | By_just_we_proved of loc * 'term just * - 'term * 'ident option * 'term option - | We_need_to_prove of loc * 'term * 'ident option * 'term option - | Bydone of loc * 'term just - | We_proceed_by_induction_on of loc * 'term * 'term - | We_proceed_by_cases_on of loc * 'term * 'term - | Byinduction of loc * 'term * 'ident - | Thesisbecomes of loc * 'term - | Case of loc * string * (string * 'term) list - | ExistsElim of loc * 'term just * 'ident * 'term * 'ident * 'lazy_term - | AndElim of loc * 'term just * 'ident * 'term * 'ident * 'term - | RewritingStep of - loc * (string option * 'term) option * 'term * - [ `Term of 'term | `Auto of 'term auto_params - | `Proof | `SolveWith of 'term ] * - bool (* last step*) - -type search_kind = [ `Locate | `Hint | `Match | `Elim ] - -type print_kind = [ `Env | `Coer ] - -type inline_param = IPPrefix of string (* undocumented *) - | IPAs of Cic.object_flavour (* preferred flavour *) - | IPCoercions (* show coercions *) - | IPDebug of int (* set debug level *) - | IPProcedural (* procedural rendering *) - | IPNoDefaults (* no default-based tactics *) - | IPLevel of int (* granularity level *) - | IPDepth of int (* undocumented *) - | IPComments (* show statistics *) - | IPCR (* detect convertible rewriting *) - type nmacro = | NCheck of loc * NotationPt.term | Screenshot of loc * string - | NAutoInteractive of loc * NotationPt.term auto_params + | NAutoInteractive of loc * auto_params | NIntroGuess of loc (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 34 +let magic = 35 type command = - | Drop of loc - | Include of loc * bool (* normal? *) * [`New | `OldAndNew] * string + | Include of loc * string | Set of loc * string * string | Print of loc * string - | Qed of loc type ncommand = | UnificationHint of loc * NotationPt.term * int (* term, precedence *) @@ -212,34 +100,16 @@ type ncommand = (string * NotationPt.term) * NotationPt.term | NQed of loc -type punctuation_tactical = - | Dot of loc - | Semicolon of loc - | Branch of loc - | Shift of loc - | Pos of loc * int list - | Wildcard of loc - | Merge of loc - -type non_punctuation_tactical = - | Focus of loc * int list - | Unfocus of loc - | Skip of loc - -type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = +type code = | Command of loc * command | NCommand of loc * ncommand | NMacro of loc * nmacro | NTactic of loc * ntactic list - | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option - * punctuation_tactical - | NonPunctuationTactical of loc * non_punctuation_tactical - * punctuation_tactical -type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment = +type comment = | Note of loc * string - | Code of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code + | Code of loc * code -type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement = - | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code - | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment +type statement = + | Executable of loc * code + | Comment of loc * comment diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index a4df0b24d..43d03b9af 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -31,69 +31,27 @@ let tactical_terminator = "" let tactic_terminator = tactical_terminator let command_terminator = tactical_terminator -let pp_idents idents = - let map = function Some s -> s | None -> "_" in - "(" ^ String.concat " " (List.map map idents) ^ ")" -let pp_hyps idents = String.concat " " idents - -let pp_reduction_kind ~term_pp = function - | `Normalize -> "normalize" - | `Reduce -> "reduce" - | `Simpl -> "simplify" - | `Unfold (Some t) -> "unfold " ^ term_pp t - | `Unfold None -> "unfold" - | `Whd -> "whd" - -let pp_tactic_pattern ~map_unicode_to_tex ~term_pp ~lazy_term_pp (what, hyp, goal) = +let pp_tactic_pattern ~map_unicode_to_tex (what, hyp, goal) = if what = None && hyp = [] && goal = None then "" else let what_text = match what with | None -> "" - | Some t -> Printf.sprintf "in match (%s) " (lazy_term_pp t) in + | Some t -> Printf.sprintf "in match (%s) " (NotationPp.pp_term t) in let hyp_text = String.concat " " - (List.map (fun (name, p) -> Printf.sprintf "%s:(%s)" name (term_pp p)) hyp) in + (List.map (fun (name, p) -> Printf.sprintf "%s:(%s)" name + (NotationPp.pp_term p)) hyp) in let goal_text = match goal with | None -> "" | Some t -> let vdash = if map_unicode_to_tex then "\\vdash" else "⊢" in - Printf.sprintf "%s (%s)" vdash (term_pp t) + Printf.sprintf "%s (%s)" vdash (NotationPp.pp_term t) in Printf.sprintf "%sin %s%s" what_text hyp_text goal_text -let pp_intros_specs s = function - | None, [] -> "" - | Some num, [] -> Printf.sprintf " %s%i" s num - | None, idents -> Printf.sprintf " %s%s" s (pp_idents idents) - | Some num, idents -> Printf.sprintf " %s%i %s" s num (pp_idents idents) - -let pp_terms ~term_pp terms = String.concat ", " (List.map term_pp terms) - -let opt_string_pp = function - | None -> "" - | Some what -> what ^ " " - -let pp_auto_params ~term_pp (univ, params) = - String.concat " " - (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) ^ - match univ with - | None -> "" - | Some l -> (if params <> [] then " " else "") ^ "by " ^ - String.concat " " (List.map term_pp l) -;; - -let pp_just ~term_pp = - function - `Term term -> "exact " ^ term_pp term - | `Auto params -> pp_auto_params ~term_pp params -;; - let rec pp_ntactic ~map_unicode_to_tex = - let term_pp = NotationPp.pp_term in - let lazy_term_pp = fun _ -> assert false in - let pp_tactic_pattern = - pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in + let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in function | NApply (_,t) -> "napply " ^ NotationPp.pp_term t | NSmartApply (_,t) -> "fixme" @@ -148,197 +106,19 @@ let rec pp_ntactic ~map_unicode_to_tex = | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic ~map_unicode_to_tex t ;; -let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp = - let pp_terms = pp_terms ~term_pp in - let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in - let pp_reduction_kind = pp_reduction_kind ~term_pp in - let pp_tactic_pattern = - pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in - let rec pp_tactic = - function - (* Higher order tactics *) - | Do (_, count, tac) -> - Printf.sprintf "do %d %s" count (pp_tactic tac) - | Repeat (_, tac) -> "repeat " ^ pp_tactic tac - | Seq (_, tacs) -> pp_tactics ~sep:"; " tacs - | Then (_, tac, tacs) -> - Printf.sprintf "%s; [%s]" (pp_tactic tac) - (pp_tactics ~sep:" | " tacs) - | First (_, tacs) -> - Printf.sprintf "tries [%s]" (pp_tactics ~sep:" | " tacs) - | Try (_, tac) -> "try " ^ pp_tactic tac - | Solve (_, tac) -> - Printf.sprintf "solve [%s]" (pp_tactics ~sep:" | " tac) - | Progress (_, tac) -> "progress " ^ pp_tactic tac - (* First order tactics *) - | Absurd (_, term) -> "absurd" ^ term_pp term - | Apply (_, term) -> "apply " ^ term_pp term - | ApplyRule (_, term) -> "apply rule " ^ term_pp term - | ApplyP (_, term) -> "applyP " ^ term_pp term - | ApplyS (_, term, params) -> - "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params - | AutoBatch (_,params) -> "autobatch " ^ - pp_auto_params ~term_pp params - | Assumption _ -> "assumption" - | Cases (_, term, pattern, specs) -> - Printf.sprintf "cases %s %s%s" - (term_pp term) - (pp_tactic_pattern pattern) - (pp_intros_specs "names " specs) - | Change (_, where, with_what) -> - Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) - | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids) - | ClearBody (_,id) -> Printf.sprintf "clearbody %s" (pp_hyps [id]) - | Constructor (_,n) -> "constructor " ^ string_of_int n - | Compose (_,t1, t2, times, intro_specs) -> - Printf.sprintf "compose %s%s %s%s" - (if times > 0 then string_of_int times ^ " " else "") - (term_pp t1) (match t2 with None -> "" | Some t2 -> "with "^term_pp t2) - (pp_intros_specs " as " intro_specs) - | Contradiction _ -> "contradiction" - | Cut (_, ident, term) -> - "cut " ^ term_pp term ^ - (match ident with None -> "" | Some id -> " as " ^ id) - | Decompose (_, names) -> - Printf.sprintf "decompose%s" - (pp_intros_specs "names " (None, names)) - | Demodulate (_, params) -> "demodulate " ^ pp_auto_params ~term_pp params - | Destruct (_, None) -> "destruct" - | Destruct (_, Some terms) -> "destruct " ^ pp_terms terms - | Elim (_, what, using, pattern, specs) -> - Printf.sprintf "elim %s%s %s%s" - (term_pp what) - (match using with None -> "" | Some term -> " using " ^ term_pp term) - (pp_tactic_pattern pattern) - (pp_intros_specs "names " specs) - | ElimType (_, term, using, specs) -> - Printf.sprintf "elim type %s%s%s" - (term_pp term) - (match using with None -> "" | Some term -> " using " ^ term_pp term) - (pp_intros_specs "names " specs) - | Exact (_, term) -> "exact " ^ term_pp term - | Exists _ -> "exists" - | Fold (_, kind, term, pattern) -> - Printf.sprintf "fold %s %s %s" (pp_reduction_kind kind) - (lazy_term_pp term) (pp_tactic_pattern pattern) - | FwdSimpl (_, hyp, names) -> - Printf.sprintf "fwd %s%s" hyp (pp_intros_specs "names " (None, names)) - | Generalize (_, pattern, ident) -> - Printf.sprintf "generalize %s%s" (pp_tactic_pattern pattern) - (match ident with None -> "" | Some id -> " as " ^ id) - | Fail _ -> "fail" - | Fourier _ -> "fourier" - | IdTac _ -> "id" - | Intros (_, specs) -> Printf.sprintf "intros%s" (pp_intros_specs "" specs) - | Inversion (_, term) -> "inversion " ^ term_pp term - | LApply (_, linear, level_opt, terms, term, ident_opt) -> - Printf.sprintf "lapply %s%s%s%s%s" - (if linear then " linear " else "") - (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") - (term_pp term) - (match terms with [] -> "" | _ -> " to " ^ pp_terms terms) - (match ident_opt with None -> "" | Some ident -> " as " ^ ident) - | Left _ -> "left" - | LetIn (_, term, ident) -> - Printf.sprintf "letin %s \\def %s" ident (term_pp term) - | Reduce (_, kind, pat) -> - Printf.sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat) - | Reflexivity _ -> "reflexivity" - | Replace (_, pattern, t) -> - Printf.sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t) - | Rewrite (_, pos, t, pattern, names) -> - Printf.sprintf "rewrite %s %s %s%s" - (if pos = `LeftToRight then ">" else "<") - (term_pp t) - (pp_tactic_pattern pattern) - (if names = [] then "" else " as " ^ pp_idents names) - | Right _ -> "right" - | Ring _ -> "ring" - | Split _ -> "split" - | Symmetry _ -> "symmetry" - | Transitivity (_, term) -> "transitivity " ^ term_pp term - (* Tattiche Aggiunte *) - | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term - | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1) - | Bydone (_, just) -> pp_just ~term_pp just ^ "done" - | By_just_we_proved (_, just, term1, ident, term2) -> pp_just ~term_pp just ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ - (match term2 with None -> " " | Some term2 -> term_pp term2) - | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1) - | We_proceed_by_cases_on (_, term, term1) -> "we proceed by cases on" ^ term_pp term ^ "to prove" ^ term_pp term1 - | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1 - | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")" - | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term - | ExistsElim (_, just, ident, term, ident1, term1) -> pp_just ~term_pp just ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ lazy_term_pp term1 ^ "(" ^ ident1 ^ ")" - | AndElim (_, just, ident1, term1, ident2, term2) -> pp_just ~term_pp just ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" - | RewritingStep (_, term, term1, term2, cont) -> - (match term with - | None -> " " - | Some (None,term) -> "conclude " ^ term_pp term - | Some (Some name,term) -> - "obtain (" ^ name ^ ") " ^ term_pp term) - ^ "=" ^ - term_pp term1 ^ - (match term2 with - | `Auto params -> pp_auto_params ~term_pp params - | `Term term2 -> " exact " ^ term_pp term2 - | `Proof -> " proof" - | `SolveWith term -> " using " ^ term_pp term) - ^ (if cont then " done" else "") - | Case (_, id, args) -> - "case" ^ id ^ - String.concat " " - (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^ ")") - args) - in pp_tactic - -and pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~sep tacs = - String.concat sep - (List.map (pp_tactic ~map_unicode_to_tex ~lazy_term_pp ~term_pp) tacs) - - let pp_search_kind = function - | `Locate -> "locate" - | `Hint -> "hint" - | `Match -> "match" - | `Elim -> "elim" - | `Instance -> "instance" - -let pp_arg ~term_pp arg = - let s = term_pp arg in - if s = "" || (s.[0] = '(' && s.[String.length s - 1] = ')') then - (* _nice_ heuristic *) - s - else - "(" ^ s ^ ")" - let pp_nmacro = function | NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term term) | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name ;; -let pp_associativity = function - | Gramext.LeftA -> "left associative" - | Gramext.RightA -> "right associative" - | Gramext.NonA -> "non associative" - -let pp_precedence i = Printf.sprintf "with precedence %d" i - -let pp_default what uris = - Printf.sprintf "default \"%s\" %s" what - (String.concat " " (List.map UriManager.string_of_uri uris)) - -let pp_coercion ~term_pp t do_composites arity saturations= - Printf.sprintf "coercion %s %d %d %s" - (term_pp t) arity saturations - (if do_composites then "" else "nocomposites") - -let pp_ncommand ~obj_pp = function +let pp_ncommand = function | UnificationHint (_,t, n) -> "unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term t | NDiscriminator (_,_) | NInverter (_,_,_,_,_) | NUnivConstraint (_) -> "not supported" | NCoercion (_) -> "not supported" - | NObj (_,obj) -> obj_pp obj + | NObj (_,obj) -> NotationPp.pp_obj NotationPp.pp_term obj | NQed (_) -> "nqed" | NCopy (_,name,uri,map) -> "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ @@ -349,56 +129,26 @@ let pp_ncommand ~obj_pp = function ;; let pp_command = function - | Drop _ -> "drop" - | Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\"" - | Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\"" - | Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ path + | Include (_,path) -> "include \"" ^ path ^ "\"" | Print (_,s) -> "print " ^ s | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value -let pp_punctuation_tactical = - function - | Dot _ -> "." - | Semicolon _ -> ";" - | Branch _ -> "[" - | Shift _ -> "|" - | Pos (_, i) -> Printf.sprintf "%s:" (String.concat "," (List.map string_of_int i)) - | Wildcard _ -> "*:" - | Merge _ -> "]" - -let pp_non_punctuation_tactical = - function - | Focus (_, goals) -> - Printf.sprintf "focus %s" (String.concat " " (List.map string_of_int goals)) - | Unfocus _ -> "unfocus" - | Skip _ -> "skip" - -let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = +let pp_executable ~map_unicode_to_tex = function | NMacro (_, macro) -> pp_nmacro macro ^ "." - | Tactic (_, Some tac, punct) -> - pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac - ^ pp_punctuation_tactical punct - | Tactic (_, None, punct) -> - pp_punctuation_tactical punct | NTactic (_,tacl) -> String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl) - | NonPunctuationTactical (_, tac, punct) -> - pp_non_punctuation_tactical tac - ^ pp_punctuation_tactical punct | Command (_, cmd) -> pp_command cmd ^ "." - | NCommand (_, cmd) -> - let obj_pp = Obj.magic obj_pp in - pp_ncommand ~obj_pp cmd ^ "." + | NCommand (_, cmd) -> pp_ncommand cmd ^ "." -let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = +let pp_comment ~map_unicode_to_tex = function | Note (_,"") -> Printf.sprintf "\n" | Note (_,str) -> Printf.sprintf "\n(* %s *)" str | Code (_,code) -> - Printf.sprintf "\n(** %s. **)" (pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp code) + Printf.sprintf "\n(** %s. **)" (pp_executable ~map_unicode_to_tex code) -let pp_statement ~term_pp ~lazy_term_pp ~obj_pp = +let pp_statement = function - | Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex - | Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c + | Executable (_, ex) -> pp_executable ex + | Comment (_, c) -> pp_comment c diff --git a/matita/components/grafite/grafiteAstPp.mli b/matita/components/grafite/grafiteAstPp.mli index 6594d2137..11c1782fa 100644 --- a/matita/components/grafite/grafiteAstPp.mli +++ b/matita/components/grafite/grafiteAstPp.mli @@ -23,53 +23,9 @@ * http://helm.cs.unibo.it/ *) -val pp_tactic: - map_unicode_to_tex:bool -> - term_pp:('term -> string) -> - lazy_term_pp:('lazy_term -> string) -> - ('term, 'lazy_term, 'term GrafiteAst.reduction, string) - GrafiteAst.tactic -> - string - -val pp_tactic_pattern: - map_unicode_to_tex:bool -> - term_pp:('term -> string) -> - lazy_term_pp:('lazy_term -> string) -> - ('term, 'lazy_term, string) GrafiteAst.pattern -> - string - -val pp_reduction_kind: - term_pp:('a -> string) -> - 'a GrafiteAst.reduction -> - string - val pp_command: GrafiteAst.command -> string -val pp_comment: - map_unicode_to_tex:bool -> - term_pp:('term -> string) -> - lazy_term_pp:('lazy_term -> string) -> - obj_pp:('obj -> string) -> - ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string) - GrafiteAst.comment -> - string - -val pp_executable: - map_unicode_to_tex:bool -> - term_pp:('term -> string) -> - lazy_term_pp:('lazy_term -> string) -> - obj_pp:('obj -> string) -> - ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string) - GrafiteAst.code -> - string - -val pp_statement: - term_pp:('term -> string) -> - lazy_term_pp:('lazy_term -> string) -> - obj_pp:('obj -> string) -> - ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string) - GrafiteAst.statement -> - map_unicode_to_tex:bool -> - string +val pp_comment: map_unicode_to_tex:bool -> GrafiteAst.comment -> string -val pp_punctuation_tactical: GrafiteAst.punctuation_tactical -> string +val pp_executable: map_unicode_to_tex:bool -> GrafiteAst.code -> string +val pp_statement: GrafiteAst.statement -> map_unicode_to_tex:bool -> string diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index b4a20c202..78564d421 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -53,8 +53,8 @@ type eval_ast = ?do_heavy_checks:bool -> GrafiteTypes.status -> - (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) - disambiguator_input -> +(* (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) *) + GrafiteAst.statement disambiguator_input -> GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } @@ -73,8 +73,7 @@ type 'a eval_comment = disambiguate_command: (GrafiteTypes.status -> GrafiteAst.command disambiguator_input -> GrafiteTypes.status * GrafiteAst.command) -> - options -> GrafiteTypes.status -> - (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input -> + options -> GrafiteTypes.status -> GrafiteAst.comment disambiguator_input -> GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } @@ -87,8 +86,7 @@ type 'a eval_executable = GrafiteTypes.status * GrafiteAst.command) -> options -> - GrafiteTypes.status -> - (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input -> + GrafiteTypes.status -> GrafiteAst.code disambiguator_input -> GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } @@ -272,6 +270,7 @@ 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 @@ -281,7 +280,7 @@ let eval_ng_punct (_text, _prefix_len, punct) = | 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) = @@ -636,9 +635,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status,cmd = disambiguate_command status (text,prefix_len,cmd) in let status,uris = match cmd with - | GrafiteAst.Drop loc -> raise Drop - | GrafiteAst.Include (loc, mode, new_or_old, baseuri) -> - (* Old Include command is not recursive; new one is *) + | 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 = @@ -654,13 +652,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status eval_from_moo.efm_go status moopath else status - in + in *) let status = NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) status in let status = GrafiteTypes.add_moo_content - [GrafiteAst.Include (loc,mode,`New,baseuri)] status + [GrafiteAst.Include (loc,baseuri)] status in status,`New [] | GrafiteAst.Print (_,_) -> status,`New [] diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index 921718611..e8ee448c5 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -37,7 +37,7 @@ val eval_ast : ?do_heavy_checks:bool -> GrafiteTypes.status -> - (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) - disambiguator_input -> + (* (('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 07e502822..5f2ac335d 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -27,10 +27,11 @@ exception BaseUriNotSetYet +(* type tactic = (NotationPt.term, NotationPt.term, NotationPt.term GrafiteAst.reduction, string) - GrafiteAst.tactic + GrafiteAst.tactic *) let singleton msg = function | [x], _ -> x @@ -211,9 +212,9 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = let estatus = LexiconEngine.set_proof_aliases estatus diff in estatus, cic ;; + let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)= match cmd with - | GrafiteAst.Drop _ | GrafiteAst.Include _ | GrafiteAst.Print _ | GrafiteAst.Set _ as cmd -> diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index e08908166..4d66251ce 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -25,10 +25,11 @@ exception BaseUriNotSetYet +(* type tactic = (NotationPt.term, NotationPt.term, NotationPt.term GrafiteAst.reduction, string) - GrafiteAst.tactic + GrafiteAst.tactic *) val disambiguate_command: LexiconEngine.status as 'status -> diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index fbd42cba0..fe4a8042c 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -36,8 +36,7 @@ type 'a localized_option = LSome of 'a | LNone of G.loc -type ast_statement = - (N.term, N.term, N.term G.reduction, N.term N.obj, string) G.statement +type ast_statement = G.statement type 'status statement = ?never_include:bool -> @@ -101,6 +100,7 @@ let nmk_rec_corec ind_kind defs loc = let loc,t = mk_rec_corec ind_kind defs loc in G.NObj (loc,t) +(* let npunct_of_punct = function | G.Branch loc -> G.NBranch loc | G.Shift loc -> G.NShift loc @@ -109,21 +109,14 @@ let npunct_of_punct = function | 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 | G.Focus (loc,l) -> G.NFocus (loc,l) -;; -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 cons_ntac t p = match t with | G.NTactic(loc,[t]) -> G.NTactic(loc,[t;p]) @@ -322,6 +315,7 @@ EXTEND | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)]) ] ]; +(* tactic: [ [ IDENT "absurd"; t = tactic_term -> G.Absurd (loc, t) @@ -444,7 +438,7 @@ EXTEND | IDENT "symmetry" -> G.Symmetry loc | IDENT "transitivity"; t = tactic_term -> - G.Transitivity (loc, t) + G.Transitivity (loc, t) (* Produzioni Aggiunte *) | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> G.Assume (loc, id, t) @@ -512,9 +506,9 @@ EXTEND | IDENT "proof" -> `Proof | params = auto_params -> `Auto params]; cont = rewriting_step_continuation -> - G.RewritingStep(loc, None, t1, t2, cont) - ] -]; + G.RewritingStep(loc, None, t1, t2, cont) + ] +]; *) auto_fixed_param: [ [ IDENT "demod" | IDENT "fast_paramod" @@ -549,6 +543,7 @@ EXTEND ] ]; +(* inline_params:[ [ params = LIST0 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix @@ -563,7 +558,7 @@ EXTEND | 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] ; @@ -581,6 +576,7 @@ EXTEND | -> false ] ]; +(* atomic_tactical: [ "sequence" LEFTA [ t1 = SELF; SYMBOL ";"; t2 = SELF -> @@ -614,6 +610,7 @@ EXTEND | tac = tactic -> tac ] ]; +*) npunctuation_tactical: [ [ SYMBOL "[" -> G.NBranch loc @@ -626,6 +623,7 @@ EXTEND | SYMBOL "." -> G.NDot loc ] ]; +(* punctuation_tactical: [ [ SYMBOL "[" -> G.Branch loc @@ -644,6 +642,14 @@ EXTEND | IDENT "skip" -> G.Skip loc ] ]; +*) + nnon_punctuation_tactical: + [ "simple" NONA + [ IDENT "focus"; goals = LIST1 int -> G.NFocus (loc, goals) + | IDENT "unfocus" -> G.NUnfocus loc + | IDENT "skip" -> G.NSkip loc + ] + ]; ntheorem_flavour: [ [ [ IDENT "ndefinition" ] -> `Definition | [ IDENT "nfact" ] -> `Fact @@ -873,12 +879,6 @@ EXTEND List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m) ]]; - grafite_command: [ [ - IDENT "set"; n = QSTRING; v = QSTRING -> - G.Set (loc, n, v) - | IDENT "drop" -> G.Drop loc - | IDENT "print"; s = IDENT -> G.Print (loc,s) - ]]; lexicon_command: [ [ IDENT "alias" ; spec = alias_spec -> L.Alias (loc, spec) @@ -889,28 +889,24 @@ EXTEND L.Interpretation (loc, id, (symbol, args), l3) ]]; executable: [ - [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd) - | 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) + [ 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 = punctuation_tactical -> - cons_ntac tac (npunct_of_punct punct) + 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]) - | tac = non_punctuation_tactical; punct = punctuation_tactical -> - G.NonPunctuationTactical (loc, tac, punct) - | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; - SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical -> - G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct]) - | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; - punct = punctuation_tactical -> - G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct]) + | SYMBOL "#" ; SYMBOL "#" ; tac = nnon_punctuation_tactical; + SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical -> + G.NTactic (loc, [tac; punct]) + | SYMBOL "#" ; SYMBOL "#" ; tac = nnon_punctuation_tactical; + punct = npunctuation_tactical -> + G.NTactic (loc, [tac; punct]) ] ]; comment: [ @@ -940,13 +936,13 @@ EXTEND begin let stm = G.Executable - (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in + (loc, G.Command (loc, G.Include (iloc,fname))) in !grafite_callback stm; let status = LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in let stm = G.Executable - (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri))) + (loc,G.Command (loc,G.Include (iloc,buri))) in status, LSome stm end diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli index 2dc833194..98942e685 100644 --- a/matita/components/grafite_parser/grafiteParser.mli +++ b/matita/components/grafite_parser/grafiteParser.mli @@ -27,11 +27,7 @@ type 'a localized_option = LSome of 'a | LNone of GrafiteAst.loc -type ast_statement = - (NotationPt.term, NotationPt.term, - NotationPt.term GrafiteAst.reduction, - NotationPt.term NotationPt.obj, string) - GrafiteAst.statement +type ast_statement = GrafiteAst.statement exception NoInclusionPerformed of string (* full path *) diff --git a/matita/components/grafite_parser/test_parser.ml b/matita/components/grafite_parser/test_parser.ml index 500c2420f..5cb8a3a34 100644 --- a/matita/components/grafite_parser/test_parser.ml +++ b/matita/components/grafite_parser/test_parser.ml @@ -94,13 +94,14 @@ let process_stream istream = | statement -> prerr_endline ("Unsupported statement: " ^ - GrafiteAstPp.pp_statement + GrafiteAstPp.pp_statement statement ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") + "matita.paste_unicode_as_tex")) +(* ~term_pp:NotationPp.pp_term ~lazy_term_pp:(fun _ -> "_lazy_term_here_") ~obj_pp:(fun _ -> "_obj_here_") - statement) + statement)*) with | End_of_file -> raise End_of_file | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) -> diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli index 070a7a48f..945e7f348 100644 --- a/matita/matita/matitaEngine.mli +++ b/matita/matita/matitaEngine.mli @@ -27,9 +27,7 @@ val eval_ast : ?do_heavy_checks:bool -> GrafiteTypes.status -> string * int * - ((NotationPt.term, NotationPt.term, - NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string) - GrafiteAst.statement) -> + GrafiteAst.statement -> (GrafiteTypes.status * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list @@ -49,9 +47,6 @@ val eval_from_stream : ?watch_statuses:(GrafiteTypes.status -> unit) -> GrafiteTypes.status -> Ulexing.lexbuf -> - (GrafiteTypes.status -> - (NotationPt.term, NotationPt.term, - NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string) - GrafiteAst.statement -> unit) -> + (GrafiteTypes.status -> GrafiteAst.statement -> unit) -> (GrafiteTypes.status * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 9fc79ca92..65fc0fcec 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -124,9 +124,7 @@ let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statem else raise (Failure ("Compiling: " ^ tgt)) ;; -let pp_eager_statement_ast = - GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term - ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) +let pp_eager_statement_ast = GrafiteAstPp.pp_statement let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = let parsed_text_length = String.length parsed_text in diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index eb4ed6991..11806a8a3 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -34,11 +34,8 @@ exception AttemptToInsertAnAlias of LexiconEngine.status let slash_n_RE = Pcre.regexp "\\n" ;; let pp_ast_statement grafite_status stm = - let stm = GrafiteAstPp.pp_statement + let stm = GrafiteAstPp.pp_statement stm ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - ~term_pp:NotationPp.pp_term - ~lazy_term_pp:NotationPp.pp_term ~obj_pp:(NotationPp.pp_obj - NotationPp.pp_term) stm in let stm = Pcre.replace ~rex:slash_n_RE stm in let stm = @@ -59,18 +56,16 @@ let dump f = let floc = H.dummy_floc in let nl_ast = G.Comment (floc, G.Note (floc, "")) in let pp_statement stm = - GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term + GrafiteAstPp.pp_statement stm ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - ~lazy_term_pp:NotationPp.pp_term - ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm in let pp_lexicon = LexiconAstPp.pp_command in let och = open_out f in let nl () = output_string och (pp_statement nl_ast) in MatitaMisc.out_preamble och; let grafite_parser_cb = function - | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> () + | G.Executable (loc, G.Command (_, G.Include (_,_))) -> () | stm -> output_string och (pp_statement stm); nl (); nl () in -- 2.39.2