From 6753156ae1618ef3fc7ff401808f769abd9eb03d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 28 Oct 2009 19:27:29 +0000 Subject: [PATCH] - lambda-delta: some fixes: now the grundlagen type-checkes through dual_rg - matita/Makefile: we removed LAMBDA-TYPES from the nightly tests (too slow ???) --- helm/software/lambda-delta/.depend.opt | 10 ---- helm/software/lambda-delta/common/entity.ml | 2 + helm/software/lambda-delta/dual_rg/drg.ml | 5 +- helm/software/lambda-delta/dual_rg/drgAut.ml | 24 +++++++-- helm/software/lambda-delta/dual_rg/drgBrg.ml | 9 ++-- .../lambda-delta/dual_rg/drgOutput.ml | 52 ++++++++++++++++++- .../lambda-delta/dual_rg/drgOutput.mli | 2 + helm/software/lambda-delta/toplevel/top.ml | 22 +++++--- helm/software/matita/Makefile | 2 +- 9 files changed, 100 insertions(+), 28 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 0aed7ab22..5335eac4f 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 diff --git a/helm/software/lambda-delta/common/entity.ml b/helm/software/lambda-delta/common/entity.ml index 3aa1ef6b5..7b8dab950 100644 --- a/helm/software/lambda-delta/common/entity.ml +++ b/helm/software/lambda-delta/common/entity.ml @@ -28,6 +28,8 @@ type uri_generator = string -> string (* this could be in CPS *) (* helpers ******************************************************************) +let common f (a, u, _) = f a u + let rec name err f = function | Name (n, r) :: _ -> f n r | _ :: tl -> name err f tl diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml index ac4021c08..b20bdb3d3 100644 --- a/helm/software/lambda-delta/dual_rg/drg.ml +++ b/helm/software/lambda-delta/dual_rg/drg.ml @@ -57,7 +57,7 @@ let resolve_lref err f id lenv = | ESort -> err () | EBind (tl, a, _) -> let err kk = aux f (succ i) (k + kk) tl in - let f j = f i j k in + let f j = f i j (k + j) in Entity.resolve err f id a | EProj _ -> assert false (* TODO *) in @@ -65,6 +65,9 @@ let resolve_lref err f id lenv = let rec get_name err f i j = function | ESort -> err i + | EBind (tl, a, Abst []) -> get_name err f i j tl + | EBind (tl, a, Abbr []) -> get_name err f i j tl + | EBind (tl, a, Void 0) -> get_name err f i j tl | EBind (_, a, _) when i = 0 -> let err () = err i in Entity.get_name err f j a diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml index aa6cf5d97..4b17faaa1 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.ml +++ b/helm/software/lambda-delta/dual_rg/drgAut.ml @@ -132,9 +132,9 @@ let rec xlate_term f st lenv = function let map2 f = xlate_term f st lenv in let g qid (a, _) = let gref = D.TGRef ([], uri_of_qid qid) in - match args with - | [] -> f gref - | args -> + match args, a with + | [], [] -> f gref + | _ -> let f args = f (D.TAppl ([], args, gref)) in let f args = f (List.rev_map (map2 C.start) args) in let f a = C.list_rev_map_append f map1 a ~tail:args in @@ -176,7 +176,14 @@ let xlate_entity err f st = function let f qid = let ww = xlate_term C.start st lenv w in H.add henv (uri_of_qid qid) cnt; - let b = Y.Abst (D.TBind (a, D.Abst ws, ww)) in + let t = match ws with + | [] -> ww + | _ -> D.TBind (a, D.Abst ws, ww) + in +(* + DrgOutput.pp_term print_string t; print_newline (); +*) + let b = Y.Abst t in let entity = [Y.Mark st.line], uri_of_qid qid, b in f {st with line = succ st.line} entity in @@ -191,7 +198,14 @@ let xlate_entity err f st = function let ww = xlate_term C.start st lenv w in let vv = xlate_term C.start st lenv v in H.add henv (uri_of_qid qid) cnt; - let b = Y.Abbr (D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))) in + let t = match ws with + | [] -> D.TCast ([], ww, vv) + | _ -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv)) + in +(* + Printf.printf "%s\n" (U.string_of_uri (uri_of_qid qid)); +*) + let b = Y.Abbr t in let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in let entity = a, uri_of_qid qid, b in f {st with line = succ st.line} entity diff --git a/helm/software/lambda-delta/dual_rg/drgBrg.ml b/helm/software/lambda-delta/dual_rg/drgBrg.ml index 1f149a759..9ff63fb7c 100644 --- a/helm/software/lambda-delta/dual_rg/drgBrg.ml +++ b/helm/software/lambda-delta/dual_rg/drgBrg.ml @@ -26,16 +26,16 @@ let rec xlate_term f = function | D.TCast (a, u, t) -> let f uu tt = f (B.Cast (a, uu, tt)) in let f uu = xlate_term (f uu) t in - xlate_term f t + xlate_term f u | D.TAppl (a, vs, t) -> let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in let f tt = C.list_fold_right f map vs tt in xlate_term f t - | D.TProj (ap, e, D.TCast (ac, u, t)) -> - xlate_term f (D.TCast (ac, D.TProj (ap, e, u), D.TProj (ap, e, t))) | D.TProj (a, e, t) -> let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in xlate_term f t + | D.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) -> + xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t))) | D.TBind (a, b, t) -> let f tt = f (xlate_bind tt a b) in xlate_term f t @@ -61,4 +61,7 @@ and xlate_proj x _ e = lenv_fold_left xlate_bind xlate_proj x e let brg_of_drg f t = +(* + print_newline (); DrgOutput.pp_term print_string t; +*) f (xlate_term C.start t) diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml index e35e82f4e..5cb9538dd 100644 --- a/helm/software/lambda-delta/dual_rg/drgOutput.ml +++ b/helm/software/lambda-delta/dual_rg/drgOutput.ml @@ -9,6 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module P = Printf module U = NUri module C = Cps module H = Hierarchy @@ -16,6 +17,47 @@ module Y = Entity module X = Library module D = Drg +(****************************************************************************) + +let pp_attrs out a = + let map = function + | Y.Name (s, true) -> out (P.sprintf "%s;" s) + | Y.Name (s, false) -> out (P.sprintf "~%s;" s) + | Y.Apix i -> out (P.sprintf "+%i;" i) + | Y.Mark i -> out (P.sprintf "@%i;" i) + | Y.Priv -> out (P.sprintf "%s;" "~") + in + List.iter map a + +let rec pp_term out = function + | D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l) + | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j) + | D.TGRef (a, u) -> pp_attrs out a; out (P.sprintf "$") + | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y + | D.TProj (a, x, y) -> assert false + | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y + | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y + +and pp_terms bg eg out vs = + let rec aux = function + | [] -> () + | [v] -> pp_term out v + | v :: vs -> pp_term out v; out ", "; aux vs + in + out bg; aux vs; out (eg ^ ".") + +and pp_bind out = function + | D.Abst x -> pp_terms "[:" "]" out x + | D.Abbr x -> pp_terms "[=" "]" out x + | D.Void x -> out (P.sprintf "[%u]" x) + +let rec pp_lenv out = function + | D.ESort -> () + | D.EProj (x, a, y) -> assert false + | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y + +(****************************************************************************) + let rec list_iter map l out tab = match l with | [] -> () | hd :: tl -> map hd out tab; list_iter map tl out tab @@ -24,7 +66,13 @@ let list_rev_iter map e ns l out tab = let rec aux err f e = function | [], [] -> f e | n :: ns, hd :: tl -> - let f e = map e hd out tab; f (D.push2 C.err C.start e n ~t:hd) in + let f e = +(* + pp_lenv print_string e; print_string " |- "; + pp_term print_string hd; print_newline (); +*) + map e hd out tab; f (D.push2 C.err C.start e n ~t:hd) + in aux err f e (ns, tl) | _ -> err () in @@ -95,4 +143,6 @@ and exp_eproj e a lenv out tab = let attrs = [] in X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab +(****************************************************************************) + let export_term = exp_term D.empty_lenv diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.mli b/helm/software/lambda-delta/dual_rg/drgOutput.mli index cceeba195..e02161b13 100644 --- a/helm/software/lambda-delta/dual_rg/drgOutput.mli +++ b/helm/software/lambda-delta/dual_rg/drgOutput.mli @@ -10,3 +10,5 @@ V_______________________________________________________________ *) val export_term: Drg.term -> Library.pp + +val pp_term: (string -> unit) -> Drg.term -> unit diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 6e6ccfc28..0c85bb0c5 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -94,6 +94,19 @@ let xlate f st entity = match !kernel, entity with let f e = f st (BagEntity e) in Y.xlate f MBag.bag_of_meta e | _, entity -> f st entity +let pp_progress e = + let f a u = + let s = U.string_of_uri u in + let err () = L.warn (P.sprintf "%s" s) in + let f i = L.warn (P.sprintf "[%u] %s" i s) in + Y.mark err f a + in + match e with + | DrgEntity e -> Y.common f e + | BrgEntity e -> Y.common f e + | BagEntity e -> Y.common f e + | MetaEntity e -> Y.common f e + 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} @@ -134,13 +147,7 @@ let graph = ref (H.graph_of_string C.err C.start "Z2") let old = ref false let process_3 f st a u = - if !progress then - let s = U.string_of_uri u in - let err () = L.warn (P.sprintf "%s" s); f st in - let f i = L.warn (P.sprintf "[%u] %s" i s); f st in - Y.mark err f a - else - f st + f st let process_2 f st entity = let st = count_entity st entity in @@ -148,6 +155,7 @@ let process_2 f st entity = if !stage > 2 then type_check (process_3 f) st !si !graph entity else f st let process_1 f st entity = + if !progress then pp_progress entity; let st = count_entity st entity in if !export && !stage = 1 then export_entity !si !graph !moch entity; if !stage > 1 then xlate (process_2 f) st entity else f st diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index 7c42dc818..fcf51b5d0 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -203,7 +203,7 @@ TEST_DIRS = \ # library_auto TEST_DIRS_OPT = \ $(TEST_DIRS) \ - contribs/LAMBDA-TYPES \ +# contribs/LAMBDA-TYPES \ $(NULL) .PHONY: tests tests.opt cleantests cleantests.opt -- 2.39.2