module U = NUri
module C = NCic
-module R = NReference
module E = NCicEnvironment
module T = NCicTypeChecker
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
(* interface functions ******************************************************)
let process_top_term s t = proc_named_term s (init ()) t
-
module T = TeX
module O = TeXOutput
module A = Anticipate
+module M = Meta
module N = Alpha
type status = {
--- /dev/null
+(*
+ ||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
let default_macro = []
+let default_sigs = []
+
(* interface ****************************************************************)
let dno_id = "_" (* identifier for not-occurring premises *)
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
alpha_type := default_alpha;
alpha_sort := default_alpha;
alpha_gref := default_alpha;
- macro_gref := default_macro
+ macro_gref := default_macro;
+ sigs_gref := default_sigs
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
\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{}
\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}
\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}
\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}
\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}
projects / helm.git / commitdiff