- 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
(* 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
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
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
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
module Un = CicUniv
module UM = UriManager
module Obj = LibraryObjects
-module HObj = HelmLibraryObjects
module A = Cic2acic
module Ut = CicUtil
module E = CicEnvironment
module DTI = DoubleTypeInference
module NU = CicNotationUtil
module L = Librarian
+module G = GrafiteAst
module Cl = ProceduralClassify
module T = ProceduralTypes
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
| 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
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
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
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
| _ ->
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 = []
}
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
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
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
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 = {
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;
| "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 =
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 = [];
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
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))
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 =
| _ -> 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"]
%}
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 }
{ 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)] }
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
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 ->
{ 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)] }
type flavour = Cic.object_flavour option
+type params = GrafiteAst.inline_param list
+
type item = Heading of (string * int)
| Line of string
| Comment of string
| 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
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 =
(* 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 }
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 *)
| 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 *)
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
| 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"
(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)
inline_flavour: [
[ attr = theorem_flavour -> attr
| [ IDENT "axiom" ] -> `Axiom
- | [ IDENT "mutual" ] -> `MutualDefinition
+ | [ IDENT "variant" ] -> `Variant
]
];
inductive_spec: [ [
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 ->
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
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/"
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
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;
*)
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 =
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
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 =
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
~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)
;;
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:
(* 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
<key name="output_type">procedural</key>
<key name="heading_lines">14</key>
<key name="theory_file"></key>
+ <key name="inline">logic/equality/symmetric_eq nodefaults</key>
+ <key name="inline">logic/equality/transitive_eq nodefaults</key>
</section>
</helm_registry>
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
"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 *)
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
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
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
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
projects / helm.git / commitdiff