From: Ferruccio Guidi Date: Tue, 23 Feb 2010 12:00:26 +0000 (+0000) Subject: - the text model now supports invocations of the entity generator (to X-Git-Tag: make_still_working~3028 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55d6dde568f1daf1fa6902428bda7caec147375a;p=helm.git - the text model now supports invocations of the entity generator (to be implemented) - the XML objects can be exported to a specified directory (via the -x command line option) --- diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index aeb161c90..1ea4aa7b9 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -15,6 +15,8 @@ XMLS = xml/brg-si/grundlagen/l/not.ld.xml \ include Makefile.common +HOME = . + INPUT = examples/grundlagen/grundlagen.aut test-si: $(MAIN).opt @@ -32,15 +34,15 @@ profile: $(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) @@ -85,4 +87,4 @@ test-si-fast-old: $(MAIN).opt 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 diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml index 75afcc52d..91272c6f8 100644 --- a/helm/software/lambda-delta/common/library.ml +++ b/helm/software/lambda-delta/common/library.ml @@ -25,7 +25,8 @@ let root = "ENTITY" 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 ******************************************************) @@ -105,8 +106,8 @@ let mark a = 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 diff --git a/helm/software/lambda-delta/common/library.mli b/helm/software/lambda-delta/common/library.mli index 97a969219..74c9fb424 100644 --- a/helm/software/lambda-delta/common/library.mli +++ b/helm/software/lambda-delta/common/library.mli @@ -16,7 +16,7 @@ type attr = string * string 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 diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.ml b/helm/software/lambda-delta/complete_rg/crgTxt.ml index 8089c79e2..e0f5feb1a 100644 --- a/helm/software/lambda-delta/complete_rg/crgTxt.ml +++ b/helm/software/lambda-delta/complete_rg/crgTxt.ml @@ -113,8 +113,14 @@ let mk_contents tt = function 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 @@ -124,14 +130,8 @@ let xlate_entity err f st = function {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; @@ -143,6 +143,8 @@ let xlate_entity err f st = function 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 ******************************************************) diff --git a/helm/software/lambda-delta/examples/exp_math/L.hln b/helm/software/lambda-delta/examples/exp_math/L.hln index 28f3bff23..55b96e6c9 100644 --- a/helm/software/lambda-delta/examples/exp_math/L.hln +++ b/helm/software/lambda-delta/examples/exp_math/L.hln @@ -14,9 +14,11 @@ \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 @@ -30,7 +32,7 @@ \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 diff --git a/helm/software/lambda-delta/examples/exp_math/Makefile b/helm/software/lambda-delta/examples/exp_math/Makefile index 93ea22279..9e7ed164e 100644 --- a/helm/software/lambda-delta/examples/exp_math/Makefile +++ b/helm/software/lambda-delta/examples/exp_math/Makefile @@ -1,23 +1,25 @@ +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 $^ diff --git a/helm/software/lambda-delta/examples/exp_math/T0.hln b/helm/software/lambda-delta/examples/exp_math/T0.hln index a1366dc7d..aab161e0e 100644 --- a/helm/software/lambda-delta/examples/exp_math/T0.hln +++ b/helm/software/lambda-delta/examples/exp_math/T0.hln @@ -19,7 +19,34 @@ \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 diff --git a/helm/software/lambda-delta/examples/exp_math/preamble.hln b/helm/software/lambda-delta/examples/exp_math/preamble.hln index 7d80ba4fa..0c25d4c57 100644 --- a/helm/software/lambda-delta/examples/exp_math/preamble.hln +++ b/helm/software/lambda-delta/examples/exp_math/preamble.hln @@ -1,5 +1,7 @@ -\* 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 *\ diff --git a/helm/software/lambda-delta/text/txt.ml b/helm/software/lambda-delta/text/txt.ml index ca32a9150..dbcc0675c 100644 --- a/helm/software/lambda-delta/text/txt.ml +++ b/helm/software/lambda-delta/text/txt.ml @@ -39,3 +39,5 @@ type command = Require of id list (* required files: names *) | 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 *) + diff --git a/helm/software/lambda-delta/text/txtLexer.mll b/helm/software/lambda-delta/text/txtLexer.mll index d42629713..073fabcba 100644 --- a/helm/software/lambda-delta/text/txtLexer.mll +++ b/helm/software/lambda-delta/text/txtLexer.mll @@ -38,34 +38,35 @@ and qstring = parse | 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 } diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly index 05af001e7..6aafbb551 100644 --- a/helm/software/lambda-delta/text/txtParser.mly +++ b/helm/software/lambda-delta/text/txtParser.mly @@ -33,7 +33,7 @@ %token IX %token 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 entry @@ -123,8 +123,6 @@ | TH { T.Th } ; xentity: - | REQUIRE ids - { Some (T.Require $2) } | GRAPH ID { Some (T.Graph $2) } | decl comment ID CN term @@ -133,6 +131,12 @@ { 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 @@ -143,8 +147,8 @@ { None } ; start: - | GRAPH {} | decl {} | def {} - | REQUIRE {} | OPEN {} | CLOSE {} | SORTS {} | EOF {} + | GRAPH {} | decl {} | def {} | GEN {} | + | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {} ; entry: | xentity { $1, false } diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 865271a4a..85587e8d8 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -121,9 +121,9 @@ let count_entity st = function | 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 -> () @@ -211,19 +211,19 @@ let progress = ref false 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 = @@ -275,6 +275,7 @@ try 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 -> () @@ -282,7 +283,7 @@ try 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 @@ -318,7 +319,7 @@ try flush_all () in let help = - "Usage: helena [ -VXcgijmopqux | -Ss | -hkr ] ...\n\n" ^ + "Usage: helena [ -VXcgijmopqu | -Ss | -x | -hkr ]* [ ]*\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" @@ -340,7 +341,7 @@ try let help_r = " set initial segment of URI hierarchy" in let help_s = " set translation stage (see above)" in let help_u = " activate sort inclusion" in - let help_x = " export kernel entities (XML)" in + let help_x = " export kernel entities (XML) to " in L.box 0; L.box_err (); at_exit exit; Arg.parse [ @@ -360,6 +361,6 @@ try ("-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