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
(* 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
| 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 =
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
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
| 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;
*)
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;
*)
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
(* 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 **************************************)
| 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) ->
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
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) ->
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 ******************************************************)
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
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
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)))
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
| 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
module U = NUri
module C = Cps
module L = Log
-module H = Hierarchy
module E = Entity
module N = Level
module D = Crg
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) ->
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) ->
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 "}"
| _ :: 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
(* 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))
err st
(* Interface functions ******************************************************)
-
+*)
let initial_status () =
Hashtbl.clear henv; {
path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
mk_uri = G.get_mk_uri ()
}
-let crg_of_txt = xlate_entity
+let crg_of_txt _ _ = assert false (* xlate_entity *)
(* 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) ->
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
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 ******************************************************)
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
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
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
projects / helm.git / commitdiff