From 7df065750ec593fb409ae8627f81927397602b9b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:20:09 +0000 Subject: [PATCH] added attributes --- .../cic_annotations/cicAnnotation2Xml.ml | 8 ++-- helm/ocaml/cic_annotations/cicXPath.ml | 10 ++--- helm/ocaml/cic_omdoc/cic2acic.ml | 20 +++++----- helm/ocaml/cic_omdoc/cic2content.ml | 26 +++++------- helm/ocaml/cic_omdoc/content2cic.ml | 5 ++- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 40 +++++++++---------- helm/ocaml/cic_omdoc/eta_fixing.ml | 4 +- 7 files changed, 53 insertions(+), 60 deletions(-) diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml index 23c3a9b68..4c028208f 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -109,7 +109,7 @@ let pp_annotation obj i2a curi = [None, "of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] begin match obj with - C.AConstant (xid, xidobj, _, te, ty, _) -> + C.AConstant (xid, xidobj, _, te, ty, _, _) -> [< print_ann i2a xid ; (match xidobj,te with Some xidobj, Some te -> @@ -121,7 +121,7 @@ let pp_annotation obj i2a curi = ) ; print_term i2a ty >] - | C.AVariable (xid, _, bo, ty,_) -> + | C.AVariable (xid, _, bo, ty,_, _) -> [< print_ann i2a xid ; (match bo with None -> [<>] @@ -129,7 +129,7 @@ let pp_annotation obj i2a curi = ) ; print_term i2a ty >] - | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_) -> + | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_, _) -> [< print_ann i2a xid ; print_ann i2a xidobj ; List.fold_right @@ -151,7 +151,7 @@ let pp_annotation obj i2a curi = print_term i2a bo ; print_term i2a ty >] - | C.AInductiveDefinition (xid, tys, params, paramsno) -> + | C.AInductiveDefinition (xid, tys, params, paramsno, _) -> [< print_ann i2a xid ; List.fold_right (fun x i -> [< print_mutual_inductive_type i2a x ; i >]) diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml index 75a598d91..b9533d18f 100644 --- a/helm/ocaml/cic_annotations/cicXPath.ml +++ b/helm/ocaml/cic_annotations/cicXPath.ml @@ -100,7 +100,7 @@ let get_ids_to_targets annobj = in let add_target_obj annobj = match annobj with - C.AConstant (id,idbody,_,bo,ty,_) -> + C.AConstant (id,idbody,_,bo,ty,_,_) -> set_target id (C.Object annobj) ; (match idbody,bo with Some idbody,Some bo -> @@ -110,14 +110,14 @@ let get_ids_to_targets annobj = | _,_ -> assert false ) ; add_target_term ty - | C.AVariable (id,_,None,ty,_) -> + | C.AVariable (id,_,None,ty,_,_) -> set_target id (C.Object annobj) ; add_target_term ty - | C.AVariable (id,_,Some bo,ty,_) -> + | C.AVariable (id,_,Some bo,ty,_,_) -> set_target id (C.Object annobj) ; add_target_term bo ; add_target_term ty - | C.ACurrentProof (id,idbody,_,cl,bo,ty,_) -> + | C.ACurrentProof (id,idbody,_,cl,bo,ty,_,_) -> set_target id (C.Object annobj) ; set_target idbody (C.ConstantBody annobj) ; List.iter (function (cid,_,context, t) as annconj -> @@ -133,7 +133,7 @@ let get_ids_to_targets annobj = add_target_term t) cl ; add_target_term bo ; add_target_term ty - | C.AInductiveDefinition (id,itl,_,_) -> + | C.AInductiveDefinition (id,itl,_,_,_) -> set_target id (C.Object annobj) ; List.iter (function (_,_,_,arity,cl) -> diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 5b95ab4d6..cf9760c25 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -428,19 +428,19 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = in let aobj = match obj with - C.Constant (id,Some bo,ty,params) -> + 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 C.AConstant - ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params) - | C.Constant (id,None,ty,params) -> + ("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 C.AConstant - ("mettereaposto",None,id,None,aty,params) - | C.Variable (id,bo,ty,params) -> + ("mettereaposto",None,id,None,aty,params,attrs) + | C.Variable (id,bo,ty,params,attrs) -> let ty' = eta_fix [] [] ty in let abo = match bo with @@ -451,8 +451,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = in let aty = acic_term_of_cic_term' ty' None in C.AVariable - ("mettereaposto",id,abo,aty, params) - | C.CurrentProof (id,conjectures,bo,ty,params) -> + ("mettereaposto",id,abo,aty,params,attrs) + | C.CurrentProof (id,conjectures,bo,ty,params,attrs) -> let conjectures' = List.map (function (i,canonical_context,term) -> @@ -556,8 +556,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ; *) C.ACurrentProof - ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params) - | C.InductiveDefinition (tys,params,paramsno) -> + ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs) + | C.InductiveDefinition (tys,params,paramsno,attrs) -> let context = List.map (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in @@ -575,7 +575,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = (id,name,inductive,acic_term_of_cic_term' ty None,acons) ) (List.rev idrefs) tys in - C.AInductiveDefinition ("mettereaposto",atys,params,paramsno) + C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs) in aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types, ids_to_conjectures,ids_to_hypotheses diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index ef6999ca0..aaf451256 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -374,10 +374,8 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,_) -> l + | Cic.InductiveDefinition (l,_,_,_) -> l + | _ -> assert false ) in let (_,_,_,constructors) = List.nth inductive_types tyno in @@ -548,7 +546,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,n) -> l,n + | Cic.InductiveDefinition (l,_,n,_) -> l,n ) in let (_,_,_,constructors) = List.nth inductive_types typeno in let name_and_arities = @@ -694,10 +692,8 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = let inductive_types,noparams = (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in match o with - Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,n) -> (l,n) + | Cic.InductiveDefinition (l,_,n,_) -> (l,n) + | _ -> assert false ) in let rec split n l = if n = 0 then ([],l) else @@ -916,7 +912,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = let module C2A = Cic2acic in let seed = ref 0 in function - C.ACurrentProof (_,_,n,conjectures,bo,ty,params) -> + C.ACurrentProof (_,_,n,conjectures,bo,ty,params,_) -> (gen_id object_prefix seed, params, Some (List.map @@ -925,27 +921,27 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = `Def (K.Const,ty, build_def_item seed (get_id bo) (C.Name n) bo ~ids_to_inner_sorts ~ids_to_inner_types)) - | C.AConstant (_,_,n,Some bo,ty,params) -> + | C.AConstant (_,_,n,Some bo,ty,params,_) -> (gen_id object_prefix seed, params, None, `Def (K.Const,ty, build_def_item seed (get_id bo) (C.Name n) bo ~ids_to_inner_sorts ~ids_to_inner_types)) - | C.AConstant (id,_,n,None,ty,params) -> + | C.AConstant (id,_,n,None,ty,params,_) -> (gen_id object_prefix seed, params, None, `Decl (K.Const, build_decl_item seed id (C.Name n) ty ~ids_to_inner_sorts)) - | C.AVariable (_,n,Some bo,ty,params) -> + | C.AVariable (_,n,Some bo,ty,params,_) -> (gen_id object_prefix seed, params, None, `Def (K.Var,ty, build_def_item seed (get_id bo) (C.Name n) bo ~ids_to_inner_sorts ~ids_to_inner_types)) - | C.AVariable (id,n,None,ty,params) -> + | C.AVariable (id,n,None,ty,params,_) -> (gen_id object_prefix seed, params, None, `Decl (K.Var, build_decl_item seed id (C.Name n) ty ~ids_to_inner_sorts)) - | C.AInductiveDefinition (id,l,params,nparams) -> + | C.AInductiveDefinition (id,l,params,nparams,_) -> (gen_id object_prefix seed, params, None, `Joint { K.joint_id = gen_id joint_prefix seed; diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index bf80a5939..fdc2cea1c 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -227,7 +227,7 @@ let cobj2obj deannotate (id,params,metasenv,obj) = (match metasenv with None -> Cic.Constant - (id, Some (proof2cic deannotate bo), deannotate ty, params) + (id, Some (proof2cic deannotate bo), deannotate ty, params, []) | Some metasenv' -> let metasenv'' = List.map @@ -259,7 +259,8 @@ let cobj2obj deannotate (id,params,metasenv,obj) = ) metasenv' in Cic.CurrentProof - (id, metasenv'', proof2cic deannotate bo, deannotate ty, params)) + (id, metasenv'', proof2cic deannotate bo, deannotate ty, params, + [])) | _ -> raise ToDo ;; diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index e16aa789f..128da869b 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -272,8 +272,8 @@ let type_of_constant uri = raise (NotWellTyped "Reference to an unchecked constant") in match cobj with - C.Constant (_,_,ty,_) -> ty - | C.CurrentProof (_,_,_,ty,_) -> ty + C.Constant (_,_,ty,_,_) -> ty + | C.CurrentProof (_,_,_,ty,_,_) -> ty | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) ;; @@ -282,7 +282,7 @@ let type_of_variable uri = let module R = CicReduction in let module U = UriManager in match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with - CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),_) -> ty + CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty | CicEnvironment.UncheckedObj (C.Variable _) -> raise (NotWellTyped "Reference to an unchecked variable") | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) @@ -299,7 +299,7 @@ let type_of_mutual_inductive_defs uri i = raise (NotWellTyped "Reference to an unchecked inductive type") in match cobj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,arity,_) = List.nth dl i in arity | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) @@ -316,7 +316,7 @@ let type_of_mutual_inductive_constr uri i j = raise (NotWellTyped "Reference to an unchecked constructor") in match cobj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty @@ -543,7 +543,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = with Not_found -> assert false in match obj with - C.InductiveDefinition (tl,_,parsno) -> + C.InductiveDefinition (tl,_,parsno,_) -> let (_,_,_,cl) = List.nth tl i in (cl,parsno) | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) @@ -645,22 +645,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri with Not_found -> assert false in - match obj with - Cic.Constant (_,_,_,params) - | Cic.CurrentProof (_,_,_,_,params) - | Cic.Variable (_,_,_,params) - | Cic.InductiveDefinition (_,params,_) -> - List.map - (function uri -> - let obj,_ = - try - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri - with Not_found -> assert false - in - match obj with - Cic.Variable (_,None,ty,_) -> uri,ty - | _ -> assert false (* the theorem is well-typed *) - ) params + let params = CicUtil.params_of_obj obj in + List.map + (function uri -> + let obj,_ = + try + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + with Not_found -> assert false + in + match obj with + Cic.Variable (_,None,ty,_,_) -> uri,ty + | _ -> assert false (* the theorem is well-typed *) + ) params in let rec check uris_and_types subst = match uris_and_types,subst with diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index 41cc72738..68dec37d6 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -242,7 +242,7 @@ let eta_fix metasenv context t = Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,n) -> l,n + | Cic.InductiveDefinition (l,_,n,_) -> l,n ) in let (_,_,_,constructors) = List.nth inductive_types tyno in let constructor_types = @@ -299,7 +299,7 @@ let eta_fix metasenv context t = let ty = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - Cic.Variable (_,_,ty,_) -> + Cic.Variable (_,_,ty,_,_) -> CicSubstitution.subst_vars newsubst ty | _ -> raise ReferenceToNonVariable in -- 2.39.2