let module C = Cic in
let module Con = Content in
let rec extend_premise_env current_env =
- function
+ function
[] -> current_env
- | p::atl ->
+ | p::atl ->
extend_premise_env
((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in
C.LetIn (C.Name s, proof2cic premise_env p, target)
| None ->
C.LetIn (C.Anonymous, proof2cic premise_env p, target))
- | `Joint ho ->
- raise TO_DO
+ | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} ->
+ (match target with
+ C.Rel n ->
+ (match kind with
+ `Recursive l ->
+ let funs =
+ List.map2
+ (fun n bo ->
+ match bo with
+ `Proof bo ->
+ (match
+ bo.Con.proof_conclude.Con.conclude_conclusion,
+ bo.Con.proof_name
+ with
+ Some ty, Some name ->
+ (name,n,term2cic ty,proof2cic premise_env bo)
+ | _,_ -> assert false)
+ | _ -> assert false)
+ l defs in
+ C.Fix (n, funs)
+ | `CoRecursive ->
+ let funs =
+ List.map
+ (function bo ->
+ match bo with
+ `Proof bo ->
+ (match
+ bo.Con.proof_conclude.Con.conclude_conclusion,
+ bo.Con.proof_name
+ with
+ Some ty, Some name ->
+ (name,term2cic ty,proof2cic premise_env bo)
+ | _,_ -> assert false)
+ | _ -> assert false)
+ defs in
+ C.CoFix (n, funs)
+ | _ -> (* no inductive types in local contexts *)
+ assert false)
+ | _ -> assert false)
and conclude2cic premise_env conclude =
let module C = Cic in
else if conclude.Con.conclude_method = "Exact" then
(match conclude.Con.conclude_args with
[Con.Term t] -> term2cic t
+ | [Con.Premise prem] ->
+ (match prem.Con.premise_n with
+ None -> assert false
+ | Some n -> C.Rel n)
| _ -> prerr_endline "3"; assert false)
else if conclude.Con.conclude_method = "Intros+LetTac" then
(match conclude.Con.conclude_args with