From: Ferruccio Guidi Date: Wed, 10 Dec 2008 21:25:21 +0000 (+0000) Subject: - new semantic log system X-Git-Tag: make_still_working~4421 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8659e85d49be1ad72622d4d3a73d384b744c3c08;p=helm.git - new semantic log system - new brg terms - bug fix im MetaOutput and MetaBrg --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 418d35ef0..7e884babc 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -1,7 +1,7 @@ lib/nUri.cmo: lib/nUri.cmi lib/nUri.cmx: lib/nUri.cmi -lib/log.cmo: lib/log.cmi -lib/log.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/autOutput.cmi: automath/aut.cmx @@ -16,29 +16,34 @@ automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx basic_rg/brg.cmo: lib/nUri.cmi automath/aut.cmx basic_rg/brg.cmx: lib/nUri.cmx automath/aut.cmx -basic_rg/brgOutput.cmi: basic_rg/brg.cmx -basic_rg/brgOutput.cmo: lib/log.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi -basic_rg/brgOutput.cmx: lib/log.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx basic_rg/brgEnvironment.cmo: lib/nUri.cmi basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi -basic_rg/brgReduction.cmi: basic_rg/brg.cmx -basic_rg/brgReduction.cmo: lib/share.cmx lib/nUri.cmi lib/cps.cmx \ +basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx +basic_rg/brgReduction.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi lib/cps.cmx \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgReduction.cmx: lib/share.cmx lib/nUri.cmx lib/cps.cmx \ +basic_rg/brgReduction.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx lib/cps.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgType.cmi: basic_rg/brgReduction.cmi basic_rg/brg.cmx -basic_rg/brgType.cmo: basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi \ - basic_rg/brg.cmx basic_rg/brgType.cmi -basic_rg/brgType.cmx: basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx \ - basic_rg/brg.cmx basic_rg/brgType.cmi +basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brgReduction.cmi \ + basic_rg/brg.cmx +basic_rg/brgOutput.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx \ + basic_rg/brgReduction.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi +basic_rg/brgOutput.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx \ + basic_rg/brgReduction.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi +basic_rg/brgType.cmi: lib/log.cmi basic_rg/brgReduction.cmi basic_rg/brg.cmx +basic_rg/brgType.cmo: lib/log.cmi basic_rg/brgReduction.cmi \ + basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi basic_rg/brg.cmx \ + basic_rg/brgType.cmi +basic_rg/brgType.cmx: lib/log.cmx basic_rg/brgReduction.cmx \ + basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ + basic_rg/brgType.cmi basic_rg/brgUntrusted.cmi: basic_rg/brg.cmx basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgReduction.cmi \ - basic_rg/brgEnvironment.cmi basic_rg/brgUntrusted.cmi + basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgReduction.cmx \ - basic_rg/brgEnvironment.cmx basic_rg/brgUntrusted.cmi + basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx @@ -56,11 +61,11 @@ toplevel/metaBrg.cmo: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmi toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/metaBrg.cmi -toplevel/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaBrg.cmi \ - toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \ - basic_rg/brgOutput.cmi automath/autParser.cmi automath/autOutput.cmi \ - automath/autLexer.cmx -toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaBrg.cmx \ - toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \ - basic_rg/brgOutput.cmx automath/autParser.cmx automath/autOutput.cmx \ - automath/autLexer.cmx +toplevel/top.cmo: lib/time.cmx lib/nUri.cmi toplevel/metaOutput.cmi \ + toplevel/metaBrg.cmi toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx \ + basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.cmi \ + automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx +toplevel/top.cmx: lib/time.cmx lib/nUri.cmx toplevel/metaOutput.cmx \ + toplevel/metaBrg.cmx toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx \ + basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.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 2b218865e..a568047d9 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -13,3 +13,15 @@ include Makefile.common test: $(MAIN).opt @echo " HELENA automath/*.aut" $(H)./$(MAIN).opt -S 3 automath/*.aut > log.txt + +meta: $(MAIN).opt + @echo " HELENA -m meta.txt automath/*.aut" + $(H)./$(MAIN).opt -m meta.txt -s 1 -S 3 automath/*.aut > /dev/null + +ifeq ($(MAKECMDGOALS), test) + include .depend.opt +endif + +ifeq ($(MAKECMDGOALS), meta) + include .depend.opt +endif diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index c4a276b82..c9173f76c 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -66,7 +66,3 @@ tgz: clean ifeq ($(MAKECMDGOALS), $(MAIN).opt) include .depend.opt endif - -ifeq ($(MAKECMDGOALS), test) - include .depend.opt -endif diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make index eb1c64a66..7085d3b57 100644 --- a/helm/software/lambda-delta/basic_rg/Make +++ b/helm/software/lambda-delta/basic_rg/Make @@ -1 +1 @@ -brg brgOutput brgEnvironment brgReduction brgType brgUntrusted +brg brgEnvironment brgReduction brgOutput brgType brgUntrusted diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 36e4fefe8..e9897c08a 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -12,16 +12,18 @@ type uri = NUri.uri type id = Aut.id -type bind = Abst | Abbr (* abstraction, abbreviation *) +type bind = Void (* exclusion *) + | Abst of term (* abstraction *) + | Abbr of term (* abbreviation *) -type term = Sort of int (* hierarchy index *) - | LRef of int (* reverse de Bruijn index *) - | GRef of uri (* reference *) - | Cast of term * term (* type, term *) - | Appl of term * term (* argument, function *) - | Bind of id * bind * term * term (* name, binder, content, scope *) +and term = Sort of int (* hierarchy index *) + | LRef of int (* reverse de Bruijn index *) + | GRef of uri (* reference *) + | Cast of term * term (* type, term *) + | Appl of term * term (* argument, function *) + | Bind of id * bind * term (* name, binder, scope *) -type obj = int * uri * bind * term (* age, uri, binder, contents *) +type obj = int * uri * bind (* age, uri, binder, contents *) type item = obj option @@ -29,8 +31,12 @@ type hierarchy = int -> int (* Currified constructors ***************************************************) +let abst w = Abst w + +let abbr v = Abbr v + let cast u t = Cast (u, t) let appl u t = Appl (u, t) -let bind id b u t = Bind (id, b, u, t) +let bind id b t = Bind (id, b, t) diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml index b0cb9596e..e640c865b 100644 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml +++ b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml @@ -24,8 +24,8 @@ let entry = ref 0 (* Interface functions ******************************************************) let set_obj f obj = - let _, uri, b, t = obj in - let obj = !entry, uri, b, t in + let _, uri, b = obj in + let obj = !entry, uri, b in incr entry; H.add env uri obj; f obj let get_obj f uri = diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index e29b3f495..4c100375d 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -10,8 +10,12 @@ V_______________________________________________________________ *) module P = Printf +module F = Format +module U = NUri +module C = Cps module L = Log module B = Brg +module R = BrgReduction type counters = { eabsts: int; @@ -30,11 +34,16 @@ let initial_counters = { tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 } -let count_term_binder f c = function - | B.Abst -> f {c with tabsts = succ c.tabsts} - | B.Abbr -> f {c with tabbrs = succ c.tabbrs} +let rec count_term_binder f c = function + | B.Abst w -> + let c = {c with tabsts = succ c.tabsts} in + count_term f c w + | B.Abbr v -> + let c = {c with tabbrs = succ c.tabbrs} in + count_term f c v + | B.Void -> f c -let rec count_term f c = function +and count_term f c = function | B.Sort _ -> f {c with tsorts = succ c.tsorts} | B.LRef _ -> @@ -49,18 +58,21 @@ let rec count_term f c = function let c = {c with tappls = succ c.tappls} in let f c = count_term f c t in count_term f c v - | B.Bind (_, b, u, t) -> + | B.Bind (_, b, t) -> let f c = count_term_binder f c b in - let f c = count_term f c t in - count_term f c u + count_term f c t let count_obj_binder f c = function - | B.Abst -> f {c with eabsts = succ c.eabsts} - | B.Abbr -> f {c with eabbrs = succ c.eabbrs} + | B.Abst w -> + let c = {c with eabsts = succ c.eabsts} in + count_term f c w + | B.Abbr v -> + let c = {c with eabbrs = succ c.eabbrs} in + count_term f c v + | B.Void -> f c -let count_obj f c (_, _, b, t) = - let f c = count_obj_binder f c b in - count_term f c t +let count_obj f c (_, _, b) = + count_obj_binder f c b let count_item f c = function | Some obj -> count_obj f c obj @@ -85,3 +97,36 @@ let print_counters f c = L.warn (P.sprintf " Abstraction items: %6u" c.tabsts); L.warn (P.sprintf " Abbreviation items: %6u" c.tabbrs); f () + +let rec pp_term c frm = function + | B.Sort h -> F.fprintf frm "@[*%u@]" h + | B.LRef i -> F.fprintf frm "@[#%u@]" i + | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) + | B.Cast (u, t) -> + F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t + | B.Appl (v, t) -> + F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t + | B.Bind (id, B.Abst w, t) -> + F.fprintf frm "@[[%s:%a].%a@]" id (pp_term c) w (pp_term c) t + | B.Bind (id, B.Abbr v, t) -> + F.fprintf frm "@[[%s=%a].%a@]" id (pp_term c) v (pp_term c) t + | B.Bind (id, B.Void, t) -> + F.fprintf frm "@[[%s].%a@]" id (pp_term c) t + +let pp_context frm c = + let pp_entry f = function + | B.Abst w -> + F.fprintf frm "%s %a\n%!" "\\decl" (pp_term c) w; f () + | B.Abbr v -> + F.fprintf frm "%s %a\n%!" "\\def " (pp_term c) v; f () + | B.Void -> + F.fprintf frm "%s\n%!" "\\void"; f () + in + R.iter C.start pp_entry c + +let pp_term frm c t = + F.fprintf frm "%a\n%!" (pp_term c) t + +let specs = { + L.pp_term = pp_term; L.pp_context = pp_context +} diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.mli b/helm/software/lambda-delta/basic_rg/brgOutput.mli index 49b5064d1..cd7e49dc5 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.mli +++ b/helm/software/lambda-delta/basic_rg/brgOutput.mli @@ -16,3 +16,5 @@ val initial_counters: counters val count_item: (counters -> 'a) -> counters -> Brg.item -> 'a val print_counters: (unit -> 'a) -> counters -> 'a + +val specs: (BrgReduction.context, Brg.term) Log.specs diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index aced1a22e..74f6a5048 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -12,16 +12,11 @@ module U = NUri module C = Cps module S = Share +module L = Log module B = Brg module E = BrgEnvironment -exception LRefNotFound of string Lazy.t - -type bind = Void_ - | Abst_ of B.term - | Abbr_ of B.term - -type environment = int * bind list +type environment = int * B.bind list type stack = B.term list @@ -31,10 +26,12 @@ type context = { s: stack } +exception LRefNotFound of (context, B.term) L.item list + type whd_result = | Sort_ of int | LRef_ of int * B.term option - | GRef_ of int * B.bind * B.term + | GRef_ of int * B.bind | Bind_ of B.term * B.term type ho_whd_result = @@ -43,6 +40,8 @@ type ho_whd_result = (* Internal functions *******************************************************) +let error i = raise (LRefNotFound (L.items1 (string_of_int i))) + let empty_e = 0, [] let push_e f b (l, e) = @@ -50,36 +49,45 @@ let push_e f b (l, e) = let get_e f c i = let (gl, ge), (ll, le) = c.g, c.l in - if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i))); + if i >= gl + ll then error i; let b = if i < gl then List.nth ge (gl - (succ i)) else List.nth le (gl + ll - (succ i)) in f b -let rec lref_map f map t = match t with - | B.LRef i -> f (B.LRef (map i)) - | B.GRef _ -> f t - | B.Sort _ -> f t - | B.Cast (w, u) -> +let rec lref_map_bind f map b = match b with + | B.Abbr v -> + let f v' = f (S.sh1 v v' b B.abbr) in + lref_map f map v + | B.Abst w -> + let f w' = f (S.sh1 w w' b B.abst) in + lref_map f map w + | B.Void -> f b + +and lref_map f map t = match t with + | B.LRef i -> f (B.LRef (map i)) + | B.GRef _ -> f t + | B.Sort _ -> f t + | B.Cast (w, u) -> let f w' u' = f (S.sh2 w w' u u' t B.cast) in let f w' = lref_map (f w') map u in lref_map f map w - | B.Appl (w, u) -> + | B.Appl (w, u) -> let f w' u' = f (S.sh2 w w' u u' t B.appl) in let f w' = lref_map (f w') map u in lref_map f map w - | B.Bind (id, b, w, u) -> - let f w' u' = f (S.sh2 w w' u u' t (B.bind id b)) in - let f w' = lref_map (f w') map u in - lref_map f map w + | B.Bind (id, b, u) -> + let f b' u' = f (S.sh2 b b' u u' t (B.bind id)) in + let f b' = lref_map (f b') map u in + lref_map_bind f map b (* to share *) let lift f c = let (gl, _), (ll, le) = c.g, c.l in let map i = if i >= gl then succ i else i in let map f = function - | Abbr_ t -> let f t' = f (Abbr_ t') in lref_map f map t + | B.Abbr t -> let f t' = f (B.Abbr t') in lref_map f map t | _ -> assert false in let f le' = f {c with l = (ll, le')} in @@ -97,52 +105,52 @@ let xchg f c t = let rec whd f c t = match t with | B.Sort h -> f c (Sort_ h) | B.GRef uri -> - let f (i, _, b, t) = f c (GRef_ (i, b, t)) in + let f (i, _, b) = f c (GRef_ (i, b)) in E.get_obj f uri - | B.LRef i -> + | B.LRef i -> let f = function - | Void_ -> f c (LRef_ (i, None)) - | Abst_ t -> f c (LRef_ (i, Some t)) - | Abbr_ t -> whd f c t + | B.Void -> f c (LRef_ (i, None)) + | B.Abst t -> f c (LRef_ (i, Some t)) + | B.Abbr t -> whd f c t in get_e f c i - | B.Appl (v, t) -> whd f {c with s = v :: c.s} t - | B.Bind (_, B.Abbr, v, t) -> - let f l = whd f {c with l = l} t in - push_e f (Abbr_ v) c.l - | B.Bind (_, B.Abst, w, t) -> + | B.Cast (_, t) -> whd f c t + | B.Appl (v, t) -> whd f {c with s = v :: c.s} t + | B.Bind (_, B.Abst w, t) -> begin match c.s with | [] -> f c (Bind_ (w, t)) | v :: tl -> let f tl l = whd f {c with l = l; s = tl} t in - push_e (f tl) (Abbr_ v) c.l + push_e (f tl) (B.Abbr v) c.l end - | B.Cast (_, t) -> whd f c t + | B.Bind (_, b, t) -> + let f l = whd f {c with l = l} t in + push_e f b c.l let push f c t = assert (c.s = []); let f c g = xchg f {c with g = g} t in - let f c = push_e (f c) Void_ c.g in + let f c = push_e (f c) B.Void c.g in lift f c (* Interface functions ******************************************************) let rec are_convertible f c1 t1 c2 t2 = let rec aux c1' r1 c2' r2 = match r1, r2 with - | Sort_ h1, Sort_ h2 -> f (h1 = h2) - | LRef_ (i1, _), LRef_ (i2, _) -> + | Sort_ h1, Sort_ h2 -> f (h1 = h2) + | LRef_ (i1, _), LRef_ (i2, _) -> if i1 = i2 then are_convertible_stacks f c1' c2' else f false - | GRef_ (a1, B.Abst, _), GRef_ (a2, B.Abst, _) -> + | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) -> if a1 = a2 then are_convertible_stacks f c1' c2' else f false - | GRef_ (a1, B.Abbr, v1), GRef_ (a2, B.Abbr, v2) -> + | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) -> if a1 = a2 then are_convertible_stacks f c1' c2' else if a1 < a2 then whd (aux c1' r1) c2' v2 else whd (aux_rev c2' r2) c1' v1 - | _, GRef_ (_, B.Abbr, v2) -> + | _, GRef_ (_, B.Abbr v2) -> whd (aux c1' r1) c2' v2 - | GRef_ (_, B.Abbr, v1), _ -> + | GRef_ (_, B.Abbr v1), _ -> whd (aux_rev c2' r2) c1' v1 - | Bind_ (w1, t1), Bind_ (w2, t2) -> + | Bind_ (w1, t1), Bind_ (w2, t2) -> let f b = if b then let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in @@ -164,31 +172,30 @@ let are_convertible f c t1 t2 = are_convertible f c t1 c t2 let rec ho_whd f c t = let aux c' = function - | Sort_ h -> f c' (Sort h) - | Bind_ (w, t) -> f c' (Abst w) - | LRef_ (_, Some w) -> ho_whd f c w - | GRef_ (_, _, u) -> ho_whd f c u - | LRef_ (_, None) -> assert false + | Sort_ h -> f c' (Sort h) + | Bind_ (w, t) -> f c' (Abst w) + | LRef_ (_, Some w) -> ho_whd f c w + | GRef_ (_, B.Abst u) -> ho_whd f c u + | GRef_ (_, B.Abbr u) -> ho_whd f c u + | LRef_ (_, None) -> assert false + | GRef_ (_, B.Void) -> assert false in whd aux c t -let push f c b t = +let push f c b = assert (c.l = empty_e && c.s = []); let f g = f {c with g = g} in - let b = match b with - | B.Abbr -> Abbr_ t - | B.Abst -> Abst_ t - in push_e f b c.g let get f c i = let gl, ge = c.g in - if i >= gl then raise (LRefNotFound (lazy (string_of_int i))); - match List.nth ge (gl - (succ i)) with - | Abbr_ v -> f (B.Abbr, v) - | Abst_ w -> f (B.Abst, w) - | Void_ -> assert false + if i >= gl then error i; + f (List.nth ge (gl - (succ i))) let empty_context = { g = empty_e; l = empty_e; s = [] } + +let iter f map c = + let _, ge = c.g in + C.list_iter f map ge diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index a8320ed55..b3a79ecae 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -9,19 +9,21 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception LRefNotFound of string Lazy.t - type context +exception LRefNotFound of (context, Brg.term) Log.item list + type ho_whd_result = | Sort of int | Abst of Brg.term val empty_context: context -val push: (context -> 'a) -> context -> Brg.bind -> Brg.term -> 'a +val push: (context -> 'a) -> context -> Brg.bind -> 'a + +val get: (Brg.bind -> 'a) -> context -> int -> 'a -val get: (Brg.bind * Brg.term -> 'a) -> context -> int -> 'a +val iter: (unit -> 'a) -> ((unit -> 'a) -> Brg.bind -> 'a) -> context -> 'a val are_convertible: (bool -> 'a) -> context -> Brg.term -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index d10ddefaa..60b5b75bc 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -9,53 +9,82 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module L = Log module B = Brg +module O = BrgOutput module E = BrgEnvironment module R = BrgReduction -exception TypeError of string Lazy.t +exception TypeError of (R.context, B.term) Log.item list (* Internal functions *******************************************************) -let error msg = raise (TypeError (lazy msg)) +let error1 s c t = + raise (TypeError (L.ct_items1 s c t)) + +let error2 s1 c1 t1 s2 c2 t2 = + raise (TypeError (L.ct_items2 s1 c1 t1 s2 c2 t2)) + +let are_convertible f c t1 t2 = + L.log O.specs 4 (L.ct_items2 "Now converting" c t1 "and" c t2); + R.are_convertible f c t1 t2 (* Interface functions ******************************************************) -let rec type_of f g c = function - | B.Sort h -> f (B.Sort (g h)) - | B.LRef i -> +let rec type_of f g c x = + L.log O.specs 5 (L.ct_items1 "now checking" c x); + match x with + | B.Sort h -> f (B.Sort (g h)) + | B.LRef i -> let f = function - | B.Abst, w -> f w - | B.Abbr, B.Cast (w, v) -> f w - | B.Abbr, _ -> error "lref" + | B.Abst w -> f w + | B.Abbr (B.Cast (w, v)) -> f w + | B.Abbr _ -> assert false + | B.Void -> assert false in R.get f c i - | B.GRef uri -> + | B.GRef uri -> let f = function - | _, _, B.Abst, w -> f w - | _, _, B.Abbr, B.Cast (w, v) -> f w - | _, _, B.Abbr, _ -> error "gref" + | _, _, B.Abst w -> f w + | _, _, B.Abbr (B.Cast (w, v)) -> f w + | _, _, B.Abbr _ -> assert false + | _, _, B.Void -> assert false in E.get_obj f uri - | B.Bind (id, b, u, t) -> - let f uu tt = match b, t with - | B.Abst, _ - | B.Abbr, B.Cast _ -> f (B.Bind (id, b, u, tt)) - | _ -> f (B.Bind (id, b, B.Cast (uu, u), tt)) + | B.Bind (id, B.Abbr u, t) -> + let f tt = f (B.Bind (id, B.Abbr u, tt)) in + let f cc = type_of f g cc t in + let f u = R.push f c (B.Abbr u) in + let f uu = match u with + | B.Cast _ -> f u + | _ -> f (B.Cast (uu, u)) in - let f uu cc = type_of (f uu) g cc t in - let f uu = R.push (f uu) c b u in type_of f g c u - | B.Appl (v, t) -> + | B.Bind (id, B.Abst u, t) -> + let f tt = f (B.Bind (id, B.Abst u, tt)) in + let f cc = type_of f g cc t in + let f _ = R.push f c (B.Abst u) in + type_of f g c u + | B.Bind (id, B.Void, t) -> + let f tt = f (B.Bind (id, B.Void, tt)) in + let f cc = type_of f g cc t in + R.push f c B.Void + | B.Appl (v, t) -> let f tt cc = function - | R.Sort _ -> error "appl" + | R.Sort _ -> error1 "not a function" c t | R.Abst w -> - let f b = if b then f (B.Appl (v, tt)) else error "appl_cast" in - type_of (R.are_convertible f cc w) g c v + let f b = + if b then f (B.Appl (v, tt)) else + error2 "the term" c v "must be of type" cc w + in + type_of (are_convertible f cc w) g c v in let f tt = R.ho_whd (f tt) c t in type_of f g c t - | B.Cast (u, t) -> - let f b = if b then f u else error "cast" in - let f _ = type_of (R.are_convertible f c u) g c t in + | B.Cast (u, t) -> + let f b = + if b then f u else + error2 "the term" c t "must be of type" c u + in + let f _ = type_of (are_convertible f c u) g c t in type_of f g c u diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index 5b351cca4..dc6fc998d 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception TypeError of string Lazy.t +exception TypeError of (BrgReduction.context, Brg.term) Log.item list val type_of: (Brg.term -> 'a) -> Brg.hierarchy -> BrgReduction.context -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index c9f425f88..d08209f12 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -9,6 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module B = Brg module E = BrgEnvironment module R = BrgReduction module T = BrgType @@ -16,8 +17,10 @@ module T = BrgType (* Interface functions ******************************************************) let type_check f g = function - | None -> f None - | Some ((_, _, _, t) as obj) -> + | None -> f None + | Some ((_, _, B.Abst t) as obj) + | Some ((_, _, B.Abbr t) as obj) -> let f tt obj = f (Some (tt, obj)) in let f tt = E.set_obj (f tt) obj in T.type_of f g R.empty_context t + | Some (_, _, B.Void) -> assert false diff --git a/helm/software/lambda-delta/lib/cps.ml b/helm/software/lambda-delta/lib/cps.ml index c235197d9..2e8b2c715 100644 --- a/helm/software/lambda-delta/lib/cps.ml +++ b/helm/software/lambda-delta/lib/cps.ml @@ -49,3 +49,6 @@ let list_rev = let list_map f = list_rev_map (list_rev f) +let list_iter f map l = + let map f () x = map f x in + list_fold_left f map () l diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index 667fef534..78e57fdfa 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -10,6 +10,22 @@ V_______________________________________________________________ *) module P = Printf +module F = Format +module C = Cps + +type ('a, 'b) item = Term of 'a * 'b + | Context of 'a + | Warn of string + | String of string + +type ('a, 'b) specs = { + pp_term : F.formatter -> 'a -> 'b -> unit; + pp_context: F.formatter -> 'a -> unit +} + +let level = ref 0 + +(* Internal functions *******************************************************) let init = let started = ref false in @@ -17,5 +33,28 @@ let init = if !started then () else begin P.printf "\n"; started := true end +let pp_items frm st l items = + let pp_item = function + | Term (c, t) -> st.pp_context frm c; st.pp_term frm c t + | Context c -> st.pp_context frm c + | Warn s -> F.fprintf frm "@[%s\n@]" s + | String s -> F.fprintf frm "@[%s @]" s + in + if !level >= l then List.iter pp_item items + +(* Interface functions ******************************************************) + let warn msg = init (); P.printf " %s\n" msg; flush stdout + +let log st l items = pp_items F.std_formatter st l items + +let error st items = pp_items F.err_formatter st 0 items + +let items1 s = [Warn s] + +let ct_items1 s c t = + [Warn s; Term (c, t)] + +let ct_items2 s1 c1 t1 s2 c2 t2 = + [Warn s1; Term (c1, t1); Warn s2; Term (c2, t2)] diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index e32f6e0fd..184594077 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -9,4 +9,26 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +type ('a, 'b) item = Term of 'a * 'b + | Context of 'a + | Warn of string + | String of string + +type ('a, 'b) specs = { + pp_term : Format.formatter -> 'a -> 'b -> unit; + pp_context: Format.formatter -> 'a -> unit +} + +val level: int ref + val warn: string -> unit + +val log: ('a, 'b) specs -> int -> ('a, 'b) item list -> unit + +val error: ('a, 'b) specs -> ('a, 'b) item list -> unit + +val items1: string -> ('a, 'b) item list + +val ct_items1: string -> 'a -> 'b -> ('a, 'b) item list + +val ct_items2: string -> 'a -> 'b -> string -> 'a -> 'b -> ('a, 'b) item list diff --git a/helm/software/lambda-delta/lib/share.ml b/helm/software/lambda-delta/lib/share.ml index 019cca982..c8097d568 100644 --- a/helm/software/lambda-delta/lib/share.ml +++ b/helm/software/lambda-delta/lib/share.ml @@ -11,6 +11,9 @@ let sh a b = if a == b then a else b - -let sh2 a1 b1 a2 b2 c1 c2 = + +let sh1 a1 a2 b1 b2 = + if a1 == a2 then b1 else b2 (sh a1 a2) + +let sh2 a1 a2 b1 b2 c1 c2 = if a1 == a2 && b1 == b2 then c1 else c2 (sh a1 a2) (sh b1 b2) diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index 4088c2982..192613264 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -20,23 +20,23 @@ let map_fold_left f map1 map2 a l = let map_args f t v = f (B.Appl (v, t)) -let map_pars f t (id, w) = f (B.Bind (id, B.Abst, w, t)) +let map_pars f t (id, w) = f (B.Bind (id, B.Abst w, t)) let rec xlate_term f = function | M.Sort s -> let f h = f (B.Sort h) in if s then f 0 else f 1 | M.LRef (l, i) -> - f (B.LRef (l - i)) + f (B.LRef (l - succ i)) | M.GRef (_, uri, vs) -> let f vs = map_fold_left f Cps.id map_args (B.GRef uri) vs in - Cps.list_rev_map f xlate_term vs + Cps.list_map f xlate_term vs | M.Appl (v, t) -> let f v t = f (B.Appl (v, t)) in let f v = xlate_term (f v) t in xlate_term f v | M.Abst (id, w, t) -> - let f w t = f (B.Bind (id, B.Abst, w, t)) in + let f w t = f (B.Bind (id, B.Abst w, t)) in let f w = xlate_term (f w) t in xlate_term f w @@ -46,14 +46,14 @@ let xlate_pars f (id, w) = let xlate_entry f = function | e, pars, uri, u, None -> - let f u = f (e, uri, B.Abst, u) in + let f u = f (e, uri, B.Abst u) in let f pars = map_fold_left f xlate_term map_pars u pars in - Cps.list_rev_map f xlate_pars pars + Cps.list_map f xlate_pars pars | e, pars, uri, u, Some (_, t) -> - let f u t = f (e, uri, B.Abbr, (B.Cast (u, t))) in + let f u t = f (e, uri, B.Abbr (B.Cast (u, t))) in let f pars u = map_fold_left (f u) xlate_term map_pars t pars in let f pars = map_fold_left (f pars) xlate_term map_pars u pars in - Cps.list_rev_map f xlate_pars pars + Cps.list_map f xlate_pars pars let xlate_item f = function | None -> f None diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 2d5bc3ad5..03995e153 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -104,6 +104,9 @@ let pp_list pp opend sep closed frm l = in if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed +let pp_rev_list pp opend sep closed frm l = + pp_list pp opend sep closed frm (List.rev l) + let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args and pp_term frm = function @@ -121,7 +124,7 @@ and pp_term frm = function let pp_par frm (id, w) = F.fprintf frm "%s:%a" id pp_term w -let pp_pars = pp_list pp_par "[" "," "]" +let pp_pars = pp_rev_list pp_par "[" "," "]" let pp_body frm = function | None -> () diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 92840d54a..7504e2c0b 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -10,6 +10,7 @@ V_______________________________________________________________ *) module P = Printf +module U = NUri module L = Log module AO = AutOutput module MA = MetaAut @@ -19,31 +20,32 @@ module BrgO = BrgOutput module BrgU = BrgUntrusted type status = { - summary: int; mst : MA.status; ac : AO.counters; mc : MO.counters; brgc: BrgO.counters } -let initial_status summary = { - summary = summary; +let initial_status = { ac = AO.initial_counters; mc = MO.initial_counters; brgc= BrgO.initial_counters; mst = MA.initial_status } -let count st count_fun c item = - if st.summary > 2 then count_fun Cps.start c item else c +let count count_fun c item = + if !L.level > 2 then count_fun Cps.start c item else c + +let brg_error s msg = + L.error BrgO.specs (L.Warn s :: msg) let main = +try let version_string = "Helena Checker 0.8.0 M - December 2008" in - let summary = ref 0 in let stage = ref 3 in let meta_file = ref None in let hierarchy = ref (fun h -> h + 2) in - let set_summary i = summary := i in + let set_summary i = L.level := i in let print_version () = L.warn version_string; exit 0 in let set_stage i = stage := i in let close = function @@ -58,33 +60,33 @@ let main = meta_file := Some (och, frm) in let read_file name = - if !summary > 0 then Time.gmtime version_string; - if !summary > 1 then + if !L.level > 0 then Time.gmtime version_string; + if !L.level > 1 then L.warn (P.sprintf "Processing file: %s" name); - if !summary > 0 then Time.utime_stamp "started"; + if !L.level > 0 then Time.utime_stamp "started"; let ich = open_in name in let lexbuf = Lexing.from_channel ich in let book = AutParser.book AutLexer.token lexbuf in close_in ich; - if !summary > 0 then Time.utime_stamp "parsed"; + if !L.level > 0 then Time.utime_stamp "parsed"; let rec aux st = function | [] -> st | item :: tl -> (* stage 3 *) let f st = function - | None -> st - | Some (_, (i, _, _, _)) -> - Log.warn (string_of_int i); st + | None -> st + | Some (_, (i, u, _)) -> + Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st in (* stage 2 *) let f st item = - let st = {st with brgc = count st BrgO.count_item st.brgc item} in + let st = {st with brgc = count BrgO.count_item st.brgc item} in if !stage > 2 then BrgU.type_check (f st) !hierarchy item else st in (* stage 1 *) let f mst item = let st = {st with - mst = mst; mc = count st MO.count_item st.mc item + mst = mst; mc = count MO.count_item st.mc item } in begin match !meta_file with | None -> () @@ -93,17 +95,17 @@ let main = if !stage > 1 then MBrg.brg_of_meta (f st) item else st in (* stage 0 *) - let st = {st with ac = count st AO.count_item st.ac item} in + let st = {st with ac = count AO.count_item st.ac item} in let st = if !stage > 0 then MA.meta_of_aut f st.mst item else st in aux st tl in - let st = aux (initial_status !summary) book in - if !summary > 0 then Time.utime_stamp "processed"; - if !summary > 2 then AO.print_counters Cps.start st.ac; - if !summary > 2 && !stage > 0 then MO.print_counters Cps.start st.mc; - if !summary > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc; + let st = aux initial_status book in + if !L.level > 0 then Time.utime_stamp "processed"; + if !L.level > 2 then AO.print_counters Cps.start st.ac; + if !L.level > 2 && !stage > 0 then MO.print_counters Cps.start st.mc; + if !L.level > 2 && !stage > 1 then BrgO.print_counters Cps.start st.brgc; in let help = "Usage: helena [ -V | -Ss | -m ] ..." in let help_S = " Set summary level" in @@ -116,4 +118,5 @@ let main = ("-m", Arg.String set_meta_file, help_m); ("-s", Arg.Int set_stage, help_s); ] read_file help; - if !summary > 0 then Time.utime_stamp "at exit" + if !L.level > 0 then Time.utime_stamp "at exit" +with BrgType.TypeError msg -> brg_error "Type Error" msg