From: Enrico Tassi Date: Thu, 27 Nov 2008 12:39:24 +0000 (+0000) Subject: cic_disambiguation splitted into disambiguation and cic_disambiguation X-Git-Tag: make_still_working~4491 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4d41a527321e5fbdc10054b46ad60fe9f7f54a1;p=helm.git cic_disambiguation splitted into disambiguation and cic_disambiguation --- diff --git a/helm/software/components/METAS/meta.helm-cic_disambiguation.src b/helm/software/components/METAS/meta.helm-cic_disambiguation.src index d2e467aae..6a5d3a38d 100644 --- a/helm/software/components/METAS/meta.helm-cic_disambiguation.src +++ b/helm/software/components/METAS/meta.helm-cic_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-whelp helm-acic_content helm-cic_unification" +requires="helm-whelp helm-acic_content helm-cic_unification helm-disambiguation" version="0.0.1" archive(byte)="cic_disambiguation.cma" archive(native)="cic_disambiguation.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index afe6c3f82..9565ddb29 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -30,6 +30,7 @@ MODULES = \ whelp \ tactics \ acic_procedural \ + disambiguation \ cic_disambiguation \ lexicon \ grafite_engine \ diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend index 6ad263c49..9fd0c6639 100644 --- a/helm/software/components/cic_disambiguation/.depend +++ b/helm/software/components/cic_disambiguation/.depend @@ -1,15 +1,6 @@ -disambiguateChoices.cmi: disambiguateTypes.cmi -disambiguate.cmi: disambiguateTypes.cmi -cicDisambiguate.cmi: disambiguateTypes.cmi disambiguate.cmi -disambiguateTypes.cmo: disambiguateTypes.cmi -disambiguateTypes.cmx: disambiguateTypes.cmi -disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi -disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi -disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi -disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi -cicDisambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi \ - cicDisambiguate.cmi -cicDisambiguate.cmx: disambiguateTypes.cmx disambiguate.cmx \ - cicDisambiguate.cmi -number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi -number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx +disambiguateChoices.cmo: disambiguateChoices.cmi +disambiguateChoices.cmx: disambiguateChoices.cmi +cicDisambiguate.cmo: cicDisambiguate.cmi +cicDisambiguate.cmx: cicDisambiguate.cmi +number_notation.cmo: disambiguateChoices.cmi +number_notation.cmx: disambiguateChoices.cmx diff --git a/helm/software/components/cic_disambiguation/Makefile b/helm/software/components/cic_disambiguation/Makefile index ca4882158..2dc2984de 100644 --- a/helm/software/components/cic_disambiguation/Makefile +++ b/helm/software/components/cic_disambiguation/Makefile @@ -1,10 +1,7 @@ - PACKAGE = cic_disambiguation NOTATIONS = number INTERFACE_FILES = \ - disambiguateTypes.mli \ disambiguateChoices.mli \ - disambiguate.mli \ cicDisambiguate.mli IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ @@ -21,13 +18,3 @@ include ../Makefile.common OCAMLARCHIVEOPTIONS += -linkall -disambiguateTypes.cmi: disambiguateTypes.mli - @echo " OCAMLC -rectypes $<" - @$(OCAMLC) -c -rectypes $< -disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi - @echo " OCAMLC -rectypes $<" - @$(OCAMLC) -c -rectypes $< -disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi - @echo " OCAMLOPT -rectypes $<" - @$(OCAMLOPT) -c -rectypes $< - diff --git a/helm/software/components/cic_disambiguation/disambiguate.crit2.ml b/helm/software/components/cic_disambiguation/disambiguate.crit2.ml deleted file mode 100644 index 7aeb65a21..000000000 --- a/helm/software/components/cic_disambiguation/disambiguate.crit2.ml +++ /dev/null @@ -1,1317 +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: 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 - diff --git a/helm/software/components/cic_disambiguation/disambiguate.crit4.ml b/helm/software/components/cic_disambiguation/disambiguate.crit4.ml deleted file mode 100644 index 0a966ba3a..000000000 --- a/helm/software/components/cic_disambiguation/disambiguate.crit4.ml +++ /dev/null @@ -1,1294 +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: 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 * CicUniv.universe_graph - | 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) - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (Lazy.force msg))); - Ko (loc,msg) - | 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) - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko (loc,msg) - | 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:env ~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 env))); - debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s" - (match universe with None -> "None" | Some _ -> "Some _"))); -*) - let current_dom = - Environment.fold (fun item _ dom -> item :: dom) env [] 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 env todo_dom = - 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 env 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 () = - refine_thing - metasenv context uri cic_thing initial_ugraph ~localization_tbl -in refine_profiler.HExtlib.profile foo () - with - | Try_again msg -> Uncertain (None,msg) - | Invalid_choice (loc,msg) -> Ko (loc,msg) - 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 envs_and_diffs lookup_in_todo_dom todo_dom rem_dom = - assert(lookup_in_todo_dom = None); (* to be removed *) - (* 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 - [] -> - [], [], - List.map - (function (env,diff) -> - env, diff, Some (List.hd locs), - lazy ("No choices for " ^ string_of_domain_item item), - true - ) envs_and_diffs -(*{{{ - | [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.flatten - (List.map - (function codomain_item -> - List.map - (function (env,diff) -> - debug_print(lazy(sprintf"%s CHOSEN"(fst codomain_item))); - let new_env = Environment.add item codomain_item env in - let new_diff = (item,codomain_item)::diff in - test_env new_env (inner_dom@rem_dom), new_env,new_diff - ) envs_and_diffs - ) choices) in - let some_outcome_ok = - List.exists - (function - (Ok (_,_,_)),_,_ - | (Uncertain (_,_)),_,_ -> true - | _ -> false) - outcomes in - let res = - List.fold_right - (fun (outcome,env,diff) res -> - (match outcome with - | Ok (thing, metasenv, univ) -> - [env,diff,metasenv,thing,univ],[],[] - | Uncertain (loc,msg) -> - [],[env,diff,loc,msg],[] - | Ko (loc,msg) -> - [],[],[env,diff,loc,msg,not some_outcome_ok]) @@ res - ) outcomes ([],[],[]) - in - visit_children res rem_dom inner_dom - and visit_children res rem_dom inner_dom = - let rec vc_aux ((ok_l,uncertain_l,error_l) as res) = - function - [] -> res - | dom::remaining_dom -> - let envs_and_diffs = - List.map (fun (env,diff,_,_,_) -> env,diff) ok_l @ - List.map (fun (env,diff,_,_) -> env,diff) uncertain_l - in - let res = aux envs_and_diffs None dom (remaining_dom@rem_dom) in - vc_aux (([],[],error_l) @@ res) remaining_dom - in - vc_aux res inner_dom - in - let aux' env diff lookup_in_todo_dom todo_dom = - match test_env env todo_dom with - | Ok (thing, metasenv,new_univ) -> - visit_children ([ env, diff, metasenv, thing, new_univ ],[],[]) - [] todo_dom -(* - _lookup_in_todo_dom_ -*) - | Uncertain (loc,msg) -> - visit_children ([],[env,diff,loc,msg],[]) [] todo_dom -(* - _lookup_in_todo_dom_ -*) - | Ko (loc,msg) -> [],[],[env,diff,loc,msg,true] in - try - let res = - match aux' env [] None todo_dom 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 - diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml deleted file mode 100644 index 4ef0d1058..000000000 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ /dev/null @@ -1,731 +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 - -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 * string) list * - (Stdpp.location * 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 'term aliases = bool * 'term 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 ('term,'metasenv,'subst,'graph) test_result = - | Ok of 'term * 'metasenv * 'subst * 'graph - | Ko of (Stdpp.location * string) Lazy.t - | Uncertain of (Stdpp.location * string) Lazy.t - -let resolve (env: 'term 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 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)) - @ dom - @ 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 = - let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in - 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) - -let domain_of_ast_term = domain_of_term;; - -let domain_of_term ~context term = - let context = - List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context - in - domain_of_term ~context term - (* 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_thing: - context:'context -> - metasenv:'metasenv -> - subst:'subst -> - mk_implicit:(bool -> 'refined_term) -> - initial_ugraph:'ugraph -> - hint: - ('metasenv -> 'raw_thing -> 'raw_thing) * - (('refined_thing,'metasenv,'subst,'ugraph) test_result -> - ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> - aliases:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> - universe:'refined_term DisambiguateTypes.codomain_item list - DisambiguateTypes.Environment.t option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - 'refined_term DisambiguateTypes.codomain_item list) -> - uri:'uri -> - pp_thing:('ast_thing -> string) -> - domain_of_thing:(context:'context -> 'ast_thing -> domain) -> - interpretate_thing:( - context:'context -> - env:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> - uri:'uri -> - is_path:bool -> - 'ast_thing -> - localization_tbl:'cichash -> - 'raw_thing) -> - refine_thing:( - 'metasenv -> 'subst -> 'context -> 'uri -> - 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> - ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> - localization_tbl:'cichash -> - string * int * 'ast_thing -> - ((DisambiguateTypes.Environment.key * - 'refined_term DisambiguateTypes.codomain_item) list * - 'metasenv * 'subst * 'refined_thing * 'ugraph) - list * bool -end - -module Make (C: Callbacks) = - struct -let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" - - let disambiguate_thing - ~context ~metasenv ~subst ~mk_implicit - ~initial_ugraph:base_univ ~hint - ~aliases ~universe ~lookup_in_library - ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing - ~localization_tbl - (thing_txt,thing_txt_prefix_len,thing) - = - debug_print (lazy "DISAMBIGUATE INPUT"); - debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); - let thing_dom = domain_of_thing ~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 = - match universe with - | None -> - lookup_in_library - C.interactive_user_uri_choice - C.input_or_locate_uri item - | 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 - C.interactive_user_uri_choice - C.input_or_locate_uri item) - 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 _ _ _ -> mk_implicit true) - | Symbol _ -> (fun _ _ _ -> mk_implicit false))) - env in - aux (aux env l) tl in - let filled_env = aux aliases todo_dom in - try - let cic_thing = - interpretate_thing ~context ~env:filled_env - ~uri ~is_path:false thing ~localization_tbl - in - let cic_thing = (fst hint) metasenv cic_thing in -let foo () = - let k = - refine_thing metasenv subst - context uri cic_thing ugraph ~localization_tbl - in - let k = (snd hint) k in - k -in refine_profiler.HExtlib.profile foo () - with - | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) - | Invalid_choice loc_msg -> Ko loc_msg - 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 remainin domains *) - let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom = - debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); - match todo_dom with - | [] -> - assert (lookup_in_todo_dom = None); - (match test_env aliases rem_dom base_univ with - | Ok (thing, metasenv,subst,new_univ) -> - [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] - | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] - | Uncertain loc_msg -> - [],[aliases,diff,loc_msg],[]) - | Node (locs,item,inner_dom) :: 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 - [] -> - [], [], - [aliases, diff, - (lazy (List.hd locs, - "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 mark_not_significant failures = - List.map - (fun (env, diff, loc_msg, _b) -> - env, diff, loc_msg, false) - failures in - let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = - if ok_l <> [] || uncertain_l <> [] then - ok_l,uncertain_l,mark_not_significant error_l - else - outcome in - let rec filter = 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 - (inner_dom@remaining_dom@rem_dom) base_univ - with - | Ok (thing, metasenv,subst,new_univ) -> - let res = - (match inner_dom with - | [] -> - [new_env,new_diff,metasenv,subst,thing,new_univ], - [], [] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Uncertain loc_msg -> - let res = - (match inner_dom with - | [] -> [],[new_env,new_diff,loc_msg],[] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Ko loc_msg -> - let res = [],[],[new_env,new_diff,loc_msg,true] in - res @@ filter tl) - in - let ok_l,uncertain_l,error_l = - classify_errors (filter choices) - in - let res_after_ok_l = - List.fold_right - (fun (env,diff,_,_,_,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) ok_l ([],[],error_l) - in - List.fold_right - (fun (env,diff,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) uncertain_l res_after_ok_l - in - let aux' aliases diff lookup_in_todo_dom todo_dom = - match test_env aliases todo_dom base_univ with - | Ok _ - | Uncertain _ -> - aux aliases diff lookup_in_todo_dom todo_dom [] - | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in - try - let res = - match aux' aliases [] None todo_dom with - | [],uncertain,errors -> - 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 - let diff= List.map (fun a,b -> a,fst b) diff in - env',diff,loc_msg,significant - ) errors - in - raise (NoWellTypedInterpretation (0,errors)) - | [_,diff,metasenv,subst,t,ugraph],_,_ -> - debug_print (lazy "SINGLE INTERPRETATION"); - [diff,metasenv,subst,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,s,t,u= List.nth l n in d,m,s,t,u) - choosed), - true - in - res - with - CicEnvironment.CircularDependency s -> - failwith "Disambiguate: circular dependency" - - end - - diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli deleted file mode 100644 index 92e11870f..000000000 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ /dev/null @@ -1,117 +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/ - *) - -(** {2 Disambiguation interface} *) - -(* the integer is an offset to be added to each location *) -(* list of located error messages, each list is a tuple: - * - environment in string form - * - environment patch - * - location - * - error message - * - significancy of the error message, if false the error is likely to be - * useless for the final user ... *) -exception NoWellTypedInterpretation of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * string) list * - (Stdpp.location * string) Lazy.t * - bool) list -exception PathNotWellFormed - -type 'a disambiguator_input = string * int * 'a - -type domain = domain_tree list -and domain_tree = - Node of Stdpp.location list * DisambiguateTypes.domain_item * domain - -type ('term,'metasenv,'subst,'graph) test_result = - | Ok of 'term * 'metasenv * 'subst * 'graph - | Ko of (Stdpp.location * string) Lazy.t - | Uncertain of (Stdpp.location * string) Lazy.t - -exception Try_again of string Lazy.t - -val resolve : - 'term DisambiguateTypes.environment -> - DisambiguateTypes.Environment.key -> - ?num:string -> ?args:'term list -> unit -> 'term - -val find_in_context: string -> Cic.name list -> int - -val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain -val domain_of_term: context: - (Cic.name * 'a) option list -> CicNotationPt.term -> domain -val domain_of_obj: - context:(Cic.name * 'a) option list -> - CicNotationPt.term CicNotationPt.obj -> domain - -module type Disambiguator = -sig - val disambiguate_thing: - context:'context -> - metasenv:'metasenv -> - subst:'subst -> - mk_implicit:(bool -> 'refined_term) -> - initial_ugraph:'ugraph -> - hint: - ('metasenv -> 'raw_thing -> 'raw_thing) * - (('refined_thing,'metasenv,'subst,'ugraph) test_result -> - ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> - aliases:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> - universe:'refined_term DisambiguateTypes.codomain_item list - DisambiguateTypes.Environment.t option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - 'refined_term DisambiguateTypes.codomain_item list) -> - uri:'uri -> - pp_thing:('ast_thing -> string) -> - domain_of_thing:(context:'context -> 'ast_thing -> domain) -> - interpretate_thing:( - context:'context -> - env:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> - uri:'uri -> - is_path:bool -> - 'ast_thing -> - localization_tbl:'cichash -> - 'raw_thing) -> - refine_thing:( - 'metasenv -> 'subst -> 'context -> 'uri -> - 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> - ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> - localization_tbl:'cichash -> - string * int * 'ast_thing -> - ((DisambiguateTypes.Environment.key * - 'refined_term DisambiguateTypes.codomain_item) list * - 'metasenv * 'subst * 'refined_thing * 'ugraph) - list * bool -end - -module Make (C : DisambiguateTypes.Callbacks) : Disambiguator - diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/cic_disambiguation/disambiguateTypes.ml deleted file mode 100644 index 0ed285af0..000000000 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml +++ /dev/null @@ -1,138 +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$ *) - -(* -type term = CicNotationPt.term -type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic -type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical -type script_entry = - | Command of tactical - | Comment of CicNotationPt.location * string -type script = CicNotationPt.location * script_entry list -*) - -type domain_item = - | Id of string (* literal *) - | Symbol of string * int (* literal, instance num *) - | Num of int (* instance num *) - -exception Invalid_choice of (Stdpp.location * string) Lazy.t - -module OrderedDomain = - struct - type t = domain_item - let compare = Pervasives.compare - end - -(* module Domain = Set.Make (OrderedDomain) *) -module Environment = -struct - module Environment' = Map.Make (OrderedDomain) - - include Environment' - - let find k env = - match k with - Symbol (sym,n) -> - (try find k env - with Not_found -> find (Symbol (sym,0)) env) - | Num n -> - (try find k env - with Not_found -> find (Num 0) env) - | _ -> find k env - - let cons k v env = - try - let current = find k env in - let dsc, _ = v in - add k (v :: (List.filter (fun (dsc', _) -> dsc' <> dsc) current)) env - with Not_found -> - add k [v] env - - let hd list_env = - try - map List.hd list_env - with Failure _ -> assert false - - let fold_flatten f env base = - fold - (fun k l acc -> List.fold_right (fun v acc -> f k v acc) l acc) - env base - -end - -type 'term codomain_item = - string * (* description *) - ('term environment -> string -> 'term list -> 'term) - (* environment, literal number, arguments as needed *) - -and 'term environment = 'term codomain_item Environment.t - -type 'term multiple_environment = 'term codomain_item list Environment.t - - -(** adds a (name,uri) list l to a disambiguation environment e **) -let multiple_env_of_list l e = - List.fold_left - (fun e (name,descr,t) -> Environment.cons (Id name) (descr,fun _ _ _ -> t) e) - e l - -let env_of_list l e = - List.fold_left - (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e) - e l - -type interactive_user_uri_choice_type = - selection_mode:[`SINGLE | `MULTIPLE] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> id:string -> UriManager.uri list -> - UriManager.uri list - -type interactive_interpretation_choice_type = string -> int -> - (Stdpp.location list * string * string) list list -> int list - -type input_or_locate_uri_type = - title:string -> ?id:string -> unit -> UriManager.uri option - -module type Callbacks = - sig - val interactive_user_uri_choice : interactive_user_uri_choice_type - - val interactive_interpretation_choice : - interactive_interpretation_choice_type - - val input_or_locate_uri: input_or_locate_uri_type - end - -let string_of_domain_item = function - | Id s -> Printf.sprintf "ID(%s)" s - | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i - | Num i -> Printf.sprintf "NUM(instance %d)" i - -let string_of_domain dom = - String.concat "; " (List.map string_of_domain_item dom) diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/cic_disambiguation/disambiguateTypes.mli deleted file mode 100644 index ae157e268..000000000 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.mli +++ /dev/null @@ -1,101 +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/ - *) - -type domain_item = - | Id of string (* literal *) - | Symbol of string * int (* literal, instance num *) - | Num of int (* instance num *) - -(* module Domain: Set.S with type elt = domain_item *) -module Environment: -sig - include Map.S with type key = domain_item - val cons: domain_item -> ('a * 'b) -> ('a * 'b) list t -> ('a * 'b) list t - val hd: 'a list t -> 'a t - - (** last alias cons-ed will be processed first *) - val fold_flatten: (domain_item -> 'a -> 'b -> 'b) -> 'a list t -> 'b -> 'b -end - - (** to be raised when a choice is invalid due to some given parameter (e.g. - * wrong number of Cic.term arguments received) *) -exception Invalid_choice of (Stdpp.location * string) Lazy.t - -type 'term codomain_item = - string * (* description *) - ('term environment -> string -> 'term list -> 'term) - (* environment, literal number, arguments as needed *) - -and 'term environment = 'term codomain_item Environment.t - -type 'term multiple_environment = 'term codomain_item list Environment.t - -(* a simple case of extension of a disambiguation environment *) -val env_of_list: - (string * string * 'term) list -> 'term environment -> 'term environment - -val multiple_env_of_list: - (string * string * 'term) list -> 'term multiple_environment -> - 'term multiple_environment - -type interactive_user_uri_choice_type = - selection_mode:[`SINGLE | `MULTIPLE] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> id:string -> UriManager.uri list -> - UriManager.uri list - -type interactive_interpretation_choice_type = string -> int -> - (Stdpp.location list * string * string) list list -> int list - -type input_or_locate_uri_type = - title:string -> ?id:string -> unit -> UriManager.uri option - -module type Callbacks = - sig - - val interactive_user_uri_choice : interactive_user_uri_choice_type - - val interactive_interpretation_choice : - interactive_interpretation_choice_type - - val input_or_locate_uri: input_or_locate_uri_type - end - -val string_of_domain_item: domain_item -> string -val string_of_domain: domain_item list -> string - -(** {3 type shortands} *) - -(* -type term = CicNotationPt.term -type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic -type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical - -type script_entry = - | Command of tactical - | Comment of CicNotationPt.location * string -type script = CicNotationPt.location * script_entry list -*) diff --git a/helm/software/components/disambiguation/Makefile b/helm/software/components/disambiguation/Makefile new file mode 100644 index 000000000..b961efbff --- /dev/null +++ b/helm/software/components/disambiguation/Makefile @@ -0,0 +1,28 @@ +PACKAGE = disambiguation +INTERFACE_FILES = \ + disambiguateTypes.mli \ + disambiguate.mli +IMPLEMENTATION_FILES = \ + $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ + $(patsubst %,%_notation.ml,$(NOTATIONS)) + +all: + +clean: +distclean: + +include ../../Makefile.defs +include ../Makefile.common + +OCAMLARCHIVEOPTIONS += -linkall + +disambiguateTypes.cmi: disambiguateTypes.mli + @echo " OCAMLC -rectypes $<" + @$(OCAMLC) -c -rectypes $< +disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi + @echo " OCAMLC -rectypes $<" + @$(OCAMLC) -c -rectypes $< +disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi + @echo " OCAMLOPT -rectypes $<" + @$(OCAMLOPT) -c -rectypes $< + diff --git a/helm/software/components/disambiguation/disambiguate.crit2.ml b/helm/software/components/disambiguation/disambiguate.crit2.ml new file mode 100644 index 000000000..7aeb65a21 --- /dev/null +++ b/helm/software/components/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 + diff --git a/helm/software/components/disambiguation/disambiguate.crit4.ml b/helm/software/components/disambiguation/disambiguate.crit4.ml new file mode 100644 index 000000000..0a966ba3a --- /dev/null +++ b/helm/software/components/disambiguation/disambiguate.crit4.ml @@ -0,0 +1,1294 @@ +(* 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 * CicUniv.universe_graph + | 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) + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppterm term) (Lazy.force msg))); + Ko (loc,msg) + | 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) + | CicRefine.RefineFailure msg -> + debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppobj obj) (Lazy.force msg))) ; + Ko (loc,msg) + | 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:env ~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 env))); + debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s" + (match universe with None -> "None" | Some _ -> "Some _"))); +*) + let current_dom = + Environment.fold (fun item _ dom -> item :: dom) env [] 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 env todo_dom = + 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 env 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 () = + refine_thing + metasenv context uri cic_thing initial_ugraph ~localization_tbl +in refine_profiler.HExtlib.profile foo () + with + | Try_again msg -> Uncertain (None,msg) + | Invalid_choice (loc,msg) -> Ko (loc,msg) + 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 envs_and_diffs lookup_in_todo_dom todo_dom rem_dom = + assert(lookup_in_todo_dom = None); (* to be removed *) + (* 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 + [] -> + [], [], + List.map + (function (env,diff) -> + env, diff, Some (List.hd locs), + lazy ("No choices for " ^ string_of_domain_item item), + true + ) envs_and_diffs +(*{{{ + | [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.flatten + (List.map + (function codomain_item -> + List.map + (function (env,diff) -> + debug_print(lazy(sprintf"%s CHOSEN"(fst codomain_item))); + let new_env = Environment.add item codomain_item env in + let new_diff = (item,codomain_item)::diff in + test_env new_env (inner_dom@rem_dom), new_env,new_diff + ) envs_and_diffs + ) choices) in + let some_outcome_ok = + List.exists + (function + (Ok (_,_,_)),_,_ + | (Uncertain (_,_)),_,_ -> true + | _ -> false) + outcomes in + let res = + List.fold_right + (fun (outcome,env,diff) res -> + (match outcome with + | Ok (thing, metasenv, univ) -> + [env,diff,metasenv,thing,univ],[],[] + | Uncertain (loc,msg) -> + [],[env,diff,loc,msg],[] + | Ko (loc,msg) -> + [],[],[env,diff,loc,msg,not some_outcome_ok]) @@ res + ) outcomes ([],[],[]) + in + visit_children res rem_dom inner_dom + and visit_children res rem_dom inner_dom = + let rec vc_aux ((ok_l,uncertain_l,error_l) as res) = + function + [] -> res + | dom::remaining_dom -> + let envs_and_diffs = + List.map (fun (env,diff,_,_,_) -> env,diff) ok_l @ + List.map (fun (env,diff,_,_) -> env,diff) uncertain_l + in + let res = aux envs_and_diffs None dom (remaining_dom@rem_dom) in + vc_aux (([],[],error_l) @@ res) remaining_dom + in + vc_aux res inner_dom + in + let aux' env diff lookup_in_todo_dom todo_dom = + match test_env env todo_dom with + | Ok (thing, metasenv,new_univ) -> + visit_children ([ env, diff, metasenv, thing, new_univ ],[],[]) + [] todo_dom +(* + _lookup_in_todo_dom_ +*) + | Uncertain (loc,msg) -> + visit_children ([],[env,diff,loc,msg],[]) [] todo_dom +(* + _lookup_in_todo_dom_ +*) + | Ko (loc,msg) -> [],[],[env,diff,loc,msg,true] in + try + let res = + match aux' env [] None todo_dom 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 + diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml new file mode 100644 index 000000000..4ef0d1058 --- /dev/null +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -0,0 +1,731 @@ +(* 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 + +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 * string) list * + (Stdpp.location * 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 'term aliases = bool * 'term 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 ('term,'metasenv,'subst,'graph) test_result = + | Ok of 'term * 'metasenv * 'subst * 'graph + | Ko of (Stdpp.location * string) Lazy.t + | Uncertain of (Stdpp.location * string) Lazy.t + +let resolve (env: 'term 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 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)) + @ dom + @ 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 = + let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in + 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) + +let domain_of_ast_term = domain_of_term;; + +let domain_of_term ~context term = + let context = + List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context + in + domain_of_term ~context term + (* 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_thing: + context:'context -> + metasenv:'metasenv -> + subst:'subst -> + mk_implicit:(bool -> 'refined_term) -> + initial_ugraph:'ugraph -> + hint: + ('metasenv -> 'raw_thing -> 'raw_thing) * + (('refined_thing,'metasenv,'subst,'ugraph) test_result -> + ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> + aliases:'refined_term DisambiguateTypes.codomain_item + DisambiguateTypes.Environment.t -> + universe:'refined_term DisambiguateTypes.codomain_item list + DisambiguateTypes.Environment.t option -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + 'refined_term DisambiguateTypes.codomain_item list) -> + uri:'uri -> + pp_thing:('ast_thing -> string) -> + domain_of_thing:(context:'context -> 'ast_thing -> domain) -> + interpretate_thing:( + context:'context -> + env:'refined_term DisambiguateTypes.codomain_item + DisambiguateTypes.Environment.t -> + uri:'uri -> + is_path:bool -> + 'ast_thing -> + localization_tbl:'cichash -> + 'raw_thing) -> + refine_thing:( + 'metasenv -> 'subst -> 'context -> 'uri -> + 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> + ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> + localization_tbl:'cichash -> + string * int * 'ast_thing -> + ((DisambiguateTypes.Environment.key * + 'refined_term DisambiguateTypes.codomain_item) list * + 'metasenv * 'subst * 'refined_thing * 'ugraph) + list * bool +end + +module Make (C: Callbacks) = + struct +let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" + + let disambiguate_thing + ~context ~metasenv ~subst ~mk_implicit + ~initial_ugraph:base_univ ~hint + ~aliases ~universe ~lookup_in_library + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + ~localization_tbl + (thing_txt,thing_txt_prefix_len,thing) + = + debug_print (lazy "DISAMBIGUATE INPUT"); + debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); + let thing_dom = domain_of_thing ~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 = + match universe with + | None -> + lookup_in_library + C.interactive_user_uri_choice + C.input_or_locate_uri item + | 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 + C.interactive_user_uri_choice + C.input_or_locate_uri item) + 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 _ _ _ -> mk_implicit true) + | Symbol _ -> (fun _ _ _ -> mk_implicit false))) + env in + aux (aux env l) tl in + let filled_env = aux aliases todo_dom in + try + let cic_thing = + interpretate_thing ~context ~env:filled_env + ~uri ~is_path:false thing ~localization_tbl + in + let cic_thing = (fst hint) metasenv cic_thing in +let foo () = + let k = + refine_thing metasenv subst + context uri cic_thing ugraph ~localization_tbl + in + let k = (snd hint) k in + k +in refine_profiler.HExtlib.profile foo () + with + | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) + | Invalid_choice loc_msg -> Ko loc_msg + 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 remainin domains *) + let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom = + debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); + match todo_dom with + | [] -> + assert (lookup_in_todo_dom = None); + (match test_env aliases rem_dom base_univ with + | Ok (thing, metasenv,subst,new_univ) -> + [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] + | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] + | Uncertain loc_msg -> + [],[aliases,diff,loc_msg],[]) + | Node (locs,item,inner_dom) :: 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 + [] -> + [], [], + [aliases, diff, + (lazy (List.hd locs, + "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 mark_not_significant failures = + List.map + (fun (env, diff, loc_msg, _b) -> + env, diff, loc_msg, false) + failures in + let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = + if ok_l <> [] || uncertain_l <> [] then + ok_l,uncertain_l,mark_not_significant error_l + else + outcome in + let rec filter = 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 + (inner_dom@remaining_dom@rem_dom) base_univ + with + | Ok (thing, metasenv,subst,new_univ) -> + let res = + (match inner_dom with + | [] -> + [new_env,new_diff,metasenv,subst,thing,new_univ], + [], [] + | _ -> + aux new_env new_diff None inner_dom + (remaining_dom@rem_dom) + ) + in + res @@ filter tl + | Uncertain loc_msg -> + let res = + (match inner_dom with + | [] -> [],[new_env,new_diff,loc_msg],[] + | _ -> + aux new_env new_diff None inner_dom + (remaining_dom@rem_dom) + ) + in + res @@ filter tl + | Ko loc_msg -> + let res = [],[],[new_env,new_diff,loc_msg,true] in + res @@ filter tl) + in + let ok_l,uncertain_l,error_l = + classify_errors (filter choices) + in + let res_after_ok_l = + List.fold_right + (fun (env,diff,_,_,_,_) res -> + aux env diff None remaining_dom rem_dom @@ res + ) ok_l ([],[],error_l) + in + List.fold_right + (fun (env,diff,_) res -> + aux env diff None remaining_dom rem_dom @@ res + ) uncertain_l res_after_ok_l + in + let aux' aliases diff lookup_in_todo_dom todo_dom = + match test_env aliases todo_dom base_univ with + | Ok _ + | Uncertain _ -> + aux aliases diff lookup_in_todo_dom todo_dom [] + | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in + try + let res = + match aux' aliases [] None todo_dom with + | [],uncertain,errors -> + 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 + let diff= List.map (fun a,b -> a,fst b) diff in + env',diff,loc_msg,significant + ) errors + in + raise (NoWellTypedInterpretation (0,errors)) + | [_,diff,metasenv,subst,t,ugraph],_,_ -> + debug_print (lazy "SINGLE INTERPRETATION"); + [diff,metasenv,subst,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,s,t,u= List.nth l n in d,m,s,t,u) + choosed), + true + in + res + with + CicEnvironment.CircularDependency s -> + failwith "Disambiguate: circular dependency" + + end + + diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli new file mode 100644 index 000000000..92e11870f --- /dev/null +++ b/helm/software/components/disambiguation/disambiguate.mli @@ -0,0 +1,117 @@ +(* 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/ + *) + +(** {2 Disambiguation interface} *) + +(* the integer is an offset to be added to each location *) +(* list of located error messages, each list is a tuple: + * - environment in string form + * - environment patch + * - location + * - error message + * - significancy of the error message, if false the error is likely to be + * useless for the final user ... *) +exception NoWellTypedInterpretation of + int * + ((Stdpp.location list * string * string) list * + (DisambiguateTypes.domain_item * string) list * + (Stdpp.location * string) Lazy.t * + bool) list +exception PathNotWellFormed + +type 'a disambiguator_input = string * int * 'a + +type domain = domain_tree list +and domain_tree = + Node of Stdpp.location list * DisambiguateTypes.domain_item * domain + +type ('term,'metasenv,'subst,'graph) test_result = + | Ok of 'term * 'metasenv * 'subst * 'graph + | Ko of (Stdpp.location * string) Lazy.t + | Uncertain of (Stdpp.location * string) Lazy.t + +exception Try_again of string Lazy.t + +val resolve : + 'term DisambiguateTypes.environment -> + DisambiguateTypes.Environment.key -> + ?num:string -> ?args:'term list -> unit -> 'term + +val find_in_context: string -> Cic.name list -> int + +val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain +val domain_of_term: context: + (Cic.name * 'a) option list -> CicNotationPt.term -> domain +val domain_of_obj: + context:(Cic.name * 'a) option list -> + CicNotationPt.term CicNotationPt.obj -> domain + +module type Disambiguator = +sig + val disambiguate_thing: + context:'context -> + metasenv:'metasenv -> + subst:'subst -> + mk_implicit:(bool -> 'refined_term) -> + initial_ugraph:'ugraph -> + hint: + ('metasenv -> 'raw_thing -> 'raw_thing) * + (('refined_thing,'metasenv,'subst,'ugraph) test_result -> + ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> + aliases:'refined_term DisambiguateTypes.codomain_item + DisambiguateTypes.Environment.t -> + universe:'refined_term DisambiguateTypes.codomain_item list + DisambiguateTypes.Environment.t option -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + 'refined_term DisambiguateTypes.codomain_item list) -> + uri:'uri -> + pp_thing:('ast_thing -> string) -> + domain_of_thing:(context:'context -> 'ast_thing -> domain) -> + interpretate_thing:( + context:'context -> + env:'refined_term DisambiguateTypes.codomain_item + DisambiguateTypes.Environment.t -> + uri:'uri -> + is_path:bool -> + 'ast_thing -> + localization_tbl:'cichash -> + 'raw_thing) -> + refine_thing:( + 'metasenv -> 'subst -> 'context -> 'uri -> + 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> + ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> + localization_tbl:'cichash -> + string * int * 'ast_thing -> + ((DisambiguateTypes.Environment.key * + 'refined_term DisambiguateTypes.codomain_item) list * + 'metasenv * 'subst * 'refined_thing * 'ugraph) + list * bool +end + +module Make (C : DisambiguateTypes.Callbacks) : Disambiguator + diff --git a/helm/software/components/disambiguation/disambiguateTypes.ml b/helm/software/components/disambiguation/disambiguateTypes.ml new file mode 100644 index 000000000..0ed285af0 --- /dev/null +++ b/helm/software/components/disambiguation/disambiguateTypes.ml @@ -0,0 +1,138 @@ +(* 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$ *) + +(* +type term = CicNotationPt.term +type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic +type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical +type script_entry = + | Command of tactical + | Comment of CicNotationPt.location * string +type script = CicNotationPt.location * script_entry list +*) + +type domain_item = + | Id of string (* literal *) + | Symbol of string * int (* literal, instance num *) + | Num of int (* instance num *) + +exception Invalid_choice of (Stdpp.location * string) Lazy.t + +module OrderedDomain = + struct + type t = domain_item + let compare = Pervasives.compare + end + +(* module Domain = Set.Make (OrderedDomain) *) +module Environment = +struct + module Environment' = Map.Make (OrderedDomain) + + include Environment' + + let find k env = + match k with + Symbol (sym,n) -> + (try find k env + with Not_found -> find (Symbol (sym,0)) env) + | Num n -> + (try find k env + with Not_found -> find (Num 0) env) + | _ -> find k env + + let cons k v env = + try + let current = find k env in + let dsc, _ = v in + add k (v :: (List.filter (fun (dsc', _) -> dsc' <> dsc) current)) env + with Not_found -> + add k [v] env + + let hd list_env = + try + map List.hd list_env + with Failure _ -> assert false + + let fold_flatten f env base = + fold + (fun k l acc -> List.fold_right (fun v acc -> f k v acc) l acc) + env base + +end + +type 'term codomain_item = + string * (* description *) + ('term environment -> string -> 'term list -> 'term) + (* environment, literal number, arguments as needed *) + +and 'term environment = 'term codomain_item Environment.t + +type 'term multiple_environment = 'term codomain_item list Environment.t + + +(** adds a (name,uri) list l to a disambiguation environment e **) +let multiple_env_of_list l e = + List.fold_left + (fun e (name,descr,t) -> Environment.cons (Id name) (descr,fun _ _ _ -> t) e) + e l + +let env_of_list l e = + List.fold_left + (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e) + e l + +type interactive_user_uri_choice_type = + selection_mode:[`SINGLE | `MULTIPLE] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> id:string -> UriManager.uri list -> + UriManager.uri list + +type interactive_interpretation_choice_type = string -> int -> + (Stdpp.location list * string * string) list list -> int list + +type input_or_locate_uri_type = + title:string -> ?id:string -> unit -> UriManager.uri option + +module type Callbacks = + sig + val interactive_user_uri_choice : interactive_user_uri_choice_type + + val interactive_interpretation_choice : + interactive_interpretation_choice_type + + val input_or_locate_uri: input_or_locate_uri_type + end + +let string_of_domain_item = function + | Id s -> Printf.sprintf "ID(%s)" s + | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i + | Num i -> Printf.sprintf "NUM(instance %d)" i + +let string_of_domain dom = + String.concat "; " (List.map string_of_domain_item dom) diff --git a/helm/software/components/disambiguation/disambiguateTypes.mli b/helm/software/components/disambiguation/disambiguateTypes.mli new file mode 100644 index 000000000..ae157e268 --- /dev/null +++ b/helm/software/components/disambiguation/disambiguateTypes.mli @@ -0,0 +1,101 @@ +(* 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/ + *) + +type domain_item = + | Id of string (* literal *) + | Symbol of string * int (* literal, instance num *) + | Num of int (* instance num *) + +(* module Domain: Set.S with type elt = domain_item *) +module Environment: +sig + include Map.S with type key = domain_item + val cons: domain_item -> ('a * 'b) -> ('a * 'b) list t -> ('a * 'b) list t + val hd: 'a list t -> 'a t + + (** last alias cons-ed will be processed first *) + val fold_flatten: (domain_item -> 'a -> 'b -> 'b) -> 'a list t -> 'b -> 'b +end + + (** to be raised when a choice is invalid due to some given parameter (e.g. + * wrong number of Cic.term arguments received) *) +exception Invalid_choice of (Stdpp.location * string) Lazy.t + +type 'term codomain_item = + string * (* description *) + ('term environment -> string -> 'term list -> 'term) + (* environment, literal number, arguments as needed *) + +and 'term environment = 'term codomain_item Environment.t + +type 'term multiple_environment = 'term codomain_item list Environment.t + +(* a simple case of extension of a disambiguation environment *) +val env_of_list: + (string * string * 'term) list -> 'term environment -> 'term environment + +val multiple_env_of_list: + (string * string * 'term) list -> 'term multiple_environment -> + 'term multiple_environment + +type interactive_user_uri_choice_type = + selection_mode:[`SINGLE | `MULTIPLE] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> msg:string -> id:string -> UriManager.uri list -> + UriManager.uri list + +type interactive_interpretation_choice_type = string -> int -> + (Stdpp.location list * string * string) list list -> int list + +type input_or_locate_uri_type = + title:string -> ?id:string -> unit -> UriManager.uri option + +module type Callbacks = + sig + + val interactive_user_uri_choice : interactive_user_uri_choice_type + + val interactive_interpretation_choice : + interactive_interpretation_choice_type + + val input_or_locate_uri: input_or_locate_uri_type + end + +val string_of_domain_item: domain_item -> string +val string_of_domain: domain_item list -> string + +(** {3 type shortands} *) + +(* +type term = CicNotationPt.term +type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic +type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical + +type script_entry = + | Command of tactical + | Comment of CicNotationPt.location * string +type script = CicNotationPt.location * script_entry list +*) diff --git a/helm/software/configure.ac b/helm/software/configure.ac index fd6ca23e1..f542372f8 100644 --- a/helm/software/configure.ac +++ b/helm/software/configure.ac @@ -73,10 +73,12 @@ zip \ # (Matita) findlib requisites FINDLIB_COMREQUIRES="\ +helm-disambiguation \ helm-cic_disambiguation \ helm-grafite \ helm-grafite_engine \ helm-tptp_grafite \ +helm-ng_disambiguation \ helm-grafite_parser \ helm-acic_procedural \ helm-content_pres \