From: Ferruccio Guidi Date: Sun, 16 Aug 2009 14:37:47 +0000 (+0000) Subject: - proper KAM with closures implemented for the brg kernel X-Git-Tag: make_still_working~3539 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f983656c56d37a50536e50a319114dbfa592c9a0;hp=c8011c7ad75be5d03c4d4bb2e6900af32ad65c07;p=helm.git - proper KAM with closures implemented for the brg kernel --- diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 148c2377a..bcaca037f 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -36,8 +36,8 @@ common/item.cmx: lib/nUri.cmx automath/aut.cmx common/library.cmi: common/item.cmx common/hierarchy.cmi common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/library.cmi common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/library.cmi -basic_rg/brg.cmo: lib/log.cmi common/item.cmx lib/cps.cmx -basic_rg/brg.cmx: lib/log.cmx common/item.cmx lib/cps.cmx +basic_rg/brg.cmo: lib/log.cmi common/item.cmx +basic_rg/brg.cmx: lib/log.cmx common/item.cmx basic_rg/brgOutput.cmi: lib/log.cmi common/item.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi @@ -51,14 +51,15 @@ basic_rg/brgEnvironment.cmx: lib/nUri.cmx lib/log.cmx basic_rg/brg.cmx \ basic_rg/brgSubstitution.cmi: basic_rg/brg.cmx basic_rg/brgSubstitution.cmo: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi basic_rg/brgSubstitution.cmx: basic_rg/brg.cmx basic_rg/brgSubstitution.cmi -basic_rg/brgReduction.cmi: basic_rg/brg.cmx +basic_rg/brgReduction.cmi: lib/log.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \ - lib/cps.cmx basic_rg/brgSubstitution.cmi basic_rg/brgOutput.cmi \ - basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi + lib/cps.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi \ + basic_rg/brg.cmx basic_rg/brgReduction.cmi basic_rg/brgReduction.cmx: common/output.cmx lib/nUri.cmx lib/log.cmx \ - lib/cps.cmx basic_rg/brgSubstitution.cmx basic_rg/brgOutput.cmx \ - basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgType.cmi: common/hierarchy.cmi basic_rg/brg.cmx + lib/cps.cmx basic_rg/brgOutput.cmx basic_rg/brgEnvironment.cmx \ + basic_rg/brg.cmx basic_rg/brgReduction.cmi +basic_rg/brgType.cmi: common/hierarchy.cmi basic_rg/brgReduction.cmi \ + basic_rg/brg.cmx basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi lib/cps.cmx basic_rg/brgSubstitution.cmi \ basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \ @@ -69,9 +70,11 @@ basic_rg/brgType.cmx: lib/share.cmx lib/nUri.cmx lib/log.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgType.cmi basic_rg/brgUntrusted.cmi: common/hierarchy.cmi basic_rg/brg.cmx 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/brgReduction.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_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx basic_rg/brg.cmx \ + basic_rg/brgUntrusted.cmi basic_ag/bag.cmo: lib/log.cmi common/item.cmx lib/cps.cmx basic_ag/bag.cmx: lib/log.cmx common/item.cmx lib/cps.cmx basic_ag/bagOutput.cmi: lib/log.cmi basic_ag/bag.cmx diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index d62a130a4..5ad05a72f 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -15,6 +15,11 @@ type uri = Item.uri type id = Item.id +type attr = Name of bool * id (* real?, name *) + | Apix of int (* additional position index *) + +type attrs = attr list + type bind = Void (* exclusion *) | Abst of term (* abstraction *) | Abbr of term (* abbreviation *) @@ -26,16 +31,13 @@ and term = Sort of attrs * int (* attrs, hierarchy index *) | Appl of attrs * term * term (* attrs, argument, function *) | Bind of attrs * bind * term (* attrs, binder, scope *) -and attr = Name of bool * id (* real?, name *) - | Entry of int * bind (* age, binder *) - -and attrs = attr list - type obj = bind Item.obj (* age, uri, binder *) type item = bind Item.item -type context = (attrs * bind) list (* attrs, binder *) +type context = Null +(* Cons: tail, relative context, attrs, binder *) + | Cons of context * context option * attrs * bind type message = (context, term) Log.item list @@ -59,30 +61,39 @@ let bind_abbr a v t = Bind (a, Abbr v, t) (* context handling functions ***********************************************) -let empty_context = [] +let empty_context = Null -let push f es a b = - let c = (a, b) :: es in f c +let push f es ?c a b = + let es = Cons (es, c, a, b) in f es -let append f es1 es2 = - f (List.append es2 es1) - -let map f map es = - Cps.list_map f map es - -let contents f es = f es - -let get f es i = - let rec aux e i = function - | [] -> f e None - | hd :: tl -> - if i = 0 then f e (Some hd) else - let e = match hd with _, Abst _ -> succ e | _ -> e in - aux e (pred i) tl +let get err f es i = + let rec aux j = function + | Null -> err i + | Cons (tl, None, a, b) when j = 0 -> f tl a b + | Cons (_, Some c, a, b) when j = 0 -> f c a b + | Cons (tl, _, _, _) -> aux (pred j) tl in - aux 0 i es - -let rec name f = function - | [] -> f None - | Name (r, n) :: _ -> f (Some (r, n)) - | _ :: tl -> name f tl + aux i es + +let rec rev_iter f map = function + | Null -> f () + | Cons (tl, None, a, b) -> + let f () = map f tl a b in rev_iter f map tl + | Cons (tl, Some c, a, b) -> + let f () = map f c a b in rev_iter f map tl + +let rec fold_left f map x = function + | Null -> f x + | Cons (tl, _, a, b) -> + let f x = fold_left f map x tl in + map f x a b + +let rec name err f = function + | [] -> err () + | Name (r, n) :: _ -> f n r + | _ :: tl -> name err f tl + +let rec apix err f = function + | [] -> err () + | Apix i :: _ -> f i + | _ :: tl -> apix err f tl diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index fb33da537..dc697bff4 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -11,6 +11,7 @@ module P = Printf module F = Format +module C = Cps module U = NUri module L = Log module H = Hierarchy @@ -58,15 +59,15 @@ and count_term f c e = function | B.Sort _ -> f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} | B.LRef (_, i) -> - let f _ = function - | None - | Some (_, B.Abst _) -> + let err _ = f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} in + let f _ _ = function + | B.Abst _ + | B.Void -> f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} - | Some (_, B.Abbr _) - | Some (_, B.Void) -> + | B.Abbr _ -> f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes} in - B.get f e i + B.get err f e i | B.GRef (_, u) -> let c = if Cps.list_mem ~eq:U.eq u c.uris @@ -96,8 +97,10 @@ let count_obj f c = function | (_, _, B.Abbr v) -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c B.empty_context v - | (_, _, B.Void) -> - let c = {c with evoids = succ c.evoids; xnodes = succ c.xnodes} in + | (_, u, B.Void) -> + let c = {c with + evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris + } in f c let count_item f c = function @@ -130,12 +133,12 @@ let print_counters f c = (* context/term pretty printing *********************************************) let id frm a = - let f = function - | None -> assert false - | Some (true, n) -> F.fprintf frm "%s" n - | Some (false, n) -> F.fprintf frm "^%s" n + let err () = assert false in + let f n = function + | true -> F.fprintf frm "%s" n + | false -> F.fprintf frm "^%s" n in - B.name f a + B.name err f a let rec pp_term c frm = function | B.Sort (_, h) -> @@ -145,11 +148,9 @@ let rec pp_term c frm = function in H.get_sort f h | B.LRef (_, i) -> - let f _ = function - | Some (a, _) -> F.fprintf frm "@[%a@]" id a - | None -> F.fprintf frm "@[#%u@]" i - in - if !O.indexes then f 0 None else B.get f c i + let err i = F.fprintf frm "@[#%u@]" i in + let f _ a _ = F.fprintf frm "@[%a@]" id a in + if !O.indexes then err i else B.get err f c 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 @@ -170,17 +171,15 @@ let rec pp_term c frm = function B.push f c a B.Void let pp_context frm c = - let pp_entry frm = function - | a, B.Abst w -> - F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w - | a, B.Abbr v -> - F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v - | a, B.Void -> - F.fprintf frm "@,%a" id a + let pp_entry f c a = function + | B.Abst w -> + F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f () + | B.Abbr v -> + F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v; f () + | B.Void -> + F.fprintf frm "@,%a" id a; f () in - let iter map frm l = List.iter (map frm) l in - let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in - B.contents f c + B.rev_iter C.start pp_entry c let specs = { L.pp_term = pp_term; L.pp_context = pp_context @@ -189,12 +188,11 @@ let specs = { (* term xml printing ********************************************************) let id frm a = - let f = function - | None -> () - | Some (true, s) -> F.fprintf frm " name=%S" s - | Some (false, n) -> F.fprintf frm " name=%S" ("^" ^ n) + let f s = function + | true -> F.fprintf frm " name=%S" s + | false -> F.fprintf frm " name=%S" ("^" ^ s) in - B.name f a + B.name C.start f a let rec exp_term frm = function | B.Sort (a, l) -> diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 3b4820abf..4a1667862 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -16,13 +16,13 @@ module P = Output module B = Brg module O = BrgOutput module E = BrgEnvironment -module S = BrgSubstitution exception TypeError of B.message type machine = { c: B.context; - s: (B.term * int) list + s: (B.context * B.term) list; + i: int } (* Internal functions *******************************************************) @@ -51,30 +51,16 @@ let error3 c t1 t2 t3 = in raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3)) -let empty_machine c = { - c = c; s = [] -} +let err () = assert false let get f m i = - let f e = function - | Some (_, b) -> f e b - | None -> error0 i - in - 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 push f m a b = - assert (m.s = []); - f {m with c = (a, b) :: m.c} + B.get error0 f m.c i (* to share *) let rec step f ?(delta=false) ?(rt=false) m x = (* L.warn "entering R.step"; *) match x with - | B.Sort _ -> f m x + | B.Sort _ -> f m None x | B.GRef (a, uri) -> let f = function | _, _, B.Abbr v when delta -> @@ -84,68 +70,69 @@ let rec step f ?(delta=false) ?(rt=false) m x = P.add ~grt:1 (); step f ~delta ~rt m w | e, _, b -> - f m (B.GRef (B.Entry (e, b) :: a, uri)) + f m (Some (e, b)) x in E.get_obj f uri | B.LRef (a, i) -> - let f e = function + let f c a = function | B.Abbr v -> P.add ~ldelta:1 (); - step f ~delta ~rt m v + step f ~delta ~rt {m with c = c} v | B.Abst w when rt -> P.add ~lrt:1 (); - step f ~delta ~rt m w + step f ~delta ~rt {m with c = c} w + | B.Void -> + f {m with c = c} None x | b -> - f m (B.LRef (B.Entry (e, b) :: a, i)) - in - let f e = S.lift_bind (f e) (succ i) (0) in + let f e = f {m with c = c} (Some (e, b)) x in + B.apix err f a + in get f m i | B.Cast (_, _, t) -> P.add ~tau:1 (); step f ~delta ~rt m t | B.Appl (_, v, t) -> - step f ~delta ~rt {m with s = (v, 0) :: m.s} t - | B.Bind (a, B.Abst w, t) -> + step f ~delta ~rt {m with s = (m.c, v) :: 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 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 + | [] -> f m None x + | (c, v) :: s -> + P.add ~beta:1 ~upsilon:(List.length s) (); + let f c = step f ~delta ~rt {m with c = c; s = s} t in + B.push f m.c ~c a (B.Abbr v) (* (B.Cast ([], w, v)) *) end - | B.Bind (a, b, t) -> + | B.Bind (a, b, t) -> P.add ~upsilon:(List.length m.s) (); - 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 f c = step f ~delta ~rt {m with c = c} t in + B.push f m.c ~c:m.c a b let domain f m t = let f r = L.unbox level; f r in - let f m = function + let f m _ = function | B.Bind (_, B.Abst w, _) -> f m w | _ -> error1 "not a function" m.c t in L.box level; log1 "Now scanning" m.c t; step f ~delta:true ~rt:true m t -let rec ac_nfs f ~si r m1 u m2 t = +let push f m a b = + assert (m.s = []); + let a, i = match b with + | B.Abst _ -> B.Apix m.i :: a, succ m.i + | _ -> a, m.i + in + let f c = f {m with c = c; i = i} in + B.push f m.c ~c:m.c a b + +let rec ac_nfs f ~si r m1 a1 u m2 a2 t = log2 "Now converting nfs" m1.c u m2.c t; - match u, t with - | B.Sort (_, h1), B.Sort (_, h2) -> + match a1, u, a2, 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 m1 m2 else f false - | B.GRef (B.Entry (e1, B.Abst _) :: _, _), - B.GRef (B.Entry (e2, B.Abst _) :: _, _) -> + | Some (e1, B.Abst _), _, Some (e2, B.Abst _), _ -> 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) :: _, _) -> + | Some (e1, B.Abbr v1), _, Some (e2, B.Abbr v2), _ -> if e1 = e2 then let f r = if r then f r @@ -157,63 +144,68 @@ let rec ac_nfs f ~si r m1 u m2 t = ac_stacks f ~si r m1 m2 else if e1 < e2 then begin P.add ~gdelta:1 (); - step (ac_nfs f ~si r m1 u) m2 v2 + step (ac_nfs f ~si r m1 a1 u) m2 v2 end else begin P.add ~gdelta:1 (); - step (ac_nfs_rev f ~si r m2 t) m1 v1 + step (ac_nfs_rev f ~si r m2 a2 t) m1 v1 end - | _, B.GRef (B.Entry (_, B.Abbr v2) :: _, _) -> + | _, _, Some (_, B.Abbr v2), _ -> P.add ~gdelta:1 (); - step (ac_nfs f ~si r m1 u) m2 v2 - | B.GRef (B.Entry (_, B.Abbr v1) :: _, _), _ -> + step (ac_nfs f ~si r m1 a1 u) m2 v2 + | Some (_, B.Abbr v1), _, _, _ -> P.add ~gdelta:1 (); - 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) -> + step (ac_nfs_rev f ~si r m2 a2 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 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 m1 w1 m2 w2 - | B.Sort _, B.Bind (a, b, t) when si -> + | _, B.Sort _, _, B.Bind (a, b, t) when si -> P.add ~si:1 (); 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 + | _ -> f false -and ac_nfs_rev f ~si r m2 t m1 u = ac_nfs f ~si r m1 u m2 t +and ac_nfs_rev f ~si r m2 a2 t m1 a1 u = ac_nfs f ~si r m1 a1 u m2 a2 t 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 m1 t1) m2 t2 in + let g m1 a1 t1 = step (ac_nfs f ~si r m1 a1 t1) m2 t2 in if r = false then f false else step g m1 t1 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 mm1 v1 mm2) h2 (0) v2 in - S.lift f h1 (0) v1 + if List.length m1.s <> List.length m2.s then f false else + let map f r (c1, v1) (c2, v2) = + let m1, m2 = {m1 with c = c1; s = []}, {m2 with c = c2; s = []} in + ac f ~si r m1 v1 m2 v2 in - if List.length m1.s <> List.length m2.s then - begin -(* L.warn (Printf.sprintf "Different lengths: %u %u" - (List.length m1.s) (List.length m2.s) - ); *) - f false - end - else - C.list_fold_left2 f map r m1.s m2.s + C.list_fold_left2 f map r m1.s m2.s + +(* Interface functions ******************************************************) -let assert_conversion f ?(si=false) ?(rt=false) c u w v = +let empty_machine = { + c = B.empty_context; s = []; i = 0 +} + +let get f m i = + assert (m.s = []); + let f c = f in + get f m i + +let assert_conversion f ?(si=false) ?(rt=false) mw u w v = let f b = L.unbox level; f b in - let mw = empty_machine c in let f mu u = let f = function | true -> f () - | false -> error3 c v w u + | false -> error3 mw.c v w u in - L.box level; log2 "Now converting" c u c w; + L.box level; log2 "Now converting" mu.c u mw.c w; ac f ~si true mu u mw w in if rt then domain f mw u else f mw u + +let message1 st m t = + L.ct_items1 "In the context" m.c st t diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index e5c670dd4..bf7c7f5d0 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -11,7 +11,18 @@ exception TypeError of Brg.message +type machine + +val empty_machine: machine + +val get: (Brg.attrs -> Brg.bind -> 'a) -> machine -> int -> 'a + +val push: (machine -> 'a) -> machine -> Brg.attrs -> Brg.bind -> '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 + machine -> Brg.term -> Brg.term -> Brg.term -> 'a + +val message1: + string -> machine -> Brg.term -> (Brg.context, Brg.term) Log.message diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index cc9245f92..bf0678647 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -24,82 +24,79 @@ module R = BrgReduction let level = 4 -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 log1 s m t = + let s = s ^ " the term" in + L.log O.specs level (R.message1 s m t) -let error1 st c t = - let sc = "In the context" in - raise (R.TypeError (L.ct_items1 sc c st t)) +let error1 s m t = + raise (R.TypeError (R.message1 s m t)) (* Interface functions ******************************************************) -let rec b_type_of f ~si g c x = - log1 "Now checking" c x; +let rec b_type_of f ~si g m x = + log1 "Now checking" m x; match x with | B.Sort (a, h) -> let f h = f x (B.Sort (a, h)) in H.apply f g h | B.LRef (_, i) -> let f _ = function - | Some (_, B.Abst w) -> + | B.Abst w -> S.lift (f x) (succ i) (0) w - | Some (_, B.Abbr (B.Cast (_, w, _))) -> + | B.Abbr (B.Cast (_, w, _)) -> S.lift (f x) (succ i) (0) w - | Some (_, B.Abbr _) -> assert false - | Some (_, B.Void) -> - error1 "reference to excluded variable" c x - | None -> - error1 "variable not found" c x + | B.Abbr _ -> assert false + | B.Void -> + error1 "reference to excluded variable" m x in - B.get f c i + R.get f m i | B.GRef (_, uri) -> let f = function | _, _, B.Abst w -> f x w | _, _, B.Abbr (B.Cast (_, w, _)) -> f x w | _, _, B.Abbr _ -> assert false | _, _, B.Void -> - error1 "reference to excluded object" c x + error1 "reference to excluded object" m x in E.get_obj f uri | B.Bind (a, B.Abbr v, t) -> 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) ~si g cc t in - let f xv = B.push (f xv) c a (B.Abbr xv) in + let f xv m = b_type_of (f xv) ~si g m t in + let f xv = R.push (f xv) m a (B.Abbr xv) in let f xv vv = match xv with | B.Cast _ -> f xv - | _ -> assert false (* f (B.Cast ([], vv, xv)) *) + | _ -> f (B.Cast ([], vv, xv)) in - type_of f ~si g c v + type_of f ~si g m 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) ~si g cc t in - let f xu _ = B.push (f xu) c a (B.Abst xu) in - type_of f ~si g c u + let f xu m = b_type_of (f xu) ~si g m t in + let f xu _ = R.push (f xu) m a (B.Abst xu) in + type_of f ~si g m 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 ~si g cc t in - B.push f c a B.Void + let f m = b_type_of f ~si g m t in + R.push f m a B.Void | B.Appl (a, v, t) -> 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 + R.assert_conversion f ~si ~rt:true m tt vv xv in - let f xv vv = b_type_of (f xv vv) ~si g c t in - type_of f ~si g c v + let f xv vv = b_type_of (f xv vv) ~si g m t in + type_of f ~si g m v | B.Cast (a, u, t) -> 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 + R.assert_conversion f ~si m xu tt xt in - let f xu _ = b_type_of (f xu) ~si g c t in - type_of f ~si g c u + let f xu _ = b_type_of (f xu) ~si g m t in + type_of f ~si g m u -and type_of f ?(si=false) g c x = +and type_of f ?(si=false) g m x = let f t u = L.unbox level; f t u in - L.box level; b_type_of f ~si g c x + L.box level; b_type_of f ~si g m x diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index 99aef9506..215132378 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -11,4 +11,4 @@ val type_of: (Brg.term -> Brg.term -> 'a) -> ?si:bool -> - Hierarchy.graph -> Brg.context -> Brg.term -> 'a + Hierarchy.graph -> BrgReduction.machine -> Brg.term -> 'a diff --git a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml index 65735066a..f9c23d73f 100644 --- a/helm/software/lambda-delta/basic_rg/brgUntrusted.ml +++ b/helm/software/lambda-delta/basic_rg/brgUntrusted.ml @@ -12,6 +12,7 @@ module L = Log module B = Brg module E = BrgEnvironment +module R = BrgReduction module T = BrgType (* Interface functions ******************************************************) @@ -22,11 +23,11 @@ let type_check f ?(si=false) g = function | 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 ~si g B.empty_context t + L.loc := e; T.type_of f ~si g R.empty_machine 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 ~si g B.empty_context t + L.loc := e; T.type_of f ~si g R.empty_machine 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/lib/log.ml b/helm/software/lambda-delta/lib/log.ml index e28ea326a..39cc5837a 100644 --- a/helm/software/lambda-delta/lib/log.ml +++ b/helm/software/lambda-delta/lib/log.ml @@ -19,6 +19,8 @@ type ('a, 'b) item = Term of 'a * 'b | String of string | Loc +type ('a, 'b) message = ('a, 'b) item list + type ('a, 'b) specs = { pp_term : 'a -> F.formatter -> 'b -> unit; pp_context: F.formatter -> 'a -> unit diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index 6a2cc90cd..b5bc99adf 100644 --- a/helm/software/lambda-delta/lib/log.mli +++ b/helm/software/lambda-delta/lib/log.mli @@ -15,6 +15,8 @@ type ('a, 'b) item = Term of 'a * 'b | String of string | Loc +type ('a, 'b) message = ('a, 'b) item list + type ('a, 'b) specs = { pp_term : 'a -> Format.formatter -> 'b -> unit; pp_context: Format.formatter -> 'a -> unit @@ -36,21 +38,21 @@ val box_err: unit -> unit val flush_err: unit -> unit -val log: ('a, 'b) specs -> int -> ('a, 'b) item list -> unit +val log: ('a, 'b) specs -> int -> ('a, 'b) message -> unit -val error: ('a, 'b) specs -> ('a, 'b) item list -> unit +val error: ('a, 'b) specs -> ('a, 'b) message -> unit -val items1: string -> ('a, 'b) item list +val items1: string -> ('a, 'b) message -val t_items1: string -> 'a -> 'b -> ('a, 'b) item list +val t_items1: string -> 'a -> 'b -> ('a, 'b) message val ct_items1: - string -> 'a -> string -> 'b -> ('a, 'b) item list + string -> 'a -> string -> 'b -> ('a, 'b) message val ct_items2: string -> 'a -> string -> 'b -> string -> 'a -> string -> 'b -> - ('a, 'b) item list + ('a, 'b) message val ct_items3: string -> 'a -> string -> 'b -> string -> 'b -> string -> 'b -> - ('a, 'b) item list + ('a, 'b) message diff --git a/helm/software/lambda-delta/toplevel/metaBrg.ml b/helm/software/lambda-delta/toplevel/metaBrg.ml index b82e51a3e..9fe774b81 100644 --- a/helm/software/lambda-delta/toplevel/metaBrg.ml +++ b/helm/software/lambda-delta/toplevel/metaBrg.ml @@ -47,8 +47,8 @@ let xlate_pars f pars = C.list_fold_right f map pars B.empty_context let unwind_to_xlate_term f c t = - let map f t (a, b) = f (B.bind a b t) in - let f t = C.list_fold_left f map t c in + let map f t a b = f (B.bind a b t) in + let f t = B.fold_left f map t c in xlate_term c f t let xlate_entry f = function