--- /dev/null
+EXEC = matex
+VERSION=0.1.0
+
+REQUIRES = helm-ng_library
+
+include ../Makefile.common
+
+REGISTRY = $(RT_BASE_DIR)/matita.conf.xml
+
+OBJ = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con
+
+test:
+ @echo MaTeX $(OBJ)
+ $(H)./matex.native -O test $(REGISTRY) $(OBJ)
+
+.PHONY: test
--- /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
+
+type item = Free of string (* free text *)
+ | Macro of string (* macro *)
+ | Group of text (* group *)
+
+and text = item list (* structured text *)
+
+let file_ext = ".tex"
+
+let empty = [Free ""]
+
+let newline = [Free "%\n"]
+
+let arg s = Group [Free s]
+
+let mk_rev_args riss =
+ L.rev_map (fun t -> Group t) (empty :: riss)
+
--- /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 P = Printf
+module S = String
+
+module T = TeX
+
+(* internal functions *******************************************************)
+
+let special = "_"
+
+let quote c =
+ if S.contains special c then '.' else c
+
+let rec out_item och = function
+ | T.Free s -> P.fprintf och "%s" (S.map quote s)
+ | T.Macro s -> P.fprintf och "\\%s" s
+ | T.Group t -> P.fprintf och "%%\n{%a}" out_text t
+
+(* interface functions ******************************************************)
+
+and out_text och t =
+ L.iter (out_item och) t
--- /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_______________________________________________________________ *)
+
+val out_text: out_channel -> TeX.text -> unit
--- /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 F = Filename
+module L = List
+module S = String
+
+module U = NUri
+module R = NReference
+module C = NCic
+module P = NCicPp
+module E = NCicEnvironment
+
+module G = Options
+module T = TeX
+module O = TeXOutput
+
+let status = new P.status
+
+(* internal functions *******************************************************)
+
+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 segments_of_uri u =
+ let s = U.string_of_uri u in
+ let s = F.chop_extension s in
+ let l = S.length s in
+ let i = S.index s ':' in
+ let s = S.sub s (i+2) (l-i-2) in
+ segments_of_string [] (l-i-2) s
+
+let rec mk_string sep r = function
+ | [] -> r
+ | s :: ss -> mk_string sep (s ^ sep ^ r) ss
+
+let alpha c s = s
+
+let malformed s =
+ failwith ("MaTeX: malformed term: " ^ s)
+
+let not_supported () =
+ failwith "MaTeX: object not supported"
+
+let proc_sort = function
+ | C.Prop -> [T.Macro "Prop"]
+ | C.Type [`Type, u] -> [T.Macro "Type"; T.arg (U.string_of_uri u)]
+ | C.Type [`CProp, u] -> [T.Macro "Crop"; T.arg (U.string_of_uri u)]
+ | C.Type _ -> malformed "1"
+
+let proc_gref r = T.Macro "GRef"
+
+let rec proc_term c = function
+ | C.Appl []
+ | C.Meta _
+ | C.Implicit _ -> malformed "2"
+ | C.Rel m ->
+ let name = L.nth c (m-1) in
+ [T.Macro "LRef"; T.arg name]
+ | C.Appl ts ->
+ let riss = L.rev_map (proc_term c) ts in
+ T.Macro "Appl" :: T.mk_rev_args riss
+ | C.Prod (s, w, t) ->
+ let s = alpha c s in
+ let is_w = proc_term c w in
+ let is_t = proc_term (s::c) t in
+ T.Macro "Prod" :: T.arg s :: T.Group is_w :: is_t
+ | C.Lambda (s, w, t) ->
+ let s = alpha c s in
+ let is_w = proc_term c w in
+ let is_t = proc_term (s::c) t in
+ T.Macro "Abst" :: T.arg s :: T.Group is_w :: is_t
+ | C.LetIn (s, w, v, t) ->
+ let s = alpha c s in
+ let is_w = proc_term c w in
+ let is_v = proc_term c v in
+ let is_t = proc_term (s::c) t in
+ T.Macro "Abbr" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
+ | C.Sort s ->
+ proc_sort s
+ | C.Const r ->
+ [proc_gref r]
+ | C.Match (w, u, v, ts) ->
+ let is_w = [proc_gref 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
+ T.Macro "Case" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss
+
+let proc_term c t = try proc_term c t with
+ | E.ObjectNotFound _
+ | Failure "nth"
+ | Invalid_argument "List.nth" -> malformed "3"
+
+let open_out_tex s =
+ open_out (F.concat !G.out_dir (s ^ T.file_ext))
+
+let proc_obj u =
+ let ss = segments_of_uri u in
+ let _, _, _, _, obj = E.get_checked_obj status u in
+ match obj with
+ | C.Constant (_, _, None, u, _) -> not_supported ()
+ | C.Constant (_, _, Some t, u, _) ->
+ let name = mk_string "." "body" ss in
+ let och = open_out_tex name in
+ O.out_text och (proc_term [] t);
+ O.out_text och T.newline;
+ close_out och;
+ let name = mk_string "." "type" ss in
+ let och = open_out_tex name in
+ O.out_text och (proc_term [] u);
+ O.out_text och T.newline;
+ close_out och
+ | C.Fixpoint (_, _, _) -> not_supported ()
+ | C.Inductive (_, _, _, _) -> not_supported ()
+
+(* interface functions ******************************************************)
+
+let process = proc_obj
--- /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_______________________________________________________________ *)
+
+val process: NUri.uri -> unit
--- /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 A = Arg
+module F = Filename
+
+module U = NUri
+module R = Helm_registry
+module L = Librarian
+module B = NCicLibrary
+module C = NCicTypeChecker
+module H = HLog
+
+module G = Options
+module E = Engine
+module O = TeXOutput
+
+let help_O = "<dir> Set this output directory"
+let help_X = " Clear configuration and options"
+
+let help = ""
+
+(* internal functions *******************************************************)
+
+let trusted _ = true
+
+let no_log _ _ = ()
+
+let init registry =
+ R.load_from registry;
+ if !G.no_init then begin
+ B.init ();
+ C.set_trust trusted;
+ H.set_log_callback no_log;
+ G.no_init := false;
+ end
+
+let is_registry s =
+ F.check_suffix s ".conf.xml"
+
+let no_init () =
+ failwith "MaTeX: registry not initialized"
+
+let malformed s =
+ failwith ("MaTeX: malformed argument: " ^ s)
+
+let process s =
+ if is_registry s then init s
+ else if !G.no_init then no_init ()
+ else if L.is_uri s then E.process (U.uri_of_string s)
+ else malformed s
+
+let main =
+ A.parse [
+ "-O", A.String ((:=) G.out_dir), help_O;
+ "-X", A.Unit G.clear, help_X;
+ ] process help
--- /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 F = Filename
+
+module R = Helm_registry
+
+(* internal *****************************************************************)
+
+let default_no_init = true
+
+let default_out_dir = F.current_dir_name
+
+(* interface ****************************************************************)
+
+let no_init = ref default_no_init
+
+let out_dir = ref default_out_dir
+
+let clear () =
+ R.clear ();
+ no_init := default_no_init;
+ out_dir := default_out_dir
--- /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_______________________________________________________________ *)
+
+val no_init: bool ref
+
+val out_dir: string ref
+
+val clear: unit -> unit
--- /dev/null
+\newcommand*\Next[1]{\def\TMP{#1}\ifx\TMP\empty\let\next=\relax\else\ #1\let\next=\Next\fi\next}
+
+\newcommand*\Prop{PROP}
+\newcommand*\Crop[1]{CROP}
+\newcommand*\Type[1]{TYPE}
+\newcommand*\LRef[1]{(L #1)}
+\newcommand*\GRef{G}
+\newcommand*\Abbr[3]{(D #1 #2 #3) }
+\newcommand*\Abst[2]{(I #1 #2) }
+\newcommand*\Prod[2]{(P #1 #2) }
+\newcommand*\Appl{(A)\Next}
+\newcommand*\Case[3]{(C #1 #2 #3)\Next}
--- /dev/null
+\documentclass{article}
+
+\usepackage{matex}
+
+\begin{document}
+
+\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
+
+\end{document}
projects / helm.git / commitdiff