From: Ferruccio Guidi Date: Mon, 27 Feb 2017 16:35:21 +0000 (+0000) Subject: - initial support for sigma-types X-Git-Tag: make_still_working~496 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4ce6264997ad60716f5845ff5474796f777e0a49;p=helm.git - initial support for sigma-types - matex.sty: some style improvements - test.tex: red boxes arround hyperlinks removed --- diff --git a/matita/components/binaries/matex/alpha.ml b/matita/components/binaries/matex/alpha.ml index 6420d20c6..b4d4b31cd 100644 --- a/matita/components/binaries/matex/alpha.ml +++ b/matita/components/binaries/matex/alpha.ml @@ -17,7 +17,6 @@ module H = Hashtbl module U = NUri module C = NCic -module R = NReference module E = NCicEnvironment module T = NCicTypeChecker @@ -115,7 +114,7 @@ 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 + P.sprintf "%s_%u" s i with Not_found -> H.add st.g s 0; s @@ -178,4 +177,3 @@ with (* interface functions ******************************************************) 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 23e6f687a..324d114a9 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -26,6 +26,7 @@ module K = Kernel module T = TeX module O = TeXOutput module A = Anticipate +module M = Meta module N = Alpha type status = { diff --git a/matita/components/binaries/matex/meta.ml b/matita/components/binaries/matex/meta.ml new file mode 100644 index 000000000..1f1e91724 --- /dev/null +++ b/matita/components/binaries/matex/meta.ml @@ -0,0 +1,80 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module L = List + +module C = NCic + +module X = Ground +module G = Options +module K = Kernel + +type term = Meta + | Sort of C.sort + | GRef of string * string + | LRef of int + | Appl of term list + | Prod of string * term * term + | Abst of string * term * term + | Abbr of string * term * term * term + | Case of term * term * term * term list + | Sigs of string list * term list * term list + +(* internal functions *******************************************************) + +let get_sigs s = + let rec aux = function + | [] -> G.nan, G.nan + | (n, i, j) :: tl -> + if n = s then i, j else aux tl + in + aux !G.sigs_gref + +let rec get_names ss j t = + if j <= 0 then ss else match t with + | Abst (s, _, t) -> get_names (s :: ss) (pred j) t + | _ -> assert false + +let rec trim_absts j t = + if j <= 0 then t else match t with + | Abst (_, _, t) -> trim_absts (pred j) t + | _ -> assert false + +let proc_appl ts = match ts with + | GRef (s, _) :: vs -> + let i, j = get_sigs s in + if L.length vs <> i + j || i = 0 || j = 0 then Appl ts else + let types, preds = X.split_at j vs in + let names = get_names [] j (L.hd preds) in + let preds = L.rev_map (trim_absts j) preds in + Sigs (names, types, preds) + | ts -> Appl ts + +let rec proc_term = function + | C.Meta _ + | C.Implicit _ -> Meta + | C.Sort s -> Sort s + | C.Const c -> + let s, name = K.resolve_reference c in + GRef (s, name) + | C.Rel m -> LRef m + | C.Appl ts -> proc_appl (proc_terms ts) + | C.Prod (s, w, t) -> Prod (s, proc_term w, proc_term t) + | C.Lambda (s, w, t) -> Abst (s, proc_term w, proc_term t) + | C.LetIn (s, w, v, t) -> Abbr (s, proc_term w, proc_term v, proc_term t) + | C.Match (c, u, v, ts) -> Case (proc_term (C.Const c), proc_term u, proc_term v, proc_terms ts) + +and proc_terms ts = + L.rev (L.rev_map proc_term ts) + +(* interface functions ******************************************************) + +let process = proc_term diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index 165b2d978..b64fb6050 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -40,6 +40,8 @@ let default_alpha = [] let default_macro = [] +let default_sigs = [] + (* interface ****************************************************************) let dno_id = "_" (* identifier for not-occurring premises *) @@ -76,6 +78,8 @@ let alpha_gref = ref default_alpha (* data for constant renaming *) let macro_gref = ref default_macro (* data for eta-conversion and constant rendering *) +let sigs_gref = ref default_sigs (* data for sigma-type rendering *) + let is_global_id s = !global_alpha && s <> dno_id @@ -98,4 +102,5 @@ let clear () = alpha_type := default_alpha; alpha_sort := default_alpha; alpha_gref := default_alpha; - macro_gref := default_macro + macro_gref := default_macro; + sigs_gref := default_sigs diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index 1c6aef077..2e97cf9bb 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -43,6 +43,8 @@ val alpha_gref: (string * string) list ref val macro_gref: (string * string * int * int) list ref +val sigs_gref: (string * int * int) list ref + val clear: unit -> unit val close_list: unit -> unit diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index eab676018..4bd7393ea 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/07/03 MaTeX Package] +\ProvidesPackage{matex}[2017/02/27 MaTeX Package] \RequirePackage{xcolor} \RequirePackage[lcgreekalpha]{stix} \ExecuteOptions{} @@ -9,6 +9,11 @@ \makeatletter +\newcommand*\ma@sort{\mathrm} +\newcommand*\ma@gref{\mathrm} +\newcommand*\ma@lref{\mathrm} +\newcommand*\ma@decl{\mathbf} + \definecolor{ma@black}{HTML}{000000} \definecolor{ma@blue}{HTML}{00005F} \definecolor{ma@purple}{HTML}{3F005F} @@ -90,20 +95,20 @@ \newcommand*\ma@bind{\ma@thop{}} \newcommand*\ma@skip[1]{} -\newcommand*\PROP{\mathord\mathrm{PROP}} -\newcommand*\CROP[1]{\mathord\mathrm{CROP}} -\newcommand*\TYPE[1]{\mathord\mathrm{TYPE}} -\newcommand*\LREF[2]{\ma@setoptlink{#1}{#2}} -\newcommand*\GREF[2]{\ma@setoptlink{\mathrm{#1}}{#2}} -\newcommand*\ABBR[4]{\ma@op\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3\ma@cp\ma@bind} -\newcommand*\ABST[3]{\ma@op\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind} +\newcommand*\PROP{\mathord\ma@sort{PROP}} +\newcommand*\CROP[1]{\mathord\ma@sort{CROP}} +\newcommand*\TYPE[1]{\mathord\ma@sort{TYPE}} +\newcommand*\LREF[2]{\ma@setoptlink{\ma@lref{#1}}{#2}} +\newcommand*\GREF[2]{\ma@setoptlink{\ma@gref{#1}}{#2}} +\newcommand*\ABBR[4]{\ma@op\ma@setopttarget{\ma@lref{#1}}{#2}\ma@abbr #4\ma@cast #3\ma@cp\ma@bind} +\newcommand*\ABST[3]{\ma@op\ma@setopttarget{\ma@lref{#1}}{#2}\ma@cast #3\ma@cp\ma@bind} \newcommand*\PROD[3]{\def\ma@tmp{#2}% \ifx\ma@tmp\empty #3\ma@arrw\else - \ma@op\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi + \ma@op\ma@prod\ma@setopttarget{\ma@lref{#1}}{#2}\ma@cast #3\ma@cp\ma@bind\fi } \newcommand*\FALL[3]{\def\ma@tmp{#2}% \ifx\ma@tmp\empty #3\ma@impl\else - \ma@op\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi + \ma@op\ma@fall\ma@setopttarget{\ma@lref{#1}}{#2}\ma@cast #3\ma@cp\ma@bind\fi } \newcommand*\APPL[1]{#1\ma@args} \newcommand*\CASE[3]{#3\ma@case\ma@cases} @@ -115,13 +120,13 @@ \newcommand*\ma@comma{, } \newcommand*\ma@stop{.\end{ma@step}} \newcommand*\ma@head[6]{\def\ma@tmp{#5}% - \ifx\ma@tmp\empty\begin{ma@step}{#1}$\mathbf{\ma@setopttarget{#2}{#3}}$% - \else\begin{ma@step}{#4}$\mathbf{\ma@setopttarget{#5}{#6}}$% + \ifx\ma@tmp\empty\begin{ma@step}{#1}$\ma@setopttarget{\ma@decl{#2}}{#3}$% + \else\begin{ma@step}{#4}$\ma@setopttarget{\ma@decl{#5}}{#6}$% \fi } \newcommand*\ma@tail{\ma@list\ma@with\ma@term\ma@comma\ma@stop} \newcommand*\ma@type[1]{\def\ma@tmp{#1}% - \ifx\ma@tmp\empty\mathrm{(omitted)}\else #1\fi + \ifx\ma@tmp\empty\ma@gref{(omitted)}\else #1\fi } \newcommand*\EXIT[1]{\ma@head{\ma@exit}{end}{}{}{}{} of block #1\ma@stop} diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index a1591d4d5..081696291 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -1,7 +1,7 @@ \documentclass[8pt,twocolumn,a4paper]{extarticle} \usepackage[margin=2cm]{geometry} -\usepackage[bookmarks=false,ps2pdf]{hyperref} +\usepackage[pdfborder={0 0 0},bookmarks=false,ps2pdf]{hyperref} \usepackage[american]{babel} \usepackage{matex} \usepackage{legacy_1}