X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=92b081c4841b00833727309e69b9787bbc41ed3e;hb=78a92e3cc2deb60d306da93d9dcf987c1cb219ba;hp=41c404392f429b2ac4a68debe6c5f9c36207a34c;hpb=616ca3a4330ac51127b0bd91644354ac888d1ce3;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 41c404392..92b081c48 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -57,12 +57,14 @@ let refine metasenv context term =
     | CicRefine.Uncertain _ ->
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
-    | _ ->
+    | CicRefine.RefineFailure _ ->
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
-  snd (Environment.find item env) env num args
+  try
+    snd (Environment.find item env) env num args
+  with Not_found -> assert false
 
   (* TODO move it to Cic *)
 let find_in_environment name context =
@@ -75,13 +77,14 @@ let find_in_environment name context =
 
 let interpretate ~context ~env ast =
   let rec aux loc context = function
-    | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-    | CicTextualParser2Ast.Appl terms ->
-        Cic.Appl (List.map (aux loc context) terms)
-    | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
+    | CicAst.AttributedTerm (`Loc loc, term) ->
+        aux loc context term
+    | CicAst.AttributedTerm (_, term) -> aux loc context term
+    | CicAst.Appl (CicAst.Symbol (symb, i) :: args) ->
         let cic_args = List.map (aux loc context) args in
         resolve env (Symbol (symb, i)) ~args:cic_args ()
-    | CicTextualParser2Ast.Binder (binder_kind, (var, typ), body) ->
+    | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
+    | CicAst.Binder (binder_kind, (var, typ), body) ->
         let cic_type = aux_option loc context typ in
         let cic_body = aux loc (var :: context) body in
         (match binder_kind with
@@ -90,7 +93,7 @@ let interpretate ~context ~env ast =
         | `Exists ->
             resolve env (Symbol ("exists", 0))
               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
-    | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
+    | CicAst.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux loc context term in
         let cic_outtype = aux_option loc context outtype in
         let do_branch ((head, args), term) =
@@ -100,7 +103,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)
@@ -108,14 +111,27 @@ 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))
-    | CicTextualParser2Ast.LetIn ((name, typ), def, body) ->
+    | CicAst.LetIn ((name, typ), def, body) ->
         let cic_def = aux loc context def in
         let cic_def =
           match typ with
@@ -124,7 +140,7 @@ let interpretate ~context ~env ast =
         in
         let cic_body = aux loc (name :: context) body in
         Cic.LetIn (name, cic_def, cic_body)
-    | CicTextualParser2Ast.LetRec (kind, defs, body) ->
+    | CicAst.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
             context defs
@@ -164,49 +180,114 @@ let interpretate ~context ~env ast =
                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
-    | CicTextualParser2Ast.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
+    | CicAst.Ident (name, subst) ->
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
+          if subst <> None then
             CicTextualParser2.fail loc
               "Explicit substitutions not allowed here";
           Cic.Rel index
