basic_ag/bagEnvironment.cmi basic_ag/bag.cmx basic_ag/bagUntrusted.cmi
basic_ag/bagUntrusted.cmx: lib/log.cmx basic_ag/bagType.cmx \
basic_ag/bagEnvironment.cmx basic_ag/bag.cmx basic_ag/bagUntrusted.cmi
-toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx
-toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx
+toplevel/meta.cmo: common/item.cmx
+toplevel/meta.cmx: common/item.cmx
toplevel/metaOutput.cmi: toplevel/meta.cmx
toplevel/metaOutput.cmo: lib/nUri.cmi toplevel/meta.cmx lib/log.cmi \
lib/cps.cmx toplevel/metaOutput.cmi
type item = bind Item.item
-type context = (int * id * bind) list (* location, name, binder *)
+type lenv = (int * id * bind) list (* location, name, binder *)
-type message = (context, term) Log.item list
+type message = (lenv, term) Log.item list
(* Currified constructors ***************************************************)
let locations () = !location
-(* context handling functions ***********************************************)
+(* local environment handling functions *************************************)
-let empty_context = []
+let empty_lenv = []
let push msg f es l id b =
let rec does_not_occur loc = function
let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in
B.push "output void" f c l id B.Void
-let pp_context frm c =
+let pp_lenv frm c =
let pp_entry frm = function
| l, id, B.Abst w ->
F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w
B.contents f c
let specs = {
- L.pp_term = pp_term; L.pp_context = pp_context
+ L.pp_term = pp_term; L.pp_lenv = pp_lenv
}
val print_counters: (unit -> 'a) -> counters -> 'a
-val specs: (Bag.context, Bag.term) Log.specs
+val specs: (Bag.lenv, Bag.term) Log.specs
type machine = {
i: int;
- c: B.context;
+ c: B.lenv;
s: B.term list
}
let level = 5
let log1 s c t =
- let sc, st = s ^ " in the context", "the term" in
- L.log O.specs level (L.ct_items1 sc c st t)
+ let sc, st = s ^ " in the environment", "the term" in
+ L.log O.specs level (L.et_items1 sc c st t)
let log2 s cu u ct t =
- let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
- L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+ let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
+ L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
-let empty_machine = {i = 0; c = B.empty_context; s = []}
+let empty_machine = {i = 0; c = B.empty_lenv; s = []}
let inc m = {m with i = succ m.i}
| Abst of Bag.term
val ho_whd:
- (ho_whd_result -> 'a) -> Bag.context -> Bag.term -> 'a
+ (ho_whd_result -> 'a) -> Bag.lenv -> Bag.term -> 'a
val are_convertible:
- (bool -> 'a) -> ?si:bool -> Bag.context -> Bag.term -> Bag.term -> 'a
+ (bool -> 'a) -> ?si:bool -> Bag.lenv -> Bag.term -> Bag.term -> 'a
let level = 4
let log1 s c t =
- let sc, st = s ^ " in the context", "the term" in
- L.log O.specs level (L.ct_items1 sc c st t)
+ let sc, st = s ^ " in the envireonment", "the term" in
+ L.log O.specs level (L.et_items1 sc c st t)
let error1 st c t =
- let sc = "In the context" in
- raise (TypeError (L.ct_items1 sc c st t))
+ let sc = "In the envireonment" in
+ raise (TypeError (L.et_items1 sc c st t))
let error3 c t1 t2 t3 =
let sc, st1, st2, st3 =
- "In the context", "the term", "is of type", "but must be of type"
+ "In the envireonment", "the term", "is of type", "but must be of type"
in
- raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
+ raise (TypeError (L.et_items3 sc c st1 t1 st2 t2 st3 t3))
let mk_gref u l =
let map t v = B.Appl (v, t) in
val type_of:
(Bag.term -> Bag.term -> 'a) -> ?si:bool ->
- Hierarchy.graph -> Bag.context -> Bag.term -> 'a
+ Hierarchy.graph -> Bag.lenv -> Bag.term -> 'a
| Some (a, uri, B.Abst t) ->
let f tt obj = f (Some tt) (Some obj) in
let f xt tt = E.set_obj (f tt) (a, uri, B.Abst xt) in
- L.loc := a; T.type_of f ~si g B.empty_context t
+ L.loc := a; T.type_of f ~si g B.empty_lenv t
| Some (a, uri, B.Abbr t) ->
let f tt obj = f (Some tt) (Some obj) in
let f xt tt = E.set_obj (f tt) (a, uri, B.Abbr xt) in
- L.loc := a; T.type_of f ~si g B.empty_context t
+ L.loc := a; T.type_of f ~si g B.empty_lenv t
| Some (a, uri, B.Void) ->
let f obj = f None (Some obj) in
L.loc := a; E.set_obj f (a, uri, B.Void)
type item = bind Item.item
-type context = Null
-(* Cons: tail, relative context, binder *)
- | Cons of context * context option * bind
+type lenv = Null
+(* Cons: tail, relative local environment, binder *)
+ | Cons of lenv * lenv option * bind
(* Currified constructors ***************************************************)
let bind_abbr a v t = Bind (Abbr (a, v), t)
-(* context handling functions ***********************************************)
+(* local environment handling functions *************************************)
-let empty_context = Null
+let empty_lenv = Null
let push f es ?c b =
let es = Cons (es, c, b) in f es
let c = {c with
eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
} in
- count_term f c B.empty_context w
+ count_term f c B.empty_lenv w
| (_, _, B.Abbr (_, v)) ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
- count_term f c B.empty_context v
+ count_term f c B.empty_lenv v
| (_, u, B.Void _) ->
let c = {c with
evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris
| B.Abbr (a, v) -> let f a = f (B.abbr a v) in rename f c a
| B.Void a -> let f a = f (B.Void a) in rename f c a
-(* context/term pretty printing *********************************************)
+(* lenv/term pretty printing ************************************************)
let id frm a =
let f n = function
let f a = B.push (f a) c (B.Void a) in
rename f c a
-let pp_context frm c =
+let pp_lenv frm c =
let pp_entry f c = function
| B.Abst (a, w) ->
let f a = F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f () in
B.rev_iter C.start pp_entry c
let specs = {
- L.pp_term = pp_term; L.pp_context = pp_context
+ L.pp_term = pp_term; L.pp_lenv = pp_lenv
}
(* term xml printing ********************************************************)
F.fprintf frm "<VOID uri=%S%a/>" str id a
let export_obj frm obj =
- F.fprintf frm "@,@[<v3> %a@]@," (exp_obj B.empty_context) obj
+ F.fprintf frm "@,@[<v3> %a@]@," (exp_obj B.empty_lenv) obj
val print_counters: (unit -> 'a) -> counters -> 'a
-val specs: (Brg.context, Brg.term) Log.specs
+val specs: (Brg.lenv, Brg.term) Log.specs
val export_obj: Format.formatter -> Brg.bind Item.obj -> unit
module E = BrgEnvironment
type machine = {
- c: B.context;
- s: (B.context * B.term) list;
+ c: B.lenv;
+ s: (B.lenv * B.term) list;
i: int
}
let level = 5
let log1 s c t =
- let sc, st = s ^ " in the context", "the term" in
- L.log O.specs level (L.ct_items1 sc c st t)
+ let sc, st = s ^ " in the environment", "the term" in
+ L.log O.specs level (L.et_items1 sc c st t)
let log2 s cu u ct t =
- let s1, s2, s3 = s ^ " in the context", "the term", "and in the context" in
- L.log O.specs level (L.ct_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+ let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
+ L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
let are_alpha_convertible err f t1 t2 =
let rec aux f = function
(* Interface functions ******************************************************)
let empty_machine = {
- c = B.empty_context; s = []; i = 0
+ c = B.empty_lenv; s = []; i = 0
}
let get err f m i =
let pp_term m frm t = O.specs.L.pp_term m.c frm t
-let pp_context frm m = O.specs.L.pp_context frm m.c
+let pp_lenv frm m = O.specs.L.pp_lenv frm m.c
let specs = {
- L.pp_term = pp_term; L.pp_context = pp_context
+ L.pp_term = pp_term; L.pp_lenv = pp_lenv
}
let level = 4
let message1 st1 m t1 =
- L.ct_items1 "In the context" m st1 t1
+ L.et_items1 "In the environment" m st1 t1
let log1 s m t =
let s = s ^ " the term" in
raise (TypeError (message1 s m t))
let message3 m t1 t2 ?mu t3 =
- let sm, st1, st2 = "In the context", "the term", "is of type" in
+ let sm, st1, st2 = "In the environment", "the term", "is of type" in
match mu with
| Some mu ->
- let smu, st3 = "but in the context", "it must be of type" in
- L.ct_items3 sm m st1 t1 st2 t2 ~sc3:smu ~c3:mu st3 t3
+ let smu, st3 = "but in the environment", "it must be of type" in
+ L.et_items3 sm m st1 t1 st2 t2 ~sc3:smu ~c3:mu st3 t3
| None ->
let st3 = "but it must be of type" in
- L.ct_items3 sm m st1 t1 st2 t2 st3 t3
+ L.et_items3 sm m st1 t1 st2 t2 st3 t3
let error3 m t1 t2 ?mu t3 =
raise (TypeError (message3 m t1 t2 ?mu t3))
module C = Cps
type ('a, 'b) item = Term of 'a * 'b
- | Context of 'a
+ | LEnv of 'a
| Warn of string
| String of string
| Loc
type ('a, 'b) message = ('a, 'b) item list
type ('a, 'b) specs = {
- pp_term : 'a -> F.formatter -> 'b -> unit;
- pp_context: F.formatter -> 'a -> unit
+ pp_term: 'a -> F.formatter -> 'b -> unit;
+ pp_lenv: F.formatter -> 'a -> unit
}
let level = ref 0
let pp_items frm st l items =
let pp_item frm = function
| Term (c, t) -> F.fprintf frm "@,%a" (st.pp_term c) t
- | Context c -> F.fprintf frm "%a" st.pp_context c
+ | LEnv c -> F.fprintf frm "%a" st.pp_lenv c
| Warn s -> F.fprintf frm "@,%s" s
| String s -> F.fprintf frm "%s " s
| Loc -> F.fprintf frm " (line %u)" !loc
let t_items1 st c t =
[Warn st; Term (c, t)]
-let ct_items1 sc c st t =
- [Warn sc; Context c; Warn st; Term (c, t)]
+let et_items1 sc c st t =
+ [Warn sc; LEnv c; Warn st; Term (c, t)]
-let ct_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 =
+let et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 =
let tl = match sc2, c2 with
- | Some sc2, Some c2 -> ct_items1 sc2 c2 st2 t2
+ | Some sc2, Some c2 -> et_items1 sc2 c2 st2 t2
| None, None -> t_items1 st2 c1 t2
| _ -> assert false
in
- ct_items1 sc1 c1 st1 t1 @ tl
+ et_items1 sc1 c1 st1 t1 @ tl
-let ct_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 =
+let et_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 =
let tl = match sc3, c3 with
- | Some sc3, Some c3 -> ct_items1 sc3 c3 st3 t3
+ | Some sc3, Some c3 -> et_items1 sc3 c3 st3 t3
| None, None -> t_items1 st3 c1 t3
| _ -> assert false
in
- ct_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl
+ et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl
let warn msg = F.fprintf std "@,%s" msg
V_______________________________________________________________ *)
type ('a, 'b) item = Term of 'a * 'b
- | Context of 'a
+ | LEnv of 'a
| Warn of string
| String of string
| Loc
type ('a, 'b) message = ('a, 'b) item list
type ('a, 'b) specs = {
- pp_term : 'a -> Format.formatter -> 'b -> unit;
- pp_context: Format.formatter -> 'a -> unit
+ pp_term: 'a -> Format.formatter -> 'b -> unit;
+ pp_lenv: Format.formatter -> 'a -> unit
}
val loc: int ref
val t_items1: string -> 'a -> 'b -> ('a, 'b) message
-val ct_items1:
+val et_items1:
string -> 'a -> string -> 'b -> ('a, 'b) message
-val ct_items2:
+val et_items2:
string -> 'a -> string -> 'b ->
?sc2:string -> ?c2:'a -> string -> 'b ->
('a, 'b) message
-val ct_items3:
+val et_items3:
string -> 'a -> string -> 'b ->
?sc2:string -> ?c2:'a -> string -> 'b ->
?sc3:string -> ?c3:'a -> string -> 'b ->
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-type uri = NUri.uri
+type uri = Item.uri
-type id = Aut.id
+type id = Item.id
type term = Sort of bool (* sorts: true = TYPE, false = PROP *)
- | LRef of int * int (* local reference: context length, de bruijn index *)
- | GRef of int * uri * term list (* global reference: context length, name, arguments *)
+ | LRef of int * int (* local reference: local environment length, de bruijn index *)
+ | GRef of int * uri * term list (* global reference: local environment length, name, arguments *)
| Appl of term * term (* application: argument, function *)
| Abst of id * term * term (* abstraction: name, type, scope *)
let f w = B.push "meta" f c l id (B.Abst w) in
xlate_term c f w
in
- C.list_fold_right f map pars B.empty_context
+ C.list_fold_right f map pars B.empty_lenv
let unwind_to_xlate_term f c t =
let map f t (l, id, b) = f (B.bind l id b t) in
let f w = B.push f c (B.abst a w) in
xlate_term c f w
in
- C.list_fold_right f map pars B.empty_context
+ C.list_fold_right f map pars B.empty_lenv
let unwind_to_xlate_term f c t =
let map f t b = f (B.bind b t) in
projects / helm.git / commitdiff