- improved style sheet and test document
let ok s =
X.log ("anticipate: ok " ^ s)
let ok s =
X.log ("anticipate: ok " ^ s)
-let not_prop1 c u = match (K.whd c (K.typeof c u)) with
+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"
| C.Sort (C.Prop) -> false
| C.Sort _ -> true
| _ -> malformed "1"
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
\ / 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 not_prop1: NCic.context -> NCic.term -> bool
val not_prop2: NCic.context -> NCic.term -> bool
module A = Anticipate
type status = {
module A = Anticipate
type status = {
- g: string; (* global object name *)
- l: string; (* local reference name *)
+ n: string; (* reference name *)
- w: bool; (* is first construction *)
}
(* internal functions *******************************************************)
let alpha c s = s
}
(* internal functions *******************************************************)
let alpha c s = s
+let internal s =
+ X.error ("engine: malformed stack: " ^ s)
+
let malformed s =
X.error ("engine: malformed term: " ^ s)
let malformed s =
X.error ("engine: malformed term: " ^ s)
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
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_concat "." "type" ss)]
+ [T.Macro "GREF"; T.arg name; T.free (X.rev_map_concat X.id "." "type" ss)]
| C.Match (w, u, v, ts) ->
let is_w = proc_term c (C.Const w) in
let is_u = proc_term c u in
| 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 init n = {
- g = n; l = "_"; s = []; w = true
-}
+let typeof c = function
+ | C.Appl [t]
+ | t -> A.typeof c t
-let push st n = {st with
- l = n; s = 1 :: st.s; w = true
+let init () = {
+ n = ""; s = [1]
-let pop st = {st with
- w = false; s = match st.s with [] -> [] | i :: tl -> succ i :: tl
+let push st n = {
+ n = n; s = 1 :: st.s;
-let next st = {st with
- w = false
+let next st = {
+ n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
+let scope st =
+ X.rev_map_concat string_of_int "." "" (L.tl st.s)
+
+let mk_exit st ris =
+ if st.n <> "" || L.tl st.s = [] then ris else
+ T.free (scope st) :: T.Macro "EXIT" :: ris
+
- if st.w then T.Macro "PRIM" :: T.arg "" :: T.Macro "OPEN" :: ris else ris
+ if st.n = "" then ris else
+ T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris
let mk_dec w s ris =
let w = if !G.no_types then [] else w in
T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: ris
let mk_dec w s ris =
let w = if !G.no_types then [] else w in
T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: ris
+let mk_inferred st c t ris =
+ let u = typeof c t in
+ let is_u = proc_term c u in
+ mk_dec is_u st.n ris
+
let rec proc_proof st ris c t = match t with
| C.Appl []
| C.Meta _
let rec proc_proof st ris c t = match t with
| C.Appl []
| C.Meta _
proc_proof (next st) (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t
| C.Appl ts ->
let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
proc_proof (next st) (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t
| C.Appl ts ->
let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
- let ris = T.Macro "STEP" :: ris in
+ let ris = T.Macro "STEP" :: mk_inferred st c t ris in
let tts = L.rev_map (proc_term c) rts 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
| C.Match (w, u, v, ts) ->
let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in
- let ris = T.Macro "DEST" :: ris in
+ let ris = T.Macro "DEST" :: mk_inferred st c t ris in
let tts = L.rev_map (proc_term c) rts 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 s = alpha c s in
let is_w = proc_term c w in
| C.LetIn (s, w, v, t) ->
let s = alpha c s in
let is_w = proc_term c w in
+ let ris = mk_open st ris in
if A.not_prop1 c w then
let is_v = proc_term c v in
proc_proof (next st) (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t
else
let ris_v = proc_proof (push st s) ris c v in
if A.not_prop1 c w then
let is_v = proc_term c v in
proc_proof (next st) (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t
else
let ris_v = proc_proof (push st s) ris c v in
- proc_proof (pop st) (mk_dec is_w s ris_v) (K.add_def s w v c) t
+ proc_proof (next st) ris_v (K.add_def s w v c) t
-let proc_proof c t = try proc_proof (init "") [] c t with
+let proc_proof rs c t = try proc_proof (init ()) rs c t with
| E.ObjectNotFound _
| Invalid_argument "List.nth"
| E.ObjectNotFound _
| Invalid_argument "List.nth"
| Failure "name_of_reference" -> malformed "P2"
| V.TypeCheckerFailure s
| V.AssertFailure s -> malformed (Lazy.force s)
| Failure "name_of_reference" -> malformed "P2"
| V.TypeCheckerFailure s
| V.AssertFailure s -> malformed (Lazy.force s)
+ | Failure "hd"
+ | Failure "tl" -> internal "P2"
(* top level processing *)
(* top level processing *)
let proc_top_proof s t =
let tt = A.process_top_term s t in (* anticipation *)
let proc_top_proof s t =
let tt = A.process_top_term s t in (* anticipation *)
- L.rev (proc_proof [] tt)
+ L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof [T.arg "proof"; T.Macro "begin"] [] tt)
let open_out_tex s =
open_out (F.concat !G.out_dir (s ^ T.file_ext))
let proc_pair s ss u xt =
let open_out_tex s =
open_out (F.concat !G.out_dir (s ^ T.file_ext))
let proc_pair s ss u xt =
- let name = X.rev_concat "." "type" ss in
+ let name = X.rev_map_concat X.id "." "type" ss in
let och = open_out_tex name in
O.out_text och (proc_top_type s u);
close_out och;
match xt with
| None -> ()
| Some t ->
let och = open_out_tex name in
O.out_text och (proc_top_type s u);
close_out och;
match xt with
| None -> ()
| Some t ->
- let name = X.rev_concat "." "body" ss in
+ let name = X.rev_map_concat X.id "." "body" ss in
let och = open_out_tex name in
let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
O.out_text och (text s t);
let och = open_out_tex name in
let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
O.out_text och (text s t);
(* interface functions ******************************************************)
(* interface 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 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 rec rev_concat sep r = function
+let rec rev_map_concat map sep r = function
- if r = "" then rev_concat sep s ss else
- rev_concat sep (s ^ sep ^ r) ss
+ if r = "" then rev_map_concat map sep (map s) ss else
+ rev_map_concat map sep (map s ^ sep ^ r) ss
let fold_string map a s =
let l = S.length s in
let fold_string map a s =
let l = S.length s in
let error s = raise (Error s)
let error s = raise (Error s)
-let log s = P.eprintf "MaTeX: %s\n" s
+let log s = P.eprintf "MaTeX: %s\n%!" s
val segments_of_string: string list -> int -> string -> string list
val segments_of_string: string list -> int -> string -> string list
-val rev_concat: string -> string -> string list -> string
+val rev_map_concat: ('a -> string) -> string -> string -> 'a list -> string
val fold_string: ('a -> char -> 'a) -> 'a -> string -> 'a
val fold_string: ('a -> char -> 'a) -> 'a -> string -> 'a
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesPackage{matex}[2015/12/21 MaTeX Package]
+\ExecuteOptions{}
+\ProcessOptions*
+
\makeatletter
\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
\makeatletter
\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
\newcommand*\ObjRef[1]{\ref{obj:#1}}
\newtheorem{prop}{Proposition}
\newcommand*\ObjRef[1]{\ref{obj:#1}}
\newtheorem{prop}{Proposition}
+\newenvironment{proof}{\setlength\parindent{0pt}}{}
+\newenvironment{ma@step}{}{\vskip0pt}
\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
\newcommand*\ma@with{ with }
\newcommand*\ma@comma{, }
\newcommand*\ma@with{ with }
\newcommand*\ma@comma{, }
-\newcommand*\ma@stop{.\vskip10pt}
+\newcommand*\ma@stop{.\end{ma@step}}
-\newcommand*\DECL[3]{\textbf{#1} : #3\vskip10pt}
-\newcommand*\PRIM{}
-\newcommand*\BODY[1]{is #1\vskip10pt}
-\newcommand*\STEP[1]{by #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
-\newcommand*\DEST[1]{by cases on #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
+\newcommand*\DECL[3]{\def\ma@tmp{#1}\begin{ma@step}\textbf{\ifx\ma@tmp\empty\_conlusion\else #1\fi} of type #3}
+\newcommand*\PRIM{\end{ma@step}}
+\newcommand*\BODY[1]{\\is #1\end{ma@step}}
+\newcommand*\STEP[1]{\\by #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
+\newcommand*\DEST[1]{\\by cases on #1\ma@next\ma@with\ma@arg\ma@comma\ma@stop}
+\newcommand*\OPEN[3]{\begin{ma@step}\textbf{#1} is the following scope #3.\end{ma@step}}
+\newcommand*\EXIT[1]{\begin{ma@step}\textbf{end} of scope #1.\end{ma@step}}
+\documentclass[8pt,twocolumn]{extarticle}
\usepackage[bookmarks=false,ps2pdf]{hyperref}
\usepackage[american]{babel}
\usepackage[bookmarks=false,ps2pdf]{hyperref}
\usepackage[american]{babel}