From a6d30b023b3b9b729563a94f278771c8cf32e123 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 22 Nov 2005 18:04:55 +0000 Subject: [PATCH] - more resilient to proof checking failures during pretty printing - do not compute inner types for sequents --- helm/ocaml/cic_omdoc/cic2acic.ml | 61 +++++++++++++------- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 17 ++++-- helm/ocaml/cic_omdoc/doubleTypeInference.mli | 1 + 3 files changed, 51 insertions(+), 28 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 81cfaaf09..1cdabc09f 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -51,7 +51,14 @@ let type_of_aux'_add_time = ref 0.0;; *) let xxx_type_of_aux' m c t = (* let t1 = Sys.time () in *) - let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in + let res,_ = + try + CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph + with + | CicTypeChecker.AssertFailure _ + | CicTypeChecker.TypeCheckerFailure _ -> + Cic.Sort Cic.Prop, CicUniv.empty_ugraph + in (* let t2 = Sys.time () in type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; *) res @@ -89,8 +96,9 @@ let rec get_nth l n = | (_,_) -> raise NotEnoughElements ;; -let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - ids_to_inner_types metasenv context idrefs t expectedty +let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes + seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types + metasenv context idrefs t expectedty = let module D = DoubleTypeInference in let module C = Cic in @@ -107,7 +115,10 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1))); res *) - D.double_type_of metasenv context t expectedty + if global_computeinnertypes then + D.double_type_of metasenv context t expectedty + else + D.CicHash.empty () in (* let time2 = Sys.time () in @@ -150,10 +161,13 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts else (* We are already in an inner-type and Coscoy's double *) (* type inference algorithm has not been applied. *) - {D.synthesized = + { D.synthesized = (***CSC: patch per provare i tempi CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *) -Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) + if global_computeinnertypes then + Cic.Sort (Cic.Type (CicUniv.fresh())) + else + CicReduction.whd context (xxx_type_of_aux' metasenv context tt); D.expected = None} in (* incr number_new_type_of_aux' ; *) @@ -355,23 +369,25 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ; res *) - aux true None context idrefs t + aux global_computeinnertypes None context idrefs t ;; -let acic_of_cic_context metasenv context idrefs t = +let acic_of_cic_context ~computeinnertypes metasenv context idrefs t = let ids_to_terms = Hashtbl.create 503 in let ids_to_father_ids = Hashtbl.create 503 in let ids_to_inner_sorts = Hashtbl.create 503 in let ids_to_inner_types = Hashtbl.create 503 in let seed = ref 0 in - acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts + acic_of_cic_context' ~computeinnertypes seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types metasenv context idrefs t, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types ;; let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed - metasenv (metano,context,goal) = + metasenv (metano,context,goal) += + let computeinnertypes = false in let acic_of_cic_context = acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types metasenv in @@ -383,11 +399,11 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids incr hypotheses_seed ; match binding with Some (n,Cic.Def (t,_)) -> - let acic = acic_of_cic_context context idrefs t None in + let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in (binding::context), ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs) | Some (n,Cic.Decl t) -> - let acic = acic_of_cic_context context idrefs t None in + let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in (binding::context), ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs) | None -> @@ -396,7 +412,7 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids ) context ([],[],[]) ) in - let agoal = acic_of_cic_context context final_idrefs goal None in + let agoal = acic_of_cic_context ~computeinnertypes context final_idrefs goal None in (metano,acontext,agoal) ;; @@ -465,13 +481,13 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = C.Constant (id,Some bo,ty,params,attrs) -> let bo' = eta_fix [] [] bo in let ty' = eta_fix [] [] ty in - let abo = acic_term_of_cic_term' bo' (Some ty') in - let aty = acic_term_of_cic_term' ty' None in + let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in + let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in C.AConstant ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs) | C.Constant (id,None,ty,params,attrs) -> let ty' = eta_fix [] [] ty in - let aty = acic_term_of_cic_term' ty' None in + let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in C.AConstant ("mettereaposto",None,id,None,aty,params,attrs) | C.Variable (id,bo,ty,params,attrs) -> @@ -481,9 +497,9 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = None -> None | Some bo -> let bo' = eta_fix [] [] bo in - Some (acic_term_of_cic_term' bo' (Some ty')) + Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty')) in - let aty = acic_term_of_cic_term' ty' None in + let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in C.AVariable ("mettereaposto",id,abo,aty,params,attrs) | C.CurrentProof (id,conjectures,bo,ty,params,attrs) -> @@ -532,8 +548,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = DoubleTypeInference.syntactic_equality_add_time := 0.0 ; *) let abo = - acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in - let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in + acic_term_of_cic_term_context' ~computeinnertypes:true conjectures' [] [] bo' (Some ty') in + let aty = acic_term_of_cic_term_context' ~computeinnertypes:false conjectures' [] [] ty' None in (* let time3 = Sys.time () in prerr_endline @@ -569,10 +585,11 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = List.map (function (name,ty) -> (name, - acic_term_of_cic_term_context' [] context idrefs ty None) + acic_term_of_cic_term_context' ~computeinnertypes:false [] context idrefs ty None) ) cons in - (id,name,inductive,acic_term_of_cic_term' ty None,acons) + (id,name,inductive, + acic_term_of_cic_term' ~computeinnertypes:false ty None,acons) ) (List.rev idrefs) tys in C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs) diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index b514319c1..692872439 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -324,12 +324,17 @@ let type_of_mutual_inductive_constr uri i j = ;; module CicHash = - Hashtbl.Make - (struct - type t = Cic.term - let equal = (==) - let hash = Hashtbl.hash - end) + struct + module Tmp = + Hashtbl.Make + (struct + type t = Cic.term + let equal = (==) + let hash = Hashtbl.hash + end) + include Tmp + let empty () = Tmp.create 1 + end ;; (* type_of_aux' is just another name (with a different scope) for type_of_aux *) diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli index 20230e3bb..138aad834 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.mli +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli @@ -18,6 +18,7 @@ module CicHash : sig type 'a t val find : 'a t -> Cic.term -> 'a + val empty: unit -> 'a t end ;; -- 2.39.2