X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=11d1952050205ba29987690e29c0762be40a933f;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=919c33eb76526e31035e13721ae25e6caffb7845;hpb=35c68efd0a44da26d4aa6ae760ee03712b33dfed;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 919c33eb7..11d195205 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -37,7 +37,7 @@ exception Try_again type aliases = bool * DisambiguateTypes.environment -let debug = true +let debug = false let debug_print = if debug then prerr_endline else ignore (* @@ -49,16 +49,6 @@ let domain_size = ref 0 let choices_avg = ref 0. *) -let floc_of_loc (loc_begin, loc_end) = - let floc_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = loc_begin } - in - let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in - (floc_begin, floc_end) - -let dummy_floc = floc_of_loc (-1, -1) - let descr_of_domain_item = function | Id s -> s | Symbol (s, _) -> s @@ -85,7 +75,7 @@ let refine_term metasenv context uri term ugraph = Uncertain,ugraph | CicRefine.RefineFailure msg -> debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) msg); + (CicPp.ppterm term) (CicRefine.explain_error msg)); Ko,ugraph let refine_obj metasenv context uri obj ugraph = @@ -101,7 +91,7 @@ let refine_obj metasenv context uri obj ugraph = Uncertain,ugraph | CicRefine.RefineFailure msg -> debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) msg); + (CicPp.ppobj obj) (CicRefine.explain_error msg)); Ko,ugraph let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = @@ -144,7 +134,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux loc context term in let cic_outtype = aux_option loc context None outtype in - let do_branch ((head, args), term) = + let do_branch ((head, _, args), term) = let rec do_branch' context = function | [] -> aux loc context term | (name, typ) :: tl -> @@ -161,7 +151,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = in let (indtype_uri, indtype_no) = match indty_ident with - | Some indty_ident -> + | Some (indty_ident, _) -> (match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) | Cic.Implicit _ -> raise Try_again @@ -169,7 +159,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | None -> let fst_constructor = match branches with - | ((head, _), _) :: _ -> head + | ((head, _, _), _) :: _ -> head | [] -> raise Invalid_choice in (match resolve env (Id fst_constructor) () with @@ -369,7 +359,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = (fun (i,res) (name,_,_,_) -> i + 1,(name,name,Cic.MutInd (uri,i,[]))::res ) (0,[]) tyl) in - let con_env = DisambiguateTypes.singleton_env_of_list name_to_uris env in + let con_env = DisambiguateTypes.env_of_list name_to_uris env in let undebrujin t = snd (List.fold_right @@ -495,9 +485,9 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function let outtype_dom = domain_rev_of_term_option loc context outtype in let get_first_constructor = function | [] -> [] - | ((head, _), _) :: _ -> [ Id head ] + | ((head, _, _), _) :: _ -> [ Id head ] in - let do_branch ((head, args), term) = + let do_branch ((head, _, args), term) = let (term_context, args_domain) = List.fold_left (fun (cont, dom) (name, typ) -> @@ -515,7 +505,7 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function branches_dom @ outtype_dom @ term_dom @ (match indty_ident with | None -> get_first_constructor branches - | Some ident -> [ Id ident ]) + | Some (ident, _) -> [ Id ident ]) | CicNotationPt.Cast (term, ty) -> let term_dom = domain_rev_of_term ~loc context term in let ty_dom = domain_rev_of_term ~loc context ty in @@ -645,7 +635,8 @@ sig context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:aliases -> (* previous interpretation status *) + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> CicNotationPt.term -> (environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) @@ -656,7 +647,8 @@ sig val disambiguate_obj : ?fresh_instances:bool -> dbd:Mysql.dbd -> - aliases:aliases -> (* previous interpretation status *) + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) GrafiteAst.obj -> (environment * (* new interpretation status *) @@ -699,15 +691,10 @@ module Make (C: Callbacks) = uris let disambiguate_thing ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing = debug_print "DISAMBIGUATE INPUT"; - let current_env, multi_aliases_env = - match aliases with - | false, e -> Environment.hd e, None - | true, e -> Environment.empty, Some e - in let disambiguate_context = (* cic context -> disambiguate context *) List.map (function None -> Cic.Anonymous | Some (name, _) -> name) @@ -718,9 +705,11 @@ module Make (C: Callbacks) = debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" (string_of_domain thing_dom)); debug_print (sprintf "DISAMBIGUATION ENVIRONMENT: %s" - (DisambiguatePp.pp_environment (snd aliases))); + (DisambiguatePp.pp_environment aliases)); + debug_print (sprintf "DISAMBIGUATION UNIVERSE: %s" + (match universe with None -> "None" | Some _ -> "Some _")); let current_dom = - Environment.fold (fun item _ dom -> item :: dom) current_env [] + Environment.fold (fun item _ dom -> item :: dom) aliases [] in let todo_dom = domain_diff thing_dom current_dom in (* (2) lookup function for any item (Id/Symbol/Num) *) @@ -737,7 +726,7 @@ module Make (C: Callbacks) = | Num instance -> DisambiguateChoices.lookup_num_choices () in - match multi_aliases_env with + match universe with | None -> lookup_in_library () | Some e -> (try @@ -774,7 +763,7 @@ module Make (C: Callbacks) = (* (3) test an interpretation filling with meta uninterpreted identifiers *) - let test_env current_env todo_dom ugraph = + let test_env aliases todo_dom ugraph = let filled_env = List.fold_left (fun env item -> @@ -783,7 +772,7 @@ module Make (C: Callbacks) = (match item with | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) - current_env todo_dom + aliases todo_dom in try let cic_thing = @@ -797,12 +786,12 @@ module Make (C: Callbacks) = | Invalid_choice -> Ko, ugraph in (* (4) build all possible interpretations *) - let rec aux current_env todo_dom base_univ = + let rec aux aliases todo_dom base_univ = match todo_dom with | [] -> - (match test_env current_env [] base_univ with + (match test_env aliases [] base_univ with | Ok (thing, metasenv),new_univ -> - [ current_env, metasenv, thing, new_univ ] + [ aliases, metasenv, thing, new_univ ] | Ko,_ | Uncertain,_ -> []) | item :: remaining_dom -> debug_print (sprintf "CHOOSED ITEM: %s" @@ -813,7 +802,7 @@ module Make (C: Callbacks) = | codomain_item :: tl -> debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ; let new_env = - Environment.add item codomain_item current_env + Environment.add item codomain_item aliases in (match test_env new_env remaining_dom univ with | Ok (thing, metasenv),new_univ -> @@ -833,7 +822,7 @@ module Make (C: Callbacks) = let base_univ = initial_ugraph in try let res = - match aux current_env todo_dom base_univ with + match aux aliases todo_dom base_univ with | [] -> raise NoWellTypedInterpretation | [ e,me,t,u ] -> debug_print "SINGLE INTERPRETATION"; @@ -868,7 +857,7 @@ module Make (C: Callbacks) = let choices, b = res in (List.map (fun (env, metasenv, t, ugraph) -> - Environment.fold Environment.cons env (snd aliases), + Environment.fold Environment.add env aliases, metasenv, t, ugraph) choices), b @@ -877,21 +866,23 @@ module Make (C: Callbacks) = failwith "Disambiguate: circular dependency" let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term = let term = if fresh_instances then CicNotationUtil.freshen_term term else term in disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases - ~uri:None ~pp_thing:CicNotationPp.pp_term + ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term ~refine_thing:refine_term term - let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~uri obj = + let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri + obj + = let obj = if fresh_instances then CicNotationUtil.freshen_obj obj else obj in - disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri + disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj obj @@ -916,7 +907,7 @@ struct let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in try fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast - ?initial_ugraph ~aliases:(false, aliases)) + ?initial_ugraph ~aliases ~universe:None) with Exit -> raise (Ambiguous_term term) end