X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=06f18080d07466aaccba41ca71b3d83599ae4678;hb=5a9b1f46a8e866382a71d686e689e9e5907f1824;hp=a539ffd8cba2c468397f61bf8658d0ba9b0741cf;hpb=e563cf1b47357253b2304eb19b7374afed1df8b5;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index a539ffd8c..06f18080d 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -102,7 +102,7 @@ let interpretate ~context ~env ast = let cic_body = do_branch' (name :: context) tl in let typ = match typ with - | None -> Cic.Implicit + | None -> Cic.Implicit (Some `Type) | Some typ -> aux loc context typ in Cic.Lambda (name, typ, cic_body) @@ -110,10 +110,23 @@ let interpretate ~context ~env ast = do_branch' context args in let (indtype_uri, indtype_no) = - match resolve env (Id indty_ident) () with - | Cic.MutInd (uri, tyno, _) -> uri, tyno - | Cic.Implicit -> raise Try_again - | _ -> raise DisambiguateChoices.Invalid_choice + 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 + | _ -> raise DisambiguateChoices.Invalid_choice) + | None -> + let fst_constructor = + match branches with + | ((head, _), _) :: _ -> head + | [] -> raise DisambiguateChoices.Invalid_choice + in + (match resolve env (Id fst_constructor) () with + | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> + (indtype_uri, indtype_no) + | Cic.Implicit _ -> raise Try_again + | _ -> raise DisambiguateChoices.Invalid_choice) in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -174,8 +187,62 @@ let interpretate ~context ~env ast = CicTextualParser2.fail loc "Explicit substitutions not allowed here"; Cic.Rel index - with Not_found -> resolve env (Id name) ()) - | CicAst.Implicit -> Cic.Implicit + with Not_found -> + let cic = 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 + List.map + (fun (s, term) -> + (try + List.assoc s ids_to_uris, aux loc context term + with Not_found -> raise DisambiguateChoices.Invalid_choice)) + subst + in + (match cic with + | Cic.Const (uri, []) -> + let uris = + match CicEnvironment.get_obj uri with + | Cic.Constant (_, _, _, uris) -> uris + | _ -> assert false + in + Cic.Const (uri, mk_subst uris) + | Cic.Var (uri, []) -> + let uris = + match CicEnvironment.get_obj uri with + | Cic.Variable (_, _, _, uris) -> uris + | _ -> assert false + in + Cic.Var (uri, mk_subst uris) + | Cic.MutInd (uri, i, []) -> + let uris = + match CicEnvironment.get_obj uri with + | Cic.InductiveDefinition (_, uris, _) -> uris + | _ -> assert false + in + Cic.MutInd (uri, i, mk_subst uris) + | Cic.MutConstruct (uri, i, j, []) -> + let uris = + match CicEnvironment.get_obj uri with + | Cic.InductiveDefinition (_, uris, _) -> uris + | _ -> assert false + in + Cic.MutConstruct (uri, i, j, mk_subst uris) + | Cic.Meta _ | Cic.Implicit _ as t -> +(* + prerr_endline (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 ^ " := " ^ CicAstPp.pp_term term) + subst))); +*) + t + | _ -> + raise DisambiguateChoices.Invalid_choice)) + | CicAst.Implicit -> Cic.Implicit None | CicAst.Num (num, i) -> resolve env (Num i) ~num () | CicAst.Meta (index, subst) -> let cic_subst = @@ -191,7 +258,7 @@ let interpretate ~context ~env ast = | CicAst.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () and aux_option loc context = function - | None -> Cic.Implicit + | None -> Cic.Implicit (Some `Type) | Some term -> aux loc context term in match ast with @@ -229,7 +296,8 @@ let domain_of_term ~context ast = let branches_dom = List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches in - branches_dom @ outtype_dom @ term_dom @ [ Id indty_ident ] + branches_dom @ outtype_dom @ term_dom @ + (match indty_ident with None -> [] | Some ident -> [ Id ident ]) | CicAst.LetIn ((var, typ), body, where) -> let body_dom = aux loc context body in let type_dom = aux_option loc context typ in @@ -256,7 +324,12 @@ let domain_of_term ~context ast = CicTextualParser2.fail loc "Explicit substitutions not allowed here"; [] - with Not_found -> [ Id name ]) + with Not_found -> + List.fold_left + (fun dom (_, term) -> + let dom' = aux loc context term in + dom' @ dom) + [ Id name ] subst) | CicAst.Implicit -> [] | CicAst.Num (num, i) -> [ Num i ] | CicAst.Meta (index, local_context) -> @@ -293,9 +366,10 @@ let domain_of_term ~context ast = List.rev uniq_rev_l in - match ast with - | CicAst.AttributedTerm (`Loc loc, term) -> rev_uniq (aux loc context term) - | term -> aux (-1, -1) context term + rev_uniq + (match ast with + | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term + | term -> aux (-1, -1) context term) (* dom1 \ dom2 *) @@ -317,13 +391,13 @@ module Make (C: Callbacks) = (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri ) result in - C.output_html (`Msg (`T "Locate query:")); + HelmLogger.log (`Msg (`T "Locate query:")); MQueryUtil.text_of_query - (fun s -> C.output_html ~append_NL:false (`Msg (`T s))) + (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s))) "" query; - C.output_html (`Msg (`T "Result:")); + HelmLogger.log (`Msg (`T "Result:")); MQueryUtil.text_of_result - (fun s -> C.output_html (`Msg (`T s))) "" result; + (fun s -> HelmLogger.log (`Msg (`T s))) "" result; let uris' = match uris with | [] -> @@ -389,7 +463,11 @@ module Make (C: Callbacks) = let filled_env = List.fold_left (fun env item -> - Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env) + Environment.add item + ("Implicit", + (match item with + | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed)) + | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env) current_env todo_dom in try