From: Ferruccio Guidi Date: Mon, 11 Jan 2016 16:46:16 +0000 (+0000) Subject: - plain anticipation for CIC proofs terms X-Git-Tag: make_still_working~663 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea6b4322051d3eb1794bfca3928f6e1773f971ba;p=helm.git - plain anticipation for CIC proofs terms - support for (co)fixpoint objects - Makefile for testing - minor updates --- diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile index 42e1360e2..4e1e3ca66 100644 --- a/matita/components/binaries/matex/Makefile +++ b/matita/components/binaries/matex/Makefile @@ -7,10 +7,11 @@ include ../Makefile.common 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 diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml index c213d4d96..184a6937c 100644 --- a/matita/components/binaries/matex/TeX.ml +++ b/matita/components/binaries/matex/TeX.ml @@ -11,7 +11,10 @@ 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 *) @@ -19,16 +22,17 @@ and text = item list (* structured text *) 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 diff --git a/matita/components/binaries/matex/TeXOutput.ml b/matita/components/binaries/matex/TeXOutput.ml index 053c890bb..f92101c30 100644 --- a/matita/components/binaries/matex/TeXOutput.ml +++ b/matita/components/binaries/matex/TeXOutput.ml @@ -13,19 +13,25 @@ module L = List 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 ******************************************************) diff --git a/matita/components/binaries/matex/anticipate.ml b/matita/components/binaries/matex/anticipate.ml new file mode 100644 index 000000000..1681d2d03 --- /dev/null +++ b/matita/components/binaries/matex/anticipate.ml @@ -0,0 +1,147 @@ +(* + ||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 diff --git a/matita/components/binaries/matex/anticipate.mli b/matita/components/binaries/matex/anticipate.mli new file mode 100644 index 000000000..e934bb462 --- /dev/null +++ b/matita/components/binaries/matex/anticipate.mli @@ -0,0 +1,18 @@ +(* + ||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 diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 4f31b07a2..9b7ba8253 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -11,139 +11,179 @@ 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 ******************************************************) diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml new file mode 100644 index 000000000..022ab63f2 --- /dev/null +++ b/matita/components/binaries/matex/ground.ml @@ -0,0 +1,53 @@ +(* + ||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 diff --git a/matita/components/binaries/matex/ground.mli b/matita/components/binaries/matex/ground.mli new file mode 100644 index 000000000..e9892a7e0 --- /dev/null +++ b/matita/components/binaries/matex/ground.mli @@ -0,0 +1,28 @@ +(* + ||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 diff --git a/matita/components/binaries/matex/kernel.ml b/matita/components/binaries/matex/kernel.ml new file mode 100644 index 000000000..f9ed0c466 --- /dev/null +++ b/matita/components/binaries/matex/kernel.ml @@ -0,0 +1,123 @@ +(* + ||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" diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index db1785c79..59460ce4a 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -15,31 +15,26 @@ module F = Filename 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 = " 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 @@ -47,10 +42,10 @@ let is_registry s = 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 @@ -59,7 +54,12 @@ let process 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 diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml index dc094441e..14dc4e2c9 100644 --- a/matita/components/binaries/matex/options.ml +++ b/matita/components/binaries/matex/options.ml @@ -11,7 +11,8 @@ module F = Filename -module R = Helm_registry +module R = Helm_registry +module P = NCicPp (* internal *****************************************************************) @@ -19,13 +20,30 @@ let default_no_init = true 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 diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli index 3cd2afa74..2c0e9b9b6 100644 --- a/matita/components/binaries/matex/options.mli +++ b/matita/components/binaries/matex/options.mli @@ -9,8 +9,16 @@ \ / 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 diff --git a/matita/components/binaries/matex/test/Make b/matita/components/binaries/matex/test/Make new file mode 100644 index 000000000..e69de29bb diff --git a/matita/components/binaries/matex/test/Makefile b/matita/components/binaries/matex/test/Makefile new file mode 100644 index 000000000..b19199965 --- /dev/null +++ b/matita/components/binaries/matex/test/Makefile @@ -0,0 +1,38 @@ +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) $< $@ diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index 195789fe3..50338f5df 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,16 +1,37 @@ -\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 diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index ddf18c408..e30233190 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -1,13 +1,26 @@ \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}