else
let p1 =
{ p with
- K.proof_id = gen_id seed;
K.proof_context = [];
K.proof_apply_context = []
} in
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