include ../Makefile.common
PROBE = ../probe/probe.native
-REGISTRY = $(RT_BASE_DIR)/matita.conf.xml
+REGISTRY = $(RT_BASE_DIR)/matita.conf.xml test/basic_1.conf.xml
OBJS = Make.objs
+SRCS = Make.srcs
BASEURI = cic:/matita/lambdadelta/basic_1/
-test: test/$(OBJS)
+test: test/$(SRCS)
-$(OBJS):
+test/$(OBJS): $(REGISTRY)
@echo probe: $(BASEURI)
$(H)$(PROBE) $(REGISTRY) -g $(BASEURI) -os > $@
-test/$(OBJS): $(OBJS) ./matex.native
- @echo MaTeX: processing $(OBJS)
- $(H)./matex.native -O test -l $(OBJS) -t -p $(REGISTRY) `cat $<`
+test/$(SRCS): test/$(OBJS) $(REGISTRY) ./matex.native
+ @echo MaTeX: processing $<
+ $(H)./matex.native -O test -l $(SRCS) -p -a $(REGISTRY) `cat $<`
.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
+module P = Printf
+module S = Scanf
+module N = String
+
+module U = NUri
+module C = NCic
+module R = NReference
+module E = NCicEnvironment
+module T = NCicTypeChecker
+
+module X = Ground
+module G = Options
+module K = Kernel
+
+let dno = "_" (* does not occur *)
+
+let nan = -1 (* not a number *)
+
+(* internal functions *******************************************************)
+
+let malformed s =
+ X.error ("alpha: malformed term: " ^ s)
+
+let ok s =
+ X.log ("alpha: ok " ^ s)
+
+let rec trim r =
+ let r1, r2 = S.sscanf r "%s@_%s" X.id2 in
+ if r2 = "" then r1 else trim r1
+
+let split s =
+ let rec aux i l =
+ let j = pred i in
+ if j >=0 && s.[j] >= '0' && s.[j] <= '9' then aux j (succ l) else i, l
+ in
+ let i, l = aux (N.length s) 0 in
+ let s1, s2 = N.sub s 0 i, N.sub s i l in
+ let s1 = if s1 = "" then "_" else s1 in
+ s1, if l = 0 then nan else int_of_string s2
+
+let rec strip = function
+ | C.Appl (t :: _)
+ | C.Prod (_, _, t) -> strip t
+ | t -> t
+
+let get_constant c t = match strip (K.whd c t) with
+ | C.Sort (C.Prop) ->
+ P.sprintf "Prop"
+ | C.Sort (C.Type [`Type, u]) ->
+ P.sprintf "Type[%s]" (U.string_of_uri u)
+ | C.Sort (C.Type [`CProp, u]) ->
+ P.sprintf "CProp[%s]" (U.string_of_uri u)
+ | C.Const (R.Ref (u, r)) ->
+ let ss = K.segments_of_uri u in
+ let _, _, _, _, obj = E.get_checked_obj G.status u in
+ let ss, _ = K.name_of_reference ss (obj, r) in
+ X.rev_map_concat X.id "." "type" ss
+ | _ -> ""
+
+let read l s r =
+ let rec aux = function
+ | [] -> ""
+ | (a, b, c) :: tl ->
+ if s = a && (r = b || r = c) then c else aux tl
+ in
+ aux l
+
+let type_check r c w =
+ let s0 = get_constant c w in
+ let r0 = read !G.alpha_type s0 r in
+ if r0 <> "" then r0 else
+ let s1 = get_constant c (K.typeof c w) in
+ let r0 = read !G.alpha_sort s1 r in
+ if r0 <> "" then r0 else begin
+ if !G.log_alpha then
+ X.log (P.sprintf "alpha: not found %s: type \"%s\" sort \"%s\"" r s0 s1);
+ r
+ end
+
+let rec get r = function
+ | [] -> r
+ | (h, d) :: tl ->
+ if fst r = h && snd r <= d then h, succ d else get r tl
+
+let alpha d c s w t =
+ if K.does_not_occur K.fst_var c t then dno, nan else
+ let r, i = split (trim s) in
+ get (type_check r c w, i) d
+
+let mk_name (s, i) =
+ if i < 0 then s else P.sprintf "%s%u" s i
+
+let add_name r d = r :: d
+
+let rec proc_term d c t = match t with
+ | C.Meta _
+ | C.Implicit _
+ | C.Sort _
+ | C.Rel _
+ | C.Const _ -> t
+ | C.Appl ts ->
+ let tts = proc_terms d c ts in
+ K.appl tts
+ | C.Match (w, u, v, ts) ->
+ let uu = proc_term d c u in
+ let vv = proc_term d c v in
+ let tts = proc_terms d c ts in
+ K.case w uu vv tts
+ | C.Prod (s, w, t) ->
+ let rr = alpha d c s w t in
+ let ss = mk_name rr in
+ let ww = proc_term d c w in
+ let tt = proc_term (add_name rr d) (K.add_dec ss w c) t in
+ K.prod ss ww tt
+ | C.Lambda (s, w, t) ->
+ let rr = alpha d c s w t in
+ let ss = mk_name rr in
+ let ww = proc_term d c w in
+ let tt = proc_term (add_name rr d) (K.add_dec ss w c) t in
+ K.lambda ss ww tt
+ | C.LetIn (s, w, v, t) ->
+ let rr = alpha d c s w t in
+ let ss = mk_name rr in
+ let ww = proc_term d c w in
+ let vv = proc_term d c v in
+ let tt = proc_term (add_name rr d) (K.add_def ss w v c) t in
+ K.letin ss ww vv tt
+
+and proc_terms d c ts =
+ let rtts = L.rev_map (proc_term d c) ts in
+ L.rev rtts
+
+let proc_named_term s d c t =
+try
+ let tt = proc_term d c t in
+ if !G.test then begin
+ let _ = K.typeof c tt in
+ ok s
+ end;
+ tt
+with
+ | T.TypeCheckerFailure s
+ | T.AssertFailure s -> malformed (Lazy.force s)
+
+(* interface functions ******************************************************)
+
+let process_top_term s t = proc_named_term s [] [] 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 process_top_term: string -> NCic.term -> NCic.term
let ok s =
X.log ("anticipate: ok " ^ s)
-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"
-
-let not_prop2 c t = not_prop1 c (K.typeof c t)
-
let anticipate c v =
incr fresh;
let w = K.typeof c v in
let proc_arg c i (d, rtts) t = match d with
| Some _ -> d, (t :: rtts)
| None ->
- if K.is_atomic t || not_prop2 c t then d, (t :: rtts) else
+ if K.is_atomic t || K.not_prop2 c t then d, (t :: rtts) else
let s, w, v, tt = anticipate c t in
Some (i, s, w, v), (tt :: rtts)
let tt = shift_term (K.add_dec s w c) t in
[], K.lambda s w tt
| C.LetIn (s, w, v, t) ->
- if not_prop1 c w then
+ if K.not_prop1 c w then
let dt, tt = proc_term (K.add_def s w v c) t in
dt @ K.add_def s w v [], tt
else
let dt, tt = proc_term (K.add_def s w vv c) t in
dt @ (K.add_def s w vv dv), tt
| C.Appl [t] -> proc_term c t
- | C.Appl (C.Appl ts :: vs) -> proc_term c (C.Appl (ts @ vs))
+ | C.Appl (C.Appl ts :: vs) -> proc_term c (K.appl (ts @ vs))
| C.Appl ts -> proc_appl c t ts
| C.Match (w, u, v, ts) -> proc_case c t w u v ts
| Some (i, s, w, v), rtts ->
let ri = L.length rtts - i in
let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
- proc_term c (K.letin s w v (C.Appl tts))
+ proc_term c (K.letin s w v (K.appl tts))
and proc_case c t w u v ts = match X.foldi_left (proc_arg c) 1 initial ts with
| None , _ ->
- if K.is_atomic v || not_prop1 c (C.Const w) then [], t else
+ if K.is_atomic v || K.not_prop1 c (C.Const w) then [], t else
let s, w0, v0, vv = anticipate c v in
let u = K.lift K.fst_var 1 u in
let ts = K.lifts K.fst_var 1 ts in
let d, tt = proc_term c t in
K.shift tt d
-let shift_named s c t =
+let shift_named_term s c t =
try
fresh := 0;
let tt = shift_term c t in
let proc_fun c =
let r, s, i, u, t = c in
- if not_prop1 [] u then c else
- r, s, i, u, shift_named s [] t
+ if K.not_prop1 [] u then c else
+ r, s, i, u, shift_named_term s [] t
let proc_obj obj = match obj with
| C.Inductive _
| C.Constant (_, _, None, _, _) -> obj
| C.Constant (r, s, Some t, u, a) ->
- if not_prop1 [] u then obj else
- let tt = shift_named s [] t in
+ if K.not_prop1 [] u then obj else
+ let tt = shift_named_term s [] t in
C.Constant (r, s, Some tt, u, a)
| C.Fixpoint (b, cs, a) ->
C.Fixpoint (b, L.map proc_fun cs, a)
(* interface functions ******************************************************)
-(* not_prop1 *)
-
-(* not_prop2 *)
-
-let process_top_term s t = shift_named s [] t
+let process_top_term s t = shift_named_term s [] t
let process_obj obj = proc_obj obj
\ / 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
-
val process_top_term: string -> NCic.term -> NCic.term
val process_obj: NCic.obj_kind -> NCic.obj_kind
module T = TeX
module O = TeXOutput
module A = Anticipate
+module N = Alpha
type status = {
n: string; (* reference name *)
let typeof c = function
| C.Appl [t]
- | t -> A.typeof c t
+ | t -> K.whd_typeof c t
let init () = {
n = ""; s = [1]
let ris = mk_open st ris in
proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t
| C.Appl (t0 :: ts) ->
- let rts = X.rev_neg_filter (A.not_prop2 c) [t0] ts in
+ let rts = X.rev_neg_filter (K.not_prop2 c) [t0] ts in
let ris = T.Macro "STEP" :: mk_inferred st c t ris in
let tts = L.rev_map (proc_term [] c) rts in
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 rts = X.rev_neg_filter (K.not_prop2 c) [v] ts in
let ris = T.Macro "DEST" :: mk_inferred st c t ris in
let tts = L.rev_map (proc_term [] c) rts in
mk_exit st (T.rev_mk_args tts ris)
| C.LetIn (s, w, v, t) ->
let is_w = proc_term [] c w in
let ris = mk_open st ris in
- if A.not_prop1 c w then
+ if K.not_prop1 c w then
let is_v = proc_term [] c v in
let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in
proc_proof (next st) ris (K.add_def s w v c) t
let note = T.Note "This file was automatically generated by MaTeX: do not edit"
-let proc_item item s t =
+let proc_item item s ss t =
+ let tt = N.process_top_term s t in (* alpha-conversion *)
let is = [T.Macro "end"; T.arg item] in
- note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t
+ note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term is [] tt
-let proc_top_proof s t =
- let tt = A.process_top_term s t in (* anticipation *)
- let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
+let proc_top_proof s ss t =
+ let t0 = A.process_top_term s t in (* anticipation *)
+ let tt = N.process_top_term s t0 in (* alpha-conversion *)
+ let ris = [T.free ss; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt)
let open_out_tex s =
| None ->
let name = X.rev_map_concat X.id "." "type" ss in
let och = open_out_tex name in
- O.out_text och (proc_item "axiom" s u);
+ O.out_text och (proc_item "axiom" s name u);
close_out och
| Some t ->
let text_u, text_t =
- if A.not_prop1 [] u then proc_item "declaration", proc_item "definition"
+ if K.not_prop1 [] u then proc_item "declaration", proc_item "definition"
else proc_item "proposition", proc_top_proof
in
let name = X.rev_map_concat X.id "." "type" ss in
let och = open_out_tex name in
- O.out_text och (text_u s u);
+ O.out_text och (text_u s name u);
close_out och;
let name = X.rev_map_concat X.id "." "body" ss in
let och = open_out_tex name in
- O.out_text och (text_t s t);
+ O.out_text och (text_t s name t);
close_out och
let proc_fun ss (r, s, i, u, t) =
let id x = x
+let id2 x y = x, y
+
let rec segments_of_string ss l s =
match try Some (S.index s '/') with Not_found -> None with
| None -> s :: ss
val id: 'a -> 'a
+val id2: 'a -> 'b -> 'a * 'b
+
val segments_of_string: string list -> int -> string -> string list
val rev_map_concat: ('a -> string) -> string -> string -> 'a list -> string
H.set_log_callback no_log;
let u0 = mk_type_universe "0" in
let u1 = mk_type_universe "1" in
- E.add_lt_constraint u0 u1
+ E.add_lt_constraint ~acyclic:true u0 u1
let fst_var = 1
let snd_var = 2
+let appl ts = C.Appl ts
+
+let prod s w t = C.Prod (s, w, t)
+
let lambda s w t = C.Lambda (s, w, t)
let letin s w v t = C.LetIn (s, w, v, t)
let typeof c t =
K.typeof G.status [] [] c t
+let whd_typeof c t = whd c (typeof c t)
+
+let not_prop1 c u = match whd_typeof c u with
+ | C.Sort (C.Prop) -> false
+ | _ -> true
+
+let not_prop2 c t = not_prop1 c (typeof c t)
+
+let does_not_occur i c t =
+ K.does_not_occur G.status ~subst:[] c 0 i t
+
let segments_of_uri u =
let s = U.string_of_uri u in
let s = F.chop_extension s in
let help_O = "<dir> Set this output directory"
let help_X = " Clear configuration and options"
+let help_a = " Log alpha-unconverted identifiers (default: no)"
let help_l = "<file> Output the list of generated files in this file"
let help_p = " omit types (default: no)"
-let help_t = " Test anticipation (default: no)"
+let help_t = " Test term transformations (default: no)"
let help = ""
(* internal functions *******************************************************)
+let alpha_decode = R.triple R.string R.string R.string
+
let init registry =
R.load_from registry;
if !G.no_init then begin
K.init ();
G.no_init := false;
- end
+ end;
+ G.alpha_type := R.get_list alpha_decode "matex.alpha.type";
+ G.alpha_sort := R.get_list alpha_decode "matex.alpha.sort"
let is_registry s =
F.check_suffix s ".conf.xml"
A.parse [
"-O", A.String ((:=) G.out_dir), help_O;
"-X", A.Unit G.clear, help_X;
+ "-a", A.Set G.log_alpha, help_a;
"-l", A.String set_list, help_l;
"-p", A.Set G.no_types, help_p;
"-t", A.Set G.test, help_t;
let default_no_types = false
+let default_log_alpha = false
+
let default_list_och = None
+let default_alpha = []
+
(* interface ****************************************************************)
let status = new P.status
let no_init = ref default_no_init
-let out_dir = ref default_out_dir (* directory of generated files *)
+let out_dir = ref default_out_dir (* directory of generated files *)
+
+let proc_id = ref default_proc_id (* identifer of anticipations *)
+
+let test = ref default_test (* test anticipation *)
+
+let no_types = ref default_no_types (* omit types *)
-let proc_id = ref default_proc_id (* identifer of anticipations *)
+let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *)
-let test = ref default_test (* test anticipation *)
+let list_och = ref default_list_och (* output stream for list file *)
-let no_types = ref default_no_types (* omit types *)
+let alpha_type = ref default_alpha (* data of type-based alpha-conversion *)
-let list_och = ref default_list_och (* output stream for list file *)
+let alpha_sort = ref default_alpha (* data of sort-based alpha-conversion *)
let close_list () = match !list_och with
| None -> ()
proc_id := default_proc_id;
test := default_test;
no_types := default_no_types;
- list_och := default_list_och
+ log_alpha := default_log_alpha;
+ list_och := default_list_och;
+ alpha_type := default_alpha;
+ alpha_sort := default_alpha
val no_types: bool ref
+val log_alpha: bool ref
+
val list_och: out_channel option ref
+val alpha_type: (string * string * string) list ref
+
+val alpha_sort: (string * string * string) list ref
+
val clear: unit -> unit
val close_list: unit -> unit
MAIN = test
-SOURCES = $(shell cat Make) $(shell cat Make.objs)
+SOURCES = $(shell cat Make) $(shell cat Make.srcs)
all: $(MAIN).dvi
$(UNLOG) $< $@
objs.tex:
- @sed "s/\(.*\).tex/\\\\input{\1}/" Make.objs > $@
+ @sed "s/\(.*\).tex/\\\\input{\1}/" Make.srcs > $@
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="matex.alpha">
+ <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type b I</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type ee I</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type x I</key>
+
+ <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type ee I</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type f I</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type x I</key>
+
+ <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type e I</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type ee I</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type k I</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type h I</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type x I</key>
+
+ <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type _ X</key>
+ <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type a X</key>
+ <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type c L</key>
+ <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type d L</key>
+ <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type e K</key>
+ <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type ee X</key>
+ <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type x X</key>
+ <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type y Y</key>
+
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type _ X</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type e X</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type ee X</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type t T</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type u U</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type v V</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type w W</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type wi W</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type x X</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type y Y</key>
+ <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type z Z</key>
+
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type _ Xs</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type e Xs</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ee Xs</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type t Ts</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ts Ts</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ul Us</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type us Us</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type vs Vs</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ws Ws</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type xs Xs</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type x Xs</key>
+ <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type y Ys</key>
+
+ <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type _ X</key>
+ <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type a A</key>
+ <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type b B</key>
+ <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type e X</key>
+ <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type ee X</key>
+ <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type l X</key>
+ <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type x X</key>
+ <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type y Y</key>
+
+ <key name="type">matita.lambdadelta.basic_1.G.defs.G.G.type g h</key>
+
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type _ x</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d' d</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d d</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type e e</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type ee e</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type f f</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type g g</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type h h</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type i i</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type j j</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type k k</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type l l</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type m m</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type n n</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type next f</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type v v</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type w w</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type x x</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type y y</key>
+
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.bool.bool.type b b</key>
+ <key name="type">matita.lambdadelta.legacy_1.coq.defs.bool.bool.type x x</key>
+
+ <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type _ f</key>
+ <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type e f</key>
+ <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type ee f</key>
+ <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type hds f</key>
+ <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type is f</key>
+ <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type p f</key>
+ <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type q f</key>
+ <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type y f</key>
+
+ <key name="type">Prop P R</key>
+ <key name="type">Prop Q R</key>
+
+ <key name="type">Type[cic:/matita/pts/Type0.univ] P S</key>
+
+ <key name="sort">Prop H H</key>
+ <key name="sort">Prop Hle H</key>
+ <key name="sort">Prop IH IH</key>
+ <key name="sort">Prop IHc IH</key>
+ <key name="sort">Prop IHd IH</key>
+ <key name="sort">Prop IHe IH</key>
+ <key name="sort">Prop IHh IH</key>
+ <key name="sort">Prop IHi IH</key>
+ <key name="sort">Prop IHj IH</key>
+ <key name="sort">Prop IHn IH</key>
+ <key name="sort">Prop IHx IH</key>
+ <key name="sort">Prop a H</key>
+ <key name="sort">Prop c H</key>
+ <key name="sort">Prop d H</key>
+ <key name="sort">Prop e H</key>
+ <key name="sort">Prop f H</key>
+ <key name="sort">Prop g H</key>
+ <key name="sort">Prop h H</key>
+ <key name="sort">Prop i H</key>
+ <key name="sort">Prop l H</key>
+ <key name="sort">Prop n H</key>
+ <key name="sort">Prop p H</key>
+ <key name="sort">Prop s H</key>
+ <key name="sort">Prop t H</key>
+ <key name="sort">Prop w H</key>
+ <key name="sort">Prop x H</key>
+
+ <key name="sort">Type[cic:/matita/pts/Type0.univ] f a</key>
+ </section>
+</helm_registry>
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/02/21 MaTeX Package]
+\ProvidesPackage{matex}[2016/04/28 MaTeX Package]
\RequirePackage{xcolor}
\ExecuteOptions{}
\ProcessOptions*
\newcommand*\ma@prim{ma@purple}
\newcommand*\ma@qed{ma@blue}
-\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
\newcommand*\neverindent{\setlength\parindent{0pt}}
-\newcommand*\ObjLabel[1]{\label{obj:#1}}
-\newcommand*\ObjRef[1]{\ref{obj:#1}}
+%\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
+%\newcommand*\ObjLabel[1]{\label{obj:#1}\hypertarget{obj:#1}{}}
+%\newcommand*\ObjRef[1]{\hyperlink{obj:#1}{\ref*{obj:#1}}}
+%\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}
+
+\newcommand*\ma@settarget[2]{\hypertarget{obj:#2}{}}
+\newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}}
+
\newcommand*\ObjIncNode{}
\newcommand*\ObjNode{}
-\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}
\newcommand*\ma@thehead[2]{\ObjIncNode\textbf{#1 \ObjNode(#2)}\neverindent\par}
\newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par}
-\newenvironment{axiom}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Axiom}{#1}}{\par}
-\newenvironment{declaration}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Declaration}{#1}}{\par}
+\newenvironment{axiom}[2]{\ma@settarget{#1}{#2}\ma@thehead{Axiom}{#1}}{\par}
+\newenvironment{declaration}[2]{\ma@settarget{#1}{#2}\ma@thehead{Declaration}{#1}}{\par}
\newenvironment{definition}[2]{}{\par}
-\newenvironment{proposition}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Proposition}{#1}}{\par}
+\newenvironment{proposition}[2]{\ma@settarget{#1}{#2}\ma@thehead{Proposition}{#1}}{\par}
\newenvironment{proof}[2]{\ma@theneck{Proof}}{\par}
\newenvironment{ma@step}[1]{\color{#1}}{\par}
\newcommand*\CROP[1]{CROP}
\newcommand*\TYPE[1]{TYPE}
\newcommand*\LREF[2]{#1}
-\newcommand*\GREF[2]{#1}
+\newcommand*\GREF[2]{\ma@setlink{#1}{#2}}
\newcommand*\ABBR[3]{(D #1 #2 #3) }
\newcommand*\ABST[2]{(I #1 #2) }
\newcommand*\PROD[2]{(P #1 #2) }
\input{objs}
-\bigskip
-
-\ObjRef{pr0}
-\ObjRef{pr0_ind}
-\ObjRef{pr0_confluence}
-
\end{document}
| [fst; snd] -> fst_unmarshaller fst, snd_unmarshaller snd
| _ -> raise (Type_error "not a pair")
+(* FG *)
+let triple fst_unmarshaller snd_unmarshaller trd_unmarshaller v =
+ match Str.split spaces_rex v with
+ | [fst; snd; trd] -> fst_unmarshaller fst, snd_unmarshaller snd, trd_unmarshaller trd
+ | _ -> raise (Type_error "not a triple")
+
(* escapes for xml configuration file *)
let (escape, unescape) =
let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in
let get_pair registry fst_unmarshaller snd_unmarshaller =
get_typed registry (pair fst_unmarshaller snd_unmarshaller)
+(* FG *)
+let get_triple registry fst_unmarshaller snd_unmarshaller trd_unmarshaller =
+ get_typed registry (triple fst_unmarshaller snd_unmarshaller trd_unmarshaller)
+
let set_list registry marshaller ~key ~value =
(* since ocaml hash table are crazy... *)
while Hashtbl.mem registry key do
let get_opt_default unmarshaller = get_opt_default default_registry unmarshaller
let get_list unmarshaller = get_list default_registry unmarshaller
let get_pair unmarshaller = get_pair default_registry unmarshaller
+let get_triple unmarshaller = get_triple default_registry unmarshaller
let set_typed marshaller = set_typed default_registry marshaller
let set_opt unmarshaller = set_opt default_registry unmarshaller
let set_list marshaller = set_list default_registry marshaller
val float: string -> float
val bool: string -> bool
val pair: (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b
+val triple: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> string -> 'a * 'b * 'c
(** {3 Typed getters} *)
(** decode values which are blank separated list of values, of length 2 *)
val get_pair: (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b
+ (** decode values which are blank separated list of values, of length 3 *)
+val get_triple: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> string -> 'a * 'b * 'c
+
(** {4 Shorthands} *)
val get_string: string -> string
projects / helm.git / commitdiff