From d1493110851b34e70d11eb419e557aad9bc9f2de Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 2 Feb 2016 00:00:19 +0000 Subject: [PATCH] - scope management begins... - improved style sheet --- matita/components/binaries/matex/engine.ml | 34 ++++++++++++++----- .../components/binaries/matex/test/matex.sty | 1 + 2 files changed, 27 insertions(+), 8 deletions(-) diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 9b7ba8253..cd8ab9a01 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -28,8 +28,10 @@ module O = TeXOutput module A = Anticipate type status = { - n: string; (* object name *) + g: string; (* global object name *) + l: string; (* local reference name *) s: int list; (* scope *) + w: bool; (* is first construction *) } (* internal functions *******************************************************) @@ -99,12 +101,27 @@ let proc_term c t = try proc_term c t with (* proof processing *) let init n = { - n = n; s = []; + g = n; l = "_"; s = []; w = true } -let mk_dec w s is = +let push st n = {st with + l = n; s = 1 :: st.s; w = true +} + +let pop st = {st with + w = false; s = match st.s with [] -> [] | i :: tl -> succ i :: tl +} + +let next st = {st with + w = false +} + +let mk_open st ris = + if st.w then T.Macro "PRIM" :: T.arg "" :: T.Macro "OPEN" :: ris else ris + +let mk_dec w s ris = let w = if !G.no_types then [] else w in - T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: is + T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: ris let rec proc_proof st ris c t = match t with | C.Appl [] @@ -117,7 +134,8 @@ let rec proc_proof st ris c t = match t with | C.Lambda (s, w, t) -> let s = alpha c s in let is_w = proc_term c w in - proc_proof st (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t + let ris = mk_open st ris in + proc_proof (next st) (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t | C.Appl ts -> let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in let ris = T.Macro "STEP" :: ris in @@ -133,10 +151,10 @@ let rec proc_proof st ris c t = match t with let is_w = proc_term c w in if A.not_prop1 c w then let is_v = proc_term c v in - proc_proof st (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t + proc_proof (next st) (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t else - let ris_v = proc_proof st ris c v in - proc_proof st (mk_dec is_w s ris_v) (K.add_def s w v c) t + let ris_v = proc_proof (push st s) ris c v in + proc_proof (pop st) (mk_dec is_w s ris_v) (K.add_def s w v c) t let proc_proof c t = try proc_proof (init "") [] c t with | E.ObjectNotFound _ diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index 6bbcfe094..de1b6a0f5 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -9,6 +9,7 @@ \newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}} +\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} -- 2.39.2