X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=bb6390bdcdb2c3d231674520882fc41c585c44f0;hb=827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8;hp=23aa20bfb50cb30d4483e5fd2c04400281ce7934;hpb=9e3eb63a93acaca0b4ad59c213e9ea430524d3ae;p=helm.git diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 23aa20bfb..bb6390bdc 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception Bad_pattern of string +exception Bad_pattern of string Lazy.t let new_meta_of_proof ~proof:(_, metasenv, _, _) = CicMkImplicit.new_meta metasenv [] @@ -46,9 +46,10 @@ let subst_meta_in_proof proof meta term newmetasenv = List.map (function Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) - | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None)) + | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def (subst_in s,None)) | None -> None - | Some (_,Cic.Def (_,Some _)) -> assert false + | Some (n,Cic.Def (bo,Some ty)) -> + Some (n,Cic.Def (subst_in bo,Some (subst_in ty))) ) canonical_context in i,canonical_context',(subst_in ty) @@ -92,8 +93,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = None -> None | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) | Some (i,Cic.Def (t,None)) -> - Some (i,Cic.Def ((subst_in t),None)) - | Some (_,Cic.Def (_,Some _)) -> assert false + Some (i,Cic.Def (subst_in t,None)) + | Some (i,Cic.Def (bo,Some ty)) -> + Some (i,Cic.Def (subst_in bo,Some (subst_in ty))) ) canonical_context in (m,canonical_context',subst_in ty)::i @@ -224,14 +226,12 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t = find subst metasenv ugraph context wanted t let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = - let add_ctx context name entry = - (Some (name, entry)) :: context - in + let add_ctx context name entry = (Some (name, entry)) :: context in let map2 error_msg f l1 l2 = try List.map2 f l1 l2 with - | Invalid_argument _ -> raise (Bad_pattern error_msg) + | Invalid_argument _ -> raise (Bad_pattern (lazy error_msg)) in let rec aux context where term = match (where, term) with @@ -292,15 +292,18 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = funs1 funs2) | x,y -> raise (Bad_pattern - (Printf.sprintf "Pattern %s versus term %s" + (lazy (Printf.sprintf "Pattern %s versus term %s" (CicPp.ppterm x) - (CicPp.ppterm y))) + (CicPp.ppterm y)))) and auxs context terms1 terms2 = (* as aux for list of terms *) List.concat (map2 "wrong number of arguments in application" (fun t1 t2 -> aux context t1 t2) terms1 terms2) in - let context_len = List.length context in - let roots = aux context where term in + let roots = + match where with + | None -> [] + | Some where -> aux context where term + in match wanted with None -> [],metasenv,ugraph,roots | Some wanted -> @@ -455,7 +458,7 @@ let pattern_of ?(equality=(==)) ~term terms = in snd (aux term) -exception Fail of string +exception Fail of string Lazy.t (** select metasenv conjecture pattern * select all subterms of [conjecture] matching [pattern]. @@ -472,15 +475,15 @@ exception Fail of string * @raise Bad_pattern * *) let select ~metasenv ~ugraph ~conjecture:(_,context,ty) - ~pattern:(what,hyp_patterns,goal_pattern) + ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern) = + let what, hyp_patterns, goal_pattern = pattern in let find_pattern_for name = try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) with Not_found -> None in let subst,metasenv,ugraph,ty_terms = select_in_term ~metasenv ~context ~ugraph ~term:ty ~pattern:(what,goal_pattern) in - let context_len = List.length context in let subst,metasenv,ugraph,context_terms = let subst,metasenv,ugraph,res,_ = (List.fold_right @@ -494,7 +497,7 @@ exception Fail of string | Some pat -> let subst,metasenv,ugraph,terms = select_in_term ~metasenv ~context ~ugraph ~term - ~pattern:(what,pat) + ~pattern:(what, Some pat) in subst,metasenv,ugraph,((Some (`Decl terms))::res), (entry::context)) @@ -507,14 +510,14 @@ exception Fail of string | Some pat -> let subst,metasenv,ugraph,terms_bo = select_in_term ~metasenv ~context ~ugraph ~term:bo - ~pattern:(what,pat) in + ~pattern:(what, Some pat) in let subst,metasenv,ugraph,terms_ty = match ty with None -> subst,metasenv,ugraph,None | Some ty -> let subst,metasenv,ugraph,res = select_in_term ~metasenv ~context ~ugraph ~term:ty - ~pattern:(what,pat) + ~pattern:(what, Some pat) in subst,metasenv,ugraph,Some res in @@ -649,7 +652,7 @@ let saturate_term newmeta metasenv context ty goal_arity = in if prod_no + 1 = goal_arity then let head = CicReduction.normalize ~delta:false context ty in - head,[],[],newmeta,goal_arity + 1 + head,[],[],lastmeta,goal_arity + 1 else (** NORMALIZE RATIONALE * we normalize the target only NOW since we may be in this case: @@ -678,6 +681,6 @@ let lookup_type metasenv context hyp = | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp -> p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph) | _ :: tail -> aux (succ p) tail - | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal") + | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal")) in aux 1 context