]> matita.cs.unibo.it Git - helm.git/blob - matita/components/binaries/matex/alpha.ml
59e8c989fb0f406076d8ffccb96a9a736f941925
[helm.git] / matita / components / binaries / matex / alpha.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 module L = List
13 module P = Printf
14 module S = Scanf
15 module N = String
16
17 module U = NUri
18 module C = NCic
19 module R = NReference
20 module E = NCicEnvironment
21 module T = NCicTypeChecker
22
23 module X = Ground
24 module G = Options
25 module K = Kernel
26
27 let dno = "_" (* does not occur *)
28
29 let nan = -1  (* not a number *)
30
31 (* internal functions *******************************************************)
32
33 let malformed s =
34    X.error ("alpha: malformed term: " ^ s)
35
36 let ok s =
37    X.log ("alpha: ok " ^ s)
38
39 let rec trim r =
40    let r1, r2 = S.sscanf r "%s@_%s" X.id2 in
41    if r2 = "" then r1 else trim r1
42
43 let split s = 
44    let rec aux i l =
45       let j = pred i in
46       if j >=0 && s.[j] >= '0' && s.[j] <= '9' then aux j (succ l) else i, l
47    in 
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
52
53 let rec strip = function
54    | C.Appl (t :: _) 
55    | C.Prod (_, _, t) -> strip t
56    | t                -> t
57
58 let get_constant c t = match strip (K.whd c t) with
59    | C.Sort (C.Prop)             ->
60       P.sprintf "Prop"
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
70    | _                           -> ""
71
72 let read l s r =
73    let rec aux = function
74       | []              -> ""
75       | (a, b, c) :: tl ->
76          if s = a && (r = b || r = c) then c else aux tl
77    in
78    aux l 
79
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
87       if !G.log_alpha then
88          X.log (P.sprintf "alpha: not found %s: type \"%s\" sort \"%s\"" r s0 s1);
89       r
90    end
91
92 let rec get r = function
93    | []           -> r
94    | (h, d) :: tl ->
95       if fst r = h && snd r <= d then h, succ d else get r tl
96
97 let alpha d c s w t =
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
101
102 let mk_name (s, i) =
103    if i < 0 then s else P.sprintf "%s%u" s i
104
105 let add_name r d = r :: d
106
107 let rec proc_term d c t = match t with
108    | C.Meta _
109    | C.Implicit _             
110    | C.Sort _
111    | C.Rel _
112    | C.Const _             -> t
113    | C.Appl ts             ->
114       let tts = proc_terms d c ts in
115       K.appl tts
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
120       K.case w uu vv tts
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
126       K.prod ss ww tt
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
132       K.lambda ss ww tt
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
139       K.letin ss ww vv tt
140
141 and proc_terms d c ts =
142    let rtts = L.rev_map (proc_term d c) ts in
143    L.rev rtts
144
145 let proc_named_term s d c t =
146 try
147    let tt = proc_term d c t in
148    if !G.test then begin
149       let _ = K.typeof c tt in
150       ok s
151    end;
152    tt
153 with
154    | T.TypeCheckerFailure s
155    | T.AssertFailure s           -> malformed (Lazy.force s)
156
157 (* interface functions ******************************************************)
158
159 let process_top_term s t = proc_named_term s [] [] t