From 573d8c989cca4fc19e3879cc2c0e51c5c3be6878 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 21 Nov 2008 16:25:55 +0000 Subject: [PATCH] one more lazy/loc --- .../cic_disambiguation/disambiguate.ml | 33 +++++++------- .../cic_disambiguation/disambiguateChoices.ml | 3 +- .../cic_disambiguation/disambiguateTypes.ml | 2 +- .../cic_disambiguation/disambiguateTypes.mli | 2 +- .../cic_disambiguation/number_notation.ml | 2 +- .../ng_disambiguation/nDisambiguate.ml | 44 ++++++++++++------- 6 files changed, 47 insertions(+), 39 deletions(-) diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 9d42899c6..47e9c1821 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -232,13 +232,13 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast 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!"))) + 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 (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")) + | [] -> 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, _, _) -> @@ -247,7 +247,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast 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!"))) + 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 @@ -255,7 +255,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast (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 \"_\"")) + 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 @@ -278,17 +278,15 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast [] -> if unrecognized != [] then raise (Invalid_choice - (Some loc, - lazy + (lazy (loc, ("Unrecognized constructors: " ^ - String.concat " " unrecognized))) + String.concat " " unrecognized)))) else if useless > 0 then raise (Invalid_choice - (Some loc, - lazy + (lazy (loc, ("The last " ^ string_of_int useless ^ "case" ^ if useless > 1 then "s are" else " is" ^ - " unused"))) + " unused")))) else [] | (Ast.Wildcard,_)::tl when not unused -> @@ -304,7 +302,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast [] -> raise (Invalid_choice - (Some loc, lazy ("Missing case: " ^ name))) + (lazy (loc, ("Missing case: " ^ name)))) | ((Ast.Wildcard, _) as branch :: _) as branches -> branch, branches | (Ast.Pattern (name',_,_),_) as branch :: tl @@ -322,8 +320,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast else raise (Invalid_choice - (Some loc, - lazy ("Wrong number of arguments for " ^ name))) + (lazy (loc,"Wrong number of arguments for " ^ + name))) | Ast.Wildcard,term -> let rec mk_lambdas = function @@ -482,7 +480,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast (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")))) + 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 @@ -526,10 +524,10 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast *) t | _ -> - raise (Invalid_choice (Some loc, lazy "??? Can this happen?")) + raise (Invalid_choice (lazy (loc, "??? Can this happen?"))) with CicEnvironment.CircularDependency _ -> - raise (Invalid_choice (None, lazy "Circular dependency in the environment")))) + 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 () @@ -1147,8 +1145,7 @@ let foo () = in refine_profiler.HExtlib.profile foo () with | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) - | Invalid_choice (None,msg) -> Ko(lazy (Stdpp.dummy_loc,Lazy.force msg)) - | Invalid_choice (Some loc,msg) -> Ko (lazy (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 diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml index c3fa7efb2..bf14623d7 100644 --- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml +++ b/helm/software/components/cic_disambiguation/disambiguateChoices.ml @@ -62,7 +62,8 @@ let mk_choice (dsc, args, appl_pattern) = try combine_with_rest names cic_args with Invalid_argument _ -> - raise (Invalid_choice (None, lazy ("The notation " ^ dsc ^ " expects more arguments"))) + raise (Invalid_choice (lazy (Stdpp.dummy_loc, + "The notation " ^ dsc ^ " expects more arguments"))) in let combined = TermAcicContent.instantiate_appl_pattern env' appl_pattern diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/cic_disambiguation/disambiguateTypes.ml index 1eade4ca0..e9927c7b6 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.ml @@ -40,7 +40,7 @@ type domain_item = | Symbol of string * int (* literal, instance num *) | Num of int (* instance num *) -exception Invalid_choice of Stdpp.location option * string Lazy.t +exception Invalid_choice of (Stdpp.location * string) Lazy.t module OrderedDomain = struct diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/cic_disambiguation/disambiguateTypes.mli index 00fe4114c..d9cedf5f0 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.mli +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.mli @@ -41,7 +41,7 @@ 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 option * string Lazy.t +exception Invalid_choice of (Stdpp.location * string) Lazy.t type codomain_item = string * (* description *) diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml index 9dece04ec..37547bf58 100644 --- a/helm/software/components/cic_disambiguation/number_notation.ml +++ b/helm/software/components/cic_disambiguation/number_notation.ml @@ -40,7 +40,7 @@ let _ = (fun _ num _ -> let num = int_of_string num in if num = 0 then - raise (DisambiguateTypes.Invalid_choice (None, lazy "0 is not a valid positive number")) + raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, "0 is not a valid positive number"))) else HelmLibraryObjects.build_bin_pos num)); DisambiguateChoices.add_num_choice diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml index 2aa873724..d350a7f23 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml @@ -34,6 +34,11 @@ module Ast = CicNotationPt let debug_print _ = ();; +let cic_name_of_name = function + | Ast.Ident (n, None) -> n + | _ -> assert false +;; + let refine_term metasenv subst context uri term _ ~localization_tbl = assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" @@ -48,22 +53,25 @@ let refine_term metasenv subst context uri term _ ~localization_tbl = in Disambiguate.Ok (term, metasenv, subst, ()) with - | NCicRefiner.Uncertain (msg) -> - debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force msg) ^ "] " ^ + | NCicRefiner.Uncertain loc_msg -> + debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^ NCicPp.ppterm ~metasenv ~subst ~context term)) ; - Disambiguate.Uncertain (loc,msg) - | NCicRefiner.RefineFailure (msg) -> + Disambiguate.Uncertain loc_msg + | NCicRefiner.RefineFailure loc_msg -> debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s" - (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force msg)))); - Disambiguate.Ko (loc,msg,()) + (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg)))); + Disambiguate.Ko loc_msg ;; let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = + assert false;; +(* 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 = @@ -83,7 +91,7 @@ let interpretate_term let rec aux ~localize loc context = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> let res = aux ~localize loc context term in - if localize then NCic.NCicHash.add localization_tbl res loc; + if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; res | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> @@ -93,7 +101,7 @@ let interpretate_term NCic.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_name = cic_name_of_name var in let cic_body = aux ~localize loc (cic_name :: context) body in (match binder_kind with | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body) @@ -109,11 +117,11 @@ let interpretate_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_name = cic_name_of_name name in let cic_body = do_branch' (cic_name :: context) tl in let typ = match typ with - | None -> NCic.Implicit (Some `Type) + | None -> NCic.Implicit `Type | Some typ -> aux ~localize loc context typ in NCic.Lambda (cic_name, typ, cic_body) @@ -127,12 +135,14 @@ let interpretate_term match indty_ident with | Some (indty_ident, _) -> (match resolve env (Id indty_ident) () with - | NCic.MutInd (uri, tyno, _) -> (uri, tyno) + | NCic.Const (NRef.Ref (uri, NRef.Ind (_, tyno))) -> (uri, tyno) | NCic.Implicit _ -> - raise (Disambiguate.Try_again (lazy "The type of the term to be matched - is still unknown")) + raise (Disambiguate.Try_again + (lazy "The type of the term to be matched is still unknown")) | _ -> - raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!"))) + raise (DisambiguateTypes.Invalid_choice + (Some loc, + lazy "The type of the term to be matched is not (co)inductive!"))) | None -> let rec fst_constructor = function @@ -247,7 +257,7 @@ let interpretate_term NCic.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_name = cic_name_of_name name in let cic_typ = match typ with | None -> NCic.Implicit (Some `Type) @@ -259,7 +269,7 @@ let interpretate_term let context' = List.fold_left (fun acc (_, (name, _), _, _) -> - CicNotationUtil.cic_name_of_name name :: acc) + cic_name_of_name name :: acc) context defs in let cic_body = @@ -315,7 +325,7 @@ let interpretate_term 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 + match cic_name_of_name name with | NCic.Anonymous -> CicNotationPt.fail loc "Recursive functions cannot be anonymous" -- 2.39.2