X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=72699f7e3cb2b584da6617a278a1b1f611945abd;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=81f0683c6390530b1fabcb87437079084c79c77f;hpb=2f15a81dcd6e5ada3f1b4fa6300e9a1347c8d12c;p=helm.git diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 81f0683c6..72699f7e3 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -122,7 +122,7 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts= with Not_found -> false) | C.AMeta (id,_,_) -> (try - Hashtbl.find ids_to_inner_sorts id = "Prop" + Hashtbl.find ids_to_inner_sorts id = `Prop with Not_found -> assert false) | C.ASort (id,_) -> false | C.AImplicit _ -> raise NotImplemented @@ -300,7 +300,7 @@ let build_decl_item seed id n s ~ids_to_inner_sorts = with Not_found -> None in match sort with - | Some "Prop" -> + | Some `Prop -> `Hypothesis { K.dec_name = name_of n; K.dec_id = gen_id declaration_prefix seed; @@ -343,9 +343,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts (match t with C.ARel (idr,idref,n,b) -> let sort = - (try Hashtbl.find ids_to_inner_sorts idr - with Not_found -> "Type") in - if sort ="Prop" then + (try + Hashtbl.find ids_to_inner_sorts idr + with Not_found -> `Type (CicUniv.fresh())) in + if sort = `Prop then K.Premise { K.premise_id = gen_id premise_prefix seed; K.premise_xref = idr; @@ -355,9 +356,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts else (K.Term t) | C.AConst(id,uri,[]) -> let sort = - (try Hashtbl.find ids_to_inner_sorts id - with Not_found -> "Type") in - if sort ="Prop" then + (try + Hashtbl.find ids_to_inner_sorts id + with Not_found -> `Type (CicUniv.fresh())) in + if sort = `Prop then K.Lemma { K.lemma_id = gen_id lemma_prefix seed; K.lemma_name = UriManager.name_of_uri uri; @@ -366,9 +368,10 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts else (K.Term t) | C.AMutConstruct(id,uri,tyno,consno,[]) -> let sort = - (try Hashtbl.find ids_to_inner_sorts id - with Not_found -> "Type") in - if sort ="Prop" then + (try + Hashtbl.find ids_to_inner_sorts id + with Not_found -> `Type (CicUniv.fresh())) in + if sort = `Prop then let inductive_types = (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri @@ -408,7 +411,7 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types = let module K = Content in try let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then (let p = (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t) in @@ -436,17 +439,17 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = match t with C.ARel (id,idref,n,b) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AVar (id,uri,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMeta (id,n,l) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.ASort (id,s) -> raise Not_a_proof @@ -455,7 +458,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = | C.ACast (id,v,t) -> aux v | C.ALambda (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then let proof = aux t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then @@ -475,7 +478,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = else raise Not_a_proof | C.ALetIn (id,n,s,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then let proof = aux t in let proof' = if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then @@ -530,13 +533,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = }) | C.AConst (id,uri,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t -> let sort = Hashtbl.find ids_to_inner_sorts id in - if sort = "Prop" then + if sort = `Prop then generate_exact seed t id name ~ids_to_inner_types else raise Not_a_proof | C.AMutCase (id,uri,typeno,ty,te,patterns) -> @@ -600,6 +603,9 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = let proofs = List.map (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in + let fun_name = + List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no + in let decreasing_args = List.map (function (_,_,n,_,_) -> n) funs in let jo = @@ -620,7 +626,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = [ K.Premise { K.premise_id = gen_id premise_prefix seed; K.premise_xref = jo.K.joint_id; - K.premise_binder = Some "tiralo fuori"; + K.premise_binder = Some fun_name; K.premise_n = Some no; } ]; @@ -725,9 +731,9 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let idarg = get_id arg in let sortarg = (try (Hashtbl.find ids_to_inner_sorts idarg) - with Not_found -> "Type") in + with Not_found -> `Type (CicUniv.fresh())) in let hdarg = - if sortarg = "Prop" then + if sortarg = `Prop then let (co,bo) = let rec bc = function @@ -810,8 +816,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = else let aid = get_id a in let asort = (try (Hashtbl.find ids_to_inner_sorts aid) - with Not_found -> "Type") in - if asort = "Prop" then + with Not_found -> `Type (CicUniv.fresh())) in + if asort = `Prop then K.ArgProof (aux a) else K.Term a in hd::(ma_aux (n-1) tl) in