From 788e7cb15734fd228e8788ea628934af483ae772 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 2 Feb 2016 16:52:55 +0000 Subject: [PATCH] - scope management completed - improved style sheet and test document --- .../components/binaries/matex/anticipate.ml | 4 +- .../components/binaries/matex/anticipate.mli | 2 + matita/components/binaries/matex/engine.ml | 65 ++++++++++++------- matita/components/binaries/matex/ground.ml | 10 +-- matita/components/binaries/matex/ground.mli | 4 +- .../components/binaries/matex/test/matex.sty | 23 +++++-- .../components/binaries/matex/test/test.tex | 2 +- 7 files changed, 73 insertions(+), 37 deletions(-) diff --git a/matita/components/binaries/matex/anticipate.ml b/matita/components/binaries/matex/anticipate.ml index 1681d2d03..1081dffcc 100644 --- a/matita/components/binaries/matex/anticipate.ml +++ b/matita/components/binaries/matex/anticipate.ml @@ -29,7 +29,9 @@ let malformed s = let ok s = X.log ("anticipate: ok " ^ s) -let not_prop1 c u = match (K.whd c (K.typeof c u)) with +let typeof c t = K.whd c (K.typeof c t) + +let not_prop1 c u = match typeof c u with | C.Sort (C.Prop) -> false | C.Sort _ -> true | _ -> malformed "1" diff --git a/matita/components/binaries/matex/anticipate.mli b/matita/components/binaries/matex/anticipate.mli index e934bb462..ec5a77775 100644 --- a/matita/components/binaries/matex/anticipate.mli +++ b/matita/components/binaries/matex/anticipate.mli @@ -9,6 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +val typeof: NCic.context -> NCic.term -> NCic.term + val not_prop1: NCic.context -> NCic.term -> bool val not_prop2: NCic.context -> NCic.term -> bool diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index cd8ab9a01..b2117aa5e 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -28,16 +28,17 @@ module O = TeXOutput module A = Anticipate type status = { - g: string; (* global object name *) - l: string; (* local reference name *) + n: string; (* reference name *) s: int list; (* scope *) - w: bool; (* is first construction *) } (* internal functions *******************************************************) let alpha c s = s +let internal s = + X.error ("engine: malformed stack: " ^ s) + let malformed s = X.error ("engine: malformed term: " ^ s) @@ -84,7 +85,7 @@ let rec proc_term c = function 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_concat "." "type" ss)] + [T.Macro "GREF"; T.arg name; T.free (X.rev_map_concat X.id "." "type" ss)] | C.Match (w, u, v, ts) -> let is_w = proc_term c (C.Const w) in let is_u = proc_term c u in @@ -100,29 +101,42 @@ let proc_term c t = try proc_term c t with (* proof processing *) -let init n = { - g = n; l = "_"; s = []; w = true -} +let typeof c = function + | C.Appl [t] + | t -> A.typeof c t -let push st n = {st with - l = n; s = 1 :: st.s; w = true +let init () = { + n = ""; s = [1] } -let pop st = {st with - w = false; s = match st.s with [] -> [] | i :: tl -> succ i :: tl +let push st n = { + n = n; s = 1 :: st.s; } -let next st = {st with - w = false +let next st = { + n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl } +let scope st = + X.rev_map_concat string_of_int "." "" (L.tl st.s) + +let mk_exit st ris = + if st.n <> "" || L.tl st.s = [] then ris else + T.free (scope st) :: T.Macro "EXIT" :: ris + let mk_open st ris = - if st.w then T.Macro "PRIM" :: T.arg "" :: T.Macro "OPEN" :: ris else ris + if st.n = "" then ris else + T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: 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" :: ris +let mk_inferred st c t ris = + let u = typeof c t in + let is_u = proc_term c u in + mk_dec is_u st.n ris + let rec proc_proof st ris c t = match t with | C.Appl [] | C.Meta _ @@ -138,31 +152,34 @@ let rec proc_proof st ris c t = match t with 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 + let ris = T.Macro "STEP" :: mk_inferred st c t ris in let tts = L.rev_map (proc_term c) rts in - T.rev_mk_args tts ris + mk_exit st (T.rev_mk_args tts ris) | C.Match (w, u, v, ts) -> let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in - let ris = T.Macro "DEST" :: ris in + let ris = T.Macro "DEST" :: mk_inferred st c t ris in let tts = L.rev_map (proc_term c) rts in - T.rev_mk_args tts ris + mk_exit st (T.rev_mk_args tts ris) | C.LetIn (s, w, v, t) -> let s = alpha c s in let is_w = proc_term c w in + let ris = mk_open st ris in if A.not_prop1 c w then let is_v = proc_term c v in 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 (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 + proc_proof (next st) ris_v (K.add_def s w v c) t -let proc_proof c t = try proc_proof (init "") [] c t with +let proc_proof rs c t = try proc_proof (init ()) rs c t with | E.ObjectNotFound _ | Invalid_argument "List.nth" - | Failure "nth" + | Failure "nth" | Failure "name_of_reference" -> malformed "P2" | V.TypeCheckerFailure s | V.AssertFailure s -> malformed (Lazy.force s) + | Failure "hd" + | Failure "tl" -> internal "P2" (* top level processing *) @@ -173,20 +190,20 @@ let proc_top_body s t = proc_term [] t let proc_top_proof s t = let tt = A.process_top_term s t in (* anticipation *) - L.rev (proc_proof [] tt) + L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof [T.arg "proof"; T.Macro "begin"] [] tt) let open_out_tex s = open_out (F.concat !G.out_dir (s ^ T.file_ext)) let proc_pair s ss u xt = - let name = X.rev_concat "." "type" ss in + let name = X.rev_map_concat X.id "." "type" ss in let och = open_out_tex name in O.out_text och (proc_top_type s u); close_out och; match xt with | None -> () | Some t -> - let name = X.rev_concat "." "body" ss in + let name = X.rev_map_concat X.id "." "body" ss in let och = open_out_tex name in let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in O.out_text och (text s t); diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml index 022ab63f2..c24162ae0 100644 --- a/matita/components/binaries/matex/ground.ml +++ b/matita/components/binaries/matex/ground.ml @@ -17,16 +17,18 @@ exception Error of string (* interface functions ******************************************************) +let id x = x + let rec segments_of_string ss l s = match try Some (S.index s '/') with Not_found -> None with | None -> s :: ss | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1)) -let rec rev_concat sep r = function +let rec rev_map_concat map sep r = function | [] -> r | s :: ss -> - if r = "" then rev_concat sep s ss else - rev_concat sep (s ^ sep ^ r) ss + if r = "" then rev_map_concat map sep (map s) ss else + rev_map_concat map sep (map s ^ sep ^ r) ss let fold_string map a s = let l = S.length s in @@ -50,4 +52,4 @@ let rec rev_map_append map l r = match l with let error s = raise (Error s) -let log s = P.eprintf "MaTeX: %s\n" s +let log s = P.eprintf "MaTeX: %s\n%!" s diff --git a/matita/components/binaries/matex/ground.mli b/matita/components/binaries/matex/ground.mli index e9892a7e0..5c02eb9d1 100644 --- a/matita/components/binaries/matex/ground.mli +++ b/matita/components/binaries/matex/ground.mli @@ -15,9 +15,11 @@ val error: string -> 'a val log: string -> unit +val id: 'a -> 'a + val segments_of_string: string list -> int -> string -> string list -val rev_concat: string -> string -> string list -> string +val rev_map_concat: ('a -> string) -> string -> string -> 'a list -> string val fold_string: ('a -> char -> 'a) -> 'a -> string -> 'a diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index de1b6a0f5..505d68176 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,3 +1,8 @@ +\NeedsTeXFormat{LaTeX2e}[1995/12/01] +\ProvidesPackage{matex}[2015/12/21 MaTeX Package] +\ExecuteOptions{} +\ProcessOptions* + \makeatletter \newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}} @@ -6,6 +11,8 @@ \newcommand*\ObjRef[1]{\ref{obj:#1}} \newtheorem{prop}{Proposition} +\newenvironment{proof}{\setlength\parindent{0pt}}{} +\newenvironment{ma@step}{}{\vskip0pt} \newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}} @@ -29,12 +36,16 @@ \newcommand*\ma@with{ with } \newcommand*\ma@comma{, } -\newcommand*\ma@stop{.\vskip10pt} +\newcommand*\ma@stop{.\end{ma@step}} -\newcommand*\DECL[3]{\textbf{#1} : #3\vskip10pt} -\newcommand*\PRIM{} -\newcommand*\BODY[1]{is #1\vskip10pt} -\newcommand*\STEP[1]{by #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop} -\newcommand*\DEST[1]{by cases on #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop} +\newcommand*\DECL[3]{\def\ma@tmp{#1}\begin{ma@step}\textbf{\ifx\ma@tmp\empty\_conlusion\else #1\fi} of type #3} +\newcommand*\PRIM{\end{ma@step}} +\newcommand*\BODY[1]{\\is #1\end{ma@step}} +\newcommand*\STEP[1]{\\by #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop} +\newcommand*\DEST[1]{\\by cases on #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop} +\newcommand*\OPEN[3]{\begin{ma@step}\textbf{#1} is the following scope #3.\end{ma@step}} +\newcommand*\EXIT[1]{\begin{ma@step}\textbf{end} of scope #1.\end{ma@step}} \makeatother + +\endinput diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index e30233190..80f765652 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -1,4 +1,4 @@ -\documentclass{article} +\documentclass[8pt,twocolumn]{extarticle} \usepackage[bookmarks=false,ps2pdf]{hyperref} \usepackage[american]{babel} -- 2.39.2