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
49 let fst_var = 1 (* first variable *)
51 let snd_var = 2 (* second variable *)
53 let fst_con = 1 (* first constructor *)
55 let appl ts = C.Appl ts
57 let prod s w t = C.Prod (s, w, t)
59 let lambda s w t = C.Lambda (s, w, t)
61 let letin s w v t = C.LetIn (s, w, v, t)
63 let case w u v ts = C.Match (w, u, v, ts)
65 let add_dec s w c = (s, C.Decl w) :: c
67 let add_def s w v c = (s, C.Def (v, w)) :: c
69 let rec shift t = function
71 | (s, C.Decl w) :: c -> shift (lambda s w t) c
72 | (s, C.Def (v, w)) :: c -> shift (letin s w v t) c
74 let rec is_atomic = function
75 | C.Appl [t] -> is_atomic t
88 let resolve_lref c i = fst (L.nth c (i - fst_var))
91 B.lift G.status ~from:d e t
94 L.rev_map (lift d e) (L.rev ts)
97 D.whd G.status ~delta:max_int ~subst:[] c t
100 K.typeof G.status [] [] c t
102 let whd_typeof c t = whd c (typeof c t)
104 let not_prop1 c u = match whd_typeof c u with
105 | C.Sort (C.Prop) -> false
108 let not_prop2 c t = not_prop1 c (typeof c t)
110 let does_not_occur i c t =
111 K.does_not_occur G.status ~subst:[] c 0 i t
113 let segments_of_uri u =
114 let s = U.string_of_uri u in
115 let s = F.chop_extension s in
116 let l = S.length s in
117 let i = S.index s ':' in
118 let s = S.sub s (i+2) (l-i-2) in
119 X.segments_of_string [] (l-i-2) s
121 let names_of_reference ss = function
122 | C.Constant (_, name, _, _, _), R.Decl ->
124 | C.Constant (_, name, _, _, _), R.Def _ ->
126 | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
127 let _, name, _, _ = L.nth us i in
129 | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
130 let _, _, _, ts = L.nth us i in
131 let _, name, _ = L.nth ts (pred j) in
133 | C.Fixpoint (_, ts, _) , R.Fix (i, _, _) ->
134 let _, name, _, _, _ = L.nth ts i in
136 | C.Fixpoint (_, ts, _) , R.CoFix i ->
137 let _, name, _, _, _ = L.nth ts i in
140 failwith "name_of_reference"
142 let resolve_reference = function
144 let ss = segments_of_uri u in
145 let _, _, _, _, obj = E.get_checked_obj G.status u in
146 let ss, name = names_of_reference ss (obj, r) in
147 X.rev_map_concat X.id "." "type" ss, name