From 7e60b896247a228beea1b2a547c1f606e1834921 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 12 Jun 2002 16:03:09 +0000 Subject: [PATCH] * Abst removed from the DTD * real double-type-inference algorithm implemented * performance improved again (25s for limit_mul). Why??? * Bug left: the double-type annotation is not generated in the case of a lambda inside another lambda. To be fixed soon. --- helm/gTopLevel/.depend | 2 + helm/gTopLevel/Makefile | 8 +- helm/gTopLevel/cic2Xml.ml | 10 +- helm/gTopLevel/cic2acic.ml | 292 ++++++++++--------- helm/gTopLevel/cic2acic.mli | 9 +- helm/gTopLevel/doubleTypeInference.ml | 372 ++++++++++++++++++++----- helm/gTopLevel/doubleTypeInference.mli | 10 +- helm/gTopLevel/gTopLevel.ml | 9 + helm/gTopLevel/logicalOperations.ml | 1 - helm/gTopLevel/mquery.ml | 1 - helm/gTopLevel/proofEngine.ml | 3 +- helm/gTopLevel/proofEngineReduction.ml | 8 +- helm/gTopLevel/sequentPp.ml | 4 +- 13 files changed, 488 insertions(+), 241 deletions(-) diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 7d0186948..4ffdddf54 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -4,6 +4,8 @@ doubleTypeInference.cmo: doubleTypeInference.cmi doubleTypeInference.cmx: doubleTypeInference.cmi cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi +cic2Xml.cmo: cic2acic.cmi +cic2Xml.cmx: cic2acic.cmx logicalOperations.cmo: proofEngine.cmo logicalOperations.cmx: proofEngine.cmx sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmo diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 8a9c5e535..0fc38eac9 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -14,13 +14,13 @@ LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICA all: gTopLevel opt: gTopLevel.opt -DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \ +DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml \ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ - cic2acic.mli logicalOperations.ml sequentPp.ml mquery.mli \ - mquery.ml gTopLevel.ml + cic2Xml.ml cic2acic.mli logicalOperations.ml sequentPp.ml \ + mquery.mli mquery.ml gTopLevel.ml TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \ - cic2Xml.cmo doubleTypeInference.cmo cic2acic.cmo \ + doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ logicalOperations.cmo sequentPp.cmo mquery.cmo gTopLevel.cmo depend: diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index ad1d1f881..e6a03a645 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -116,7 +116,6 @@ let print_term curi ids_to_inner_sorts = let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort] - | C.AAbst (id,uri) -> raise NotImplemented | C.AMutInd (id,uri,_,i) -> X.xml_empty "MUTIND" ["uri", (U.string_of_uri uri) ; @@ -236,13 +235,18 @@ let print_object curi ids_to_inner_sorts = ;; let print_inner_types curi ids_to_inner_sorts ids_to_inner_types = + let module C2A = Cic2acic in let module X = Xml in X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi] (Hashtbl.fold - (fun id ty x -> + (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x -> [< x ; X.xml_nempty "TYPE" ["of",id] - (print_term curi ids_to_inner_sorts ty) + [< print_term curi ids_to_inner_sorts synty ; + match expty with + None -> [<>] + | Some expty' -> print_term curi ids_to_inner_sorts expty' + >] >] ) ids_to_inner_types [<>] ) diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index 7b9511da1..81e944196 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -25,6 +25,10 @@ exception NotImplemented;; +type anntypes = + {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} +;; + let fresh_id seed ids_to_terms ids_to_father_ids = fun father t -> let res = "i" ^ string_of_int !seed in @@ -48,158 +52,168 @@ let rec get_nth l n = ;; let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts - ids_to_inner_types metasenv context t + ids_to_inner_types metasenv context t expectedty = + let module D = DoubleTypeInference in let module T = CicTypeChecker in let module C = Cic in let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in - let terms_to_types = DoubleTypeInference.double_type_of metasenv context t in - let rec aux computeinnertypes father context tt = - let fresh_id'' = fresh_id' father tt in - (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) - let aux' = aux computeinnertypes (Some fresh_id'') in - (* First of all we compute the inner type and the inner sort *) - (* of the term. They may be useful in what follows. *) - (*CSC: This is a very inefficient way of computing inner types *) - (*CSC: and inner sorts: very deep terms have their types/sorts *) - (*CSC: computed again and again. *) - let string_of_sort = - function - C.Sort C.Prop -> "Prop" - | C.Sort C.Set -> "Set" - | C.Sort C.Type -> "Type" - | _ -> assert false - in - let ainnertype,innertype,innersort = + let terms_to_types = + D.double_type_of metasenv context t expectedty + in + let rec aux computeinnertypes father context tt = + let fresh_id'' = fresh_id' father tt in + (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *) + let aux' = aux computeinnertypes (Some fresh_id'') in + (* First of all we compute the inner type and the inner sort *) + (* of the term. They may be useful in what follows. *) + (*CSC: This is a very inefficient way of computing inner types *) + (*CSC: and inner sorts: very deep terms have their types/sorts *) + (*CSC: computed again and again. *) + let string_of_sort = + function + C.Sort C.Prop -> "Prop" + | C.Sort C.Set -> "Set" + | C.Sort C.Type -> "Type" + | _ -> assert false + in + let ainnertypes,innertype,innersort = (*CSC: Here we need the algorithm for Coscoy's double type-inference *) (*CSC: (expected type + inferred type). Just for now we use the usual *) (*CSC: type-inference, but the result is very poor. As a very weak *) (*CSC: patch, I apply whd to the computed type. Full beta *) (*CSC: reduction would be a much better option. *) - let innertype = + let {D.synthesized = synthesized; D.expected = expected} = if computeinnertypes then - let {DoubleTypeInference.synthesized = synthesized} = - DoubleTypeInference.CicHash.find terms_to_types tt - in - synthesized + D.CicHash.find terms_to_types tt else (* We are already in an inner-type and Coscoy's double *) (* type inference algorithm has not been applied. *) - CicReduction.whd context (T.type_of_aux' metasenv context tt) + {D.synthesized = + CicReduction.whd context (T.type_of_aux' metasenv context tt) ; + D.expected = None} in - let innersort = T.type_of_aux' metasenv context innertype in - let ainnertype = + let innersort = T.type_of_aux' metasenv context synthesized in + let ainnertypes = if computeinnertypes then - Some (aux false (Some fresh_id'') context innertype) + Some + {annsynthesized = + aux false (Some fresh_id'') context synthesized ; + annexpected = + match expected with + None -> None + | Some expectedty' -> + Some (aux false (Some fresh_id'') context expectedty') + } else None in - ainnertype, innertype, string_of_sort innersort - in - let add_inner_type id = - match ainnertype with - None -> () - | Some ainnertype -> Hashtbl.add ids_to_inner_types id ainnertype - in - match tt with - C.Rel n -> - let id = - match get_nth context n with - (Some (C.Name s,_)) -> s - | _ -> raise NameExpected - in + ainnertypes, synthesized, string_of_sort innersort + in + let add_inner_type id = + match ainnertypes with + None -> () + | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes + in + match tt with + C.Rel n -> + let id = + match get_nth context n with + (Some (C.Name s,_)) -> s + | _ -> raise NameExpected + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.ARel (fresh_id'', n, id) + | C.Var uri -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.AVar (fresh_id'', uri) + | C.Meta (n,l) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.AMeta (fresh_id'', n, + (List.map + (function None -> None | Some t -> Some (aux' context t)) l)) + | C.Sort s -> C.ASort (fresh_id'', s) + | C.Implicit -> C.AImplicit (fresh_id'') + | C.Cast (v,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.ACast (fresh_id'', aux' context v, aux' context t) + | C.Prod (n,s,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' + (string_of_sort innertype) ; + C.AProd + (fresh_id'', n, aux' context s, + aux' ((Some (n, C.Decl s))::context) t) + | C.Lambda (n,s,t) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + begin + let father_is_lambda = + match father with + None -> false + | Some father' -> + match Hashtbl.find ids_to_terms father' with + C.Lambda _ -> true + | _ -> false + in + if not father_is_lambda then + add_inner_type fresh_id'' + end ; + C.ALambda + (fresh_id'',n, aux' context s, + aux' ((Some (n, C.Decl s)::context)) t) + | C.LetIn (n,s,t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.ARel (fresh_id'', n, id) - | C.Var uri -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.AVar (fresh_id'', uri) - | C.Meta (n,l) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.AMeta (fresh_id'', n, - (List.map - (function None -> None | Some t -> Some (aux' context t)) l)) - | C.Sort s -> C.ASort (fresh_id'', s) - | C.Implicit -> C.AImplicit (fresh_id'') - | C.Cast (v,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.ACast (fresh_id'', aux' context v, aux' context t) - | C.Prod (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' - (string_of_sort innertype) ; - C.AProd + C.ALetIn (fresh_id'', n, aux' context s, - aux' ((Some (n, C.Decl s))::context) t) - | C.Lambda (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - begin - let father_is_lambda = - match father with - None -> false - | Some father' -> - match Hashtbl.find ids_to_terms father' with - C.Lambda _ -> true - | _ -> false + aux' ((Some (n, C.Def s))::context) t) + | C.Appl l -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.AAppl (fresh_id'', List.map (aux' context) l) + | C.Const (uri,cn) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.AConst (fresh_id'', uri, cn) + | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno) + | C.MutConstruct (uri,cn,tyno,consno) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + C.AMutConstruct (fresh_id'', uri, cn, tyno, consno) + | C.MutCase (uri, cn, tyno, outty, term, patterns) -> + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.AMutCase (fresh_id'', uri, cn, tyno, aux' context outty, + aux' context term, List.map (aux' context) patterns) + | C.Fix (funno, funs) -> + let tys = + List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs in - if not father_is_lambda then - add_inner_type fresh_id'' - end ; - C.ALambda - (fresh_id'',n, aux' context s, - aux' ((Some (n, C.Decl s)::context)) t) - | C.LetIn (n,s,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.ALetIn - (fresh_id'', n, aux' context s, - aux' ((Some (n, C.Def s))::context) t) - | C.Appl l -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.AAppl (fresh_id'', List.map (aux' context) l) - | C.Const (uri,cn) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.AConst (fresh_id'', uri, cn) - | C.Abst _ -> raise NotImplemented - | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno) - | C.MutConstruct (uri,cn,tyno,consno) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - C.AMutConstruct (fresh_id'', uri, cn, tyno, consno) - | C.MutCase (uri, cn, tyno, outty, term, patterns) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.AMutCase (fresh_id'', uri, cn, tyno, aux' context outty, - aux' context term, List.map (aux' context) patterns) - | C.Fix (funno, funs) -> - let tys = - List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.AFix (fresh_id'', funno, - List.map - (fun (name, indidx, ty, bo) -> - (name, indidx, aux' context ty, aux' (tys@context) bo) - ) funs - ) - | C.CoFix (funno, funs) -> - let tys = - List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if innersort = "Prop" then - add_inner_type fresh_id'' ; - C.ACoFix (fresh_id'', funno, - List.map - (fun (name, ty, bo) -> - (name, aux' context ty, aux' (tys@context) bo) - ) funs - ) - in - aux true None context t + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.AFix (fresh_id'', funno, + List.map + (fun (name, indidx, ty, bo) -> + (name, indidx, aux' context ty, aux' (tys@context) bo) + ) funs + ) + | C.CoFix (funno, funs) -> + let tys = + List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs + in + Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; + if innersort = "Prop" then + add_inner_type fresh_id'' ; + C.ACoFix (fresh_id'', funno, + List.map + (fun (name, ty, bo) -> + (name, aux' context ty, aux' (tys@context) bo) + ) funs + ) + in + aux true None context t ;; let acic_of_cic_context metasenv context t = @@ -231,9 +245,8 @@ let acic_object_of_cic_object obj = let aobj = match obj with C.Definition (id,bo,ty,params) -> - let abo = acic_term_of_cic_term' bo in - let aty = acic_term_of_cic_term' ty - in + let abo = acic_term_of_cic_term' bo (Some ty) in + let aty = acic_term_of_cic_term' ty None in C.ADefinition ("mettereaposto",id,abo,aty,(Cic.Actual params)) | C.Axiom (id,ty,params) -> raise NotImplemented | C.Variable (id,bo,ty) -> raise NotImplemented @@ -255,12 +268,12 @@ let acic_object_of_cic_object obj = match hyp with (Some (n,C.Decl t)) -> let at = - acic_term_of_cic_term_context' conjectures tl t + acic_term_of_cic_term_context' conjectures tl t None in (hid,Some (n,C.ADecl at))::(aux tl) | (Some (n,C.Def t)) -> let at = - acic_term_of_cic_term_context' conjectures tl t + acic_term_of_cic_term_context' conjectures tl t None in (hid,Some (n,C.ADef at))::(aux tl) | None -> (hid,None)::(aux tl) @@ -268,12 +281,13 @@ let acic_object_of_cic_object obj = aux canonical_context in let aterm = - acic_term_of_cic_term_context' conjectures canonical_context term + acic_term_of_cic_term_context' conjectures canonical_context + term None in (cid,i,acanonical_context,aterm) ) conjectures in - let abo = acic_term_of_cic_term_context' conjectures [] bo in - let aty = acic_term_of_cic_term_context' conjectures [] ty in + 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 C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty) | C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented in diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli index a2c0497f1..a07b9d297 100644 --- a/helm/gTopLevel/cic2acic.mli +++ b/helm/gTopLevel/cic2acic.mli @@ -27,15 +27,20 @@ exception NotImplemented exception NotEnoughElements exception NameExpected +type anntypes = + {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option} +;; + val acic_of_cic_context' : int ref -> (* seed *) (Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *) (Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *) (Cic.id, string) Hashtbl.t -> (* ids_to_inner_sorts *) - (Cic.id, Cic.annterm) Hashtbl.t -> (* ids_to_inner_types *) + (Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *) Cic.metasenv -> (* metasenv *) Cic.context -> (* context *) Cic.term -> (* term *) + Cic.term option -> (* expected type *) Cic.annterm (* annotated term *) val acic_object_of_cic_object : @@ -44,6 +49,6 @@ val acic_object_of_cic_object : (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *) (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *) (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *) - (Cic.id, Cic.annterm) Hashtbl.t * (* ids_to_inner_types *) + (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *) (Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *) (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *) diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml index 50a81c56a..b9a79b64f 100644 --- a/helm/gTopLevel/doubleTypeInference.ml +++ b/helm/gTopLevel/doubleTypeInference.ml @@ -31,7 +31,125 @@ exception WrongUriToMutualInductiveDefinitions of string;; exception ListTooShort;; exception RelToHiddenHypothesis;; -type types = {synthesized : Cic.term ; expected : Cic.term};; +type types = {synthesized : Cic.term ; expected : Cic.term option};; + +(*CSC: potrebbe creare applicazioni di applicazioni *) +(*CSC: ora non e' piu' head, ma completa!!! *) +let rec head_beta_reduce = + let module S = CicSubstitution in + let module C = Cic in + function + C.Rel _ + | C.Var _ as t -> t + | C.Meta (n,l) -> + C.Meta (n, + List.map + (function None -> None | Some t -> Some (head_beta_reduce t)) l + ) + | C.Sort _ as t -> t + | C.Implicit -> assert false + | C.Cast (te,ty) -> + C.Cast (head_beta_reduce te, head_beta_reduce ty) + | C.Prod (n,s,t) -> + C.Prod (n, head_beta_reduce s, head_beta_reduce t) + | C.Lambda (n,s,t) -> + C.Lambda (n, head_beta_reduce s, head_beta_reduce t) + | C.LetIn (n,s,t) -> + C.LetIn (n, head_beta_reduce s, head_beta_reduce t) + | C.Appl ((C.Lambda (name,s,t))::he::tl) -> + let he' = S.subst he t in + if tl = [] then + head_beta_reduce he' + else + head_beta_reduce (C.Appl (he'::tl)) + | C.Appl l -> + C.Appl (List.map head_beta_reduce l) + | C.Const _ as t -> t + | C.MutInd _ + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cno,i,outt,t,pl) -> + C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t, + List.map head_beta_reduce pl) + | C.Fix (i,fl) -> + let fl' = + List.map + (function (name,i,ty,bo) -> + name,i,head_beta_reduce ty,head_beta_reduce bo + ) fl + in + C.Fix (i,fl') + | C.CoFix (i,fl) -> + let fl' = + List.map + (function (name,ty,bo) -> + name,head_beta_reduce ty,head_beta_reduce bo + ) fl + in + C.CoFix (i,fl') +;; + +(* syntactic_equality up to cookingsno for uris *) +(* (which is often syntactically irrilevant), *) +(* distinction between fake dependent products *) +(* and non-dependent products, alfa-conversion *) +(*CSC: must alfa-conversion be considered or not? *) +let syntactic_equality t t' = + let module C = Cic in + let rec syntactic_equality t t' = + if t = t' then true + else + match t, t' with + C.Rel _, C.Rel _ + | C.Var _, C.Var _ + | C.Meta _, C.Meta _ + | C.Sort _, C.Sort _ + | C.Implicit, C.Implicit -> false (* we already know that t != t' *) + | C.Cast (te,ty), C.Cast (te',ty') -> + syntactic_equality te te' && + syntactic_equality ty ty' + | C.Prod (_,s,t), C.Prod (_,s',t') -> + syntactic_equality s s' && + syntactic_equality t t' + | C.Lambda (_,s,t), C.Lambda (_,s',t') -> + syntactic_equality s s' && + syntactic_equality t t' + | C.LetIn (_,s,t), C.LetIn(_,s',t') -> + syntactic_equality s s' && + syntactic_equality t t' + | C.Appl l, C.Appl l' -> + List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' + | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri' + | C.MutInd (uri,_,i), C.MutInd (uri',_,i') -> + UriManager.eq uri uri' && i = i' + | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') -> + UriManager.eq uri uri' && i = i' && j = j' + | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') -> + UriManager.eq sp sp' && i = i' && + syntactic_equality outt outt' && + syntactic_equality t t' && + List.fold_left2 + (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' + | C.Fix (i,fl), C.Fix (i',fl') -> + i = i' && + List.fold_left2 + (fun b (_,i,ty,bo) (_,i',ty',bo') -> + b && i = i' && + syntactic_equality ty ty' && + syntactic_equality bo bo') true fl fl' + | C.CoFix (i,fl), C.CoFix (i',fl') -> + i = i' && + List.fold_left2 + (fun b (_,ty,bo) (_,ty',bo') -> + b && + syntactic_equality ty ty' && + syntactic_equality bo bo') true fl fl' + | _,_ -> false + in + try + syntactic_equality t t' + with + _ -> false +;; let rec split l n = match (l,n) with @@ -114,12 +232,12 @@ module CicHash = ;; (* type_of_aux' is just another name (with a different scope) for type_of_aux *) -let rec type_of_aux' subterms_to_types metasenv context t = +let rec type_of_aux' subterms_to_types metasenv context t expectedty = (* Coscoy's double type-inference algorithm *) (* It computes the inner-types of every subterm of [t], *) (* even when they are not needed to compute the types *) (* of other terms. *) - let rec type_of_aux context t = + let rec type_of_aux context t expectedty = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in @@ -130,7 +248,7 @@ let rec type_of_aux' subterms_to_types metasenv context t = (try match List.nth context (n - 1) with Some (_,C.Decl t) -> S.lift n t - | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) + | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty | None -> raise RelToHiddenHypothesis with _ -> raise (NotWellTyped "Not a close term") @@ -140,7 +258,10 @@ let rec type_of_aux' subterms_to_types metasenv context t = (* Let's visit all the subterms that will not be visited later *) let _ = List.iter - (function None -> () | Some t -> ignore (type_of_aux context t)) l + (function + None -> () + | Some t -> ignore (type_of_aux context t None) + ) l in let (_,canonical_context,ty) = List.find (function (m,_,_) -> n = m) metasenv @@ -151,92 +272,144 @@ let rec type_of_aux' subterms_to_types metasenv context t = | C.Implicit -> raise (Impossible 21) | C.Cast (te,ty) -> (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context te in - let _ = type_of_aux context ty in + let _ = type_of_aux context te (Some (head_beta_reduce ty)) in + let _ = type_of_aux context ty None in (* Checks suppressed *) ty | C.Prod (name,s,t) -> - let sort1 = type_of_aux context s - and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in + let sort1 = type_of_aux context s None + and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in sort_of_prod context (name,s) (sort1,sort2) | C.Lambda (n,s,t) -> (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context s in - let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in - (* Checks suppressed *) - C.Prod (n,s,type2) + let _ = type_of_aux context s None in + let expected_target_type = + match expectedty with + None -> None + | Some expectedty' -> + let ty = + match R.whd context expectedty' with + C.Prod (_,_,expected_target_type) -> + head_beta_reduce expected_target_type + | _ -> assert false + in + Some ty + in + let type2 = + type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type + in + (* Checks suppressed *) + C.Prod (n,s,type2) | C.LetIn (n,s,t) -> +(*CSC: What are the right expected types for the source and *) +(*CSC: target of a LetIn? None used. *) (* Let's visit all the subterms that will not be visited later *) - let _ = type_of_aux context s in + let _ = type_of_aux context s None in (* Checks suppressed *) - C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t) + C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None) | C.Appl (he::tl) when List.length tl > 0 -> - let hetype = type_of_aux context he - and tlbody_and_type = - List.map (fun x -> (x, type_of_aux context x)) tl + let hetype = type_of_aux context he None in + let tlbody_and_type = + let rec aux = + function + _,[] -> [] + | C.Prod (n,s,t),he::tl -> + (he, type_of_aux context he (Some (head_beta_reduce s))):: + (aux (R.whd context (S.subst he t), tl)) + | _ -> assert false + in + aux (R.whd context hetype, tl) in eat_prods context hetype tlbody_and_type | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") | C.Const (uri,cookingsno) -> cooked_type_of_constant uri cookingsno - | C.Abst _ -> raise (Impossible 22) | C.MutInd (uri,cookingsno,i) -> cooked_type_of_mutual_inductive_defs uri cookingsno i | C.MutConstruct (uri,cookingsno,i,j) -> let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in cty | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> - (* Let's visit all the subterms that will not be visited later *) - let _ = List.map (type_of_aux context) pl in - let outsort = type_of_aux context outtype in - let (need_dummy, k) = - let rec guess_args context t = - match CicReduction.whd context t with - C.Sort _ -> (true, 0) - | C.Prod (name, s, t) -> - let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in - if n = 0 then - (* last prod before sort *) - match CicReduction.whd context s with - (*CSC vedi nota delirante su cookingsno in cicReduction.ml *) - C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> - (false, 1) - | C.Appl ((C.MutInd (uri',_,i')) :: _) - when U.eq uri' uri && i' = i -> (false, 1) - | _ -> (true, 1) - else - (b, n + 1) - | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") - in - (*CSC whd non serve dopo type_of_aux ? *) - let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) + let outsort = type_of_aux context outtype None in + let (need_dummy, k) = + let rec guess_args context t = + match CicReduction.whd context t with + C.Sort _ -> (true, 0) + | C.Prod (name, s, t) -> + let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in + if n = 0 then + (* last prod before sort *) + match CicReduction.whd context s with + (*CSC vedi nota delirante su cookingsno in cicReduction.ml *) + C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> + (false, 1) + | C.Appl ((C.MutInd (uri',_,i')) :: _) + when U.eq uri' uri && i' = i -> (false, 1) + | _ -> (true, 1) + else + (b, n + 1) + | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") in - let (_, arguments) = - match R.whd context (type_of_aux context term) with - (*CSC manca il caso dei CAST *) - C.MutInd (uri',_,i') -> - (* Checks suppressed *) - [],[] - | C.Appl (C.MutInd (uri',_,i') :: tl) -> - split tl (List.length tl - k) - | _ -> - raise (NotWellTyped "MutCase: the term is not an inductive one") + let (b, k) = guess_args context outsort in + if not b then (b, k - 1) else (b, k) + in + let (parameters, arguments) = + let type_of_term = + CicTypeChecker.type_of_aux' metasenv context term in - (* Checks suppressed *) - if not need_dummy then - C.Appl ((outtype::arguments)@[term]) - else if arguments = [] then - outtype - else - C.Appl (outtype::arguments) + match + R.whd context (type_of_aux context term + (Some (head_beta_reduce type_of_term))) + with + (*CSC manca il caso dei CAST *) + C.MutInd (uri',_,i') -> + (* Checks suppressed *) + [],[] + | C.Appl (C.MutInd (uri',_,i') :: tl) -> + split tl (List.length tl - k) + | _ -> + raise (NotWellTyped "MutCase: the term is not an inductive one") + in + (* Checks suppressed *) + (* Let's visit all the subterms that will not be visited later *) + let (cl,parsno) = + match CicEnvironment.get_cooked_obj uri cookingsno with + C.InductiveDefinition (tl,_,parsno) -> + let (_,_,_,cl) = List.nth tl i in (cl,parsno) + | _ -> + raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + in + let _ = + List.fold_left + (fun j (p,(_,c,_)) -> + let cons = + if parameters = [] then + (C.MutConstruct (uri,cookingsno,i,j)) + else + (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters)) + in + let expectedtype = + type_of_branch context parsno need_dummy outtype cons + (CicTypeChecker.type_of_aux' metasenv context cons) + in + ignore (type_of_aux context p + (Some (head_beta_reduce expectedtype))) ; + j+1 + ) 1 (List.combine pl cl) + in + if not need_dummy then + C.Appl ((outtype::arguments)@[term]) + else if arguments = [] then + outtype + else + C.Appl (outtype::arguments) | C.Fix (i,fl) -> (* Let's visit all the subterms that will not be visited later *) let context' = List.rev (List.map (fun (n,_,ty,_) -> - let _ = type_of_aux context ty in + let _ = type_of_aux context ty None in (Some (C.Name n,(C.Decl ty))) ) fl ) @ @@ -244,7 +417,12 @@ let rec type_of_aux' subterms_to_types metasenv context t = in let _ = List.iter - (fun (_,_,_,bo) -> ignore (type_of_aux context' bo)) + (fun (_,_,ty,bo) -> + let expectedty = + head_beta_reduce (CicSubstitution.lift (List.length fl) ty) + in + ignore (type_of_aux context' bo (Some expectedty)) + ) fl in (* Checks suppressed *) let (_,_,ty,_) = List.nth fl i in @@ -255,7 +433,7 @@ let rec type_of_aux' subterms_to_types metasenv context t = List.rev (List.map (fun (n,ty,_) -> - let _ = type_of_aux context ty in + let _ = type_of_aux context ty None in (Some (C.Name n,(C.Decl ty))) ) fl ) @ @@ -263,20 +441,35 @@ let rec type_of_aux' subterms_to_types metasenv context t = in let _ = List.iter - (fun (_,_,bo) -> ignore (type_of_aux context' bo)) + (fun (_,ty,bo) -> + let expectedty = + head_beta_reduce (CicSubstitution.lift (List.length fl) ty) + in + ignore (type_of_aux context' bo (Some expectedty)) + ) fl in (* Checks suppressed *) let (_,ty,_) = List.nth fl i in ty in - (*CSC: Is whd the right thing to do? Or should full beta *) - (*CSC: reduction be more appropriate? *) -(*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *) -(*CSC: costosa quando fatta ogni passo. Fare solo un passo? *) - let synthesized' = CicReduction.whd context synthesized in - CicHash.add subterms_to_types t - {synthesized = synthesized' ; expected = Cic.Implicit} ; - synthesized' + let synthesized' = head_beta_reduce synthesized in + let types,res = + match expectedty with + None -> + (* No expected type *) + {synthesized = synthesized' ; expected = None}, synthesized + | Some ty when syntactic_equality synthesized' ty -> + (* The expected type is synthactically equal to *) + (* the synthesized type. Let's forget it. *) + {synthesized = synthesized' ; expected = None}, synthesized + | Some expectedty' -> +prerr_endline ("t: " ^ CicPp.ppterm t) ; flush stderr ; +prerr_endline (CicPp.ppterm synthesized' ^ " <-> " ^ CicPp.ppterm expectedty') ; flush stderr ; + {synthesized = synthesized' ; expected = Some expectedty'}, + expectedty' + in + CicHash.add subterms_to_types t types ; + res and sort_of_prod context (name,s) (t1, t2) = let module C = Cic in @@ -305,12 +498,39 @@ let rec type_of_aux' subterms_to_types metasenv context t = | _ -> raise (NotWellTyped "Appl: wrong Prod-type") ) +and type_of_branch context argsno need_dummy outtype term constype = + let module C = Cic in + let module R = CicReduction in + match R.whd context constype with + C.MutInd (_,_,_) -> + if need_dummy then + outtype + else + C.Appl [outtype ; term] + | C.Appl (C.MutInd (_,_,_)::tl) -> + let (_,arguments) = split tl argsno + in + if need_dummy && arguments = [] then + outtype + else + C.Appl (outtype::arguments@(if need_dummy then [] else [term])) + | C.Prod (name,so,de) -> + let term' = + match CicSubstitution.lift 1 term with + C.Appl l -> C.Appl (l@[C.Rel 1]) + | t -> C.Appl [t ; C.Rel 1] + in + C.Prod (C.Anonimous,so,type_of_branch + ((Some (name,(C.Decl so)))::context) argsno need_dummy + (CicSubstitution.lift 1 outtype) term' de) + | _ -> raise (Impossible 20) + in - type_of_aux context t + type_of_aux context t expectedty ;; -let double_type_of metasenv context t = +let double_type_of metasenv context t expectedty = let subterms_to_types = CicHash.create 503 in - ignore (type_of_aux' subterms_to_types metasenv context t) ; + ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ; subterms_to_types ;; diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/gTopLevel/doubleTypeInference.mli index 4de5bc00c..aa151988b 100644 --- a/helm/gTopLevel/doubleTypeInference.mli +++ b/helm/gTopLevel/doubleTypeInference.mli @@ -6,14 +6,14 @@ exception WrongUriToMutualInductiveDefinitions of string exception ListTooShort exception RelToHiddenHypothesis -type types = {synthesized : Cic.term ; expected : Cic.term};; +type types = {synthesized : Cic.term ; expected : Cic.term option};; module CicHash : sig - type key = Cic.term - and 'a t - val find : 'a t -> key -> 'a + type 'a t + val find : 'a t -> Cic.term -> 'a end +;; val double_type_of : - Cic.metasenv -> Cic.context -> Cic.term -> types CicHash.t + Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 26c0b2e65..4a8b0a382 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -744,6 +744,14 @@ let save rendering_window () = "/public/sacerdot/currentproof") ;; +(* Used to typecheck the loaded proofs *) +let typecheck_loaded_proof metasenv bo ty = + let module T = CicTypeChecker in + (*CSC: bisogna controllare anche il metasenv!!! *) + ignore (T.type_of_aux' metasenv [] ty) ; + ignore (T.type_of_aux' metasenv [] bo) +;; + let load rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in let output = (rendering_window#output : GMathView.math_view) in @@ -752,6 +760,7 @@ let load rendering_window () = let uri = UriManager.uri_of_string "cic:/dummy.con" in match CicParser.obj_of_xml "/public/sacerdot/currentproof" uri with Cic.CurrentProof (_,metasenv,bo,ty) -> + typecheck_loaded_proof metasenv bo ty ; ProofEngine.proof := Some (uri, metasenv, bo, ty) ; ProofEngine.goal := diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index a9274fba6..074e66c80 100644 --- a/helm/gTopLevel/logicalOperations.ml +++ b/helm/gTopLevel/logicalOperations.ml @@ -27,7 +27,6 @@ let get_context ids_to_terms ids_to_father_ids = | C.LetIn _ -> [] | C.Appl _ | C.Const _ -> [] - | C.Abst _ -> assert false | C.MutInd _ | C.MutConstruct _ | C.MutCase _ -> [] diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml index 0cf33c83c..2812bd64e 100644 --- a/helm/gTopLevel/mquery.ml +++ b/helm/gTopLevel/mquery.ml @@ -187,7 +187,6 @@ let rec inspect_term main l v = function | Meta (i, _) -> l | Sort s -> l | Implicit -> l - | Abst u -> l | Var u -> inspect_uri main l u None None v | Const (u, i) -> inspect_uri main l u None None v | MutInd (u, i, t) -> inspect_uri main l u (Some t) None v diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index f33c69e35..c605d41a9 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -133,7 +133,6 @@ let metas_in_term term = | C.LetIn (_,s,t) -> (aux s) @ (aux t) | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l | C.Const _ - | C.Abst _ | C.MutInd _ | C.MutConstruct _ -> [] | C.MutCase (sp,cookingsno,i,outt,t,pl) -> @@ -450,7 +449,6 @@ let eta_expand metasenv context t arg = | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t) | C.Appl l -> C.Appl (List.map (aux n) l) | C.Const _ as t -> t - | C.Abst _ -> assert false | C.MutInd _ | C.MutConstruct _ as t -> t | C.MutCase (sp,cookingsno,i,outt,t,pl) -> @@ -579,6 +577,7 @@ let elim_intros_simpl term = | _ ->raise NotTheRightEliminatorShape in find_head he,fargs + | C.Meta (emeta,_) -> emeta,[] (* *) | _ -> raise NotTheRightEliminatorShape in diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 460c8d726..941a701a9 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -75,7 +75,6 @@ let rec syntactic_equality t t' = | C.Appl l, C.Appl l' -> List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri' - | C.Abst _, C.Abst _ -> assert false | C.MutInd (uri,_,i), C.MutInd (uri',_,i') -> UriManager.eq uri uri' && i = i' | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') -> @@ -124,7 +123,6 @@ let replace ~equality ~what ~with_what ~where = (C.Appl l')::tl -> C.Appl (l'@tl) | l' -> C.Appl l') | C.Const _ as t -> t - | C.Abst _ as t -> t | C.MutInd _ as t -> t | C.MutConstruct _ as t -> t | C.MutCase (sp,cookingsno,i,outt,t,pl) -> @@ -203,7 +201,6 @@ let reduce context = | C.CurrentProof (_,_,body,_) -> reduceaux context l body | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) - | C.Abst _ as t -> t (*CSC l should be empty ????? *) | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l) | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l) | C.MutCase (mutind,cookingsno,i,outtype,term,pl) -> @@ -265,7 +262,7 @@ let reduce context = eat_first (num_to_eat,tl) in reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Abst _ | C.Cast _ | C.Implicit -> + | C.Cast _ | C.Implicit -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let outtype' = reduceaux context [] outtype in @@ -483,7 +480,6 @@ let simpl context = | C.CurrentProof (_,_,body,_) -> reduceaux context l body | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) - | C.Abst _ as t -> t (*CSC l should be empty ????? *) | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l) | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l) | C.MutCase (mutind,cookingsno,i,outtype,term,pl) -> @@ -543,7 +539,7 @@ let simpl context = eat_first (num_to_eat,tl) in reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Abst _ | C.Cast _ | C.Implicit -> + | C.Cast _ | C.Implicit -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let outtype' = reduceaux context [] outtype in diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index df504e75a..c3ab41f88 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -59,7 +59,7 @@ module XmlPp = match binding with (Some (n,(Cic.Def t as b)) as entry) | (Some (n,(Cic.Decl t as b)) as entry) -> - let acic = acic_of_cic_context context t in + let acic = acic_of_cic_context context t None in [< s ; X.xml_nempty (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def") @@ -74,7 +74,7 @@ module XmlPp = ) context ([<>],[]) ) in - let acic = acic_of_cic_context context goal in + let acic = acic_of_cic_context context goal None in X.xml_nempty "Sequent" ["no",string_of_int metano] [< final_s ; Xml.xml_nempty "Goal" [] -- 2.39.2