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_______________________________________________________________ *)
16 module T = NCicTypeChecker
22 (* internal functions *******************************************************)
27 X.error ("anticipate: malformed term: " ^ s)
30 X.log ("anticipate: ok " ^ s)
32 let not_prop1 c u = match (K.whd c (K.typeof c u)) with
33 | C.Sort (C.Prop) -> false
37 let not_prop2 c t = not_prop1 c (K.typeof c t)
41 let w = K.typeof c v in
42 P.sprintf "%s%u" !G.proc_id !fresh, w, v, C.Rel K.fst_var
44 let initial = None, []
46 let proc_arg c i (d, rtts) t = match d with
47 | Some _ -> d, (t :: rtts)
49 if K.is_atomic t || not_prop2 c t then d, (t :: rtts) else
50 let s, w, v, tt = anticipate c t in
51 Some (i, s, w, v), (tt :: rtts)
53 let lift_arg ri i tts t =
54 if ri = i then t :: tts
55 else K.lift K.fst_var 1 t :: tts
57 let rec proc_term c t = match t with
60 | C.Implicit _ -> malformed "2"
65 | C.Lambda (s, w, t) ->
66 let tt = shift_term (K.add_dec s w c) t in
68 | C.LetIn (s, w, v, t) ->
70 let dt, tt = proc_term (K.add_def s w v c) t in
71 dt @ K.add_def s w v [], tt
73 let dv, vv = proc_term c v in
74 let l = L.length dv in
76 let w = K.lift K.fst_var l w in
77 let t = K.lift K.snd_var l t in
78 let dt, tt = proc_term (K.add_def s w vv c) t in
79 dt @ (K.add_def s w vv dv), tt
80 | C.Appl [t] -> proc_term c t
81 | C.Appl (C.Appl ts :: vs) -> proc_term c (C.Appl (ts @ vs))
82 | C.Appl ts -> proc_appl c t ts
83 | C.Match (w, u, v, ts) -> proc_case c t w u v ts
85 and proc_appl c t ts = match X.foldi_left (proc_arg c) 1 initial ts with
87 | Some (i, s, w, v), rtts ->
88 let ri = L.length rtts - i in
89 let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
90 proc_term c (K.letin s w v (C.Appl tts))
92 and proc_case c t w u v ts = match X.foldi_left (proc_arg c) 1 initial ts with
94 if K.is_atomic v || not_prop1 c (C.Const w) then [], t else
95 let s, w0, v0, vv = anticipate c v in
96 let u = K.lift K.fst_var 1 u in
97 let ts = K.lifts K.fst_var 1 ts in
98 proc_term c (K.letin s w0 v0 (K.case w u vv ts))
99 | Some (i, s, w0, v0), rtts ->
100 let ri = L.length rtts - i in
101 let u = K.lift K.fst_var 1 u in
102 let v = K.lift K.fst_var 1 v in
103 let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
104 proc_term c (K.letin s w0 v0 (K.case w u v tts))
107 let d, tt = proc_term c t in
110 let shift_named s c t =
113 let tt = shift_term c t in
114 if !G.test then begin
115 let _ = K.typeof c tt in
120 | T.TypeCheckerFailure s
121 | T.AssertFailure s -> malformed (Lazy.force s)
122 | Invalid_argument "List.nth" -> malformed "4" (* to be removed *)
125 let r, s, i, u, t = c in
126 if not_prop1 [] u then c else
127 r, s, i, u, shift_named s [] t
129 let proc_obj obj = match obj with
131 | C.Constant (_, _, None, _, _) -> obj
132 | C.Constant (r, s, Some t, u, a) ->
133 if not_prop1 [] u then obj else
134 let tt = shift_named s [] t in
135 C.Constant (r, s, Some tt, u, a)
136 | C.Fixpoint (b, cs, a) ->
137 C.Fixpoint (b, L.map proc_fun cs, a)
139 (* interface functions ******************************************************)
145 let process_top_term s t = shift_named s [] t
147 let process_obj obj = proc_obj obj