src/common/output.cmi
src/common/output.cmx: src/common/options.cmx src/lib/log.cmx \
src/common/output.cmi
-src/common/marks.cmo: src/common/entity.cmx
-src/common/marks.cmx: src/common/entity.cmx
+src/common/marks.cmi: src/common/entity.cmx
+src/common/marks.cmo: src/common/entity.cmx src/common/marks.cmi
+src/common/marks.cmx: src/common/entity.cmx src/common/marks.cmi
src/common/alpha.cmi: src/common/entity.cmx
src/common/alpha.cmo: src/common/entity.cmx src/common/alpha.cmi
src/common/alpha.cmx: src/common/entity.cmx src/common/alpha.cmi
src/lib/cps.cmx src/common/ccs.cmi
src/common/status.cmo: src/common/options.cmx src/common/ccs.cmi
src/common/status.cmx: src/common/options.cmx src/common/ccs.cmx
-src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx
-src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx
+src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx \
+ src/lib/cps.cmx
+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/basic_rg/brg.cmo: src/common/level.cmi src/common/entity.cmx
src/basic_rg/brg.cmx: src/common/level.cmx src/common/entity.cmx
src/basic_rg/brgCrg.cmi: src/complete_rg/crg.cmx src/basic_rg/brg.cmx
-src/basic_rg/brgCrg.cmo: src/common/marks.cmx src/common/level.cmi \
+src/basic_rg/brgCrg.cmo: src/common/marks.cmi src/common/level.cmi \
src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
src/basic_rg/brg.cmx src/basic_rg/brgCrg.cmi
src/basic_rg/brgCrg.cmx: src/common/marks.cmx src/common/level.cmx \
src/basic_rg/brgUntrusted.cmi
src/basic_ag/bag.cmo: src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx
src/basic_ag/bag.cmx: src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx
-src/basic_ag/bagOutput.cmi: src/lib/log.cmi src/basic_ag/bag.cmx
-src/basic_ag/bagOutput.cmo: src/common/options.cmx src/lib/log.cmi \
- src/common/hierarchy.cmi src/common/entity.cmx src/basic_ag/bag.cmx \
+src/basic_ag/bagCrg.cmi: src/complete_rg/crg.cmx src/basic_ag/bag.cmx
+src/basic_ag/bagCrg.cmo: src/common/marks.cmi src/common/level.cmi \
+ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi
+src/basic_ag/bagCrg.cmx: src/common/marks.cmx src/common/level.cmx \
+ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
+ src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi
+src/basic_ag/bagOutput.cmi: src/xml/xmlLibrary.cmi src/lib/log.cmi \
+ src/basic_ag/bag.cmx
+src/basic_ag/bagOutput.cmo: src/xml/xmlCrg.cmi src/common/options.cmx \
+ src/common/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \
+ src/common/entity.cmx src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \
src/basic_ag/bagOutput.cmi
-src/basic_ag/bagOutput.cmx: src/common/options.cmx src/lib/log.cmx \
- src/common/hierarchy.cmx src/common/entity.cmx src/basic_ag/bag.cmx \
+src/basic_ag/bagOutput.cmx: src/xml/xmlCrg.cmx src/common/options.cmx \
+ src/common/marks.cmx src/lib/log.cmx src/common/hierarchy.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/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \
src/basic_ag/bagSubstitution.cmi
src/basic_ag/bagReduction.cmi: src/basic_ag/bag.cmx
-src/basic_ag/bagReduction.cmo: src/lib/log.cmi src/common/entity.cmx \
- src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \
+src/basic_ag/bagReduction.cmo: src/common/marks.cmi src/lib/log.cmi \
+ src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \
src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \
src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi
-src/basic_ag/bagReduction.cmx: src/lib/log.cmx src/common/entity.cmx \
- src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \
+src/basic_ag/bagReduction.cmx: src/common/marks.cmx src/lib/log.cmx \
+ src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \
src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \
src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi
src/basic_ag/bagType.cmi: src/common/status.cmx src/basic_ag/bag.cmx
src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \
- src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \
+ src/basic_ag/bagOutput.cmi src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \
src/automath/autProcess.cmi src/automath/autParser.cmi \
src/automath/autOutput.cmi src/automath/autLexer.cmx \
src/automath/autCrg.cmi src/automath/aut.cmx
src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \
- src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \
+ src/basic_ag/bagOutput.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \
src/automath/autProcess.cmx src/automath/autParser.cmx \
src/automath/autOutput.cmx src/automath/autLexer.cmx \
src/automath/autCrg.cmx src/automath/aut.cmx
CLEAN = etc/log.txt etc/profile.txt
-TAGS = test-si test-si-fast xml-si-crg xml-si profile
+TAGS = test-si test-si-fast profile xml-si xml-si-crg html test-html \
+ install-html install-lddl install-dtd install-xml
-XMLLINTLOCAL = --nonet --path xml --dtdvalid ld.dtd
XMLS = xml/brg-si/grundlagen/l/not.ld.xml \
xml/brg-si/grundlagen/l/et.ld.xml \
xml/crg-si/grundlagen/l/not.ld.xml \
xml/crg-si/grundlagen/l/et.ld.xml \
xml/crg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
- xml/crg-si/grundlagen/l/e/pairis1.ld.xml
-
-LOCALXMLS = xml/brg-si/grundlagen/ccs.ldc.xml
+ xml/crg-si/grundlagen/l/e/pairis1.ld.xml \
+ xml/brg-si/grundlagen/ccs.ldc.xml
include Makefile.common
OCAMLLEX = ocamllex.opt
OCAMLYACC = ocamlyacc -v
XMLLINT = xmllint --noout
-
-
XSLT = xsltproc
-#TAR = tar -czf etc/$(MAIN:%=%.tgz)
+TAR = tar -czf etc/$(MAIN:%=%.tgz)
define DIR_TEMPLATE
MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make))
@echo XMLLINT --valid
$(H)$(XMLLINT) --valid $^
-lint-xml-local: $(LOCALXMLS)
- @echo XMLLINT --valid
- $(H)$(XMLLINT) $(XMLLINTLOCAL) --valid $^
-
-#tgz: clean
-# @echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)"
-# $(H)find -name "Make*" | xargs $(TAR) $(KEEP)
+tgz: clean
+ @echo " TAR -czf $(MAIN:%=%.tgz) . $(DIRECTORIES)"
+ $(H)find -name "Make*" | xargs $(TAR) $(KEEP)
%.ml %.mli: %.mly
@echo " OCAMLYACC $<"
-bag bagOutput
+bag bagCrg bagOutput
bagEnvironment bagSubstitution bagReduction bagType bagUntrusted
module E = Entity
type uri = E.uri
-type id = E.id
+type attrs = E.attrs
type bind = Void (* exclusion *)
| Abst of term (* abstraction *)
| Abbr of term (* abbreviation *)
-and term = Sort of int (* hierarchy index *)
- | LRef of int (* location *)
- | GRef of uri (* reference *)
- | Cast of term * term (* domain, element *)
- | Appl of term * term (* argument, function *)
- | Bind of int * id * bind * term (* location, name, binder, scope *)
+and term = Sort of int (* hierarchy index *)
+ | LRef of int (* location *)
+ | GRef of uri (* reference *)
+ | Cast of term * term (* domain, element *)
+ | Appl of term * term (* argument, function *)
+ | Bind of attrs * int * bind * term (* name, location, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
-type lenv = (int * id * bind) list (* location, name, binder *)
+type lenv = (attrs * int * bind) list (* location, name, binder *)
type message = (lenv, term) Log.item list
let appl u t = Appl (u, t)
-let bind l id b t = Bind (l, id, b, t)
+let bind a l b t = Bind (a, l, b, t)
-let bind_abst l id u t = Bind (l, id, Abst u, t)
+let bind_abst a l u t = Bind (a, l, Abst u, t)
-let bind_abbr l id v t = Bind (l, id, Abbr v, t)
-
-(* location handling functions **********************************************)
-
-let location = ref 0
-
-let new_location () = let loc = !location in incr location; loc
-
-let locations () = !location
+let bind_abbr a l v t = Bind (a, l, Abbr v, t)
(* local environment handling functions *************************************)
let empty_lenv = []
-let push msg f es l id b =
+let push msg f es a l b =
let rec does_not_occur loc = function
| [] -> true
- | (l, _, _) :: _ when l = loc -> false
+ | (_, 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 = (l, id, b) :: es in f c
+ let c = (a, l, b) :: es in f c
let append f es1 es2 =
f (List.append es2 es1)
let contents f es = f es
-let get f es i =
+let get err f es i =
let rec aux = function
- | [] -> f None
- | (l, id, b) :: tl -> if l = i then f (Some (id, b)) else aux tl
+ | [] -> err ()
+ | (a, l, b) :: tl -> if l = i then f a b else aux tl
in
aux es
+
+let nth err f loc e =
+ let rec aux n = function
+ | [] -> err loc
+ | (_, l, _) :: _ when l = loc -> f n
+ | _ :: e -> aux (succ n) e
+ in
+ aux 0 e
(* internal functions: crg to bag term **************************************)
-let rec lenv_fold_left map1 map2 x = function
- | D.ESort -> x
- | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
- | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
+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 f = function
- | D.TSort (a, l) -> f (Z.Sort (a, l))
- | D.TGRef (a, n) -> f (Z.GRef (a, n))
- | D.TLRef (a, _, _) -> let f i = f (Z.LRef (a, i)) in E.apix C.err f a
- | D.TCast (a, u, t) ->
- let f uu tt = f (Z.Cast (a, uu, tt)) in
- let f uu = xlate_term (f uu) t in
- xlate_term f u
- | D.TAppl (a, vs, t) ->
- let map f v tt = let f vv = f (Z.Appl (a, vv, tt)) in xlate_term f v in
+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 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 f t
- | D.TProj (a, e, t) ->
- let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
- xlate_term f t
+ xlate_term xlate_bind f c t
+ | D.TProj (_, e, t) ->
+ xlate_term xlate_bind f c (D.tshift e t)
| D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
- xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst (N.pred n, ws), u), D.TBind (ab, D.Abst (n, ws), 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 f tt = f (xlate_bind tt a b) in xlate_term f 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
-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 = Z.Bind (n :: J.new_mark () :: a, Z.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 = Z.Bind (n :: a, Z.Abbr vv, x) in
- xlate_term f v
- in
- List.fold_left2 map x ns vs
- | D.Void _ ->
- let map x n = Z.Bind (n :: a, Z.Void, x) in
- List.fold_left map x ns
-
-and xlate_proj x _ e =
- lenv_fold_left xlate_bind xlate_proj x e
+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
+ 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
(* internal functions: bag to crg term **************************************)
-let rec xlate_bk_term f = function
- | Z.Sort (a, l) -> f (D.TSort (a, l))
- | Z.GRef (a, n) -> f (D.TGRef (a, n))
- | Z.LRef (a, i) -> f (D.TLRef (a, i, 0))
- | Z.Cast (a, u, t) ->
- let f uu tt = f (D.TCast (a, uu, tt)) in
- let f uu = xlate_bk_term (f uu) t in
- xlate_bk_term f u
- | Z.Appl (a, u, t) ->
- let f uu tt = f (D.TAppl (a, [uu], tt)) in
- let f uu = xlate_bk_term (f uu) t in
- xlate_bk_term f u
- | Z.Bind (a, b, t) ->
- let f bb tt = f (D.TBind (a, bb, tt)) in
- let f bb = xlate_bk_term (f bb) t in
- xlate_bk_bind f b
+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
+ 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 = 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
+ 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
+ xlate_bk_term f cc t
-and xlate_bk_bind f = function
- | Z.Abst (n, t) ->
- let f tt = f (D.Abst (n, [tt])) in
- xlate_bk_term f t
- | Z.Abbr t ->
+and xlate_bk_bind f c = function
+ | Z.Abst t ->
+ 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
- xlate_bk_term f t
- | Z.Void -> f (D.Void 1)
-
+ xlate_bk_term f c t
+ | Z.Void -> f (D.Void 1)
+
(* interface functions ******************************************************)
let bag_of_crg f t =
- f (xlate_term C.start t)
+ xlate_term xlate_bind f Z.empty_lenv t
-let crg_of_bag = xlate_bk_term
+let crg_of_bag f t = xlate_bk_term f Z.empty_lenv t
V_______________________________________________________________ *)
val bag_of_crg: (Bag.term -> 'a) -> Crg.term -> 'a
-(*
+
val crg_of_bag: (Crg.term -> 'a) -> Bag.term -> 'a
-*)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module P = Printf
-module F = Format
-module U = NUri
-module L = Log
-module G = Options
-module E = Entity
-module H = Hierarchy
-module Z = Bag
+module P = Printf
+module F = Format
+module U = NUri
+module L = Log
+module G = Options
+module E = Entity
+module J = Marks
+module H = Hierarchy
+module XD = XmlCrg
+module Z = Bag
+module ZD = BagCrg
type counters = {
eabsts: int;
c.tabbrs
in
let items = c.eabsts + c.eabbrs in
- let locations = Z.locations () in
+ let locations = J.locations () in
L.warn (P.sprintf " Kernel representation summary (basic_ag)");
L.warn (P.sprintf " Total entry items: %7u" items);
L.warn (P.sprintf " Declaration items: %7u" c.eabsts);
L.warn (P.sprintf " Total binder locations: %7u" locations);
f ()
-let res l id =
- if !G.indexes then P.sprintf "#%u" l else id
+let name err frm a =
+ let f n = function
+ | true -> F.fprintf frm "%s" n
+ | false -> F.fprintf frm "-%s" n
+ in
+ E.name err f a
+
+let res a l frm =
+ let err () = F.fprintf frm "@[#%u@]" l in
+ if !G.indexes then err () else name err frm a
let rec pp_term c frm = function
| Z.Sort h ->
let f s = F.fprintf frm "@[%s@]" s in
H.string_of_sort err f h
| Z.LRef i ->
- let f = function
- | Some (id, _) -> F.fprintf frm "@[%s@]" id
- | None -> F.fprintf frm "@[#%u@]" i
- in
- if !G.indexes then f None else Z.get f c i
+ let err () = F.fprintf frm "@[#%u@]" i in
+ let f a _ = name err frm a in
+ if !G.indexes then err () else Z.get err f c i
| Z.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
| Z.Cast (u, t) ->
F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
| Z.Appl (v, t) ->
F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
- | Z.Bind (l, id, Z.Abst w, t) ->
+ | Z.Bind (a, l, Z.Abst w, t) ->
let f cc =
- F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t
+ F.fprintf frm "@[[%t:%a].%a@]" (res a l) (pp_term c) w (pp_term cc) t
in
- Z.push "output abst" f c l id (Z.Abst w)
- | Z.Bind (l, id, Z.Abbr v, t) ->
+ Z.push "output abst" f c a l (Z.Abst w)
+ | Z.Bind (a, l, Z.Abbr v, t) ->
let f cc =
- F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t
+ F.fprintf frm "@[[%t=%a].%a@]" (res a l) (pp_term c) v (pp_term cc) t
in
- Z.push "output abbr" f c l id (Z.Abbr v)
- | Z.Bind (l, id, Z.Void, t) ->
- let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in
- Z.push "output void" f c l id Z.Void
+ Z.push "output abbr" f c a l (Z.Abbr v)
+ | Z.Bind (a, l, Z.Void, t) ->
+ let f cc = F.fprintf frm "@[[%t].%a@]" (res a l) (pp_term cc) t in
+ Z.push "output void" f c a l Z.Void
let pp_lenv frm c =
let pp_entry frm = function
- | l, id, Z.Abst w ->
- F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w
- | l, id, Z.Abbr v ->
- F.fprintf frm "@,@[%s = %a@]" (res l id) (pp_term c) v
- | l, id, Z.Void ->
- F.fprintf frm "@,%s" (res l id)
+ | a, l, Z.Abst w ->
+ F.fprintf frm "@,@[%t : %a@]" (res a l) (pp_term c) w
+ | a, l, Z.Abbr v ->
+ F.fprintf frm "@,@[%t = %a@]" (res a l) (pp_term c) v
+ | a, l, Z.Void ->
+ F.fprintf frm "@,%t" (res a l)
in
let iter map frm l = List.iter (map frm) l in
let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in
let specs = {
L.pp_term = pp_term; L.pp_lenv = pp_lenv
}
+
+(* term xml printing ********************************************************)
+
+let export_term =
+ ZD.crg_of_bag XD.export_term
val print_counters: (unit -> 'a) -> counters -> 'a
val specs: (Bag.lenv, Bag.term) Log.specs
+
+val export_term: Bag.term -> XmlLibrary.pp
module C = Cps
module L = Log
module E = Entity
+module J = Marks
module Z = Bag
module ZO = BagOutput
module ZE = BagEnvironment
| Sort_ of int
| LRef_ of int * Z.term option
| GRef_ of Z.entity
- | Bind_ of int * Z.id * Z.term * Z.term
+ | Bind_ of Z.attrs * int * Z.term * Z.term
type ho_whd_result =
| Sort of int
| Sort_ h -> Z.Sort h
| LRef_ (i, _) -> Z.LRef i
| GRef_ (_, uri, _) -> Z.GRef uri
- | Bind_ (l, id, w, t) -> Z.bind_abst l id w t
+ | Bind_ (a, l, w, t) -> Z.bind_abst a l w t
let level = 5
let inc m = {m with i = succ m.i}
let unwind_to_term f m t =
- let map f t (l, id, b) = f (Z.Bind (l, id, b, t)) in
+ let map f t (a, l, b) = f (Z.Bind (a, l, b, t)) in
let f mc = C.list_fold_left f map t mc in
Z.contents f m.c
C.list_map f map m.s
let get f c m i =
- let f = function
- | Some (_, b) -> f b
- | None -> assert false
- in
- let f c = Z.get f c i in
+ let f _ b = f b in
+ let f c = Z.get C.err f c i in
Z.append f c m.c
-let push msg f c m l id w =
+let push msg f c m a l w =
assert (m.s = []);
- let f w = Z.push msg f c l id (Z.Abst w) in
+ let f w = Z.push msg f c a l (Z.Abst w) in
unwind_to_term f m w
(* to share *)
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 (l, id, Z.Abst w, t) ->
+ | Z.Bind (a, l, Z.Abst w, t) ->
begin match m.s with
- | [] -> f m (Bind_ (l, id, w, t))
+ | [] -> f m (Bind_ (a, l, w, t))
| v :: tl ->
- let nl = Z.new_location () in
+ let nl = J.new_location () in
let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
- Z.push "!" f m.c nl id (Z.Abbr (Z.Cast (w, v)))
+ Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
end
- | Z.Bind (l, id, b, t) ->
- let nl = Z.new_location () in
+ | Z.Bind (a, l, b, t) ->
+ let nl = J.new_location () in
let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
- Z.push "!" f m.c nl id b
+ Z.push "!" f m.c a nl b
(* Interface functions ******************************************************)
whd (aux m1 r1) c m2 v2
| GRef_ (_, _, E.Abbr v1), _ ->
whd (aux_rev m2 r2) c m1 v1
- | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) ->
- let l = Z.new_location () in
+ | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) ->
+ let l = J.new_location () in
let h c =
let m1, m2 = inc m1, inc m2 in
let f t1 = ZS.subst (are_convertible f ~si 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 l id1 w1 else f false in
+ let f r = if r then push "!" h c m1 a1 l w1 else f false in
are_convertible f ~si a c m1 w1 m2 w2
(* we detect the AUT-QE reduction rule for type/prop inclusion *)
- | Sort_ _, Bind_ (l2, id2, w2, t2) when si ->
+ | Sort_ _, Bind_ (a2, l2, w2, t2) when si ->
let m1, m2 = inc m1, inc m2 in
let f c = are_convertible f ~si a c m1 (term_of_whdr r1) m2 t2 in
- push "nsi" f c m2 l2 id2 w2
+ push "nsi" f c m2 a2 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
let f w' u' = f (W.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 (l, id, b, u) ->
- let f b' u' = f (W.sh2 b b' u u' t (Z.bind l id)) in
+ | Z.Bind (a, l, b, u) ->
+ let f b' u' = f (W.sh2 b b' u u' t (Z.bind a l)) in
let f b' = lref_map (f b') map u in
lref_map_bind f map b
| Z.Sort h ->
let h = H.apply h in f x (Z.Sort h)
| Z.LRef i ->
- let f = function
- | Some (_, Z.Abst w) -> f x w
- | Some (_, Z.Abbr (Z.Cast (w, v))) -> f x w
- | Some (_, Z.Abbr _) -> assert false
- | Some (_, Z.Void) ->
- error1 "reference to excluded variable" c x
- | None ->
- error1 "variable not found" c x
+ let err () = error1 "variable not found" c x in
+ let f _ = function
+ | Z.Abst w -> f x w
+ | Z.Abbr (Z.Cast (w, v)) -> f x w
+ | Z.Abbr _ -> assert false
+ | Z.Void -> error1 "reference to excluded variable" c x
in
- Z.get f c i
+ Z.get err f c i
| Z.GRef uri ->
let f = function
| _, _, E.Abst (_, w) -> f x w
| _, _, E.Void -> assert false
in
ZE.get_entity f uri
- | Z.Bind (l, id, Z.Abbr v, t) ->
+ | Z.Bind (a, l, Z.Abbr v, t) ->
let f xv xt tt =
- f (W.sh2 v xv t xt x (Z.bind_abbr l id)) (Z.bind_abbr l id xv tt)
+ f (W.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt)
in
let f xv cc = b_type_of (f xv) st cc t in
- let f xv = Z.push "type abbr" (f xv) c l id (Z.Abbr xv) in
+ let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in
let f xv vv = match xv with
| Z.Cast _ -> f xv
| _ -> f (Z.Cast (vv, xv))
in
type_of f st c v
- | Z.Bind (l, id, Z.Abst u, t) ->
+ | Z.Bind (a, l, Z.Abst u, t) ->
let f xu xt tt =
- f (W.sh2 u xu t xt x (Z.bind_abst l id)) (Z.bind_abst l id xu tt)
+ f (W.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt)
in
let f xu cc = b_type_of (f xu) st cc t in
- let f xu _ = Z.push "type abst" (f xu) c l id (Z.Abst xu) in
+ let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in
type_of f st c u
- | Z.Bind (l, id, Z.Void, t) ->
+ | Z.Bind (a, l, Z.Void, t) ->
let f xt tt =
- f (W.sh1 t xt x (Z.bind l id Z.Void)) (Z.bind l id Z.Void tt)
+ f (W.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt)
in
let f cc = b_type_of f st cc t in
- Z.push "type void" f c l id Z.Void
+ Z.push "type void" f c a l Z.Void
| Z.Appl (v, t) ->
let f xv vv xt tt = function
| ZR.Abst w ->
module N = Level
type uri = E.uri
-type id = E.id
type attrs = E.attrs
type bind = Void (* *)
let rec fold_right f map e x = match e with
| Null -> f x
| Cons (e, c, a, b) -> fold_right (map f e c a b) map e x
-
-(* used in MetaBrg.unwind_to_xlate_term *)
-let rec fold_left map x = function
- | Null -> x
- | Cons (e, _, a, b) -> fold_left map (map x a b) e
(* internal functions: crg to brg term **************************************)
-let rec lenv_fold_left map1 map2 x = function
- | D.ESort -> x
- | D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
- | D.EProj (tl, a, e) -> lenv_fold_left map1 map2 (map2 x a e) tl
-
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.TCast (a, u, t) ->
- let f uu tt = f (B.Cast (a, uu, tt)) in
- let f uu = xlate_term (f uu) t in
- xlate_term f u
+ 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.TProj (a, e, t) ->
- let f tt = f (lenv_fold_left xlate_bind xlate_proj tt e) in
- xlate_term f t
+ | D.TProj (_, e, t) ->
+ xlate_term f (D.tshift e t)
| D.TBind (ab, D.Abst (n, ws), D.TCast (ac, u, t)) ->
xlate_term f (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 map x n = B.Bind (n :: a, B.Void, x) in
List.fold_left map x ns
-and xlate_proj x _ e =
- lenv_fold_left xlate_bind xlate_proj x e
-
(* internal functions: brg to crg term **************************************)
let rec xlate_bk_term f = function
| B.GRef (a, n) -> f (D.TGRef (a, n))
| B.LRef (a, i) -> f (D.TLRef (a, i, 0))
| B.Cast (a, u, t) ->
- let f uu tt = f (D.TCast (a, uu, tt)) in
- let f uu = xlate_bk_term (f uu) t in
- xlate_bk_term f u
+ 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 uu tt = f (D.TAppl (a, [uu], tt)) in
- let f uu = xlate_bk_term (f uu) t in
- xlate_bk_term f u
+ 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) ->
- let f bb tt = f (D.TBind (a, bb, tt)) in
- let f bb = xlate_bk_term (f bb) t in
- xlate_bk_bind f b
+ let f tt bb = f (D.TBind (a, bb, tt)) in
+ let f tt = xlate_bk_bind (f tt) b in
+ xlate_bk_term f t
and xlate_bk_bind f = function
| B.Abst (n, t) ->
(* interface functions ******************************************************)
-let brg_of_crg f t =
- f (xlate_term C.start t)
+let brg_of_crg f t = f (xlate_term C.start t)
let crg_of_brg = xlate_bk_term
val specs: (Brg.lenv, Brg.term) Log.specs
val export_term: Brg.term -> XmlLibrary.pp
-(*
-val export_term: Format.formatter -> Brg.term -> unit
-*)
module E = Entity
+let location = ref 0
+
(* interface functions ******************************************************)
-let new_location =
- let location = ref 0 in
- fun () -> incr location; !location
+let locations () = !location
+
+let new_location () =
+ incr location; !location
let new_mark () =
E.Mark (new_location ())
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+val locations: unit -> int
+
+val new_location: unit -> int
+
+val new_mark: unit -> Entity.attr
(* kernel version: complete, relative, global *)
(* note : fragment of complete lambda-delta serving as abstract layer *)
+module C = Cps
module E = Entity
module N = Level
(* 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 tshift c t = tshift t c
+
+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 empty_lenv = ESort
let push_bind f lenv a b = f (EBind (lenv, 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 _ -> assert false (* TODO *)
+ | EProj (tl, _, d) -> aux f i k (eshift C.start tl d)
in
aux f 0 0 lenv
if E.count_names a > j then f (k + j) else err i
| EBind (tl, a, _) ->
aux f (pred i) (k + E.count_names a) tl
- | EProj _ -> assert false (* TODO *)
+ | EProj (tl, _, d) -> aux f i k (eshift C.start tl d)
in
aux f i 0 lenv
| EBind (e, _, Void 0) -> get i e
| EBind (e, a, b) when i = 0 -> e, a, b
| EBind (e, _, _) -> get (pred i) e
- | EProj _ -> assert false (* TODO *)
+ | EProj (e, _, d) -> get i (eshift C.start e d)
let get e i = get i e
uris = []; nodes = 0; xnodes = 0
}
-let rec shift t = function
- | D.ESort -> t
- | D.EBind (e, a, b) -> shift (D.TBind (a, b, t)) e
- | D.EProj (e, a, d) -> shift (D.TProj (a, d, t)) e
-
let rec count_term f c e = function
| D.TSort _ ->
f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
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 (shift t d)
+ count_term f c e (D.tshift 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
| [] -> f a
| hd :: tl -> list_fold_right (map f hd) map tl a
+let rec list_fold_right2 f map l1 l2 a = match l1, l2 with
+ | [], [] -> f a
+ | hd1 :: tl1, hd2 :: tl2 -> list_fold_right2 (map f hd1 hd2) map tl1 tl2 a
+ | _ -> failwith "Cps.list_fold_right2"
+
let list_map f map l =
let map f hd a =
let f hd = f (hd :: a) in map f hd
module BO = BrgOutput
module BR = BrgReduction
module BU = BrgUntrusted
+module ZD = BagCrg
module ZO = BagOutput
module ZT = BagType
module ZU = BagUntrusted
let xlate_entity entity = match !G.kernel, entity with
| G.Brg, CrgEntity e ->
let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e
+ | G.Bag, CrgEntity e ->
+ let f e = (BagEntity e) in E.xlate f ZD.bag_of_crg e
| _, entity -> entity
let pp_progress e =
let export_entity = function
| CrgEntity e -> XL.export_entity XD.export_term e
| BrgEntity e -> XL.export_entity BO.export_term e
- | BagEntity _ -> ()
+ | BagEntity e -> XL.export_entity ZO.export_term e
let type_check st k =
let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
<!ELEMENT Abst %terms;>
<!ATTLIST Abst
- name NMTOKENS #IMPLIED
+ level NMTOKEN #IMPLIED
+ name NMTOKENS #IMPLIED
arity NMTOKEN #IMPLIED
mark NMTOKEN #IMPLIED
meta CDATA #IMPLIED
<!ELEMENT ABST %term;>
<!ATTLIST ABST
- uri CDATA #REQUIRED
- name NMTOKEN #IMPLIED
- mark NMTOKEN #IMPLIED
- meta CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ level NMTOKEN #IMPLIED
+ name NMTOKEN #IMPLIED
+ mark NMTOKEN #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT ABBR %term;>
projects / helm.git / commitdiff