module C = Cic
module Un = CicUniv
module E = CicEnvironment
+module Ut = CicUtil
+module TC = CicTypeChecker
let hashtbl_size = 11
let debug = ref false
+let out = prerr_string
+
(* helper functions *********************************************************)
+let typecheck t =
+ if !debug then begin
+ let _ = TC.type_of_aux' [] [] t Un.default_ugraph in
+ out "Typecheck : OK\n"
+ end
+
let list_pos found l =
let rec aux n = function
| [] -> raise Not_found
if vs' == vs then t else C.Appl (flatten vs')
| C.Cast (v, w) ->
let v', w' = discharge_term st v, discharge_term st w in
- if v' = v && w' = w then t else
+ if v' == v && w' == w then t else
C.Cast (sh v v', sh w w')
| C.MutCase (u, m, w, v, vs) ->
+ let args = get_args st u in
+ let u' = if args = [] then u else st.du u in
let w', v', vs' =
discharge_term st w, discharge_term st v,
list_map_sh (discharge_term st) vs
in
- if w' = w && v' = v && vs' == vs then t else
- C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
+ if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
+ C.MutCase (u', m, sh w w', sh v v', sh vs vs')
| C.Prod (b, w, v) ->
let w', v' = discharge_term st w, discharge_term (add st 1) v in
- if w' = w && v' = v then t else
+ if w' == w && v' == v then t else
C.Prod (b, sh w w', sh v v')
| C.Lambda (b, w, v) ->
let w', v' = discharge_term st w, discharge_term (add st 1) v in
- if w' = w && v' = v then t else
+ if w' == w && v' == v then t else
C.Lambda (b, sh w w', sh v v')
| C.LetIn (b, y, w, v) ->
let y', w', v' =
discharge_term st y, discharge_term st w, discharge_term (add st 1) v
in
- if y' = y && w' = w && v' == v then t else
+ if y' == y && w' == w && v' == v then t else
C.LetIn (b, sh y y', sh w w', sh v v')
| C.CoFix (i, s) ->
let no = List.length s in
and discharge_cofun st no f =
let b, w, v = f in
let w', v' = discharge_term st w, discharge_term (add st no) v in
- if w' = w && v' = v then f else
+ if w' == w && v' == v then f else
b, sh w w', sh v v'
and discharge_fun st no f =
let b, i, w, v = f in
let w', v' = discharge_term st w, discharge_term (add st no) v in
- if w' = w && v' = v then f else
+ if w' == w && v' == v then f else
b, i, sh w w', sh v v'
let close is_type st t =
| C.Variable (b, None, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w' = discharge_term st w in
- if w' = w && vars = [] then obj else
+ if w' == w && vars = [] then obj else
let w'' = sh w w' in
+ let _ = typecheck w'' in
C.Variable (dn b, None, w'', [], attrs)
| C.Variable (b, Some v, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w', v' = discharge_term st w, discharge_term st v in
- if w' = w && v' = v && vars = [] then obj else
+ if w' == w && v' == v && vars = [] then obj else
let w'', v'' = sh w w', sh v v' in
+ let _ = typecheck (C.Cast (v'', w'')) in
C.Variable (dn b, Some v'', w'', [], attrs)
| C.Constant (b, None, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w' = discharge_term st w in
- if w' = w && vars = [] then obj else
+ if w' == w && vars = [] then obj else
let w'' = close true st (sh w w') in
+ let _ = typecheck w'' in
C.Constant (dn b, None, w'', [], attrs)
| C.Constant (b, Some v, w, vars, attrs) ->
let st = init_status dn du ls vars in
let w', v' = discharge_term st w, discharge_term st v in
- if w' = w && v' = v && vars = [] then obj else
+ if w' == w && v' == v && vars = [] then obj else
let w'', v'' = close true st (sh w w'), close false st (sh v v') in
+ let _ = typecheck (C.Cast (v'', w'')) in
C.Constant (dn b, Some v'', w'', [], attrs)
| C.InductiveDefinition (types, vars, lpsno, attrs) ->
let st = init_status dn du ls vars in
HLog.warn not_implemented; obj
and discharge_uri dn du uri =
+ let prerr msg obj =
+ if !debug then begin
+ out msg; Ut.pp_obj out obj; out "\n"
+ end
+ in
let obj, _ = E.get_obj Un.default_ugraph uri in
- if !debug then prerr_endline ("Plain : " ^ CicPp.ppobj obj);
+ prerr "Plain : " obj;
let obj' = discharge_object dn du obj in
- if !debug then prerr_endline ("Discharged: " ^ CicPp.ppobj obj');
+ prerr "Discharged: " obj';
obj', obj' == obj
and discharge_vars dn du vars =