X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foptions.ml;h=cdf88c308df83927b8309dc7c227a44f5d6689bf;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=3ac27296dce78667cb9ec589b38ff6463dc84023;hpb=98fef490e55d1d780e8c0bb19de0218e08ae73b1;p=helm.git diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index 3ac27296d..cdf88c308 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -17,66 +17,103 @@ type uri_generator = string -> string type kernel = V4 | V3 | V0 +IFDEF MANAGER THEN + type manager = Quiet | Coq | Matita - | LP1 (* newelpi *) - | LP2 (* newelpi *) - | TJ2 (* teyjus *) - | TJ3 (* teyjus *) + | LP1 (* elpi helena *) + | LP2 (* elpi helena *) + | TJ2 (* teyjus helena *) + | TJ3 (* teyjus helena *) +(* + | CC0 (* elpi cic *) +*) + | LYP (* elpi lyp *) + +END (* interface functions ******************************************************) -let version_string = "Helena 0.8.2 M (June 2015)" +let version_string b = + if b then "Helena 0.8.3 M (December 2017)" + else "Helena 0.8.3 M - December 2017" -let stage = ref 3 (* stage *) +let kernel = ref V3 (* kernel type *) -let trace = ref 0 (* trace level *) +let si = ref false (* use sort inclusion *) -let ct = ref 0 (* current trace level *) +let cover = ref "" (* initial uri segment *) -let summary = ref false (* log summary information *) +let cc = ref false (* activate conversion constraints *) -let xdir = ref "" (* directory for XML output *) +let indexes = ref false (* show de Bruijn indexes *) -let kernel = ref V3 (* kernel type *) +let alpha = ref "" (* prefix of numeric identifiers *) -let si = ref false (* use sort inclusion *) +let first = ref 0 (* begin trace here *) -let cover = ref "" (* initial uri segment *) +let last = ref max_int (* end trace here *) -let cc = ref false (* activate conversion constraints *) +let restricted = ref true (* restricted applications *) -let expand = ref false (* always expand global definitions *) +let infinity = ref false (* use ∞-abstractions in contexts *) -let indexes = ref false (* show de Bruijn indexes *) +let short = ref false (* short global constants *) -let icm = ref 0 (* complexity measure of relocated terms *) +let cast = ref false (* anticipate cast *) -let unquote = ref false (* do not quote identifiers when lexing *) +let root = ref "" (* initial segment of URI hierarchy *) -let debug_parser = ref false (* output parser debug information *) +let trace = ref 0 (* trace level *) +IFDEF LEXER THEN let debug_lexer = ref false (* output lexer debug information *) +END -let manager_dir = ref "" (* output directory for manager *) +IFDEF PARSER THEN +let debug_parser = ref false (* output parser debug information *) +END -let manager = ref Quiet (* manager *) +IFDEF TRACE THEN +let ct = ref 0 (* current trace level *) +END -let preamble = ref "" (* preamble file for manager *) +IFDEF SUMMARY THEN +let summary = ref false (* log summary information *) +END -let alpha = ref "" (* prefix of numeric identifiers *) +IFDEF EXPAND THEN +let expand = ref false (* always expand global definitions *) +END -let first = ref 0 (* begin trace here *) +IFDEF MANAGER THEN +let manager_dir = ref "" (* output directory for manager *) +let manager = ref Quiet (* manager *) +let preamble = ref "" (* preamble file for manager *) +END -let last = ref max_int (* end trace here *) +IFDEF STAGE THEN +let stage = ref 3 (* stage *) +END -let extended = ref false (* extended applications *) +IFDEF OBJECTS THEN +let export = ref false (* export entities to XML *) +let xdir = ref "" (* directory for XML output *) +END -let short = ref false (* short global constants *) +IFDEF PREPROCESS THEN +let preprocess = ref false (* preprocess source *) +END -let set_current_trace n = - ct := if !first <= n && n <= !last then !trace else 0 +IFDEF QUOTE THEN +let quote = ref false (* quote identifiers when lexing *) +END + +IFDEF TYPE THEN +let validate = ref true (* validate vs. typecheck *) +let icm = ref 0 (* complexity measure of relocated terms *) +END let kernel_id () = let id = match !kernel with @@ -85,8 +122,8 @@ let kernel_id () = | V0 -> "Environment_V0" in let si = if !si then "_si" else "" in - let ext = if !extended then "_x" else "" in - id ^ si ^ ext + let rest = if !restricted then "" else "_x" in + id ^ si ^ rest let get_baseuri () = String.concat "/" ["ld:"; kernel_id (); !cover; "" ] @@ -95,9 +132,22 @@ let get_mk_uri () = let bu = get_baseuri () in fun s -> KF.concat bu (s ^ ".ld") +IFDEF TRACE THEN +let set_current_trace n = + ct := if !first <= n && n <= !last then !trace else 0 +END + let clear () = - stage := 3; trace := 0; summary := false; first := 0; last := max_int; - xdir := ""; kernel := V3; si := false; extended := false; cover := ""; - expand := false; indexes := false; icm := 0; unquote := false; short := false; - debug_parser := false; debug_lexer := false; - manager_dir := ""; manager := Quiet + root := ""; first := 0; last := max_int; + kernel := V3; si := false; restricted := true; infinity := false; cast := false; cover := ""; + indexes := false; short := false; trace := 0; + IFDEF LEXER THEN debug_lexer := false ELSE () END; + IFDEF PARSER THEN debug_parser := false ELSE () END; + IFDEF SUMMARY THEN summary := false ELSE () END; + IFDEF EXPAND THEN expand := false ELSE () END; + IFDEF MANAGER THEN manager_dir := ""; manager := Quiet; preamble := "" ELSE () END; + IFDEF STAGE THEN stage := 3 ELSE () END; + IFDEF OBJECTS THEN export := false; xdir := "" ELSE () END; + IFDEF PREPROCESS THEN preprocess := false ELSE () END; + IFDEF QUOTE THEN quote := false ELSE () END; + IFDEF TYPE THEN validate := true; icm := 0 ELSE () END