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 inc st =
{st with case = match st.case with
- | [] -> assert false
+ | [] -> []
| hd :: tl -> succ hd :: tl
}
with Not_found -> `Type (CicUniv.fresh())
with Invalid_argument _ -> failwith "A2P.get_sort"
*)
-let get_type msg st bo =
-try
- let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
- ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
let get_entry st id =
let rec aux = function
| [] -> assert false
in
aux st.context
-let get_ind_names uri tno =
-try
- let ts = match E.get_obj Un.oblivion_ugraph uri with
- | C.InductiveDefinition (ts, _, _, _), _ -> ts
- | _ -> assert false
- in
- match List.nth ts tno with
- | (_, _, _, cs) -> List.map fst cs
-with Invalid_argument _ -> failwith "A2P.get_ind_names"
-
let string_of_atomic = function
| C.ARel (_, _, _, s) -> s
| C.AVar (_, uri, _) -> H.name_of_uri uri None None
let names, _ = List.fold_left map ([], 1) l in
List.rev names
+let get_type msg st t = H.get_type msg st.context (H.cic t)
+
(* proof construction *******************************************************)
let anonymous_premise = C.Name "PREMISE"
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
let classes2, tl2, _, where = split2_last classes tl in
let script2 = List.rev (mk_arg st where) @ script in
let synth2 = I.S.add 1 synth in
- let names = get_ind_names uri tyno in
+ let names = H.get_ind_names uri tyno in
let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
if List.length qs <> List.length names then
let qs = proc_bkd_proofs (next st) synth [] classes tl in
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 =