include Makefile.common
+HOME = .
+
INPUT = examples/grundlagen/grundlagen.aut
test-si: $(MAIN).opt
hal: $(MAIN).opt
@echo " HELENA -o -x -m $(INPUT)"
- $(H)./$(MAIN).opt -o -x -m -s 1 -S 1 $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -o -x $(HOME) -m -s 1 -S 1 $(INPUT) > etc/log.txt
xml-si: $(MAIN).opt
@echo " HELENA -u -x -s 2 $(INPUT)"
- $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt
xml-si-crg: $(MAIN).opt
@echo " HELENA -u -x -s 1 $(INPUT)"
- $(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -u -x $(HOME) -s 1 -S 1 $(INPUT) > etc/log.txt
%.ld: BASEURL = --stringparam baseurl $(LDDLURL)
xml-si-old: $(MAIN).opt
@echo " HELENA -o -u -x -s 2 $(INPUT)"
- $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -o -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt
let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
-let path_of_uri uri =
+let path_of_uri xdir uri =
+ let base = F.concat xdir base in
F.concat base (Str.string_after (U.string_of_uri uri) 3)
(* interface functions ******************************************************)
let f i = "mark", string_of_int i in
Y.mark err f a
-let export_entity pp_term si (a, u, b) =
- let path = path_of_uri u in
+let export_entity pp_term si xdir (a, u, b) =
+ let path = path_of_uri xdir u in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
let och = open_out (path ^ obj_ext) in
let out = output_string och in
type pp = och -> int -> unit
val export_entity:
- ('term -> pp) -> bool -> 'term Entity.entity -> unit
+ ('term -> pp) -> bool -> string -> 'term Entity.entity -> unit
val tag: string -> attr list -> ?contents:pp -> pp
let xlate_entity err f st = function
| T.Require _ ->
err st
- | T.Graph id ->
- assert (H.set_graph id); err st
+ | T.Section (Some name) ->
+ err {st with path = name :: st.path}
+ | T.Section None ->
+ begin match st.path with
+ | _ :: ptl ->
+ err {st with path = ptl}
+ | _ -> assert false
+ end
| T.Sorts sorts ->
let map st (xix, s) =
let ix = match xix with
{st with sort = H.set_sorts ix [s]}
in
err (List.fold_left map st sorts)
- | T.Section (Some name) ->
- err {st with path = name :: st.path}
- | T.Section None ->
- begin match st.path with
- | _ :: ptl ->
- err {st with path = ptl}
- | _ -> assert false
- end
+ | T.Graph id ->
+ assert (H.set_graph id); err st
| T.Entity (kind, id, meta, t) ->
let uri = uri_of_id st id st.path in
Hashtbl.add henv id uri;
let a = if meta <> "" then Y.Meta meta :: a else a in
let entity = Y.Mark st.line :: a, uri, b in
f {st with line = succ st.line} entity
+ | T.Generate _ ->
+ err st
(* Interface functions ******************************************************)
\def "logical implication"
Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
- \decl "logical comprehension" All: (*Obj -> *Prop) -> *Prop
+\* comprehension and dependent abstraction are isomorphic *\
+ \def "unrestricted logical comprehension"
+ All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
- \decl "logical existence" Ex: (*Obj -> *Prop) -> *Prop
+ \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
\decl "syntactical identity" Id: *Obj => *Obj -> *Prop
\def "logical equivalence"
Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
- \def "logical strict existence"
+ \def "unrestricted strict logical existence"
EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
: (*Obj -> *Prop) -> *Prop
+HOME = ../..
ROOT = exp_math
+HELENAOPTS = -r $(ROOT) -u
H = @
-HELENA = ../../helena.opt
+HELENA = $(HOME)/helena.opt
HLNS = $(shell cat Make)
all: $(HLNS)
- @echo " HELENA -r $(ROOT)"
- $(H)$(HELENA) -r $(ROOT) -u $^
+ @echo " HELENA -u"
+ $(H)$(HELENA) $(HELENAOPTS) $^
progress: $(HLNS)
- @echo " HELENA -r $(ROOT) -j"
- $(H)$(HELENA) -r $(ROOT) -j -u $^
+ @echo " HELENA -u -j"
+ $(H)$(HELENA) $(HELENAOPTS) -j $^
xml: $(HLNS)
- @echo " HELENA -r $(ROOT) -x"
- $(H)$(HELENA) -r $(ROOT) -x -s 2 $^
+ @echo " HELENA -u -x"
+ $(H)$(HELENA) $(HELENAOPTS) -x $(HOME) -s 2 $^
xml-crg: $(HLNS)
- @echo " HELENA -r $(ROOT) -x"
- $(H)$(HELENA) -r $(ROOT) -x -s 1 $^
+ @echo " HELENA -u -x"
+ $(H)$(HELENA) $(HELENAOPTS) -x $(HOME) -s 1 $^
\close
-\open logical_abbreviations \* [1] 2.3. *\
+\open logical_abbreviations \* [1] 2.3. 2.5. *\
+
+ \def "logical comprehension restricted to classifications"
+ CAll = [q:*Obj->*Prop] [x:*Obj] Cl(x) -> q(x)
+ : (*Obj -> *Prop) -> *Prop
+
+ \def "logical existence restricted to classifications"
+ CEx = [q:*Obj->*Prop] Ex([x:*Obj] And(Cl(x), q(x)))
+ : (*Obj -> *Prop) -> *Prop
+
+ \def "logical comprehension restricted to a classification"
+ EAll = [a:*Obj, q:*Obj->*Prop] [x:*Obj] Eta(x, a) -> q(x)
+ : *Obj => (*Obj -> *Prop) -> *Prop
+
+ \def "logical existence restricted to a classification"
+ EEx = [a:*Obj, q:*Obj->*Prop] Ex([x:*Obj] And(Eta(x, a), q(x)))
+ : *Obj => (*Obj -> *Prop) -> *Prop
+
+\close
+
+\open non_logical_abbreviations \* [1] 2.4. *\
+
+ \def "convergence of a term to an object"
+ Conv = [t:*Term] EX([y:*Obj] E(t, y)) : *Term -> *Prop
+
+ \def "term-term equivalence"
+ Eq = [t1:*Term, t2:*Term] [y:*Obj] Iff(E(t1, y), E(t2, y))
+ : *Term => *Term -> *Prop
\close
-\* Systematic Explicit Mathematics *\
-\* [1] F. Feferman: *\
+\* Systematic Explicit Mathematics
+ * [1] F. Feferman: A language and axioms for explicit mathematics.
+ * Lecture Notes in Mathematics, 450. Springer (1975). pp 87-139.
+ *\
\* Development started: 2010 Feb 20 *\
| Sorts of (int option * id) list (* sorts: index, name *)
| Section of id option (* section: Some id = open, None = close last *)
| Entity of kind * id * desc * term (* entity: class, name, description, contents *)
+ | Generate of term list (* predefined generated entity: arguments *)
+
| BS QT { "\"" ^ qstring lexbuf }
| _ { Lexing.lexeme lexbuf ^ qstring lexbuf }
and token = parse
- | SPC { token lexbuf }
- | OC { block_comment lexbuf; token lexbuf }
- | ID as id { out "ID"; P.ID id }
- | IX as ix { out "IX"; P.IX (int_of_string ix) }
- | QT { let s = qstring lexbuf in out "STR"; P.STR s }
- | "\\require" { out "REQUIRE"; P.REQUIRE }
- | "\\graph" { out "GRAPH"; P.GRAPH }
- | "\\decl" { out "DECL"; P.DECL }
- | "\\ax" { out "AX"; P.AX }
- | "\\def" { out "DEF"; P.DEF }
- | "\\th" { out "TH"; P.TH }
- | "\\open" { out "OPEN"; P.OPEN }
- | "\\close" { out "CLOSE"; P.CLOSE }
- | "\\sorts" { out "SORTS"; P.SORTS }
- | "(" { out "OP"; P.OP }
- | ")" { out "CP"; P.CP }
- | "[" { out "OB"; P.OB }
- | "]" { out "CB"; P.CB }
- | "<" { out "OA"; P.OA }
- | ">" { out "CA"; P.CA }
- | "." { out "FS"; P.FS }
- | ":" { out "CN"; P.CN }
- | "," { out "CM"; P.CM }
- | "=" { out "EQ"; P.EQ }
- | "*" { out "STAR"; P.STAR }
- | "#" { out "HASH"; P.HASH }
- | "+" { out "PLUS"; P.PLUS }
- | "~" { out "TE"; P.TE }
- | "->" { out "WTO"; P.WTO }
- | "=>" { out "STO"; P.STO }
- | eof { out "EOF"; P.EOF }
+ | SPC { token lexbuf }
+ | OC { block_comment lexbuf; token lexbuf }
+ | ID as id { out "ID"; P.ID id }
+ | IX as ix { out "IX"; P.IX (int_of_string ix) }
+ | QT { let s = qstring lexbuf in out "STR"; P.STR s }
+ | "\\graph" { out "GRAPH"; P.GRAPH }
+ | "\\decl" { out "DECL"; P.DECL }
+ | "\\ax" { out "AX"; P.AX }
+ | "\\def" { out "DEF"; P.DEF }
+ | "\\th" { out "TH"; P.TH }
+ | "\\generate" { out "GEN"; P.GEN }
+ | "\\require" { out "REQ"; P.REQ }
+ | "\\open" { out "OPEN"; P.OPEN }
+ | "\\close" { out "CLOSE"; P.CLOSE }
+ | "\\sorts" { out "SORTS"; P.SORTS }
+ | "(" { out "OP"; P.OP }
+ | ")" { out "CP"; P.CP }
+ | "[" { out "OB"; P.OB }
+ | "]" { out "CB"; P.CB }
+ | "<" { out "OA"; P.OA }
+ | ">" { out "CA"; P.CA }
+ | "." { out "FS"; P.FS }
+ | ":" { out "CN"; P.CN }
+ | "," { out "CM"; P.CM }
+ | "=" { out "EQ"; P.EQ }
+ | "*" { out "STAR"; P.STAR }
+ | "#" { out "HASH"; P.HASH }
+ | "+" { out "PLUS"; P.PLUS }
+ | "~" { out "TE"; P.TE }
+ | "->" { out "WTO"; P.WTO }
+ | "=>" { out "STO"; P.STO }
+ | eof { out "EOF"; P.EOF }
%token <int> IX
%token <string> ID STR
%token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO
- %token REQUIRE GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF
+ %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
%type <Txt.command option * bool> entry
| TH { T.Th }
;
xentity:
- | REQUIRE ids
- { Some (T.Require $2) }
| GRAPH ID
{ Some (T.Graph $2) }
| decl comment ID CN term
{ Some (T.Entity ($1, $3, $2, $5)) }
| def comment ID EQ term CN term
{ Some (T.Entity ($1, $3, $2, T.Cast ($7, $5))) }
+ | GEN term
+ { Some (T.Generate [$2]) }
+ | GEN terms
+ { Some (T.Generate $2) }
+ | REQ ids
+ { Some (T.Require $2) }
| OPEN ID
{ Some (T.Section (Some $2)) }
| CLOSE
{ None }
;
start:
- | GRAPH {} | decl {} | def {}
- | REQUIRE {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+ | GRAPH {} | decl {} | def {} | GEN {} |
+ | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
;
entry:
| xentity { $1, false }
| BagEntity e -> {st with bagc = BagO.count_entity C.start st.bagc e}
| _ -> st
-let export_entity si moch = function
- | CrgEntity e -> X.export_entity DO.export_term si e
- | BrgEntity e -> X.export_entity BrgO.export_term si e
+let export_entity si xdir moch = function
+ | CrgEntity e -> X.export_entity DO.export_term si xdir e
+ | BrgEntity e -> X.export_entity BrgO.export_term si xdir e
| MetaEntity e ->
begin match moch with
| None -> ()
let preprocess = ref false
let root = ref ""
let cc = ref false
-let export = ref false
+let export = ref ""
let old = ref false
let st = ref (initial_status ())
let process_2 st entity =
let st = if !L.level > 2 then count_entity st entity else st in
- if !export then export_entity !O.si !moch entity;
+ if !export <> "" then export_entity !O.si !export !moch entity;
if !stage > 2 then type_check st entity else st
let process_1 st entity =
if !progress then pp_progress entity;
let st = if !L.level > 2 then count_entity st entity else st in
- if !export && !stage = 1 then export_entity !O.si !moch entity;
+ if !export <> "" && !stage = 1 then export_entity !O.si !export !moch entity;
if !stage > 1 then process_2 st (xlate_entity entity) else st
let process_0 st entity =
let f och = moch := Some och in
ML.open_out f name
in
+ let set_xdir s = export := s in
let set_root s = root := s in
let close = function
| None -> ()
in
let clear_options () =
stage := 3; moch := None; meta := false; progress := false;
- preprocess := false; root := ""; cc := false; export := false;
+ preprocess := false; root := ""; cc := false; export := "";
old := false; kernel := Brg; st := initial_status ();
L.clear (); O.clear (); H.clear (); Op.clear_reductions ()
in
flush_all ()
in
let help =
- "Usage: helena [ -VXcgijmopqux | -Ss <number> | -hkr <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -VXcgijmopqu | -Ss <number> | -x <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
"Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
3 data information, 4 typing information, 5 reduction information\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
let help_r = "<string> set initial segment of URI hierarchy" in
let help_s = "<number> set translation stage (see above)" in
let help_u = " activate sort inclusion" in
- let help_x = " export kernel entities (XML)" in
+ let help_x = "<dir> export kernel entities (XML) to <dir>" in
L.box 0; L.box_err ();
at_exit exit;
Arg.parse [
("-r", Arg.String set_root, help_r);
("-s", Arg.Int set_stage, help_s);
("-u", Arg.Set O.si, help_u);
- ("-x", Arg.Set export, help_x)
+ ("-x", Arg.String set_xdir, help_x)
] process_file help;
with BagT.TypeError msg -> bag_error "Type Error" msg
projects / helm.git / commitdiff