From: Andrea Asperti Date: Thu, 7 Oct 2010 09:51:17 +0000 (+0000) Subject: cic_unification removed X-Git-Tag: make_still_working~2796 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=907f919aba0f21b18acff8a8e1c266ab92d10baf;p=helm.git cic_unification removed --- diff --git a/matita/components/METAS/meta.helm-cic_unification.src b/matita/components/METAS/meta.helm-cic_unification.src deleted file mode 100644 index 75e2d4d31..000000000 --- a/matita/components/METAS/meta.helm-cic_unification.src +++ /dev/null @@ -1,5 +0,0 @@ -requires="helm-cic_proof_checking helm-library" -version="0.0.1" -archive(byte)="cic_unification.cma" -archive(native)="cic_unification.cmxa" -linkopts="" diff --git a/matita/components/METAS/meta.helm-grafite_engine.src b/matita/components/METAS/meta.helm-grafite_engine.src index a8f4e2f12..918352ed5 100644 --- a/matita/components/METAS/meta.helm-grafite_engine.src +++ b/matita/components/METAS/meta.helm-grafite_engine.src @@ -1,4 +1,4 @@ -requires="helm-library helm-grafite helm-cic_unification helm-ng_tactics helm-ng_library" +requires="helm-library helm-grafite helm-cic_proof_checking helm-ng_tactics helm-ng_library" version="0.0.1" archive(byte)="grafite_engine.cma" archive(native)="grafite_engine.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index 361d79610..43503fe26 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -26,7 +26,6 @@ MODULES = \ ng_kernel \ acic_content \ grafite \ - cic_unification \ disambiguation \ ng_kernel \ ng_refiner \ diff --git a/matita/components/cic_unification/.depend b/matita/components/cic_unification/.depend deleted file mode 100644 index 2e054f73d..000000000 --- a/matita/components/cic_unification/.depend +++ /dev/null @@ -1,23 +0,0 @@ -cicMetaSubst.cmi: -cicMkImplicit.cmi: -termUtil.cmi: -coercGraph.cmi: -cicUnification.cmi: -cicReplace.cmi: -cicRefine.cmi: -cicMetaSubst.cmo: cicMetaSubst.cmi -cicMetaSubst.cmx: cicMetaSubst.cmi -cicMkImplicit.cmo: cicMkImplicit.cmi -cicMkImplicit.cmx: cicMkImplicit.cmi -termUtil.cmo: cicMkImplicit.cmi termUtil.cmi -termUtil.cmx: cicMkImplicit.cmx termUtil.cmi -coercGraph.cmo: termUtil.cmi cicMkImplicit.cmi coercGraph.cmi -coercGraph.cmx: termUtil.cmx cicMkImplicit.cmx coercGraph.cmi -cicUnification.cmo: coercGraph.cmi cicMetaSubst.cmi cicUnification.cmi -cicUnification.cmx: coercGraph.cmx cicMetaSubst.cmx cicUnification.cmi -cicReplace.cmo: cicReplace.cmi -cicReplace.cmx: cicReplace.cmi -cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicReplace.cmi \ - cicMkImplicit.cmi cicMetaSubst.cmi cicRefine.cmi -cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicReplace.cmx \ - cicMkImplicit.cmx cicMetaSubst.cmx cicRefine.cmi diff --git a/matita/components/cic_unification/.depend.opt b/matita/components/cic_unification/.depend.opt deleted file mode 100644 index 2e054f73d..000000000 --- a/matita/components/cic_unification/.depend.opt +++ /dev/null @@ -1,23 +0,0 @@ -cicMetaSubst.cmi: -cicMkImplicit.cmi: -termUtil.cmi: -coercGraph.cmi: -cicUnification.cmi: -cicReplace.cmi: -cicRefine.cmi: -cicMetaSubst.cmo: cicMetaSubst.cmi -cicMetaSubst.cmx: cicMetaSubst.cmi -cicMkImplicit.cmo: cicMkImplicit.cmi -cicMkImplicit.cmx: cicMkImplicit.cmi -termUtil.cmo: cicMkImplicit.cmi termUtil.cmi -termUtil.cmx: cicMkImplicit.cmx termUtil.cmi -coercGraph.cmo: termUtil.cmi cicMkImplicit.cmi coercGraph.cmi -coercGraph.cmx: termUtil.cmx cicMkImplicit.cmx coercGraph.cmi -cicUnification.cmo: coercGraph.cmi cicMetaSubst.cmi cicUnification.cmi -cicUnification.cmx: coercGraph.cmx cicMetaSubst.cmx cicUnification.cmi -cicReplace.cmo: cicReplace.cmi -cicReplace.cmx: cicReplace.cmi -cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicReplace.cmi \ - cicMkImplicit.cmi cicMetaSubst.cmi cicRefine.cmi -cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicReplace.cmx \ - cicMkImplicit.cmx cicMetaSubst.cmx cicRefine.cmi diff --git a/matita/components/cic_unification/Makefile b/matita/components/cic_unification/Makefile deleted file mode 100644 index ad87356d1..000000000 --- a/matita/components/cic_unification/Makefile +++ /dev/null @@ -1,16 +0,0 @@ -PACKAGE = cic_unification -PREDICATES = - -INTERFACE_FILES = \ - cicMetaSubst.mli \ - cicMkImplicit.mli \ - termUtil.mli \ - coercGraph.mli \ - cicUnification.mli \ - cicReplace.mli \ - cicRefine.mli -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/cic_unification/cicMetaSubst.ml b/matita/components/cic_unification/cicMetaSubst.ml deleted file mode 100644 index 8db1cf82f..000000000 --- a/matita/components/cic_unification/cicMetaSubst.ml +++ /dev/null @@ -1,941 +0,0 @@ -(* Copyright (C) 2003, 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 - -(* PROFILING *) -(* -let deref_counter = ref 0 -let apply_subst_context_counter = ref 0 -let apply_subst_metasenv_counter = ref 0 -let lift_counter = ref 0 -let subst_counter = ref 0 -let whd_counter = ref 0 -let are_convertible_counter = ref 0 -let metasenv_length = ref 0 -let context_length = ref 0 -let reset_counters () = - apply_subst_counter := 0; - apply_subst_context_counter := 0; - apply_subst_metasenv_counter := 0; - lift_counter := 0; - subst_counter := 0; - whd_counter := 0; - are_convertible_counter := 0; - metasenv_length := 0; - context_length := 0 -let print_counters () = - debug_print (lazy (Printf.sprintf -"apply_subst: %d -apply_subst_context: %d -apply_subst_metasenv: %d -lift: %d -subst: %d -whd: %d -are_convertible: %d -metasenv length: %d (avg = %.2f) -context length: %d (avg = %.2f) -" - !apply_subst_counter !apply_subst_context_counter - !apply_subst_metasenv_counter !lift_counter !subst_counter !whd_counter - !are_convertible_counter !metasenv_length - ((float !metasenv_length) /. (float !apply_subst_metasenv_counter)) - !context_length - ((float !context_length) /. (float !apply_subst_context_counter)) - ))*) - - - -exception MetaSubstFailure of string Lazy.t -exception Uncertain of string Lazy.t -exception AssertFailure of string Lazy.t -exception DeliftingARelWouldCaptureAFreeVariable;; - -let debug_print = fun _ -> () - -type substitution = (int * (Cic.context * Cic.term)) list - -(* -let rec deref subst = - let third _,_,a = a in - function - Cic.Meta(n,l) as t -> - (try - deref subst - (CicSubstitution.subst_meta - l (third (CicUtil.lookup_subst n subst))) - with - CicUtil.Subst_not_found _ -> t) - | t -> t -;; -*) - -let lookup_subst = CicUtil.lookup_subst -;; - -(* clean_up_meta take a metasenv and a term and make every local context -of each occurrence of a metavariable consistent with its canonical context, -with respect to the hidden hipothesis *) - -(* -let clean_up_meta subst metasenv t = - let module C = Cic in - let rec aux t = - match t with - C.Rel _ - | C.Sort _ -> t - | C.Implicit _ -> assert false - | C.Meta (n,l) as t -> - let cc = - (try - let (cc,_) = lookup_subst n subst in cc - with CicUtil.Subst_not_found _ -> - try - let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc - with CicUtil.Meta_not_found _ -> assert false) in - let l' = - (try - List.map2 - (fun t1 t2 -> - match t1,t2 with - None , _ -> None - | _ , t -> t) cc l - with - Invalid_argument _ -> assert false) in - C.Meta (n, l') - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest) - | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest) - | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest) - | C.Appl l -> C.Appl (List.map aux l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Const (uri, exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.MutInd (uri, tyno, exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst - in - C.MutConstruct (uri, tyno, consno, exp_named_subst') - | C.MutCase (uri,tyno,out,te,pl) -> - C.MutCase (uri, tyno, aux out, aux te, List.map aux pl) - | C.Fix (i,fl) -> - let fl' = - List.map - (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i,fl) -> - let fl' = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl - in - C.CoFix (i, fl') - in - aux t *) - -(*** Functions to apply a substitution ***) - -let apply_subst_gen ~appl_fun subst term = - let rec um_aux = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Meta (i, l) -> - (try - let (_, t,_) = lookup_subst i subst in - um_aux (S.subst_meta l t) - with CicUtil.Subst_not_found _ -> - (* unconstrained variable, i.e. free in subst*) - let l' = - List.map (function None -> None | Some t -> Some (um_aux t)) l - in - C.Meta (i,l')) - | C.Sort _ - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) - | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t) - | C.Appl (hd :: tl) -> appl_fun um_aux hd tl - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.MutInd (uri,typeno,exp_named_subst') - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst - in - C.MutConstruct (uri,typeno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - let pl' = List.map um_aux pl in - C.MutCase (sp, i, um_aux outty, um_aux t, pl') - | C.Fix (i, fl) -> - let fl' = - List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i, fl) -> - let fl' = - List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl - in - C.CoFix (i, fl') - in - um_aux term -;; - -let apply_subst = - let appl_fun um_aux he tl = - let tl' = List.map um_aux tl in - let t' = - match um_aux he with - Cic.Appl l -> Cic.Appl (l@tl') - | he' -> Cic.Appl (he'::tl') - in - begin - match he with - Cic.Meta (m,_) -> CicReduction.head_beta_reduce t' - | _ -> t' - end - in - fun subst t -> -(* incr apply_subst_counter; *) -match subst with - [] -> t - | _ -> apply_subst_gen ~appl_fun subst t -;; - -let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst" -let apply_subst s t = - profiler.HExtlib.profile (apply_subst s) t - - -let apply_subst_context subst context = - match subst with - [] -> context - | _ -> -(* - incr apply_subst_context_counter; - context_length := !context_length + List.length context; -*) - List.fold_right - (fun item context -> - match item with - | Some (n, Cic.Decl t) -> - let t' = apply_subst subst t in - Some (n, Cic.Decl t') :: context - | Some (n, Cic.Def (t, ty)) -> - let ty' = apply_subst subst ty in - let t' = apply_subst subst t in - Some (n, Cic.Def (t', ty')) :: context - | None -> None :: context) - context [] - -let apply_subst_metasenv subst metasenv = -(* - incr apply_subst_metasenv_counter; - metasenv_length := !metasenv_length + List.length metasenv; -*) -match subst with - [] -> metasenv - | _ -> - List.map - (fun (n, context, ty) -> - (n, apply_subst_context subst context, apply_subst subst ty)) - (List.filter - (fun (i, _, _) -> not (List.mem_assoc i subst)) - metasenv) - -(***** Pretty printing functions ******) - -let ppterm ~metasenv subst term = - CicPp.ppterm ~metasenv (apply_subst subst term) - -let ppterm_in_context ~metasenv subst term context = - let name_context = - List.map (function None -> None | Some (n,_) -> Some n) context - in - CicPp.pp ~metasenv (apply_subst subst term) name_context - -let ppterm_in_context_ref = ref ppterm_in_context -let set_ppterm_in_context f = - ppterm_in_context_ref := f -let use_low_level_ppterm_in_context = ref false - -let ppterm_in_context ~metasenv subst term context = - if !use_low_level_ppterm_in_context then - ppterm_in_context ~metasenv subst term context - else - !ppterm_in_context_ref ~metasenv subst term context - -let ppcontext' ~metasenv ?(sep = "\n") subst context = - let separate s = if s = "" then "" else s ^ sep in - List.fold_right - (fun context_entry (i,context) -> - match context_entry with - Some (n,Cic.Decl t) -> - sprintf "%s%s : %s" (separate i) (CicPp.ppname n) - (ppterm_in_context ~metasenv subst t context), - context_entry::context - | Some (n,Cic.Def (bo,ty)) -> - sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) - (ppterm_in_context ~metasenv subst ty context) - (ppterm_in_context ~metasenv subst bo context), - context_entry::context - | None -> - sprintf "%s_ :? _" (separate i), context_entry::context - ) context ("",[]) - -let ppsubst_unfolded ~metasenv subst = - String.concat "\n" - (List.map - (fun (idx, (c, t,ty)) -> - let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in - sprintf "%s |- ?%d : %s := %s" scontext idx -(ppterm_in_context ~metasenv [] ty context) - (ppterm_in_context ~metasenv subst t context)) - subst) -(* - Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) - subst) *) -;; - -let ppsubst ~metasenv subst = - String.concat "\n" - (List.map - (fun (idx, (c, t, ty)) -> - let scontext,context = ppcontext' ~metasenv ~sep:"; " [] c in - sprintf "%s |- ?%d : %s := %s" scontext idx (ppterm_in_context ~metasenv [] ty context) - (ppterm_in_context ~metasenv [] t context)) - subst) -;; - -let ppcontext ~metasenv ?sep subst context = - fst (ppcontext' ~metasenv ?sep subst context) - -let ppmetasenv ?(sep = "\n") subst metasenv = - String.concat sep - (List.map - (fun (i, c, t) -> - let scontext,context = ppcontext' ~metasenv ~sep:"; " subst c in - sprintf "%s |- ?%d: %s" scontext i - (ppterm_in_context ~metasenv subst t context)) - (List.filter - (fun (i, _, _) -> not (List.mem_assoc i subst)) - metasenv)) - -let tempi_type_of_aux_subst = ref 0.0;; -let tempi_subst = ref 0.0;; -let tempi_type_of_aux = ref 0.0;; - -(**** DELIFT ****) -(* the delift function takes in input a metavariable index, an ordered list of - * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some - * (rel(nk)) with rel(k). Typically, the list of optional terms is the explicit - * substitution that is applied to a metavariable occurrence and the result of - * the delift function is a term the implicit variable can be substituted with - * to make the term [t] unifiable with the metavariable occurrence. In general, - * the problem is undecidable if we consider equivalence in place of alpha - * convertibility. Our implementation, though, is even weaker than alpha - * convertibility, since it replace the term [tk] if and only if [tk] is a Rel - * (missing all the other cases). Does this matter in practice? - * The metavariable index is the index of the metavariable that must not occur - * in the term (for occur check). - *) - -exception NotInTheList;; - -let position n = - let rec aux k = - function - [] -> raise NotInTheList - | (Some (Cic.Rel m))::_ when m=n -> k - | _::tl -> aux (k+1) tl in - aux 1 -;; - -exception Occur;; - -let rec force_does_not_occur subst to_be_restricted t = - let module C = Cic in - let more_to_be_restricted = ref [] in - let rec aux k = function - C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur - | C.Rel _ - | C.Sort _ as t -> t - | C.Implicit _ -> assert false - | C.Meta (n, l) -> - (* we do not retrieve the term associated to ?n in subst since *) - (* in this way we can restrict if something goes wrong *) - let l' = - let i = ref 0 in - List.map - (function t -> - incr i ; - match t with - None -> None - | Some t -> - try - Some (aux k t) - with Occur -> - more_to_be_restricted := (n,!i) :: !more_to_be_restricted; - None) - l - in - C.Meta (n, l') - | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) - | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest) - | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest) - | C.LetIn (name,so,ty,dest) -> - C.LetIn (name, aux k so, aux k ty, aux (k+1) dest) - | C.Appl l -> C.Appl (List.map (aux k) l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Const (uri, exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.MutInd (uri, tyno, exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.MutConstruct (uri, tyno, consno, exp_named_subst') - | C.MutCase (uri,tyno,out,te,pl) -> - C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl) - | C.Fix (i,fl) -> - let len = List.length fl in - let k_plus_len = k + len in - let fl' = - List.map - (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i,fl) -> - let len = List.length fl in - let k_plus_len = k + len in - let fl' = - List.map - (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl - in - C.CoFix (i, fl') - in - let res = aux 0 t in - (!more_to_be_restricted, res) - -let rec restrict subst to_be_restricted metasenv = - match to_be_restricted with - | [] -> metasenv, subst - | _ -> - let names_of_context_indexes context indexes = - String.concat ", " - (List.map - (fun i -> - try - match List.nth context (i-1) with - | None -> assert false - | Some (n, _) -> CicPp.ppname n - with - Failure _ -> assert false - ) indexes) - in - let force_does_not_occur_in_context to_be_restricted = function - | None -> [], None - | Some (name, Cic.Decl t) -> - let (more_to_be_restricted, t') = - force_does_not_occur subst to_be_restricted t - in - more_to_be_restricted, Some (name, Cic.Decl t') - | Some (name, Cic.Def (bo, ty)) -> - let (more_to_be_restricted, bo') = - force_does_not_occur subst to_be_restricted bo - in - let more_to_be_restricted, ty' = - let more_to_be_restricted', ty' = - force_does_not_occur subst to_be_restricted ty - in - more_to_be_restricted @ more_to_be_restricted', - ty' - in - more_to_be_restricted, Some (name, Cic.Def (bo', ty')) - in - let rec erase i to_be_restricted n = function - | [] -> [], to_be_restricted, [] - | hd::tl -> - let more_to_be_restricted,restricted,tl' = - erase (i+1) to_be_restricted n tl - in - let restrict_me = List.mem i restricted in - if restrict_me then - more_to_be_restricted, restricted, None:: tl' - else - (try - let more_to_be_restricted', hd' = - let delifted_restricted = - let rec aux = - function - [] -> [] - | j::tl when j > i -> (j - i)::aux tl - | _::tl -> aux tl - in - aux restricted - in - force_does_not_occur_in_context delifted_restricted hd - in - more_to_be_restricted @ more_to_be_restricted', - restricted, hd' :: tl' - with Occur -> - more_to_be_restricted, (i :: restricted), None :: tl') - in - let (more_to_be_restricted, metasenv) = (* restrict metasenv *) - List.fold_right - (fun (n, context, t) (more, metasenv) -> - let to_be_restricted = - List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) - in - let (more_to_be_restricted, restricted, context') = - (* just an optimization *) - if to_be_restricted = [] then - [],[],context - else - erase 1 to_be_restricted n context - in - try - let more_to_be_restricted', t' = - force_does_not_occur subst restricted t - in - let metasenv' = (n, context', t') :: metasenv in - (more @ more_to_be_restricted @ more_to_be_restricted', - metasenv') - with Occur -> - raise (MetaSubstFailure (lazy (sprintf - "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" - n (names_of_context_indexes context to_be_restricted))))) - metasenv ([], []) - in - let (more_to_be_restricted', subst) = (* restrict subst *) - List.fold_right - (* TODO: cambiare dopo l'aggiunta del ty *) - (fun (n, (context, term,ty)) (more, subst') -> - let to_be_restricted = - List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) - in - (try - let (more_to_be_restricted, restricted, context') = - (* just an optimization *) - if to_be_restricted = [] then - [], [], context - else - erase 1 to_be_restricted n context - in - let more_to_be_restricted', term' = - force_does_not_occur subst restricted term - in - let more_to_be_restricted'', ty' = - force_does_not_occur subst restricted ty in - let subst' = (n, (context', term',ty')) :: subst' in - let more = - more @ more_to_be_restricted - @ more_to_be_restricted'@more_to_be_restricted'' in - (more, subst') - with Occur -> - let error_msg = lazy (sprintf - "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" - n (names_of_context_indexes context to_be_restricted) n - (ppterm ~metasenv subst term)) - in - (* DEBUG - debug_print (lazy error_msg); - debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst))); - debug_print (lazy ("subst = \n" ^ (ppsubst subst))); - debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *) - raise (MetaSubstFailure error_msg))) - subst ([], []) - in - restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv -;; - -(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*) - -let delift n subst context metasenv l t = -(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), - otherwise the occur check does not make sense *) - -(* - debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto - al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))))); -*) - - let module S = CicSubstitution in - let l = - let (_, canonical_context, _) = - try - CicUtil.lookup_meta n metasenv - with CicUtil.Meta_not_found _ -> - raise (MetaSubstFailure (lazy - ("delifting error: the metavariable " ^ string_of_int n ^ " is not " ^ - "declared in the metasenv"))) - in - List.map2 (fun ct lt -> - match (ct, lt) with - | None, _ -> None - | Some _, _ -> lt) - canonical_context l - in - let to_be_restricted = ref [] in - let rec deliftaux k = - let module C = Cic in - function - | C.Rel m as t-> - if m <=k then - t - else - (try - match List.nth context (m-k-1) with - Some (_,C.Def (t,_)) -> - (try - C.Rel ((position (m-k) l) + k) - with - NotInTheList -> - (*CSC: Hmmm. This bit of reduction is not in the spirit of *) - (*CSC: first order unification. Does it help or does it harm? *) - (*CSC: ANSWER: it hurts performances since it is possible to *) - (*CSC: have an exponential explosion of the size of the proof.*) - (*CSC: However, without this bit of reduction some "apply" in *) - (*CSC: the library fail (e.g. nat/nth_prime.ma). *) - deliftaux k (S.lift m t)) - | Some (_,C.Decl t) -> - C.Rel ((position (m-k) l) + k) - | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) - with - Failure _ -> - raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) - ) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l1) as t -> - (try - let (_,t,_) = CicUtil.lookup_subst i subst in - deliftaux k (CicSubstitution.subst_meta l1 t) - with CicUtil.Subst_not_found _ -> - (* see the top level invariant *) - if (i = n) then - raise (MetaSubstFailure (lazy (sprintf - "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" - i (ppterm ~metasenv subst t)))) - else - begin - (* I do not consider the term associated to ?i in subst since *) - (* in this way I can restrict if something goes wrong. *) - let rec deliftl j = - function - [] -> [] - | None::tl -> None::(deliftl (j+1) tl) - | (Some t)::tl -> - let l1' = (deliftl (j+1) tl) in - try - Some (deliftaux k t)::l1' - with - NotInTheList - | MetaSubstFailure _ -> - to_be_restricted := - (i,j)::!to_be_restricted ; None::l1' - in - let l' = deliftl 1 l1 in - C.Meta(i,l') - end) - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) - | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) - | C.LetIn (n,s,ty,t) -> - C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t) - | C.Appl l -> C.Appl (List.map (deliftaux k) l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.MutInd (uri,typeno,exp_named_subst') - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.MutConstruct (uri,typeno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, i, deliftaux k outty, deliftaux k t, - List.map (deliftaux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> - (name, i, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) - in - let res = - try - deliftaux 0 t - with - NotInTheList -> - (* This is the case where we fail even first order unification. *) - (* The reason is that our delift function is weaker than first *) - (* order (in the sense of alpha-conversion). See comment above *) - (* related to the delift function. *) -(* debug_print (lazy "First Order UnificationFailure during delift") ; -debug_print(lazy (sprintf - "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm subst t) - (String.concat "; " - (List.map - (function Some t -> ppterm subst t | None -> "_") l - )))); *) - let msg = (lazy (sprintf - "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm ~metasenv subst t) - (String.concat "; " - (List.map - (function Some t -> ppterm ~metasenv subst t | None -> "_") - l)))) - in - if - List.exists - (function - Some t -> CicUtil.is_meta_closed (apply_subst subst t) - | None -> true) l - then - raise (Uncertain msg) - else - raise (MetaSubstFailure msg) - in - let (metasenv, subst) = restrict subst !to_be_restricted metasenv in - res, metasenv, subst -;; - -(* delifts a term t of n levels strating from k, that is changes (Rel m) - * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails - *) -let delift_rels_from subst metasenv k n = - let rec liftaux subst metasenv k = - let module C = Cic in - function - C.Rel m as t -> - if m < k then - t, subst, metasenv - else if m < k + n then - raise DeliftingARelWouldCaptureAFreeVariable - else - C.Rel (m - n), subst, metasenv - | C.Var (uri,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.Var (uri,exp_named_subst'),subst,metasenv - | C.Meta (i,l) -> - (try - let (_, t,_) = lookup_subst i subst in - liftaux subst metasenv k (CicSubstitution.subst_meta l t) - with CicUtil.Subst_not_found _ -> - let l',to_be_restricted,subst,metasenv = - let rec aux con l subst metasenv = - match l with - [] -> [],[],subst,metasenv - | he::tl -> - let tl',to_be_restricted,subst,metasenv = - aux (con + 1) tl subst metasenv in - let he',more_to_be_restricted,subst,metasenv = - match he with - None -> None,[],subst,metasenv - | Some t -> - try - let t',subst,metasenv = liftaux subst metasenv k t in - Some t',[],subst,metasenv - with - DeliftingARelWouldCaptureAFreeVariable -> - None,[i,con],subst,metasenv - in - he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv - in - aux 1 l subst metasenv in - let metasenv,subst = restrict subst to_be_restricted metasenv in - C.Meta(i,l'),subst,metasenv) - | C.Sort _ as t -> t,subst,metasenv - | C.Implicit _ as t -> t,subst,metasenv - | C.Cast (te,ty) -> - let te',subst,metasenv = liftaux subst metasenv k te in - let ty',subst,metasenv = liftaux subst metasenv k ty in - C.Cast (te',ty'),subst,metasenv - | C.Prod (n,s,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.Prod (n,s',t'),subst,metasenv - | C.Lambda (n,s,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.Lambda (n,s',t'),subst,metasenv - | C.LetIn (n,s,ty,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let ty',subst,metasenv = liftaux subst metasenv k ty in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.LetIn (n,s',ty',t'),subst,metasenv - | C.Appl l -> - let l',subst,metasenv = - List.fold_right - (fun t (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - t'::l,subst,metasenv) l ([],subst,metasenv) in - C.Appl l',subst,metasenv - | C.Const (uri,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.Const (uri,exp_named_subst'),subst,metasenv - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv - | C.MutCase (sp,i,outty,t,pl) -> - let outty',subst,metasenv = liftaux subst metasenv k outty in - let t',subst,metasenv = liftaux subst metasenv k t in - let pl',subst,metasenv = - List.fold_right - (fun t (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - t'::l,subst,metasenv) pl ([],subst,metasenv) - in - C.MutCase (sp,i,outty',t',pl'),subst,metasenv - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl,subst,metasenv = - List.fold_right - (fun (name, i, ty, bo) (l,subst,metasenv) -> - let ty',subst,metasenv = liftaux subst metasenv k ty in - let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in - (name,i,ty',bo')::l,subst,metasenv - ) fl ([],subst,metasenv) - in - C.Fix (i, liftedfl),subst,metasenv - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl,subst,metasenv = - List.fold_right - (fun (name, ty, bo) (l,subst,metasenv) -> - let ty',subst,metasenv = liftaux subst metasenv k ty in - let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in - (name,ty',bo')::l,subst,metasenv - ) fl ([],subst,metasenv) - in - C.CoFix (i, liftedfl),subst,metasenv - in - liftaux subst metasenv k - -let delift_rels subst metasenv n t = - delift_rels_from subst metasenv 1 n t - - -(**** END OF DELIFT ****) - - -(** {2 Format-like pretty printers} *) - -let fpp_gen ppf s = - Format.pp_print_string ppf s; - Format.pp_print_newline ppf (); - Format.pp_print_flush ppf () - -let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst) -let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) -let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv) diff --git a/matita/components/cic_unification/cicMetaSubst.mli b/matita/components/cic_unification/cicMetaSubst.mli deleted file mode 100644 index 0d2a08d55..000000000 --- a/matita/components/cic_unification/cicMetaSubst.mli +++ /dev/null @@ -1,96 +0,0 @@ -(* Copyright (C) 2004, 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://helm.cs.unibo.it/ - *) - -exception MetaSubstFailure of string Lazy.t -exception Uncertain of string Lazy.t -exception AssertFailure of string Lazy.t -exception DeliftingARelWouldCaptureAFreeVariable;; - -(* The entry (i,t) in a substitution means that *) -(* (META i) have been instantiated with t. *) -(* type substitution = (int * (Cic.context * Cic.term)) list *) - - (** @raise SubstNotFound *) - -(* apply_subst subst t *) -(* applies the substitution [subst] to [t] *) -(* [subst] must be already unwinded *) - -val apply_subst : Cic.substitution -> Cic.term -> Cic.term -val apply_subst_context : Cic.substitution -> Cic.context -> Cic.context -val apply_subst_metasenv: Cic.substitution -> Cic.metasenv -> Cic.metasenv - -(*** delifting ***) - -val delift : - int -> Cic.substitution -> Cic.context -> Cic.metasenv -> - (Cic.term option) list -> Cic.term -> - Cic.term * Cic.metasenv * Cic.substitution -val restrict : - Cic.substitution -> (int * int) list -> Cic.metasenv -> - Cic.metasenv * Cic.substitution - -(** delifts the Rels in t of n - * @raise DeliftingARelWouldCaptureAFreeVariable - *) -val delift_rels : - Cic.substitution -> Cic.metasenv -> int -> Cic.term -> - Cic.term * Cic.substitution * Cic.metasenv - -(** {2 Pretty printers} *) -val use_low_level_ppterm_in_context : bool ref -val set_ppterm_in_context : - (metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> - string) -> unit - -val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string -val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string -val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string -val ppcontext: - metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context -> - string -val ppterm_in_context: - metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string -val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string - -(** {2 Format-like pretty printers} - * As above with prototypes suitable for toplevel/ocamldebug printers. No - * subsitutions are applied here since such printers are required to be invoked - * with only one argument. - *) - -val fppsubst: Format.formatter -> Cic.substitution -> unit -val fppterm: Format.formatter -> Cic.term -> unit -val fppmetasenv: Format.formatter -> Cic.metasenv -> unit - -(* -(* DEBUG *) -val print_counters: unit -> unit -val reset_counters: unit -> unit -*) - -(* val clean_up_meta : - Cic.substitution -> Cic.metasenv -> Cic.term -> Cic.term -*) diff --git a/matita/components/cic_unification/cicMkImplicit.ml b/matita/components/cic_unification/cicMkImplicit.ml deleted file mode 100644 index 36679223c..000000000 --- a/matita/components/cic_unification/cicMkImplicit.ml +++ /dev/null @@ -1,122 +0,0 @@ -(* Copyright (C) 2004, 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$ *) - -(* identity_relocation_list_for_metavariable i canonical_context *) -(* returns the identity relocation list, which is the list [1 ; ... ; n] *) -(* where n = List.length [canonical_context] *) -(*CSC: ma mi basta la lunghezza del contesto canonico!!!*) -let identity_relocation_list_for_metavariable ?(start = 1) canonical_context = - let rec aux = - function - (_,[]) -> [] - | (n,None::tl) -> None::(aux ((n+1),tl)) - | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) - in - aux (start,canonical_context) - -(* Returns the first meta whose number is above the *) -(* number of the higher meta. *) -let new_meta metasenv subst = - let rec aux = - function - None, [] -> 1 - | Some n, [] -> n - | None, n::tl -> aux (Some n,tl) - | Some m, n::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) - in - let indexes = - (List.map (fun (i, _, _) -> i) metasenv) @ (List.map fst subst) - in - 1 + aux (None, indexes) - -(* let apply_subst_context = CicMetaSubst.apply_subst_context;; *) -(* questa o la precedente sembrano essere equivalenti come tempi *) -let apply_subst_context _ context = context ;; - -let mk_implicit metasenv subst context = - let newmeta = new_meta metasenv subst in - let newuniv = CicUniv.fresh () in - let irl = identity_relocation_list_for_metavariable context in - (* in the following mk_* functions we apply substitution to canonical - * context since we have the invariant that the metasenv has already been - * instantiated with subst *) - let context = apply_subst_context subst context in - ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ; - (* TASSI: ?? *) - newmeta + 1, context, Cic.Meta (newmeta, []); - newmeta + 2, context, Cic.Meta (newmeta + 1,irl) ] @ metasenv, - newmeta + 2) - -let mk_implicit_type metasenv subst context = - let newmeta = new_meta metasenv subst in - let newuniv = CicUniv.fresh () in - let context = apply_subst_context subst context in - ([ newmeta, [], Cic.Sort (Cic.Type newuniv); - (* TASSI: ?? *) - newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv, - newmeta + 1) - -let mk_implicit_sort metasenv subst = - let newmeta = new_meta metasenv subst in - let newuniv = CicUniv.fresh () in - ([ newmeta, [], Cic.Sort (Cic.Type newuniv)] @ metasenv, newmeta) - (* TASSI: ?? *) - -let n_fresh_metas metasenv subst context n = - if n = 0 then metasenv, [] - else - let irl = identity_relocation_list_for_metavariable context in - let context = apply_subst_context subst context in - let newmeta = new_meta metasenv subst in - let newuniv = CicUniv.fresh () in - let rec aux newmeta n = - if n = 0 then metasenv, [] - else - let metasenv', l = aux (newmeta + 3) (n-1) in - (* TASSI: ?? *) - (newmeta, context, Cic.Sort (Cic.Type newuniv)):: - (newmeta + 1, context, Cic.Meta (newmeta, irl)):: - (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', - Cic.Meta(newmeta+2,irl)::l in - aux newmeta n - -let fresh_subst metasenv subst context uris = - let irl = identity_relocation_list_for_metavariable context in - let context = apply_subst_context subst context in - let newmeta = new_meta metasenv subst in - let newuniv = CicUniv.fresh () in - let rec aux newmeta = function - [] -> metasenv, [] - | uri::tl -> - let metasenv', l = aux (newmeta + 3) tl in - (* TASSI: ?? *) - (newmeta, context, Cic.Sort (Cic.Type newuniv)):: - (newmeta + 1, context, Cic.Meta (newmeta, irl)):: - (newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv', - (uri,Cic.Meta(newmeta+2,irl))::l in - aux newmeta uris - diff --git a/matita/components/cic_unification/cicMkImplicit.mli b/matita/components/cic_unification/cicMkImplicit.mli deleted file mode 100644 index 476270144..000000000 --- a/matita/components/cic_unification/cicMkImplicit.mli +++ /dev/null @@ -1,60 +0,0 @@ -(* Copyright (C) 2004, 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://helm.cs.unibo.it/ - *) - - -(* identity_relocation_list_for_metavariable i canonical_context *) -(* returns the identity relocation list, which is the list *) -(* [Rel 1 ; ... ; Rel n] where n = List.length [canonical_context] *) -val identity_relocation_list_for_metavariable : - ?start: int -> 'a option list -> Cic.term option list - -(* Returns the first meta whose number is above the *) -(* number of the higher meta. *) -val new_meta : Cic.metasenv -> Cic.substitution -> int - -(** [mk_implicit metasenv context] - * add a fresh metavariable to the given metasenv, using given context - * @return the new metasenv and the index of the added conjecture *) -val mk_implicit: Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.metasenv * int - -(** as above, but the fresh metavariable represents a type *) -val mk_implicit_type: Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.metasenv * int - -(** as above, but the fresh metavariable represents a sort *) -val mk_implicit_sort: Cic.metasenv -> Cic.substitution -> Cic.metasenv * int - -(** [mk_implicit metasenv context] create n fresh metavariables *) -val n_fresh_metas: - Cic.metasenv -> Cic.substitution -> Cic.context -> int -> Cic.metasenv * Cic.term list - -(** [fresh_subst metasenv context uris] takes in input a list of uri and -creates a fresh explicit substitution *) -val fresh_subst: - Cic.metasenv -> - Cic.substitution -> - Cic.context -> - UriManager.uri list -> - Cic.metasenv * (Cic.term Cic.explicit_named_substitution) - diff --git a/matita/components/cic_unification/cicRefine.ml b/matita/components/cic_unification/cicRefine.ml deleted file mode 100644 index b535b9ebe..000000000 --- a/matita/components/cic_unification/cicRefine.ml +++ /dev/null @@ -1,2283 +0,0 @@ -(* 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 - -exception RefineFailure of string Lazy.t;; -exception Uncertain of string Lazy.t;; -exception AssertFailure of string Lazy.t;; - -(* for internal use only; the integer is the number of surplus arguments *) -exception MoreArgsThanExpected of int * exn;; - -let insert_coercions = ref true -let pack_coercions = ref true - -let debug = false;; - -let debug_print = - if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());; - -let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" - -let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph = - try -let foo () = - CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph -in profiler_eat_prods2.HExtlib.profile foo () - with - (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) - | (CicUnification.Uncertain msg) -> raise (Uncertain msg) -;; - -let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods" - -let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph = - try -let foo () = - CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph -in profiler_eat_prods.HExtlib.profile foo () - with - (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) - | (CicUnification.Uncertain msg) -> raise (Uncertain msg) -;; - -let profiler = HExtlib.profile "CicRefine.fo_unif" - -let fo_unif_subst subst context metasenv t1 t2 ugraph = - try -let foo () = - CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph -in profiler.HExtlib.profile foo () - with - (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) - | (CicUnification.Uncertain msg) -> raise (Uncertain msg) -;; - -let enrich localization_tbl t ?(f = fun msg -> msg) exn = - let exn' = - match exn with - RefineFailure msg -> RefineFailure (f msg) - | Uncertain msg -> Uncertain (f msg) - | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg) - | Sys.Break -> raise exn - | _ -> prerr_endline (Printexc.to_string exn); assert false - in - let loc = - try - Cic.CicHash.find localization_tbl t - with Not_found -> - HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); - raise exn' - in - raise (HExtlib.Localized (loc,exn')) - -let relocalize localization_tbl oldt newt = - try - let infos = Cic.CicHash.find localization_tbl oldt in - Cic.CicHash.remove localization_tbl oldt; - Cic.CicHash.add localization_tbl newt infos; - with - Not_found -> () -;; - -let rec split l n = - match (l,n) with - (l,0) -> ([], l) - | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) - | (_,_) -> raise (AssertFailure (lazy "split: list too short")) -;; - -let exp_impl metasenv subst context = - function - | Some `Type -> - let (metasenv', idx) = - CicMkImplicit.mk_implicit_type metasenv subst context in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (idx, irl) - | Some `Closed -> - let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in - metasenv', Cic.Meta (idx, []) - | None -> - let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in - metasenv', Cic.Meta (idx, irl) - | _ -> assert false -;; - -let unvariant newt = - match newt with - | Cic.Appl (hd::args) -> - let uri = CicUtil.uri_of_term hd in - (match - CicEnvironment.get_obj CicUniv.oblivion_ugraph uri - with - | Cic.Constant (_,Some t,_,[],attrs),_ - when List.exists ((=) (`Flavour `Variant)) attrs -> - Cic.Appl (t::args) - | _ -> newt) - | _ -> newt -;; - -let is_a_double_coercion t = - let rec subst_nth n x l = - match n,l with - | _, [] -> [] - | 0, _::tl -> x :: tl - | n, hd::tl -> hd :: subst_nth (n-1) x tl - in - let imp = Cic.Implicit None in - let dummyres = false,imp, imp,imp,imp in - match t with - | Cic.Appl l1 -> - (match CoercGraph.coerced_arg l1 with - | Some (Cic.Appl l2, pos1) -> - (match CoercGraph.coerced_arg l2 with - | Some (x, pos2) -> - true, List.hd l1, List.hd l2, x, - Cic.Appl (subst_nth (pos1 + 1) - (Cic.Appl (subst_nth (pos2+1) imp l2)) l1) - | _ -> dummyres) - | _ -> dummyres) - | _ -> dummyres -;; - -let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn -= - let len = List.length tlbody_and_type in - let msg = - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ - " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^ - ") is here applied to " ^ string_of_int len ^ - " arguments but here it can handle only up to " ^ - string_of_int (len - residuals) ^ " arguments") - in - enrich localization_tbl he ~f:(fun _-> msg) exn -;; - -let mk_prod_of_metas metasenv context subst args = - let rec mk_prod metasenv context' = function - | [] -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - metasenv,Cic.Meta (idx, irl) - | (_,argty)::tl -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - let meta = Cic.Meta (idx,irl) in - let name = - (* The name must be fresh for context. *) - (* Nevertheless, argty is well-typed only in context. *) - (* Thus I generate a name (name_hint) in context and *) - (* then I generate a name --- using the hint name_hint *) - (* --- that is fresh in context'. *) - let name_hint = - FreshNamesGenerator.mk_fresh_name ~subst metasenv - (CicMetaSubst.apply_subst_context subst context) - Cic.Anonymous - ~typ:(CicMetaSubst.apply_subst subst argty) - in - FreshNamesGenerator.mk_fresh_name ~subst - [] context' name_hint ~typ:(Cic.Sort Cic.Prop) - in - let metasenv,target = - mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl - in - metasenv,Cic.Prod (name,meta,target) - in - mk_prod metasenv context args -;; - -let rec type_of_constant uri ugraph = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let _ = CicTypeChecker.typecheck uri in - let obj,u = - try - CicEnvironment.get_cooked_obj ugraph uri - with Not_found -> assert false - in - match obj with - C.Constant (_,_,ty,_,_) -> ty,u - | C.CurrentProof (_,_,_,ty,_,_) -> ty,u - | _ -> - raise - (RefineFailure - (lazy ("Unknown constant definition " ^ U.string_of_uri uri))) - -and type_of_variable uri ugraph = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let _ = CicTypeChecker.typecheck uri in - let obj,u = - try - CicEnvironment.get_cooked_obj ugraph uri - with Not_found -> assert false - in - match obj with - C.Variable (_,_,ty,_,_) -> ty,u - | _ -> - raise - (RefineFailure - (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri))) - -and type_of_mutual_inductive_defs uri i ugraph = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let _ = CicTypeChecker.typecheck uri in - let obj,u = - try - CicEnvironment.get_cooked_obj ugraph uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity,u - | _ -> - raise - (RefineFailure - (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri))) - -and type_of_mutual_inductive_constr uri i j ugraph = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - let _ = CicTypeChecker.typecheck uri in - let obj,u = - try - CicEnvironment.get_cooked_obj ugraph uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,_,cl) = List.nth dl i in - let (_,ty) = List.nth cl (j-1) in - ty,u - | _ -> - raise - (RefineFailure - (lazy - ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) - - -(* type_of_aux' is just another name (with a different scope) for type_of_aux *) - -(* the check_branch function checks if a branch of a case is refinable. - It returns a pair (outype_instance,args), a subst and a metasenv. - outype_instance is the expected result of applying the case outtype - to args. - The problem is that outype is in general unknown, and we should - try to synthesize it from the above information, that is in general - a second order unification problem. *) - -and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph = - let module C = Cic in - let module R = CicReduction in - match R.whd ~subst context expectedtype with - C.MutInd (_,_,_) -> - (n,context,actualtype, [term]), subst, metasenv, ugraph - | C.Appl (C.MutInd (_,_,_)::tl) -> - let (_,arguments) = split tl left_args_no in - (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph - | C.Prod (_,so,de) -> - (* we expect that the actual type of the branch has the due - number of Prod *) - (match R.whd ~subst context actualtype with - C.Prod (name',so',de') -> - let subst, metasenv, ugraph1 = - fo_unif_subst subst context metasenv so so' ugraph in - let term' = - (match CicSubstitution.lift 1 term with - C.Appl l -> C.Appl (l@[C.Rel 1]) - | t -> C.Appl [t ; C.Rel 1]) in - (* we should also check that the name variable is anonymous in - the actual type de' ?? *) - check_branch (n+1) - ((Some (name',(C.Decl so)))::context) - metasenv subst left_args_no de' term' de ugraph1 - | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) - | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) - -and type_of_aux' ?(clean_dummy_dependent_types=true) - ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph -= - let rec type_of_aux subst metasenv context t ugraph = - let module C = Cic in - let module S = CicSubstitution in - let module U = UriManager in - let (t',_,_,_,_) as res = - match t with - (* function *) - C.Rel n -> - (try - match List.nth context (n - 1) with - Some (_,C.Decl ty) -> - t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (_,ty)) -> - t,S.lift n ty,subst,metasenv, ugraph - | None -> - enrich localization_tbl t - (RefineFailure (lazy "Rel to hidden hypothesis")) - with - Failure _ -> - enrich localization_tbl t - (RefineFailure (lazy "Not a closed term"))) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst',subst',metasenv',ugraph1 = - check_exp_named_subst - subst metasenv context exp_named_subst ugraph - in - let ty_uri,ugraph1 = type_of_variable uri ugraph in - let ty = - CicSubstitution.subst_vars exp_named_subst' ty_uri - in - C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1 - | C.Meta (n,l) -> - (try - let (canonical_context, term,ty) = - CicUtil.lookup_subst n subst - in - let l',subst',metasenv',ugraph1 = - check_metasenv_consistency n subst metasenv context - canonical_context l ugraph - in - (* trust or check ??? *) - C.Meta (n,l'),CicSubstitution.subst_meta l' ty, - subst', metasenv', ugraph1 - (* type_of_aux subst metasenv - context (CicSubstitution.subst_meta l term) *) - with CicUtil.Subst_not_found _ -> - let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in - let l',subst',metasenv', ugraph1 = - check_metasenv_consistency n subst metasenv context - canonical_context l ugraph - in - C.Meta (n,l'),CicSubstitution.subst_meta l' ty, - subst', metasenv',ugraph1) - | C.Sort (C.Type tno) -> - let tno' = CicUniv.fresh() in - (try - let ugraph1 = CicUniv.add_gt tno' tno ugraph in - t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | C.Sort (C.CProp tno) -> - let tno' = CicUniv.fresh() in - (try - let ugraph1 = CicUniv.add_gt tno' tno ugraph in - t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | C.Sort (C.Prop|C.Set) -> - t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph - | C.Implicit infos -> - let metasenv',t' = exp_impl metasenv subst context infos in - type_of_aux subst metasenv' context t' ugraph - | C.Cast (te,ty) -> - let ty',_,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context ty ugraph - in - let te',inferredty,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' context te ugraph1 - in - let rec count_prods context ty = - match CicReduction.whd context ~subst:subst'' ty with - | Cic.Prod (n,s,t) -> - 1 + count_prods (Some (n,Cic.Decl s)::context) t - | _ -> 0 - in - let exp_prods = count_prods context ty' in - let inf_prods = count_prods context inferredty in - let te', inferredty, metasenv'', subst'', ugraph2 = - let rec aux t m s ug it = function - | 0 -> t,it,m,s,ug - | n -> - match CicReduction.whd context ~subst:s it with - | Cic.Prod (_,src,tgt) -> - let newmeta, metaty, s, m, ug = - type_of_aux s m context (Cic.Implicit None) ug - in - let s,m,ug = - fo_unif_subst s context m metaty src ug - in - let t = - match t with - | Cic.Appl l -> Cic.Appl (l @ [newmeta]) - | _ -> Cic.Appl [t;newmeta] - in - aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1) - | _ -> t,it,m,s,ug - in - aux te' metasenv'' subst'' ugraph2 inferredty - (max 0 (inf_prods - exp_prods)) - in - let (te', ty'), subst''',metasenv''',ugraph3 = - coerce_to_something true localization_tbl te' inferredty ty' - subst'' metasenv'' context ugraph2 - in - C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 - | C.Prod (name,s,t) -> - let s',sort1,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context s ugraph - in - let s',sort1,subst', metasenv',ugraph1 = - coerce_to_sort localization_tbl - s' sort1 subst' context metasenv' ugraph1 - in - let context_for_t = ((Some (name,(C.Decl s')))::context) in - let t',sort2,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' - context_for_t t ugraph1 - in - let t',sort2,subst'',metasenv'',ugraph2 = - coerce_to_sort localization_tbl - t' sort2 subst'' context_for_t metasenv'' ugraph2 - in - let sop,subst''',metasenv''',ugraph3 = - sort_of_prod localization_tbl subst'' metasenv'' - context (name,s') t' (sort1,sort2) ugraph2 - in - C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 - | C.Lambda (n,s,t) -> - let s',sort1,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context s ugraph - in - let s',sort1,subst',metasenv',ugraph1 = - coerce_to_sort localization_tbl - s' sort1 subst' context metasenv' ugraph1 - in - let context_for_t = ((Some (n,(C.Decl s')))::context) in - let t',type2,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' context_for_t t ugraph1 - in - C.Lambda (n,s',t'),C.Prod (n,s',type2), - subst'',metasenv'',ugraph2 - | C.LetIn (n,s,ty,t) -> - (* only to check if s is well-typed *) - let s',ty',subst',metasenv',ugraph1 = - type_of_aux subst metasenv context s ugraph in - let ty,_,subst',metasenv',ugraph1 = - type_of_aux subst' metasenv' context ty ugraph1 in - let subst',metasenv',ugraph1 = - try - fo_unif_subst subst' context metasenv' - ty ty' ugraph1 - with - exn -> - enrich localization_tbl s' exn - ~f:(function _ -> - lazy ("(2) The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s' - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty' - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty - context)) - in - let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in - - let t',inferredty,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' - context_for_t t ugraph1 - in - (* One-step LetIn reduction. - * Even faster than the previous solution. - * Moreover the inferred type is closer to the expected one. - *) - C.LetIn (n,s',ty,t'), - CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty, - subst'',metasenv'',ugraph2 - | C.Appl (he::((_::_) as tl)) -> - let he',hetype,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context he ugraph - in - let tlbody_and_type,subst'',metasenv'',ugraph2 = - typeof_list subst' metasenv' context ugraph1 tl - in - let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 = - eat_prods true subst'' metasenv'' context - he' hetype tlbody_and_type ugraph2 - in - let newappl = (C.Appl (coerced_he::coerced_args)) in - avoid_double_coercion - context subst''' metasenv''' ugraph3 newappl applty - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst',subst',metasenv',ugraph1 = - check_exp_named_subst subst metasenv context - exp_named_subst ugraph in - let ty_uri,ugraph2 = type_of_constant uri ugraph1 in - let cty = - CicSubstitution.subst_vars exp_named_subst' ty_uri - in - C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2 - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst',subst',metasenv',ugraph1 = - check_exp_named_subst subst metasenv context - exp_named_subst ugraph - in - let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in - let cty = - CicSubstitution.subst_vars exp_named_subst' ty_uri in - C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2 - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst',subst',metasenv',ugraph1 = - check_exp_named_subst subst metasenv context - exp_named_subst ugraph - in - let ty_uri,ugraph2 = - type_of_mutual_inductive_constr uri i j ugraph1 - in - let cty = - CicSubstitution.subst_vars exp_named_subst' ty_uri - in - C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst', - metasenv',ugraph2 - | C.MutCase (uri, i, outtype, term, pl) -> - (* first, get the inductive type (and noparams) - * in the environment *) - let (_,b,arity,constructors), expl_params, no_left_params,ugraph = - let _ = CicTypeChecker.typecheck uri in - let obj,u = CicEnvironment.get_cooked_obj ugraph uri in - match obj with - C.InductiveDefinition (l,expl_params,parsno,_) -> - List.nth l i , expl_params, parsno, u - | _ -> - enrich localization_tbl t - (RefineFailure - (lazy ("Unkown mutual inductive definition " ^ - U.string_of_uri uri))) - in - if List.length constructors <> List.length pl then - enrich localization_tbl t - (RefineFailure - (lazy "Wrong number of cases")) ; - let rec count_prod t = - match CicReduction.whd ~subst context t with - C.Prod (_, _, t) -> 1 + (count_prod t) - | _ -> 0 - in - let no_args = count_prod arity in - (* now, create a "generic" MutInd *) - let metasenv,left_args = - CicMkImplicit.n_fresh_metas metasenv subst context no_left_params - in - let metasenv,right_args = - let no_right_params = no_args - no_left_params in - if no_right_params < 0 then assert false - else CicMkImplicit.n_fresh_metas - metasenv subst context no_right_params - in - let metasenv,exp_named_subst = - CicMkImplicit.fresh_subst metasenv subst context expl_params in - let expected_type = - if no_args = 0 then - C.MutInd (uri,i,exp_named_subst) - else - C.Appl - (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args)) - in - (* check consistency with the actual type of term *) - let term',actual_type,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context term ugraph in - let expected_type',_, subst, metasenv,ugraph2 = - type_of_aux subst metasenv context expected_type ugraph1 - in - let actual_type = CicReduction.whd ~subst context actual_type in - let subst,metasenv,ugraph3 = - try - fo_unif_subst subst context metasenv - expected_type' actual_type ugraph2 - with - exn -> - enrich localization_tbl term' exn - ~f:(function _ -> - lazy ("(3) The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst term' - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst actual_type - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' - context)) - in - let rec instantiate_prod t = - function - [] -> t - | he::tl -> - match CicReduction.whd ~subst context t with - C.Prod (_,_,t') -> - instantiate_prod (CicSubstitution.subst he t') tl - | _ -> assert false - in - let arity_instantiated_with_left_args = - instantiate_prod arity left_args in - (* TODO: check if the sort elimination - * is allowed: [(I q1 ... qr)|B] *) - let (pl',_,outtypeinstances,subst,metasenv,ugraph4) = - List.fold_right - (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) -> - let constructor = - if left_args = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl - (C.MutConstruct (uri,i,j,exp_named_subst)::left_args)) - in - let p',actual_type,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context p ugraph - in - let constructor',expected_type, subst, metasenv,ugraph2 = - type_of_aux subst metasenv context constructor ugraph1 - in - let outtypeinstance,subst,metasenv,ugraph3 = - try - check_branch 0 context metasenv subst - no_left_params actual_type constructor' expected_type - ugraph2 - with - exn -> - enrich localization_tbl constructor' - ~f:(fun _ -> - lazy ("(4) The term " ^ - CicMetaSubst.ppterm_in_context metasenv subst p' - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context metasenv subst actual_type - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context metasenv subst expected_type - context)) exn - in - (p'::pl,j-1, - outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) - pl ([],List.length pl,[],subst,metasenv,ugraph3) - in - - (* we are left to check that the outype matches his instances. - The easy case is when the outype is specified, that amount - to a trivial check. Otherwise, we should guess a type from - its instances - *) - - let outtype,outtypety, subst, metasenv,ugraph4 = - type_of_aux subst metasenv context outtype ugraph4 in - (match outtype with - | C.Meta (n,l) -> - (let candidate,ugraph5,metasenv,subst = - let exp_name_subst, metasenv = - let o,_ = - CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri - in - let uris = CicUtil.params_of_obj o in - List.fold_right ( - fun uri (acc,metasenv) -> - let metasenv',new_meta = - CicMkImplicit.mk_implicit metasenv subst context - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable - context - in - (uri, Cic.Meta(new_meta,irl))::acc, metasenv' - ) uris ([],metasenv) - in - let ty = - match left_args,right_args with - [],[] -> Cic.MutInd(uri, i, exp_name_subst) - | _,_ -> - let rec mk_right_args = - function - 0 -> [] - | n -> (Cic.Rel n)::(mk_right_args (n - 1)) - in - let right_args_no = List.length right_args in - let lifted_left_args = - List.map (CicSubstitution.lift right_args_no) left_args - in - Cic.Appl (Cic.MutInd(uri,i,exp_name_subst):: - (lifted_left_args @ mk_right_args right_args_no)) - in - let fresh_name = - FreshNamesGenerator.mk_fresh_name ~subst metasenv - context Cic.Anonymous ~typ:ty - in - match outtypeinstances with - | [] -> - let extended_context = - let rec add_right_args = - function - Cic.Prod (name,ty,t) -> - Some (name,Cic.Decl ty)::(add_right_args t) - | _ -> [] - in - (Some (fresh_name,Cic.Decl ty)):: - (List.rev - (add_right_args arity_instantiated_with_left_args))@ - context - in - let metasenv,new_meta = - CicMkImplicit.mk_implicit metasenv subst extended_context - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable - extended_context - in - let rec add_lambdas b = - function - Cic.Prod (name,ty,t) -> - Cic.Lambda (name,ty,(add_lambdas b t)) - | _ -> Cic.Lambda (fresh_name, ty, b) - in - let candidate = - add_lambdas (Cic.Meta (new_meta,irl)) - arity_instantiated_with_left_args - in - (Some candidate),ugraph4,metasenv,subst - | (constructor_args_no,_,instance,_)::tl -> - try - let instance',subst,metasenv = - CicMetaSubst.delift_rels subst metasenv - constructor_args_no instance - in - let candidate,ugraph,metasenv,subst = - List.fold_left ( - fun (candidate_oty,ugraph,metasenv,subst) - (constructor_args_no,_,instance,_) -> - match candidate_oty with - | None -> None,ugraph,metasenv,subst - | Some ty -> - try - let instance',subst,metasenv = - CicMetaSubst.delift_rels subst metasenv - constructor_args_no instance - in - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv - instance' ty ugraph - in - candidate_oty,ugraph,metasenv,subst - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable - | RefineFailure _ | Uncertain _ -> - None,ugraph,metasenv,subst - ) (Some instance',ugraph4,metasenv,subst) tl - in - match candidate with - | None -> None, ugraph,metasenv,subst - | Some t -> - let rec add_lambdas n b = - function - Cic.Prod (name,ty,t) -> - Cic.Lambda (name,ty,(add_lambdas (n + 1) b t)) - | _ -> - Cic.Lambda (fresh_name, ty, - CicSubstitution.lift (n + 1) t) - in - Some - (add_lambdas 0 t arity_instantiated_with_left_args), - ugraph,metasenv,subst - with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - None,ugraph4,metasenv,subst - in - match candidate with - | None -> raise (Uncertain (lazy "can't solve an higher order unification problem")) - | Some candidate -> - let subst,metasenv,ugraph = - try - fo_unif_subst subst context metasenv - candidate outtype ugraph5 - with - exn -> assert false(* unification against a metavariable *) - in - C.MutCase (uri, i, outtype, term', pl'), - CicReduction.head_beta_reduce - (CicMetaSubst.apply_subst subst - (Cic.Appl (outtype::right_args@[term']))), - subst,metasenv,ugraph) - | _ -> (* easy case *) - let tlbody_and_type,subst,metasenv,ugraph4 = - typeof_list subst metasenv context ugraph4 (right_args @ [term']) - in - let _,_,_,subst,metasenv,ugraph4 = - eat_prods false subst metasenv context - outtype outtypety tlbody_and_type ugraph4 - in - let _,_, subst, metasenv,ugraph5 = - type_of_aux subst metasenv context - (C.Appl ((outtype :: right_args) @ [term'])) ugraph4 - in - let (subst,metasenv,ugraph6) = - List.fold_left2 - (fun (subst,metasenv,ugraph) - p (constructor_args_no,context,instance,args) - -> - let instance' = - let appl = - let outtype' = - CicSubstitution.lift constructor_args_no outtype - in - C.Appl (outtype'::args) - in - CicReduction.head_beta_reduce ~delta:false - ~upto:(List.length args) appl - in - try - fo_unif_subst subst context metasenv instance instance' - ugraph - with - exn -> - enrich localization_tbl p exn - ~f:(function _ -> - lazy ("(5) The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst p - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst instance' - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst instance - context))) - (subst,metasenv,ugraph5) pl' outtypeinstances - in - C.MutCase (uri, i, outtype, term', pl'), - CicReduction.head_beta_reduce - (CicMetaSubst.apply_subst subst - (C.Appl(outtype::right_args@[term']))), - subst,metasenv,ugraph6) - | C.Fix (i,fl) -> - let fl_ty',subst,metasenv,types,ugraph1,len = - List.fold_left - (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) -> - let ty',_,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context ty ugraph - in - fl @ [ty'],subst',metasenv', - Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) - :: types, ugraph, len+1 - ) ([],subst,metasenv,[],ugraph,0) fl - in - let context' = types@context in - let fl_bo',subst,metasenv,ugraph2 = - List.fold_left - (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) -> - let bo',ty_of_bo,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context' bo ugraph in - let expected_ty = CicSubstitution.lift len ty in - let subst',metasenv',ugraph' = - try - fo_unif_subst subst context' metasenv - ty_of_bo expected_ty ugraph1 - with - exn -> - enrich localization_tbl bo exn - ~f:(function _ -> - lazy ("(7) The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst bo - context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo - context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty - context')) - in - fl @ [bo'] , subst',metasenv',ugraph' - ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') - in - let ty = List.nth fl_ty' i in - (* now we have the new ty in fl_ty', the new bo in fl_bo', - * and we want the new fl with bo' and ty' injected in the right - * place. - *) - let rec map3 f l1 l2 l3 = - match l1,l2,l3 with - | [],[],[] -> [] - | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3) - | _ -> assert false - in - let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') ) - fl_ty' fl_bo' fl - in - C.Fix (i,fl''),ty,subst,metasenv,ugraph2 - | C.CoFix (i,fl) -> - let fl_ty',subst,metasenv,types,ugraph1,len = - List.fold_left - (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) -> - let ty',_,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context ty ugraph - in - fl @ [ty'],subst',metasenv', - Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) :: - types, ugraph1, len+1 - ) ([],subst,metasenv,[],ugraph,0) fl - in - let context' = types@context in - let fl_bo',subst,metasenv,ugraph2 = - List.fold_left - (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) -> - let bo',ty_of_bo,subst,metasenv,ugraph1 = - type_of_aux subst metasenv context' bo ugraph in - let expected_ty = CicSubstitution.lift len ty in - let subst',metasenv',ugraph' = - try - fo_unif_subst subst context' metasenv - ty_of_bo expected_ty ugraph1 - with - exn -> - enrich localization_tbl bo exn - ~f:(function _ -> - lazy ("(8) The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst bo - context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo - context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty - context)) - in - fl @ [bo'],subst',metasenv',ugraph' - ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') - in - let ty = List.nth fl_ty' i in - (* now we have the new ty in fl_ty', the new bo in fl_bo', - * and we want the new fl with bo' and ty' injected in the right - * place. - *) - let rec map3 f l1 l2 l3 = - match l1,l2,l3 with - | [],[],[] -> [] - | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3) - | _ -> assert false - in - let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') ) - fl_ty' fl_bo' fl - in - C.CoFix (i,fl''),ty,subst,metasenv,ugraph2 - in - relocalize localization_tbl t t'; - res - - (* check_metasenv_consistency checks that the "canonical" context of a - metavariable is consitent - up to relocation via the relocation list l - - with the actual context *) - and check_metasenv_consistency - metano subst metasenv context canonical_context l ugraph - = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let lifted_canonical_context = - let rec aux i = - function - [] -> [] - | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) - | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (t,ty)))::tl -> - (Some - (n, - C.Def - (S.subst_meta l (S.lift i t), - S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl) - in - aux 1 canonical_context - in - try - List.fold_left2 - (fun (l,subst,metasenv,ugraph) t ct -> - match (t,ct) with - _,None -> - l @ [None],subst,metasenv,ugraph - | Some t,Some (_,C.Def (ct,_)) -> - (*CSC: the following optimization is to avoid a possibly - expensive reduction that can be easily avoided and - that is quite frequent. However, this is better - handled using levels to control reduction *) - let optimized_t = - match t with - Cic.Rel n -> - (try - match List.nth context (n - 1) with - Some (_,C.Def (te,_)) -> S.lift n te - | _ -> t - with - Failure _ -> t) - | _ -> t - in - let subst',metasenv',ugraph' = - (try -(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' - * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*) - fo_unif_subst subst context metasenv optimized_t ct ugraph - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) - in - l @ [Some t],subst',metasenv',ugraph' - | Some t,Some (_,C.Decl ct) -> - let t',inferredty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context t ugraph - in - let subst'',metasenv'',ugraph2 = - (try - fo_unif_subst - subst' context metasenv' inferredty ct ugraph1 - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) - in - l @ [Some t'], subst'',metasenv'',ugraph2 - | None, Some _ -> - raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context - with - Invalid_argument _ -> - raise - (RefineFailure - (lazy (sprintf - "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" - (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext ~metasenv subst canonical_context)))) - - and check_exp_named_subst metasubst metasenv context tl ugraph = - let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = - match tl with - [] -> [],metasubst,metasenv,ugraph - | (uri,t)::tl -> - let ty_uri,ugraph1 = type_of_variable uri ugraph in - let typeofvar = - CicSubstitution.subst_vars substs ty_uri in - (* CSC: why was this code here? it is wrong - (match CicEnvironment.get_cooked_obj ~trust:false uri with - Cic.Variable (_,Some bo,_,_) -> - raise - (RefineFailure (lazy - "A variable with a body can not be explicit substituted")) - | Cic.Variable (_,None,_,_) -> () - | _ -> - raise - (RefineFailure (lazy - ("Unkown variable definition " ^ UriManager.string_of_uri uri))) - ) ; - *) - let t',typeoft,metasubst',metasenv',ugraph2 = - type_of_aux metasubst metasenv context t ugraph1 in - let subst = uri,t' in - let metasubst'',metasenv'',ugraph3 = - try - fo_unif_subst - metasubst' context metasenv' typeoft typeofvar ugraph2 - with _ -> - raise (RefineFailure (lazy - ("Wrong Explicit Named Substitution: " ^ - CicMetaSubst.ppterm metasenv' metasubst' typeoft ^ - " not unifiable with " ^ - CicMetaSubst.ppterm metasenv' metasubst' typeofvar))) - in - (* FIXME: no mere tail recursive! *) - let exp_name_subst, metasubst''', metasenv''', ugraph4 = - check_exp_named_subst_aux - metasubst'' metasenv'' (substs@[subst]) tl ugraph3 - in - ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4 - in - check_exp_named_subst_aux metasubst metasenv [] tl ugraph - - - and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2) - ugraph - = - let module C = Cic in - let context_for_t2 = (Some (name,C.Decl s))::context in - let t1'' = CicReduction.whd ~subst context t1 in - let t2'' = CicReduction.whd ~subst context_for_t2 t2 in - match (t1'', t2'') with - | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> - (* different than Coq manual!!! *) - C.Sort s2,subst,metasenv,ugraph - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - let t' = CicUniv.fresh() in - (try - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.Type t'),subst,metasenv,ugraph2 - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> - let t' = CicUniv.fresh() in - (try - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.CProp t'),subst,metasenv,ugraph2 - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> - let t' = CicUniv.fresh() in - (try - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.CProp t'),subst,metasenv,ugraph2 - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> - let t' = CicUniv.fresh() in - (try - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.Type t'),subst,metasenv,ugraph2 - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | (C.Sort _,C.Sort (C.Type t1)) -> - C.Sort (C.Type t1),subst,metasenv,ugraph - | (C.Sort _,C.Sort (C.CProp t1)) -> - C.Sort (C.CProp t1),subst,metasenv,ugraph - | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph - | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) -> - (* TODO how can we force the meta to become a sort? If we don't we - * break the invariant that refine produce only well typed terms *) - (* TODO if we check the non meta term and if it is a sort then we - * are likely to know the exact value of the result e.g. if the rhs - * is a Sort (Prop | Set | CProp) then the result is the rhs *) - let (metasenv,idx) = - CicMkImplicit.mk_implicit_sort metasenv subst in - let (subst, metasenv,ugraph1) = - try - fo_unif_subst subst context_for_t2 metasenv - (C.Meta (idx,[])) t2'' ugraph - with _ -> assert false (* unification against a metavariable *) - in - t2'',subst,metasenv,ugraph1 - | (C.Sort _,_) - | (C.Meta _,_) -> - enrich localization_tbl s - (RefineFailure - (lazy - (sprintf - "%s is supposed to be a type, but its type is %s" - (CicMetaSubst.ppterm_in_context ~metasenv subst t context) - (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)))) - | _,_ -> - enrich localization_tbl t - (RefineFailure - (lazy - (sprintf - "%s is supposed to be a type, but its type is %s" - (CicMetaSubst.ppterm_in_context ~metasenv subst s context) - (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)))) - - and avoid_double_coercion context subst metasenv ugraph t ty = - if not !pack_coercions then - t,ty,subst,metasenv,ugraph - else - let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in - 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 metasenv subst context source_carr tgt_carr - with - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (fun (metasenv,last,c) _ -> - 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 c)); - let newt,_,subst,metasenv,ugraph = - 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 ??? *) - fo_unif_subst subst context metasenv newt t ugraph - in - debug_print (lazy "unifica..."); - Some (newt, ty, subst, metasenv, ugraph) - with - | RefineFailure s | Uncertain s when not !pack_coercions-> - debug_print s; debug_print (lazy "stop\n");None - | RefineFailure s | Uncertain s -> - debug_print s;debug_print (lazy "goon\n"); - try - let old_pack_coercions = !pack_coercions in - pack_coercions := false; (* to avoid diverging *) - let refined_c1_c2_implicit,ty,subst,metasenv,ugraph = - type_of_aux subst metasenv context c1_c2_implicit ugraph - in - pack_coercions := old_pack_coercions; - let b, _, _, _, _ = - is_a_double_coercion refined_c1_c2_implicit - in - if b then - None - else - let head' = - match refined_c1_c2_implicit with - | Cic.Appl l -> HExtlib.list_last l - | _ -> assert false - in - let subst, metasenv, ugraph = - try fo_unif_subst subst context metasenv - head head' ugraph - with RefineFailure s| Uncertain s-> - debug_print s;assert false - in - let subst, metasenv, ugraph = - fo_unif_subst subst context metasenv - refined_c1_c2_implicit t ugraph - in - Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph) - with - | RefineFailure s | Uncertain s -> - pack_coercions := true;debug_print s;None - | exn -> pack_coercions := true; raise exn)) - candidates - in - (match selected with - | Some x -> x - | None -> - debug_print - (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t)); - t, ty, subst, metasenv, ugraph) - | _ -> t, ty, subst, metasenv, ugraph) - else - t, ty, subst, metasenv, ugraph - - and typeof_list subst metasenv context ugraph l = - let tlbody_and_type,subst,metasenv,ugraph = - List.fold_right - (fun x (res,subst,metasenv,ugraph) -> - let x',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context x ugraph - in - (x', ty)::res,subst',metasenv',ugraph1 - ) l ([],subst,metasenv,ugraph) - in - tlbody_and_type,subst,metasenv,ugraph - - and eat_prods - allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph - = - (* given he:hety, gives beack all (c he) such that (c e):?->? *) - let fix_arity n metasenv context subst he hetype ugraph = - let hetype = CicMetaSubst.apply_subst subst hetype in - (* instead of a dummy functional type we may create the real product - * using args_bo_and_ty, but since coercions lookup ignores the - * actual ariety we opt for the simple solution *) - let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in - match CoercGraph.look_for_coercion metasenv subst context hetype fty with - | CoercGraph.NoCoercion -> [] - | CoercGraph.NotHandled -> - raise (MoreArgsThanExpected (n,Uncertain (lazy ""))) - | CoercGraph.SomeCoercionToTgt candidates - | CoercGraph.SomeCoercion candidates -> - HExtlib.filter_map - (fun (metasenv,last,coerc) -> - let pp t = - CicMetaSubst.ppterm_in_context ~metasenv subst t context in - try - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last he ugraph in - debug_print (lazy ("New head: "^ pp coerc)); - let tty,ugraph = - CicTypeChecker.type_of_aux' ~subst metasenv context coerc - ugraph - in - debug_print (lazy (" has type: "^ pp tty)); - - Some (unvariant coerc,tty,subst,metasenv,ugraph) - with - | Uncertain _ | RefineFailure _ - | HExtlib.Localized (_,Uncertain _) - | HExtlib.Localized (_,RefineFailure _) -> None - | exn -> assert false) - candidates - in - (* aux function to process the type of the head and the args in parallel *) - let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs = - function - | [] -> newargs,subst,metasenv,he,hetype,ugraph - | (hete, hety)::tl as args -> - match (CicReduction.whd ~subst context hetype) with - | Cic.Prod (n,s,t) -> - let arg,subst,metasenv,ugraph = - coerce_to_something allow_coercions localization_tbl - hete hety s subst metasenv context ugraph in - eat_prods_and_args - metasenv subst context he (CicSubstitution.subst (fst arg) t) - ugraph (newargs@[arg]) tl - | _ -> - let he = - match he, newargs with - | _, [] -> he - | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs) - | _ -> Cic.Appl (he::List.map fst newargs) - in - (*{{{*) debug_print (lazy - let pp x = - CicMetaSubst.ppterm_in_context ~metasenv subst x context in - "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^ - "\n but is applyed to: " ^ String.concat ";" - (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*) - let error = ref None in - let possible_fixes = - fix_arity (List.length args) metasenv context subst he hetype - ugraph in - match - HExtlib.list_findopt - (fun (he,hetype,subst,metasenv,ugraph) _ -> - (* {{{ *)debug_print (lazy ("Try fix: "^ - CicMetaSubst.ppterm_in_context ~metasenv subst he context)); - debug_print (lazy (" of type: "^ - CicMetaSubst.ppterm_in_context - ~metasenv subst hetype context)); (* }}} *) - try - Some (eat_prods_and_args - metasenv subst context he hetype ugraph [] args) - with - | RefineFailure _ | Uncertain _ - | HExtlib.Localized (_,RefineFailure _) - | HExtlib.Localized (_,Uncertain _) as exn -> - error := Some exn; None) - possible_fixes - with - | Some x -> x - | None -> - match !error with - None -> - raise - (MoreArgsThanExpected - (List.length args, RefineFailure (lazy ""))) - | Some exn -> raise exn - in - (* first we check if we are in the simple case of a meta closed term *) - let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = - if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then - (* this optimization is to postpone fix_arity (the most common case)*) - subst,metasenv,ugraph,hetype,he,args_bo_and_ty - else - (* this (says CSC) is also useful to infer dependent types *) - let pristinemenv = metasenv in - let metasenv,hetype' = - mk_prod_of_metas metasenv context subst args_bo_and_ty - in - try - let subst,metasenv,ugraph = - fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph - in - subst,metasenv,ugraph,hetype',he,args_bo_and_ty - with RefineFailure _ | Uncertain _ -> - subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty - in - let coerced_args,subst,metasenv,he,t,ugraph = - try - eat_prods_and_args - metasenv subst context he hetype' ugraph1 [] args_bo_and_ty - with - MoreArgsThanExpected (residuals,exn) -> - more_args_than_expected localization_tbl metasenv - subst he context hetype' residuals args_bo_and_ty exn - in - he,(List.map fst coerced_args),t,subst,metasenv,ugraph - - and coerce_to_something - allow_coercions localization_tbl t infty expty subst metasenv context ugraph - = - let module CS = CicSubstitution in - let module CR = CicReduction in - let cs_subst = CS.subst ~avoid_beta_redexes:true in - let coerce_atom_to_something t infty expty subst metasenv context ugraph = - debug_print (lazy ("COERCE_ATOM_TO_SOMETHING")); - let coer = - CoercGraph.look_for_coercion metasenv subst context infty expty - in - match coer with - | CoercGraph.NoCoercion - | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy - "coerce_atom_to_something fails since no coercions found")) - | CoercGraph.NotHandled when - not (CicUtil.is_meta_closed infty) || - not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy - "coerce_atom_to_something fails since carriers have metas")) - | CoercGraph.NotHandled -> raise (RefineFailure (lazy - "coerce_atom_to_something fails since no coercions found")) - | CoercGraph.SomeCoercion candidates -> - debug_print (lazy (string_of_int (List.length candidates) ^ - " candidates found")); - let uncertain = ref false in - let selected = - let posibilities = - HExtlib.filter_map - (fun (metasenv,last,c) -> - try - (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst last context ^ - " <==> " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ - "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c - context)); - debug_print (lazy ("FO_UNIF_SUBST: " ^ - CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *) - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last t ugraph - in - let newt,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context c ugraph in - let newt, newty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph newt - expty - in - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv newhety expty ugraph - in - let b, ugraph = - CicReduction.are_convertible - ~subst ~metasenv context infty expty ugraph - in - if b then - Some ((t,infty), subst, metasenv, ugraph) - else - let newt = unvariant newt in - Some ((newt,newty), subst, metasenv, ugraph) - with - | Uncertain _ -> uncertain := true; None - | RefineFailure _ -> None) - candidates - in - match - List.fast_sort - (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2) - posibilities - with - | [] -> None - | x::_ -> Some x - in - match selected with - | Some x -> x - | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails")) - | None -> raise (RefineFailure (lazy "coerce_atom fails")) - in - let rec coerce_to_something_aux - t infty expty subst metasenv context ugraph - = - try - let subst, metasenv, ugraph = - fo_unif_subst subst context metasenv infty expty ugraph - in - (t, expty), subst, metasenv, ugraph - with (Uncertain _ | RefineFailure _ as exn) - when allow_coercions && !insert_coercions -> - let whd = CicReduction.whd ~delta:false in - let clean t s c = whd c (CicMetaSubst.apply_subst s t) in - let infty = clean infty subst context in - let expty = clean expty subst context in - let t = clean t subst context in - (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^ - CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*) - let (coerced,_),subst,metasenv,_ as result = - match infty, expty, t with - | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) -> - (*{{{*) debug_print (lazy "FIX"); - (match fl with - [name,i,_(* infty *),bo] -> - let context_bo = - Some (Cic.Name name,Cic.Decl expty)::context in - let (rel1, _), subst, metasenv, ugraph = - coerce_to_something_aux (Cic.Rel 1) - (CS.lift 1 expty) (CS.lift 1 infty) subst - metasenv context_bo ugraph in - let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in - let (bo,_), subst, metasenv, ugraph = - coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1 - expty) subst - metasenv context_bo ugraph - in - (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph - | _ -> assert false (* not implemented yet *)) (*}}}*) - | _,_, Cic.MutCase (uri,tyno,outty,m,pl) -> - (*{{{*) debug_print (lazy "CASE"); - (* {{{ helper functions *) - let get_cl_and_left_p uri tyno outty ugraph = - match CicEnvironment.get_obj ugraph uri with - | Cic.InductiveDefinition (tl, _, leftno, _),ugraph -> - let count_pis t = - let rec aux ctx t = - match CicReduction.whd ~delta:false ctx t with - | Cic.Prod (name,src,tgt) -> - let ctx = Some (name, Cic.Decl src) :: ctx in - 1 + aux ctx tgt - | _ -> 0 - in - aux [] t - in - let rec skip_lambda_delifting t n = - match t,n with - | _,0 -> t - | Cic.Lambda (_,_,t),n -> - skip_lambda_delifting - (CS.subst (Cic.Implicit None) t) (n - 1) - | _ -> assert false - in - let get_l_r_p n = function - | Cic.Lambda (_,Cic.MutInd _,_) -> [],[] - | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) -> - HExtlib.split_nth n args - | _ -> assert false - in - let _, _, ty, cl = List.nth tl tyno in - let pis = count_pis ty in - let rno = pis - leftno in - let t = skip_lambda_delifting outty rno in - let left_p, _ = get_l_r_p leftno t in - let instantiale_with_left cl = - List.map - (fun ty -> - List.fold_left - (fun t p -> match t with - | Cic.Prod (_,_,t) -> - cs_subst p t - | _-> assert false) - ty left_p) - cl - in - let cl = instantiale_with_left (List.map snd cl) in - cl, left_p, leftno, rno, ugraph - | _ -> raise exn - in - let rec keep_lambdas_and_put_expty ctx t bo right_p matched n = - match t,n with - | _,0 -> - let rec mkr n = function - | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl - in - let bo = - CicReplace.replace_lifting - ~equality:(fun _ -> CicUtil.alpha_equivalence) - ~context:ctx - ~what:(matched::right_p) - ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p)) - ~where:bo - in - bo - | Cic.Lambda (name, src, tgt),_ -> - Cic.Lambda (name, src, - keep_lambdas_and_put_expty - (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo) - (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1)) - | _ -> assert false - in - let eq_uri, eq, eq_refl = - match LibraryObjects.eq_URI () with - | None -> HLog.warn "no default equality"; raise exn - | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[]) - in - let add_params - metasenv subst context uri tyno cty outty mty m leftno i - = - let rec aux context outty par k mty m = function - | Cic.Prod (name, src, tgt) -> - let t,k = - aux - (Some (name, Cic.Decl src) :: context) - (CS.lift 1 outty) (Cic.Rel k::par) (k+1) - (CS.lift 1 mty) (CS.lift 1 m) tgt - in - Cic.Prod (name, src, t), k - | Cic.MutInd _ -> - let k = - let k = Cic.MutConstruct (uri,tyno,i,[]) in - if par <> [] then Cic.Appl (k::par) else k - in - Cic.Prod (Cic.Name "p", - Cic.Appl [eq; mty; m; k], - (CS.lift 1 - (CR.head_beta_reduce ~delta:false - (Cic.Appl [outty;k])))),k - | Cic.Appl (Cic.MutInd _::pl) -> - let left_p,right_p = HExtlib.split_nth leftno pl in - let has_rights = right_p <> [] in - let k = - let k = Cic.MutConstruct (uri,tyno,i,[]) in - Cic.Appl (k::left_p@par) - in - let right_p = - try match - CicTypeChecker.type_of_aux' ~subst metasenv context k - CicUniv.oblivion_ugraph - with - | Cic.Appl (Cic.MutInd _::args),_ -> - snd (HExtlib.split_nth leftno args) - | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _-> assert false - in - if has_rights then - CR.head_beta_reduce ~delta:false - (Cic.Appl (outty ::right_p @ [k])),k - else - Cic.Prod (Cic.Name "p", - Cic.Appl [eq; mty; m; k], - (CS.lift 1 - (CR.head_beta_reduce ~delta:false - (Cic.Appl (outty ::right_p @ [k]))))),k - | _ -> assert false - in - aux context outty [] 1 mty m cty - in - let add_lambda_for_refl_m pbo rno mty m k cty = - (* k lives in the right context *) - if rno <> 0 then pbo else - let rec aux mty m = function - | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) -> - Cic.Lambda (name,src, - (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty))) - | t,_ -> - Cic.Lambda (Cic.Name "p", - Cic.Appl [eq; mty; m; k],CS.lift 1 t) - in - aux mty m (pbo,cty) - in - let add_pi_for_refl_m new_outty mty m rno = - if rno <> 0 then new_outty else - let rec aux m mty = function - | Cic.Lambda (name, src, tgt) -> - Cic.Lambda (name, src, - aux (CS.lift 1 m) (CS.lift 1 mty) tgt) - | t -> - Cic.Prod - (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1], - CS.lift 1 t) - in - aux m mty new_outty - in (* }}} end helper functions *) - (* constructors types with left params already instantiated *) - let outty = CicMetaSubst.apply_subst subst outty in - let cl, left_p, leftno,rno,ugraph = - get_cl_and_left_p uri tyno outty ugraph - in - let right_p, mty = - try - match - CicTypeChecker.type_of_aux' ~subst metasenv context m - CicUniv.oblivion_ugraph - with - | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty - | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ -> - snd (HExtlib.split_nth leftno args), mty - | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _ -> - raise (AssertFailure(lazy "already ill-typed matched term")) - in - let new_outty = - keep_lambdas_and_put_expty context outty expty right_p m (rno+1) - in - debug_print - (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst new_outty context)); - let _,pl,subst,metasenv,ugraph = - List.fold_right2 - (fun cty pbo (i, acc, s, menv, ugraph) -> - (* Pi k_par, (Pi H:m=(K_i left_par k_par)), - * (new_)outty right_par (K_i left_par k_par) *) - let infty_pbo, _ = - add_params menv s context uri tyno - cty outty mty m leftno i in - debug_print - (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context - ~metasenv subst infty_pbo context)); - let expty_pbo, k = (* k is (K_i left_par k_par) *) - add_params menv s context uri tyno - cty new_outty mty m leftno i in - debug_print - (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context - ~metasenv subst expty_pbo context)); - let pbo = add_lambda_for_refl_m pbo rno mty m k cty in - debug_print - (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst pbo context)); - let (pbo, _), subst, metasenv, ugraph = - coerce_to_something_aux pbo infty_pbo expty_pbo - s menv context ugraph - in - debug_print - (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst pbo context)); - (i-1, pbo::acc, subst, metasenv, ugraph)) - cl pl (List.length pl, [], subst, metasenv, ugraph) - in - let new_outty = add_pi_for_refl_m new_outty mty m rno in - debug_print - (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context - ~metasenv subst new_outty context)); - let t = - if rno = 0 then - let refl_m=Cic.Appl[eq_refl;mty;m]in - Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] - else - Cic.MutCase(uri,tyno,new_outty,m,pl) - in - (t, expty), subst, metasenv, ugraph (*}}}*) - | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> - (*{{{*) debug_print (lazy "LAM"); - let name_con = - FreshNamesGenerator.mk_fresh_name - ~subst metasenv context ~typ:src2 Cic.Anonymous - in - let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in - (* contravariant part: the argument of f:src->ty *) - let (rel1, _), subst, metasenv, ugraph = - coerce_to_something_aux - (Cic.Rel 1) (CS.lift 1 src2) - (CS.lift 1 src) subst metasenv context_src2 ugraph - in - (* covariant part: the result of f(c x); x:src2; (c x):src *) - let name_t, bo = - match t with - | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo) - | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1] - in - (* we fix the possible dependency problem in the source ty *) - let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in - let (bo, _), subst, metasenv, ugraph = - coerce_to_something_aux - bo ty ty2 subst metasenv context_src2 ugraph - in - let coerced = Cic.Lambda (name_t,src2, bo) in - (coerced, expty), subst, metasenv, ugraph (*}}}*) - | _ -> - (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context - ~metasenv subst infty context ^ " ==> " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst expty context)); - coerce_atom_to_something - t infty expty subst metasenv context ugraph (*}}}*) - in - debug_print (lazy ("COERCE TO SOMETHING END: "^ - CicMetaSubst.ppterm_in_context ~metasenv subst coerced context)); - result - in - try - coerce_to_something_aux t infty expty subst metasenv context ugraph - with Uncertain _ | RefineFailure _ as exn -> - let f _ = - lazy ("(9) The term " ^ - CicMetaSubst.ppterm_in_context metasenv subst t context ^ - " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst - infty context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context metasenv subst expty context) - in - enrich localization_tbl ~f t exn - - and coerce_to_sort localization_tbl t infty subst context metasenv uragph = - match CicReduction.whd ~delta:false ~subst context infty with - | Cic.Meta _ | Cic.Sort _ -> - t,infty, subst, metasenv, ugraph - | src -> - debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context - ~metasenv subst src context)); - let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in - try - let (t, ty_t), subst, metasenv, ugraph = - coerce_to_something true - localization_tbl t src tgt subst metasenv context ugraph - in - debug_print (lazy ("COERCE TO SORT END: "^ - CicMetaSubst.ppterm_in_context ~metasenv subst t context)); - t, ty_t, subst, metasenv, ugraph - with HExtlib.Localized (_, exn) -> - let f _ = - lazy ("(7)The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst t context - ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst src context - ^ " that is not a sort") - in - enrich localization_tbl ~f t exn - in - - (* eat prods ends here! *) - - let t',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context t ugraph - in - let substituted_t = CicMetaSubst.apply_subst subst' t' in - let substituted_ty = CicMetaSubst.apply_subst subst' ty in - (* Andrea: ho rimesso qui l'applicazione della subst al - metasenv dopo che ho droppato l'invariante che il metsaenv - e' sempre istanziato *) - let substituted_metasenv = - CicMetaSubst.apply_subst_metasenv subst' metasenv' in - (* metasenv' *) - (* substituted_t,substituted_ty,substituted_metasenv *) - (* ANDREA: spostare tutta questa robaccia da un altra parte *) - let cleaned_t = - if clean_dummy_dependent_types then - FreshNamesGenerator.clean_dummy_dependent_types substituted_t - else substituted_t in - let cleaned_ty = - if clean_dummy_dependent_types then - FreshNamesGenerator.clean_dummy_dependent_types substituted_ty - else substituted_ty in - let cleaned_metasenv = - if clean_dummy_dependent_types then - List.map - (function (n,context,ty) -> - let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in - let context' = - List.map - (function - None -> None - | Some (n, Cic.Decl t) -> - Some (n, - Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t)) - | Some (n, Cic.Def (bo,ty)) -> - let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in - let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty - in - Some (n, Cic.Def (bo',ty')) - ) context - in - (n,context',ty') - ) substituted_metasenv - else - substituted_metasenv - in - (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1) -;; - -let type_of metasenv subst context t ug = - type_of_aux' metasenv subst context t ug -;; - -let type_of_aux' - ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug -= - let t,ty,m,s,ug = - type_of_aux' ?clean_dummy_dependent_types ?localization_tbl - metasenv [] context t ug - in - t,ty,m,ug -;; - -let undebrujin uri typesno tys t = - snd - (List.fold_right - (fun (name,_,_,_) (i,t) -> - (* here the explicit_named_substituion is assumed to be *) - (* of length 0 *) - let t' = Cic.MutInd (uri,i,[]) in - let t = CicSubstitution.subst t' t in - i - 1,t - ) tys (typesno - 1,t)) - -let map_first_n n start f g l = - let rec aux acc k l = - if k < n then - match l with - | [] -> raise (Invalid_argument "map_first_n") - | hd :: tl -> f hd k (aux acc (k+1) tl) - else - g acc l - in - aux start 0 l - -(*CSC: this is a very rough approximation; to be finished *) -let are_all_occurrences_positive metasenv ugraph uri tys leftno = - let subst,metasenv,ugraph,tys = - List.fold_right - (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) -> - let subst,metasenv,ugraph,cl = - List.fold_right - (fun (name,ty) (subst,metasenv,ugraph,acc) -> - let rec aux ctx k subst = function - | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'-> - let subst,metasenv,ugraph,tl = - map_first_n leftno - (subst,metasenv,ugraph,[]) - (fun t n (subst,metasenv,ugraph,acc) -> - let subst,metasenv,ugraph = - fo_unif_subst - subst ctx metasenv t (Cic.Rel (k-n)) ugraph - in - subst,metasenv,ugraph,(t::acc)) - (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl)) - tl - in - subst,metasenv,ugraph,(Cic.Appl (hd::tl)) - | Cic.MutInd(uri',_,_) as t when uri = uri'-> - subst,metasenv,ugraph,t - | Cic.Prod (name,s,t) -> - let ctx = (Some (name,Cic.Decl s))::ctx in - let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in - subst,metasenv,ugraph,Cic.Prod (name,s,t) - | _ -> - raise - (RefineFailure - (lazy "not well formed constructor type")) - in - let subst,metasenv,ugraph,ty = aux [] 0 subst ty in - subst,metasenv,ugraph,(name,ty) :: acc) - cl (subst,metasenv,ugraph,[]) - in - subst,metasenv,ugraph,(name,ind,arity,cl)::acc) - tys ([],metasenv,ugraph,[]) - in - let substituted_tys = - List.map - (fun (name,ind,arity,cl) -> - let cl = - List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl - in - name,ind,CicMetaSubst.apply_subst subst arity,cl) - tys - in - metasenv,ugraph,substituted_tys - -let typecheck metasenv uri obj ~localization_tbl = - let ugraph = CicUniv.oblivion_ugraph in - match obj with - Cic.Constant (name,Some bo,ty,args,attrs) -> - (* CSC: ugly code. Here I need to retrieve in advance the loc of bo - since type_of_aux' destroys localization information (which are - preserved by type_of_aux *) - let loc exn' = - try - Cic.CicHash.find localization_tbl bo - with Not_found -> - HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo); - raise exn' in - let bo',boty,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv [] bo ugraph in - let ty',_,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv [] ty ugraph in - let subst,metasenv,ugraph = - try - fo_unif_subst [] [] metasenv boty ty' ugraph - with - RefineFailure _ - | Uncertain _ as exn -> - let msg = - lazy ("(1) The term " ^ - CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^ - " has type " ^ - CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^ - " but is here used with type " ^ - CicMetaSubst.ppterm_in_context ~metasenv [] ty' []) - in - let exn' = - match exn with - RefineFailure _ -> RefineFailure msg - | Uncertain _ -> Uncertain msg - | _ -> assert false - in - raise (HExtlib.Localized (loc exn',exn')) - in - let bo' = CicMetaSubst.apply_subst subst bo' in - let ty' = CicMetaSubst.apply_subst subst ty' in - let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph - | Cic.Constant (name,None,ty,args,attrs) -> - let ty',sort,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv [] ty ugraph - in - (match CicReduction.whd [] sort with - Cic.Sort _ - | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph - | _ -> raise (RefineFailure (lazy ""))) - | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> - assert (metasenv' = metasenv); - (* Here we do not check the metasenv for correctness *) - let bo',boty,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv [] bo ugraph in - let ty',sort,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv [] ty ugraph in - begin - match CicReduction.whd ~delta:true [] sort with - Cic.Sort _ - (* instead of raising Uncertain, let's hope that the meta will become - a sort *) - | Cic.Meta _ -> () - | _ -> raise (RefineFailure (lazy "The term provided is not a type")) - end; - let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in - let bo' = CicMetaSubst.apply_subst subst bo' in - let ty' = CicMetaSubst.apply_subst subst ty' in - let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph - | Cic.Variable _ -> assert false (* not implemented *) - | Cic.InductiveDefinition (tys,args,paramsno,attrs) -> - (*CSC: this code is greately simplified and many many checks are missing *) - (*CSC: e.g. the constructors are not required to build their own types, *) - (*CSC: the arities are not required to have as type a sort, etc. *) - let uri = match uri with Some uri -> uri | None -> assert false in - let typesno = List.length tys in - (* first phase: we fix only the types *) - let metasenv,ugraph,tys = - List.fold_right - (fun (name,b,ty,cl) (metasenv,ugraph,res) -> - let ty',_,metasenv,ugraph = - (* clean_dummy_dependent_types: false to avoid cleaning the names - of the left products, that must be identical to those of the - constructors; however, non-left products should probably be - cleaned *) - type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl - metasenv [] ty ugraph - in - metasenv,ugraph,(name,b,ty',cl)::res - ) tys (metasenv,ugraph,[]) in - let con_context = - List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in - (* second phase: we fix only the constructors *) - let saved_menv = metasenv in - let metasenv,ugraph,tys = - List.fold_right - (fun (name,b,ty,cl) (metasenv,ugraph,res) -> - let metasenv,ugraph,cl' = - List.fold_right - (fun (name,ty) (metasenv,ugraph,res) -> - let ty = - CicTypeChecker.debrujin_constructor - ~cb:(relocalize localization_tbl) uri typesno [] ty in - let ty',_,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv con_context ty ugraph in - let ty' = undebrujin uri typesno tys ty' in - metasenv@saved_menv,ugraph,(name,ty')::res - ) cl (metasenv,ugraph,[]) - in - metasenv,ugraph,(name,b,ty,cl')::res - ) tys (metasenv,ugraph,[]) in - (* third phase: we check the positivity condition *) - let metasenv,ugraph,tys = - are_all_occurrences_positive metasenv ugraph uri tys paramsno - in - Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph -;; - -(* sara' piu' veloce che raffinare da zero? mah.... *) -let pack_coercion metasenv ctx t = - let module C = Cic in - let rec merge_coercions ctx = - let aux = (fun (u,t) -> u,merge_coercions ctx t) in - function - | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t - | C.Meta (n,subst) -> - let subst' = - List.map - (function None -> None | Some t -> Some (merge_coercions ctx t)) subst - in - C.Meta (n,subst') - | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty) - | C.Prod (name,so,dest) -> - let ctx' = (Some (name,C.Decl so))::ctx in - C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest) - | C.Lambda (name,so,dest) -> - let ctx' = (Some (name,C.Decl so))::ctx in - C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) - | C.LetIn (name,so,ty,dest) -> - let ctx' = Some (name,(C.Def (so,ty)))::ctx in - C.LetIn - (name, merge_coercions ctx so, merge_coercions ctx ty, - merge_coercions ctx' dest) - | C.Appl l -> - let l = List.map (merge_coercions ctx) l in - let t = C.Appl l in - let b,_,_,_,_ = is_a_double_coercion t in - if b then - let ugraph = CicUniv.oblivion_ugraph in - let old_insert_coercions = !insert_coercions in - insert_coercions := false; - let newt, _, menv, _ = - try - type_of_aux' metasenv ctx t ugraph - with RefineFailure _ | Uncertain _ -> - t, t, [], ugraph - in - insert_coercions := old_insert_coercions; - if metasenv <> [] || menv = [] then - newt - else - (prerr_endline "PUO' SUCCEDERE!!!!!";t) - else - t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.Var (uri, exp_named_subst) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.Const (uri, exp_named_subst) - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.MutInd (uri,tyno,exp_named_subst) - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.MutConstruct (uri,tyno,consno,exp_named_subst) - | C.MutCase (uri,tyno,out,te,pl) -> - let pl = List.map (merge_coercions ctx) pl in - C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl) - | C.Fix (fno, fl) -> - let ctx' = - List.fold_left - (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) - ctx fl - in - let fl = - List.map - (fun (name,idx,ty,bo) -> - (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo)) - fl - in - C.Fix (fno, fl) - | C.CoFix (fno, fl) -> - let ctx' = - List.fold_left - (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) - ctx fl - in - let fl = - List.map - (fun (name,ty,bo) -> - (name, merge_coercions ctx ty, merge_coercions ctx' bo)) - fl - in - C.CoFix (fno, fl) - in - merge_coercions ctx t -;; - -let pack_coercion_metasenv conjectures = conjectures (* - - TASSI: this code war written when coercions were a toy, - now packing coercions involves unification thus - the metasenv may change, and this pack coercion - does not handle that. - - let module C = Cic in - List.map - (fun (i, ctx, ty) -> - let ctx = - List.fold_right - (fun item ctx -> - let item' = - match item with - Some (name, C.Decl t) -> - Some (name, C.Decl (pack_coercion conjectures ctx t)) - | Some (name, C.Def (t,None)) -> - Some (name,C.Def (pack_coercion conjectures ctx t,None)) - | Some (name, C.Def (t,Some ty)) -> - Some (name, C.Def (pack_coercion conjectures ctx t, - Some (pack_coercion conjectures ctx ty))) - | None -> None - in - item'::ctx - ) ctx [] - in - ((i,ctx,pack_coercion conjectures ctx ty)) - ) conjectures - *) -;; - -let pack_coercion_obj obj = obj (* - - TASSI: this code war written when coercions were a toy, - now packing coercions involves unification thus - the metasenv may change, and this pack coercion - does not handle that. - - let module C = Cic in - match obj with - | C.Constant (id, body, ty, params, attrs) -> - let body = - match body with - | None -> None - | Some body -> Some (pack_coercion [] [] body) - in - let ty = pack_coercion [] [] ty in - C.Constant (id, body, ty, params, attrs) - | C.Variable (name, body, ty, params, attrs) -> - let body = - match body with - | None -> None - | Some body -> Some (pack_coercion [] [] body) - in - let ty = pack_coercion [] [] ty in - C.Variable (name, body, ty, params, attrs) - | C.CurrentProof (name, conjectures, body, ty, params, attrs) -> - let conjectures = pack_coercion_metasenv conjectures in - let body = pack_coercion conjectures [] body in - let ty = pack_coercion conjectures [] ty in - C.CurrentProof (name, conjectures, body, ty, params, attrs) - | C.InductiveDefinition (indtys, params, leftno, attrs) -> - let indtys = - List.map - (fun (name, ind, arity, cl) -> - let arity = pack_coercion [] [] arity in - let cl = - List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl - in - (name, ind, arity, cl)) - indtys - in - C.InductiveDefinition (indtys, params, leftno, attrs) *) -;; - - -(* DEBUGGING ONLY -let type_of_aux' metasenv context term = - try - let (t,ty,m) = - type_of_aux' metasenv context term in - debug_print (lazy - ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty)); - debug_print (lazy - ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m [])); - (t,ty,m) - with - | RefineFailure msg as e -> - debug_print (lazy ("@@@ REFINE FAILED: " ^ msg)); - raise e - | Uncertain msg as e -> - debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg)); - raise e -;; *) - -let profiler2 = HExtlib.profile "CicRefine" - -let type_of_aux' ?localization_tbl metasenv context term ugraph = - profiler2.HExtlib.profile - (type_of_aux' ?localization_tbl metasenv context term) ugraph - -let typecheck ~localization_tbl metasenv uri obj = - profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj - -let _ = DoubleTypeInference.pack_coercion := pack_coercion;; -(* vim:set foldmethod=marker: *) diff --git a/matita/components/cic_unification/cicRefine.mli b/matita/components/cic_unification/cicRefine.mli deleted file mode 100644 index 666099dce..000000000 --- a/matita/components/cic_unification/cicRefine.mli +++ /dev/null @@ -1,58 +0,0 @@ -(* 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/. - *) - -exception RefineFailure of string Lazy.t;; -exception Uncertain of string Lazy.t;; -exception AssertFailure of string Lazy.t;; - -(* type_of_aux' metasenv context term graph *) -(* refines [term] and returns the refined form of [term], *) -(* its type, the new metasenv and universe graph. *) -val type_of_aux': - ?localization_tbl:Stdpp.location Cic.CicHash.t -> - Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> - Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph - - (* this is the correct one and should be used by tactics to fold subst *) -val type_of: - Cic.metasenv -> Cic.substitution -> - Cic.context -> Cic.term -> CicUniv.universe_graph -> - Cic.term * Cic.term * Cic.metasenv * Cic.substitution *CicUniv.universe_graph - -(* typecheck metasenv uri obj graph *) -(* refines [obj] and returns the refined form of [obj], *) -(* the new metasenv and universe graph. *) -(* the [uri] is required only for inductive definitions *) -val typecheck : - localization_tbl:Stdpp.location Cic.CicHash.t -> - Cic.metasenv -> UriManager.uri option -> Cic.obj -> - Cic.obj * Cic.metasenv * CicUniv.universe_graph - -val insert_coercions: bool ref (* initially true *) -val pack_coercions : bool ref - -val pack_coercion_obj: Cic.obj -> Cic.obj - -val pack_coercion_metasenv: Cic.metasenv -> Cic.metasenv diff --git a/matita/components/cic_unification/cicReplace.ml b/matita/components/cic_unification/cicReplace.ml deleted file mode 100644 index 0b8b67497..000000000 --- a/matita/components/cic_unification/cicReplace.ml +++ /dev/null @@ -1,129 +0,0 @@ -(* 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: cicRefine.ml 7618 2007-09-05 10:07:39Z sacerdot $ *) - -exception WhatAndWithWhatDoNotHaveTheSameLength;; - -module C = Cic -module S = CicSubstitution - -let replace_lifting ~equality ~context ~what ~with_what ~where = - let find_image ctx what t = - let rec find_image_aux = - function - [],[] -> raise Not_found - | what::tl1,with_what::tl2 -> - if equality ctx what t then with_what else find_image_aux (tl1,tl2) - | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength - in - find_image_aux (what,with_what) - in - let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in - let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in - let rec substaux k ctx what t = - try - S.lift (k-1) (find_image ctx what t) - with Not_found -> - match t with - C.Rel n as t -> t - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l) -> - let l' = - List.map - (function - None -> None - | Some t -> Some (substaux k ctx what t) - ) l - in - C.Meta(i,l') - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (substaux k ctx what te, substaux k ctx what ty) - | C.Prod (n,s,t) -> - C.Prod - (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t) - | C.Lambda (n,s,t) -> - C.Lambda - (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t) - | C.LetIn (n,s,ty,t) -> - C.LetIn - (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t) - | C.Appl (he::tl) -> - (* Invariant: no Appl applied to another Appl *) - let tl' = List.map (substaux k ctx what) tl in - begin - match substaux k ctx what he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - end - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst - in - C.MutInd (uri,i,exp_named_subst') - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst - in - C.MutConstruct (uri,i,j,exp_named_subst') - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,substaux k ctx what outt, substaux k ctx what t, - List.map (substaux k ctx what) pl) - | C.Fix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (* WRONG CTX *) - (name, i, substaux k ctx what ty, - substaux (k+len) ctx (List.map (S.lift len) what) bo) - ) fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> (* WRONG CTX *) - (name, substaux k ctx what ty, - substaux (k+len) ctx (List.map (S.lift len) what) bo) - ) fl - in - C.CoFix (i, substitutedfl) - in - substaux 1 context what where -;; - - diff --git a/matita/components/cic_unification/cicReplace.mli b/matita/components/cic_unification/cicReplace.mli deleted file mode 100644 index c2f9aaff3..000000000 --- a/matita/components/cic_unification/cicReplace.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* 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: cicRefine.ml 7618 2007-09-05 10:07:39Z sacerdot $ *) - -exception WhatAndWithWhatDoNotHaveTheSameLength - - -val replace_lifting : - equality:(Cic.context -> Cic.term -> Cic.term -> bool) -> - context:Cic.context -> - what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term diff --git a/matita/components/cic_unification/cicUnification.ml b/matita/components/cic_unification/cicUnification.ml deleted file mode 100644 index fca316fa3..000000000 --- a/matita/components/cic_unification/cicUnification.ml +++ /dev/null @@ -1,997 +0,0 @@ -(* 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 - -exception UnificationFailure of string Lazy.t;; -exception Uncertain of string Lazy.t;; -exception AssertFailure of string Lazy.t;; - -let verbose = false;; -let debug_print = fun _ -> () - -let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'" -let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand" -let profiler_deref = HExtlib.profile "fo_unif_subst.deref'" -let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible" - -let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'" - -let type_of_aux' metasenv subst context term ugraph = -let foo () = - try - profile.HExtlib.profile - (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph - with - CicTypeChecker.TypeCheckerFailure msg -> - let msg = - lazy - (sprintf - "Kernel Type checking error: -%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." - (CicMetaSubst.ppterm ~metasenv subst term) - (CicMetaSubst.ppterm ~metasenv [] term) - (CicMetaSubst.ppcontext ~metasenv subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in - raise (AssertFailure msg) - | CicTypeChecker.AssertFailure msg -> - let msg = lazy - (sprintf - "Kernel Type checking assertion failure: -%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." - (CicMetaSubst.ppterm ~metasenv subst term) - (CicMetaSubst.ppterm ~metasenv [] term) - (CicMetaSubst.ppcontext ~metasenv subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in - raise (AssertFailure msg) -in profiler_toa.HExtlib.profile foo () -;; - -let exists_a_meta l = - List.exists - (function - | Cic.Meta _ - | Cic.Appl (Cic.Meta _::_) -> true - | _ -> false) l - -let rec deref subst t = - let snd (_,a,_) = a in - match t with - Cic.Meta(n,l) -> - (try - deref subst - (CicSubstitution.subst_meta - l (snd (CicUtil.lookup_subst n subst))) - with - CicUtil.Subst_not_found _ -> t) - | Cic.Appl(Cic.Meta(n,l)::args) -> - (match deref subst (Cic.Meta(n,l)) with - | Cic.Lambda _ as t -> - deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) - | r -> Cic.Appl(r::args)) - | Cic.Appl(((Cic.Lambda _) as t)::args) -> - deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) - | t -> t -;; - -let deref subst t = - let foo () = deref subst t - in profiler_deref.HExtlib.profile foo () - -exception WrongShape;; -let eta_reduce after_beta_expansion after_beta_expansion_body - before_beta_expansion - = - try - match before_beta_expansion,after_beta_expansion_body with - Cic.Appl l, Cic.Appl l' -> - let rec all_but_last check_last = - function - [] -> assert false - | [Cic.Rel 1] -> [] - | [_] -> if check_last then raise WrongShape else [] - | he::tl -> he::(all_but_last check_last tl) - in - let all_but_last check_last l = - match all_but_last check_last l with - [] -> assert false - | [he] -> he - | l -> Cic.Appl l - in - let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in - let all_but_last = all_but_last false l in - (* here we should test alpha-equivalence; however we know by - construction that here alpha_equivalence is equivalent to = *) - if t = all_but_last then - all_but_last - else - after_beta_expansion - | _,_ -> after_beta_expansion - with - WrongShape -> after_beta_expansion - -let rec beta_expand num test_equality_only metasenv subst context t arg ugraph = - let module S = CicSubstitution in - let module C = Cic in -let foo () = - let rec aux metasenv subst n context t' ugraph = - try - - let subst,metasenv,ugraph1 = - fo_unif_subst test_equality_only subst context metasenv - (CicSubstitution.lift n arg) t' ugraph - - in - subst,metasenv,C.Rel (1 + n),ugraph1 - with - Uncertain _ - | UnificationFailure _ -> - match t' with - | C.Rel m -> subst,metasenv, - (if m <= n then C.Rel m else C.Rel (m+1)),ugraph - | C.Var (uri,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1 - | C.Meta (i,l) -> - (* andrea: in general, beta_expand can create badly typed - terms. This happens quite seldom in practice, UNLESS we - iterate on the local context. For this reason, we renounce - to iterate and just lift *) - let l = - List.map - (function - Some t -> Some (CicSubstitution.lift 1 t) - | None -> None) l in - subst, metasenv, C.Meta (i,l), ugraph - | C.Sort _ - | C.Implicit _ as t -> subst,metasenv,t,ugraph - | C.Cast (te,ty) -> - let subst,metasenv,te',ugraph1 = - aux metasenv subst n context te ugraph in - let subst,metasenv,ty',ugraph2 = - aux metasenv subst n context ty ugraph1 in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Cast (te', ty')),ugraph2 - | C.Prod (nn,s,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t - ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Prod (nn, s', t')),ugraph2 - | C.Lambda (nn,s,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 - | C.LetIn (nn,s,ty,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,ty',ugraph1 = - aux metasenv subst n context ty ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t - ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2 - | C.Appl l -> - let subst,metasenv,revl',ugraph1 = - List.fold_left - (fun (subst,metasenv,appl,ugraph) t -> - let subst,metasenv,t',ugraph1 = - aux metasenv subst n context t ugraph in - subst,metasenv,(t'::appl),ugraph1 - ) (subst,metasenv,[],ugraph) l - in - subst,metasenv,(C.Appl (List.rev revl')),ugraph1 - | C.Const (uri,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1 - | C.MutInd (uri,i,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1 - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1 - | C.MutCase (sp,i,outt,t,pl) -> - let subst,metasenv,outt',ugraph1 = - aux metasenv subst n context outt ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst n context t ugraph1 in - let subst,metasenv,revpl',ugraph3 = - List.fold_left - (fun (subst,metasenv,pl,ugraph) t -> - let subst,metasenv,t',ugraph1 = - aux metasenv subst n context t ugraph in - subst,metasenv,(t'::pl),ugraph1 - ) (subst,metasenv,[],ugraph2) pl - in - subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3 - (* TASSI: not sure this is serial *) - | C.Fix (i,fl) -> -(*CSC: not implemented - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) - fl - in - C.Fix (i, substitutedfl) -*) - subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph - | C.CoFix (i,fl) -> -(*CSC: not implemented - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) - fl - in - C.CoFix (i, substitutedfl) - -*) - subst,metasenv,(CicSubstitution.lift 1 t'), ugraph - - and aux_exp_named_subst metasenv subst n context ens ugraph = - List.fold_right - (fun (uri,t) (subst,metasenv,l,ugraph) -> - let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in - subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph) - in - let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in - let fresh_name = - FreshNamesGenerator.mk_fresh_name ~subst - metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty - in - let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in - let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in - subst, metasenv, t'', ugraph2 -in profiler_beta_expand.HExtlib.profile foo () - - -and beta_expand_many test_equality_only metasenv subst context t args ugraph = - let _,subst,metasenv,hd,ugraph = - List.fold_right - (fun arg (num,subst,metasenv,t,ugraph) -> - let subst,metasenv,t,ugraph1 = - beta_expand num test_equality_only - metasenv subst context t arg ugraph - in - num+1,subst,metasenv,t,ugraph1 - ) args (1,subst,metasenv,t,ugraph) - in - subst,metasenv,hd,ugraph - -and warn_if_not_unique xxx car1 car2 = - let unopt = - function - | Some (_,Cic.Appl(Cic.Const(u,_)::_)) -> UriManager.string_of_uri u - | Some (_,t) -> CicPp.ppterm t - | None -> "id" - in - match xxx with - | [] -> () - | _ -> - HLog.warn - ("There are "^string_of_int (List.length xxx + 1)^ - " minimal joins of "^ CoercDb.string_of_carr car1^" and "^ - CoercDb.string_of_carr car2^": " ^ - String.concat " and " - (List.map - (fun (m2,_,c2,c2') -> - " via "^CoercDb.string_of_carr m2^" via "^unopt c2^" + "^unopt c2') - xxx)) - -(* NUOVA UNIFICAZIONE *) -(* A substitution is a (int * Cic.term) list that associates a - metavariable i with its body. - A metaenv is a (int * Cic.term) list that associate a metavariable - i with is type. - fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back - a new substitution which is _NOT_ unwinded. It must be unwinded before - applying it. *) - -and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let t1 = deref subst t1 in - let t2 = deref subst t2 in - let (&&&) a b = (a && b) || ((not a) && (not b)) in -(* let bef = Sys.time () in *) - let b,ugraph = - if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then - false,ugraph - else -let foo () = - R.are_convertible ~subst ~metasenv context t1 t2 ugraph -in profiler_are_convertible.HExtlib.profile foo () - in -(* let aft = Sys.time () in -if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ -CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ -CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *) - if b then - subst, metasenv, ugraph - else - match (t1, t2) with - | (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> - let _,subst,metasenv,ugraph1 = - (try - List.fold_left2 - (fun (j,subst,metasenv,ugraph) t1 t2 -> - match t1,t2 with - None,_ - | _,None -> j+1,subst,metasenv,ugraph - | Some t1', Some t2' -> - (* First possibility: restriction *) - (* Second possibility: unification *) - (* Third possibility: convertibility *) - let b, ugraph1 = - R.are_convertible - ~subst ~metasenv context t1' t2' ugraph - in - if b then - j+1,subst,metasenv, ugraph1 - else - (try - let subst,metasenv,ugraph2 = - fo_unif_subst - test_equality_only - subst context metasenv t1' t2' ugraph - in - j+1,subst,metasenv,ugraph2 - with - Uncertain _ - | UnificationFailure _ -> -debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); - let metasenv, subst = - CicMetaSubst.restrict - subst [(n,j)] metasenv in - j+1,subst,metasenv,ugraph1) - ) (1,subst,metasenv,ugraph) ln lm - with - Exit -> - raise - (UnificationFailure (lazy "1")) - (* - (sprintf - "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2))) *) - | Invalid_argument _ -> - raise - (UnificationFailure (lazy "2"))) - (* - (sprintf - "Error trying to unify %s with %s: the lengths of the two local contexts do not match." - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) *) - in subst,metasenv,ugraph1 - | (C.Meta (n,_), C.Meta (m,_)) when n>m -> - fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph - | (C.Meta (n,l), t) - | (t, C.Meta (n,l)) -> - let swap = - match t1,t2 with - C.Meta (n,_), C.Meta (m,_) when n < m -> false - | _, C.Meta _ -> false - | _,_ -> true - in - let lower = fun x y -> if swap then y else x in - let upper = fun x y -> if swap then x else y in - let fo_unif_subst_ordered - test_equality_only subst context metasenv m1 m2 ugraph = - fo_unif_subst test_equality_only subst context metasenv - (lower m1 m2) (upper m1 m2) ugraph - in - begin - let subst,metasenv,ugraph1 = - let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in - (try - let tyt,ugraph1 = - type_of_aux' metasenv subst context t ugraph - in - fo_unif_subst - test_equality_only - subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 - with - UnificationFailure _ as e -> raise e - | Uncertain msg -> raise (UnificationFailure msg) - | AssertFailure _ -> - debug_print (lazy "siamo allo huge hack"); - (* TODO huge hack!!!! - * we keep on unifying/refining in the hope that - * the problem will be eventually solved. - * In the meantime we're breaking a big invariant: - * the terms that we are unifying are no longer well - * typed in the current context (in the worst case - * we could even diverge) *) - (subst, metasenv,ugraph)) in - let t',metasenv,subst = - try - CicMetaSubst.delift n subst context metasenv l t - with - (CicMetaSubst.MetaSubstFailure msg)-> - raise (UnificationFailure msg) - | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) - in - let t'',ugraph2 = - match t' with - C.Sort (C.Type u) when not test_equality_only -> - let u' = CicUniv.fresh () in - let s = C.Sort (C.Type u') in - (try - let ugraph2 = - CicUniv.add_ge (upper u u') (lower u u') ugraph1 - in - s,ugraph2 - with - CicUniv.UniverseInconsistency msg -> - raise (UnificationFailure msg)) - | _ -> t',ugraph1 - in - (* Unifying the types may have already instantiated n. Let's check *) - try - let (_, oldt,_) = CicUtil.lookup_subst n subst in - let lifted_oldt = S.subst_meta l oldt in - fo_unif_subst_ordered - test_equality_only subst context metasenv t lifted_oldt ugraph2 - with - CicUtil.Subst_not_found _ -> - let (_, context, ty) = CicUtil.lookup_meta n metasenv in - let subst = (n, (context, t'',ty)) :: subst in - let metasenv = - List.filter (fun (m,_,_) -> not (n = m)) metasenv in - subst, metasenv, ugraph2 - end - | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) - | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) -> - if UriManager.eq uri1 uri2 then - fo_unif_subst_exp_named_subst test_equality_only subst context metasenv - exp_named_subst1 exp_named_subst2 ugraph - else - raise (UnificationFailure (lazy - (sprintf - "Can't unify %s with %s due to different constants" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> - if UriManager.eq uri1 uri2 && i1 = i2 then - fo_unif_subst_exp_named_subst - test_equality_only - subst context metasenv exp_named_subst1 exp_named_subst2 ugraph - else - raise (UnificationFailure - (lazy - (sprintf - "Can't unify %s with %s due to different inductive principles" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - | C.MutConstruct (uri1,i1,j1,exp_named_subst1), - C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> - if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then - fo_unif_subst_exp_named_subst - test_equality_only - subst context metasenv exp_named_subst1 exp_named_subst2 ugraph - else - raise (UnificationFailure - (lazy - (sprintf - "Can't unify %s with %s due to different inductive constructors" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - | (C.Implicit _, _) | (_, C.Implicit _) -> assert false - | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only - subst context metasenv te t2 ugraph - | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only - subst context metasenv t1 te ugraph - | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> - let subst',metasenv',ugraph1 = - fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph - in - fo_unif_subst test_equality_only - subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 - | (C.LetIn (_,s1,ty1,t1), t2) - | (t2, C.LetIn (_,s1,ty1,t1)) -> - fo_unif_subst - test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph - | (C.Appl l1, C.Appl l2) -> - (* andrea: this case should be probably rewritten in the - spirit of deref *) - (match l1,l2 with - | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j -> - (try - List.fold_left2 - (fun (subst,metasenv,ugraph) t1 t2 -> - fo_unif_subst - test_equality_only subst context metasenv t1 t2 ugraph) - (subst,metasenv,ugraph) l1 l2 - with (Invalid_argument msg) -> - raise (UnificationFailure (lazy msg))) - | C.Meta (i,l)::args, _ when not(exists_a_meta args) -> - (* we verify that none of the args is a Meta, - since beta expanding with respoect to a metavariable - makes no sense *) - (* - (try - let (_,t,_) = CicUtil.lookup_subst i subst in - let lifted = S.subst_meta l t in - let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in - fo_unif_subst - test_equality_only - subst context metasenv reduced t2 ugraph - with CicUtil.Subst_not_found _ -> *) - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - test_equality_only metasenv subst context t2 args ugraph - in - fo_unif_subst test_equality_only subst context metasenv - (C.Meta (i,l)) beta_expanded ugraph1 - | _, C.Meta (i,l)::args when not(exists_a_meta args) -> - (* (try - let (_,t,_) = CicUtil.lookup_subst i subst in - let lifted = S.subst_meta l t in - let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in - fo_unif_subst - test_equality_only - subst context metasenv t1 reduced ugraph - with CicUtil.Subst_not_found _ -> *) - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - test_equality_only - metasenv subst context t1 args ugraph - in - fo_unif_subst test_equality_only subst context metasenv - (C.Meta (i,l)) beta_expanded ugraph1 - | _,_ -> - let lr1 = List.rev l1 in - let lr2 = List.rev l2 in - let rec - fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph = - match (l1,l2) with - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> - fo_unif_subst - test_equality_only subst context metasenv h1 h2 ugraph - | ([h],l) - | (l,[h]) -> - fo_unif_subst test_equality_only subst context metasenv - h (C.Appl (List.rev l)) ugraph - | ((h1::l1),(h2::l2)) -> - let subst', metasenv',ugraph1 = - fo_unif_subst - test_equality_only - subst context metasenv h1 h2 ugraph - in - fo_unif_l - test_equality_only subst' metasenv' (l1,l2) ugraph1 - in - (try - fo_unif_l - test_equality_only subst metasenv (lr1, lr2) ugraph - with - | UnificationFailure s - | Uncertain s as exn -> - (match l1, l2 with - (* {{{ pullback *) - | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), - (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when - CoercDb.is_a_coercion cc1 <> None && - CoercDb.is_a_coercion cc2 <> None && - not (UriManager.eq uri1 uri2) -> -(*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 inner_coerced ?(skip_non_c=false) t = - let t = CicMetaSubst.apply_subst subst t in - let rec aux c x t = - match t with - | Cic.Appl l -> - (match CoercGraph.coerced_arg l with - | None when skip_non_c -> - aux c (HExtlib.list_last l) - (HExtlib.list_last l) - | None -> c, x - | Some (t,_) -> aux (List.hd l) t t) - | _ -> c, x - in - aux (Cic.Implicit None) (Cic.Implicit None) t - in - let c1,last_tl1 = inner_coerced (Cic.Appl l1) in - let c2,last_tl2 = inner_coerced (Cic.Appl l2) in - let car1, car2 = - match - CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2 - with - | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2 - | _ -> assert false - in - let head1_c, head2_c = - match - CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2 - with - | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2 - | _ -> assert false - in - let unfold uri ens args = - let o, _ = - CicEnvironment.get_obj CicUniv.oblivion_ugraph uri - in - assert (ens = []); - match o with - | Cic.Constant (_,Some bo,_,_,_) -> - CicReduction.head_beta_reduce ~delta:false - (Cic.Appl (bo::args)) - | _ -> assert false - in - let conclude subst metasenv ugraph last_tl1' last_tl2' = - let subst',metasenv,ugraph = -(*DEBUGGING ONLY: -prerr_endline - ("conclude: " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ - " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context); -*) - fo_unif_subst test_equality_only subst context - metasenv last_tl1' last_tl2' ugraph - in - if subst = subst' then raise exn - else -(*DEBUGGING ONLY: -let subst,metasenv,ugrph as res = -*) - fo_unif_subst test_equality_only subst' context - metasenv (C.Appl l1) (C.Appl l2) ugraph -(*DEBUGGING ONLY: -in -(prerr_endline - ("OK: "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ - " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); -res) -*) - in -(*DEBUGGING ONLY: -prerr_endline (Printf.sprintf -"Pullback problem\nterm1: %s\nterm2: %s\ncar1: %s\ncar2: %s\nlast_tl1: %s -last_tl2: %s\nhead1_c: %s\nhead2_c: %s\n" -(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context) -(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context) -(CoercDb.string_of_carr car1) -(CoercDb.string_of_carr car2) -(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1 context) -(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2 context) -(CoercDb.string_of_carr head1_c) -(CoercDb.string_of_carr head2_c) -); -*) - 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 (Cic.Appl l1) (Cic.Appl l2) ugraph - | _ when CoercDb.eq_carr head1_c head2_c -> - (* composite VS composition + metas avoiding - * coercions not only in coerced position *) - if c1 <> cc1 && c2 <> cc2 then - conclude subst metasenv ugraph - last_tl1 last_tl2 - else - let l1, l2 = - if c1 = cc1 then - unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2) - else - Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2 - in - fo_unif_subst test_equality_only subst context - metasenv l1 l2 ugraph - | _ -> raise exn - else - let grow1 = - match last_tl1 with Cic.Meta _ -> true | _ -> false in - let grow2 = - match last_tl2 with Cic.Meta _ -> true | _ -> false in - if not (grow1 || grow2) then - let _,last_tl1 = - inner_coerced ~skip_non_c:true (Cic.Appl l1) in - let _,last_tl2 = - inner_coerced ~skip_non_c:true (Cic.Appl l2) in - conclude subst metasenv ugraph last_tl1 last_tl2 - else - let meets = - CoercGraph.meets - metasenv subst context (grow1,car1) (grow2,car2) - in - (match - HExtlib.list_findopt - (fun (carr,metasenv,to1,to2) meet_no -> - try - let last_tl1',(subst,metasenv,ugraph) = - match grow1,to1 with - | true,Some (last,coerced) -> - last, - fo_unif_subst test_equality_only subst context - metasenv coerced last_tl1 ugraph - | _ -> last_tl1,(subst,metasenv,ugraph) - in - let last_tl2',(subst,metasenv,ugraph) = - match grow2,to2 with - | true,Some (last,coerced) -> - last, - fo_unif_subst test_equality_only subst context - metasenv coerced last_tl2 ugraph - | _ -> last_tl2,(subst,metasenv,ugraph) - in - if meet_no > 0 then - HLog.warn ("Using pullback number " ^ string_of_int - meet_no); - Some - (conclude subst metasenv ugraph last_tl1' last_tl2') - with - | UnificationFailure _ - | Uncertain _ -> None) - meets - with - | Some x -> x - | None -> raise exn) - (* }}} pullback *) - (* {{{ 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 - types to any rigid term. However, the code is - duplicated in two places: inside applications and - outside them. Probably it would be better to - work with lambda-bar terms instead. *) - | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn - | (_, Cic.MutInd _::_) -> - let t1' = R.whd ~subst context t1 in - (match t1' with - C.Appl (C.MutInd _::_) -> - fo_unif_subst test_equality_only - subst context metasenv t1' t2 ugraph - | _ -> raise (UnificationFailure (lazy "88"))) - | (Cic.MutInd _::_,_) -> - let t2' = R.whd ~subst context t2 in - (match t2' with - C.Appl (C.MutInd _::_) -> - fo_unif_subst test_equality_only - subst context metasenv t1 t2' ugraph - | _ -> raise - (UnificationFailure - (lazy ("not a mutind :"^ - CicMetaSubst.ppterm ~metasenv subst t2 )))) - (* }}} elim H *) - | _ -> raise exn))) - | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> - let subst', metasenv',ugraph1 = - fo_unif_subst test_equality_only subst context metasenv outt1 outt2 - ugraph in - let subst'',metasenv'',ugraph2 = - fo_unif_subst test_equality_only subst' context metasenv' t1' t2' - ugraph1 in - (try - List.fold_left2 - (fun (subst,metasenv,ugraph) t1 t2 -> - fo_unif_subst - test_equality_only subst context metasenv t1 t2 ugraph - ) (subst'',metasenv'',ugraph2) pl1 pl2 - with - Invalid_argument _ -> - raise (UnificationFailure (lazy "6.1"))) - (* (sprintf - "Error trying to unify %s with %s: the number of branches is not the same." - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) *) - | (C.Rel _, _) | (_, C.Rel _) -> - if t1 = t2 then - subst, metasenv,ugraph - else - raise (UnificationFailure (lazy - (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) -> - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - test_equality_only metasenv subst context t2 args ugraph - in - fo_unif_subst test_equality_only subst context metasenv - (C.Meta (i,l)) beta_expanded ugraph1 - | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) -> - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - test_equality_only metasenv subst context t1 args ugraph - in - fo_unif_subst test_equality_only subst context metasenv - beta_expanded (C.Meta (i,l)) ugraph1 -(* Works iff there are no arguments applied to it; similar to the - case below - | (_, C.MutInd _) -> - let t1' = R.whd ~subst context t1 in - (match t1' with - C.MutInd _ -> - fo_unif_subst test_equality_only - subst context metasenv t1' t2 ugraph - | _ -> raise (UnificationFailure (lazy "8"))) -*) - | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - let subst',metasenv',ugraph1 = - fo_unif_subst true subst context metasenv s1 s2 ugraph - in - fo_unif_subst test_equality_only - subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 - | (C.Prod _, _) -> - (match CicReduction.whd ~subst context t2 with - | C.Prod _ as t2 -> - fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph - | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product")))) - | (_, C.Prod _) -> - (match CicReduction.whd ~subst context t1 with - | C.Prod _ as t1 -> - fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph - | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product")))) - | (_,_) -> - (* delta-beta reduction should almost never be a problem for - unification since: - 1. long computations require iota reduction - 2. it is extremely rare that a close term t1 (that could be unified - to t2) beta-delta reduces to t1' while t2 does not beta-delta - reduces in the same way. This happens only if one meta of t2 - occurs in head position during beta reduction. In this unluky - case too much reduction will be performed on t1 and unification - will surely fail. *) - let t1' = CicReduction.head_beta_reduce ~delta:true t1 in - let t2' = CicReduction.head_beta_reduce ~delta:true t2 in - if t1 = t1' && t2 = t2' then - raise (UnificationFailure - (lazy - (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - else - try - fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph - with - UnificationFailure _ - | Uncertain _ -> - raise (UnificationFailure - (lazy - (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - -and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv - exp_named_subst1 exp_named_subst2 ugraph -= - try - List.fold_left2 - (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) -> - assert (uri1=uri2) ; - fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph - ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2 - with - Invalid_argument _ -> - let print_ens ens = - String.concat " ; " - (List.map - (fun (uri,t) -> - UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t) - ) ens) - in - raise (UnificationFailure (lazy (sprintf - "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))) - -(* A substitution is a (int * Cic.term) list that associates a *) -(* metavariable i with its body. *) -(* metasenv is of type Cic.metasenv *) -(* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *) -(* a new substitution which is already unwinded and ready to be applied and *) -(* a new metasenv in which some hypothesis in the contexts of the *) -(* metavariables may have been restricted. *) -let fo_unif metasenv context t1 t2 ugraph = - fo_unif_subst false [] context metasenv t1 t2 ugraph ;; - -let enrich_msg msg subst context metasenv t1 t2 ugraph = - lazy ( - if verbose then - sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" - (CicMetaSubst.ppterm ~metasenv subst t1) - (try - let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in - CicPp.ppterm ty_t1 - with - | UnificationFailure s - | Uncertain s - | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppterm ~metasenv subst t2) - (try - let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in - CicPp.ppterm ty_t2 - with - | UnificationFailure s - | Uncertain s - | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppcontext ~metasenv subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg) - else - sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" - (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context) - (try - let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in - CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context - with - | UnificationFailure s - | Uncertain s - | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context) - (try - let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in - CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context - with - | UnificationFailure s - | Uncertain s - | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppcontext ~metasenv subst context) - ("OMITTED" (*CicMetaSubst.ppmetasenv subst metasenv*)) - (Lazy.force msg) - ) - -let fo_unif_subst subst context metasenv t1 t2 ugraph = - try - fo_unif_subst false subst context metasenv t1 t2 ugraph - with - | AssertFailure msg -> - raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) - | UnificationFailure msg -> - raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) -;; diff --git a/matita/components/cic_unification/cicUnification.mli b/matita/components/cic_unification/cicUnification.mli deleted file mode 100644 index e1a6c2899..000000000 --- a/matita/components/cic_unification/cicUnification.mli +++ /dev/null @@ -1,58 +0,0 @@ -(* 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/. - *) - -exception UnificationFailure of string Lazy.t;; -exception Uncertain of string Lazy.t;; -exception AssertFailure of string Lazy.t;; - -(* fo_unif metasenv context t1 t2 *) -(* unifies [t1] and [t2] in a context [context]. *) -(* Only the metavariables declared in [metasenv] *) -(* can be used in [t1] and [t2]. *) -(* The returned substitution can be directly *) -(* withouth first unwinding it. *) -val fo_unif : - Cic.metasenv -> Cic.context -> - Cic.term -> Cic.term -> CicUniv.universe_graph -> - Cic.substitution * Cic.metasenv * CicUniv.universe_graph - -(* fo_unif_subst metasenv subst context t1 t2 *) -(* unifies [t1] and [t2] in a context [context] *) -(* and with [subst] as the current substitution *) -(* (i.e. unifies ([subst] [t1]) and *) -(* ([subst] [t2]) in a context *) -(* ([subst] [context]) using the metasenv *) -(* ([subst] [metasenv]) *) -(* Only the metavariables declared in [metasenv] *) -(* can be used in [t1] and [t2]. *) -(* [subst] and the substitution returned are not *) -(* unwinded. *) -(*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la - cosa all'apply_subst!!!*) -val fo_unif_subst : - Cic.substitution -> Cic.context -> Cic.metasenv -> - Cic.term -> Cic.term -> CicUniv.universe_graph -> - Cic.substitution * Cic.metasenv * CicUniv.universe_graph - diff --git a/matita/components/cic_unification/coercGraph.ml b/matita/components/cic_unification/coercGraph.ml deleted file mode 100644 index 9f953ccf8..000000000 --- a/matita/components/cic_unification/coercGraph.ml +++ /dev/null @@ -1,332 +0,0 @@ -(* 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 - | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list - | NoCoercion - | NotHandled - -let debug = false -let debug_print s = if debug then prerr_endline (Lazy.force s) else () - -let saturate_coercion ul metasenv subst context = - let cl = - List.map - (fun u,saturations -> - let t = CicUtil.term_of_uri u in - let arity = - match CoercDb.is_a_coercion t with - | Some (_,CoercDb.Fun i,_,_,_) -> i - | _ -> 0 - in - arity,t,saturations) ul - in - let freshmeta = CicMkImplicit.new_meta metasenv subst in - List.map - (fun (arity,c,saturations) -> - let ty,_ = - CicTypeChecker.type_of_aux' ~subst metasenv context c - CicUniv.oblivion_ugraph in - let _,metasenv,args,lastmeta = - TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - metasenv, Cic.Meta (lastmeta - saturations - 1,irl), - match args with - [] -> c - | _ -> Cic.Appl (c::args) - ) cl -;; - -(* searches a coercion fron src to tgt in the !coercions list *) -let look_for_coercion_carr metasenv subst context src tgt = - let is_dead = function CoercDb.Dead -> true | _ -> false in - let pp_l s l = - match l with - | [] -> - debug_print - (lazy - (sprintf ":-( coercion non trovata[%s] da %s a %s" s - (CoercDb.string_of_carr src) - (CoercDb.string_of_carr tgt))); - | _::_ -> - debug_print (lazy ( - sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s - (List.length l) - (CoercDb.string_of_carr src) - (CoercDb.string_of_carr tgt))); - in - if is_dead src || is_dead tgt then NotHandled - else - let l = - CoercDb.find_coercion - (fun (s,t) -> - CoercDb.eq_carr s src && - match t, tgt with - | CoercDb.Sort Cic.Prop, CoercDb.Sort Cic.Prop - | CoercDb.Sort Cic.Set, CoercDb.Sort Cic.Set - | CoercDb.Sort _, CoercDb.Sort (Cic.Type _|Cic.CProp _) -> true - | _ -> CoercDb.eq_carr t tgt) - in - pp_l "precise" l; - (match l with - | [] -> - let l = - CoercDb.find_coercion - (fun (_,t) -> CoercDb.eq_carr t tgt) - in - pp_l "approx" l; - (match l with - | [] -> NoCoercion - | ul -> - SomeCoercionToTgt (saturate_coercion ul metasenv subst context)) - | ul -> SomeCoercion (saturate_coercion ul metasenv subst context)) -;; - -let rec count_pi c s t = - match CicReduction.whd ~delta:false ~subst:s c t with - | Cic.Prod (_,_,t) -> 1 + count_pi c s t - | _ -> 0 -;; - -let look_for_coercion metasenv subst context src tgt = - let src_arity = count_pi context subst src in - let tgt_arity = count_pi context subst tgt in - let src_carr = CoercDb.coerc_carr_of_term src src_arity in - let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in - look_for_coercion_carr metasenv subst context src_carr tgt_carr - -let source_of t = - match CoercDb.is_a_coercion t with - | None -> assert false - | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s - | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u - | Some _ -> assert false (* t must be a coercion not to funclass *) -;; - -let generate_dot_file fmt = - let l = CoercDb.to_list (CoercDb.dump ()) in - let module Pp = GraphvizPp.Dot in - if List.exists (fun (_,t,_) -> CoercDb.string_of_carr t = "Type") l then - Format.fprintf fmt "subgraph cluster_rest { style=\"filled\"; - color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n" - (" - - - "^ - String.concat "" - (List.map - (fun (src,tgt,ul) -> - let src_name = CoercDb.string_of_carr src in - let tgt_name = CoercDb.string_of_carr tgt in - let names = - List.map (fun (u,_,_) -> - UriManager.name_of_uri u ^ - (match CicEnvironment.get_obj CicUniv.empty_ugraph u with - | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _ - when List.exists ((=) (`Flavour `Variant)) attrs -> "*" - | _ -> "") - ) ul - in - "") - (List.sort (fun (x,y,_) (x1,y1,_) -> - let rc = compare x x1 in - if rc = 0 then compare y y1 else rc) l)) - ^ "
SourceTargetArrows
" ^ src_name ^ "" ^ tgt_name ^ "" ^ - String.concat ", " names ^ "
") - (String.concat ";" ["Type"]); - let type_uri u = - let ty, _ = - CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u) - CicUniv.oblivion_ugraph - in - ty - in - let deref_coercion u = - match CicEnvironment.get_obj CicUniv.empty_ugraph u with - | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _ - when List.exists ((=) (`Flavour `Variant)) attrs -> - UriManager.name_of_uri u' - | Cic.Constant (_,Some t,_,_,_), _ when - let rec is_id = function - | Cic.Lambda (_,_,t) -> is_id t - | Cic.Rel _ -> true - | _ -> false - in is_id t -> "ID" - | _ -> UriManager.name_of_uri u - in - List.iter - (fun (src, tgt, ul) -> - List.iter - (fun (u,saturations,cpos) -> - let ty = type_uri u in - let src_name, tgt_name = - let rec aux ctx cpos t = - match cpos, t with - | 0,Cic.Prod (_,src,tgt) -> - CicPp.pp src ctx, tgt, (Some (Cic.Name "_")::ctx) - | 0,t -> CicPp.pp t ctx, Cic.Implicit None, [] - | n,Cic.Prod (_,_,tgt) -> aux (Some (Cic.Name "_")::ctx) (n-1) tgt - | _ -> assert false - in - let ssrc, rest, ctx = aux [] cpos ty in - let stgt, rest, _ = aux ctx saturations rest in - let stgt = - if rest <> Cic.Implicit None then - match tgt with - | CoercDb.Fun _ -> CoercDb.string_of_carr tgt - | _ -> assert false - else - stgt - in - ssrc, stgt - in - Pp.node src_name fmt; - Pp.node tgt_name fmt; - Pp.edge src_name tgt_name - ~attrs:[ "label", - (deref_coercion u ^ - if saturations = 0 then "" - else "(" ^ string_of_int saturations ^ ")"); - "href", UriManager.string_of_uri u ] - fmt) - ul) - l; -;; - -let coerced_arg l = - match l with - | [] | [_] -> None - | c::tl -> - match CoercDb.is_a_coercion c with - | None -> None - | Some (_,_,_,_,cpos) -> - if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None -;; - -(************************* meet calculation stuff ********************) -let eq_uri_opt u1 u2 = - match u1,u2 with - | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2 - | None,Some _ | Some _, None -> false - | None, None -> true -;; - -let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;; - -let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) = - CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22 -;; - -let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;; - -let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;; - -let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;; - -(* : carr -> (carr * uri option) where the option is always Some *) -let get_coercions_to carr = - let l = CoercDb.to_list (CoercDb.dump ()) in - let splat_coercion_to carr (src,tgt,cl) = - if CoercDb.eq_carr tgt carr then Some (splat src cl) else None - in - let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in - l -;; - -(* : carr -> (carr * uri option) where the option is always Some *) -let get_coercions_from carr = - let l = CoercDb.to_list (CoercDb.dump ()) in - let splat_coercion_from carr (src,tgt,cl) = - if CoercDb.eq_carr src carr then Some (splat tgt cl) else None - in - List.flatten (HExtlib.filter_map (splat_coercion_from carr) l) -;; - -(* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 } - * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *) -let intersect l1 l2 = - let is_in_l1 (x,u2) = - HExtlib.filter_map - (fun (src,u1) -> - if CoercDb.eq_carr x src then Some (src,u1,u2) else None) - l1 - in - uniq2 (List.flatten (List.map is_in_l1 l2)) -;; - -(* grow tgt gives all the (src,u) such that u:tgt->src *) -let grow tgt = - uniq ((tgt,None)::(get_coercions_to tgt)) -;; - -let lb (c,_,_) = - let l = get_coercions_from c in - fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l -;; - -(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements - * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *) -let rec min acc skipped = function - | c::tl -> - if List.exists (lb c) (tl@acc) - then min acc (c::skipped) tl else min (c::acc) skipped tl - | [] -> acc, skipped -;; - - -let sort l = - let low, high = min [] [] l in low @ high -;; - -let meets metasenv subst context (grow_left,left) (grow_right,right) = - let saturate metasenv uo = - match uo with - | None -> metasenv, None - | Some u -> - match saturate_coercion [u] metasenv subst context with - | [metasenv, sat, last] -> metasenv, Some (sat, last) - | _ -> assert false - in - List.map - (fun (c,uo1,uo2) -> - let metasenv, uo1 = saturate metasenv uo1 in - let metasenv, uo2 = saturate metasenv uo2 in - c,metasenv, uo1, uo2) - (sort (intersect - (if grow_left then grow left else [left,None]) - (if grow_right then grow right else [right,None]))) -;; - -(* EOF *) diff --git a/matita/components/cic_unification/coercGraph.mli b/matita/components/cic_unification/coercGraph.mli deleted file mode 100644 index 44f30d278..000000000 --- a/matita/components/cic_unification/coercGraph.mli +++ /dev/null @@ -1,56 +0,0 @@ -(* 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 - | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list - | NoCoercion - | NotHandled - -val look_for_coercion : - Cic.metasenv -> Cic.substitution -> Cic.context -> - Cic.term -> Cic.term -> coercion_search_result - -val source_of: Cic.term -> Cic.term - -val generate_dot_file: Format.formatter -> unit - -(* given the Appl contents returns the argument of the head coercion *) -val coerced_arg: Cic.term list -> (Cic.term * int) option - -(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *) -val meets : - Cic.metasenv -> Cic.substitution -> Cic.context -> - bool * CoercDb.coerc_carr -> bool * CoercDb.coerc_carr -> - (CoercDb.coerc_carr * Cic.metasenv * - (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list - diff --git a/matita/components/cic_unification/termUtil.ml b/matita/components/cic_unification/termUtil.ml deleted file mode 100644 index 1886b25d7..000000000 --- a/matita/components/cic_unification/termUtil.ml +++ /dev/null @@ -1,89 +0,0 @@ -(* 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 ?(delta=true) 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 ~delta 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 diff --git a/matita/components/cic_unification/termUtil.mli b/matita/components/cic_unification/termUtil.mli deleted file mode 100644 index c851bb588..000000000 --- a/matita/components/cic_unification/termUtil.mli +++ /dev/null @@ -1,37 +0,0 @@ -(* 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: - ?delta: bool -> (* default true *) - int -> Cic.metasenv -> Cic.context -> Cic.term -> int -> - Cic.term * Cic.metasenv * Cic.term list * int diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index b122366c1..23e713915 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -320,31 +320,6 @@ let add_coercions_of_lemmas lemmas status = status#set_coercions (CoercDb.dump ()), lemmas -let eval_coercion status ~add_composites uri arity saturations = - let uri = - try CicUtil.uri_of_term uri - with Invalid_argument _ -> - raise (Invalid_argument "coercion can only be constants/constructors") - in - let status, lemmas = - GrafiteSync.add_coercion ~add_composites - ~pack_coercion_obj:CicRefine.pack_coercion_obj - status uri arity saturations status#baseuri in - let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in - let status = GrafiteTypes.add_moo_content [moo_content] status in - add_coercions_of_lemmas lemmas status - -let eval_prefer_coercion status c = - let uri = - try CicUtil.uri_of_term c - with Invalid_argument _ -> - raise (Invalid_argument "coercion can only be constants/constructors") - in - let status = GrafiteSync.prefer_coercion status uri in - let moo_content = GrafiteAst.PreferCoercion (HExtlib.dummy_floc,c) in - let status = GrafiteTypes.add_moo_content [moo_content] status in - status, `Old [] - let eval_ng_punct (_text, _prefix_len, punct) = match punct with | GrafiteAst.Dot _ -> NTactics.dot_tac @@ -709,13 +684,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status,cmd = disambiguate_command status (text,prefix_len,cmd) in let status,uris = match cmd with - | GrafiteAst.PreferCoercion (loc, coercion) -> - eval_prefer_coercion status coercion - | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> - let res,uris = - eval_coercion status ~add_composites uri arity saturations - in - res,`Old uris | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,`Old [] diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index 584623e6a..ad51250d8 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -157,44 +157,6 @@ let txt_of_cic_term ~map_unicode_to_tex size metasenv context t = metasenv fake_sequent ;; -ignore ( - CicMetaSubst.set_ppterm_in_context - (fun ~metasenv subst term context -> - try - let context' = CicMetaSubst.apply_subst_context subst context in - let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - let term' = CicMetaSubst.apply_subst subst term in - let res = - txt_of_cic_term - ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - 30 metasenv context' term' in - if String.contains res '\n' then - "\n" ^ res ^ "\n" - else - res - with - Sys.Break as exn -> raise exn - | exn -> - "[[ Exception raised during pretty-printing: " ^ - (try - Printexc.to_string exn - with - Sys.Break as exn -> raise exn - | _ -> "<>" - ) ^ " ]] " ^ - (CicMetaSubst.use_low_level_ppterm_in_context := true; - try - let res = - CicMetaSubst.ppterm_in_context ~metasenv subst term context - in - CicMetaSubst.use_low_level_ppterm_in_context := false; - res - with - exc -> - CicMetaSubst.use_low_level_ppterm_in_context := false; - raise exc)) -);; - (****************************************************************************) (* txt_of_cic_object: IMPROVE ME *) @@ -350,68 +312,6 @@ let discharge_uri params uri = let discharge_name s = s ^ "_discharged" -let txt_of_inline_uri ~map_unicode_to_tex params suri = -(* - Ds.debug := true; -*) - let print_exc = Printexc.to_string in - let dbd = LibraryDb.instance () in - let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in - let error uri e = - let msg = - Printf.sprintf - "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" - (UM.string_of_uri uri) e - in - Printf.eprintf "%s\n" msg; - GrafiteTypes.command_error msg - in - let map uri = - Librarian.time_stamp "AT: BEGIN MAP"; - try -(* FG: for now the explicit variables must be discharged *) - let do_it obj = - let r = txt_of_cic_object ~map_unicode_to_tex 78 params obj in - Librarian.time_stamp "AT: END MAP "; r - in - let obj, real = - let s = UM.string_of_uri uri in - if Str.string_match matita_prefix s 0 then begin - Librarian.time_stamp "AT: GETTING OBJECT"; - let obj, _ = E.get_obj Un.default_ugraph uri in - Librarian.time_stamp "AT: DONE "; - obj, true - end else - Ds.discharge_uri discharge_name (discharge_uri params) uri - in - if real then do_it obj else - let newuri = discharge_uri params uri in - let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in - do_it obj - with - | TC.TypeCheckerFailure s -> - error uri ("failure : " ^ Lazy.force s) - | TC.AssertFailure s -> - error uri ("assert : " ^ Lazy.force s) - | E.Object_not_found u -> - error uri ("not found: " ^ UM.string_of_uri u) - | e -> error uri (print_exc e) - in - String.concat "" (List.map map sorted_uris) - -let txt_of_inline_macro ~map_unicode_to_tex params name = - let suri = - if Librarian.is_uri name then name else - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" - in - let _, baseuri, _, _ = - Librarian.baseuri_of_script ~include_paths name - in - baseuri ^ "/" - in - txt_of_inline_uri ~map_unicode_to_tex params suri - let txt_of_macro ~map_unicode_to_tex metasenv context m = GrafiteAstPp.pp_macro ~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context) diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli index 1b1b749e7..b5b596927 100644 --- a/matita/matita/applyTransformation.mli +++ b/matita/matita/applyTransformation.mli @@ -114,11 +114,6 @@ val txt_of_cic_object_all: (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *) -(* params, uri or baseuri *) -val txt_of_inline_macro: - map_unicode_to_tex:bool -> GrafiteAst.inline_param list -> string -> - string - val txt_of_macro: map_unicode_to_tex:bool -> Cic.metasenv -> diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index e9909890e..b145c157a 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -148,7 +148,7 @@ let _ = *) addDebugSeparator (); addDebugCheckbox "high level pretty printer" ~init:true - (fun mi () -> CicMetaSubst.use_low_level_ppterm_in_context := mi#active); + (fun mi () -> assert false (* MATITA 1.0 *)); addDebugSeparator (); addDebugItem "always show all disambiguation errors" (fun _ -> MatitaGui.all_disambiguation_passes := true); diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml index 260ac2f29..8ccd85b2e 100644 --- a/matita/matita/matitaExcPp.ml +++ b/matita/matita/matitaExcPp.ml @@ -134,9 +134,6 @@ let rec to_string = sprintf "format/version mismatch for file '%s', please recompile it'" fname | Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s - | CicRefine.RefineFailure msg - | CicRefine.AssertFailure msg -> - None, "Refiner error: " ^ Lazy.force msg | NCicRefiner.RefineFailure msg -> None, "NRefiner failure: " ^ snd (Lazy.force msg) | NCicRefiner.Uncertain msg -> diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index e82a01650..5881c6d83 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -1023,12 +1023,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let status = (MatitaScript.current ())#grafite_status in NCicCoercion.generate_dot_file status fmt; Pp.trailer fmt; - Pp.header - ~name:"OLDCoercions" - ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] - ~edge_attrs:["fontsize", "10"] fmt; - CoercGraph.generate_dot_file fmt; - Pp.trailer fmt; Pp.raw "@." fmt; close_out oc; if tred then @@ -1042,8 +1036,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) object (self) inherit scriptAccessor - (* Whelp bar queries *) - val mutable gviz_graph = MetadataDeps.DepGraph.dummy val mutable gviz_uri = UriManager.uri_of_string "cic:/dummy.con"; diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 9fa039b31..b6ec2a51f 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -224,14 +224,6 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); [(grafite_status#set_proof_status No_proof), parsed_text ],"", parsed_text_length *) - | TA.Inline (_, suri, params) -> - let str = "\n\n" ^ - ApplyTransformation.txt_of_inline_macro - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - params suri - in - [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text skipped_txt nonskipped_txt diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index 7869482ba..583911e3e 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -70,13 +70,6 @@ let dump f = let nl () = output_string och (pp_statement nl_ast) in MatitaMisc.out_preamble och; let grafite_parser_cb = function - | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) -> - let str = - ApplyTransformation.txt_of_inline_macro params uri - ~map_unicode_to_tex: - (Helm_registry.get_bool "matita.paste_unicode_as_tex") - in - output_string och str | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> () | stm -> output_string och (pp_statement stm); nl (); nl ()