From d3548c16f481b14ce94e64c790bc767c59590050 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 5 May 2009 17:23:49 +0000 Subject: [PATCH] - hExtlib: new function "list_assoc_all" - procedural: new flag "nodefaults" to turn off "default" based tactics. The `Variant flavour is now activated - grafiteAst: now inline accepts a list of flags that can be easily extended current flags are: procedural, nodefaults, depth=n, prefix="string" (untested), theorem, definition, etc. - transcript: support for explicitly provided inline flags --- .../acic_procedural/acic2Procedural.ml | 12 +- .../acic_procedural/acic2Procedural.mli | 4 +- .../components/acic_procedural/procedural2.ml | 66 +++++----- .../acic_procedural/procedural2.mli | 8 +- .../components/binaries/transcript/.depend | 5 - .../binaries/transcript/.depend.opt | 5 - .../components/binaries/transcript/engine.ml | 24 +++- .../binaries/transcript/gallina8Parser.mly | 16 +-- .../components/binaries/transcript/grafite.ml | 24 ++-- .../binaries/transcript/grafiteParser.mly | 2 +- .../components/binaries/transcript/types.ml | 4 +- helm/software/components/extlib/hExtlib.ml | 8 +- helm/software/components/extlib/hExtlib.mli | 4 + .../software/components/grafite/grafiteAst.ml | 11 +- .../components/grafite/grafiteAstPp.ml | 40 +++--- .../grafite_parser/grafiteParser.ml | 24 ++-- helm/software/matita/applyTransformation.ml | 115 +++++++++--------- helm/software/matita/applyTransformation.mli | 12 +- .../procedural/library/library.conf.xml | 2 + helm/software/matita/matita.ml | 2 +- helm/software/matita/matitaScript.ml | 8 +- helm/software/matita/matitacLib.ml | 7 +- 22 files changed, 218 insertions(+), 185 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 0eb8d8efb..c8168aa47 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -34,11 +34,11 @@ let tex_formatter = ref None (* interface functions ******************************************************) let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types - ?info ?depth ?flavour prefix anobj = - let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth [] in + ?info params anobj = + let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types params [] in L.time_stamp "P : LEVEL 2 "; HLog.debug "Procedural: level 2 transformation"; - let steps = P2.proc_obj st ?flavour ?info anobj in + let steps = P2.proc_obj st ?info anobj in let _ = match !tex_formatter with | None -> () | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps @@ -48,9 +48,9 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types let r = List.rev (T.render_steps [] steps) in L.time_stamp "P : DONE "; r -let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth - prefix context annterm = - let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context in +let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params + context annterm = + let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context in HLog.debug "Procedural: level 2 transformation"; let steps = P2.proc_proof st annterm in let _ = match !tex_formatter with diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli index 082bb071b..cca20ba5f 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -26,7 +26,7 @@ val procedural_of_acic_object: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> ?info:string -> - ?depth:int -> ?flavour:Cic.object_flavour -> string -> Cic.annobj -> + GrafiteAst.inline_param list -> Cic.annobj -> (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) GrafiteAst.statement list @@ -34,7 +34,7 @@ val procedural_of_acic_object: val procedural_of_acic_term: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> - ?depth:int -> string -> Cic.context -> Cic.annterm -> + GrafiteAst.inline_param list -> Cic.context -> Cic.annterm -> (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) GrafiteAst.statement list diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index f8007d3fc..958fc4abb 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -30,7 +30,6 @@ module TC = CicTypeChecker module Un = CicUniv module UM = UriManager module Obj = LibraryObjects -module HObj = HelmLibraryObjects module A = Cic2acic module Ut = CicUtil module E = CicEnvironment @@ -40,6 +39,7 @@ module HEL = HExtlib module DTI = DoubleTypeInference module NU = CicNotationUtil module L = Librarian +module G = GrafiteAst module Cl = ProceduralClassify module T = ProceduralTypes @@ -47,12 +47,14 @@ module Cn = ProceduralConversion module H = ProceduralHelpers type status = { - sorts : (C.id, A.sort_kind) Hashtbl.t; - types : (C.id, A.anntypes) Hashtbl.t; + sorts : (C.id, A.sort_kind) Hashtbl.t; + types : (C.id, A.anntypes) Hashtbl.t; + params : G.inline_param list; max_depth: int option; - depth: int; - context: C.context; - case: int list + depth : int; + defaults : bool; + context : C.context; + case : int list } let debug = ref false @@ -109,24 +111,22 @@ try | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: " with Invalid_argument _ -> failwith "A2P.test_depth" -let is_rewrite_right = function - | C.AConst (_, uri, []) -> - UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri +let is_rewrite_right st = function + | C.AConst (_, uri, []) -> st.defaults && Obj.is_eq_ind_r_URI uri | _ -> false -let is_rewrite_left = function - | C.AConst (_, uri, []) -> - UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri +let is_rewrite_left st = function + | C.AConst (_, uri, []) -> st.defaults && Obj.is_eq_ind_URI uri | _ -> false -let is_fwd_rewrite_right hd tl = - if is_rewrite_right hd then match List.nth tl 3 with +let is_fwd_rewrite_right st hd tl = + if is_rewrite_right st hd then match List.nth tl 3 with | C.ARel _ -> true | _ -> false else false -let is_fwd_rewrite_left hd tl = - if is_rewrite_left hd then match List.nth tl 3 with +let is_fwd_rewrite_left st hd tl = + if is_rewrite_left st hd then match List.nth tl 3 with | C.ARel _ -> true | _ -> false else false @@ -291,11 +291,11 @@ and proc_letin st what name v w t = let st, hyp, rqv = match get_inner_types st v with | Some (ity, _) -> let st, rqv = match v with - | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl -> + | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl -> mk_fwd_rewrite st dtext intro tl true v t ity - | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl -> + | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left st hd tl -> mk_fwd_rewrite st dtext intro tl false v t ity - | v -> + | v -> assert (Ut.is_sober st.context (H.cic ity)); let ity = H.acic_bc st.context ity in let qs = [proc_proof (next st) v; [T.Id ""]] in @@ -365,9 +365,9 @@ and proc_appl st what hd tl = let qs = proc_bkd_proofs (next st) synth [] classes tl in let b, hd = mk_exp_args hd tl classes synth in script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")] - else if is_rewrite_right hd then + else if is_rewrite_right st hd then script2 @ mk_rewrite st dtext where qs tl2 false what - else if is_rewrite_left hd then + else if is_rewrite_left st hd then script2 @ mk_rewrite st dtext where qs tl2 true what else let predicate = List.nth tl2 (parsno - i) in @@ -462,22 +462,26 @@ with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s) let th_flavours = [`Theorem; `Lemma; `Remark; `Fact] -let def_flavours = [`Definition] +let def_flavours = [`Definition; `Variant] -let get_flavour ?flavour st v attrs = +let get_flavour st v attrs = let rec aux = function | [] -> if is_proof st v then List.hd th_flavours else List.hd def_flavours | `Flavour fl :: _ -> fl | _ :: tl -> aux tl in - match flavour with + let flavour_map x y = match x, y with + | None, G.IPAs flavour -> Some flavour + | _ -> x + in + match List.fold_left flavour_map None st.params with | Some fl -> fl | None -> aux attrs -let proc_obj ?flavour ?(info="") st = function +let proc_obj ?(info="") st = function | C.AConstant (_, _, s, Some v, t, [], attrs) -> - begin match get_flavour ?flavour st v attrs with + begin match get_flavour st v attrs with | flavour when List.mem flavour th_flavours -> let ast = proc_proof st v in let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in @@ -497,12 +501,18 @@ let proc_obj ?flavour ?(info="") st = function | _ -> failwith "not a theorem, definition, axiom or inductive type" -let init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context = +let init ~ids_to_inner_sorts ~ids_to_inner_types params context = + let depth_map x y = match x, y with + | None, G.IPDepth depth -> Some depth + | _ -> x + in { sorts = ids_to_inner_sorts; types = ids_to_inner_types; - max_depth = depth; + params = params; + max_depth = List.fold_left depth_map None params; depth = 0; + defaults = not (List.mem G.IPNoDefaults params); context = context; case = [] } diff --git a/helm/software/components/acic_procedural/procedural2.mli b/helm/software/components/acic_procedural/procedural2.mli index 708e698df..71cbe4253 100644 --- a/helm/software/components/acic_procedural/procedural2.mli +++ b/helm/software/components/acic_procedural/procedural2.mli @@ -28,14 +28,12 @@ type status val init: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> - ?depth:int -> Cic.context -> status + GrafiteAst.inline_param list-> Cic.context -> status val proc_proof: - status -> Cic.annterm -> - ProceduralTypes.step list + status -> Cic.annterm -> ProceduralTypes.step list val proc_obj: - ?flavour:Cic.object_flavour -> ?info:string -> status -> Cic.annobj -> - ProceduralTypes.step list + ?info:string -> status -> Cic.annobj -> ProceduralTypes.step list val debug: bool ref diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 87d1ed25c..bb6f22a64 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index f17459162..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 916338368..3184aad36 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -25,10 +25,11 @@ module R = Helm_registry module X = HExtlib -module T = Types -module G = Grafite module HG = Http_getter +module GA = GrafiteAst +module T = Types +module G = Grafite module O = Options type script = { @@ -52,6 +53,7 @@ type status = { remove_lines: int; excludes: string list; includes: (string * string) list; + iparams: (string * string) list; coercions: (string * string) list; files: string list; requires: (string * string) list; @@ -109,13 +111,13 @@ let make registry = | "gallina8", _ -> T.Gallina8, ".v", [] | "grafite", "" -> T.Grafite "", ".ma", [] | "grafite", s -> T.Grafite s, ".ma", [s] - | _ -> failwith "unknown input type" + | s, _ -> failwith ("unknown input type: " ^ s) in let get_output_type key = match R.get_string key with | "procedural" -> T.Procedural | "declarative" -> T.Declarative - | _ -> failwith "unknown output type" + | s -> failwith ("unknown output type: " ^ s) in load_registry registry; let input_type, input_ext, excludes = @@ -136,6 +138,7 @@ let make registry = remove_lines = R.get_int "package.heading_lines"; excludes = excludes; includes = get_pairs "package.include"; + iparams = get_pairs "package.inline"; coercions = get_pairs "package.coercion"; files = []; requires = []; @@ -192,6 +195,13 @@ 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 map = function + | "nodefaults" -> GA.IPNoDefaults + | s -> 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 @@ -219,13 +229,15 @@ 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) -> + | T.Inline (b, k, obj, p, f, params) -> let obj, p = if b then Filename.concat (make_path path) obj, make_prefix path else obj, p in let s = obj ^ G.string_of_inline_kind k in - path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p, f)) + let full_s = Filename.concat in_base_uri s in + let params = params @ get_iparams st (Filename.concat name obj) in + path, Some (T.Inline (b, k, full_s, p, f, params)) | T.Include s -> begin try path, Some (T.Include (List.assoc s st.requires)) diff --git a/helm/software/components/binaries/transcript/gallina8Parser.mly b/helm/software/components/binaries/transcript/gallina8Parser.mly index 8bba4fb0b..632bd7e1d 100644 --- a/helm/software/components/binaries/transcript/gallina8Parser.mly +++ b/helm/software/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/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index 8776185b8..8e98b3757 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -81,12 +81,20 @@ let require value = let coercion value = command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0)) -let inline kind uri prefix flavour = - let kind = match kind with - | T.Declarative -> G.Declarative - | T.Procedural -> G.Procedural None +let inline kind uri prefix flavour params = + let params = match prefix with + | "" -> params + | prefix -> G.IPPrefix prefix :: params in - command_of_macro (G.Inline (floc, kind, uri, prefix, flavour)) + let params = match flavour with + | None -> params + | Some flavour -> G.IPAs flavour :: params + in + let params = match kind with + | T.Declarative -> params + | T.Procedural -> G.IPProcedural :: params + in + command_of_macro (G.Inline (floc, uri, params)) let out_alias och name uri = Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri @@ -108,15 +116,15 @@ 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 (* FG: we do not export variables because we cook the other objects * let name = UriManager.name_of_uri (UriManager.uri_of_string src) in * out_alias och name src *) - | T.Inline (_, _, src, pre, fl) -> + | T.Inline (_, _, src, pre, fl, params) -> if !O.getter then check och src; - out_command och (inline kind src pre fl) + out_command och (inline kind src pre fl params) | T.Section specs -> if !O.comments then out_unexported och "UNEXPORTED" (trd specs) | T.Comment comment -> diff --git a/helm/software/components/binaries/transcript/grafiteParser.mly b/helm/software/components/binaries/transcript/grafiteParser.mly index 1e6855f55..03ca0cdf4 100644 --- a/helm/software/components/binaries/transcript/grafiteParser.mly +++ b/helm/software/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)] } diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml index 3b774f832..28641d3d3 100644 --- a/helm/software/components/binaries/transcript/types.ml +++ b/helm/software/components/binaries/transcript/types.ml @@ -37,6 +37,8 @@ type prefix = string type flavour = Cic.object_flavour option +type params = GrafiteAst.inline_param list + type item = Heading of (string * int) | Line of string | Comment of string @@ -45,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) + | Inline of (local * inline_kind * source * prefix * flavour * params) | Verbatim of string | Discard of string diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 3ef795e9f..5f2c7f78c 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -270,7 +270,13 @@ let list_last l = let l = List.rev l in try List.hd l with exn -> raise (Failure "HExtlib.list_last") ;; - + +let rec list_assoc_all a = function + | [] -> [] + | (x, y) :: tl when x = a -> y :: list_assoc_all a tl + | _ :: tl -> list_assoc_all a tl +;; + (** {2 File predicates} *) let is_dir fname = diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli index 0a8921b1b..69843b235 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -119,6 +119,10 @@ val mk_list: 'a -> int -> 'a list (* makes the list [start; ...; stop - 1] *) val list_seq: int -> int -> int list + +(* like List.assoc but returns all bindings *) +val list_assoc_all: 'a -> ('a * 'b) list -> 'b list + (** {2 Debugging & Profiling} *) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b } diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index f6555fa04..4006320be 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -147,8 +147,11 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] -type presentation_style = Declarative - | Procedural of int option +type inline_param = IPPrefix of string + | IPProcedural + | IPDepth of int + | IPAs of Cic.object_flavour + | IPNoDefaults type ('term,'lazy_term) macro = (* Whelp's stuff *) @@ -162,8 +165,8 @@ type ('term,'lazy_term) macro = | Check of loc * 'term | Hint of loc * bool | AutoInteractive of loc * 'term auto_params - | Inline of loc * presentation_style * string * string * Cic.object_flavour option - (* URI or base-uri, name prefix, flavour *) + | Inline of loc * string * inline_param list + (* URI or base-uri, parameters *) (** To be increased each time the command type below changes, used for "safe" * marshalling *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 0fddb2163..ce7fdcfdf 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -267,24 +267,26 @@ let pp_arg ~term_pp arg = let pp_macro ~term_pp ~lazy_term_pp = let term_pp = pp_arg ~term_pp in - let style_pp = function - | Declarative -> "" - | Procedural None -> "procedural " - | Procedural (Some i) -> Printf.sprintf "procedural %u " i - in - let prefix_pp prefix = - if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix - in let flavour_pp = function - | None -> "" - | Some `Definition -> " as definition" - | Some `MutualDefinition -> " as mutual" - | Some `Fact -> " as fact" - | Some `Lemma -> " as lemma" - | Some `Remark -> " as remark" - | Some `Theorem -> " as theorem" - | Some `Variant -> " as variant" - | Some `Axiom -> " as axiom" + | `Definition -> "definition" + | `Fact -> "fact" + | `Lemma -> "lemma" + | `Remark -> "remark" + | `Theorem -> "theorem" + | `Variant -> "variant" + | `Axiom -> "axiom" + | `MutualDefinition -> assert false + in + let pp_inline_params l = + let pp_param = function + | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\"" + | IPAs flavour -> flavour_pp flavour + | IPProcedural -> "procedural" + | IPDepth depth -> "depth = " ^ string_of_int depth + | IPNoDefaults -> "nodefaults" + in + let s = String.concat " " (List.map pp_param l) in + if s = "" then s else " " ^ s in let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in function @@ -301,8 +303,8 @@ let pp_macro ~term_pp ~lazy_term_pp = | Hint (_, true) -> "hint rewrite" | Hint (_, false) -> "hint" | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params - | Inline (_, style, suri, prefix, flavour) -> - Printf.sprintf "inline %s\"%s\"%s%s" (style_pp style) suri (prefix_pp prefix) (flavour_pp flavour) + | Inline (_, suri, params) -> + Printf.sprintf "inline \"%s\"%s" suri (pp_inline_params params) let pp_associativity = function | Gramext.LeftA -> "left associative" diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 5a22a4b62..e2ab011da 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -449,6 +449,16 @@ EXTEND (match tl with Some l -> l | None -> []), params ] +]; + inline_params:[ + [ params = LIST0 + [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix + | IDENT "procedural" -> G.IPProcedural + | flavour = inline_flavour -> G.IPAs flavour + | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth + | IDENT "nodefaults" -> G.IPNoDefaults + ] -> 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) @@ -537,7 +547,7 @@ EXTEND inline_flavour: [ [ attr = theorem_flavour -> attr | [ IDENT "axiom" ] -> `Axiom - | [ IDENT "mutual" ] -> `MutualDefinition + | [ IDENT "variant" ] -> `Variant ] ]; inductive_spec: [ [ @@ -592,16 +602,8 @@ EXTEND G.Check (loc, t) | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term -> G.Eval (loc, kind, t) - | [ IDENT "inline"]; - style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; - suri = QSTRING; prefix = OPT QSTRING; - flavour = OPT [ "as"; attr = inline_flavour -> attr ] -> - let style = match style with - | None -> G.Declarative - | Some depth -> G.Procedural depth - in - let prefix = match prefix with None -> "" | Some prefix -> prefix in - G.Inline (loc,style,suri,prefix, flavour) + | IDENT "inline"; suri = QSTRING; params = inline_params -> + G.Inline (loc, suri, params) | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> if rew = None then G.Hint (loc, false) else G.Hint (loc,true) | IDENT "auto"; params = auto_params -> diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 9f5f5c311..2988af421 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -185,8 +185,7 @@ let enable_notations = function CicNotation.set_active_notations [] let txt_of_cic_object - ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas - n style ?flavour prefix obj + ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n params obj = let get_aobj obj = try @@ -202,55 +201,53 @@ let txt_of_cic_object let msg = "txt_of_cic_object: " ^ Printexc.to_string e in failwith msg in - match style with - | G.Declarative -> - let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in - let cobj = - Acic2content.annobj2content - ids_to_inner_sorts ids_to_inner_types aobj - in - let bobj = - Content2pres.content2pres - ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj - in - remove_closed_substs ( - BoxPp.render_to_string ~map_unicode_to_tex - (function _::x::_ -> x | _ -> assert false) n - (CicNotationPres.mpres_of_box bobj) - ^ "\n\n" ) - | G.Procedural depth -> -(* - PO.debug := true; - PO.critical := false; - Acic2Procedural.tex_formatter := Some Format.std_formatter; - let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in + if List.mem G.IPProcedural params then begin +(* + PO.debug := true; + PO.critical := false; + Acic2Procedural.tex_formatter := Some Format.std_formatter; + let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in *) - let obj, info = PO.optimize_obj obj in + let obj, info = PO.optimize_obj obj in (* - let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in + let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in *) - let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in - let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in - let lazy_term_pp = term_pp in - let obj_pp = CicNotationPp.pp_obj term_pp in - let stm_pp = - GrafiteAstPp.pp_statement - ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp - in - let aux = function - | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm - -> - enable_notations false; - let str = stm_pp stm in enable_notations true; str + let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in + let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in + let lazy_term_pp = term_pp in + let obj_pp = CicNotationPp.pp_obj term_pp in + let stm_pp = + GrafiteAstPp.pp_statement + ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp + in + let aux = function + | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm + -> + enable_notations false; + let str = stm_pp stm in enable_notations true; str (* FG: we disable notation for Inductive to avoid recursive notation *) - | stm -> stm_pp stm - in - let script = - Acic2Procedural.procedural_of_acic_object - ~ids_to_inner_sorts ~ids_to_inner_types ~info - ?depth ?flavour prefix aobj - in - String.concat "" (List.map aux script) ^ "\n\n" + | stm -> stm_pp stm + in + let script = + Acic2Procedural.procedural_of_acic_object + ~ids_to_inner_sorts ~ids_to_inner_types ~info params aobj + in + String.concat "" (List.map aux script) ^ "\n\n" + end else + let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in + let cobj = + Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj + in + let bobj = + Content2pres.content2pres + ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj + in + remove_closed_substs ( + BoxPp.render_to_string ~map_unicode_to_tex + (function _::x::_ -> x | _ -> assert false) n + (CicNotationPres.mpres_of_box bobj) + ^ "\n\n" + ) let cic_prefix = Str.regexp_string "cic:/" let matita_prefix = Str.regexp_string "cic:/matita/" @@ -264,10 +261,10 @@ let replacement (ok, u) (l, s, x, t) = if ok then ok, u else if Str.last_chars u l = s then true, Str.replace_first x t u else ok, u -let discharge_uri style uri = - let template = match style with - | G.Declarative -> "cic:/matita/declarative/" - | G.Procedural _ -> "cic:/matita/procedural/" +let discharge_uri params uri = + let template = + if List.mem G.IPProcedural params then "cic:/matita/procedural/" + else "cic:/matita/declarative/" in let s = UM.string_of_uri uri in if Str.string_match matita_prefix s 0 then uri else @@ -277,7 +274,7 @@ let discharge_uri style uri = let discharge_name s = s ^ "_discharged" -let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri = +let txt_of_inline_uri ~map_unicode_to_tex params suri = (* Ds.debug := true; *) @@ -302,7 +299,7 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri = try (* FG: for now the explicit variables must be discharged *) let do_it obj = - let r = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in + let r = txt_of_cic_object ~map_unicode_to_tex 78 params obj in Librarian.time_stamp "AT: END MAP "; r in let obj, real = @@ -313,10 +310,10 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri = Librarian.time_stamp "AT: DONE "; obj, true end else - Ds.discharge_uri discharge_name (discharge_uri style) uri + Ds.discharge_uri discharge_name (discharge_uri params) uri in if real then do_it obj else - let newuri = discharge_uri style uri in + let newuri = discharge_uri params uri in let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in do_it obj with @@ -330,7 +327,7 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri = in String.concat "" (List.map map sorted_uris) -let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name = +let txt_of_inline_macro ~map_unicode_to_tex params name = let suri = if Librarian.is_uri name then name else let include_paths = @@ -341,12 +338,12 @@ let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name = in baseuri ^ "/" in - txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri + txt_of_inline_uri ~map_unicode_to_tex params suri (****************************************************************************) (* procedural_txt_of_cic_term *) -let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term = +let procedural_txt_of_cic_term ~map_unicode_to_tex n params context term = let term, _info = PO.optimize_term context term in let annterm, ids_to_inner_sorts, ids_to_inner_types = try Cic2acic.acic_term_of_cic_term context term @@ -361,7 +358,7 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term = ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in let script = Acic2Procedural.procedural_of_acic_term - ~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm + ~ids_to_inner_sorts ~ids_to_inner_types params context annterm in String.concat "" (List.map aux script) ;; diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index a65e1e70c..1297be57f 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -69,18 +69,16 @@ val txt_of_cic_sequent_conclusion: map_unicode_to_tex:bool -> output_type:[`Pattern | `Term] -> int -> Cic.metasenv -> Cic.conjecture -> string -(* columns, rendering style, flavour, name prefix, object *) +(* columns, params, object *) val txt_of_cic_object: map_unicode_to_tex:bool -> ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:int -> - int -> GrafiteAst.presentation_style -> ?flavour:Cic.object_flavour -> - string -> Cic.obj -> + int -> GrafiteAst.inline_param list -> Cic.obj -> string -(* presentation_style, flavour, name prefix, uri or baseuri *) +(* params, uri or baseuri *) val txt_of_inline_macro: - map_unicode_to_tex:bool -> GrafiteAst.presentation_style -> - ?flavour:Cic.object_flavour -> string -> string -> + map_unicode_to_tex:bool -> GrafiteAst.inline_param list -> string -> string val txt_of_macro: @@ -91,6 +89,6 @@ val txt_of_macro: (* columns, rendering depth, context, term *) val procedural_txt_of_cic_term: - map_unicode_to_tex:bool -> int -> ?depth:int -> + map_unicode_to_tex:bool -> int -> GrafiteAst.inline_param list -> Cic.context -> Cic.term -> string diff --git a/helm/software/matita/contribs/procedural/library/library.conf.xml b/helm/software/matita/contribs/procedural/library/library.conf.xml index 967ca4cdc..d20adfe2d 100644 --- a/helm/software/matita/contribs/procedural/library/library.conf.xml +++ b/helm/software/matita/contribs/procedural/library/library.conf.xml @@ -11,5 +11,7 @@ procedural 14 + logic/equality/symmetric_eq nodefaults + logic/equality/transitive_eq nodefaults diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index fb7ad27bf..392a35ab7 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -206,7 +206,7 @@ let _ = addDebugItem "Print current proof (natural language) to stderr" (fun _ -> prerr_endline - (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative "" + (ApplyTransformation.txt_of_cic_object 120 [] ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") (match diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 9fb92c274..fadc55105 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -549,7 +549,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status "matita.paste_unicode_as_tex") ~skip_thm_and_qed:true ~skip_initial_lambdas:how_many_lambdas - 80 GrafiteAst.Declarative "" obj + 80 [] obj else if true then (* use cic2grafite *) @@ -560,7 +560,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status Helm_registry.get_bool "matita.paste_unicode_as_tex" in ApplyTransformation.procedural_txt_of_cic_term - ~map_unicode_to_tex 78 cc proof_term + ~map_unicode_to_tex 78 [] cc proof_term in let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in [],text,parsed_text_length @@ -568,12 +568,12 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status ProofEngineTypes.Fail _ as exn -> raise exn (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) - | TA.Inline (_,style,suri,prefix,flavour) -> + | TA.Inline (_, suri, params) -> let str = "\n\n" ^ ApplyTransformation.txt_of_inline_macro ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - style ?flavour prefix suri + params suri in [], str, String.length parsed_text diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 5a14b2703..489e37c86 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -70,10 +70,9 @@ let dump f = let nl () = output_string och (pp_statement nl_ast) in MatitaMisc.out_preamble och; let grafite_parser_cb status = function - | G.Executable (_, G.Macro (_, G.Inline (_, style, uri, prefix, flavour))) -> + | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) -> let str = - ApplyTransformation.txt_of_inline_macro style prefix uri - ?flavour + ApplyTransformation.txt_of_inline_macro params uri ~map_unicode_to_tex: (Helm_registry.get_bool "matita.paste_unicode_as_tex") in @@ -239,7 +238,7 @@ let compile atstart options fname = with MatitaEngine.EnrichedWithStatus (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn -> match f (get_macro_context (Some grafite)) with - | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) -> + | _, GrafiteAst.Inline (_, _suri, _params) -> (* let str = ApplyTransformation.txt_of_inline_macro style prefix suri -- 2.39.2