* 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 =
# 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']
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]<x>p:'prop'
+%end of suggestion
[a1:all(sigma,p)][s:sigma]
alle:=<s>a1:<s>p
+all
-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]<x>b:'prop'
+%end of suggestion
[a1:a][i:imp(a,b)]
mp:=<a1>i:<a1>b
+imp
+++ /dev/null
-# 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(<x>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:<s>p][i:is(s,t)]
-isp:=PRIM:<t>p
-p@amone:=[x,sigma][y,sigma][u,<x>p][v,<y>p]is(x,y):PROP
-one:=and(amone(sigma,p),some(sigma,p)):PROP
-[o1:one(sigma,p)]
-ind:=PRIM:sigma
-oneax:=PRIM:<ind>p
-sigma@[tau:TYPE][f:[x,sigma]tau]
-injective:=all([x,sigma]all([y,sigma]imp(is(tau,<x>f,<y>f),is(x,y)))):PROP
-[t0:tau]
-image:=some([x,sigma]is(tau,t0,<x>f)):PROP
-tau@[f:[x,sigma]tau][g:[x,sigma]tau][i:[x,sigma]is(tau,<x>f,<x>g)]
-fisi:=PRIM:is([x,sigma]tau,f,g)
-p@ot:=PRIM:TYPE
-[o1:ot]
-in:=PRIM:sigma
-inp:=PRIM:<in>p
-p@otax1:=PRIM:injective(ot,sigma,[x,ot]in(x))
-[s:sigma][sp:<s>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:<s>p]
-estii:=PRIM:esti(s,setof(p))
-s@[e:esti(s,setof(p))]
-estie:=PRIM:<s>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(<x>suc,1)
-ax4:=PRIM:[x,nat][y,nat][u,is(<x>suc,<y>suc)]is(x,y)
-[s:set(nat)]
-cond1:=in(1,s):PROP
-cond2:=all([x,nat]imp(in(x,s),in(<x>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
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
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? *)
}
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
}
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
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
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
* http://cs.unibo.it/helm/.
*)
+module F = Format
module M = Meta
type 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
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
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 ()
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
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
projects / helm.git / commitdiff