end
module NCicBlob(C : NCicContext) : Terms.Blob
-with type t = NCic.term and type input = NCic.term = struct
+with type t = NCic.term = struct
type t = NCic.term
let pp t =
NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
- type input = NCic.term
-
- let rec embed = function
- | NCic.Meta (i,_) -> Terms.Var i, [i]
- | NCic.Appl l ->
- let rec aux acc l = function
- |[] -> acc@l
- |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
- in
- let res,vars = List.fold_left
- (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
- in (Terms.Node (List.rev res)), vars
- | t -> Terms.Leaf t, []
- ;;
-
- let embed t = fst (embed t) ;;
-
- let saturate t ty =
- let sty, _, args =
- NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
- ty 0
- in
- let proof =
- if args = [] then Terms.Leaf t
- else Terms.Node (Terms.Leaf t :: List.map embed args)
- in
- let sty = embed sty in
- proof, sty
- ;;
-
let eqP =
let r =
OCic2NCic.reference_of_oxuri