From e8236af508187f6446f5af481d545d433628ee00 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:26:13 +0000 Subject: [PATCH] attributes support --- .../cic_proof_checking/cicReductionMachine.ml | 24 ++++---- .../cic_proof_checking/cicReductionNaif.ml | 12 ++-- .../cic_proof_checking/cicSubstitution.ml | 10 ++-- .../cic_proof_checking/cicTypeChecker.ml | 58 +++++++++---------- helm/ocaml/cic_proof_checking/cicUnivUtils.ml | 16 ++--- helm/ocaml/cic_unification/cicRefine.ml | 12 ++-- helm/ocaml/cic_unification/coercGraph.ml | 14 +++-- 7 files changed, 74 insertions(+), 72 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index e456a1731..0610504c4 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -38,7 +38,7 @@ let debug t env s = let rec debug_aux t i = let module C = Cic in let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i + CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i in if !fdebug = 0 then prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") @@ -358,7 +358,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - in (match o with C.Constant _ -> raise ReferenceToConstant - | C.Variable (_,_,_,params) -> params + | C.Variable (_,_,_,params,_) -> params | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) @@ -389,9 +389,9 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in (match o with - C.Constant (_,_,_,params) -> params + C.Constant (_,_,_,params,_) -> params | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,_,_,params) -> params + | C.CurrentProof (_,_,_,_,params,_) -> params | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) in @@ -408,7 +408,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition (_,params,_) -> params + | C.InductiveDefinition (_,params,_,_) -> params ) in let exp_named_subst' = @@ -424,7 +424,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition (_,params,_) -> params + | C.InductiveDefinition (_,params,_,_) -> params ) in let exp_named_subst' = @@ -549,11 +549,11 @@ if List.mem uri params then prerr_endline "---- OK2" ; C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> + | C.Variable (_,None,_,_,_) -> let t' = unwind k e ens t in if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) - | C.Variable (_,Some body,_,_) -> + | C.Variable (_,Some body,_,_,_) -> let ens' = push_exp_named_subst k e ens exp_named_subst in reduce (0, [], ens', body, s) ) @@ -604,15 +604,15 @@ if List.mem uri params then prerr_endline "---- OK2" ; CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in match o with - C.Constant (_,Some body,_,_) -> + C.Constant (_,Some body,_,_,_) -> let ens' = push_exp_named_subst k e ens exp_named_subst in (* constants are closed *) reduce (0, [], ens', body, s) - | C.Constant (_,None,_,_) -> + | C.Constant (_,None,_,_,_) -> let t' = unwind k e ens t in if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> + | C.CurrentProof (_,_,body,_,_,_) -> let ens' = push_exp_named_subst k e ens exp_named_subst in (* constants are closed *) reduce (0, [], ens', body, s) @@ -662,7 +662,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind in match o with - C.InductiveDefinition (tl,ingredients,r) -> + C.InductiveDefinition (tl,ingredients,r,_) -> let (_,_,arity,_) = List.nth tl i in (arity,r) | _ -> raise WrongUriToInductiveDefinition diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index 4df3a5bd4..04067ccbf 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -31,7 +31,7 @@ let debug t env s = let rec debug_aux t i = let module C = Cic in let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i + CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i in if !fdebug = 0 then prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") @@ -64,8 +64,8 @@ let whd context = C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> if l = [] then t else C.Appl (t::l) - | C.Variable (_,Some body,_,_) -> + | C.Variable (_,None,_,_,_) -> if l = [] then t else C.Appl (t::l) + | C.Variable (_,Some body,_,_,_) -> whdaux l (CicSubstitution.subst_vars exp_named_subst body) ) | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) @@ -87,11 +87,11 @@ let whd context = CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri in (match o with - C.Constant (_,Some body,_,_) -> + C.Constant (_,Some body,_,_,_) -> whdaux l (CicSubstitution.subst_vars exp_named_subst body) | C.Constant _ -> if l = [] then t else C.Appl (t::l) | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> + | C.CurrentProof (_,_,body,_,_,_) -> whdaux l (CicSubstitution.subst_vars exp_named_subst body) | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) @@ -128,7 +128,7 @@ let whd context = let (arity, r) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in match o with - C.InductiveDefinition (tl,ingredients,r) -> + C.InductiveDefinition (tl,ingredients,r,_) -> let (_,_,arity,_) = List.nth tl i in (arity,r) | _ -> raise WrongUriToInductiveDefinition diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index a7124d4a3..431fa4b50 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -208,7 +208,7 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ; let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match obj with C.Constant _ -> raise ReferenceToConstant - | C.Variable (_,_,_,params) -> params + | C.Variable (_,_,_,params,_) -> params | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) @@ -256,9 +256,9 @@ prerr_endline "---- END\n\n " ; let params = let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in (match obj with - C.Constant (_,_,_,params) -> params + C.Constant (_,_,_,params,_) -> params | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,_,_,params) -> params + | C.CurrentProof (_,_,_,_,params,_) -> params | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) in @@ -273,7 +273,7 @@ prerr_endline "---- END\n\n " ; C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition (_,params,_) -> params + | C.InductiveDefinition (_,params,_,_) -> params ) in let exp_named_subst'' = @@ -287,7 +287,7 @@ prerr_endline "---- END\n\n " ; C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition (_,params,_) -> params + | C.InductiveDefinition (_,params,_,_) -> params ) in let exp_named_subst'' = diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index cab4640c8..2a7f8c4ae 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -36,7 +36,7 @@ let debug t context = let rec debug_aux t i = let module C = Cic in let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i + CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i in if !fdebug = 0 then raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) "")) @@ -136,7 +136,7 @@ let rec type_of_constant ~logger uri ugraph = let ugraph_dust = (match uobj with - C.Constant (_,Some te,ty,_) -> + C.Constant (_,Some te,ty,_,_) -> let _,ugraph = type_of ~logger ty ugraph in let type_of_te,ugraph' = type_of ~logger te ugraph in let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in @@ -147,11 +147,11 @@ let rec type_of_constant ~logger uri ugraph = (CicPp.ppterm ty))) else ugraph' - | C.Constant (_,None,ty,_) -> + | C.Constant (_,None,ty,_,_) -> (* only to check that ty is well-typed *) let _,ugraph' = type_of ~logger ty ugraph in ugraph' - | C.CurrentProof (_,conjs,te,ty,_) -> + | C.CurrentProof (_,conjs,te,ty,_,_) -> let _,ugraph1 = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> @@ -188,8 +188,8 @@ let rec type_of_constant ~logger uri ugraph = uobj,ugraph_dust in match cobj,ugraph with - (C.Constant (_,_,ty,_)),g -> ty,g - | (C.CurrentProof (_,_,_,ty,_)),g -> ty,g + (C.Constant (_,_,ty,_,_)),g -> ty,g + | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g | _ -> raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri)) @@ -199,8 +199,8 @@ and type_of_variable ~logger uri ugraph = let module U = UriManager in (* 0 because a variable is never cooked => no partial cooking at one level *) match CicEnvironment.is_type_checked ~trust:true ugraph uri with - CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> ty,ugraph' - | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) -> + CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph' + | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) -> logger#log (`Start_type_checking uri) ; (* only to check that ty is well-typed *) let _,ugraph1 = type_of ~logger ty ugraph in @@ -220,7 +220,7 @@ and type_of_variable ~logger uri ugraph = CicEnvironment.set_type_checking_info uri ; logger#log (`Type_checking_completed uri) ; match CicEnvironment.is_type_checked ~trust:false ugraph uri with - CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> + CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph' | CicEnvironment.CheckedObj _ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError @@ -406,7 +406,7 @@ and strictly_positive context n nn te = let (ok,paramsno,ity,cl,name) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let (name,_,ity,cl) = List.nth tl i in (List.length tl = 1, paramsno, ity, cl, name) | _ -> @@ -545,7 +545,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (* inductive block definition. *) and check_mutual_inductive_defs uri obj ugraph = match obj with - Cic.InductiveDefinition (itl, params, indparamsno) -> + Cic.InductiveDefinition (itl, params, indparamsno, _) -> typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph | _ -> raise (TypeCheckerFailure ( @@ -578,7 +578,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph = uobj,ugraph1_dust in match cobj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,arity,_) = List.nth dl i in arity,ugraph1 | _ -> @@ -613,7 +613,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph = uobj,ugraph1_dust 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,ugraph1 @@ -742,7 +742,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl @@ -781,7 +781,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let (_,isinductive,_,cl) = List.nth tl i in let tys = List.map (fun (n,_,ty,_) -> @@ -908,7 +908,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let len = List.length tl in let (_,isinductive,_,cl) = List.nth tl i in let tys = @@ -953,7 +953,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let (_,isinductive,_,cl) = List.nth tl i in let tys = List.map @@ -1068,7 +1068,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = with Not_found -> assert false in match obj with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,_,_,cl) = List.nth itl i in let (_,cons) = List.nth cl (j - 1) in CicSubstitution.subst_vars exp_named_subst cons @@ -1253,7 +1253,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *) (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,_,_,cl) = List.nth itl i in (* is a singleton definition or the empty proposition? *) (List.length cl = 1 || List.length cl = 0) , ugraph @@ -1273,7 +1273,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,paramsno) -> + C.InductiveDefinition (itl,_,paramsno,_) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in @@ -1301,7 +1301,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind | (C.Sort C.Set | C.Sort C.CProp) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,_,_,cl) = List.nth itl i in (* is a singleton definition? *) List.length cl = 1,ugraph1 @@ -1327,7 +1327,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind (* TASSI: da verificare *) (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,paramsno) -> + C.InductiveDefinition (itl,_,paramsno,_) -> let (_,_,_,cl) = List.nth itl i in let tys = List.map @@ -1727,7 +1727,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = with Not_found -> assert false in match obj with - C.InductiveDefinition (_,_,parsno) -> parsno + C.InductiveDefinition (_,_,parsno,_) -> parsno | _ -> raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ @@ -1966,7 +1966,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = with Not_found -> assert false in (match obj with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) | _ -> @@ -1977,7 +1977,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.Appl ((C.MutInd (uri,i,_))::_) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) | _ -> @@ -2045,7 +2045,7 @@ let typecheck uri ugraph = (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *) let ugraph1 = (match uobj with - C.Constant (_,Some te,ty,_) -> + C.Constant (_,Some te,ty,_,_) -> let _,ugraph1 = type_of ~logger ty ugraph in let ty_te,ugraph2 = type_of ~logger te ugraph1 in let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in @@ -2054,11 +2054,11 @@ let typecheck uri ugraph = ("Unknown constant:" ^ U.string_of_uri uri)) else ugraph3 - | C.Constant (_,None,ty,_) -> + | C.Constant (_,None,ty,_,_) -> (* only to check that ty is well-typed *) let _,ugraph1 = type_of ~logger ty ugraph in ugraph1 - | C.CurrentProof (_,conjs,te,ty,_) -> + | C.CurrentProof (_,conjs,te,ty,_,_) -> let _,ugraph1 = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> @@ -2080,7 +2080,7 @@ let typecheck uri ugraph = (CicPp.ppterm ty))) else ugraph4 - | C.Variable (_,bo,ty,_) -> + | C.Variable (_,bo,ty,_,_) -> (* only to check that ty is well-typed *) let _,ugraph1 = type_of ~logger ty ugraph in (match bo with diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml index c02719454..a7861444e 100644 --- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml +++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml @@ -54,7 +54,7 @@ let universes_of_obj uri t = don := u::!don; (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with - | C.InductiveDefinition (l,_,_) -> + | C.InductiveDefinition (l,_,_,_) -> List.fold_left ( fun y (_,_,t,l') -> y @ (aux t) @ @@ -72,7 +72,7 @@ let universes_of_obj uri t = begin don := u::!don; (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with - | C.InductiveDefinition (l,_,_) -> + | C.InductiveDefinition (l,_,_,_) -> List.fold_left ( fun x (_,_,_t,l') -> x @ aux t @ @@ -113,37 +113,37 @@ let universes_of_obj uri t = List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs and aux_obj ?(boo=false) (t,_) = (match t with - C.Constant (_,Some te,ty,v) -> aux te @ aux ty @ + C.Constant (_,Some te,ty,v,_) -> aux te @ aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v - | C.Constant (_,None,ty,v) -> aux ty @ + | C.Constant (_,None,ty,v,_) -> aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v - | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @ + | C.CurrentProof (_,conjs,te,ty,v,_) -> aux te @ aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v - | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @ + | C.Variable (_,Some bo,ty,v,_) -> aux bo @ aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v - | C.Variable (_,None ,ty,v) -> aux ty @ + | C.Variable (_,None ,ty,v,_) -> aux ty @ List.fold_left ( fun l u -> l @ if eq u uri then [] else (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u))) [] v - | C.InductiveDefinition (l,v,_) -> + | C.InductiveDefinition (l,v,_,_) -> (List.fold_left ( fun x (_,_,t,l') -> x @ aux t @ List.fold_left ( diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 24171327c..fe70f250a 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -76,8 +76,8 @@ let rec type_of_constant uri ugraph = *) let obj,u= CicEnvironment.get_obj ugraph uri in match obj with - C.Constant (_,_,ty,_) -> ty,u - | C.CurrentProof (_,_,_,ty,_) -> ty,u + C.Constant (_,_,ty,_,_) -> ty,u + | C.CurrentProof (_,_,_,ty,_,_) -> ty,u | _ -> raise (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri)) @@ -95,7 +95,7 @@ and type_of_variable uri ugraph = *) let obj,u = CicEnvironment.get_obj ugraph uri in match obj with - C.Variable (_,_,ty,_) -> ty,u + C.Variable (_,_,ty,_,_) -> ty,u | _ -> raise (RefineFailure @@ -114,7 +114,7 @@ and type_of_mutual_inductive_defs uri i ugraph = *) let obj,u = CicEnvironment.get_obj ugraph uri in match obj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,arity,_) = List.nth dl i in arity,u | _ -> @@ -135,7 +135,7 @@ and type_of_mutual_inductive_constr uri i j ugraph = *) let obj,u = CicEnvironment.get_obj ugraph uri in match obj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty,u @@ -366,7 +366,7 @@ and type_of_aux' metasenv context t ugraph = *) let obj,u = CicEnvironment.get_obj ugraph uri in match obj with - C.InductiveDefinition (l,expl_params,parsno) -> + C.InductiveDefinition (l,expl_params,parsno,_) -> List.nth l i , expl_params, parsno, u | _ -> raise diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index 4dd05073b..e01f28eb3 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -94,7 +94,7 @@ let get_closure_coercions src tgt uri = [] c_to_src) ;; - +let obj_attrs = [`Class `Coercion; `Generated] (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) let generate_composite_closure c1 c2 univ = @@ -129,7 +129,7 @@ let generate_composite_closure c1 c2 univ = let cleaned_ty = FreshNamesGenerator.clean_dummy_dependent_types c_ty in - let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[]) in + let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in obj,univ ;; @@ -161,13 +161,14 @@ let close_coercion_graph src tgt uri = CicUtil.term_of_uri (UriManager.string_of_uri uri) in let first_step = - (Cic.Constant ("",Some (term_of_uri' he),Cic.Sort Cic.Prop,[])) + Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [], + obj_attrs) in let o,u = List.fold_left (fun (o,u) coer -> match o with - | Cic.Constant (_,Some c,_,[]) -> - generate_composite_closure c (term_of_uri' coer) u + | Cic.Constant (_,Some c,_,[],_) -> + generate_composite_closure c (term_of_uri' coer) u | _ -> assert false ) (first_step, CicUniv.empty_ugraph) tl in @@ -180,7 +181,8 @@ let close_coercion_graph src tgt uri = in let named_obj = match o with - | Cic.Constant (_,bo,ty,vl) -> Cic.Constant (name,bo,ty,vl) + | Cic.Constant (_,bo,ty,vl,attrs) -> + Cic.Constant (name,bo,ty,vl,attrs) | _ -> assert false in ((src,tgt,c_uri),(c_uri,named_obj,u)) -- 2.39.2