2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
19 module B = NCicSubstitution
20 module D = NCicReduction
21 module K = NCicTypeChecker
23 module A = NCicLibrary
24 module E = NCicEnvironment
30 (* internal functions *******************************************************)
36 let mk_type_universe i =
37 [`Type, U.uri_of_string (P.sprintf "cic:/matita/pts/Type%s.univ" i)]
39 (* interface functions ******************************************************)
44 H.set_log_callback no_log;
45 let u0 = mk_type_universe "0" in
46 let u1 = mk_type_universe "1" in
47 E.add_lt_constraint ~acyclic:true u0 u1
53 let appl ts = C.Appl ts
55 let prod s w t = C.Prod (s, w, t)
57 let lambda s w t = C.Lambda (s, w, t)
59 let letin s w v t = C.LetIn (s, w, v, t)
61 let case w u v ts = C.Match (w, u, v, ts)
63 let add_dec s w c = (s, C.Decl w) :: c
65 let add_def s w v c = (s, C.Def (v, w)) :: c
67 let rec shift t = function
69 | (s, C.Decl w) :: c -> shift (lambda s w t) c
70 | (s, C.Def (v, w)) :: c -> shift (letin s w v t) c
72 let rec is_atomic = function
73 | C.Appl [t] -> is_atomic t
86 let resolve_lref c i = fst (L.nth c (i - fst_var))
89 B.lift G.status ~from:d e t
92 L.rev_map (lift d e) (L.rev ts)
95 D.whd G.status ~delta:max_int ~subst:[] c t
98 K.typeof G.status [] [] c t
100 let whd_typeof c t = whd c (typeof c t)
102 let not_prop1 c u = match whd_typeof c u with
103 | C.Sort (C.Prop) -> false
106 let not_prop2 c t = not_prop1 c (typeof c t)
108 let does_not_occur i c t =
109 K.does_not_occur G.status ~subst:[] c 0 i t
111 let segments_of_uri u =
112 let s = U.string_of_uri u in
113 let s = F.chop_extension s in
114 let l = S.length s in
115 let i = S.index s ':' in
116 let s = S.sub s (i+2) (l-i-2) in
117 X.segments_of_string [] (l-i-2) s
119 let name_of_reference ss = function
120 | C.Constant (_, name, _, _, _), R.Decl ->
122 | C.Constant (_, name, _, _, _), R.Def _ ->
124 | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
125 let _, name, _, _ = L.nth us i in
127 | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
128 let _, _, _, ts = L.nth us i in
129 let _, name, _ = L.nth ts (pred j) in
131 | C.Fixpoint (_, ts, _) , R.Fix (i, _, _) ->
132 let _, name, _, _, _ = L.nth ts i in
134 | C.Fixpoint (_, ts, _) , R.CoFix i ->
135 let _, name, _, _, _ = L.nth ts i in
138 failwith "name_of_reference"