(match conclude.Con.conclude_args with
[Con.ArgProof p] -> proof2cic [] p (* empty! *)
| _ -> prerr_endline "4"; assert false)
- else if (conclude.Con.conclude_method = "ByInduction") then
+ else if (conclude.Con.conclude_method = "ByInduction" ||
+ conclude.Con.conclude_method = "AndInd" ||
+ conclude.Con.conclude_method = "Exists" ||
+ conclude.Con.conclude_method = "FalseInd") then
(match (List.tl conclude.Con.conclude_args) with
- Con.Term (C.AAppl
- id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->
+ Con.Term (C.AAppl (
+ id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
let subst =
List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
let cargs = args2cic premise_env args in
let cargs = args2cic premise_env args in
C.Appl (C.Const(uri,subst)::cargs)
| _ -> prerr_endline "6"; assert false)
+ else if (conclude.Con.conclude_method = "Case") then
+ (match conclude.Con.conclude_args with
+ Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
+ C.MutCase
+ (UriManager.uri_of_string uri,
+ int_of_string notype, deannotate ty,
+ List.assoc prem.Con.premise_xref premise_env,
+ List.map
+ (function
+ Con.ArgProof p -> proof2cic [] p
+ | _ -> prerr_endline "7a"; assert false) patterns)
+ | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase
+ (UriManager.uri_of_string uri,
+ int_of_string notype, deannotate ty, deannotate te,
+ List.map
+ (function
+ (Con.ArgProof p) -> proof2cic [] p
+ | _ -> prerr_endline "7a"; assert false) patterns)
+ | _ -> (prerr_endline "7"; assert false))
else if (conclude.Con.conclude_method = "Apply") then
let cargs = (args2cic premise_env conclude.Con.conclude_args) in
C.Appl cargs
- else (prerr_endline "7"; assert false)
+ else (prerr_endline "8"; assert false)
and args2cic premise_env l =
List.map (arg2cic premise_env) l
with Not_found ->
prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
raise Not_found))
- | Con.Term t ->
- deannotate t
- | Con.ArgProof p ->
- proof2cic [] p (* empty! *)
+ | Con.Lemma lemma -> CicUtil.term_of_uri lemma.Con.lemma_uri
+ | Con.Term t -> deannotate t
+ | Con.ArgProof p -> proof2cic [] p (* empty! *)
| Con.ArgMethod s -> raise TO_DO
in proof2cic [] p
(match metasenv with
None ->
Cic.Constant
- (id, Some (proof2cic deannotate bo), deannotate ty, params)
+ (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
| Some metasenv' ->
let metasenv'' =
List.map
let canonical_context' =
List.map
(function
- _,None -> None
- | _,Some (`Declaration d)
- | _,Some (`Hypothesis d) ->
+ None -> None
+ | Some (`Declaration d)
+ | Some (`Hypothesis d) ->
(match d with
{K.dec_name = Some n ; K.dec_type = t} ->
Some (Cic.Name n, Cic.Decl (deannotate t))
| _ -> assert false)
- | _,Some (`Definition d) ->
+ | Some (`Definition d) ->
(match d with
{K.def_name = Some n ; K.def_term = t} ->
- Some (Cic.Name n, Cic.Def (deannotate t))
+ Some (Cic.Name n, Cic.Def ((deannotate t),None))
| _ -> assert false)
- | _,Some (`Proof d) ->
+ | Some (`Proof d) ->
(match d with
{K.proof_name = Some n } ->
- Some (Cic.Name n, Cic.Def (proof2cic deannotate d))
+ Some (Cic.Name n,
+ Cic.Def ((proof2cic deannotate d),None))
| _ -> assert false)
) canonical_context
in
) metasenv'
in
Cic.CurrentProof
- (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
+ (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
+ []))
| _ -> raise ToDo
;;