5.33. 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: 
     5: val metatype:
     6:   sym_state_t ->
     7:   (int * btypecode_t) list ->
     8:   btypecode_t ->
     9:   btypecode_t
    10: 
    11: val beta_reduce:
    12:   sym_state_t ->
    13:   (int * btypecode_t) list ->
    14:   btypecode_t ->
    15:   btypecode_t
    16: 
End ocaml section to src/flx_beta.mli[1]
Start ocaml section to src/flx_beta.ml[1 /1 ]
     1: # 21 "./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: (* params is list of string * bound_typecode *)
    19: let rec metatype syms (params:(int * btypecode_t) list) term =
    20:   (*
    21:   print_endline ("Find Metatype  of: " ^ string_of_btypecode syms.dfns term);
    22:   *)
    23:   let t = metatype' syms params term in
    24:   (*
    25:   print_endline "Done";
    26:   *)
    27:   t
    28: 
    29: and metatype' syms (params:(int * btypecode_t) list) term =
    30:   let st t = string_of_btypecode syms.dfns t in
    31:   let mt t = metatype' syms params t in
    32:   match term with
    33:   | `BTYP_typefun (a,b,c) ->
    34:     let ps = List.map snd a in
    35:     let argt =
    36:       match ps with
    37:       | [x] -> x
    38:       | _ -> `BTYP_tuple ps
    39:     in
    40:       let rt = metatype syms (a @ params) c in
    41:       if b<>rt
    42:       then
    43:         failwith
    44:         (
    45:           "In abstraction\n" ^
    46:           st term ^
    47:           "\nFunction body metatype \n"^
    48:           st rt^
    49:           "\ndoesn't agree with declared type \n" ^
    50:           st b
    51:         )
    52:       else `BTYP_function (argt,b)
    53: 
    54:   | `BTYP_type_tuple ts ->
    55:     `BTYP_tuple (List.map (metatype syms params) ts)
    56: 
    57:   | `BTYP_apply (a,b) ->
    58:     begin
    59:       let ta = mt a
    60:       and tb = mt b
    61:       in match ta with
    62:       | `BTYP_function (x,y) ->
    63:         if x = tb then y
    64:         else
    65:           failwith "Metatype error: function argument wrong metatype"
    66:       | _ -> failwith "Metatype error: function required for LHS of application"
    67:     end
    68:   | `BTYP_var (i,mt) ->  mt
    69:     (*
    70:     begin try
    71:       List.assoc i params
    72:       with
    73:         Not_found ->
    74:           print_endline "assoc list = ";
    75:           List.iter
    76:           (fun (i,s) ->
    77:             print_string
    78:             (
    79:               string_of_int i ^
    80:               ": " ^
    81:               string_of_btypecode syms.dfns s ^
    82:               " "
    83:             )
    84:           )
    85:           params
    86:           ;
    87:           print_endline "";
    88:           failwith
    89:           (
    90:             "[metatype] Type variable " ^ string_of_int i ^ " not found in generic assoc list"
    91:           )
    92:     end
    93:     *)
    94: 
    95:   | _ -> `BTYP_type (* THIS ISN'T RIGHT *)
    96: 
    97: 
    98: 
    99: (* fixpoint reduction: reduce
   100:    Fix f. Lam x. e ==> Lam x. Fix z. e [f x -> z]
   101:    to replace a recursive function
   102:    with a recursive data structure
   103: *)
   104: 
   105: and fixup syms ps body =
   106:  let param = match ps with
   107:    | [] -> assert false
   108:    | [i,mt] -> `BTYP_var (i,mt)
   109:    | x -> `BTYP_type_tuple (List.map (fun (i,mt) -> `BTYP_var (i,mt)) x)
   110:  in
   111:  (*
   112:  print_endline ("Body  = " ^ sbt syms.dfns body);
   113:  print_endline ("Param = " ^ sbt syms.dfns param);
   114:  *)
   115:  let rec aux term depth =
   116:    let fx t = aux t (depth+1) in
   117:    match map_btype fx term with
   118:    | `BTYP_apply (`BTYP_fix i, arg)
   119:      when arg = param
   120:      && i + depth +1  = 0 (* looking inside application, one more level *)
   121:      -> `BTYP_fix (i+2) (* elide application AND skip under lambda abstraction *)
   122: 
   123:    | `BTYP_typefun (a,b,c) ->
   124:       (* NOTE we have to add 2 to depth here, an extra
   125:       level for the lambda binder.
   126:       NOTE also: this is NOT a recusive call to fixup!
   127:       It doesn't fixup this function.
   128:       *)
   129: 
   130:       `BTYP_typefun (a, fx b, aux c (depth + 2))
   131:    | x -> x
   132:  in
   133:    (* note depth 1: we seek a fix to an abstraction
   134:    of which we're given only the body, that's an
   135:    extra level in the term structure
   136:    *)
   137:    aux body 1
   138: 
   139: and mk_prim_type_inst syms i args =
   140:   print_endline "MK_PRIM_TYPE";
   141:   let t = `BTYP_inst (i,args) in
   142:   (*
   143:   let _,t' = normalise_type t in
   144:   let args = match t' with
   145:     | `BTYP_inst (_,args) -> args
   146:     | _ -> assert false
   147:   in
   148:   if not (Hashtbl.mem syms.prim_inst (i,args))
   149:   then begin
   150:     let n = !(syms.counter) in
   151:     incr (syms.counter);
   152:     Hashtbl.add syms.prim_inst (i, args) n;
   153:     Hashtbl.add syms.rev_prim_inst n (i, args)
   154:   end;
   155:   *)
   156:   t
   157: 
   158: 
   159: and beta_reduce syms (btvars:(int * btypecode_t) list) t =
   160:   (*
   161:   print_endline ("Beta reduce " ^ sbt syms.dfns t);
   162:   *)
   163:   let t =
   164:   try
   165:   beta_reduce' syms btvars [] t
   166:   with Failure s -> failwith ("beta-reduce failed in " ^ sbt syms.dfns t ^ "msg: " ^ s)
   167:   in
   168:   (*
   169:   print_endline ("  reduced= " ^ sbt syms.dfns t);
   170:   *)
   171:   t
   172: 
   173: and beta_reduce' syms (btvars:(int * btypecode_t) list) termlist t =
   174:   (*
   175:   print_endline ("BETA REDUCE " ^ string_of_btypecode syms.dfns t);
   176:   *)
   177:   match list_index termlist t with
   178:   | Some i -> print_endline ("Beta find fixpoint " ^ si (-i-1)); `BTYP_fix (-i - 1)
   179:   | None ->
   180:   let br t' = beta_reduce' syms btvars (t::termlist) t' in
   181:   let st t = string_of_btypecode syms.dfns t in
   182:   let mt t = metatype syms btvars t in
   183:   (* hhmm .. this has to handle a free fixpoint, because it
   184:   is called during construction of a recursive type .. so
   185:   we can't do an unfold.. but them beta-reduce won't
   186:   find fix points .. hmm .. hmm .. we could fix that by
   187:   replacing a fixpoint with a copy of the recursed expression ..
   188:   then let beta-reduce find it..
   189:   *)
   190:   match t with
   191:   | `BTYP_inst (i,ts) ->
   192:     let ts = map br ts in
   193:     begin try match Hashtbl.find syms.dfns i with
   194:     | {id=id; symdef=`SYMDEF_type_alias _ } ->
   195:       failwith ("Beta reduce found a type instance of "^id^" to be an alias, which it can't handle")
   196:     | _ -> `BTYP_inst (i,ts)
   197:     with Not_found -> `BTYP_inst (i,ts) (* could be reparented class *)
   198:     end
   199:   | `BTYP_tuple ls -> `BTYP_tuple (map br ls)
   200:   | `BTYP_array (i,t) -> `BTYP_array (i, br t)
   201:   | `BTYP_sum ls -> `BTYP_sum (map br ls)
   202:   | `BTYP_record ts ->
   203:      let ss,ls = split ts in
   204:      `BTYP_record (combine ss (map br ls))
   205: 
   206:   | `BTYP_variant ts ->
   207:      let ss,ls = split ts in
   208:      `BTYP_variant (combine ss (map br ls))
   209: 
   210:   (* Intersection type reduction rule: if any term is 0,
   211:      the result is 0, otherwise the result is the intersection
   212:      of the reduced terms with 1 terms removed: if there
   213:      are no terms return 1, if a single term return it,
   214:      otherwise return the intersection of non units
   215:      (at least two)
   216:   *)
   217:   | `BTYP_intersect ls ->
   218:     let ls = map br ls in
   219:     if mem `BTYP_void ls then `BTYP_void
   220:     else let ls = filter (fun i -> i <> `BTYP_tuple []) ls in
   221:     begin match ls with
   222:     | [] -> `BTYP_tuple []
   223:     | [t] -> t
   224:     | ls -> `BTYP_intersect ls
   225:     end
   226: 
   227:   | `BTYP_typeset ls -> `BTYP_typeset (map br ls)
   228: 
   229:   | `BTYP_typesetunion ls ->
   230:     let ls = rev_map br ls in
   231:     (* split into explicit typesets and other terms
   232:       at the moment, there shouldn't be any 'other'
   233:       terms (since there are no typeset variables ..
   234:     *)
   235:     let rec aux ts ot ls  = match ls with
   236:     | [] ->
   237:       begin match ot with
   238:       | [] -> `BTYP_typeset ts
   239:       | _ ->
   240:         print_endline "WARNING UNREDUCED TYPESET UNION";
   241:         `BTYP_typesetunion (`BTYP_typeset ts :: ot)
   242:       end
   243: 
   244:     | `BTYP_typeset xs :: t -> aux (xs @ ts) ot t
   245:     | h :: t -> aux ts (h :: ot) t
   246:     in aux [] [] ls
   247: 
   248:   (* NOTE: sets have no unique unit *)
   249:   (* WARNING: this representation is dangerous:
   250:      we can only calculate the real intersection
   251:      of discrete types *without type variables*
   252: 
   253:      If there are pattern variables, we may be able
   254:      to apply unification as a reduction. However
   255:      we have to be very careful doing that: we can't
   256:      unify variables bound by universal or lambda quantifiers
   257:      or the environment: technically I think we can only
   258:      unify existentials. For example the intersection
   259: 
   260:      'a * int & long & 'b
   261: 
   262:      may seem to be long * int, but only if 'a and 'b are
   263:      pattern variables, i.e. dependent variables we're allowed
   264:      to assign. If they're actually function parameters, or
   265:      just names for types in the environment, we have to stop
   266:      the unification algorithm from assigning them (since they're
   267:      actually particular constants at that point).
   268: 
   269:      but the beta-reduction can be applied anywhere .. so I'm
   270:      not at all confident of the right reduction rule yet.
   271: 
   272:      Bottom line: the rule below is a hack.
   273:   *)
   274:   | `BTYP_typesetintersection ls ->
   275:     let ls = map br ls in
   276:     if mem (`BTYP_typeset []) ls then `BTYP_typeset []
   277:     else begin match ls with
   278:     | [t] -> t
   279:     | ls -> `BTYP_typesetintersection ls
   280:     end
   281: 
   282: 
   283:   | `BTYP_type_tuple ls -> `BTYP_type_tuple (map br ls)
   284:   | `BTYP_function (a,b) -> `BTYP_function (br a, br b)
   285:   | `BTYP_cfunction (a,b) -> `BTYP_cfunction (br a, br b)
   286:   | `BTYP_pointer a -> `BTYP_pointer (br a)
   287:   | `BTYP_lvalue a -> `BTYP_lvalue (br a)
   288: 
   289:   | `BTYP_void -> t
   290:   | `BTYP_type -> t
   291:   | `BTYP_fix _ -> t
   292:   | `BTYP_var _ -> t
   293:   | `BTYP_unitsum _ -> t
   294: 
   295:   | `BTYP_apply (t1,t2) ->
   296:     (*
   297:     print_endline "-----------------------";
   298:     print_endline ("Application " ^ st t);
   299:     print_endline "";
   300:     print_endline ("Unreduced function is " ^ st t1);
   301:     print_endline ("Unreduced Argument is " ^ st t2);
   302:     *)
   303:     let t2 = br t2 in (* eager evaluation *)
   304:     let t1 = br t1 in (* eager evaluation *)
   305:     (*
   306:     print_endline ("reduced function is " ^ st t1);
   307:     print_endline ("reduced Argument is " ^ st t2);
   308:     *)
   309:     let mt1 = mt t1
   310:     and mt2 = mt t2
   311:     in
   312:     (*
   313:     print_endline ("Function metatype is" ^ st mt1);
   314:     print_endline ("Argument metatype is" ^ st mt2);
   315:     *)
   316:     begin match t1 with
   317:     | `BTYP_fix _ -> `BTYP_apply(t1,t2)
   318:     | _ ->
   319:     begin match mt1 with
   320:     | `BTYP_function (a,b) ->
   321:       if a <> mt2
   322:       then failwith ("Argument metatype not same as function parameter")
   323:     | _ ->
   324:       failwith (
   325:         "[beta_reduce] Expected LHS of application to be type function, got\n" ^
   326:         st t1^"\nmeta type: " ^ st mt1
   327:       )
   328:     end
   329:     ;
   330:     begin match t1 with
   331:     | `BTYP_typefun (ps,r,body) ->
   332:       let v = Hashtbl.create 97 in
   333:       begin match ps with
   334:       | [] -> ()
   335:       | [i,_] -> Hashtbl.add v i t2
   336:       | _ ->
   337:         let ts = match t2 with
   338:         | `BTYP_type_tuple ts -> ts
   339:         | _ -> assert false
   340:         in
   341:           if List.length ps <> List.length ts
   342:           then failwith "Wrong number of arguments to typefun"
   343:           else List.iter2 (fun (i,_) y -> Hashtbl.add v i y) ps ts
   344:       end
   345:       ;
   346:       (*
   347:       print_endline "Variable assignments are ";
   348:       Hashtbl.iter
   349:       (fun i t -> print_endline (string_of_int i ^ " -> " ^ st t))
   350:       v
   351:       ;
   352:       print_endline ("Body is " ^ st body);
   353:       *)
   354:       let t = varmap_subst v body in
   355:       (*
   356:       print_endline ("Result of application = " ^ st t);
   357:       *)
   358:       br t
   359: 
   360:     | `BTYP_var _ -> t (* can't reduce it yet *)
   361:     | `BTYP_fix _ -> t (* can't reduce it yet *)
   362: 
   363:     | _ -> failwith
   364:       (
   365:         "[beta-reduce] Expected type function or variable, got " ^
   366:         string_of_btypecode syms.dfns t1
   367:       )
   368:     end
   369:     end
   370: 
   371:   | `BTYP_typefun (p,r,b) ->
   372:     let p' = List.map (fun (i,t) -> (i, br t)) p in
   373:     (*
   374:     print_endline ("fixing up function " ^ st t);
   375:     *)
   376:     (*
   377:     print_endline ("body is " ^ st b);
   378:     *)
   379:     let b = fixup syms p b in
   380:     (*
   381:     print_endline ("After fixup body is " ^ st b);
   382:     *)
   383:     let b' = beta_reduce syms (p' @ btvars) b in
   384:     (*
   385:     print_endline ("Reducing body inside lambda, result is" ^ sbt syms.dfns b');
   386:     *)
   387:     `BTYP_typefun (p', br r, b')
   388: 
   389:   | `BTYP_type_match (tt,pts) ->
   390:     (*
   391:     print_endline ("Typematch [before reduction] " ^ sbt syms.dfns t);
   392:     *)
   393:     let tt = br tt in
   394:     let pts =
   395:       map (fun (tp,t) ->
   396:         {
   397:           tp with pattern=br tp.pattern;
   398:            assignments= map (fun (j,t) -> j, br t) tp.assignments
   399:          }, br t
   400:       )
   401:       pts
   402:     in
   403:     (*
   404:     let xx = `BTYP_type_match (tt,pts) in
   405:     print_endline ("Typematch [after reduction] " ^ sbt syms.dfns xx);
   406:     *)
   407:     let new_matches = ref [] in
   408:     iter (fun (({pattern=p'; pattern_vars=dvars; assignments=eqns}, t') as x) ->
   409:       (*
   410:       print_endline ("Tring to unify argument with " ^ sbt syms.dfns p');
   411:       *)
   412:       match maybe_unification syms.dfns [p',tt] with
   413:       | Some _ -> new_matches := x :: !new_matches
   414:       | None ->
   415:         (*
   416:         print_endline ("Discarding pattern " ^ sbt syms.dfns p');
   417:         *)
   418:         ()
   419:     )
   420:     pts
   421:     ;
   422:     let pts = rev !new_matches in
   423:     match pts with
   424:     | [] ->
   425:       failwith "[beta-reduce] typematch failure"
   426:     | ({pattern=p';pattern_vars=dvars;assignments=eqns},t') :: _ ->
   427:       try
   428:         let mgu = unification false syms.dfns [p', tt] dvars in
   429:         let t' = list_subst eqns t' in
   430:         list_subst mgu t'
   431:       with Not_found -> `BTYP_type_match (tt,pts)
   432: 
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: val type_of_tpattern:
     7:   sym_state_t -> tpattern_t ->
     8:   typecode_t *
     9:   (int * string) list *     (* variables for '?' terms *)
    10:   int list *                (* variables for 'any' terms *)
    11:   (int * string) list *     (* variables for 'as' terms *)
    12:   (int * typecode_t) list   (* variables for as terms *)
    13: 
End ocaml section to src/flx_tpat.mli[1]
Start ocaml section to src/flx_tpat.ml[1 /1 ]
     1: # 17 "./lpsrc/flx_tpat.ipk"
     2: open Flx_ast
     3: open List
     4: open Flx_mtypes2
     5: 
     6: let type_of_tpattern syms p :
     7:   typecode_t *
     8:   (int * string) list *     (* variables for '?' terms *)
     9:   int list *                (* variables for 'any' terms *)
    10:   (int * string) list *     (* variables for 'as' terms *)
    11:   (int * typecode_t) list   (* assignments for as terms *)
    12: =
    13:   let sr = "unk",0,0,0,0 in
    14:   let explicit_vars = ref [] in
    15:   let any_vars = ref [] in
    16:   let as_vars = ref [] in
    17:   let eqns = ref [] in
    18:   let rec tp p =
    19:     match p with
    20:     | `TPAT_function (a,b) -> `TYP_function (tp a, tp b)
    21:     | `TPAT_tuple ps -> `TYP_tuple (map tp ps)
    22:     | `TPAT_sum ps -> `TYP_sum (map tp ps)
    23:     | `TPAT_pointer p -> `TYP_pointer (tp p)
    24:     | `TPAT_name (n,ps) -> `AST_name (sr,n,map tp ps)
    25:     | `TPAT_void -> `AST_void sr
    26: 
    27:     | `TPAT_var n ->
    28:       let j = !(syms.counter) in
    29:       incr (syms.counter);
    30:       explicit_vars := (j,n) :: !explicit_vars;
    31:       `TYP_var j
    32: 
    33:     | `TPAT_any ->
    34:       let j = !(syms.counter) in
    35:       incr (syms.counter);
    36:       any_vars := j :: !any_vars;
    37:       `TYP_var j
    38: 
    39:     | `TPAT_as (t,n) ->
    40:       let t = tp t in
    41:       let j = !(syms.counter) in
    42:       incr (syms.counter);
    43:       as_vars := (j,n) :: !as_vars;
    44:       eqns := (j,t) :: !eqns;
    45:       t
    46: 
    47:     | `TPAT_unitsum j -> `TYP_unitsum j
    48:     | `TPAT_type_tuple ts -> `TYP_type_tuple (map tp ts)
    49:   in
    50:     let t = tp p in
    51:     t,!explicit_vars, !any_vars, !as_vars, !eqns
    52: 
    53: 
End ocaml section to src/flx_tpat.ml[1]