X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=6dd82cc288c42731702bd8b94220d31b5502e8a9;hb=87cebf96248da4c901973d563c05b76c0010943a;hp=1d4a6a61ef9ecd8a1cbf8613035014c768fc568c;hpb=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 1d4a6a61e..6dd82cc28 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -35,9 +35,9 @@ module Ast = CicNotationPt (* the integer is an offset to be added to each location *) exception NoWellTypedInterpretation of int * - ((Token.flocation list * string * string) list * + ((Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - Token.flocation option * string Lazy.t * bool) list + Stdpp.location option * string Lazy.t * bool) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) @@ -47,7 +47,7 @@ type aliases = bool * DisambiguateTypes.environment type 'a disambiguator_input = string * int * 'a type domain = domain_tree list -and domain_tree = Node of Token.flocation list * domain_item * domain +and domain_tree = Node of Stdpp.location list * domain_item * domain let rec string_of_domain = function @@ -105,8 +105,8 @@ let descr_of_domain_item = function type 'a test_result = | Ok of 'a * Cic.metasenv - | Ko of Token.flocation option * string Lazy.t - | Uncertain of Token.flocation option * string Lazy.t + | 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; *) @@ -172,9 +172,10 @@ let find_in_context name context = in aux 1 context -let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast +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) -> @@ -216,7 +217,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast in do_branch' context args in - let (indtype_uri, indtype_no) = + 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 @@ -225,12 +229,12 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast raise (Try_again (lazy "The type of the term to be matched is still unknown")) | _ -> - raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!"))) + raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!"))) | None -> let fst_constructor = match branches with | ((head, _, _), _) :: _ -> head - | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined")) + | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined")) in (match resolve env (Id fst_constructor) () with | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> @@ -239,7 +243,57 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast raise (Try_again (lazy "The type of the term to be matched is still unknown")) | _ -> - raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!"))) + raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!"))) + in + let branches = + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with + Cic.InductiveDefinition (il,_,_,_) -> + 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 + [] -> + if branches = [] then [] + else + raise (Invalid_choice + (Some loc, + lazy + ("Unrecognized constructors: " ^ + String.concat " " + (List.map (fun ((head,_,_),_) -> head) branches)))) + | (name,ty)::cltl -> + let rec find_and_remove = + function + [] -> + raise + (Invalid_choice + (Some loc, lazy ("Missing case: " ^ name))) + | ((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 + let (_,_,args),_ = branch in + if List.length args = count_prod ty then + branch::sort tl cltl + else + raise + (Invalid_choice + (Some loc, + lazy ("Wrong number of arguments for " ^ name))) + in + sort branches cl + | _ -> assert false in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -267,14 +321,14 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast let cic_body = let unlocalized_body = aux ~localize:false loc context' body in match unlocalized_body with - Cic.Rel 1 -> `AvoidLetInNoAppl - | Cic.Appl (Cic.Rel 1::l) -> + 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 [] [] 1 t + CicMetaSubst.delift_rels [] [] (List.length defs) t in assert (subst=[]); assert (metasenv=[]); @@ -286,10 +340,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast match body with CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> let l' = List.map (aux ~localize loc context) l in - `AvoidLetIn l' + `AvoidLetIn (n,l') | _ -> assert false else - `AvoidLetIn l' + `AvoidLetIn (n,l') with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> if localize then @@ -324,42 +378,32 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast (name, decr_idx, cic_type, cic_body)) defs in - let counter = ref ~-1 in - let build_term funs = - (* this is the body of the fold_right function below. Rationale: Fix - * and CoFix cases differs only in an additional index in the - * inductiveFun list, see Cic.term *) - match kind with - | `Inductive -> - (fun (var, _, _, _) cic -> - incr counter; - let fix = Cic.Fix (!counter,funs) in - match cic with - `Recipe (`AddLetIn cic) -> - `Term (Cic.LetIn (Cic.Name var, fix, cic)) - | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l)) - | `Recipe `AvoidLetInNoAppl -> `Term fix - | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t))) + let fix_or_cofix n = + match kind with + `Inductive -> Cic.Fix (n,inductiveFuns) | `CoInductive -> - let funs = - List.map (fun (name, _, typ, body) -> (name, typ, body)) funs + let coinductiveFuns = + List.map + (fun (name, _, typ, body) -> name, typ, body) + inductiveFuns in - (fun (var, _, _, _) cic -> - incr counter; - let cofix = Cic.CoFix (!counter,funs) in - match cic with - `Recipe (`AddLetIn cic) -> - `Term (Cic.LetIn (Cic.Name var, cofix, cic)) - | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l)) - | `Recipe `AvoidLetInNoAppl -> `Term cofix - | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t))) + Cic.CoFix (n,coinductiveFuns) in - (match - List.fold_right (build_term inductiveFuns) inductiveFuns - (`Recipe cic_body) - with - `Recipe _ -> assert false - | `Term t -> t) + 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) @@ -392,7 +436,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast (try List.assoc s ids_to_uris, aux ~localize loc context term with Not_found -> - raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) + 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 @@ -436,10 +480,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast *) t | _ -> - raise (Invalid_choice (lazy "??? Can this happen?")) + raise (Invalid_choice (Some loc, lazy "??? Can this happen?")) with CicEnvironment.CircularDependency _ -> - raise (Invalid_choice (lazy "Circular dependency in the environment")))) + 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 () @@ -469,7 +513,8 @@ let interpretate_path ~context path = let localization_tbl = Cic.CicHash.create 23 in (* here we are throwing away useful localization informations!!! *) fst ( - interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true + 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 = @@ -694,7 +739,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function 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 typ + @ domain_of_term_option ~loc ~context:context' typ @ domain_of_term ~loc ~context:context' body ) [] defs in @@ -819,7 +864,7 @@ module type Disambiguator = sig val disambiguate_term : ?fresh_instances:bool -> - dbd:HMysql.dbd -> + dbd:HSql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> @@ -834,7 +879,7 @@ sig val disambiguate_obj : ?fresh_instances:bool -> - dbd:HMysql.dbd -> + dbd:HSql.dbd -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) @@ -995,7 +1040,7 @@ let foo () = in refine_profiler.HExtlib.profile foo () with | Try_again msg -> Uncertain (None,msg), ugraph - | Invalid_choice msg -> Ko (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 @@ -1194,7 +1239,7 @@ in refine_profiler.HExtlib.profile foo () 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 + ~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