OBJS = Make.objs
SRCS = Make.srcs
-BASEURI = cic:/matita/lambdadelta/basic_1/
+DEVEL = ../../../matita/contribs/lambdadelta/basic_1/
test: test/$(SRCS)
test/$(OBJS): $(REGISTRY)
- @echo probe: $(BASEURI)
- $(H)$(PROBE) $(REGISTRY) -g $(BASEURI) -os > $@
+ @echo probe: $(DEVEL)
+ $(H)$(PROBE) $(REGISTRY) -g $(DEVEL) -os > $@
test/$(SRCS): test/$(OBJS) $(REGISTRY) ./matex.native
@echo MaTeX: processing $<
- $(H)./matex.native -O test -l $(SRCS) -p -a $(REGISTRY) `cat $<`
+ $(H)./matex.native -O test -l $(SRCS) -p -g -a $(REGISTRY) `cat $<`
.PHONY: test
module P = Printf
module S = Scanf
module N = String
+module H = Hashtbl
module U = NUri
module C = NCic
module G = Options
module K = Kernel
-let dno = "_" (* does not occur *)
+type global = (string, int) H.t
-let nan = -1 (* not a number *)
+type local = (string * int) list
+
+type status = {
+ g: global; (* global context for alpha-conversion *)
+ d: local; (* local context for alpha-conversion *)
+ c: C.context; (* local context for kernel calls *)
+}
(* internal functions *******************************************************)
let ok s =
X.log ("alpha: ok " ^ s)
+let init () = {
+ g = H.create 11; d = []; c = [];
+}
+
let rec trim r =
let r1, r2 = S.sscanf r "%s@_%s" X.id2 in
if r2 = "" then r1 else trim r1
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
+ s1, if l = 0 then G.nan else int_of_string s2
let rec strip = function
| C.Appl (t :: _)
| (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 local_alpha st s w t =
+ if K.does_not_occur K.fst_var st.c t then G.dno_id, G.nan else
+ let r, i = split (trim s) in
+ get (type_check r st.c w, i) st.d
+
+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
+with Not_found ->
+ H.add st.g s 0;
+ s
+
+let alpha st s w t =
+ let r = local_alpha st s w t in
+ let s = mk_name r in
+ r, if G.is_global_id s then global_apha st s else s
+
let add_name r d = r :: d
-let rec proc_term d c t = match t with
+let rec proc_term st 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
+ let tts = proc_terms st 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
+ let uu = proc_term st u in
+ let vv = proc_term st v in
+ let tts = proc_terms st 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
+ let rr, ss = alpha st s w t in
+ let ww = proc_term st w in
+ let tt = proc_term {st with d=add_name rr st.d; c=K.add_dec ss w st.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
+ let rr, ss = alpha st s w t in
+ let ww = proc_term st w in
+ let tt = proc_term {st with d=add_name rr st.d; c=K.add_dec ss w st.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
+ let rr, ss = alpha st s w t in
+ let ww = proc_term st w in
+ let vv = proc_term st v in
+ let tt = proc_term {st with d=add_name rr st.d; c=K.add_def ss w v st.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
+and proc_terms st ts =
+ let rtts = L.rev_map (proc_term st) ts in
L.rev rtts
-let proc_named_term s d c t =
+let proc_named_term s st t =
try
- let tt = proc_term d c t in
+ let tt = proc_term st t in
if !G.test then begin
- let _ = K.typeof c tt in
+ let _ = K.typeof st.c tt in
ok s
end;
tt
(* interface functions ******************************************************)
-let process_top_term s t = proc_named_term s [] [] t
+let process_top_term s t = proc_named_term s (init ()) t
+
module N = Alpha
type status = {
+ i: string; (* item name *)
n: string; (* reference name *)
s: int list; (* scope *)
+ c: C.context (* context for kernel calls *)
}
(* internal functions *******************************************************)
(* generic term processing *)
-let proc_sort is = function
+let mk_ptr st name =
+ if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
+
+let proc_sort st is = function
| C.Prop -> T.Macro "PROP" :: is
| C.Type [`Type, u] -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
| C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
| C.Type _ -> malformed "T1"
-let rec proc_term is c = function
+let rec proc_term st is = function
| C.Appl []
| C.Meta _
| C.Implicit _ -> malformed "T2"
| C.Rel m ->
- let name = K.resolve_lref c m in
- T.Macro "LREF" :: T.arg name :: T.free name :: is
+ let name = K.resolve_lref st.c m in
+ T.Macro "LREF" :: T.arg name :: T.free (mk_ptr st name) :: is
| C.Appl ts ->
- let riss = L.rev_map (proc_term [] c) ts in
+ let riss = L.rev_map (proc_term st []) ts in
T.Macro "APPL" :: T.mk_rev_args riss is
| C.Prod (s, w, t) ->
- let is_w = proc_term [] c w in
- let is_t = proc_term is (K.add_dec s w c) t in
- T.Macro "PROD" :: T.arg s :: T.Group is_w :: is_t
+ let is_w = proc_term st [] w in
+ let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
+ T.Macro "PROD" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
| C.Lambda (s, w, t) ->
- let is_w = proc_term [] c w in
- let is_t = proc_term is (K.add_dec s w c) t in
- T.Macro "ABST" :: T.arg s :: T.Group is_w :: is_t
+ let is_w = proc_term st [] w in
+ let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
+ T.Macro "ABST" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
| C.LetIn (s, w, v, t) ->
- let is_w = proc_term [] c w in
- let is_v = proc_term [] c v in
- let is_t = proc_term is (K.add_def s w v c) t in
- T.Macro "ABBR" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
+ let is_w = proc_term st [] w in
+ let is_v = proc_term st [] v in
+ let is_t = proc_term {st with c=K.add_def s w v st.c} is t in
+ T.Macro "ABBR" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
| C.Sort s ->
- proc_sort is s
+ proc_sort st is s
| 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, name = K.name_of_reference ss (obj, r) in
T.Macro "GREF" :: T.arg name :: T.free (X.rev_map_concat X.id "." "type" ss) :: is
| C.Match (w, u, v, ts) ->
- let is_w = proc_term [] c (C.Const 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
+ let is_w = proc_term st [] (C.Const w) in
+ let is_u = proc_term st [] u in
+ let is_v = proc_term st [] v in
+ let riss = L.rev_map (proc_term st []) ts in
T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
-let proc_term is c t = try proc_term is c t with
+let proc_term st is t = try proc_term st is t with
| E.ObjectNotFound _
| Invalid_argument "List.nth"
| Failure "nth"
(* proof processing *)
-let typeof c = function
+let typeof st = function
| C.Appl [t]
- | t -> K.whd_typeof c t
+ | t -> K.whd_typeof st.c t
-let init () = {
- n = ""; s = [1]
+let init i = {
+ i = i;
+ n = ""; s = [1]; c = [];
}
-let push st n = {
+let push st n = {st with
n = n; s = 1 :: st.s;
}
-let next st = {
+let next st f = {st with
+ c = f st.c;
n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
}
let mk_open st ris =
if st.n = "" then ris else
- T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris
+ T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg st.n :: T.Macro "OPEN" :: ris
-let mk_dec kind w s ris =
+let mk_dec st kind w s ris =
let w = if !G.no_types then [] else w in
- T.Group w :: T.free s :: T.arg s :: T.Macro kind :: ris
+ T.Group w :: T.free (mk_ptr st s) :: T.arg s :: T.Macro kind :: ris
-let mk_inferred st c t ris =
- let u = typeof c t in
- let is_u = proc_term [] c u in
- mk_dec "DECL" is_u st.n ris
+let mk_inferred st t ris =
+ let u = typeof st t in
+ let is_u = proc_term st [] u in
+ mk_dec st "DECL" is_u st.n ris
-let rec proc_proof st ris c t = match t with
+let rec proc_proof st ris t = match t with
| C.Appl []
| C.Meta _
| C.Implicit _
| C.Sort _
| C.Prod _ -> malformed "P1"
| C.Const _
- | C.Rel _ -> proc_proof st ris c (C.Appl [t])
+ | C.Rel _ -> proc_proof st ris (C.Appl [t])
| C.Lambda (s, w, t) ->
- let is_w = proc_term [] c w in
+ let is_w = proc_term st [] w in
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
+ proc_proof (next st (K.add_dec s w)) (mk_dec st "PRIM" is_w s ris) t
| C.Appl (t0 :: ts) ->
- 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
+ let rts = X.rev_neg_filter (K.not_prop2 st.c) [t0] ts in
+ let ris = T.Macro "STEP" :: mk_inferred st t ris in
+ let tts = L.rev_map (proc_term st []) rts in
mk_exit st (T.rev_mk_args tts ris)
| C.Match (w, u, v, ts) ->
- 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
+ let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in
+ let ris = T.Macro "DEST" :: mk_inferred st t ris in
+ let tts = L.rev_map (proc_term st []) 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 is_w = proc_term st [] w in
let ris = mk_open st ris in
- 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
+ if K.not_prop1 st.c w then
+ let is_v = proc_term st [] v in
+ let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec st "DECL" is_w s ris in
+ proc_proof (next st (K.add_def s w v)) ris t
else
- let ris_v = proc_proof (push st s) ris c v in
- proc_proof (next st) ris_v (K.add_def s w v c) t
+ let ris_v = proc_proof (push st s) ris v in
+ proc_proof (next st (K.add_def s w v)) ris_v t
-let proc_proof rs c t = try proc_proof (init ()) rs c t with
+let proc_proof st rs t = try proc_proof st rs t with
| E.ObjectNotFound _
| Invalid_argument "List.nth"
| Failure "nth"
let note = T.Note "This file was automatically generated by MaTeX: do not edit"
let proc_item item s ss t =
+ let st = init ss in
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 ss :: proc_term is [] tt
+ note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term st is tt
let proc_top_proof s ss t =
+ let st = init ss in
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)
+ L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt)
let open_out_tex s =
let fname = s ^ T.file_ext 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_g = " Global alpha-conversion (default: no)"
let help_l = "<file> Output the list of generated files in this file"
-let help_p = " omit types (default: no)"
+let help_p = " Omit types (default: no)"
let help_t = " Test term transformations (default: no)"
let help = ""
"-O", A.String ((:=) G.out_dir), help_O;
"-X", A.Unit G.clear, help_X;
"-a", A.Set G.log_alpha, help_a;
+ "-g", A.Set G.global_alpha, help_g;
"-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_global_alpha = false
+
let default_log_alpha = false
let default_list_och = None
(* interface ****************************************************************)
+let dno_id = "_" (* identifier for not-occurring premises *)
+
+let nan = -1 (* not a number *)
+
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 for anticipations *)
+
+let test = ref default_test (* test anticipation *)
-let proc_id = ref default_proc_id (* identifer of anticipations *)
+let no_types = ref default_no_types (* omit types *)
-let test = ref default_test (* test anticipation *)
+let global_alpha = ref default_global_alpha (* log alpha-unconverted identifiers *)
-let no_types = ref default_no_types (* omit types *)
+let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *)
-let log_alpha = ref default_log_alpha (* log alpha-unconverted identifiers *)
+let list_och = ref default_list_och (* output stream for list file *)
-let list_och = ref default_list_och (* output stream for list file *)
+let alpha_type = ref default_alpha (* data of type-based alpha-conversion *)
-let alpha_type = ref default_alpha (* data of type-based alpha-conversion *)
+let alpha_sort = ref default_alpha (* data of sort-based alpha-conversion *)
-let alpha_sort = ref default_alpha (* data of sort-based alpha-conversion *)
+let is_global_id s =
+ !global_alpha && s <> dno_id
let close_list () = match !list_och with
| None -> ()
proc_id := default_proc_id;
test := default_test;
no_types := default_no_types;
+ global_alpha := default_global_alpha;
log_alpha := default_log_alpha;
list_och := default_list_och;
alpha_type := default_alpha;
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+val dno_id: string
+
+val nan: int
+
val status: NCicPp.status
val no_init: bool ref
val no_types: bool ref
+val global_alpha: bool ref
+
val log_alpha: bool ref
val list_och: out_channel option ref
val clear: unit -> unit
val close_list: unit -> unit
+
+val is_global_id: string -> bool
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/04/28 MaTeX Package]
+\ProvidesPackage{matex}[2016/05/22 MaTeX Package]
\RequirePackage{xcolor}
\ExecuteOptions{}
\ProcessOptions*
%\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@settarget[2]{\hypertarget{obj:#2}{#1}}
\newcommand*\ma@setlink[2]{\hyperlink{obj:#2}{#1}}
\newcommand*\ObjIncNode{}
\newcommand*\ObjNode{}
-\newcommand*\ma@thehead[2]{\ObjIncNode\textbf{#1 \ObjNode(#2)}\neverindent\par}
+\newcommand*\ma@thehead[3]{\ObjIncNode\textbf{#1 \ObjNode(\ma@settarget{#2}{#3})}\neverindent\par}
\newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\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{axiom}[2]{\ma@thehead{Axiom}{#1}{#2}}{\par}
+\newenvironment{declaration}[2]{\ma@thehead{Declaration}{#1}{#2}}{\par}
\newenvironment{definition}[2]{}{\par}
-\newenvironment{proposition}[2]{\ma@settarget{#1}{#2}\ma@thehead{Proposition}{#1}}{\par}
+\newenvironment{proposition}[2]{\ma@thehead{Proposition}{#1}{#2}}{\par}
\newenvironment{proof}[2]{\ma@theneck{Proof}}{\par}
\newenvironment{ma@step}[1]{\color{#1}}{\par}
\newcommand*\ma@tmp{}
\newcommand*\ma@skip[4]{}
-\newcommand*\ma@next[5]{\def\ma@tmp{#5}\ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi\ma@tmp #3#2#3#4}
+\newcommand*\ma@next[5]{\def\ma@tmp{#5}%
+ \ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi
+ \ma@tmp #3#2#3#4%
+}
\newcommand*\ma@space{ }
\newcommand*\ma@arg[1]{#1}
+\newcommand*\ma@setopttarget[2]{\def\ma@tmp{#2}%
+ \ifx\ma@tmp\empty #1\else\ma@settarget{#1}{#2}\fi
+}
+
\newcommand*\PROP{PROP}
\newcommand*\CROP[1]{CROP}
\newcommand*\TYPE[1]{TYPE}
-\newcommand*\LREF[2]{#1}
+\newcommand*\LREF[2]{\def\ma@tmp{#2}%
+ \ifx\ma@tmp\empty #1\else\ma@setlink{#1}{#2}\fi
+}
\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) }
+\newcommand*\ABBR[4]{(D \ma@setopttarget{#1}{#2} #3 #4) }
+\newcommand*\ABST[3]{(I \ma@setopttarget{#1}{#2} #3) }
+\newcommand*\PROD[3]{(P \ma@setopttarget{#1}{#2} #3) }
\newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax}
\newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax}
\newcommand*\ma@with{ with }
\newcommand*\ma@comma{, }
\newcommand*\ma@stop{.\end{ma@step}}
-\newcommand*\ma@head[4]{\def\ma@tmp{#4}%
- \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{#2}%
- \else\begin{ma@step}{#3}\textbf{#4}%
+\newcommand*\ma@head[6]{\def\ma@tmp{#5}%
+ \ifx\ma@tmp\empty\begin{ma@step}{#1}\textbf{\ma@setopttarget{#2}{#3}}%
+ \else\begin{ma@step}{#4}\textbf{\ma@setopttarget{#5}{#6}}%
\fi
}
\newcommand*\ma@tail{\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
-\newcommand*\EXIT[1]{\ma@head{}{}{\ma@exit}{end} of block #1\ma@stop}
-\newcommand*\OPEN[3]{\ma@head{}{}{\ma@open}{#1} is this block #3\ma@stop}
-\newcommand*\PRIM[3]{\ma@head{}{}{\ma@prim}{#1} will have type #3\ma@stop}
-\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\par}
+\newcommand*\EXIT[1]{\ma@head{}{}{}{\ma@exit}{end}{} of block #1\ma@stop}
+\newcommand*\OPEN[3]{\ma@head{}{}{}{\ma@open}{#1}{#2} is this block #3\ma@stop}
+\newcommand*\PRIM[3]{\ma@head{}{}{}{\ma@prim}{#1}{#2} will have type #3\ma@stop}
+\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{}{\ma@fwd}{#1}{#2} has type #3\par}
\newcommand*\BODY[1]{being #1\ma@stop}
\newcommand*\STEP[1]{by #1\ma@tail}
\newcommand*\DEST[1]{by cases on #1\ma@tail}
projects / helm.git / commitdiff