parse mutually inductive definitions

src/parser/parser.mly

@@ -151,8 +151,8 @@
 %left prec_ident
 %left LEFTSQ
 
-%nonassoc prec_logics prec_types
-%nonassoc LOGIC TYPE
+%nonassoc prec_decls
+%nonassoc LOGIC TYPE INDUCTIVE
 
 /* Entry points */
 
@@ -273,45 +273,44 @@ logic_def_option:
 
 logic_decl:
 | LOGIC lident params logic_type_option logic_def_option
-    { { ld_loc = loc ();
-	ld_ident = $2; ld_params = $3; ld_type = $4; ld_def = $5; } }
+  { { ld_loc = loc (); ld_ident = $2; ld_params = $3; 
+      ld_type = $4; ld_def = $5; } }
 ;
 
 list1_logic_decl:
-| logic_decl                  %prec prec_logics { [$1] }
-| logic_decl list1_logic_decl                   { $1 :: $2 }
+| logic_decl                  %prec prec_decls { [$1] }
+| logic_decl list1_logic_decl                  { $1 :: $2 }
 ;
 
 type_decl:
-| TYPE typedecl typedefn
-  { let _, pl, id = $2 in
-    { td_loc = loc (); td_ident = id; td_params = pl; td_def = $3 } }
+| TYPE type_args lident typedefn
+  { { td_loc = loc (); td_ident = $3; td_params = $2; td_def = $4 } }
 ;
 
 list1_type_decl:
-| type_decl                  %prec prec_types { [$1] }
+| type_decl                  %prec prec_decls { [$1] }
 | type_decl list1_type_decl                   { $1 :: $2 }
 ;
 
-decl:
-| list1_type_decl
-   { TypeDecl (loc (), $1) }
-| list1_logic_decl
-   { Logic (loc (), $1) }
-| AXIOM uident COLON lexpr
-   { Prop (loc (), Kaxiom, $2, $4) }
-| GOAL uident COLON lexpr
-   { Prop (loc (), Kgoal, $2, $4) }
-| LEMMA uident COLON lexpr
-   { Prop (loc (), Klemma, $2, $4) }
+inductive_decl:
 | INDUCTIVE lident primitive_types inddefn
-   { Inductive_def (loc (), $2, $3, $4) }
-| CLONE use clone_subst
-   { UseClone (loc (), $2, Some $3) }
-| USE use
-   { UseClone (loc (), $2, None) }
-| NAMESPACE uident list0_decl END
-   { Namespace (loc (), $2, $3) }
+  { { in_loc = loc (); in_ident = $2; in_params = $3; in_def = $4 } }
+
+list1_inductive_decl:
+| inductive_decl                      %prec prec_decls { [$1] }
+| inductive_decl list1_inductive_decl                  { $1 :: $2 }
+;
+
+decl:
+| list1_type_decl                 { TypeDecl $1 }
+| list1_logic_decl                { LogicDecl $1 }
+| list1_inductive_decl            { IndDecl $1 }
+| AXIOM uident COLON lexpr        { PropDecl (loc (), Kaxiom, $2, $4) }
+| LEMMA uident COLON lexpr        { PropDecl (loc (), Klemma, $2, $4) }
+| GOAL uident COLON lexpr         { PropDecl (loc (), Kgoal, $2, $4) }
+| USE use                         { UseClone (loc (), $2, None) }
+| CLONE use clone_subst           { UseClone (loc (), $2, Some $3) }
+| NAMESPACE uident list0_decl END { Namespace (loc (), $2, $3) }
 ;
 
 list1_theory:
