X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2FdrgAut.ml;h=aa6cf5d9766649c92d474caa2f4ac18b14925fb1;hb=d88c6bdb650d69ffccac2031cecf7a50cd7e6917;hp=3b371afd72a5371a2804d4b623ad4df36f6e2d0f;hpb=552427acaacc2ebd0737c2b6038085f7ea5f423b;p=helm.git diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml index 3b371afd7..aa6cf5d97 100644 --- a/helm/software/lambda-delta/dual_rg/drgAut.ml +++ b/helm/software/lambda-delta/dual_rg/drgAut.ml @@ -12,42 +12,50 @@ module U = NUri module H = U.UriHash module C = Cps -module E = Entity +module Y = Entity module A = Aut module D = Drg (* qualified identifier: uri, name, qualifiers *) type qid = D.uri * D.id * D.id list -type environment = D.lenv H.t +type context = Y.attrs * D.term list type context_node = qid option (* context node: None = root *) -type 'b status = { - henv: environment; (* optimized global environment *) +type status = { path: D.id list; (* current section path *) - hcnt: environment; (* optimized context *) node: context_node; (* current context node *) nodes: context_node list; (* context node list *) line: int; (* line number *) - mk_uri:'b E.uri_generator (* uri generator *) + mk_uri:Y.uri_generator (* uri generator *) } type resolver = Local of int - | Global of D.lenv + | Global of context -let hsize = 7000 (* hash tables initial size *) +let henv_size, hcnt_size = 7000, 4300 (* hash tables initial sizes *) + +let henv = H.create henv_size (* optimized global environment *) + +let hcnt = H.create hcnt_size (* optimized context *) (* Internal functions *******************************************************) -let initial_status size mk_uri = { - path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri; - henv = H.create size; hcnt = H.create size +let initial_status mk_uri = + H.clear henv; H.clear hcnt; { + path = []; node = None; nodes = []; line = 1; mk_uri = mk_uri } -let mk_lref f i = f (D.LRef ([], i)) +let empty_cnt = [], [] + +let add_abst (a, ws) id w = + Y.Name (id, true) :: a, w :: ws + +let lenv_of_cnt (a, ws) = + D.push_bind C.start D.empty_lenv a (D.Abst ws) -let mk_abst id w = D.Abst ([D.Name (id, true)], w) +let mk_lref f i j k = f (D.TLRef ([Y.Apix k], i, j)) let id_of_name (id, _, _) = id @@ -55,7 +63,7 @@ let mk_qid f st id path = let str = String.concat "/" path in let str = Filename.concat str id in let f str = f (U.uri_of_string str, id, path) in - st.mk_uri f str + f (st.mk_uri str) let uri_of_qid (uri, _, _) = uri @@ -80,108 +88,113 @@ let relax_opt_qid f st = function | Some qid -> let f qid = f (Some qid) in relax_qid f st qid let resolve_gref err f st qid = - try let cnt = H.find st.henv (uri_of_qid qid) in f qid cnt - with Not_found -> err () + try let cnt = H.find henv (uri_of_qid qid) in f qid cnt + with Not_found -> err qid let resolve_gref_relaxed f st qid = - let rec err () = relax_qid (resolve_gref err f st) st qid in +(* 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 get_cnt err f st = function - | None -> f [] + | None -> f empty_cnt | Some qid as node -> - try let cnt = H.find st.hcnt (uri_of_qid qid) in f cnt + try let cnt = H.find hcnt (uri_of_qid qid) in f cnt with Not_found -> err node let get_cnt_relaxed f st = +(* 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 +(* this is not tail recursive in the GRef branch *) let rec xlate_term f st lenv = function | A.Sort s -> - let f h = f (D.Sort ([], h)) in + let f h = f (D.TSort ([], h)) in if s then f 0 else f 1 | A.Appl (v, t) -> - let f vv tt = f (D.Appl ([], [vv], tt)) in + let f vv tt = f (D.TAppl ([], [vv], tt)) in let f vv = xlate_term (f vv) st lenv t in xlate_term f st lenv v | A.Abst (name, w, t) -> let f ww = - let b = mk_abst name ww in - let f tt = f (D.Bind ([b], tt)) in - xlate_term f st (b :: lenv) t + let a, b = [Y.Name (name, true)], (D.Abst [ww]) in + let f tt = f (D.TBind (a, b, tt)) in + let f lenv = xlate_term f st lenv t in + D.push_bind f lenv a b in xlate_term f st lenv w | A.GRef (name, args) -> - let g qid cnt = - let map1 f = xlate_term f st lenv in - let map2 f b = - let f id _ = D.resolve_lref Cps.err (mk_lref f) id lenv in - D.name_of_binder C.err f b - in - let f tail = - let f args = f (D.Appl ([], args, D.GRef ([], uri_of_qid qid))) in - let f cnt = C.list_rev_map_append f map2 cnt ~tail in - C.list_sub_strict f cnt args - in - C.list_map f map1 args + let map1 f = function + | Y.Name (id, _) -> f (A.GRef ((id, true, []), [])) + | _ -> C.err () + in + let map2 f = xlate_term f st lenv in + let g qid (a, _) = + let gref = D.TGRef ([], uri_of_qid qid) in + match args with + | [] -> f gref + | args -> + let f args = f (D.TAppl ([], args, gref)) in + let f args = f (List.rev_map (map2 C.start) args) in + let f a = C.list_rev_map_append f map1 a ~tail:args in + C.list_sub_strict f a args in let g qid = resolve_gref_relaxed g st qid in let err () = complete_qid g st name in D.resolve_lref err (mk_lref f) (id_of_name name) lenv -let xlate_entity f st = function +let xlate_entity err f st = function | A.Section (Some (_, name)) -> - f {st with path = name :: st.path; nodes = st.node :: st.nodes} None + err {st with path = name :: st.path; nodes = st.node :: st.nodes} | A.Section None -> begin match st.path, st.nodes with | _ :: ptl, nhd :: ntl -> - f {st with path = ptl; node = nhd; nodes = ntl} None + err {st with path = ptl; node = nhd; nodes = ntl} | _ -> assert false end | A.Context None -> - f {st with node = None} None + err {st with node = None} | A.Context (Some name) -> - let f name = f {st with node = Some name} None in + let f name = err {st with node = Some name} in complete_qid f st name | A.Block (name, w) -> let f qid = let f cnt = - let f ww = - H.add st.hcnt (uri_of_qid qid) (mk_abst name ww :: cnt); - f {st with node = Some qid} None - in - xlate_term f st cnt w + let lenv = lenv_of_cnt cnt in + let ww = xlate_term C.start st lenv w in + H.add hcnt (uri_of_qid qid) (add_abst cnt name ww); + err {st with node = Some qid} in get_cnt_relaxed f st in complete_qid f st (name, true, []) | A.Decl (name, w) -> - let f cnt = - let f qid = - let f ww = - let b = D.Abst ([], D.Bind (cnt, ww)) in - let entry = st.line, uri_of_qid qid, b in - H.add st.henv (uri_of_qid qid) cnt; - f {st with line = succ st.line} (Some entry) - in - xlate_term f st cnt w + let f cnt = + let a, ws = cnt in + let lenv = lenv_of_cnt cnt in + let f qid = + let ww = xlate_term C.start st lenv w in + H.add henv (uri_of_qid qid) cnt; + let b = Y.Abst (D.TBind (a, D.Abst ws, ww)) in + let entity = [Y.Mark st.line], uri_of_qid qid, b in + f {st with line = succ st.line} entity in complete_qid f st (name, true, []) in get_cnt_relaxed f st | A.Def (name, w, trans, v) -> let f cnt = + let a, ws = cnt in + let lenv = lenv_of_cnt cnt in let f qid = - let f ww vv = - let a = if trans then [] else [D.Priv] in - let b = D.Abbr (a, D.Bind (cnt, D.Cast ([], ww, vv))) in - let entry = st.line, uri_of_qid qid, b in - H.add st.henv (uri_of_qid qid) cnt; - f {st with line = succ st.line} (Some entry) - in - let f ww = xlate_term (f ww) st cnt v in - xlate_term f st cnt w + let ww = xlate_term C.start st lenv w in + let vv = xlate_term C.start st lenv v in + H.add henv (uri_of_qid qid) cnt; + let b = Y.Abbr (D.TBind (a, D.Abst ws, D.TCast ([], ww, vv))) in + let a = Y.Mark st.line :: if trans then [] else [Y.Priv] in + let entity = a, uri_of_qid qid, b in + f {st with line = succ st.line} entity in complete_qid f st (name, true, []) in @@ -190,6 +203,6 @@ let xlate_entity f st = function (* Interface functions ******************************************************) let initial_status mk_uri = - initial_status hsize mk_uri + initial_status mk_uri let drg_of_aut = xlate_entity