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_______________________________________________________________ *)
20 module E = NCicEnvironment
21 module T = NCicTypeChecker
27 let dno = "_" (* does not occur *)
29 let nan = -1 (* not a number *)
31 (* internal functions *******************************************************)
34 X.error ("alpha: malformed term: " ^ s)
37 X.log ("alpha: ok " ^ s)
40 let r1, r2 = S.sscanf r "%s@_%s" X.id2 in
41 if r2 = "" then r1 else trim r1
46 if j >=0 && s.[j] >= '0' && s.[j] <= '9' then aux j (succ l) else i, l
48 let i, l = aux (N.length s) 0 in
49 let s1, s2 = N.sub s 0 i, N.sub s i l in
50 let s1 = if s1 = "" then "_" else s1 in
51 s1, if l = 0 then nan else int_of_string s2
53 let rec strip = function
55 | C.Prod (_, _, t) -> strip t
58 let get_constant c t = match strip (K.whd c t) with
61 | C.Sort (C.Type [`Type, u]) ->
62 P.sprintf "Type[%s]" (U.string_of_uri u)
63 | C.Sort (C.Type [`CProp, u]) ->
64 P.sprintf "CProp[%s]" (U.string_of_uri u)
65 | C.Const (R.Ref (u, r)) ->
66 let ss = K.segments_of_uri u in
67 let _, _, _, _, obj = E.get_checked_obj G.status u in
68 let ss, _ = K.name_of_reference ss (obj, r) in
69 X.rev_map_concat X.id "." "type" ss
73 let rec aux = function
76 if s = a && (r = b || r = c) then c else aux tl
80 let type_check r c w =
81 let s0 = get_constant c w in
82 let r0 = read !G.alpha_type s0 r in
83 if r0 <> "" then r0 else
84 let s1 = get_constant c (K.typeof c w) in
85 let r0 = read !G.alpha_sort s1 r in
86 if r0 <> "" then r0 else begin
88 X.log (P.sprintf "alpha: not found %s: type \"%s\" sort \"%s\"" r s0 s1);
92 let rec get r = function
95 if fst r = h && snd r <= d then h, succ d else get r tl
98 if K.does_not_occur K.fst_var c t then dno, nan else
99 let r, i = split (trim s) in
100 get (type_check r c w, i) d
103 if i < 0 then s else P.sprintf "%s%u" s i
105 let add_name r d = r :: d
107 let rec proc_term d c t = match t with
114 let tts = proc_terms d c ts in
116 | C.Match (w, u, v, ts) ->
117 let uu = proc_term d c u in
118 let vv = proc_term d c v in
119 let tts = proc_terms d c ts in
121 | C.Prod (s, w, t) ->
122 let rr = alpha d c s w t in
123 let ss = mk_name rr in
124 let ww = proc_term d c w in
125 let tt = proc_term (add_name rr d) (K.add_dec ss w c) t in
127 | C.Lambda (s, w, t) ->
128 let rr = alpha d c s w t in
129 let ss = mk_name rr in
130 let ww = proc_term d c w in
131 let tt = proc_term (add_name rr d) (K.add_dec ss w c) t in
133 | C.LetIn (s, w, v, t) ->
134 let rr = alpha d c s w t in
135 let ss = mk_name rr in
136 let ww = proc_term d c w in
137 let vv = proc_term d c v in
138 let tt = proc_term (add_name rr d) (K.add_def ss w v c) t in
141 and proc_terms d c ts =
142 let rtts = L.rev_map (proc_term d c) ts in
145 let proc_named_term s d c t =
147 let tt = proc_term d c t in
148 if !G.test then begin
149 let _ = K.typeof c tt in
154 | T.TypeCheckerFailure s
155 | T.AssertFailure s -> malformed (Lazy.force s)
157 (* interface functions ******************************************************)
159 let process_top_term s t = proc_named_term s [] [] t