- changed ast for pattern matching so that type annotations are possible

- bugfix for indexes in Fix/CoFix cases

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 3d2325c05b7cbb21d10e67dc20023615a2de12ce..5a8b9a646b02749946276b92e65206ed971deb77 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -76,11 +76,12 @@ 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 terms ->
+        Cic.Appl (List.map (aux loc context) terms)
     | CicTextualParser2Ast.Appl_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) ->
+    | CicTextualParser2Ast.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
@@ -92,16 +93,19 @@ let interpretate ~context ~env ast =
     | CicTextualParser2Ast.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 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
@@ -111,30 +115,41 @@ let interpretate ~context ~env ast =
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
-    | CicTextualParser2Ast.LetIn (var, def, body) ->
+    | CicTextualParser2Ast.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) ->
         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,6 +160,7 @@ 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
@@ -153,7 +169,8 @@ let interpretate ~context ~env ast =
         (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 ()
@@ -185,21 +202,24 @@ let domain_of_term ~context ast =
     | 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) ->
+    | CicTextualParser2Ast.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) ->
         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 -> Domain.union dom (aux loc cont typ))))
+              (context, Domain.empty) args
+          in
+          Domain.union (aux loc term_context term) args_domain
         in
         let branches_dom =
           List.fold_left (fun dom branch -> Domain.union dom (do_branch branch))
@@ -207,19 +227,24 @@ let domain_of_term ~context ast =
         in
         Domain.add (Id indty_ident)
           (Domain.union outtype_dom (Domain.union term_dom branches_dom))
-    | CicTextualParser2Ast.LetIn (var, body, where) ->
+    | CicTextualParser2Ast.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
+        let type_dom = 
+          match typ with
+          | None -> Domain.empty
+          | Some typ -> aux 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) ->
         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, _) ->
+            (fun dom ((_, typ), body, _) ->
               Domain.union (aux loc context' body) (aux_option loc context typ))
             Domain.empty defs
         in
@@ -229,7 +254,8 @@ let domain_of_term ~context ast =
         (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";
           Domain.empty
         with Not_found -> Domain.singleton (Id name))
     | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i)