+ subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
+ (entry::context))
+ ) context (subst,metasenv,ugraph,[],[]))
+ in
+ subst,metasenv,ugraph,res
+ in
+ subst,metasenv,ugraph,context_terms, ty_terms
+
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
+* [equality] defaults to physical equality
+* [context] must be the context of [where]
+*)
+let locate_in_term ?(equality=(fun _ -> (==))) what ~where context =
+ let add_ctx context name entry =
+ (Some (name, entry)) :: context in
+ let rec aux context where =
+ if equality context what where then [context,where]
+ else
+ match where with
+ | Cic.Implicit _
+ | Cic.Meta _
+ | Cic.Rel _
+ | Cic.Sort _
+ | Cic.Var _
+ | Cic.Const _
+ | Cic.MutInd _
+ | Cic.MutConstruct _ -> []
+ | Cic.Cast (te, ty) -> aux context te @ aux context ty
+ | Cic.Prod (name, s, t)
+ | Cic.Lambda (name, s, t) ->
+ aux context s @ aux (add_ctx context name (Cic.Decl s)) t
+ | Cic.LetIn (name, s, t) ->
+ aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
+ | Cic.Appl tl -> auxs context tl
+ | Cic.MutCase (_, _, out, t, pat) ->
+ aux context out @ aux context t @ auxs context pat
+ | Cic.Fix (_, funs) ->
+ let tys =
+ List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
+ in
+ List.concat
+ (List.map
+ (fun (_, _, ty, bo) ->
+ aux context ty @ aux (tys @ context) bo)
+ funs)
+ | Cic.CoFix (_, funs) ->
+ let tys =
+ List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
+ in
+ List.concat
+ (List.map
+ (fun (_, ty, bo) ->
+ aux context ty @ aux (tys @ context) bo)
+ funs)
+ and auxs context tl = (* as aux for list of terms *)
+ List.concat (List.map (fun t -> aux context t) tl)
+ in
+ aux context where
+
+(** locate_in_conjecture equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
+* [equality] defaults to physical equality
+* [context] must be the context of [where]
+*)
+let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) =
+ let context,res =
+ List.fold_right
+ (fun entry (context,res) ->
+ match entry with
+ None -> entry::context, res
+ | Some (_, Cic.Decl ty) ->
+ let res = res @ locate_in_term what ~where:ty context in
+ let context' = entry::context in
+ context',res
+ | Some (_, Cic.Def (bo,ty)) ->
+ let res = res @ locate_in_term what ~where:bo context in
+ let res =
+ match ty with
+ None -> res
+ | Some ty ->
+ res @ locate_in_term what ~where:ty context in
+ let context' = entry::context in
+ context',res
+ ) context ([],[])
+ in
+ res @ locate_in_term what ~where:ty context
+
+(* saturate_term newmeta metasenv context ty goal_arity *)
+(* Given a type [ty] (a backbone), it returns its suffix of length *)
+(* [goal_arity] head and a new metasenv in which there is new a META for each *)
+(* hypothesis, a list of arguments for the new applications and the index of *)
+(* the last new META introduced. The nth argument in the list of arguments is *)
+(* just the nth new META. *)
+let saturate_term newmeta metasenv context ty goal_arity =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ assert (goal_arity >= 0);
+ let rec aux newmeta ty =
+ match ty with
+ C.Cast (he,_) -> aux newmeta he
+(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
+ (* If the expected type is a Type, then also Set is OK ==>
+ * we accept any term of type Type *)
+ (*CSC: BUG HERE: in this way it is possible for the term of
+ * type Type to be different from a Sort!!! *)
+ | C.Prod (name,(C.Sort (C.Type _) as s),t) ->
+ (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *)
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let newargument = C.Meta (newmeta+1,irl) in
+ let (res,newmetasenv,arguments,lastmeta) =
+ aux (newmeta + 2) (S.subst newargument t)
+ in
+ res,
+ (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv,
+ newargument::arguments,lastmeta
+*)
+ | C.Prod (name,s,t) ->
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let newargument = C.Meta (newmeta,irl) in
+ let res,newmetasenv,arguments,lastmeta,prod_no =
+ aux (newmeta + 1) (S.subst newargument t)
+ in
+ if prod_no + 1 = goal_arity then
+ let head = CicReduction.normalize ~delta:false context ty in
+ head,[],[],lastmeta,goal_arity + 1
+ else
+ (** NORMALIZE RATIONALE
+ * we normalize the target only NOW since we may be in this case:
+ * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k
+ * and we want a mesasenv with ?1:A1 and ?2:A2 and not
+ * ?1, ?2, ?3 (that is the one we whould get if we start from the
+ * beta-normalized A1 -> A2 -> A3 -> P **)
+ let s' = CicReduction.normalize ~delta:false context s in
+ res,(newmeta,context,s')::newmetasenv,newargument::arguments,
+ lastmeta,prod_no + 1
+ | t ->
+ let head = CicReduction.normalize ~delta:false context t in
+ match CicReduction.whd context head with
+ C.Prod _ as head' -> aux newmeta head'
+ | _ -> head,[],[],newmeta,0
+ in
+ (* WARNING: here we are using the invariant that above the most *)
+ (* recente new_meta() there are no used metas. *)
+ let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in
+ res,metasenv @ newmetasenv,arguments,lastmeta
+
+let lookup_type metasenv context hyp =
+ let rec aux p = function
+ | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
+ | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
+ | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
+ p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
+ | _ :: tail -> aux (succ p) tail
+ | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))