try
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = "Prop" then
- `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
+ `Proof (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
else
`Definition
{ K.def_name = name_of n;
Prop. For debugging purposes this is tested again, possibly raising an
Not_a_proof exception *)
-and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
- let rec aux ?(name = None) t =
+and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
+ let rec aux ?name t =
let module C = Cic in
let module K = Content in
let module C2A = Cic2acic in
| C.ALambda (id,n,s,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = "Prop" then
- let proof = aux t ~name:None in
+ let proof = aux t in
let proof' =
if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
match proof.K.proof_conclude.K.conclude_args with
let subproofs =
match args_to_lift with
[_] -> List.map aux args_to_lift
- | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
+ | _ -> List.map (aux ~name:"H") args_to_lift in
let args = build_args seed li subproofs
~ids_to_inner_types ~ids_to_inner_sorts in
{ K.proof_name = name;
}
}
)
- | C.AFix (id, no, [(id1,n,_,ty,bo)]) ->
- let proof = (aux bo) in (* must be recursive !! *)
- { K.proof_name = name;
- K.proof_id = gen_id seed;
- K.proof_context = [`Proof proof];
- K.proof_apply_context = [];
- K.proof_conclude =
- { K.conclude_id = gen_id seed;
- K.conclude_aref = id;
- K.conclude_method = "Exact";
- K.conclude_args =
- [ K.Premise
- { K.premise_id = gen_id seed;
- K.premise_xref = proof.K.proof_id;
- K.premise_binder = proof.K.proof_name;
- K.premise_n = Some 1;
- }
- ];
- K.conclude_conclusion =
- try Some
- (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
- with Not_found -> None
- }
- }
| C.AFix (id, no, funs) ->
let proofs =
- List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in
+ List.map
+ (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
+ let decreasing_args =
+ List.map (function (_,_,n,_,_) -> n) funs in
let jo =
{ K.joint_id = gen_id seed;
- K.joint_kind = `Recursive;
+ K.joint_kind = `Recursive decreasing_args;
K.joint_defs = proofs
}
in
with Not_found -> None
}
}
- | C.ACoFix (id,no,[(id1,n,ty,bo)]) ->
- let proof = (aux bo) in (* must be recursive !! *)
- { K.proof_name = name;
- K.proof_id = gen_id seed;
- K.proof_context = [`Proof proof];
- K.proof_apply_context = [];
- K.proof_conclude =
- { K.conclude_id = gen_id seed;
- K.conclude_aref = id;
- K.conclude_method = "Exact";
- K.conclude_args =
- [ K.Premise
- { K.premise_id = gen_id seed;
- K.premise_xref = proof.K.proof_id;
- K.premise_binder = proof.K.proof_name;
- K.premise_n = Some 1;
- }
- ];
- K.conclude_conclusion =
- try Some
- (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
- with Not_found -> None
- }
- }
| C.ACoFix (id,no,funs) ->
let proofs =
- List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in
+ List.map
+ (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
let jo =
{ K.joint_id = gen_id seed;
- K.joint_kind = `Recursive;
+ K.joint_kind = `CoRecursive;
K.joint_defs = proofs
}
in
in
let id = get_id t in
generate_conversion seed false id t1 ~ids_to_inner_types
-in aux ~name:name t
+in aux ?name t
and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
- let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
+ let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
let subproofs =
match args_to_lift with
[_] -> List.map aux args_to_lift
- | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
+ | _ -> List.map (aux ~name:"H") args_to_lift in
prerr_endline "****** end subproofs *******"; flush stderr;
let other_method_args =
build_args seed other_args subproofs
( prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr;
let (context,body) = bc (t,t1) in
(ce::context,body))
- | _ , t -> ([],aux t ~name:None) in
+ | _ , t -> ([],aux t) in
bc (ty,arg) in
K.ArgProof
{ bo with
| _ -> raise NotApplicable
and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
- let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
+ let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic 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
projects / helm.git / commitdiff