From: Ferruccio Guidi Date: Fri, 19 Jun 2015 16:58:43 +0000 (+0000) Subject: new options activated X-Git-Tag: make_still_working~719 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=67686e04702688cc822e809e5168f765bf69d7cb;p=helm.git new options activated - tracing can be restricted to specific constants with -b and -e - restricted applications are now used by default for Automath inputs use -n to activate extended applications (this may lead to longer computations) --- diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index f26c4e857..61891b69b 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -40,7 +40,7 @@ PREAMBLE_ELPI = elpi/elpi.template 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)" @@ -87,12 +87,13 @@ export-matita matita/$(MA): $(MAIN).opt etc 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 diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index c17b83f07..667b18cc1 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -118,7 +118,7 @@ let rec xlate_term f st lst y lenv = function 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) -> @@ -146,15 +146,15 @@ let rec xlate_term f st lst y lenv = function | 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 @@ -201,6 +201,7 @@ let xlate_entity err f st lst = function *) 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 @@ -222,6 +223,7 @@ let xlate_entity err f st lst = function 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 diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index 08f342496..b9ce1d344 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -19,15 +19,15 @@ module Z = Bag (* 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 @@ -36,7 +36,7 @@ let rec xlate_term st f c = function (* 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 @@ -67,7 +67,7 @@ let rec xlate_bk_term f c = function 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) -> diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml index 88e64e5d0..4867c7180 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.ml +++ b/helm/software/helena/src/basic_ag/bagOutput.ml @@ -111,18 +111,18 @@ let res a l och = 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 = diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index 287978f50..cc3cb36f8 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -81,19 +81,19 @@ let push msg f c m a l w = 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)) @@ -102,7 +102,7 @@ let rec whd f c m x = 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 @@ -124,7 +124,7 @@ let rec ho_whd f c m x = 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 = @@ -132,7 +132,7 @@ 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 @@ -189,5 +189,5 @@ and are_convertible_stacks f st a c m1 m2 = 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 diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index b6f3deb55..009a2eaf9 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -45,11 +45,11 @@ let mk_gref u l = 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 @@ -58,7 +58,7 @@ let rec b_type_of err f st c x = | 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 @@ -90,10 +90,10 @@ let rec b_type_of err f st c x = 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) @@ -106,7 +106,7 @@ let rec b_type_of err f st c x = 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 diff --git a/helm/software/helena/src/basic_rg/brg.ml b/helm/software/helena/src/basic_rg/brg.ml index 7be7dc939..a321a32b0 100644 --- a/helm/software/helena/src/basic_rg/brg.ml +++ b/helm/software/helena/src/basic_rg/brg.ml @@ -23,12 +23,12 @@ type bind = Void (* *) | 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 *) @@ -40,7 +40,7 @@ type manager = (N.status -> entity -> bool) * (unit -> unit) (* 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 @@ -48,11 +48,11 @@ let lref a i = LRef (a, i) 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) diff --git a/helm/software/helena/src/basic_rg/brgCrg.ml b/helm/software/helena/src/basic_rg/brgCrg.ml index 1715494d4..645610dd4 100644 --- a/helm/software/helena/src/basic_rg/brgCrg.ml +++ b/helm/software/helena/src/basic_rg/brgCrg.ml @@ -18,25 +18,25 @@ module B = Brg (* 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 @@ -47,25 +47,25 @@ and xlate_bind f a b t = match b with (* 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 diff --git a/helm/software/helena/src/basic_rg/brgELPI.ml b/helm/software/helena/src/basic_rg/brgELPI.ml index 0ead75280..969cb8ae9 100644 --- a/helm/software/helena/src/basic_rg/brgELPI.ml +++ b/helm/software/helena/src/basic_rg/brgELPI.ml @@ -24,7 +24,7 @@ module B = Brg let ok = ref true -let level = ref 0 +let uris = ref [] let base = "elpi" @@ -74,7 +74,7 @@ let out_name och a = 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 @@ -83,12 +83,13 @@ let rec out_term st e och = function 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" @@ -107,35 +108,75 @@ let rec out_term st e och = function 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 diff --git a/helm/software/helena/src/basic_rg/brgELPI.mli b/helm/software/helena/src/basic_rg/brgELPI.mli index d96b7f45d..96c16ec37 100644 --- a/helm/software/helena/src/basic_rg/brgELPI.mli +++ b/helm/software/helena/src/basic_rg/brgELPI.mli @@ -9,4 +9,6 @@ \ / 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 diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml index c886c27f4..caa8ab465 100644 --- a/helm/software/helena/src/basic_rg/brgGallina.ml +++ b/helm/software/helena/src/basic_rg/brgGallina.ml @@ -85,15 +85,15 @@ let rec out_term st p e och = function 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", " =>" diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml index e6b8cd8da..71b189dac 100644 --- a/helm/software/helena/src/basic_rg/brgGrafite.ml +++ b/helm/software/helena/src/basic_rg/brgGrafite.ml @@ -80,14 +80,14 @@ let rec out_term st p e och = function 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 -> "∀" diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index ac873ec66..5153ced07 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -63,9 +63,9 @@ let rec count_term_binder f c e = function 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 -> @@ -73,22 +73,22 @@ and count_term f c e = function | _, _, _, 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 @@ -155,12 +155,12 @@ let rec pp_term st e och = function 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 diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index bb31fc976..6c5ac1e98 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -55,21 +55,21 @@ let zero = Some 0 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 @@ -92,7 +92,7 @@ let get m i = (* 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) -> @@ -102,7 +102,7 @@ let rec step st m r = | 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 @@ -138,7 +138,7 @@ let rec step st m r = 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 @@ -183,7 +183,7 @@ let push m a b = {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 @@ -238,6 +238,15 @@ and ac_stacks st m1 m2 = 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 = { @@ -249,12 +258,11 @@ let get m i = 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 diff --git a/helm/software/helena/src/basic_rg/brgSubstitution.ml b/helm/software/helena/src/basic_rg/brgSubstitution.ml index fe5915f74..5661982a3 100644 --- a/helm/software/helena/src/basic_rg/brgSubstitution.ml +++ b/helm/software/helena/src/basic_rg/brgSubstitution.ml @@ -18,22 +18,22 @@ let rec icm a = function | 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 diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index 929dcbce8..15b0b851c 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -55,8 +55,9 @@ let assert_convertibility err f st m u w v = 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), _) -> @@ -65,32 +66,32 @@ let assert_applicability err f st m u w v = 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 @@ -99,28 +100,28 @@ let rec b_type_of err f st m r = | _ -> 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 @@ -128,4 +129,4 @@ let rec b_type_of err f st m r = (* 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 diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index 8425774d2..877fee9d8 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -44,7 +44,7 @@ let validate err f st e = 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 diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml index ad4154fc1..c616b22df 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.ml +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -46,41 +46,42 @@ let zero = Some 0 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 @@ -89,8 +90,8 @@ let rec b_validate err f st m x = | 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) -> @@ -100,4 +101,4 @@ let rec b_validate err f st m x = (* 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 diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml index ede703d6d..1ad6cf28c 100644 --- a/helm/software/helena/src/common/layer.ml +++ b/helm/software/helena/src/common/layer.ml @@ -85,18 +85,18 @@ let rec generated st h i = 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 @@ -106,12 +106,12 @@ let assert_finite st n j = 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) @@ -132,19 +132,19 @@ let one = finite 1 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)) @@ -163,14 +163,14 @@ let to_string st n = 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 @@ -186,9 +186,9 @@ let assert_equal st n1 n2 = | 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 = diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index 77a7e2c25..ffef0796e 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -20,7 +20,8 @@ type kernel = V4 | V3 | V0 type manager = Quiet | Coq | Matita - | ELPI + | ELPI1 + | ELPI2 (* interface functions ******************************************************) @@ -30,6 +31,8 @@ let stage = ref 3 (* stage *) 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 *) @@ -62,6 +65,15 @@ let preamble = ref "" (* preamble file for manager *) 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" @@ -69,7 +81,8 @@ let kernel_id () = | 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; "" ] @@ -79,8 +92,8 @@ let get_mk_uri () = 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 diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index d84012c2f..94bf217da 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -43,11 +43,13 @@ let add ?(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; diff --git a/helm/software/helena/src/complete_rg/crg.ml b/helm/software/helena/src/complete_rg/crg.ml index ae1a81222..ea3ec54bf 100644 --- a/helm/software/helena/src/complete_rg/crg.ml +++ b/helm/software/helena/src/complete_rg/crg.ml @@ -20,22 +20,22 @@ type uri = E.uri 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 @@ -45,43 +45,43 @@ let empty_lenv = ESort 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 @@ -94,7 +94,7 @@ let rec get e i = match e with | 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 @@ -108,19 +108,19 @@ let rec fold_names f map x = function | _ -> 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 diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index dc5d78ce1..95c3e8801 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -48,33 +48,33 @@ let initial_counters = { } 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 @@ -137,22 +137,22 @@ let pp_attrs out a = 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 "} " diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml index 974145812..b2d0c99e1 100644 --- a/helm/software/helena/src/text/txtCrg.ml +++ b/helm/software/helena/src/text/txtCrg.ml @@ -25,6 +25,7 @@ type status = { 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 *) } @@ -80,7 +81,7 @@ let rec xlate_term f st lenv = function 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) -> @@ -89,7 +90,7 @@ let rec xlate_term f st lenv = function 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 @@ -171,7 +172,7 @@ let xlate_entity err f gen st = function 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 diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 3ce7bbc70..984933290 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -236,7 +236,7 @@ let process_2 st entity = | 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 @@ -313,10 +313,11 @@ let main = 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; @@ -335,7 +336,8 @@ let main = 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 (); @@ -357,12 +359,12 @@ let main = if !G.trace >= 1 then Y.utime_stamp "at exit" in let help = - "Usage: helena [ -LPVXdgilopqtx1 | -Ts | -MO | -c | -ahkmr ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXdgilnopqtx1 | -Ts | -MO | -c | -ahkmr | -be ]* [ ]*\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 = " set location of output directory (manager) to (default: current directory)" in @@ -373,20 +375,23 @@ let main = let help_X = " clear options" in let help_a = " set prefix of numeric identifiers (default: empty)" in + let help_b = " begin trace at this global constant (default: first)" in let help_c = " set preamble to this file (default: empty)" in let help_d = " show summary information (requires trace >= 2)" in + let help_e = " end trace at this global constant (default: last)" in let help_g = " always expand global definitions" in let help_h = " set type hierarchy (default: \"Z1\")" in let help_i = " show local references by index" in let help_k = " 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 = " 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 = " set initial segment of URI hierarchy (default: empty)" in let help_s = " 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 @@ -400,14 +405,17 @@ let main = ("-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); diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index f04930851..b5e3b9b40 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -27,9 +27,9 @@ let lenv_iter map_bind map_appl map_proj st e lenv out tab = (* 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) @@ -61,9 +61,9 @@ let rec exp_term st e t out tab = match t with 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 @@ -75,9 +75,9 @@ let rec exp_term st e t out tab = match t with 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) -> diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index 584dc776a..3c77fe68b 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -75,7 +75,7 @@ let gref = "GRef" let cast = "Cast" -let appl = "Appl" +let appl x = if x then "Appx" else "Appr" let proj = "Proj" diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index ed7901f57..4ac5dc913 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -27,7 +27,7 @@ val gref: string val cast: string -val appl: string +val appl: bool -> string val proj: string