From: Ferruccio Guidi Date: Sun, 30 Nov 2008 18:23:11 +0000 (+0000) Subject: lambda-delta/toplevel: improved transformation from automath (20 secs gained) X-Git-Tag: make_still_working~4475 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f870943aedc6ef6f51be134ed3e82bbc03b3eea1;p=helm.git lambda-delta/toplevel: improved transformation from automath (20 secs gained) bug fix in the default arguments specification reverse indexes are now supported transcript: unused parser productions removed --- diff --git a/helm/software/components/binaries/transcript/Makefile b/helm/software/components/binaries/transcript/Makefile index 4bcb2d53f..9ac3969b6 100644 --- a/helm/software/components/binaries/transcript/Makefile +++ b/helm/software/components/binaries/transcript/Makefile @@ -73,7 +73,7 @@ depend.opt: .depend.opt %.cmo %.cmi: %.ml $(EXTRAS) $(LIBRARIES) @echo " OCAMLC $<" $(H)$(OCAMLC) -c $< -%.cmx: %.ml $(EXTRAS) $(LIBRARIES_OPT) +%.o %.cmx %.cmi: %.ml $(EXTRAS) $(LIBRARIES_OPT) @echo " OCAMLOPT $<" $(H)$(OCAMLOPT) -c $< %.ml %.mli: %.mly $(EXTRAS) @@ -83,8 +83,6 @@ depend.opt: .depend.opt @echo " OCAMLLEX $<" $(H)$(OCAMLLEX) $< -include ../../../Makefile.defs - ifeq ($(MAKECMDGOALS),) include .depend endif diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly index 721cdd141..8bba4fb0b 100644 --- a/helm/software/components/binaries/transcript/v8Parser.mly +++ b/helm/software/components/binaries/transcript/v8Parser.mly @@ -100,10 +100,7 @@ ind: IND spcs { $1 ^ $2 }; set: SET spcs { $1 ^ $2 }; notation: NOT spcs { $1 ^ $2 }; - oc: OC spcs { $1 ^ $2 }; - coe: COE spcs { $1 ^ $2 }; cn: CN spcs { $1 ^ $2 }; - sc: SC spcs { $1 ^ $2 }; str: STR spcs { $1 ^ $2 }; id: ID spcs { $1 ^ $2 }; coerc: COERC spcs { $1 ^ $2 }; @@ -372,6 +369,10 @@ /* + oc: OC spcs { $1 ^ $2 }; + coe: COE spcs { $1 ^ $2 }; + sc: SC spcs { $1 ^ $2 }; + cnot: | EXTRA { $1 } | INT { $1 } diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 3ae365e6d..60e0390bd 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -8,18 +8,18 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi automath/autLexer.cmo: automath/autParser.cmi automath/autLexer.cmx: automath/autParser.cmx -toplevel/meta.cmo: automath/aut.cmx -toplevel/meta.cmx: automath/aut.cmx +toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx +toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx toplevel/metaOutput.cmi: toplevel/meta.cmx -toplevel/metaOutput.cmo: toplevel/meta.cmx lib/cps.cmx \ +toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \ toplevel/metaOutput.cmi -toplevel/metaOutput.cmx: toplevel/meta.cmx lib/cps.cmx \ +toplevel/metaOutput.cmx: lib/nUri.cmx toplevel/meta.cmx lib/cps.cmx \ toplevel/metaOutput.cmi toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx -toplevel/metaAut.cmo: toplevel/meta.cmx lib/cps.cmx automath/aut.cmx \ - toplevel/metaAut.cmi -toplevel/metaAut.cmx: toplevel/meta.cmx lib/cps.cmx automath/aut.cmx \ - toplevel/metaAut.cmi +toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \ + automath/aut.cmx toplevel/metaAut.cmi +toplevel/metaAut.cmx: lib/nUri.cmx toplevel/meta.cmx lib/cps.cmx \ + automath/aut.cmx toplevel/metaAut.cmi toplevel/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaAut.cmi \ lib/cps.cmx automath/autParser.cmi automath/autOutput.cmi \ automath/autLexer.cmx diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml index 4b04e3af8..af3f9b0af 100644 --- a/helm/software/lambda-delta/toplevel/meta.ml +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -23,19 +23,19 @@ * http://cs.unibo.it/helm/. *) -type id = Aut.id +type uri = NUri.uri -type qid = id * id list (* qualified identifier: name, qualifiers *) +type id = Aut.id type term = Sort of bool (* sorts: true = TYPE, false = PROP *) - | LRef of int (* local reference: de bruijn index *) - | GRef of int * qid * term list (* global reference: context length, name, arguments *) + | LRef of int * int (* local reference: context length, de bruijn index *) + | GRef of int * uri * term list (* global reference: context length, name, arguments *) | Appl of term * term (* application: argument, function *) | Abst of id * term * term (* abstraction: name, type, body *) -type pars = (qid * term) list (* parameter declarations: name, type *) +type pars = (id * term) list (* parameter declarations: name, type *) (* entry: line number, parameters, name, type, (transparent?, body) *) -type entry = int * pars * qid * term * (bool * term) option +type entry = int * pars * uri * term * (bool * term) option type item = entry option 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 diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 7a15d07c2..a12818ee3 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -24,6 +24,7 @@ *) module F = Format +module U = NUri module M = Meta type counters = { @@ -103,10 +104,6 @@ let string_of_sort = function | true -> "Type" | false -> "Prop" -let string_of_qid (id, path) = - let path = String.concat "/" path in - Filename.concat path id - let string_of_transparent = function | true -> "=" | false -> "~" @@ -124,17 +121,17 @@ let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args and pp_term frm = function | M.Sort s -> F.fprintf frm "@[*%s@]" (string_of_sort s) - | M.LRef i -> - F.fprintf frm "@[#%u@]" i - | M.GRef (l, qid, ts) -> - F.fprintf frm "@[%u@@$%s%a@]" l (string_of_qid qid) pp_args ts + | M.LRef (l, i) -> + F.fprintf frm "@[%u@@#%u@]" l i + | M.GRef (l, uri, ts) -> + F.fprintf frm "@[%u@@$%s%a@]" l (U.string_of_uri uri) pp_args ts | M.Appl (v, t) -> F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t | M.Abst (id, w, t) -> F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t -let pp_par frm (qid, w) = - F.fprintf frm "%s:%a" (string_of_qid qid) pp_term w +let pp_par frm (id, w) = + F.fprintf frm "%s:%a" id pp_term w let pp_pars = pp_list pp_par "[" "," "]" @@ -143,9 +140,9 @@ let pp_body frm = function | Some (trans, t) -> F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t -let pp_entry frm (l, pars, qid, u, body) = +let pp_entry frm (l, pars, uri, u, body) = F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" - l (string_of_qid qid) pp_pars pars pp_body body pp_term u + l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u let pp_item f frm = function | Some entry -> pp_entry frm entry; f ()