REGISTRY = $(RT_BASE_DIR)/matita.conf.xml
-OBJ = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con
+OBJS = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con\
+ cic:/matita/lambdadelta/basic_1/pr0/defs/pr0_ind.con
test:
- @echo MaTeX $(OBJ)
- $(H)./matex.native -O test $(REGISTRY) $(OBJ)
+ @echo MaTeX: $(OBJS:cic:/matita/lambdadelta/basic_1/pr0/%.con=%)
+ $(H)./matex.native -O test -t -p $(REGISTRY) $(OBJS)
.PHONY: test
module L = List
+module X = Ground
+
type item = Free of string (* free text *)
+ | Text of string (* quoted text *)
| Macro of string (* macro *)
| Group of text (* group *)
let file_ext = ".tex"
-let empty = [Free ""]
-
-let newline = [Free "%\n"]
-
let group s = Group s
-let arg s = Group [Free s]
+let arg s = Group [Text s]
-let mk_rev_args riss =
- L.rev_map group (empty :: riss)
+let free s = Group [Free s]
let mk_segs us =
L.rev_map arg ("" :: (L.rev us))
+
+let mk_rev_args riss =
+ L.rev_map group ([] :: riss)
+
+let rev_mk_args iss is =
+ free "" :: X.rev_map_append group iss is
module P = Printf
module S = String
+module X = Ground
module T = TeX
(* internal functions *******************************************************)
let special = "\\{}$&#^_~%" (* LaTeX reserves these characters *)
-let quote c =
- if S.contains special c then '.' else c
+let special = [
+ '_', "\\_";
+]
+
+let quote s c = try s ^ L.assoc c special with
+ | Not_found -> s ^ S.make 1 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
+ | T.Free s -> P.fprintf och "%s" s
+ | T.Text s -> P.fprintf och "%s" (X.fold_string quote "" s)
+ | T.Macro s -> P.fprintf och "\\%s%%\n" s
+ | T.Group t -> P.fprintf och "{%a}%%\n" out_text t
(* interface functions ******************************************************)
--- /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 C = NCic
+module T = NCicTypeChecker
+
+module X = Ground
+module G = Options
+module K = Kernel
+
+(* internal functions *******************************************************)
+
+let fresh = ref 0
+
+let malformed s =
+ X.error ("anticipate: malformed term: " ^ s)
+
+let ok s =
+ X.log ("anticipate: ok " ^ s)
+
+let not_prop1 c u = match (K.whd c (K.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
+ P.sprintf "%s%u" !G.proc_id !fresh, w, v, C.Rel K.fst_var
+
+let initial = None, []
+
+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
+ let s, w, v, tt = anticipate c t in
+ Some (i, s, w, v), (tt :: rtts)
+
+let lift_arg ri i tts t =
+ if ri = i then t :: tts
+ else K.lift K.fst_var 1 t :: tts
+
+let rec proc_term c t = match t with
+ | C.Appl []
+ | C.Meta _
+ | C.Implicit _ -> malformed "2"
+ | C.Sort _
+ | C.Rel _
+ | C.Const _
+ | C.Prod _ -> [], t
+ | C.Lambda (s, w, t) ->
+ 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
+ let dt, tt = proc_term (K.add_def s w v c) t in
+ dt @ K.add_def s w v [], tt
+ else
+ let dv, vv = proc_term c v in
+ let l = L.length dv in
+ let c = dv @ c in
+ let w = K.lift K.fst_var l w in
+ let t = K.lift K.snd_var l t in
+ 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 ts -> proc_appl c t ts
+ | C.Match (w, u, v, ts) -> proc_case c t w u v ts
+
+and proc_appl c t ts = match X.foldi_left (proc_arg c) 1 initial ts with
+ | None , _ -> [], t
+ | 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))
+
+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
+ 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
+ proc_term c (K.letin s w0 v0 (K.case w u vv ts))
+ | Some (i, s, w0, v0), rtts ->
+ let ri = L.length rtts - i in
+ let u = K.lift K.fst_var 1 u in
+ let v = K.lift K.fst_var 1 v in
+ let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
+ proc_term c (K.letin s w0 v0 (K.case w u v tts))
+
+and shift_term c t =
+ let d, tt = proc_term c t in
+ K.shift tt d
+
+let shift_named s c t =
+try
+ fresh := 0;
+ let tt = shift_term 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)
+ | Invalid_argument "List.nth" -> malformed "4" (* to be removed *)
+
+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
+
+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
+ 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_obj obj = proc_obj 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 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 F = Filename
module L = List
+module P = Printf
module S = String
module U = NUri
module R = NReference
module C = NCic
-module P = NCicPp
module E = NCicEnvironment
+module V = NCicTypeChecker
+module X = Ground
module G = Options
+module K = Kernel
module T = TeX
module O = TeXOutput
+module A = Anticipate
-let status = new P.status
+type status = {
+ n: string; (* object name *)
+ s: int list; (* scope *)
+}
(* 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)
+ X.error ("engine: malformed term: " ^ s)
let not_supported () =
- failwith "MaTeX: object not supported"
+ X.error "engine: object not supported"
+
+(* generic term processing *)
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 ss = function
- | C.Constant _ , R.Decl ->
- T.Macro "GRef" :: T.mk_segs ("type" :: ss)
- | C.Constant _ , R.Def _ ->
- T.Macro "GRef" :: T.mk_segs ("body" :: ss)
- | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
- let _, name, _, _ = L.nth us i in
- T.Macro "IRef" :: T.mk_segs (name :: ss)
- | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
- let _, _, _, ts = L.nth us i in
- let _, name, _ = L.nth ts (pred j) in
- T.Macro "IRef" :: T.mk_segs (name :: ss)
- | C.Fixpoint (_, ts, _) , R.Fix (i, _, _) ->
- let _, name, _, _, _ = L.nth ts i in
- T.Macro "IRef" :: T.mk_segs (name :: ss)
- | C.Fixpoint (_, ts, _) , R.CoFix i ->
- let _, name, _, _, _ = L.nth ts i in
- T.Macro "IRef" :: T.mk_segs (name :: ss)
- | _ ->
- malformed "2"
+ | 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 "T1"
let rec proc_term c = function
| C.Appl []
| C.Meta _
- | C.Implicit _ -> malformed "3"
- | C.Rel m ->
- let name = L.nth c (m-1) in
- [T.Macro "LRef"; T.arg name]
- | C.Appl ts ->
+ | C.Implicit _ -> malformed "T2"
+ | C.Rel m ->
+ let name = K.resolve_lref c m in
+ [T.Macro "LREF"; T.arg name; T.free 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) ->
+ 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 is_t = proc_term (K.add_dec s w 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 is_t = proc_term (K.add_dec s w 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 ->
+ let is_t = proc_term (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
+ | C.Sort s ->
proc_sort s
- | C.Const (R.Ref (u, r)) ->
- let ss = segments_of_uri u in
- let _, _, _, _, obj = E.get_checked_obj status u in
- proc_gref ss (obj, r)
- | C.Match (w, u, v, ts) ->
+ | 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_concat "." "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
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
+ 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 _
+ | Invalid_argument "List.nth"
| Failure "nth"
- | Invalid_argument "List.nth" -> malformed "4"
+ | Failure "name_of_reference" -> malformed "T3"
+
+(* proof processing *)
+
+let init n = {
+ n = n; s = [];
+}
+
+let mk_dec w s is =
+ let w = if !G.no_types then [] else w in
+ T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: is
+
+let rec proc_proof st ris c 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.Lambda (s, w, t) ->
+ let s = alpha c s in
+ let is_w = proc_term c w in
+ proc_proof 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 tts = L.rev_map (proc_term c) rts in
+ 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 ris = T.Macro "DEST" :: ris in
+ let tts = L.rev_map (proc_term c) rts in
+ 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
+ if A.not_prop1 c w then
+ let is_v = proc_term c v in
+ proc_proof 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 st ris c v in
+ proc_proof st (mk_dec is_w s ris_v) (K.add_def s w v c) t
+
+let proc_proof c t = try proc_proof (init "") [] c t with
+ | E.ObjectNotFound _
+ | Invalid_argument "List.nth"
+ | Failure "nth"
+ | Failure "name_of_reference" -> malformed "P2"
+ | V.TypeCheckerFailure s
+ | V.AssertFailure s -> malformed (Lazy.force s)
+
+(* top level processing *)
+
+let proc_top_type s t =
+ [T.Macro "Object"; T.arg s; T.free s; T.Group (proc_term [] t)]
+
+let proc_top_body s t = proc_term [] t
+
+let proc_top_proof s t =
+ let tt = A.process_top_term s t in (* anticipation *)
+ L.rev (proc_proof [] tt)
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 proc_pair s ss u xt =
+ let name = X.rev_concat "." "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 name = X.rev_concat "." "body" ss in
let och = open_out_tex name in
- O.out_text och (proc_term [] u);
- O.out_text och T.newline;
+ let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
+ O.out_text och (text s t);
close_out och
- | C.Fixpoint (_, _, _) -> not_supported ()
- | C.Inductive (_, _, _, _) -> not_supported ()
+
+let proc_fun ss (r, s, i, u, t) =
+ proc_pair s (s :: ss) u (Some t)
+
+let proc_obj u =
+ let ss = K.segments_of_uri u in
+ let _, _, _, _, obj = E.get_checked_obj G.status u in
+ match obj with
+ | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
+ | C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs
+ | C.Inductive (_, _, _, _) -> not_supported ()
(* interface functions ******************************************************)
--- /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
+
+exception Error of string
+
+(* 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 rev_concat sep r = function
+ | [] -> r
+ | s :: ss ->
+ if r = "" then rev_concat sep s ss else
+ rev_concat sep (s ^ sep ^ r) ss
+
+let fold_string map a s =
+ let l = S.length s in
+ let rec aux i a =
+ if i >= l then a else aux (succ i) (map a s.[i])
+ in
+ aux 0 a
+
+let rec rev_neg_filter filter r = function
+ | [] -> r
+ | hd :: tl ->
+ if filter hd then rev_neg_filter filter r tl else rev_neg_filter filter (hd :: r) tl
+
+let rec foldi_left mapi i a = function
+ | [] -> a
+ | hd :: tl -> foldi_left mapi (succ i) (mapi i a hd) tl
+
+let rec rev_map_append map l r = match l with
+ | [] -> r
+ | hd :: tl -> rev_map_append map tl (map hd :: r)
+
+let error s = raise (Error s)
+
+let log s = P.eprintf "MaTeX: %s\n" s
--- /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_______________________________________________________________ *)
+
+exception Error of string
+
+val error: string -> 'a
+
+val log: string -> unit
+
+val segments_of_string: string list -> int -> string -> string list
+
+val rev_concat: string -> string -> string list -> string
+
+val fold_string: ('a -> char -> 'a) -> 'a -> string -> 'a
+
+val rev_neg_filter : ('a -> bool) -> 'a list -> 'a list -> 'a list
+
+val foldi_left: (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
+
+val rev_map_append: ('a -> 'b) -> 'a list -> 'b list -> 'b list
--- /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 F = Filename
+module P = Printf
+module S = String
+
+module U = NUri
+module C = NCic
+module B = NCicSubstitution
+module D = NCicReduction
+module K = NCicTypeChecker
+module H = HLog
+module A = NCicLibrary
+module E = NCicEnvironment
+module R = NReference
+
+module X = Ground
+module G = Options
+
+(* internal functions *******************************************************)
+
+let trusted _ = true
+
+let no_log _ _ = ()
+
+let mk_type_universe i =
+ [`Type, U.uri_of_string (P.sprintf "cic:/matita/pts/Type%s.univ" i)]
+
+(* interface functions ******************************************************)
+
+let init () =
+ A.init ();
+ K.set_trust trusted;
+ 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
+
+let fst_var = 1
+
+let snd_var = 2
+
+let lambda s w t = C.Lambda (s, w, t)
+
+let letin s w v t = C.LetIn (s, w, v, t)
+
+let case w u v ts = C.Match (w, u, v, ts)
+
+let add_dec s w c = (s, C.Decl w) :: c
+
+let add_def s w v c = (s, C.Def (v, w)) :: c
+
+let rec shift t = function
+ | [] -> t
+ | (s, C.Decl w) :: c -> shift (lambda s w t) c
+ | (s, C.Def (v, w)) :: c -> shift (letin s w v t) c
+
+let rec is_atomic = function
+ | C.Appl [t] -> is_atomic t
+ | C.Appl []
+ | C.Meta _
+ | C.Implicit _
+ | C.Sort _
+ | C.Rel _
+ | C.Const _ -> true
+ | C.Appl _
+ | C.Prod _
+ | C.Lambda _
+ | C.LetIn _
+ | C.Match _ -> false
+
+let resolve_lref c i = fst (L.nth c (i - fst_var))
+
+let lift d e t =
+ B.lift G.status ~from:d e t
+
+let lifts d e ts =
+ L.rev_map (lift d e) (L.rev ts)
+
+let whd c t =
+ D.whd G.status ~delta:max_int ~subst:[] c t
+
+let typeof c t =
+ K.typeof G.status [] [] c t
+
+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
+ X.segments_of_string [] (l-i-2) s
+
+let name_of_reference ss = function
+ | C.Constant (_, name, _, _, _), R.Decl ->
+ ss, name
+ | C.Constant (_, name, _, _, _), R.Def _ ->
+ ss, name
+ | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
+ let _, name, _, _ = L.nth us i in
+ (name :: ss), name
+ | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
+ let _, _, _, ts = L.nth us i in
+ let _, name, _ = L.nth ts (pred j) in
+ (name :: ss), name
+ | C.Fixpoint (_, ts, _) , R.Fix (i, _, _) ->
+ let _, name, _, _, _ = L.nth ts i in
+ (name :: ss), name
+ | C.Fixpoint (_, ts, _) , R.CoFix i ->
+ let _, name, _, _, _ = L.nth ts i in
+ (name :: ss), name
+ | _ ->
+ failwith "name_of_reference"
module U = NUri
module R = Helm_registry
module L = Librarian
-module B = NCicLibrary
-module C = NCicTypeChecker
-module H = HLog
+module X = Ground
module G = Options
module E = Engine
module O = TeXOutput
+module K = Kernel
let help_O = "<dir> Set this output directory"
let help_X = " Clear configuration and options"
+let help_p = " omit types (default: no)"
+let help_t = " Test anticipation (default: no)"
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;
+ K.init ();
G.no_init := false;
end
F.check_suffix s ".conf.xml"
let no_init () =
- failwith "MaTeX: registry not initialized"
+ failwith "MaTeX: main: registry not initialized"
let malformed s =
- failwith ("MaTeX: malformed argument: " ^ s)
+ failwith ("MaTeX: main: malformed argument: " ^ s)
let process s =
if is_registry s then init s
else malformed s
let main =
+try
A.parse [
"-O", A.String ((:=) G.out_dir), help_O;
"-X", A.Unit G.clear, help_X;
+ "-p", A.Set G.no_types, help_p;
+ "-t", A.Set G.test, help_t;
] process help
+with
+ | X.Error s -> X.log s
module F = Filename
-module R = Helm_registry
+module R = Helm_registry
+module P = NCicPp
(* internal *****************************************************************)
let default_out_dir = F.current_dir_name
+let default_proc_id = "H"
+
+let default_test = false
+
+let default_no_types = false
+
(* interface ****************************************************************)
+let status = new P.status
+
let no_init = ref default_no_init
-let out_dir = ref default_out_dir
+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 clear () =
R.clear ();
no_init := default_no_init;
- out_dir := default_out_dir
+ out_dir := default_out_dir;
+ proc_id := default_proc_id;
+ test := default_test;
+ no_types := default_no_types
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+val status: NCicPp.status
+
val no_init: bool ref
val out_dir: string ref
+val proc_id: string ref
+
+val test: bool ref
+
+val no_types: bool ref
+
val clear: unit -> unit
--- /dev/null
+LATEX = latex
+DVIPS = dvips
+BIBTEX = bibtex
+PSPDF = ps2pdf -dEmbedAllFonts=true -dPDFSETTINGS=/prepress
+UNLOG = ./unlog.pl
+
+MAIN = test
+
+SOURCES = $(shell cat Make)
+
+all: $(MAIN).dvi
+
+ps: $(MAIN).ps
+
+pdf: $(MAIN).pdf
+
+tar: $(MAIN).tar
+
+again:
+ $(MAKE) --no-print-directory -B
+
+clean:
+ $(RM) *.log *.dvi *.aux *.spl *.ps *.blg *.pdf *.tar *~
+
+bibtex: $(MAIN).log
+ $(BIBTEX) $(MAIN)
+
+$(MAIN).dvi $(MAIN).log $(MAIN).aux: $(MAIN).tex $(SOURCES)
+ $(LATEX) $<
+
+$(MAIN).ps: $(MAIN).dvi
+ $(DVIPS) $<
+
+$(MAIN).pdf: $(MAIN).ps
+ $(PSPDF) $<
+
+$(MAIN).tar: $(MAIN).log
+ $(UNLOG) $< $@
-\newcommand*\Skip[1]{}
-\newcommand*\Next[2]{\def\TMP{#2}\ifx\TMP\empty\let\next=\Skip\else #1{#2}\let\next=\Next\fi\next #1}
-
-\newcommand*\Visit[1]{ #1}
-
-\newcommand*\Prop{PROP}
-\newcommand*\Crop[1]{CROP}
-\newcommand*\Type[1]{TYPE}
-\newcommand*\LRef[1]{(L #1)}
-\newcommand*\GRef[2]{(G #2)\Next\Skip}
-\newcommand*\IRef[1]{(J #1)\Next\Skip}
-\newcommand*\Abbr[3]{(D #1 #2 #3) }
-\newcommand*\Abst[2]{(I #1 #2) }
-\newcommand*\Prod[2]{(P #1 #2) }
-\newcommand*\Appl{(A)\Next\Visit}
-\newcommand*\Case[3]{(C #1 #2 #3)\Next\Visit}
+\makeatletter
+
+\newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
+
+\newtheorem{prop}{Proposition}
+
+\newcommand*\ObjLabel[1]{\label{obj:#1}}
+\newcommand*\ObjRef[1]{\ref{obj:#1}}
+
+\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
+
+\newcommand*\@skip[2]{}
+\newcommand*\Next[3]{\def\@tmp{#3}\ifx\@tmp\empty #2\let\next=\@skip\else #1{#3}\let\next=\Next\fi\next #1#2}
+
+\newcommand*\@proc[1]{ #1}
+
+\newcommand*\PROP{PROP}
+\newcommand*\CROP[1]{CROP}
+\newcommand*\TYPE[1]{TYPE}
+\newcommand*\LREF[2]{#1}
+\newcommand*\GREF[2]{#1}
+\newcommand*\ABBR[3]{(D #1 #2 #3) }
+\newcommand*\ABST[2]{(I #1 #2) }
+\newcommand*\PROD[2]{(P #1 #2) }
+\newcommand*\APPL{(A)\Next\@proc\relax}
+\newcommand*\CASE[3]{(C #1 #2 #3)\Next\@proc\relax}
+
+\def\@arg#1{, #1}
+\def\@stop{.\vskip10pt}
+
+\newcommand*\DECL[3]{\textbf{#1} : #3\vskip10pt}
+\newcommand*\PRIM{}
+\newcommand*\BODY[1]{is #1\vskip10pt}
+\newcommand*\STEP[1]{by #1\Next\@arg\@stop}
+\newcommand*\DEST[1]{by cases on #1\Next\@arg\@stop}
+
+\makeatother
\documentclass{article}
+\usepackage[bookmarks=false,ps2pdf]{hyperref}
+\usepackage[american]{babel}
\usepackage{matex}
\begin{document}
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type.tex}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body.tex}
+
+\bigskip
+
\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.type}
-% \bigskip
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
-% \input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
+\ObjRef{pr0_ind}
+\ObjRef{pr0_confluence}
\end{document}
projects / helm.git / commitdiff