+++ /dev/null
-requires="helm-cic_proof_checking helm-library"
-version="0.0.1"
-archive(byte)="cic_unification.cma"
-archive(native)="cic_unification.cmxa"
-linkopts=""
-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"
ng_kernel \
acic_content \
grafite \
- cic_unification \
disambiguation \
ng_kernel \
ng_refiner \
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* 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)
+++ /dev/null
-(* 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
-*)
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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)
-
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-open Printf
-
-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: *)
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id: 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
-;;
-
-
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id: 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
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-open Printf
-
-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<BEGIN>%s\n<END>" (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<BEGIN>%s\n<END>" (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<BEGIN>%s\n<END>" (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<BEGIN>%s\n<END>" (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))
-;;
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-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
-
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-open Printf;;
-
-type coercion_search_result =
- (* metasenv, last coercion argument, fully saturated coercion *)
- (* to apply the coercion it is sufficient to unify the last coercion
- argument (that is a Meta) with the term to be coerced *)
- | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
- | 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"
- ("<FONT POINT-SIZE=\"10.0\"><TABLE BORDER=\"1\" CELLBORDER=\"1\" >
- <TR><TD BGCOLOR=\"gray95\">Source</TD>
- <TD BGCOLOR=\"gray95\">Target</TD>
- <TD BGCOLOR=\"gray95\">Arrows</TD></TR>"^
- String.concat "</TR>"
- (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
- "<TR><TD>" ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
- String.concat ", " names ^ "</TD>")
- (List.sort (fun (x,y,_) (x1,y1,_) ->
- let rc = compare x x1 in
- if rc = 0 then compare y y1 else rc) l))
- ^ "</TR></TABLE></FONT>")
- (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 *)
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id$ *)
-
-(* This module implements the Query interface to the Coercion Graph *)
-
-type coercion_search_result =
- (* metasenv, last coercion argument, fully saturated coercion *)
- (* to apply the coercion it is sufficient to unify the last coercion
- argument (that is a Meta) with the term to be coerced *)
- | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
- | 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
-
+++ /dev/null
-(* Copyright (C) 2002, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id: proofEngineHelpers.ml 7022 2006-11-15 19:47:41Z fguidi $ *)
-
-(* saturate_term newmeta metasenv context ty goal_arity *)
-(* Given a type [ty] (a backbone), it returns its suffix of length *)
-(* [goal_arity] head and a new metasenv in which there is new a META for each *)
-(* hypothesis, a list of arguments for the new applications and the index of *)
-(* the last new META introduced. The nth argument in the list of arguments is *)
-(* just the nth new META. *)
-let saturate_term ?(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
+++ /dev/null
-(* Copyright (C) 2000-2002, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* $Id: proofEngineHelpers.ml 7022 2006-11-15 19:47:41Z fguidi $ *)
-
-(* saturate_term newmeta metasenv context ty goal_arity *)
-(* Given a type [ty] (a backbone), it returns its suffix of length *)
-(* [goal_arity] head and a new metasenv in which there is new a META for each *)
-(* hypothesis, a list of arguments for the new applications and the index of *)
-(* the last new META introduced. The nth argument in the list of arguments is *)
-(* just the nth new META. *)
-val saturate_term:
- ?delta: bool -> (* default true *)
- int -> Cic.metasenv -> Cic.context -> Cic.term -> int ->
- Cic.term * Cic.metasenv * Cic.term list * int
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
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 []
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
- | _ -> "<<exception raised pretty-printing the exception>>"
- ) ^ " ]] " ^
- (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 *)
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)
(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 ->
*)
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);
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 ->
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
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";
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
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 ()
projects / helm.git / commitdiff