From: Claudio Sacerdoti Coen Date: Fri, 23 Nov 2007 15:59:43 +0000 (+0000) Subject: This alternative version of disambiguate.crit2 implements the following X-Git-Tag: 0.4.98@7921~4 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0cc3c93f4253c80f993adf8b8d5b476545043796 This alternative version of disambiguate.crit2 implements the following criterion for spurious error detection: an error is spurious iff: a) it is obtained interpreting the symbol s with the interpretation \phi b) there exists another interpretation \phi' such that 1) dom(\phi) = dom(\phi') 2) \phi' is valid 3) \phi(x)=\phi'(x) for each x != s More (but not too many) errors are spurious according to this criterion. --- diff --git a/components/cic_disambiguation/disambiguate.crit2.ml b/components/cic_disambiguation/disambiguate.crit2.ml new file mode 100644 index 000000000..7aeb65a21 --- /dev/null +++ b/components/cic_disambiguation/disambiguate.crit2.ml @@ -0,0 +1,1317 @@ +(* 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 7760 2007-10-26 12:37:21Z sacerdot $ *) + +open Printf + +open DisambiguateTypes +open UriManager + +module Ast = CicNotationPt + +(* the integer is an offset to be added to each location *) +exception NoWellTypedInterpretation of + int * + ((Stdpp.location list * string * string) list * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Stdpp.location option * string Lazy.t * bool) list +exception PathNotWellFormed + + (** raised when an environment is not enough informative to decide *) +exception Try_again of string Lazy.t + +type aliases = bool * DisambiguateTypes.environment +type 'a disambiguator_input = string * int * 'a + +type domain = domain_tree list +and domain_tree = Node of Stdpp.location list * domain_item * domain + +let rec string_of_domain = + function + [] -> "" + | Node (_,domain_item,l)::tl -> + DisambiguateTypes.string_of_domain_item domain_item ^ + " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl + +let rec filter_map_domain f = + function + [] -> [] + | Node (locs,domain_item,l)::tl -> + match f locs domain_item with + None -> filter_map_domain f l @ filter_map_domain f tl + | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl + +let rec map_domain f = + function + [] -> [] + | Node (locs,domain_item,l)::tl -> + f locs domain_item :: map_domain f l @ map_domain f tl + +let uniq_domain dom = + let rec aux seen = + function + [] -> seen,[] + | Node (locs,domain_item,l)::tl -> + if List.mem domain_item seen then + let seen,l = aux seen l in + let seen,tl = aux seen tl in + seen, l @ tl + else + let seen,l = aux (domain_item::seen) l in + let seen,tl = aux seen tl in + seen, Node (locs,domain_item,l)::tl + in + snd (aux [] dom) + +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + +(* + (** print benchmark information *) +let benchmark = true +let max_refinements = ref 0 (* benchmarking is not thread safe *) +let actual_refinements = ref 0 +let domain_size = ref 0 +let choices_avg = ref 0. +*) + +let descr_of_domain_item = function + | Id s -> s + | Symbol (s, _) -> s + | Num i -> string_of_int i + +type 'a test_result = + | Ok of 'a * Cic.metasenv + | Ko of Stdpp.location option * string Lazy.t + | Uncertain of Stdpp.location option * string Lazy.t + +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 = + CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in + debug_print (lazy (sprintf "OK!!!")); + (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)) ; + Uncertain (loc,msg),ugraph + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (Lazy.force msg))); + Ko (loc,msg),ugraph + | exn -> raise exn + in + process_exn None exn + +let refine_obj metasenv context uri obj ugraph ~localization_tbl = + assert (context = []); + debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; + try + let obj', metasenv,ugraph = + CicRefine.typecheck metasenv uri obj ~localization_tbl + in + debug_print (lazy (sprintf "OK!!!")); + (Ok (obj', metasenv)),ugraph + 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.ppobj obj)) ; + Uncertain (loc,msg),ugraph + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppobj obj) (Lazy.force msg))) ; + 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: Cic.name list) ~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: Cic.name list) = 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 (Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (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 (Try_again (lazy "The type of the term to be matched + is still unknown")) + | _ -> + raise (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 (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.empty_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 (Invalid_choice + (Some loc, + lazy + ("Unrecognized constructors: " ^ + String.concat " " unrecognized))) + else if useless > 0 then + raise (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 + (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 + (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_def = + match typ with + | None -> cic_def + | Some t -> Cic.Cast (cic_def, aux ~localize loc context t) + in + let cic_body = aux ~localize loc (cic_name :: context) body in + Cic.LetIn (cic_name, cic_def, 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)) -> + 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,_,_,_) t = + incr counter; + Cic.LetIn (Cic.Name var, fix_or_cofix !counter, 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 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.empty_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.empty_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.empty_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.empty_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 -> Cic.Sort Cic.CProp + | CicNotationPt.Symbol (symbol, instance) -> + resolve env (Symbol (symbol, instance)) () + | _ -> assert false (* god bless Bologna *) + and aux_option ~localize loc (context: Cic.name list) annotation = function + | None -> Cic.Implicit annotation + | Some term -> aux ~localize loc context term + in + aux ~localize:true HExtlib.dummy_floc context ast + +let interpretate_path ~context path = + let localization_tbl = Cic.CicHash.create 23 in + (* here we are throwing away useful localization informations!!! *) + fst ( + interpretate_term ~create_dummy_ids:true + ~context ~env:Environment.empty ~uri:None ~is_path:true + path ~localization_tbl, localization_tbl) + +let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = + assert (context = []); + assert (is_path = false); + let interpretate_term = interpretate_term ~localization_tbl in + match obj with + | CicNotationPt.Inductive (params,tyl) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in + let name_to_uris = + snd ( + List.fold_left + (*here the explicit_named_substituion is assumed to be of length 0 *) + (fun (i,res) (name,_,_,_) -> + i + 1,(name,name,Cic.MutInd (uri,i,[]))::res + ) (0,[]) tyl) in + let con_env = DisambiguateTypes.env_of_list name_to_uris env in + let tyl = + List.map + (fun (name,b,ty,cl) -> + let ty' = add_params (interpretate_term context env None false ty) in + let cl' = + List.map + (fun (name,ty) -> + let ty' = + add_params (interpretate_term context con_env None false ty) + in + name,ty' + ) cl + in + name,b,ty',cl' + ) tyl + in + Cic.InductiveDefinition (tyl,[],List.length params,[]) + | CicNotationPt.Record (params,name,ty,fields) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit + | Some t -> t in + let name = CicNotationUtil.cic_name_of_name name in + name::context,(name, interpretate_term context env None false t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right + (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in + let ty' = add_params (interpretate_term context env None false ty) in + let fields' = + snd ( + List.fold_left + (fun (context,res) (name,ty,_coercion,arity) -> + let context' = Cic.Name name :: context in + context',(name,interpretate_term context env None false ty)::res + ) (context,[]) fields) in + let concl = + (*here the explicit_named_substituion is assumed to be of length 0 *) + let mutind = Cic.MutInd (uri,0,[]) in + if params = [] then mutind + else + Cic.Appl + (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in + let con = + List.fold_left + (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t)) + concl fields' in + let con' = add_params con in + let tyl = [name,true,ty',["mk_" ^ name,con']] in + let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in + Cic.InductiveDefinition + (tyl,[],List.length params,[`Class (`Record field_names)]) + | CicNotationPt.Theorem (flavour, name, ty, bo) -> + let attrs = [`Flavour flavour] in + let ty' = interpretate_term [] env None false ty in + (match bo,flavour with + None,`Axiom -> + Cic.Constant (name,None,ty',[],attrs) + | Some bo,`Axiom -> assert false + | None,_ -> + Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs) + | Some bo,_ -> + let bo' = Some (interpretate_term [] env None false bo) in + Cic.Constant (name,bo',ty',[],attrs)) + +let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function + | Ast.AttributedTerm (`Loc loc, term) -> + domain_of_term ~loc ~context term + | Ast.AttributedTerm (_, term) -> + domain_of_term ~loc ~context term + | Ast.Symbol (symbol, instance) -> + [ Node ([loc], Symbol (symbol, instance), []) ] + (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *) + | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args) + -> + let args_dom = + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + args [] in + let loc = + match hd with + Ast.AttributedTerm (`Loc loc,_) -> loc + | _ -> loc + in + [ Node ([loc], Symbol (symbol, instance), args_dom) ] + | Ast.Appl (Ast.Ident (name, subst) as hd :: args) + | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) -> + let args_dom = + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + args [] in + let loc = + match hd with + Ast.AttributedTerm (`Loc loc,_) -> loc + | _ -> loc + in + (try + (* the next line can raise Not_found *) + ignore(find_in_context name context); + if subst <> None then + Ast.fail loc "Explicit substitutions not allowed here" + else + args_dom + with Not_found -> + (match subst with + | None -> [ Node ([loc], Id name, args_dom) ] + | Some subst -> + let terms = + List.fold_left + (fun dom (_, term) -> + let dom' = domain_of_term ~loc ~context term in + dom @ dom') + [] subst in + [ Node ([loc], Id name, terms @ args_dom) ])) + | Ast.Appl terms -> + List.fold_right + (fun term acc -> domain_of_term ~loc ~context term @ acc) + terms [] + | Ast.Binder (kind, (var, typ), body) -> + let type_dom = domain_of_term_option ~loc ~context typ in + let body_dom = + domain_of_term ~loc + ~context:(CicNotationUtil.cic_name_of_name var :: context) body in + (match kind with + | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ] + | _ -> type_dom @ body_dom) + | Ast.Case (term, indty_ident, outtype, branches) -> + let term_dom = domain_of_term ~loc ~context term in + let outtype_dom = domain_of_term_option ~loc ~context outtype in + let rec get_first_constructor = function + | [] -> [] + | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ] + | _ :: tl -> get_first_constructor tl in + let do_branch = + function + Ast.Pattern (head, _, args), term -> + let (term_context, args_domain) = + List.fold_left + (fun (cont, dom) (name, typ) -> + (CicNotationUtil.cic_name_of_name name :: cont, + (match typ with + | None -> dom + | Some typ -> dom @ domain_of_term ~loc ~context:cont typ))) + (context, []) args + in + domain_of_term ~loc ~context:term_context term @ args_domain + | Ast.Wildcard, term -> + domain_of_term ~loc ~context term + in + let branches_dom = + List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in + (match indty_ident with + | None -> get_first_constructor branches + | Some (ident, _) -> [ Node ([loc], Id ident, []) ]) + @ term_dom @ outtype_dom @ branches_dom + | Ast.Cast (term, ty) -> + let term_dom = domain_of_term ~loc ~context term in + let ty_dom = domain_of_term ~loc ~context ty in + term_dom @ ty_dom + | Ast.LetIn ((var, typ), body, where) -> + let body_dom = domain_of_term ~loc ~context body in + let type_dom = domain_of_term_option ~loc ~context typ in + let where_dom = + domain_of_term ~loc + ~context:(CicNotationUtil.cic_name_of_name var :: context) where in + body_dom @ type_dom @ where_dom + | Ast.LetRec (kind, defs, where) -> + let add_defs context = + List.fold_left + (fun acc (_, (var, _), _, _) -> + CicNotationUtil.cic_name_of_name var :: acc + ) context defs in + let where_dom = domain_of_term ~loc ~context:(add_defs context) where in + let defs_dom = + List.fold_left + (fun dom (params, (_, typ), body, _) -> + let context' = + add_defs + (List.fold_left + (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc) + context params) + in + List.rev + (snd + (List.fold_left + (fun (context,res) (var,ty) -> + CicNotationUtil.cic_name_of_name var :: context, + domain_of_term_option ~loc ~context ty @ res) + (add_defs context,[]) params)) + @ domain_of_term_option ~loc ~context:context' typ + @ domain_of_term ~loc ~context:context' body + ) [] defs + in + defs_dom @ where_dom + | Ast.Ident (name, subst) -> + (try + (* the next line can raise Not_found *) + ignore(find_in_context name context); + if subst <> None then + Ast.fail loc "Explicit substitutions not allowed here" + else + [] + with Not_found -> + (match subst with + | None -> [ Node ([loc], Id name, []) ] + | Some subst -> + let terms = + List.fold_left + (fun dom (_, term) -> + let dom' = domain_of_term ~loc ~context term in + dom @ dom') + [] subst in + [ Node ([loc], Id name, terms) ])) + | Ast.Uri _ -> [] + | Ast.Implicit -> [] + | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] + | Ast.Meta (index, local_context) -> + List.fold_left + (fun dom term -> dom @ domain_of_term_option ~loc ~context term) + [] local_context + | Ast.Sort _ -> [] + | Ast.UserInput + | Ast.Literal _ + | Ast.Layout _ + | Ast.Magic _ + | Ast.Variable _ -> assert false + +and domain_of_term_option ~loc ~context = function + | None -> [] + | Some t -> domain_of_term ~loc ~context t + +let domain_of_term ~context term = + uniq_domain (domain_of_term ~context term) + +let domain_of_obj ~context ast = + assert (context = []); + match ast with + | Ast.Theorem (_,_,ty,bo) -> + domain_of_term [] ty + @ (match bo with + None -> [] + | Some bo -> domain_of_term [] bo) + | Ast.Inductive (params,tyl) -> + let context, dom = + List.fold_left + (fun (context, dom) (var, ty) -> + let context' = CicNotationUtil.cic_name_of_name var :: context in + match ty with + None -> context', dom + | Some ty -> context', dom @ domain_of_term context ty + ) ([], []) params in + let context_w_types = + List.rev_map + (fun (var, _, _, _) -> Cic.Name var) tyl + @ context in + dom + @ List.flatten ( + List.map + (fun (_,_,ty,cl) -> + domain_of_term context ty + @ List.flatten ( + List.map + (fun (_,ty) -> domain_of_term context_w_types ty) cl)) + tyl) + | CicNotationPt.Record (params,var,ty,fields) -> + let context, dom = + List.fold_left + (fun (context, dom) (var, ty) -> + let context' = CicNotationUtil.cic_name_of_name var :: context in + match ty with + None -> context', dom + | Some ty -> context', dom @ domain_of_term context ty + ) ([], []) params in + let context_w_types = Cic.Name var :: context in + dom + @ domain_of_term context ty + @ snd + (List.fold_left + (fun (context,res) (name,ty,_,_) -> + Cic.Name name::context, res @ domain_of_term context ty + ) (context_w_types,[]) fields) + +let domain_of_obj ~context obj = + uniq_domain (domain_of_obj ~context obj) + + (* dom1 \ dom2 *) +let domain_diff dom1 dom2 = +(* let domain_diff = Domain.diff *) + let is_in_dom2 elt = + List.exists + (function + | Symbol (symb, 0) -> + (match elt with + Symbol (symb',_) when symb = symb' -> true + | _ -> false) + | Num i -> + (match elt with + Num _ -> true + | _ -> false) + | item -> elt = item + ) dom2 + in + let rec aux = + function + [] -> [] + | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl) + | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl) + in + aux dom1 + +module type Disambiguator = +sig + val disambiguate_term : + ?fresh_instances:bool -> + dbd:HSql.dbd -> + context:Cic.context -> + metasenv:Cic.metasenv -> + ?initial_ugraph:CicUniv.universe_graph -> + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> + CicNotationPt.term disambiguator_input -> + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Cic.metasenv * (* new metasenv *) + Cic.term* + CicUniv.universe_graph) list * (* disambiguated term *) + bool + + val disambiguate_obj : + ?fresh_instances:bool -> + dbd:HSql.dbd -> + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> + uri:UriManager.uri option -> (* required only for inductive types *) + CicNotationPt.term CicNotationPt.obj disambiguator_input -> + ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Cic.metasenv * (* new metasenv *) + Cic.obj * + CicUniv.universe_graph) list * (* disambiguated obj *) + bool +end + +module Make (C: Callbacks) = + struct + let choices_of_id dbd id = + let uris = Whelp.locate ~dbd id in + let uris = + match uris with + | [] -> + (match + (C.input_or_locate_uri + ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ()) + with + | None -> [] + | Some uri -> [uri]) + | [uri] -> [uri] + | _ -> + C.interactive_user_uri_choice ~selection_mode:`MULTIPLE + ~ok:"Try selected." ~enable_button_for_non_vars:true + ~title:"Ambiguous input." ~id + ~msg: ("Ambiguous input \"" ^ id ^ + "\". Please, choose one or more interpretations:") + uris + in + List.map + (fun uri -> + (UriManager.string_of_uri uri, + let term = + try + CicUtil.term_of_uri uri + with exn -> + debug_print (lazy (UriManager.string_of_uri uri)); + debug_print (lazy (Printexc.to_string exn)); + assert false + in + fun _ _ _ -> term)) + uris + +let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" + + let disambiguate_thing ~dbd ~context ~metasenv + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + (thing_txt,thing_txt_prefix_len,thing) + = + debug_print (lazy "DISAMBIGUATE INPUT"); + let disambiguate_context = (* cic context -> disambiguate context *) + List.map + (function None -> Cic.Anonymous | Some (name, _) -> name) + context + in + debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); + let thing_dom = domain_of_thing ~context:disambiguate_context thing in + debug_print + (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); +(* + debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s" + (DisambiguatePp.pp_environment aliases))); + debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s" + (match universe with None -> "None" | Some _ -> "Some _"))); +*) + let current_dom = + Environment.fold (fun item _ dom -> item :: dom) aliases [] in + let todo_dom = domain_diff thing_dom current_dom in + debug_print + (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom))); + (* (2) lookup function for any item (Id/Symbol/Num) *) + let lookup_choices = + fun item -> + let choices = + let lookup_in_library () = + match item with + | Id id -> choices_of_id dbd id + | Symbol (symb, _) -> + (try + List.map DisambiguateChoices.mk_choice + (TermAcicContent.lookup_interpretations symb) + with + TermAcicContent.Interpretation_not_found -> []) + | Num instance -> + DisambiguateChoices.lookup_num_choices () + in + match universe with + | None -> lookup_in_library () + | Some e -> + (try + let item = + match item with + | Symbol (symb, _) -> Symbol (symb, 0) + | item -> item + in + Environment.find item e + with Not_found -> lookup_in_library ()) + in + choices + in +(* + (* *) + let _ = + if benchmark then begin + let per_item_choices = + List.map + (fun dom_item -> + try + let len = List.length (lookup_choices dom_item) in + debug_print (lazy (sprintf "BENCHMARK %s: %d" + (string_of_domain_item dom_item) len)); + len + with No_choices _ -> 0) + thing_dom + in + max_refinements := List.fold_left ( * ) 1 per_item_choices; + actual_refinements := 0; + domain_size := List.length thing_dom; + choices_avg := + (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size) + end + in + (* *) +*) + + (* (3) test an interpretation filling with meta uninterpreted identifiers + *) + let test_env aliases todo_dom ugraph = + let rec aux env = function + | [] -> env + | Node (_, item, l) :: tl -> + let env = + Environment.add item + ("Implicit", + (match item with + | Id _ | Num _ -> + (fun _ _ _ -> Cic.Implicit (Some `Closed)) + | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) + env in + aux (aux env l) tl in + let filled_env = aux aliases todo_dom in + try + let localization_tbl = Cic.CicHash.create 503 in + let cic_thing = + interpretate_thing ~context:disambiguate_context ~env:filled_env + ~uri ~is_path:false thing ~localization_tbl + in +let foo () = + let k,ugraph1 = + refine_thing metasenv context uri cic_thing ugraph ~localization_tbl + in + (k , ugraph1 ) +in refine_profiler.HExtlib.profile foo () + with + | Try_again msg -> Uncertain (None,msg), ugraph + | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph + in + (* (4) build all possible interpretations *) + let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in + (* aux returns triples Ok/Uncertain/Ko *) + (* rem_dom is the concatenation of all the remaining domains *) + let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ = + (* debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); *) + match todo_dom with + | Node (locs,item,inner_dom) -> + debug_print (lazy (sprintf "CHOOSED ITEM: %s" + (string_of_domain_item item))); + let choices = + match lookup_in_todo_dom with + None -> lookup_choices item + | Some choices -> choices in + match choices with + [] -> + [], [], + [aliases, diff, Some (List.hd locs), + lazy ("No choices for " ^ string_of_domain_item item), + true] +(* + | [codomain_item] -> + (* just one choice. We perform a one-step look-up and + if the next set of choices is also a singleton we + skip this refinement step *) + debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); + let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in + let lookup_in_todo_dom,next_choice_is_single = + match remaining_dom with + [] -> None,false + | (_,he)::_ -> + let choices = lookup_choices he in + Some choices,List.length choices = 1 + in + if next_choice_is_single then + aux new_env new_diff lookup_in_todo_dom remaining_dom + base_univ + else + (match test_env new_env remaining_dom base_univ with + | Ok (thing, metasenv),new_univ -> + (match remaining_dom with + | [] -> + [ new_env, new_diff, metasenv, thing, new_univ ], [] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Uncertain (loc,msg),new_univ -> + (match remaining_dom with + | [] -> [], [new_env,new_diff,loc,msg,true] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true]) +*) + | _::_ -> + let outcomes = + List.map + (function codomain_item -> + debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); + let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in + test_env new_env (inner_dom@rem_dom) base_univ, + new_env,new_diff + ) choices in + let some_outcome_ok = + List.exists + (function + (Ok (_,_),_),_,_ + | (Uncertain (_,_),_),_,_ -> true + | _ -> false) + outcomes in + let rec filter univ = function + | [] -> [],[],[] + | (outcome,new_env,new_diff) :: tl -> + match outcome with + | Ok (thing, metasenv),new_univ -> + let res = + (match inner_dom with + | [] -> + [new_env,new_diff,metasenv,thing,new_univ], [], [] + | _ -> + visit_children new_env new_diff new_univ rem_dom inner_dom) + in + res @@ filter univ tl + | Uncertain (loc,msg),new_univ -> + let res = + (match inner_dom with + | [] -> [],[new_env,new_diff,loc,msg,new_univ],[] + | _ -> + visit_children new_env new_diff new_univ rem_dom inner_dom) + in + res @@ filter univ tl + | Ko (loc,msg),_ -> + let res = + [],[],[new_env,new_diff,loc,msg,not some_outcome_ok] + in + res @@ filter univ tl + in + filter base_univ outcomes + and visit_children env diff univ rem_dom = + function + [] -> assert false + | [dom] -> aux env diff None dom rem_dom univ + | dom::remaining_dom -> + let ok_l,uncertain_l,error_l = + aux env diff None dom (remaining_dom@rem_dom) univ + in + let res_after_ok_l = + List.fold_right + (fun (env,diff,_,_,univ) res -> + visit_children env diff univ rem_dom remaining_dom + @@ res + ) ok_l ([],[],error_l) + in + List.fold_right + (fun (env,diff,_,_,univ) res -> + visit_children env diff univ rem_dom remaining_dom + @@ res + ) uncertain_l res_after_ok_l + in + let aux' aliases diff lookup_in_todo_dom todo_dom base_univ = + match test_env aliases todo_dom base_univ with + | Ok (thing, metasenv),new_univ -> + if todo_dom = [] then + [ aliases, diff, metasenv, thing, new_univ ], [], [] + else + visit_children aliases diff base_univ [] todo_dom +(* + _lookup_in_todo_dom_ +*) + | Uncertain (loc,msg),new_univ -> + if todo_dom = [] then + [],[aliases,diff,loc,msg,new_univ],[] + else + visit_children aliases diff base_univ [] todo_dom +(* + _lookup_in_todo_dom_ +*) + | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in + let base_univ = initial_ugraph in + try + let res = + match aux' aliases [] None todo_dom base_univ with + | [],uncertain,errors -> + debug_print (lazy "NO INTERPRETATIONS"); + let errors = + List.map + (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true) + ) uncertain @ errors + in + let errors = + List.map + (fun (env,diff,loc,msg,significant) -> + let env' = + filter_map_domain + (fun locs domain_item -> + try + let description = + fst (Environment.find domain_item env) + in + Some (locs,descr_of_domain_item domain_item,description) + with + Not_found -> None) + thing_dom + in + env',diff,loc,msg,significant + ) errors + in + raise (NoWellTypedInterpretation (0,errors)) + | [_,diff,metasenv,t,ugraph],_,_ -> + debug_print (lazy "SINGLE INTERPRETATION"); + [diff,metasenv,t,ugraph], false + | l,_,_ -> + debug_print + (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); + let choices = + List.map + (fun (env, _, _, _, _) -> + map_domain + (fun locs domain_item -> + let description = + fst (Environment.find domain_item env) + in + locs,descr_of_domain_item domain_item, description) + thing_dom) + l + in + let choosed = + C.interactive_interpretation_choice + thing_txt thing_txt_prefix_len choices + in + (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed), + true + in + res + with + CicEnvironment.CircularDependency s -> + failwith "Disambiguate: circular dependency" + + let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe + (text,prefix_len,term) + = + let term = + if fresh_instances then CicNotationUtil.freshen_term term else term + in + 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) + + let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri + (text,prefix_len,obj) + = + let obj = + if fresh_instances then CicNotationUtil.freshen_obj obj else obj + in + disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj + ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj + (text,prefix_len,obj) + end +