-let select ~term ~context =
- let rec aux context term =
- match (context, term) with
- | Cic.Implicit (Some `Hole), t -> [t]
- | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
- List.concat
- (List.map2
- (fun t1 t2 ->
- (match (t1, t2) with Some t1, Some t2 -> aux t1 t2 | _ -> []))
- ctxt1 ctxt2)
- | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux te1 te2 @ aux ty1 ty2
- | Cic.Prod (_, s1, t1), Cic.Prod (_, s2, t2)
- | Cic.Lambda (_, s1, t1), Cic.Lambda (_, s2, t2)
- | Cic.LetIn (_, s1, t1), Cic.LetIn (_, s2, t2) -> aux s1 s2 @ aux t1 t2
- | Cic.Appl terms1, Cic.Appl terms2 -> auxs terms1 terms2
- | Cic.Var (_, subst1), Cic.Var (_, subst2)
- | Cic.Const (_, subst1), Cic.Const (_, subst2)
- | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2)
- | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) ->
- auxs (List.map snd subst1) (List.map snd subst2)
- | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) ->
- aux out1 out2 @ aux t1 t2 @ auxs pat1 pat2
- | Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
- List.concat
- (List.map2
- (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> aux ty1 ty2 @ aux bo1 bo2)
- funs1 funs2)
- | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
- List.concat
- (List.map2
- (fun (_, ty1, bo1) (_, ty2, bo2) -> aux ty1 ty2 @ aux bo1 bo2)
- funs1 funs2)
- | _ -> assert false
- and auxs terms1 terms2 = (* as aux for list of terms *)
- List.concat (List.map2 aux terms1 terms2)
- in
- aux context term
+let uri_of_term = function
+ | Cic.Const (uri, [])
+ | Cic.Var (uri, []) -> uri
+ | Cic.MutInd (baseuri, tyno, []) ->
+ UriManager.uri_of_string
+ (sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1))
+ | Cic.MutConstruct (baseuri, tyno, consno, []) ->
+ UriManager.uri_of_string
+ (sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
+ (tyno + 1) consno)
+ | _ -> raise (Invalid_argument "uri_of_term")