module HEL = HExtlib
module DTI = DoubleTypeInference
module NU = CicNotationUtil
+module L = Librarian
module Cl = ProceduralClassify
module T = ProceduralTypes
case: int list
}
-let debug = false
+let debug = ref false
(* helpers ******************************************************************)
let e = Cn.hole "" in
let csty, cety = H.cic sty, H.cic ety in
let script =
- if debug then
+ if !debug then
let sname = match name with None -> "" | Some (id, _) -> id in
let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
note sname (Pp.ppterm csty) (Pp.ppterm cety)
let convert st ?name v =
match get_inner_types st v with
| None ->
- if debug then [T.Note "NORMAL: NO INNER TYPES"] else []
+ if !debug then [T.Note "NORMAL: NO INNER TYPES"] else []
| Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
let convert_elim st ?name t v pattern =
and proc_appl st what hd tl =
let proceed, dtext = test_depth st in
let script = if proceed then
- let ty = get_type "TC2" st hd in
+ let ty = match get_inner_types st hd with
+ | Some (ity, _) -> H.cic ity
+ | None -> get_type "TC2" st hd
+ in
let classes, rc = Cl.classify st.context ty in
let goal_arity, goal = match get_inner_types st what with
| None -> 0, None
context = [];
case = []
} in
+ L.time_stamp "P : LEVEL 2 ";
HLog.debug "Procedural: level 2 transformation";
let steps = proc_obj st ?flavour anobj in
+ L.time_stamp "P : RENDERING";
HLog.debug "Procedural: grafite rendering";
- List.rev (T.render_steps [] steps)
+ let r = List.rev (T.render_steps [] steps) in
+ L.time_stamp "P : DONE "; r
let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
prefix context annterm =