From d03e9fa5ea709a937148a67fc115d894e5990063 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 22 May 2016 20:00:11 +0000 Subject: [PATCH] - support fof global alpha-conversion with hyperlinks - Makefile: a bug fixed --- matita/components/binaries/matex/Makefile | 8 +- matita/components/binaries/matex/alpha.ml | 87 ++++++++----- matita/components/binaries/matex/engine.ml | 117 ++++++++++-------- matita/components/binaries/matex/matex.ml | 4 +- matita/components/binaries/matex/options.ml | 28 +++-- matita/components/binaries/matex/options.mli | 8 ++ .../components/binaries/matex/test/matex.sty | 45 ++++--- 7 files changed, 180 insertions(+), 117 deletions(-) diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile index 9212a0662..e177cc077 100644 --- a/matita/components/binaries/matex/Makefile +++ b/matita/components/binaries/matex/Makefile @@ -10,16 +10,16 @@ REGISTRY = $(RT_BASE_DIR)/matita.conf.xml test/basic_1.conf.xml OBJS = Make.objs SRCS = Make.srcs -BASEURI = cic:/matita/lambdadelta/basic_1/ +DEVEL = ../../../matita/contribs/lambdadelta/basic_1/ test: test/$(SRCS) test/$(OBJS): $(REGISTRY) - @echo probe: $(BASEURI) - $(H)$(PROBE) $(REGISTRY) -g $(BASEURI) -os > $@ + @echo probe: $(DEVEL) + $(H)$(PROBE) $(REGISTRY) -g $(DEVEL) -os > $@ test/$(SRCS): test/$(OBJS) $(REGISTRY) ./matex.native @echo MaTeX: processing $< - $(H)./matex.native -O test -l $(SRCS) -p -a $(REGISTRY) `cat $<` + $(H)./matex.native -O test -l $(SRCS) -p -g -a $(REGISTRY) `cat $<` .PHONY: test diff --git a/matita/components/binaries/matex/alpha.ml b/matita/components/binaries/matex/alpha.ml index 59e8c989f..816edd4a5 100644 --- a/matita/components/binaries/matex/alpha.ml +++ b/matita/components/binaries/matex/alpha.ml @@ -13,6 +13,7 @@ module L = List module P = Printf module S = Scanf module N = String +module H = Hashtbl module U = NUri module C = NCic @@ -24,9 +25,15 @@ module X = Ground module G = Options module K = Kernel -let dno = "_" (* does not occur *) +type global = (string, int) H.t -let nan = -1 (* not a number *) +type local = (string * int) list + +type status = { + g: global; (* global context for alpha-conversion *) + d: local; (* local context for alpha-conversion *) + c: C.context; (* local context for kernel calls *) +} (* internal functions *******************************************************) @@ -36,6 +43,10 @@ let malformed s = let ok s = X.log ("alpha: ok " ^ s) +let init () = { + g = H.create 11; d = []; c = []; +} + let rec trim r = let r1, r2 = S.sscanf r "%s@_%s" X.id2 in if r2 = "" then r1 else trim r1 @@ -48,7 +59,7 @@ let split s = let i, l = aux (N.length s) 0 in let s1, s2 = N.sub s 0 i, N.sub s i l in let s1 = if s1 = "" then "_" else s1 in - s1, if l = 0 then nan else int_of_string s2 + s1, if l = 0 then G.nan else int_of_string s2 let rec strip = function | C.Appl (t :: _) @@ -94,59 +105,70 @@ let rec get r = function | (h, d) :: tl -> if fst r = h && snd r <= d then h, succ d else get r tl -let alpha d c s w t = - if K.does_not_occur K.fst_var c t then dno, nan else - let r, i = split (trim s) in - get (type_check r c w, i) d - let mk_name (s, i) = if i < 0 then s else P.sprintf "%s%u" s i +let local_alpha st s w t = + if K.does_not_occur K.fst_var st.c t then G.dno_id, G.nan else + let r, i = split (trim s) in + get (type_check r st.c w, i) st.d + +let global_apha st s = +try + let i = H.find st.g s in + H.replace st.g s (succ i); + P.sprintf "%s.%u" s i +with Not_found -> + H.add st.g s 0; + s + +let alpha st s w t = + let r = local_alpha st s w t in + let s = mk_name r in + r, if G.is_global_id s then global_apha st s else s + let add_name r d = r :: d -let rec proc_term d c t = match t with +let rec proc_term st t = match t with | C.Meta _ | C.Implicit _ | C.Sort _ | C.Rel _ | C.Const _ -> t | C.Appl ts -> - let tts = proc_terms d c ts in + let tts = proc_terms st ts in K.appl tts | C.Match (w, u, v, ts) -> - let uu = proc_term d c u in - let vv = proc_term d c v in - let tts = proc_terms d c ts in + let uu = proc_term st u in + let vv = proc_term st v in + let tts = proc_terms st ts in K.case w uu vv tts | C.Prod (s, w, t) -> - let rr = alpha d c s w t in - let ss = mk_name rr in - let ww = proc_term d c w in - let tt = proc_term (add_name rr d) (K.add_dec ss w c) t in + let rr, ss = alpha st s w t in + let ww = proc_term st w in + let tt = proc_term {st with d=add_name rr st.d; c=K.add_dec ss w st.c} t in K.prod ss ww tt | C.Lambda (s, w, t) -> - let rr = alpha d c s w t in - let ss = mk_name rr in - let ww = proc_term d c w in - let tt = proc_term (add_name rr d) (K.add_dec ss w c) t in + let rr, ss = alpha st s w t in + let ww = proc_term st w in + let tt = proc_term {st with d=add_name rr st.d; c=K.add_dec ss w st.c} t in K.lambda ss ww tt | C.LetIn (s, w, v, t) -> - let rr = alpha d c s w t in - let ss = mk_name rr in - let ww = proc_term d c w in - let vv = proc_term d c v in - let tt = proc_term (add_name rr d) (K.add_def ss w v c) t in + let rr, ss = alpha st s w t in + let ww = proc_term st w in + let vv = proc_term st v in + let tt = proc_term {st with d=add_name rr st.d; c=K.add_def ss w v st.c} t in K.letin ss ww vv tt -and proc_terms d c ts = - let rtts = L.rev_map (proc_term d c) ts in +and proc_terms st ts = + let rtts = L.rev_map (proc_term st) ts in L.rev rtts -let proc_named_term s d c t = +let proc_named_term s st t = try - let tt = proc_term d c t in + let tt = proc_term st t in if !G.test then begin - let _ = K.typeof c tt in + let _ = K.typeof st.c tt in ok s end; tt @@ -156,4 +178,5 @@ with (* interface functions ******************************************************) -let process_top_term s t = proc_named_term s [] [] t +let process_top_term s t = proc_named_term s (init ()) t + diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 0174af613..7001fb99e 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -29,8 +29,10 @@ module A = Anticipate module N = Alpha type status = { + i: string; (* item name *) n: string; (* reference name *) s: int list; (* scope *) + c: C.context (* context for kernel calls *) } (* internal functions *******************************************************) @@ -43,50 +45,53 @@ let malformed s = (* generic term processing *) -let proc_sort is = function +let mk_ptr st name = + if G.is_global_id name then P.sprintf "%s.%s" st.i name else "" + +let proc_sort st is = function | C.Prop -> T.Macro "PROP" :: is | C.Type [`Type, u] -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is | C.Type _ -> malformed "T1" -let rec proc_term is c = function +let rec proc_term st is = function | C.Appl [] | C.Meta _ | C.Implicit _ -> malformed "T2" | C.Rel m -> - let name = K.resolve_lref c m in - T.Macro "LREF" :: T.arg name :: T.free name :: is + let name = K.resolve_lref st.c m in + T.Macro "LREF" :: T.arg name :: T.free (mk_ptr st name) :: is | C.Appl ts -> - let riss = L.rev_map (proc_term [] c) ts in + let riss = L.rev_map (proc_term st []) ts in T.Macro "APPL" :: T.mk_rev_args riss is | C.Prod (s, w, t) -> - let is_w = proc_term [] c w in - let is_t = proc_term is (K.add_dec s w c) t in - T.Macro "PROD" :: T.arg s :: T.Group is_w :: is_t + let is_w = proc_term st [] w in + let is_t = proc_term {st with c=K.add_dec s w st.c} is t in + T.Macro "PROD" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t | C.Lambda (s, w, t) -> - let is_w = proc_term [] c w in - let is_t = proc_term is (K.add_dec s w c) t in - T.Macro "ABST" :: T.arg s :: T.Group is_w :: is_t + let is_w = proc_term st [] w in + let is_t = proc_term {st with c=K.add_dec s w st.c} is t in + T.Macro "ABST" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t | C.LetIn (s, w, v, t) -> - let is_w = proc_term [] c w in - let is_v = proc_term [] c v in - let is_t = proc_term is (K.add_def s w v c) t in - T.Macro "ABBR" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t + let is_w = proc_term st [] w in + let is_v = proc_term st [] v in + let is_t = proc_term {st with c=K.add_def s w v st.c} is t in + T.Macro "ABBR" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t | C.Sort s -> - proc_sort is s + proc_sort st is s | C.Const (R.Ref (u, r)) -> let ss = K.segments_of_uri u in let _, _, _, _, obj = E.get_checked_obj G.status u in let ss, name = K.name_of_reference ss (obj, r) in T.Macro "GREF" :: T.arg name :: T.free (X.rev_map_concat X.id "." "type" ss) :: is | C.Match (w, u, v, ts) -> - let is_w = proc_term [] c (C.Const w) in - let is_u = proc_term [] c u in - let is_v = proc_term [] c v in - let riss = L.rev_map (proc_term [] c) ts in + let is_w = proc_term st [] (C.Const w) in + let is_u = proc_term st [] u in + let is_v = proc_term st [] v in + let riss = L.rev_map (proc_term st []) ts in T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is -let proc_term is c t = try proc_term is c t with +let proc_term st is t = try proc_term st is t with | E.ObjectNotFound _ | Invalid_argument "List.nth" | Failure "nth" @@ -94,19 +99,21 @@ let proc_term is c t = try proc_term is c t with (* proof processing *) -let typeof c = function +let typeof st = function | C.Appl [t] - | t -> K.whd_typeof c t + | t -> K.whd_typeof st.c t -let init () = { - n = ""; s = [1] +let init i = { + i = i; + n = ""; s = [1]; c = []; } -let push st n = { +let push st n = {st with n = n; s = 1 :: st.s; } -let next st = { +let next st f = {st with + c = f st.c; n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl } @@ -119,51 +126,51 @@ let mk_exit st ris = let mk_open st ris = if st.n = "" then ris else - T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris + T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg st.n :: T.Macro "OPEN" :: ris -let mk_dec kind w s ris = +let mk_dec st kind w s ris = let w = if !G.no_types then [] else w in - T.Group w :: T.free s :: T.arg s :: T.Macro kind :: ris + T.Group w :: T.free (mk_ptr st s) :: T.arg s :: T.Macro kind :: ris -let mk_inferred st c t ris = - let u = typeof c t in - let is_u = proc_term [] c u in - mk_dec "DECL" is_u st.n ris +let mk_inferred st t ris = + let u = typeof st t in + let is_u = proc_term st [] u in + mk_dec st "DECL" is_u st.n ris -let rec proc_proof st ris c t = match t with +let rec proc_proof st ris t = match t with | C.Appl [] | C.Meta _ | C.Implicit _ | C.Sort _ | C.Prod _ -> malformed "P1" | C.Const _ - | C.Rel _ -> proc_proof st ris c (C.Appl [t]) + | C.Rel _ -> proc_proof st ris (C.Appl [t]) | C.Lambda (s, w, t) -> - let is_w = proc_term [] c w in + let is_w = proc_term st [] w in let ris = mk_open st ris in - proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t + proc_proof (next st (K.add_dec s w)) (mk_dec st "PRIM" is_w s ris) t | C.Appl (t0 :: ts) -> - let rts = X.rev_neg_filter (K.not_prop2 c) [t0] ts in - let ris = T.Macro "STEP" :: mk_inferred st c t ris in - let tts = L.rev_map (proc_term [] c) rts in + let rts = X.rev_neg_filter (K.not_prop2 st.c) [t0] ts in + let ris = T.Macro "STEP" :: mk_inferred st t ris in + let tts = L.rev_map (proc_term st []) rts in mk_exit st (T.rev_mk_args tts ris) | C.Match (w, u, v, ts) -> - let rts = X.rev_neg_filter (K.not_prop2 c) [v] ts in - let ris = T.Macro "DEST" :: mk_inferred st c t ris in - let tts = L.rev_map (proc_term [] c) rts in + let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in + let ris = T.Macro "DEST" :: mk_inferred st t ris in + let tts = L.rev_map (proc_term st []) rts in mk_exit st (T.rev_mk_args tts ris) | C.LetIn (s, w, v, t) -> - let is_w = proc_term [] c w in + let is_w = proc_term st [] w in let ris = mk_open st ris in - if K.not_prop1 c w then - let is_v = proc_term [] c v in - let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in - proc_proof (next st) ris (K.add_def s w v c) t + if K.not_prop1 st.c w then + let is_v = proc_term st [] v in + let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec st "DECL" is_w s ris in + proc_proof (next st (K.add_def s w v)) ris t else - let ris_v = proc_proof (push st s) ris c v in - proc_proof (next st) ris_v (K.add_def s w v c) t + let ris_v = proc_proof (push st s) ris v in + proc_proof (next st (K.add_def s w v)) ris_v t -let proc_proof rs c t = try proc_proof (init ()) rs c t with +let proc_proof st rs t = try proc_proof st rs t with | E.ObjectNotFound _ | Invalid_argument "List.nth" | Failure "nth" @@ -178,15 +185,17 @@ let proc_proof rs c t = try proc_proof (init ()) rs c t with let note = T.Note "This file was automatically generated by MaTeX: do not edit" let proc_item item s ss t = + let st = init ss in let tt = N.process_top_term s t in (* alpha-conversion *) let is = [T.Macro "end"; T.arg item] in - note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term is [] tt + note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term st is tt let proc_top_proof s ss t = + let st = init ss in let t0 = A.process_top_term s t in (* anticipation *) let tt = N.process_top_term s t0 in (* alpha-conversion *) let ris = [T.free ss; T.arg s; T.arg "proof"; T.Macro "begin"; note] in - L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt) + L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt) let open_out_tex s = let fname = s ^ T.file_ext in diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index 46ef1c894..9ca51c1fe 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -25,8 +25,9 @@ module K = Kernel let help_O = " Set this output directory" let help_X = " Clear configuration and options" let help_a = " Log alpha-unconverted identifiers (default: no)" +let help_g = " Global alpha-conversion (default: no)" let help_l = " Output the list of generated files in this file" -let help_p = " omit types (default: no)" +let help_p = " Omit types (default: no)" let help_t = " Test term transformations (default: no)" let help = "" @@ -69,6 +70,7 @@ begin try "-O", A.String ((:=) G.out_dir), help_O; "-X", A.Unit G.clear, help_X; "-a", A.Set G.log_alpha, help_a; + "-g", A.Set G.global_alpha, help_g; "-l", A.String set_list, help_l; "-p", A.Set G.no_types, help_p; "-t", A.Set G.test, help_t; diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index 8b94b003d..da60a79bb 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -26,6 +26,8 @@ let default_test = false let default_no_types = false +let default_global_alpha = false + let default_log_alpha = false let default_list_och = None @@ -34,25 +36,34 @@ let default_alpha = [] (* interface ****************************************************************) +let dno_id = "_" (* identifier for not-occurring premises *) + +let nan = -1 (* not a number *) + let status = new P.status let no_init = ref default_no_init -let out_dir = ref default_out_dir (* directory of generated files *) +let out_dir = ref default_out_dir (* directory of generated files *) + +let proc_id = ref default_proc_id (* identifer for anticipations *) + +let test = ref default_test (* test anticipation *) -let proc_id = ref default_proc_id (* identifer of anticipations *) +let no_types = ref default_no_types (* omit types *) -let test = ref default_test (* test anticipation *) +let global_alpha = ref default_global_alpha (* log alpha-unconverted identifiers *) -let no_types = ref default_no_types (* omit types *) +let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *) -let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *) +let list_och = ref default_list_och (* output stream for list file *) -let list_och = ref default_list_och (* output stream for list file *) +let alpha_type = ref default_alpha (* data of type-based alpha-conversion *) -let alpha_type = ref default_alpha (* data of type-based alpha-conversion *) +let alpha_sort = ref default_alpha (* data of sort-based alpha-conversion *) -let alpha_sort = ref default_alpha (* data of sort-based alpha-conversion *) +let is_global_id s = + !global_alpha && s <> dno_id let close_list () = match !list_och with | None -> () @@ -65,6 +76,7 @@ let clear () = proc_id := default_proc_id; test := default_test; no_types := default_no_types; + global_alpha := default_global_alpha; log_alpha := default_log_alpha; list_och := default_list_och; alpha_type := default_alpha; diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index 15a272520..b2ad2cf47 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -9,6 +9,10 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +val dno_id: string + +val nan: int + val status: NCicPp.status val no_init: bool ref @@ -21,6 +25,8 @@ val test: bool ref val no_types: bool ref +val global_alpha: bool ref + val log_alpha: bool ref val list_och: out_channel option ref @@ -32,3 +38,5 @@ val alpha_sort: (string * string * string) list ref val clear: unit -> unit val close_list: unit -> unit + +val is_global_id: string -> bool diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index 11becffe8..a25d051cb 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,5 +1,5 @@ \NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesPackage{matex}[2016/04/28 MaTeX Package] +\ProvidesPackage{matex}[2016/05/22 MaTeX Package] \RequirePackage{xcolor} \ExecuteOptions{} \ProcessOptions* @@ -23,54 +23,63 @@ %\newcommand*\ObjRef[1]{\hyperlink{obj:#1}{\ref*{obj:#1}}} %\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}} -\newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{}} +\newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{#1}} \newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}} \newcommand*\ObjIncNode{} \newcommand*\ObjNode{} -\newcommand*\ma@thehead[2]{\ObjIncNode\textbf{#1 \ObjNode(#2)}\neverindent\par} +\newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par} \newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par} -\newenvironment{axiom}[2]{\ma@settarget{#1}{#2}\ma@thehead{Axiom}{#1}}{\par} -\newenvironment{declaration}[2]{\ma@settarget{#1}{#2}\ma@thehead{Declaration}{#1}}{\par} +\newenvironment{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}}{\par} +\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}}{\par} \newenvironment{definition}[2]{}{\par} -\newenvironment{proposition}[2]{\ma@settarget{#1}{#2}\ma@thehead{Proposition}{#1}}{\par} +\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}}{\par} \newenvironment{proof}[2]{\ma@theneck{Proof}}{\par} \newenvironment{ma@step}[1]{\color{#1}}{\par} \newcommand*\ma@tmp{} \newcommand*\ma@skip[4]{} -\newcommand*\ma@next[5]{\def\ma@tmp{#5}\ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi\ma@tmp #3#2#3#4} +\newcommand*\ma@next[5]{\def\ma@tmp{#5}% + \ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi + \ma@tmp #3#2#3#4% +} \newcommand*\ma@space{ } \newcommand*\ma@arg[1]{#1} +\newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}% + \ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi +} + \newcommand*\PROP{PROP} \newcommand*\CROP[1]{CROP} \newcommand*\TYPE[1]{TYPE} -\newcommand*\LREF[2]{#1} +\newcommand*\LREF[2]{\def\ma@tmp{#2}% + \ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi +} \newcommand*\GREF[2]{\ma@setlink{#1}{#2}} -\newcommand*\ABBR[3]{(D #1 #2 #3) } -\newcommand*\ABST[2]{(I #1 #2) } -\newcommand*\PROD[2]{(P #1 #2) } +\newcommand*\ABBR[4]{(D \ma@setopttarget{#1}{#2} #3 #4) } +\newcommand*\ABST[3]{(I \ma@setopttarget{#1}{#2} #3) } +\newcommand*\PROD[3]{(P \ma@setopttarget{#1}{#2} #3) } \newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax} \newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax} \newcommand*\ma@with{ with } \newcommand*\ma@comma{, } \newcommand*\ma@stop{.\end{ma@step}} -\newcommand*\ma@head[4]{\def\ma@tmp{#4}% - \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{#2}% - \else\begin{ma@step}{#3}\textbf{#4}% +\newcommand*\ma@head[6]{\def\ma@tmp{#5}% + \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{\ma@setopttarget{#2}{#3}}% + \else\begin{ma@step}{#4}\textbf{\ma@setopttarget{#5}{#6}}% \fi } \newcommand*\ma@tail{\ma@next\ma@with\ma@arg\ma@comma\ma@stop} -\newcommand*\EXIT[1]{\ma@head{}{}{\ma@exit}{end} of block #1\ma@stop} -\newcommand*\OPEN[3]{\ma@head{}{}{\ma@open}{#1} is this block #3\ma@stop} -\newcommand*\PRIM[3]{\ma@head{}{}{\ma@prim}{#1} will have type #3\ma@stop} -\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\par} +\newcommand*\EXIT[1]{\ma@head{}{}{}{\ma@exit}{end}{} of block #1\ma@stop} +\newcommand*\OPEN[3]{\ma@head{}{}{}{\ma@open}{#1}{#2} is this block #3\ma@stop} +\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type #3\ma@stop} +\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type #3\par} \newcommand*\BODY[1]{being #1\ma@stop} \newcommand*\STEP[1]{by #1\ma@tail} \newcommand*\DEST[1]{by cases on #1\ma@tail} -- 2.39.2