X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaAut.ml;h=767a44afb4c8b313c744f6976f366ac976771e76;hb=f870943aedc6ef6f51be134ed3e82bbc03b3eea1;hp=031e74cf2a731b17b7c5dc113c1e0b67b6266d01;hpb=761967afe1bd46b21a6bd69232bf09e1658b0734;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 031e74cf2..767a44afb 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -24,13 +24,15 @@ *) module H = Hashtbl - +module U = NUri module M = Meta module A = Aut -type environment = (M.qid, M.pars) H.t +type qid = M.id * M.id list (* qualified identifier: name, qualifiers *) + +type environment = (qid, M.pars) H.t -type context_node = M.qid option (* context node: None = root *) +type context_node = qid option (* context node: None = root *) type status = { henv: environment; (* optimized global environment *) @@ -54,6 +56,13 @@ let initial_status size = { henv = H.create size; hcnt = H.create size } +let id_of_name (id, _, _) = id + +let uri_of_qid (id, path) = + let path = String.concat "/" path in + let str = Filename.concat path id in + U.uri_of_string ("ld:/" ^ str) + let complete_qid f st (id, is_local, qs) = let f qs = f (id, qs) in let f path = Cps.list_rev_append f path ~tail:qs in @@ -76,33 +85,31 @@ let relax_opt_qid f = function | None -> f None | Some qid -> let f qid = f (Some qid) in relax_qid f qid -let resolve_gref f st local lenv gref = - let rec get_local f i = function - | [] -> f None - | (name, _) :: _ when fst name = fst gref -> f (Some i) - | _ :: tl -> get_local f (succ i) tl - in - let get_global f = - try - let args = H.find st.henv gref in f (Some args) - with Not_found -> f None - in - let g = function - | Some args -> f gref (Some (Global args)) - | None -> f gref None - in - let f = function - | Some i -> f gref (Some (Local i)) - | None -> get_global g - in - if local then get_local f 0 lenv else f None - -let resolve_gref_relaxed f st lenv gref = - let rec g gref = function - | None -> relax_qid (resolve_gref g st false lenv) gref - | Some resolved -> f gref resolved +let resolve_lref f st l lenv id = + let rec aux f i = function + | [] -> f None + | (name, _) :: _ when name = id -> f (Some (M.LRef (l, i))) + | _ :: tl -> aux f (succ i) tl + in + aux f 0 lenv + +let resolve_lref_strict f st l lenv id = + let f = function + | Some t -> f t + | None -> assert false in - resolve_gref g st true lenv gref + resolve_lref f st l lenv id + +let resolve_gref f st qid = + try let args = H.find st.henv qid in f qid (Some args) + with Not_found -> f qid None + +let resolve_gref_relaxed f st qid = + let rec g qid = function + | None -> relax_qid (resolve_gref g st) qid + | Some args -> f qid args + in + resolve_gref g st qid let get_pars f st = function | None -> f [] None @@ -118,35 +125,35 @@ let get_pars_relaxed f st = get_pars g st st.node let rec xlate_term f st lenv = function - | A.Sort sort -> f (M.Sort sort) + | A.Sort sort -> + f (M.Sort sort) | A.Appl (v, t) -> let f vv tt = f (M.Appl (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 add name w lenv = - let f name = (name, w) :: lenv in - complete_qid f st (name, true, []) - in + let add name w lenv = (name, w) :: lenv in let f ww tt = f (M.Abst (name, ww, tt)) in let f ww = xlate_term (f ww) st (add name ww lenv) t in xlate_term f st lenv w | A.GRef (name, args) -> - let f name = function - | Local i -> f (M.LRef i) - | Global defs -> - let l = List.length lenv in - let map1 f = xlate_term f st lenv in - let map2 f (name, _) = f (M.GRef (l, name, [])) in - let f tail = - let f args = f (M.GRef (l, name, args)) in - let f defs = Cps.list_rev_map_append f map2 defs ~tail in - Cps.list_sub_strict f defs args - in - Cps.list_map f map1 args + let l = List.length lenv in + let g qid defs = + let map1 f = xlate_term f st lenv in + let map2 f (id, _) = resolve_lref_strict f st l lenv id in + let f tail = + let f args = f (M.GRef (l, uri_of_qid qid, args)) in + let f defs = Cps.list_rev_map_append f map2 defs ~tail in + Cps.list_sub_strict f defs args + in + Cps.list_map f map1 args + in + let g qid = resolve_gref_relaxed g st qid in + let f = function + | Some t -> f t + | None -> complete_qid g st name in - let f name = resolve_gref_relaxed f st lenv name in - complete_qid f st name + resolve_lref f st l lenv (id_of_name name) let xlate_item f st = function | A.Section (Some name) -> @@ -163,11 +170,11 @@ let xlate_item f st = function let f name = f {st with node = Some name} None in complete_qid f st name | A.Block (name, w) -> - let f name = + let f qid = let f pars = let f ww = - H.add st.hcnt name ((name, ww) :: pars); - f {st with node = Some name} None + H.add st.hcnt qid ((name, ww) :: pars); + f {st with node = Some qid} None in xlate_term f st pars w in @@ -176,10 +183,10 @@ let xlate_item f st = function complete_qid f st (name, true, []) | A.Decl (name, w) -> let f pars = - let f name = + let f qid = let f ww = - let entry = (st.line, pars, name, ww, None) in - H.add st.henv name pars; + let entry = (st.line, pars, uri_of_qid qid, ww, None) in + H.add st.henv qid pars; f {st with line = succ st.line} (Some entry) in xlate_term f st pars w @@ -189,10 +196,10 @@ let xlate_item f st = function get_pars_relaxed f st | A.Def (name, w, trans, v) -> let f pars = - let f name = + let f qid = let f ww vv = - let entry = (st.line, pars, name, ww, Some (trans, vv)) in - H.add st.henv name pars; + let entry = (st.line, pars, uri_of_qid qid, ww, Some (trans, vv)) in + H.add st.henv qid pars; f {st with line = succ st.line} (Some entry) in let f ww = xlate_term (f ww) st pars v in