@@ -326,13 +325,10 @@ theory:
    { { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
 ;
 
-typedecl:
-| lident
-    { (loc_i 1, [], $1) }
-| type_var lident
-    { (loc_i 2, [$1], $2) }
-| LEFTPAR type_var COMMA list1_type_var_sep_comma RIGHTPAR lident
-    { (loc_i 6, $2 :: $4, $6) }
+type_args:
+| /* epsilon */                                             { [] }
+| type_var                                                  { [$1] }
+| LEFTPAR type_var COMMA list1_type_var_sep_comma RIGHTPAR  { $2 :: $4 }
 ;
 
 typedefn:

src/parser/ptree.mli

@@ -119,14 +119,21 @@ type logic_decl = {
   ld_def    : lexpr option;
 }
 
+type ind_decl = {
+  in_loc    : loc;
+  in_ident  : ident;
+  in_params : pty list;
+  in_def    : (ident * lexpr) list;
+}
+
 type prop_kind =
   | Kaxiom | Klemma | Kgoal
 
 type decl = 
-  | TypeDecl of loc * type_decl list
-  | Logic of loc * logic_decl list
-  | Prop of loc * prop_kind * ident * lexpr
-  | Inductive_def of loc * ident * pty list * (ident * lexpr) list
+  | TypeDecl of type_decl list
+  | LogicDecl of logic_decl list
+  | IndDecl of ind_decl list
+  | PropDecl of loc * prop_kind * ident * lexpr
   | UseClone of loc * use * clone_subst list option
   | Namespace of loc * ident * decl list
 

src/parser/typing.ml

@@ -726,7 +726,7 @@ and fmla env = function
 
 open Ptree
 
-let add_types loc dl th =
+let add_types dl th =
   let ns = get_namespace th in
   let def = 
     List.fold_left 
@@ -826,7 +826,7 @@ let add_types loc dl th =
 let env_of_vsymbol_list vl =
   List.fold_left (fun env v -> M.add v.vs_name.id_short v env) M.empty vl
 
-let add_logics loc dl th =
+let add_logics dl th =
   let ns = get_namespace th in
   let fsymbols = Hashtbl.create 17 in
   let psymbols = Hashtbl.create 17 in
@@ -834,8 +834,9 @@ let add_logics loc dl th =
   (* 1. create all symbols and make an environment with these symbols *)
   let create_symbol th d = 
     let id = d.ld_ident.id in
-    if Hashtbl.mem denvs id || Mnm.mem id ns.ns_ls then error ~loc (Clash id);
-    let v = id_user id loc in
+    if Hashtbl.mem denvs id || Mnm.mem id ns.ns_ls 
+      then error ~loc:d.ld_loc (Clash id);
+    let v = id_user id d.ld_ident.id_loc in
     let denv = create_denv th in
     Hashtbl.add denvs id denv;
     let type_ty (_,t) = ty_of_dty (dty denv t) in
@@ -990,19 +991,37 @@ let rec check_clausal_form loc ps f = match f.f_node with
   | _ -> 
       check_unquantified_clausal_form loc ps f
 
-let add_inductive loc id tyl cl th =
-  let denv = create_denv th in
-  let pl = List.map (fun ty -> ty_of_dty (dty denv ty)) tyl in
-  let ps = create_psymbol (id_user id.id loc) pl in
-  let th' = add_decl th (create_logic_decl [Lpredicate (ps, None)]) in
-  let clause (id, f) = 
-    let loc = f.pp_loc in
-    let f' = fmla th' f in
-    check_clausal_form loc ps f';
-    create_prop (id_user id.id id.id_loc) f'
+let add_inductives dl th =
+  let ns = get_namespace th in
+  let psymbols = Hashtbl.create 17 in
+  (* 1. create all symbols and make an environment with these symbols *)
+  let create_symbol th d = 
+    let id = d.in_ident.id in
+    if Hashtbl.mem psymbols id || Mnm.mem id ns.ns_ls 
+      then error ~loc:d.in_loc (Clash id);
+    let v = id_user id d.in_ident.id_loc in
+    let denv = create_denv th in
+    let type_ty t = ty_of_dty (dty denv t) in
+    let pl = List.map type_ty d.in_params in
+    let ps = create_psymbol v pl in
+    Hashtbl.add psymbols id ps;
+    add_decl th (create_logic_decl [Lpredicate (ps, None)])
   in
-  let cl = List.map clause cl in
-  add_decl th (create_ind_decl [(ps,cl)])
+  let th' = List.fold_left create_symbol th dl in
+  (* 2. then type-check all definitions *)
+  let type_decl d = 
+    let id = d.in_ident.id in
+    let ps = Hashtbl.find psymbols id in
+    let clause (id, f) = 
+      let loc = f.pp_loc in
+      let f' = fmla th' f in
+      check_clausal_form loc ps f';
+      create_prop (id_user id.id id.id_loc) f'
+    in
+    ps, List.map clause d.in_def
+  in
+  let dl = List.map type_decl dl in
+  add_decl th (create_ind_decl dl)
 
 let find_in_loadpath env f =
   let rec find c lp = match lp, c with
@@ -1092,14 +1111,14 @@ and type_theory env id pt =
 and add_decls env th = List.fold_left (add_decl env) th
 
 and add_decl env th = function
-  | TypeDecl (loc, dl) ->
-      add_types loc dl th
-  | Logic (loc, dl) ->
-      add_logics loc dl th
-  | Prop (loc, k, s, f) ->
+  | TypeDecl dl ->
+      add_types dl th
+  | LogicDecl dl ->
+      add_logics dl th
+  | IndDecl dl ->
+      add_inductives dl th
+  | PropDecl (loc, k, s, f) ->
       add_prop (prop_kind k) loc s f th
-  | Inductive_def (loc, id, tyl, cl) ->
-      add_inductive loc id tyl cl th
   | UseClone (loc, use, subst) ->
       let t = find_theory env use.use_theory in
       let use_or_clone th = match subst with