--- /dev/null
+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)
--- /dev/null
+EXEC = xoa
+VERSION=0.2.0
+
+REQUIRES = helm-grafite
+
+include ../Makefile.common
--- /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_______________________________________________________________ *)
+
+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
--- /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 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
--- /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 generate: out_channel -> out_channel -> Ast.directive -> unit
--- /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 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
--- /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 get_preamble: string -> string
+
+val open_out: string -> string -> out_channel
+
+val out_include: out_channel -> string -> unit
--- /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 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 [ <configuration file> ]*\n" in
+ Arg.parse [] process help
--- /dev/null
+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)
*)
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 *************************************************************)
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="matita">
+ <key name="rt_base_dir">$(MATITA_RT_BASE_DIR)</key>
+<!--
+ <key name="system">false</key>
+ <key name="map_unicode_to_tex">false</key>
+ <key name="do_heavy_checks">true</key>
+ <key name="include_path">lib</key>
+-->
+ </section>
+ <section name="xoa">
+ <key name="output_dir">lib/lambda-delta</key>
+ <key name="objects">xoa_defs</key>
+ <key name="notations">xoa_notation</key>
+ <key name="include">basics/pts.ma</key>
+ <key name="ex">2 1</key>
+ <key name="ex">2 2</key>
+ <key name="ex">3 1</key>
+ <key name="ex">3 2</key>
+ <key name="ex">3 3</key>
+ <key name="ex">4 3</key>
+ <key name="ex">4 4</key>
+ <key name="ex">5 3</key>
+ <key name="ex">5 4</key>
+ <key name="ex">6 6</key>
+ <key name="ex">7 6</key>
+ <key name="or">3</key>
+ <key name="or">4</key>
+ </section>
+</helm_registry>
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
projects / helm.git / commitdiff