From: Ferruccio Guidi Date: Thu, 28 Jul 2011 11:14:01 +0000 (+0000) Subject: xoa: new binary for the generation of multiple logical constants X-Git-Tag: make_still_working~2347 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4de2411d2cecf21630f6675f58e64f8ec6de9b60;p=helm.git xoa: new binary for the generation of multiple logical constants lambda-delta: integration with xoa and a lemma about a xoa constant --- diff --git a/matita/components/binaries/Makefile.common b/matita/components/binaries/Makefile.common new file mode 100644 index 000000000..8f8033dbb --- /dev/null +++ b/matita/components/binaries/Makefile.common @@ -0,0 +1,25 @@ +H=@ + +include ../../../Makefile.defs + +DIST=$(EXEC)---$(VERSION) +DATE=$(shell date +%y%m%d) + +OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) + +all: + @echo " OCAMLBUILD $(EXEC).native" + $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" $(EXEC).native + +clean: + ocamlbuild -clean + rm -rf $(DIST) $(DIST).tgz + +dist: + mkdir -p $(DIST)/Sources + cp ReadMe $(DIST) + cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources + cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC) + tar -cvzf $(DIST).tgz $(DIST) diff --git a/matita/components/binaries/xoa/Makefile b/matita/components/binaries/xoa/Makefile new file mode 100644 index 000000000..dd5a763f7 --- /dev/null +++ b/matita/components/binaries/xoa/Makefile @@ -0,0 +1,6 @@ +EXEC = xoa +VERSION=0.2.0 + +REQUIRES = helm-grafite + +include ../Makefile.common diff --git a/matita/components/binaries/xoa/ast.ml b/matita/components/binaries/xoa/ast.ml new file mode 100644 index 000000000..4de0c1057 --- /dev/null +++ b/matita/components/binaries/xoa/ast.ml @@ -0,0 +1,21 @@ +(* + ||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_______________________________________________________________ *) + +type arity = int + +type subarity = int + +type directive = Exists of arity * subarity + | Or of arity + +let mk_exists c v = Exists (c, v) + +let mk_or c = Or c diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml new file mode 100644 index 000000000..bc9a8be5d --- /dev/null +++ b/matita/components/binaries/xoa/engine.ml @@ -0,0 +1,132 @@ +(* + ||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 P = Printf +module A = Ast + +let string_iter sep f n = + let rec aux = function + | n when n < 1 -> "" + | 1 -> f 1 + | n -> f n ^ sep ^ aux (pred n) + in + aux n + +let void_iter f n = + let rec aux = function + | n when n < 1 -> () + | 1 -> f 1 + | n -> f n; aux (pred n) + in + aux n + +let mk_exists ooch noch c v = + let description = "multiple existental quantifier" in + let in_prec = "non associative with precedence 20\n" in +(* let out_prec = "right associative with precedence 20\n" in *) + let name s = P.sprintf "%s%u_%u" s c v in + let o_name = name "ex" in + let i_name = "'Ex" in + + let set n = P.sprintf "A%u" (v - n) in + let set_list = string_iter "," set v in + let set_type = string_iter "→" set v in + + let ele n = P.sprintf "x%u" (v - n) in + let ele_list = string_iter "," ele v in + let ele_seq = string_iter " " ele v in + + let pre n = P.sprintf "P%u" (c - n) in + let pre_list = string_iter "," pre c in + let pre_seq = string_iter " " pre c in + let pre_appl n = P.sprintf "%s %s" (pre n) ele_seq in + let pre_type = string_iter " → " pre_appl c in + + let qm n = "?" in + let qm_set = string_iter " " qm v in + let qm_pre = string_iter " " qm c in + + let id n = P.sprintf "ident x%u" (v - n) in + let id_list = string_iter " , " id v in + + let term n = P.sprintf "term 19 P%u" (c - n) in + let term_conj = string_iter " break & " term c in + + let abst b n = let xty = if b then P.sprintf ":$T%u" (v - n) else "" in + P.sprintf "λ${ident x%u}%s" (v - n) xty in + + let abst_clo b = string_iter "." (abst b) v in + + let full b n = P.sprintf "(%s.$P%u)" (abst_clo b) (c - n) in + let full_seq b = string_iter " " (full b) c in + + P.fprintf ooch "(* %s (%u, %u) *)\n\n" description c v; + + P.fprintf ooch "inductive %s (%s:Type[0]) (%s:%s→Prop) : Prop ≝\n" + o_name set_list pre_list set_type; + P.fprintf ooch " | %s_intro: ∀%s. %s → %s %s %s\n.\n\n" + o_name ele_list pre_type o_name qm_set qm_pre; + + P.fprintf ooch "interpretation \"%s (%u, %u)\" %s %s = (%s %s %s).\n\n" + description c v i_name pre_seq o_name qm_set pre_seq; + + P.fprintf noch "(* %s (%u, %u) *)\n\n" description c v; + + P.fprintf noch "notation > \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n" + id_list term_conj in_prec i_name (full_seq false); + + P.fprintf noch "notation < \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n" + id_list term_conj in_prec i_name (full_seq true) + +let mk_or ooch noch c = + let description = "multiple disjunction connective" in + let in_prec = "non associative with precedence 30\n" in + let name s = P.sprintf "%s%u" s c in + let o_name = name "or" in + let i_name = "'Or" in + + let pre n = P.sprintf "P%u" (c - n) in + let pre_list = string_iter "," pre c in + let pre_seq = string_iter " " pre c in + + let qm n = "?" in + let qm_pre = string_iter " " qm c in + + let term n = P.sprintf "term 29 P%u" (c - n) in + let term_disj = string_iter " break | " term c in + + let par n = P.sprintf "$P%u" (c - n) in + let par_seq = string_iter " " par c in + + let mk_con n = P.fprintf ooch " | %s_intro%u: %s → %s %s\n" + o_name (c - n) (pre n) o_name qm_pre + in + + P.fprintf ooch "(* %s (%u) *)\n\n" description c; + + P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n" + o_name pre_list; + void_iter mk_con c; + P.fprintf ooch ".\n\n"; + + P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n" + description c i_name pre_seq o_name pre_seq; + + P.fprintf noch "(* %s (%u) *)\n\n" description c; + + P.fprintf noch "notation \"hvbox(∨∨ %s)\"\n %s for @{ %s %s }.\n\n" + term_disj in_prec i_name par_seq + +let generate ooch noch = function + | A.Exists (c, v) -> + if c > 0 && v > 0 then mk_exists ooch noch c v + | A.Or c -> + if c > 1 then mk_or ooch noch c diff --git a/matita/components/binaries/xoa/engine.mli b/matita/components/binaries/xoa/engine.mli new file mode 100644 index 000000000..231221cd3 --- /dev/null +++ b/matita/components/binaries/xoa/engine.mli @@ -0,0 +1,12 @@ +(* + ||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 generate: out_channel -> out_channel -> Ast.directive -> unit diff --git a/matita/components/binaries/xoa/lib.ml b/matita/components/binaries/xoa/lib.ml new file mode 100644 index 000000000..e6e203e62 --- /dev/null +++ b/matita/components/binaries/xoa/lib.ml @@ -0,0 +1,48 @@ +(* + ||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 F = Filename + +module R = Helm_registry + +let template = "matita.ma.templ" + +let myself = F.basename Sys.argv.(0) + +let get_preamble conf = + R.load_from conf; + let rt_base_dir = R.get_string "matita.rt_base_dir" in + F.concat rt_base_dir template + +let copy_preamble preamble och = + let ich = open_in preamble in + let rec read () = + Printf.fprintf och "%s\n" (input_line ich); read () + in + try read () with End_of_file -> close_in ich + +let print_comment och = + let stars = String.make (30 - String.length myself) '*' in + Printf.fprintf och "(* This file was generated by %s: do not edit %s*)\n\n" myself stars + +let open_out preamble name = + let path = [ + R.get_string "matita.rt_base_dir"; + R.get_string "xoa.output_dir"; + name + ] in + let name = List.fold_left F.concat "" path in + let och = open_out (name ^ ".ma") in + copy_preamble preamble och; print_comment och; + och + +let out_include och s = + Printf.fprintf och "include \"%s\".\n\n" s diff --git a/matita/components/binaries/xoa/lib.mli b/matita/components/binaries/xoa/lib.mli new file mode 100644 index 000000000..756d7478c --- /dev/null +++ b/matita/components/binaries/xoa/lib.mli @@ -0,0 +1,16 @@ +(* + ||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 get_preamble: string -> string + +val open_out: string -> string -> out_channel + +val out_include: out_channel -> string -> unit diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml new file mode 100644 index 000000000..92b473d79 --- /dev/null +++ b/matita/components/binaries/xoa/xoa.ml @@ -0,0 +1,35 @@ +(* + ||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 R = Helm_registry + +module L = Lib +module A = Ast +module E = Engine + +let unm_ex s = + Scanf.sscanf s "%u %u" A.mk_exists + +let unm_or s = + Scanf.sscanf s "%u" A.mk_or + +let process conf = + let preamble = L.get_preamble conf in + let ooch = L.open_out preamble (R.get_string "xoa.objects") in + let noch = L.open_out preamble (R.get_string "xoa.notations") in + List.iter (L.out_include ooch) (R.get_list R.string "xoa.include"); + List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex"); + List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or"); + close_out noch; close_out ooch + +let _ = + let help = "Usage: xoa [ ]*\n" in + Arg.parse [] process help diff --git a/matita/matita/lib/lambda-delta/Makefile b/matita/matita/lib/lambda-delta/Makefile new file mode 100644 index 000000000..648904368 --- /dev/null +++ b/matita/matita/lib/lambda-delta/Makefile @@ -0,0 +1,12 @@ +H = @ +XOA_DIR = ../../../components/binaries/xoa +XOA = xoa.native + +CONF = xoa.conf.xml +TARGETS = xoa_natation.ma xoa_defs.ma + +all: $(TARGETS) + +$(TARGETS): $(CONF) + @echo " EXEC $(XOA) $(CONF)" + $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(CONF) diff --git a/matita/matita/lib/lambda-delta/syntax/item.ma b/matita/matita/lib/lambda-delta/syntax/item.ma index c9673b47e..d813a2dc8 100644 --- a/matita/matita/lib/lambda-delta/syntax/item.ma +++ b/matita/matita/lib/lambda-delta/syntax/item.ma @@ -16,8 +16,7 @@ *) include "lambda-delta/ground.ma". -include "lambda-delta/xoa_defs.ma". -include "lambda-delta/xoa_notation.ma". +include "lambda-delta/xoa_props.ma". include "lambda-delta/notation.ma". (* BINARY ITEMS *************************************************************) diff --git a/matita/matita/lib/lambda-delta/xoa.conf.xml b/matita/matita/lib/lambda-delta/xoa.conf.xml new file mode 100644 index 000000000..5718c3c73 --- /dev/null +++ b/matita/matita/lib/lambda-delta/xoa.conf.xml @@ -0,0 +1,31 @@ + + +
+ $(MATITA_RT_BASE_DIR) + +
+
+ lib/lambda-delta + xoa_defs + xoa_notation + basics/pts.ma + 2 1 + 2 2 + 3 1 + 3 2 + 3 3 + 4 3 + 4 4 + 5 3 + 5 4 + 6 6 + 7 6 + 3 + 4 +
+ diff --git a/matita/matita/lib/lambda-delta/xoa_props.ma b/matita/matita/lib/lambda-delta/xoa_props.ma new file mode 100644 index 000000000..967656716 --- /dev/null +++ b/matita/matita/lib/lambda-delta/xoa_props.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda-delta/xoa_notation.ma". +include "lambda-delta/xoa_defs.ma". + +lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0. +#A0 #P0 #P1 * /2/ +qed.