-        with Not_found -> resolve env (Id name) ())
-    | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num ()
-    | CicTextualParser2Ast.Meta (index, subst) ->
+        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
+            (match subst with
+            | Some subst ->
+                List.map
+                  (fun (s, term) ->
+                    (try
+                      List.assoc s ids_to_uris, aux loc context term
+                     with Not_found ->
+                       raise DisambiguateChoices.Invalid_choice))
+                  subst
+            | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
+         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 =
           List.map
             (function None -> None | Some term -> Some (aux loc context term))
             subst
         in
         Cic.Meta (index, cic_subst)
-    | CicTextualParser2Ast.Sort `Prop -> Cic.Sort Cic.Prop
-    | CicTextualParser2Ast.Sort `Set -> Cic.Sort Cic.Set
-    | CicTextualParser2Ast.Sort `Type -> Cic.Sort Cic.Type
-    | CicTextualParser2Ast.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
+    | CicAst.Sort `Set -> Cic.Sort Cic.Set
+    | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+    | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
+    | 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
-  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-  | _ -> assert false
+  | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+  | term -> aux (-1, -1) context term
 
 let domain_of_term ~context ast =
+    (* "aux" keeps domain in reverse order and doesn't care about duplicates.
+     * Domain item more in deep in the list will be processed first.
+     *)
   let rec aux loc context = function
-    | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
-    | CicTextualParser2Ast.Appl terms ->
-        List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
-          Domain.empty terms
-    | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
-        List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
-          (Domain.singleton (Symbol (symb, i))) args
-    | CicTextualParser2Ast.Binder (_, (var, typ), body) ->
+    | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+    | CicAst.AttributedTerm (_, term) -> aux loc context term
+    | CicAst.Appl terms ->
+        List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
+    | CicAst.Binder (kind, (var, typ), body) ->
+        let kind_dom =
+          match kind with
+          | `Exists -> [ Symbol ("exists", 0) ]
+          | _ -> []
+        in
         let type_dom = aux_option loc context typ in
         let body_dom = aux loc (var :: context) body in
-        Domain.union type_dom body_dom
-    | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
+        body_dom @ type_dom @ kind_dom
+    | CicAst.Case (term, indty_ident, outtype, branches) ->
         let term_dom = aux loc context term in
         let outtype_dom = aux_option loc context outtype in
         let do_branch ((head, args), term) =
@@ -216,27 +297,22 @@ let domain_of_term ~context ast =
                 (name :: cont,
                  (match typ with
                  | None -> dom
-                 | Some typ -> Domain.union dom (aux loc cont typ))))
-              (context, Domain.empty) args
+                 | Some typ -> aux loc cont typ @ dom)))
+              (context, []) args
           in
-          Domain.union (aux loc term_context term) args_domain
+          args_domain @ aux loc term_context term
         in
         let branches_dom =
-          List.fold_left (fun dom branch -> Domain.union dom (do_branch branch))
-            Domain.empty branches
+          List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
         in
-        Domain.add (Id indty_ident)
-          (Domain.union outtype_dom (Domain.union term_dom branches_dom))
-    | CicTextualParser2Ast.LetIn ((var, typ), body, where) ->
+        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 = 
-          match typ with
-          | None -> Domain.empty
-          | Some typ -> aux loc context typ
-        in
+        let type_dom = aux_option loc context typ in
         let where_dom = aux loc (var :: context) where in
-        Domain.union (Domain.union body_dom where_dom) type_dom
-    | CicTextualParser2Ast.LetRec (kind, defs, where) ->
+        where_dom @ type_dom @ body_dom
+    | CicAst.LetRec (kind, defs, where) ->
         let context' =
           List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
             context defs
@@ -245,32 +321,77 @@ let domain_of_term ~context ast =
         let defs_dom =
           List.fold_left
             (fun dom ((_, typ), body, _) ->
-              Domain.union (aux loc context' body) (aux_option loc context typ))
-            Domain.empty defs
+              aux loc context' body @ aux_option loc context typ)
+            [] defs
         in
-        Domain.union where_dom defs_dom
-    | CicTextualParser2Ast.Ident (name, subst) ->
-        (* TODO hanlde explicit substitutions *)
+        where_dom @ defs_dom
+    | CicAst.Ident (name, subst) ->
         (try
           let index = find_in_environment name context in
-          if subst <> [] then
+          if subst <> None then
             CicTextualParser2.fail loc
-              "Explicit substitutions not allowed here";
-          Domain.empty
-        with Not_found -> Domain.singleton (Id name))
-    | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i)
-    | CicTextualParser2Ast.Meta (index, local_context) ->
-        List.fold_left
-          (fun dom term -> Domain.union dom (aux_option loc context term))
-            Domain.empty local_context
-    | CicTextualParser2Ast.Sort _ -> Domain.empty
+              "Explicit substitutions not allowed here"
+          else
+            []
+        with Not_found ->
+          (match subst with
+          | None -> [Id name]
+          | Some subst ->
+              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) ->
+        List.fold_left (fun dom term -> aux_option loc context term @ dom) []
+          local_context
+    | CicAst.Sort _ -> []
+    | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+
   and aux_option loc context = function
-    | None -> Domain.empty
+    | None -> []
     | Some t -> aux loc context t
   in
-  match ast with
-  | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
-  | _ -> assert false
+
+    (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
+  let rev_uniq =
+    let module SortedItem =
+      struct
+        type t = DisambiguateTypes.domain_item
+        let compare = Pervasives.compare
+      end
+    in
+    let module Set = Set.Make (SortedItem) in
+    fun l ->
+      let rev_l = List.rev l in
+      let (_, uniq_rev_l) =
+        List.fold_left
+          (fun (members, rev_l) elt ->
+            if Set.mem elt members then
+              (members, rev_l)
+            else
+              Set.add elt members, elt :: rev_l)
+          (Set.empty, []) rev_l
+      in
+      List.rev uniq_rev_l
+  in
+            
+  rev_uniq
+    (match ast with
+    | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+    | term -> aux (-1, -1) context term)
+
+
+  (* dom1 \ dom2 *)
+let domain_diff dom1 dom2 =
+(* let domain_diff = Domain.diff *)
+  let is_in_dom2 =
+    List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
+      (fun _ -> false) dom2
+  in
+  List.filter (fun elt -> not (is_in_dom2 elt)) dom1
 
 module Make (C: Callbacks) =
   struct
@@ -282,18 +403,11 @@ module Make (C: Callbacks) =
        (function uri,_ ->
          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
        ) result in
-      C.output_html (`Msg (`T "Locate query:"));
-      MQueryUtil.text_of_query
-       (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
-       "" query; 
-      C.output_html (`Msg (`T "Result:"));
-      MQueryUtil.text_of_result
-        (fun s -> C.output_html (`Msg (`T s))) "" result;
       let uris' =
        match uris with
         | [] ->
            [UriManager.string_of_uri (C.input_or_locate_uri
-            ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+            ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id)]
         | [uri] -> [uri]
         | _ ->
             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
@@ -316,10 +430,6 @@ module Make (C: Callbacks) =
 
     let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
     =
-      let current_dom = (* TODO temporary, remove ASAP *)
-        Environment.fold (fun item _ dom -> Domain.add item dom)
-          current_env Domain.empty
-      in
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
         List.map
@@ -329,7 +439,10 @@ module Make (C: Callbacks) =
       let term_dom = domain_of_term ~context:disambiguate_context term in
       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
         (string_of_domain term_dom));
-      let todo_dom = Domain.diff term_dom current_dom in
+      let current_dom =
+        Environment.fold (fun item _ dom -> item :: dom) current_env []
+      in
+      let todo_dom = domain_diff term_dom current_dom in
       (* (2) lookup function for any item (Id/Symbol/Num) *)
       let lookup_choices =
         let id_choices = Hashtbl.create 1023 in
@@ -353,10 +466,14 @@ module Make (C: Callbacks) =
        *)
       let test_env current_env todo_dom =
         let filled_env =
-          Domain.fold
-            (fun item env ->
-              Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
-            todo_dom current_env
+          List.fold_left
+            (fun env item ->
+              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
           let cic_term =
@@ -369,60 +486,56 @@ module Make (C: Callbacks) =
       in
       (* (4) build all possible interpretations *)
       let rec aux current_env todo_dom =
-        if Domain.is_empty todo_dom then
-          match test_env current_env Domain.empty with
-          | Ok (term, metasenv) -> [ current_env, term, metasenv ]
-          | Ko | Uncertain -> []
-        else
-          let item = Domain.choose todo_dom in
-          let remaining_dom = Domain.remove item todo_dom in
-          debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item));
-          let choices = lookup_choices item in
-          let rec filter = function
-            | [] -> []
-            | codomain_item :: tl ->
-                let new_env = Environment.add item codomain_item current_env in
-                (match test_env new_env remaining_dom with
-                | Ok (term, metasenv) ->
-                    (if Domain.is_empty remaining_dom then
-                      [ new_env, term, metasenv ]
-                    else
-                      aux new_env remaining_dom)
-                    @ filter tl
-                | Uncertain ->
-                    (if Domain.is_empty remaining_dom then
-                      []
-                    else
-                      aux new_env remaining_dom)
-                    @ filter tl
-                | Ko -> filter tl)
-          in
-          filter choices
-      in
-      let (choosed_env, choosed_term, choosed_metasenv) =
-        match aux current_env todo_dom with
-        | [] -> raise NoWellTypedInterpretation
-        | [ x ] ->
-            debug_print "UNA SOLA SCELTA";
-            x
-        | l ->
-            debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
-            let choices =
-              List.map
-                (fun (env, _, _) ->
-                  List.map
-                    (fun domain_item ->
-                      let description =
-                        fst (Environment.find domain_item env)
-                      in
-                      (descr_of_domain_item domain_item, description))
-                    (Domain.elements term_dom))
-                l
+        match todo_dom with
+        | [] ->
+            (match test_env current_env [] with
+            | Ok (term, metasenv) -> [ current_env, metasenv, term ]
+            | Ko | Uncertain -> [])
+        | item :: remaining_dom ->
+            debug_print (sprintf "CHOOSED ITEM: %s"
+              (string_of_domain_item item));
+            let choices = lookup_choices item in
+            let rec filter = function
+              | [] -> []
+              | codomain_item :: tl ->
+                  debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
+                  let new_env =
+                    Environment.add item codomain_item current_env
+                  in
+                  (match test_env new_env remaining_dom with
+                  | Ok (term, metasenv) ->
+                      (match remaining_dom with
+                      | [] -> [ new_env, metasenv, term ]
+                      | _ -> aux new_env remaining_dom) @ filter tl
+                  | Uncertain ->
+                      (match remaining_dom with
+                      | [] -> []
+                      | _ -> aux new_env remaining_dom) @ filter tl
+                  | Ko -> filter tl)
             in
-            let choosed = C.interactive_interpretation_choice choices in
-            List.nth l choosed
+            filter choices
       in
-      (choosed_env, choosed_metasenv, choosed_term)
+       match aux current_env todo_dom with
+       | [] -> raise NoWellTypedInterpretation
+       | [ _ ] as l ->
+           debug_print "UNA SOLA SCELTA";
+           l
+       | l ->
+           debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
+           let choices =
+             List.map
+               (fun (env, _, _) ->
+                 List.map
+                   (fun domain_item ->
+                     let description =
+                       fst (Environment.find domain_item env)
+                     in
+                     (descr_of_domain_item domain_item, description))
+                   term_dom)
+               l
+           in
+           let choosed = C.interactive_interpretation_choice choices in
+            List.map (List.nth l) choosed
 
   end