From 13bfd154ade0996d34e7e723398ac7ab76a51717 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 27 Nov 2008 12:24:38 +0000 Subject: [PATCH] 1. grafiteDisambiguator => multiPassDisambiguator 2. --- .../components/cic_disambiguation/.depend | 11 +- .../components/cic_disambiguation/.depend.opt | 11 +- .../components/cic_disambiguation/Makefile | 3 +- .../cic_disambiguation/disambiguate.ml | 723 +----------------- .../cic_disambiguation/disambiguate.mli | 125 +-- .../cic_disambiguation/disambiguateTypes.ml | 30 +- .../cic_disambiguation/disambiguateTypes.mli | 34 +- .../components/cic_proof_checking/.depend | 4 +- .../components/cic_proof_checking/.depend.opt | 4 +- .../components/grafite_parser/.depend | 8 +- .../components/grafite_parser/.depend.opt | 8 +- .../components/grafite_parser/Makefile | 2 +- .../grafite_parser/grafiteDisambiguate.ml | 17 +- ...mbiguator.ml => multiPassDisambiguator.ml} | 18 +- ...iguator.mli => multiPassDisambiguator.mli} | 16 +- .../ng_disambiguation/nDisambiguate.ml | 26 +- helm/software/components/ng_kernel/.depend | 12 +- .../software/components/ng_kernel/.depend.opt | 14 +- helm/software/components/ng_refiner/.depend | 4 +- helm/software/components/tactics/.depend | 4 +- helm/software/components/tactics/.depend.opt | 4 +- helm/software/matita/matita.ml | 4 +- helm/software/matita/matitaExcPp.ml | 2 +- helm/software/matita/matitaGui.ml | 12 +- helm/software/matita/matitaGui.mli | 4 +- helm/software/matita/matitaInit.ml | 2 +- helm/software/matita/matitaScript.ml | 6 +- 27 files changed, 204 insertions(+), 904 deletions(-) rename helm/software/components/grafite_parser/{grafiteDisambiguator.ml => multiPassDisambiguator.ml} (93%) rename helm/software/components/grafite_parser/{grafiteDisambiguator.mli => multiPassDisambiguator.mli} (80%) diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend index ca4124461..6ad263c49 100644 --- a/helm/software/components/cic_disambiguation/.depend +++ b/helm/software/components/cic_disambiguation/.depend @@ -1,12 +1,15 @@ 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 disambiguateChoices.cmi \ - disambiguate.cmi -disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \ - disambiguate.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 diff --git a/helm/software/components/cic_disambiguation/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt index ca4124461..6ad263c49 100644 --- a/helm/software/components/cic_disambiguation/.depend.opt +++ b/helm/software/components/cic_disambiguation/.depend.opt @@ -1,12 +1,15 @@ 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 disambiguateChoices.cmi \ - disambiguate.cmi -disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \ - disambiguate.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 diff --git a/helm/software/components/cic_disambiguation/Makefile b/helm/software/components/cic_disambiguation/Makefile index cd03e8281..ca4882158 100644 --- a/helm/software/components/cic_disambiguation/Makefile +++ b/helm/software/components/cic_disambiguation/Makefile @@ -4,7 +4,8 @@ NOTATIONS = number INTERFACE_FILES = \ disambiguateTypes.mli \ disambiguateChoices.mli \ - disambiguate.mli + disambiguate.mli \ + cicDisambiguate.mli IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ $(patsubst %,%_notation.ml,$(NOTATIONS)) diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 655747365..4ef0d1058 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -108,57 +108,6 @@ type ('term,'metasenv,'subst,'graph) test_result = | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t -let refine_term metasenv subst context uri term ugraph ~localization_tbl = -(* if benchmark then incr actual_refinements; *) - assert (uri=None); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); - try - let term', _, metasenv',ugraph1 = - CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in - (Ok (term', metasenv',[],ugraph1)) - with - exn -> - let rec process_exn loc = - function - HExtlib.Localized (loc,exn) -> process_exn loc exn - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Uncertain (lazy (loc,Lazy.force msg)) - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (Lazy.force msg))); - Ko (lazy (loc,Lazy.force msg)) - | exn -> raise exn - in - process_exn Stdpp.dummy_loc exn - -let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = - assert (context = []); - assert (metasenv = []); - assert (subst = []); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; - try - let obj', metasenv,ugraph = - CicRefine.typecheck metasenv uri obj ~localization_tbl - in - (Ok (obj', metasenv,[],ugraph)) - with - exn -> - let rec process_exn loc = - function - HExtlib.Localized (loc,exn) -> process_exn loc exn - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ - (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; - Uncertain (lazy (loc,Lazy.force msg)) - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) (Lazy.force msg))) ; - Ko (lazy (loc,Lazy.force msg)) - | exn -> raise exn - in - process_exn Stdpp.dummy_loc exn - let resolve (env: 'term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try snd (Environment.find item env) env num args @@ -175,504 +124,6 @@ let find_in_context name context = in aux 1 context -let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl -= - (* create_dummy_ids shouldbe used only for interpretating patterns *) - assert (uri = None); - let rec aux ~localize loc context = function - | CicNotationPt.AttributedTerm (`Loc loc, term) -> - let res = aux ~localize loc context term in - if localize then Cic.CicHash.add localization_tbl res loc; - res - | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term - | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> - let cic_args = List.map (aux ~localize loc context) args in - resolve env (Symbol (symb, i)) ~args:cic_args () - | CicNotationPt.Appl terms -> - Cic.Appl (List.map (aux ~localize loc context) terms) - | CicNotationPt.Binder (binder_kind, (var, typ), body) -> - let cic_type = aux_option ~localize loc context (Some `Type) typ in - let cic_name = CicNotationUtil.cic_name_of_name var in - let cic_body = aux ~localize loc (cic_name :: context) body in - (match binder_kind with - | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body) - | `Pi - | `Forall -> Cic.Prod (cic_name, cic_type, cic_body) - | `Exists -> - resolve env (Symbol ("exists", 0)) - ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ()) - | CicNotationPt.Case (term, indty_ident, outtype, branches) -> - let cic_term = aux ~localize loc context term in - let cic_outtype = aux_option ~localize loc context None outtype in - let do_branch ((head, _, args), term) = - let rec do_branch' context = function - | [] -> aux ~localize loc context term - | (name, typ) :: tl -> - let cic_name = CicNotationUtil.cic_name_of_name name in - let cic_body = do_branch' (cic_name :: context) tl in - let typ = - match typ with - | None -> Cic.Implicit (Some `Type) - | Some typ -> aux ~localize loc context typ - in - Cic.Lambda (cic_name, typ, cic_body) - in - do_branch' context args - in - let indtype_uri, indtype_no = - if create_dummy_ids then - (UriManager.uri_of_string "cic:/fake_indty.con", 0) - else - match indty_ident with - | Some (indty_ident, _) -> - (match resolve env (Id indty_ident) () with - | Cic.MutInd (uri, tyno, _) -> (uri, tyno) - | Cic.Implicit _ -> - raise (Try_again (lazy "The type of the term to be matched - is still unknown")) - | _ -> - raise (Invalid_choice (lazy (loc,"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 (lazy (loc,"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 (lazy (loc,"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 (lazy (loc, "Syntax error: the left hand side of a branch patterns must be \"_\""))) - ) branches - else - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with - Cic.InductiveDefinition (il,_,leftsno,_) -> - let _,_,_,cl = - try - List.nth il indtype_no - with _ -> assert false - in - let rec count_prod t = - match CicReduction.whd [] t with - Cic.Prod (_, _, t) -> 1 + (count_prod t) - | _ -> 0 - in - let rec sort branches cl = - match cl with - [] -> - let rec analyze unused unrecognized useless = - function - [] -> - if unrecognized != [] then - raise (Invalid_choice - (lazy (loc, - ("Unrecognized constructors: " ^ - String.concat " " unrecognized)))) - else if useless > 0 then - raise (Invalid_choice - (lazy (loc, - ("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 - (lazy (loc, ("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 - (lazy (loc,"Wrong number of arguments for " ^ - name))) - | Ast.Wildcard,term -> - let rec mk_lambdas = - function - 0 -> term - | n -> - CicNotationPt.Binder - (`Lambda, (CicNotationPt.Ident ("_", None), None), - mk_lambdas (n - 1)) - in - (("wildcard",None,[]), - mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl - in - sort branches cl - | _ -> assert false - in - Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, - (List.map do_branch branches)) - | CicNotationPt.Cast (t1, t2) -> - let cic_t1 = aux ~localize loc context t1 in - let cic_t2 = aux ~localize loc context t2 in - Cic.Cast (cic_t1, cic_t2) - | CicNotationPt.LetIn ((name, typ), def, body) -> - let cic_def = aux ~localize loc context def in - let cic_name = CicNotationUtil.cic_name_of_name name in - let cic_typ = - match typ with - | None -> Cic.Implicit (Some `Type) - | Some t -> aux ~localize loc context t - in - let cic_body = aux ~localize loc (cic_name :: context) body in - Cic.LetIn (cic_name, cic_def, cic_typ, cic_body) - | CicNotationPt.LetRec (kind, defs, body) -> - let context' = - List.fold_left - (fun acc (_, (name, _), _, _) -> - CicNotationUtil.cic_name_of_name name :: acc) - context defs - in - let cic_body = - let unlocalized_body = aux ~localize:false loc context' body in - match unlocalized_body with - Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n - | Cic.Appl (Cic.Rel n::l) when n <= List.length defs -> - (try - let l' = - List.map - (function t -> - let t',subst,metasenv = - CicMetaSubst.delift_rels [] [] (List.length defs) t - in - assert (subst=[]); - assert (metasenv=[]); - t') l - in - (* We can avoid the LetIn. But maybe we need to recompute l' - so that it is localized *) - if localize then - match body with - CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> - (* since we avoid the letin, the context has no - * recfuns in it *) - let l' = List.map (aux ~localize loc context) l in - `AvoidLetIn (n,l') - | _ -> assert false - else - `AvoidLetIn (n,l') - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - if localize then - `AddLetIn (aux ~localize loc context' body) - else - `AddLetIn unlocalized_body) - | _ -> - if localize then - `AddLetIn (aux ~localize loc context' body) - else - `AddLetIn unlocalized_body - in - let inductiveFuns = - List.map - (fun (params, (name, typ), body, decr_idx) -> - let add_binders kind t = - List.fold_right - (fun var t -> CicNotationPt.Binder (kind, var, t)) params t - in - let cic_body = - aux ~localize loc context' (add_binders `Lambda body) in - let cic_type = - aux_option ~localize loc context (Some `Type) - (HExtlib.map_option (add_binders `Pi) typ) in - let name = - match CicNotationUtil.cic_name_of_name name with - | Cic.Anonymous -> - CicNotationPt.fail loc - "Recursive functions cannot be anonymous" - | Cic.Name name -> name - in - (name, decr_idx, cic_type, cic_body)) - defs - in - let fix_or_cofix n = - match kind with - `Inductive -> Cic.Fix (n,inductiveFuns) - | `CoInductive -> - let coinductiveFuns = - List.map - (fun (name, _, typ, body) -> name, typ, body) - inductiveFuns - in - Cic.CoFix (n,coinductiveFuns) - in - let counter = ref ~-1 in - let build_term funs (var,_,ty,_) t = - incr counter; - Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t) - in - (match cic_body with - `AvoidLetInNoAppl n -> - let n' = List.length inductiveFuns - n in - fix_or_cofix n' - | `AvoidLetIn (n,l) -> - let n' = List.length inductiveFuns - n in - Cic.Appl (fix_or_cofix n'::l) - | `AddLetIn cic_body -> - List.fold_right (build_term inductiveFuns) inductiveFuns - cic_body) - | CicNotationPt.Ident _ - | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed - | CicNotationPt.Ident (name, subst) - | CicNotationPt.Uri (name, subst) as ast -> - let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in - (try - if is_uri ast then raise Not_found;(* don't search the env for URIs *) - let index = find_in_context name context in - if subst <> None then - CicNotationPt.fail loc "Explicit substitutions not allowed here"; - Cic.Rel index - with Not_found -> - let cic = - if is_uri ast then (* we have the URI, build the term out of it *) - try - CicUtil.term_of_uri (UriManager.uri_of_string name) - with UriManager.IllFormedUri _ -> - CicNotationPt.fail loc "Ill formed URI" - else - resolve env (Id name) () - in - let mk_subst uris = - let ids_to_uris = - List.map (fun uri -> UriManager.name_of_uri uri, uri) uris - in - (match subst with - | Some subst -> - List.map - (fun (s, term) -> - (try - List.assoc s ids_to_uris, aux ~localize loc context term - with Not_found -> - raise (Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))) - subst - | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) - in - (try - match cic with - | Cic.Const (uri, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.Const (uri, mk_subst uris) - | Cic.Var (uri, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.Var (uri, mk_subst uris) - | Cic.MutInd (uri, i, []) -> - (try - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.MutInd (uri, i, mk_subst uris) - with - CicEnvironment.Object_not_found _ -> - (* if we are here it is probably the case that during the - definition of a mutual inductive type we have met an - occurrence of the type in one of its constructors. - However, the inductive type is not yet in the environment - *) - (*here the explicit_named_substituion is assumed to be of length 0 *) - Cic.MutInd (uri,i,[])) - | Cic.MutConstruct (uri, i, j, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.MutConstruct (uri, i, j, mk_subst uris) - | Cic.Meta _ | Cic.Implicit _ as t -> -(* - debug_print (lazy (sprintf - "Warning: %s must be instantiated with _[%s] but we do not enforce it" - (CicPp.ppterm t) - (String.concat "; " - (List.map - (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term) - subst)))); -*) - t - | _ -> - raise (Invalid_choice (lazy (loc, "??? Can this happen?"))) - with - CicEnvironment.CircularDependency _ -> - raise (Invalid_choice (lazy (loc,"Circular dependency in the environment"))))) - | CicNotationPt.Implicit -> Cic.Implicit None - | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) - | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num () - | CicNotationPt.Meta (index, subst) -> - let cic_subst = - List.map - (function - None -> None - | Some term -> Some (aux ~localize loc context term)) - subst - in - Cic.Meta (index, cic_subst) - | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop - | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set - | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) - | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) - | CicNotationPt.Symbol (symbol, instance) -> - resolve env (Symbol (symbol, instance)) () - | _ -> assert false (* god bless Bologna *) - and aux_option ~localize loc context annotation = function - | None -> Cic.Implicit annotation - | Some term -> aux ~localize loc context term - in - aux ~localize:true HExtlib.dummy_floc context ast - -let interpretate_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 interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast - ~localization_tbl -= - let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in -interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast -~localization_tbl -;; - - let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function | Ast.AttributedTerm (`Loc loc, term) -> domain_of_term ~loc ~context term @@ -903,7 +354,6 @@ let domain_of_term ~context term = 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 *) @@ -935,95 +385,43 @@ sig context:'context -> metasenv:'metasenv -> subst:'subst -> - mk_implicit:([ `Closed ] option -> 'refined_thing) -> + 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_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> - universe:'refined_thing DisambiguateTypes.codomain_item list - DisambiguateTypes.Environment.t option -> - lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> - msg:string -> - id:string -> - UriManager.uri list -> UriManager.uri list) -> - (title:string -> ?id:string -> unit -> UriManager.uri option) -> - DisambiguateTypes.Environment.key -> - 'refined_thing DisambiguateTypes.codomain_item list) -> + 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_thing 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) -> + 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_thing DisambiguateTypes.codomain_item) list * + 'refined_term DisambiguateTypes.codomain_item) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) - list * bool - - val disambiguate_term : - ?fresh_instances:bool -> - context:Cic.context -> - metasenv:Cic.metasenv -> - subst:Cic.substitution -> - ?goal:int -> - ?initial_ugraph:CicUniv.universe_graph -> - aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *) - universe:Cic.term DisambiguateTypes.multiple_environment option -> - lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> - msg:string -> - id:string -> - UriManager.uri list -> UriManager.uri list) -> - (title:string -> ?id:string -> unit -> UriManager.uri option) -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term disambiguator_input -> - ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * (* new metasenv *) - Cic.substitution * - Cic.term* - CicUniv.universe_graph) list * (* disambiguated term *) - bool - - val disambiguate_obj : - ?fresh_instances:bool -> - aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *) - universe:Cic.term DisambiguateTypes.multiple_environment option -> - uri:UriManager.uri option -> (* required only for inductive types *) - lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> - msg:string -> - id:string -> - UriManager.uri list -> UriManager.uri list) -> - (title:string -> ?id:string -> unit -> UriManager.uri option) -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term CicNotationPt.obj disambiguator_input -> - ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * (* new metasenv *) - Cic.substitution * - Cic.obj * - CicUniv.universe_graph) list * (* disambiguated obj *) - bool + list * bool end module Make (C: Callbacks) = @@ -1114,8 +512,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" ("Implicit", (match item with | Id _ | Num _ -> - (fun _ _ _ -> mk_implicit (Some `Closed)) - | Symbol _ -> (fun _ _ _ -> mk_implicit None))) + (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 @@ -1328,65 +726,6 @@ in refine_profiler.HExtlib.profile foo () CicEnvironment.CircularDependency s -> failwith "Disambiguate: circular dependency" - let disambiguate_term ?(fresh_instances=false) ~context ~metasenv - ~subst ?goal - ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe - ~lookup_in_library - (text,prefix_len,term) - = - let term = - if fresh_instances then CicNotationUtil.freshen_term term else term - in - let mk_implicit x = Cic.Implicit x in - let hint = match goal with - | None -> (fun _ x -> x), fun k -> k - | Some i -> - (fun metasenv t -> - let _,c,ty = CicUtil.lookup_meta i metasenv in - assert(c=context); - Cic.Cast(t,ty)), - function - | Ok (t,m,s,ug) -> - (match t with - | Cic.Cast(t,_) -> Ok (t,m,s,ug) - | _ -> assert false) - | k -> k - in - let localization_tbl = Cic.CicHash.create 503 in - disambiguate_thing ~context ~metasenv ~subst - ~initial_ugraph ~aliases ~mk_implicit - ~universe ~lookup_in_library - ~uri:None ~pp_thing:CicNotationPp.pp_term - ~domain_of_thing:domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) - ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl - ~hint - - let disambiguate_obj - ?(fresh_instances=false) ~aliases ~universe ~uri ~lookup_in_library - (text,prefix_len,obj) - = - let mk_implicit x = Cic.Implicit x in - let obj = - if fresh_instances then CicNotationUtil.freshen_obj obj else obj - in - let hint = - (fun _ x -> x), - fun k -> k - in - let localization_tbl = Cic.CicHash.create 503 in - disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] - ~aliases ~universe ~uri ~mk_implicit - ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) - ~domain_of_thing:domain_of_obj - ~lookup_in_library - ~initial_ugraph:CicUniv.empty_ugraph - ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj - ~localization_tbl - ~hint - (text,prefix_len,obj) - end diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index 201bdb3b7..92e11870f 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -41,9 +41,6 @@ exception NoWellTypedInterpretation of bool) list exception PathNotWellFormed -val interpretate_path : - context:Cic.name list -> CicNotationPt.term -> Cic.term - type 'a disambiguator_input = string * int * 'a type domain = domain_tree list @@ -57,7 +54,19 @@ type ('term,'metasenv,'subst,'graph) test_result = 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 @@ -65,95 +74,43 @@ sig context:'context -> metasenv:'metasenv -> subst:'subst -> - mk_implicit:([ `Closed ] option -> 'refined_thing) -> + 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_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> - universe:'refined_thing DisambiguateTypes.codomain_item list - DisambiguateTypes.Environment.t option -> - lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> - msg:string -> - id:string -> - UriManager.uri list -> UriManager.uri list) -> - (title:string -> ?id:string -> unit -> UriManager.uri option) -> - DisambiguateTypes.Environment.key -> - 'refined_thing DisambiguateTypes.codomain_item list) -> + 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_thing 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) -> + 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_thing DisambiguateTypes.codomain_item) list * + 'refined_term DisambiguateTypes.codomain_item) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) - list * bool - - val disambiguate_term : - ?fresh_instances:bool -> - context:Cic.context -> - metasenv:Cic.metasenv -> - subst:Cic.substitution -> - ?goal:int -> - ?initial_ugraph:CicUniv.universe_graph -> - aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *) - universe:Cic.term DisambiguateTypes.multiple_environment option -> - lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> - msg:string -> - id:string -> - UriManager.uri list -> UriManager.uri list) -> - (title:string -> ?id:string -> unit -> UriManager.uri option) -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term disambiguator_input -> - ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * (* new metasenv *) - Cic.substitution * - Cic.term* - CicUniv.universe_graph) list * (* disambiguated term *) - bool - - val disambiguate_obj : - ?fresh_instances:bool -> - aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *) - universe:Cic.term DisambiguateTypes.multiple_environment option -> - uri:UriManager.uri option -> (* required only for inductive types *) - lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> - msg:string -> - id:string -> - UriManager.uri list -> UriManager.uri list) -> - (title:string -> ?id:string -> unit -> UriManager.uri option) -> - DisambiguateTypes.Environment.key -> - Cic.term DisambiguateTypes.codomain_item list) -> - CicNotationPt.term CicNotationPt.obj disambiguator_input -> - ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list * - Cic.metasenv * (* new metasenv *) - Cic.substitution * - Cic.obj * - CicUniv.universe_graph) list * (* disambiguated obj *) - bool + 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 index dae0542b9..0ed285af0 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.ml @@ -106,19 +106,27 @@ let env_of_list l e = (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: - selection_mode:[`SINGLE | `MULTIPLE] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> id:string -> UriManager.uri list -> - UriManager.uri list - val interactive_interpretation_choice: - string -> int -> - (Stdpp.location list * string * string) list list -> int list - val input_or_locate_uri: - title:string -> ?id:string -> unit -> UriManager.uri option + 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 diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/cic_disambiguation/disambiguateTypes.mli index c33013ee6..ae157e268 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.mli +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.mli @@ -60,24 +60,28 @@ 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 : - selection_mode:[`SINGLE | `MULTIPLE] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> id:string -> UriManager.uri list -> - UriManager.uri list - - val interactive_interpretation_choice : - string -> int -> - (Stdpp.location list * string * string) list list -> int list - - (** @param title gtk window title for user prompting - * @param id unbound identifier which originated this callback invocation *) - val input_or_locate_uri: - title:string -> ?id:string -> unit -> UriManager.uri option + 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 diff --git a/helm/software/components/cic_proof_checking/.depend b/helm/software/components/cic_proof_checking/.depend index 84367a6e9..5669c0845 100644 --- a/helm/software/components/cic_proof_checking/.depend +++ b/helm/software/components/cic_proof_checking/.depend @@ -22,5 +22,5 @@ freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \ freshNamesGenerator.cmi freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \ freshNamesGenerator.cmi -cicDischarge.cmo: cicEnvironment.cmi cicDischarge.cmi -cicDischarge.cmx: cicEnvironment.cmx cicDischarge.cmi +cicDischarge.cmo: cicTypeChecker.cmi cicEnvironment.cmi cicDischarge.cmi +cicDischarge.cmx: cicTypeChecker.cmx cicEnvironment.cmx cicDischarge.cmi diff --git a/helm/software/components/cic_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt index 84367a6e9..5669c0845 100644 --- a/helm/software/components/cic_proof_checking/.depend.opt +++ b/helm/software/components/cic_proof_checking/.depend.opt @@ -22,5 +22,5 @@ freshNamesGenerator.cmo: cicTypeChecker.cmi cicSubstitution.cmi \ freshNamesGenerator.cmi freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \ freshNamesGenerator.cmi -cicDischarge.cmo: cicEnvironment.cmi cicDischarge.cmi -cicDischarge.cmx: cicEnvironment.cmx cicDischarge.cmi +cicDischarge.cmo: cicTypeChecker.cmi cicEnvironment.cmi cicDischarge.cmi +cicDischarge.cmx: cicTypeChecker.cmx cicEnvironment.cmx cicDischarge.cmi diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index bc5bede45..168732022 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -5,10 +5,10 @@ grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi -grafiteDisambiguator.cmo: grafiteDisambiguator.cmi -grafiteDisambiguator.cmx: grafiteDisambiguator.cmi -grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi +multiPassDisambiguator.cmo: multiPassDisambiguator.cmi +multiPassDisambiguator.cmx: multiPassDisambiguator.cmi +grafiteDisambiguate.cmo: multiPassDisambiguator.cmi grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: multiPassDisambiguator.cmx grafiteDisambiguate.cmi grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi print_grammar.cmo: print_grammar.cmi diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt index bc5bede45..168732022 100644 --- a/helm/software/components/grafite_parser/.depend.opt +++ b/helm/software/components/grafite_parser/.depend.opt @@ -5,10 +5,10 @@ grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi -grafiteDisambiguator.cmo: grafiteDisambiguator.cmi -grafiteDisambiguator.cmx: grafiteDisambiguator.cmi -grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi +multiPassDisambiguator.cmo: multiPassDisambiguator.cmi +multiPassDisambiguator.cmx: multiPassDisambiguator.cmi +grafiteDisambiguate.cmo: multiPassDisambiguator.cmi grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: multiPassDisambiguator.cmx grafiteDisambiguate.cmi grafiteWalker.cmo: grafiteParser.cmi grafiteWalker.cmi grafiteWalker.cmx: grafiteParser.cmx grafiteWalker.cmi print_grammar.cmo: print_grammar.cmi diff --git a/helm/software/components/grafite_parser/Makefile b/helm/software/components/grafite_parser/Makefile index 3df8517a9..ace33c397 100644 --- a/helm/software/components/grafite_parser/Makefile +++ b/helm/software/components/grafite_parser/Makefile @@ -5,7 +5,7 @@ INTERFACE_FILES = \ dependenciesParser.mli \ grafiteParser.mli \ cicNotation2.mli \ - grafiteDisambiguator.mli \ + multiPassDisambiguator.mli \ grafiteDisambiguate.mli \ grafiteWalker.mli \ print_grammar.mli \ diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 24fdadd5e..ef9da1f20 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -101,7 +101,7 @@ term = let lexicon_status = !lexicon_status_ref in let (diff, metasenv, subst, cic, _) = singleton "first" - (GrafiteDisambiguator.disambiguate_term + (MultiPassDisambiguator.disambiguate_term ~aliases:lexicon_status.LexiconEngine.aliases ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~lookup_in_library @@ -122,7 +122,7 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = let lexicon_status = !lexicon_status_ref in let (diff, metasenv, _, cic, ugraph) = singleton "second" - (GrafiteDisambiguator.disambiguate_term ~lookup_in_library + (MultiPassDisambiguator.disambiguate_term ~lookup_in_library ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~context ~metasenv ~subst:[] ?goal @@ -135,7 +135,7 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = let disambiguate_pattern text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path) = - let interp path = Disambiguate.interpretate_path [] path in + let interp path =CicDisambiguate.interpretate_path [] path in let goal_path = HExtlib.map_option interp goal_path in let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in let wanted = @@ -507,12 +507,12 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = | None -> raise BaseUriNotSetYet) | CicNotationPt.Inductive _ -> assert false | CicNotationPt.Theorem _ -> None in -(* + (* (match obj with CicNotationPt.Theorem (_,_,ty,_) -> (try let [_,_,_,ty],_ = - NGrafiteDisambiguator.disambiguate_term + NMultiPassDisambiguator.disambiguate_term ~context:[] ~metasenv:[] ~subst:[] ~aliases:DisambiguateTypes.Environment.empty ~universe:(Some DisambiguateTypes.Environment.empty) @@ -520,16 +520,15 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = in prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!! " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty) - with NGrafiteDisambiguator.DisambiguationError _ -> + with NMultiPassDisambiguator.DisambiguationError _ -> prerr_endline "ERRORE NUOVA DISAMBIGUAZIONE"; assert false | exn -> ()) | _ -> () - ); -*) + ); *) let (diff, metasenv, _, cic, _) = singleton "third" - (GrafiteDisambiguator.disambiguate_obj ~lookup_in_library + (MultiPassDisambiguator.disambiguate_obj ~lookup_in_library ~aliases:lexicon_status.LexiconEngine.aliases ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri (text,prefix_len,obj)) in diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/multiPassDisambiguator.ml similarity index 93% rename from helm/software/components/grafite_parser/grafiteDisambiguator.ml rename to helm/software/components/grafite_parser/multiPassDisambiguator.ml index 4b647c780..a81709f23 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ b/helm/software/components/grafite_parser/multiPassDisambiguator.ml @@ -41,14 +41,8 @@ exception DisambiguationError of (** parameters are: option name, error message *) exception Unbound_identifier of string -type choose_uris_callback = - id:string -> UriManager.uri list -> UriManager.uri list - -type choose_interp_callback = - string -> int -> - (Stdpp.location list * string * string) list list -> int list - -let mono_uris_callback ~id = +let mono_uris_callback ~selection_mode ?ok + ?(enable_button_for_non_vars = true) ~title ~msg ~id = if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation" then @@ -65,9 +59,7 @@ let set_choose_interp_callback f = _choose_interp_callback := f module Callbacks = struct - let interactive_user_uri_choice ~selection_mode ?ok - ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = - !_choose_uris_callback ~id uris + let interactive_user_uri_choice = !_choose_uris_callback let interactive_interpretation_choice interp = !_choose_interp_callback interp @@ -78,7 +70,7 @@ module Callbacks = * query is a syntax error *) end -module Disambiguator = Disambiguate.Make (Callbacks) +module Disambiguator = CicDisambiguate.Make (Callbacks) (* implement module's API *) @@ -221,5 +213,3 @@ let disambiguate_obj ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff obj - -let disambiguate_thing ~context = assert false diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.mli b/helm/software/components/grafite_parser/multiPassDisambiguator.mli similarity index 80% rename from helm/software/components/grafite_parser/grafiteDisambiguator.mli rename to helm/software/components/grafite_parser/multiPassDisambiguator.mli index 1d97b1b6b..337c92e2f 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.mli +++ b/helm/software/components/grafite_parser/multiPassDisambiguator.mli @@ -37,24 +37,22 @@ exception DisambiguationError of (** initially false; for debugging only (???) *) val only_one_pass: bool ref -type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list -type choose_interp_callback = - string -> int -> (Stdpp.location list * string * string) list list -> - int list +val set_choose_uris_callback: + DisambiguateTypes.interactive_user_uri_choice_type -> unit -val set_choose_uris_callback: choose_uris_callback -> unit -val set_choose_interp_callback: choose_interp_callback -> unit +val set_choose_interp_callback: + DisambiguateTypes.interactive_interpretation_choice_type -> unit (** @raise Ambiguous_input if called, default value for internal * choose_uris_callback if not set otherwise with set_choose_uris_callback * above *) -val mono_uris_callback: choose_uris_callback +val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type (** @raise Ambiguous_input if called, default value for internal * choose_interp_callback if not set otherwise with set_choose_interp_callback * above *) -val mono_interp_callback: choose_interp_callback +val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type (** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) -include Disambiguate.Disambiguator +include CicDisambiguate.CicDisambiguator diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml index f4213bc30..0429cc988 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml @@ -50,14 +50,6 @@ let refine_term metasenv subst context uri term _ ~localization_tbl = Disambiguate.Ko loc_msg ;; -let resolve (env: NCic.term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = - ignore (env,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 @@ -81,7 +73,7 @@ let interpretate_term | 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 () + Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args () | CicNotationPt.Appl terms -> NCic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> @@ -93,7 +85,7 @@ let interpretate_term | `Pi | `Forall -> NCic.Prod (cic_name, cic_type, cic_body) | `Exists -> - resolve env (Symbol ("exists", 0)) + Disambiguate.resolve env (Symbol ("exists", 0)) ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ()) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in @@ -132,7 +124,7 @@ let interpretate_term let indtype_ref = match indty_ident with | Some (indty_ident, _) -> - (match resolve env (Id indty_ident) () with + (match Disambiguate.resolve env (Id indty_ident) () with | NCic.Const r -> r | NCic.Implicit _ -> raise (Disambiguate.Try_again @@ -151,7 +143,7 @@ let interpretate_term "because it is an inductive type without constructors "^ "or because all patterns use wildcards"))) in - (match resolve env (Id (fst_constructor branches)) () with + (match Disambiguate.resolve env (Id (fst_constructor branches)) () with | NCic.Const r -> r | NCic.Implicit _ -> raise (Disambiguate.Try_again @@ -355,7 +347,7 @@ let interpretate_term assert (subst = None); (try NCic.Rel (find_in_context name context) - with Not_found -> resolve env (Id name) ()) + with Not_found -> Disambiguate.resolve env (Id name) ()) | CicNotationPt.Uri (name, subst) -> assert (subst = None); (try @@ -365,7 +357,7 @@ let interpretate_term | CicNotationPt.Implicit -> NCic.Implicit `Term | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole) patterns not implemented *) - | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num () + | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (Num i) ~num () | CicNotationPt.Meta (index, subst) -> let cic_subst = List.map @@ -380,7 +372,7 @@ patterns not implemented *) | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"]) | CicNotationPt.Symbol (symbol, instance) -> - resolve env (Symbol (symbol, instance)) () + Disambiguate.resolve env (Symbol (symbol, instance)) () | _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> NCic.Implicit annotation @@ -430,8 +422,8 @@ module Make (C : DisambiguateTypes.Callbacks) = struct Disambiguator.disambiguate_thing ~context ~metasenv ~initial_ugraph:() ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term - ~mk_implicit:(function None -> NCic.Implicit `Term - | Some `Closed -> NCic.Implicit `Closed) + ~mk_implicit:(function false -> NCic.Implicit `Term + | true -> NCic.Implicit `Closed) ~lookup_in_library ~domain_of_thing:domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index aafbcd14e..6cf3cb970 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -7,7 +7,7 @@ nCicLibrary.cmi: nUri.cmi nCic.cmo nCicPp.cmi: nCic.cmo nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo nCicReduction.cmi: nCic.cmo -nCicTypeChecker.cmi: nUri.cmi nCic.cmo +nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo nCicUntrusted.cmi: nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx @@ -29,16 +29,18 @@ nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi -nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo nCicPp.cmi -nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi +nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicLibrary.cmi \ + nCic.cmo nCicPp.cmi +nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicLibrary.cmx \ + nCic.cmx nCicPp.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo \ nCicEnvironment.cmi nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \ nCicEnvironment.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicEnvironment.cmi nCic.cmo nCicReduction.cmi + nCicPp.cmi nCicEnvironment.cmi nCic.cmo nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi + nCicPp.cmx nCicEnvironment.cmx nCic.cmx nCicReduction.cmi nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicSubstitution.cmi nCicReduction.cmi nCicPp.cmi nCicEnvironment.cmi \ nCic.cmo nCicTypeChecker.cmi diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index 985fec0df..f5b6e9fe6 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -1,13 +1,13 @@ nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmx -nCicPp.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmx nCicLibrary.cmi: nUri.cmi nCic.cmx +nCicPp.cmi: nCic.cmx nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx nCicReduction.cmi: nCic.cmx -nCicTypeChecker.cmi: nUri.cmi nCic.cmx +nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx nCicUntrusted.cmi: nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx @@ -17,8 +17,6 @@ nReference.cmo: nUri.cmi nReference.cmi nReference.cmx: nUri.cmx nReference.cmi nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi -nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx nCicPp.cmi -nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmx \ nCicSubstitution.cmi nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \ @@ -31,14 +29,18 @@ nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi +nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicLibrary.cmi \ + nCic.cmx nCicPp.cmi +nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicLibrary.cmx \ + nCic.cmx nCicPp.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx \ nCicEnvironment.cmi nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \ nCicEnvironment.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ - nCicEnvironment.cmi nCic.cmx nCicReduction.cmi + nCicPp.cmi nCicEnvironment.cmi nCic.cmx nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi + nCicPp.cmx nCicEnvironment.cmx nCic.cmx nCicReduction.cmi nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicSubstitution.cmi nCicReduction.cmi nCicPp.cmi nCicEnvironment.cmi \ nCic.cmx nCicTypeChecker.cmi diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 42a02ebf1..863921720 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -4,5 +4,5 @@ nCicMetaSubst.cmo: nCicMetaSubst.cmi nCicMetaSubst.cmx: nCicMetaSubst.cmi nCicUnification.cmo: nCicMetaSubst.cmi nCicUnification.cmi nCicUnification.cmx: nCicMetaSubst.cmx nCicUnification.cmi -nCicRefiner.cmo: nCicRefiner.cmi -nCicRefiner.cmx: nCicRefiner.cmi +nCicRefiner.cmo: nCicUnification.cmi nCicMetaSubst.cmi nCicRefiner.cmi +nCicRefiner.cmx: nCicUnification.cmx nCicMetaSubst.cmx nCicRefiner.cmi diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 94235e520..a278f6f08 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -91,11 +91,11 @@ paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \ paramodulation/equality.cmx paramodulation/equality_indexing.cmi paramodulation/indexing.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi paramodulation/founif.cmi \ + paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/founif.cmi \ paramodulation/equality_indexing.cmi paramodulation/equality.cmi \ paramodulation/indexing.cmi paramodulation/indexing.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx paramodulation/founif.cmx \ + paramodulation/subst.cmx proofEngineTypes.cmx paramodulation/founif.cmx \ paramodulation/equality_indexing.cmx paramodulation/equality.cmx \ paramodulation/indexing.cmi paramodulation/saturation.cmo: paramodulation/utils.cmi \ diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt index 94235e520..a278f6f08 100644 --- a/helm/software/components/tactics/.depend.opt +++ b/helm/software/components/tactics/.depend.opt @@ -91,11 +91,11 @@ paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \ paramodulation/equality.cmx paramodulation/equality_indexing.cmi paramodulation/indexing.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi paramodulation/founif.cmi \ + paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/founif.cmi \ paramodulation/equality_indexing.cmi paramodulation/equality.cmi \ paramodulation/indexing.cmi paramodulation/indexing.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx paramodulation/founif.cmx \ + paramodulation/subst.cmx proofEngineTypes.cmx paramodulation/founif.cmx \ paramodulation/equality_indexing.cmx paramodulation/equality.cmx \ paramodulation/indexing.cmi paramodulation/saturation.cmo: paramodulation/utils.cmi \ diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index d63e327f0..247e07d7a 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -236,9 +236,9 @@ let _ = *) addDebugSeparator (); addDebugItem "enable multiple disambiguation passes (default)" - (fun _ -> GrafiteDisambiguator.only_one_pass := false); + (fun _ -> MultiPassDisambiguator.only_one_pass := false); addDebugItem "enable only one disambiguation pass" - (fun _ -> GrafiteDisambiguator.only_one_pass := true); + (fun _ -> MultiPassDisambiguator.only_one_pass := true); addDebugItem "always show all disambiguation errors" (fun _ -> MatitaGui.all_disambiguation_passes := true); addDebugItem "prune disambiguation errors" diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml index 17cc7c942..0671037a3 100644 --- a/helm/software/matita/matitaExcPp.ml +++ b/helm/software/matita/matitaExcPp.ml @@ -150,7 +150,7 @@ let rec to_string = None, ("Disambiguation choice not found: " ^ Lazy.force msg) | MatitaEngine.EnrichedWithLexiconStatus (exn,_) -> None, "EnrichedWithLexiconStatus "^snd(to_string exn) - | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> + | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> let loc = match errorll with | ((_,_,loc_msg,_)::_)::_ -> diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 234d44be9..429bb6b2c 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -263,7 +263,7 @@ let rec interactive_error_interp ~all_passes | [loffset,[_,envs_and_diffs,msg,significant]] -> let _,env,diff = List.hd envs_and_diffs in notify_exn - (GrafiteDisambiguator.DisambiguationError + (MultiPassDisambiguator.DisambiguationError (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]])); | _::_ -> let dialog = new disambiguationErrors () in @@ -298,7 +298,7 @@ let rec interactive_error_interp ~all_passes ~start:source_buffer#start_iter ~stop:source_buffer#end_iter; notify_exn - (GrafiteDisambiguator.DisambiguationError + (MultiPassDisambiguator.DisambiguationError (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]])) )); let return _ = @@ -689,7 +689,7 @@ class gui () = f (); unlock_world () with - | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> + | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> (try interactive_error_interp ~all_passes:!all_disambiguation_passes source_buffer @@ -1570,8 +1570,10 @@ let interactive_interp_choice () text prefix_len choices = let _ = (* disambiguator callbacks *) - GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); - GrafiteDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); + MultiPassDisambiguator.set_choose_uris_callback + (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg -> + interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ()); + MultiPassDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); (* gtk initialization *) GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf; diff --git a/helm/software/matita/matitaGui.mli b/helm/software/matita/matitaGui.mli index 388c79e1a..796c33fef 100644 --- a/helm/software/matita/matitaGui.mli +++ b/helm/software/matita/matitaGui.mli @@ -43,10 +43,10 @@ val interactive_uri_choice: ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string -> ?ok_action:[`AUTO|`SELECT] -> ?copy_cb:(string -> unit) -> unit -> - GrafiteDisambiguator.choose_uris_callback + id:'a -> UriManager.uri list -> UriManager.uri list (** @raise MatitaTypes.Cancel *) val interactive_interp_choice: unit -> - GrafiteDisambiguator.choose_interp_callback + DisambiguateTypes.interactive_interpretation_choice_type diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index 5ca8ffc82..2655798a9 100644 --- a/helm/software/matita/matitaInit.ml +++ b/helm/software/matita/matitaInit.ml @@ -229,7 +229,7 @@ let parse_cmdline init_status = ("Do not catch top-level exception " ^ "(useful for backtrace inspection)"); "-onepass", - Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true), + Arg.Unit (fun () -> MultiPassDisambiguator.only_one_pass := true), "Enable only one disambiguation pass"; ] else [] diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 65d7be828..d8e66dbf2 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -582,7 +582,7 @@ lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt script ex loc = let module TAPp = GrafiteAstPp in - let module MD = GrafiteDisambiguator in + let module MD = MultiPassDisambiguator in let module ML = MatitaMisc in try ignore (buffer#move_mark (`NAME "beginning_of_statement") @@ -642,9 +642,9 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn - | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> + | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> raise - (GrafiteDisambiguator.DisambiguationError + (MultiPassDisambiguator.DisambiguationError (offset+parsed_text_length, errorll)) in assert (text=""); (* no macros inside comments, please! *) -- 2.39.2