X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=110f3d75ea1578b8f5ae2eb7735a48e61147eeae;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;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..110f3d75e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -58,6 +58,7 @@ let refine metasenv context term =
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
     | _ ->
+        (* TODO we should catch only the RefineFailure excecption *)
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
@@ -75,13 +76,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 +92,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 +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,12 +112,12 @@ let interpretate ~context ~env ast =
         let (indtype_uri, indtype_no) =
           match resolve env (Id indty_ident) () with
           | Cic.MutInd (uri, tyno, _) -> uri, tyno
-          | Cic.Implicit -> raise Try_again
+          | 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 +126,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,7 +166,7 @@ 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) ->
+    | CicAst.Ident (name, subst) ->
         (* TODO hanlde explicit substitutions *)
         (try
           let index = find_in_environment name context in
@@ -173,40 +175,43 @@ let interpretate ~context ~env ast =
               "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) ->
+    | 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
+    | 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 (_, (var, typ), body) ->
         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
+    | 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 +221,21 @@ 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 @ [ Id indty_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 +244,69 @@ 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) ->
+        where_dom @ defs_dom
+    | CicAst.Ident (name, subst) ->
         (* TODO hanlde explicit substitutions *)
         (try
           let index = find_in_environment name context in
           if subst <> [] 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
+          []
+        with Not_found -> [ Id name ])
+    | 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
@@ -316,10 +352,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 +361,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 +388,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,35 +408,34 @@ 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
+        match todo_dom with
+        | [] ->
+            (match test_env current_env [] with
+            | Ok (term, metasenv) -> [ current_env, term, metasenv ]
+            | 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, term, metasenv ]
+                      | _ -> aux new_env remaining_dom) @ filter tl
+                  | Uncertain ->
+                      (match remaining_dom with
+                      | [] -> []
+                      | _ -> 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
@@ -416,7 +454,7 @@ module Make (C: Callbacks) =
                         fst (Environment.find domain_item env)
                       in
                       (descr_of_domain_item domain_item, description))
-                    (Domain.elements term_dom))
+                    term_dom)
                 l
             in
             let choosed = C.interactive_interpretation_choice choices in