test-si-fast: $(MAIN).opt etc
@echo " HELENA -o -q -1 $(INPUTFAST)"
- $(H)./$(MAIN).opt -T 1 -o -q -1 $(O) $(INPUTFAST) > etc/log.txt
+ $(H)./$(MAIN).opt -T 1 -n -o -q -1 $(O) $(INPUTFAST) > etc/log.txt
test-si: $(MAIN).opt etc
@echo " HELENA -d -l -p -o $(INPUT)"
export-elpi elpi/$(ELPI): $(MAIN).opt etc
@echo " HELENA -l -m ELPI -o $(INPUT)"
$(H)mkdir -p elpi
- $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI -o $(O) $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI1 -o $(O) $(INPUT) > etc/log.txt
+ $(H)./$(MAIN).opt -T 1 -a n -c $(PREAMBLE_ELPI) -l -m ELPI2 -o $(O) $(INPUT) >> etc/log.txt
profile-fast: $(MAIN).opt etc
@echo " HELENA -o -q $(INPUTFAST) (31 TIMES)"
$(H)rm -f etc/log.txt
- $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
+ $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -n -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
$(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt
profile: $(MAIN).opt etc
let a = E.node_attrs ~sort:h () in
f a (D.TSort (a, h))
| A.Appl (v, t) ->
- let f vv at tt = f at (D.TAppl (at, vv, tt)) in
+ let f vv at tt = f at (D.TAppl (at, !G.extended, vv, tt)) in
let f _ vv = xlate_term (f vv) st lst y lenv t in
xlate_term f st lst false lenv v
| A.Abst (name, w, t) ->
| A.GRef (name, args) ->
let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
let map2 f arg args =
- let f _ arg = f (D.EAppl (args, E.empty_node, arg)) in
+ let f _ arg = f (D.EAppl (args, E.empty_node, !G.extended, arg)) in
xlate_term f st lst false lenv arg
in
let g qid a cnt =
let gref = D.TGRef (a, uri_of_qid qid) in
if cnt = D.ESort then f a gref else
let f = function
- | D.EAppl (D.ESort, _, v) -> f a (D.TAppl (a, v, gref))
- | args -> f a (D.TProj (a, args, gref))
+ | D.EAppl (D.ESort, _, x, v) -> f a (D.TAppl (a, x, v, gref))
+ | args -> f a (D.TProj (a, args, gref))
in
let f args = C.list_fold_right f map2 args D.ESort in
D.sub_list_strict (D.fold_names f map1 args) cnt args
*)
let b = E.Abst t in
let entity = E.empty_root, aw, uri_of_qid qid, b in
+ G.set_current_trace lst.line;
f {lst with line = succ lst.line} entity
in
xlate_term f st lst true lenv w
let b = E.Abbr t in
let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in
let entity = ra, na, uri_of_qid qid, b in
+ G.set_current_trace lst.line;
f {lst with line = succ lst.line} entity
in
xlate_term f st lst false lenv v
(* internal functions: crg to bag term **************************************)
let rec xlate_term st f c = function
- | D.TSort (_, h) -> f (Z.Sort h)
- | D.TGRef (_, s) -> f (Z.GRef s)
- | D.TLRef (a, i) ->
+ | D.TSort (_, 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) ->
+ | D.TCast (_, u, t) ->
let f tt uu = f (Z.Cast (uu, tt)) in
let f tt = xlate_term st (f tt) c u in
xlate_term st f c t
- | D.TAppl (_, v, t) ->
+ | D.TAppl (_, _, v, t) ->
let f tt vv = f (Z.Appl (vv, tt)) in
let f tt = xlate_term st (f tt) c v in
xlate_term st f c t
(* this case should be removed by improving alpha-conversion *)
| D.TBind (ab, D.Abst (x, n, ws), D.TCast (ac, u, t)) ->
xlate_term st f c (D.TCast (ac, D.TBind (ab, D.Abst (x, N.minus st n 1, ws), u), D.TBind (ab, D.Abst (x, n, ws), t)))
- | D.TBind (a, b, t) ->
+ | D.TBind (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
let f tt = xlate_bk_term (f tt) c u in
xlate_bk_term f c t
| Z.Appl (u, t) ->
- let f tt uu = f (D.TAppl (E.empty_node, uu, tt)) in
+ let f tt uu = f (D.TAppl (E.empty_node, true, uu, tt)) in
let f tt = xlate_bk_term (f tt) c u in
xlate_bk_term f c t
| Z.Bind (a, l, b, t) ->
if !G.indexes then err () else name err och a
let rec pp_term st c och = function
- | Z.Sort h ->
+ | Z.Sort h ->
let err () = KP.fprintf och "*%u" h in
let f s = KP.fprintf och "%s" s in
H.string_of_sort err f h
- | Z.LRef i ->
+ | Z.LRef i ->
let err () = KP.fprintf och "#%s" (P.string_of_mark i) in
let f a _ = name err och a in
if !G.indexes then err () else Z.get err f c i
- | Z.GRef s -> KP.fprintf och "$%s" (U.string_of_uri s)
- | Z.Cast (u, t) ->
+ | Z.GRef s -> KP.fprintf och "$%s" (U.string_of_uri s)
+ | Z.Cast (u, t) ->
KP.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t
- | Z.Appl (v, t) ->
+ | Z.Appl (v, t) ->
KP.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t
| Z.Bind (a, l, Z.Abst w, t) ->
let f cc =
let rec whd f c m x =
(* L.warn "entering R.whd"; *)
match x with
- | Z.Sort h -> f m (Sort_ h)
- | Z.GRef uri ->
+ | Z.Sort h -> f m (Sort_ h)
+ | Z.GRef uri ->
let f entry = f m (GRef_ entry) in
ZE.get_entity f uri
- | Z.LRef i ->
+ | Z.LRef i ->
let f = function
| Z.Void -> f m (LRef_ (i, None))
| Z.Abst t -> f m (LRef_ (i, Some t))
| Z.Abbr t -> whd f c m t
in
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.Cast (_, t) -> whd f c m t
+ | Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t
| Z.Bind (a, l, Z.Abst w, t) ->
begin match m.s with
| [] -> f m (Bind_ (a, l, w, t))
let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in
Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v)))
end
- | Z.Bind (a, l, b, t) ->
+ | Z.Bind (a, l, b, t) ->
let nl = P.new_mark () in
let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in
Z.push "!" f m.c a nl b
whd aux c m x
let ho_whd f st c t =
- if !G.trace >= level then log1 st "Now scanning" c t;
+ if !G.ct >= level then log1 st "Now scanning" c t;
ho_whd f c empty_machine t
let rec are_convertible f st a c m1 t1 m2 t2 =
let rec aux m1 r1 m2 r2 =
(* L.warn "entering R.are_convertible_aux"; *)
let u, t = term_of_whdr r1, term_of_whdr r2 in
- if !G.trace >= level then log2 st "Now really converting" c u c t;
+ if !G.ct >= level then log2 st "Now really converting" c u c t;
match r1, r2 with
| Sort_ h1, Sort_ h2 ->
if h1 = h2 then f a else f false
C.list_fold_left2 f map a m1.s m2.s
let are_convertible f st c u t =
- if !G.trace >= level then log2 st "Now converting" c u c t;
+ if !G.ct >= level then log2 st "Now converting" c u c t;
are_convertible f st true c empty_machine u empty_machine t
let rec b_type_of err f st c x =
(* L.warn "Entering T.b_type_of"; *)
- if !G.trace >= level then log1 st "Now checking" c x;
+ if !G.ct >= level then log1 st "Now checking" c x;
match x with
- | Z.Sort h ->
+ | Z.Sort h ->
let h = H.apply h in f x (Z.Sort h)
- | Z.LRef i ->
+ | Z.LRef i ->
let err0 () = error1 err "variable not found" c x in
let f _ = function
| Z.Abst w -> f x w
| Z.Void -> error1 err "reference to excluded variable" c x
in
Z.get err0 f c i
- | Z.GRef uri ->
+ | Z.GRef uri ->
let f = function
| _, _, _, E.Abst w -> f x w
| _, _, _, E.Abbr (Z.Cast (w, v)) -> f x w
in
let f cc = b_type_of err f st cc t in
Z.push "type void" f c a l Z.Void
- | Z.Appl (v, t) ->
+ | Z.Appl (v, t) ->
let f xv vv xt tt = function
| ZR.Abst w ->
- if !G.trace > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
+ if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
let f a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) st c tt in
let f xv vv = b_type_of err (f xv vv) st c t in
type_of err f st c v
- | Z.Cast (u, t) ->
+ | Z.Cast (u, t) ->
let f xu xt tt a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (S.sh2 u xu t xt x Z.cast) xu else error3 err c xt tt xu
| Abst of bool * N.layer * term (* x-reduced?, layer, type *)
| Abbr of term (* body *)
-and term = Sort of attrs * int (* attrs, hierarchy index *)
- | LRef of attrs * int (* attrs, position index *)
- | GRef of attrs * uri (* attrs, reference *)
- | Cast of attrs * term * term (* attrs, type, term *)
- | Appl of attrs * term * term (* attrs, argument, function *)
- | Bind of attrs * bind * term (* attrs, binder, scope *)
+and term = Sort of attrs * int (* attrs, hierarchy index *)
+ | LRef of attrs * int (* attrs, position index *)
+ | GRef of attrs * uri (* attrs, reference *)
+ | Cast of attrs * term * term (* attrs, type, term *)
+ | Appl of attrs * bool * term * term (* attrs, extended?, argument, function *)
+ | Bind of attrs * bind * term (* attrs, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
(* Currified constructors ***************************************************)
-let abst x n w = Abst (x, n, w)
+let abst r n w = Abst (r, n, w)
let abbr v = Abbr v
let cast a u t = Cast (a, u, t)
-let appl a u t = Appl (a, u, t)
+let appl a x u t = Appl (a, x, u, t)
let bind a b t = Bind (a, b, t)
-let bind_abst x n a u t = Bind (a, Abst (x, n, u), t)
+let bind_abst r n a u t = Bind (a, Abst (r, n, u), t)
let bind_abbr a u t = Bind (a, Abbr u, t)
(* internal functions: crg to brg term **************************************)
let rec xlate_term f = function
- | D.TSort (a, l) -> f (B.Sort (a, l))
- | D.TGRef (a, n) -> f (B.GRef (a, n))
- | D.TLRef (a, i) -> f (B.LRef (a, i))
- | D.TCast (a, u, t) ->
+ | D.TSort (a, l) -> f (B.Sort (a, l))
+ | D.TGRef (a, n) -> f (B.GRef (a, n))
+ | D.TLRef (a, i) -> f (B.LRef (a, i))
+ | D.TCast (a, u, t) ->
let f tt uu = f (B.Cast (a, uu, tt)) in
let f tt = xlate_term (f tt) u in
xlate_term f t
- | D.TAppl (a, v, t) ->
- let f tt vv = f (B.Appl (a, vv, tt)) in
+ | D.TAppl (a, x, v, t) ->
+ let f tt vv = f (B.Appl (a, x, vv, tt)) in
let f tt = xlate_term (f tt) v in
xlate_term f t
- | D.TProj (_, e, t) ->
+ | D.TProj (_, e, t) ->
D.shift (xlate_term f) e t
- | D.TBind (a, b, t) ->
+ | D.TBind (a, b, t) ->
xlate_term (xlate_bind f a b) t
and xlate_bind f a b t = match b with
- | D.Abst (x, n, w) ->
- let f ww = f (B.Bind (a, B.Abst (x, n, ww), t)) in
+ | D.Abst (r, n, w) ->
+ let f ww = f (B.Bind (a, B.Abst (r, n, ww), t)) in
xlate_term f w
| D.Abbr v ->
let f vv = f (B.Bind (a, B.Abbr vv, t)) in
(* internal functions: brg to crg term **************************************)
let rec xlate_bk_term f = function
- | B.Sort (a, l) -> f (D.TSort (a, l))
- | B.GRef (a, n) -> f (D.TGRef (a, n))
- | B.LRef (a, i) -> f (D.TLRef (a, i))
- | B.Cast (a, u, t) ->
+ | B.Sort (a, l) -> f (D.TSort (a, l))
+ | B.GRef (a, n) -> f (D.TGRef (a, n))
+ | B.LRef (a, i) -> f (D.TLRef (a, i))
+ | B.Cast (a, u, t) ->
let f tt uu = f (D.TCast (a, uu, tt)) in
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
+ | B.Appl (a, x, u, t) ->
+ let f tt uu = f (D.TAppl (a, x, uu, tt)) in
let f tt = xlate_bk_term (f tt) u in
xlate_bk_term f t
- | B.Bind (a, b, t) ->
+ | B.Bind (a, b, t) ->
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 (x, n, t) ->
- let f tt = f (D.Abst (x, n, tt)) in
+ | B.Abst (r, n, t) ->
+ let f tt = f (D.Abst (r, n, tt)) in
xlate_bk_term f t
| B.Abbr t ->
let f tt = f (D.Abbr tt) in
let ok = ref true
-let level = ref 0
+let uris = ref []
let base = "elpi"
let rec out_term st e och = function
| B.Sort (_, h) ->
- let sort = if h = 0 then "k+0" else if h = 1 then "k+1" else assert false in
+ let sort = if h = 0 then "k+set" else if h = 1 then "k+prop" else assert false in
KP.fprintf och "(sort %s)" sort
| B.LRef (_, i) ->
let _, _, a, b = B.get e i in
KP.fprintf och "%a" out_uri s
| B.Cast (_, u, t) ->
KP.fprintf och "(cast %a %a)" (out_term st e) u (out_term st e) t
- | B.Appl (_, v, t) ->
- KP.fprintf och "(appr %a %a)" (out_term st e) v (out_term st e) t
- | B.Bind (a, B.Abst (x, n, w), t) ->
+ | B.Appl (_, x, v, t) ->
+ let c = if x then "appx" else "appr" in
+ KP.fprintf och "(%s %a %a)" c (out_term st e) v (out_term st e) t
+ | B.Bind (a, B.Abst (r, n, w), t) ->
let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst x n w) in
- let c = if x then "prod" else "abst" in
+ let ee = B.push e B.empty a (B.abst r n w) in
+ let c = if r then "prod" else "abst" in
let l = match N.to_string st n with
| "1" -> "l+1"
| "2" -> "l+2"
KP.fprintf och "(void %a\\ %a)"
out_name a (out_term st ee) t
-let output_entity och st (_, na, s, b) =
+(* variant 1 *************************************************)
+
+let output_entity_1 och st (_, na, s, b) =
(* if na.E.n_apix <= 4500 then begin *)
- out_comment och (KP.sprintf "constant %u" na.E.n_apix);
+(* out_comment och (KP.sprintf "constant %u" na.E.n_apix); *)
match b with
| E.Abbr t ->
- KP.fprintf och "(gdef c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s;
- incr level; !ok
+ KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s;
+ uris := (true, s) :: !uris; !ok
| E.Abst u ->
- KP.fprintf och "(gdec c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s;
- incr level; !ok
+ KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s;
+ uris := (false, s) :: !uris; !ok
| E.Void -> C.err ()
(* end else !ok *)
-let close_out och () =
- let rec aux () =
- if !level <= 0 then KP.fprintf och "%s" "\n\n).\n"
- else begin KP.fprintf och "%s" ")"; decr level; aux () end
+let close_out_1 och () =
+ let aux_sep _ = KP.fprintf och "%s" ")" in
+ KP.fprintf och "%s" "gtop";
+ List.iter aux_sep !uris;
+ out_clause och "\n\n).";
+ close_out och
+
+(* Variant 2 *************************************************)
+
+let output_entity_2 och st (_, na, s, b) =
+(* out_comment och (KP.sprintf "constant %u" na.E.n_apix); *)
+(* if na.E.n_apix <= 9 then begin *)
+ match b with
+ | E.Abbr t ->
+ KP.fprintf och "g+line %a c+%u\n %a\n.\n\n"
+ out_uri s na.E.n_apix (out_term st B.empty) t;
+ uris := (true, s) :: !uris; !ok
+ | E.Abst u ->
+ KP.fprintf och "g+line %a c+%u\n %a\n.\n\n"
+ out_uri s na.E.n_apix (out_term st B.empty) u;
+ uris := (false, s) :: !uris; !ok
+ | E.Void -> C.err ()
+(* end else !ok *)
+
+let close_out_2 och () =
+ let aux_name (b, s) =
+ let gde = if b then "gdef+2" else "gdec+2" in
+ KP.fprintf och "(%s %a\n" gde out_uri s
in
+ let aux_sep _ = KP.fprintf och "%s" ")" in
+ out_clause och "main :- grundlagen.";
+ out_clause och "grundlagen :- (gv+ ";
+ List.iter aux_name (List.rev !uris);
KP.fprintf och "%s" "gtop";
- aux (); close_out och
+ List.iter aux_sep !uris;
+ out_clause och "\n\n).";
+ close_out och
(* Interface functions ******************************************************)
-let open_out fname =
+let open_out_1 fname =
let dir = KF.concat !G.manager_dir base in
let path = KF.concat dir fname in
- let och = open_out (path ^ ext) in
+ let och = open_out (path ^ "1" ^ ext) in
out_preamble och;
out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
out_clause och "main :- grundlagen.";
out_clause och "grundlagen :- gv+ (";
- output_entity och, close_out och
+ output_entity_1 och, close_out_1 och
+
+let open_out_2 fname =
+ let dir = KF.concat !G.manager_dir base in
+ let path = KF.concat dir fname in
+ let och = open_out (path ^ "2" ^ ext) in
+ out_preamble och;
+ out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+ output_entity_2 och, close_out_2 och
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val open_out: string -> Brg.manager
+val open_out_1: string -> Brg.manager
+
+val open_out_2: string -> Brg.manager
KP.fprintf och "%a" out_uri s
| B.Cast (_, u, t) ->
KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u
- | B.Appl (_, v, t) ->
+ | B.Appl (_, _, v, t) ->
let pt = match t with B.Appl _ -> false | _ -> true in
let op, cp = if p then "(", ")" else "", "" in
KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
- | B.Bind (a, B.Abst (x, n, w), t) ->
+ | B.Bind (a, B.Abst (r, n, w), t) ->
let p = true in
let op, cp = if p then "(", ")" else "", "" in
let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst x n w) in
+ let ee = B.push e B.empty a (B.abst r n w) in
let ob, cb = match N.to_string st n with
| "1" -> "forall", ","
| "2" -> "fun", " =>"
KP.fprintf och "%a" out_uri s
| B.Cast (_, u, t) ->
KP.fprintf och "(%a : %a)" (out_term st false e) t (out_term st false e) u
- | B.Appl (_, v, t) ->
+ | B.Appl (_, _, v, t) ->
let pt = match t with B.Appl _ -> false | _ -> true in
let op, cp = if p then "(", ")" else "", "" in
KP.fprintf och "%s%a %a%s" op (out_term st pt e) t (out_term st true e) v cp
- | B.Bind (a, B.Abst (x, n, w), t) ->
+ | B.Bind (a, B.Abst (r, n, w), t) ->
let op, cp = if p then "(", ")" else "", "" in
let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst x n w) in
+ let ee = B.push e B.empty a (B.abst r n w) in
let binder = match N.to_string st n, a.E.n_sort with
| "1", 0 -> "Î "
| "1", 1 -> "∀"
f c
and count_term f c e = function
- | B.Sort _ ->
+ | B.Sort _ ->
f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
- | B.LRef (_, i) ->
+ | B.LRef (_, i) ->
begin match B.get e i with
| _, _, _, B.Abst _
| _, _, _, B.Void ->
| _, _, _, B.Abbr _ ->
f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
end
- | B.GRef (_, u) ->
+ | B.GRef (_, u) ->
let c =
if Cps.list_mem ~eq:U.eq u c.uris
then {c with nodes = succ c.nodes}
else {c with xnodes = succ c.xnodes}
in
f {c with tgrefs = succ c.tgrefs}
- | B.Cast (_, v, t) ->
+ | B.Cast (_, v, t) ->
let c = {c with tcasts = succ c.tcasts} in
let f c = count_term f c e t in
count_term f c e v
- | B.Appl (_, v, t) ->
+ | B.Appl (_, _, v, t) ->
let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
let f c = count_term f c e t in
count_term f c e v
- | B.Bind (a, b, t) ->
+ | B.Bind (a, b, t) ->
let f c = count_term f c (B.push e B.empty a b) t in
count_term_binder f c e b
KP.fprintf och "$%s" (U.string_of_uri s)
| B.Cast (_, u, t) ->
KP.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t
- | B.Appl (_, v, t) ->
+ | B.Appl (_, _, v, t) ->
KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
- | B.Bind (a, B.Abst (x, n, w), t) ->
+ | B.Bind (a, B.Abst (r, n, w), t) ->
let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst x n w) in
- KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced x (name C.start) a (pp_term st e) w (pp_term st ee) t
+ let ee = B.push e B.empty a (B.abst r n w) in
+ KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) a (pp_term st e) w (pp_term st ee) t
| B.Bind (a, B.Abbr v, t) ->
let a = R.alpha B.mem e a in
let ee = B.push e B.empty a (B.abbr v) in
let are_alpha_convertible err f t1 t2 =
let rec aux f = function
| B.Sort (_, p1), B.Sort (_, p2)
- | B.LRef (_, p1), B.LRef (_, p2) ->
+ | B.LRef (_, p1), B.LRef (_, p2) ->
if p1 = p2 then f () else err ()
- | B.GRef (_, u1), B.GRef (_, u2) ->
+ | B.GRef (_, u1), B.GRef (_, u2) ->
if U.eq u1 u2 then f () else err ()
| B.Cast (_, v1, t1), B.Cast (_, v2, t2)
- | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
+ | B.Appl (_, _, v1, t1), B.Appl (_, _, v2, t2) ->
let f _ = aux f (t1, t2) in
aux f (v1, v2)
- | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
+ | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
let f _ = aux f (t1, t2) in
aux_bind f (b1, b2)
- | _ -> err ()
+ | _ -> err ()
and aux_bind f = function
| B.Abbr v1, B.Abbr v2 -> aux f (v1, v2)
- | B.Abst (x1, n1, v1), B.Abst (x2, n2, v2) when x1 = x2 && n1 = n2 -> aux f (v1, v2)
+ | B.Abst (r1, n1, v1), B.Abst (r2, n2, v2) when r1 = r2 && n1 = n2 -> aux f (v1, v2)
| B.Void, B.Void -> f ()
| _ -> err ()
in
(* to share *)
let rec step st m r =
- if !G.trace >= sublevel then
+ if !G.ct >= sublevel then
log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r;
match r with
| B.Sort (a, h) ->
| B.GRef (_, uri) ->
begin match BE.get_entity uri with
| _, _, _, E.Abbr v ->
- if m.n = None || !G.expand then begin
+ if !G.expand then begin
if !G.summary then O.add ~gdelta:1 ();
step st m v
end else
if !G.summary then O.add ~epsilon:1 ();
step st m t
end
- | B.Appl (_, v, t) ->
+ | B.Appl (_, _, v, t) ->
step st {m with s = (m.e, v) :: m.s} t
| B.Bind (a, B.Abst (false, n, w), t) ->
let i = tsteps m in
{m with e = e; l = l}
let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
- if !G.trace >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
+ if !G.ct >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
match t1, r1, t2, r2 with
| B.Sort (_, h1), _, B.Sort (_, h2), _ ->
h1 = h2
in
list_and map (m1.s, m2.s)
+let rec ih_nfs st (m, t, r) =
+ match t, r with
+ | B.GRef _, Some v ->
+ if !G.summary then O.add ~gdelta:1 ();
+ ih st m v
+ | _ -> m, t
+
+and ih st m t = ih_nfs st (step st m t)
+
(* Interface functions ******************************************************)
let empty_rtm = {
let _, _, _, b = B.get m.e i in b
let xwhd st m n t =
- if !G.trace >= level then log1 st "Now scanning" m.e t;
- let m, t, _ = step st (reset m n) t in
- m, t
+ if !G.ct >= level then log1 st "Now scanning" m.e t;
+ ih st (reset m n) t
let are_convertible st m1 n1 t1 m2 n2 t2 =
- if !G.trace >= level then log2 st "Now converting" m1.e t1 m2.e t2;
+ if !G.ct >= level then log2 st "Now converting" m1.e t1 m2.e t2;
let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in
r
(* let err _ = in
| B.GRef _ -> succ a
| B.Bind (_, B.Void, t) -> icm (succ a) t
| B.Cast (_, u, t) -> icm (icm a u) t
- | B.Appl (_, u, t)
+ | B.Appl (_, _, u, t)
| B.Bind (_, B.Abst (_, _, u), t)
| B.Bind (_, B.Abbr u, t) -> icm (icm (succ a) u) t
let iter map d =
let rec iter_bind d = function
| B.Void -> B.Void
- | B.Abst (x, n, w) -> B.Abst (x, n, iter_term d w)
+ | B.Abst (r, n, w) -> B.Abst (r, n, iter_term d w)
| B.Abbr v -> B.Abbr (iter_term d v)
and iter_term d = function
- | B.Sort _ as t -> t
- | B.GRef _ as t -> t
+ | B.Sort _ as t -> t
+ | B.GRef _ as t -> t
| B.LRef (a, i) as t -> if i < d then t else map d a i
- | B.Cast (a, w, v) -> B.Cast (a, iter_term d w, iter_term d v)
- | B.Appl (a, w, u) -> B.Appl (a, iter_term d w, iter_term d u)
- | B.Bind (a, b, u) -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
+ | B.Cast (a, w, v) -> B.Cast (a, iter_term d w, iter_term d v)
+ | B.Appl (a, x, w, u) -> B.Appl (a, x, iter_term d w, iter_term d u)
+ | B.Bind (a, b, u) -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
in
iter_term d
if BR.are_convertible st m zero u m zero w then f () else
error3 err m v w u
-let assert_applicability err f st m u w v =
- match BR.xwhd st m None u with
+let assert_applicability err f st m x u w v =
+ let mode = if x then None else zero in
+ match BR.xwhd st m mode u with
| _, B.Sort _ ->
error1 err "not a function type" m u
| mu, B.Bind (_, B.Abst (true, n, u), _) ->
error3 err m v w ~mu u
| _ -> assert false (**)
-let rec b_type_of err f st m r =
- if !G.trace >= level then log1 st "Now checking" m r;
- match r with
+let rec b_type_of err f st m y =
+ if !G.ct >= level then log1 st "Now checking" m y;
+ match y with
| B.Sort (a, h) ->
- let h = H.apply h in f r (B.Sort (a, h))
+ let h = H.apply h in f y (B.Sort (a, h))
| B.LRef (_, i) ->
begin match BR.get m i with
| B.Abst (_, _, w) ->
- f r (BS.lift (succ i) (0) w)
+ f y (BS.lift (succ i) (0) w)
| B.Abbr (B.Cast (_, w, _)) ->
- f r (BS.lift (succ i) (0) w)
+ f y (BS.lift (succ i) (0) w)
| B.Abbr _ -> assert false
| B.Void ->
- error1 err "reference to excluded variable" m r
+ error1 err "reference to excluded variable" m y
end
| B.GRef (_, uri) ->
begin match BE.get_entity uri with
- | _, _, _, E.Abst w -> f r w
- | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f r w
+ | _, _, _, E.Abst w -> f y w
+ | _, _, _, E.Abbr (B.Cast (_, w, _)) -> f y w
| _, _, _, E.Abbr _ -> assert false
| _, _, _, E.Void ->
- error1 err "reference to unknown entry" m r
+ error1 err "reference to unknown entry" m y
end
| B.Bind (a, B.Abbr v, t) ->
let f rv rt tt =
- f (S.sh2 v rv t rt r (B.bind_abbr a)) (B.bind_abbr a rv tt)
+ f (S.sh2 v rv t rt y (B.bind_abbr a)) (B.bind_abbr a rv tt)
in
let f rv m = b_type_of err (f rv) st m t in
let f rv = f rv (BR.push m a (B.abbr rv)) in
| _ -> f (B.Cast (E.empty_node, vv, rv))
in
type_of err f st m v
- | B.Bind (a, B.Abst (x, n, u), t) ->
+ | B.Bind (a, B.Abst (r, n, u), t) ->
let f ru rt tt =
- f (S.sh2 u ru t rt r (B.bind_abst x n a)) (B.bind_abst x (N.minus st n 1) a ru tt)
+ f (S.sh2 u ru t rt y (B.bind_abst r n a)) (B.bind_abst r (N.minus st n 1) a ru tt)
in
let f ru m = b_type_of err (f ru) st m t in
- let f ru _ = f ru (BR.push m a (B.abst x n ru)) in
+ let f ru _ = f ru (BR.push m a (B.abst r n ru)) in
type_of err f st m u
| B.Bind (a, B.Void, t) ->
let f rt tt =
- f (S.sh1 t rt r (B.bind_void a)) (B.bind_void a tt)
+ f (S.sh1 t rt y (B.bind_void a)) (B.bind_void a tt)
in
b_type_of err f st (BR.push m a B.Void) t
- | B.Appl (a, v, t) ->
+ | B.Appl (a, x, v, t) ->
let f rv vv rt tt =
- let f _ = f (S.sh2 v rv t rt r (B.appl a)) (B.appl a rv tt) in
- assert_applicability err f st m tt vv rv
+ let f _ = f (S.sh2 v rv t rt y (B.appl a x)) (B.appl a x rv tt) in
+ assert_applicability err f st m x tt vv rv
in
let f rv vv = b_type_of err (f rv vv) st m t in
type_of err f st m v
| B.Cast (a, u, t) ->
let f ru rt tt =
- let f _ = f (S.sh2 u ru t rt r (B.cast a)) ru in
+ let f _ = f (S.sh2 u ru t rt y (B.cast a)) ru in
assert_convertibility err f st m ru tt rt
in
let f ru _ = b_type_of err (f ru) st m t in
(* Interface functions ******************************************************)
-and type_of err f st m r = b_type_of err f st m r
+and type_of err f st m t = b_type_of err f st m t
let uri, t = match e with
| _, _, uri, E.Abst t -> uri, t
| _, _, uri, E.Abbr t -> uri, t
- | _, _, _, E.Void -> assert false
+ | _, _, _, E.Void -> assert false
in
let err msg = err (L.Uri uri :: msg) in
let f () = let _ = BE.set_entity e in f () in
let one = Some 1
let assert_convertibility err f st m u t =
- if !G.trace >= level then warn "Asserting convertibility for cast";
+ if !G.ct >= level then warn "Asserting convertibility for cast";
if BR.are_convertible st m zero u m one t then f () else
error2 err m u m t
-let assert_applicability err f st m v t =
- if !G.trace >= level then warn "Asserting applicability";
- match BR.xwhd st m None t with
- | _, B.Sort _ ->
- error1 err "not a function" m t
+let assert_applicability err f st m x v t =
+ let mode, msg = if x then None, "extended" else one, "restricted" in
+ if !G.ct >= level then warn ("Asserting " ^ msg ^ " applicability");
+ match BR.xwhd st m mode t with
| mw, B.Bind (_, B.Abst (true, n, w), _) ->
if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function" m t
else begin
- if !G.trace >= level then warn "Asserting convertibility for application";
+ if !G.ct >= level then warn "Asserting convertibility for application";
if BR.are_convertible st mw zero w m one v then f () else
error2 err mw w m v
end
- | _ -> assert false (**)
+ | _, B.Sort _ ->
+ error1 err "not a function" m t
+ | _ -> assert false (**)
-let rec b_validate err f st m x =
- if !G.trace >= level then log1 st "Now checking" m x;
- match x with
+let rec b_validate err f st m y =
+ if !G.ct >= level then log1 st "Now checking" m y;
+ match y with
| B.Sort _ -> f ()
| B.LRef (_, i) ->
begin match BR.get m i with
| B.Abst _
| B.Abbr _ -> f ()
| B.Void ->
- error1 err "reference to excluded variable" m x
+ error1 err "reference to excluded variable" m y
end
| B.GRef (_, uri) ->
begin match BE.get_entity uri with
| _, _, _, E.Abst _
| _, _, _, E.Abbr _ -> f ()
| _, _, _, E.Void ->
- error1 err "reference to unknown entry" m x
+ error1 err "reference to unknown entry" m y
end
| B.Bind (a, b, t) ->
let f () = b_validate err f st (BR.push m a b) t in
| B.Abbr v -> validate err f st m v
| B.Void -> f ()
end
- | B.Appl (_, v, t) ->
- let f () = assert_applicability err f st m v t in
+ | B.Appl (_, x, v, t) ->
+ let f () = assert_applicability err f st m x v t in
let f () = b_validate err f st m t in
validate err f st m v
| B.Cast (_, u, t) ->
(* Interface functions ******************************************************)
-and validate err f st m x = b_validate err f st m x
+and validate err f st m t = b_validate err f st m t
let k, n = resolve_key_with_default st default k in
if n.s then generated st h i else begin
if n <> default then KH.replace st k default;
- if !G.trace >= level then pp_table st; default
+ if !G.ct >= level then pp_table st; default
end
let assert_finite st n j =
- if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
+ if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
let rec aux (k, n) j = match n.v with
| Fin i when i = j -> true
| Fin i ->
Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
| Inf ->
Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
- | Unk -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
+ | Unk -> n.v <- Fin j; if !G.ct >= level then pp_table st; true
| Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j)
in
let k, n = resolve_layer st n in
aux (k, n) j
let assert_infinite st n =
- if !G.trace >= level then warn "ASSERT INFINITE";
+ if !G.ct >= level then warn "ASSERT INFINITE";
let rec aux (k, n) = match n.v with
| Inf -> true
| Fin i ->
Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
- | Unk -> n.v <- Inf; if !G.trace >= level then pp_table st; true
+ | Unk -> n.v <- Inf; if !G.ct >= level then pp_table st; true
| Ref (k, _) -> n.v <- Inf; aux (resolve_key st k)
in
aux (resolve_layer st n)
let two = finite 2
let rec unknown st =
- if !G.trace >= level then warn "UNKNOWN";
+ if !G.ct >= level then warn "UNKNOWN";
let default = empty () in
let k = P.new_mark () in
let k, n = resolve_key_with_default st default k in
if n.s then match n.v with
| Inf
| Fin _ -> n
- | Unk -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+ | Unk -> if !G.ct >= level then pp_table st; cell true (Ref (k, 0))
| Ref _ -> assert false
else unknown st
let minus st n j =
- if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
+ if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j);
let rec aux k n j = match n.v with
| Inf -> cell false n.v
| Fin i when i > j -> cell false (Fin (i - j))
string_of_value k n.v
let assert_not_zero st n =
- if !G.trace >= level then warn "ASSERT NOT ZERO";
+ if !G.ct >= level then warn "ASSERT NOT ZERO";
let k, n = resolve_layer st n in
match n.b, n.v with
| true, _ -> n.b
(* | _ , Fin i when i = 0 ->
Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
(* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)
- | _ -> n.b <- true; if !G.trace >= level then pp_table st; n.b
+ | _ -> n.b <- true; if !G.ct >= level then pp_table st; n.b
let assert_zero st n = assert_finite st n 0
| Ref _ -> assert false
else false
in begin
- if !G.trace >= level then warn "ASSERT EQUAL";
+ if !G.ct >= level then warn "ASSERT EQUAL";
if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
- n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
+ n1.v <- Ref (k2, 0); if !G.ct >= level then pp_table st
end; b end
let is_not_zero st n =
type manager = Quiet
| Coq
| Matita
- | ELPI
+ | ELPI1
+ | ELPI2
(* interface functions ******************************************************)
let trace = ref 0 (* trace level *)
+let ct = ref 0 (* current trace level *)
+
let summary = ref false (* log summary information *)
let xdir = ref "" (* directory for XML output *)
let alpha = ref "" (* prefix of numeric identifiers *)
+let first = ref 0 (* begin trace here *)
+
+let last = ref max_int (* end trace here *)
+
+let extended = ref false (* extended applications *)
+
+let set_current_trace n =
+ ct := if !first <= n && n <= !last then !trace else 0
+
let kernel_id () =
let id = match !kernel with
| V4 -> "Environment"
| V0 -> "Environment_V0"
in
let si = if !si then "_si" else "" in
- id ^ si
+ let ext = if !extended then "_x" else "" in
+ id ^ si ^ ext
let get_baseuri () =
String.concat "/" ["ld:"; kernel_id (); !cover; "" ]
fun s -> KF.concat bu (s ^ ".ld")
let clear () =
- stage := 3; trace := 0; summary := false;
- xdir := ""; kernel := V3; si := false; cover := "";
+ stage := 3; trace := 0; summary := false; first := 0; last := max_int;
+ xdir := ""; kernel := V3; si := false; extended := false; cover := "";
expand := false; indexes := false; icm := 0; unquote := false;
debug_parser := false; debug_lexer := false;
manager_dir := ""; manager := Quiet
?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0)
?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
=
- if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
- if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
- if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
- if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
- if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt);
+ if !G.ct >= level then begin
+ if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
+ if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
+ if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
+ if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
+ if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt);
+ end;
reductions := {
beta = !reductions.beta + beta;
zeta = !reductions.zeta + zeta;
type id = E.id
type attrs = E.node_attrs
-type bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *)
- | Abbr of term (* body *)
- | Void (* *)
-
-and term = TSort of attrs * int (* attrs, hierarchy index *)
- | TLRef of attrs * int (* attrs, position indexe *)
- | TGRef of attrs * uri (* attrs, reference *)
- | TCast of attrs * term * term (* attrs, domain, element *)
- | TAppl of attrs * 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 *)
- | 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 bind = Abst of bool * N.layer * term (* x-reduced?, layer, type *)
+ | Abbr of term (* body *)
+ | Void (* *)
+
+and term = TSort of attrs * int (* attrs, hierarchy index *)
+ | TLRef of attrs * int (* attrs, position indexe *)
+ | TGRef of attrs * uri (* attrs, reference *)
+ | TCast of attrs * term * term (* attrs, domain, element *)
+ | TAppl of attrs * bool * term * term (* attrs, extended?, argument, function *)
+ | TBind of attrs * bind * term (* attrs, binder, scope *)
+ | TProj of attrs * lenv * term (* attrs, closure, member *)
+
+and lenv = ESort (* top *)
+ | EBind of lenv * attrs * bind (* environment, attrs, binder *)
+ | EAppl of lenv * attrs * bool * term (* environment, attrs, extended?, argument *)
+ | EProj of lenv * attrs * lenv (* environment, attrs, closure *)
type entity = term E.entity
let push_bind f a b lenv = f (EBind (lenv, a, b))
-let push_appl f a t lenv = f (EAppl (lenv, a, t))
+let push_appl f a x t lenv = f (EAppl (lenv, a, x, t))
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 add_appl f a x v t = f (TAppl (a, x, v, t))
let add_proj f a e t = f (TProj (a, e, t))
let rec shift f c t = match c with
- | ESort -> f t
- | EBind (e, a, b) -> add_bind (shift f e) a b t
- | EAppl (e, a, v) -> add_appl (shift f e) a v t
- | EProj (e, a, d) -> add_proj (shift f e) a d t
+ | ESort -> f t
+ | EBind (e, a, b) -> add_bind (shift f e) a b t
+ | EAppl (e, a, x, v) -> add_appl (shift f e) a x v t
+ | EProj (e, a, d) -> add_proj (shift f e) a d t
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
+ | ESort -> f c
+ | EBind (e, a, b) -> append (push_bind f a b) c e
+ | EAppl (e, a, x, t) -> append (push_appl f a x t) c e
+ | EProj (e, a, d) -> append (push_proj f a d) c e
let resolve_lref err f id lenv =
let rec aux i = function
- | ESort -> err ()
- | EAppl (tl, _, _) -> aux i tl
- | EBind (tl, a, _) ->
+ | ESort -> err ()
+ | EAppl (tl, _, _, _) -> aux i tl
+ | EBind (tl, a, _) ->
let f id0 _ = if id0 = id then f a i else aux (succ i) tl in
let err () = aux (succ i) tl in
E.name err f a
- | EProj (tl, _, d) -> append (aux i) tl d
+ | 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
+ | EAppl (tl, _, _, _) -> get_name err f i tl
| EBind (_, a, _) when i = 0 ->
let err () = err i in
E.name err f a
| ESort -> ESort, E.empty_node, Void
| EBind (e, a, b) when i = 0 -> e, a, b
| EBind (e, _, _) -> get e (pred i)
- | EAppl (e, _, _) -> get e i
+ | 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
| _ -> assert false
let rec mem err f e b = match e with
- | ESort -> err ()
- | EBind (e, a, _) ->
+ | ESort -> err ()
+ | EBind (e, a, _) ->
if a.E.n_name = b.E.n_name then f () else mem err f e b
- | EAppl (e, _, _) -> mem err f e b
- | EProj (e, _, d) ->
+ | EAppl (e, _, _, _) -> mem err f e b
+ | EProj (e, _, d) ->
let err () = mem err f e b in mem err f d b
let replace f n0 e =
let rec aux f = function
| ESort -> f ESort
- | EBind (e, a, Abst (x, n, w)) -> aux (push_bind f a (Abst (x, n0, w))) e
+ | EBind (e, a, Abst (r, n, w)) -> aux (push_bind f a (Abst (r, n0, w))) e
| EBind (e, a, b) -> aux (push_bind f a b) e
- | EAppl (e, a, v) -> aux (push_appl f a v) e
+ | EAppl (e, a, x, v) -> aux (push_appl f a x v) e
| EProj (e, a, d) -> let f d = aux (push_proj f a d) e in aux f d
in
}
let rec count_term f c e = function
- | D.TSort _ ->
+ | D.TSort _ ->
f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
- | D.TLRef (_, i) ->
+ | D.TLRef (_, i) ->
begin match D.get e i with
| _, _, D.Abbr _ ->
f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
| _ ->
f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
end
- | D.TGRef (_, u) ->
+ | D.TGRef (_, u) ->
let c =
if C.list_mem ~eq:U.eq u c.uris
then {c with nodes = succ c.nodes}
else {c with xnodes = succ c.xnodes}
in
f {c with tgrefs = succ c.tgrefs}
- | D.TCast (_, v, t) ->
+ | D.TCast (_, v, t) ->
let c = {c with tcasts = succ c.tcasts} in
let f c = count_term f c e t in
count_term f c e v
- | D.TAppl (_, v, t) ->
+ | D.TAppl (_, _, v, t) ->
let c = {c with tappls = succ c.tappls} in
let f c = count_term f c e t in
count_term f c e v
- | D.TProj (_, d, t) ->
+ | D.TProj (_, d, t) ->
D.shift (count_term f c e) d t
- | D.TBind (a, b, t) ->
+ | D.TBind (a, b, t) ->
let f c e = count_term f c e t in
count_binder f c e a b
let pp_state out x = if x then out "^"
let rec pp_term out st = function
- | D.TSort (a, l) -> pp_attrs out a; out (KP.sprintf "*%u" l)
- | D.TLRef (a, i ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
- | D.TGRef (a, u) -> pp_attrs out a; out (KP.sprintf "$")
- | D.TCast (a, u, t) -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t
- | D.TAppl (a, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t
- | D.TBind (a, u, t) -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t
- | D.TProj (a, u, t) -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t
+ | D.TSort (a, l) -> pp_attrs out a; out (KP.sprintf "*%u" l)
+ | D.TLRef (a, i ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
+ | D.TGRef (a, u) -> pp_attrs out a; out (KP.sprintf "$")
+ | D.TCast (a, u, t) -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t
+ | D.TAppl (a, _, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t
+ | D.TBind (a, u, t) -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t
+ | D.TProj (a, u, t) -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t
and pp_bind out st = function
- | D.Abst (x, n, u) ->
- out "[:"; pp_term out st u; out "]"; pp_state out x; out (N.to_string st n); out " "
+ | D.Abst (r, n, u) ->
+ out "[:"; pp_term out st u; out "]"; pp_state out r; out (N.to_string st n); out " "
| D.Abbr u -> out "[="; pp_term out st u; out "] ";
| D.Void -> out "[] "
and pp_lenv out st = function
- | D.ESort -> ()
- | D.EBind (u, a, t) -> pp_lenv out st u; pp_attrs out a; pp_bind out st t
- | D.EAppl (u, a, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
- | D.EProj (u, a, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "
+ | D.ESort -> ()
+ | D.EBind (u, a, t) -> pp_lenv out st u; pp_attrs out a; pp_bind out st t
+ | D.EAppl (u, a, _, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
+ | D.EProj (u, a, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "
path : T.id list; (* current section path *)
line : int; (* line number *)
sort : int; (* first default sort index *)
+ ext : bool; (* extended applications *)
mk_uri: G.uri_generator (* uri generator *)
}
let f _ uu = xlate_term (f uu) st lenv t in
xlate_term f st lenv u
| T.Appl (v, t) ->
- let f vv a tt = f a (D.TAppl (a, vv, tt)) in
+ let f vv a tt = f a (D.TAppl (a, st.ext, vv, tt)) in
let f _ vv = xlate_term (f vv) st lenv t in
xlate_term f st lenv v
| T.Proj (bs, t) ->
C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
| T.Inst (t, vs) ->
let map f v e =
- let f _ vv = D.push_appl f E.empty_node vv e in
+ let f _ vv = D.push_appl f E.empty_node st.ext vv e in
xlate_term f st lenv v
in
let f e a tt = f a (D.TProj (a, e, tt)) in
let initial_status () =
KH.clear henv; {
- path = []; line = 1; sort = 0; mk_uri = G.get_mk_uri ()
+ path = []; line = 1; sort = 0; ext = false; mk_uri = G.get_mk_uri ()
}
let refresh_status st = {st with
| Some (export_entity, _) -> manager st export_entity entity
let process_1 st entity =
- if !G.trace >= 3 then pp_progress entity;
+ if !G.ct >= 3 then pp_progress entity;
let st = if !G.summary then count_entity st entity else st in
if !export && !G.stage = 1 then export_entity st entity;
if !G.stage >= 2 then process_2 st (xlate_entity st entity) else st
if !G.trace >= 2 then begin preprocess := true; G.summary := true end
in
let set_manager s = match KS.lowercase s with
- | "v8" -> G.manager := G.Coq
- | "ma2" -> G.manager := G.Matita
- | "elpi" -> G.manager := G.ELPI
- | s -> L.warn level (KP.sprintf "Unknown manager: %s" s)
+ | "v8" -> G.manager := G.Coq
+ | "ma2" -> G.manager := G.Matita
+ | "elpi1" -> G.manager := G.ELPI1
+ | "elpi2" -> G.manager := G.ELPI2
+ | s -> L.warn level (KP.sprintf "Unknown manager: %s" s)
in
let clear_options () =
export := false; preprocess := false;
begin match !G.manager with
| G.Coq -> st := {!st with mst = Some (BA.open_out base_name)}
| G.Matita -> st := {!st with mst = Some (BG.open_out base_name)}
- | G.ELPI -> st := {!st with mst = Some (BP.open_out base_name)}
+ | G.ELPI1 -> st := {!st with mst = Some (BP.open_out_1 base_name)}
+ | G.ELPI2 -> st := {!st with mst = Some (BP.open_out_2 base_name)}
| G.Quiet -> ()
end;
P.clear_marks ();
if !G.trace >= 1 then Y.utime_stamp "at exit"
in
let help =
- "Usage: helena [ -LPVXdgilopqtx1 | -Ts <number> | -MO <dir> | -c <file> | -ahkmr <string> ]* [ <file> ]*\n\n" ^
+ "Usage: helena [ -LPVXdgilnopqtx1 | -Ts <number> | -MO <dir> | -c <file> | -ahkmr <string> | -be <age> ]* [ <file> ]*\n\n" ^
"Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, 3 processed objects,\n" ^
" 4 typing information, 5 conversion information, 6 reduction information,\n" ^
" 7 level disambiguation\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n\n" ^
- "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi\" (lambda-Prolog)\n"
+ "Supported manages: \"ma2\" (Grafite NG), \"v8\" (Gallina 8), \"elpi1\" \"elpi2\" (lambda-Prolog)\n"
in
let help_L = " show lexer debug information" in
let help_M = "<dir> set location of output directory (manager) to <dir> (default: current directory)" in
let help_X = " clear options" in
let help_a = "<string> set prefix of numeric identifiers (default: empty)" in
+ let help_b = "<age> begin trace at this global constant (default: first)" in
let help_c = "<file> set preamble to this file (default: empty)" in
let help_d = " show summary information (requires trace >= 2)" in
+ let help_e = "<age> end trace at this global constant (default: last)" in
let help_g = " always expand global definitions" in
let help_h = "<string> set type hierarchy (default: \"Z1\")" in
let help_i = " show local references by index" in
let help_k = "<string> set kernel version (default: \"V3\")" in
- let help_l = " disambiguate binders level (Automath)" in
+ let help_l = " disambiguate binders layer (Automath)" in
let help_m = "<string> export kernel entities for this manager (see above, default: no manager)" in
+ let help_n = " use extended (i.e. native) applications (Automath)" in
let help_o = " activate sort inclusion (default: false)" in
let help_p = " preprocess source (Automath)" in
let help_q = " disable quotation of identifiers" in
let help_r = "<string> set initial segment of URI hierarchy (default: empty)" in
let help_s = "<number> set translation stage (see above)" in
- let help_t = " type check [version 1]" in
+ let help_t = " type check (version 1)" in
let help_x = " export kernel entities (XML)" in
let help_1 = " parse files with streaming policy" in
("-V", Arg.Unit print_version, help_V);
("-X", Arg.Unit clear_options, help_X);
("-a", Arg.String ((:=) G.alpha), help_a);
+ ("-b", Arg.Int ((:=) G.first), help_b);
("-c", Arg.String ((:=) G.preamble), help_c);
("-d", Arg.Unit set_summary, help_d);
+ ("-e", Arg.Int ((:=) G.last), help_e);
("-g", Arg.Set G.expand, help_g);
("-h", Arg.String set_hierarchy, help_h);
("-i", Arg.Set G.indexes, help_i);
("-k", Arg.String set_kernel, help_k);
("-l", Arg.Set G.cc, help_l);
("-m", Arg.String set_manager, help_m);
+ ("-n", Arg.Set G.extended, help_n);
("-o", Arg.Set G.si, help_o);
("-p", Arg.Unit set_preprocess, help_p);
("-q", Arg.Set G.unquote, help_q);
(* NOTE: the inner binders are alpha-converted first *)
let a = R.alpha D.mem e a in
map_bind st e a b out tab; D.EBind (e, a, b)
- | D.EAppl (e, a, v) ->
+ | D.EAppl (e, a, x, v) ->
let e = aux e in
- map_appl st e a v out tab; D.EAppl (e, a, v)
+ map_appl st e a x v out tab; D.EAppl (e, a, x, v)
| D.EProj (e, a, d) ->
let e = aux e in
map_proj st e a d out tab; D.EProj (e, a, d)
let attrs = [] in
XL.tag XL.cast attrs ~contents:(exp_term st e u) out tab;
exp_term st e t out tab
- | D.TAppl (a, v, t) ->
+ | D.TAppl (a, x, v, t) ->
let attrs = [] in
- XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+ XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
exp_term st e t out tab
| D.TProj (a, lenv, t) ->
let attrs = [] in
exp_bind st e a b out tab;
exp_term st (D.push_bind C.start a b e) t out tab
-and exp_appl st e a v out tab =
+and exp_appl st e a x v out tab =
let attrs = [] in
- XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
+ XL.tag (XL.appl x) attrs ~contents:(exp_term st e v) out tab;
and exp_bind st e a b out tab = match b with
| D.Abst (_, n, w) ->
let cast = "Cast"
-let appl = "Appl"
+let appl x = if x then "Appx" else "Appr"
let proj = "Proj"
val cast: string
-val appl: string
+val appl: bool -> string
val proj: string
projects / helm.git / commitdiff