From e626927b4c1c77bdcd6b545203a0a9c17a9ff136 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 6 Feb 2004 17:16:20 +0000 Subject: [PATCH] added annotations to Cic.Implicit --- helm/gTopLevel/logicalOperations.ml | 2 +- helm/gTopLevel/proofEngine.ml | 2 +- helm/ocaml/cic/cic.ml | 6 ++++-- helm/ocaml/cic/cicParser3.ml | 2 +- helm/ocaml/cic/deannotate.ml | 2 +- helm/ocaml/cic_annotations/cicXPath.ml | 2 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 14 +++++++++----- .../ocaml/cic_disambiguation/logic_notation.ml | 2 +- helm/ocaml/cic_omdoc/cic2acic.ml | 2 +- helm/ocaml/cic_omdoc/cic2content.ml | 2 +- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 8 ++++---- helm/ocaml/cic_omdoc/eta_fixing.ml | 2 +- .../ocaml/cic_proof_checking/cicEnvironment.ml | 2 +- .../cic_proof_checking/cicMiniReduction.ml | 2 +- helm/ocaml/cic_proof_checking/cicPp.ml | 2 +- .../cic_proof_checking/cicReductionMachine.ml | 8 ++++---- .../cic_proof_checking/cicReductionNaif.ml | 6 +++--- .../cic_proof_checking/cicSubstitution.ml | 8 ++++---- .../ocaml/cic_proof_checking/cicTypeChecker.ml | 18 +++++++++--------- helm/ocaml/cic_unification/cicMetaSubst.ml | 6 +++--- helm/ocaml/cic_unification/cicMkImplicit.ml | 9 ++++++++- helm/ocaml/cic_unification/cicRefine.ml | 2 +- helm/ocaml/cic_unification/cicUnification.ml | 2 +- .../cic_unification/freshNamesGenerator.ml | 2 +- .../mathql_generator/cGMatchConclusion.ml | 2 +- helm/ocaml/mathql_generator/cGSearchPattern.ml | 2 +- helm/ocaml/tactics/primitiveTactics.ml | 2 +- helm/ocaml/tactics/proofEngineReduction.ml | 14 +++++++------- 28 files changed, 73 insertions(+), 60 deletions(-) diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index 5d06c95d2..93c511f13 100644 --- a/helm/gTopLevel/logicalOperations.ml +++ b/helm/gTopLevel/logicalOperations.ml @@ -42,7 +42,7 @@ let get_context ids_to_terms ids_to_father_ids = | C.Var _ | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ -> [] | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)] | C.Prod _ -> [] diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index f320f0837..a9199c0e8 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -83,7 +83,7 @@ let metas_in_term term = C.Rel _ -> [] | C.Meta (n,_) -> [n] | C.Sort _ - | C.Implicit -> [] + | C.Implicit _ -> [] | C.Cast (te,ty) -> (aux te) @ (aux ty) | C.Prod (_,s,t) -> (aux s) @ (aux t) | C.Lambda (_,s,t) -> (aux s) @ (aux t) diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 46126ff31..55a338b3f 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -39,6 +39,8 @@ type id = string (* the abstract type of the (annotated) node identifiers *) type 'term explicit_named_substitution = (UriManager.uri * 'term) list +type implicit_annotation = [ `Closed | `Type ] + type anntarget = Object of annobj (* if annobj is a Constant, this is its type *) | ConstantBody of annobj @@ -62,7 +64,7 @@ and term = | Meta of int * (term option) list (* numeric id, *) (* local context *) | Sort of sort (* sort *) - | Implicit (* *) + | Implicit of implicit_annotation option (* *) | Cast of term * term (* value, type *) | Prod of name * term * term (* binder, source, target *) | Lambda of name * term * term (* binder, source, target *) @@ -123,7 +125,7 @@ and annterm = | AMeta of id * int * (annterm option) list (* numeric id, *) (* local context *) | ASort of id * sort (* sort *) - | AImplicit of id (* *) + | AImplicit of id * implicit_annotation option (* *) | ACast of id * annterm * annterm (* value, type *) | AProd of id * name * annterm * annterm (* binder, source, target *) | ALambda of id * name * annterm * annterm (* binder, source, target *) diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml index 02d22b321..121f36453 100644 --- a/helm/ocaml/cic/cicParser3.ml +++ b/helm/ocaml/cic/cicParser3.ml @@ -205,7 +205,7 @@ class eltype_implicit = assert (exp_named_subst = []) ; let n = self#node in let id = string_of_xml_attr (n#attribute "id") in - Cic.AImplicit id + Cic.AImplicit (id, None) end ;; diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml index 2bee18d6f..289fe7db4 100644 --- a/helm/ocaml/cic/deannotate.ml +++ b/helm/ocaml/cic/deannotate.ml @@ -43,7 +43,7 @@ let rec deannotate_term = in C.Meta (n, l') | C.ASort (_,s) -> C.Sort s - | C.AImplicit _ -> C.Implicit + | C.AImplicit (_, annotation) -> C.Implicit annotation | C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty) | C.AProd (_,name,so,ta) -> C.Prod (name, deannotate_term so, deannotate_term ta) diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml index b20fbd5c0..75a598d91 100644 --- a/helm/ocaml/cic_annotations/cicXPath.ml +++ b/helm/ocaml/cic_annotations/cicXPath.ml @@ -59,7 +59,7 @@ let get_ids_to_targets annobj = C.ARel (id,_,_,_) | C.AMeta (id,_,_) | C.ASort (id,_) - | C.AImplicit id -> + | C.AImplicit (id, _) -> set_target id (C.Term t) | C.ACast (id,va,ty) -> set_target id (C.Term t) ; diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index f75941475..110f3d75e 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -102,7 +102,7 @@ let interpretate ~context ~env ast = let cic_body = do_branch' (name :: context) tl in let typ = match typ with - | None -> Cic.Implicit + | None -> Cic.Implicit (Some `Type) | Some typ -> aux loc context typ in Cic.Lambda (name, typ, cic_body) @@ -112,7 +112,7 @@ let interpretate ~context ~env ast = let (indtype_uri, indtype_no) = match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> uri, tyno - | Cic.Implicit -> raise Try_again + | Cic.Implicit _ -> raise Try_again | _ -> raise DisambiguateChoices.Invalid_choice in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, @@ -175,7 +175,7 @@ let interpretate ~context ~env ast = "Explicit substitutions not allowed here"; Cic.Rel index with Not_found -> resolve env (Id name) ()) - | CicAst.Implicit -> Cic.Implicit + | CicAst.Implicit -> Cic.Implicit None | CicAst.Num (num, i) -> resolve env (Num i) ~num () | CicAst.Meta (index, subst) -> let cic_subst = @@ -191,7 +191,7 @@ let interpretate ~context ~env ast = | CicAst.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () and aux_option loc context = function - | None -> Cic.Implicit + | None -> Cic.Implicit (Some `Type) | Some term -> aux loc context term in match ast with @@ -390,7 +390,11 @@ module Make (C: Callbacks) = let filled_env = List.fold_left (fun env item -> - Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env) + Environment.add item + ("Implicit", + (match item with + | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) + | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) current_env todo_dom in try diff --git a/helm/ocaml/cic_disambiguation/logic_notation.ml b/helm/ocaml/cic_disambiguation/logic_notation.ml index a19361b32..1d47711da 100644 --- a/helm/ocaml/cic_disambiguation/logic_notation.ml +++ b/helm/ocaml/cic_disambiguation/logic_notation.ml @@ -57,6 +57,6 @@ let _ = in Cic.Appl [ Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); - Cic.Implicit; t1; t2 + Cic.Implicit (Some `Type); t1; t2 ])) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index f7c2317ba..8418a64d4 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -203,7 +203,7 @@ Cic.Sort Cic.Type ; | Some _, None -> assert false (* due to typing rules *)) canonical_context l)) | C.Sort s -> C.ASort (fresh_id'', s) - | C.Implicit -> C.AImplicit (fresh_id'') + | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation) | C.Cast (v,t) -> xxx_add ids_to_inner_sorts fresh_id'' innersort ; if innersort = "Prop" then diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index eac04e7aa..61003f930 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -70,7 +70,7 @@ let rec occur uri = | C.Var _ -> false | C.Meta _ -> false | C.Sort _ -> false - | C.Implicit -> raise NotImplemented + | C.Implicit _ -> assert false | C.Prod (_,s,t) -> (occur uri s) or (occur uri t) | C.Cast (te,ty) -> (occur uri te) | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *) diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 8880ff3f4..3163dfe09 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -58,7 +58,7 @@ let rec does_not_occur n = | C.Rel _ | C.Meta _ | C.Sort _ - | C.Implicit -> true + | C.Implicit _ -> true | C.Cast (te,ty) -> does_not_occur n te && does_not_occur n ty | C.Prod (name,so,dest) -> @@ -123,7 +123,7 @@ let rec head_beta_reduce = (function None -> None | Some t -> Some (head_beta_reduce t)) l ) | C.Sort _ as t -> t - | C.Implicit -> assert false + | C.Implicit _ -> assert false | C.Cast (te,ty) -> C.Cast (head_beta_reduce te, head_beta_reduce ty) | C.Prod (n,s,t) -> @@ -404,7 +404,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (* Checks suppressed *) CicSubstitution.lift_meta l ty | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) - | C.Implicit -> raise (Impossible 21) + | 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 (Some (head_beta_reduce ty)) in @@ -447,7 +447,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = if does_not_occur 1 t_typ then (* since [Rel 1] does not occur in typ, substituting any term *) (* in place of [Rel 1] is equivalent to delifting once *) - CicSubstitution.subst C.Implicit t_typ + CicSubstitution.subst (C.Implicit None) t_typ else C.LetIn (n,s,t_typ) | C.Appl (he::tl) when List.length tl > 0 -> diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index 49a68d1d0..24242b426 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -192,7 +192,7 @@ let eta_fix metasenv t = in C.Meta (n,l') | C.Sort s -> C.Sort s - | C.Implicit -> C.Implicit + | C.Implicit _ as t -> t | C.Cast (v,t) -> C.Cast (eta_fix' context v, eta_fix' context t) | C.Prod (n,s,t) -> C.Prod diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 3a201ad69..22138dde8 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -129,7 +129,7 @@ module Cache : in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty) | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t) | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t) diff --git a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml index 1f6b72636..bbf515a99 100644 --- a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml @@ -34,7 +34,7 @@ let rec letin_nf = C.Var (uri,exp_named_subst') | C.Meta _ as t -> t | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty) | C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t) | C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 152cdd198..b0e7d64ed 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -88,7 +88,7 @@ let rec pp t l = | C.Type -> "Type" | C.CProp -> "CProp" ) - | C.Implicit -> "?" + | C.Implicit _ -> "?" | C.Prod (b,s,t) -> (match b with C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l) diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index 8c1c5017d..dbe22fb3e 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -374,7 +374,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - in C.Meta (i, l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*) | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) @@ -546,7 +546,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; let t' = unwind k e ens t in if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)) | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *) - | (k, e, _, (C.Implicit as t), s) -> t (* s should be empty *) + | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *) | (k, e, ens, (C.Cast (te,ty) as t), s) -> reduce (k, e, ens, te, s) (* s should be empty *) | (k, e, ens, (C.Prod _ as t), s) -> @@ -654,7 +654,7 @@ if List.mem uri params then prerr_endline "---- OK2" ; in (* ts are already unwinded because they are a sublist of tl *) reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s) - | C.Cast _ | C.Implicit -> + | C.Cast _ | C.Implicit _ -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let t' = unwind k e ens t in @@ -877,7 +877,7 @@ let are_convertible = b && aux context ty1 ty2 && aux (tys@context) bo1 bo2) fl1 fl2 true | (C.Cast _, _) | (_, C.Cast _) - | (C.Implicit, _) | (_, C.Implicit) -> + | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (_,_) -> false end diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index 5dce7c68d..436200644 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -67,7 +67,7 @@ let whd context = ) | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> whdaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *) | C.Prod _ as t -> t (* l should be empty *) | C.Lambda (name,s,t) as t' -> @@ -136,7 +136,7 @@ let whd context = eat_first (r,tl) in whdaux (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> + | C.Cast _ | C.Implicit _ -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> if l = [] then t else C.Appl (t::l) ) @@ -290,7 +290,7 @@ let are_convertible = b && aux context ty1 ty2 && aux (tys@context) bo1 bo2) fl1 fl2 true | (C.Cast _, _) | (_, C.Cast _) - | (C.Implicit, _) | (_, C.Implicit) -> + | (C.Implicit _, _) | (_, C.Implicit _) -> raise (Impossible 3) (* we don't trust our whd ;-) *) | (_,_) -> false end diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 704a8325a..17ee01b53 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -54,7 +54,7 @@ let lift n = in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t) @@ -126,7 +126,7 @@ let subst arg = in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) @@ -234,7 +234,7 @@ prerr_endline "---- END\n\n " ; in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) @@ -370,7 +370,7 @@ let lift_meta l t = in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *) | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 395979505..8403f5f0c 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -66,7 +66,7 @@ let debrujin_constructor uri number_of_types = C.Var (uri,exp_named_subst') | C.Meta _ -> assert false | C.Sort _ - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t) @@ -205,7 +205,7 @@ and does_not_occur context n nn te = | C.Rel _ | C.Meta _ | C.Sort _ - | C.Implicit -> true + | C.Implicit _ -> true | C.Cast (te,ty) -> does_not_occur context n nn te && does_not_occur context n nn ty | C.Prod (name,so,dest) -> @@ -567,7 +567,7 @@ and recursive_args context n nn te = | C.Var _ | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ (*CSC ??? *) -> raise (AssertFailure "3") (* due to type-checking *) | C.Prod (name,so,de) -> @@ -646,7 +646,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = | C.Var _ | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ (* | C.Cast (te,ty) -> check_is_really_smaller_arg n nn kl x safes te && @@ -799,7 +799,7 @@ and guarded_by_destructors context n nn kl x safes = ) | C.Meta _ | C.Sort _ - | C.Implicit -> true + | C.Implicit _ -> true | C.Cast (te,ty) -> guarded_by_destructors context n nn kl x safes te && guarded_by_destructors context n nn kl x safes ty @@ -977,7 +977,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Rel _ -> true | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ | C.Prod _ | C.LetIn _ -> @@ -1008,7 +1008,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Var _ | C.Sort _ -> does_not_occur context n nn te - | C.Implicit + | C.Implicit _ | C.Cast _ -> raise (AssertFailure "24")(* due to type-checking *) | C.Prod (name,so,de) -> @@ -1042,7 +1042,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Var _ | C.Meta _ | C.Sort _ - | C.Implicit + | C.Implicit _ | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *) | C.Prod (name,so,de) -> begin @@ -1353,7 +1353,7 @@ and type_of_aux' metasenv context t = check_metasenv_consistency metasenv context canonical_context l; CicSubstitution.lift_meta l ty | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) - | C.Implicit -> raise (AssertFailure "21") + | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) as t -> let _ = type_of_aux context ty in if R.are_convertible context (type_of_aux context te) ty then diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 4ee371684..a19bb2b25 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -27,7 +27,7 @@ let apply_subst_gen ~appl_fun subst term = in C.Meta (i,l')) | C.Sort _ as t -> t - | C.Implicit -> assert false + | C.Implicit _ -> assert false | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) @@ -280,7 +280,7 @@ let rec force_does_not_occur subst to_be_restricted t = C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur | C.Rel _ | C.Sort _ as t -> t - | C.Implicit -> assert false + | C.Implicit _ -> assert false | C.Meta (n, l) -> (* we do not retrieve the term associated to ?n in subst since *) (* in this way we can restrict if something goes wrong *) @@ -516,7 +516,7 @@ let delift n subst context metasenv l t = let l' = deliftl 1 l1 in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 1817ac861..99e599ab2 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -87,7 +87,14 @@ let expand_implicits metasenv context term = | Cic.Meta (n,l) -> let metasenv', l' = do_local_context metasenv context l in metasenv', Cic.Meta (n, l') - | Cic.Implicit -> + | Cic.Implicit (Some `Type) -> + let (metasenv', idx) = mk_implicit_type metasenv context in + let irl = identity_relocation_list_for_metavariable context in + metasenv', Cic.Meta (idx, irl) + | Cic.Implicit (Some `Closed) -> + let (metasenv', idx) = mk_implicit metasenv [] in + metasenv', Cic.Meta (idx, []) + | Cic.Implicit None -> let (metasenv', idx) = mk_implicit metasenv context in let irl = identity_relocation_list_for_metavariable context in metasenv', Cic.Meta (idx, irl) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 77b376d63..43ecd8929 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -169,7 +169,7 @@ and type_of_aux' metasenv context t = | C.Sort s -> C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) subst,metasenv - | C.Implicit -> raise (Impossible 21) + | C.Implicit _ -> raise (Impossible 21) | C.Cast (te,ty) -> let _,subst',metasenv' = type_of_aux subst metasenv context ty in diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 1dc4ae2bd..3c8b07729 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -144,7 +144,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; raise (UnificationFailure (sprintf "Can't unify %s with %s due to different inductive constructors" (CicPp.ppterm t1) (CicPp.ppterm t1))) - | (C.Implicit, _) | (_, C.Implicit) -> assert false + | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2 | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml index fc1b4f36e..1a94c3185 100644 --- a/helm/ocaml/cic_unification/freshNamesGenerator.ml +++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml @@ -95,7 +95,7 @@ let clean_dummy_dependent_types t = in C.Meta(i,l'),rels | C.Sort _ as t -> t,[] - | C.Implicit as t -> t,[] + | C.Implicit _ as t -> t,[] | C.Cast (te,ty) -> let te',rels1 = aux k te in let ty',rels2 = aux k ty in diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml index bb87b461e..42d52a7ac 100644 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml @@ -70,7 +70,7 @@ let levels_of_term metasenv context term = Cic.Rel _ -> l | Cic.Meta _ -> l | Cic.Sort _ -> l - | Cic.Implicit -> l + | Cic.Implicit _ -> l | Cic.Var (u,exp_named_subst) -> let l' = inspect_uri main l u [] v term in inspect_exp_named_subst l' (succ v) exp_named_subst diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml index a56d65959..7640a6b76 100644 --- a/helm/ocaml/mathql_generator/cGSearchPattern.ml +++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml @@ -101,7 +101,7 @@ let get_constraints term = [],[],[!!kind,s'] | _ -> [],[],[]) | C.Meta _ - | C.Implicit -> assert false + | C.Implicit _ -> assert false | C.Cast (te,_) -> (* type ignored *) process_type_aux kind te diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index a518edaa6..326d9e2c2 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -74,7 +74,7 @@ let eta_expand metasenv context t arg = C.Var (uri,exp_named_subst') | C.Meta _ | C.Sort _ - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t) | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t) diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index 9e5aa04ff..99eb43f6a 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -142,7 +142,7 @@ let replace ~equality ~what ~with_what ~where = C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) | C.Meta _ -> t | C.Sort _ -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux te, aux ty) | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) @@ -216,7 +216,7 @@ let replace_lifting ~equality ~what ~with_what ~where = in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty) | C.Prod (n,s,t) -> C.Prod @@ -315,7 +315,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where = in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) @@ -402,7 +402,7 @@ let reduce context = ) | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (reduceaux context l te, reduceaux context l ty) | C.Prod (name,s,t) -> @@ -506,7 +506,7 @@ let reduce context = eat_first (r,tl) in reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> + | C.Cast _ | C.Implicit _ -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let outtype' = reduceaux context [] outtype in @@ -625,7 +625,7 @@ let simpl context = ) | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (reduceaux context l te, reduceaux context l ty) | C.Prod (name,s,t) -> @@ -726,7 +726,7 @@ let simpl context = eat_first (r,tl) in reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> + | C.Cast _ | C.Implicit _ -> raise (Impossible 2) (* we don't trust our whd ;-) *) | _ -> let outtype' = reduceaux context [] outtype in -- 2.39.2