From 251534dbf294c645d2121df2d9ce240011fa0c91 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 20 Nov 2014 16:02:51 +0000 Subject: [PATCH] new intermediate language complete_rg, more similar to what lambdadelta version 4 should be --- helm/software/helena/.depend.opt | 8 +- helm/software/helena/src/automath/autCrg.ml | 82 +++++------ helm/software/helena/src/basic_ag/bag.ml | 2 +- helm/software/helena/src/basic_ag/bagCrg.ml | 89 +++++------- helm/software/helena/src/basic_rg/brgCrg.ml | 54 +++---- .../helena/src/basic_rg/brgReduction.ml | 4 +- helm/software/helena/src/complete_rg/crg.ml | 136 ++++++++++-------- .../helena/src/complete_rg/crgOutput.ml | 84 +++++------ helm/software/helena/src/lib/cps.ml | 4 + helm/software/helena/src/text/txtCrg.ml | 6 +- helm/software/helena/src/xml/xmlCrg.ml | 90 +++++------- helm/software/helena/src/xml/xmlLibrary.ml | 15 +- helm/software/helena/src/xml/xmlLibrary.mli | 4 - 13 files changed, 257 insertions(+), 321 deletions(-) diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index b2015af33..22608ffa0 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -41,11 +41,11 @@ src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx \ src/lib/cps.cmx src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ - src/lib/cps.cmx src/complete_rg/crgOutput.cmi + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/complete_rg/crgOutput.cmi src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ - src/lib/cps.cmx src/complete_rg/crgOutput.cmi + src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ + src/complete_rg/crgOutput.cmi src/text/txt.cmo: src/common/level.cmi src/text/txt.cmx: src/common/level.cmx src/text/txtParser.cmi: src/text/txt.cmx diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index dfd51aa47..025459d2e 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -44,12 +44,12 @@ let hcnt = K.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) -let empty_cnt = [], [] +let empty_cnt = D.ESort -let add_abst (a, ws) id w = - E.Name (id, true) :: a, w :: ws +let add_abst cnt id w = + D.EBind (cnt, [E.Name (id, true)], D.Abst (N.infinite, w)) -let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) +let mk_lref f i = f (D.TLRef ([], i)) let id_of_name (id, _, _) = id @@ -82,7 +82,7 @@ let relax_opt_qid f st = function | Some qid -> let f qid = f (Some qid) in relax_qid f st qid let resolve_gref err f st qid = - try let cnt = K.find henv (uri_of_qid qid) in f qid cnt + try let age, cnt = K.find henv (uri_of_qid qid) in f qid age cnt with Not_found -> err qid let resolve_gref_relaxed f st qid = @@ -101,15 +101,16 @@ let get_cnt_relaxed f st = let rec err node = relax_opt_qid (get_cnt err f st) st node in get_cnt err f st st.node -(****************************************************************************) +let push_abst f a w lenv = + let bw = D.Abst (N.infinite, w) in + D.push_bind f a bw lenv -let push_abst f lenv a w = - let bw = D.Abst (N.infinite, [w]) in - let f lenv = f lenv in - D.push_bind f lenv a bw +let add_proj e t = match e with + | D.ESort -> t + | D.EBind (D.ESort, a, b) -> D.TBind (a, b, t) + | _ -> D.TProj ([], e, t) -let lenv_of_cnt (a, ws) = - D.push_bind C.start D.empty_lenv a (D.Abst (N.infinite, ws)) +let lenv_of_cnt cnt = cnt (* this is not tail recursive in the GRef branch *) let rec xlate_term f st lenv = function @@ -117,36 +118,38 @@ let rec xlate_term f st lenv = function let f h = f (D.TSort ([], h)) in if s then f 0 else f 1 | A.Appl (v, t) -> - let f vv tt = f (D.TAppl ([], [vv], tt)) in + let f vv tt = f (D.TAppl ([], vv, tt)) in let f vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | A.Abst (name, w, t) -> let f ww = let a = [E.Name (name, true)] in let f tt = - let b = D.Abst (N.infinite, [ww]) in + let b = D.Abst (N.infinite, ww) in f (D.TBind (a, b, tt)) in let f lenv = xlate_term f st lenv t in - push_abst f lenv a ww + push_abst f a ww lenv in xlate_term f st lenv w | A.GRef (name, args) -> - let map1 f = function - | E.Name (id, _) -> f (A.GRef ((id, true, []), [])) - | _ -> C.err () + let map1 args a = + let f id _ = A.GRef ((id, true, []), []) :: args in + E.name C.err f a in - let map2 f t = xlate_term f st lenv t in - let g qid (a, _) = - let gref age = D.TGRef ([age], uri_of_qid qid) in - match args, a with - | [], [age] -> f (gref age) - | _ , age :: a -> - let f args = f (D.TAppl ([], args, gref age)) in - let f args = C.list_rev_map f map2 args in - let f a = C.list_rev_map_append f map1 a ~tail:args in - C.list_sub_strict f a args - | _ -> assert false + let map2 f arg args = + let f arg = f (D.EAppl (args, [], arg)) in + xlate_term f st lenv arg + in + let g qid age cnt = + let gref = D.TGRef ([age], uri_of_qid qid) in + if cnt = D.ESort then f gref else + let f = function + | D.EAppl (D.ESort, a, v) -> f (D.TAppl (a, v, gref)) + | args -> f (D.TProj ([], args, gref)) + in + let f args = C.list_fold_right f map2 args D.ESort in + D.sub_list_strict (D.fold_attrs f map1 args) cnt args in let g qid = resolve_gref_relaxed g st qid in let err () = complete_qid g st name in @@ -169,28 +172,23 @@ let xlate_entity err f st = function | A.Block (name, w) -> let f qid = let f cnt = - let lenv = lenv_of_cnt cnt in let f ww = K.add hcnt (uri_of_qid qid) (add_abst cnt name ww); err {st with node = Some qid} in - xlate_term f st lenv w + xlate_term f st cnt w in get_cnt_relaxed f st in complete_qid f st (name, true, []) | A.Decl (name, w) -> let f cnt = - let a, ws = cnt in let lenv = lenv_of_cnt cnt in let f qid = let f ww = let age = E.Apix st.line in - K.add henv (uri_of_qid qid) (age :: a, ws); - let t = match ws with - | [] -> ww - | _ -> D.TBind (a, D.Abst (N.infinite, ws), ww) - in + K.add henv (uri_of_qid qid) (age, cnt); + let t = add_proj lenv ww in (* print_newline (); CrgOutput.pp_term print_string t; *) @@ -204,18 +202,14 @@ let xlate_entity err f st = function in get_cnt_relaxed f st | A.Def (name, w, trans, v) -> - let f cnt = - let a, ws = cnt in + let f cnt = let lenv = lenv_of_cnt cnt in let f qid = let f ww = let f vv = let age = E.Apix st.line in - K.add henv (uri_of_qid qid) (age :: a, ws); - let t = match ws with - | [] -> D.TCast ([], ww, vv) - | _ -> D.TBind (a, D.Abst (N.infinite, ws), D.TCast ([], ww, vv)) - in + K.add henv (uri_of_qid qid) (age, cnt); + let t = add_proj lenv (D.TCast ([], ww, vv)) in (* print_newline (); CrgOutput.pp_term print_string t; *) diff --git a/helm/software/helena/src/basic_ag/bag.ml b/helm/software/helena/src/basic_ag/bag.ml index fc0f72f9a..5e7c07b5b 100644 --- a/helm/software/helena/src/basic_ag/bag.ml +++ b/helm/software/helena/src/basic_ag/bag.ml @@ -30,7 +30,7 @@ and term = Sort of int (* hierarchy index *) type entity = term E.entity (* attrs, uri, binder *) -type lenv = (attrs * int * bind) list (* location, name, binder *) +type lenv = (attrs * int * bind) list (* name, location, binder *) type message = (lenv, term) Log.item list diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index 8fbf7cf79..1bd594503 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -18,56 +18,41 @@ module Z = Bag (* internal functions: crg to bag term **************************************) -let rec shift t = function - | _, [] -> t - | (a, l, b) :: c, _ :: ns -> shift (Z.Bind (a, l, b, t)) (c, ns) - | _ -> assert false - -let rec xlate_term xlate_bind f c = function - | D.TSort (_, h) -> f (Z.Sort h) - | D.TGRef (_, s) -> f (Z.GRef s) - | D.TLRef (a, _, _) -> - let f i = - let _, l, _ = List.nth c i in - f (Z.LRef l) - in - E.apix C.err f a - | D.TCast (_, u, t) -> +let rec xlate_term f c = function + | D.TSort (_, h) -> f (Z.Sort h) + | D.TGRef (_, s) -> f (Z.GRef s) + | D.TLRef (a, i) -> + let _, l, _ = List.nth c i in f (Z.LRef l) + | D.TCast (_, u, t) -> let f tt uu = f (Z.Cast (uu, tt)) in - let f tt = xlate_term xlate_bind (f tt) c u in - xlate_term xlate_bind f c t - | D.TAppl (_, vs, t) -> - let map f v tt = let f vv = f (Z.Appl (vv, tt)) in xlate_term xlate_bind f c v in - let f tt = C.list_fold_right f map vs tt in - xlate_term xlate_bind f c t - | D.TProj (_, e, t) -> - xlate_term xlate_bind f c (D.tshift e t) + let f tt = xlate_term (f tt) c u in + xlate_term f c t + | D.TAppl (_, v, t) -> + let f tt vv = f (Z.Appl (vv, tt)) in + let f tt = xlate_term (f tt) c v in + xlate_term f c t + | D.TProj (_, e, t) -> + D.shift (xlate_term f c) e t (* this case should be removed by improving alpha-conversion *) | D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) -> - xlate_term xlate_bind f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t))) - | D.TBind (a, b, t) -> - let g _ ns = ns in - let ns = E.get_names g a in - let cc = xlate_bind C.start c ns b in - let f tt = f (shift tt (cc, ns)) in - xlate_term xlate_bind f cc t - -let rec xlate_bind f c ns = function - | D.Abst (_, ws) -> - let map f n w c = - let f ww = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abst ww) in - xlate_term xlate_bind f c w + xlate_term f c (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), t))) + | D.TBind (a, 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 f cc t in - C.list_fold_right2 f map ns ws c - | D.Abbr vs -> - let map f n v c = - let f vv = Z.push "xlate_bind" f c [n] (J.new_location ()) (Z.Abbr vv) in - xlate_term xlate_bind f c v - in - C.list_fold_right2 f map ns vs c - | D.Void _ -> - let map f n c = Z.push "xlate_bind" f c [n] (J.new_location ()) Z.Void in - C.list_fold_right f map ns c + xlate_bind f c a b + +and xlate_bind f c a = function + | D.Abst (_, w) -> + let f ww = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abst ww) in + xlate_term f c w + | D.Abbr v -> + let f vv = Z.push "xlate_bind" f c a (J.new_location ()) (Z.Abbr vv) in + xlate_term f c v + | D.Void -> + Z.push "xlate_bind" f c a (J.new_location ()) Z.Void (* internal functions: bag to crg term **************************************) @@ -75,14 +60,14 @@ let rec xlate_bk_term f c = function | Z.Sort h -> f (D.TSort ([], h)) | Z.GRef s -> f (D.TGRef ([], s)) | Z.LRef l -> - let f i = f (D.TLRef ([], i, 0)) in + let f i = f (D.TLRef ([], i)) in Z.nth C.err f l c | Z.Cast (u, t) -> 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 ([], [uu], tt)) in + let f tt uu = f (D.TAppl ([], 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) -> @@ -93,16 +78,16 @@ let rec xlate_bk_term f c = function and xlate_bk_bind f c = function | Z.Abst t -> - let f tt = f (D.Abst (N.infinite, [tt])) in + let f tt = f (D.Abst (N.infinite, tt)) in xlate_bk_term f c t | Z.Abbr t -> - let f tt = f (D.Abbr [tt]) in + let f tt = f (D.Abbr tt) in xlate_bk_term f c t - | Z.Void -> f (D.Void 1) + | Z.Void -> f D.Void (* interface functions ******************************************************) let bag_of_crg f t = - xlate_term xlate_bind f Z.empty_lenv t + xlate_term f Z.empty_lenv t let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml index 8514de641..f646145ed 100644 --- a/helm/software/helena/src/basic_rg/brgCrg.ml +++ b/helm/software/helena/src/basic_rg/brgCrg.ml @@ -21,52 +21,42 @@ module B = Brg 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, _, _) -> let f i = f (B.LRef (a, i)) in E.apix C.err f a + | 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 let f tt = xlate_term (f tt) u in xlate_term f t - | D.TAppl (a, vs, t) -> - let map f v tt = let f vv = f (B.Appl (a, vv, tt)) in xlate_term f v in - let f tt = C.list_fold_right f map vs tt in - xlate_term f t + | D.TAppl (a, v, t) -> + let f tt vv = f (B.Appl (a, vv, tt)) in + let f tt = xlate_term (f tt) v in + xlate_term f t | D.TProj (_, e, t) -> - xlate_term f (D.tshift e t) - | D.TBind (a, b, t) -> - let f tt = f (xlate_bind tt a b) in xlate_term f t + D.shift (xlate_term f) e t + | D.TBind (a, b, t) -> + xlate_term (xlate_bind f a b) t -and xlate_bind x a b = - let f a ns = a, ns in - let a, ns = E.get_names f a in - match b with - | D.Abst (m, ws) -> - let map x n w = - let f ww = B.Bind (n :: J.new_mark () :: a, B.Abst (m, ww), x) in - xlate_term f w - in - List.fold_left2 map x ns ws - | D.Abbr vs -> - let map x n v = - let f vv = B.Bind (n :: a, B.Abbr vv, x) in - xlate_term f v - in - List.fold_left2 map x ns vs - | D.Void _ -> - let map x n = B.Bind (n :: a, B.Void, x) in - List.fold_left map x ns +and xlate_bind f a b x = match b with + | D.Abst (n, w) -> + let f ww = f (B.Bind (J.new_mark () :: a, B.Abst (n, ww), x)) in + xlate_term f w + | D.Abbr v -> + let f vv = f (B.Bind (a, B.Abbr vv, x)) in + xlate_term f v + | D.Void -> + f (B.Bind (a, B.Void, x)) (* 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, 0)) + | 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 let f tt = xlate_bk_term (f tt) u in xlate_bk_term f t | B.Appl (a, u, t) -> - let f tt uu = f (D.TAppl (a, [uu], tt)) in + let f tt uu = f (D.TAppl (a, uu, tt)) in let f tt = xlate_bk_term (f tt) u in xlate_bk_term f t | B.Bind (a, b, t) -> @@ -76,12 +66,12 @@ let rec xlate_bk_term f = function and xlate_bk_bind f = function | B.Abst (n, t) -> - let f tt = f (D.Abst (n, [tt])) in + let f tt = f (D.Abst (n, tt)) in xlate_bk_term f t | B.Abbr t -> - let f tt = f (D.Abbr [tt]) in + let f tt = f (D.Abbr tt) in xlate_bk_term f t - | B.Void -> f (D.Void 1) + | B.Void -> f D.Void (* interface functions ******************************************************) diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index c3ef9795b..09e262d12 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -181,7 +181,7 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = let e2 = E.apix C.err C.start a2 in if e1 = e2 then ac_stacks st m1 m2 else false | B.GRef (_, u1), None, B.GRef (_, u2), None -> - if U.eq u1 u2 & assert_iterations m1 m2 then ac_stacks st m1 m2 else false + if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false | B.GRef (a1, u1), Some v1, B.GRef (a2, u2), Some v2 -> let e1 = E.apix C.err C.start a1 in let e2 = E.apix C.err C.start a2 in @@ -191,7 +191,7 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = end else if e2 < e1 then begin if !G.summary then O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, t2, r2) - end else if U.eq u1 u2 & assert_iterations m1 m2 && ac_stacks st m1 m2 then true + end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true else begin if !G.summary then O.add ~gdelta:2 (); ac st m1 v1 m2 v2 diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index 9518ff60b..7ba80ddfb 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -20,44 +20,76 @@ type uri = E.uri type id = E.id type attrs = E.attrs -type bind = Abst of N.level * term list (* level, domains *) - | Abbr of term list (* bodies *) - | Void of int (* number of exclusions *) - -and term = TSort of attrs * int (* attrs, hierarchy index *) - | TLRef of attrs * int * int (* attrs, position indexes *) - | TGRef of attrs * uri (* attrs, reference *) - | TCast of attrs * term * term (* attrs, domain, element *) - | TAppl of attrs * term list * term (* attrs, arguments, function *) - | TProj of attrs * lenv * term (* attrs, closure, member *) - | TBind of attrs * bind * term (* attrs, binder, scope *) +type bind = Abst of N.level * term (* level, 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 * term * term (* attrs, argument, function *) + | TBind of attrs * bind * term (* attrs, binder, scope *) + | TProj of attrs * lenv * term (* attrs, closure, member *) and lenv = ESort (* top *) - | EProj of lenv * attrs * lenv (* environment, attrs, closure *) | EBind of lenv * attrs * bind (* environment, attrs, binder *) + | EAppl of lenv * attrs * term (* environment, attrs, argument *) + | EProj of lenv * attrs * lenv (* environment, attrs, closure *) type entity = term E.entity (* helpers ******************************************************************) -let rec tshift t = function - | ESort -> t - | EBind (e, a, b) -> tshift (TBind (a, b, t)) e - | EProj (e, a, d) -> tshift (TProj (a, d, t)) e +let empty_lenv = ESort -let tshift c t = tshift t c +let push_bind f a b lenv = f (EBind (lenv, a, b)) -let rec eshift f c = function - | ESort -> f c - | EBind (e, a, b) -> let f ee = f (EBind (ee, a, b)) in eshift f c e - | EProj (e, a, d) -> let f ee = f (EProj (ee, a, d)) in eshift f c e +let push_appl f a t lenv = f (EAppl (lenv, a, t)) -let empty_lenv = ESort +let push_proj f a e lenv = f (EProj (lenv, a, e)) + +let add_bind f a b t = f (TBind (a, b, t)) + +let add_appl f a v t = f (TAppl (a, v, t)) -let push_bind f lenv a b = f (EBind (lenv, a, b)) +let add_proj f a e t = f (TProj (a, e, t)) -let push_proj f lenv a e = f (EProj (lenv, a, e)) +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, v) -> add_appl (shift f e) a v t + | EProj (e, a, d) -> add_proj (shift f e) a 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, t) -> append (push_appl f a t) c e + | EProj (e, a, d) -> append (push_proj f a 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 i else aux (succ i) tl in + E.name err f a + | 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 -> + let err () = err i in + E.name err f a + | 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 push2 err f lenv ?attr ?t () = match lenv, attr, t with | EBind (e, a, Abst (n, ws)), Some attr, Some t -> f (EBind (e, (attr :: a), Abst (n, t :: ws))) @@ -73,35 +105,6 @@ let push2 err f lenv ?attr ?t () = match lenv, attr, t with f (EBind (e, a, Void (succ n))) | _ -> err () -(* this id not tail recursive *) -let resolve_lref err f id lenv = - let rec aux f i k = function - | ESort -> err () - | EBind (tl, _, Abst (_, [])) - | EBind (tl, _, Abbr []) - | EBind (tl, _, Void 0) -> aux f i k tl - | EBind (tl, a, b) -> - let err kk = aux f (succ i) (k + kk) tl in - let f j = f i j (k + j) in - E.resolve err f id a - | EProj (tl, _, d) -> aux f i k (eshift C.start tl d) - in - aux f 0 0 lenv - -let rec get_name err f i j = function - | ESort -> err i - | EBind (tl, _, Abst (_, [])) - | EBind (tl, _, Abbr []) - | EBind (tl, _, Void 0) -> get_name err f i j tl - | EBind (_, a, _) when i = 0 -> - let err () = err i in - E.get_name err f j a - | EBind (tl, _, _) -> - get_name err f (pred i) j tl - | EProj (tl, _, e) -> - let err i = get_name err f i j tl in - get_name err f i j e - let get_index err f i j lenv = let rec aux f i k = function | ESort -> err i @@ -115,19 +118,26 @@ let get_index err f i j lenv = | EProj (tl, _, d) -> aux f i k (eshift C.start tl d) in aux f i 0 lenv - +*) let rec names_of_lenv ns = function | ESort -> ns | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl + | EAppl (tl, _, _) -> names_of_lenv ns tl | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl -let rec get i = function - | ESort -> ESort, [], Void 0 - | EBind (e, _, Abst (_, [])) - | EBind (e, _, Abbr []) - | EBind (e, _, Void 0) -> get i e +let rec get e i = match e with + | ESort -> ESort, [], Void | EBind (e, a, b) when i = 0 -> e, a, b - | EBind (e, _, _) -> get (pred i) e - | EProj (e, _, d) -> get i (eshift C.start e d) - -let get e i = get i e + | 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 + +let rec fold_attrs f map a0 = function + | ESort -> f a0 + | EBind (e, a, Abst _) -> fold_attrs f map (map a0 a) e + | _ -> assert false diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index 49acbb49b..d5f639b39 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -13,7 +13,6 @@ module P = Printf module U = NUri module C = Cps module L = Log -module H = Hierarchy module E = Entity module N = Level module D = Crg @@ -49,11 +48,11 @@ let initial_counters = { let rec count_term f c e = function | D.TSort _ -> f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} - | D.TLRef (_, i, j) -> + | D.TLRef (_, i) -> begin match D.get e i with - | _, _, D.Abbr vs when j < List.length vs -> + | _, _, 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) -> @@ -67,40 +66,28 @@ let rec count_term f c e = function 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 (_, vs, t) -> - let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in + | D.TAppl (_, v, t) -> + let c = {c with tappls = succ c.tappls} in let f c = count_term f c e t in - C.list_fold_right f (map1 e) vs c - | D.TProj (a, d, t) -> - count_term f c e (D.tshift d t) + count_term f c e v + | D.TProj (_, d, t) -> + D.shift (count_term f c e) d t | D.TBind (a, b, t) -> let f c e = count_term f c e t in count_binder f c e a b -and count_binder f c e a = function - | D.Abst (n, ws) -> - let k = List.length ws in - let c = {c with tabsts = c.tabsts + k; nodes = c.nodes + k} in - let e = D.push_bind C.start e a (D.Abst (n, [])) in - let f (c, e) = f c e in - C.list_fold_right f map2 ws (c, e) - | D.Abbr vs -> - let k = List.length vs in - let c = {c with tabbrs = c.tabbrs + k; xnodes = c.xnodes + k} in - let e = D.push_bind C.start e a (D.Abbr []) in - let f (c, e) = f c e in - C.list_fold_right f map2 vs (c, e) - | D.Void k -> - let c = {c with tvoids = c.tvoids + k; xnodes = c.xnodes + k} in - let e = D.push_bind C.start e a (D.Void k) in - f c e - -and map1 e f t c = count_term f c e t - -and map2 f t (c, e) = - let f c e = f (c, e) in - let f c = D.push2 C.err (f c) e ~t () in - count_term f c e t +and count_binder f c e a 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 + 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 + 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 let count_entity f c = function | _, u, E.Abst (_, w) -> @@ -151,29 +138,22 @@ let pp_attrs out a = let rec pp_term out = function | D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l) - | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j) + | D.TLRef (a, i ) -> pp_attrs out a; out (P.sprintf "#%u" i) | D.TGRef (a, u) -> pp_attrs out a; out (P.sprintf "$") | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y - | D.TProj (a, x, y) -> assert false - | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y - | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y - -and pp_terms bg eg out vs = - let rec aux = function - | [] -> () - | [v] -> pp_term out v - | v :: vs -> pp_term out v; out ", "; aux vs - in - out bg; aux vs; out (eg ^ ".") + | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out x; out ")."; pp_term out y + | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; out "."; pp_term out y + | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out x; out "}."; pp_term out y and pp_bind out = function - | D.Abst (n, x) when N.is_infinite n -> pp_terms "[:" "]" out x - | D.Abst (n, x) -> - pp_terms "[:" (P.sprintf "]^%s" (N.to_string n)) out x - | D.Abbr x -> pp_terms "[=" "]" out x - | D.Void x -> out (P.sprintf "[%u]" x) + | D.Abst (n, x) -> + out "[:"; pp_term out x; out "]"; + if N.is_infinite n then () else out (N.to_string n) + | D.Abbr x -> out "[="; pp_term out x; out "]"; + | D.Void -> out "[]" -let rec pp_lenv out = function +and pp_lenv out = function | D.ESort -> () - | D.EProj (x, a, y) -> assert false | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y + | D.EAppl (x, a, y) -> pp_lenv out x; out "("; pp_term out y; out ")" + | D.EProj (x, a, y) -> pp_lenv out x; out "{"; pp_lenv out y; out "}" diff --git a/helm/software/helena/src/lib/cps.ml b/helm/software/helena/src/lib/cps.ml index f993ffb04..0ce60a8f0 100644 --- a/helm/software/helena/src/lib/cps.ml +++ b/helm/software/helena/src/lib/cps.ml @@ -20,6 +20,10 @@ let rec list_sub_strict f l1 l2 = match l1, l2 with | _ :: tl1, _ :: tl2 -> list_sub_strict f tl1 tl2 | _ -> assert false +let rec list_fold f map a = function + | [] -> f a + | hd :: tl -> list_fold f map (map a hd) tl + (* this is not tail recursive *) let rec list_fold_left f map a = function | [] -> f a diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index ce3853fcb..a6839b89c 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -32,7 +32,7 @@ let henv = Hashtbl.create henv_size (* optimized global environment *) (* Internal functions *******************************************************) let name_of_id ?(r=true) id = E.Name (id, r) - +(* let mk_lref f i j k = f (D.TLRef ([E.Apix k], i, j)) let mk_gref f uri = f (D.TGRef ([], uri)) @@ -151,7 +151,7 @@ let xlate_entity err f gen st = function err st (* Interface functions ******************************************************) - +*) let initial_status () = Hashtbl.clear henv; { path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri () @@ -161,4 +161,4 @@ let refresh_status st = {st with mk_uri = G.get_mk_uri () } -let crg_of_txt = xlate_entity +let crg_of_txt _ _ = assert false (* xlate_entity *) diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index c11614af5..ce14855e0 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -19,33 +19,20 @@ module D = Crg (* internal functions *******************************************************) -let rec list_iter map l out tab = match l with - | [] -> () - | hd :: tl -> map hd out tab; list_iter map tl out tab - -let list_rev_iter map e ns l out tab = - let rec aux err f e = function - | [], [] -> f e - | n :: ns, hd :: tl -> - let f e = -(* - pp_lenv print_string e; print_string " |- "; - pp_term print_string hd; print_newline (); -*) - map e hd out tab; f (D.push2 C.err C.start e ~attr:n ~t:hd ()) - in - aux err f e (ns, tl) - | _ -> err () +let lenv_iter map_bind map_appl map_proj e lenv out tab = + let rec aux = function + | D.ESort -> e + | D.EBind (e, a, b) -> + let e = aux e in + map_bind e a b out tab; D.EBind (e, a, b) + | D.EAppl (e, a, v) -> + let e = aux e in + map_appl e a v out tab; D.EAppl (e, a, v) + | D.EProj (e, a, d) -> + let e = aux e in + map_proj e a d out tab; D.EProj (e, a, d) in - ignore (aux C.err C.start e (ns, l)) - -let lenv_iter map1 map2 l out tab = - let rec aux f = function - | D.ESort -> f () - | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv - | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv - in - aux C.start l + ignore (aux lenv) let rec exp_term e t out tab = match t with | D.TSort (a, l) -> @@ -56,13 +43,13 @@ let rec exp_term e t out tab = match t with in let attrs = [XL.position l; XL.name a] in XL.tag XL.sort attrs out tab - | D.TLRef (a, i, j) -> + | D.TLRef (a, i) -> let a = let err _ = a in let f n r = Y.Name (n, r) :: a in - D.get_name err f i j e + D.get_name err f i e in - let attrs = [XL.position i; XL.offset j; XL.name a] in + let attrs = [XL.position i; XL.name a] in XL.tag XL.lref attrs out tab | D.TGRef (a, n) -> let a = Y.Name (U.name_of_uri n, true) :: a in @@ -72,39 +59,38 @@ let rec exp_term e t out tab = match t with let attrs = [] in XL.tag XL.cast attrs ~contents:(exp_term e u) out tab; exp_term e t out tab - | D.TAppl (a, vs, t) -> - let attrs = [XL.arity vs] in - XL.tag XL.appl attrs ~contents:(list_iter (exp_term e) vs) out tab; + | D.TAppl (a, v, t) -> + let attrs = [] in + XL.tag XL.appl attrs ~contents:(exp_term e v) out tab; exp_term e t out tab | D.TProj (a, lenv, t) -> let attrs = [] in - XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab; - exp_term (D.push_proj C.start e a lenv) t out tab + XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab; + exp_term (D.push_proj C.start a lenv e) t out tab | D.TBind (a, b, t) -> (* NOTE: the inner binders are alpha-converted first *) let a = R.alpha (D.names_of_lenv [] e) a in exp_bind e a b out tab; - exp_term (D.push_bind C.start e a b) t out tab + exp_term (D.push_bind C.start a b e) t out tab + +and exp_appl e a v out tab = + let attrs = [] in + XL.tag XL.appl attrs ~contents:(exp_term e v) out tab; -and exp_bind e a b out tab = - let f a ns = a, ns in - let a, ns = Y.get_names f a in - match b with - | D.Abst (n, ws) -> - let e = D.push_bind C.start e a (D.Abst (n, [])) in - let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in - XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab - | D.Abbr vs -> - let e = D.push_bind C.start e a (D.Abbr []) in - let attrs = [XL.name ns; XL.mark a; XL.arity vs] in - XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab - | D.Void n -> - let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in - XL.tag XL.void attrs out tab +and exp_bind e a b out tab = match b with + | D.Abst (n, w) -> + let attrs = [XL.level n; XL.name a; XL.mark a] in + XL.tag XL.abst attrs ~contents:(exp_term e w) out tab + | D.Abbr v -> + let attrs = [XL.name a] in + XL.tag XL.abbr attrs ~contents:(exp_term e v) out tab + | D.Void -> + let attrs = [XL.name a] in + XL.tag XL.void attrs out tab -and exp_eproj e a lenv out tab = +and exp_proj e a lenv out tab = let attrs = [] in - XL.tag XL.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab + XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab (* interface functions ******************************************************) diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index a7f5ae29a..e182ab9a3 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -92,21 +92,9 @@ let void = "Void" let position i = "position", string_of_int i -let offset j = - let contents = if j > 0 then string_of_int j else "" in - "offset", contents - let uri u = "uri", U.string_of_uri u -let arity ?n l = - let n = match n with - | None -> List.length l - | Some n -> n - in - let contents = if n > 1 then string_of_int n else "" in - "arity", contents - let name a = let map f i n r s = let n = if r then n else "-" ^ n in @@ -140,6 +128,9 @@ let meta a = let f ms = "meta", String.concat " " (List.rev_map map ms) in E.meta err f a +let arity l = + "arity", string_of_int (List.length l) + (* TODO: the string tx must be quoted *) let info a = let err () = ["lang", ""; "info", ""] in diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index 7b3a476c3..9db373c47 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -41,12 +41,8 @@ val void: string val position: int -> attr -val offset: int -> attr - val uri: Entity.uri -> attr -val arity: ?n:int -> 'a list -> attr - val level: Level.level -> attr val name: Entity.attrs -> attr -- 2.39.2