module PEH = ProofEngineHelpers
module E = CicEnvironment
module UM = UriManager
+module D = Deannotate
+module PER = ProofEngineReduction
+module Ut = CicUtil
+
+(* raw cic prettyprinter ****************************************************)
+
+let xiter out so ss sc map l =
+ let rec aux = function
+ | hd :: tl when tl <> [] -> map hd; out ss; aux tl
+ | hd :: tl -> map hd; aux tl
+ | [] -> ()
+ in
+ out so; aux l; out sc
+
+let abst s w = Some (s, C.Decl w)
+
+let abbr s v w = Some (s, C.Def (v, w))
+
+let pp_sort out = function
+ | C.Type _ -> out "*Type"
+ | C.Prop -> out "*Prop"
+ | C.CProp _ -> out "*CProp"
+ | C.Set -> out "*Set"
+
+let pp_name out = function
+ | C.Name s -> out s
+ | C.Anonymous -> out "_"
+
+let pp_rel out c i =
+ try match List.nth c (pred i) with
+ | None -> out (Printf.sprintf "%u[?]" i)
+ | Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
+ with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
+
+let pp_implict out = function
+ | None -> out "?"
+ | Some `Closed -> out "?[Closed]"
+ | Some `Type -> out "?[Type]"
+ | Some `Hole -> out "?[Hole]"
+
+let pp_uri out a =
+ out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
+
+let rec pp_term out e c = function
+ | C.Sort h -> pp_sort out h
+ | C.Rel i -> pp_rel out c i
+ | C.Implicit x -> pp_implict out x
+ | C.Meta (i, iss) ->
+ let map = function None -> out "_" | Some v -> pp_term out e c v in
+ out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
+ | C.Var (a, xss) ->
+ pp_uri out a; pp_xss out e c xss
+ | C.Const (a, xss) ->
+ pp_uri out a; pp_xss out e c xss
+ | C.MutInd (a, m, xss) ->
+ pp_uri out a; out (Printf.sprintf "/%u" m);
+ pp_xss out e c xss
+ | C.MutConstruct (a, m, n, xss) ->
+ pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
+ pp_xss out e c xss
+ | C.Cast (v, w) ->
+ out "type "; pp_term out e c w; out " contains "; pp_term out e c v
+ | C.Appl vs ->
+ xiter out "(" " @ " ")" (pp_term out e c) vs
+ | C.MutCase (a, m, w, v, vs) ->
+ out "match "; pp_term out e c v;
+ out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
+ out " to "; pp_term out e c w;
+ xiter out " cases " " | " "" (pp_term out e c) vs
+ | C.Prod (s, w, t) ->
+ out "forall "; pp_name out s; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abst s w :: c) t
+ | C.Lambda (s, w, t) ->
+ out "fun "; pp_name out s; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abst s w :: c) t
+ | C.LetIn (s, v, w, t) ->
+ out "let "; pp_name out s;
+ out " def "; pp_term out e c v; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abbr s v w :: c) t
+ | C.Fix (i, fs) ->
+ let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
+ let c' = List.fold_left map c fs in
+ let map (s, i, w, v) =
+ out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
+ out " of "; pp_term out e c w;
+ in
+ xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
+ | C.CoFix (i, fs) ->
+ let map c (s, w, v) = abbr (C.Name s) v w :: c in
+ let c' = List.fold_left map c fs in
+ let map (s, w, v) =
+ out s; pp_term out e c' v;
+ out " of "; pp_term out e c w;
+ in
+ xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
+
+and pp_xss out e c xss =
+ let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
+ xiter out "[" "; " "]" map xss
(* fresh name generator *****************************************************)
let join (s, i) =
C.Name (if i < 0 then s else s ^ string_of_int i)
-let mk_fresh_name context name =
+let mk_fresh_name context (name, k) =
let rec aux i = function
| [] -> name, i
| Some (C.Name s, _) :: entries ->
if m = name && j >= i then aux (succ j) entries else aux i entries
| _ :: entries -> aux i entries
in
- join (aux (-1) context)
+ join (aux k context)
let mk_fresh_name context = function
| C.Anonymous -> C.Anonymous
- | C.Name s -> mk_fresh_name context s
+ | C.Name s -> mk_fresh_name context (split s)
(* helper functions *********************************************************)
+let rec list_fold_right_cps g map l a =
+ match l with
+ | [] -> g a
+ | hd :: tl ->
+ let h a = map g hd a in
+ list_fold_right_cps h map tl a
+
+let rec list_fold_left_cps g map a = function
+ | [] -> g a
+ | hd :: tl ->
+ let h a = list_fold_left_cps g map a tl in
+ map h a hd
+
let rec list_map_cps g map = function
| [] -> g []
| hd :: tl ->
let fst3 (x, _, _) = x
let refine c t =
- try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
+ try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
with e ->
Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
raise e
-let get_type c t =
- try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
- with e ->
- Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
- Printf.eprintf "TC: term : %s\n" (Pp.ppterm t);
- raise e
+let get_type msg c t =
+ let log s =
+ prerr_endline ("TC: " ^ s);
+ prerr_endline ("TC: context: " ^ Pp.ppcontext c);
+ prerr_string "TC: term : "; pp_term prerr_string [] c t;
+ prerr_newline (); prerr_endline ("TC: location: " ^ msg)
+ in
+ try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
+ | TC.TypeCheckerFailure s as e ->
+ log ("failure: " ^ Lazy.force s); raise e
+ | TC.AssertFailure s as e ->
+ log ("assert : " ^ Lazy.force s); raise e
let get_tail c t =
match PEH.split_with_whd (c, t) with
| _ -> assert false
let is_proof c t =
- match get_tail c (get_type c (get_type c t)) with
+ match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
| C.Sort C.Prop -> true
| C.Sort _ -> false
| _ -> assert false
+let is_sort = function
+ | C.Sort _ -> true
+ | _ -> false
+
let is_unsafe h (c, t) = true
let is_not_atomic = function
| C.MutConstruct _ -> false
| _ -> true
+let is_atomic t = not (is_not_atomic t)
+
let get_ind_type uri tyno =
- match E.get_obj Un.empty_ugraph uri with
+ match E.get_obj Un.default_ugraph uri with
| C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
| _ -> assert false
+let get_ind_names uri tno =
+try
+ let ts = match E.get_obj Un.default_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 "get_ind_names"
+
let get_default_eliminator context uri tyno ty =
let _, (name, _, _, _) = get_ind_type uri tyno in
- let ext = match get_tail context (get_type context ty) with
- | C.Sort C.Prop -> "_ind"
- | C.Sort C.Set -> "_rec"
- | C.Sort C.CProp -> "_rec"
- | C.Sort (C.Type _) -> "_rect"
- | t ->
+ let ext = match get_tail context (get_type "get_def_elim" context ty) with
+ | C.Sort C.Prop -> "_ind"
+ | C.Sort C.Set -> "_rec"
+ | C.Sort (C.CProp _) -> "_rect"
+ | C.Sort (C.Type _) -> "_rect"
+ | t ->
Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
assert false
in
C.Const (uri, [])
let get_ind_parameters c t =
- let ty = get_type c t in
+ let ty = get_type "get_ind_pars 1" c t in
let ps = match get_tail c ty with
| C.MutInd _ -> []
| C.Appl (C.MutInd _ :: args) -> args
| _ -> assert false
in
- let disp = match get_tail c (get_type c ty) with
+ let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
| C.Sort C.Prop -> 0
| C.Sort _ -> 1
| _ -> assert false
in
ps, disp
+
+let cic = D.deannotate_term
+
+let occurs c ~what ~where =
+ let result = ref false in
+ let equality c t1 t2 =
+ let r = Ut.alpha_equivalence t1 t2 in
+ result := !result || r; r
+ in
+ let context, what, with_what = c, [what], [C.Rel 0] in
+ let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
+ !result
+
+let name_of_uri uri tyno cno =
+ let get_ind_type tys tyno =
+ let s, _, _, cs = List.nth tys tyno in s, cs
+ in
+ match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
+ | C.Variable (s, _, _, _, _), _, _ -> s
+ | C.Constant (s, _, _, _, _), _, _ -> s
+ | C.InductiveDefinition (tys, _, _, _), Some i, None ->
+ let s, _ = get_ind_type tys i in s
+ | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
+ let _, cs = get_ind_type tys i in
+ let s, _ = List.nth cs (pred j) in s
+ | _ -> assert false
+
+(* Ensuring Barendregt convenction ******************************************)
+
+let rec add_entries map c = function
+ | [] -> c
+ | hd :: tl ->
+ let sname, w = map hd in
+ let entry = Some (Cic.Name sname, C.Decl w) in
+ add_entries map (entry :: c) tl
+
+let get_sname c i =
+ try match List.nth c (pred i) with
+ | Some (Cic.Name sname, _) -> sname
+ | _ -> assert false
+ with
+ | Failure _ -> assert false
+ | Invalid_argument _ -> assert false
+
+let cic_bc c t =
+ let get_fix_decl (sname, i, w, v) = sname, w in
+ let get_cofix_decl (sname, w, v) = sname, w in
+ let rec bc c = function
+ | C.LetIn (name, v, ty, t) ->
+ let name = mk_fresh_name c name in
+ let entry = Some (name, C.Def (v, ty)) in
+ let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+ C.LetIn (name, v, ty, t)
+ | C.Lambda (name, w, t) ->
+ let name = mk_fresh_name c name in
+ let entry = Some (name, C.Decl w) in
+ let w, t = bc c w, bc (entry :: c) t in
+ C.Lambda (name, w, t)
+ | C.Prod (name, w, t) ->
+ let name = mk_fresh_name c name in
+ let entry = Some (name, C.Decl w) in
+ let w, t = bc c w, bc (entry :: c) t in
+ C.Prod (name, w, t)
+ | C.Appl vs ->
+ let vs = List.map (bc c) vs in
+ C.Appl vs
+ | C.MutCase (uri, tyno, u, v, ts) ->
+ let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
+ C.MutCase (uri, tyno, u, v, ts)
+ | C.Cast (t, u) ->
+ let t, u = bc c t, bc c u in
+ C.Cast (t, u)
+ | C.Fix (i, fixes) ->
+ let d = add_entries get_fix_decl c fixes in
+ let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
+ let fixes = List.map bc_fix fixes in
+ C.Fix (i, fixes)
+ | C.CoFix (i, cofixes) ->
+ let d = add_entries get_cofix_decl c cofixes in
+ let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
+ let cofixes = List.map bc_cofix cofixes in
+ C.CoFix (i, cofixes)
+ | t -> t
+ in
+ bc c t
+
+let acic_bc c t =
+ let get_fix_decl (id, sname, i, w, v) = sname, cic w in
+ let get_cofix_decl (id, sname, w, v) = sname, cic w in
+ let rec bc c = function
+ | C.ALetIn (id, name, v, ty, t) ->
+ let name = mk_fresh_name c name in
+ let entry = Some (name, C.Def (cic v, cic ty)) in
+ let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+ C.ALetIn (id, name, v, ty, t)
+ | C.ALambda (id, name, w, t) ->
+ let name = mk_fresh_name c name in
+ let entry = Some (name, C.Decl (cic w)) in
+ let w, t = bc c w, bc (entry :: c) t in
+ C.ALambda (id, name, w, t)
+ | C.AProd (id, name, w, t) ->
+ let name = mk_fresh_name c name in
+ let entry = Some (name, C.Decl (cic w)) in
+ let w, t = bc c w, bc (entry :: c) t in
+ C.AProd (id, name, w, t)
+ | C.AAppl (id, vs) ->
+ let vs = List.map (bc c) vs in
+ C.AAppl (id, vs)
+ | C.AMutCase (id, uri, tyno, u, v, ts) ->
+ let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
+ C.AMutCase (id, uri, tyno, u, v, ts)
+ | C.ACast (id, t, u) ->
+ let t, u = bc c t, bc c u in
+ C.ACast (id, t, u)
+ | C.AFix (id, i, fixes) ->
+ let d = add_entries get_fix_decl c fixes in
+ let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
+ let fixes = List.map bc_fix fixes in
+ C.AFix (id, i, fixes)
+ | C.ACoFix (id, i, cofixes) ->
+ let d = add_entries get_cofix_decl c cofixes in
+ let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
+ let cofixes = List.map bc_cofix cofixes in
+ C.ACoFix (id, i, cofixes)
+ | C.ARel (id1, id2, i, sname) ->
+ let sname = get_sname c i in
+ C.ARel (id1, id2, i, sname)
+ | t -> t
+ in
+ bc c t