From: Ferruccio Guidi Date: Fri, 7 Aug 2009 10:57:18 +0000 (+0000) Subject: basic_rg: improved interface, unwind removed from applicability check X-Git-Tag: make_still_working~3557 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=94c6cfe7e6b833190904c6b546668d716978a812;hp=29cfb9e2961e62c836cb50217905c0594a074e81;p=helm.git basic_rg: improved interface, unwind removed from applicability check basic_ag: improved interface common: kernel code sharing started --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 1f272e29e..f1c7339ee 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -31,8 +31,10 @@ 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 -basic_rg/brg.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx -basic_rg/brg.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx +common/common.cmo: lib/nUri.cmi automath/aut.cmx +common/common.cmx: lib/nUri.cmx automath/aut.cmx +basic_rg/brg.cmo: lib/log.cmi lib/cps.cmx common/common.cmx +basic_rg/brg.cmx: lib/log.cmx lib/cps.cmx common/common.cmx basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ lib/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi @@ -67,8 +69,8 @@ basic_rg/brgUntrusted.cmo: lib/log.cmi basic_rg/brgType.cmi \ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgUntrusted.cmi basic_rg/brgUntrusted.cmx: lib/log.cmx basic_rg/brgType.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi -basic_ag/bag.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx -basic_ag/bag.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx +basic_ag/bag.cmo: lib/log.cmi lib/cps.cmx common/common.cmx +basic_ag/bag.cmx: lib/log.cmx lib/cps.cmx common/common.cmx basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ lib/hierarchy.cmi basic_ag/bag.cmx basic_ag/bagOutput.cmi @@ -130,16 +132,16 @@ toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \ toplevel/top.cmo: lib/time.cmx lib/output.cmi lib/nUri.cmi \ toplevel/metaOutput.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \ toplevel/metaAut.cmi lib/log.cmi lib/hierarchy.cmi lib/cps.cmx \ - basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.cmi \ - basic_rg/brg.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \ + basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \ + basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \ basic_ag/bagReduction.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 lib/output.cmx lib/nUri.cmx \ toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \ toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx lib/cps.cmx \ - basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.cmx \ - basic_rg/brg.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \ + basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \ + basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \ basic_ag/bagReduction.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/Make b/helm/software/lambda-delta/Make index af2aa18aa..c9c8ff41a 100644 --- a/helm/software/lambda-delta/Make +++ b/helm/software/lambda-delta/Make @@ -1 +1 @@ -lib automath basic_rg basic_ag toplevel +lib automath common basic_rg basic_ag toplevel diff --git a/helm/software/lambda-delta/README b/helm/software/lambda-delta/README index cdedd30aa..2f2f894fc 100644 --- a/helm/software/lambda-delta/README +++ b/helm/software/lambda-delta/README @@ -1,4 +1,4 @@ -Helena 0.8.0 M (July 2008) +Helena 0.8.0 M * type "make" or "make opt" to compile the native executable diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index b04fc5ab6..585e8e388 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -12,8 +12,8 @@ (* kernel version: basic, absolute, global *) (* note : experimental *) -type uri = NUri.uri -type id = Aut.id +type uri = Common.uri +type id = Common.id type bind = Void (* exclusion *) | Abst of term (* abstraction *) @@ -26,9 +26,9 @@ and term = Sort of int (* hierarchy index *) | Appl of term * term (* argument, function *) | Bind of int * id * bind * term (* location, name, binder, scope *) -type obj = int * uri * bind (* age, uri, binder, contents *) +type obj = bind Common.obj (* age, uri, binder *) -type item = obj option +type item = bind Common.item type context = (int * id * bind) list (* location, name, binder *) diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml index fc1efcd77..4e147ae6d 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.ml +++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml @@ -17,7 +17,7 @@ module O = BagOutput module E = BagEnvironment module S = BagSubstitution -exception LRefNotFound of B.message +exception TypeError of B.message type machine = { i: int; @@ -45,15 +45,17 @@ let term_of_whdr = function let level = 5 -let error i = raise (LRefNotFound (L.items1 (string_of_int i))) +let error i = + let s = Printf.sprintf "local reference not found %u" i in + raise (TypeError (L.items1 s)) let log1 s c t = let sc, st = s ^ " in the context", "the term" in L.log O.specs level (L.ct_items1 sc c st t) -let log2 s c u t = - let sc, su, st = s ^ " in the context", "the term", "and the term" in - L.log O.specs level (L.ct_items2 sc c su u st t) +let log2 s cu u ct t = + let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in + L.log O.specs level (L.ct_items2 s1 cu s2 u s3 ct s2 t) let empty_machine = {i = 0; c = B.empty_context; s = []} @@ -113,8 +115,6 @@ let rec whd f c m x = (* Interface functions ******************************************************) -let nsi = ref false - let rec ho_whd f c m x = (* L.warn "entering R.ho_whd"; *) let aux m = function @@ -134,23 +134,25 @@ let ho_whd f c t = L.box level; log1 "Now scanning" c t; ho_whd f c empty_machine t -let rec are_convertible f a c m1 t1 m2 t2 = +let rec are_convertible f ~si a c m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) let rec aux m1 r1 m2 r2 = (* L.warn "entering R.are_convertible_aux"; *) let u, t = term_of_whdr r1, term_of_whdr r2 in - log2 "Now really converting" c u t; + log2 "Now really converting" c u c t; match r1, r2 with | Sort_ h1, Sort_ h2 -> if h1 = h2 then f a else f false | LRef_ (i1, _), LRef_ (i2, _) -> - if i1 = i2 then are_convertible_stacks f a c m1 m2 else f false + if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false | GRef_ (a1, _, B.Abst _), GRef_ (a2, _, B.Abst _) -> - if a1 = a2 then are_convertible_stacks f a c m1 m2 else f false + if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false | GRef_ (a1, _, B.Abbr v1), GRef_ (a2, _, B.Abbr v2) -> if a1 = a2 then - let f a = if a then f a else are_convertible f true c m1 v1 m2 v2 in - are_convertible_stacks f a c m1 m2 + let f a = + if a then f a else are_convertible f ~si true c m1 v1 m2 v2 + in + are_convertible_stacks f ~si a c m1 m2 else if a1 < a2 then whd (aux m1 r1) c m2 v2 else whd (aux_rev m2 r2) c m1 v1 @@ -162,25 +164,25 @@ let rec are_convertible f a c m1 t1 m2 t2 = let l = B.new_location () in let h c = let m1, m2 = inc m1, inc m2 in - let f t1 = S.subst (are_convertible f a c m1 t1 m2) l l2 t2 in + let f t1 = S.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in S.subst f l l1 t1 in let f r = if r then push "!" h c m1 l id1 w1 else f false in - are_convertible f a c m1 w1 m2 w2 + are_convertible f ~si a c m1 w1 m2 w2 (* we detect the AUT-QE reduction rule for type/prop inclusion *) - | Sort_ _, Bind_ (l2, id2, w2, t2) when !nsi -> + | Sort_ _, Bind_ (l2, id2, w2, t2) when si -> let m1, m2 = inc m1, inc m2 in - let f c = are_convertible f a c m1 (term_of_whdr r1) m2 t2 in + let f c = are_convertible f ~si a c m1 (term_of_whdr r1) m2 t2 in push "nsi" f c m2 l2 id2 w2 | _ -> f false and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in let g m1 r1 = whd (aux m1 r1) c m2 t2 in if a = false then f false else whd g c m1 t1 -and are_convertible_stacks f a c m1 m2 = +and are_convertible_stacks f ~si a c m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in - let map f a v1 v2 = are_convertible f a c mm1 v1 mm2 v2 in + let map f a v1 v2 = are_convertible f ~si a c mm1 v1 mm2 v2 in if List.length m1.s <> List.length m2.s then begin (* L.warn (Printf.sprintf "Different lengths: %u %u" @@ -191,7 +193,7 @@ and are_convertible_stacks f a c m1 m2 = else C.list_fold_left2 f map a m1.s m2.s -let are_convertible f c u t = +let are_convertible f ?(si=false) c u t = let f b = L.unbox level; f b in - L.box level; log2 "Now converting" c u t; - are_convertible f true c empty_machine u empty_machine t + L.box level; log2 "Now converting" c u c t; + are_convertible f ~si true c empty_machine u empty_machine t diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.mli b/helm/software/lambda-delta/basic_ag/bagReduction.mli index 28c29e7f2..35c017581 100644 --- a/helm/software/lambda-delta/basic_ag/bagReduction.mli +++ b/helm/software/lambda-delta/basic_ag/bagReduction.mli @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception LRefNotFound of Bag.message +exception TypeError of Bag.message type ho_whd_result = | Sort of int @@ -19,6 +19,4 @@ val ho_whd: (ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a val are_convertible: - (bool -> 'a) -> Bag.context -> Bag.term -> Bag.term -> 'a - -val nsi: bool ref + (bool -> 'a) -> ?si:bool -> Bag.context -> Bag.term -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml index 9cf5c5cb7..c398e034d 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.ml +++ b/helm/software/lambda-delta/basic_ag/bagType.ml @@ -19,8 +19,6 @@ module O = BagOutput module E = BagEnvironment module R = BagReduction -exception TypeError of B.message - (* Internal functions *******************************************************) let level = 4 @@ -31,13 +29,13 @@ let log1 s c t = let error1 st c t = let sc = "In the context" in - raise (TypeError (L.ct_items1 sc c st t)) + raise (R.TypeError (L.ct_items1 sc c st t)) let error3 c t1 t2 t3 = let sc, st1, st2, st3 = "In the context", "the term", "is of type", "but must be of type" in - raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) + raise (R.TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) let mk_gref u l = let map t v = B.Appl (v, t) in @@ -45,7 +43,7 @@ let mk_gref u l = (* Interface functions ******************************************************) -let rec b_type_of f g c x = +let rec b_type_of f ~si g c x = (* L.warn "Entering T.b_type_of"; *) log1 "Now checking" c x; match x with @@ -75,25 +73,25 @@ let rec b_type_of f g c x = let f xv xt tt = f (S.sh2 v xv t xt x (B.bind_abbr l id)) (B.bind_abbr l id xv tt) in - let f xv cc = b_type_of (f xv) g cc t in + let f xv cc = b_type_of (f xv) ~si g cc t in let f xv = B.push "type abbr" (f xv) c l id (B.Abbr xv) in let f xv vv = match xv with | B.Cast _ -> f xv | _ -> f (B.Cast (vv, xv)) in - type_of f g c v + type_of f ~si g c v | B.Bind (l, id, B.Abst u, t) -> let f xu xt tt = f (S.sh2 u xu t xt x (B.bind_abst l id)) (B.bind_abst l id xu tt) in - let f xu cc = b_type_of (f xu) g cc t in + let f xu cc = b_type_of (f xu) ~si g cc t in let f xu _ = B.push "type abst" (f xu) c l id (B.Abst xu) in - type_of f g c u + type_of f ~si g c u | B.Bind (l, id, B.Void, t) -> let f xt tt = f (S.sh1 t xt x (B.bind l id B.Void)) (B.bind l id B.Void tt) in - let f cc = b_type_of f g cc t in + let f cc = b_type_of f ~si g cc t in B.push "type void" f c l id B.Void | B.Appl (v, t) -> let f xv vv xt tt = function @@ -106,22 +104,22 @@ let rec b_type_of f g c x = if a then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else error3 c xv vv w in - R.are_convertible f c w vv + R.are_convertible f ~si c w vv | _ -> error1 "not a function" c xt in let f xv vv xt tt = R.ho_whd (f xv vv xt tt) c tt in - let f xv vv = b_type_of (f xv vv) g c t in - type_of f g c v + let f xv vv = b_type_of (f xv vv) ~si g c t in + type_of f ~si g c v | B.Cast (u, t) -> let f xu xt tt a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) if a then f (S.sh2 u xu t xt x B.cast) xu else error3 c xt tt xu in - let f xu xt tt = R.are_convertible (f xu xt tt) c xu tt in - let f xu _ = b_type_of (f xu) g c t in - type_of f g c u + let f xu xt tt = R.are_convertible (f xu xt tt) ~si c xu tt in + let f xu _ = b_type_of (f xu) ~si g c t in + type_of f ~si g c u -and type_of f g c x = +and type_of f ?(si=false) g c x = let f t u = L.unbox level; f t u in - L.box level; b_type_of f g c x + L.box level; b_type_of f ~si g c x diff --git a/helm/software/lambda-delta/basic_ag/bagType.mli b/helm/software/lambda-delta/basic_ag/bagType.mli index 24d1f57a2..e0ec3c3c2 100644 --- a/helm/software/lambda-delta/basic_ag/bagType.mli +++ b/helm/software/lambda-delta/basic_ag/bagType.mli @@ -9,8 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception TypeError of Bag.message - val type_of: - (Bag.term -> Bag.term -> 'a) -> + (Bag.term -> Bag.term -> 'a) -> ?si:bool -> Hierarchy.graph -> Bag.context -> Bag.term -> 'a diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml index 600807c67..e588caa49 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.ml +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.ml @@ -17,16 +17,16 @@ module T = BagType (* Interface functions ******************************************************) (* to share *) -let type_check f g = function +let type_check f ?(si=false) g = function | None -> f None None | Some (a, uri, B.Abst t) -> let f tt obj = f (Some tt) (Some obj) in let f xt tt = E.set_obj (f tt) (a, uri, B.Abst xt) in - L.loc := a; T.type_of f g B.empty_context t + L.loc := a; T.type_of f ~si g B.empty_context t | Some (a, uri, B.Abbr t) -> let f tt obj = f (Some tt) (Some obj) in let f xt tt = E.set_obj (f tt) (a, uri, B.Abbr xt) in - L.loc := a; T.type_of f g B.empty_context t + L.loc := a; T.type_of f ~si g B.empty_context t | Some (a, uri, B.Void) -> let f obj = f None (Some obj) in L.loc := a; E.set_obj f (a, uri, B.Void) diff --git a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli index 54ae7717c..3ecd2f0d8 100644 --- a/helm/software/lambda-delta/basic_ag/bagUntrusted.mli +++ b/helm/software/lambda-delta/basic_ag/bagUntrusted.mli @@ -10,4 +10,5 @@ V_______________________________________________________________ *) val type_check: - (Bag.term option -> Bag.item -> 'a) -> Hierarchy.graph -> Bag.item -> 'a + (Bag.term option -> Bag.item -> 'a) -> ?si:bool -> + Hierarchy.graph -> Bag.item -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index e42db3319..8b0d54533 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -12,8 +12,8 @@ (* kernel version: basic, relative, global *) (* note : ufficial basic lambda-delta *) -type uri = NUri.uri -type id = Aut.id +type uri = Common.uri +type id = Common.id type bind = Void (* exclusion *) | Abst of term (* abstraction *) @@ -31,9 +31,9 @@ and attr = Name of bool * id (* real?, name *) and attrs = attr list -type obj = int * uri * bind (* age, uri, binder, contents *) +type obj = bind Common.obj (* age, uri, binder *) -type item = obj option +type item = bind Common.item type context = (attrs * bind) list (* attrs, binder *) diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 16dc395bb..3b4820abf 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -18,7 +18,7 @@ module O = BrgOutput module E = BrgEnvironment module S = BrgSubstitution -exception LRefNotFound of B.message +exception TypeError of B.message type machine = { c: B.context; @@ -29,44 +29,49 @@ type machine = { let level = 5 -let error i = raise (LRefNotFound (L.items1 (string_of_int i))) - let log1 s c t = let sc, st = s ^ " in the context", "the term" in L.log O.specs level (L.ct_items1 sc c st t) -let log2 s c u t = - let sc, su, st = s ^ " in the context", "the term", "and the term" in - L.log O.specs level (L.ct_items2 sc c su u st t) +let log2 s cu u ct t = + let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in + L.log O.specs level (L.ct_items2 s1 cu s2 u s3 ct s2 t) + +let error0 i = + let s = Printf.sprintf "local reference not found %u" i in + raise (TypeError (L.items1 s)) + +let error1 st c t = + let sc = "In the context" in + raise (TypeError (L.ct_items1 sc c st t)) -let empty_machine = { - c = B.empty_context; s = [] +let error3 c t1 t2 t3 = + let sc, st1, st2, st3 = + "In the context", "the term", "is of type", "but must be of type" + in + raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) + +let empty_machine c = { + c = c; s = [] } -let get f c m i = +let get f m i = let f e = function | Some (_, b) -> f e b - | None -> error i + | None -> error0 i in - let f c = B.get f c i in - B.append f c m.c + B.get f m.c i let lift_stack f s = let map f (v, i) = f (v, succ i) in Cps.list_map f map s -let unwind_to_term f m t = - let map f t (a, b) = f (B.Bind (a, b, t)) in - let f mc = C.list_fold_left f map t mc in - assert (m.s = []); - B.contents f m.c - let push f m a b = assert (m.s = []); f {m with c = (a, b) :: m.c} (* to share *) -let rec step f ?(delta=false) ?(rt=false) c m x = +let rec step f ?(delta=false) ?(rt=false) m x = (* L.warn "entering R.step"; *) match x with | B.Sort _ -> f m x @@ -74,10 +79,10 @@ let rec step f ?(delta=false) ?(rt=false) c m x = let f = function | _, _, B.Abbr v when delta -> P.add ~gdelta:1 (); - step f ~delta ~rt c m v + step f ~delta ~rt m v | _, _, B.Abst w when rt -> P.add ~grt:1 (); - step f ~delta ~rt c m w + step f ~delta ~rt m w | e, _, b -> f m (B.GRef (B.Entry (e, b) :: a, uri)) in @@ -86,61 +91,59 @@ let rec step f ?(delta=false) ?(rt=false) c m x = let f e = function | B.Abbr v -> P.add ~ldelta:1 (); - step f ~delta ~rt c m v + step f ~delta ~rt m v | B.Abst w when rt -> P.add ~lrt:1 (); - step f ~delta ~rt c m w + step f ~delta ~rt m w | b -> f m (B.LRef (B.Entry (e, b) :: a, i)) in let f e = S.lift_bind (f e) (succ i) (0) in - get f c m i + get f m i | B.Cast (_, _, t) -> P.add ~tau:1 (); - step f ~delta ~rt c m t + step f ~delta ~rt m t | B.Appl (_, v, t) -> - step f ~delta ~rt c {m with s = (v, 0) :: m.s} t + step f ~delta ~rt {m with s = (v, 0) :: m.s} t | B.Bind (a, B.Abst w, t) -> begin match m.s with | [] -> f m x | (v, h) :: tl -> P.add ~beta:1 ~upsilon:(List.length tl) (); - let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in - let f mc = lift_stack (f mc) tl in + let f c s = step f ~delta ~rt {c = c; s = s} t in + let f c = lift_stack (f c) tl in let f v = B.push f m.c a (B.Abbr v (* (B.Cast ([], w, v)) *) ) in S.lift f h (0) v end | B.Bind (a, b, t) -> P.add ~upsilon:(List.length m.s) (); - let f sc mc = step f ~delta ~rt c {c = mc; s = sc} t in - let f sc = B.push (f sc) m.c a b in + let f s c = step f ~delta ~rt {c = c; s = s} t in + let f s = B.push (f s) m.c a b in lift_stack f m.s (* Interface functions ******************************************************) - -let domain f c t = + +let domain f m t = let f r = L.unbox level; f r in let f m = function - | B.Bind (_, B.Abst w, _) -> - let f w = f (Some w) in unwind_to_term f m w - | x -> f None + | B.Bind (_, B.Abst w, _) -> f m w + | _ -> error1 "not a function" m.c t in - L.box level; log1 "Now scanning" c t; - step f ~delta:true ~rt:true c empty_machine t + L.box level; log1 "Now scanning" m.c t; + step f ~delta:true ~rt:true m t -let rec ac_nfs f ~si r c m1 u m2 t = -(* L.warn "entering R.are_convertible_aux"; *) - log2 "Now converting nfs" c u t; +let rec ac_nfs f ~si r m1 u m2 t = + log2 "Now converting nfs" m1.c u m2.c t; match u, t with | B.Sort (_, h1), B.Sort (_, h2) -> if h1 = h2 then f r else f false | B.LRef (B.Entry (e1, B.Abst _) :: _, i1), B.LRef (B.Entry (e2, B.Abst _) :: _, i2) -> P.add ~zeta:(i1+i2-e1-e2) (); - if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false + if e1 = e2 then ac_stacks f ~si r m1 m2 else f false | B.GRef (B.Entry (e1, B.Abst _) :: _, _), B.GRef (B.Entry (e2, B.Abst _) :: _, _) -> - if e1 = e2 then ac_stacks f ~si r c m1 m2 else f false + if e1 = e2 then ac_stacks f ~si r m1 m2 else f false | B.GRef (B.Entry (e1, B.Abbr v1) :: _, _), B.GRef (B.Entry (e2, B.Abbr v2) :: _, _) -> if e1 = e2 then @@ -148,48 +151,48 @@ let rec ac_nfs f ~si r c m1 u m2 t = if r then f r else begin P.add ~gdelta:2 (); - ac f ~si true c m1 v1 m2 v2 + ac f ~si true m1 v1 m2 v2 end in - ac_stacks f ~si r c m1 m2 + ac_stacks f ~si r m1 m2 else if e1 < e2 then begin P.add ~gdelta:1 (); - step (ac_nfs f ~si r c m1 u) c m2 v2 + step (ac_nfs f ~si r m1 u) m2 v2 end else begin P.add ~gdelta:1 (); - step (ac_nfs_rev f ~si r c m2 t) c m1 v1 + step (ac_nfs_rev f ~si r m2 t) m1 v1 end | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) -> P.add ~gdelta:1 (); - step (ac_nfs f ~si r c m1 u) c m2 v2 + step (ac_nfs f ~si r m1 u) m2 v2 | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ -> P.add ~gdelta:1 (); - step (ac_nfs_rev f ~si r c m2 t) c m1 v1 + step (ac_nfs_rev f ~si r m2 t) m1 v1 | B.Bind (a1, (B.Abst w1 as b1), t1), B.Bind (a2, (B.Abst w2 as b2), t2) -> - let g m1 m2 = ac f ~si r c m1 t1 m2 t2 in + let g m1 m2 = ac f ~si r m1 t1 m2 t2 in let g m1 = push (g m1) m2 a2 b2 in let f r = if r then push g m1 a1 b1 else f false in - ac f ~si r c m1 w1 m2 w2 + ac f ~si r m1 w1 m2 w2 | B.Sort _, B.Bind (a, b, t) when si -> P.add ~si:1 (); - let f m1 m2 = ac f ~si r c m1 u m2 t in + let f m1 m2 = ac f ~si r m1 u m2 t in let f m1 = push (f m1) m2 a b in push f m1 a b | _ -> f false -and ac_nfs_rev f ~si r c m2 t m1 u = ac_nfs f ~si r c m1 u m2 t +and ac_nfs_rev f ~si r m2 t m1 u = ac_nfs f ~si r m1 u m2 t -and ac f ~si r c m1 t1 m2 t2 = +and ac f ~si r m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) - let g m1 t1 = step (ac_nfs f ~si r c m1 t1) c m2 t2 in - if r = false then f false else step g c m1 t1 + let g m1 t1 = step (ac_nfs f ~si r m1 t1) m2 t2 in + if r = false then f false else step g m1 t1 -and ac_stacks f ~si r c m1 m2 = +and ac_stacks f ~si r m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in let map f r (v1, h1) (v2, h2) = - let f v1 = S.lift (ac f ~si r c mm1 v1 mm2) h2 (0) v2 in + let f v1 = S.lift (ac f ~si r mm1 v1 mm2) h2 (0) v2 in S.lift f h1 (0) v1 in if List.length m1.s <> List.length m2.s then @@ -202,7 +205,15 @@ and ac_stacks f ~si r c m1 m2 = else C.list_fold_left2 f map r m1.s m2.s -let are_convertible f ?(si=false) c u t = +let assert_conversion f ?(si=false) ?(rt=false) c u w v = let f b = L.unbox level; f b in - L.box level; log2 "Now converting" c u t; - ac f ~si true c empty_machine u empty_machine t + let mw = empty_machine c in + let f mu u = + let f = function + | true -> f () + | false -> error3 c v w u + in + L.box level; log2 "Now converting" c u c w; + ac f ~si true mu u mw w + in + if rt then domain f mw u else f mw u diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index 57e2bfb41..e5c670dd4 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -9,11 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +exception TypeError of Brg.message -exception LRefNotFound of Brg.message - -val domain: - (Brg.term option -> 'a) -> Brg.context -> Brg.term -> 'a - -val are_convertible: - (bool -> 'a) -> ?si:bool -> Brg.context -> Brg.term -> Brg.term -> 'a +(* arguments: expected type, inferred type, typed term *) +val assert_conversion: + (unit -> 'a) -> ?si:bool -> ?rt:bool -> + Brg.context -> Brg.term -> 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 85ecf995a..cc9245f92 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -20,8 +20,6 @@ module E = BrgEnvironment module S = BrgSubstitution module R = BrgReduction -exception TypeError of B.message - (* Internal functions *******************************************************) let level = 4 @@ -32,20 +30,11 @@ let log1 s c t = let error1 st c t = let sc = "In the context" in - raise (TypeError (L.ct_items1 sc c st t)) - -let error3 c t1 t2 t3 = - let sc, st1, st2, st3 = - "In the context", "the term", "is of type", "but must be of type" - in - raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) + raise (R.TypeError (L.ct_items1 sc c st t)) (* Interface functions ******************************************************) -let si = ref false - -let rec b_type_of f g c x = -(* L.warn "Entering T.b_type_of"; *) +let rec b_type_of f ~si g c x = log1 "Now checking" c x; match x with | B.Sort (a, h) -> @@ -76,53 +65,41 @@ let rec b_type_of f g c x = let f xv xt tt = f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt) in - let f xv cc = b_type_of (f xv) g cc t in + let f xv cc = b_type_of (f xv) ~si g cc t in let f xv = B.push (f xv) c a (B.Abbr xv) in let f xv vv = match xv with | B.Cast _ -> f xv | _ -> assert false (* f (B.Cast ([], vv, xv)) *) in - type_of f g c v + type_of f ~si g c v | B.Bind (a, B.Abst u, t) -> let f xu xt tt = f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt) in - let f xu cc = b_type_of (f xu) g cc t in + let f xu cc = b_type_of (f xu) ~si g cc t in let f xu _ = B.push (f xu) c a (B.Abst xu) in - type_of f g c u + type_of f ~si g c u | B.Bind (a, B.Void, t) -> let f xt tt = f (A.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt) in - let f cc = b_type_of f g cc t in + let f cc = b_type_of f ~si g cc t in B.push f c a B.Void | B.Appl (a, v, t) -> - let f xv vv xt tt = function - | Some w -> - L.box (succ level); - L.log O.specs (succ level) (L.t_items1 "Just scanned" c w); - L.unbox (succ level); - let f r = -(* L.warn (Printf.sprintf "Convertible: %b" a); *) - if r then f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) - else error3 c xv vv w - in - R.are_convertible f ~si:!si c w vv - | None -> - error1 "not a function" c xt + let f xv vv xt tt = + let f () = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in + R.assert_conversion f ~si ~rt:true c tt vv xv in - let f xv vv xt tt = R.domain (f xv vv xt tt) c tt in - let f xv vv = b_type_of (f xv vv) g c t in - type_of f g c v + let f xv vv = b_type_of (f xv vv) ~si g c t in + type_of f ~si g c v | B.Cast (a, u, t) -> - let f xu xt tt r = - (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if r then f (A.sh2 u xu t xt x (B.cast a)) xu else error3 c xt tt xu + let f xu xt tt = + let f () = f (A.sh2 u xu t xt x (B.cast a)) xu in + R.assert_conversion f ~si c xu tt xt in - let f xu xt tt = R.are_convertible ~si:!si (f xu xt tt) c xu tt in - let f xu _ = b_type_of (f xu) g c t in - type_of f g c u + let f xu _ = b_type_of (f xu) ~si g c t in + type_of f ~si g c u -and type_of f g c x = +and type_of f ?(si=false) g c x = let f t u = L.unbox level; f t u in - L.box level; b_type_of f g c x + L.box level; b_type_of f ~si g c x diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index 26a33509c..99aef9506 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -9,10 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception TypeError of Brg.message - val type_of: - (Brg.term -> Brg.term -> 'a) -> + (Brg.term -> Brg.term -> 'a) -> ?si:bool -> Hierarchy.graph -> Brg.context -> Brg.term -> 'a - -val si: bool ref diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index c57b6eb16..65735066a 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -17,16 +17,16 @@ module T = BrgType (* Interface functions ******************************************************) (* to share *) -let type_check f g = function +let type_check f ?(si=false) g = function | None -> f None None | Some (e, uri, B.Abst t) -> let f tt obj = f (Some tt) (Some obj) in let f xt tt = E.set_obj (f tt) (e, uri, B.Abst xt) in - L.loc := e; T.type_of f g B.empty_context t + L.loc := e; T.type_of f ~si g B.empty_context t | Some (e, uri, B.Abbr t) -> let f tt obj = f (Some tt) (Some obj) in let f xt tt = E.set_obj (f tt) (e, uri, B.Abbr xt) in - L.loc := e; T.type_of f g B.empty_context t + L.loc := e; T.type_of f ~si g B.empty_context t | Some (e, uri, B.Void) -> let f obj = f None (Some obj) in L.loc := e; E.set_obj f (e, uri, B.Void) diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli index 92e401e7d..e2066f998 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.mli +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.mli @@ -10,4 +10,5 @@ V_______________________________________________________________ *) val type_check: - (Brg.term option -> Brg.item -> 'a) -> Hierarchy.graph -> Brg.item -> 'a + (Brg.term option -> Brg.item -> 'a) -> ?si:bool -> + Hierarchy.graph -> Brg.item -> 'a diff --git a/helm/software/lambda-delta/common/Make b/helm/software/lambda-delta/common/Make new file mode 100644 index 000000000..30e1159c2 --- /dev/null +++ b/helm/software/lambda-delta/common/Make @@ -0,0 +1 @@ +common diff --git a/helm/software/lambda-delta/common/common.ml b/helm/software/lambda-delta/common/common.ml new file mode 100644 index 000000000..7e9b7cea8 --- /dev/null +++ b/helm/software/lambda-delta/common/common.ml @@ -0,0 +1,17 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +type uri = NUri.uri +type id = Aut.id + +type 'bind obj = int * uri * 'bind (* age, uri, binder *) + +type 'bind item = 'bind obj option diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index 9c2ecefa2..e28ea326a 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -71,10 +71,10 @@ let t_items1 st c t = let ct_items1 sc c st t = [Warn sc; Context c; Warn st; Term (c, t)] -let ct_items2 sc c st1 t1 st2 t2 = - ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2)] +let ct_items2 sc1 c1 st1 t1 sc2 c2 st2 t2 = + ct_items1 sc1 c1 st1 t1 @ ct_items1 sc2 c2 st2 t2 let ct_items3 sc c st1 t1 st2 t2 st3 t3 = - ct_items2 sc c st1 t1 st2 t2 @ [Warn st3; Term (c, t3)] + ct_items1 sc c st1 t1 @ [Warn st2; Term (c, t2); Warn st3; Term (c, t3)] let warn msg = F.fprintf std "@,%s" msg diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index 241247c18..6a2cc90cd 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -48,7 +48,8 @@ val ct_items1: string -> 'a -> string -> 'b -> ('a, 'b) item list val ct_items2: - string -> 'a -> string -> 'b -> string -> 'b -> ('a, 'b) item list + string -> 'a -> string -> 'b -> string -> 'a -> string -> 'b -> + ('a, 'b) item list val ct_items3: string -> 'a -> string -> 'b -> string -> 'b -> string -> 'b -> diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 873d5c590..507d11908 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -13,6 +13,7 @@ module P = Printf module U = NUri module C = Cps module L = Log +module T = Time module H = Hierarchy module O = Output module AP = AutProcess @@ -21,7 +22,7 @@ module MA = MetaAut module MO = MetaOutput module MBrg = MetaBrg module BrgO = BrgOutput -module BrgT = BrgType +module BrgR = BrgReduction module BrgU = BrgUntrusted module MBag = MetaBag module BagO = BagOutput @@ -34,16 +35,18 @@ type status = { ac : AO.counters; mc : MO.counters; brgc: BrgO.counters; - bagc: BagO.counters + bagc: BagO.counters; + si : bool } -let initial_status cover = { +let initial_status cover si = { ac = AO.initial_counters; mc = MO.initial_counters; brgc = BrgO.initial_counters; bagc = BagO.initial_counters; mst = MA.initial_status ~cover (); - ast = AP.initial_status + ast = AP.initial_status; + si = si } let count count_fun c item = @@ -86,33 +89,25 @@ let count_item st = function | BrgItem item -> {st with brgc = count BrgO.count_item st.brgc item} | BagItem item -> {st with bagc = count BagO.count_item st.bagc item} -let type_check f st g = function - | BrgItem item -> - let f _ = function - | None -> f st None - | Some (i, u, _) -> f st (Some (i, u)) - in - BrgU.type_check f g item - | BagItem item -> - let f _ = function - | None -> f st None - | Some (i, u, _) -> f st (Some (i, u)) - in - BagU.type_check f g item - -let si () = match !kernel with - | Brg -> BrgT.si := true - | Bag -> BagR.nsi := true +let type_check f st g k = + let f _ = function + | None -> f st None + | Some (i, u, _) -> f st (Some (i, u)) + in + match k with + | BrgItem item -> BrgU.type_check f ~si:st.si g item + | BagItem item -> BagU.type_check f ~si:st.si g item (****************************************************************************) let main = try - let version_string = "Helena 0.8.0 M - July 2009" in + let version_string = "Helena 0.8.0 M - August 2009" in let stage = ref 3 in let meta_file = ref None in let progress = ref false in let use_cover = ref true in + let si = ref false in let set_hierarchy s = let f = function | Some g -> H.graph := g @@ -140,15 +135,15 @@ try meta_file := Some (och, frm) in let read_file name = - if !L.level > 0 then Time.gmtime version_string; + if !L.level > 0 then T.gmtime version_string; if !L.level > 1 then L.warn (P.sprintf "Processing file: %s" name); - if !L.level > 0 then Time.utime_stamp "started"; + if !L.level > 0 then T.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 !L.level > 0 then Time.utime_stamp "parsed"; + if !L.level > 0 then T.utime_stamp "parsed"; let rec aux st = function | [] -> st | item :: tl -> @@ -157,7 +152,7 @@ try | None -> st | Some (i, u) -> if !progress then - Log.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); + L.warn (P.sprintf "[%u] %s" i (U.string_of_uri u)); st in (* stage 2 *) @@ -191,8 +186,8 @@ try if !use_cover then Filename.chop_extension (Filename.basename name) else "" in - let st = aux (initial_status cover) book in - if !L.level > 0 then Time.utime_stamp "processed"; + let st = aux (initial_status cover !si) book in + 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 then AO.print_process_counters C.start st.ast; if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc; @@ -226,10 +221,10 @@ try ("-k", Arg.String set_kernel, help_k); ("-m", Arg.String set_meta_file, help_m); ("-p", Arg.Set progress, help_p); - ("-u", Arg.Unit si, help_u); + ("-u", Arg.Set si, help_u); ("-s", Arg.Int set_stage, help_s) ] read_file help; - if !L.level > 0 then Time.utime_stamp "at exit"; + if !L.level > 0 then T.utime_stamp "at exit"; flush () -with BagType.TypeError msg -> bag_error "Type Error" msg - | BrgT.TypeError msg -> brg_error "Type Error" msg +with BagR.TypeError msg -> bag_error "Type Error" msg + | BrgR.TypeError msg -> brg_error "Type Error" msg