let rec compare x y =
match x,y with
| NCic.Rel i, NCic.Rel j -> i-j
+ | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
| NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
- | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *)
+ | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
+ | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
+ | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
+ | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
+ | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
+ | NCic.Appl _, NCic.Meta _ -> ~-1
+ | NCic.Meta _, NCic.Appl _ -> 1
| _ -> assert false
;;
+
+ let compare x y =
+ if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0
+ else compare x y
+ ;;
let pp t =
NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;;
proof, sty
;;
- let is_eq_predicate t = assert false;;
+ let eqP =
+ let r =
+ OCic2NCic.reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
+ in
+ NCic.Const r
+ ;;
+
+ let eq_ind =
+ let r =
+ OCic2NCic.reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_ind.con")
+ in
+ NCic.Const r
+ ;;
+
+ let eq_ind_r =
+ let r =
+ OCic2NCic.reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_elim_r.con")
+ in
+ NCic.Const r
+ ;;
+
+ let eq_refl =
+ let r =
+ OCic2NCic.reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
+ in
+ NCic.Const r
+ ;;
+ let extract lift vl t =
+ let rec pos i = function
+ | [] -> raise Not_found
+ | j :: tl when j <> i -> 1+ pos i tl
+ | _ -> 1
+ in
+ let vl_len = List.length vl in
+ let rec extract = function
+ | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
+ | Terms.Var j ->
+ (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term)
+ | Terms.Node l -> NCic.Appl (List.map extract l)
+ in
+ extract t
+ ;;
+
+ let rec ppfot = function
+ | Terms.Leaf _ -> "."
+ | Terms.Var i -> "?" ^ string_of_int i
+ | Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")"
+ ;;
+
+ let mk_predicate hole_type amount ft p vl =
+ let rec aux t p =
+ match p with
+ | [] -> NCic.Rel 1
+ | n::tl ->
+ match t with
+ | Terms.Leaf _
+ | Terms.Var _ ->
+ prerr_endline ("term: " ^ ppfot ft);
+ prerr_endline ("path: " ^ String.concat ","
+ (List.map string_of_int p));
+ assert false
+ | Terms.Node l ->
+ let l =
+ HExtlib.list_mapi
+ (fun t i ->
+ if i = n then aux t tl
+ else extract amount (0::vl) t)
+ l
+ in
+ NCic.Appl l
+ in
+ NCic.Lambda("x", hole_type, aux ft (List.rev p))
+ ;;
+
+ let mk_proof (bag : NCic.term Terms.bag) mp steps =
+ let module Subst = FoSubst in
+ let position i l =
+ let rec aux = function
+ | [] -> assert false
+ | (j,_) :: tl when i = j -> 1
+ | _ :: tl -> 1 + aux tl
+ in
+ aux l
+ in
+ let vars_of i l = fst (List.assoc i l) in
+ let ty_of i l = snd (List.assoc i l) in
+ let close_with_lambdas vl t =
+ List.fold_left
+ (fun t i ->
+ NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
+ t vl
+ in
+ let close_with_forall vl t =
+ List.fold_left
+ (fun t i ->
+ NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
+ t vl
+ in
+ let rec aux ongoal seen = function
+ | [] -> NCic.Rel 1
+ | id :: tl ->
+ let amount = List.length seen in
+ let _, lit, vl, proof = Terms.M.find id bag in
+ let lit =
+ match lit with
+ | Terms.Predicate t -> assert false
+ | Terms.Equation (l,r,ty,_) ->
+ Terms.Node [ Terms.Leaf eqP; ty; l; r]
+ in
+ if not ongoal && id = mp then
+ (assert (vl = []);
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ extract amount vl lit,
+ (NCic.Appl [eq_refl;NCic.Implicit `Type;NCic.Implicit `Term]),
+ aux true ((id,([],lit))::seen) (id::tl)))
+ else
+ match proof with
+ | Terms.Exact _ when tl=[] -> aux ongoal seen tl
+ | Terms.Step _ when tl=[] -> assert false
+ | Terms.Exact ft ->
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ close_with_forall vl (extract amount vl lit),
+ close_with_lambdas vl (extract amount vl ft),
+ aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+ | Terms.Step (_, id1, id2, dir, pos, subst) ->
+ let id, id1 = if ongoal then id1,id else id,id1 in
+ let proof_of_id id =
+ let vars = List.rev (vars_of id seen) in
+ let args = List.map (Subst.apply_subst subst) vars in
+ let args = List.map (extract amount vl) args in
+ NCic.Appl (NCic.Rel (List.length vl + position id seen) :: args)
+ in
+ let p_id1 = proof_of_id id1 in
+ let p_id2 = proof_of_id id2 in
+ let pred, hole_type, l, r =
+ let id1_ty = ty_of id1 seen in
+ let id2_ty,l,r =
+ match ty_of id2 seen with
+ | Terms.Node [ _; t; l; r ] ->
+ extract amount vl (Subst.apply_subst subst t),
+ extract amount vl (Subst.apply_subst subst l),
+ extract amount vl (Subst.apply_subst subst r)
+ | _ -> assert false
+ in
+ mk_predicate
+ id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
+ id2_ty,
+ l,r
+ in
+ let l, r, eq_ind =
+ if (ongoal=true) = (dir=Terms.Left2Right) then
+ r,l,eq_ind_r
+ else
+ l,r,eq_ind
+ in
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ close_with_forall vl (extract amount vl lit),
+ close_with_lambdas vl
+ (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
+ aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
+ in
+ aux false [] steps
+ ;;
end
projects / helm.git / blobdiff