/[mojave]/metaprl/theories/tactic/mptop.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/mptop.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2502 by nogin, Tue Oct 13 09:01:06 1998 UTC revision 2525 by jyh, Mon Dec 28 21:07:52 1998 UTC
# Line 11  Line 11 
11   * OCaml, and more information about this system.   * OCaml, and more information about this system.
12   *   *
13   * Copyright (C) 1998 Jason Hickey, Cornell University   * Copyright (C) 1998 Jason Hickey, Cornell University
14   *   *
15   * This program is free software; you can redistribute it and/or   * This program is free software; you can redistribute it and/or
16   * modify it under the terms of the GNU General Public License   * modify it under the terms of the GNU General Public License
17   * as published by the Free Software Foundation; either version 2   * as published by the Free Software Foundation; either version 2
18   * of the License, or (at your option) any later version.   * of the License, or (at your option) any later version.
19   *   *
20   * This program is distributed in the hope that it will be useful,   * This program is distributed in the hope that it will be useful,
21   * but WITHOUT ANY WARRANTY; without even the implied warranty of   * but WITHOUT ANY WARRANTY; without even the implied warranty of
22   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
23   * GNU General Public License for more details.   * GNU General Public License for more details.
24   *   *
25   * You should have received a copy of the GNU General Public License   * You should have received a copy of the GNU General Public License
26   * along with this program; if not, write to the Free Software   * along with this program; if not, write to the Free Software
27   * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.   * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
28   *   *
29   * Author: Jason Hickey   * Author: Jason Hickey
30   * jyh@cs.cornell.edu   * jyh@cs.cornell.edu
31   *)   *)
# Line 466  Line 466 
466         | (<:expr< ( $e$ : $t$ ) >>) ->         | (<:expr< ( $e$ : $t$ ) >>) ->
467              mk_expr base e              mk_expr base e
468         | (<:expr< $uid:s$ >>) ->         | (<:expr< $uid:s$ >>) ->
469              if s = "()" then              mk_var_expr base loc s
                UnitExpr ()  
             else  
                not_supported loc "expr uid"  
470         | (<:expr< while $e$ do $list:el$ done >>) ->         | (<:expr< while $e$ do $list:el$ done >>) ->
471              not_supported loc "while"              not_supported loc "while"
472         | MLast.ExAnt (_, e) ->         | MLast.ExAnt (_, e) ->
# Line 652  Line 649 
649  let int_int_fun_int_expr f =  let int_int_fun_int_expr f =
650     IntFunExpr (fun i -> IntFunExpr (fun j -> IntExpr (f i j)))     IntFunExpr (fun i -> IntFunExpr (fun j -> IntExpr (f i j)))
651    
652    let cons_expr =
653       FunExpr (fun e1 ->
654             FunExpr (fun e2 ->
655                   match e2 with
656                      ListExpr e2 ->
657                         ListExpr (e1 :: e2)
658                    | _ ->
659                         raise (RefineError ("cons_expr", StringError "type mismatch"))))
660    
661  let values =  let values =
662     ["+",                int_int_fun_int_expr ( + );     ["+",                int_int_fun_int_expr ( + );
663      "-",                int_int_fun_int_expr ( - );      "-",                int_int_fun_int_expr ( - );
664      "*",                int_int_fun_int_expr ( * );      "*",                int_int_fun_int_expr ( * );
665      "/",                int_int_fun_int_expr ( / )]      "/",                int_int_fun_int_expr ( / );
666        "::",               cons_expr;
667        "()",               UnitExpr ();
668        "[]",               ListExpr [];
669        "true",             BoolExpr true;
670        "false",            BoolExpr false]
671    
672    
673  let rec add_resources base = function  let rec add_resources base = function
674     (name, expr) :: tl ->     (name, expr) :: tl ->

Legend:
Removed from v.2502  
changed lines
  Added in v.2525

  ViewVC Help
Powered by ViewVC 1.1.26