From: Ferruccio Guidi Date: Wed, 1 Jul 2015 19:00:12 +0000 (+0000) Subject: - simpler attribute system X-Git-Tag: make_still_working~713 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fec20705af4705f8eb9542aece87769b82a6a6b4;p=helm.git - simpler attribute system - some renaming --- diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index a07afc02e..ea95cf09b 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -223,10 +223,12 @@ src/basic_ag/bagOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ src/common/entity.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi : src/basic_ag/bag.cmx -src/basic_ag/bagEnvironment.cmo : src/lib/log.cmi src/common/entity.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagEnvironment.cmx : src/lib/log.cmx src/common/entity.cmx \ - src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi +src/basic_ag/bagEnvironment.cmo : src/common/options.cmx src/lib/log.cmi \ + src/common/entity.cmx src/basic_ag/bag.cmx \ + src/basic_ag/bagEnvironment.cmi +src/basic_ag/bagEnvironment.cmx : src/common/options.cmx src/lib/log.cmx \ + src/common/entity.cmx src/basic_ag/bag.cmx \ + src/basic_ag/bagEnvironment.cmi src/basic_ag/bagSubstitution.cmi : src/lib/marks.cmi src/basic_ag/bag.cmx src/basic_ag/bagSubstitution.cmo : src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmi diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 637aa4a89..7a6600898 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -46,19 +46,19 @@ let alpha id = let attrs_for_abst id aw = let id = if !G.alpha <> "" then alpha id else id in - let main = E.succ aw.E.n_main in - E.node_attrs ~name:(id, true) ~side:aw.E.n_main ~main () + let main = E.succ aw.E.b_main in + E.bind_attrs ~name:(id, true) ~side:aw.E.b_main ~main () let attrs_for_decl aw = - let main = E.succ aw.E.n_main in - E.node_attrs ~side:aw.E.n_main ~main () + let main = E.succ aw.E.b_main in + E.bind_attrs ~side:aw.E.b_main ~main () let add_abst cnt id aw w = - let a = attrs_for_abst id aw in + let y = attrs_for_abst id aw in let l = if !G.infinity then N.infinity else N.two in - D.EBind (cnt, a, D.Abst (false, l, w)) + D.EBind (cnt, E.empty_node, y, D.Abst (false, l, w)) -let mk_lref f a i = f a (D.TLRef (a, i)) +let mk_lref f _ y i = f y (D.TLRef (E.empty_node, i)) let id_of_name (id, _, _) = if !G.alpha <> "" then alpha id else id @@ -92,7 +92,7 @@ let relax_opt_qid f lst = function | Some qid -> let f qid = f (Some qid) in relax_qid f lst qid let resolve_gref err f lst qid = - try let a, cnt = UH.find henv (uri_of_qid qid) in f qid a cnt + try let y, cnt = UH.find henv (uri_of_qid qid) in f qid y cnt with Not_found -> err qid let resolve_gref_relaxed f lst qid = @@ -111,40 +111,35 @@ let get_cnt_relaxed f lst = let rec err node = relax_opt_qid (get_cnt err f lst) lst node in get_cnt err f lst lst.node -let push_abst f a w lenv = +let push_abst f y w lenv = let bw = D.Abst (false, N.infinity, w) in - D.push_bind f a bw lenv - -let add_proj at e t = match e with - | D.ESort -> t - | D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t) - | _ -> -IFDEF MANAGER OR OBJS THEN - D.TProj (at, D.set_attrs C.start at e, t) -ELSE - D.TProj (at, e, t) -END + D.push_bind f E.empty_node y bw lenv + +let add_proj yt e t = match e with + | D.ESort -> t + | D.EBind (D.ESort, _, y, b) -> D.TBind (E.compose y yt, b, t) + | _ -> + D.TProj (D.set_attrs C.start yt e, t) (* this is not tail recursive in the GRef branch *) -let rec xlate_term f st lst y lenv = function +let rec xlate_term f st lst z lenv = function | A.Sort s -> - let h = if s then 0 else 1 in - let a = E.node_attrs ~main:(h, 0) () in - f a (D.TSort (a, h)) + let k = if s then 0 else 1 in + let y = E.bind_attrs ~main:(k, 0) () in + f y (D.TSort k) | A.Appl (v, t) -> - let f av vv at tt = - let at = E.compose av at in - f at (D.TAppl (at, !G.extended, vv, tt)) + let f vv yt tt = + f yt (D.TAppl (!G.extended, vv, tt)) in - let f av vv = xlate_term (f av vv) st lst y lenv t in + let f _ vv = xlate_term (f vv) st lst z lenv t in xlate_term f st lst false lenv v | A.Abst (name, w, t) -> - let f aw ww = - let aw = attrs_for_abst name aw in - let f at tt = - let at = E.compose aw at in + let f yw ww = + let yw = attrs_for_abst name yw in + let f yt tt = + let yt = E.compose yw yt in let l = - if !G.cc then match y, snd at.E.n_main with + if !G.cc then match z, snd yt.E.b_main with | true, _ -> N.one | _ , 0 -> N.one | _ , 1 -> N.unknown st @@ -153,31 +148,24 @@ let rec xlate_term f st lst y lenv = function else N.infinity in let b = D.Abst (false, l, ww) in - f at (D.TBind (at, b, tt)) + f yt (D.TBind (yt, b, tt)) in - let f lenv = xlate_term f st lst y lenv t in - push_abst f aw ww lenv + let f lenv = xlate_term f st lst z lenv t in + push_abst f yw ww lenv in xlate_term f st lst true lenv w | A.GRef (name, args) -> let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in let map2 f arg args = - let f av v = f (D.EAppl (args, E.shift av, !G.extended, v)) in + let f _ v = f (D.EAppl (args, !G.extended, v)) in xlate_term f st lst false lenv arg in - let g qid a cnt = - let gref = D.TGRef (a, uri_of_qid qid) in - if cnt = D.ESort then f a gref else + let g qid y cnt = + let gref = D.TGRef (E.empty_node, uri_of_qid qid) in + if cnt = D.ESort then f y gref else let f = function - | D.EAppl (D.ESort, av, x, v) -> - let a = E.compose av a in - f a (D.TAppl (a, x, v, gref)) - | args -> -IFDEF MANAGER OR OBJS THEN - f a (D.TProj (a, D.set_attrs C.start a args, gref)) -ELSE - f a (D.TProj (a, args, gref)) -END + | D.EAppl (D.ESort, x, v) -> f y (D.TAppl (x, v, gref)) + | args -> f y (D.TProj (args, gref)) in let f args = C.list_fold_right f map2 args D.ESort in D.sub_list_strict (D.fold_names f map1 args) cnt args @@ -215,14 +203,14 @@ let xlate_entity err f st lst = function | A.Decl (name, w) -> let f lenv = let f qid = - let f aw ww = - let a = attrs_for_decl aw in - UH.add henv (uri_of_qid qid) (a, lenv); - let t = add_proj aw lenv ww in + let f yw ww = + let y = attrs_for_decl yw in + UH.add henv (uri_of_qid qid) (y, lenv); + let t = add_proj yw lenv ww in (* print_newline (); CrgOutput.pp_term print_string t; *) - let na = {aw with E.n_apix = lst.line} in + let na = E.node_attrs ~apix:lst.line () in let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in G.set_current_trace lst.line; f {lst with line = succ lst.line} entity @@ -237,13 +225,13 @@ let xlate_entity err f st lst = function let f lenv = let f qid = let f _ ww = - let f av vv = - UH.add henv (uri_of_qid qid) (av, lenv); - let t = add_proj av lenv (D.TCast (av, ww, vv)) in + let f yv vv = + UH.add henv (uri_of_qid qid) (yv, lenv); + let t = add_proj yv lenv (D.TCast (ww, vv)) in (* print_newline (); CrgOutput.pp_term print_string t; *) - let na = {av with E.n_apix = lst.line} in + let na = E.node_attrs ~apix:lst.line () in let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in let entity = ra, na, uri_of_qid qid, E.Abbr t in G.set_current_trace lst.line; diff --git a/helm/software/helena/src/basic_ag/bag.ml b/helm/software/helena/src/basic_ag/bag.ml index c0e540963..51c644148 100644 --- a/helm/software/helena/src/basic_ag/bag.ml +++ b/helm/software/helena/src/basic_ag/bag.ml @@ -16,22 +16,22 @@ module P = Marks module E = Entity type uri = E.uri -type attrs = E.node_attrs +type b_attrs = E.bind_attrs type bind = Void (* exclusion *) | Abst of term (* abstraction *) | Abbr of term (* abbreviation *) -and term = Sort of int (* hierarchy index *) - | LRef of P.mark (* location *) - | GRef of uri (* reference *) - | Cast of term * term (* domain, element *) - | Appl of term * term (* argument, function *) - | Bind of attrs * P.mark * bind * term (* name, location, binder, scope *) +and term = Sort of int (* hierarchy index *) + | LRef of P.mark (* location *) + | GRef of uri (* reference *) + | Cast of term * term (* domain, element *) + | Appl of term * term (* argument, function *) + | Bind of b_attrs * P.mark * bind * term (* name, location, binder, scope *) type entity = term E.entity (* attrs, uri, binder *) -type lenv = (attrs * P.mark * bind) list (* name, location, binder *) +type lenv = (b_attrs * P.mark * bind) list (* name, location, binder *) type message = (lenv, term) Log.item list @@ -47,24 +47,24 @@ let cast u t = Cast (u, t) let appl u t = Appl (u, t) -let bind a l b t = Bind (a, l, b, t) +let bind y l b t = Bind (y, l, b, t) -let bind_abst a l u t = Bind (a, l, Abst u, t) +let bind_abst y l u t = Bind (y, l, Abst u, t) -let bind_abbr a l v t = Bind (a, l, Abbr v, t) +let bind_abbr y l v t = Bind (y, l, Abbr v, t) (* local environment handling functions *************************************) let empty_lenv = [] -let push msg f es a l b = +let push msg f es y l b = let rec does_not_occur loc = function | [] -> true | (_, l, _) :: _ when l = loc -> false | _ :: es -> does_not_occur l es in if not (does_not_occur l es) then failwith msg else - let c = (a, l, b) :: es in f c + let c = (y, l, b) :: es in f c let append f es1 es2 = f (List.append es2 es1) @@ -77,7 +77,7 @@ let contents f es = f es let get err f es i = let rec aux = function | [] -> err () - | (a, l, b) :: tl -> if l = i then f a b else aux tl + | (y, l, b) :: tl -> if l = i then f y b else aux tl in aux es diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index cb21d0247..e9ad2417e 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -19,61 +19,61 @@ module Z = Bag (* internal functions: crg to bag term **************************************) let rec xlate_term st f c = function - | D.TSort (_, h) -> f (Z.Sort h) - | D.TGRef (_, s) -> f (Z.GRef s) - | D.TLRef (a, i) -> + | D.TSort k -> f (Z.Sort k) + | D.TGRef (_, s) -> f (Z.GRef s) + | D.TLRef (_, i) -> let _, l, _ = List.nth c i in f (Z.LRef l) - | D.TCast (_, u, t) -> + | D.TCast (u, t) -> let f tt uu = f (Z.Cast (uu, tt)) in let f tt = xlate_term st (f tt) c u in xlate_term st f c t - | D.TAppl (_, _, v, t) -> + | D.TAppl (_, v, t) -> let f tt vv = f (Z.Appl (vv, tt)) in let f tt = xlate_term st (f tt) c v in xlate_term st f c t - | D.TProj (_, e, t) -> + | D.TProj (e, t) -> D.shift (xlate_term st f c) e t (* this case should be removed by improving alpha-conversion *) - | D.TBind (ab, D.Abst (x, n, ws), D.TCast (ac, u, t)) -> - xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (x, N.minus st n 1, ws), u), D.TBind (ab, D.Abst (x, n, ws), t))) - | D.TBind (a, b, t) -> + | D.TBind (y, D.Abst (x, n, ws), D.TCast (u, t)) -> + xlate_term st f c (D.TCast (D.TBind (y, D.Abst (x, N.minus st n 1, ws), u), D.TBind (y, D.Abst (x, n, ws), t))) + | D.TBind (y, b, t) -> let f cc = let a, l, b = List.hd cc in let f tt = f (Z.Bind (a, l, b, tt)) in xlate_term st f cc t in - xlate_bind st f c a b + xlate_bind st f c y b -and xlate_bind st f c a = function +and xlate_bind st f c y = function | D.Abst (_, _, w) -> - let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in + let f ww = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abst ww) in xlate_term st f c w | D.Abbr v -> - let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in + let f vv = Z.push "xlate_bind" f c y (P.new_mark ()) (Z.Abbr vv) in xlate_term st f c v | D.Void -> - Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void + Z.push "xlate_bind" f c y (P.new_mark ()) Z.Void (* internal functions: bag to crg term **************************************) let rec xlate_bk_term f c = function - | Z.Sort h -> f (D.TSort (E.empty_node, h)) + | Z.Sort k -> f (D.TSort k) | Z.GRef s -> f (D.TGRef (E.empty_node, s)) | Z.LRef l -> let f i = f (D.TLRef (E.empty_node, i)) in Z.nth C.err f l c | Z.Cast (u, t) -> - let f tt uu = f (D.TCast (E.empty_node, uu, tt)) in + let f tt uu = f (D.TCast (uu, tt)) in let f tt = xlate_bk_term (f tt) c u in xlate_bk_term f c t | Z.Appl (u, t) -> - let f tt uu = f (D.TAppl (E.empty_node, true, uu, tt)) in + let f tt uu = f (D.TAppl (true, uu, tt)) in let f tt = xlate_bk_term (f tt) c u in xlate_bk_term f c t - | Z.Bind (a, l, b, t) -> - let f tt bb = f (D.TBind (a, bb, tt)) in + | Z.Bind (y, l, b, t) -> + let f tt bb = f (D.TBind (y, bb, tt)) in let f tt = xlate_bk_bind (f tt) c b in - let cc = Z.push "xlate_bk_term" C.start c a l b in + let cc = Z.push "xlate_bk_term" C.start c y l b in xlate_bk_term f cc t and xlate_bk_bind f c = function diff --git a/helm/software/helena/src/basic_ag/bagEnvironment.ml b/helm/software/helena/src/basic_ag/bagEnvironment.ml index 61e823836..3f2b5534d 100644 --- a/helm/software/helena/src/basic_ag/bagEnvironment.ml +++ b/helm/software/helena/src/basic_ag/bagEnvironment.ml @@ -12,28 +12,30 @@ module U = NUri module UH = U.UriHash module L = Log +module G = Options module E = Entity module Z = Bag exception ObjectNotFound of Z.message -let hsize = 7000 +let hsize = 7000 let env = UH.create hsize (* Internal functions *******************************************************) -let get_age = - let age = ref 0 in - fun () -> incr age; !age - let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) (* Interface functions ******************************************************) -let set_entity f (ra, na, uri, b) = - let age = get_age () in - let entry = ra, {na with E.n_apix = age}, uri, b in - UH.add env uri entry; f entry +let set_entity f entity = +IFDEF EXPAND THEN + let ra, na, uri, b = entity in + let entity0 = if !G.expand then ra, E.node_attrs ~apix:0 (), uri, b else entity in + UH.add env uri entity0; f entity +ELSE + let _, _, uri, _ = entity in + UH.add env uri entity; f entity +END let get_entity f uri = try f (UH.find env uri) with Not_found -> error uri diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml index 4867c7180..41914b062 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.ml +++ b/helm/software/helena/src/basic_ag/bagOutput.ml @@ -124,28 +124,28 @@ let rec pp_term st c och = function KP.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t | Z.Appl (v, t) -> KP.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t - | Z.Bind (a, l, Z.Abst w, t) -> + | Z.Bind (y, l, Z.Abst w, t) -> let f cc = - KP.fprintf och "[%t:%a].%a" (res a l) (pp_term st c) w (pp_term st cc) t + KP.fprintf och "[%t:%a].%a" (res y l) (pp_term st c) w (pp_term st cc) t in - Z.push "output abst" f c a l (Z.Abst w) - | Z.Bind (a, l, Z.Abbr v, t) -> + Z.push "output abst" f c y l (Z.Abst w) + | Z.Bind (y, l, Z.Abbr v, t) -> let f cc = - KP.fprintf och "[%t=%a].%a" (res a l) (pp_term st c) v (pp_term st cc) t + KP.fprintf och "[%t=%a].%a" (res y l) (pp_term st c) v (pp_term st cc) t in - Z.push "output abbr" f c a l (Z.Abbr v) - | Z.Bind (a, l, Z.Void, t) -> - let f cc = KP.fprintf och "[%t].%a" (res a l) (pp_term st cc) t in - Z.push "output void" f c a l Z.Void + Z.push "output abbr" f c y l (Z.Abbr v) + | Z.Bind (y, l, Z.Void, t) -> + let f cc = KP.fprintf och "[%t].%a" (res y l) (pp_term st cc) t in + Z.push "output void" f c y l Z.Void let pp_lenv st och c = let pp_entry och = function - | a, l, Z.Abst w -> - KP.fprintf och "%t : %a\n" (res a l) (pp_term st c) w - | a, l, Z.Abbr v -> - KP.fprintf och "%t = %a\n" (res a l) (pp_term st c) v - | a, l, Z.Void -> - KP.fprintf och "%t\n" (res a l) + | y, l, Z.Abst w -> + KP.fprintf och "%t : %a\n" (res y l) (pp_term st c) w + | y, l, Z.Abbr v -> + KP.fprintf och "%t = %a\n" (res y l) (pp_term st c) v + | y, l, Z.Void -> + KP.fprintf och "%t\n" (res y l) in let iter map och l = List.iter (map och) l in let f es = KP.fprintf och "%a" (iter pp_entry) (List.rev es) in diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index cc3cb36f8..a0e4fa739 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -30,7 +30,7 @@ type whd_result = | Sort_ of int | LRef_ of P.mark * Z.term option | GRef_ of Z.entity - | Bind_ of Z.attrs * P.mark * Z.term * Z.term + | Bind_ of Z.b_attrs * P.mark * Z.term * Z.term type ho_whd_result = | Sort of int @@ -59,7 +59,7 @@ let empty_machine = {i = 0; c = Z.empty_lenv; s = []} let inc m = {m with i = succ m.i} let unwind_to_term f m t = - let map f t (a, l, b) = f (Z.Bind (a, l, b, t)) in + let map f t (y, l, b) = f (Z.Bind (y, l, b, t)) in let f mc = C.list_fold_left f map t mc in Z.contents f m.c @@ -94,18 +94,18 @@ let rec whd f c m x = get f c m i | Z.Cast (_, t) -> whd f c m t | Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t - | Z.Bind (a, l, Z.Abst w, t) -> + | Z.Bind (y, l, Z.Abst w, t) -> begin match m.s with - | [] -> f m (Bind_ (a, l, w, t)) + | [] -> f m (Bind_ (y, l, w, t)) | v :: tl -> let nl = P.new_mark () in let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in - Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v))) + Z.push "!" f m.c y nl (Z.Abbr (Z.Cast (w, v))) end - | Z.Bind (a, l, b, t) -> + | Z.Bind (y, l, b, t) -> let nl = P.new_mark () in let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in - Z.push "!" f m.c a nl b + Z.push "!" f m.c y nl b (* Interface functions ******************************************************) @@ -134,15 +134,15 @@ let rec are_convertible f st a c m1 t1 m2 t2 = let u, t = term_of_whdr r1, term_of_whdr r2 in if !G.ct >= level then log2 st "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, _) -> + | Sort_ k1, Sort_ k2 -> + if k1 = k2 then f a else f false + | LRef_ (i1, _), LRef_ (i2, _) -> if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false | GRef_ (_, {E.n_apix = a1}, _, E.Abst _), - GRef_ (_, {E.n_apix = a2}, _, E.Abst _) -> + GRef_ (_, {E.n_apix = a2}, _, E.Abst _) -> if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1), - GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) -> + GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) -> if a1 = a2 then let f a = if a then f a else are_convertible f st true c m1 v1 m2 v2 @@ -151,25 +151,25 @@ let rec are_convertible f st a c m1 t1 m2 t2 = else if a1 < a2 then whd (aux m1 r1) c m2 v2 else whd (aux_rev m2 r2) c m1 v1 - | _, GRef_ (_, _, _, E.Abbr v2) -> + | _, GRef_ (_, _, _, E.Abbr v2) -> whd (aux m1 r1) c m2 v2 - | GRef_ (_, _, _, E.Abbr v1), _ -> + | GRef_ (_, _, _, E.Abbr v1), _ -> whd (aux_rev m2 r2) c m1 v1 - | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) -> + | Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) -> let l = P.new_mark () in let h c = let m1, m2 = inc m1, inc m2 in let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in ZS.subst f l l1 t1 in - let f r = if r then push "!" h c m1 a1 l w1 else f false in + let f r = if r then push "!" h c m1 y1 l w1 else f false in are_convertible f st a c m1 w1 m2 w2 (* we detect the AUT-QE reduction rule for type/prop inclusion *) - | Sort_ _, Bind_ (a2, l2, w2, t2) when !G.si -> + | Sort_ _, Bind_ (y2, l2, w2, t2) when !G.si -> let m1, m2 = inc m1, inc m2 in let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in - push "nsi" f c m2 a2 l2 w2 - | _ -> f false + push "nsi" f c m2 y2 l2 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 diff --git a/helm/software/helena/src/basic_ag/bagSubstitution.ml b/helm/software/helena/src/basic_ag/bagSubstitution.ml index 5585b5d6a..f35cdf4ff 100644 --- a/helm/software/helena/src/basic_ag/bagSubstitution.ml +++ b/helm/software/helena/src/basic_ag/bagSubstitution.ml @@ -36,8 +36,8 @@ and lref_map f map t = match t with let f w' u' = f (S.sh2 w w' u u' t Z.appl) in let f w' = lref_map (f w') map u in lref_map f map w - | Z.Bind (a, l, b, u) -> - let f b' u' = f (S.sh2 b b' u u' t (Z.bind a l)) in + | Z.Bind (y, l, b, u) -> + let f b' u' = f (S.sh2 b b' u u' t (Z.bind y l)) in let f b' = lref_map (f b') map u in lref_map_bind f map b diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index 009a2eaf9..1f47b60dd 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -66,33 +66,33 @@ let rec b_type_of err f st c x = | _, _, _, E.Void -> assert false in ZE.get_entity f uri - | Z.Bind (a, l, Z.Abbr v, t) -> + | Z.Bind (y, l, Z.Abbr v, t) -> let f xv xt tt = - f (S.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt) + f (S.sh2 v xv t xt x (Z.bind_abbr y l)) (Z.bind_abbr y l xv tt) in let f xv cc = b_type_of err (f xv) st cc t in - let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in + let f xv = Z.push "type abbr" (f xv) c y l (Z.Abbr xv) in let f xv vv = match xv with | Z.Cast _ -> f xv | _ -> f (Z.Cast (vv, xv)) in type_of err f st c v - | Z.Bind (a, l, Z.Abst u, t) -> + | Z.Bind (y, l, Z.Abst u, t) -> let f xu xt tt = - f (S.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt) + f (S.sh2 u xu t xt x (Z.bind_abst y l)) (Z.bind_abst y l xu tt) in let f xu cc = b_type_of err (f xu) st cc t in - let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in + let f xu _ = Z.push "type abst" (f xu) c y l (Z.Abst xu) in type_of err f st c u - | Z.Bind (a, l, Z.Void, t) -> + | Z.Bind (y, l, Z.Void, t) -> let f xt tt = - f (S.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt) + f (S.sh1 t xt x (Z.bind y l Z.Void)) (Z.bind y l Z.Void tt) in let f cc = b_type_of err f st cc t in - Z.push "type void" f c a l Z.Void + Z.push "type void" f c y l Z.Void | Z.Appl (v, t) -> let f xv vv xt tt = function - | ZR.Abst w -> + | ZR.Abst w -> if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w); let f a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) @@ -100,7 +100,7 @@ let rec b_type_of err f st c x = else error3 err c xv vv w in ZR.are_convertible f st c w vv - | _ -> + | _ -> error1 err "not a function" c xt in let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) st c tt in diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml index a39010f80..e6ac94e5b 100644 --- a/helm/software/helena/src/basic_rg/brg.ml +++ b/helm/software/helena/src/basic_rg/brg.ml @@ -16,25 +16,26 @@ module N = Layer module E = Entity type uri = E.uri -type attrs = E.node_attrs +type n_attrs = E.node_attrs +type b_attrs = E.bind_attrs (* x-reduced abstractions are output by RTM only *) type bind = Void (* *) | Abst of bool * N.layer * term (* x-reduced?, layer, type *) | Abbr of term (* body *) -and term = Sort of attrs * int (* attrs, hierarchy index *) - | LRef of attrs * int (* attrs, position index *) - | GRef of attrs * uri (* attrs, reference *) - | Cast of attrs * term * term (* attrs, type, term *) - | Appl of attrs * bool * term * term (* attrs, extended?, argument, function *) - | Bind of attrs * bind * term (* attrs, binder, scope *) +and term = Sort of int (* hierarchy index *) + | LRef of n_attrs * int (* attrs, position index *) + | GRef of n_attrs * uri (* attrs, reference *) + | Cast of term * term (* type, term *) + | Appl of bool * term * term (* extended?, argument, function *) + | Bind of b_attrs * bind * term (* attrs, binder, scope *) type entity = term E.entity (* attrs, uri, binder *) type lenv = Null (* Cons: tail, relative local environment, attrs, binder *) - | Cons of lenv * lenv * attrs * bind + | Cons of lenv * lenv * n_attrs * b_attrs * bind type manager = (N.status -> entity -> bool) * (unit -> unit) @@ -48,37 +49,35 @@ let lref a i = LRef (a, i) let gref a u = GRef (a, u) -let cast a u t = Cast (a, u, t) +let cast u t = Cast (u, t) -let appl a x u t = Appl (a, x, u, t) +let appl x u t = Appl (x, u, t) -let bind a b t = Bind (a, b, t) +let bind y b t = Bind (y, b, t) -let bind_abst r n a u t = Bind (a, Abst (r, n, u), t) +let bind_abst r n y u t = Bind (y, Abst (r, n, u), t) -let bind_abbr a u t = Bind (a, Abbr u, t) +let bind_abbr y u t = Bind (y, Abbr u, t) -let bind_void a t = Bind (a, Void, t) +let bind_void y t = Bind (y, Void, t) (* local environment handling functions *************************************) let empty = Null -let push e c a b = Cons (e, c, a, b) +let push e c a y b = Cons (e, c, a, y, b) -let rec get i = function - | Null -> empty, empty, E.empty_node, Void - | Cons (e, c, a, b) when i = 0 -> e, c, a, b - | Cons (e, _, _, _) -> get (pred i) e - -let get e i = get i e +let rec get e i = match e with + | Null -> empty, empty, E.empty_node, E.empty_bind, Void + | Cons (e, c, a, y, b) when i = 0 -> e, c, a, y, b + | Cons (e, _, _, _, _) -> get e (pred i) (* used in BrgOutput.pp_lenv *) let rec fold_right f map e x = match e with - | Null -> f x - | Cons (e, c, a, b) -> fold_right (map f c a b) map e x + | Null -> f x + | Cons (e, c, a, y, b) -> fold_right (map f c a y b) map e x -let rec mem err f e b = match e with - | Null -> err () - | Cons (e, _, a, _) -> - if a.E.n_name = b.E.n_name then f () else mem err f e b +let rec mem err f e y0 = match e with + | Null -> err () + | Cons (e, _, _, y, _) -> + if y.E.b_name = y0.E.b_name then f () else mem err f e y0 diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml index 645610dd4..a7064d074 100644 --- a/helm/software/helena/src/basic_rg/brgCrg.ml +++ b/helm/software/helena/src/basic_rg/brgCrg.ml @@ -18,48 +18,48 @@ module B = Brg (* internal functions: crg to brg term **************************************) let rec xlate_term f = function - | D.TSort (a, l) -> f (B.Sort (a, l)) - | D.TGRef (a, n) -> f (B.GRef (a, n)) - | D.TLRef (a, i) -> f (B.LRef (a, i)) - | D.TCast (a, u, t) -> - let f tt uu = f (B.Cast (a, uu, tt)) in + | D.TSort k -> f (B.Sort k) + | D.TGRef (a, n) -> f (B.GRef (a, n)) + | D.TLRef (a, i) -> f (B.LRef (a, i)) + | D.TCast (u, t) -> + let f tt uu = f (B.Cast (uu, tt)) in let f tt = xlate_term (f tt) u in - xlate_term f t - | D.TAppl (a, x, v, t) -> - let f tt vv = f (B.Appl (a, x, vv, tt)) in + xlate_term f t + | D.TAppl (x, v, t) -> + let f tt vv = f (B.Appl (x, vv, tt)) in let f tt = xlate_term (f tt) v in xlate_term f t - | D.TProj (_, e, t) -> + | D.TProj (e, t) -> D.shift (xlate_term f) e t - | D.TBind (a, b, t) -> - xlate_term (xlate_bind f a b) t + | D.TBind (y, b, t) -> + xlate_term (xlate_bind f y b) t -and xlate_bind f a b t = match b with +and xlate_bind f y b t = match b with | D.Abst (r, n, w) -> - let f ww = f (B.Bind (a, B.Abst (r, n, ww), t)) in + let f ww = f (B.Bind (y, B.Abst (r, n, ww), t)) in xlate_term f w | D.Abbr v -> - let f vv = f (B.Bind (a, B.Abbr vv, t)) in + let f vv = f (B.Bind (y, B.Abbr vv, t)) in xlate_term f v | D.Void -> - f (B.Bind (a, B.Void, t)) + f (B.Bind (y, B.Void, t)) (* internal functions: brg to crg term **************************************) let rec xlate_bk_term f = function - | B.Sort (a, l) -> f (D.TSort (a, l)) - | B.GRef (a, n) -> f (D.TGRef (a, n)) - | B.LRef (a, i) -> f (D.TLRef (a, i)) - | B.Cast (a, u, t) -> - let f tt uu = f (D.TCast (a, uu, tt)) in + | B.Sort k -> f (D.TSort k) + | B.GRef (a, n) -> f (D.TGRef (a, n)) + | B.LRef (a, i) -> f (D.TLRef (a, i)) + | B.Cast (u, t) -> + let f tt uu = f (D.TCast (uu, tt)) in let f tt = xlate_bk_term (f tt) u in xlate_bk_term f t - | B.Appl (a, x, u, t) -> - let f tt uu = f (D.TAppl (a, x, uu, tt)) in + | B.Appl (x, u, t) -> + let f tt uu = f (D.TAppl (x, uu, tt)) in let f tt = xlate_bk_term (f tt) u in xlate_bk_term f t - | B.Bind (a, b, t) -> - let f tt bb = f (D.TBind (a, bb, tt)) in + | B.Bind (y, b, t) -> + let f tt bb = f (D.TBind (y, bb, tt)) in let f tt = xlate_bk_bind (f tt) b in xlate_bk_term f t diff --git a/helm/software/helena/src/basic_rg/brgEnvironment.ml b/helm/software/helena/src/basic_rg/brgEnvironment.ml index 231027ad8..01a38f89f 100644 --- a/helm/software/helena/src/basic_rg/brgEnvironment.ml +++ b/helm/software/helena/src/basic_rg/brgEnvironment.ml @@ -23,7 +23,7 @@ let env = UH.create hsize let set_entity entity = IFDEF EXPAND THEN let ra, na, uri, b = entity in - let entity0 = if !G.expand then ra, {na with E.n_apix = 0}, uri, b else entity in + let entity0 = if !G.expand then ra, E.node_attrs ~apix:0 (), uri, b else entity in UH.add env uri entity0; entity ELSE let _, _, uri, _ = entity in diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml index b8274ca30..d78f2a215 100644 --- a/helm/software/helena/src/basic_rg/brgGallina.ml +++ b/helm/software/helena/src/basic_rg/brgGallina.ml @@ -77,38 +77,38 @@ let out_name och a = E.name err f a let rec out_term st p e och = function - | B.Sort (_, h) -> - let sort = if h = 0 then "Type" else if h = 1 then "Prop" else assert false in + | B.Sort k -> + let sort = if k = 0 then "Type" else if k = 1 then "Prop" else assert false in KP.fprintf och "%s" sort | B.LRef (_, i) -> - let _, _, a, b = B.get e i in - KP.fprintf och "%a" out_name a + let _, _, _, y, b = B.get e i in + KP.fprintf och "%a" out_name y | B.GRef (_, s) -> KP.fprintf och "%a" out_uri s - | B.Cast (_, u, t) -> + | B.Cast (u, t) -> KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u - | B.Appl (_, _, v, t) -> + | B.Appl (_, v, t) -> let pt = match t with B.Appl _ -> false | _ -> true in let op, cp = if p then "(", ")" else "", "" in KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp - | B.Bind (a, B.Abst (r, n, w), t) -> + | B.Bind (y, B.Abst (r, n, w), t) -> let p = true in let op, cp = if p then "(", ")" else "", "" in - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abst r n w) in + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abst r n w) in let ob, cb = match N.to_string st n with | "1" -> "forall", "," | "2" -> "fun", " =>" | _ -> ok := false; "?", "?" in KP.fprintf och "%s%s (%a:%a)%s %a%s" - op ob out_name a (out_term st false e) w cb (out_term st false ee) t cp - | B.Bind (a, B.Abbr v, t) -> + op ob out_name y (out_term st false e) w cb (out_term st false ee) t cp + | B.Bind (y, B.Abbr v, t) -> let op, cp = if p then "(", ")" else "", "" in - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abbr v) in + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abbr v) in KP.fprintf och "%slet %a := %a in %a%s" - op out_name a (out_term st false e) v (out_term st false ee) t cp + op out_name y (out_term st false e) v (out_term st false ee) t cp | B.Bind (a, B.Void, t) -> C.err () let close_out och () = close_out och diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml index 6aa4ac34d..b3721e0ee 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ b/helm/software/helena/src/basic_rg/brgGrafite.ml @@ -72,38 +72,38 @@ let out_name och a = E.name err f a let rec out_term st p e och = function - | B.Sort (_, h) -> - let sort = if h = 0 then "Type[0]" else if h = 1 then "Prop" else assert false in + | B.Sort k -> + let sort = if k = 0 then "Type[0]" else if k = 1 then "Prop" else assert false in KP.fprintf och "%s" sort | B.LRef (_, i) -> - let _, _, a, b = B.get e i in - KP.fprintf och "%a" out_name a + let _, _, _, y, b = B.get e i in + KP.fprintf och "%a" out_name y | B.GRef (_, s) -> KP.fprintf och "%a" out_uri s - | B.Cast (_, u, t) -> + | B.Cast (u, t) -> KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u - | B.Appl (_, _, v, t) -> + | B.Appl (_, v, t) -> let pt = match t with B.Appl _ -> false | _ -> true in let op, cp = if p then "(", ")" else "", "" in KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp - | B.Bind (a, B.Abst (r, n, w), t) -> + | B.Bind (y, B.Abst (r, n, w), t) -> let op, cp = if p then "(", ")" else "", "" in - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abst r n w) in - let binder = match N.to_string st n, fst a.E.n_main with + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abst r n w) in + let binder = match N.to_string st n, fst y.E.b_main with | "1", 0 -> "Π" | "1", 1 -> "∀" | "2", _ -> "λ" | _ -> ok := false; "?" in KP.fprintf och "%s%s%a:%a.%a%s" - op binder out_name a (out_term st false e) w (out_term st false ee) t cp - | B.Bind (a, B.Abbr v, t) -> + op binder out_name y (out_term st false e) w (out_term st false ee) t cp + | B.Bind (y, B.Abbr v, t) -> let op, cp = if p then "(", ")" else "", "" in - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abbr v) in + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abbr v) in KP.fprintf och "%slet %a ≝ %a in %a%s" - op out_name a (out_term st false e) v (out_term st false ee) t cp + op out_name y (out_term st false e) v (out_term st false ee) t cp | B.Bind (a, B.Void, t) -> C.err () let close_out och () = close_out och diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml index 857d5ccac..1eb1bae3d 100644 --- a/helm/software/helena/src/basic_rg/brgLP.ml +++ b/helm/software/helena/src/basic_rg/brgLP.ml @@ -78,22 +78,22 @@ let out_name och a = E.name err f a let rec out_term st e och = function - | B.Sort (_, h) -> - let sort = if h = 0 then "k+set" else if h = 1 then "k+prop" else assert false in + | B.Sort k -> + let sort = if k = 0 then "k+set" else if k = 1 then "k+prop" else assert false in KP.fprintf och "(sort %s)" sort | B.LRef (_, i) -> - let _, _, a, b = B.get e i in - KP.fprintf och "%a" out_name a + let _, _, _, y, b = B.get e i in + KP.fprintf och "%a" out_name y | B.GRef (_, s) -> KP.fprintf och "%a" out_uri s - | B.Cast (_, u, t) -> + | B.Cast (u, t) -> KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t - | B.Appl (_, x, v, t) -> + | B.Appl (x, v, t) -> let c = if x then "appx" else "appr" in KP.fprintf och "(%s %a %a)" c (out_term st e) v (out_term st e) t - | B.Bind (a, B.Abst (r, n, w), t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abst r n w) in + | B.Bind (y, B.Abst (r, n, w), t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abst r n w) in let c = if r then "prod" else "abst" in let l = match N.to_string st n with | "1" -> "l+1" @@ -101,17 +101,13 @@ let rec out_term st e och = function | _ -> ok := false; "?" in KP.fprintf och "(%s %s %a %a\\ %a)" - c l (out_term st e) w out_name a (out_term st ee) t - | B.Bind (a, B.Abbr v, t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abbr v) in + c l (out_term st e) w out_name y (out_term st ee) t + | B.Bind (y, B.Abbr v, t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abbr v) in KP.fprintf och "(abbr %a %a\\ %a)" - (out_term st e) v out_name a (out_term st ee) t - | B.Bind (a, B.Void, t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.Void) in - KP.fprintf och "(void %a\\ %a)" - out_name a (out_term st ee) t + (out_term st e) v out_name y (out_term st ee) t + | B.Bind (_, B.Void, _) -> C.err () (* elpi variant 1 ***********************************************************) diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index 6a40aecd4..0c692045e 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -64,33 +64,33 @@ let rec count_term_binder f c e = function f c and count_term f c e = function - | B.Sort _ -> + | B.Sort _ -> f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} - | B.LRef (_, i) -> + | B.LRef (_, i) -> begin match B.get e i with - | _, _, _, B.Abst _ - | _, _, _, B.Void -> + | _, _, _, _, B.Abst _ + | _, _, _, _, B.Void -> f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} - | _, _, _, B.Abbr _ -> + | _, _, _, _, B.Abbr _ -> f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes} end - | B.GRef (_, u) -> + | B.GRef (_, u) -> let c = if Cps.list_mem ~eq:U.eq u c.uris then {c with nodes = succ c.nodes} else {c with xnodes = succ c.xnodes} in f {c with tgrefs = succ c.tgrefs} - | B.Cast (_, v, t) -> + | B.Cast (v, t) -> let c = {c with tcasts = succ c.tcasts} in let f c = count_term f c e t in count_term f c e v - | B.Appl (_, _, v, t) -> + | B.Appl (_, v, t) -> let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in let f c = count_term f c e t in count_term f c e v - | B.Bind (a, b, t) -> - let f c = count_term f c (B.push e B.empty a b) t in + | B.Bind (y, b, t) -> + let f c = count_term f c (B.push e B.empty E.empty_node y b) t in count_term_binder f c e b let count_entity f c = function @@ -106,7 +106,7 @@ let count_entity f c = function let print_counters f c = let terms = - c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts + + c.tsorts + c.tlrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts + c.tabbrs in let items = c.eabsts + c.eabbrs in @@ -143,46 +143,46 @@ let pp_level st och n = KP.fprintf och "%s" (N.to_string st n) let rec pp_term st e och = function - | B.Sort (_, h) -> - let err _ = KP.fprintf och "*%u" h in + | B.Sort k -> + let err _ = KP.fprintf och "*%u" k in let f s = KP.fprintf och "%s" s in - H.string_of_sort err f h + H.string_of_sort err f k | B.LRef (_, i) -> let err _ = KP.fprintf och "#%u" i in if !G.indexes then err () else - let _, _, a, b = B.get e i in - KP.fprintf och "%a" (name err) a + let _, _, _, y, b = B.get e i in + KP.fprintf och "%a" (name err) y | B.GRef (_, s) -> let u = U.string_of_uri s in KP.fprintf och "$%s" (if !G.short then KF.basename u else u) - | B.Cast (_, u, t) -> + | B.Cast (u, t) -> KP.fprintf och "<%a>.%a" (pp_term st e) u (pp_term st e) t - | B.Appl (_, _, v, t) -> + | B.Appl (_, v, t) -> KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t - | B.Bind (a, B.Abst (r, n, w), t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abst r n w) in - KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) a (pp_term st e) w (pp_term st ee) t - | B.Bind (a, B.Abbr v, t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abbr v) in - KP.fprintf och "[%a=%a].%a" (name C.start) a (pp_term st e) v (pp_term st ee) t - | B.Bind (a, B.Void, t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a B.Void in - KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) t + | B.Bind (y, B.Abst (r, n, w), t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abst r n w) in + KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) y (pp_term st e) w (pp_term st ee) t + | B.Bind (y, B.Abbr v, t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abbr v) in + KP.fprintf och "[%a=%a].%a" (name C.start) y (pp_term st e) v (pp_term st ee) t + | B.Bind (y, B.Void, t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y B.Void in + KP.fprintf och "[%a].%a" (name C.start) y (pp_term st ee) t let pp_lenv st och e = - let pp_entry f c a b x = - let a = R.alpha B.mem e a in - let x = B.push x c a b in + let pp_entry f c a y b x = + let y = R.alpha B.mem e y in + let x = B.push x c a y b in match b with | B.Abst (_, _, w) -> - KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x + KP.fprintf och "[%a : %a] " (name C.start) y (pp_term st c) w; f x | B.Abbr v -> - KP.fprintf och "[%a = %a] " (name C.start) a (pp_term st c) v; f x + KP.fprintf och "[%a = %a] " (name C.start) y (pp_term st c) v; f x | B.Void -> - KP.fprintf och "[%a]" (name C.start) a; f x + KP.fprintf och "[%a]" (name C.start) y; f x in if e = B.empty then KP.fprintf och "%s" "empty" else B.fold_right ignore pp_entry e B.empty diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 35f5f0222..8747e6425 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -54,19 +54,19 @@ let zero = Some 0 (* check closure *) let are_alpha_convertible err f t1 t2 = let rec aux f = function - | B.Sort (_, p1), B.Sort (_, p2) - | B.LRef (_, p1), B.LRef (_, p2) -> + | B.Sort p1, B.Sort p2 + | B.LRef (_, p1), B.LRef (_, p2) -> if p1 = p2 then f () else err () - | B.GRef (_, u1), B.GRef (_, u2) -> + | B.GRef (_, u1), B.GRef (_, u2) -> if U.eq u1 u2 then f () else err () - | B.Cast (_, v1, t1), B.Cast (_, v2, t2) - | B.Appl (_, _, v1, t1), B.Appl (_, _, v2, t2) -> + | B.Cast (v1, t1), B.Cast (v2, t2) + | B.Appl (_, v1, t1), B.Appl (_, v2, t2) -> let f _ = aux f (t1, t2) in aux f (v1, v2) - | B.Bind (_, b1, t1), B.Bind (_, b2, t2) -> + | B.Bind (_, b1, t1), B.Bind (_, b2, t2) -> let f _ = aux f (t1, t2) in aux_bind f (b1, b2) - | _ -> err () + | _ -> err () and aux_bind f = function | B.Abbr v1, B.Abbr v2 -> aux f (v1, v2) | B.Abst (r1, n1, v1), B.Abst (r2, n2, v2) when r1 = r2 && n1 = n2 -> aux f (v1, v2) @@ -88,21 +88,21 @@ let tsteps m = match m.n with | None -> 0 let get m i = - let _, c, a, b = B.get m.e i in c, a, b + let _, c, a, _, b = B.get m.e i in c, a, b (* to share *) let rec step st m r = if !G.ct >= sublevel then log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r; match r with - | B.Sort (a, h) -> + | B.Sort k -> if assert_tstep m false then - step st (tstep m) (B.Sort (a, H.apply h)) + step st (tstep m) (B.Sort (H.apply k)) else m, r, None - | B.GRef (_, uri) -> - begin match BE.get_entity uri with + | B.GRef (_, u) -> + begin match BE.get_entity u with | _, a, _, E.Abbr v -> - m, B.gref a uri, Some v + m, B.gref a u, Some v | _, _, _, E.Abst w -> if assert_tstep m true then begin if !G.summary then O.add ~grt:1 (); @@ -126,7 +126,7 @@ let rec step st m r = | _, _, B.Void -> assert false end - | B.Cast (_, u, t) -> + | B.Cast (u, t) -> if assert_tstep m false then begin if !G.summary then O.add ~e:1 (); step st (tstep m) u @@ -134,31 +134,31 @@ let rec step st m r = if !G.summary then O.add ~epsilon:1 (); step st m t end - | B.Appl (_, _, v, t) -> + | B.Appl (_, v, t) -> step st {m with s = (m.e, v) :: m.s} t - | B.Bind (a, B.Abst (false, n, w), t) -> + | B.Bind (y, B.Abst (false, n, w), t) -> let i = tsteps m in if !G.summary then O.add ~x:i (); let n = if i = 0 then n else N.minus st n i in - let r = B.Bind (a, B.Abst (true, n, w), t) in + let r = B.Bind (y, B.Abst (true, n, w), t) in step st m r - | B.Bind (a, B.Abst (true, n, w), t) -> + | B.Bind (y, B.Abst (true, n, w), t) -> if !G.si || N.is_not_zero st n then begin match m.s with | [] -> - m, B.Bind (a, B.Abst (true, n, w), t), None + m, B.Bind (y, B.Abst (true, n, w), t), None | (c, v) :: s -> if !G.summary then O.add ~beta:1 ~theta:(List.length s) (); - let v = B.Cast (E.empty_node, w, v) in - let e = B.push m.e c a (B.abbr v) in + let v = B.Cast (w, v) in + let e = B.push m.e c E.empty_node y (B.abbr v) in step st {m with e = e; s = s} t end else begin if !G.summary then O.add ~upsilon:1 (); - let e = B.push m.e m.e a B.Void in (**) (* this is wrong in general *) + let e = B.push m.e m.e E.empty_node y B.Void in (**) (* this is wrong in general *) step st {m with e = e} t end - | B.Bind (a, b, t) -> + | B.Bind (y, b, t) -> if !G.summary then O.add ~theta:(List.length m.s) (); - let e = B.push m.e m.e a b in + let e = B.push m.e m.e E.empty_node y b in step st {m with e = e} t let assert_iterations m1 m2 = @@ -167,19 +167,19 @@ let assert_iterations m1 m2 = let reset m ?(e=m.e) n = {m with e = e; n = n; s = []} -let push m a b = +let push m y b = let a, l = match b with - | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l - | _ -> a, m.l + | B.Abst _ -> E.node_attrs ~apix:m.l (), succ m.l + | _ -> E.empty_node, m.l in - let e = B.push m.e m.e a b in + let e = B.push m.e m.e a y b in {m with e = e; l = l} let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = if !G.ct >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2; match t1, r1, t2, r2 with - | B.Sort (_, h1), _, B.Sort (_, h2), _ -> - h1 = h2 + | B.Sort k1, _, B.Sort k2, _ -> + k1 = k2 | B.LRef ({E.n_apix = e1}, _), _, B.LRef ({E.n_apix = e2}, _), _ -> if e1 = e2 then ac_stacks st m1 m2 else false @@ -204,17 +204,17 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = | B.GRef _, Some v1, _, _ -> if !G.summary then O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, t2, r2) - | B.Bind (a1, (B.Abst (true, n1, w1) as b1), t1), _, - B.Bind (a2, (B.Abst (true, n2, w2) as b2), t2), _ -> + | B.Bind (y1, (B.Abst (true, n1, w1) as b1), t1), _, + B.Bind (y2, (B.Abst (true, n2, w2) as b2), t2), _ -> if ((!G.cc && N.assert_equal st n1 n2) || N.are_equal st n1 n2) && ac st (reset m1 zero) w1 (reset m2 zero) w2 - then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2 + then ac st (push m1 y1 b1) t1 (push m2 y2 b2) t2 else false - | B.Sort _, _, B.Bind (a, B.Abst (true, n, _), t), _ -> + | B.Sort _, _, B.Bind (y, B.Abst (true, n, _), t), _ -> if !G.si then if !G.cc && not (N.assert_zero st n) then false else begin if !G.summary then O.add ~upsilon:1 (); - ac st (push m1 a B.Void) t1 (push m2 a B.Void) t end + ac st (push m1 y B.Void) t1 (push m2 y B.Void) t end else false | _ -> false @@ -248,7 +248,7 @@ let empty_rtm = { let get m i = assert (m.s = []); - let _, _, _, b = B.get m.e i in b + let _, _, _, _, b = B.get m.e i in b let xwhd st m n t = if !G.ct >= level then log1 st "Now scanning" m.e t; diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli index 1a2f35007..50935000a 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.mli +++ b/helm/software/helena/src/basic_rg/brgReduction.mli @@ -17,7 +17,7 @@ val empty_rtm: rtm val get: rtm -> int -> Brg.bind -val push: rtm -> Entity.node_attrs -> Brg.bind -> rtm +val push: rtm -> Entity.bind_attrs -> Brg.bind -> rtm val xwhd: Layer.status -> rtm -> int option -> Brg.term -> rtm * Brg.term diff --git a/helm/software/helena/src/basic_rg/brgSubstitution.ml b/helm/software/helena/src/basic_rg/brgSubstitution.ml index 5661982a3..6fd4575dd 100644 --- a/helm/software/helena/src/basic_rg/brgSubstitution.ml +++ b/helm/software/helena/src/basic_rg/brgSubstitution.ml @@ -17,8 +17,8 @@ let rec icm a = function | B.LRef _ | B.GRef _ -> succ a | B.Bind (_, B.Void, t) -> icm (succ a) t - | B.Cast (_, u, t) -> icm (icm a u) t - | B.Appl (_, _, u, t) + | B.Cast (u, t) -> icm (icm a u) t + | B.Appl (_, u, t) | B.Bind (_, B.Abst (_, _, u), t) | B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t @@ -28,12 +28,12 @@ let iter map d = | B.Abst (r, n, w) -> B.Abst (r, n, iter_term d w) | B.Abbr v -> B.Abbr (iter_term d v) and iter_term d = function - | B.Sort _ as t -> t - | B.GRef _ as t -> t + | B.Sort _ as t -> t + | B.GRef _ as t -> t | B.LRef (a, i) as t -> if i < d then t else map d a i - | B.Cast (a, w, v) -> B.Cast (a, iter_term d w, iter_term d v) - | B.Appl (a, x, w, u) -> B.Appl (a, x, iter_term d w, iter_term d u) - | B.Bind (a, b, u) -> B.Bind (a, iter_bind d b, iter_term (succ d) u) + | B.Cast (w, v) -> B.Cast (iter_term d w, iter_term d v) + | B.Appl (x, w, u) -> B.Appl (x, iter_term d w, iter_term d u) + | B.Bind (y, b, u) -> B.Bind (y, iter_bind d b, iter_term (succ d) u) in iter_term d diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index 15b0b851c..7cdeb653a 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -66,62 +66,62 @@ let assert_applicability err f st m x u w v = error3 err m v w ~mu u | _ -> assert false (**) -let rec b_type_of err f st m y = - if !G.ct >= level then log1 st "Now checking" m y; - match y with - | B.Sort (a, h) -> - let h = H.apply h in f y (B.Sort (a, h)) +let rec b_type_of err f st m z = + if !G.ct >= level then log1 st "Now checking" m z; + match z with + | B.Sort k -> + let k = H.apply k in f z (B.Sort k) | B.LRef (_, i) -> begin match BR.get m i with - | B.Abst (_, _, w) -> - f y (BS.lift (succ i) (0) w) - | B.Abbr (B.Cast (_, w, _)) -> - f y (BS.lift (succ i) (0) w) - | B.Abbr _ -> assert false - | B.Void -> - error1 err "reference to excluded variable" m y + | B.Abst (_, _, w) -> + f z (BS.lift (succ i) (0) w) + | B.Abbr (B.Cast (w, _)) -> + f z (BS.lift (succ i) (0) w) + | B.Abbr _ -> assert false + | B.Void -> + error1 err "reference to excluded variable" m z end - | B.GRef (_, uri) -> - begin match BE.get_entity uri with - | _, _, _, E.Abst w -> f y w - | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f y w - | _, _, _, E.Abbr _ -> assert false - | _, _, _, E.Void -> - error1 err "reference to unknown entry" m y + | B.GRef (_, u) -> + begin match BE.get_entity u with + | _, _, _, E.Abst w -> f z w + | _, _, _, E.Abbr (B.Cast (w, _)) -> f z w + | _, _, _, E.Abbr _ -> assert false + | _, _, _, E.Void -> + error1 err "reference to unknown entry" m z end - | B.Bind (a, B.Abbr v, t) -> + | B.Bind (y, B.Abbr v, t) -> let f rv rt tt = - f (S.sh2 v rv t rt y (B.bind_abbr a)) (B.bind_abbr a rv tt) + f (S.sh2 v rv t rt z (B.bind_abbr y)) (B.bind_abbr y rv tt) in let f rv m = b_type_of err (f rv) st m t in - let f rv = f rv (BR.push m a (B.abbr rv)) in + let f rv = f rv (BR.push m y (B.abbr rv)) in let f rv vv = match rv with | B.Cast _ -> f rv - | _ -> f (B.Cast (E.empty_node, vv, rv)) + | _ -> f (B.Cast (vv, rv)) in type_of err f st m v - | B.Bind (a, B.Abst (r, n, u), t) -> + | B.Bind (y, B.Abst (r, n, u), t) -> let f ru rt tt = - f (S.sh2 u ru t rt y (B.bind_abst r n a)) (B.bind_abst r (N.minus st n 1) a ru tt) + f (S.sh2 u ru t rt z (B.bind_abst r n y)) (B.bind_abst r (N.minus st n 1) y ru tt) in let f ru m = b_type_of err (f ru) st m t in - let f ru _ = f ru (BR.push m a (B.abst r n ru)) in + let f ru _ = f ru (BR.push m y (B.abst r n ru)) in type_of err f st m u - | B.Bind (a, B.Void, t) -> + | B.Bind (y, B.Void, t) -> let f rt tt = - f (S.sh1 t rt y (B.bind_void a)) (B.bind_void a tt) + f (S.sh1 t rt z (B.bind_void y)) (B.bind_void y tt) in - b_type_of err f st (BR.push m a B.Void) t - | B.Appl (a, x, v, t) -> + b_type_of err f st (BR.push m y B.Void) t + | B.Appl (x, v, t) -> let f rv vv rt tt = - let f _ = f (S.sh2 v rv t rt y (B.appl a x)) (B.appl a x rv tt) in + let f _ = f (S.sh2 v rv t rt z (B.appl x)) (B.appl x rv tt) in assert_applicability err f st m x tt vv rv in let f rv vv = b_type_of err (f rv vv) st m t in type_of err f st m v - | B.Cast (a, u, t) -> + | B.Cast (u, t) -> let f ru rt tt = - let f _ = f (S.sh2 u ru t rt y (B.cast a)) ru in + let f _ = f (S.sh2 u ru t rt z (B.cast)) ru in assert_convertibility err f st m ru tt rt in let f ru _ = b_type_of err (f ru) st m t in diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index 877fee9d8..d6333552f 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -33,7 +33,7 @@ let type_check err f st = function let f xt tt = let xt = match xt with | B.Cast _ -> xt - | _ -> B.Cast (E.empty_node, tt, xt) + | _ -> B.Cast (tt, xt) in let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e in @@ -44,7 +44,7 @@ let validate err f st e = let uri, t = match e with | _, _, uri, E.Abst t -> uri, t | _, _, uri, E.Abbr t -> uri, t - | _, _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false in let err msg = err (L.Uri uri :: msg) in let f () = let _ = BE.set_entity e in f () in diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml index c616b22df..5de70fbfa 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.ml +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -83,18 +83,18 @@ let rec b_validate err f st m y = | _, _, _, E.Void -> error1 err "reference to unknown entry" m y end - | B.Bind (a, b, t) -> - let f () = b_validate err f st (BR.push m a b) t in + | B.Bind (y, b, t) -> + let f () = b_validate err f st (BR.push m y b) t in begin match b with | B.Abst (_, n, u) -> validate err f st m u | B.Abbr v -> validate err f st m v | B.Void -> f () end - | B.Appl (_, x, v, t) -> + | B.Appl (x, v, t) -> let f () = assert_applicability err f st m x v t in let f () = b_validate err f st m t in validate err f st m v - | B.Cast (_, u, t) -> + | B.Cast (u, t) -> let f () = assert_convertibility err f st m u t in let f () = b_validate err f st m t in validate err f st m u diff --git a/helm/software/helena/src/common/alpha.ml b/helm/software/helena/src/common/alpha.ml index 67293fac8..9eddedc73 100644 --- a/helm/software/helena/src/common/alpha.ml +++ b/helm/software/helena/src/common/alpha.ml @@ -15,8 +15,8 @@ module E = Entity let rec alpha mem x a = let err () = a in - let f () = match a.E.n_name with + let f () = match a.E.b_name with | None -> a - | Some (token, mode) -> alpha mem x {a with E.n_name = Some (token ^ "_", mode)} + | Some (token, mode) -> alpha mem x {a with E.b_name = Some (token ^ "_", mode)} in mem err f x a diff --git a/helm/software/helena/src/common/alpha.mli b/helm/software/helena/src/common/alpha.mli index cf0fafd05..e1ea7a726 100644 --- a/helm/software/helena/src/common/alpha.mli +++ b/helm/software/helena/src/common/alpha.mli @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val alpha: ((unit -> Entity.node_attrs) -> (unit -> Entity.node_attrs) -> - 'a -> Entity.node_attrs -> Entity.node_attrs +val alpha: ((unit -> Entity.bind_attrs) -> (unit -> Entity.bind_attrs) -> + 'a -> Entity.bind_attrs -> Entity.bind_attrs ) -> - 'a -> Entity.node_attrs -> Entity.node_attrs + 'a -> Entity.bind_attrs -> Entity.bind_attrs diff --git a/helm/software/helena/src/common/entity.ml b/helm/software/helena/src/common/entity.ml index d834ed53e..ab99e24cd 100644 --- a/helm/software/helena/src/common/entity.ml +++ b/helm/software/helena/src/common/entity.ml @@ -26,10 +26,13 @@ type meta = Main (* main object *) | Private (* private global definition *) type node_attrs = { - n_name: name option; (* name *) - n_apix: int; (* additional position index *) - n_main: arity; (* main arity *) - n_side: arity; (* side arity *) + n_apix: int; (* additional position index *) +} + +type bind_attrs = { + b_name: name option; (* name *) + b_main: arity; (* main arity *) + b_side: arity; (* side arity *) } type root_attrs = { @@ -45,8 +48,12 @@ type 'term entity = root_attrs * node_attrs * uri * 'term bind (* attrs, uri, bi (* helpers ******************************************************************) -let node_attrs ?name ?(main=(0,0)) ?(side=(0,0)) () = { - n_apix = 0; n_name = name; n_main = main; n_side = side; +let node_attrs ?(apix=0) () = { + n_apix = apix; +} + +let bind_attrs ?name ?(main=(0,0)) ?(side=(0,0)) () = { + b_name = name; b_main = main; b_side = side; } let root_attrs ?(meta=[]) ?info () = { @@ -55,17 +62,19 @@ let root_attrs ?(meta=[]) ?info () = { let empty_node = node_attrs () +let empty_bind = bind_attrs () + let empty_root = root_attrs () let common f (ra, na, u, _) = f ra na u let succ (sort, degr) = sort, succ degr -let compose av at = {av with n_main = at.n_main} +let compose av at = {av with b_main = at.b_main} -let shift av = {av with n_side = av.n_main} +let shift av = {av with b_side = av.b_main} -let rec name err f a = match a.n_name with +let rec name err f a = match a.b_name with | Some (n, r) -> f n r | None -> err () diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index a250d3edd..36a1c8d59 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -18,24 +18,26 @@ module E = Entity type uri = E.uri type id = E.id -type attrs = E.node_attrs +type n_attrs = E.node_attrs +type b_attrs = E.bind_attrs -type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *) - | Abbr of term (* body *) - | Void (* *) -and term = TSort of attrs * int (* attrs, hierarchy index *) - | TLRef of attrs * int (* attrs, position indexe *) - | TGRef of attrs * uri (* attrs, reference *) - | TCast of attrs * term * term (* attrs, domain, element *) - | TAppl of attrs * bool * term * term (* attrs, extended?, argument, function *) - | TBind of attrs * bind * term (* attrs, binder, scope *) - | TProj of attrs * lenv * term (* attrs, closure, member *) +type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *) + | Abbr of term (* body *) + | Void (* *) -and lenv = ESort (* top *) - | EBind of lenv * attrs * bind (* environment, attrs, binder *) - | EAppl of lenv * attrs * bool * term (* environment, attrs, extended?, argument *) - | EProj of lenv * attrs * lenv (* environment, attrs, closure *) +and term = TSort of int (* hierarchy index *) + | TLRef of n_attrs * int (* attrs, position indexe *) + | TGRef of n_attrs * uri (* attrs, reference *) + | TCast of term * term (* domain, element *) + | TAppl of bool * term * term (* extended?, argument, function *) + | TBind of b_attrs * bind * term (* attrs, binder, scope *) + | TProj of lenv * term (* closure, member *) + +and lenv = ESort (* top *) + | EBind of lenv * n_attrs * b_attrs * bind (* environment, attrs, binder *) + | EAppl of lenv * bool * term (* environment, extended?, argument *) + | EProj of lenv * lenv (* environment, closure *) type entity = term E.entity @@ -43,100 +45,98 @@ type entity = term E.entity let empty_lenv = ESort -let push_bind f a b lenv = f (EBind (lenv, a, b)) +let push_bind f a y b lenv = f (EBind (lenv, a, y, b)) -let push_appl f a x t lenv = f (EAppl (lenv, a, x, t)) +let push_appl f x t lenv = f (EAppl (lenv, x, t)) -let push_proj f a e lenv = f (EProj (lenv, a, e)) +let push_proj f e lenv = f (EProj (lenv, e)) -let add_bind f a b t = f (TBind (a, b, t)) +let add_bind f y b t = f (TBind (y, b, t)) -let add_appl f a x v t = f (TAppl (a, x, v, t)) +let add_appl f x v t = f (TAppl (x, v, t)) -let add_proj f a e t = f (TProj (a, e, t)) +let add_proj f e t = f (TProj (e, t)) let rec shift f c t = match c with | ESort -> f t - | EBind (e, a, b) -> add_bind (shift f e) a b t - | EAppl (e, a, x, v) -> add_appl (shift f e) a x v t - | EProj (e, a, d) -> add_proj (shift f e) a d t + | EBind (e, _, y, b) -> add_bind (shift f e) y b t + | EAppl (e, x, v) -> add_appl (shift f e) x v t + | EProj (e, d) -> add_proj (shift f e) d t let rec append f c = function | ESort -> f c - | EBind (e, a, b) -> append (push_bind f a b) c e - | EAppl (e, a, x, t) -> append (push_appl f a x t) c e - | EProj (e, a, d) -> append (push_proj f a d) c e + | EBind (e, a, y, b) -> append (push_bind f a y b) c e + | EAppl (e, x, t) -> append (push_appl f x t) c e + | EProj (e, d) -> append (push_proj f d) c e let resolve_lref err f id lenv = let rec aux i = function | ESort -> err () - | EAppl (tl, _, _, _) -> aux i tl - | EBind (tl, a, _) -> - let f id0 _ = if id0 = id then f a i else aux (succ i) tl in + | EAppl (tl, _, _) -> aux i tl + | EBind (tl, a, y, _) -> + let f id0 _ = if id0 = id then f a y i else aux (succ i) tl in let err () = aux (succ i) tl in - E.name err f a - | EProj (tl, _, d) -> append (aux i) tl d + E.name err f y + | EProj (tl, d) -> append (aux i) tl d in aux 0 lenv let rec get_name err f i = function - | ESort -> err i - | EAppl (tl, _, _, _) -> get_name err f i tl - | EBind (_, a, _) when i = 0 -> + | ESort -> err i + | EAppl (tl, _, _) -> get_name err f i tl + | EBind (_, _, y, _) when i = 0 -> let err () = err i in - E.name err f a - | EBind (tl, _, _) -> get_name err f (pred i) tl - | EProj (tl, _, e) -> + E.name err f y + | EBind (tl, _, _, _) -> get_name err f (pred i) tl + | EProj (tl, e) -> let err i = get_name err f i tl in get_name err f i e let rec get e i = match e with - | ESort -> ESort, E.empty_node, Void - | EBind (e, a, b) when i = 0 -> e, a, b - | EBind (e, _, _) -> get e (pred i) - | EAppl (e, _, _, _) -> get e i - | EProj (e, _, d) -> get (append C.start e d) i + | ESort -> ESort, E.empty_node, E.empty_bind, Void + | EBind (e, a, y, b) when i = 0 -> e, a, y, b + | EBind (e, _, _, _) -> get e (pred i) + | EAppl (e, _, _) -> get e i + | EProj (e, d) -> get (append C.start e d) i let rec sub_list_strict f e l = match e, l with - | _, [] -> f e - | EBind (e, _, Abst _), _ :: tl -> sub_list_strict f e tl - | _ -> assert false + | _, [] -> f e + | EBind (e, _, _, Abst _), _ :: tl -> sub_list_strict f e tl + | _ -> assert false let rec fold_names f map x = function - | ESort -> f x - | EBind (e, {E.n_name = Some n}, Abst _) -> fold_names f map (map x n) e - | _ -> assert false + | ESort -> f x + | EBind (e, _, {E.b_name = Some n}, Abst _) -> fold_names f map (map x n) e + | _ -> assert false -let rec mem err f e b = match e with +let rec mem err f e y0 = match e with | ESort -> err () - | EBind (e, a, _) -> - if a.E.n_name = b.E.n_name then f () else mem err f e b - | EAppl (e, _, _, _) -> mem err f e b - | EProj (e, _, d) -> - let err () = mem err f e b in mem err f d b + | EBind (e, _, y, _) -> + if y.E.b_name = y0.E.b_name then f () else mem err f e y0 + | EAppl (e, _, _) -> mem err f e y0 + | EProj (e, d) -> + let err () = mem err f e y0 in mem err f d y0 let set_layer f n0 e = let rec aux f = function - | ESort -> f ESort - | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e - | EBind (e, a, b) -> aux (push_bind f a b) e - | EAppl (e, a, x, v) -> aux (push_appl f a x v) e - | EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d + | ESort -> f ESort + | EBind (e, a, y, Abst (r, n, w)) -> aux (push_bind f a y (Abst (r, n0, w))) e + | EBind (e, a, y, b) -> aux (push_bind f a y b) e + | EAppl (e, x, v) -> aux (push_appl f x v) e + | EProj (e, d) -> let f d = aux (push_proj f d) e in aux f d in aux f e -let set_attrs f a0 e = +let set_attrs f y0 e = let rec aux f = function | ESort -> f ESort - | EBind (e, a, b) -> - let a = E.compose a a0 in - aux (push_bind f a b) e - | EAppl (e, a, x, v) -> - let a = E.compose a a0 in - aux (push_appl f a x v) e - | EProj (e, a, d) -> - let a = E.compose a a0 in - let f d = aux (push_proj f a d) e in + | EBind (e, a, y, b) -> + let y = E.compose y y0 in + aux (push_bind f a y b) e + | EAppl (e, x, v) -> + aux (push_appl f x v) e + | EProj (e, d) -> + let f d = aux (push_proj f d) e in aux f d in aux f e diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index 95c3e8801..7463c769a 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -48,48 +48,48 @@ let initial_counters = { } let rec count_term f c e = function - | D.TSort _ -> + | D.TSort _ -> f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} - | D.TLRef (_, i) -> + | D.TLRef (_, i) -> begin match D.get e i with - | _, _, D.Abbr _ -> + | _, _, _, D.Abbr _ -> f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes} - | _ -> + | _ -> f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} end - | D.TGRef (_, u) -> + | D.TGRef (_, u) -> let c = if C.list_mem ~eq:U.eq u c.uris then {c with nodes = succ c.nodes} else {c with xnodes = succ c.xnodes} in f {c with tgrefs = succ c.tgrefs} - | D.TCast (_, v, t) -> + | D.TCast (v, t) -> let c = {c with tcasts = succ c.tcasts} in let f c = count_term f c e t in count_term f c e v - | D.TAppl (_, _, v, t) -> + | D.TAppl (_, v, t) -> let c = {c with tappls = succ c.tappls} in let f c = count_term f c e t in count_term f c e v - | D.TProj (_, d, t) -> + | D.TProj (d, t) -> D.shift (count_term f c e) d t - | D.TBind (a, b, t) -> + | D.TBind (y, b, t) -> let f c e = count_term f c e t in - count_binder f c e a b + count_binder f c e y b -and count_binder f c e a b = match b with +and count_binder f c e y b = match b with | D.Abst (_, _, w) -> let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in - let f c = D.push_bind (f c) a b e in + let f c = D.push_bind (f c) E.empty_node y b e in count_term f c e w | D.Abbr v -> let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in - let f c = D.push_bind (f c) a b e in + let f c = D.push_bind (f c) E.empty_node y b e in count_term f c e v | D.Void -> let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in - D.push_bind (f c) a b e + D.push_bind (f c) E.empty_node y b e let count_entity f c = function | _, _, u, E.Abst w -> @@ -129,21 +129,23 @@ let print_counters f c = (* term/environment pretty printer ******************************************) -let pp_attrs out a = +let pp_b_attrs out a = let f s b = if b then out (KP.sprintf "%s;" s) else out (KP.sprintf "~%s;" s) in - E.name ignore f a; + E.name ignore f a + +let pp_n_attrs out a = out (KP.sprintf "+%i;" a.E.n_apix) let pp_state out x = if x then out "^" let rec pp_term out st = function - | D.TSort (a, l) -> pp_attrs out a; out (KP.sprintf "*%u" l) - | D.TLRef (a, i ) -> pp_attrs out a; out (KP.sprintf "#%u" i) - | D.TGRef (a, u) -> pp_attrs out a; out (KP.sprintf "$") - | D.TCast (a, u, t) -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t - | D.TAppl (a, _, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t - | D.TBind (a, u, t) -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t - | D.TProj (a, u, t) -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t + | D.TSort k -> out (KP.sprintf "*%u" k) + | D.TLRef (a, i) -> pp_n_attrs out a; out (KP.sprintf "#%u" i) + | D.TGRef (a, u) -> pp_n_attrs out a; out (KP.sprintf "$") + | D.TCast (u, t) -> out "<"; pp_term out st u; out ">."; pp_term out st t + | D.TAppl (_, u, t) -> out "("; pp_term out st u; out ")."; pp_term out st t + | D.TBind (y, u, t) -> pp_b_attrs out y; pp_bind out st u; out "."; pp_term out st t + | D.TProj (u, t) -> out "{"; pp_lenv out st u; out "}."; pp_term out st t and pp_bind out st = function | D.Abst (r, n, u) -> @@ -153,6 +155,6 @@ and pp_bind out st = function and pp_lenv out st = function | D.ESort -> () - | D.EBind (u, a, t) -> pp_lenv out st u; pp_attrs out a; pp_bind out st t - | D.EAppl (u, a, _, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") " - | D.EProj (u, a, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} " + | D.EBind (u, a, y, t) -> pp_lenv out st u; pp_b_attrs out y; pp_n_attrs out a; pp_bind out st t + | D.EAppl (u, _, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") " + | D.EProj (u, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} " diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index 1ba830669..174857d43 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -38,17 +38,17 @@ let xerr s () = (* Internal functions *******************************************************) -let mk_lref f a i = f a (D.TLRef (a, i)) +let mk_lref f a y i = f y (D.TLRef (a, i)) -let mk_gref f a uri = f a (D.TGRef (a, uri)) +let mk_gref f y uri = f y (D.TGRef (E.empty_node, uri)) let get err f e i = match D.get e i with - | _, _, D.Void -> err () - | _, a, _ -> mk_lref f a i + | _, _, _, D.Void -> err () + | _, a, y, _ -> mk_lref f a y i let resolve_gref err f st id = try - let a, uri = KH.find henv id in f a uri + let y, uri = KH.find henv id in f y uri with Not_found -> err () let name_of_id ?(r=true) id = @@ -65,9 +65,9 @@ let rec xlate_term f st lenv = function CrgOutput.pp_lenv print_string (Layer.initial_status ()) lenv; Printf.printf "\n"; *) - | T.Sort h -> - let a = E.node_attrs ~main:(h, 0) () in - f a (D.TSort (a, h)) + | T.Sort k -> + let y = E.bind_attrs ~main:(k, 0) () in + f y (D.TSort k) | T.NSrt id -> let f h = xlate_term f st lenv (T.Sort h) in H.sort_of_string (xerr "sort not found") f id @@ -77,46 +77,46 @@ let rec xlate_term f st lenv = function let err () = resolve_gref (xerr "global constant not found") (mk_gref f) st id in D.resolve_lref err (mk_lref f) id lenv | T.Cast (u, t) -> - let f uu a tt = f a (D.TCast (a, uu, tt)) in + let f uu y tt = f y (D.TCast (uu, tt)) in let f _ uu = xlate_term (f uu) st lenv t in xlate_term f st lenv u | T.Appl (v, t) -> - let f vv a tt = f a (D.TAppl (a, st.ext, vv, tt)) in + let f vv y tt = f y (D.TAppl (st.ext, vv, tt)) in let f _ vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | T.Proj (bs, t) -> - let f e a tt = f a (D.TProj (a, e, tt)) in + let f e y tt = f y (D.TProj (e, tt)) in let f (lenv, e) = xlate_term (f e) st lenv t in C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs | T.Inst (t, vs) -> let map f v e = - let f _ vv = D.push_appl f E.empty_node st.ext vv e in + let f _ vv = D.push_appl f st.ext vv e in xlate_term f st lenv v in - let f e a tt = f a (D.TProj (a, e, tt)) in + let f e y tt = f y (D.TProj (e, tt)) in let f e = xlate_term (f e) st lenv t in C.list_fold_right f map vs D.empty_lenv and xlate_bind st f (lenv, e) b = let f lenv e = f (lenv, e) in - let f a b lenv = D.push_bind (f lenv) a b e in - let f a b = D.push_bind (f a b) a b lenv in + let f y b lenv = D.push_bind (f lenv) E.empty_node y b e in + let f y b = D.push_bind (f y b) E.empty_node y b lenv in match b with | T.Abst (n, id, r, w) -> - let f a ww = - let a = {a with E.n_name = name_of_id ~r id} in - f a (D.Abst (false, n, ww)) + let f y ww = + let y = E.bind_attrs ?name:(name_of_id id) () in + f y (D.Abst (false, n, ww)) in xlate_term f st lenv w | T.Abbr (id, v) -> - let f a vv = - let a = {a with E.n_name = name_of_id id} in - f a (D.Abbr vv) + let f y vv = + let y = E.bind_attrs ?name:(name_of_id id) () in + f y (D.Abbr vv) in xlate_term f st lenv v | T.Void id -> - let a = E.node_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in - f a D.Void + let y = E.bind_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in + f y D.Void let mk_contents main kind tt = let ms, b = match kind with @@ -152,17 +152,16 @@ let xlate_entity err f gen st = function assert (H.set_graph id); err st | T.Constant (main, kind, id, info, t) -> let uri = uri_of_id st id st.path in - let g na tt = + let g ya tt = + KH.add henv id (ya, uri); (* print_newline (); CrgOutput.pp_term print_string tt; *) - let na = {na with E.n_apix = st.line} in - KH.add henv id (na, uri); let meta, b = mk_contents main kind tt in + let na = E.node_attrs ~apix:st.line () in let ra = E.root_attrs ~meta ~info () in let entity = ra, na, uri, b in f {st with line = succ st.line} entity - in xlate_term g st D.empty_lenv t | T.Generate _ -> diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index b2029149b..673eefa0c 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -21,76 +21,76 @@ module D = Crg let lenv_iter map_bind map_appl map_proj st e lenv out tab = let rec aux = function - | D.ESort -> e - | D.EBind (e, a, b) -> + | D.ESort -> e + | D.EBind (e, a, y, b) -> let e = aux e in (* NOTE: the inner binders are alpha-converted first *) - let a = R.alpha D.mem e a in - map_bind st e a b out tab; D.EBind (e, a, b) - | D.EAppl (e, a, x, v) -> + let y = R.alpha D.mem e y in + map_bind st e a y b out tab; D.EBind (e, a, y, b) + | D.EAppl (e, x, v) -> let e = aux e in - map_appl st e a x v out tab; D.EAppl (e, a, x, v) - | D.EProj (e, a, d) -> + map_appl st e x v out tab; D.EAppl (e, x, v) + | D.EProj (e, d) -> let e = aux e in - map_proj st e a d out tab; D.EProj (e, a, d) + map_proj st e d out tab; D.EProj (e, d) in ignore (aux lenv) let rec exp_term st e t out tab = match t with - | D.TSort (a, h) -> - let a = - let err _ = a in - let f s = {a with E.n_name = Some (s, true)} in - H.string_of_sort err f h + | D.TSort k -> + let y = + let err _ = E.empty_bind in + let f s = E.bind_attrs ~name:(s, true) () in + H.string_of_sort err f k in - let attrs = [XL.position h; XL.name a] in + let attrs = [XL.position k; XL.name y] in XL.tag XL.sort attrs out tab - | D.TLRef (a, i) -> - let a = - let err _ = a in - let f n r = {a with E.n_name = Some (n, r)} in + | D.TLRef (_, i) -> + let y = + let err _ = E.empty_bind in + let f s r = E.bind_attrs ~name:(s, r) () in D.get_name err f i e in - let attrs = [XL.depth i; XL.name a] in + let attrs = [XL.depth i; XL.name y] in XL.tag XL.lref attrs out tab - | D.TGRef (a, n) -> - let a = {a with E.n_name = Some (U.name_of_uri n, true)} in - let attrs = [XL.uri n; XL.name a] in + | D.TGRef (_, n) -> + let y = E.bind_attrs ~name:(U.name_of_uri n, true) () in + let attrs = [XL.uri n; XL.name y] in XL.tag XL.gref attrs out tab - | D.TCast (a, u, t) -> + | D.TCast (u, t) -> let attrs = [] in XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab; exp_term st e t out tab - | D.TAppl (a, x, v, t) -> + | D.TAppl (x, v, t) -> let attrs = [] in XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab; exp_term st e t out tab - | D.TProj (a, lenv, t) -> + | D.TProj (lenv, t) -> let attrs = [] in XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab; - exp_term st (D.push_proj C.start a lenv e) t out tab - | D.TBind (a, b, t) -> + exp_term st (D.push_proj C.start lenv e) t out tab + | D.TBind (y, b, t) -> (* NOTE: the inner binders are alpha-converted first *) - let a = R.alpha D.mem e a in - exp_bind st e a b out tab; - exp_term st (D.push_bind C.start a b e) t out tab + let y = R.alpha D.mem e y in + exp_bind st e E.empty_node y b out tab; + exp_term st (D.push_bind C.start E.empty_node y b e) t out tab -and exp_appl st e a x v out tab = +and exp_appl st e x v out tab = let attrs = [] in XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab; -and exp_bind st e a b out tab = match b with +and exp_bind st e a y b out tab = match b with | D.Abst (_, n, w) -> - let attrs = [XL.layer st n; XL.name a] in + let attrs = XL.layer st n :: XL.name y :: XL.side y @ XL.main y in XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab | D.Abbr v -> - let attrs = [XL.name a] in + let attrs = [XL.name y] in XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab | D.Void -> - let attrs = [XL.name a] in + let attrs = [XL.name y] in XL.tag XL.void attrs out tab -and exp_proj st e a lenv out tab = +and exp_proj st e lenv out tab = let attrs = [] in XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj st e lenv) out tab diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index 002688b31..901c783a2 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -103,13 +103,13 @@ let layer st n = "layer", N.to_string st n let main a = - let sort, degr = a.E.n_main in + let sort, degr = a.E.b_main in ["main-position", string_of_int sort; "main-degree", string_of_int degr; ] let side a = - let sort, degr = a.E.n_side in + let sort, degr = a.E.b_side in ["side-position", string_of_int sort; "side-degree", string_of_int degr; ] @@ -138,8 +138,8 @@ let export_entity pp_term (ra, na, u, b) = let och = open_out (path ^ ext) in let out = output_string och in xml out "1.0" "UTF-8"; doctype out obj_root system; - let na = {na with E.n_name = Some (U.name_of_uri u, true)} in - let attrs = uri u :: name na :: apix na :: meta ra :: info ra in + let ba = E.bind_attrs ~name:(U.name_of_uri u, true) () in + let attrs = uri u :: name ba :: apix na :: meta ra :: info ra in let contents = match b with | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w) | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v) diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index 0dbfb54aa..202ec2c27 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -45,11 +45,11 @@ val uri: Entity.uri -> attr val layer: Layer.status -> Layer.layer -> attr -val name: Entity.node_attrs -> attr +val name: Entity.bind_attrs -> attr -val main: Entity.node_attrs -> attr list +val main: Entity.bind_attrs -> attr list -val side: Entity.node_attrs -> attr list +val side: Entity.bind_attrs -> attr list val apix: Entity.node_attrs -> attr