X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=110f3d75ea1578b8f5ae2eb7735a48e61147eeae;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=3d2325c05b7cbb21d10e67dc20023615a2de12ce;hpb=e82d6ed939d9ab6b0cff9b6a469a006732d0da51;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 3d2325c05..110f3d75e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -51,13 +51,14 @@ let refine metasenv context term =
   let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
   debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
   try
-    let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in
+    let term', _, metasenv' = CicRefine.type_of_aux' metasenv context term in
     Ok (term', metasenv')
   with
     | CicRefine.Uncertain _ ->
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
     | _ ->
+        (* TODO we should catch only the RefineFailure excecption *)
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
@@ -75,12 +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
@@ -89,52 +92,66 @@ 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 (pat, term) =
+        let do_branch ((head, args), term) =
           let rec do_branch' context = function
             | [] -> aux loc context term
-            | hd :: tl ->
-                let cic_body = do_branch' (Cic.Name hd :: context) tl in
-                Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body)
+            | (name, typ) :: tl ->
+                let cic_body = do_branch' (name :: context) tl in
+                let typ =
+                  match typ with
+                  | None -> Cic.Implicit (Some `Type)
+                  | Some typ -> aux loc context typ
+                in
+                Cic.Lambda (name, typ, cic_body)
           in
-          match pat with
-          | _ :: tl -> (* ignoring constructor *) do_branch' context tl
-          | [] -> assert false
+          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
+          | 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 (var, def, body) ->
+    | CicAst.LetIn ((name, typ), def, body) ->
         let cic_def = aux loc context def in
-        let name = Cic.Name var in
+        let cic_def =
+          match typ with
+          | None -> cic_def
+          | Some t -> Cic.Cast (cic_def, aux loc context t)
+        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 (var, _, _, _) -> Cic.Name var :: acc)
+          List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
             context defs
         in
         let cic_body = aux loc context' body in
         let inductiveFuns =
           List.map
-            (fun (var, body, typ, decr_idx) ->
+            (fun ((name, typ), body, decr_idx) ->
               let cic_body = aux loc context' body in
               let cic_type = aux_option loc context typ in
-              (var, decr_idx, cic_type, cic_body))
+              let name =
+                match name with
+                | Cic.Anonymous ->
+                    CicTextualParser2.fail loc
+                      "Recursive functions cannot be anonymous"
+                | Cic.Name name -> name
+              in
+              (name, decr_idx, cic_type, cic_body))
             defs
         in
-        let counter = ref 0 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
-           * indcutiveFun list, see Cic.term *)
+           * inductiveFun list, see Cic.term *)
           match kind with
           | `Inductive ->
               (fun (var, _, _, _) cic ->
@@ -145,106 +162,151 @@ let interpretate ~context ~env ast =
                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
               in
               (fun (var, _, _, _) cic ->
+                incr counter;
                 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
           if subst <> [] then
-            CicTextualParser2.fail loc "Explicit substitutions not allowed here";
+            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) ->
+    | 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 (pat, term) =
-          match pat with
-          | _ :: tl ->
-              aux loc
-                (List.fold_left (fun acc var -> (Cic.Name var) :: acc)
-                  context tl)
-                term
-          | [] -> assert false
+        let do_branch ((head, args), term) =
+          let (term_context, args_domain) =
+            List.fold_left
+              (fun (cont, dom) (name, typ) ->
+                (name :: cont,
+                 (match typ with
+                 | None -> dom
+                 | Some typ -> aux loc cont typ @ dom)))
+              (context, []) args
+          in
+          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, 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 where_dom = aux loc (Cic.Name var :: context) where in
-        Domain.union body_dom where_dom
-    | CicTextualParser2Ast.LetRec (kind, defs, where) ->
+        let type_dom = aux_option loc context typ in
+        let where_dom = aux loc (var :: context) where in
+        where_dom @ type_dom @ body_dom
+    | CicAst.LetRec (kind, defs, where) ->
         let context' =
-          List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
+          List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
             context defs
         in
         let where_dom = aux loc context' where in
         let defs_dom =
           List.fold_left
-            (fun dom (_, body, typ, _) ->
-              Domain.union (aux loc context' body) (aux_option loc context typ))
-            Domain.empty defs
+            (fun dom ((_, typ), body, _) ->
+              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
+            CicTextualParser2.fail loc
+              "Explicit substitutions not allowed here";
+          []
+        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
@@ -290,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
@@ -303,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
@@ -327,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 =
@@ -343,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
@@ -390,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