- matita/Makefile: we removed LAMBDA-TYPES from the nightly tests (too slow ???)
-lib/nUri.cmi:
lib/nUri.cmo: lib/nUri.cmi
lib/nUri.cmx: lib/nUri.cmi
-lib/cps.cmo:
-lib/cps.cmx:
-lib/share.cmo:
-lib/share.cmx:
-lib/log.cmi:
lib/log.cmo: lib/cps.cmx lib/log.cmi
lib/log.cmx: lib/cps.cmx lib/log.cmi
lib/time.cmo: lib/log.cmi
lib/time.cmx: lib/log.cmx
-automath/aut.cmo:
-automath/aut.cmx:
automath/autProcess.cmi: automath/aut.cmx
automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi
automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi
automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi
automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi
automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx
-common/hierarchy.cmi:
common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi
common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi
-common/output.cmi:
common/output.cmo: lib/log.cmi common/output.cmi
common/output.cmx: lib/log.cmx common/output.cmi
common/entity.cmo: lib/nUri.cmi automath/aut.cmx
(* helpers ******************************************************************)
+let common f (a, u, _) = f a u
+
let rec name err f = function
| Name (n, r) :: _ -> f n r
| _ :: tl -> name err f tl
| ESort -> err ()
| EBind (tl, a, _) ->
let err kk = aux f (succ i) (k + kk) tl in
- let f j = f i j k in
+ let f j = f i j (k + j) in
Entity.resolve err f id a
| EProj _ -> assert false (* TODO *)
in
let rec get_name err f i j = function
| ESort -> err i
+ | EBind (tl, a, Abst []) -> get_name err f i j tl
+ | EBind (tl, a, Abbr []) -> get_name err f i j tl
+ | EBind (tl, a, Void 0) -> get_name err f i j tl
| EBind (_, a, _) when i = 0 ->
let err () = err i in
Entity.get_name err f j a
let map2 f = xlate_term f st lenv in
let g qid (a, _) =
let gref = D.TGRef ([], uri_of_qid qid) in
- match args with
- | [] -> f gref
- | args ->
+ match args, a with
+ | [], [] -> f gref
+ | _ ->
let f args = f (D.TAppl ([], args, gref)) in
let f args = f (List.rev_map (map2 C.start) args) in
let f a = C.list_rev_map_append f map1 a ~tail:args in
let f qid =
let ww = xlate_term C.start st lenv w in
H.add henv (uri_of_qid qid) cnt;
- let b = Y.Abst (D.TBind (a, D.Abst ws, ww)) in
+ let t = match ws with
+ | [] -> ww
+ | _ -> D.TBind (a, D.Abst ws, ww)
+ in
+(*
+ DrgOutput.pp_term print_string t; print_newline ();
+*)
+ let b = Y.Abst t in
let entity = [Y.Mark st.line], uri_of_qid qid, b in
f {st with line = succ st.line} entity
in
let ww = xlate_term C.start st lenv w in
let vv = xlate_term C.start st lenv v in
H.add henv (uri_of_qid qid) cnt;
- let b = Y.Abbr (D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))) in
+ let t = match ws with
+ | [] -> D.TCast ([], ww, vv)
+ | _ -> D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))
+ in
+(*
+ Printf.printf "%s\n" (U.string_of_uri (uri_of_qid qid));
+*)
+ let b = Y.Abbr t in
let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in
let entity = a, uri_of_qid qid, b in
f {st with line = succ st.line} entity
| 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 t
+ xlate_term f u
| 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 (ap, e, D.TCast (ac, u, t)) ->
- xlate_term f (D.TCast (ac, D.TProj (ap, e, u), D.TProj (ap, e, 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.TBind (ab, D.Abst ws, D.TCast (ac, u, t)) ->
+ xlate_term f (D.TCast (ac, D.TBind (ab, D.Abst ws, u), D.TBind (ab, D.Abst ws, t)))
| D.TBind (a, b, t) ->
let f tt = f (xlate_bind tt a b) in xlate_term f t
lenv_fold_left xlate_bind xlate_proj x e
let brg_of_drg f t =
+(*
+ print_newline (); DrgOutput.pp_term print_string t;
+*)
f (xlate_term C.start t)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module P = Printf
module U = NUri
module C = Cps
module H = Hierarchy
module X = Library
module D = Drg
+(****************************************************************************)
+
+let pp_attrs out a =
+ let map = function
+ | Y.Name (s, true) -> out (P.sprintf "%s;" s)
+ | Y.Name (s, false) -> out (P.sprintf "~%s;" s)
+ | Y.Apix i -> out (P.sprintf "+%i;" i)
+ | Y.Mark i -> out (P.sprintf "@%i;" i)
+ | Y.Priv -> out (P.sprintf "%s;" "~")
+ in
+ List.iter map 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.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 ^ ".")
+
+and pp_bind out = function
+ | D.Abst x -> pp_terms "[:" "]" out x
+ | D.Abbr x -> pp_terms "[=" "]" out x
+ | D.Void x -> out (P.sprintf "[%u]" x)
+
+let rec 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
+
+(****************************************************************************)
+
let rec list_iter map l out tab = match l with
| [] -> ()
| hd :: tl -> map hd out tab; list_iter map tl out tab
let rec aux err f e = function
| [], [] -> f e
| n :: ns, hd :: tl ->
- let f e = map e hd out tab; f (D.push2 C.err C.start e n ~t:hd) in
+ 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 n ~t:hd)
+ in
aux err f e (ns, tl)
| _ -> err ()
in
let attrs = [] in
X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+(****************************************************************************)
+
let export_term = exp_term D.empty_lenv
V_______________________________________________________________ *)
val export_term: Drg.term -> Library.pp
+
+val pp_term: (string -> unit) -> Drg.term -> unit
let f e = f st (BagEntity e) in Y.xlate f MBag.bag_of_meta e
| _, entity -> f st entity
+let pp_progress e =
+ let f a u =
+ let s = U.string_of_uri u in
+ let err () = L.warn (P.sprintf "%s" s) in
+ let f i = L.warn (P.sprintf "[%u] %s" i s) in
+ Y.mark err f a
+ in
+ match e with
+ | DrgEntity e -> Y.common f e
+ | BrgEntity e -> Y.common f e
+ | BagEntity e -> Y.common f e
+ | MetaEntity e -> Y.common f e
+
let count_entity st = function
| MetaEntity e -> {st with mc = count MO.count_entity st.mc e}
| BrgEntity e -> {st with brgc = count BrgO.count_entity st.brgc e}
let old = ref false
let process_3 f st a u =
- if !progress then
- let s = U.string_of_uri u in
- let err () = L.warn (P.sprintf "%s" s); f st in
- let f i = L.warn (P.sprintf "[%u] %s" i s); f st in
- Y.mark err f a
- else
- f st
+ f st
let process_2 f st entity =
let st = count_entity st entity in
if !stage > 2 then type_check (process_3 f) st !si !graph entity else f st
let process_1 f st entity =
+ if !progress then pp_progress entity;
let st = count_entity st entity in
if !export && !stage = 1 then export_entity !si !graph !moch entity;
if !stage > 1 then xlate (process_2 f) st entity else f st
# library_auto
TEST_DIRS_OPT = \
$(TEST_DIRS) \
- contribs/LAMBDA-TYPES \
+# contribs/LAMBDA-TYPES \
$(NULL)
.PHONY: tests tests.opt cleantests cleantests.opt
projects / helm.git / commitdiff