From 7ec7262cfa317c1962164350361f82a56c5d1826 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 1 Jul 2004 14:12:30 +0000 Subject: [PATCH] New handling of substitution: - splitted metasenv from substitution - substitution enriched with canonical context information for checking_metasenv_consistency --- helm/ocaml/cic_omdoc/cic2acic.ml | 8 +- helm/ocaml/cic_omdoc/doubleTypeInference.ml | 8 +- helm/ocaml/cic_omdoc/eta_fixing.ml | 6 +- .../cic_proof_checking/cicTypeChecker.ml | 7 +- helm/ocaml/cic_unification/.depend | 5 +- helm/ocaml/cic_unification/Makefile | 2 +- helm/ocaml/cic_unification/cicMetaSubst.ml | 161 ++++++++++++------ helm/ocaml/cic_unification/cicMetaSubst.mli | 11 +- helm/ocaml/cic_unification/cicMkImplicit.ml | 51 +++--- helm/ocaml/cic_unification/cicMkImplicit.mli | 21 +-- helm/ocaml/cic_unification/cicRefine.ml | 46 +++-- helm/ocaml/cic_unification/cicUnification.ml | 56 +++--- helm/ocaml/tactics/primitiveTactics.ml | 6 +- helm/ocaml/tactics/proofEngineHelpers.ml | 5 +- helm/ocaml/tactics/variousTactics.ml | 4 +- 15 files changed, 253 insertions(+), 144 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 37e56406e..f86e22f84 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -113,7 +113,9 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts | 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 *) @@ -192,9 +194,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *) 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'' ; diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml index 441d7c9a9..ea29f46fa 100644 --- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml +++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml @@ -361,9 +361,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 @@ -398,9 +396,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = | _,_ -> 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 *) diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml index 167244c28..29d22ccb9 100644 --- a/helm/ocaml/cic_omdoc/eta_fixing.ml +++ b/helm/ocaml/cic_omdoc/eta_fixing.ml @@ -177,10 +177,8 @@ let eta_fix metasenv context t = 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 diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index d36493da6..1577b2f3f 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1390,7 +1390,8 @@ and type_of_aux' metasenv context t = | 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 @@ -1423,8 +1424,8 @@ and type_of_aux' metasenv context t = (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) -> diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index c71893c83..f78ca1699 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -1,8 +1,9 @@ +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 \ diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index 4f19b765f..9762f5936 100644 --- a/helm/ocaml/cic_unification/Makefile +++ b/helm/ocaml/cic_unification/Makefile @@ -3,8 +3,8 @@ REQUIRES = helm-cic_proof_checking PREDICATES = INTERFACE_FILES = \ - cicMkImplicit.mli \ cicMetaSubst.mli \ + cicMkImplicit.mli \ freshNamesGenerator.mli \ cicUnification.mli \ cicRefine.mli diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index d5262f44b..f5daaf3d7 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -25,14 +25,60 @@ 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 ***) @@ -49,9 +95,9 @@ let apply_subst_gen ~appl_fun subst term = 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 @@ -132,10 +178,14 @@ let apply_subst = | _ -> 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 @@ -154,11 +204,13 @@ let rec apply_subst_context subst context = 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 ******) @@ -166,7 +218,8 @@ let apply_subst_metasenv subst metasenv = 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) ;; @@ -203,13 +256,14 @@ let ppmetasenv ?(sep = "\n") metasenv 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 @@ -217,6 +271,7 @@ let lift subst 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 @@ -225,6 +280,7 @@ let subst subst t1 t2 = 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 @@ -234,6 +290,7 @@ let whd subst context term = 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 @@ -243,29 +300,24 @@ let tempi_type_of_aux_subst = ref 0.0;; 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 @@ -433,9 +485,9 @@ let rec restrict subst to_be_restricted metasenv = 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 @@ -451,33 +503,44 @@ let rec restrict subst to_be_restricted metasenv = 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 *) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 546a71dea..46a50a63a 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -27,9 +27,14 @@ exception MetaSubstFailure of string 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] *) @@ -81,3 +86,7 @@ val fppsubst: Format.formatter -> 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 + diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 41f058945..748307013 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -28,7 +28,6 @@ (* 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 (_,[]) -> [] @@ -39,45 +38,54 @@ let identity_relocation_list_for_metavariable ?(start = 1) canonical_context = (* 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, [] @@ -90,9 +98,10 @@ let n_fresh_metas metasenv context n = 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, [] @@ -105,7 +114,7 @@ let fresh_subst metasenv context uris = (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 @@ -125,14 +134,14 @@ let expand_implicits metasenv context term = 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) -> diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli index 923332ae0..1356fce58 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.mli +++ b/helm/ocaml/cic_unification/cicMkImplicit.mli @@ -32,32 +32,33 @@ val identity_relocation_list_for_metavariable : (* 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 diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 7bd3de5c2..c1b70df8d 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -132,11 +132,12 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | _ -> 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 @@ -156,11 +157,20 @@ and type_of_aux' metasenv context t = 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 @@ -214,7 +224,7 @@ and type_of_aux' metasenv context t = (* 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 @@ -267,13 +277,13 @@ and type_of_aux' metasenv context t = 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) @@ -506,7 +516,7 @@ and type_of_aux' metasenv context t = * 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 @@ -521,13 +531,13 @@ and type_of_aux' metasenv context t = 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 @@ -539,8 +549,8 @@ and type_of_aux' metasenv context t = (* 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) @@ -630,8 +640,8 @@ and type_of_aux' metasenv context t = 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 diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 81e794c8c..c8ed00477 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -47,7 +47,6 @@ let rec beta_expand test_equality_only metasenv subst context t arg = 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' @@ -65,10 +64,10 @@ let rec beta_expand test_equality_only metasenv subst context t arg = 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) -> @@ -155,15 +154,13 @@ let rec beta_expand test_equality_only metasenv subst context t arg = 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 @@ -240,18 +237,24 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = 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) @@ -286,13 +289,20 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; 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)) -> @@ -401,14 +411,20 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; 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 diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 2d741f1d1..cc743d7cc 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -326,7 +326,9 @@ let apply_tac ~term (proof, goal) = 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 @@ -501,7 +503,7 @@ let elim_tac ~term = 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 diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 73f465494..03257dfa1 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -24,11 +24,12 @@ *) 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 diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 0566564dc..ccbf6c63c 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -220,11 +220,13 @@ let rec auto_new mqi_handle = function 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 -> -- 2.39.2