From: Claudio Sacerdoti Coen Date: Thu, 13 Mar 2008 18:48:26 +0000 (+0000) Subject: :-( X-Git-Tag: make_still_working~5531 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b699884bb9816aa55f9bd0a2d7bffde4dc03c643;p=helm.git :-( This commit introduces an hack in deannotate.ml to compute on-the-fly the types for the body in a LetIn parsed from an XML file. This happens when parsing Coq files. We should re-export everything from Coq sooner or later. --- diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml index 3d1d3d1aa..9fac7badb 100644 --- a/helm/software/components/cic/cicParser.ml +++ b/helm/software/components/cic/cicParser.ml @@ -406,8 +406,15 @@ let end_element ctxt tag = | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source) | _ -> attribute_error ()) | "def" -> (* same as "decl" above *) - let ty = pop_cic ctxt in - let source = pop_cic ctxt in + let ty,source = + (*CSC: hack to parse Coq files where the LetIn is not typed *) + let ty = pop_cic ctxt in + try + let source = pop_cic ctxt in + ty,source + with + Parser_failure _ -> Cic.AImplicit ("MISSING_def_TYPE",None),ty + in push ctxt (match pop_tag_attrs ctxt with | ["binder", binder; "id", id] diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml index f1dfbffed..69eccd9b9 100644 --- a/helm/software/components/cic/deannotate.ml +++ b/helm/software/components/cic/deannotate.ml @@ -106,7 +106,100 @@ let deannotate_conjectures = (id,context,deannotate_term con)) ;; +let type_of_aux' = ref (fun _ _ -> assert false);; +let lift = ref (fun _ _ -> assert false);; + +let rec compute_letin_type context te = + let module C = Cic in + match te with + C.Rel _ + | C.Sort _ -> te + | C.Implicit _ -> assert false + | C.Meta (n,l) -> + C.Meta (n, + List.map + (fun x -> + match x with + None -> None + | Some x -> Some (compute_letin_type context x)) l) + | C.Cast (te,ty) -> + C.Cast + (compute_letin_type context te, + compute_letin_type context ty) + | C.Prod (name,so,dest) -> + C.Prod (name, + compute_letin_type context so, + compute_letin_type ((Some (name,(C.Decl so)))::context) dest) + | C.Lambda (name,so,dest) -> + C.Lambda (name, + compute_letin_type context so, + compute_letin_type ((Some (name,(C.Decl so)))::context) dest) + | C.LetIn (name,so,C.Implicit _,dest) -> + let ty = !type_of_aux' context so in + C.LetIn (name, + compute_letin_type context so, + ty, + compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest) + | C.LetIn (name,so,ty,dest) -> + C.LetIn (name, + compute_letin_type context so, + compute_letin_type context ty, + compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest) + | C.Appl l -> + C.Appl (List.map (fun x -> compute_letin_type context x) l) + | C.Var (uri,exp_named_subst) -> + C.Var (uri, + List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst) + | C.Const (uri,exp_named_subst) -> + C.Const (uri, + List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst) + | C.MutInd (uri,i,exp_named_subst) -> + C.MutInd (uri,i, + List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst) + | C.MutConstruct (uri,i,j,exp_named_subst) -> + C.MutConstruct (uri,i,j, + List.map (fun (u,x) -> u,compute_letin_type context x) exp_named_subst) + | C.MutCase (uri,i,out,te,pl) -> + C.MutCase (uri,i, + compute_letin_type context out, + compute_letin_type context te, + List.map (fun x -> compute_letin_type context x) pl) + | C.Fix (fno,fl) -> + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (!lift len ty)))::types, + len+1) + ) ([],0) fl + in + C.Fix (fno, + List.map + (fun (name,recno,ty,bo) -> + name, recno, + compute_letin_type context ty, + compute_letin_type (tys @ context) bo + ) fl) + | C.CoFix (fno,fl) -> + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (!lift len ty)))::types, + len+1) + ) ([],0) fl + in + C.CoFix (fno, + List.map + (fun (name,ty,bo) -> + name, + compute_letin_type context ty, + compute_letin_type (tys @ context) bo + ) fl) +;; + let deannotate_obj = + let deannotate_term t = + compute_letin_type [] (deannotate_term t) + in let module C = Cic in function C.AConstant (_, _, id, bo, ty, params, attrs) -> diff --git a/helm/software/components/cic/deannotate.mli b/helm/software/components/cic/deannotate.mli index 1e29b5b64..f4fdd2d5d 100644 --- a/helm/software/components/cic/deannotate.mli +++ b/helm/software/components/cic/deannotate.mli @@ -32,6 +32,9 @@ (* *) (******************************************************************************) +val type_of_aux' : (Cic.context -> Cic.term -> Cic.term) ref +val lift : (int -> Cic.term -> Cic.term) ref + val deannotate_term : Cic.annterm -> Cic.term val deannotate_conjectures : Cic.annmetasenv -> Cic.metasenv val deannotate_obj : Cic.annobj -> Cic.obj diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml index 4f888a3a5..8d1dad9e2 100644 --- a/helm/software/components/cic_proof_checking/cicSubstitution.ml +++ b/helm/software/components/cic_proof_checking/cicSubstitution.ml @@ -440,3 +440,4 @@ let subst_meta l t = aux 0 t ;; +Deannotate.lift := lift;; diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index c23555494..7b98a59be 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -2303,3 +2303,6 @@ let check_allowed_sort_elimination uri i s1 s2 = ~logger:(new CicLogger.logger) [] uri i true (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2) CicUniv.empty_ugraph) +;; + +Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;