1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
(** Typing context. *)
open Term
open Lplib open Extra
open Timed
open Common open Name
(** [type_of x ctx] returns the type of [x] in the context [ctx] when it
appears in it, and @raise [Not_found] otherwise. *)
let type_of : var -> ctxt -> term = fun x ctx ->
let (_,a,_) = List.find (fun (y,_,_) -> eq_vars x y) ctx in a
(** [def_of x ctx] returns the definition of [x] in the context [ctx] if it
appears, and [None] otherwise *)
let rec def_of : var -> ctxt -> ctxt * term option = fun x c ->
match c with
| [] -> [], None
| (y,_,d)::c -> if eq_vars x y then c,d else def_of x c
(** [to_prod ctx t] builds a product by abstracting over the context [ctx], in
the term [t]. It returns the number of products as well. *)
let to_prod : ctxt -> term -> term * int = fun ctx t ->
let f (t,k) (x,a,d) =
let b = bind_var x t in
let u =
match d with
| None -> mk_Prod (a,b)
| Some d -> mk_LLet (a,d,b)
in
u, k+1
in
List.fold_left f (t,0) ctx
(** [unfold ctx t] behaves like {!val:Term.unfold} unless term [t] is of the
form [Vari(x)] with [x] defined in [ctx]. In this case, [t] is replaced by
the definition of [x] in [ctx]. In particular, if no operation is carried
out on [t], we have [unfold ctx t == t]. *)
let rec unfold : ctxt -> term -> term = fun ctx t ->
match t with
| Meta(m, ts) ->
begin
match !(m.meta_value) with
| None -> t
| Some(b) -> unfold ctx (msubst b ts)
end
| TRef(r) ->
begin
match !r with
| None -> t
| Some(v) -> unfold ctx v
end
| Vari(x) ->
begin
match def_of x ctx with
| _, None -> t
| ctx', Some t -> unfold ctx' t
end
| _ -> t
(** [to_map] builds a map from a context. *)
let to_map : ctxt -> term VarMap.t =
let add_def m (x,_,v) =
match v with Some v -> VarMap.add x v m | None -> m
in List.fold_left add_def VarMap.empty
(** [names c] returns the set of names in [c]. *)
let names : ctxt -> int StrMap.t =
let add_decl idmap (v,_,_) = add_name (base_name v) idmap in
List.fold_left add_decl StrMap.empty
(** [fresh c id] returns a string starting with [id] and not in [c]. *)
let fresh (c:ctxt) (id:string) : string = fst (get_safe_prefix id (names c))