5.34. Meta typing and Beta reduction

Start ocaml section to src/flx_beta.mli[1 /1 ]
     1: # 4 "./lpsrc/flx_beta.ipk"
     2: open Flx_types
     3: open Flx_mtypes2
     4: open Flx_ast
     5: 
     6: val metatype:
     7:   sym_state_t ->
     8:   range_srcref ->
     9:   btypecode_t ->
    10:   btypecode_t
    11: 
    12: val beta_reduce:
    13:   sym_state_t ->
    14:   range_srcref ->
    15:   btypecode_t ->
    16:   btypecode_t
    17: 
End ocaml section to src/flx_beta.mli[1]
Start ocaml section to src/flx_beta.ml[1 /1 ]
     1: # 22 "./lpsrc/flx_beta.ipk"
     2: open Flx_util
     3: open Flx_ast
     4: open Flx_types
     5: open Flx_mtypes1
     6: open Flx_mtypes2
     7: 
     8: open Flx_print
     9: open Flx_exceptions
    10: open Flx_typing
    11: open List
    12: open Flx_srcref
    13: open Flx_unify
    14: open Flx_maps
    15: 
    16: exception BTfound of btypecode_t
    17: 
    18: let rec metatype syms sr term =
    19:   (*
    20:   print_endline ("Find Metatype  of: " ^ string_of_btypecode syms.dfns term);
    21:   *)
    22:   let t = metatype' syms sr term in
    23:   (*
    24:   print_endline ("Metatype  of: " ^ string_of_btypecode syms.dfns term ^ " is " ^ sbt syms.dfns t);
    25:   print_endline "Done";
    26:   *)
    27:   t
    28: 
    29: and metatype' syms sr term =
    30:   let st t = string_of_btypecode syms.dfns t in
    31:   let mt t = metatype' syms sr t in
    32:   match term with
    33:   | `BTYP_lift t -> t
    34:   | `BTYP_case _ -> `BTYP_function (`BTYP_type 0, `BTYP_type 0)
    35: 
    36:   | `BTYP_typefun (a,b,c) ->
    37:     let ps = List.map snd a in
    38:     let argt =
    39:       match ps with
    40:       | [x] -> x
    41:       | _ -> `BTYP_tuple ps
    42:     in
    43:       let rt = metatype syms sr c in
    44:       if b<>rt
    45:       then
    46:         clierr sr
    47:         (
    48:           "In abstraction\n" ^
    49:           st term ^
    50:           "\nFunction body metatype \n"^
    51:           st rt^
    52:           "\ndoesn't agree with declared type \n" ^
    53:           st b
    54:         )
    55:       else `BTYP_function (argt,b)
    56: 
    57:   | `BTYP_type_tuple ts ->
    58:     `BTYP_tuple (map mt ts)
    59: 
    60:   | `BTYP_apply (a,b) ->
    61:     begin
    62:       let ta = mt a
    63:       and tb = mt b
    64:       in match ta with
    65:       | `BTYP_function (x,y) ->
    66:         if x = tb then y
    67:         else
    68:           clierr sr (
    69:             "Metatype error: function argument wrong metatype, expected:\n" ^
    70:             sbt syms.dfns x ^
    71:             "\nbut got:\n" ^
    72:             sbt syms.dfns tb
    73:           )
    74: 
    75:       | _ -> clierr sr
    76:         (
    77:           "Metatype error: function required for LHS of application:\n"^
    78:           sbt syms.dfns term ^
    79:           ", got metatype:\n" ^
    80:           sbt syms.dfns ta
    81:         )
    82:     end
    83:   | `BTYP_var (i,mt) ->
    84:     (*
    85:     print_endline ("Type variable " ^ si i^ " has encoded meta type " ^ sbt syms.dfns mt);
    86:     (
    87:       try
    88:         let symdef = Hashtbl.find syms.dfns i in begin match symdef with
    89:         | {symdef=`SYMDEF_typevar mt} -> print_endline ("Table shows metatype is " ^ string_of_typecode mt);
    90:         | _ -> print_endline "Type variable isn't a type variable?"
    91:         end
    92:       with Not_found -> print_endline "Cannot find type variable in symbol table"
    93:     );
    94:     *)
    95:     mt
    96: 
    97:   | `BTYP_type i -> `BTYP_type (i+1)
    98:   | `BTYP_inst (index,ts) ->
    99:     let {id=id; symdef=entry} =
   100:       try Hashtbl.find syms.dfns index
   101:       with Not_found -> failwith ("[metatype'] can't find type instance index " ^ si index)
   102:     in
   103:     (*
   104:     print_endline ("Yup .. instance id=" ^ id);
   105:     *)
   106: 
   107:     (* this is hacked: we should really bind the types and take
   108:       the metatype of them but we don't have access to the
   109:       bind type routine due to module factoring .. we could pass
   110:       in the bind-type routine as an argument .. yuck ..
   111:     *)
   112:     begin match entry with
   113:     | `SYMDEF_nonconst_ctor (_,ut,_,_,argt) ->
   114:       `BTYP_function (`BTYP_type 0,`BTYP_type 0)
   115: 
   116:     | `SYMDEF_const_ctor (_,t,_,_) ->
   117:       `BTYP_type 0
   118: 
   119:     | `SYMDEF_abs _ -> `BTYP_type 0
   120: 
   121:     | _ ->  clierr sr ("Unexpected argument to metatype: " ^ sbt syms.dfns term)
   122:     end
   123: 
   124: 
   125:   | _ ->
   126:      print_endline ("Questionable meta typing of term: " ^ sbt syms.dfns term);
   127:      `BTYP_type 0 (* THIS ISN'T RIGHT *)
   128: 
   129: 
   130: 
   131: (* fixpoint reduction: reduce
   132:    Fix f. Lam x. e ==> Lam x. Fix z. e [f x -> z]
   133:    to replace a recursive function
   134:    with a recursive data structure.
   135: 
   136:    Example: consider:
   137: 
   138:    list t = t * list t
   139: 
   140:    which is
   141: 
   142:    list = fix f. lam t. t * f t
   143: 
   144:    We can apply list to int:
   145: 
   146:    list int = (fix f. lam t. t * f t) int
   147: 
   148:    unfolding:
   149: 
   150:    list int = (lam t. t * (fix f. lam t. t * f t)) int
   151:             = int * (fix f. lam t. t * f t) int
   152:             = int * list int
   153: 
   154:    which is just
   155: 
   156:    list int = fix z. int * z
   157: 
   158:   The rule ONLY works when a recursive function f
   159:   is applied in its own definition to its own parameter.
   160: 
   161:   The rule traps in infinite expansion of a data type,
   162:   and creates instead an recursive data type, eliminating
   163:   the function.
   164: 
   165:   The normal beta reduction rule is
   166: 
   167:   (lam t. b) a => b [t->a]
   168: 
   169:   For a recursive function:
   170: 
   171:   (fix f. lam t. b) a => b[f-> fix f. lam t. b; t-> a]
   172: 
   173:   and the result must be reduced again.
   174: 
   175: *)
   176: 
   177: and fixup syms ps body =
   178:  let param = match ps with
   179:    | [] -> assert false
   180:    | [i,mt] -> `BTYP_var (i,mt)
   181:    | x -> `BTYP_type_tuple (List.map (fun (i,mt) -> `BTYP_var (i,mt)) x)
   182:  in
   183:  (*
   184:  print_endline ("Body  = " ^ sbt syms.dfns body);
   185:  print_endline ("Param = " ^ sbt syms.dfns param);
   186:  *)
   187:  let rec aux term depth =
   188:    let fx t = aux t (depth+1) in
   189:    match map_btype fx term with
   190:    | `BTYP_apply (`BTYP_fix i, arg)
   191:      when arg = param
   192:      && i + depth +1  = 0 (* looking inside application, one more level *)
   193:      -> print_endline "SPECIAL REDUCTION";
   194:      `BTYP_fix (i+2) (* elide application AND skip under lambda abstraction *)
   195: 
   196:    | `BTYP_typefun (a,b,c) ->
   197:       (* NOTE we have to add 2 to depth here, an extra
   198:       level for the lambda binder.
   199:       NOTE also: this is NOT a recusive call to fixup!
   200:       It doesn't fixup this function.
   201:       *)
   202: 
   203:       `BTYP_typefun (a, fx b, aux c (depth + 2))
   204:    | x -> x
   205:  in
   206:    (* note depth 1: we seek a fix to an abstraction
   207:    of which we're given only the body, that's an
   208:    extra level in the term structure
   209:    *)
   210:    aux body 1
   211: 
   212: (* generic fixpoint adjuster: add amt to the fixpoint
   213:    to make it span less deep term, to compensate
   214:    for removing the top combinator of the term as a result
   215:    of a one level adjustment eg: reduce a type match
   216: *)
   217: 
   218: and adjust t =
   219:   let rec adj depth t =
   220:     let fx t = adj (depth + 1) t in
   221:     match map_btype fx t with
   222:     | `BTYP_fix i when i + depth < 0 -> `BTYP_fix (i+1)
   223:     | x -> x
   224:   in adj 0 t
   225: 
   226: and mk_prim_type_inst syms i args =
   227:   print_endline "MK_PRIM_TYPE";
   228:   let t = `BTYP_inst (i,args) in
   229:   (*
   230:   let _,t' = normalise_type t in
   231:   let args = match t' with
   232:     | `BTYP_inst (_,args) -> args
   233:     | _ -> assert false
   234:   in
   235:   if not (Hashtbl.mem syms.prim_inst (i,args))
   236:   then begin
   237:     let n = !(syms.counter) in
   238:     incr (syms.counter);
   239:     Hashtbl.add syms.prim_inst (i, args) n;
   240:     Hashtbl.add syms.rev_prim_inst n (i, args)
   241:   end;
   242:   *)
   243:   t
   244: 
   245: 
   246: and beta_reduce syms sr t1 =
   247:   (*
   248:   print_endline ("---------- Beta reduce " ^ sbt syms.dfns t1);
   249:   *)
   250:   let t2 =
   251:   try
   252:   beta_reduce' syms sr [] t1
   253:   with Failure s -> failwith ("beta-reduce failed in " ^ sbt syms.dfns t1 ^ "msg: " ^ s)
   254:   in
   255:   (*
   256:   print_endline ("============  reduced= " ^ sbt syms.dfns t2);
   257:   if t1 <> t2 then print_endline "!!!!!!!!!!!! CHANGED";
   258:   *)
   259:   t2
   260: 
   261: and beta_reduce' syms sr termlist t =
   262:   (*
   263:   print_endline (spc ^ "BETA REDUCE " ^ string_of_btypecode syms.dfns t);
   264:   *)
   265:   match list_index termlist t with
   266:   | Some j ->
   267:         (*
   268:         print_endline "+++Trail:";
   269:         let i = ref 0 in
   270:         iter (fun t -> print_endline (
   271:           "    " ^ si (!i) ^ " ---> " ^sbt syms.dfns t)
   272:           ; decr i
   273:         )
   274:         (t::termlist)
   275:         ;
   276:         print_endline "++++End";
   277:     print_endline ("Beta find fixpoint " ^ si (-j-1));
   278:     print_endline ("Repeated term " ^ sbt syms.dfns t);
   279:     *)
   280:     `BTYP_fix (-j - 1)
   281: 
   282:   | None ->
   283: 
   284:   let br t' = beta_reduce' syms sr (t::termlist) t' in
   285:   let st t = string_of_btypecode syms.dfns t in
   286:   let mt t = metatype syms sr t in
   287:   match t with
   288:   | `BTYP_lift t -> `BTYP_lift (br t)
   289:   | `BTYP_fix _ -> t
   290:   | `BTYP_var (i,_) -> t
   291: 
   292:   | `BTYP_typefun (p,r,b) ->
   293:     let b = fixup syms p b in
   294:     let b' = beta_reduce' syms sr (t::termlist) b in
   295:     let t = `BTYP_typefun (p, br r, b') in
   296:     t
   297: 
   298:   | `BTYP_inst (i,ts) ->
   299:     let ts = map br ts in
   300:     begin try match Hashtbl.find syms.dfns i with
   301:     | {id=id; symdef=`SYMDEF_type_alias _ } ->
   302:       failwith ("Beta reduce found a type instance of "^id^" to be an alias, which it can't handle")
   303:     | _ -> `BTYP_inst (i,ts)
   304:     with Not_found -> `BTYP_inst (i,ts) (* could be reparented class *)
   305:     end
   306: 
   307:   | `BTYP_case (a,b,c) -> `BTYP_case (br a, b, br c)
   308:   | `BTYP_tuple ls -> `BTYP_tuple (map br ls)
   309:   | `BTYP_array (i,t) -> `BTYP_array (i, br t)
   310:   | `BTYP_sum ls -> `BTYP_sum (map br ls)
   311:   | `BTYP_record ts ->
   312:      let ss,ls = split ts in
   313:      `BTYP_record (combine ss (map br ls))
   314: 
   315:   | `BTYP_variant ts ->
   316:      let ss,ls = split ts in
   317:      `BTYP_variant (combine ss (map br ls))
   318: 
   319:   (* Intersection type reduction rule: if any term is 0,
   320:      the result is 0, otherwise the result is the intersection
   321:      of the reduced terms with 1 terms removed: if there
   322:      are no terms return 1, if a single term return it,
   323:      otherwise return the intersection of non units
   324:      (at least two)
   325:   *)
   326:   | `BTYP_intersect ls ->
   327:     let ls = map br ls in
   328:     if mem `BTYP_void ls then `BTYP_void
   329:     else let ls = filter (fun i -> i <> `BTYP_tuple []) ls in
   330:     begin match ls with
   331:     | [] -> `BTYP_tuple []
   332:     | [t] -> t
   333:     | ls -> `BTYP_intersect ls
   334:     end
   335: 
   336:   | `BTYP_typeset ls -> `BTYP_typeset (map br ls)
   337: 
   338:   | `BTYP_typesetunion ls ->
   339:     let ls = rev_map br ls in
   340:     (* split into explicit typesets and other terms
   341:       at the moment, there shouldn't be any 'other'
   342:       terms (since there are no typeset variables ..
   343:     *)
   344:     let rec aux ts ot ls  = match ls with
   345:     | [] ->
   346:       begin match ot with
   347:       | [] -> `BTYP_typeset ts
   348:       | _ ->
   349:         (*
   350:         print_endline "WARNING UNREDUCED TYPESET UNION";
   351:         *)
   352:         `BTYP_typesetunion (`BTYP_typeset ts :: ot)
   353:       end
   354: 
   355:     | `BTYP_typeset xs :: t -> aux (xs @ ts) ot t
   356:     | h :: t -> aux ts (h :: ot) t
   357:     in aux [] [] ls
   358: 
   359:   (* NOTE: sets have no unique unit *)
   360:   (* WARNING: this representation is dangerous:
   361:      we can only calculate the real intersection
   362:      of discrete types *without type variables*
   363: 
   364:      If there are pattern variables, we may be able
   365:      to apply unification as a reduction. However
   366:      we have to be very careful doing that: we can't
   367:      unify variables bound by universal or lambda quantifiers
   368:      or the environment: technically I think we can only
   369:      unify existentials. For example the intersection
   370: 
   371:      'a * int & long & 'b
   372: 
   373:      may seem to be long * int, but only if 'a and 'b are
   374:      pattern variables, i.e. dependent variables we're allowed
   375:      to assign. If they're actually function parameters, or
   376:      just names for types in the environment, we have to stop
   377:      the unification algorithm from assigning them (since they're
   378:      actually particular constants at that point).
   379: 
   380:      but the beta-reduction can be applied anywhere .. so I'm
   381:      not at all confident of the right reduction rule yet.
   382: 
   383:      Bottom line: the rule below is a hack.
   384:   *)
   385:   | `BTYP_typesetintersection ls ->
   386:     let ls = map br ls in
   387:     if mem (`BTYP_typeset []) ls then `BTYP_typeset []
   388:     else begin match ls with
   389:     | [t] -> t
   390:     | ls -> `BTYP_typesetintersection ls
   391:     end
   392: 
   393: 
   394:   | `BTYP_type_tuple ls -> `BTYP_type_tuple (map br ls)
   395:   | `BTYP_function (a,b) -> `BTYP_function (br a, br b)
   396:   | `BTYP_cfunction (a,b) -> `BTYP_cfunction (br a, br b)
   397:   | `BTYP_pointer a -> `BTYP_pointer (br a)
   398:   | `BTYP_lvalue a -> `BTYP_lvalue (br a)
   399: 
   400:   | `BTYP_void -> t
   401:   | `BTYP_type _ -> t
   402:   | `BTYP_unitsum _ -> t
   403: 
   404:   | `BTYP_apply (t1,t2) ->
   405:     let t1 = br t1 in (* eager evaluation *)
   406:     let t2 = br t2 in (* eager evaluation *)
   407:     let t1 =
   408:       match t1 with
   409:       | `BTYP_fix j ->
   410:         (*
   411:         print_endline ("++++Fixpoint application " ^ si j);
   412:         print_endline "+++Trail:";
   413:         let i = ref 0 in
   414:         iter (fun t -> print_endline (
   415:           "    " ^ si (!i) ^ " ---> " ^sbt syms.dfns t)
   416:           ; decr i
   417:         )
   418:         (t1::t::termlist)
   419:         ;
   420:         print_endline "++++End";
   421:         *)
   422:         let whole = nth termlist (-2-j) in
   423:         (*
   424:         print_endline ("Recfun = " ^ sbt syms.dfns whole);
   425:         *)
   426:         begin match whole with
   427:         | `BTYP_typefun _ -> ()
   428:         | _ -> assert false
   429:         end;
   430:         whole
   431: 
   432:       | _ -> t1
   433:     in
   434:     (*
   435:     print_endline ("Function = " ^ sbt syms.dfns t1);
   436:     print_endline ("Argument = " ^ sbt syms.dfns t2);
   437:     print_endline ("Unfolded = " ^ sbt syms.dfns (unfold syms.dfns t1));
   438:     *)
   439:     begin match unfold syms.dfns t1 with
   440:     | `BTYP_typefun (ps,r,body) ->
   441:       let params' =
   442:         match ps with
   443:         | [] -> []
   444:         | [i,_] -> [i,t2]
   445:         | _ ->
   446:           let ts = match t2 with
   447:           | `BTYP_type_tuple ts -> ts
   448:           | _ -> assert false
   449:           in
   450:             if List.length ps <> List.length ts
   451:             then failwith "Wrong number of arguments to typefun"
   452:             else List.map2 (fun (i,_) t -> i, t) ps ts
   453:       in
   454:       (*
   455:       print_endline ("Body before subs" ^ sbt syms.dfns body);
   456:       *)
   457:       let t' = list_subst params' body in
   458:       (*
   459:       print_endline ("Body after subs" ^ sbt syms.dfns t');
   460:       *)
   461:       let t' = beta_reduce' syms sr (t::termlist) t' in
   462:       (*
   463:       print_endline ("Body after reduction" ^ sbt syms.dfns t');
   464:       *)
   465:       let t' = adjust t' in
   466:       t'
   467: 
   468:     | _ ->
   469:       (*
   470:       print_endline "Apply nonfunction .. can't reduce";
   471:       *)
   472:       `BTYP_apply (t1,t2)
   473:     end
   474: 
   475:   | `BTYP_type_match (tt,pts) ->
   476:     (*
   477:     print_endline ("Typematch [before reduction] " ^ sbt syms.dfns t);
   478:     *)
   479:     let tt = br tt in
   480:     let new_matches = ref [] in
   481:     iter (fun ({pattern=p; pattern_vars=dvars; assignments=eqns}, t') ->
   482:       (*
   483:       print_endline (spc ^"Tring to unify argument with " ^ sbt syms.dfns p');
   484:       *)
   485:       let p =  br p in
   486:       let x =
   487:         {
   488:           pattern=p;
   489:           assignments= map (fun (j,t) -> j, br t) eqns;
   490:           pattern_vars=dvars;
   491:         }, t'
   492:       in
   493:       match maybe_unification syms.dfns [p,tt] with
   494:       | Some _ -> new_matches := x :: !new_matches
   495:       | None ->
   496:         (*
   497:         print_endline (spc ^"Discarding pattern " ^ sbt syms.dfns p');
   498:         *)
   499:         ()
   500:     )
   501:     pts
   502:     ;
   503:     let pts = rev !new_matches in
   504:     match pts with
   505:     | [] ->
   506:       failwith "[beta-reduce] typematch failure"
   507:     | ({pattern=p';pattern_vars=dvars;assignments=eqns},t') :: _ ->
   508:       try
   509:         let mgu = unification false syms.dfns [p', tt] dvars in
   510:         (*
   511:         print_endline "Typematch success";
   512:         *)
   513:         let t' = list_subst (mgu @ eqns) t' in
   514:         let t' = br t' in
   515:         (*
   516:         print_endline ("type match reduction result=" ^ sbt syms.dfns t');
   517:         *)
   518:         adjust t'
   519:       with Not_found -> `BTYP_type_match (tt,pts)
   520: 
End ocaml section to src/flx_beta.ml[1]
Start ocaml section to src/flx_tpat.mli[1 /1 ]
     1: # 3 "./lpsrc/flx_tpat.ipk"
     2: open Flx_ast
     3: open Flx_types
     4: open Flx_mtypes2
     5: 
     6: (*
     7: val type_of_tpattern:
     8:   sym_state_t -> tpattern_t ->
     9:   typecode_t *
    10:   (int * string) list *     (* variables for '?' terms *)
    11:   int list *                (* variables for 'any' terms *)
    12:   (int * string) list *     (* variables for 'as' terms *)
    13:   (int * typecode_t) list   (* variables for as terms *)
    14: *)
    15: 
    16: val type_of_tpattern:
    17:   sym_state_t -> typecode_t ->
    18:   typecode_t *
    19:   (int * string) list *     (* variables for '?' terms *)
    20:   int list *                (* variables for 'any' terms *)
    21:   (int * string) list *     (* variables for 'as' terms *)
    22:   (int * typecode_t) list   (* variables for as terms *)
    23: 
End ocaml section to src/flx_tpat.mli[1]
Start ocaml section to src/flx_tpat.ml[1 /1 ]
     1: # 27 "./lpsrc/flx_tpat.ipk"
     2: open Flx_ast
     3: open List
     4: open Flx_mtypes2
     5: open Flx_maps
     6: 
     7: (*
     8: let type_of_tpattern syms p :
     9:   typecode_t *
    10:   (int * string) list *     (* variables for '?' terms *)
    11:   int list *                (* variables for 'any' terms *)
    12:   (int * string) list *     (* variables for 'as' terms *)
    13:   (int * typecode_t) list   (* assignments for as terms *)
    14: =
    15:   let sr = "unk",0,0,0,0 in
    16:   let explicit_vars = ref [] in
    17:   let any_vars = ref [] in
    18:   let as_vars = ref [] in
    19:   let eqns = ref [] in
    20:   let rec tp p =
    21:     match p with
    22:     | `TPAT_function (a,b) -> `TYP_function (tp a, tp b)
    23:     | `TPAT_tuple ps -> `TYP_tuple (map tp ps)
    24:     | `TPAT_sum ps -> `TYP_sum (map tp ps)
    25:     | `TPAT_pointer p -> `TYP_pointer (tp p)
    26:     | `TPAT_name (n,ps) -> `AST_name (sr,n,map tp ps)
    27:     | `TPAT_void -> `AST_void sr
    28: 
    29:     | `TPAT_var n ->
    30:       let j = !(syms.counter) in
    31:       incr (syms.counter);
    32:       explicit_vars := (j,n) :: !explicit_vars;
    33:       `TYP_var j
    34: 
    35:     | `TPAT_any ->
    36:       let j = !(syms.counter) in
    37:       incr (syms.counter);
    38:       any_vars := j :: !any_vars;
    39:       `TYP_var j
    40: 
    41:     | `TPAT_as (t,n) ->
    42:       let t = tp t in
    43:       let j = !(syms.counter) in
    44:       incr (syms.counter);
    45:       as_vars := (j,n) :: !as_vars;
    46:       eqns := (j,t) :: !eqns;
    47:       t
    48: 
    49:     | `TPAT_unitsum j -> `TYP_unitsum j
    50:     | `TPAT_type_tuple ts -> `TYP_type_tuple (map tp ts)
    51:   in
    52:     let t = tp p in
    53:     t,!explicit_vars, !any_vars, !as_vars, !eqns
    54: 
    55: *)
    56: let type_of_tpattern syms p :
    57:   typecode_t *
    58:   (int * string) list *     (* variables for '?' terms *)
    59:   int list *                (* variables for 'any' terms *)
    60:   (int * string) list *     (* variables for 'as' terms *)
    61:   (int * typecode_t) list   (* assignments for as terms *)
    62: =
    63:   let sr = "unk",0,0,0,0 in
    64:   let explicit_vars = ref [] in
    65:   let any_vars = ref [] in
    66:   let as_vars = ref [] in
    67:   let eqns = ref [] in
    68: 
    69:   let rec tp p = match map_type tp p with
    70:     | `AST_patvar (sr,n) ->
    71:       let j = !(syms.counter) in
    72:       incr (syms.counter);
    73:       explicit_vars := (j,n) :: !explicit_vars;
    74:       `TYP_var j
    75: 
    76:     | `AST_patany _ ->
    77:       let j = !(syms.counter) in
    78:       incr (syms.counter);
    79:       any_vars := j :: !any_vars;
    80:       `TYP_var j
    81: 
    82:     (* NOTE CONFUSION! Is this a pattern assignment,
    83:        or is it fixpoint binder? Or is this the
    84:        same thing ..?
    85: 
    86:        Treated here as pattern assignment.
    87: 
    88:        1 + int * list as list => list
    89:     *)
    90:     | `TYP_as (t,n) ->
    91:       let t = tp t in
    92:       let j = !(syms.counter) in
    93:       incr (syms.counter);
    94:       as_vars := (j,n) :: !as_vars;
    95:       eqns := (j,t) :: !eqns;
    96:       t
    97: 
    98:     | x -> x
    99:   in
   100:     let t = tp p in
   101:     t,!explicit_vars, !any_vars, !as_vars, !eqns
   102: 
   103: 
End ocaml section to src/flx_tpat.ml[1]