X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;fp=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=0000000000000000000000000000000000000000;hb=55b82bd235d82ff7f0a40d980effe1efde1f5073;hp=667c50770536bb7187df52a2cc460991b32cf20f;hpb=771ee8b9d122fa963881c876e86f90531bb7434f;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml deleted file mode 100644 index 667c50770..000000000 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ /dev/null @@ -1,1009 +0,0 @@ -(* 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$ *) - -open Printf - -open DisambiguateTypes -open UriManager - -(* the integer is an offset to be added to each location *) -exception NoWellTypedInterpretation of - int * (Token.flocation option * string Lazy.t) 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 - -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 Token.flocation option * string Lazy.t - | Uncertain of Token.flocation 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 - (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 - (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 ~(context: Cic.name list) ~env ~uri ~is_path ast - ~localization_tbl -= - 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) = - 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 (lazy "The type of the term to be matched is not (co)inductive!"))) - | None -> - let fst_constructor = - match branches with - | ((head, _, _), _) :: _ -> head - | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined")) - in - (match resolve env (Id fst_constructor) () 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 (lazy "The type of the term to be matched is not (co)inductive!"))) - 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 1 -> `AvoidLetInNoAppl - | Cic.Appl (Cic.Rel 1::l) -> - (try - let l' = - List.map - (function t -> - let t',subst,metasenv = - CicMetaSubst.delift_rels [] [] 1 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 l' - | _ -> assert false - else - `AvoidLetIn 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 ((name, typ), body, decr_idx) -> - let cic_body = aux ~localize loc context' body in - let cic_type = - aux_option ~localize loc context (Some `Type) 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 counter = ref ~-1 in - let build_term funs = - (* this is the body of the fold_right function below. Rationale: Fix - * and CoFix cases differs only in an additional index in the - * inductiveFun list, see Cic.term *) - match kind with - | `Inductive -> - (fun (var, _, _, _) cic -> - incr counter; - let fix = Cic.Fix (!counter,funs) in - match cic with - `Recipe (`AddLetIn cic) -> - `Term (Cic.LetIn (Cic.Name var, fix, cic)) - | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l)) - | `Recipe `AvoidLetInNoAppl -> `Term fix - | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t))) - | `CoInductive -> - let funs = - List.map (fun (name, _, typ, body) -> (name, typ, body)) funs - in - (fun (var, _, _, _) cic -> - incr counter; - let cofix = Cic.CoFix (!counter,funs) in - match cic with - `Recipe (`AddLetIn cic) -> - `Term (Cic.LetIn (Cic.Name var, cofix, cic)) - | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l)) - | `Recipe `AvoidLetInNoAppl -> `Term cofix - | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t))) - in - (match - List.fold_right (build_term inductiveFuns) inductiveFuns - (`Recipe cic_body) - with - `Recipe _ -> assert false - | `Term t -> t) - | 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 (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 (lazy "??? Can this happen?")) - with - CicEnvironment.CircularDependency _ -> - raise (Invalid_choice (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 ~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) -> - Cic.Name 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 (Cic.Name 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) -> - (Cic.Name 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 (Cic.Name 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) -> - 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) -> x,y) 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 with - 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)) - - - (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *) -let rev_uniq = - let module SortedItem = - struct - type t = DisambiguateTypes.domain_item - let compare = Pervasives.compare - end - in - let module Set = Set.Make (SortedItem) in - fun l -> - let rev_l = List.rev l in - let (_, uniq_rev_l) = - List.fold_left - (fun (members, rev_l) elt -> - if Set.mem elt members then - (members, rev_l) - else - Set.add elt members, elt :: rev_l) - (Set.empty, []) rev_l - in - List.rev uniq_rev_l - -(* "aux" keeps domain in reverse order and doesn't care about duplicates. - * Domain item more in deep in the list will be processed first. - *) -let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function - | CicNotationPt.AttributedTerm (`Loc loc, term) -> - domain_rev_of_term ~loc context term - | CicNotationPt.AttributedTerm (_, term) -> - domain_rev_of_term ~loc context term - | CicNotationPt.Appl terms -> - List.fold_left - (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms - | CicNotationPt.Binder (kind, (var, typ), body) -> - let kind_dom = - match kind with - | `Exists -> [ Symbol ("exists", 0) ] - | _ -> [] - in - let type_dom = domain_rev_of_term_option loc context typ in - let body_dom = - domain_rev_of_term ~loc - (CicNotationUtil.cic_name_of_name var :: context) body - in - body_dom @ type_dom @ kind_dom - | CicNotationPt.Case (term, indty_ident, outtype, branches) -> - let term_dom = domain_rev_of_term ~loc context term in - let outtype_dom = domain_rev_of_term_option loc context outtype in - let get_first_constructor = function - | [] -> [] - | ((head, _, _), _) :: _ -> [ Id head ] - in - let do_branch ((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 -> domain_rev_of_term ~loc cont typ @ dom))) - (context, []) args - in - args_domain @ domain_rev_of_term ~loc term_context term - in - let branches_dom = - List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches - in - branches_dom @ outtype_dom @ term_dom @ - (match indty_ident with - | None -> get_first_constructor branches - | Some (ident, _) -> [ Id ident ]) - | CicNotationPt.Cast (term, ty) -> - let term_dom = domain_rev_of_term ~loc context term in - let ty_dom = domain_rev_of_term ~loc context ty in - ty_dom @ term_dom - | CicNotationPt.LetIn ((var, typ), body, where) -> - let body_dom = domain_rev_of_term ~loc context body in - let type_dom = domain_rev_of_term_option loc context typ in - let where_dom = - domain_rev_of_term ~loc - (CicNotationUtil.cic_name_of_name var :: context) where - in - where_dom @ type_dom @ body_dom - | CicNotationPt.LetRec (kind, defs, where) -> - let context' = - List.fold_left - (fun acc ((var, typ), _, _) -> - CicNotationUtil.cic_name_of_name var :: acc) - context defs - in - let where_dom = domain_rev_of_term ~loc context' where in - let defs_dom = - List.fold_left - (fun dom ((_, typ), body, _) -> - domain_rev_of_term ~loc context' body @ - domain_rev_of_term_option loc context typ) - [] defs - in - where_dom @ defs_dom - | CicNotationPt.Ident (name, subst) -> - (try - (* the next line can raise Not_found *) - ignore(find_in_context name context); - if subst <> None then - CicNotationPt.fail loc "Explicit substitutions not allowed here" - else - [] - with Not_found -> - (match subst with - | None -> [Id name] - | Some subst -> - List.fold_left - (fun dom (_, term) -> - let dom' = domain_rev_of_term ~loc context term in - dom' @ dom) - [Id name] subst)) - | CicNotationPt.Uri _ -> [] - | CicNotationPt.Implicit -> [] - | CicNotationPt.Num (num, i) -> [ Num i ] - | CicNotationPt.Meta (index, local_context) -> - List.fold_left - (fun dom term -> domain_rev_of_term_option loc context term @ dom) [] - local_context - | CicNotationPt.Sort _ -> [] - | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] - | CicNotationPt.UserInput - | CicNotationPt.Literal _ - | CicNotationPt.Layout _ - | CicNotationPt.Magic _ - | CicNotationPt.Variable _ -> assert false - -and domain_rev_of_term_option loc context = function - | None -> [] - | Some t -> domain_rev_of_term ~loc context t - -let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast) - -let domain_of_obj ~context ast = - assert (context = []); - let domain_rev = - match ast with - | CicNotationPt.Theorem (_,_,ty,bo) -> - (match bo with - None -> [] - | Some bo -> domain_rev_of_term [] bo) @ - domain_of_term [] ty - | CicNotationPt.Inductive (params,tyl) -> - let dom = - List.flatten ( - List.rev_map - (fun (_,_,ty,cl) -> - List.flatten ( - List.rev_map - (fun (_,ty) -> domain_rev_of_term [] ty) cl) @ - domain_rev_of_term [] ty) tyl) in - let dom = - List.fold_left - (fun dom (_,ty) -> - domain_rev_of_term [] ty @ dom - ) dom params - in - List.filter - (fun name -> - not ( List.exists (fun (name',_) -> name = Id name') params - || List.exists (fun (name',_,_,_) -> name = Id name') tyl) - ) dom - | CicNotationPt.Record (params,_,ty,fields) -> - let dom = - List.flatten - (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in - let dom = - List.fold_left - (fun dom (_,ty) -> - domain_rev_of_term [] ty @ dom - ) (dom @ domain_rev_of_term [] ty) params - in - List.filter - (fun name-> - not ( List.exists (fun (name',_) -> name = Id name') params - || List.exists (fun (name',_,_) -> name = Id name') fields) - ) dom - in - rev_uniq domain_rev - - (* dom1 \ dom2 *) -let domain_diff dom1 dom2 = -(* let domain_diff = Domain.diff *) - let is_in_dom2 = - List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt')) - (fun _ -> false) dom2 - in - List.filter (fun elt -> not (is_in_dom2 elt)) dom1 - -module type Disambiguator = -sig - val disambiguate_term : - ?fresh_instances:bool -> - dbd:HMysql.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 -> - ((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:HMysql.dbd -> - aliases:DisambiguateTypes.environment ->(* previous interpretation status *) - universe:DisambiguateTypes.multiple_environment option -> - uri:UriManager.uri option -> (* required only for inductive types *) - CicNotationPt.obj -> - ((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 - | [] -> - [(C.input_or_locate_uri - ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())] - | [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 - = - 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 - (* (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, _) -> - List.map DisambiguateChoices.mk_choice - (TermAcicContent.lookup_interpretations symb) - | 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 -> []) - 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 filled_env = - List.fold_left - (fun env item -> - Environment.add item - ("Implicit", - (match item with - | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) - | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) - 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 msg -> Ko (None,msg), ugraph - in - (* (4) build all possible interpretations *) - let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in - let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ = - match todo_dom with - | [] -> - assert (lookup_in_todo_dom = None); - (match test_env aliases [] base_univ with - | Ok (thing, metasenv),new_univ -> - [ aliases, diff, metasenv, thing, new_univ ], [] - | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg]) - | item :: remaining_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 - [] -> - [], [None,lazy ("No choices for " ^ string_of_domain_item item)] - | [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 - | [] -> [], [loc,msg] - | _ -> - aux new_env new_diff lookup_in_todo_dom - remaining_dom new_univ) - | Ko (loc,msg),_ -> [], [loc,msg]) - | _::_ -> - let rec filter univ = function - | [] -> [],[] - | codomain_item :: tl -> - 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 - (match test_env new_env remaining_dom univ with - | Ok (thing, metasenv),new_univ -> - (match remaining_dom with - | [] -> [ new_env, new_diff, metasenv, thing, new_univ ], [] - | _ -> aux new_env new_diff None remaining_dom new_univ - ) @@ - filter univ tl - | Uncertain (loc,msg),new_univ -> - (match remaining_dom with - | [] -> [],[loc,msg] - | _ -> aux new_env new_diff None remaining_dom new_univ - ) @@ - filter univ tl - | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl) - in - filter base_univ choices - in - let base_univ = initial_ugraph in - try - let res = - match aux aliases [] None todo_dom base_univ with - | [],errors -> 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, _, _, _, _) -> - List.map - (fun domain_item -> - let description = - fst (Environment.find domain_item env) - in - (descr_of_domain_item domain_item, description)) - thing_dom) - l - in - let choosed = C.interactive_interpretation_choice 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 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 - ~refine_thing:refine_term term - - let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri - 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 ~domain_of_thing:domain_of_obj - ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj - obj - end -