exception TO_DO;;
-let proof2cic term2cic p =
+let proof2cic deannotate p =
let rec proof2cic premise_env p =
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
`Declaration d ->
(match d.Con.dec_name with
Some s ->
- C.Lambda (C.Name s, term2cic d.Con.dec_type, target)
+ C.Lambda (C.Name s, deannotate d.Con.dec_type, target)
| None ->
- C.Lambda (C.Anonymous, term2cic d.Con.dec_type, target))
+ C.Lambda (C.Anonymous, deannotate d.Con.dec_type, target))
| `Hypothesis h ->
(match h.Con.dec_name with
Some s ->
- C.Lambda (C.Name s, term2cic h.Con.dec_type, target)
+ C.Lambda (C.Name s, deannotate h.Con.dec_type, target)
| None ->
- C.Lambda (C.Anonymous, term2cic h.Con.dec_type, target))
+ C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target))
| `Proof p ->
(match p.Con.proof_name with
Some s ->
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,deannotate 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,deannotate 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
[Con.Premise prem] ->
(try List.assoc prem.Con.premise_xref premise_env
with Not_found ->
- prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
+ prerr_endline
+ ("Not_found in BU_Conversion: " ^ prem.Con.premise_xref);
raise Not_found)
| _ -> prerr_endline "2"; assert false)
else if conclude.Con.conclude_method = "Exact" then
(match conclude.Con.conclude_args with
- [Con.Term t] -> term2cic t
+ [Con.Term t] -> deannotate 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
[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, term2cic t)) exp_named_subst in
+ List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
let cargs = args2cic premise_env args in
- let cparams_and_IP = List.map term2cic params_and_IP in
+ let cparams_and_IP = List.map deannotate params_and_IP in
C.Appl (C.Const(uri,subst)::cparams_and_IP@cargs)
| _ -> prerr_endline "5"; assert false)
else if (conclude.Con.conclude_method = "Rewrite") then
(match conclude.Con.conclude_args with
Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
let subst =
- List.map (fun (u,t) -> (u, term2cic t)) exp_named_subst in
+ List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst 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
Con.Aux n -> prerr_endline "8"; assert false
| Con.Premise prem ->
(match prem.Con.premise_n with
- Some n ->
- C.Rel n
- | _ ->
+ Some n -> C.Rel n
+ | None ->
(try List.assoc prem.Con.premise_xref premise_env
with Not_found ->
- prerr_endline ("Not_found: " ^ prem.Con.premise_xref);
+ 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 ->
- term2cic t
- | Con.ArgProof p ->
- proof2cic [] p (* empty! *)
+ | Con.Lemma lemma ->
+ CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
+ | Con.Term t -> deannotate t
+ | Con.ArgProof p -> proof2cic [] p (* empty! *)
| Con.ArgMethod s -> raise TO_DO
in proof2cic [] p
;;
-let proof2cic = proof2cic Deannotate.deannotate_term;;
+exception ToDo;;
+
+let cobj2obj deannotate (id,params,metasenv,obj) =
+ let module K = Content in
+ match obj with
+ `Def (Content.Const,ty,`Proof bo) ->
+ (match metasenv with
+ None ->
+ Cic.Constant
+ (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
+ | Some metasenv' ->
+ let metasenv'' =
+ List.map
+ (function (_,i,canonical_context,term) ->
+ let canonical_context' =
+ List.map
+ (function
+ 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) ->
+ (match d with
+ {K.def_name = Some n ; K.def_term = t} ->
+ Some (Cic.Name n, Cic.Def ((deannotate t),None))
+ | _ -> assert false)
+ | Some (`Proof d) ->
+ (match d with
+ {K.proof_name = Some n } ->
+ Some (Cic.Name n,
+ Cic.Def ((proof2cic deannotate d),None))
+ | _ -> assert false)
+ ) canonical_context
+ in
+ (i,canonical_context',deannotate term)
+ ) metasenv'
+ in
+ Cic.CurrentProof
+ (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
+ []))
+ | _ -> raise ToDo
+;;
+
+let cobj2obj = cobj2obj Deannotate.deannotate_term;;
projects / helm.git / blobdiff