module E = CicEnvironment
module UM = UriManager
module D = Deannotate
+module PER = ProofEngineReduction
+module Ut = CicUtil
(* fresh name generator *****************************************************)
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.oblivion_ugraph in t
with e ->
Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
raise e
let get_type c t =
- try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+ try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty
with e ->
Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
Printf.eprintf "TC: term : %s\n" (Pp.ppterm t);
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.oblivion_ugraph uri with
| C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
| _ -> assert false
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.CProp _) -> "_rect"
| C.Sort (C.Type _) -> "_rect"
| t ->
Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
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
+
+(* 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
projects / helm.git / blobdiff