From: Ferruccio Guidi Date: Mon, 14 Jul 2008 20:17:22 +0000 (+0000) Subject: lambda-delta: we added the support for position indexes in global references X-Git-Tag: make_still_working~4932 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=591ffe6f23ec9d2a4d368d2c1e7b213986189e44;p=helm.git lambda-delta: we added the support for position indexes in global references we added a pretty printer for the intermediate language librarian : utime stamps now appear only in debug mode --- diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index e79fe6356..8b7bdb09f 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -23,13 +23,15 @@ * http://helm.cs.unibo.it/ *) -let timestamp msg = - let times = Unix.times () in - let msg = Printf.sprintf "UTIMESTAMP (%s): %f" msg times.Unix.tms_utime in - prerr_endline msg - let debug = false;; +let timestamp msg = + if debug then + let times = Unix.times () in + let utime = times.Unix.tms_utime in + let msg = Printf.sprintf "UTIMESTAMP (%s): %f" msg utime in + prerr_endline msg + exception NoRootFor of string let absolutize path = diff --git a/helm/software/lambda-delta/automath/grundlagen.aut b/helm/software/lambda-delta/automath/grundlagen.aut index 34e5493ab..4a856c245 100644 --- a/helm/software/lambda-delta/automath/grundlagen.aut +++ b/helm/software/lambda-delta/automath/grundlagen.aut @@ -1,6 +1,7 @@ # Landau's "Grundlagen der Analysis", formal specification in AUTOMATH # Copyright (C) 1977, L.S. van Benthem Jutting # 1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/) +# 2008, revised by F. Guidi to remove the eta-reductions +l @[a:'prop'][b:'prop'] @@ -224,7 +225,10 @@ i@[o:orec(c,a)] thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b) -iff @[sigma:'type'][p:[x:sigma]'prop'] -all:=p:'prop' +%suggestion by van Daalen to remove the first eta-reduction +%all:=p:'prop' %original line +all:=[x:sigma]p:'prop' +%end of suggestion [a1:all(sigma,p)][s:sigma] alle:=a1:p +all @@ -662,7 +666,10 @@ th6:=th1"e.bij"(sigma,sigma,tau,wissel(s0,t0),f,th3(s0,t0),b):bijective(changef) -e +r a@[b:[x:a]'prop'] -imp:=b:'prop' +%suggestion by van Daalen to remove the second eta-reduction +%imp:=b:'prop' %original line +imp:=[x:a]b:'prop' +%end of suggestion [a1:a][i:imp(a,b)] mp:=i:b +imp diff --git a/helm/software/lambda-delta/automath/grundlagen_pn.aut b/helm/software/lambda-delta/automath/grundlagen_pn.aut deleted file mode 100644 index 0b1462053..000000000 --- a/helm/software/lambda-delta/automath/grundlagen_pn.aut +++ /dev/null @@ -1,89 +0,0 @@ -# Landau's "Grundlagen der Analysis", formal specification in AUTOMATH -# Copyright (C) 1977, L.S. van Benthem Jutting -# 1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/) - -+l -[a:PROP][b:PROP] -imp:=[x,a]b:PROP -@con:=PRIM:PROP -a@not:=imp(con):PROP -wel:=not(not(a)):PROP -[w:wel(a)] -et:=PRIM:a -b@ec:=imp(a,not(b)):PROP -and:=not(ec(a,b)):PROP -@[sigma:TYPE][p:[x,sigma]PROP] -all:=p:PROP -non:=[x,sigma]not(p):[x,sigma]PROP -some:=not(non(p)):PROP -+e -sigma@[s:sigma][t:sigma] -is:=PRIM:PROP -s@refis:=PRIM:is(s,s) -p@[s:sigma][t:sigma][sp:p][i:is(s,t)] -isp:=PRIM:p -p@amone:=[x,sigma][y,sigma][u,p][v,p]is(x,y):PROP -one:=and(amone(sigma,p),some(sigma,p)):PROP -[o1:one(sigma,p)] -ind:=PRIM:sigma -oneax:=PRIM:p -sigma@[tau:TYPE][f:[x,sigma]tau] -injective:=all([x,sigma]all([y,sigma]imp(is(tau,f,f),is(x,y)))):PROP -[t0:tau] -image:=some([x,sigma]is(tau,t0,f)):PROP -tau@[f:[x,sigma]tau][g:[x,sigma]tau][i:[x,sigma]is(tau,f,g)] -fisi:=PRIM:is([x,sigma]tau,f,g) -p@ot:=PRIM:TYPE -[o1:ot] -in:=PRIM:sigma -inp:=PRIM:p -p@otax1:=PRIM:injective(ot,sigma,[x,ot]in(x)) -[s:sigma][sp:p] -otax2:=PRIM:image(ot,sigma,[x,ot]in(x),s) -tau@pairtype:=PRIM:TYPE -[s:sigma][t:tau] -pair:=PRIM:pairtype -tau@[p1:pairtype] -first:=PRIM:sigma -second:=PRIM:tau -pairis1:=PRIM:is(pairtype,pair(first,second),p1) -t@firstis1:=PRIM:is(sigma,first(pair),s) -secondis1:=PRIM:is(tau,second(pair),t) -+st -sigma@set:=PRIM:TYPE -[s:sigma][s0:set] -esti:=PRIM:PROP -p@setof:=PRIM:set -[s:sigma][sp:p] -estii:=PRIM:esti(s,setof(p)) -s@[e:esti(s,setof(p))] -estie:=PRIM:p -sigma@[s0:set][t0:set] -incl:=all([x,sigma]imp(esti(x,s0),esti(x,t0))):PROP -[i:incl(s0,t0)][j:incl(t0,s0)] -isseti:=PRIM:is(set,s0,t0) -+eq -+landau -+n -@nat:=PRIM:TYPE -[x:nat][y:nat] -is:=is(nat,x,y):PROP -nis:=not(is(x,y)):PROP -x@[s:set(nat)] -in:=esti(nat,x,s):PROP -@[p:[x,nat]PROP] -all:=all(nat,p):PROP -@1:=PRIM:nat -suc:=PRIM:[x,nat]nat -ax3:=PRIM:[x,nat]nis(suc,1) -ax4:=PRIM:[x,nat][y,nat][u,is(suc,suc)]is(x,y) -[s:set(nat)] -cond1:=in(1,s):PROP -cond2:=all([x,nat]imp(in(x,s),in(suc,s))):PROP -@ax5:=PRIM:[s,set(nat)][u,cond1(s)][v,cond2(s)][x,nat]in(x,s) --n --landau --eq --st --e --l diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml index a35ecab8b..23f8f52f5 100644 --- a/helm/software/lambda-delta/toplevel/meta.ml +++ b/helm/software/lambda-delta/toplevel/meta.ml @@ -27,13 +27,13 @@ type id = Aut.id type qid = id * id list (* qualified identifier: name, qualifiers *) -type term = Sort of bool (* sorts: true = TYPE, false = PROP *) - | LRef of int (* local reference: de bruijn index *) - | GRef of qid * term list (* global reference: name, arguments *) - | Appl of term * term (* application: argument, function *) - | Abst of id * term * term (* abstraction: name, type, body *) +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 *) + | 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 *) -(* environment: parameters, name, type, (transparent?, body) *) -type environment = (pars * qid * term * (bool * term) option) list +(* environment: line number, parameters, name, type, (transparent?, body) *) +type environment = (int * pars * qid * term * (bool * term) option) list diff --git a/helm/software/lambda-delta/toplevel/metaAut.ml b/helm/software/lambda-delta/toplevel/metaAut.ml index 370bf4cfd..5b85e46cb 100644 --- a/helm/software/lambda-delta/toplevel/metaAut.ml +++ b/helm/software/lambda-delta/toplevel/metaAut.ml @@ -39,6 +39,7 @@ type status = { hcnt: environment; (* optimized context *) node: context_node; (* current context node *) nodes: context_node list; (* context node list *) + line: int; (* line number *) explicit: bool (* need explicit context root? *) } @@ -48,7 +49,7 @@ type resolver = Local of int let hsize = 11 (* hash tables initial size *) let initial_status size = { - genv = []; path = []; node = None; nodes = []; explicit = true; + genv = []; path = []; node = None; nodes = []; line = 1; explicit = true; henv = H.create size; hcnt = H.create size } @@ -133,10 +134,11 @@ let rec xlate_term f st lenv = function let f name = function | Local i -> f (M.LRef i) | Global defs -> - let map1 f = xlate_term f st lenv in - let map2 f (name, _) = f (M.GRef (name, [])) in + 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 (name, args)) in + 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 @@ -175,9 +177,9 @@ let xlate_item f st = function let f pars = let f name = let f ww = - let entry = (pars, name, ww, None) in + let entry = (st.line, pars, name, ww, None) in H.add st.henv name pars; - f {st with genv = entry :: st.genv} + f {st with genv = entry :: st.genv; line = succ st.line} in xlate_term f st pars w in @@ -188,9 +190,9 @@ let xlate_item f st = function let f pars = let f name = let f ww vv = - let entry = (pars, name, ww, Some (trans, vv)) in + let entry = (st.line, pars, name, ww, Some (trans, vv)) in H.add st.henv name pars; - f {st with genv = entry :: st.genv} + f {st with genv = entry :: st.genv; line = succ st.line} in let f ww = xlate_term (f ww) st pars v in xlate_term f st pars w diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 27157de37..4efee4a68 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -23,6 +23,7 @@ * http://cs.unibo.it/helm/. *) +module F = Format module M = Meta type counters = { @@ -43,19 +44,19 @@ let initial_counters = { } let rec count_term f c = function - | M.Sort _ -> + | M.Sort _ -> f {c with tsorts = succ c.tsorts} - | M.LRef _ -> + | M.LRef _ -> f {c with tlrefs = succ c.tlrefs} - | M.GRef (_, ts) -> + | M.GRef (_, _, ts) -> let c = {c with tgrefs = succ c.tgrefs} in let c = {c with pappls = c.pappls + List.length ts} in Cps.list_fold_left f count_term c ts - | M.Appl (v, t) -> + | M.Appl (v, t) -> let c = {c with tappls = succ c.tappls} in let f c = count_term f c t in count_term f c v - | M.Abst (_, w, t) -> + | M.Abst (_, w, t) -> let c = {c with tabsts = succ c.tabsts} in let f c = count_term f c t in count_term f c w @@ -63,12 +64,12 @@ let rec count_term f c = function let count_par f c (_, w) = count_term f c w let count_item f c = function - | pars, _, w, None -> + | _, pars, _, w, None -> let c = {c with eabsts = succ c.eabsts} in let c = {c with pabsts = c.pabsts + List.length pars} in let f c = count_term f c w in Cps.list_fold_left f count_par c pars - | pars, _, w, Some (_, v) -> + | _, pars, _, w, Some (_, v) -> let c = {c with eabbrs = succ c.eabbrs} in let c = {c with pabsts = c.pabsts + List.length pars} in let f c = count_term f c v in @@ -97,7 +98,53 @@ let print_counters f c = Printf.printf " Abstraction items: %6u\n" c.tabsts; flush stdout; f () +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 -> "~" + +let pp_list pp opend sep closed frm l = + let rec aux frm = function + | [] -> () + | [hd] -> pp frm hd + | hd :: tl -> F.fprintf frm "%a%s%a" pp hd sep aux tl + in + if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed + +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.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_pars = pp_list pp_par "[" "," "]" + +let pp_body frm = function + | None -> () + | Some (trans, t) -> + F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t + +let pp_item frm (l, pars, qid, 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 + +let pp_environment f frm genv = + List.iter (pp_item frm) genv; f () diff --git a/helm/software/lambda-delta/toplevel/metaOutput.mli b/helm/software/lambda-delta/toplevel/metaOutput.mli index d0d5766c9..83da0591e 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.mli +++ b/helm/software/lambda-delta/toplevel/metaOutput.mli @@ -30,3 +30,5 @@ val initial_counters: counters val count: (counters -> 'a) -> counters -> Meta.environment -> 'a val print_counters: (unit -> 'a) -> counters -> 'a + +val pp_environment: (unit -> 'a) -> Format.formatter -> Meta.environment -> 'a diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index f7839a6f9..dc2bfee93 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -44,8 +44,11 @@ let main = if !summary > 1 then AO.count (AO.print_counters Cps.id) AO.initial_counters book; let f env = - if !summary > 1 then - MO.count (MO.print_counters Cps.id) MO.initial_counters env + if !summary > 1 then + MO.count (MO.print_counters Cps.id) MO.initial_counters env; + let frm = Format.err_formatter in + Format.pp_set_margin frm max_int; + MO.pp_environment Cps.id frm (List.rev env) in if !stage > 0 then MA.meta_of_aut f book in