From: Ferruccio Guidi Date: Mon, 24 Nov 2014 23:07:39 +0000 (+0000) Subject: - static disambiguation of Automath unified binders X-Git-Tag: make_still_working~794 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39cf453a20e35416d0fd932cc5bf14733e918587;p=helm.git - static disambiguation of Automath unified binders by position heuristics + degree heuristics fixed [ grundlagen_2: now 1217 binders out of 47115 remain ambiguous ] - brgReduction: we did not check the sort-inclusion flag - new constraints system continues ... --- diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index abec72608..d82862170 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -33,8 +33,8 @@ src/common/ccs.cmo: src/common/options.cmx src/common/entity.cmx \ src/lib/cps.cmx src/common/ccs.cmi src/common/ccs.cmx: src/common/options.cmx src/common/entity.cmx \ src/lib/cps.cmx src/common/ccs.cmi -src/common/status.cmo: src/common/options.cmx src/common/ccs.cmi -src/common/status.cmx: src/common/options.cmx src/common/ccs.cmx +src/common/status.cmo: src/common/options.cmx src/common/level.cmi +src/common/status.cmx: src/common/options.cmx src/common/level.cmx src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx \ src/lib/cps.cmx src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx \ @@ -88,13 +88,16 @@ src/automath/autLexer.cmo: src/common/options.cmx src/lib/log.cmi \ src/automath/autParser.cmi src/automath/autLexer.cmx: src/common/options.cmx src/lib/log.cmx \ src/automath/autParser.cmx -src/automath/autCrg.cmi: src/complete_rg/crg.cmx src/automath/aut.cmx -src/automath/autCrg.cmo: src/common/options.cmx src/common/marks.cmi \ - src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ - src/lib/cps.cmx src/automath/aut.cmx src/automath/autCrg.cmi -src/automath/autCrg.cmx: src/common/options.cmx src/common/marks.cmx \ - src/common/level.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ - src/lib/cps.cmx src/automath/aut.cmx src/automath/autCrg.cmi +src/automath/autCrg.cmi: src/common/status.cmx src/complete_rg/crg.cmx \ + src/automath/aut.cmx +src/automath/autCrg.cmo: src/common/status.cmx src/common/options.cmx \ + src/common/marks.cmi src/common/level.cmi src/common/entity.cmx \ + src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \ + src/automath/autCrg.cmi +src/automath/autCrg.cmx: src/common/status.cmx src/common/options.cmx \ + src/common/marks.cmx src/common/level.cmx src/common/entity.cmx \ + src/complete_rg/crg.cmx src/lib/cps.cmx src/automath/aut.cmx \ + src/automath/autCrg.cmi src/xml/xmlLibrary.cmi: src/common/level.cmi src/common/entity.cmx src/xml/xmlLibrary.cmo: src/common/options.cmx src/common/level.cmi \ src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 48e34b90f..0c840fbfb 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -21,8 +21,8 @@ INPUT = examples/grundlagen/grundlagen_2.aut INPUTFAST = examples/grundlagen/grundlagen_1.aut test-si: $(MAIN).opt etc - @echo " HELENA -p -o -c $(INPUT)" - $(H)./$(MAIN).opt -T 2 -p -o -c -O $(XMLDIR) $(O) $(INPUT) > etc/log.txt + @echo " HELENA -d -l -p -o $(INPUT)" + $(H)./$(MAIN).opt -T 2 -d -l -p -o $(O) $(INPUT) > etc/log.txt test-si-fast: $(MAIN).opt etc @echo " HELENA -o -q $(INPUTFAST)" @@ -35,9 +35,9 @@ profile: $(MAIN).opt etc $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt xml-si: $(MAIN).opt etc - @echo " HELENA -o -x -s 2 $(INPUT)" - $(H)./$(MAIN).opt -T 1 -o -x -s 2 -O $(XMLDIR) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 2 -x $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -x $(INPUT) > etc/log.txt xml-si-crg: $(MAIN).opt etc - @echo " HELENA -o -x -s 1 $(INPUT)" - $(H)./$(MAIN).opt -T 1 -o -x -s 1 -O $(XMLDIR) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 1 -x $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -x $(INPUT) > etc/log.txt diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 9093ffbb2..69a8c072d 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -12,10 +12,11 @@ module U = NUri module K = U.UriHash module C = Cps -module G = Options module J = Marks module N = Level module E = Entity +module G = Options +module S = Status module A = Aut module D = Crg @@ -30,7 +31,6 @@ type status = { nodes: context_node list; (* context node list *) line: int; (* line number *) mk_uri: G.uri_generator; (* uri generator *) - lenv: N.status; (* level environment *) } let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) @@ -43,60 +43,61 @@ let hcnt = K.create hcnt_size (* optimized context *) let empty_cnt = D.ESort -let add_abst cnt id w = - D.EBind (cnt, E.node_attrs ~name:(id, true) (), D.Abst (N.two, w)) +let add_abst cnt id d w = + let a = E.node_attrs ~name:(id, true) ~degr:(succ d) () in + D.EBind (cnt, a, D.Abst (N.two, w)) let mk_lref f a i = f a.E.n_degr (D.TLRef (E.empty_node, i)) let id_of_name (id, _, _) = id -let mk_qid f st id path = +let mk_qid f lst id path = let str = String.concat "/" path in let str = Filename.concat str id in - let str = st.mk_uri str in + let str = lst.mk_uri str in f (U.uri_of_string str, id, path) let uri_of_qid (uri, _, _) = uri -let complete_qid f st (id, is_local, qs) = - let f path = C.list_rev_append (mk_qid f st id) path ~tail:qs in +let complete_qid f lst (id, is_local, qs) = + let f path = C.list_rev_append (mk_qid f lst id) path ~tail:qs in let rec skip f = function | phd :: ptl, qshd :: _ when phd = qshd -> f ptl | _ :: ptl, _ :: _ -> skip f (ptl, qs) | _ -> f [] in - if is_local then f st.path else skip f (st.path, qs) + if is_local then f lst.path else skip f (lst.path, qs) -let relax_qid f st (_, id, path) = +let relax_qid f lst (_, id, path) = let f = function - | _ :: tl -> C.list_rev (mk_qid f st id) tl + | _ :: tl -> C.list_rev (mk_qid f lst id) tl | [] -> assert false in C.list_rev f path -let relax_opt_qid f st = function +let relax_opt_qid f lst = function | None -> f None - | Some qid -> let f qid = f (Some qid) in relax_qid f st qid + | Some qid -> let f qid = f (Some qid) in relax_qid f lst qid -let resolve_gref err f st qid = +let resolve_gref err f lst qid = try let a, cnt = K.find henv (uri_of_qid qid) in f qid a cnt with Not_found -> err qid -let resolve_gref_relaxed f st qid = +let resolve_gref_relaxed f lst qid = (* this is not tail recursive *) - let rec err qid = relax_qid (resolve_gref err f st) st qid in - resolve_gref err f st qid + let rec err qid = relax_qid (resolve_gref err f lst) lst qid in + resolve_gref err f lst qid -let get_cnt err f st = function +let get_cnt err f lst = function | None -> f empty_cnt | Some qid as node -> try let cnt = K.find hcnt (uri_of_qid qid) in f cnt with Not_found -> err node -let get_cnt_relaxed f st = +let get_cnt_relaxed f lst = (* this is not tail recursive *) - let rec err node = relax_opt_qid (get_cnt err f st) st node in - get_cnt err f st st.node + let rec err node = relax_opt_qid (get_cnt err f lst) lst node in + get_cnt err f lst lst.node let push_abst f a w lenv = let bw = D.Abst (N.infinite, w) in @@ -108,36 +109,38 @@ let add_proj e t = match e with | _ -> D.TProj (E.empty_node, e, t) (* this is not tail recursive in the GRef branch *) -let rec xlate_term f st lenv = function +let rec xlate_term f st lst y lenv = function | A.Sort s -> let f h = f 0 (D.TSort (E.empty_node, h)) in if s then f 0 else f 1 | A.Appl (v, t) -> let f vv d tt = f d (D.TAppl (E.empty_node, vv, tt)) in - let f _ vv = xlate_term (f vv) st lenv t in - xlate_term f st lenv v + 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) -> let f d ww = let a = E.node_attrs ~name:(name, true) () in let f d tt = - let l = match d with - | 0 -> N.one - | 1 -> N.unknown st.lenv (J.new_mark ()) - | 2 -> N.two - | _ -> assert false + let l = if !G.cc then match y, d with + | true, _ -> N.one + | _ , 0 -> N.one + | _ , 1 -> N.unknown st.S.lenv (J.new_mark ()) + | _ , 2 -> N.two + | _ -> assert false + else N.infinite in let b = D.Abst (l, ww) in f d (D.TBind (a, b, tt)) in - let f lenv = xlate_term f st lenv t in + let f lenv = xlate_term f st lst y lenv t in push_abst f {a with E.n_degr = succ d} ww lenv in - xlate_term f st lenv w + xlate_term f st lst true lenv w | 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 - xlate_term f st lenv arg + xlate_term f st lst false lenv arg in let g qid a cnt = let gref = D.TGRef (a, uri_of_qid qid) in @@ -149,41 +152,41 @@ let rec xlate_term f st lenv = function 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 in - let g qid = resolve_gref_relaxed g st qid in - let err () = complete_qid g st name in + let g qid = resolve_gref_relaxed g lst qid in + let err () = complete_qid g lst name in D.resolve_lref err (mk_lref f) (id_of_name name) lenv -let xlate_entity err f st = function +let xlate_entity err f st lst = function | A.Section (Some (_, name)) -> - err {st with path = name :: st.path; nodes = st.node :: st.nodes} + err {lst with path = name :: lst.path; nodes = lst.node :: lst.nodes} | A.Section None -> - begin match st.path, st.nodes with + begin match lst.path, lst.nodes with | _ :: ptl, nhd :: ntl -> - err {st with path = ptl; node = nhd; nodes = ntl} + err {lst with path = ptl; node = nhd; nodes = ntl} | _ -> assert false end | A.Context None -> - err {st with node = None} + err {lst with node = None} | A.Context (Some name) -> - let f name = err {st with node = Some name} in - complete_qid f st name + let f name = err {lst with node = Some name} in + complete_qid f lst name | A.Block (name, w) -> let f qid = let f cnt = - let f _ ww = - K.add hcnt (uri_of_qid qid) (add_abst cnt name ww); - err {st with node = Some qid} + let f d ww = + K.add hcnt (uri_of_qid qid) (add_abst cnt name d ww); + err {lst with node = Some qid} in - xlate_term f st cnt w + xlate_term f st lst true cnt w in - get_cnt_relaxed f st + get_cnt_relaxed f lst in - complete_qid f st (name, true, []) + complete_qid f lst (name, true, []) | A.Decl (name, w) -> let f lenv = let f qid = let f d ww = - let a = E.node_attrs ~apix:st.line ~degr:(succ d) () in + let a = E.node_attrs ~apix:lst.line ~degr:(succ d) () in K.add henv (uri_of_qid qid) (a, lenv); let t = add_proj lenv ww in (* @@ -191,19 +194,19 @@ let xlate_entity err f st = function *) let b = E.Abst t in let entity = E.empty_root, a, uri_of_qid qid, b in - f {st with line = succ st.line} entity + f {lst with line = succ lst.line} entity in - xlate_term f st lenv w + xlate_term f st lst true lenv w in - complete_qid f st (name, true, []) + complete_qid f lst (name, true, []) in - get_cnt_relaxed f st + get_cnt_relaxed f lst | A.Def (name, w, trans, v) -> let f lenv = let f qid = let f _ ww = let f d vv = - let na = E.node_attrs ~apix:st.line ~degr:d () in + let na = E.node_attrs ~apix:lst.line ~degr:d () in K.add henv (uri_of_qid qid) (na, lenv); let t = add_proj lenv (D.TCast (E.empty_node, ww, vv)) in (* @@ -212,25 +215,24 @@ let xlate_entity err f st = 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 - f {st with line = succ st.line} entity + f {lst with line = succ lst.line} entity in - xlate_term f st lenv v + xlate_term f st lst false lenv v in - xlate_term f st lenv w + xlate_term f st lst true lenv w in - complete_qid f st (name, true, []) + complete_qid f lst (name, true, []) in - get_cnt_relaxed f st + get_cnt_relaxed f lst (* Interface functions ******************************************************) let initial_status () = K.clear henv; K.clear hcnt; { path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri (); - lenv = N.initial_status (); } -let refresh_status st = {st with +let refresh_status lst = {lst with mk_uri = G.get_mk_uri () } diff --git a/helm/software/helena/src/automath/autCrg.mli b/helm/software/helena/src/automath/autCrg.mli index c7d93d3ce..9d58247ea 100644 --- a/helm/software/helena/src/automath/autCrg.mli +++ b/helm/software/helena/src/automath/autCrg.mli @@ -16,4 +16,4 @@ val initial_status: unit -> status val refresh_status: status -> status val crg_of_aut: (status -> 'a) -> (status -> Crg.entity -> 'a) -> - status -> Aut.command -> 'a + Status.status -> status -> Aut.command -> 'a diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index f397c1c6f..c0ff77575 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -205,9 +205,11 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2 else false | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ -> -(* if N.is_zero n then () else Q.add_zero st.S.cc a; *) - if !G.summary then O.add ~si:1 (); - ac st (push m1 a b) t1 (push m2 a b) t + if st.S.si then begin +(* if N.is_zero n then () else Q.add_zero st.S.cc a; *) + if !G.summary then O.add ~si:1 (); + ac st (push m1 a b) t1 (push m2 a b) t + end else false | _ -> false and ac st m1 t1 m2 t2 = diff --git a/helm/software/helena/src/common/level.ml b/helm/software/helena/src/common/level.ml index 60f7ac438..75058cf83 100644 --- a/helm/software/helena/src/common/level.ml +++ b/helm/software/helena/src/common/level.ml @@ -13,23 +13,27 @@ module H = Hashtbl module J = Marks -type level = Inf (* infinite *) - | Fin of int (* finite *) - | Ref of J.mark (* unknown *) +type value = Inf (* infinite level *) + | Fin of int (* finite level *) + | Ref of J.mark (* referred level *) -type const = NotZero (* not zero: beta and whnf allowed *) +type level = bool * value (* static level? value *) -type contents = Value of level (* defined with this level *) +type const = NotZero (* not zero: beta allowed *) + +type contents = Value of value (* defined with this level *) | Const of const list (* undefined with these constraints *) type status = (J.mark, contents) H.t (* environment for level variables *) (* Internal functions *******************************************************) -let env_size = 2000 +let env_size = 1300 let empty_ref = Const [] +let zero = Fin 0 + let find st k = try H.find st k with Not_found -> H.add st k empty_ref; empty_ref @@ -42,30 +46,39 @@ let rec resolve st k = match find st k with let initial_status () = H.create env_size -let infinite = Inf - -let zero = Fin 0 +let infinite = true, Inf -let one = Fin 1 +let one = true, Fin 1 -let two = Fin 2 +let two = true, Fin 2 -let finite i = Fin i +let finite i = true, Fin i let unknown st k = match resolve st k with - | _, Value l -> l - | k, Const _ -> Ref k + | _, Value l -> true, l + | k, Const _ -> true, Ref k -let is_zero l = - l = zero +let to_string = function + | _, Inf -> "" + | _, Fin i -> string_of_int i + | _, Ref k -> "-" ^ J.to_string k +(* +let is_finite j l = + let b, k = l in + match resolve st k with + | k, Value (Fin i) -> + if i <> j then Printf.printf "%s is %u but it must be %u\n" (to_string l) i j; + i = j + | k, Value Inf -> + Printf.printf "%s is infinite but it must be %u\n" j; + + | k, +*) +let is_zero (_, n) = + n = zero let minus n j = match n with - | Inf -> Inf - | Fin i when i > j -> Fin (i - j) - | Fin _ -> zero - | Ref i -> Inf (* assert false *) - -let to_string = function - | Inf -> "" - | Fin i -> string_of_int i - | Ref k -> "-" ^ J.to_string k + | _, Inf -> false, Inf + | _, Fin i when i > j -> false, Fin (i - j) + | _, Fin _ -> false, zero + | _, Ref i -> false, Inf (* assert false *) diff --git a/helm/software/helena/src/common/marks.ml b/helm/software/helena/src/common/marks.ml index 5b45cc79f..b376a2c51 100644 --- a/helm/software/helena/src/common/marks.ml +++ b/helm/software/helena/src/common/marks.ml @@ -11,7 +11,7 @@ type mark = int -let mark = ref 1 +let mark = ref 0 (* interface functions ******************************************************) diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml index a076a9aae..bc04a5afd 100644 --- a/helm/software/helena/src/common/status.ml +++ b/helm/software/helena/src/common/status.ml @@ -9,22 +9,22 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module N = Level module G = Options -module Q = Ccs type status = { - delta: bool; (* global delta-expansion *) - si: bool; (* sort inclusion *) -(* cc: Q.csys; (* conversion constraints *) *) + delta: bool; (* global delta-expansion *) + si: bool; (* sort inclusion *) + lenv: N.status; (* level environment *) } (* helpers ******************************************************************) let initial_status () = { delta = false; - si = !G.si; (* cc = Q.init () *) + si = !G.si; lenv = N.initial_status (); } let refresh_status st = {st with - si = !G.si; (* cc = Q.init () *) + si = !G.si; lenv = N.initial_status (); } diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index d64857d32..72ab254cd 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -229,7 +229,7 @@ let process_0 st entity = | AutEntity e -> let err ast = {st with ast = ast} in let g ast e = process_1 {st with ast = ast} (CrgEntity e) in - AD.crg_of_aut err g st.ast e + AD.crg_of_aut err g st.kst st.ast e | TxtEntity e -> let crr tst = {st with tst = tst} in let d tst e = process_1 {st with tst = tst} (CrgEntity e) in @@ -328,7 +328,7 @@ let main = if !G.trace >= 1 then Y.utime_stamp "at exit" in let help = - "Usage: helena [ -LPVXcdgiopqtx1 | -Ts | -O | -hkr ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXdgilopqtx1 | -Ts | -O | -hkr ]* [ ]*\n\n" ^ "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, \ 3 typing information, 4 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" @@ -340,14 +340,14 @@ let main = let help_V = " show version information" in let help_X = " clear options" in - let help_c = " read/write conversion constraints" in let help_d = " show summary information (requires trace >= 2)" 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: \"brg\")" in - let help_o = " activate sort inclusion" in - let help_p = " preprocess source" in + let help_l = " disambiguate binders level (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 @@ -363,12 +363,12 @@ let main = ("-T", Arg.Int set_trace, help_T); ("-V", Arg.Unit print_version, help_V); ("-X", Arg.Unit clear_options, help_X); - ("-c", Arg.Set G.cc, help_c); ("-d", Arg.Unit set_summary, help_d); ("-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); ("-o", Arg.Set G.si, help_o); ("-p", Arg.Unit set_preprocess, help_p); ("-q", Arg.Set G.unquote, help_q);