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)
34 let w = K.typeof c v in
35 P.sprintf "%s%u" !G.proc_id !fresh, w, v, C.Rel K.fst_var
37 let initial = None, []
39 let proc_arg c i (d, rtts) t = match d with
40 | Some _ -> d, (t :: rtts)
42 if K.is_atomic t || K.not_prop2 c t then d, (t :: rtts) else
43 let s, w, v, tt = anticipate c t in
44 Some (i, s, w, v), (tt :: rtts)
46 let lift_arg ri i tts t =
47 if ri = i then t :: tts
48 else K.lift K.fst_var 1 t :: tts
50 let rec proc_term c t = match t with
53 | C.Implicit _ -> malformed "2"
58 | C.Lambda (s, w, t) ->
59 let tt = shift_term (K.add_dec s w c) t in
61 | C.LetIn (s, w, v, t) ->
62 if K.not_prop1 c w then
63 let dt, tt = proc_term (K.add_def s w v c) t in
64 dt @ K.add_def s w v [], tt
66 let dv, vv = proc_term c v in
67 let l = L.length dv in
69 let w = K.lift K.fst_var l w in
70 let t = K.lift K.snd_var l t in
71 let dt, tt = proc_term (K.add_def s w vv c) t in
72 dt @ (K.add_def s w vv dv), tt
73 | C.Appl [t] -> proc_term c t
74 | C.Appl (C.Appl ts :: vs) -> proc_term c (K.appl (ts @ vs))
75 | C.Appl ts -> proc_appl c t ts
76 | C.Match (w, u, v, ts) -> proc_case c t w u v ts
78 and proc_appl c t ts = match X.foldi_left (proc_arg c) 1 initial ts with
80 | Some (i, s, w, v), rtts ->
81 let ri = L.length rtts - i in
82 let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
83 proc_term c (K.letin s w v (K.appl tts))
85 and proc_case c t w u v ts = match X.foldi_left (proc_arg c) 1 initial ts with
87 if K.is_atomic v || K.not_prop1 c (C.Const w) then [], t else
88 let s, w0, v0, vv = anticipate c v in
89 let u = K.lift K.fst_var 1 u in
90 let ts = K.lifts K.fst_var 1 ts in
91 proc_term c (K.letin s w0 v0 (K.case w u vv ts))
92 | Some (i, s, w0, v0), rtts ->
93 let ri = L.length rtts - i in
94 let u = K.lift K.fst_var 1 u in
95 let v = K.lift K.fst_var 1 v in
96 let tts = X.foldi_left (lift_arg ri) 0 [] rtts in
97 proc_term c (K.letin s w0 v0 (K.case w u v tts))
100 let d, tt = proc_term c t in
103 let shift_named_term s c t =
106 let tt = shift_term c t in
107 if !G.test then begin
108 let _ = K.typeof c tt in
113 | T.TypeCheckerFailure s
114 | T.AssertFailure s -> malformed (Lazy.force s)
117 let r, s, i, u, t = c in
118 if K.not_prop1 [] u then c else
119 r, s, i, u, shift_named_term s [] t
121 let proc_obj obj = match obj with
123 | C.Constant (_, _, None, _, _) -> obj
124 | C.Constant (r, s, Some t, u, a) ->
125 if K.not_prop1 [] u then obj else
126 let tt = shift_named_term s [] t in
127 C.Constant (r, s, Some tt, u, a)
128 | C.Fixpoint (b, cs, a) ->
129 C.Fixpoint (b, L.map proc_fun cs, a)
131 (* interface functions ******************************************************)
133 let process_top_term s t = shift_named_term s [] t
135 let process_obj obj = proc_obj obj