From 651d745df2454a9e232aff3c9d8bf3e77653936d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 3 Dec 2010 16:14:02 +0000 Subject: [PATCH] first commit for Helena 0.8.2 autCrg: we removed the computation of the de Bruijn degree output: we renamed some reductions to reflect the latest terminology brgSubstitution: icm related bugfix --- helm/software/lambda-delta/.depend.opt | 4 +- .../lambda-delta/src/automath/autCrg.ml | 70 ++++++++----------- .../lambda-delta/src/basic_rg/brgReduction.ml | 4 +- .../src/basic_rg/brgSubstitution.ml | 8 ++- .../lambda-delta/src/common/output.ml | 16 ++--- .../lambda-delta/src/common/output.mli | 2 +- .../software/lambda-delta/src/toplevel/top.ml | 2 +- 7 files changed, 51 insertions(+), 55 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index ab31669d6..38ad66834 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -135,9 +135,9 @@ src/basic_rg/brgEnvironment.cmo: src/common/entity.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgEnvironment.cmx: src/common/entity.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgEnvironment.cmi src/basic_rg/brgSubstitution.cmi: src/basic_rg/brg.cmx -src/basic_rg/brgSubstitution.cmo: src/basic_rg/brg.cmx \ +src/basic_rg/brgSubstitution.cmo: src/common/options.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgSubstitution.cmi -src/basic_rg/brgSubstitution.cmx: src/basic_rg/brg.cmx \ +src/basic_rg/brgSubstitution.cmx: src/common/options.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgSubstitution.cmi src/basic_rg/brgReduction.cmi: src/common/status.cmx src/lib/log.cmi \ src/common/entity.cmx src/basic_rg/brg.cmx diff --git a/helm/software/lambda-delta/src/automath/autCrg.ml b/helm/software/lambda-delta/src/automath/autCrg.ml index 66de6c3d3..bba3fc265 100644 --- a/helm/software/lambda-delta/src/automath/autCrg.ml +++ b/helm/software/lambda-delta/src/automath/autCrg.ml @@ -44,12 +44,12 @@ let hcnt = K.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) -let empty_cnt = [], [], [] +let empty_cnt = [], [] -let add_abst (a, ws, ns) id w n = - E.Name (id, true) :: a, w :: ws, N.succ n :: ns +let add_abst (a, ws) id w = + E.Name (id, true) :: a, w :: ws -let mk_lref f n i j k = f n (D.TLRef ([E.Apix k], i, j)) +let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) let id_of_name (id, _, _) = id @@ -82,7 +82,7 @@ let relax_opt_qid f st = function | Some qid -> let f qid = f (Some qid) in relax_qid f st qid let resolve_gref err f st qid = - try let n, cnt = K.find henv (uri_of_qid qid) in f n qid cnt + try let cnt = K.find henv (uri_of_qid qid) in f qid cnt with Not_found -> err qid let resolve_gref_relaxed f st qid = @@ -103,37 +103,32 @@ let get_cnt_relaxed f st = (****************************************************************************) -let push_abst f (lenv, ns) a n w = +let push_abst f lenv a w = let bw = D.Abst (N.infinite, [w]) in - let f lenv = f (lenv, N.succ n :: ns) in + let f lenv = f lenv in D.push_bind f lenv a bw -let resolve_lref err f id (lenv, ns) = - let f i j k = f (List.nth ns k) i j k in - D.resolve_lref err f id lenv - -let lenv_of_cnt (a, ws, ns) = - D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)), ns +let lenv_of_cnt (a, ws) = + D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)) (* this is not tail recursive in the GRef branch *) let rec xlate_term f st lenv = function | A.Sort s -> - let f h = f (N.finite 0) (D.TSort ([], 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 n tt = f n (D.TAppl ([], [vv], tt)) in - let f _ vv = xlate_term (f vv) st lenv t 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 nw ww = + let f ww = let a = [E.Name (name, true)] in - let f nt tt = - let nnt = N.infinite (* if N.is_zero nt then N.infinite else nt *) in - let b = D.Abst (nnt, [ww]) in - f nt (D.TBind (a, b, tt)) + let f tt = + let b = D.Abst (N.infinite, [ww]) in + f (D.TBind (a, b, tt)) in let f lenv = xlate_term f st lenv t in - push_abst f lenv a nw ww + push_abst f lenv a ww in xlate_term f st lenv w | A.GRef (name, args) -> @@ -141,22 +136,20 @@ let rec xlate_term f st lenv = function | E.Name (id, _) -> f (A.GRef ((id, true, []), [])) | _ -> C.err () in - let map2 f t = - let f _ tt = f tt in xlate_term f st lenv t - in - let g n qid (a, _, _) = + let map2 f t = xlate_term f st lenv t in + let g qid (a, _) = let gref = D.TGRef ([], uri_of_qid qid) in match args, a with - | [], [] -> f n gref + | [], [] -> f gref | _ -> - let f args = f n (D.TAppl ([], args, gref)) in + let f args = f (D.TAppl ([], args, gref)) in let f args = C.list_rev_map f map2 args in let f a = C.list_rev_map_append f map1 a ~tail:args in C.list_sub_strict f a args in let g qid = resolve_gref_relaxed g st qid in let err () = complete_qid g st name in - resolve_lref err (mk_lref f) (id_of_name name) lenv + D.resolve_lref err (mk_lref f) (id_of_name name) lenv let xlate_entity err f st = function | A.Section (Some (_, name)) -> @@ -176,8 +169,8 @@ let xlate_entity err f st = function let f qid = let f cnt = let lenv = lenv_of_cnt cnt in - let f nw ww = - K.add hcnt (uri_of_qid qid) (add_abst cnt name ww nw); + let f ww = + K.add hcnt (uri_of_qid qid) (add_abst cnt name ww); err {st with node = Some qid} in xlate_term f st lenv w @@ -187,11 +180,11 @@ let xlate_entity err f st = function complete_qid f st (name, true, []) | A.Decl (name, w) -> let f cnt = - let a, ws, _ = cnt in + let a, ws = cnt in let lenv = lenv_of_cnt cnt in let f qid = - let f nw ww = - K.add henv (uri_of_qid qid) (N.succ nw, cnt); + let f ww = + K.add henv (uri_of_qid qid) cnt; let t = match ws with | [] -> ww | _ -> D.TBind (a, D.Abst (N.infinite, ws), ww) @@ -210,13 +203,12 @@ let xlate_entity err f st = function get_cnt_relaxed f st | A.Def (name, w, trans, v) -> let f cnt = - let a, ws, _ = cnt in + let a, ws = cnt in let lenv = lenv_of_cnt cnt in let f qid = - let f nw ww = - let f nv vv = - assert (nv = N.succ nw); (**) - K.add henv (uri_of_qid qid) (nv, cnt); + let f ww = + let f vv = + K.add henv (uri_of_qid qid) cnt; let t = match ws with | [] -> D.TCast ([], ww, vv) | _ -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv)) diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml index c4b2e9c15..98747ab55 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml @@ -115,12 +115,12 @@ let rec step st m x = | [] -> m, None, x | (c, v) :: s -> if N.is_zero n then Q.add_nonzero st.S.cc a; - O.add ~beta:1 ~upsilon:(List.length s) (); + O.add ~beta:1 ~theta:(List.length s) (); let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in step st {m with e = e; s = s} t end | B.Bind (a, b, t) -> - O.add ~upsilon:(List.length m.s) (); + O.add ~theta:(List.length m.s) (); let e = B.push m.e m.e a b in step st {m with e = e} t diff --git a/helm/software/lambda-delta/src/basic_rg/brgSubstitution.ml b/helm/software/lambda-delta/src/basic_rg/brgSubstitution.ml index 4e5eb481f..152b8c069 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgSubstitution.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgSubstitution.ml @@ -9,8 +9,8 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module G = Options module B = Brg -(* module O = Output *) let rec icm a = function | B.Sort _ @@ -42,5 +42,9 @@ let lift_map h _ a i = let lift h d t = if h = 0 then t else begin -(* O.icm := succ (* icm *) !O.icm (*t*); *) iter (lift_map h) d t +(* + G.icm := succ !G.icm; + G.icm := icm !G.icm t; +*) + iter (lift_map h) d t end diff --git a/helm/software/lambda-delta/src/common/output.ml b/helm/software/lambda-delta/src/common/output.ml index 38ebf8a34..112476488 100644 --- a/helm/software/lambda-delta/src/common/output.ml +++ b/helm/software/lambda-delta/src/common/output.ml @@ -16,7 +16,7 @@ module G = Options type reductions = { beta : int; zeta : int; - upsilon: int; + theta: int; tau : int; ldelta : int; gdelta : int; @@ -26,7 +26,7 @@ type reductions = { } let initial_reductions = { - beta = 0; upsilon = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0; + beta = 0; theta = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0; si = 0; lrt = 0; grt = 0 } @@ -35,12 +35,12 @@ let reductions = ref initial_reductions let clear_reductions () = reductions := initial_reductions let add - ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) + ?(beta=0) ?(theta=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) ?(si=0) ?(lrt=0) ?(grt=0) () = reductions := { beta = !reductions.beta + beta; zeta = !reductions.zeta + zeta; - upsilon = !reductions.upsilon + upsilon; + theta = !reductions.theta + theta; tau = !reductions.tau + tau; ldelta = !reductions.ldelta + ldelta; gdelta = !reductions.gdelta + gdelta; @@ -51,7 +51,7 @@ let add let print_reductions () = let r = !reductions in - let rs = r.beta + r.ldelta + r.zeta + r.upsilon + r.tau + r.gdelta in + let rs = r.beta + r.ldelta + r.zeta + r.theta + r.tau + r.gdelta in let prs = r.si + r.lrt + r.grt in let delta = r.ldelta + r.gdelta in let rt = r.lrt + r.grt in @@ -61,9 +61,9 @@ let print_reductions () = L.warn (P.sprintf " Delta: %7u" delta); L.warn (P.sprintf " Local: %7u" r.ldelta); L.warn (P.sprintf " Global: %7u" r.gdelta); - L.warn (P.sprintf " Zeta: %7u" r.zeta); - L.warn (P.sprintf " Upsilon: %7u" r.upsilon); - L.warn (P.sprintf " Tau: %7u" r.tau); + L.warn (P.sprintf " Theta: %7u" r.theta); + L.warn (P.sprintf " Zeta for abbreviation: %7u" r.zeta); + L.warn (P.sprintf " Zeta for cast: %7u" r.tau); L.warn (P.sprintf " Pseudo reductions: %7u" prs); L.warn (P.sprintf " Reference typing: %7u" rt); L.warn (P.sprintf " Local: %7u" r.lrt); diff --git a/helm/software/lambda-delta/src/common/output.mli b/helm/software/lambda-delta/src/common/output.mli index 20b83f0fc..5cfe82b43 100644 --- a/helm/software/lambda-delta/src/common/output.mli +++ b/helm/software/lambda-delta/src/common/output.mli @@ -12,7 +12,7 @@ val clear_reductions: unit -> unit val add: - ?beta:int -> ?upsilon:int -> ?tau:int -> ?ldelta:int -> ?gdelta:int -> + ?beta:int -> ?theta:int -> ?tau:int -> ?ldelta:int -> ?gdelta:int -> ?zeta:int -> ?si:int -> ?lrt:int -> ?grt:int -> unit -> unit diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index aad48387e..00e443388 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -261,7 +261,7 @@ let process st name = let main = try - let version_string = "Helena 0.8.1 M - November 2010" in + let version_string = "Helena 0.8.2 M - December 2010" in let print_version () = L.warn (version_string ^ "\n"); exit 0 in let set_hierarchy s = if H.set_graph s then () else -- 2.39.2