From: Ferruccio Guidi Date: Tue, 6 Oct 2009 14:46:38 +0000 (+0000) Subject: drg: we added the "positive projection" in environments X-Git-Tag: make_still_working~3367 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ece36f3adcdf55739b4686168b49506439bff2ba;p=helm.git drg: we added the "positive projection" in environments top: we enabled the automath/drg transformation --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 1bf429989..a7c69ab8d 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,17 +1,9 @@ -lib/nUri.cmi: lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi -lib/cps.cmo: -lib/cps.cmx: -lib/share.cmo: -lib/share.cmx: -lib/log.cmi: lib/log.cmo: lib/cps.cmx lib/log.cmi lib/log.cmx: lib/cps.cmx lib/log.cmi lib/time.cmo: lib/log.cmi lib/time.cmx: lib/log.cmx -automath/aut.cmo: -automath/aut.cmx: automath/autProcess.cmi: automath/aut.cmx automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi @@ -25,10 +17,8 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx -common/hierarchy.cmi: common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi -common/output.cmi: common/output.cmo: lib/log.cmi common/output.cmi common/output.cmx: lib/log.cmx common/output.cmi common/entity.cmo: lib/nUri.cmi automath/aut.cmx @@ -164,18 +154,18 @@ toplevel/metaBrg.cmx: toplevel/meta.cmx common/entity.cmx lib/cps.cmx \ toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \ toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \ toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \ - common/library.cmi common/hierarchy.cmi common/entity.cmx dual_rg/drg.cmx \ - lib/cps.cmx basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \ - basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \ - basic_ag/bagType.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \ - automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \ - automath/autLexer.cmx + common/library.cmi common/hierarchy.cmi common/entity.cmx \ + dual_rg/drgAut.cmi dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmi \ + basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \ + basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi basic_ag/bagOutput.cmi \ + basic_ag/bag.cmx automath/autProcess.cmi automath/autParser.cmi \ + automath/autOutput.cmi automath/autLexer.cmx toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \ toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \ toplevel/metaBag.cmx toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx \ - common/library.cmx common/hierarchy.cmx common/entity.cmx dual_rg/drg.cmx \ - lib/cps.cmx basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \ - basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \ - basic_ag/bagType.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \ - automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \ - automath/autLexer.cmx + common/library.cmx common/hierarchy.cmx common/entity.cmx \ + dual_rg/drgAut.cmx dual_rg/drg.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ + basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \ + basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx basic_ag/bagOutput.cmx \ + basic_ag/bag.cmx automath/autProcess.cmx automath/autParser.cmx \ + automath/autOutput.cmx automath/autLexer.cmx diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 19421a032..653898fb2 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -19,24 +19,24 @@ INPUT = automath/grundlagen.aut INPUT-ORIG = automath/grundlagen-orig.aut test: $(MAIN).opt - @echo " HELENA -p -r $(INPUT)" - $(H)./$(MAIN).opt -p -r -S 3 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -o -p -r $(INPUT)" + $(H)./$(MAIN).opt -o -p -r -S 3 $(O) $(INPUT) > etc/log.txt test-si: $(MAIN).opt - @echo " HELENA -p -r -u $(INPUT)" - $(H)./$(MAIN).opt -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -o -p -r -u $(INPUT)" + $(H)./$(MAIN).opt -o -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt test-si-fast: $(MAIN).opt - @echo " HELENA -r -u $(INPUT)" - $(H)./$(MAIN).opt -r -u -S 1 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -o -r -u $(INPUT)" + $(H)./$(MAIN).opt -o -r -u -S 1 $(O) $(INPUT) > etc/log.txt hal: $(MAIN).opt - @echo " HELENA -m $(INPUT)" - $(H)./$(MAIN).opt -m -s 1 -S 1 $(INPUT) > etc/log.txt + @echo " HELENA -o -m $(INPUT)" + $(H)./$(MAIN).opt -o -m -s 1 -S 1 $(INPUT) > etc/log.txt xml-si: $(MAIN).opt - @echo " HELENA -u -x $(INPUT)" - $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > etc/log.txt + @echo " HELENA -o -u -x $(INPUT)" + $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt %.ld: BASEURL = --stringparam baseurl $(LDDLURL) diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index 292b1e921..4a16c77e7 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -24,7 +24,7 @@ type 'term bind = Abst of 'term (* declaration: domain *) type 'term entity = attrs * uri * 'term bind (* attrs, name, binder *) -type 'a uri_generator = (string -> 'a) -> string -> 'a +type uri_generator = string -> string (* this could be in CPS *) (* helpers ******************************************************************) diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml index a30082046..4557aadb3 100644 --- a/helm/software/lambda-delta/dual_rg/drg.ml +++ b/helm/software/lambda-delta/dual_rg/drg.ml @@ -20,35 +20,36 @@ type bind = Abst of term list (* domains *) | Abbr of term list (* bodies *) | Void of int (* number of exclusions *) -and term = Sort of attrs * int (* attrs, hierarchy index *) - | LRef of attrs * int * int (* attrs, position indexes *) - | GRef of attrs * uri (* attrs, reference *) - | Cast of attrs * term * term (* attrs, domain, element *) - | Appl of attrs * term list * term (* attrs, arguments, function *) - | Proj of attrs * lenv * term (* attrs, closure, member *) - | Bind of attrs * bind * term (* attrs, binder, scope *) - -and lenv = Null - | Cons of lenv * attrs * bind (* closure, attrs, binder *) +and term = TSort of attrs * int (* attrs, hierarchy index *) + | TLRef of attrs * int * int (* attrs, position indexes *) + | TGRef of attrs * uri (* attrs, reference *) + | TCast of attrs * term * term (* attrs, domain, element *) + | TAppl of attrs * term list * term (* attrs, arguments, function *) + | TProj of attrs * lenv * term (* attrs, closure, member *) + | TBind of attrs * bind * term (* attrs, binder, scope *) + +and lenv = ESort (* top *) + | EProj of lenv * attrs * lenv (* environment, attrs, closure *) + | EBind of lenv * attrs * bind (* environment, attrs, binder *) type entity = term Entity.entity (* helpers ******************************************************************) -let mk_uri root f s = - let str = String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] in - f str +let mk_uri root s = + String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"] -let empty_lenv = Null +let empty_lenv = ESort -let push f lenv a b = f (Cons (lenv, a, b)) +let push f lenv a b = f (EBind (lenv, a, b)) let resolve_lref err f id lenv = let rec aux f i k = function - | Null -> err () - | Cons (tl, a, _) -> + | ESort -> err () + | EBind (tl, a, _) -> let err kk = aux f (succ i) (k + kk) tl in let f j = f i j k in Entity.resolve err f id a + | EProj _ -> assert false (* TODO *) in aux f 0 0 lenv diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml index b6d8b166c..3e1944408 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.ml +++ b/helm/software/lambda-delta/dual_rg/drgAut.ml @@ -25,14 +25,14 @@ type environment = context H.t type context_node = qid option (* context node: None = root *) -type 'a status = { +type status = { henv: environment; (* optimized global environment *) path: D.id list; (* current section path *) hcnt: environment; (* optimized context *) node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) - mk_uri:'a Y.uri_generator (* uri generator *) + mk_uri:Y.uri_generator (* uri generator *) } type resolver = Local of int @@ -55,7 +55,7 @@ let add_abst (a, ws) id w = let lenv_of_cnt (a, ws) = D.push C.start D.empty_lenv a (D.Abst ws) -let mk_lref f i j k = f (D.LRef ([Y.Apix k], i, j)) +let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j)) let id_of_name (id, _, _) = id @@ -63,7 +63,7 @@ let mk_qid f st id path = let str = String.concat "/" path in let str = Filename.concat str id in let f str = f (U.uri_of_string str, id, path) in - st.mk_uri f str + f (st.mk_uri str) let uri_of_qid (uri, _, _) = uri @@ -107,16 +107,16 @@ let get_cnt_relaxed f st = let rec xlate_term f st lenv = function | A.Sort s -> - let f h = f (D.Sort ([], h)) in + let f h = f (D.TSort ([], h)) in if s then f 0 else f 1 | A.Appl (v, t) -> - let f vv tt = f (D.Appl ([], [vv], tt)) in + let f vv tt = f (D.TAppl ([], [vv], tt)) in let f vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | A.Abst (name, w, t) -> let f ww = let a, b = [Y.Name (name, true)], (D.Abst [ww]) in - let f tt = f (D.Bind (a, b, tt)) in + let f tt = f (D.TBind (a, b, tt)) in let f lenv = xlate_term f st lenv t in D.push f lenv a b in @@ -129,7 +129,7 @@ let rec xlate_term f st lenv = function | _ -> assert false in let f tail = - let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in + let f args = f (D.TAppl ([], args, D.TGRef ([], uri_of_qid qid))) in let f a = C.list_rev_map_append f map2 a ~tail in C.list_sub_strict f a args in @@ -173,7 +173,7 @@ let xlate_entity err f st = function let f qid = let f ww = H.add st.henv (uri_of_qid qid) cnt; - let b = Y.Abst (D.Bind (a, D.Abst ws, ww)) in + let b = Y.Abst (D.TBind (a, D.Abst ws, ww)) in let entity = [Y.Mark st.line], uri_of_qid qid, b in f {st with line = succ st.line} entity in @@ -189,7 +189,7 @@ let xlate_entity err f st = function let f qid = let f ww vv = H.add st.henv (uri_of_qid qid) cnt; - let b = Y.Abbr (D.Bind (a, D.Abst ws, D.Cast ([], ww, vv))) in + let b = Y.Abbr (D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))) in let a = if trans then [Y.Mark st.line] else [Y.Mark st.line; Y.Priv] in diff --git a/helm/software/lambda-delta/dual_rg/drgAut.mli b/helm/software/lambda-delta/dual_rg/drgAut.mli index 1133f20bd..5de7f7e85 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.mli +++ b/helm/software/lambda-delta/dual_rg/drgAut.mli @@ -9,9 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type 'a status +type status -val initial_status: 'a Entity.uri_generator -> 'a status +val initial_status: Entity.uri_generator -> status -val drg_of_aut: ('a status -> 'a) -> ('a status -> Drg.entity -> 'a) -> - 'a status -> Aut.entity -> 'a +val drg_of_aut: (status -> 'a) -> (status -> Drg.entity -> 'a) -> + status -> Aut.entity -> 'a diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml index f6782d556..c291cbf8a 100644 --- a/helm/software/lambda-delta/dual_rg/drgOutput.ml +++ b/helm/software/lambda-delta/dual_rg/drgOutput.ml @@ -16,33 +16,34 @@ let rec list_iter map l f = match l with | [] -> f | hd :: tl -> map hd (list_iter map tl f) -let rec lenv_iter map l f = match l with - | D.Null -> f - | D.Cons (lenv, a, b) -> lenv_iter map lenv (map a b f) +let rec lenv_iter map1 map2 l f = match l with + | D.ESort -> f + | D.EBind (lenv, a, b) -> lenv_iter map1 map2 lenv (map1 a b f) + | D.EProj (lenv, a, e) -> lenv_iter map1 map2 lenv (map2 a e f) let rec exp_term t f = match t with - | D.Sort (a, h) -> + | D.TSort (a, h) -> let attrs = [X.position h; X.name a] in X.tag X.sort attrs f - | D.LRef (a, i, j) -> + | D.TLRef (a, i, j) -> let attrs = [X.position i; X.offset j; X.name a] in X.tag X.lref attrs f - | D.GRef (a, n) -> + | D.TGRef (a, n) -> let attrs = [X.uri n; X.name a] in X.tag X.gref attrs f - | D.Cast (a, u, t) -> + | D.TCast (a, u, t) -> let attrs = [] in X.tag X.cast attrs (exp_term t f) ~contents:(exp_term u) - | D.Appl (a, vs, t) -> + | D.TAppl (a, vs, t) -> let attrs = [X.arity (List.length vs)] in X.tag X.appl attrs (exp_term t f) ~contents:(list_iter exp_term vs) - | D.Proj (a, lenv, t) -> + | D.TProj (a, lenv, t) -> let attrs = [] in - X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_lenv lenv) - | D.Bind (a, b, t) -> - exp_lenv a b (exp_term t f) + X.tag X.proj attrs (exp_term t f) ~contents:(lenv_iter exp_bind exp_eproj lenv) + | D.TBind (a, b, t) -> + exp_bind a b (exp_term t f) -and exp_lenv a b f = match b with +and exp_bind a b f = match b with | D.Abst ws -> let attrs = [X.name a; X.mark a; X.arity (List.length ws)] in X.tag X.abst attrs f ~contents:(list_iter exp_term ws) @@ -53,4 +54,8 @@ and exp_lenv a b f = match b with let attrs = [X.name a; X.mark a; X.arity n] in X.tag X.void attrs f +and exp_eproj a lenv f = + let attrs = [] in + X.tag X.proj attrs f ~contents:(lenv_iter exp_bind exp_eproj lenv) + let export_term = exp_term diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index ff35879ff..3556db37a 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -20,7 +20,7 @@ module Y = Entity module X = Library module AP = AutProcess module AO = AutOutput -(* module DA = DrgAut *) +module DA = DrgAut module MA = MetaAut module MO = MetaOutput module ML = MetaLibrary @@ -33,9 +33,9 @@ module BagO = BagOutput module BagT = BagType module BagU = BagUntrusted -type 'a status = { +type status = { ast : AP.status; -(* dst : 'a DA.status; *) + dst : DA.status; mst : MA.status; ac : AO.counters; mc : MO.counters; @@ -49,7 +49,7 @@ let initial_status mk_uri cover = { brgc = BrgO.initial_counters; bagc = BagO.initial_counters; mst = MA.initial_status ~cover (); -(* dst = DA.initial_status (mk_uri cover); *) + dst = DA.initial_status (mk_uri cover); ast = AP.initial_status } @@ -74,7 +74,7 @@ type kernel = Brg | Bag type kernel_entity = BrgEntity of Brg.entity | BagEntity of Bag.entity -(* | DrgEntity of Drg.entity *) + | DrgEntity of Drg.entity | MetaEntity of Meta.entity let kernel = ref Brg @@ -94,7 +94,7 @@ let count_entity st = function | MetaEntity e -> {st with mc = count MO.count_entity st.mc e} | BrgEntity e -> {st with brgc = count BrgO.count_entity st.brgc e} | BagEntity e -> {st with bagc = count BagO.count_entity st.bagc e} -(* | _ -> st *) + | _ -> st let export_entity si g moch = function | BrgEntity e -> X.old_export_entity BrgO.export_term si g e @@ -111,7 +111,7 @@ let type_check f st si g k = match k with | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity | BagEntity entity -> BagU.type_check ok ~si g entity -(* | DrgEntity (a, u, _) *) + | DrgEntity (a, u, _) | MetaEntity (a, u, _) -> f st a u (****************************************************************************) @@ -120,13 +120,13 @@ let stage = ref 3 let moch = ref None let meta = ref false let progress = ref false -let process = ref false +let preprocess = ref false let use_cover = ref true let si = ref false let cc = ref false let export = ref false let graph = ref (H.graph_of_string C.err C.start "Z2") -let old = ref true +let old = ref false let process_3 f st a u = if !progress then @@ -147,29 +147,30 @@ let process_1 f st entity = export_entity !si !graph !moch entity; if !stage > 1 then xlate (process_2 f) st entity else f st -let rec process_0 f st = function +let process_0 f st entity = + let f st entity = + if !stage = 0 then f st else + let frr mst = f {st with mst = mst} in + let h mst e = process_1 f {st with mst = mst} (MetaEntity e) in + let err dst = f {st with dst = dst} in + let g dst e = process_1 f {st with dst = dst} (DrgEntity e) in + if !old then MA.meta_of_aut frr h st.mst entity else + DA.drg_of_aut err g st.dst entity + in + let st = {st with ac = count AO.count_entity st.ac entity} in + if !preprocess then process_entity f st entity else f st entity + +let rec process f book st = match book with | [] -> f st - | entity :: tl -> - let f st = process_0 f st tl in - let frr st mst = {st with mst = mst} in - let h st mst e = - process_1 C.start {st with mst = mst} (MetaEntity e) - in - let f st entity = - if !stage = 0 then f st else -(* let err st dst = f {st with dst = dst} in - let g st dst e = process_1 f {st with dst = dst} (DrgEntity e) in - if !old then *) f (MA.meta_of_aut (frr st) (h st) st.mst entity) (* else - DA.drg_of_aut (err st) (g st) st.dst entity *) - in - let st = {st with ac = count AO.count_entity st.ac entity} in - if !process then process_entity f st entity else f st entity + | entity :: tl -> + process f tl (process_0 C.start st entity) +(* process_0 (process f tl) st entity *) (* CPS variant of the above *) (****************************************************************************) let main = try - let version_string = "Helena 0.8.1 M - September 2009" in + let version_string = "Helena 0.8.1 M - October 2009" in let set_hierarchy s = let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in let f g = graph := g in @@ -208,12 +209,12 @@ try let f st = if !L.level > 0 then T.utime_stamp "processed"; if !L.level > 2 then AO.print_counters C.start st.ac; - if !L.level > 2 && !process then AO.print_process_counters C.start st.ast; + if !L.level > 2 && !preprocess then AO.print_process_counters C.start st.ast; if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc; if !L.level > 2 && !stage > 1 then print_counters st; if !L.level > 2 && !stage > 1 then O.print_reductions () in - process_0 f (initial_status Drg.mk_uri cover) book + process f book (initial_status Drg.mk_uri cover) in let exit () = close !moch; @@ -221,7 +222,7 @@ try flush_all () in let help = - "Usage: helena [ -Vcijmpux | -Ss | -hk ] ...\n\n" ^ + "Usage: helena [ -Vcijmopux | -Ss | -hk ] ...\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" @@ -235,6 +236,7 @@ try let help_j = " show URI of processed kernel objects" in let help_k = " set kernel version (default: brg)" in let help_m = " output intermediate representation (HAL)" in + let help_o = " use old abstract language instead of drg" in let help_p = " preprocess Automath source" in let help_r = " disable initial segment of URI hierarchy" in let help_s = " set translation stage (see above)" in @@ -252,7 +254,8 @@ try ("-j", Arg.Set progress, help_j); ("-k", Arg.String set_kernel, help_k); ("-m", Arg.Set meta, help_m); - ("-p", Arg.Set process, help_p); + ("-o", Arg.Set old, help_o); + ("-p", Arg.Set preprocess, help_p); ("-r", Arg.Clear use_cover, help_r); ("-s", Arg.Int set_stage, help_s); ("-u", Arg.Set si, help_u);