| C.Meta _ ->
prerr_endline "Cic2acic: string_of_sort applied to a meta" ;
"?"
- | _ -> assert false
+ | t ->
+prerr_endline ("Cic2acic: string_of_sort applied to: " ^ CicPp.ppterm t) ;
+ assert false
in
let ainnertypes,innertype,innersort,expected_available =
(*CSC: Here we need the algorithm for Coscoy's double type-inference *)
in
C.AVar (fresh_id'', uri,exp_named_subst')
| C.Meta (n,l) ->
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> n = m) metasenv
- in
+ let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
xxx_add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
| C.Meta (n,l) ->
(* Let's visit all the subterms that will not be visited later *)
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> n = m) metasenv
- in
+ let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
let lifted_canonical_context =
let rec aux i =
function
| _,_ -> assert false (* the term is not well typed!!! *)
) l lifted_canonical_context
in
- let (_,canonical_context,ty) =
- List.find (function (m,_,_) -> n = m) metasenv
- in
+ let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
(* Checks suppressed *)
CicSubstitution.lift_meta l ty
| C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
C.Var (uri,exp_named_subst')
| C.Meta (n,l) ->
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> n = m) metasenv
- in
- let l' =
+ let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
+ let l' =
List.map2
(fun ct t ->
match (ct, t) with
| C.Prod (name,s,t) ->
let sort1 = type_of_aux context s
and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
- sort_of_prod context (name,s) (sort1,sort2)
+ let res = sort_of_prod context (name,s) (sort1,sort2) in
+ res
| C.Lambda (n,s,t) ->
let sort1 = type_of_aux context s in
(match R.whd context sort1 with
(CicSubstitution.subst s
(type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
| C.Appl (he::tl) when List.length tl > 0 ->
- let hetype = type_of_aux context he
- and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
+ let hetype = type_of_aux context he in
+ let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (AssertFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
+cicMkImplicit.cmi: cicMetaSubst.cmi
cicUnification.cmi: cicMetaSubst.cmi
-cicMkImplicit.cmo: cicMkImplicit.cmi
-cicMkImplicit.cmx: cicMkImplicit.cmi
cicMetaSubst.cmo: cicMetaSubst.cmi
cicMetaSubst.cmx: cicMetaSubst.cmi
+cicMkImplicit.cmo: cicMkImplicit.cmi
+cicMkImplicit.cmx: cicMkImplicit.cmi
freshNamesGenerator.cmo: freshNamesGenerator.cmi
freshNamesGenerator.cmx: freshNamesGenerator.cmi
cicUnification.cmo: cicMetaSubst.cmi freshNamesGenerator.cmi \
PREDICATES =
INTERFACE_FILES = \
- cicMkImplicit.mli \
cicMetaSubst.mli \
+ cicMkImplicit.mli \
freshNamesGenerator.mli \
cicUnification.mli \
cicRefine.mli
open Printf
+let apply_subst_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 () =
+ prerr_endline (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
exception Uncertain of string
exception AssertFailure of string
+exception SubstNotFound of int
let debug_print = prerr_endline
-type substitution = (int * Cic.term) list
+type substitution = (int * (Cic.context * Cic.term)) list
+
+let lookup_subst n subst =
+ try
+ List.assoc n subst
+ with Not_found -> raise (SubstNotFound n)
(*** Functions to apply a substitution ***)
C.Var (uri, exp_named_subst')
| C.Meta (i, l) ->
(try
- let t = List.assoc i subst in
+ let (context, t) = lookup_subst i subst in
um_aux (S.lift_meta l t)
- with Not_found -> (* not constrained variable, i.e. free in subst*)
+ with SubstNotFound _ -> (* unconstrained variable, i.e. free in subst*)
let l' =
List.map (function None -> None | Some t -> Some (um_aux t)) l
in
| _ -> t'
end
in
- apply_subst_gen ~appl_fun
+ fun s t ->
+ incr apply_subst_counter;
+ apply_subst_gen ~appl_fun s t
;;
let rec apply_subst_context subst context =
+ incr apply_subst_context_counter;
+ context_length := !context_length + List.length context;
List.fold_right
(fun item context ->
match item with
context []
let apply_subst_metasenv subst metasenv =
+ incr apply_subst_metasenv_counter;
+ metasenv_length := !metasenv_length + List.length metasenv;
List.map
(fun (n, context, ty) ->
(n, apply_subst_context subst context, apply_subst subst ty))
(List.filter
- (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+ (fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv)
(***** Pretty printing functions ******)
let ppsubst subst =
String.concat "\n"
(List.map
- (fun (idx, term) -> Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
+ (fun (idx, (_, term)) ->
+ Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
subst)
;;
sprintf "%s |- ?%d: %s" context i
(ppterm_in_context subst t name_context))
(List.filter
- (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+ (fun (i, _, _) -> not (List.mem_assoc i subst))
metasenv))
(* From now on we recreate a kernel abstraction where substitutions are part of
* the calculus *)
let lift subst n term =
+ incr subst_counter;
let term = apply_subst subst term in
try
CicSubstitution.lift n term
raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
let subst subst t1 t2 =
+ incr subst_counter;
let t1 = apply_subst subst t1 in
let t2 = apply_subst subst t2 in
try
raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
let whd subst context term =
+ incr whd_counter;
let term = apply_subst subst term in
let context = apply_subst_context subst context in
try
Printexc.to_string e))
let are_convertible subst context t1 t2 =
+ incr are_convertible_counter;
let context = apply_subst_context subst context in
let t1 = apply_subst subst t1 in
let t2 = apply_subst subst t2 in
let tempi_subst = ref 0.0;;
let tempi_type_of_aux = ref 0.0;;
+ (* assumption: metasenv is already instantiated wrt subst *)
let type_of_aux' metasenv subst context term =
-let time1 = Unix.gettimeofday () in
+ let time1 = Unix.gettimeofday () in
let term = apply_subst subst term in
let context = apply_subst_context subst context in
- let metasenv =
- List.map
- (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
- (List.filter
- (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
- metasenv)
+(* let metasenv = apply_subst_metasenv subst metasenv in *)
+ let time2 = Unix.gettimeofday () in
+ let res =
+ try
+ CicTypeChecker.type_of_aux' metasenv context term
+ with CicTypeChecker.TypeCheckerFailure msg ->
+ raise (MetaSubstFailure ("Type checker failure: " ^ msg))
in
-let time2 = Unix.gettimeofday () in
-let res =
- try
- CicTypeChecker.type_of_aux' metasenv context term
- with CicTypeChecker.TypeCheckerFailure msg ->
- raise (MetaSubstFailure ("Type checker failure: " ^ msg))
-in
-let time3 = Unix.gettimeofday () in
- tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ;
- tempi_subst := !tempi_subst +. time2 -. time1 ;
- tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ;
- res
+ let time3 = Unix.gettimeofday () in
+ tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ;
+ tempi_subst := !tempi_subst +. time2 -. time1 ;
+ tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ;
+ res
(**** DELIFT ****)
(* the delift function takes in input a metavariable index, an ordered list of
with Occur ->
more_to_be_restricted, (i :: restricted), None :: tl')
in
- let (more_to_be_restricted, metasenv, subst) =
+ let (more_to_be_restricted, metasenv) = (* restrict metasenv *)
List.fold_right
- (fun (n, context, t) (more, metasenv, subst) ->
+ (fun (n, context, t) (more, metasenv) ->
let to_be_restricted =
List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
in
force_does_not_occur subst restricted t
in
let metasenv' = (n, context', t') :: metasenv in
- (try
- let s = List.assoc n subst in
- try
- let more_to_be_restricted'', s' =
- force_does_not_occur subst restricted s
- in
- let subst' = (n, s') :: (List.remove_assoc n subst) in
- let more =
- more @ more_to_be_restricted @ more_to_be_restricted' @
- more_to_be_restricted''
- in
- (more, metasenv', subst')
- with Occur ->
- raise (MetaSubstFailure (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 subst s)))
- with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
+ (more @ more_to_be_restricted @ more_to_be_restricted',
+ metasenv')
with Occur ->
raise (MetaSubstFailure (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 ([], [], subst)
+ metasenv ([], [])
+ in
+ let (more_to_be_restricted', subst) = (* restrict subst *)
+ List.fold_right
+ (fun (n, (context, term)) (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 subst' = (n, (context', term')) :: subst in
+ let more = more @ more_to_be_restricted @ more_to_be_restricted' in
+ (more, subst')
+ with Occur ->
+ raise (MetaSubstFailure (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 subst term)))))
+ subst ([], [])
in
- match more_to_be_restricted with
+ match more_to_be_restricted @ more_to_be_restricted' with
| [] -> (metasenv, subst)
- | _ -> restrict subst more_to_be_restricted metasenv
+ | l -> restrict subst l metasenv
;;
(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
exception Uncertain of string
exception AssertFailure of string
+exception SubstNotFound of int
+
(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
-type substitution = (int * Cic.term) list
+type substitution = (int * (Cic.context * Cic.term)) list
+
+ (** @raise SubstNotFound *)
+val lookup_subst: int -> substitution -> Cic.context * Cic.term
(* apply_subst subst t *)
(* applies the substitution [subst] to [t] *)
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
+
(* 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 canonical_context_length = List.length canonical_context in
let rec aux =
function
(_,[]) -> []
(* Returns the first meta whose number is above the *)
(* number of the higher meta. *)
-let new_meta metasenv =
+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)
+ 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
- 1 + aux (None,metasenv)
+ let indexes =
+ (List.map (fun (i, _, _) -> i) metasenv) @ (List.map fst subst)
+ in
+ 1 + aux (None, indexes)
-let mk_implicit metasenv context =
- let newmeta = new_meta metasenv in
+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 = CicMetaSubst.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 context =
- let newmeta = new_meta metasenv in
+let mk_implicit_type metasenv subst context =
+ let newmeta = new_meta metasenv subst in
let newuniv = CicUniv.fresh () in
+ let context = CicMetaSubst.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 =
- let newmeta = new_meta metasenv in
+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 context n =
+let n_fresh_metas metasenv subst context n =
if n = 0 then metasenv, []
else
let irl = identity_relocation_list_for_metavariable context in
- let newmeta = new_meta metasenv in
+ let context = CicMetaSubst.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, []
Cic.Meta(newmeta+2,irl)::l in
aux newmeta n
-let fresh_subst metasenv context uris =
+let fresh_subst metasenv subst context uris =
let irl = identity_relocation_list_for_metavariable context in
- let newmeta = new_meta metasenv in
+ let context = CicMetaSubst.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,Cic.Meta(newmeta+2,irl))::l in
aux newmeta uris
-let expand_implicits metasenv context term =
+let expand_implicits metasenv subst context term =
let rec aux metasenv context = function
| (Cic.Rel _) as t -> metasenv, t
| (Cic.Sort _) as t -> metasenv, t
let metasenv', l' = do_local_context metasenv context l in
metasenv', Cic.Meta (n, l')
| Cic.Implicit (Some `Type) ->
- let (metasenv', idx) = mk_implicit_type metasenv context in
+ let (metasenv', idx) = mk_implicit_type metasenv subst context in
let irl = identity_relocation_list_for_metavariable context in
metasenv', Cic.Meta (idx, irl)
| Cic.Implicit (Some `Closed) ->
- let (metasenv', idx) = mk_implicit metasenv [] in
+ let (metasenv', idx) = mk_implicit metasenv subst [] in
metasenv', Cic.Meta (idx, [])
| Cic.Implicit None ->
- let (metasenv', idx) = mk_implicit metasenv context in
+ let (metasenv', idx) = mk_implicit metasenv subst context in
let irl = identity_relocation_list_for_metavariable context in
metasenv', Cic.Meta (idx, irl)
| Cic.Cast (te, ty) ->
(* Returns the first meta whose number is above the *)
(* number of the higher meta. *)
-val new_meta : Cic.metasenv -> int
+val new_meta : Cic.metasenv -> CicMetaSubst.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.context -> Cic.metasenv * int
+val mk_implicit: Cic.metasenv -> CicMetaSubst.substitution -> Cic.context -> Cic.metasenv * int
(** as above, but the fresh metavariable represents a type *)
-val mk_implicit_type: Cic.metasenv -> Cic.context -> Cic.metasenv * int
+val mk_implicit_type: Cic.metasenv -> CicMetaSubst.substitution -> Cic.context -> Cic.metasenv * int
(** as above, but the fresh metavariable represents a sort *)
-val mk_implicit_sort: Cic.metasenv -> Cic.metasenv * int
+val mk_implicit_sort: Cic.metasenv -> CicMetaSubst.substitution -> Cic.metasenv * int
(** [mk_implicit metasenv context] create n fresh metavariables *)
val n_fresh_metas:
- Cic.metasenv -> Cic.context -> int -> Cic.metasenv * Cic.term list
+ Cic.metasenv -> CicMetaSubst.substitution -> Cic.context -> int -> Cic.metasenv * Cic.term list
-(** [mk_implicit metasenv context] takes in input a list of uri and
+(** [fresh_subst metasenv context uris] takes in input a list of uri and
creates a fresh explicit substitution *)
val fresh_subst:
Cic.metasenv ->
- Cic.context ->
- UriManager.uri list ->
- Cic.metasenv * (Cic.term Cic.explicit_named_substitution)
+ CicMetaSubst.substitution ->
+ Cic.context ->
+ UriManager.uri list ->
+ Cic.metasenv * (Cic.term Cic.explicit_named_substitution)
val expand_implicits:
- Cic.metasenv -> Cic.context -> Cic.term ->
+ Cic.metasenv -> CicMetaSubst.substitution -> Cic.context -> Cic.term ->
Cic.metasenv * Cic.term
| _ -> raise (AssertFailure "Prod or MutInd expected")
and type_of_aux' metasenv context t =
- let rec type_of_aux subst metasenv context =
+ let rec type_of_aux subst metasenv context t =
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
- function
+ match t with
+(* function *)
C.Rel n ->
(try
match List.nth context (n - 1) with
in
ty,subst',metasenv'
| C.Meta (n,l) ->
- let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
- let subst',metasenv' =
- check_metasenv_consistency n subst metasenv context canonical_context l
- in
- CicSubstitution.lift_meta l ty, subst', metasenv'
+ (try
+ let (canonical_context, term) = CicMetaSubst.lookup_subst n subst in
+ let subst,metasenv =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l
+ in
+ type_of_aux subst metasenv context (CicSubstitution.lift_meta l term)
+ with CicMetaSubst.SubstNotFound _ ->
+ let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
+ let subst,metasenv =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l
+ in
+ CicSubstitution.lift_meta l ty, subst, metasenv)
(* TASSI: CONSTRAINT *)
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
(* One-step LetIn reduction. Even faster than the previous solution.
Moreover the inferred type is closer to the expected one. *)
CicSubstitution.subst s inferredty,subst',metasenv'
- | C.Appl (he::tl) when List.length tl > 0 ->
+ | C.Appl (he::((_::_) as tl)) ->
let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
let tlbody_and_type,subst'',metasenv'' =
List.fold_right
let no_args = count_prod arity in
(* now, create a "generic" MutInd *)
let metasenv,left_args =
- CicMkImplicit.n_fresh_metas metasenv context no_left_params in
+ 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 context no_right_params in
+ else CicMkImplicit.n_fresh_metas metasenv subst context no_right_params in
let metasenv,exp_named_subst =
- CicMkImplicit.fresh_subst metasenv context expl_params in
+ CicMkImplicit.fresh_subst metasenv subst context expl_params in
let expected_type =
if no_args = 0 then
C.MutInd (uri,i,exp_named_subst)
* 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 in
+ CicMkImplicit.mk_implicit_sort metasenv subst in
let (subst, metasenv) =
fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
in
let rec mk_prod metasenv context =
function
[] ->
- let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+ 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 context in
+ let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in
(* then I generate a name --- using the hint name_hint *)
(* --- that is fresh in (context'@context). *)
let name_hint =
- FreshNamesGenerator.mk_fresh_name
- (CicMetaSubst.apply_subst_metasenv subst metasenv)
+ FreshNamesGenerator.mk_fresh_name metasenv
+(* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
(CicMetaSubst.apply_subst_context subst context)
Cic.Anonymous
(CicMetaSubst.apply_subst subst argty)
in
let substituted_t = CicMetaSubst.apply_subst subst' t in
let substituted_ty = CicMetaSubst.apply_subst subst' ty in
- let substituted_metasenv =
- CicMetaSubst.apply_subst_metasenv subst' metasenv'
+ let substituted_metasenv = metasenv'
+(* CicMetaSubst.apply_subst_metasenv subst' metasenv' *)
in
let cleaned_t =
FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
let module S = CicSubstitution in
let module C = Cic in
let rec aux metasenv subst n context t' =
-(*prerr_endline ("1 ciclo di beta_expand arg=" ^ CicMetaSubst.ppterm subst arg ^ " ; term=" ^ CicMetaSubst.ppterm subst t') ;*)
try
let subst,metasenv =
fo_unif_subst test_equality_only subst context metasenv arg t'
subst,metasenv,C.Var (uri,exp_named_subst')
| C.Meta (i,l) as t->
(try
- let t' = List.assoc i subst in
- aux metasenv subst n context t'
+ let (_, t') = CicMetaSubst.lookup_subst i subst in
+ aux metasenv subst n context (CicSubstitution.lift_meta l t')
with
- Not_found -> subst,metasenv,t)
+ CicMetaSubst.SubstNotFound _ -> subst,metasenv,t)
| C.Sort _
| C.Implicit _ as t -> subst,metasenv,t
| C.Cast (te,ty) ->
let subst,metasenv,t' = aux metasenv subst n context t in
subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
in
- let argty =
- type_of_aux' metasenv subst context arg
- in
+ let argty = type_of_aux' metasenv subst context arg in
let fresh_name =
FreshNamesGenerator.mk_fresh_name
metasenv context (Cic.Name "Heta") ~typ:argty
in
let subst,metasenv,t' = aux metasenv subst 0 context t in
- subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
+ subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
and beta_expand_many test_equality_only metasenv subst context t =
List.fold_left
in
begin
try
- let oldt = (List.assoc n subst) in
- let lifted_oldt = S.lift_meta l oldt in
+ let (_, oldt) = CicMetaSubst.lookup_subst n subst in
+ let lifted_oldt = S.lift_meta l oldt in
+ let ty_lifted_oldt =
+ type_of_aux' metasenv subst context lifted_oldt
+ in
+ let tyt = type_of_aux' metasenv subst context t in
+ let (subst, metasenv) =
+ fo_unif_subst_ordered test_equality_only subst context metasenv
+ tyt ty_lifted_oldt
+ in
fo_unif_subst_ordered
- test_equality_only subst context metasenv t lifted_oldt
- with Not_found ->
+ test_equality_only subst context metasenv t lifted_oldt
+ with CicMetaSubst.SubstNotFound _ ->
(* First of all we unify the type of the meta with the type of the term *)
let subst,metasenv =
let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
(try
- let tyt =
- type_of_aux' metasenv subst context t
- in
+ let tyt = type_of_aux' metasenv subst context t in
fo_unif_subst
test_equality_only
subst context metasenv tyt (S.lift_meta l meta_type)
in
(* Unifying the types may have already instantiated n. Let's check *)
try
- let oldt = (List.assoc n subst) in
+ let (_, oldt) = CicMetaSubst.lookup_subst n subst in
let lifted_oldt = S.lift_meta l oldt in
fo_unif_subst_ordered
test_equality_only subst context metasenv t lifted_oldt
with
- Not_found ->
- (n,t'')::subst, metasenv
+ CicMetaSubst.SubstNotFound _ ->
+ let (_, context, _) = CicUtil.lookup_meta n metasenv in
+ let subst = (n, (context, t'')) :: subst in
+ let metasenv =
+(* CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
+ CicMetaSubst.apply_subst_metasenv subst metasenv
+ in
+ subst, metasenv
+(* (n,t'')::subst, metasenv *)
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)) ->
Invalid_argument _ ->
raise (UnificationFailure (sprintf
"Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
- | (C.Rel _, _) | (_, C.Rel _)
+ | (C.Rel _, _) | (_, C.Rel _) ->
+ if t1 = t2 then
+ subst, metasenv
+ else
+ raise (UnificationFailure (sprintf
+ "Can't unify %s with %s because they are not convertible"
+ (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
| (C.Sort _ ,_) | (_, C.Sort _)
| (C.Const _, _) | (_, C.Const _)
| (C.MutInd _, _) | (_, C.MutInd _)
| (C.MutConstruct _, _) | (_, C.MutConstruct _)
| (C.Fix _, _) | (_, C.Fix _)
| (C.CoFix _, _) | (_, C.CoFix _) ->
- if R.are_convertible subst context t1 t2 then
+ if t1 = t2 || R.are_convertible subst context t1 t2 then
subst, metasenv
else
raise (UnificationFailure (sprintf
in
let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
let (newproof, newmetasenv''') =
- let subst_in = CicMetaSubst.apply_subst ((metano,bo')::subst) in
+ let subst_in =
+ CicMetaSubst.apply_subst ((metano,(context, bo'))::subst)
+ in
subst_meta_and_metasenv_in_proof
proof metano subst_in newmetasenv''
in
C.Appl (eliminator_ref :: make_tl term (args_no - 1))
in
let metasenv', term_to_refine' =
- CicMkImplicit.expand_implicits metasenv context term_to_refine in
+ CicMkImplicit.expand_implicits metasenv [] context term_to_refine in
let refined_term,_,metasenv'' =
CicRefine.type_of_aux' metasenv' context term_to_refine'
in
*)
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
- CicMkImplicit.new_meta metasenv
+ CicMkImplicit.new_meta metasenv []
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,bo,ty = proof in
- let subst_in = CicMetaSubst.apply_subst [meta,term] in
+ (* empty context is ok for term since it wont be used by apply_subst *)
+ let subst_in = CicMetaSubst.apply_subst [meta,([], term)] in
let metasenv' =
newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
in
let auto_tac mqi_handle =
+ CicMetaSubst.reset_counters ();
let auto_tac mqi_handle (proof,goal) =
prerr_endline "Entro in Auto";
try
let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in
-prerr_endline "AUTO_TAC HA FINITO";
+ prerr_endline "AUTO_TAC HA FINITO";
+ CicMetaSubst.print_counters ();
(proof,[])
with
| NoOtherChoices ->
projects / helm.git / commitdiff