basic_rg/brgEnvironment.cmi
basic_rg/brgEnvironment.cmx: lib/nUri.cmx basic_rg/brg.cmx \
basic_rg/brgEnvironment.cmi
-basic_rg/brgReduction.cmo: lib/nUri.cmi basic_rg/brgEnvironment.cmi \
- basic_rg/brg.cmx basic_rg/brgReduction.cmi
-basic_rg/brgReduction.cmx: lib/nUri.cmx basic_rg/brgEnvironment.cmx \
- basic_rg/brg.cmx basic_rg/brgReduction.cmi
+basic_rg/brgReduction.cmi: basic_rg/brg.cmx
+basic_rg/brgReduction.cmo: lib/share.cmx lib/nUri.cmi lib/cps.cmx \
+ basic_rg/brgEnvironment.cmi basic_rg/brg.cmx basic_rg/brgReduction.cmi
+basic_rg/brgReduction.cmx: lib/share.cmx lib/nUri.cmx lib/cps.cmx \
+ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi
+basic_rg/brgType.cmi: basic_rg/brgReduction.cmi basic_rg/brg.cmx
+basic_rg/brgType.cmo: basic_rg/brgReduction.cmi basic_rg/brgEnvironment.cmi \
+ basic_rg/brg.cmx basic_rg/brgType.cmi
+basic_rg/brgType.cmx: basic_rg/brgReduction.cmx basic_rg/brgEnvironment.cmx \
+ basic_rg/brg.cmx basic_rg/brgType.cmi
+basic_rg/brgUntrusted.cmi: basic_rg/brg.cmx
+basic_rg/brgUntrusted.cmo: basic_rg/brgType.cmi basic_rg/brgReduction.cmi \
+ basic_rg/brgEnvironment.cmi basic_rg/brgUntrusted.cmi
+basic_rg/brgUntrusted.cmx: basic_rg/brgType.cmx basic_rg/brgReduction.cmx \
+ basic_rg/brgEnvironment.cmx basic_rg/brgUntrusted.cmi
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/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \
toplevel/metaBrg.cmi
toplevel/top.cmo: lib/time.cmx toplevel/metaOutput.cmi toplevel/metaBrg.cmi \
- toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx basic_rg/brgOutput.cmi \
- automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx
+ toplevel/metaAut.cmi lib/log.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \
+ basic_rg/brgOutput.cmi automath/autParser.cmi automath/autOutput.cmi \
+ automath/autLexer.cmx
toplevel/top.cmx: lib/time.cmx toplevel/metaOutput.cmx toplevel/metaBrg.cmx \
- toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx basic_rg/brgOutput.cmx \
- automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx
+ toplevel/metaAut.cmx lib/log.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
+ basic_rg/brgOutput.cmx automath/autParser.cmx automath/autOutput.cmx \
+ automath/autLexer.cmx
-brg brgOutput brgEnvironment brgReduction
+brg brgOutput brgEnvironment brgReduction brgType brgUntrusted
type obj = int * uri * bind * term (* age, uri, binder, contents *)
type item = obj option
+
+type hierarchy = int -> int
+
+(* Currified constructors ***************************************************)
+
+let cast u t = Cast (u, t)
+
+let appl u t = Appl (u, t)
+
+let bind id b u t = Bind (id, b, u, t)
V_______________________________________________________________ *)
module U = NUri
+module C = Cps
+module S = Share
module B = Brg
module E = BrgEnvironment
exception LRefNotFound of string Lazy.t
-type environment = int * (B.bind * B.term) list
+type bind = Void_
+ | Abst_ of B.term
+ | Abbr_ of B.term
+
+type environment = int * bind list
type stack = B.term list
type whd_result =
| Sort_ of int
- | LRef_ of int
- | GRef_ of int * U.uri * B.bind
- | Abst_ of B.term
+ | LRef_ of int * B.term option
+ | GRef_ of int * B.bind * B.term
+ | Bind_ of B.term * B.term
+
+type ho_whd_result =
+ | Sort of int
+ | Abst of B.term
(* Internal functions *******************************************************)
-let push_e f b t (l, e) =
- f (succ l, (b, t) :: e)
+let empty_e = 0, []
+
+let push_e f b (l, e) =
+ f (succ l, b :: e)
-let rec find_e f c i =
+let get_e f c i =
let (gl, ge), (ll, le) = c.g, c.l in
if i >= gl + ll then raise (LRefNotFound (lazy (string_of_int i)));
- let b, t =
+ let b =
if i < gl then List.nth ge (gl - (succ i))
else List.nth le (gl + ll - (succ i))
in
- f t b
-
+ f b
+
+let rec lref_map f map t = match t with
+ | B.LRef i -> f (B.LRef (map i))
+ | B.GRef _ -> f t
+ | B.Sort _ -> f t
+ | B.Cast (w, u) ->
+ let f w' u' = f (S.sh2 w w' u u' t B.cast) in
+ let f w' = lref_map (f w') map u in
+ lref_map f map w
+ | B.Appl (w, u) ->
+ let f w' u' = f (S.sh2 w w' u u' t B.appl) in
+ let f w' = lref_map (f w') map u in
+ lref_map f map w
+ | B.Bind (id, b, w, u) ->
+ let f w' u' = f (S.sh2 w w' u u' t (B.bind id b)) in
+ let f w' = lref_map (f w') map u in
+ lref_map f map w
+
+(* to share *)
+let lift f c =
+ let (gl, _), (ll, le) = c.g, c.l in
+ let map i = if i >= gl then succ i else i in
+ let map f = function
+ | Abbr_ t -> let f t' = f (Abbr_ t') in lref_map f map t
+ | _ -> assert false
+ in
+ let f le' = f {c with l = (ll, le')} in
+ C.list_map f map le
+
+let xchg f c t =
+ let (gl, _), (ll, _) = c.g, c.l in
+ let map i =
+ if i < gl || i > gl + ll then i else
+ if i >= gl && i < gl + ll then succ i else gl
+ in
+ lref_map (f c) map t
+
+(* to share *)
let rec whd f c t = match t with
- | B.Sort h -> f c t (Sort_ h)
+ | B.Sort h -> f c (Sort_ h)
| B.GRef uri ->
- let f (i, _, b, t) = f c t (GRef_ (i, uri, b)) in
+ let f (i, _, b, t) = f c (GRef_ (i, b, t)) in
E.get_obj f uri
| B.LRef i ->
- let f t = function
- | B.Abst -> f c t (LRef_ i)
- | B.Abbr -> whd f c t
+ let f = function
+ | Void_ -> f c (LRef_ (i, None))
+ | Abst_ t -> f c (LRef_ (i, Some t))
+ | Abbr_ t -> whd f c t
in
- find_e f c i
+ get_e f c i
| B.Appl (v, t) -> whd f {c with s = v :: c.s} t
| B.Bind (_, B.Abbr, v, t) ->
let f l = whd f {c with l = l} t in
- push_e f B.Abbr v c.l
+ push_e f (Abbr_ v) c.l
| B.Bind (_, B.Abst, w, t) ->
begin match c.s with
- | [] -> f c t (Abst_ w)
+ | [] -> f c (Bind_ (w, t))
| v :: tl ->
let f tl l = whd f {c with l = l; s = tl} t in
- push_e (f tl) B.Abbr v c.l
+ push_e (f tl) (Abbr_ v) c.l
end
| B.Cast (_, t) -> whd f c t
+let push f c t =
+ assert (c.s = []);
+ let f c g = xchg f {c with g = g} t in
+ let f c = push_e (f c) Void_ c.g in
+ lift f c
+
(* Interface functions ******************************************************)
+let rec are_convertible f c1 t1 c2 t2 =
+ let rec aux c1' r1 c2' r2 = match r1, r2 with
+ | Sort_ h1, Sort_ h2 -> f (h1 = h2)
+ | LRef_ (i1, _), LRef_ (i2, _) ->
+ if i1 = i2 then are_convertible_stacks f c1' c2' else f false
+ | GRef_ (a1, B.Abst, _), GRef_ (a2, B.Abst, _) ->
+ if a1 = a2 then are_convertible_stacks f c1' c2' else f false
+ | GRef_ (a1, B.Abbr, v1), GRef_ (a2, B.Abbr, v2) ->
+ if a1 = a2 then are_convertible_stacks f c1' c2' else
+ if a1 < a2 then whd (aux c1' r1) c2' v2 else
+ whd (aux_rev c2' r2) c1' v1
+ | _, GRef_ (_, B.Abbr, v2) ->
+ whd (aux c1' r1) c2' v2
+ | GRef_ (_, B.Abbr, v1), _ ->
+ whd (aux_rev c2' r2) c1' v1
+ | Bind_ (w1, t1), Bind_ (w2, t2) ->
+ let f b =
+ if b then
+ let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in
+ push f c1' t1
+ else f false
+ in
+ are_convertible f c1' w1 c2' w2
+ | _ -> f false
+ and aux_rev c2 r2 c1 r1 = aux c1 r1 c2 r2 in
+ let f c1' r1 = whd (aux c1' r1) c2 t2 in
+ whd f c1 t1
+
+and are_convertible_stacks f c1 c2 =
+ let map f v1 v2 = are_convertible f c1 v1 c2 v2 in
+ if List.length c1.s <> List.length c2.s then f false else
+ C.forall2 f map c1.s c2.s
+
+let are_convertible f c t1 t2 = are_convertible f c t1 c t2
+
+let rec ho_whd f c t =
+ let aux c' = function
+ | Sort_ h -> f c' (Sort h)
+ | Bind_ (w, t) -> f c' (Abst w)
+ | LRef_ (_, Some w) -> ho_whd f c w
+ | GRef_ (_, _, u) -> ho_whd f c u
+ | LRef_ (_, None) -> assert false
+ in
+ whd aux c t
+
let push f c b t =
- assert (fst c.l = 0 && c.s = []);
+ assert (c.l = empty_e && c.s = []);
let f g = f {c with g = g} in
- push_e f b t c.g
+ let b = match b with
+ | B.Abbr -> Abbr_ t
+ | B.Abst -> Abst_ t
+ in
+ push_e f b c.g
+
+let get f c i =
+ let gl, ge = c.g in
+ if i >= gl then raise (LRefNotFound (lazy (string_of_int i)));
+ match List.nth ge (gl - (succ i)) with
+ | Abbr_ v -> f (B.Abbr, v)
+ | Abst_ w -> f (B.Abst, w)
+ | Void_ -> assert false
+
+let empty_context = {
+ g = empty_e; l = empty_e; s = []
+}
exception LRefNotFound of string Lazy.t
type context
+
+type ho_whd_result =
+ | Sort of int
+ | Abst of Brg.term
+
+val empty_context: context
+
+val push: (context -> 'a) -> context -> Brg.bind -> Brg.term -> 'a
+
+val get: (Brg.bind * Brg.term -> 'a) -> context -> int -> 'a
+
+val are_convertible: (bool -> 'a) -> context -> Brg.term -> Brg.term -> 'a
+
+val ho_whd: (context -> ho_whd_result -> 'a) -> context -> Brg.term -> 'a
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+module B = Brg
+module E = BrgEnvironment
+module R = BrgReduction
+
+exception TypeError of string Lazy.t
+
+(* Internal functions *******************************************************)
+
+let error msg = raise (TypeError (lazy msg))
+
+(* Interface functions ******************************************************)
+
+let rec type_of f g c = function
+ | B.Sort h -> f (B.Sort (g h))
+ | B.LRef i ->
+ let f = function
+ | B.Abst, w -> f w
+ | B.Abbr, B.Cast (w, v) -> f w
+ | B.Abbr, _ -> error "lref"
+ in
+ R.get f c i
+ | B.GRef uri ->
+ let f = function
+ | _, _, B.Abst, w -> f w
+ | _, _, B.Abbr, B.Cast (w, v) -> f w
+ | _, _, B.Abbr, _ -> error "gref"
+ in
+ E.get_obj f uri
+ | B.Bind (id, b, u, t) ->
+ let f uu tt = match b, t with
+ | B.Abst, _
+ | B.Abbr, B.Cast _ -> f (B.Bind (id, b, u, tt))
+ | _ -> f (B.Bind (id, b, B.Cast (uu, u), tt))
+ in
+ let f uu cc = type_of (f uu) g cc t in
+ let f uu = R.push (f uu) c b u in
+ type_of f g c u
+ | B.Appl (v, t) ->
+ let f tt cc = function
+ | R.Sort _ -> error "appl"
+ | R.Abst w ->
+ let f b = if b then f (B.Appl (v, tt)) else error "appl_cast" in
+ type_of (R.are_convertible f cc w) g c v
+ in
+ let f tt = R.ho_whd (f tt) c t in
+ type_of f g c t
+ | B.Cast (u, t) ->
+ let f b = if b then f u else error "cast" in
+ let f _ = type_of (R.are_convertible f c u) g c t in
+ type_of f g c u
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+exception TypeError of string Lazy.t
+
+val type_of: (Brg.term -> 'a) ->
+ Brg.hierarchy -> BrgReduction.context -> Brg.term -> 'a
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+module E = BrgEnvironment
+module R = BrgReduction
+module T = BrgType
+
+(* Interface functions ******************************************************)
+
+let type_check f g = function
+ | None -> f None
+ | Some ((_, _, _, t) as obj) ->
+ let f tt obj = f (Some (tt, obj)) in
+ let f tt = E.set_obj (f tt) obj in
+ T.type_of f g R.empty_context t
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+val type_check: ((Brg.term * Brg.obj) option -> 'a) ->
+ Brg.hierarchy -> Brg.item -> 'a
-nUri cps log time
+nUri cps share log time
let f hd = list_rev_map_append f map ~tail:(hd :: tail) tl in
map f hd
+let rec forall2 f map l1 l2 = match l1, l2 with
+ | [], [] -> f true
+ | hd1 :: tl1, hd2 :: tl2 ->
+ let f b = if b then forall2 f map tl1 tl2 else f false in
+ map f hd1 hd2
+ | _ -> f false
+
let list_rev_append f =
list_rev_map_append f (fun f t -> f t)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+let sh a b =
+ if a == b then a else b
+
+let sh2 a1 b1 a2 b2 c1 c2 =
+ if a1 == a2 && b1 == b2 then c1 else c2 (sh a1 a2) (sh b1 b2)
module MO = MetaOutput
module MBrg = MetaBrg
module BrgO = BrgOutput
+module BrgU = BrgUntrusted
type status = {
summary: int;
let main =
let version_string = "Helena Checker 0.8.0 M - December 2008" in
let summary = ref 0 in
- let stage = ref 2 in
+ let stage = ref 3 in
let meta_file = ref None in
+ let hierarchy = ref (fun h -> h + 2) in
let set_summary i = summary := i in
let print_version () = L.warn version_string; exit 0 in
let set_stage i = stage := i in
let rec aux st = function
| [] -> st
| item :: tl ->
- let st = {st with ac = count st AO.count_item st.ac item} in
+(* stage 3 *)
+ let f st = function
+ | None -> st
+ | Some (_, (i, _, _, _)) ->
+ Log.warn (string_of_int i); st
+ in
+(* stage 2 *)
let f st item =
- {st with brgc = count st BrgO.count_item st.brgc item}
+ let st = {st with brgc = count st BrgO.count_item st.brgc item} in
+ if !stage > 2 then BrgU.type_check (f st) !hierarchy item else st
in
+(* stage 1 *)
let f mst item =
let st = {st with
mst = mst; mc = count st MO.count_item st.mc item
end;
if !stage > 1 then MBrg.brg_of_meta (f st) item else st
in
+(* stage 0 *)
+ let st = {st with ac = count st AO.count_item st.ac item} in
let st =
if !stage > 0 then MA.meta_of_aut f st.mst item else st
in
projects / helm.git / commitdiff