| ((Cic.AConst _) as he)::tl
| ((Cic.AMutInd _) as he)::tl
| ((Cic.AMutConstruct _) as he)::tl when
- CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+ CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
!hide_coercions ->
let rec last =
function
| l -> idref aid (Ast.Appl l)
in
let deannot_he = Deannotate.deannotate_term he in
- if CoercGraph.is_a_coercion deannot_he && !Acic2content.hide_coercions
+ if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions
then
- match CoercGraph.is_a_coercion_to_funclass deannot_he with
+ match CoercDb.is_a_coercion_to_funclass deannot_he with
| None -> idref aid (last_n 1 (List.map k tl))
| Some i -> idref aid (last_n (i+1) (List.map k tl))
else
+termUtil.cmo: cicMkImplicit.cmi termUtil.cmi
+termUtil.cmx: cicMkImplicit.cmx termUtil.cmi
+coercGraph.cmo: coercGraph.cmi
+coercGraph.cmx: coercGraph.cmi
cicMetaSubst.cmo: cicMetaSubst.cmi
cicMetaSubst.cmx: cicMetaSubst.cmi
cicMkImplicit.cmo: cicMkImplicit.cmi
cicMkImplicit.cmx: cicMkImplicit.cmi
-cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi
-cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi
-cicRefine.cmo: cicUnification.cmi cicMkImplicit.cmi cicMetaSubst.cmi \
- cicRefine.cmi
-cicRefine.cmx: cicUnification.cmx cicMkImplicit.cmx cicMetaSubst.cmx \
- cicRefine.cmi
+cicUnification.cmo: coercGraph.cmi cicMkImplicit.cmi cicMetaSubst.cmi \
+ cicUnification.cmi
+cicUnification.cmx: coercGraph.cmx cicMkImplicit.cmx cicMetaSubst.cmx \
+ cicUnification.cmi
+cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \
+ cicMetaSubst.cmi cicRefine.cmi
+cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \
+ cicMetaSubst.cmx cicRefine.cmi
INTERFACE_FILES = \
cicMetaSubst.mli \
cicMkImplicit.mli \
+ termUtil.mli \
+ coercGraph.mli \
cicUnification.mli \
cicRefine.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
let imp = Cic.Implicit None in
let dummyres = false,imp, imp,imp,imp in
match t with
- | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
+ | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
(match last_of tl with
- | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
+ | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
let sib2,head = last_of tl2 in
true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
(c2::sib2@[imp])])
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
- let try_coercion t subst metasenv context ugraph coercion_tgt c =
- let coerced =
- match c with
- C.Appl l2 -> C.Appl (l2@[t])
- | _ -> C.Appl [c;t]
+ let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) =
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last t ugraph
in
try
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context coerced ugraph
- in
let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv ugraph newt coercion_tgt
+ avoid_double_coercion context subst metasenv ugraph coerced
+ coercion_tgt
in
Some (newt, tty, subst, metasenv, ugraph)
with
| term ->
let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
let boh =
- CoercGraph.look_for_coercion coercion_src coercion_tgt
+ CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
in
(match boh with
| CoercGraph.NoCoercion
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (try_coercion
- t subst metasenv context ugraph coercion_tgt)
+ (try_coercion t subst context ugraph coercion_tgt)
candidates
in
match selected with
| coercion_src ->
let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
let boh =
- CoercGraph.look_for_coercion coercion_src coercion_tgt
+ CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt
in
match boh with
| CoercGraph.NoCoercion
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (try_coercion
- s' subst' metasenv' context ugraph1 coercion_tgt)
- candidates
+ (try_coercion s' subst' context ugraph1 coercion_tgt)
+ candidates
in
match selected with
| Some x -> x
if b then
let source_carr = CoercGraph.source_of c2 in
let tgt_carr = CicMetaSubst.apply_subst subst ty in
- (match CoercGraph.look_for_coercion source_carr tgt_carr
+ (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
with
| CoercGraph.SomeCoercion candidates ->
- let selected =
+ let selected =
HExtlib.list_findopt
- (function
+ (function (metasenv,last,c) ->
+ match c with
| c when not (CoercGraph.is_composite c) ->
debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
None
| c ->
- let newt =
- match c with
- | Cic.Appl l -> Cic.Appl (l @ [head])
- | _ -> Cic.Appl [c;head]
- in
- debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt));
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last head ugraph in
+ debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
(try
debug_print
(lazy
("packing: " ^
- CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context newt ugraph in
+ type_of_aux subst metasenv context c ugraph in
debug_print (lazy "tipa...");
let subst, metasenv, ugraph =
(* COME MAI C'ERA UN IF su !pack_coercions ??? *)
CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
in
let carr_tgt = CoercDb.Fun 0 in
- match CoercGraph.look_for_coercion' carr_src carr_tgt with
+ match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
| CoercGraph.NoCoercion
| CoercGraph.NotMetaClosed
| CoercGraph.NotHandled _ -> raise exn
| CoercGraph.SomeCoercion candidates ->
match
HExtlib.list_findopt
- (fun coerc ->
- let t = Cic.Appl [coerc;x] in
- debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t));
+ (fun (metasenv,last,coerc) ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last x ugraph in
+ debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
try
(* we want this to be available in the error handler fo the
* following (so it has its own try. *)
let t,tty,subst,metasenv,ugraph =
- type_of_aux subst metasenv context t ugraph
+ type_of_aux subst metasenv context coerc ugraph
in
try
let metasenv, hetype' =
in
Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
with Uncertain _ | RefineFailure _ -> None
- with Uncertain _ | RefineFailure _ -> None
- | exn -> assert false) (* ritornare None, e' un localized *)
+ with
+ Uncertain _
+ | RefineFailure _
+ | HExtlib.Localized (_,Uncertain _)
+ | HExtlib.Localized (_,RefineFailure _) -> None
+ | exn -> assert false) (* ritornare None, e' un localized *)
candidates
with
| Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
in
let c_hety = carr hety subst context in
let c_s = carr s subst context in
- CoercGraph.look_for_coercion c_hety c_s, c_s
+ CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s
in
(match coer with
| CoercGraph.NoCoercion
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (fun c ->
+ (fun (metasenv,last,c) ->
try
- let t = Cic.Appl[c;hete] in
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last hete
+ ugraph in
let newt,newhety,subst,metasenv,ugraph =
type_of_aux subst metasenv context
- t ugraph
+ c ugraph
in
let newt, newty, subst, metasenv, ugraph =
avoid_double_coercion context subst metasenv
(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
- CoercGraph.is_a_coercion c1 &&
- CoercGraph.is_a_coercion c2 &&
+ CoercDb.is_a_coercion' c1 &&
+ CoercDb.is_a_coercion' c2 &&
not (UriManager.eq uri1 uri2) ->
- let body1, attrs1, ugraph =
- match CicEnvironment.get_obj ugraph uri1 with
- | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
- | _ -> assert false
- in
- let body2, attrs2, ugraph =
- match CicEnvironment.get_obj ugraph uri2 with
- | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
- | _ -> assert false
- in
- let is_composite1 =
- List.exists
- (function `Class (`Coercion _) -> true | _-> false)
- attrs1
- in
- let is_composite2 =
- List.exists
- (function `Class (`Coercion _) -> true | _-> false)
- attrs2
- in
- (match is_composite1, is_composite2 with
- | false, false -> raise exn
- | true, false ->
- let body1 = CicSubstitution.subst_vars ens1 body1 in
- let appl = Cic.Appl (body1::tl1) in
- let redappl = CicReduction.head_beta_reduce appl in
- fo_unif_subst
- test_equality_only subst context metasenv
- redappl t2 ugraph
- | false, true ->
- let body2 = CicSubstitution.subst_vars ens2 body2 in
- let appl = Cic.Appl (body2::tl2) in
- let redappl = CicReduction.head_beta_reduce appl in
- fo_unif_subst
- test_equality_only subst context metasenv
- t1 redappl ugraph
- | true, true ->
- let body1 = CicSubstitution.subst_vars ens1 body1 in
- let appl1 = Cic.Appl (body1::tl1) in
- let redappl1 = CicReduction.head_beta_reduce appl1 in
- let body2 = CicSubstitution.subst_vars ens2 body2 in
- let appl2 = Cic.Appl (body2::tl2) in
- let redappl2 = CicReduction.head_beta_reduce appl2 in
- fo_unif_subst
- test_equality_only subst context metasenv
- redappl1 redappl2 ugraph)
+(*DEBUGGING ONLY:
+prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+let res =
+*)
+ let rec look_for_first_coercion c tl =
+ match
+ CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
+ with
+ Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
+ when CoercDb.is_a_coercion' c' ->
+ look_for_first_coercion c' tl'
+ | last_tl -> c,last_tl
+ in
+ let c1,last_tl1 = look_for_first_coercion c1 tl1 in
+ let c2,last_tl2 = look_for_first_coercion c2 tl2 in
+ let car1 =
+ CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
+ let car2 =
+ CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
+ if CoercDb.eq_carr car1 car2 then
+ (match last_tl1,last_tl2 with
+ C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn
+ | C.Meta _, _
+ | _, C.Meta _ ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1 last_tl2 ugraph
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv (C.Appl l1) (C.Appl l2) ugraph
+ | _ -> raise exn)
+ else
+ let meets = CoercGraph.meets car1 car2 in
+ (match meets with
+ | [] -> raise exn
+ | _::_::_ ->
+prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
+assert false
+ | [m] ->
+ let last_tl1',(subst,metasenv,ugraph) =
+ match last_tl1 with
+ | Cic.Meta (i1,l1)
+ when not (CoercDb.eq_carr m car1) ->
+ (match
+ CoercGraph.look_for_coercion' metasenv subst
+ context m car1
+ with
+ | CoercGraph.SomeCoercion [metasenv,last,coerced]
+ ->
+ last,
+ fo_unif_subst test_equality_only subst context
+ metasenv coerced last_tl1 ugraph
+ | _ ->
+prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
+assert false)
+ | _ -> last_tl1,(subst,metasenv,ugraph) in
+ let last_tl2',(subst,metasenv,ugraph) =
+ match last_tl2 with
+ Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) ->
+ (match
+ CoercGraph.look_for_coercion' metasenv subst
+ context m car2
+ with
+ | CoercGraph.SomeCoercion [metasenv,last,coerced]
+ ->
+ last,
+ fo_unif_subst test_equality_only subst context
+ metasenv coerced last_tl2 ugraph
+ | _ ->
+prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
+assert false)
+ | _ -> last_tl2,(subst,metasenv,ugraph)
+ in
+(*DEBUGGING ONLY:
+prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
+*)
+ let subst,metasenv,ugraph =
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1' last_tl2' ugraph
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv (C.Appl l1) (C.Appl l2) ugraph)
+(*DEBUGGING ONLY:
+in
+let subst,metasenv,ugraph = res in
+prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res
+*)
(*CSC: This is necessary because of the "elim H" tactic
where the type of H is only reducible to an
inductive type. This could be extended from inductive
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id$ *)
+
+open Printf;;
+
+type coercion_search_result =
+ (* metasenv, last coercion argument, fully saturated coercion *)
+ (* to apply the coercion it is sufficient to unify the last coercion
+ argument (that is a Meta) with the term to be coerced *)
+ | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+ | NoCoercion
+ | NotMetaClosed
+ | NotHandled of string Lazy.t
+
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+(* searches a coercion fron src to tgt in the !coercions list *)
+let look_for_coercion' metasenv subst context src tgt =
+ try
+ let l =
+ CoercDb.find_coercion
+ (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
+ let uri =
+ match l with
+ | [] ->
+ debug_print
+ (lazy
+ (sprintf ":-( coercion non trovata da %s a %s"
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ None
+ | _::_ ->
+ debug_print (lazy (
+ sprintf ":-) TROVATE %d coercion(s) da %s a %s"
+ (List.length l)
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ Some l
+ in
+ (match uri with
+ None -> NoCoercion
+ | Some ul ->
+ let cl = List.map CicUtil.term_of_uri ul in
+ let funclass_arityl =
+ let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+ List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+ in
+ let freshmeta = CicMkImplicit.new_meta metasenv subst in
+ let newtl =
+ List.map2
+ (fun arity c ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' ~subst metasenv context c
+ CicUniv.empty_ugraph in
+ let _,metasenv,args,lastmeta =
+ TermUtil.saturate_term freshmeta metasenv context ty arity in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ metasenv, Cic.Meta (lastmeta-1,irl),
+ match args with
+ [] -> c
+ | _ -> Cic.Appl (c::args)
+ ) funclass_arityl cl
+ in
+ SomeCoercion newtl)
+ with
+ | CoercDb.EqCarrNotImplemented s -> NotHandled s
+ | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
+;;
+
+let look_for_coercion metasenv subst context src tgt =
+ let src_uri = CoercDb.coerc_carr_of_term src in
+ let tgt_uri = CoercDb.coerc_carr_of_term tgt in
+ look_for_coercion' metasenv subst context src_uri tgt_uri
+
+let source_of t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
+ with Invalid_argument _ -> assert false (* t must be a coercion *)
+
+let generate_dot_file () =
+ let module Pp = GraphvizPp.Dot in
+ let buf = Buffer.create 10240 in
+ let fmt = Format.formatter_of_buffer buf in
+ Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+ ~edge_attrs:["fontsize", "10"] fmt;
+ let l = CoercDb.to_list () in
+ let pp_description carr =
+ match CoercDb.uri_of_carr carr with
+ | None -> ()
+ | Some uri ->
+ Pp.node (CoercDb.name_of_carr carr)
+ ~attrs:["href", UriManager.string_of_uri uri] fmt in
+ List.iter
+ (fun (src, tgt, cl) ->
+ let src_name = CoercDb.name_of_carr src in
+ let tgt_name = CoercDb.name_of_carr tgt in
+ pp_description src;
+ pp_description tgt;
+ List.iter
+ (fun c ->
+ Pp.edge src_name tgt_name
+ ~attrs:[ "label", UriManager.name_of_uri c;
+ "href", UriManager.string_of_uri c ]
+ fmt)
+ cl)
+ l;
+ Pp.trailer fmt;
+ Buffer.contents buf
+;;
+
+let is_composite t =
+ try
+ let uri =
+ match t with
+ | Cic.Appl (he::_) -> CicUtil.uri_of_term he
+ | _ -> CicUtil.uri_of_term t
+ in
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ | Cic.Constant (_,_, _, _, attrs),_ ->
+ List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
+ | _ -> false
+ with Invalid_argument _ -> false
+;;
+
+let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;
+
+let splat e l = List.map (fun x -> e, x) l;;
+
+let get_coercions_to carr =
+ let l = CoercDb.to_list () in
+ List.flatten
+ (HExtlib.filter_map
+ (fun (src,tgt,cl) ->
+ if CoercDb.eq_carr tgt carr then Some (splat src cl) else None)
+ l)
+;;
+
+let get_coercions_from carr =
+ let l = CoercDb.to_list () in
+ List.flatten
+ (HExtlib.filter_map
+ (fun (src,tgt,cl) ->
+ if CoercDb.eq_carr src carr then Some (splat tgt cl) else None)
+ l)
+;;
+
+let intersect l1 l2 =
+ let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in
+ uniq (List.filter is_in_l1 l2)
+;;
+
+let grow s =
+ uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s)
+;;
+
+let lb c =
+ let l = get_coercions_from c in
+ function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
+;;
+
+let rec min acc = function
+ | c::tl ->
+ if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
+ | [] -> acc
+;;
+
+let meets left right =
+ let u = UriManager.uri_of_string "cic:/foo.con" in
+ min [] (List.map fst (intersect (grow [left,u]) (grow [right,u])))
+;;
+
+(* EOF *)
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id$ *)
+
+(* This module implements the Query interface to the Coercion Graph *)
+
+type coercion_search_result =
+ (* metasenv, last coercion argument, fully saturated coercion *)
+ (* to apply the coercion it is sufficient to unify the last coercion
+ argument (that is a Meta) with the term to be coerced *)
+ | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+ | NoCoercion
+ | NotMetaClosed
+ | NotHandled of string Lazy.t
+
+val look_for_coercion :
+ Cic.metasenv -> Cic.substitution -> Cic.context ->
+ Cic.term -> Cic.term -> coercion_search_result
+
+val look_for_coercion' :
+ Cic.metasenv -> Cic.substitution -> Cic.context ->
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result
+
+(* checks if term is a constant or
+ * a constant applyed that is marked with (`Class `Coercion) *)
+val is_composite: Cic.term -> bool
+
+val source_of: Cic.term -> Cic.term
+
+val generate_dot_file: unit -> string
+
+val meets :
+ CoercDb.coerc_carr -> CoercDb.coerc_carr ->
+ CoercDb.coerc_carr list
+
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: proofEngineHelpers.ml 7022 2006-11-15 19:47:41Z fguidi $ *)
+
+(* 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,[],[],newmeta,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
--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: proofEngineHelpers.ml 7022 2006-11-15 19:47:41Z fguidi $ *)
+
+(* 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. *)
+val saturate_term:
+ int -> Cic.metasenv -> Cic.context -> Cic.term -> int ->
+ Cic.term * Cic.metasenv * Cic.term list * int
cicCoercion.cmi: refinementTool.cmo coercDb.cmi
-coercGraph.cmi: coercDb.cmi
librarySync.cmi: refinementTool.cmo
cicElim.cmo: cicElim.cmi
cicElim.cmx: cicElim.cmi
coercDb.cmx: coercDb.cmi
cicCoercion.cmo: refinementTool.cmo coercDb.cmi cicCoercion.cmi
cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi
-coercGraph.cmo: coercDb.cmi coercGraph.cmi
-coercGraph.cmx: coercDb.cmx coercGraph.cmi
-librarySync.cmo: refinementTool.cmo libraryDb.cmi coercGraph.cmi coercDb.cmi \
- cicRecord.cmi cicElim.cmi cicCoercion.cmi librarySync.cmi
-librarySync.cmx: refinementTool.cmx libraryDb.cmx coercGraph.cmx coercDb.cmx \
- cicRecord.cmx cicElim.cmx cicCoercion.cmx librarySync.cmi
+librarySync.cmo: refinementTool.cmo libraryDb.cmi coercDb.cmi cicRecord.cmi \
+ cicElim.cmi cicCoercion.cmi librarySync.cmi
+librarySync.cmx: refinementTool.cmx libraryDb.cmx coercDb.cmx cicRecord.cmx \
+ cicElim.cmx cicCoercion.cmx librarySync.cmi
libraryNoDb.cmo: libraryNoDb.cmi
libraryNoDb.cmx: libraryNoDb.cmi
libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \
libraryDb.mli \
coercDb.mli \
cicCoercion.mli \
- coercGraph.mli \
librarySync.mli \
libraryNoDb.mli \
libraryClean.mli \
(HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
;;
-let is_a_coercion u =
- List.exists
- (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl)
- !db
-;;
-
let get_carr uri =
try
let src, tgt, _ =
with Not_found -> assert false (* uri must be a coercion *)
;;
+let is_a_coercion u =
+ List.exists
+ (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl)
+ !db
+;;
+
+let is_a_coercion' t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ is_a_coercion uri
+ with Invalid_argument _ -> false
+;;
+
+let is_a_coercion_to_funclass t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ match snd (get_carr uri) with
+ | Fun i -> Some i
+ | _ -> None
+ with Invalid_argument _ -> None
+
+
let term_of_carr = function
| Uri u -> CicUtil.term_of_uri u
| Sort s -> Cic.Sort s
(coerc_carr * coerc_carr -> bool) -> UriManager.uri list
val is_a_coercion: UriManager.uri -> bool
+val is_a_coercion': Cic.term -> bool
+val is_a_coercion_to_funclass: Cic.term -> int option
val get_carr: UriManager.uri -> coerc_carr * coerc_carr
val term_of_carr: coerc_carr -> Cic.term
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-open Printf;;
-
-type coercion_search_result =
- | SomeCoercion of Cic.term list
- | NoCoercion
- | NotMetaClosed
- | NotHandled of string Lazy.t
-
-let debug = false
-let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
-
-(* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion' src tgt =
- let arity_of con =
- try
- let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
- let rec count_pi = function
- | Cic.Prod (_,_,t) -> 1 + count_pi t
- | _ -> 0
- in
- count_pi ty
- with Invalid_argument _ -> assert false (* all coercions have an uri *)
- in
- let rec mk_implicits = function
- | 0 -> []
- | n -> Cic.Implicit None :: mk_implicits (n-1)
- in
- try
- let l =
- CoercDb.find_coercion
- (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
- let uri =
- match l with
- | [] ->
- debug_print
- (lazy
- (sprintf ":-( coercion non trovata da %s a %s"
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
- None
- | _::_ ->
- debug_print (lazy (
- sprintf ":-) TROVATE %d coercion(s) da %s a %s"
- (List.length l)
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
- Some l
- in
- (match uri with
- None -> NoCoercion
- | Some ul ->
- let cl = List.map CicUtil.term_of_uri ul in
- let funclass_arityl =
- let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
- List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
- in
- let arityl = List.map arity_of cl in
- let argsl =
- List.map2
- (fun arity fn_arity ->
- mk_implicits (arity - 1 - fn_arity)) arityl funclass_arityl
- in
- let newtl =
- List.map2
- (fun args c ->
- match args with
- | [] -> c
- | _ -> Cic.Appl (c::args))
- argsl cl
- in
- SomeCoercion newtl)
- with
- | CoercDb.EqCarrNotImplemented s -> NotHandled s
- | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
-;;
-
-let look_for_coercion src tgt =
- let src_uri = CoercDb.coerc_carr_of_term src in
- let tgt_uri = CoercDb.coerc_carr_of_term tgt in
- look_for_coercion' src_uri tgt_uri
-
-let is_a_coercion t =
- try
- let uri = CicUtil.uri_of_term t in
- CoercDb.is_a_coercion uri
- with Invalid_argument _ -> false
-
-let source_of t =
- try
- let uri = CicUtil.uri_of_term t in
- CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
- with Invalid_argument _ -> assert false (* t must be a coercion *)
-
-let is_a_coercion_to_funclass t =
- try
- let uri = CicUtil.uri_of_term t in
- match snd (CoercDb.get_carr uri) with
- | CoercDb.Fun i -> Some i
- | _ -> None
- with Invalid_argument _ -> None
-
-let generate_dot_file () =
- let module Pp = GraphvizPp.Dot in
- let buf = Buffer.create 10240 in
- let fmt = Format.formatter_of_buffer buf in
- Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
- ~edge_attrs:["fontsize", "10"] fmt;
- let l = CoercDb.to_list () in
- let pp_description carr =
- match CoercDb.uri_of_carr carr with
- | None -> ()
- | Some uri ->
- Pp.node (CoercDb.name_of_carr carr)
- ~attrs:["href", UriManager.string_of_uri uri] fmt in
- List.iter
- (fun (src, tgt, cl) ->
- let src_name = CoercDb.name_of_carr src in
- let tgt_name = CoercDb.name_of_carr tgt in
- pp_description src;
- pp_description tgt;
- List.iter
- (fun c ->
- Pp.edge src_name tgt_name
- ~attrs:[ "label", UriManager.name_of_uri c;
- "href", UriManager.string_of_uri c ]
- fmt)
- cl)
- l;
- Pp.trailer fmt;
- Buffer.contents buf
-;;
-
-let is_composite t =
- try
- let uri =
- match t with
- | Cic.Appl (he::_) -> CicUtil.uri_of_term he
- | _ -> CicUtil.uri_of_term t
- in
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
- | Cic.Constant (_,_, _, _, attrs),_ ->
- List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
- | _ -> false
- with Invalid_argument _ -> false
-;;
-
-let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;
-
-let splat e l = List.map (fun x -> e, x) l;;
-
-let get_coercions_to carr =
- let l = CoercDb.to_list () in
- List.flatten
- (HExtlib.filter_map
- (fun (src,tgt,cl) ->
- if CoercDb.eq_carr tgt carr then Some (splat src cl) else None)
- l)
-;;
-
-let get_coercions_from carr =
- let l = CoercDb.to_list () in
- List.flatten
- (HExtlib.filter_map
- (fun (src,tgt,cl) ->
- if CoercDb.eq_carr src carr then Some (splat tgt cl) else None)
- l)
-;;
-
-let intersect l1 l2 =
- let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in
- uniq (List.filter is_in_l1 l2)
-;;
-
-let grow s =
- uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s)
-;;
-
-let lb c =
- let l = get_coercions_from c in
- function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
-;;
-
-let rec min acc = function
- | c::tl ->
- if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
- | [] -> acc
-;;
-
-let meets left right =
- let u = UriManager.uri_of_string "cic:/foo.con" in
- min [] (List.map fst (intersect (grow [left,u]) (grow [right,u])))
-;;
-
-(* EOF *)
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-(* This module implements the Query interface to the Coercion Graph *)
-
-type coercion_search_result =
- | SomeCoercion of Cic.term list
- | NoCoercion
- | NotMetaClosed
- | NotHandled of string Lazy.t
-
-val look_for_coercion :
- Cic.term -> Cic.term -> coercion_search_result
-
-val look_for_coercion' :
- CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result
-
-val is_a_coercion: Cic.term -> bool
-val is_a_coercion_to_funclass: Cic.term -> int option
-
-(* checks if term is a constant or
- * a constant applyed that is marked with (`Class `Coercion) *)
-val is_composite: Cic.term -> bool
-
-val source_of: Cic.term -> Cic.term
-
-val generate_dot_file: unit -> string
-
-val meets :
- CoercDb.coerc_carr -> CoercDb.coerc_carr ->
- CoercDb.coerc_carr list
-
let module RT = RefinementTool in
let obj =
if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
- not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
+ not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
then
refinement_toolkit.RT.pack_coercion_obj obj
else
let is_unit_equation context metasenv oldnewmeta term =
let head, metasenv, args, newmeta =
- ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+ TermUtil.saturate_term oldnewmeta metasenv context term 0
in
let propositional_args =
HExtlib.filter_map
let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
let head, metasenv, args, newmeta =
- ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+ TermUtil.saturate_term oldnewmeta metasenv context term 0
in
let propositional_args =
HExtlib.filter_map
context term' ty termty goal_arity
=
let (consthead,newmetasenv,arguments,_) =
- ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
+ TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
let term'' =
match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
in
CicTypeChecker.type_of_aux' metasenv context equality
CicUniv.empty_ugraph in
let (ty_eq,metasenv',arguments,fresh_meta) =
- ProofEngineHelpers.saturate_term
+ TermUtil.saturate_term
(ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in
let equality =
if List.length arguments = 0 then
let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
let (consthead,newmetasenv,arguments,_) =
- ProofEngineHelpers.saturate_term newmeta' metasenv' context termty
+ TermUtil.saturate_term newmeta' metasenv' context termty
goal_arity in
let subst,newmetasenv',_ =
CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let termty = CicReduction.whd context termty in
let (termty,metasenv',arguments,fresh_meta) =
- ProofEngineHelpers.saturate_term
+ TermUtil.saturate_term
(ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
let term = if arguments = [] then term else Cic.Appl (term::arguments) in
let uri,exp_named_subst,typeno,args =
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
?equality:(Cic.context -> Cic.term -> Cic.term -> bool) ->
Cic.term -> Cic.conjecture -> (Cic.context * Cic.term) list
-(* 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. *)
-val saturate_term:
- int -> Cic.metasenv -> Cic.context -> Cic.term -> int ->
- Cic.term * Cic.metasenv * Cic.term list * int
-
(* returns the index and the type of a premise in a context *)
val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
let rec dummies_of_coercions =
function
- | Cic.Appl (c::l) when CoercGraph.is_a_coercion c ->
+ | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
Cic.Meta (-1,[])
| Cic.Appl l ->
let l' = List.map dummies_of_coercions l in Cic.Appl l'
projects / helm.git / commitdiff