(* 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/ *) (* $Id: disambiguate.ml 9178 2008-11-12 12:09:52Z tassi $ *) open Printf open DisambiguateTypes open UriManager module Ast = CicNotationPt let debug_print _ = ();; let refine_term metasenv context uri term ugraph ~localization_tbl = (* if benchmark then incr actual_refinements; *) assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); try let term', _, metasenv',ugraph1 = NCicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in (Disambiguate.Ok (term', metasenv')),ugraph1 with exn -> let rec process_exn loc = function HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn | CicRefine.Uncertain msg -> debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; Disambiguate.Uncertain (loc,msg),ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" (CicPp.ppterm term) (Lazy.force msg))); Disambiguate.Ko (loc,msg),ugraph | exn -> raise exn in process_exn None exn let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try snd (Environment.find item env) env num args with Not_found -> failwith ("Domain item not found: " ^ (DisambiguateTypes.string_of_domain_item item)) (* TODO move it to Cic *) let find_in_context name context = let rec aux acc = function | [] -> raise Not_found | Cic.Name hd :: tl when hd = name -> acc | _ :: tl -> aux (acc + 1) tl in aux 1 context let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); let rec aux ~localize loc context = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> let res = aux ~localize loc context term in if localize then Cic.CicHash.add localization_tbl res loc; res | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in resolve env (Symbol (symb, i)) ~args:cic_args () | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> let cic_type = aux_option ~localize loc context (Some `Type) typ in let cic_name = CicNotationUtil.cic_name_of_name var in let cic_body = aux ~localize loc (cic_name :: context) body in (match binder_kind with | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body) | `Pi | `Forall -> Cic.Prod (cic_name, cic_type, cic_body) | `Exists -> resolve env (Symbol ("exists", 0)) ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ()) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in let cic_outtype = aux_option ~localize loc context None outtype in let do_branch ((head, _, args), term) = let rec do_branch' context = function | [] -> aux ~localize loc context term | (name, typ) :: tl -> let cic_name = CicNotationUtil.cic_name_of_name name in let cic_body = do_branch' (cic_name :: context) tl in let typ = match typ with | None -> Cic.Implicit (Some `Type) | Some typ -> aux ~localize loc context typ in Cic.Lambda (cic_name, typ, cic_body) in do_branch' context args in let indtype_uri, indtype_no = if create_dummy_ids then (UriManager.uri_of_string "cic:/fake_indty.con", 0) else match indty_ident with | Some (indty_ident, _) -> (match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) | Cic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) | _ -> raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!"))) | None -> let rec fst_constructor = function (Ast.Pattern (head, _, _), _) :: _ -> head | (Ast.Wildcard, _) :: tl -> fst_constructor tl | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards")) in (match resolve env (Id (fst_constructor branches)) () with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> (indtype_uri, indtype_no) | Cic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) | _ -> raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!"))) in let branches = if create_dummy_ids then List.map (function Ast.Wildcard,term -> ("wildcard",None,[]), term | Ast.Pattern _,_ -> raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\"")) ) branches else match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with Cic.InductiveDefinition (il,_,leftsno,_) -> let _,_,_,cl = try List.nth il indtype_no with _ -> assert false in let rec count_prod t = match CicReduction.whd [] t with Cic.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in let rec sort branches cl = match cl with [] -> let rec analyze unused unrecognized useless = function [] -> if unrecognized != [] then raise (DisambiguateTypes.Invalid_choice (Some loc, lazy ("Unrecognized constructors: " ^ String.concat " " unrecognized))) else if useless > 0 then raise (DisambiguateTypes.Invalid_choice (Some loc, lazy ("The last " ^ string_of_int useless ^ "case" ^ if useless > 1 then "s are" else " is" ^ " unused"))) else [] | (Ast.Wildcard,_)::tl when not unused -> analyze true unrecognized useless tl | (Ast.Pattern (head,_,_),_)::tl when not unused -> analyze unused (head::unrecognized) useless tl | _::tl -> analyze unused unrecognized (useless + 1) tl in analyze false [] 0 branches | (name,ty)::cltl -> let rec find_and_remove = function [] -> raise (DisambiguateTypes.Invalid_choice (Some loc, lazy ("Missing case: " ^ name))) | ((Ast.Wildcard, _) as branch :: _) as branches -> branch, branches | (Ast.Pattern (name',_,_),_) as branch :: tl when name = name' -> branch,tl | branch::tl -> let found,rest = find_and_remove tl in found, branch::rest in let branch,tl = find_and_remove branches in match branch with Ast.Pattern (name,y,args),term -> if List.length args = count_prod ty - leftsno then ((name,y,args),term)::sort tl cltl else raise (DisambiguateTypes.Invalid_choice (Some loc, lazy ("Wrong number of arguments for " ^ name))) | Ast.Wildcard,term -> let rec mk_lambdas = function 0 -> term | n -> CicNotationPt.Binder (`Lambda, (CicNotationPt.Ident ("_", None), None), mk_lambdas (n - 1)) in (("wildcard",None,[]), mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl in sort branches cl | _ -> assert false in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) | CicNotationPt.Cast (t1, t2) -> let cic_t1 = aux ~localize loc context t1 in let cic_t2 = aux ~localize loc context t2 in Cic.Cast (cic_t1, cic_t2) | CicNotationPt.LetIn ((name, typ), def, body) -> let cic_def = aux ~localize loc context def in let cic_name = CicNotationUtil.cic_name_of_name name in let cic_typ = match typ with | None -> Cic.Implicit (Some `Type) | Some t -> aux ~localize loc context t in let cic_body = aux ~localize loc (cic_name :: context) body in Cic.LetIn (cic_name, cic_def, cic_typ, cic_body) | CicNotationPt.LetRec (kind, defs, body) -> let context' = List.fold_left (fun acc (_, (name, _), _, _) -> CicNotationUtil.cic_name_of_name name :: acc) context defs in let cic_body = let unlocalized_body = aux ~localize:false loc context' body in match unlocalized_body with Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n | Cic.Appl (Cic.Rel n::l) when n <= List.length defs -> (try let l' = List.map (function t -> let t',subst,metasenv = CicMetaSubst.delift_rels [] [] (List.length defs) t in assert (subst=[]); assert (metasenv=[]); t') l in (* We can avoid the LetIn. But maybe we need to recompute l' so that it is localized *) if localize then match body with CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> (* since we avoid the letin, the context has no * recfuns in it *) let l' = List.map (aux ~localize loc context) l in `AvoidLetIn (n,l') | _ -> assert false else `AvoidLetIn (n,l') with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> if localize then `AddLetIn (aux ~localize loc context' body) else `AddLetIn unlocalized_body) | _ -> if localize then `AddLetIn (aux ~localize loc context' body) else `AddLetIn unlocalized_body in let inductiveFuns = List.map (fun (params, (name, typ), body, decr_idx) -> let add_binders kind t = List.fold_right (fun var t -> CicNotationPt.Binder (kind, var, t)) params t in let cic_body = aux ~localize loc context' (add_binders `Lambda body) in let cic_type = aux_option ~localize loc context (Some `Type) (HExtlib.map_option (add_binders `Pi) typ) in let name = match CicNotationUtil.cic_name_of_name name with | Cic.Anonymous -> CicNotationPt.fail loc "Recursive functions cannot be anonymous" | Cic.Name name -> name in (name, decr_idx, cic_type, cic_body)) defs in let fix_or_cofix n = match kind with `Inductive -> Cic.Fix (n,inductiveFuns) | `CoInductive -> let coinductiveFuns = List.map (fun (name, _, typ, body) -> name, typ, body) inductiveFuns in Cic.CoFix (n,coinductiveFuns) in let counter = ref ~-1 in let build_term funs (var,_,ty,_) t = incr counter; Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t) in (match cic_body with `AvoidLetInNoAppl n -> let n' = List.length inductiveFuns - n in fix_or_cofix n' | `AvoidLetIn (n,l) -> let n' = List.length inductiveFuns - n in Cic.Appl (fix_or_cofix n'::l) | `AddLetIn cic_body -> List.fold_right (build_term inductiveFuns) inductiveFuns cic_body) | CicNotationPt.Ident _ | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed | CicNotationPt.Ident (name, subst) | CicNotationPt.Uri (name, subst) as ast -> let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in (try if is_uri ast then raise Not_found;(* don't search the env for URIs *) let index = find_in_context name context in if subst <> None then CicNotationPt.fail loc "Explicit substitutions not allowed here"; Cic.Rel index with Not_found -> let cic = if is_uri ast then (* we have the URI, build the term out of it *) try CicUtil.term_of_uri (UriManager.uri_of_string name) with UriManager.IllFormedUri _ -> CicNotationPt.fail loc "Ill formed URI" else resolve env (Id name) () in let mk_subst uris = let ids_to_uris = List.map (fun uri -> UriManager.name_of_uri uri, uri) uris in (match subst with | Some subst -> List.map (fun (s, term) -> (try List.assoc s ids_to_uris, aux ~localize loc context term with Not_found -> raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) subst | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) in (try match cic with | Cic.Const (uri, []) -> let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in Cic.Const (uri, mk_subst uris) | Cic.Var (uri, []) -> let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in Cic.Var (uri, mk_subst uris) | Cic.MutInd (uri, i, []) -> (try let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in Cic.MutInd (uri, i, mk_subst uris) with CicEnvironment.Object_not_found _ -> (* if we are here it is probably the case that during the definition of a mutual inductive type we have met an occurrence of the type in one of its constructors. However, the inductive type is not yet in the environment *) (*here the explicit_named_substituion is assumed to be of length 0 *) Cic.MutInd (uri,i,[])) | Cic.MutConstruct (uri, i, j, []) -> let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in Cic.MutConstruct (uri, i, j, mk_subst uris) | Cic.Meta _ | Cic.Implicit _ as t -> (* debug_print (lazy (sprintf "Warning: %s must be instantiated with _[%s] but we do not enforce it" (CicPp.ppterm t) (String.concat "; " (List.map (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term) subst)))); *) t | _ -> raise (Invalid_choice (Some loc, lazy "??? Can this happen?")) with CicEnvironment.CircularDependency _ -> raise (Invalid_choice (None, lazy "Circular dependency in the environment")))) | CicNotationPt.Implicit -> Cic.Implicit None | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num () | CicNotationPt.Meta (index, subst) -> let cic_subst = List.map (function None -> None | Some term -> Some (aux ~localize loc context term)) subst in Cic.Meta (index, cic_subst) | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () | _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> Cic.Implicit annotation | Some term -> aux ~localize loc context term in aux ~localize:true HExtlib.dummy_floc context ast let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl = assert false (* let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast ~localization_tbl *) ;; let domain_of_term ~context = let context = List.map (fun x -> Cic.Name (fst x)) context in Disambiguate.domain_of_ast_term ~context ;; module Make (C : DisambiguateTypes.Callbacks) = struct module Disambiguator = Disambiguate.Make(C) let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe (text,prefix_len,term) = let term = if fresh_instances then CicNotationUtil.freshen_term term else term in let localization_tbl = Cic.CicHash.create 503 in Disambiguator.disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) ~localization_tbl ;; end